Theory Store

(*  Title:       Jive Data and Store Model
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

section ‹Store›

theory Store
imports Location
begin

subsection ‹New›
text ‹The store provides a uniform interface to allocate new objects and
new arrays. The constructors of this datatype distinguish both cases.
›
datatype New = new_instance CTypeId    ― ‹New object, can only be of a concrete class type› 
             | new_array Arraytype nat ― ‹New array with given size›

text ‹The discriminator ‹isNewArr› can be used to distinguish both 
kinds of newly created elements.
›

definition isNewArr :: "New ⇒ bool" where
"isNewArr t = (case t of 
                 new_instance C ⇒ False     
               | new_array T l ⇒ True)"   

lemma isNewArr_simps [simp]:
"isNewArr (new_instance C) = False"
"isNewArr (new_array T l)  = True"
  by (simp_all add: isNewArr_def)

text ‹The function ‹typeofNew› yields the type of the newly created
element.›

definition typeofNew :: "New ⇒ Javatype" where
"typeofNew n = (case n of
                  new_instance C ⇒ CClassT C
                | new_array T l  ⇒ ArrT T)"

lemma typeofNew_simps:
"typeofNew (new_instance C) = CClassT C"
"typeofNew (new_array T l)  = ArrT T"
  by (simp_all add: typeofNew_def)

subsection ‹The Definition of the Store›

text ‹In our store model, all objects\footnote{In the following, the term ``objects'' 
includes arrays. This keeps the explanations compact.}
of all classes exist at all times, but only those objects that have already been allocated
are alive. Objects cannot be deallocated, thus an object that once gained
the aliveness status cannot lose it later on.
\\[12pt]
 To model the store, we need two functions that give us fresh object Id's for 
the allocation of new objects (function ‹newOID›) and arrays
(function ‹newAID›) as well as a function that maps locations to
their contents (function ‹vals›).›

record StoreImpl = newOID :: "CTypeId ⇒ ObjectId"
                   newAID :: "Arraytype ⇒ ObjectId"
                   vals   :: "Location ⇒ Value"

text ‹The function ‹aliveImpl› determines for a given value whether
it is alive in a given store.
›

definition aliveImpl::"Value ⇒ StoreImpl ⇒ bool" where
"aliveImpl x s = (case x of
                    boolV b  ⇒ True
                  | intgV i  ⇒ True
                  | shortV s  ⇒ True
                  | byteV by  ⇒ True
                  | objV C a ⇒ (a < newOID s C)
                  | arrV T a ⇒ (a < newAID s T)
                  | nullV    ⇒ True)"


text ‹The store itself is defined as new type. The store ensures
and maintains the following 
properties: All stored values are alive; for all locations whose values are
not alive, the store yields the location type's init value; and
all stored values are of the correct type (i.e.~of the type of the location
they are stored in).
›

definition "Store = {s. (∀ l. aliveImpl (vals s l) s) ∧ 
                  (∀ l. ¬ aliveImpl (ref l) s ⟶ vals s l = init (ltype l)) ∧
                  (∀ l. typeof (vals s l) ≤ ltype l)}"

