Session Core_SC_DOM

Theory Hiding_Type_Variables

(***********************************************************************************
 * Copyright (c) 2018 Achim D. Brucker
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 * Repository:   https://git.logicalhacking.com/adbrucker/isabelle-hacks/
 * Dependencies: None (assert.thy is used for testing the theory but it is 
 *                     not required for providing the functionality of this hack)
 ***********************************************************************************)

(* 
   This file is based on commit 8a5e95421521c36ab71ab2711435a9bc0fa2c5cc from upstream 
   (https://git.logicalhacking.com/adbrucker/isabelle-hacks/). Merely the dependency to 
   Assert.thy has been removed by disabling the example section (which include assert 
   checks).
*)

section‹Hiding Type Variables›
text‹  This theory\footnote{This theory can be used ``stand-alone,'' i.e., this theory is 
  not specific to the DOM formalization. The latest version is part of the ``Isabelle Hacks''
  repository: \url{https://git.logicalhacking.com/adbrucker/isabelle-hacks/}.} implements 
  a mechanism for declaring default type variables for data types. This comes handy for complex 
  data types with many type variables.›
theory
  "Hiding_Type_Variables"
imports 
  Main
keywords
    "register_default_tvars"
    "update_default_tvars_mode"::thy_decl
begin
(*<*)
section‹Implementation›
subsection‹Theory Managed Data Structure›
MLsignature HIDE_TVAR = sig
  datatype print_mode = print_all | print | noprint
  datatype tvar_subst = right | left
  datatype parse_mode = parse | noparse 
  type hide_varT     = {
                         name: string,
                         tvars:  typ list,
                         typ_syn_tab : (string * typ list*string) Symtab.table, 
                         print_mode: print_mode,
                         parse_mode: parse_mode
                       } 
  val parse_print_mode : string -> print_mode
  val parse_parse_mode : string -> parse_mode
  val register    : string -> print_mode option -> parse_mode option -> 
                    theory -> theory
  val update_mode : string -> print_mode option -> parse_mode option ->
                    theory -> theory
  val lookup      : theory -> string -> hide_varT option
  val hide_tvar_tr' : string -> Proof.context -> term list -> term 
  val hide_tvar_ast_tr : Proof.context -> Ast.ast list -> Ast.ast
  val hide_tvar_subst_ast_tr : tvar_subst -> Proof.context -> Ast.ast list 
                               -> Ast.ast
  val hide_tvar_subst_return_ast_tr : tvar_subst -> Proof.context 
                               -> Ast.ast list -> Ast.ast
end

structure Hide_Tvar : HIDE_TVAR = struct
  datatype print_mode = print_all | print | noprint
  datatype tvar_subst = right | left
  datatype parse_mode = parse | noparse 
  type hide_varT     = {
                         name: string,
                         tvars:  typ list,
                         typ_syn_tab : (string * typ list*string) Symtab.table, 
                         print_mode: print_mode,
                         parse_mode: parse_mode
                       } 
  type hide_tvar_tab = (hide_varT) Symtab.table
  fun hide_tvar_eq (a, a') = (#name a) = (#name a')
  fun merge_tvar_tab (tab,tab') = Symtab.merge hide_tvar_eq (tab,tab')

  structure Data = Generic_Data
  (
    type T = hide_tvar_tab
    val empty  = Symtab.empty:hide_tvar_tab
    val extend = I
    fun merge(t1,t2)  = merge_tvar_tab (t1, t2)
  );


  fun parse_print_mode "print_all" = print_all
    | parse_print_mode "print"     = print
    | parse_print_mode "noprint"   = noprint
    | parse_print_mode s           = error("Print mode not supported: "^s)
 
  fun parse_parse_mode "parse"     = parse
    | parse_parse_mode "noparse"   = noparse
    | parse_parse_mode s           = error("Parse mode not supported: "^s)

  fun update_mode typ_str print_mode parse_mode thy   =
    let       
      val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
      val typ   = Syntax.parse_typ ctx typ_str (* no type checking *)
      val name = case typ of 
                   Type(name,_) => name
                 | _ => error("Complex type not (yet) supported.")
      fun update tab =
          let 
            val old_entry = (case Symtab.lookup tab name of 
                               SOME t => t 
                             | NONE   => error ("Type shorthand not registered: "^name))
            val print_m = case print_mode of
                            SOME m => m
                          | NONE   => #print_mode old_entry
            val parse_m = case parse_mode of 
                            SOME m => m
                          | NONE   => #parse_mode old_entry
            val entry = {
                          name        = name,
                          tvars       = #tvars old_entry,
                          typ_syn_tab = #typ_syn_tab old_entry,
                          print_mode  = print_m,
                          parse_mode  = parse_m
                        }
          in 
            Symtab.update (name,entry) tab
          end
    in  
     Context.theory_of ( (Data.map update) (Context.Theory thy))
    end

  fun lookup thy name =
    let
      val tab = (Data.get o Context.Theory) thy
    in 
      Symtab.lookup tab name
    end

  fun obtain_normalized_vname lookup_table vname = 
                           case List.find (fn e => fst e = vname) lookup_table of
                                SOME (_,idx) => (lookup_table, Int.toString idx)
                              | NONE => let 
                                          fun max_idx [] = 0  
                                            | max_idx ((_,idx)::lt) = Int.max(idx,max_idx lt)
  
                                          val idx = (max_idx lookup_table ) + 1
                                        in
                                          ((vname,idx)::lookup_table, Int.toString idx) end
  
  fun normalize_typvar_type lt (Type (a, Ts)) =
             let 
               fun switch (a,b) = (b,a)
               val (Ts', lt') = fold_map (fn t => fn lt => switch (normalize_typvar_type lt t)) Ts lt
             in 
               (lt', Type (a, Ts'))
             end
        | normalize_typvar_type lt (TFree (vname, S)) = 
             let 
               val (lt, vname) = obtain_normalized_vname lt (vname)
             in 
               (lt, TFree( vname, S))
             end
        | normalize_typvar_type lt (TVar (xi, S)) = 
             let 
               val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
             in 
               (lt, TFree( vname, S))
             end

  fun normalize_typvar_type' t = snd ( normalize_typvar_type [] t)

  fun mk_p s = s (* "("^s^")" *)

  fun key_of_type (Type(a, TS))      = mk_p (a^String.concat(map key_of_type TS))
    | key_of_type (TFree (vname, _)) = mk_p vname
    | key_of_type (TVar (xi, _ ))    = mk_p (Term.string_of_vname xi)
  val key_of_type' = key_of_type o normalize_typvar_type'


  fun normalize_typvar_term lt (Const (a, t)) = (lt, Const(a, t))
    | normalize_typvar_term lt (Free (a, t))  =  let  
                                 val (lt, vname) = obtain_normalized_vname lt a
                               in
                                 (lt, Free(vname,t))
                               end
    | normalize_typvar_term lt (Var (xi, t))   =
                               let  
                                 val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
                               in
                                 (lt, Free(vname,t))
                               end
    | normalize_typvar_term lt (Bound (i))    = (lt, Bound(i))  
    | normalize_typvar_term lt (Abs(s,ty,tr)) = 
                                let 
                                  val (lt,tr) = normalize_typvar_term lt tr
                                in
                                  (lt, Abs(s,ty,tr))
                                end
    | normalize_typvar_term lt (t1$t2) =
                                let 
                                  val (lt,t1) = normalize_typvar_term lt t1
                                  val (lt,t2) = normalize_typvar_term lt t2
                                in
                                  (lt, t1$t2)
                                end


  fun normalize_typvar_term' t = snd(normalize_typvar_term [] t) 

  fun key_of_term (Const(s,_)) = if String.isPrefix "type" s
                                 then Lexicon.unmark_type s
                                 else ""
    | key_of_term (Free(s,_))  = s
    | key_of_term (Var(xi,_))  = Term.string_of_vname xi 
    | key_of_term (Bound(_))   = error("Bound() not supported in key_of_term")
    | key_of_term (Abs(_,_,_)) = error("Abs() not supported in key_of_term")
    | key_of_term (t1$t2)      = (key_of_term t1)^(key_of_term t2)

  val key_of_term' = key_of_term o normalize_typvar_term'
  

  fun hide_tvar_tr' tname ctx terms =
      let

        val mtyp   = Syntax.parse_typ ctx tname (* no type checking *) 

        val (fq_name, _) = case mtyp of
                     Type(s,ts) => (s,ts)
                    | _        => error("Complex type not (yet) supported.") 

        val local_name_of = hd o rev o String.fields (fn c => c = #".")

        fun hide_type tname = Syntax.const("(_) "^tname) 
 
        val reg_type_as_term = Term.list_comb(Const(Lexicon.mark_type tname,dummyT),terms)
        val key = key_of_term' reg_type_as_term
        val actual_tvars_key = key_of_term reg_type_as_term

      in
        case lookup (Proof_Context.theory_of ctx) fq_name of 
          NONE   => raise Match
        | SOME e => let
                      val (tname,default_tvars_key) = 
                              case Symtab.lookup (#typ_syn_tab e) key  of
                                  NONE       => (local_name_of tname, "")
                                | SOME (s,_,tv) => (local_name_of s,tv)
                    in 
                    case (#print_mode e) of
                      print_all  => hide_type tname
                    | print      => if default_tvars_key=actual_tvars_key
                                    then hide_type tname
                                    else raise Match
                    | noprint    => raise Match
                   end  
      end
  
  fun hide_tvar_ast_tr ctx ast= 
      let 
        val thy = Proof_Context.theory_of ctx

        fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
          | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[]) 
                                      = (const,SOME sort)  
          |  parse_ast _ = error("AST type not supported.") 

        val (decorated_name, decorated_sort) = parse_ast ast 

        val name = Lexicon.unmark_type decorated_name
        val default_info = case lookup thy name of 
                              NONE   => error("No default type vars registered: "^name)
                            | SOME e => e
        val _ = if #parse_mode default_info = noparse 
                then error("Default type vars disabled (option noparse): "^name)
                else ()
        fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n 
                                | _ => error("Unsupported type structure.")
        val type_vars_ast = 
            let fun mk_tvar n = 
               case decorated_sort of 
                  NONE      => Ast.Variable(name_of_tvar n)
                | SOME sort =>  Ast.Appl([Ast.Constant("_ofsort"),
                                               Ast.Variable(name_of_tvar n),
                                                   Ast.Constant(sort)])
            in
              map mk_tvar (#tvars default_info)
            end
      in
        Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
      end   

  fun register typ_str print_mode parse_mode thy   =
    let   
      val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
      val typ   = Syntax.parse_typ ctx typ_str
      val (name,tvars) = case typ  of Type(name,tvars) => (name,tvars)
                             | _             => error("Unsupported type structure.")
      
      val base_typ   = Syntax.read_typ ctx typ_str
      val (base_name,base_tvars) = case base_typ  of Type(name,tvars) => (name,tvars)
                             | _             => error("Unsupported type structure.")

      val base_key = key_of_type' base_typ
      val base_tvar_key = key_of_type base_typ

      val print_m = case print_mode of 
                      SOME m => m
                    | NONE   => print_all
      val parse_m = case parse_mode of 
                      SOME m => m
                    | NONE   => parse
      val entry = {
                    name       = name,
                    tvars        = tvars,
                    typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
                    print_mode = print_m,
                    parse_mode = parse_m
                  }

      val base_entry = if name = base_name 
                       then 
                         {
                           name       = "",
                           tvars        = [],
                           typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
                           print_mode = noprint,
                           parse_mode = noparse
                         }
                       else case lookup thy base_name of 
                            SOME e => e
                          | NONE   => error ("No entry found for "^base_name^
                                             " (via "^name^")")

      val base_entry = {
                    name       = #name base_entry,
                    tvars        = #tvars base_entry,
                    typ_syn_tab = Symtab.update (base_key, (name, base_tvars, base_tvar_key))
                                                (#typ_syn_tab (base_entry)), 
                    print_mode = #print_mode base_entry,
                    parse_mode = #parse_mode base_entry
                  }

      fun reg tab = let 
                      val tab = Symtab.update_new(name, entry) tab
                      val tab = if name = base_name 
                                then tab 
                                else Symtab.update(base_name, base_entry) tab
                    in
                      tab
                    end

      val thy =   Sign.print_translation
                      [(Lexicon.mark_type name, hide_tvar_tr' name)] thy

    in  
     Context.theory_of ( (Data.map reg) (Context.Theory thy))
     handle Symtab.DUP _ => error("Type shorthand already registered: "^name)
    end

  fun  hide_tvar_subst_ast_tr hole ctx (ast::[]) =
      let 

        val thy = Proof_Context.theory_of ctx
        val (decorated_name, args) = case ast
               of (Ast.Appl ((Ast.Constant s)::args)) => (s, args)
                | _ =>  error "Error in obtaining type constructor."

        val name = Lexicon.unmark_type decorated_name
        val default_info = case lookup thy name of
                              NONE   => error("No default type vars registered: "^name)
                            | SOME e => e
        val _ = if #parse_mode default_info = noparse 
                then error("Default type vars disabled (option noparse): "^name)
                else ()
        fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n 
                                | _ => error("Unsupported type structure.")
        val type_vars_ast = map (fn n => Ast.Variable(name_of_tvar n)) (#tvars default_info)
        val type_vars_ast =  case hole of 
                right => (List.rev(List.drop(List.rev type_vars_ast, List.length args)))@args
              | left  => args@List.drop(type_vars_ast, List.length args)
      in
        Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
      end   
    | hide_tvar_subst_ast_tr _ _ _ = error("hide_tvar_subst_ast_tr: empty AST.")

  fun hide_tvar_subst_return_ast_tr hole ctx (retval::constructor::[]) = 
         hide_tvar_subst_ast_tr hole ctx [Ast.Appl (constructor::retval::[])]
    | hide_tvar_subst_return_ast_tr _ _ _ = 
           error("hide_tvar_subst_return_ast_tr: error in parsing AST")


end



subsection‹Register Parse Translations›
syntax "_tvars_wildcard" :: "type  type" ("'('_') _") 
syntax "_tvars_wildcard_retval" :: "type  type  type" ("'('_, _') _")
syntax "_tvars_wildcard_sort" :: "sort  type  type" ("'('_::_') _")
syntax "_tvars_wildcard_right" :: "type  type" ("_ '_..")
syntax "_tvars_wildcard_left" :: "type  type" ("_ ..'_")

parse_ast_translation[
    (@{syntax_const "_tvars_wildcard_sort"}, Hide_Tvar.hide_tvar_ast_tr),
    (@{syntax_const "_tvars_wildcard"}, Hide_Tvar.hide_tvar_ast_tr),
    (@{syntax_const "_tvars_wildcard_retval"}, Hide_Tvar.hide_tvar_subst_return_ast_tr Hide_Tvar.right),
    (@{syntax_const "_tvars_wildcard_right"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.right),
    (@{syntax_const "_tvars_wildcard_left"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.left)
  ]

subsection‹Register Top-Level Isar Commands›
MLval modeP = (Parse.$$$ "("
       |-- (Parse.name --| Parse.$$$ ","
         -- Parse.name --| 
            Parse.$$$ ")"))
  val typ_modeP = Parse.typ -- (Scan.optional modeP ("print_all","parse"))

  val _ = Outer_Syntax.command @{command_keyword "register_default_tvars"}
          "Register default variables (and hiding mechanims) for a type."
          (typ_modeP >> (fn (typ,(print_m,parse_m)) => 
                  (Toplevel.theory 
                     (Hide_Tvar.register typ 
                                (SOME (Hide_Tvar.parse_print_mode print_m)) 
                                (SOME (Hide_Tvar.parse_parse_mode parse_m)))))); 

  val _ = Outer_Syntax.command @{command_keyword "update_default_tvars_mode"}
          "Update print and/or parse mode or the default type variables for a certain type."
          (typ_modeP >> (fn (typ,(print_m,parse_m)) => 
                  (Toplevel.theory 
                     (Hide_Tvar.update_mode typ 
                                (SOME (Hide_Tvar.parse_print_mode print_m)) 
                                (SOME (Hide_Tvar.parse_parse_mode parse_m))))));
(*
section‹Examples›
subsection‹Print Translation›
datatype ('a, 'b) hide_tvar_foobar = hide_tvar_foo 'a | hide_tvar_bar 'b 
type_synonym ('a, 'b, 'c, 'd) hide_tvar_baz = "('a+'b, 'a × 'b) hide_tvar_foobar"

definition hide_tvar_f::"('a, 'b) hide_tvar_foobar ⇒ ('a, 'b) hide_tvar_foobar ⇒ ('a, 'b) hide_tvar_foobar" 
     where "hide_tvar_f a b = a"
definition hide_tvar_g::"('a, 'b, 'c, 'd) hide_tvar_baz ⇒ ('a, 'b, 'c, 'd) hide_tvar_baz ⇒ ('a, 'b, 'c, 'd) hide_tvar_baz" 
     where "hide_tvar_g a b = a"

assert[string_of_thm_equal,
       thm_def="hide_tvar_f_def", 
       str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
       thm_def="hide_tvar_g_def", 
       str="hide_tvar_g (a::('a + 'b, 'a × 'b) hide_tvar_foobar) (b::('a + 'b, 'a × 'b) hide_tvar_foobar) = a"]

register_default_tvars  "('alpha, 'beta) hide_tvar_foobar" (print_all,parse)
register_default_tvars  "('alpha, 'beta, 'gamma, 'delta) hide_tvar_baz" (print_all,parse)

update_default_tvars_mode "_ hide_tvar_foobar" (noprint,noparse)
assert[string_of_thm_equal,
       thm_def="hide_tvar_f_def",
       str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
       thm_def="hide_tvar_g_def", 
       str="hide_tvar_g (a::('a + 'b, 'a × 'b) hide_tvar_foobar) (b::('a + 'b, 'a × 'b) hide_tvar_foobar) = a"]

update_default_tvars_mode "_ hide_tvar_foobar" (print_all,noparse)

assert[string_of_thm_equal,
       thm_def="hide_tvar_f_def", str="hide_tvar_f (a::(_) hide_tvar_foobar) (b::(_) hide_tvar_foobar) = a"]
assert[string_of_thm_equal,
       thm_def="hide_tvar_g_def", str="hide_tvar_g (a::(_) hide_tvar_baz) (b::(_) hide_tvar_baz) = a"]

subsection‹Parse Translation›
update_default_tvars_mode "_ hide_tvar_foobar" (print_all,parse)

declare [[show_types]]
definition hide_tvar_A :: "'x ⇒ (('x::linorder) hide_tvar_foobar) .._"
  where "hide_tvar_A x = hide_tvar_foo x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_A_def", str="hide_tvar_A (x::'x) = hide_tvar_foo x"]

definition hide_tvar_A' :: "'x ⇒ (('x,'b) hide_tvar_foobar) .._"
  where "hide_tvar_A' x = hide_tvar_foo x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]

definition hide_tvar_B' :: "(_) hide_tvar_foobar ⇒ (_) hide_tvar_foobar ⇒ (_) hide_tvar_foobar" 
  where "hide_tvar_B' x y = x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]


definition hide_tvar_B :: "(_) hide_tvar_foobar ⇒ (_) hide_tvar_foobar ⇒ (_) hide_tvar_foobar" 
  where "hide_tvar_B x y = x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_B_def", str="hide_tvar_B (x::(_) hide_tvar_foobar) (y::(_) hide_tvar_foobar) = x"]

definition hide_tvar_C :: "(_) hide_tvar_baz ⇒ (_) hide_tvar_foobar ⇒ (_) hide_tvar_baz" 
  where "hide_tvar_C x y = x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]

definition hide_tvar_E :: "(_::linorder) hide_tvar_baz ⇒ (_::linorder) hide_tvar_foobar ⇒ (_::linorder) hide_tvar_baz" 
  where "hide_tvar_E x y = x"
assert[string_of_thm_equal,
       thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]

definition hide_tvar_X :: "(_, 'retval::linorder) hide_tvar_baz 
                 ⇒ (_,'retval) hide_tvar_foobar 
                 ⇒ (_,'retval) hide_tvar_baz"
  where "hide_tvar_X x y = x"
*)
(*>*)

subsection‹Introduction›
text‹
  When modelling object-oriented data models in HOL with the goal of preserving ‹extensibility› 
  (e.g., as described in~\cite{brucker.ea:extensible:2008-b,brucker:interactive:2007}) one needs 
  to define type constructors with a large number of type variables. This can reduce the readability
  of the overall formalization. Thus, we use a short-hand notation in cases were the names of 
  the type variables are known from the context. In more detail, this theory  sets up both 
  configurable print and parse translations that allows for replacing @{emph ‹all›} type variables 
  by (_)›, e.g., a five-ary constructor ('a, 'b, 'c, 'd, 'e) hide_tvar_foo› can 
  be shorted to (_) hide_tvar_foo›. The use of this shorthand in output (printing) and 
  input (parsing) is, on a per-type basis, user-configurable using the top-level commands 
  register_default_tvars› (for registering the names of the default type variables and 
  the print/parse mode) and update_default_tvars_mode› (for changing the print/parse mode 
  dynamically).  

  The input also supports short-hands for declaring default sorts (e.g., (_::linorder)› 
  specifies that all default variables need to be instances of the sort (type class) 
  @{class ‹linorder›} and short-hands of overriding a suffice (or prefix) of the default type 
  variables. For example, ('state) hide_tvar_foo _.› is a short-hand for 
  ('a, 'b, 'c, 'd, 'state) hide_tvar_foo›. In this document, we omit the implementation 
  details (we refer the interested reader to theory file)  and continue directly with a few 
  examples. 
›

subsection‹Example›
text‹Given the following type definition:›
datatype ('a, 'b) hide_tvar_foobar = hide_tvar_foo 'a | hide_tvar_bar 'b 
type_synonym ('a, 'b, 'c, 'd) hide_tvar_baz = "('a+'b, 'a × 'b) hide_tvar_foobar"
text‹We can register default values for the type variables for the abstract
data type as well as the type synonym:› 
register_default_tvars  "('alpha, 'beta) hide_tvar_foobar" (print_all,parse)
register_default_tvars  "('alpha, 'beta, 'gamma, 'delta) hide_tvar_baz" (print_all,parse)
text‹This allows us to write›
definition hide_tvar_f::"(_) hide_tvar_foobar  (_) hide_tvar_foobar  (_) hide_tvar_foobar" 
     where "hide_tvar_f a b = a"
definition hide_tvar_g::"(_) hide_tvar_baz  (_) hide_tvar_baz  (_) hide_tvar_baz" 
  where "hide_tvar_g a b = a"

text‹Instead of specifying the type variables explicitely. This makes, in particular
for type constructors with a large number of type variables, definitions much 
more concise. This syntax is also used in the output of antiquotations, e.g., 
@{term[show_types] "x = hide_tvar_g"}. Both the print translation and the parse 
translation can be disabled for each type individually:›

update_default_tvars_mode "_ hide_tvar_foobar" (noprint,noparse)
update_default_tvars_mode "_ hide_tvar_foobar" (noprint,noparse)

text‹ Now, Isabelle's interactive output and the antiquotations will show 
all type variables, e.g., @{term[show_types] "x = hide_tvar_g"}.›



end

Theory Ref

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹References›
text‹
  This theory, we introduce a generic reference. All our typed pointers include such 
  a reference, which allows us to distinguish pointers of the same type, but also to 
  iterate over all pointers in a set.›
theory 
  Ref
  imports
    "HOL-Library.Adhoc_Overloading"
    "../preliminaries/Hiding_Type_Variables"
begin

instantiation sum :: (linorder, linorder) linorder
begin
definition less_eq_sum :: "'a + 'b  'a + 'b  bool"
  where
    "less_eq_sum t t' = (case t of
      Inl l  (case t' of
        Inl l'  l  l'
      | Inr r'  True)
    | Inr r  (case t' of
        Inl l'  False
      | Inr r'  r  r'))"
definition less_sum :: "'a + 'b  'a + 'b  bool"
  where
    "less_sum t t'  t  t'  ¬ t'  t"
instance by(standard) (auto simp add: less_eq_sum_def less_sum_def split: sum.splits)
end

type_synonym ref = nat
consts cast :: 'a

end

Theory Core_DOM_Basic_Datatypes

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 *******************************************************************************\***)

section‹Basic Data Types›
text‹
  \label{sec:Core_DOM_Basic_Datatypes}
  This theory formalizes the primitive data types used by the DOM standard~\cite{dom-specification}.
› 
theory Core_DOM_Basic_Datatypes
  imports
    Main
begin

type_synonym USVString = string
text‹
  In the official standard, the type @{type "USVString"} corresponds to the set of all possible   
  sequences of Unicode scalar values. As we are not interested in analyzing the specifics of Unicode
  strings, we just model @{type "USVString"} using the standard type @{type "string"} of Isabelle/HOL.
› 

type_synonym DOMString = string
text‹
  In the official standard, the type @{type "DOMString"} corresponds to the set of all possible 
  sequences of code units, commonly interpreted as UTF-16 encoded strings. Again, as we are not 
  interested in analyzing the specifics of Unicode strings, we just model @{type "DOMString"} using 
  the standard type @{type "string"} of Isabelle/HOL.
›

type_synonym doctype = DOMString

paragraph‹Examples›
definition html :: doctype
  where "html = ''<!DOCTYPE html>''"

hide_const id

text ‹This dummy locale is used to create scoped definitions by using global interpretations
  and defines.›
locale l_dummy
end

Theory BaseClass

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹The Class Infrastructure›
text‹In this theory, we introduce the basic infrastructure for our encoding 
of classes.›
theory BaseClass
  imports
    "HOL-Library.Finite_Map"
    "../pointers/Ref"
    "../Core_DOM_Basic_Datatypes" 
begin

named_theorems instances

consts get :: 'a
consts put :: 'a
consts delete :: 'a

text ‹Overall, the definition of the class types follows closely the one of the pointer 
  types. Instead of datatypes, we use records for our classes. This allows us to, first, 
  make use of record inheritance, which is, in addition to the type synonyms of
  previous class types, the second place where the inheritance relationship of 
  our types manifest. Second, we get a convenient notation to define classes, in
  addition to automatically generated getter and setter functions.›

text ‹Along with our class types, we also develop our heap type, which is a finite 
  map at its core. It is important to note that while the map stores a mapping 
  from @{term "object_ptr"} to @{term "Object"}, we restrict the type variables 
  of the record extension slot of @{term "Object"} in such a way that allows 
  down-casting, but requires a bit of taking-apart and re-assembling of our records 
  before they are stored in the heap.›

text ‹Throughout the theory files, we will use underscore case to reference pointer 
      types, and camel case for class types.›

text ‹Every class type contains at least one attribute; nothing. This is used for 
  two purposes: first, the record package does not allow records without any 
  attributes. Second, we will use the getter of nothing later to check whether a 
  class of the correct type could be retrieved, for which we will be able to use
  our infrastructure regarding the behaviour of getters across different heaps.›


locale l_type_wf = fixes type_wf :: "'heap  bool"

locale l_known_ptr = fixes known_ptr :: "'ptr  bool"

end

Theory Heap_Error_Monad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹The Heap Error Monad›
text ‹In this theory, we define a heap and error monad for modeling exceptions. 
This allows us to define composite methods similar to stateful programming in Haskell, 
but also to stay close to the official DOM specification.›
theory 
  Heap_Error_Monad
  imports
    Hiding_Type_Variables
    "HOL-Library.Monad_Syntax"
begin

subsection ‹The Program Data Type›

datatype ('heap, 'e, 'result) prog = Prog (the_prog: "'heap  'e + 'result × 'heap")
register_default_tvars "('heap, 'e, 'result) prog" (print, parse)

subsection ‹Basic Functions›

definition 
  bind :: "(_, 'result) prog  ('result  (_, 'result2) prog)  (_, 'result2) prog"
  where
    "bind f g = Prog (λh. (case (the_prog f) h of Inr (x, h')  (the_prog (g x)) h' 
                                                | Inl exception  Inl exception))"

adhoc_overloading Monad_Syntax.bind bind

definition 
  execute :: "'heap  ('heap, 'e, 'result) prog  ('e + 'result × 'heap)" 
  ("((_)/  (_))" [51, 52] 55)
  where
    "execute h p = (the_prog p) h"

definition 
  returns_result :: "'heap  ('heap, 'e, 'result) prog  'result  bool" 
  ("((_)/  (_)/ r (_))" [60, 35, 61] 65)
  where
    "returns_result h p r  (case h  p of Inr (r', _)  r = r' | Inl _  False)"

fun select_result ("|(_)|r")
  where
    "select_result (Inr (r, _)) = r"
  | "select_result (Inl _) = undefined"

lemma returns_result_eq [elim]: "h  f r y  h  f r y'  y = y'"
  by(auto simp add: returns_result_def split: sum.splits)

definition 
  returns_heap :: "'heap  ('heap, 'e, 'result) prog  'heap  bool" 
  ("((_)/  (_)/ h (_))" [60, 35, 61] 65)
  where
    "returns_heap h p h'  (case h  p of Inr (_ , h'')  h' = h'' | Inl _  False)"

fun select_heap ("|(_)|h")
  where
    "select_heap (Inr ( _, h)) = h"
  | "select_heap (Inl _) = undefined"

lemma returns_heap_eq [elim]: "h  f h h'  h  f h h''  h' = h''"
  by(auto simp add: returns_heap_def split: sum.splits)

definition 
  returns_result_heap :: "'heap  ('heap, 'e, 'result) prog  'result  'heap  bool" 
  ("((_)/  (_)/ r (_) h (_))" [60, 35, 61, 62] 65)
  where
    "returns_result_heap h p r h'  h  p r r  h  p h h'"

lemma return_result_heap_code [code]:
  "returns_result_heap h p r h'  (case h  p of Inr (r', h'')  r = r'  h' = h'' | Inl _  False)"
  by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)

fun select_result_heap ("|(_)|rh")
  where
    "select_result_heap (Inr (r, h)) = (r, h)"
  | "select_result_heap (Inl _) = undefined"

definition 
  returns_error :: "'heap  ('heap, 'e, 'result) prog  'e  bool" 
  ("((_)/  (_)/ e (_))" [60, 35, 61] 65)
  where
    "returns_error h p e = (case h  p of Inr _  False | Inl e'  e = e')"

definition is_OK :: "'heap  ('heap, 'e, 'result) prog  bool" ("((_)/  ok (_))" [75, 75])
  where
    "is_OK h p = (case h  p of Inr _  True | Inl _  False)"

lemma is_OK_returns_result_I [intro]: "h  f r y  h  ok f"
  by(auto simp add: is_OK_def returns_result_def split: sum.splits)

lemma is_OK_returns_result_E [elim]:
  assumes "h  ok f"
  obtains x where "h  f r x"
  using assms by(auto simp add: is_OK_def returns_result_def split: sum.splits)

lemma is_OK_returns_heap_I [intro]: "h  f h h'  h  ok f"
  by(auto simp add: is_OK_def returns_heap_def split: sum.splits)

lemma is_OK_returns_heap_E [elim]:
  assumes "h  ok f"
  obtains h' where "h  f h h'"
  using assms by(auto simp add: is_OK_def returns_heap_def split: sum.splits)

lemma select_result_I:
  assumes "h  ok f"
    and "x. h  f r x  P x"
  shows "P |h  f|r"
  using assms
  by(auto simp add: is_OK_def returns_result_def split: sum.splits)

lemma select_result_I2 [simp]:
  assumes "h  f r x"
  shows "|h  f|r = x"
  using assms
  by(auto simp add: is_OK_def returns_result_def split: sum.splits)

lemma returns_result_select_result [simp]:
  assumes "h  ok f"
  shows "h  f r |h  f|r"
  using assms
  by (simp add: select_result_I)

lemma select_result_E:
  assumes "P |h  f|r" and "h  ok f" 
  obtains x where "h  f r x" and "P x"
  using assms
  by(auto simp add: is_OK_def returns_result_def split: sum.splits)

lemma select_result_eq: "(x .h  f r x = h'  f r x)  |h  f|r = |h'  f|r"
  by (metis (no_types, lifting) is_OK_def old.sum.simps(6) select_result.elims 
      select_result_I select_result_I2)

definition error :: "'e  ('heap, 'e, 'result) prog"
  where
    "error exception = Prog (λh. Inl exception)"

lemma error_bind [iff]: "(error e  g) = error e"
  unfolding error_def bind_def by auto

lemma error_returns_result [simp]: "¬ (h  error e r y)"
  unfolding returns_result_def error_def execute_def by auto

lemma error_returns_heap [simp]: "¬ (h  error e h h')"
  unfolding returns_heap_def error_def execute_def by auto

lemma error_returns_error [simp]: "h  error e e e"
  unfolding returns_error_def error_def execute_def by auto

definition return :: "'result  ('heap, 'e, 'result) prog"
  where
    "return result = Prog (λh. Inr (result, h))"

lemma return_ok [simp]: "h  ok (return x)"
  by(simp add: return_def is_OK_def execute_def)

lemma return_bind [iff]: "(return x  g) = g x"
  unfolding return_def bind_def by auto

lemma return_id [simp]: "f  return = f"
  by (induct f) (auto simp add: return_def bind_def split: sum.splits prod.splits)

lemma return_returns_result [iff]: "(h  return x r y) = (x = y)"
  unfolding returns_result_def return_def execute_def by auto

lemma return_returns_heap [iff]: "(h  return x h h') = (h = h')"
  unfolding returns_heap_def return_def execute_def by auto

lemma return_returns_error [iff]: "¬ h  return x e e"
  unfolding returns_error_def execute_def return_def by auto

definition noop :: "('heap, 'e, unit) prog"
  where
    "noop = return ()"

lemma noop_returns_heap [simp]: "h  noop h h'  h = h'"
  by(simp add: noop_def)

definition get_heap :: "('heap, 'e, 'heap) prog"
  where
    "get_heap = Prog (λh. h  return h)"

lemma get_heap_ok [simp]: "h  ok (get_heap)"
  by (simp add: get_heap_def execute_def is_OK_def return_def)

lemma get_heap_returns_result [simp]: "(h  get_heap  (λh'. f h') r x) = (h  f h r x)"
  by(simp add: get_heap_def returns_result_def bind_def return_def execute_def)

lemma get_heap_returns_heap [simp]: "(h  get_heap  (λh'. f h') h h'') = (h  f h h h'')"
  by(simp add: get_heap_def returns_heap_def bind_def return_def execute_def)

lemma get_heap_is_OK [simp]: "(h  ok (get_heap  (λh'. f h'))) = (h  ok (f h))"
  by(auto simp add: get_heap_def is_OK_def bind_def return_def execute_def)

lemma get_heap_E [elim]: "(h  get_heap r x)  x = h"
  by(simp add: get_heap_def returns_result_def return_def execute_def)

definition return_heap :: "'heap  ('heap, 'e, unit) prog"
  where
    "return_heap h = Prog (λ_. h  return ())"

lemma return_heap_E [iff]: "(h  return_heap h' h h'') = (h'' = h')"
  by(simp add: return_heap_def returns_heap_def return_def execute_def)

lemma return_heap_returns_result [simp]: "h  return_heap h' r ()"
  by(simp add: return_heap_def execute_def returns_result_def return_def)


subsection ‹Pure Heaps›

definition pure :: "('heap, 'e, 'result) prog  'heap  bool"
  where "pure f h  h  ok f  h  f h h"

lemma return_pure [simp]: "pure (return x) h"
  by(simp add: pure_def return_def is_OK_def returns_heap_def execute_def)

lemma error_pure [simp]: "pure (error e) h"
  by(simp add: pure_def error_def is_OK_def returns_heap_def execute_def)

lemma noop_pure [simp]: "pure (noop) h"
  by (simp add: noop_def)

lemma get_pure [simp]: "pure get_heap h"
  by(simp add: pure_def get_heap_def is_OK_def returns_heap_def return_def execute_def)

lemma pure_returns_heap_eq:
  "h  f h h'  pure f h  h = h'"
  by (meson pure_def is_OK_returns_heap_I returns_heap_eq)

lemma pure_eq_iff:     
  "(h' x. h  f r x  h  f h h'  h = h')  pure f h"
  by(auto simp add: pure_def)

subsection ‹Bind›

lemma bind_assoc [simp]:
  "((bind f g)  h) = (f  (λx. (g x  h)))"
  by(auto simp add: bind_def split: sum.splits)

lemma bind_returns_result_E:
  assumes "h  f  g r y"
  obtains x h' where "h  f r x" and "h  f h h'" and "h'  g x r y"
  using assms by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)

lemma bind_returns_result_E2:
  assumes "h  f  g r y" and "pure f h"
  obtains x where "h  f r x" and "h  g x r y"
  using assms pure_returns_heap_eq bind_returns_result_E by metis

lemma bind_returns_result_E3:
  assumes "h  f  g r y" and "h  f r x" and "pure f h"
  shows "h  g x r y"
  using assms returns_result_eq bind_returns_result_E2 by metis

lemma bind_returns_result_E4:
  assumes "h  f  g r y" and "h  f r x" 
  obtains h' where "h  f h h'" and "h'  g x r y"
  using assms returns_result_eq bind_returns_result_E by metis

lemma bind_returns_heap_E:
  assumes "h  f  g h h''"
  obtains x h' where "h  f r x" and "h  f h h'" and "h'  g x h h''"
  using assms by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)

lemma bind_returns_heap_E2 [elim]:
  assumes "h  f  g h h'" and "pure f h"
  obtains x where "h  f r x" and "h  g x h h'"
  using assms pure_returns_heap_eq by (fastforce elim: bind_returns_heap_E)

lemma bind_returns_heap_E3 [elim]:
  assumes "h  f  g h h'" and "h  f r x" and "pure f h" 
  shows "h  g x h h'"
  using assms pure_returns_heap_eq returns_result_eq by (fastforce elim: bind_returns_heap_E)

lemma bind_returns_heap_E4:
  assumes "h  f  g h h''" and "h  f h h'"
  obtains x where "h  f r x" and "h'  g x h h''"
  using assms
  by (metis bind_returns_heap_E returns_heap_eq)

lemma bind_returns_error_I [intro]:
  assumes "h  f e e"
  shows "h  f  g e e"
  using assms
  by(auto simp add: returns_error_def bind_def execute_def split: sum.splits)

lemma bind_returns_error_I3:
  assumes "h  f r x" and "h  f h h'" and "h'  g x e e"
  shows "h  f  g e e"
  using assms
  by(auto simp add: returns_error_def bind_def execute_def returns_heap_def returns_result_def 
      split: sum.splits)

lemma bind_returns_error_I2 [intro]:
  assumes "pure f h" and "h  f r x" and "h  g x e e"
  shows "h  f  g e e"
  using assms
  by (meson bind_returns_error_I3 is_OK_returns_result_I pure_def)

lemma bind_is_OK_E [elim]:
  assumes "h  ok (f  g)"
  obtains x h' where "h  f r x" and "h  f h h'" and "h'  ok (g x)"
  using assms 
  by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def 
      split: sum.splits)

lemma bind_is_OK_E2:
  assumes "h  ok (f  g)" and "h  f r x"
  obtains h' where "h  f h h'" and "h'  ok (g x)"
  using assms 
  by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def 
      split: sum.splits)

lemma bind_returns_result_I [intro]:
  assumes "h  f r x" and "h  f h h'" and "h'  g x r y"
  shows "h  f  g r y"
  using assms 
  by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)

lemma bind_pure_returns_result_I [intro]:
  assumes "pure f h" and "h  f r x" and "h  g x r y"
  shows "h  f  g r y"
  using assms
  by (meson bind_returns_result_I pure_def is_OK_returns_result_I)

lemma bind_pure_returns_result_I2 [intro]:
  assumes "pure f h" and "h  ok f" and "x. h  f r x  h  g x r y"
  shows "h  f  g r y"
  using assms by auto

lemma bind_returns_heap_I [intro]:
  assumes "h  f r x" and "h  f h h'" and "h'  g x h h''"
  shows "h  f  g h h''"
  using assms 
  by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)

lemma bind_returns_heap_I2 [intro]:
  assumes "h  f h h'" and "x. h  f r x  h'  g x h h''"
  shows "h  f  g h h''"
  using assms
  by (meson bind_returns_heap_I is_OK_returns_heap_I is_OK_returns_result_E)

lemma bind_is_OK_I [intro]:
  assumes "h  f r x" and "h  f h h'" and "h'  ok (g x)"
  shows "h  ok (f  g)"
  by (meson assms(1) assms(2) assms(3) bind_returns_heap_I is_OK_returns_heap_E 
      is_OK_returns_heap_I)

lemma bind_is_OK_I2 [intro]:
  assumes "h  ok f" and "x h'. h  f r x  h  f h h'  h'  ok (g x)"
  shows "h  ok (f  g)"
  using assms by blast  

lemma bind_is_OK_pure_I [intro]:
  assumes "pure f h" and "h  ok f" and "x. h  f r x  h  ok (g x)"
  shows "h  ok (f  g)"
  using assms by blast

lemma bind_pure_I:
  assumes "pure f h" and "x. h  f r x  pure (g x) h"
  shows "pure (f  g) h"
  using assms
  by (metis bind_returns_heap_E2 pure_def pure_returns_heap_eq is_OK_returns_heap_E)

lemma pure_pure:
  assumes "h  ok f" and "pure f h"
  shows "h  f h h"
  using assms returns_heap_eq 
  unfolding pure_def
  by auto

lemma bind_returns_error_eq: 
  assumes "h  f e e"
    and "h  g e e"
  shows "h  f = h  g"
  using assms 
  by(auto simp add: returns_error_def split: sum.splits)

subsection ‹Map›

fun map_M :: "('x  ('heap, 'e, 'result) prog)  'x list  ('heap, 'e, 'result list) prog"
  where
    "map_M f [] = return []"
  | "map_M f (x#xs) = do {
      y  f x;
      ys  map_M f xs;
      return (y # ys)
    }"

lemma map_M_ok_I [intro]: 
  "(x. x  set xs  h  ok (f x))  (x. x  set xs  pure (f x) h)  h  ok (map_M f xs)"
  apply(induct xs)
  by (simp_all add: bind_is_OK_I2 bind_is_OK_pure_I)

lemma map_M_pure_I : "h. (x. x  set xs  pure (f x) h)  pure (map_M f xs) h"
  apply(induct xs)
   apply(simp)
  by(auto intro!: bind_pure_I)

lemma map_M_pure_E :
  assumes "h  map_M g xs r ys" and "x  set xs" and "x h. x  set xs  pure (g x) h"
  obtains y where "h  g x r y" and "y  set ys"
  apply(insert assms, induct xs arbitrary: ys)
   apply(simp)
  apply(auto elim!: bind_returns_result_E)[1]
  by (metis (full_types) pure_returns_heap_eq)

lemma map_M_pure_E2:
  assumes "h  map_M g xs r ys" and "y  set ys" and "x h. x  set xs  pure (g x) h"
  obtains x where "h  g x r y" and "x  set xs"
  apply(insert assms, induct xs arbitrary: ys)
   apply(simp)
  apply(auto elim!: bind_returns_result_E)[1]
  by (metis (full_types) pure_returns_heap_eq)


subsection ‹Forall›

fun forall_M :: "('y  ('heap, 'e, 'result) prog)  'y list  ('heap, 'e, unit) prog"
  where
    "forall_M P [] = return ()"
  | "forall_M P (x # xs) = do {
      P x;
      forall_M P xs
    }"
    

lemma pure_forall_M_I: "(x. x  set xs  pure (P x) h)  pure (forall_M P xs) h"
  apply(induct xs)
  by(auto intro!: bind_pure_I)
   

subsection ‹Fold›

fun fold_M :: "('result  'y  ('heap, 'e, 'result) prog)  'result  'y list
   ('heap, 'e, 'result) prog"
  where 
    "fold_M f d [] = return d" |
    "fold_M f d (x # xs) = do { y  f d x; fold_M f y xs }"

lemma fold_M_pure_I : "(d x. pure (f d x) h)  (d. pure (fold_M f d xs) h)"
  apply(induct xs)
  by(auto intro: bind_pure_I)

subsection ‹Filter›

fun filter_M :: "('x  ('heap, 'e, bool) prog)  'x list  ('heap, 'e, 'x list) prog"
  where
    "filter_M P [] = return []"
  | "filter_M P (x#xs) = do {
      p  P x;
      ys  filter_M P xs;
      return (if p then x # ys else ys)
    }"

lemma filter_M_pure_I [intro]: "(x. x  set xs  pure (P x) h)  pure (filter_M P xs)h"
  apply(induct xs) 
  by(auto intro!: bind_pure_I)

lemma filter_M_is_OK_I [intro]:
  "(x. x  set xs  h  ok (P x))  (x. x  set xs  pure (P x) h)  h  ok (filter_M P xs)"
  apply(induct xs)
   apply(simp)
  by(auto intro!: bind_is_OK_pure_I)

lemma filter_M_not_more_elements:
  assumes "h  filter_M P xs r ys" and "x. x  set xs  pure (P x) h" and "x  set ys"
  shows "x  set xs"
  apply(insert assms, induct xs arbitrary: ys)
  by(auto elim!: bind_returns_result_E2 split: if_splits intro!: set_ConsD)

lemma filter_M_in_result_if_ok:
  assumes "h  filter_M P xs r ys" and "h x. x  set xs  pure (P x) h" and "x  set xs" and
    "h  P x r True"
  shows "x  set ys"
  apply(insert assms, induct xs arbitrary: ys)
   apply(simp)
  apply(auto elim!: bind_returns_result_E2)[1]
  by (metis returns_result_eq)

lemma filter_M_holds_for_result:
  assumes "h  filter_M P xs r ys" and "x  set ys" and "x h. x  set xs  pure (P x) h"
  shows "h  P x r True"
  apply(insert assms, induct xs arbitrary: ys)
  by(auto elim!: bind_returns_result_E2 split: if_splits intro!: set_ConsD)

lemma filter_M_empty_I:
  assumes "x. pure (P x) h"
    and "x  set xs. h  P x r False"
  shows "h  filter_M P xs r []"
  using assms
  apply(induct xs)
  by(auto intro!: bind_pure_returns_result_I)

lemma filter_M_subset_2: "h  filter_M P xs r ys  h'  filter_M P xs r ys' 
                           (x. pure (P x) h)  (x. pure (P x) h') 
                           (b. x  set xs. h  P x r True  h'  P x r b  b) 
                           set ys  set ys'"
proof -
  assume 1: "h  filter_M P xs r ys" and 2: "h'  filter_M P xs r ys'" 
    and 3: "(x. pure (P x) h)" and "(x. pure (P x) h')" 
    and 4: "b. xset xs. h  P x r True  h'  P x r b  b"
  have h1: "x  set xs. h'  ok (P x)"
    using 2 3 (x. pure (P x) h')
    apply(induct xs arbitrary: ys')
    by(auto elim!: bind_returns_result_E2)
  then have 5: "xset xs. h  P x r True  h'  P x r True"
    using 4
    apply(auto)[1]
    by (metis is_OK_returns_result_E)
  show ?thesis
    using 1 2 3 5 (x. pure (P x) h')
    apply(induct xs arbitrary: ys ys')
     apply(auto)[1]
    apply(auto elim!: bind_returns_result_E2 split: if_splits)[1]
          apply auto[1]
         apply auto[1]
        apply(metis returns_result_eq)
       apply auto[1]
      apply auto[1]
     apply auto[1]
    by(auto)
qed

lemma filter_M_subset: "h  filter_M P xs r ys  set ys  set xs"
  apply(induct xs arbitrary: h ys)
   apply(auto)[1]
  apply(auto elim!: bind_returns_result_E split: if_splits)[1]
   apply blast
  by blast

lemma filter_M_distinct: "h  filter_M P xs r ys  distinct xs  distinct ys"
  apply(induct xs arbitrary: h ys)
   apply(auto)[1]
  using filter_M_subset
  apply(auto elim!: bind_returns_result_E)[1]
  by fastforce

lemma filter_M_filter: "h  filter_M P xs r ys  (x. x  set xs  pure (P x) h) 
                        (x  set xs. h  ok P x)  ys = filter (λx. |h  P x|r) xs"
  apply(induct xs arbitrary: ys)
  by(auto elim!: bind_returns_result_E2)

lemma filter_M_filter2: "(x. x  set xs  pure (P x) h   h  ok P x) 
                        filter (λx. |h  P x|r) xs = ys  h  filter_M P xs r ys"
  apply(induct xs arbitrary: ys)
  by(auto elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I)

lemma filter_ex1: "∃!x  set xs. P x  P x  x  set xs  distinct xs 
                   filter P xs = [x]"
  apply(auto)[1]
  apply(induct xs)
   apply(auto)[1]
  apply(auto)[1]
  using filter_empty_conv by fastforce

lemma filter_M_ex1:
  assumes "h  filter_M P xs r ys"
    and "x  set xs"
    and "∃!x  set xs. h  P x r True"
    and "x. x  set xs  pure (P x) h"
    and "distinct xs"
    and "h  P x r True"
  shows "ys = [x]"
proof -
  have *: "∃!x  set xs. |h  P x|r"
    apply(insert assms(1) assms(3) assms(4))
    apply(drule filter_M_filter) 
     apply(simp)
    apply(auto simp add: select_result_I2)[1]
    by (metis (full_types) is_OK_returns_result_E select_result_I2)
  then show ?thesis
    apply(insert assms(1) assms(4))
    apply(drule filter_M_filter)
     apply(auto)[1] 
    by (metis * assms(2) assms(5) assms(6) distinct_filter 
        distinct_length_2_or_more filter_empty_conv filter_set list.exhaust 
        list.set_intros(1) list.set_intros(2) member_filter select_result_I2)
qed

lemma filter_M_eq:
  assumes "x. pure (P x) h" and "x. pure (P x) h'"
    and "b x. x  set xs  h  P x r b = h'  P x r b"
  shows "h  filter_M P xs r ys  h'  filter_M P xs r ys"
  using assms
  apply (induct xs arbitrary: ys)
  by(auto elim!: bind_returns_result_E2 intro!: bind_pure_returns_result_I 
      dest: returns_result_eq)


subsection ‹Map Filter›

definition map_filter_M :: "('x  ('heap, 'e, 'y option) prog)  'x list
   ('heap, 'e, 'y list) prog"
  where
    "map_filter_M f xs = do {
      ys_opts  map_M f xs;
      ys_no_opts  filter_M (λx. return (x  None)) ys_opts;
      map_M (λx. return (the x)) ys_no_opts
    }"

lemma map_filter_M_pure: "(x h. x  set xs  pure (f x) h)  pure (map_filter_M f xs) h"
  by(auto simp add: map_filter_M_def map_M_pure_I intro!: bind_pure_I)

lemma map_filter_M_pure_E:
  assumes "h  (map_filter_M::('x  ('heap, 'e, 'y option) prog)  'x list
   ('heap, 'e, 'y list) prog) f xs r ys" and "y  set ys" and "x h. x  set xs  pure (f x) h"
  obtains x where "h  f x r Some y" and "x  set xs"
proof -
  obtain ys_opts ys_no_opts where
    ys_opts: "h  map_M f xs r ys_opts" and
    ys_no_opts: "h  filter_M (λx. (return (x  None)::('heap, 'e, bool) prog)) ys_opts r ys_no_opts" and
    ys: "h  map_M (λx. (return (the x)::('heap, 'e, 'y) prog)) ys_no_opts r ys"
    using assms
    by(auto simp add: map_filter_M_def map_M_pure_I elim!: bind_returns_result_E2)
  have "y  set ys_no_opts. y  None"
    using ys_no_opts filter_M_holds_for_result
    by fastforce
  then have "Some y  set ys_no_opts"
    using map_M_pure_E2 ys y  set ys
    by (metis (no_types, lifting) option.collapse return_pure return_returns_result)
  then have "Some y  set ys_opts"
    using filter_M_subset ys_no_opts by fastforce
  then show "(x. h  f x r Some y  x  set xs  thesis)  thesis"
    by (metis assms(3) map_M_pure_E2 ys_opts)
qed


subsection ‹Iterate›

fun iterate_M :: "('heap, 'e, 'result) prog list  ('heap, 'e, 'result) prog"
  where
    "iterate_M [] = return undefined"
  | "iterate_M (x # xs) = x  (λ_. iterate_M xs)"


lemma iterate_M_concat:
  assumes "h  iterate_M xs h h'"
    and "h'  iterate_M ys h h''"
  shows "h  iterate_M (xs @ ys) h h''"
  using assms
  apply(induct "xs" arbitrary: h h'')
   apply(simp)
  apply(auto)[1]
  by (meson bind_returns_heap_E bind_returns_heap_I)

subsection‹Miscellaneous Rules›

lemma execute_bind_simp:
  assumes "h  f r x" and "h  f h h'"
  shows "h  f  g = h'  g x"
  using assms 
  by(auto simp add: returns_result_def returns_heap_def bind_def execute_def  
      split: sum.splits)

lemma bind_cong [fundef_cong]:
  fixes f1 f2 :: "('heap, 'e, 'result) prog"
    and g1 g2 :: "'result  ('heap, 'e, 'result2) prog"
  assumes "h  f1 = h  f2"
    and "y h'. h  f1 r y  h  f1 h h'  h'  g1 y = h'  g2 y"
  shows "h  (f1  g1) = h  (f2  g2)"
  apply(insert assms, cases "h  f1") 
  by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)

lemma bind_cong_2:
  assumes "pure f h" and "pure f h'"
    and "x. h  f r x = h'  f r x"
    and "x. h  f r x  h  g x r y = h'  g x r y'"
  shows "h  f  g r y = h'  f  g r y'"
  using assms
  by(auto intro!: bind_pure_returns_result_I elim!: bind_returns_result_E2)

lemma bind_case_cong [fundef_cong]:
  assumes "x = x'" and "a. x = Some a  f a h = f' a h"
  shows "(case x of Some a  f a | None  g) h = (case x' of Some a  f' a | None  g) h"
  by (insert assms, simp add: option.case_eq_if)


subsection ‹Reasoning About Reads and Writes›

definition preserved :: "('heap, 'e, 'result) prog  'heap  'heap  bool"
  where
    "preserved f h h'  (x. h  f r x  h'  f r x)"

lemma preserved_code [code]:
  "preserved f h h' = (((h  ok f)  (h'  ok f)  |h  f|r = |h'  f|r)  ((¬h  ok f)  (¬h'  ok f)))"
  apply(auto simp add: preserved_def)[1]
   apply (meson is_OK_returns_result_E is_OK_returns_result_I)+
  done

lemma reflp_preserved_f [simp]: "reflp (preserved f)"
  by(auto simp add: preserved_def reflp_def)
lemma transp_preserved_f [simp]: "transp (preserved f)"
  by(auto simp add: preserved_def transp_def)


definition 
  all_args :: "('a  ('heap, 'e, 'result) prog)  ('heap, 'e, 'result) prog set"
  where
    "all_args f = (arg. {f arg})"


definition  
  reads :: "('heap  'heap  bool) set  ('heap, 'e, 'result) prog  'heap 
             'heap  bool"
  where
    "reads S getter h h'  (P  S. reflp P  transp P)  ((P  S. P h h') 
                               preserved getter h h')"

lemma reads_singleton [simp]: "reads {preserved f} f h h'"
  by(auto simp add: reads_def)

lemma reads_bind_pure:
  assumes "pure f h" and "pure f h'"
    and "reads S f h h'"
    and "x. h  f r x  reads S (g x) h h'"
  shows "reads S (f  g) h h'"
  using assms
  by(auto simp add: reads_def pure_pure preserved_def 
      intro!: bind_pure_returns_result_I is_OK_returns_result_I 
      dest: pure_returns_heap_eq 
      elim!: bind_returns_result_E)

lemma reads_insert_writes_set_left:
  "P  S. reflp P  transp P  reads {getter} f h h'  reads (insert getter S) f h h'"
  unfolding reads_def by simp

lemma reads_insert_writes_set_right:
  "reflp getter  transp getter  reads S f h h'  reads (insert getter S) f h h'"
  unfolding reads_def by blast

lemma reads_subset:
  "reads S f h h'  P  S' - S. reflp P  transp P  S  S'  reads S' f h h'"
  by(auto simp add: reads_def)

lemma return_reads [simp]: "reads {} (return x) h h'"
  by(simp add: reads_def preserved_def)

lemma error_reads [simp]: "reads {} (error e) h h'"
  by(simp add: reads_def preserved_def)

lemma noop_reads [simp]: "reads {} noop h h'"
  by(simp add: reads_def noop_def preserved_def)

lemma filter_M_reads:
  assumes "x. x  set xs  pure (P x) h" and "x. x  set xs  pure (P x) h'"
    and "x. x  set xs  reads S (P x) h h'"
    and "P  S. reflp P  transp P"
  shows "reads S (filter_M P xs) h h'"
  using assms
  apply(induct xs)
  by(auto intro: reads_subset[OF return_reads] intro!: reads_bind_pure)

definition writes :: 
  "('heap, 'e, 'result) prog set  ('heap, 'e, 'result2) prog  'heap  'heap  bool"
  where                                                                                
    "writes S setter h h' 
      (h  setter h h'  (progs. set progs  S  h  iterate_M progs h h'))"

lemma writes_singleton [simp]: "writes (all_args f) (f a) h h'"
  apply(auto simp add: writes_def all_args_def)[1]
  apply(rule exI[where x="[f a]"])
  by(auto)

lemma writes_singleton2 [simp]: "writes {f} f h h'"
  apply(auto simp add: writes_def all_args_def)[1]
  apply(rule exI[where x="[f]"])
  by(auto)

lemma writes_union_left_I:
  assumes "writes S f h h'"
  shows "writes (S  S') f h h'"
  using assms
  by(auto simp add: writes_def)

lemma writes_union_right_I:
  assumes "writes S' f h h'"
  shows "writes (S  S') f h h'"
  using assms
  by(auto simp add: writes_def)

lemma writes_union_minus_split:
  assumes "writes (S - S2) f h h'"
    and "writes (S' - S2) f h h'"
  shows "writes ((S  S') - S2) f h h'"
  using assms
  by(auto simp add: writes_def)

lemma writes_subset: "writes S f h h'  S  S'  writes S' f h h'"
  by(auto simp add: writes_def)

lemma writes_error [simp]: "writes S (error e) h h'"
  by(simp add: writes_def)

lemma writes_not_ok [simp]: "¬h  ok f  writes S f h h'"
  by(auto simp add: writes_def)

lemma writes_pure [simp]:
  assumes "pure f h"
  shows "writes S f h h'"
  using assms
  apply(auto simp add: writes_def)[1]
  by (metis bot.extremum iterate_M.simps(1) list.set(1) pure_returns_heap_eq return_returns_heap)

lemma writes_bind:
  assumes "h2. writes S f h h2" 
  assumes "x h2. h  f r x  h  f h h2  writes S (g x) h2 h'"
  shows "writes S (f  g) h h'"
  using assms
  apply(auto simp add: writes_def elim!: bind_returns_heap_E)[1]
  by (metis iterate_M_concat le_supI set_append)

lemma writes_bind_pure:
  assumes "pure f h"
  assumes "x. h  f r x  writes S (g x) h h'"
  shows "writes S (f  g) h h'"
  using assms
  by(auto simp add: writes_def elim!: bind_returns_heap_E2)

lemma writes_small_big:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h' w. w  SW   h  w h h'  P h h'"
  assumes "reflp P"
  assumes "transp P"
  shows "P h h'"
proof -
  obtain progs where "set progs  SW" and iterate: "h  iterate_M progs h h'"
    by (meson assms(1) assms(2) writes_def)
  then have "h h'. prog  set progs. h  prog h h'  P h h'"
    using assms(3) by auto
  with iterate assms(4) assms(5) have "h  iterate_M progs h h'  P h h'"
  proof(induct progs arbitrary: h)
    case Nil
    then show ?case
      using reflpE by force
  next
    case (Cons a progs)
    then show ?case
      apply(auto elim!: bind_returns_heap_E)[1]
      by (metis (full_types) transpD)
  qed
  then show ?thesis
    using assms(1) iterate by blast
qed

lemma reads_writes_preserved:
  assumes "reads SR getter h h'"
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h'. w  SW. h  w h h'  (r  SR. r h h')"
  shows "h  getter r x  h'  getter r x"
proof -
  obtain progs where "set progs  SW" and iterate: "h  iterate_M progs h h'"
    by (meson assms(2) assms(3) writes_def)
  then have "h h'. prog  set progs. h  prog h h'  (r  SR. r h h')"
    using assms(4) by blast
  with iterate have "r  SR. r h h'"
    using writes_small_big assms(1) unfolding reads_def
    by (metis assms(2) assms(3) assms(4))
  then show ?thesis
    using assms(1)
    by (simp add: preserved_def reads_def)
qed

lemma reads_writes_separate_forwards:
  assumes "reads SR getter h h'"
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h  getter r x"
  assumes "h h'. w  SW. h  w h h'  (r  SR. r h h')"
  shows "h'  getter r x"
  using reads_writes_preserved[OF assms(1) assms(2) assms(3) assms(5)] assms(4)
  by(auto simp add: preserved_def)

lemma reads_writes_separate_backwards:
  assumes "reads SR getter h h'"
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h'  getter r x"
  assumes "h h'. w  SW. h  w h h'  (r  SR. r h h')"
  shows "h  getter r x"
  using reads_writes_preserved[OF assms(1) assms(2) assms(3) assms(5)] assms(4)
  by(auto simp add: preserved_def)

end

Theory BaseMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹The Monad Infrastructure›
text‹In this theory, we introduce the basic infrastructure for our monadic class encoding.›
theory BaseMonad
  imports
    "../classes/BaseClass"
    "../preliminaries/Heap_Error_Monad"
begin
subsection‹Datatypes›

datatype exception = NotFoundError | HierarchyRequestError | NotSupportedError | SegmentationFault
  | AssertException | NonTerminationException | InvokeError | TypeError

lemma finite_set_in [simp]: "x  fset FS  x |∈| FS"
  by (meson notin_fset)

consts put_M :: 'a
consts get_M :: 'a
consts delete_M :: 'a

lemma sorted_list_of_set_eq [dest]: 
  "sorted_list_of_set (fset x) = sorted_list_of_set (fset y)  x = y"
  by (metis finite_fset fset_inject sorted_list_of_set(1))


locale l_ptr_kinds_M =
  fixes ptr_kinds :: "'heap  'ptr::linorder fset"
begin
definition a_ptr_kinds_M :: "('heap, exception, 'ptr list) prog"
  where
    "a_ptr_kinds_M = do {
      h  get_heap;
      return (sorted_list_of_set (fset (ptr_kinds h)))
    }"

lemma ptr_kinds_M_ok [simp]: "h  ok a_ptr_kinds_M"
  by(simp add: a_ptr_kinds_M_def)

lemma ptr_kinds_M_pure [simp]: "pure a_ptr_kinds_M h"
  by (auto simp add: a_ptr_kinds_M_def intro: bind_pure_I)

lemma ptr_kinds_ptr_kinds_M [simp]: "ptr  set |h  a_ptr_kinds_M|r  ptr |∈| ptr_kinds h"
  by(simp add: a_ptr_kinds_M_def)

lemma ptr_kinds_M_ptr_kinds [simp]: 
  "h  a_ptr_kinds_M r xa  xa = sorted_list_of_set (fset (ptr_kinds h))"
  by(auto simp add: a_ptr_kinds_M_def)
lemma ptr_kinds_M_ptr_kinds_returns_result [simp]: 
  "h  a_ptr_kinds_M  f r x  h  f (sorted_list_of_set (fset (ptr_kinds h))) r x"
  by(auto simp add: a_ptr_kinds_M_def)
lemma ptr_kinds_M_ptr_kinds_returns_heap [simp]: 
  "h  a_ptr_kinds_M  f h h'  h  f (sorted_list_of_set (fset (ptr_kinds h))) h h'"
  by(auto simp add: a_ptr_kinds_M_def)
end

locale l_get_M = 
  fixes get :: "'ptr  'heap  'obj option"
  fixes type_wf :: "'heap  bool"
  fixes ptr_kinds :: "'heap  'ptr fset"
  assumes "type_wf h  ptr |∈| ptr_kinds h  get ptr h  None"
  assumes "get ptr h  None  ptr |∈| ptr_kinds h"
begin

definition a_get_M :: "'ptr  ('obj  'result)   ('heap, exception, 'result) prog"
  where
    "a_get_M ptr getter = (do {
      h  get_heap;
      (case get ptr h of
        Some res  return (getter res)
      | None  error SegmentationFault)
    })"

lemma get_M_pure [simp]: "pure (a_get_M ptr getter) h"
  by(auto simp add: a_get_M_def bind_pure_I split: option.splits)

lemma get_M_ok:
  "type_wf h  ptr |∈| ptr_kinds h  h  ok (a_get_M ptr getter)"
  apply(simp add: a_get_M_def)
  by (metis l_get_M_axioms l_get_M_def option.case_eq_if return_ok)
lemma get_M_ptr_in_heap:
  "h  ok (a_get_M ptr getter)  ptr |∈| ptr_kinds h"
  apply(simp add: a_get_M_def)
  by (metis error_returns_result is_OK_returns_result_E l_get_M_axioms l_get_M_def option.simps(4))

end

locale l_put_M = l_get_M get for get :: "'ptr  'heap  'obj option" +
  fixes put :: "'ptr  'obj  'heap  'heap"
begin
definition a_put_M :: "'ptr  (('v  'v)  'obj  'obj)  'v  ('heap, exception, unit) prog"
  where
    "a_put_M ptr setter v = (do {
      obj  a_get_M ptr id;
      h  get_heap;
      return_heap (put ptr (setter (λ_. v) obj) h)
    })"

lemma put_M_ok:
  "type_wf h  ptr |∈| ptr_kinds h  h  ok (a_put_M ptr setter v)"
  by(auto simp add: a_put_M_def intro!: bind_is_OK_I2 dest: get_M_ok elim!: bind_is_OK_E)

lemma put_M_ptr_in_heap:
  "h  ok (a_put_M ptr setter v)  ptr |∈| ptr_kinds h"
  by(auto simp add: a_put_M_def intro!: bind_is_OK_I2 elim: get_M_ptr_in_heap 
      dest: is_OK_returns_result_I elim!: bind_is_OK_E)

end

subsection ‹Setup for Defining Partial Functions›

lemma execute_admissible: 
  "ccpo.admissible (fun_lub (flat_lub (Inl (e::'e)))) (fun_ord (flat_ord (Inl e)))
     ((λa. (h::'heap) h2 (r::'result). h  a = Inr (r, h2)  P h h2 r)  Prog)"
proof (unfold comp_def, rule ccpo.admissibleI, clarify)
  fix A :: "('heap  'e + 'result × 'heap) set"
  let ?lub = "Prog (fun_lub (flat_lub (Inl e)) A)"
  fix h h2 r
  assume 1: "Complete_Partial_Order.chain (fun_ord (flat_ord (Inl e))) A"
    and 2: "xaA. h h2 r. h  Prog xa = Inr (r, h2)   P h h2 r"
    and 4: "h  Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r, h2)"
  have h1:"a. Complete_Partial_Order.chain (flat_ord (Inl e)) {y. fA. y = f a}"
    by (rule chain_fun[OF 1])
  show "P h h2 r"
    using CollectD Inl_Inr_False prog.sel chain_fun[OF 1] flat_lub_in_chain[OF chain_fun[OF 1]] 2 4 
    unfolding execute_def fun_lub_def
  proof -
    assume a1: "the_prog (Prog (λx. flat_lub (Inl e) {y. fA. y = f x})) h = Inr (r, h2)"
    assume a2: "xaA. h h2 r. the_prog (Prog xa) h = Inr (r, h2)  P h h2 r"
    have "Inr (r, h2)  {s. f. f  A  s = f h}  Inr (r, h2) = Inl e"
      using a1 by (metis (lifting) aa a. flat_lub (Inl e) {y. fA. y = f aa} = a  a = Inl e  a  {y. fA. y = f aa} prog.sel)
    then show ?thesis
      using a2 by fastforce
  qed
qed

lemma execute_admissible2:
  "ccpo.admissible (fun_lub (flat_lub (Inl (e::'e)))) (fun_ord (flat_ord (Inl e)))
     ((λa. (h::'heap) h' h2 h2' (r::'result) r'. 
                    h  a = Inr (r, h2)  h'  a = Inr (r', h2')  P h h' h2 h2' r r')  Prog)"
proof (unfold comp_def, rule ccpo.admissibleI, clarify)
  fix A :: "('heap  'e + 'result × 'heap) set"
  let ?lub = "Prog (fun_lub (flat_lub (Inl e)) A)"
  fix h h' h2 h2' r r'
  assume 1: "Complete_Partial_Order.chain (fun_ord (flat_ord (Inl e))) A"
    and 2 [rule_format]: "xaA. h h' h2 h2' r r'. h  Prog xa = Inr (r, h2) 
                           h'  Prog xa = Inr (r', h2')  P h h' h2 h2' r r'"
    and 4: "h  Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r, h2)"
    and 5: "h'  Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r', h2')"
  have h1:"a. Complete_Partial_Order.chain (flat_ord (Inl e)) {y. fA. y = f a}"
    by (rule chain_fun[OF 1])
  have "h  ?lub  {y. fA. y = f h}"
    using flat_lub_in_chain[OF h1] 4
    unfolding execute_def fun_lub_def
    by (metis (mono_tags, lifting) Collect_cong Inl_Inr_False prog.sel)
  moreover have "h'  ?lub  {y. fA. y = f h'}"
    using flat_lub_in_chain[OF h1] 5
    unfolding execute_def fun_lub_def
    by (metis (no_types, lifting) Collect_cong Inl_Inr_False prog.sel)
  ultimately obtain f where
    "f  A" and
    "h  Prog f = Inr (r, h2)" and
    "h'  Prog f = Inr (r', h2')"
    using 1 4 5 
    apply(auto simp add:  chain_def fun_ord_def flat_ord_def execute_def)[1]
    by (metis Inl_Inr_False)
  then show "P h h' h2 h2' r r'"
    by(fact 2)
qed

definition dom_prog_ord :: 
  "('heap, exception, 'result) prog  ('heap, exception, 'result) prog  bool" where
  "dom_prog_ord = img_ord (λa b. execute b a) (fun_ord (flat_ord (Inl NonTerminationException)))"

definition dom_prog_lub :: 
  "('heap, exception, 'result) prog set  ('heap, exception, 'result) prog" where
  "dom_prog_lub = img_lub (λa b. execute b a) Prog (fun_lub (flat_lub (Inl NonTerminationException)))"

lemma dom_prog_lub_empty: "dom_prog_lub {} = error NonTerminationException"
  by(simp add: dom_prog_lub_def img_lub_def fun_lub_def flat_lub_def error_def)

lemma dom_prog_interpretation: "partial_function_definitions dom_prog_ord dom_prog_lub"
proof -
  have "partial_function_definitions (fun_ord (flat_ord (Inl NonTerminationException))) 
                                     (fun_lub (flat_lub (Inl NonTerminationException)))"
    by (rule partial_function_lift) (rule flat_interpretation)
  then show ?thesis
    apply (simp add: dom_prog_lub_def dom_prog_ord_def flat_interpretation execute_def)
    using partial_function_image prog.expand prog.sel by blast
qed

interpretation dom_prog: partial_function_definitions dom_prog_ord dom_prog_lub
  rewrites "dom_prog_lub {}  error NonTerminationException"
  by (fact dom_prog_interpretation)(simp add: dom_prog_lub_empty)

lemma admissible_dom_prog: 
  "dom_prog.admissible (λf. x h h' r. h  f x r r  h  f x h h'  P x h h' r)"
proof (rule admissible_fun[OF dom_prog_interpretation])
  fix x
  show "ccpo.admissible dom_prog_lub dom_prog_ord (λa. h h' r. h  a r r  h  a h h' 
          P x h h' r)"
    unfolding dom_prog_ord_def dom_prog_lub_def
  proof (intro admissible_image partial_function_lift flat_interpretation)
    show "ccpo.admissible (fun_lub (flat_lub (Inl NonTerminationException))) 
                          (fun_ord (flat_ord (Inl NonTerminationException)))
     ((λa. h h' r. h  a r r  h  a h h'  P x h h' r)  Prog)"
      by(auto simp add: execute_admissible returns_result_def returns_heap_def split: sum.splits)
  next
    show "x y. (λb. b  x) = (λb. b  y)  x = y"
      by(simp add: execute_def prog.expand)
  next
    show "x. (λb. b  Prog x) = x"
      by(simp add: execute_def)
  qed
qed

lemma admissible_dom_prog2:
  "dom_prog.admissible (λf. x h h2 h' h2' r r2. h  f x r r  h  f x h h' 
             h2  f x r r2  h2  f x h h2'  P x h h2 h' h2' r r2)"
proof (rule admissible_fun[OF dom_prog_interpretation])
  fix x
  show "ccpo.admissible dom_prog_lub dom_prog_ord (λa. h h2 h' h2' r r2. h  a r r 
                    h  a h h'  h2  a r r2  h2  a h h2'  P x h h2 h' h2' r r2)"
    unfolding dom_prog_ord_def dom_prog_lub_def
  proof (intro admissible_image partial_function_lift flat_interpretation)
    show "ccpo.admissible (fun_lub (flat_lub (Inl NonTerminationException))) 
                          (fun_ord (flat_ord (Inl NonTerminationException)))
     ((λa. h h2 h' h2' r r2. h  a r r  h  a h h'  h2  a r r2  h2  a h h2' 
                  P x h h2 h' h2' r r2)  Prog)"
      by(auto simp add: returns_result_def returns_heap_def intro!: ccpo.admissibleI 
          dest!: ccpo.admissibleD[OF execute_admissible2[where P="P x"]] 
          split: sum.splits)
  next
    show "x y. (λb. b  x) = (λb. b  y)  x = y"
      by(simp add: execute_def prog.expand)
  next
    show "x. (λb. b  Prog x) = x"
      by(simp add: execute_def)
  qed
qed

lemma fixp_induct_dom_prog:
  fixes F :: "'c  'c" and
    U :: "'c  'b  ('heap, exception, 'result) prog" and
    C :: "('b  ('heap, exception, 'result) prog)  'c" and
    P :: "'b  'heap  'heap  'result  bool"
  assumes mono: "x. monotone (fun_ord dom_prog_ord) dom_prog_ord (λf. U (F (C f)) x)"
  assumes eq: "f  C (ccpo.fixp (fun_lub dom_prog_lub) (fun_ord dom_prog_ord) (λf. U (F (C f))))"
  assumes inverse2: "f. U (C f) = f"
  assumes step: "f x h h' r. (x h h' r. h  (U f x) r r  h  (U f x) h h'  P x h h' r) 
     h  (U (F f) x) r r  h  (U (F f) x) h h'  P x h h' r"
  assumes defined: "h  (U f x) r r" and "h  (U f x) h h'"
  shows "P x h h' r"
  using step defined dom_prog.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_dom_prog, of P]
  by (metis assms(6) error_returns_heap)

declaration Partial_Function.init "dom_prog" @{term dom_prog.fixp_fun}
  @{term dom_prog.mono_body} @{thm dom_prog.fixp_rule_uc} @{thm dom_prog.fixp_induct_uc}
  (SOME @{thm fixp_induct_dom_prog})


abbreviation "mono_dom_prog  monotone (fun_ord dom_prog_ord) dom_prog_ord"

lemma dom_prog_ordI:
  assumes "h. h  f e NonTerminationException  h  f = h  g"
  shows "dom_prog_ord f g"
proof(auto simp add: dom_prog_ord_def img_ord_def fun_ord_def flat_ord_def)[1]
  fix x
  assume "x  f  x  g"
  then show "x  f = Inl NonTerminationException"
    using assms[where h=x]
    by(auto simp add: returns_error_def split: sum.splits)
qed

lemma dom_prog_ordE:
  assumes "dom_prog_ord x y"
  obtains "h  x e NonTerminationException" | " h  x = h  y"
  using assms unfolding dom_prog_ord_def img_ord_def fun_ord_def flat_ord_def
  using returns_error_def by force


lemma bind_mono [partial_function_mono]:
  fixes B :: "('a  ('heap, exception, 'result) prog)  ('heap, exception, 'result2) prog"
  assumes mf: "mono_dom_prog B" and mg: "y. mono_dom_prog (λf. C y f)"
  shows "mono_dom_prog (λf. B f  (λy. C y f))"
proof (rule monotoneI)
  fix f g :: "'a  ('heap, exception, 'result) prog"
  assume fg: "dom_prog.le_fun f g"
  from mf
  have 1: "dom_prog_ord (B f) (B g)" by (rule monotoneD) (rule fg)
  from mg
  have 2: "y'. dom_prog_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)

  have "dom_prog_ord (B f  (λy. C y f)) (B g  (λy. C y f))"
    (is "dom_prog_ord ?L ?R")
  proof (rule dom_prog_ordI)
    fix h
    from 1 show "h  ?L e NonTerminationException  h  ?L = h  ?R"
      apply(rule dom_prog_ordE) 
       apply(auto)[1]
      using bind_cong by fastforce
  qed
  also
  have h1: "dom_prog_ord (B g  (λy'. C y' f)) (B g  (λy'. C y' g))"
    (is "dom_prog_ord ?L ?R")
  proof (rule dom_prog_ordI)
    (* { *)
    fix h
    show "h  ?L e NonTerminationException  h  ?L = h  ?R"
    proof (cases "h  ok (B g)")
      case True
      then obtain x h' where x: "h  B g r x" and h': "h  B g h h'"
        by blast
      then have "dom_prog_ord (C x f) (C x g)"
        using 2 by simp
      then show ?thesis
        using x h'
        apply(auto intro!: bind_returns_error_I3 dest: returns_result_eq dest!: dom_prog_ordE)[1]
        apply(auto simp add: execute_bind_simp)[1]
        using "2" dom_prog_ordE by metis
    next
      case False
      then obtain e where e: "h  B g e e"
        by(simp add: is_OK_def returns_error_def split: sum.splits)
      have "h  B g  (λy'. C y' f) e e"
        using e by(auto)
      moreover have "h  B g  (λy'. C y' g) e e"
        using e by auto
      ultimately show ?thesis
        using bind_returns_error_eq by metis
    qed
  qed
  finally (dom_prog.leq_trans)
  show "dom_prog_ord (B f  (λy. C y f)) (B g  (λy'. C y' g))" .
qed

lemma mono_dom_prog1 [partial_function_mono]:
  fixes g ::  "('a  ('heap, exception, 'result) prog)  'b  ('heap, exception, 'result) prog"
  assumes "x. (mono_dom_prog (λf. g f x))"
  shows "mono_dom_prog (λf. map_M (g f) xs)"
  using assms
  apply (induct xs) 
  by(auto simp add: call_mono dom_prog.const_mono intro!: bind_mono)

lemma mono_dom_prog2 [partial_function_mono]:
  fixes g ::  "('a  ('heap, exception, 'result) prog)  'b  ('heap, exception, 'result) prog"
  assumes "x. (mono_dom_prog (λf. g f x))"
  shows "mono_dom_prog (λf. forall_M (g f) xs)"
  using assms
  apply (induct xs) 
  by(auto simp add: call_mono dom_prog.const_mono intro!: bind_mono)

lemma sorted_list_set_cong [simp]: 
  "sorted_list_of_set (fset FS) = sorted_list_of_set (fset FS')  FS = FS'"
  by auto

end

Theory ObjectPointer

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Object›
text‹In this theory, we introduce the typed pointer for the class Object. This class is the 
common superclass of our class model.›
theory ObjectPointer
  imports
    Ref
begin

datatype 'object_ptr object_ptr = Ext 'object_ptr
register_default_tvars "'object_ptr object_ptr" 

instantiation object_ptr :: (linorder) linorder
begin
definition less_eq_object_ptr :: "'object_ptr::linorder object_ptr  'object_ptr object_ptr  bool"
  where "less_eq_object_ptr x y  (case x of Ext i  (case y of Ext j  i  j))"
definition less_object_ptr :: "'object_ptr::linorder object_ptr  'object_ptr object_ptr  bool"
  where "less_object_ptr x y  x  y  ¬ y  x"
instance by(standard, auto simp add: less_eq_object_ptr_def less_object_ptr_def 
      split: object_ptr.splits)
end

end

Theory ObjectClass

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Object›
text‹In this theory, we introduce the definition of the class Object. This class is the 
common superclass of our class model.›

theory ObjectClass
  imports
    BaseClass
    "../pointers/ObjectPointer"
begin

record RObject =
  nothing :: unit
register_default_tvars "'Object RObject_ext" 
type_synonym 'Object Object = "'Object RObject_scheme"
register_default_tvars "'Object Object" 

datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
register_default_tvars "('object_ptr, 'Object) heap"  
type_synonym heapfinal = "(unit, unit) heap"

definition object_ptr_kinds :: "(_) heap  (_) object_ptr fset"
  where
    "object_ptr_kinds = fmdom  the_heap"

lemma object_ptr_kinds_simp [simp]: 
  "object_ptr_kinds (Heap (fmupd object_ptr object (the_heap h))) 
           = {|object_ptr|} |∪| object_ptr_kinds h"
  by(auto simp add: object_ptr_kinds_def)

definition getObject :: "(_) object_ptr  (_) heap  (_) Object option"
  where
    "getObject ptr h = fmlookup (the_heap h) ptr"
adhoc_overloading get getObject 

locale l_type_wf_defObject
begin
definition a_type_wf :: "(_) heap  bool"
  where
    "a_type_wf h = True"
end
global_interpretation l_type_wf_defObject defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfObject = l_type_wf type_wf for type_wf :: "((_) heap  bool)" +
  assumes type_wfObject: "type_wf h  ObjectClass.type_wf h"

locale l_getObject_lemmas = l_type_wfObject
begin
lemma getObject_type_wf:
  assumes "type_wf h"
  shows "object_ptr |∈| object_ptr_kinds h  getObject object_ptr h  None"
  using l_type_wfObject_axioms assms
  apply(simp add: type_wf_def getObject_def)
  by (simp add: fmlookup_dom_iff object_ptr_kinds_def)
end

global_interpretation l_getObject_lemmas type_wf
  by (simp add: l_getObject_lemmas.intro l_type_wfObject.intro)

definition putObject :: "(_) object_ptr  (_) Object  (_) heap  (_) heap"
  where
    "putObject ptr obj h = Heap (fmupd ptr obj (the_heap h))"
adhoc_overloading put putObject

lemma putObject_ptr_in_heap:
  assumes "putObject object_ptr object h = h'"
  shows "object_ptr |∈| object_ptr_kinds h'"
  using assms
  unfolding putObject_def
  by auto

lemma putObject_put_ptrs:
  assumes "putObject object_ptr object h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|object_ptr|}"
  using assms
  by (metis comp_apply fmdom_fmupd funion_finsert_right heap.sel object_ptr_kinds_def 
      sup_bot.right_neutral putObject_def)

lemma object_more_extend_id [simp]: "more (extend x y) = y"
  by(simp add: extend_def)

lemma object_empty [simp]: "nothing = (),  = more x = x"
  by simp

locale l_known_ptrObject
begin
definition a_known_ptr :: "(_) object_ptr  bool"
  where
    "a_known_ptr ptr = False"

lemma known_ptr_not_object_ptr: 
  "a_known_ptr ptr  ¬is_object_ptr ptr  known_ptr ptr"
  by(simp add: a_known_ptr_def)
end
global_interpretation l_known_ptrObject defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def

locale l_known_ptrs = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr  bool" +
  fixes known_ptrs :: "(_) heap  bool"
  assumes known_ptrs_known_ptr: "known_ptrs h  ptr |∈| object_ptr_kinds h  known_ptr ptr"
  assumes known_ptrs_preserved:
    "object_ptr_kinds h = object_ptr_kinds h'  known_ptrs h = known_ptrs h'"
  assumes known_ptrs_subset:
    "object_ptr_kinds h' |⊆| object_ptr_kinds h  known_ptrs h  known_ptrs h'"
  assumes known_ptrs_new_ptr:
    "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|}  known_ptr new_ptr 
known_ptrs h  known_ptrs h'"

locale l_known_ptrsObject = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr  bool"
begin
definition a_known_ptrs :: "(_) heap  bool"
  where
    "a_known_ptrs h = (ptr  fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr: 
  "a_known_ptrs h  ptr |∈| object_ptr_kinds h  known_ptr ptr"
  apply(simp add: a_known_ptrs_def)
  using notin_fset by fastforce

lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h'  a_known_ptrs h = a_known_ptrs h'"
  by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
  "object_ptr_kinds h' |⊆| object_ptr_kinds h  a_known_ptrs h  a_known_ptrs h'"
  by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|}  known_ptr new_ptr 
a_known_ptrs h  a_known_ptrs h'"
  by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrsObject known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
  using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr
  by blast


lemma get_object_ptr_simp1 [simp]: "getObject object_ptr (putObject object_ptr object h) = Some object"
  by(simp add: getObject_def putObject_def)
lemma get_object_ptr_simp2 [simp]: 
  "object_ptr  object_ptr' 
    getObject object_ptr (putObject object_ptr' object h) = getObject object_ptr h"
  by(simp add: getObject_def putObject_def)


subsection‹Limited Heap Modifications›

definition heap_unchanged_except :: "(_) object_ptr set  (_) heap  (_) heap  bool"
  where
    "heap_unchanged_except S h h' = (ptr  (fset (object_ptr_kinds h) 
                                    (fset (object_ptr_kinds h'))) - S. get ptr h = get ptr h')"

definition deleteObject :: "(_) object_ptr  (_) heap  (_) heap option" where
  "deleteObject ptr h = (if ptr |∈| object_ptr_kinds h then Some (Heap (fmdrop ptr (the_heap h))) 
                                                      else None)"

lemma deleteObject_pointer_removed:
  assumes "deleteObject ptr h = Some h'"
  shows "ptr |∉| object_ptr_kinds h'"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)

lemma deleteObject_pointer_ptr_in_heap:
  assumes "deleteObject ptr h = Some h'"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)

lemma deleteObject_ok:
  assumes "ptr |∈| object_ptr_kinds h"
  shows "deleteObject ptr h  None"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)


subsection ‹Code Generator Setup›

definition "create_heap xs = Heap (fmap_of_list xs)"

code_datatype ObjectClass.heap.Heap create_heap

lemma object_ptr_kinds_code3 [code]: 
  "fmlookup (the_heap (create_heap xs)) x = map_of xs x"
  by(auto simp add: create_heap_def fmlookup_of_list)

lemma object_ptr_kinds_code4 [code]: 
  "the_heap (create_heap xs) = fmap_of_list xs"
  by(simp add: create_heap_def)

lemma object_ptr_kinds_code5 [code]: 
  "the_heap (Heap x) = x"
  by simp


end

Theory ObjectMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Object›
text‹In this theory, we introduce the monadic method setup for the Object class.›
theory ObjectMonad
  imports
    BaseMonad
    "../classes/ObjectClass"
begin

type_synonym ('object_ptr, 'Object, 'result) dom_prog
  = "((_) heap, exception, 'result) prog"
register_default_tvars "('object_ptr, 'Object, 'result) dom_prog" 

global_interpretation l_ptr_kinds_M object_ptr_kinds defines object_ptr_kinds_M = a_ptr_kinds_M .
lemmas object_ptr_kinds_M_defs = a_ptr_kinds_M_def


global_interpretation l_dummy defines get_MObject = "l_get_M.a_get_M getObject" .
lemma get_M_is_l_get_M: "l_get_M getObject type_wf object_ptr_kinds"
  by (simp add: a_type_wf_def getObject_type_wf l_get_M_def)
lemmas get_M_defs = get_MObject_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_MObject

locale l_get_MObject_lemmas = l_type_wfObject
begin
interpretation l_get_M getObject type_wf object_ptr_kinds
  apply(unfold_locales)
   apply (simp add: getObject_type_wf local.type_wfObject)
  by (simp add: a_type_wf_def getObject_type_wf)
lemmas get_MObject_ok = get_M_ok[folded get_MObject_def]
lemmas get_MObject_ptr_in_heap = get_M_ptr_in_heap[folded get_MObject_def]
end

global_interpretation l_get_MObject_lemmas type_wf
  by (simp add: l_get_MObject_lemmas_def l_type_wfObject_axioms)

lemma object_ptr_kinds_M_reads: 
  "reads (object_ptr. {preserved (get_MObject object_ptr RObject.nothing)}) object_ptr_kinds_M h h'"
  apply(auto simp add: object_ptr_kinds_M_defs getObject_type_wf type_wf_defs reads_def 
      preserved_def get_M_defs  
      split: option.splits)[1]
  using a_type_wf_def getObject_type_wf by blast+


global_interpretation l_put_M type_wf object_ptr_kinds getObject putObject 
  rewrites "a_get_M = get_MObject" 
  defines put_MObject = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_MObject_def)
lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_MObject


locale l_put_MObject_lemmas = l_type_wfObject
begin
interpretation l_put_M  type_wf object_ptr_kinds getObject putObject
  apply(unfold_locales)
  using getObject_type_wf l_type_wfObject.type_wfObject local.l_type_wfObject_axioms apply blast
  by (simp add: a_type_wf_def getObject_type_wf)
lemmas put_MObject_ok = put_M_ok[folded put_MObject_def]
lemmas put_MObject_ptr_in_heap = put_M_ptr_in_heap[folded put_MObject_def]
end

global_interpretation l_put_MObject_lemmas type_wf
  by (simp add: l_put_MObject_lemmas_def l_type_wfObject_axioms)


definition check_in_heap :: "(_) object_ptr  (_, unit) dom_prog"
  where
    "check_in_heap ptr = do {
      h  get_heap;
      (if ptr |∈| object_ptr_kinds h then
        return ()
      else
        error SegmentationFault
      )}"

lemma check_in_heap_ptr_in_heap: "ptr |∈| object_ptr_kinds h  h  ok (check_in_heap ptr)"
  by(auto simp add: check_in_heap_def)
lemma check_in_heap_pure [simp]: "pure (check_in_heap ptr) h"
  by(auto simp add: check_in_heap_def intro!: bind_pure_I)
lemma check_in_heap_is_OK [simp]: 
  "ptr |∈| object_ptr_kinds h  h  ok (check_in_heap ptr  f) = h  ok (f ())"
  by(simp add: check_in_heap_def)
lemma check_in_heap_returns_result [simp]: 
  "ptr |∈| object_ptr_kinds h  h  (check_in_heap ptr  f) r x = h  f () r x"
  by(simp add: check_in_heap_def)
lemma check_in_heap_returns_heap [simp]: 
  "ptr |∈| object_ptr_kinds h  h  (check_in_heap ptr  f) h h' = h  f () h h'"
  by(simp add: check_in_heap_def)

lemma check_in_heap_reads: 
  "reads {preserved (get_M object_ptr nothing)} (check_in_heap object_ptr) h h'"
  apply(simp add: check_in_heap_def reads_def preserved_def)
  by (metis a_type_wf_def get_MObject_ok get_MObject_ptr_in_heap is_OK_returns_result_E 
      is_OK_returns_result_I unit_all_impI)

subsection‹Invoke›

fun invoke_rec :: "(((_) object_ptr  bool) × ((_) object_ptr  'args 
                   (_, 'result) dom_prog)) list  (_) object_ptr  'args 
                   (_, 'result) dom_prog"
  where
    "invoke_rec ((P, f)#xs) ptr args = (if P ptr then f ptr args else invoke_rec xs ptr args)"
  | "invoke_rec [] ptr args = error InvokeError"

definition invoke :: "(((_) object_ptr  bool) × ((_) object_ptr  'args 
                      (_, 'result) dom_prog)) list 
                      (_) object_ptr  'args  (_, 'result) dom_prog"
  where                               
    "invoke xs ptr args = do { check_in_heap ptr; invoke_rec xs ptr args}"

lemma invoke_split: "P (invoke ((Pred, f) # xs) ptr args) =
    ((¬(Pred ptr)  P (invoke xs ptr args))
   (Pred ptr  P (do {check_in_heap ptr; f ptr args})))"
  by(simp add: invoke_def)

lemma invoke_split_asm: "P (invoke ((Pred, f) # xs) ptr args) =
    (¬((¬(Pred ptr)  (¬ P (invoke xs ptr args)))
     (Pred ptr  (¬ P (do {check_in_heap ptr; f ptr args})))))"
  by(simp add: invoke_def)
lemmas invoke_splits = invoke_split invoke_split_asm

lemma invoke_ptr_in_heap: "h  ok (invoke xs ptr args)  ptr |∈| object_ptr_kinds h"
  by (metis bind_is_OK_E check_in_heap_ptr_in_heap invoke_def is_OK_returns_heap_I)

lemma invoke_pure [simp]: "pure (invoke [] ptr args) h"
  by(auto simp add: invoke_def intro!: bind_pure_I)

lemma invoke_is_OK [simp]: 
  "ptr |∈| object_ptr_kinds h  Pred ptr 
     h  ok (invoke ((Pred, f) # xs) ptr args) = h  ok (f ptr args)"
  by(simp add: invoke_def)
lemma invoke_returns_result [simp]: 
  "ptr |∈| object_ptr_kinds h  Pred ptr 
    h  (invoke ((Pred, f) # xs) ptr args) r x = h  f ptr args r x"
  by(simp add: invoke_def)
lemma invoke_returns_heap [simp]: 
  "ptr |∈| object_ptr_kinds h  Pred ptr 
    h  (invoke ((Pred, f) # xs) ptr args) h h' = h  f ptr args h h'"
  by(simp add: invoke_def)

lemma invoke_not [simp]: "¬Pred ptr  invoke ((Pred, f) # xs) ptr args = invoke xs ptr args"
  by(auto simp add: invoke_def)

lemma invoke_empty [simp]: "¬h  ok (invoke [] ptr args)"
  by(auto simp add: invoke_def check_in_heap_def)

lemma invoke_empty_reads [simp]: "P  S. reflp P  transp P  reads S (invoke [] ptr args) h h'"
  apply(simp add: invoke_def reads_def preserved_def)
  by (meson bind_returns_result_E error_returns_result)


subsection‹Modified Heaps›

lemma get_object_ptr_simp [simp]: 
  "getObject object_ptr (putObject ptr obj h) = (if ptr = object_ptr then Some obj else get object_ptr h)"
  by(auto simp add: getObject_def putObject_def split: option.splits Option.bind_splits)

lemma object_ptr_kinds_simp [simp]: "object_ptr_kinds (putObject ptr obj h) = object_ptr_kinds h |∪| {|ptr|}"
  by(auto simp add: object_ptr_kinds_def putObject_def split: option.splits)

lemma type_wf_put_I:
  assumes "type_wf h"
  shows "type_wf (putObject ptr obj h)"
  using assms
  by(auto simp add: type_wf_defs split: option.splits)

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs split: option.splits if_splits)

lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs split: option.splits if_splits)


subsection‹Preserving Types›

lemma type_wf_preserved: "type_wf h = type_wf h'"
  by(auto simp add: type_wf_defs)


lemma object_ptr_kinds_preserved_small:
  assumes "object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms
  apply(auto simp add: object_ptr_kinds_def preserved_def get_M_defs getObject_def 
      split: option.splits)[1]
   apply (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq 
      old.unit.exhaust option.case_eq_if return_returns_result)
  by (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq fmember.rep_eq 
      old.unit.exhaust option.case_eq_if return_returns_result)

lemma object_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h' w object_ptr. w  SW  h  w h h' 
           preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
proof -
  {
    fix object_ptr w
    have "preserved (get_MObject object_ptr RObject.nothing) h h'"
      apply(rule writes_small_big[OF assms])
      by auto
  }
  then show ?thesis
    using object_ptr_kinds_preserved_small by blast
qed


lemma reads_writes_preserved2:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h' x. w  SW. h  w h h'  preserved (get_MObject ptr getter) h h'"
  shows "preserved (get_M ptr getter) h h'"
  apply(clarsimp simp add: preserved_def)
  using reads_singleton assms(1) assms(2)
  apply(rule reads_writes_preserved)
  using assms(3)
  by(auto simp add: preserved_def)
end

Theory NodePointer

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Node›
text‹In this theory, we introduce the typed pointers for the class Node.›   
theory NodePointer
  imports
    ObjectPointer
begin

datatype 'node_ptr node_ptr = Ext 'node_ptr
register_default_tvars "'node_ptr node_ptr" 

type_synonym ('object_ptr, 'node_ptr) object_ptr = "('node_ptr node_ptr + 'object_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr) object_ptr" 

definition castnode_ptr2object_ptr :: "(_) node_ptr   (_) object_ptr"
  where
    "castnode_ptr2object_ptr ptr = object_ptr.Ext (Inl ptr)"

definition castobject_ptr2node_ptr :: "(_) object_ptr  (_) node_ptr option"
  where
    "castobject_ptr2node_ptr object_ptr = (case object_ptr of object_ptr.Ext (Inl node_ptr) 
                                            Some node_ptr | _  None)"

adhoc_overloading cast castnode_ptr2object_ptr castobject_ptr2node_ptr

definition is_node_ptr_kind :: "(_) object_ptr  bool"
  where
    "is_node_ptr_kind ptr = (castobject_ptr2node_ptr ptr  None)"

instantiation node_ptr :: (linorder) linorder
begin
definition less_eq_node_ptr :: "(_::linorder) node_ptr  (_) node_ptr  bool"
  where "less_eq_node_ptr x y  (case x of Ext i  (case y of Ext j  i  j))"
definition less_node_ptr :: "(_::linorder) node_ptr  (_) node_ptr  bool"
  where "less_node_ptr x y  x  y  ¬ y  x"
instance 
  apply(standard)
  by(auto simp add: less_eq_node_ptr_def less_node_ptr_def split: node_ptr.splits)
end

lemma node_ptr_casts_commute [simp]: 
  "castobject_ptr2node_ptr ptr = Some node_ptr  castnode_ptr2object_ptr node_ptr = ptr"
  unfolding castobject_ptr2node_ptr_def castnode_ptr2object_ptr_def
  by(auto split: object_ptr.splits sum.splits)

lemma node_ptr_casts_commute2 [simp]: 
  "castobject_ptr2node_ptr (castnode_ptr2object_ptr node_ptr) = Some node_ptr"
  by simp

lemma node_ptr_casts_commute3 [simp]:
  assumes "is_node_ptr_kind ptr"
  shows "castnode_ptr2object_ptr (the (castobject_ptr2node_ptr ptr)) = ptr"
  using assms
  by(auto simp add: is_node_ptr_kind_def castnode_ptr2object_ptr_def castobject_ptr2node_ptr_def 
      split: object_ptr.splits sum.splits)

lemma is_node_ptr_kind_obtains:
  assumes "is_node_ptr_kind ptr"
  obtains node_ptr where "castobject_ptr2node_ptr ptr = Some node_ptr"
  using assms is_node_ptr_kind_def by auto

lemma is_node_ptr_kind_none:
  assumes "¬is_node_ptr_kind ptr"
  shows "castobject_ptr2node_ptr ptr = None"
  using assms
  unfolding is_node_ptr_kind_def castobject_ptr2node_ptr_def
  by auto

lemma is_node_ptr_kind_cast [simp]: "is_node_ptr_kind (castnode_ptr2object_ptr node_ptr)"
  unfolding is_node_ptr_kind_def by simp

lemma castnode_ptr2object_ptr_inject [simp]: 
  "castnode_ptr2object_ptr x = castnode_ptr2object_ptr y  x = y"
  by(simp add: castnode_ptr2object_ptr_def)

lemma castobject_ptr2node_ptr_ext_none [simp]: 
  "castobject_ptr2node_ptr (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
  by(simp add: castobject_ptr2node_ptr_def)

lemma node_ptr_inclusion [simp]: 
  "castnode_ptr2object_ptr node_ptr  castnode_ptr2object_ptr ` node_ptrs  node_ptr  node_ptrs"
  by auto
end

Theory NodeClass

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section‹Node›
text‹In this theory, we introduce the types for the Node class.›

theory NodeClass
  imports
    ObjectClass
    "../pointers/NodePointer"
begin

subsubsection‹Node›

record RNode = RObject
  + nothing :: unit
register_default_tvars "'Node RNode_ext" 
type_synonym 'Node Node = "'Node RNode_scheme"
register_default_tvars "'Node Node" 
type_synonym ('Object, 'Node) Object = "('Node RNode_ext + 'Object) Object"
register_default_tvars "('Object, 'Node) Object" 

type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node) heap
  = "('node_ptr node_ptr + 'object_ptr, 'Node RNode_ext + 'Object) heap"
register_default_tvars
  "('object_ptr, 'node_ptr, 'Object, 'Node) heap" 
type_synonym heapfinal = "(unit, unit, unit, unit) heap"


definition node_ptr_kinds :: "(_) heap  (_) node_ptr fset"
  where
    "node_ptr_kinds heap = 
    (the |`| (castobject_ptr2node_ptr |`| (ffilter is_node_ptr_kind (object_ptr_kinds heap))))"

lemma node_ptr_kinds_simp [simp]: 
  "node_ptr_kinds (Heap (fmupd (cast node_ptr) node (the_heap h))) 
       = {|node_ptr|} |∪| node_ptr_kinds h"
  apply(auto simp add: node_ptr_kinds_def)[1]
  by force

definition castObject2Node :: "(_) Object  (_) Node option"
  where
    "castObject2Node obj = (case RObject.more obj of Inl node 
     Some (RObject.extend (RObject.truncate obj) node) | _  None)"
adhoc_overloading cast castObject2Node

definition castNode2Object:: "(_) Node  (_) Object"
  where
    "castNode2Object node = (RObject.extend (RObject.truncate node) (Inl (RObject.more node)))"
adhoc_overloading cast castNode2Object

definition is_node_kind :: "(_) Object  bool"
  where
    "is_node_kind ptr  castObject2Node ptr  None"

definition getNode :: "(_) node_ptr  (_) heap  (_) Node option"
  where                             
    "getNode node_ptr h = Option.bind (get (cast node_ptr) h) cast"
adhoc_overloading get getNode

locale l_type_wf_defNode
begin
definition a_type_wf :: "(_) heap  bool"
  where
    "a_type_wf h = (ObjectClass.type_wf h 
                     (node_ptr  fset( node_ptr_kinds h). getNode node_ptr h  None))"
end
global_interpretation l_type_wf_defNode defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfNode = l_type_wf type_wf for type_wf :: "((_) heap  bool)" +
  assumes type_wfNode: "type_wf h  NodeClass.type_wf h"

sublocale l_type_wfNode  l_type_wfObject
  apply(unfold_locales)
  using ObjectClass.a_type_wf_def by auto

locale l_getNode_lemmas = l_type_wfNode
begin
sublocale l_getObject_lemmas by unfold_locales
lemma getNode_type_wf:
  assumes "type_wf h"
  shows "node_ptr |∈| node_ptr_kinds h  getNode node_ptr h  None"
  using l_type_wfNode_axioms assms
  apply(simp add: type_wf_defs getNode_def l_type_wfNode_def)
  by (metis bind_eq_None_conv ffmember_filter fimage_eqI fmember.rep_eq is_node_ptr_kind_cast 
            getObject_type_wf node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3))
end

global_interpretation l_getNode_lemmas type_wf
  by unfold_locales

definition putNode :: "(_) node_ptr  (_) Node  (_) heap  (_) heap"
  where
    "putNode node_ptr node = put (cast node_ptr) (cast node)"
adhoc_overloading put putNode

lemma putNode_ptr_in_heap:
  assumes "putNode node_ptr node h = h'"
  shows "node_ptr |∈| node_ptr_kinds h'"
  using assms
  unfolding putNode_def node_ptr_kinds_def
  by (metis ffmember_filter fimage_eqI is_node_ptr_kind_cast node_ptr_casts_commute2 
      option.sel putObject_ptr_in_heap)

lemma putNode_put_ptrs:
  assumes "putNode node_ptr node h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast node_ptr|}"
  using assms
  by (simp add: putNode_def putObject_put_ptrs)

lemma node_ptr_kinds_commutes [simp]: 
  "cast node_ptr |∈| object_ptr_kinds h  node_ptr |∈| node_ptr_kinds h"
  apply(auto simp add: node_ptr_kinds_def split: option.splits)[1]
  by (metis (no_types, lifting) ffmember_filter fimage_eqI fset.map_comp 
      is_node_ptr_kind_none node_ptr_casts_commute2
      option.distinct(1) option.sel)

lemma node_empty [simp]: 
  "RObject.nothing = (), RNode.nothing = (),  = RNode.more node = node"
  by simp

lemma castNode2Object_inject [simp]: "castNode2Object x = castNode2Object y  x = y"
  apply(simp add: castNode2Object_def RObject.extend_def)
  by (metis (full_types) RObject.surjective old.unit.exhaust)

lemma castObject2Node_none [simp]: 
  "castObject2Node obj = None  ¬ (node. castNode2Object node = obj)"
  apply(auto simp add: castObject2Node_def castNode2Object_def RObject.extend_def split: sum.splits)[1]
  by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)

lemma castObject2Node_some [simp]: "castObject2Node obj = Some node  cast node = obj"
  by(auto simp add: castObject2Node_def castNode2Object_def RObject.extend_def split: sum.splits)

lemma castObject2Node_inv [simp]: "castObject2Node (castNode2Object node) = Some node"
  by simp

locale l_known_ptrNode
begin
definition a_known_ptr :: "(_) object_ptr  bool"
  where
    "a_known_ptr ptr = False"
end
global_interpretation l_known_ptrNode defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def


locale l_known_ptrsNode = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr  bool"
begin
definition a_known_ptrs :: "(_) heap  bool"
  where
    "a_known_ptrs h = (ptr  fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr: "a_known_ptrs h  ptr |∈| object_ptr_kinds h  known_ptr ptr"
  apply(simp add: a_known_ptrs_def)
  using notin_fset by fastforce
lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h'  a_known_ptrs h = a_known_ptrs h'"
  by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
  "object_ptr_kinds h' |⊆| object_ptr_kinds h  a_known_ptrs h  a_known_ptrs h'"
  by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|}  known_ptr new_ptr 
a_known_ptrs h  a_known_ptrs h'"
  by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrsNode known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
  using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
    known_ptrs_new_ptr
  by blast

lemma get_node_ptr_simp1 [simp]: "getNode node_ptr (putNode node_ptr node h) = Some node"
  by(auto simp add: getNode_def putNode_def)
lemma get_node_ptr_simp2 [simp]: 
  "node_ptr  node_ptr'  getNode node_ptr (putNode node_ptr' node h) = getNode node_ptr h"
  by(auto simp add: getNode_def putNode_def)

end

Theory NodeMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Node›
text‹In this theory, we introduce the monadic method setup for the Node class.›
theory NodeMonad
  imports
    ObjectMonad
    "../classes/NodeClass"
begin

type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node, 'result) dom_prog
  = "((_) heap, exception, 'result) prog"
register_default_tvars "('object_ptr, 'node_ptr, 'Object, 'Node, 'result) dom_prog" 


global_interpretation l_ptr_kinds_M node_ptr_kinds defines node_ptr_kinds_M = a_ptr_kinds_M .
lemmas node_ptr_kinds_M_defs = a_ptr_kinds_M_def

lemma node_ptr_kinds_M_eq:
  assumes "|h  object_ptr_kinds_M|r = |h'  object_ptr_kinds_M|r"
  shows "|h  node_ptr_kinds_M|r = |h'  node_ptr_kinds_M|r"
  using assms 
  by(auto simp add: node_ptr_kinds_M_defs object_ptr_kinds_M_defs node_ptr_kinds_def)


global_interpretation l_dummy defines get_MNode = "l_get_M.a_get_M getNode" .
lemma get_M_is_l_get_M: "l_get_M getNode type_wf node_ptr_kinds"
  apply(simp add: getNode_type_wf l_get_M_def)
  by (metis ObjectClass.a_type_wf_def ObjectClass.getObject_type_wf bind_eq_None_conv getNode_def 
      node_ptr_kinds_commutes option.simps(3))
lemmas get_M_defs = get_MNode_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_MNode

locale l_get_MNode_lemmas = l_type_wfNode
begin
sublocale l_get_MObject_lemmas by unfold_locales

interpretation l_get_M getNode type_wf node_ptr_kinds
  apply(unfold_locales)
   apply (simp add: getNode_type_wf local.type_wfNode)
  by (meson NodeMonad.get_M_is_l_get_M l_get_M_def)
lemmas get_MNode_ok = get_M_ok[folded get_MNode_def]
end

global_interpretation l_get_MNode_lemmas type_wf by unfold_locales

lemma node_ptr_kinds_M_reads: 
  "reads (object_ptr. {preserved (get_MObject object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
  using object_ptr_kinds_M_reads
  apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
      object_ptr_kinds_M_reads preserved_def)
  by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)

