Theory StoreProperties

(*  Title:       Jive Data and Store Model
    ID:          $Id: StoreProperties.thy,v 1.9 2007/07/19 21:23:12 makarius Exp $
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

header {* Store Properties *}

theory StoreProperties imports Store begin

text {* This theory formalizes advanced concepts and properties of stores. *}

subsection {* Reachability of a Location from a Reference *}

text {* For a given store, the function @{text "reachS"} yields the set of all pairs 
$(l,v)$ where $l$ is a location that is reachable from the value $v$ (which must be a reference)
in the given store.
The predicate @{text "reach"} decides whether a location is reachable from a value in a store.
*}

inductive
  reach :: "Store => Location => Value => bool" 
    ("_\<turnstile> _ reachable'_from _" [91,91,91]90)
  for s :: Store
where
  Immediate: "ref l ≠ nullV ==> s\<turnstile> l reachable_from (ref l)"
| Indirect: "[|s\<turnstile> l reachable_from (s@@k); ref k ≠ nullV|] 
             ==> s\<turnstile> l reachable_from (ref k)" 

text {* Note that we explicitly exclude @{text "nullV"} as legal reference
for reachability. 
Keep in mind that static fields are not associated to any object,
therefore @{text "ref"} yields @{text "nullV"} if invoked on static fields 
(see the
definition of the function @{text "ref"}, Sect. \ref{ref_def}).
Reachability only describes the locations directly 
reachable from the object or array by following the pointers and should not include 
the static fields if we encounter a @{text "nullV"} reference in the pointer 
chain.*}

text {* We formalize some properties of reachability. 
Especially, Lemma 3.2 as given in \cite[p. 53]{Poetzsch-Heffter97specification} is proven. *}

lemma unreachable_Null: 
  assumes reach: "s\<turnstile> l reachable_from x" shows "x≠nullV"
  using reach by (induct) auto

corollary unreachable_Null_simp [simp]:
  "¬ s\<turnstile> l reachable_from nullV"
  by (iprover dest: unreachable_Null)

corollary unreachable_NullE [elim]:
  "s\<turnstile> l reachable_from nullV ==> P"
  by (simp)

lemma reachObjLoc [simp,intro]: 
  "C=cls cf ==> s\<turnstile> objLoc cf a reachable_from objV C a"
  by (iprover intro: reach.Immediate [of "objLoc cf a",simplified])

lemma reachArrLoc [simp,intro]: "s\<turnstile> arrLoc T a i reachable_from arrV T a"
  by (rule reach.Immediate [of "arrLoc T a i",simplified])

lemma reachArrLen [simp,intro]: "s\<turnstile> arrLenLoc T a reachable_from arrV T a"
  by (rule reach.Immediate [of "arrLenLoc T a",simplified])

lemma unreachStatic [simp]: "¬ s\<turnstile> staticLoc f reachable_from x"
proof -
  {
    fix y assume "s\<turnstile> y reachable_from x" "y=staticLoc f"
    then have False
      by induct auto
  }
  thus ?thesis
    by auto
qed

lemma unreachStaticE [elim]: "s\<turnstile> staticLoc f reachable_from x ==> P"
  by (simp add: unreachStatic)

lemma reachable_from_ArrLoc_impl_Arr [simp,intro]:
  assumes reach_loc: "s\<turnstile> l reachable_from (s@@arrLoc T a i)"
  shows "s\<turnstile> l reachable_from (arrV T a)"
  using reach.Indirect [OF reach_loc]
  by simp

lemma reachable_from_ObjLoc_impl_Obj [simp,intro]:
  assumes reach_loc: "s\<turnstile> l reachable_from (s@@objLoc cf a)"
  assumes C: "C=cls cf"
  shows "s\<turnstile> l reachable_from (objV C a)"
  using C reach.Indirect [OF reach_loc]
  by simp


text {* Lemma 3.2 (i) *}
lemma reach_update [simp]:
  assumes unreachable_l_x: "¬ s\<turnstile> l reachable_from x" 
  shows "s⟨l:=y⟩\<turnstile> k reachable_from  x = s\<turnstile> k reachable_from x"
proof
  assume "s\<turnstile> k reachable_from x"
  from this unreachable_l_x
  show "s⟨l := y⟩\<turnstile> k reachable_from x"
  proof (induct)
    case (Immediate k)
    have "ref k ≠ nullV" by fact
    then show "s⟨l := y⟩\<turnstile> k reachable_from (ref k)"
      by (rule reach.Immediate)
  next
    case (Indirect k m)
    have hyp: "¬ s\<turnstile> l reachable_from (s@@m) 
               ==> s⟨l:=y⟩ \<turnstile> k reachable_from (s@@m)" by fact
    have "ref m ≠ nullV" and "¬ s\<turnstile> l reachable_from (ref m)" by fact+
    hence "l≠m" "¬ s\<turnstile> l reachable_from (s@@m)"
      by (auto intro: reach.intros)
    with hyp have "s⟨l := y⟩ \<turnstile> k reachable_from (s⟨l := y⟩@@m)"
      by simp
    then show "s⟨l := y⟩\<turnstile> k reachable_from (ref m)"
      by (rule reach.Indirect) (rule Indirect.hyps)
  qed
next
  assume "s⟨l := y⟩\<turnstile> k reachable_from x"
  from this unreachable_l_x
  show "s\<turnstile> k reachable_from x"
  proof (induct)
    case (Immediate k)
    have "ref k ≠ nullV" by fact
    then show "s \<turnstile> k reachable_from (ref k)"
      by (rule reach.Immediate)
  next
    case (Indirect k m)
    with Indirect.hyps 
    have hyp: "¬ s\<turnstile> l reachable_from (s⟨l := y⟩@@m)  
               ==> s\<turnstile> k reachable_from (s⟨l := y⟩@@m)" by simp
    have "ref m ≠ nullV" and "¬ s\<turnstile> l reachable_from (ref m)" by fact+
    hence "l≠m" "¬ s \<turnstile> l reachable_from (s@@m)"  
      by (auto intro: reach.intros)
    with hyp have "s \<turnstile> k reachable_from (s@@m)"
      by simp
    thus "s\<turnstile> k reachable_from (ref m)"
      by (rule reach.Indirect) (rule Indirect.hyps)
  qed
qed


text {* Lemma 3.2 (ii) *}
lemma reach2: 
  "¬ s\<turnstile> l reachable_from x ==> ¬ s⟨l:=y⟩\<turnstile> l reachable_from x"
  by (simp)

text {* Lemma 3.2 (iv) *}
lemma reach4: "¬ s \<turnstile> l reachable_from (ref k) ==> k ≠ l ∨ (ref k) = nullV"
  by (auto intro: reach.intros)

lemma reachable_isRef: 
  assumes reach: "s\<turnstile>l reachable_from x" 
  shows "isRefV x"
  using reach 
proof (induct)
  case (Immediate l)
  show "isRefV (ref l)"
    by (cases l) simp_all
next
  case (Indirect l k)
  show "isRefV (ref k)"
    by (cases k) simp_all
qed


lemma val_ArrLen_IntgT: "isArrLenLoc l ==> typeof (s@@l) = IntgT"
proof -
  assume isArrLen: "isArrLenLoc l"
  have T: "typeof (s@@l) ≤ ltype l"
    by (simp)
  also from isArrLen have I: "ltype l = IntgT"
    by (cases l) simp_all
  finally show ?thesis
    by (auto elim: rtranclE simp add: le_Javatype_def subtype_defs)
qed

lemma access_alloc' [simp]:
  assumes no_arr_len: "¬ isArrLenLoc l"
  shows "s⟨t⟩@@l = s@@l"
proof -
  from no_arr_len 
  have "isNewArr t --> l ≠ arr_len (new s t)"
    by (cases t) (auto simp add: new_def isArrLenLoc_def split: Location.splits)
  thus ?thesis 
    by (rule access_alloc)
qed
 
text {* Lemma 3.2 (v) *}
lemma reach_alloc [simp]: "s⟨t⟩\<turnstile> l reachable_from x = s\<turnstile> l reachable_from x"
proof 
  assume "s⟨t⟩\<turnstile> l reachable_from x"
  thus "s\<turnstile> l reachable_from x"
  proof (induct)
    case (Immediate l)
    thus "s\<turnstile> l reachable_from ref l"
      by (rule reach.intros)
  next
    case (Indirect l k)
    have reach_k: "s\<turnstile> l reachable_from (s⟨t⟩@@k)" by fact
    moreover
    have "s⟨t⟩@@k = s@@k"
    proof -
      from reach_k have isRef: "isRefV (s⟨t⟩@@k)"
        by (rule reachable_isRef)
      have "¬ isArrLenLoc k"
      proof (rule ccontr,simp)
        assume "isArrLenLoc k"
        then have "typeof (s⟨t⟩@@k) = IntgT"
          by (rule val_ArrLen_IntgT)
        with isRef 
        show "False"
          by (cases "(s⟨t⟩@@k)") simp_all
      qed
      thus ?thesis
        by (rule access_alloc')
    qed
    ultimately have "s\<turnstile> l reachable_from (s@@k)"
      by simp
    thus "s\<turnstile> l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
next
  assume "s\<turnstile> l reachable_from x"
  thus "s⟨t⟩\<turnstile> l reachable_from x"
  proof (induct)
    case (Immediate l)
    thus "s⟨t⟩\<turnstile> l reachable_from ref l"
      by (rule reach.intros)
  next
    case (Indirect l k)
    have reach_k: "s⟨t⟩\<turnstile> l reachable_from (s@@k)" by fact
    moreover
    have "s⟨t⟩@@k = s@@k"
    proof -
      from reach_k have isRef: "isRefV (s@@k)"
        by (rule reachable_isRef)
      have "¬ isArrLenLoc k"
      proof (rule ccontr,simp)
        assume "isArrLenLoc k"
        then have "typeof (s@@k) = IntgT"
          by (rule val_ArrLen_IntgT)
        with isRef 
        show "False"
          by (cases "(s@@k)") simp_all
      qed
      thus ?thesis
        by (rule access_alloc')
    qed
    ultimately have "s⟨t⟩\<turnstile> l reachable_from (s⟨t⟩@@k)"
      by simp
    thus "s⟨t⟩\<turnstile> l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
qed
       

text {* Lemma 3.2 (vi) *}
lemma reach6: "isprimitive(typeof x) ==> ¬ s \<turnstile> l reachable_from x"
proof 
  assume prim: "isprimitive(typeof x)"
  assume "s \<turnstile> l reachable_from x"
  hence "isRefV x"
    by (rule reachable_isRef)
  with prim show False
    by (cases x) simp_all
qed

text {* Lemma 3.2 (iii) *}
lemma reach3: 
  assumes k_y: "¬ s\<turnstile> k reachable_from y"
  assumes k_x: "¬ s\<turnstile> k reachable_from x"
  shows "¬ s⟨l:=y⟩\<turnstile> k reachable_from x"
proof
  assume "s⟨l:=y⟩\<turnstile> k reachable_from x"
  from this k_y k_x
  show False
  proof (induct)
    case (Immediate l)
    have "¬ s\<turnstile> l reachable_from ref l" and "ref l ≠ nullV" by fact+
    thus False
      by (iprover intro: reach.intros)
  next
    case (Indirect m k)
    have k_not_Null: "ref k ≠ nullV" by fact
    have not_m_y: "¬ s\<turnstile> m reachable_from y" by fact
    have not_m_k: "¬ s\<turnstile> m reachable_from ref k" by fact
    have hyp: "[|¬ s\<turnstile> m reachable_from y; ¬ s\<turnstile> m reachable_from (s⟨l := y⟩@@k)|]
               ==> False" by fact
    have m_upd_k: "s⟨l := y⟩\<turnstile> m reachable_from (s⟨l := y⟩@@k)" by fact
    show False
    proof (cases "l=k")
      case False
      then have "s⟨l := y⟩@@k = s@@k" by simp
      moreover 
      from not_m_k k_not_Null have "¬ s\<turnstile> m reachable_from (s@@k)"
        by (iprover intro: reach.intros)
      ultimately show False
        using not_m_y hyp by simp
    next
      case True note eq_l_k = this
      show ?thesis
      proof (cases "alive (ref l) s ∧ alive y s ∧ typeof y ≤ ltype l")
        case True
        with eq_l_k have "s⟨l := y⟩@@k = y"
          by simp
        with not_m_y hyp show False by simp
      next
        case False
        hence "s⟨l := y⟩ = s"
          by auto
        moreover 
        from not_m_k k_not_Null have "¬ s\<turnstile> m reachable_from (s@@k)"
          by (iprover intro: reach.intros)
        ultimately show False
          using not_m_y hyp by simp
      qed
    qed
  qed
qed



text {* Lemma 3.2 (vii). *}

lemma unreachable_from_init [simp,intro]: "¬ s\<turnstile> l reachable_from (init T)"
  using reach6 by (cases T) simp_all

lemma ref_reach_unalive: 
  assumes unalive_x:"¬ alive x s" 
  assumes l_x: "s\<turnstile> l reachable_from x" 
  shows "x = ref l"
using l_x unalive_x
proof induct
  case (Immediate l)
  show "ref l = ref l"
    by simp
next
  case (Indirect l k)
  have "ref k ≠ nullV" by fact
  have "¬ alive (ref k) s" by fact
  hence "s@@k = init (ltype k)" by simp
  moreover have "s\<turnstile> l reachable_from (s@@k)" by fact
  ultimately have False by simp
  thus ?case ..
qed

lemma loc_new_reach: 
  assumes l: "ref l = new s t"
  assumes l_x: "s\<turnstile> l reachable_from x"
  shows "x = new s t"
using l_x l
proof induct
  case (Immediate l)
  show "ref l = new s t" by fact
next
  case (Indirect l k)
  hence "s@@k = new s t" by iprover
  moreover 
  have "¬ alive (new s t) s"
    by simp
  moreover 
  have "alive (s@@k) s"
    by simp
  ultimately have False by simp
  thus ?case ..
qed
 

text {* Lemma 3.2 (viii) *}
lemma alive_reach_alive: 
  assumes alive_x: "alive x s" 
  assumes reach_l: "s \<turnstile> l reachable_from x" 
  shows "alive (ref l) s"
using reach_l alive_x
proof (induct)
  case (Immediate l)
  show ?case by fact
next
  case (Indirect l k)
  have hyp: "alive (s@@k) s ==> alive (ref l) s" by fact
  moreover have "alive (s@@k) s" by simp
  ultimately
  show "alive (ref l) s"
    by iprover
qed
 
text {* Lemma 3.2 (ix) *}
lemma reach9: 
  assumes reach_impl_access_eq: "∀l. s1\<turnstile>l reachable_from x --> (s1@@l = s2@@l)"
  shows "s1\<turnstile> l reachable_from x = s2\<turnstile> l reachable_from x"
proof 
  assume "s1\<turnstile> l reachable_from x"
  from this reach_impl_access_eq 
  show "s2\<turnstile> l reachable_from x"
  proof (induct)
    case (Immediate l)
    show "s2\<turnstile> l reachable_from ref l"
      by (rule reach.intros) (rule Immediate.hyps)
  next
    case (Indirect l k)
    have hyp: "∀l. s1\<turnstile> l reachable_from (s1@@k) --> s1@@l = s2@@l 
               ==> s2\<turnstile> l reachable_from (s1@@k)" by fact
    have k_not_Null: "ref k ≠ nullV" by fact
    have reach_impl_access_eq: 
      "∀l. s1\<turnstile> l reachable_from ref k --> s1@@l = s2@@l" by fact
    have "s1\<turnstile> l reachable_from (s1@@k)" by fact
    with k_not_Null
    have "s1@@k = s2@@k"
      by (iprover intro: reach_impl_access_eq [rule_format] reach.intros)
    moreover from reach_impl_access_eq k_not_Null
    have "∀l. s1\<turnstile> l reachable_from (s1@@k) --> s1@@l = s2@@l"
      by (iprover intro: reach.intros)
    then have "s2\<turnstile> l reachable_from (s1@@k)"
      by (rule hyp)
    ultimately have "s2\<turnstile> l reachable_from (s2@@k)"
      by simp
    thus "s2\<turnstile> l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
  qed
next
  assume "s2\<turnstile> l reachable_from x"
  from this reach_impl_access_eq 
  show "s1\<turnstile> l reachable_from x"
  proof (induct)
    case (Immediate l)
    show "s1\<turnstile> l reachable_from ref l"
      by (rule reach.intros) (rule Immediate.hyps)
  next
    case (Indirect l k)
    have hyp: "∀l. s1\<turnstile> l reachable_from (s2@@k) --> s1@@l = s2@@l 
               ==> s1\<turnstile> l reachable_from (s2@@k)" by fact
    have k_not_Null: "ref k ≠ nullV" by fact
    have reach_impl_access_eq: 
      "∀l. s1\<turnstile> l reachable_from ref k --> s1@@l = s2@@l" by fact
    have "s1\<turnstile> k reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
    with reach_impl_access_eq
    have eq_k: "s1@@k = s2@@k"
      by simp
    from reach_impl_access_eq k_not_Null
    have "∀l. s1\<turnstile> l reachable_from (s1@@k) --> s1@@l = s2@@l"
      by (iprover intro: reach.intros)
    then 
    have "∀l. s1\<turnstile> l reachable_from (s2@@k) --> s1@@l = s2@@l"
      by (simp add: eq_k)
    with eq_k hyp have "s1\<turnstile> l reachable_from (s1@@k)"
      by simp
    thus "s1\<turnstile> l reachable_from ref k"
      by (rule reach.intros) (rule Indirect.hyps)
   qed
qed


subsection {* Reachability of a Reference from a Reference *}

text {* The predicate @{text "rreach"} tests whether a value is reachable from
another value. This is an extension of the predicate @{text "oreach"} as described
in \cite[p. 54]{Poetzsch-Heffter97specification} because now arrays are handled as well.
*}

consts rreach:: "Store => Value => Value => bool" 
                            ("_|-Ref _ reachable'_from _" [91,91,91]90)
syntax (xsymbols)
rreach:: "Store => Value => Value => bool" 
                      ("_\<turnstile>Ref _ reachable'_from _" [91,91,91]90)

defs rreach_def:
"s\<turnstile>Ref y reachable_from x ≡ ∃ l. s\<turnstile> l reachable_from x ∧ y = ref l"

    
subsection {* Disjointness of Reachable Locations *}

text {* The predicate @{text "disj"} tests whether two values are disjoint
in a given store. Its properties as given in 
\cite[Lemma 3.3, p. 54]{Poetzsch-Heffter97specification} are then proven.
*}

constdefs disj:: "Value => Value => Store => bool"
"disj x y s ≡ ∀ l. ¬ s\<turnstile> l reachable_from x ∨ ¬ s\<turnstile> l reachable_from y"


lemma disjI1: "[|!! l. s\<turnstile> l reachable_from x ==> ¬ s\<turnstile> l reachable_from y|] 
 ==> disj x y s"
  by (simp add: disj_def)

lemma disjI2: "[|!! l. s\<turnstile> l reachable_from y ==> ¬ s\<turnstile> l reachable_from x|] 
 ==> disj x y s"
  by (auto simp add: disj_def)

lemma disj_cases [consumes 1]: 
  assumes "disj x y s"
  assumes "!! l.  ¬ s\<turnstile> l reachable_from x ==> P"
  assumes "!! l.  ¬ s\<turnstile> l reachable_from y ==> P"
  shows "P"
using prems by (auto simp add: disj_def)

text {* Lemma 3.3 (i) in \cite{Poetzsch-Heffter97specification} *}
lemma disj1: "[|disj x y s; ¬ s\<turnstile> l reachable_from x; ¬ s\<turnstile> l reachable_from y|] 
              ==> disj x y (s⟨l:=z⟩)"
  by (auto simp add: disj_def)

text {* Lemma 3.3 (ii) *}
lemma disj2: 
  assumes disj_x_y: "disj x y s" 
  assumes disj_x_z: "disj x z s"
  assumes unreach_l_x: "¬ s\<turnstile> l reachable_from x"
  shows "disj x y (s⟨l:=z⟩)"
proof (rule disjI1)
  fix k 
  assume reach_k_x: "s⟨l := z⟩\<turnstile> k reachable_from x"
  show "¬ s⟨l := z⟩\<turnstile> k reachable_from y"
  proof - 
    from unreach_l_x reach_k_x 
    have reach_s_k_x: "s\<turnstile> k reachable_from x"
      by simp
    with disj_x_z 
    have "¬ s\<turnstile> k reachable_from z"
      by (simp add: disj_def)
    moreover from reach_s_k_x disj_x_y
    have "¬ s\<turnstile> k reachable_from y"
      by (simp add: disj_def)
    ultimately show ?thesis
      by (rule reach3)
  qed
qed

   

text {* Lemma 3.3 (iii) *}
lemma disj3: assumes alive_x_s: "alive x s" 
  shows "disj x (new s t) (s⟨t⟩)"
proof (rule disjI1,simp only: reach_alloc)
  fix l
  assume reach_l_x: "s\<turnstile> l reachable_from x"
  show "¬ s\<turnstile> l reachable_from new s t"
  proof 
    assume reach_l_new: "s\<turnstile> l reachable_from new s t" 
    have unalive_new: "¬ alive (new s t) s" by simp
    from this reach_l_new
    have  "new s t = ref l"
      by (rule ref_reach_unalive)
    moreover from alive_x_s reach_l_x 
    have "alive (ref l) s"
      by (rule alive_reach_alive)
    ultimately show False
      using unalive_new
      by simp
  qed
qed

text {* Lemma 3.3 (iv) *}
lemma disj4: "[|disj (objV C a) y s; CClassT C ≤ dtype f |]  
              ==> disj (s@@(objV C a)..f) y s"
  by (auto simp add: disj_def)
  
lemma disj4': "[|disj (arrV T a) y s |]  
              ==> disj (s@@(arrV T a).[i]) y s"
  by (auto simp add: disj_def)


subsection {* X-Equivalence *}

text {* We call two stores $s_1$ and $s_2$ equivalent wrt. a given value $X$
(which is called X-equivalence)
 iff $X$ and all values
reachable from $X$ in $s_1$ or $s_2$ have the same state \cite[p. 55]{Poetzsch-Heffter97specification}. 
This is tested by  the predicate
@{text "xeq"}. Lemma 3.4 of  \cite{Poetzsch-Heffter97specification} is then proven for @{text "xeq"}.
*} 

constdefs xeq:: "Value => Store => Store => bool"  
                                     
"xeq x s t ≡ alive x s = alive x t ∧ 
             (∀ l. s\<turnstile> l reachable_from x --> s@@l = t@@l)"



syntax (xsymbols) "@xeq":: "Store => Value => Store => bool" 
 ("_/ (≡[_])/ _" [900,0,900] 900) 

syntax (ascii) "@xeq":: "Store => Value => Store => bool"
("_/ (==[_])/ _" [900,0,900] 900)

translations "s ≡[x] t" == "xeq x s t"
             "s ==[x] t" == "xeq x s t"


lemma xeqI: "[|alive x s = alive x t;  
             !! l. s\<turnstile> l reachable_from x ==> s@@l = t@@l
             |] ==> s ≡[x] t"
  by (auto simp add: xeq_def)

text {* Lemma 3.4 (i) in  \cite{Poetzsch-Heffter97specification}.  *}
lemma xeq1_refl: "s ≡[x] s"
  by (simp add: xeq_def)

text {* Lemma 3.4 (i)  *}
lemma xeq1_sym': 
  assumes s_t: "s ≡[x] t"
  shows "t ≡[x] s"
proof -
  from s_t have "alive x s = alive x t" by (simp add: xeq_def)
  moreover
  from s_t have "∀ l. s\<turnstile> l reachable_from x --> s@@l = t@@l" 
    by (simp add: xeq_def)
  with reach9 [OF this]
  have "∀ l. t\<turnstile> l reachable_from x --> t@@l = s@@l" 
    by simp
  ultimately show ?thesis
    by (simp add: xeq_def)
qed
 
lemma xeq1_sym: "s ≡[x] t = t ≡[x] s"
  by (auto intro: xeq1_sym')


text {* Lemma 3.4 (i) *}
lemma xeq1_trans [trans]: 
  assumes s_t: "s ≡[x] t" 
  assumes t_r: "t ≡[x] r" 
  shows "s ≡[x] r"
proof -
  from s_t t_r
  have "alive x s = alive x r"
    by (simp add: xeq_def)
  moreover
  have "∀ l. s\<turnstile> l reachable_from x --> s@@l = r@@l"
  proof (intro allI impI)
    fix l
    assume reach_l: "s\<turnstile> l reachable_from x"
    show "s@@l = r@@l"
    proof -
      from reach_l s_t have "s@@l=t@@l"
        by (simp add: xeq_def)
      also have "t@@l = r@@l"
      proof -
        from s_t have "∀ l. s\<turnstile> l reachable_from x --> s@@l = t@@l"
          by (simp add: xeq_def)
        from reach9 [OF this] reach_l have "t\<turnstile> l reachable_from x"
          by simp
        with t_r show ?thesis
          by (simp add: xeq_def)
      qed
      finally show ?thesis .
    qed
  qed
  ultimately show ?thesis
    by (simp add: xeq_def)
qed
   

  
text {* Lemma 3.4 (ii) *}
lemma xeq2: 
  assumes xeq: "∀ x. s ≡[x] t" 
  assumes static_eq: "∀ f. s@@(staticLoc f) = t@@(staticLoc f)" 
  shows "s = t"
proof (rule Store_eqI)
  from xeq 
  show "∀x. alive x s = alive x t"
    by (simp add: xeq_def)
next
  show "∀l. s@@l = t@@l"
  proof 
    fix l 
    show "s@@l = t@@l"
    proof (cases l)
      case (objLoc cf a)
      have "l = objLoc cf a" by fact
      hence "s\<turnstile> l reachable_from (objV (cls cf) a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    next
      case (staticLoc f)
      have "l = staticLoc f" by fact
      with static_eq show ?thesis 
        by (simp add: xeq_def)
    next
      case (arrLenLoc T a)
      have "l = arrLenLoc T a" by fact
      hence "s\<turnstile> l reachable_from (arrV T a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    next
      case (arrLoc T a i)
      have "l = arrLoc T a i" by fact
      hence "s\<turnstile> l reachable_from (arrV T a)"
        by simp
      with xeq show ?thesis
        by (simp add: xeq_def)
    qed
  qed
qed


text {* Lemma 3.4 (iii) *}
lemma xeq3: 
  assumes unreach_l: "¬ s\<turnstile> l reachable_from x" 
  shows "s ≡[x] s⟨l:=y⟩"
proof (rule xeqI)
  show "alive x s = alive x (s⟨l := y⟩)"
    by simp
next
  fix k 
  assume reach_k: "s\<turnstile> k reachable_from x"
  with unreach_l have "l≠k" by auto
  then show "s@@k = s⟨l := y⟩@@k"
    by simp
qed



text {* Lemma 3.4 (iv) *}
lemma xeq4: assumes not_new: "x ≠ new s t" 
  shows "s ≡[x] s⟨t⟩"
proof (rule xeqI)
  from not_new 
  show "alive x s = alive x (s⟨t⟩)"
    by (simp add: alive_alloc_exhaust)
next
  fix l
  assume reach_l: "s\<turnstile> l reachable_from x"
  show "s@@l = s⟨t⟩@@l"
  proof (cases "isNewArr t --> l ≠ arr_len (new s t)")
    case True
    with reach_l show ?thesis
      by simp
  next
    case False
    then obtain T n where t: "t = new_array T n" and
                          l: "l = arr_len (new s t)"
      by (cases t) auto
    hence "ref l = new s t"
      by simp
    from this reach_l
    have "x = new s t"
      by (rule loc_new_reach)
    with not_new show ?thesis ..
  qed
qed

text {* Lemma 3.4 (v) *}
lemma xeq5: "s ≡[x] t ==> s\<turnstile> l reachable_from x = t\<turnstile> l reachable_from x"
  by (rule reach9) (simp add:  xeq_def)
  

subsection {* T-Equivalence *}

text {* T-equivalence is the extension of X-equivalence from values to types. Two stores are
T-equivalent iff they are X-equivalent for all values of type T. This is formalized by the
predicate @{text "teq"} \cite[p. 55]{Poetzsch-Heffter97specification}. *}

constdefs teq:: "Javatype => Store => Store => bool"
"teq t s1 s2 ≡ ∀ x. typeof x ≤ t --> s1 ≡[x] s2"

subsection {* Less Alive *}

text {* To specify that methods have no side-effects, the following binary relation on stores 
plays a prominent role. It expresses that the two stores differ only in values that are alive
in the store passed as first argument. This is formalized by the predicate @{text "lessalive"}
\cite[p. 55]{Poetzsch-Heffter97specification}.
The stores have to be X-equivalent for the references of the
first store that are alive, and the values of the static fields have to be the same in both stores.
*}

consts lessalive:: "Store => Store => bool" ("_/ << _" [70,71] 70)

syntax (xsymbols) "@lessalive":: "Store => Store => bool" ("_/ \<lless> _" [70,71] 70)
translations "s \<lless> t" == "lessalive s t"

defs lessalive_def:
"s \<lless> t ≡ (∀ x. alive x s --> s ≡[x] t) ∧ (∀ f. s@@staticLoc f = t@@staticLoc f)"

text {* We define an introduction rule for the new operator. *}

lemma lessaliveI: 
  "[|!! x. alive x s ==>  s ≡[x] t; !! f. s@@staticLoc f = t@@staticLoc f|]
   ==> s \<lless> t"
by (simp add: lessalive_def)

text {* It can be shown that @{text "lessalive"} is reflexive, transitive and antisymmetric. *}

lemma lessalive_refl: "s \<lless> s"
  by (simp add: lessalive_def xeq1_refl)

lemma lessalive_trans [trans]: 
  assumes s_t: "s \<lless> t"
  assumes t_w: "t \<lless> w"
  shows "s \<lless> w"
proof (rule lessaliveI)
  fix x 
  assume alive_x_s: "alive x s"
  with s_t have "s ≡[x] t"
    by (simp add: lessalive_def)
  also
  have "t ≡[x] w"
  proof -
    from alive_x_s s_t have "alive x t" by (simp add: lessalive_def xeq_def)
    with t_w show ?thesis
      by (simp add: lessalive_def)
  qed
  finally show "s ≡[x] w".
next
  fix f
  from s_t t_w show "s@@staticLoc f = w@@staticLoc f"
    by (simp add: lessalive_def)
qed

lemma lessalive_antisym:
  assumes s_t: "s \<lless> t"
  assumes t_s: "t \<lless> s"
  shows "s = t"
proof (rule xeq2)
  show "∀x. s ≡[x] t"
  proof 
    fix x show "s ≡[x] t"
    proof (cases "alive x s")
      case True
      with s_t show ?thesis by (simp add: lessalive_def)
    next
      case False note unalive_x_s = this
      show ?thesis
      proof (cases "alive x t")
        case True
        with t_s show ?thesis 
          by (subst xeq1_sym) (simp add: lessalive_def)
      next
        case False 
        show ?thesis
        proof (rule xeqI)
          from False unalive_x_s show "alive x s = alive x t" by simp
        next
          fix l assume reach_s_x: "s\<turnstile> l reachable_from x"
          with unalive_x_s have x: "x = ref l" 
            by (rule ref_reach_unalive)
          with unalive_x_s have "s@@l = init (ltype l)"
            by simp
          also from reach_s_x x have "t\<turnstile> l reachable_from x"
            by (auto intro: reach.Immediate unreachable_Null)
          with False x have "t@@l = init (ltype l)"
            by simp
          finally show "s@@l = t@@l"
            by simp
        qed
      qed
    qed
  qed
next
  from s_t show "∀f. s@@staticLoc f = t@@staticLoc f"
    by (simp add: lessalive_def)
qed

text {* This gives us a partial ordering on the store. Thus, the type @{typ "Store"}
can be added to the appropriate type class @{term "ord"} which lets us define the $<$ and
$\leq$ symbols, and to the type class  @{term "order"} which axiomatizes partial orderings.
*}

instance Store:: ord ..
defs (overloaded)
le_Store_def: "s ≤ t ≡ s \<lless> t"
less_Store_def: "(s::Store) < t ≡ s ≤ t ∧ s ≠ t"


text {* We prove Lemma 3.5 of \cite[p. 56]{Poetzsch-Heffter97specification} for this relation.
*}

text {* Lemma 3.5 (i) *}
instance Store:: order
proof 
  fix s t w:: "Store"
  {
    show "s ≤ s"
      by (simp add: le_Store_def lessalive_refl)
  next
    assume "s ≤ t" "t ≤ w"
    then show "s ≤ w"
      by (unfold le_Store_def) (rule lessalive_trans) 
  next
    assume "s ≤ t" "t ≤ s" 
    then show "s = t"
      by (unfold le_Store_def) (rule lessalive_antisym) 
  next
    show "(s < t) = (s ≤ t ∧ s ≠ t)"
      by (simp add: less_Store_def)
  }
qed

text {* Lemma 3.5 (ii) *}
lemma lessalive2: "[|s \<lless> t; alive x s|] ==> alive x t"
  by (simp add: lessalive_def xeq_def)
  

text {* Lemma 3.5 (iii) *}
lemma lessalive3: 
  assumes s_t: "s \<lless> t" 
  assumes alive: "alive x s ∨ ¬ alive x t"
  shows "s ≡[x] t"
proof (cases "alive x s")
  case True
  with s_t show ?thesis
    by (simp add: lessalive_def)
next
  case False
  note unalive_x_s = this
  with alive have unalive_x_t: "¬ alive x t"
    by simp
  show ?thesis
  proof (rule xeqI)
    from False alive show "alive x s = alive x t"
      by simp
  next
    fix l assume reach_s_x: "s\<turnstile> l reachable_from x"
    with unalive_x_s have x: "x = ref l" 
      by (rule ref_reach_unalive)
    with unalive_x_s have "s@@l = init (ltype l)"
      by simp
    also from reach_s_x x have "t\<turnstile> l reachable_from x"
      by (auto intro: reach.Immediate unreachable_Null)
    with unalive_x_t x have "t@@l = init (ltype l)"
      by simp
    finally show "s@@l = t@@l"
      by simp
  qed
qed
   
text {* Lemma 3.5 (iv) *}
lemma lessalive_update [simp,intro]: 
  assumes s_t: "s \<lless> t" 
  assumes unalive_l: "¬ alive (ref l) t"
  shows "s \<lless> t⟨l:=x⟩"
proof -
  from unalive_l have "t⟨l:=x⟩ = t"
    by simp
  with s_t show ?thesis by simp
qed

lemma Xequ4':  
  assumes alive: "alive x s" 
  shows "s ≡[x] s⟨t⟩"
proof -
  from alive have "x ≠ new s t"
    by auto
  thus ?thesis
    by (rule xeq4)
qed

  

text {* Lemma 3.5 (v)  *}
lemma lessalive_alloc [simp,intro]: "s \<lless> s⟨t⟩"
  by (simp add: lessalive_def Xequ4')
 

subsection {* Reachability of Types from Types *}

text {* The predicate @{text "treach"} denotes the fact that the first type reaches 
the second type by stepping finitely many times from a type to the range type of one 
of its fields. This formalization diverges from \cite[p. 106]{Poetzsch-Heffter97specification} 
in that it does not include the number of steps that are allowed to reach the second type.
Reachability of types is a static approximation of reachability in
the store. If I cannot reach the type of a location from the type of a
reference, I cannot reach the location from the reference. See lemma  
@{text "not_treach_ref_impl_not_reach"} below.
*}

inductive
  treach :: "Javatype => Javatype => bool"
where
  Subtype:       "U ≤ T ==> treach T U"
| Attribute:     "[|treach T S; S ≤ dtype f; U ≤ rtype f|]  ==> treach T U"
| ArrLength:     "treach (ArrT AT) IntgT"
| ArrElem:       "treach (ArrT AT) (at2jt AT)"
| Trans [trans]: "[|treach T U; treach U V|] ==> treach T V"


lemma treach_ref_l [simp,intro]: 
  assumes not_Null: "ref l ≠ nullV"
  shows "treach (typeof (ref l)) (ltype l)"
proof (cases l)
  case (objLoc cf a)
  have "l=objLoc cf a" by fact
  moreover
  have "treach (CClassT (cls cf)) (rtype (att cf))"
    by (rule treach.Attribute [where ?f="att cf" and ?S="CClassT (cls cf)"])
       (auto intro: treach.Subtype)
  ultimately show ?thesis
    by simp
next
  case (staticLoc f)
  have "l=staticLoc f" by fact
  hence "ref l = nullV" by simp
  with not_Null show ?thesis
    by simp
next
  case (arrLenLoc T a)
  have "l=arrLenLoc T a" by fact
  then show ?thesis
    by (auto intro: treach.ArrLength)
next
  case (arrLoc T a i)
  have "l=arrLoc T a i" by fact
  then show ?thesis
    by (auto intro: treach.ArrElem)
qed

lemma treach_ref_l' [simp,intro]:
  assumes not_Null: "ref l ≠ nullV"
  shows "treach (typeof (ref l)) (typeof (s@@l))"
proof -
  from not_Null have "treach (typeof (ref l)) (ltype l)" by (rule treach_ref_l)
  also have "typeof (s@@l) ≤ ltype l"
    by simp
  hence "treach (ltype l) (typeof (s@@l))"
    by (rule treach.intros)
  finally show ?thesis .
qed
  

lemma reach_impl_treach: 
  assumes reach_l: "s \<turnstile> l reachable_from x"
  shows "treach (typeof x) (ltype l)"
using reach_l
proof (induct)
  case (Immediate l)
  have "ref l ≠ nullV" by fact
  then show "treach (typeof (ref l)) (ltype l)"
    by (rule treach_ref_l)
next
  case (Indirect l k)
  have "treach (typeof (s@@k)) (ltype l)" by fact
  moreover
  have "ref k ≠ nullV" by fact
  hence "treach (typeof (ref k)) (typeof (s@@k))"
    by simp
  ultimately show "treach (typeof (ref k)) (ltype l)"
    by (iprover intro: treach.Trans)
qed

lemma not_treach_ref_impl_not_reach: 
  assumes not_treach: "¬ treach (typeof x) (typeof (ref l))"
  shows "¬ s \<turnstile> l reachable_from x"
proof 
  assume reach_l: "s\<turnstile> l reachable_from x"
  from this not_treach
  show False
  proof (induct)
    case (Immediate l)
    have "¬ treach (typeof (ref l)) (typeof (ref l))" by fact
    thus False by (iprover intro: treach.intros order_refl)
  next
    case (Indirect l k)
    have hyp: "¬ treach (typeof (s@@k)) (typeof (ref l)) ==> False" by fact
    have not_Null: "ref k ≠ nullV" by fact
    have not_k_l:"¬ treach (typeof (ref k)) (typeof (ref l))" by fact
    show False
    proof (cases "treach (typeof (s@@k)) (typeof (ref l))")
      case False thus False by (rule hyp)
    next
      case True
      from not_Null have "treach (typeof (ref k)) (typeof (s@@k))"
        by (rule treach_ref_l')
      also note True
      finally have "treach (typeof (ref k)) (typeof (ref l))" .
      with not_k_l show False ..
    qed
  qed
qed

text {* Lemma 4.6 in \cite[p. 107]{Poetzsch-Heffter97specification}.  *}
lemma treach1: 
  assumes x_t: "typeof x ≤ T" 
  assumes not_treach: "¬ treach T (typeof (ref l))"
  shows "¬ s \<turnstile> l reachable_from x"
proof -
  have "¬ treach (typeof x) (typeof (ref l))"
  proof 
    from x_t have "treach T (typeof x)" by (rule treach.intros)
    also assume "treach (typeof x) (typeof (ref l))"
    finally have "treach T (typeof (ref l))" .
    with not_treach show False ..
  qed
  thus ?thesis
    by (rule not_treach_ref_impl_not_reach)
qed

  
end