typedef Store = Store
  unfolding Store_def
  apply (rule exI [where ?x="⦇ newOID = (λC. 0),
                          newAID = (λT. 0),
                          vals = (λl. init (ltype l)) ⦈"])
  apply (auto simp add: aliveImpl_def init_def NullT_leaf_array split: Javatype.splits)
  done

text ‹One might also model the Store as axiomatic type class and prove that the type StoreImpl belongs
to this type class. This way, a clearer separation between the axiomatic description of the store and its
properties on the one hand and the realization that has been chosen in this formalization on the other hand
could be achieved. Additionally, it would be easier to make use of  different store implementations that
might have different additional features. This separation remains to be performed as future work.
›

subsection‹The Store Interface›

text ‹The Store interface consists of five functions:
‹access› to read the value that is stored at a location;
‹alive› to test whether a value is alive in the store;
‹alloc› to allocate a new element in the store;
‹new› to read the value of a newly allocated element;
‹update› to change the value that is stored at a location.
›

consts access:: "Store ⇒ Location ⇒ Value"  ("_@@_" [71,71] 70)     
       alive:: "Value ⇒ Store ⇒ bool"
       alloc:: "Store ⇒ New ⇒ Store" 
       new:: "Store ⇒ New ⇒ Value"
       update:: "Store ⇒ Location ⇒ Value ⇒ Store"
       
nonterminal smodifybinds and smodifybind
syntax
  "_smodifybind" :: "['a, 'a]     ⇒ smodifybind" ("(2_ :=/ _)")
  ""         :: "smodifybind ⇒ smodifybinds"     ("_")
  ""         :: "CTypeId ⇒ smodifybind"          ("_")
  "_smodifybinds":: "[smodifybind, smodifybinds] => smodifybinds" ("_,/ _")
  "_sModify"  :: "['a, smodifybinds] ⇒ 'a"       ("_/⟨(_)⟩" [900,0] 900)
translations
  "_sModify s (_smodifybinds b bs)"  == "_sModify (_sModify s b) bs"
  "s⟨x:=y⟩"                          == "CONST update s x y"
  "s⟨c⟩"                             == "CONST alloc s c" 
 

text ‹With this syntactic setup we can write chains of (array) updates and 
allocations like in the
following term  
@{term "s⟨new_instance Node,x:=y,z:=intgV 3,new_array IntgAT 3,a.[i]:=intgV 4,k:=boolV True⟩"}. 
›

text ‹In the following, the definitions of the five store interface functions and some lemmas 
about them are given.›

overloading alive ≡ alive
begin
  definition alive where "alive x s ≡ aliveImpl x (Rep_Store s)"
end

lemma alive_trivial_simps [simp,intro]:
"alive (boolV b) s"
"alive (intgV i) s"
"alive (shortV sh) s"
"alive (byteV by) s"
"alive nullV     s"
  by (simp_all add: alive_def aliveImpl_def)

overloading
  access ≡ access
  update ≡ update
  alloc ≡ alloc
  new ≡ new
begin

definition access
  where "access s l ≡ vals (Rep_Store s) l"

definition update
  where "update s l v ≡
    if alive (ref l) s ∧ alive v s ∧ typeof v ≤ ltype l 
    then Abs_Store ((Rep_Store s)⦇vals:=(vals (Rep_Store s))(l:=v)⦈)
    else s"

definition alloc
  where "alloc s t ≡
    (case t of 
       new_instance C 
        ⇒ Abs_Store 
            ((Rep_Store s)⦇newOID := λ D. if C=D 
                              then Suc (newOID (Rep_Store s) C) 
                              else newOID (Rep_Store s) D⦈)
     | new_array T l
        ⇒ Abs_Store
            ((Rep_Store s)⦇newAID := λ S. if T=S 
                             then Suc (newAID (Rep_Store s) T)
                             else newAID (Rep_Store s) S,
                           vals :=  (vals (Rep_Store s))
                                      (arrLenLoc T (newAID (Rep_Store s) T) 
                                        := intgV (int l))⦈))"

definition new
  where "new s t ≡
    (case t of
      new_instance C ⇒ objV C (newOID (Rep_Store s) C)
    | new_array T l  ⇒ arrV T (newAID (Rep_Store s) T))"

end

text ‹The predicate ‹wts› tests whether the store is well-typed.›

definition
wts :: "Store ⇒ bool" where
"wts OS = (∀ (l::Location) . (typeof (OS@@l)) ≤ (ltype l))"


subsection ‹Derived Properties of the Store›

text ‹In this subsection, a number of lemmas formalize various properties of the Store.
Especially the 13 axioms are proven that must hold for a modelling of a Store 
(see \<^cite>‹‹p. 45› in "Poetzsch-Heffter97specification"›). They are labeled with
Store1 to Store13.›

lemma alive_init [simp,intro]: "alive (init T) s"
  by (cases T) (simp_all add: alive_def aliveImpl_def) 

lemma alive_loc [simp]: 
  "⟦isObjV x; typeof x ≤ dtype f⟧ ⟹ alive (ref (x..f)) s = alive x s"
  by (cases x) (simp_all)

lemma alive_arr_loc [simp]: 
  "isArrV x ⟹ alive (ref (x.[i])) s = alive x s"
  by (cases x) (simp_all)

lemma alive_arr_len [simp]: 
  "isArrV x ⟹ alive (ref (arr_len x)) s = alive x s"
  by (cases x) (simp_all)

lemma ref_arr_len_new [simp]: 
  "ref (arr_len (new s (new_array T n))) = new s (new_array T n)"
  by (simp add: new_def)

lemma ref_arr_loc_new [simp]: 
  "ref ((new s (new_array T n)).[i]) = new s (new_array T n)"
  by (simp add: new_def)

lemma ref_loc_new [simp]: "CClassT C ≤ dtype f 
  ⟹ ref ((new s (new_instance C))..f) = new s (new_instance C)"
  by (simp add: new_def)

lemma access_type_safe [simp,intro]: "typeof (s@@l) ≤ ltype l" 
proof -
  have "Rep_Store s ∈ Store"    
    by (rule Rep_Store)
  thus ?thesis
    by (auto simp add: access_def Store_def)
qed

text ‹The store is well-typed by construction.›
lemma always_welltyped_store: "wts OS"
  by (simp add: wts_def access_type_safe)


text ‹Store8›
lemma alive_access [simp,intro]: "alive (s@@l) s"
proof -
  have "Rep_Store s ∈ Store"
    by (rule Rep_Store)
  thus ?thesis
    by (auto simp add: access_def Store_def alive_def aliveImpl_def)
qed

text ‹Store3›
lemma access_unalive [simp]: 
  assumes unalive: "¬ alive (ref l) s" 
  shows "s@@l = init (ltype l)"
proof -
  have "Rep_Store s ∈ Store"
    by (rule Rep_Store)
  with unalive show ?thesis
    by (simp add: access_def Store_def alive_def aliveImpl_def)
qed


lemma update_induct:
  assumes skip: "P s"
  assumes update: "⟦alive (ref l) s; alive v s; typeof v ≤ ltype l⟧ ⟹
               P (Abs_Store ((Rep_Store s)⦇vals:=(vals (Rep_Store s))(l:=v)⦈))" 
  shows "P (s⟨l:=v⟩)"
  using update skip 
  by (simp add: update_def)

lemma vals_update_in_Store:
  assumes alive_l: "alive (ref l) s" 
  assumes alive_y: "alive y s" 
  assumes type_conform: "typeof y ≤ ltype l"
  shows "(Rep_Store s⦇vals := (vals (Rep_Store s))(l := y)⦈) ∈ Store" 
  (is "?s_upd ∈ Store")
proof -
  have s: "Rep_Store s ∈ Store"
    by (rule Rep_Store)
  have alloc_eq: "newOID ?s_upd = newOID (Rep_Store s)"
    by simp
  have "∀ l. aliveImpl (vals ?s_upd l) ?s_upd"
  proof 
    fix k
    show "aliveImpl (vals ?s_upd k) ?s_upd"
    proof (cases "k=l")
      case True
      with alive_y show ?thesis
        by (simp add: alloc_eq alive_def aliveImpl_def split: Value.splits)
    next
      case False
      from s have "∀ l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
        by (simp add: Store_def)
      with False show ?thesis
        by (simp add: aliveImpl_def split: Value.splits)
    qed
  qed
  moreover
  have "∀ l. ¬ aliveImpl (ref l) ?s_upd ⟶ vals ?s_upd l = init (ltype l)"
  proof (intro allI impI)
    fix k
    assume unalive: "¬ aliveImpl (ref k) ?s_upd"
    show "vals ?s_upd k = init (ltype k)"
    proof -
      from unalive alive_l
      have "k≠l"
        by (auto simp add: alive_def aliveImpl_def split: Value.splits)
      hence "vals ?s_upd k = vals (Rep_Store s) k"
        by simp
      moreover from unalive 
      have "¬ aliveImpl (ref k) (Rep_Store s)"
        by (simp add: aliveImpl_def split: Value.splits)
      ultimately show ?thesis
        using s by (simp add: Store_def)
    qed
  qed
  moreover
  have "∀ l. typeof (vals ?s_upd l) ≤ ltype l"
  proof
    fix k show "typeof (vals ?s_upd k) ≤ ltype k"
    proof (cases "k=l")
      case True
      with type_conform show ?thesis
        by simp
    next
      case False
      hence "vals ?s_upd k = vals (Rep_Store s) k"
        by simp
      with s show ?thesis
        by (simp add: Store_def)
    qed
  qed
  ultimately show ?thesis
    by (simp add: Store_def)
qed

text ‹Store6›
lemma alive_update_invariant [simp]: "alive x (s⟨l:=y⟩) = alive x s"
proof (rule update_induct)
  show "alive x s = alive x s"..
next
  assume "alive (ref l) s" "alive y s" "typeof y ≤ ltype l"
  hence "Rep_Store 
          (Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := y)⦈))
         = Rep_Store s⦇vals := (vals (Rep_Store s))(l := y)⦈"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  thus "alive x
         (Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := y)⦈)) =
        alive x s"
    by (simp add: alive_def aliveImpl_def split: Value.split)