global_interpretation l_put_M type_wf node_ptr_kinds getNode putNode 
  rewrites "a_get_M = get_MNode" 
  defines put_MNode = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_MNode_def)

lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_MNode


locale l_put_MNode_lemmas = l_type_wfNode
begin
sublocale l_put_MObject_lemmas by unfold_locales

interpretation l_put_M type_wf node_ptr_kinds getNode putNode
  apply(unfold_locales)
   apply (simp add: getNode_type_wf local.type_wfNode)
  by (meson NodeMonad.get_M_is_l_get_M l_get_M_def)
lemmas put_MNode_ok = put_M_ok[folded put_MNode_def]
end

global_interpretation l_put_MNode_lemmas type_wf by unfold_locales

lemma get_M_Object_preserved1 [simp]: 
  "(x. getter (cast (setter (λ_. v) x)) = getter (cast x))  h  put_MNode node_ptr setter v h h' 
     preserved (get_MObject object_ptr getter) h h'"
  apply(cases "cast node_ptr = object_ptr") 
  by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs getNode_def preserved_def putNode_def 
      bind_eq_Some_conv 
      split: option.splits)

lemma get_M_Object_preserved2 [simp]: 
  "cast node_ptr  object_ptr  h  put_MNode node_ptr setter v h h' 
     preserved (get_MObject object_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs getNode_def putNode_def ObjectMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma get_M_Object_preserved3 [simp]: 
  "h  put_MNode node_ptr setter v h h'  (x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
     preserved (get_MObject object_ptr getter) h h'"
  apply(cases "cast node_ptr  object_ptr")
  by(auto simp add: put_M_defs get_M_defs getNode_def putNode_def ObjectMonad.get_M_defs preserved_def 
      split: option.splits bind_splits dest: get_heap_E)

lemma get_M_Object_preserved4 [simp]: 
  "cast node_ptr  object_ptr  h  put_MObject object_ptr setter v h h' 
       preserved (get_MNode node_ptr getter) h h'"
  by(auto simp add: ObjectMonad.put_M_defs get_M_defs getNode_def ObjectMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)

subsection‹Modified Heaps›

lemma get_node_ptr_simp [simp]: 
  "getNode node_ptr (putObject ptr obj h) = (if ptr = cast node_ptr then cast obj else get node_ptr h)"
  by(auto simp add: getNode_def)

lemma node_ptr_kinds_simp [simp]: 
  "node_ptr_kinds (putObject ptr obj h) 
                = node_ptr_kinds h |∪| (if is_node_ptr_kind ptr then {|the (cast ptr)|} else {||})"
  by(auto simp add: node_ptr_kinds_def)

lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "ObjectClass.type_wf (putObject ptr obj h)"
  assumes "is_node_ptr_kind ptr  is_node_kind obj"
  shows "type_wf (putObject ptr obj h)"
  using assms
  apply(auto simp add: type_wf_defs split: option.splits)[1]
  using castObject2Node_none is_node_kind_def apply blast
  using castObject2Node_none is_node_kind_def apply blast
  done

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs elim!: ObjectMonad.type_wf_put_ptr_not_in_heap_E  
      split: option.splits if_splits)

lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "ObjectClass.type_wf h"
  assumes "is_node_ptr_kind ptr  is_node_kind (the (get ptr h))"
  shows "type_wf h"
  using assms
  apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
  by (metis ObjectClass.getObject_type_wf bind.bind_lunit finite_set_in getNode_def is_node_kind_def option.exhaust_sel)


subsection‹Preserving Types›

lemma node_ptr_kinds_small:
  assumes "object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
  by(simp add: node_ptr_kinds_def preserved_def object_ptr_kinds_preserved_small[OF assms])

lemma node_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h'. w  SW. h  w h h' 
             (object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h')"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
  using writes_small_big[OF assms]
  apply(simp add: reflp_def transp_def preserved_def node_ptr_kinds_def)
  by (metis assms object_ptr_kinds_preserved)


lemma type_wf_preserved_small:
  assumes "object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  assumes "node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
  using type_wf_preserved allI[OF assms(2), of id, simplified]
  apply(auto simp add: type_wf_defs)[1]
   apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits)[1]
  apply (metis notin_fset option.simps(3))
  by(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits, force)[1]

lemma type_wf_preserved:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h' w. w  SW  h  w h h' 
            object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  assumes "h h' w. w  SW  h  w h h' 
            node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "h h' w. w  SW  h  w h h'  type_wf h = type_wf h'"
    using assms type_wf_preserved_small by fast
  with assms(1) assms(2) show ?thesis
    apply(rule writes_small_big)
    by(auto simp add: reflp_def transp_def)