qed

text ‹Store1›
lemma access_update_other [simp]: 
  assumes neq_l_m: "l ≠ m" 
  shows "s⟨l:=x⟩@@m = s@@m"
proof (rule update_induct)
  show "s@@m = s@@m" ..
next
  assume "alive (ref l) s" "alive x s" "typeof x ≤ ltype l"
  hence "Rep_Store 
          (Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈))
         = Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  with neq_l_m 
  show "Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈)@@m = s@@m"
    by (auto simp add: access_def)
qed

text ‹Store2›
lemma update_access_same [simp]: 
  assumes alive_l: "alive (ref l) s" 
  assumes alive_x: "alive x s" 
  assumes widen_x_l: "typeof x ≤ ltype l"
  shows "s⟨l:=x⟩@@l = x"
proof -
  from alive_l alive_x widen_x_l
  have "Rep_Store 
          (Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈))
         = Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈"
    by (rule vals_update_in_Store [THEN Abs_Store_inverse])
  hence "Abs_Store (Rep_Store s⦇vals := (vals (Rep_Store s))(l := x)⦈)@@l = x"
    by (simp add: access_def)
  with alive_l alive_x widen_x_l 
  show ?thesis
    by (simp add: update_def)
qed

text ‹Store4›
lemma update_unalive_val [simp,intro]: "¬ alive x s ⟹ s⟨l:=x⟩ = s"
  by (simp add: update_def)

lemma update_unalive_loc [simp,intro]: "¬ alive (ref l) s ⟹ s⟨l:=x⟩ = s"
  by (simp add: update_def)

lemma update_type_mismatch [simp,intro]: "¬ typeof x ≤ ltype l ⟹ s⟨l:=x⟩ = s"
  by (simp add: update_def)


text ‹Store9›
lemma alive_primitive [simp,intro]: "isprimitive (typeof x) ⟹ alive x s"
  by (cases x) (simp_all)

text ‹Store10›
lemma new_unalive_old_Store [simp]: "¬ alive (new s t) s"
  by (cases t) (simp_all add: alive_def aliveImpl_def new_def)

lemma alloc_new_instance_in_Store:
"(Rep_Store s⦇newOID := λD. if C = D
                                   then Suc (newOID (Rep_Store s) C)
                                   else newOID (Rep_Store s) D⦈) ∈ Store"
(is "?s_alloc ∈ Store")
proof -
  have s: "Rep_Store s ∈ Store"
    by (rule Rep_Store)
  hence "∀ l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
    by (simp add: Store_def)
  then
  have "∀ l. aliveImpl (vals ?s_alloc l) ?s_alloc"
    by (auto intro: less_SucI simp add: aliveImpl_def split: Value.splits)
  moreover
  have "∀ l. ¬ aliveImpl (ref l) ?s_alloc ⟶ vals ?s_alloc l = init (ltype l)"
  proof (intro allI impI)
    fix l
    assume "¬ aliveImpl (ref l) ?s_alloc"
    hence "¬ aliveImpl (ref l) (Rep_Store s)"
      by (simp add: aliveImpl_def split: Value.splits if_split_asm)
    with s have "vals (Rep_Store s) l = init (ltype l)"
      by (simp add: Store_def)
    thus "vals ?s_alloc l = init (ltype l)"
      by simp
  qed
  moreover 
  from s have "∀ l. typeof (vals ?s_alloc l) ≤ ltype l"
    by (simp add: Store_def)
  ultimately
  show ?thesis
    by (simp add: Store_def)
qed

lemma alloc_new_array_in_Store:
"(Rep_Store s ⦇newAID :=
                  λS. if T = S
                      then Suc (newAID (Rep_Store s) T)
                      else newAID (Rep_Store s) S,
               vals := (vals (Rep_Store s))
                         (arrLenLoc T
                           (newAID (Rep_Store s) T) :=
                           intgV (int n))⦈) ∈ Store"
(is "?s_alloc ∈ Store")
proof -
  have s: "Rep_Store s ∈ Store"
    by (rule Rep_Store)
  have "∀ l. aliveImpl (vals ?s_alloc l) ?s_alloc"
  proof 
    fix l show "aliveImpl (vals ?s_alloc l) ?s_alloc"
    proof (cases "l = arrLenLoc T (newAID (Rep_Store s) T)")
      case True
      thus ?thesis
        by (simp add: aliveImpl_def split: Value.splits)
    next
      case False
      from s have "∀ l. aliveImpl (vals (Rep_Store s) l) (Rep_Store s)"
        by (simp add: Store_def)
      with False show ?thesis
        by (auto intro: less_SucI simp add: aliveImpl_def split: Value.splits)
    qed
  qed
  moreover
  have "∀ l. ¬ aliveImpl (ref l) ?s_alloc ⟶ vals ?s_alloc l = init (ltype l)"
  proof (intro allI impI)
    fix l
    assume unalive: "¬ aliveImpl (ref l) ?s_alloc"
    show "vals ?s_alloc l = init (ltype l)"
    proof (cases "l = arrLenLoc T (newAID (Rep_Store s) T)")
      case True
      with unalive show ?thesis by (simp add: aliveImpl_def)
    next
      case False
      from unalive
      have "¬ aliveImpl (ref l) (Rep_Store s)"
        by (simp add: aliveImpl_def split: Value.splits if_split_asm)
      with s have "vals (Rep_Store s) l = init (ltype l)"
        by (simp add: Store_def)
      with False show ?thesis 
        by simp
    qed
  qed
  moreover 
  from s have "∀ l. typeof (vals ?s_alloc l) ≤ ltype l"
    by (simp add: Store_def)
  ultimately
  show ?thesis
    by (simp add: Store_def)