qed
end

Theory ElementPointer

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Element›
text‹In this theory, we introduce the typed pointers for the class Element.›   
theory ElementPointer
  imports
    NodePointer
begin

datatype 'element_ptr element_ptr = Ref (the_ref: ref) | Ext 'element_ptr
register_default_tvars "'element_ptr element_ptr" 

type_synonym ('node_ptr, 'element_ptr) node_ptr
  = "('element_ptr element_ptr + 'node_ptr) node_ptr"
register_default_tvars "('node_ptr, 'element_ptr) node_ptr" 
type_synonym ('object_ptr, 'node_ptr, 'element_ptr) object_ptr
  = "('object_ptr, 'element_ptr element_ptr + 'node_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr) object_ptr" 


definition castelement_ptr2element_ptr :: "(_) element_ptr  (_) element_ptr"
  where
    "castelement_ptr2element_ptr = id"

definition castelement_ptr2node_ptr :: "(_) element_ptr  (_) node_ptr"
  where
    "castelement_ptr2node_ptr ptr = node_ptr.Ext (Inl ptr)"

abbreviation castelement_ptr2object_ptr :: "(_) element_ptr  (_) object_ptr"
  where
    "castelement_ptr2object_ptr ptr  castnode_ptr2object_ptr (castelement_ptr2node_ptr ptr)"

definition castnode_ptr2element_ptr :: "(_) node_ptr  (_) element_ptr option"
  where
    "castnode_ptr2element_ptr node_ptr = (case node_ptr of node_ptr.Ext (Inl element_ptr) 
                                           Some element_ptr | _  None)"