qed


lemma new_alive_alloc [simp,intro]: "alive (new s t) (s⟨t⟩)"
proof (cases t)
  case new_instance thus ?thesis 
    by (simp add: alive_def aliveImpl_def new_def alloc_def
                  alloc_new_instance_in_Store [THEN Abs_Store_inverse])
next
  case new_array thus ?thesis
    by (simp add: alive_def aliveImpl_def new_def alloc_def
                  alloc_new_array_in_Store [THEN Abs_Store_inverse])
qed
 
lemma value_class_inhabitants: 
"(∀x. typeof x = CClassT typeId ⟶ P x) = (∀ a. P (objV typeId a))"
  (is "(∀ x. ?A x) = ?B")
proof 
  assume "∀ x. ?A x" thus "?B"
    by simp
next
  assume B: "?B" show "∀ x. ?A x"
  proof
    fix x from B show "?A x"
      by (cases x) auto
  qed
qed
   
lemma value_array_inhabitants: 
"(∀x. typeof x = ArrT typeId ⟶ P x) = (∀ a. P (arrV typeId a))"
  (is "(∀ x. ?A x) = ?B")
proof 
  assume "∀ x. ?A x" thus "?B"
    by simp
next
  assume B: "?B" show "∀ x. ?A x"
  proof
    fix x from B show "?A x"
      by (cases x) auto
  qed
qed


text ‹The following three lemmas are helper lemmas that are not related to the store theory.
They might as well be stored in a separate helper theory.
›

lemma le_Suc_eq: "(∀a. (a < Suc n) = (a < Suc m)) = (∀a. (a < n) = (a < m))"
 (is "(∀a. ?A a) = (∀ a. ?B a)")
proof
  assume "∀a. ?A a" thus "∀ a. ?B a"
    by fastforce
next
  assume B: "∀ a. ?B a"
  show "∀a. ?A a"
  proof
    fix a 
    from B show "?A a"
      by (cases a) simp_all
  qed
qed

lemma all_le_eq_imp_eq: "⋀ c::nat. (∀a. (a < d) = (a < c)) ⟶ (d = c)" 
proof (induct d)
  case 0 thus ?case by fastforce
next
  case (Suc n c)
  thus ?case
    by (cases c) (auto simp add: le_Suc_eq)
qed
 
lemma all_le_eq: "(∀ a::nat. (a < d) = (a < c)) = (d = c)"
using all_le_eq_imp_eq by auto

text ‹Store11›
lemma typeof_new: "typeof (new s t) = typeofNew t"
  by (cases t) (simp_all add: new_def typeofNew_def)

text ‹Store12›
lemma new_eq: "(new s1 t = new s2 t) = 
                 (∀ x. typeof x = typeofNew t ⟶ alive x s1 = alive x s2)"
by (cases t)
   (auto simp add: new_def typeofNew_def alive_def aliveImpl_def
                   value_class_inhabitants value_array_inhabitants all_le_eq)

lemma new_update [simp]: "new (s⟨l:=x⟩) t = new s t"
  by (simp add: new_eq)

lemma alive_alloc_propagation: 
  assumes alive_s: "alive x s" shows  "alive x (s⟨t⟩)"
proof (cases t)
  case new_instance with alive_s show ?thesis
    by (cases x) 
       (simp_all add: alive_def aliveImpl_def alloc_def 
                      alloc_new_instance_in_Store [THEN Abs_Store_inverse])
next
  case new_array with alive_s show ?thesis
    by (cases x) 
       (simp_all add: alive_def aliveImpl_def alloc_def 
                      alloc_new_array_in_Store [THEN Abs_Store_inverse])
qed
  
text ‹Store7› 
lemma alive_alloc_exhaust: "alive x (s⟨t⟩) = (alive x s ∨ (x = new s t))"
proof 
  assume alive_alloc: "alive x (s⟨t⟩)"
  show "alive x s ∨ x = new s t"
  proof (cases t)
    case (new_instance C) 
    with alive_alloc show ?thesis 
      by (cases x) (auto split: if_split_asm 
                         simp add: alive_def new_def alloc_def aliveImpl_def
                              alloc_new_instance_in_Store [THEN Abs_Store_inverse])
  next
    case (new_array T l)
    with alive_alloc show ?thesis
      by (cases x) (auto split: if_split_asm
                         simp add: alive_def new_def alloc_def aliveImpl_def
                         alloc_new_array_in_Store [THEN Abs_Store_inverse])
  qed
next
  assume "alive x s ∨ x = new s t"
  then show "alive x (s⟨t⟩)"
  proof 
    assume "alive x s" thus ?thesis by (rule alive_alloc_propagation)
  next
    assume new: "x=new s t" show ?thesis 
    proof (cases t)
      case new_instance with new show ?thesis
        by (simp add: alive_def aliveImpl_def new_def alloc_def
                      alloc_new_instance_in_Store [THEN Abs_Store_inverse])
    next
      case new_array with new show ?thesis
        by (simp add: alive_def aliveImpl_def new_def alloc_def
                      alloc_new_array_in_Store [THEN Abs_Store_inverse])
    qed
  qed
qed

lemma alive_alloc_cases [consumes 1]: 
  "⟦alive x (s⟨t⟩); alive x s ⟹ P; x=new s t ⟹ P⟧
   ⟹ P"
  by (auto simp add: alive_alloc_exhaust)

lemma aliveImpl_vals_independent: "aliveImpl x (s⦇vals := z⦈) = aliveImpl x s"
  by (cases x) (simp_all add: aliveImpl_def)

lemma access_arr_len_new_alloc [simp]: 
  "s⟨new_array T l⟩@@arr_len (new s (new_array T l)) = intgV (int l)"
  by (subst access_def) 
     (simp add: new_def alloc_def alive_def 
                alloc_new_array_in_Store [THEN Abs_Store_inverse] access_def)

lemma access_new [simp]:
  assumes ref_new: "ref l = new s t"
  assumes no_arr_len: "isNewArr t ⟶ l ≠ arr_len (new s t)"
  shows "s⟨t⟩@@l = init (ltype l)"
proof -
  from ref_new 
  have "¬ alive (ref l) s"
    by simp
  hence "s@@l = init (ltype l)"
    by simp
  moreover
  from ref_new
  have "alive (ref l) (s⟨t⟩)"
    by simp
  moreover
  from no_arr_len
  have "vals (Rep_Store (s⟨t⟩)) l = s@@l"
    by (cases t)
       (simp_all add: alloc_def new_def access_def
                  alloc_new_instance_in_Store [THEN Abs_Store_inverse] 
                  alloc_new_array_in_Store [THEN Abs_Store_inverse] )
  ultimately show "s⟨t⟩@@l = init (ltype l)"
    by (subst access_def) (simp)
qed

text ‹Store5. We have to take into account that the length of an array
is changed during allocation.›
lemma access_alloc [simp]:
  assumes no_arr_len_new: "isNewArr t ⟶ l ≠ arr_len (new s t)"
  shows "s⟨t⟩@@l = s@@l"
proof -
  show ?thesis
  proof (cases "alive (ref l) (s⟨t⟩)")
    case True
    then
    have access_alloc_vals: "s⟨t⟩@@l = vals (Rep_Store (s⟨t⟩)) l"
      by (simp add: access_def alloc_def)
    from True show ?thesis
    proof (cases rule: alive_alloc_cases)
      assume alive_l_s: "alive (ref l) s"
      with new_unalive_old_Store
      have l_not_new: "ref l ≠ new s t"
        by fastforce
      hence "vals (Rep_Store (s⟨t⟩)) l = s@@l"
        by (cases t) 
           (auto simp add: alloc_def new_def access_def 
                 alloc_new_instance_in_Store [THEN Abs_Store_inverse] 
                 alloc_new_array_in_Store [THEN Abs_Store_inverse])
      with access_alloc_vals 
      show ?thesis 
        by simp
    next
      assume ref_new: "ref l = new s t"
      with no_arr_len_new
      have "s⟨t⟩@@l = init (ltype l)"
        by (simp add: access_new)
      moreover
      from ref_new have "s@@l = init (ltype l)"
        by simp
      ultimately
      show ?thesis by simp
    qed
  next
    case False
    hence "s⟨t⟩@@l = init (ltype l)"
      by (simp)
    moreover
    from False have "¬ alive (ref l) s"
      by (auto simp add: alive_alloc_propagation)
    hence "s@@l = init (ltype l)"
      by simp
    ultimately show ?thesis by simp
  qed