abbreviation castobject_ptr2element_ptr :: "(_) object_ptr  (_) element_ptr option"
  where
    "castobject_ptr2element_ptr ptr  (case castobject_ptr2node_ptr ptr of 
                                  Some node_ptr  castnode_ptr2element_ptr node_ptr 
                                | None  None)"

adhoc_overloading cast castelement_ptr2node_ptr castelement_ptr2object_ptr 
  castnode_ptr2element_ptr castobject_ptr2element_ptr castelement_ptr2element_ptr

consts is_element_ptr_kind :: 'a
definition is_element_ptr_kindnode_ptr :: "(_) node_ptr  bool"
  where
    "is_element_ptr_kindnode_ptr ptr = (case castnode_ptr2element_ptr ptr of Some _  True | _  False)"

abbreviation is_element_ptr_kindobject_ptr :: "(_) object_ptr  bool"
  where
    "is_element_ptr_kindobject_ptr ptr  (case cast ptr of 
                                             Some node_ptr  is_element_ptr_kindnode_ptr node_ptr 
                                           | None  False)"

adhoc_overloading is_element_ptr_kind is_element_ptr_kindobject_ptr is_element_ptr_kindnode_ptr
lemmas is_element_ptr_kind_def = is_element_ptr_kindnode_ptr_def