qed
   
text ‹Store13›
lemma Store_eqI: 
  assumes eq_alive: "∀ x. alive x s1 = alive x s2" 
  assumes eq_access: "∀ l. s1@@l = s2@@l"
  shows "s1=s2"
proof (cases "s1=s2")
  case True thus ?thesis .
next
  case False note neq_s1_s2 = this
  show ?thesis
  proof (cases "newOID (Rep_Store s1) = newOID (Rep_Store s2)")
    case False
    have "∃ C. newOID (Rep_Store s1) C ≠ newOID (Rep_Store s2) C"
    proof (rule ccontr)
      assume "¬ (∃C. newOID (Rep_Store s1) C ≠ newOID (Rep_Store s2) C)"
      then have "newOID (Rep_Store s1) = newOID (Rep_Store s2)"
        by (blast intro: ext)
      with False show False ..
    qed
    with eq_alive obtain C 
      where "newOID (Rep_Store s1) C ≠ newOID (Rep_Store s2) C"
            "∀ a. alive (objV C a) s1 = alive (objV C a) s2" by auto
    then show ?thesis
      by (simp add: all_le_eq alive_def aliveImpl_def)
  next
    case True note eq_newOID = this
    show ?thesis
    proof (cases "newAID (Rep_Store s1) = newAID (Rep_Store s2)")
      case False
      have "∃ T. newAID (Rep_Store s1) T ≠ newAID (Rep_Store s2) T"
      proof (rule ccontr)
        assume "¬ (∃T. newAID (Rep_Store s1) T ≠ newAID (Rep_Store s2) T)"
        then have "newAID (Rep_Store s1) = newAID (Rep_Store s2)"
          by (blast intro: ext)
        with False show False ..
      qed
      with eq_alive obtain T 
        where "newAID (Rep_Store s1) T ≠ newAID (Rep_Store s2) T"
              "∀ a. alive (arrV T a) s1 = alive (arrV T a) s2" by auto
      then show ?thesis
        by (simp add: all_le_eq alive_def aliveImpl_def)
    next
      case True note eq_newAID = this
      show ?thesis
      proof (cases "vals (Rep_Store s1) = vals (Rep_Store s2)")
        case True
        with eq_newOID eq_newAID 
        have "(Rep_Store s1) = (Rep_Store s2)"
          by (cases "Rep_Store s1",cases "Rep_Store s2") simp
        hence "s1=s2"
          by (simp add: Rep_Store_inject)
        with neq_s1_s2 show ?thesis
          by simp
      next
        case False
        have "∃ l. vals (Rep_Store s1) l ≠ vals (Rep_Store s2) l"
        proof (rule ccontr)
          assume "¬ (∃l. vals (Rep_Store s1) l ≠ vals (Rep_Store s2) l)"
          hence "vals (Rep_Store s1) = vals (Rep_Store s2)"
            by (blast intro: ext)
          with False show False ..
        qed
        then obtain l
          where "vals (Rep_Store s1) l ≠ vals (Rep_Store s2) l"
          by auto
        with eq_access have "False"
          by (simp add: access_def)
        thus ?thesis ..
      qed
    qed
  qed
qed

text ‹Lemma 3.1 in [Poetzsch-Heffter97]. The proof of this lemma is quite an
impressive demostration of readable Isar proofs since it closely follows the
textual proof.›
lemma comm: 
  assumes neq_l_new: "ref l ≠ new s t"
  assumes neq_x_new: "x ≠ new s t"
  shows "s⟨t⟩⟨l:=x⟩ = s⟨l:=x⟩⟨t⟩"
proof (rule Store_eqI [rule_format])
  fix y
  show "alive y (s⟨t⟩⟨l:=x⟩) = alive y (s⟨l:=x⟩⟨t⟩)"                          
  proof -
    have "alive y (s⟨t⟩⟨l:=x⟩) = alive y (s⟨t⟩)"
      by (rule alive_update_invariant)
    also have "… = (alive y s ∨ (y = new s t))"
      by (rule alive_alloc_exhaust)
    also have "… = (alive y (s⟨l:=x⟩) ∨ y = new s t)"
      by (simp only: alive_update_invariant)
    also have "… = (alive y (s⟨l:=x⟩) ∨ y = new (s⟨l:=x⟩) t)"
    proof -
      have "new s t = new (s⟨l:=x⟩) t"
        by simp
      thus ?thesis by simp
    qed
    also have "… = alive y (s⟨l:=x⟩⟨t⟩)"
      by (simp add: alive_alloc_exhaust)
    finally show ?thesis .
  qed
next
  fix k
  show "s⟨t⟩⟨l := x⟩@@k = s⟨l := x⟩⟨t⟩@@k"
  proof (cases "l=k")
    case False note neq_l_k = this
    show ?thesis
    proof (cases "isNewArr t ⟶ k ≠ arr_len (new s t)")
      case True
      from neq_l_k 
      have  "s⟨t⟩⟨l := x⟩@@k = s⟨t⟩@@k" by simp
      also from True 
      have "… = s@@k" by simp
      also from neq_l_k 
      have "… = s⟨l:=x⟩@@k" by simp
      also from True
      have "… = s⟨l := x⟩⟨t⟩@@k"  by simp
      finally show ?thesis .
    next
      case False
      then obtain T n where 
        t: "t=new_array T n" and k: "k=arr_len (new s (new_array T n))"
        by (cases t) auto
      from k have k': "k=arr_len (new (s⟨l := x⟩) (new_array T n))"
        by simp
      from neq_l_k 
      have  "s⟨t⟩⟨l := x⟩@@k = s⟨t⟩@@k" by simp
      also from t k 
      have "… = intgV (int n)"
        by simp
      also from t k'
      have "… = s⟨l := x⟩⟨t⟩@@k"
        by (simp del: new_update)
      finally show ?thesis .
    qed
  next
    case True note eq_l_k = this
    have lemma_3_1: 
      "ref l ≠ new s t ⟹ alive (ref l) (s⟨t⟩) = alive (ref l) s"         
      by (simp add: alive_alloc_exhaust)
    have lemma_3_2: 
      "x ≠ new s t ⟹ alive x (s⟨t⟩) = alive x s"    
      by (simp add: alive_alloc_exhaust)
    have lemma_3_3: "s⟨l:=x,t⟩@@l = s⟨l:=x⟩@@l"
    proof -
      from neq_l_new have "ref l ≠ new (s⟨l:=x⟩) t"
        by simp
      hence "isNewArr t ⟶ l ≠ arr_len (new (s⟨l:=x⟩) t)"
        by (cases t) auto
      thus ?thesis
        by (simp)
    qed
    show ?thesis
    proof (cases "alive x s")
      case True note alive_x = this
      show ?thesis
      proof (cases "alive (ref l) s")
        case True note alive_l = this
        show ?thesis
        proof (cases "typeof x ≤ ltype l")
          case True 
          with alive_l alive_x
          have "s⟨l:=x⟩@@l = x"
            by (rule update_access_same)
          moreover
          have "s⟨t⟩⟨l:=x⟩@@l = x"
          proof -
            from alive_l neq_l_new have "alive (ref l) (s⟨t⟩)"
              by (simp add: lemma_3_1)
            moreover
            from alive_x neq_x_new have "alive x (s⟨t⟩)"
              by (simp add: lemma_3_2)
            ultimately
            show "s⟨t⟩⟨l:=x⟩@@l = x"
              using True by (rule update_access_same)
          qed
          ultimately show ?thesis 
            using eq_l_k lemma_3_3 by simp
        next
          case False
          thus ?thesis by simp
        qed
      next
        case False note not_alive_l = this
        from not_alive_l neq_l_new have "¬ alive (ref l) (s⟨t⟩)"
          by (simp add: lemma_3_1)
        then have "s⟨t⟩⟨l:=x⟩@@l = init (ltype l)"
          by simp
        also from not_alive_l have "… = s⟨l:=x⟩@@l"
          by simp
        also have "… = s⟨l:=x⟩⟨t⟩@@l" 
          by (simp add: lemma_3_3)
        finally show ?thesis by (simp add: eq_l_k)
      qed
    next
      case False note not_alive_x = this
      from not_alive_x neq_x_new have "¬ alive x (s⟨t⟩)"
        by (simp add: lemma_3_2)
      then have "s⟨t⟩⟨l:=x⟩@@l = s⟨t⟩@@l"
        by (simp)
      also have "… = s@@l"
      proof -
        from neq_l_new 
        have "isNewArr t ⟶ l ≠ arr_len (new s t)"
          by (cases t) auto
        thus ?thesis
          by (simp)
      qed
      also from not_alive_x have "… = s⟨l:=x⟩@@l"
        by (simp)
      also have "… = s⟨l:=x⟩⟨t⟩@@l"
        by (simp add: lemma_3_3)
      finally show ?thesis by (simp add: eq_l_k)
    qed
  qed
qed


end