consts is_element_ptr :: 'a
definition is_element_ptrelement_ptr :: "(_) element_ptr  bool"
  where
    "is_element_ptrelement_ptr ptr = (case ptr of element_ptr.Ref _  True | _  False)"

abbreviation is_element_ptrnode_ptr :: "(_) node_ptr  bool"
  where
    "is_element_ptrnode_ptr ptr  (case cast ptr of 
                                   Some element_ptr  is_element_ptrelement_ptr element_ptr 
                                 | _  False)"

abbreviation is_element_ptrobject_ptr :: "(_) object_ptr  bool"
  where
    "is_element_ptrobject_ptr ptr  (case cast ptr of 
                                    Some node_ptr  is_element_ptrnode_ptr node_ptr 
                                  | None  False)"

adhoc_overloading is_element_ptr is_element_ptrobject_ptr is_element_ptrnode_ptr is_element_ptrelement_ptr
lemmas is_element_ptr_def = is_element_ptrelement_ptr_def

consts is_element_ptr_ext :: 'a
abbreviation "is_element_ptr_extelement_ptr ptr  ¬ is_element_ptrelement_ptr ptr"

abbreviation "is_element_ptr_extnode_ptr ptr  is_element_ptr_kind ptr  (¬ is_element_ptrnode_ptr ptr)"

abbreviation "is_element_ptr_extobject_ptr ptr  is_element_ptr_kind ptr  (¬ is_element_ptrobject_ptr ptr)"
adhoc_overloading is_element_ptr_ext is_element_ptr_extobject_ptr is_element_ptr_extnode_ptr


instantiation element_ptr :: (linorder) linorder
begin
definition 
  less_eq_element_ptr :: "(_::linorder) element_ptr  (_)element_ptr  bool"
  where 
    "less_eq_element_ptr x y  (case x of Ext i  (case y of Ext j  i  j | Ref _  False)
                                        | Ref i  (case y of Ext _  True | Ref j  i  j))"
definition 
  less_element_ptr :: "(_::linorder) element_ptr  (_) element_ptr  bool"
  where "less_element_ptr x y  x  y  ¬ y  x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_element_ptr_def less_element_ptr_def split: element_ptr.splits)
end

lemma is_element_ptr_ref [simp]: "is_element_ptr (element_ptr.Ref n)"
  by(simp add: is_element_ptrelement_ptr_def)

lemma element_ptr_casts_commute [simp]:
  "castnode_ptr2element_ptr node_ptr = Some element_ptr  castelement_ptr2node_ptr element_ptr = node_ptr"
  unfolding castnode_ptr2element_ptr_def castelement_ptr2node_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma element_ptr_casts_commute2 [simp]: 
  "(castnode_ptr2element_ptr (castelement_ptr2node_ptr element_ptr) = Some element_ptr)"
  by simp

lemma element_ptr_casts_commute3 [simp]:
  assumes "is_element_ptr_kindnode_ptr node_ptr"
  shows "castelement_ptr2node_ptr (the (castnode_ptr2element_ptr node_ptr)) = node_ptr"
  using assms
  by(auto simp add: is_element_ptr_kind_def castelement_ptr2node_ptr_def castnode_ptr2element_ptr_def 
      split: node_ptr.splits sum.splits)

lemma is_element_ptr_kind_obtains:
  assumes "is_element_ptr_kind node_ptr"
  obtains element_ptr where "node_ptr = castelement_ptr2node_ptr element_ptr"
  by (metis assms is_element_ptr_kind_def case_optionE element_ptr_casts_commute)

lemma is_element_ptr_kind_none:
  assumes "¬is_element_ptr_kind node_ptr"
  shows "castnode_ptr2element_ptr node_ptr = None"
  using assms
  unfolding is_element_ptr_kind_def castnode_ptr2element_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma is_element_ptr_kind_cast [simp]: 
  "is_element_ptr_kind (castelement_ptr2node_ptr element_ptr)"
  by (metis element_ptr_casts_commute is_element_ptr_kind_none option.distinct(1))

lemma castelement_ptr2node_ptr_inject [simp]: 
  "castelement_ptr2node_ptr x = castelement_ptr2node_ptr y  x = y"
  by(simp add: castelement_ptr2node_ptr_def)

lemma castnode_ptr2element_ptr_ext_none [simp]: 
  "castnode_ptr2element_ptr (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None"
  by(simp add: castnode_ptr2element_ptr_def)

lemma is_element_ptr_implies_kind [dest]: "is_element_ptrnode_ptr ptr  is_element_ptr_kindnode_ptr ptr"
  by(auto split: option.splits)

end

Theory CharacterDataPointer

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹CharacterData›
text‹In this theory, we introduce the typed pointers for the class CharacterData.›   
theory CharacterDataPointer
  imports
    ElementPointer
begin

datatype 'character_data_ptr character_data_ptr = Ref (the_ref: ref) | Ext 'character_data_ptr
register_default_tvars "'character_data_ptr character_data_ptr" 
type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr
  = "('character_data_ptr character_data_ptr + 'node_ptr, 'element_ptr) node_ptr"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr" 
type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr) object_ptr
  = "('object_ptr, 'character_data_ptr character_data_ptr + 'node_ptr, 'element_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr) object_ptr" 

definition castcharacter_data_ptr2node_ptr :: "(_) character_data_ptr  (_) node_ptr"
  where
    "castcharacter_data_ptr2node_ptr ptr = node_ptr.Ext (Inr (Inl ptr))"

abbreviation castcharacter_data_ptr2object_ptr :: "(_) character_data_ptr  (_) object_ptr"
  where
    "castcharacter_data_ptr2object_ptr ptr  castnode_ptr2object_ptr (castcharacter_data_ptr2node_ptr ptr)"

definition castnode_ptr2character_data_ptr :: "(_) node_ptr  (_) character_data_ptr option"
  where
    "castnode_ptr2character_data_ptr node_ptr = (case node_ptr of 
                        node_ptr.Ext (Inr (Inl character_data_ptr))  Some character_data_ptr
                       | _  None)"

abbreviation castobject_ptr2character_data_ptr :: "(_) object_ptr  (_) character_data_ptr option"
  where
    "castobject_ptr2character_data_ptr ptr  (case castobject_ptr2node_ptr ptr of
                               Some node_ptr  castnode_ptr2character_data_ptr node_ptr
                             | None  None)"

adhoc_overloading cast castcharacter_data_ptr2node_ptr castcharacter_data_ptr2object_ptr 
  castnode_ptr2character_data_ptr castobject_ptr2character_data_ptr

consts is_character_data_ptr_kind :: 'a
definition is_character_data_ptr_kindnode_ptr :: "(_) node_ptr  bool"
  where
    "is_character_data_ptr_kindnode_ptr ptr = (case castnode_ptr2character_data_ptr ptr 
                                             of Some _  True | _  False)"

abbreviation is_character_data_ptr_kindobject_ptr :: "(_) object_ptr  bool"
  where
    "is_character_data_ptr_kindobject_ptr ptr  (case cast ptr of 
                        Some node_ptr  is_character_data_ptr_kindnode_ptr node_ptr
                      | None  False)"

adhoc_overloading is_character_data_ptr_kind is_character_data_ptr_kindobject_ptr 
  is_character_data_ptr_kindnode_ptr
lemmas is_character_data_ptr_kind_def = is_character_data_ptr_kindnode_ptr_def

consts is_character_data_ptr :: 'a
definition is_character_data_ptrcharacter_data_ptr :: "(_) character_data_ptr  bool"
  where
    "is_character_data_ptrcharacter_data_ptr ptr = (case ptr 
                                 of character_data_ptr.Ref _  True | _  False)"

abbreviation is_character_data_ptrnode_ptr :: "(_) node_ptr  bool"
  where
    "is_character_data_ptrnode_ptr ptr  (case cast ptr of
      Some character_data_ptr  is_character_data_ptrcharacter_data_ptr character_data_ptr
    | _  False)"

abbreviation is_character_data_ptrobject_ptr :: "(_) object_ptr  bool"
  where
    "is_character_data_ptrobject_ptr ptr  (case castobject_ptr2node_ptr ptr of
      Some node_ptr  is_character_data_ptrnode_ptr node_ptr
    | None  False)"

adhoc_overloading is_character_data_ptr
  is_character_data_ptrobject_ptr is_character_data_ptrnode_ptr is_character_data_ptrcharacter_data_ptr
lemmas is_character_data_ptr_def = is_character_data_ptrcharacter_data_ptr_def

consts is_character_data_ptr_ext :: 'a
abbreviation 
  "is_character_data_ptr_extcharacter_data_ptr ptr  ¬ is_character_data_ptrcharacter_data_ptr ptr"

abbreviation "is_character_data_ptr_extnode_ptr ptr  (case castnode_ptr2character_data_ptr ptr of
  Some character_data_ptr  is_character_data_ptr_extcharacter_data_ptr character_data_ptr
| None  False)"

abbreviation "is_character_data_ptr_extobject_ptr ptr  (case castobject_ptr2node_ptr ptr of
  Some node_ptr  is_character_data_ptr_extnode_ptr node_ptr
| None  False)"

adhoc_overloading is_character_data_ptr_ext
  is_character_data_ptr_extobject_ptr is_character_data_ptr_extnode_ptr is_character_data_ptr_extcharacter_data_ptr

instantiation character_data_ptr :: (linorder) linorder
begin
definition 
  less_eq_character_data_ptr :: "(_::linorder) character_data_ptr  (_) character_data_ptr  bool"
  where 
    "less_eq_character_data_ptr x y  (case x of Ext i  (case y of Ext j  i  j | Ref _  False)
                                               | Ref i  (case y of Ext _  True | Ref j  i  j))"
definition 
  less_character_data_ptr :: "(_::linorder) character_data_ptr  (_) character_data_ptr  bool"
  where "less_character_data_ptr x y  x  y  ¬ y  x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_character_data_ptr_def less_character_data_ptr_def 
      split: character_data_ptr.splits)
end

lemma is_character_data_ptr_ref [simp]: "is_character_data_ptr (character_data_ptr.Ref n)"
  by(simp add: is_character_data_ptrcharacter_data_ptr_def)

lemma cast_element_ptr_not_character_data_ptr [simp]:
  "(castelement_ptr2node_ptr element_ptr  castcharacter_data_ptr2node_ptr character_data_ptr)"
  "(castcharacter_data_ptr2node_ptr character_data_ptr  castelement_ptr2node_ptr element_ptr)"
  unfolding castelement_ptr2node_ptr_def castcharacter_data_ptr2node_ptr_def 
  by(auto)

lemma is_character_data_ptr_kind_not_element_ptr [simp]: 
  "¬ is_character_data_ptr_kind (castelement_ptr2node_ptr element_ptr)"
  unfolding is_character_data_ptr_kind_def castelement_ptr2node_ptr_def castnode_ptr2character_data_ptr_def
  by auto
lemma is_element_ptr_kind_not_character_data_ptr [simp]: 
  "¬ is_element_ptr_kind (castcharacter_data_ptr2node_ptr character_data_ptr)"
  using is_element_ptr_kind_obtains by fastforce

lemma is_character_data_ptr_kind_cast [simp]: 
  "is_character_data_ptr_kind (castcharacter_data_ptr2node_ptr character_data_ptr)"
  by (simp add: castcharacter_data_ptr2node_ptr_def castnode_ptr2character_data_ptr_def 
      is_character_data_ptr_kindnode_ptr_def)

lemma character_data_ptr_casts_commute [simp]:
  "castnode_ptr2character_data_ptr node_ptr = Some character_data_ptr
    castcharacter_data_ptr2node_ptr character_data_ptr = node_ptr"
  unfolding castnode_ptr2character_data_ptr_def castcharacter_data_ptr2node_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma character_data_ptr_casts_commute2 [simp]:
  "(castnode_ptr2character_data_ptr (castcharacter_data_ptr2node_ptr character_data_ptr) = Some character_data_ptr)"
  by simp

lemma character_data_ptr_casts_commute3 [simp]:
  assumes "is_character_data_ptr_kindnode_ptr node_ptr"
  shows "castcharacter_data_ptr2node_ptr (the (castnode_ptr2character_data_ptr node_ptr)) = node_ptr"
  using assms
  by(auto simp add: is_character_data_ptr_kindnode_ptr_def castnode_ptr2character_data_ptr_def 
      castcharacter_data_ptr2node_ptr_def
      split: node_ptr.splits sum.splits)

lemma is_character_data_ptr_kind_obtains:
  assumes "is_character_data_ptr_kindnode_ptr node_ptr"
  obtains character_data_ptr where "castcharacter_data_ptr2node_ptr character_data_ptr = node_ptr"
  by (metis assms is_character_data_ptr_kindnode_ptr_def case_optionE 
      character_data_ptr_casts_commute)

lemma is_character_data_ptr_kind_none:
  assumes "¬is_character_data_ptr_kindnode_ptr node_ptr"
  shows "castnode_ptr2character_data_ptr node_ptr = None"
  using assms
  unfolding is_character_data_ptr_kindnode_ptr_def castnode_ptr2character_data_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma castcharacter_data_ptr2node_ptr_inject [simp]: 
  "castcharacter_data_ptr2node_ptr x = castcharacter_data_ptr2node_ptr y  x = y"
  by(simp add: castcharacter_data_ptr2node_ptr_def)

lemma castnode_ptr2character_data_ptr_ext_none [simp]: 
  "castnode_ptr2character_data_ptr (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None"
  by(simp add: castnode_ptr2character_data_ptr_def)

end

Theory DocumentPointer

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Document›
text‹In this theory, we introduce the typed pointers for the class Document.›   
theory DocumentPointer
  imports
    CharacterDataPointer
begin

datatype 'document_ptr document_ptr = Ref (the_ref: ref) | Ext 'document_ptr
register_default_tvars "'document_ptr document_ptr" 
type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr) object_ptr
  = "('document_ptr document_ptr + 'object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr) object_ptr" 

definition castdocument_ptr2object_ptr :: "(_)document_ptr  (_) object_ptr"
  where
    "castdocument_ptr2object_ptr ptr = object_ptr.Ext (Inr (Inl ptr))"

definition castobject_ptr2document_ptr :: "(_) object_ptr  (_) document_ptr option"
  where
    "castobject_ptr2document_ptr ptr = (case ptr of 
                    object_ptr.Ext (Inr (Inl document_ptr))  Some document_ptr 
                  | _  None)"

adhoc_overloading cast castdocument_ptr2object_ptr castobject_ptr2document_ptr


definition is_document_ptr_kind :: "(_) object_ptr  bool"
  where
    "is_document_ptr_kind ptr = (case castobject_ptr2document_ptr ptr of 
                                     Some _  True | None  False)"

consts is_document_ptr :: 'a
definition is_document_ptrdocument_ptr :: "(_) document_ptr  bool"
  where
    "is_document_ptrdocument_ptr ptr = (case ptr of document_ptr.Ref _  True | _  False)"

abbreviation is_document_ptrobject_ptr :: "(_) object_ptr  bool"
  where
    "is_document_ptrobject_ptr ptr  (case castobject_ptr2document_ptr ptr of
      Some document_ptr  is_document_ptrdocument_ptr document_ptr
    | None  False)"
adhoc_overloading is_document_ptr is_document_ptrobject_ptr is_document_ptrdocument_ptr
lemmas is_document_ptr_def = is_document_ptrdocument_ptr_def

consts is_document_ptr_ext :: 'a
abbreviation "is_document_ptr_extdocument_ptr ptr  ¬ is_document_ptrdocument_ptr ptr"

abbreviation "is_document_ptr_extobject_ptr ptr  (case castobject_ptr2document_ptr ptr of
  Some document_ptr  is_document_ptr_extdocument_ptr document_ptr
| None  False)"
adhoc_overloading is_document_ptr_ext is_document_ptr_extobject_ptr is_document_ptr_extdocument_ptr

instantiation document_ptr :: (linorder) linorder
begin
definition less_eq_document_ptr :: "(_::linorder) document_ptr  (_) document_ptr  bool"
  where "less_eq_document_ptr x y  (case x of Ext i  (case y of Ext j  i  j | Ref _  False)
                                             | Ref i  (case y of Ext _  True | Ref j  i  j))"
definition less_document_ptr :: "(_::linorder) document_ptr  (_) document_ptr  bool"
  where "less_document_ptr x y  x  y  ¬ y  x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_document_ptr_def less_document_ptr_def split: document_ptr.splits)
end

lemma is_document_ptr_ref [simp]: "is_document_ptr (document_ptr.Ref n)"
  by(simp add: is_document_ptrdocument_ptr_def)

lemma cast_document_ptr_not_node_ptr [simp]:
  "castdocument_ptr2object_ptr document_ptr  castnode_ptr2object_ptr node_ptr"
  "castnode_ptr2object_ptr node_ptr  castdocument_ptr2object_ptr document_ptr"
  unfolding castdocument_ptr2object_ptr_def castnode_ptr2object_ptr_def 
  by auto

lemma document_ptr_no_node_ptr_cast [simp]: 
  "¬ is_document_ptr_kind (castnode_ptr2object_ptr node_ptr)"
  by(simp add: castnode_ptr2object_ptr_def castobject_ptr2document_ptr_def is_document_ptr_kind_def)
lemma node_ptr_no_document_ptr_cast [simp]: 
  "¬ is_node_ptr_kind (castdocument_ptr2object_ptr document_ptr)"
  using is_node_ptr_kind_obtains by fastforce

lemma document_ptr_document_ptr_cast [simp]: 
  "is_document_ptr_kind (castdocument_ptr2object_ptr document_ptr)"
  by (simp add: castdocument_ptr2object_ptr_def cast