src/HOL/Hoare/SchorrWaite.thy
author wenzelm
Mon Mar 22 20:58:52 2010 +0100 (2010-03-22)
changeset 35898 c890a3835d15
parent 32960 69916a850301
child 36866 426d5781bb25
permissions -rw-r--r--
recovered header;
     1 (*  Title:      HOL/Hoare/SchorrWaite.thy
     2     ID:         $Id$
     3     Author:     Farhad Mehta
     4     Copyright   2003 TUM
     5 
     6 Proof of the Schorr-Waite graph marking algorithm.
     7 *)
     8 
     9 
    10 theory SchorrWaite imports HeapSyntax begin
    11 
    12 section {* Machinery for the Schorr-Waite proof*}
    13 
    14 constdefs
    15   -- "Relations induced by a mapping"
    16   rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
    17   "rel m == {(x,y). m x = Ref y}"
    18   relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
    19   "relS M == (\<Union> m \<in> M. rel m)"
    20   addrs :: "'a ref set \<Rightarrow> 'a set"
    21   "addrs P == {a. Ref a \<in> P}"
    22   reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
    23   "reachable r P == (r\<^sup>* `` addrs P)"
    24 
    25 lemmas rel_defs = relS_def rel_def
    26 
    27 text {* Rewrite rules for relations induced by a mapping*}
    28 
    29 lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
    30 apply blast
    31 done
    32 
    33 lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
    34 apply blast
    35 done
    36 
    37 lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
    38 apply (clarsimp simp only:Image_iff intro:subsetI)
    39 apply (erule rtrancl_induct)
    40  apply blast
    41 apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
    42  apply (erule UnE)
    43  apply (auto intro:rtrancl_into_rtrancl)
    44 apply blast
    45 done
    46 
    47 lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A =  Rb\<^sup>*``B "
    48 apply (rule equalityI)
    49  apply (erule still_reachable ,assumption)+
    50 done
    51 
    52 lemma reachable_null: "reachable mS {Null} = {}"
    53 apply (simp add: reachable_def addrs_def)
    54 done
    55 
    56 lemma reachable_empty: "reachable mS {} = {}"
    57 apply (simp add: reachable_def addrs_def)
    58 done
    59 
    60 lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
    61 apply (simp add: reachable_def rel_defs addrs_def)
    62 apply blast
    63 done
    64 
    65 lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
    66 apply (simp add: reachable_def rel_defs addrs_def)
    67 apply blast
    68 done
    69 
    70 lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
    71 apply (rule classical)
    72 apply (simp add:rel_defs fun_upd_apply)
    73 done
    74 
    75 lemma rel_upd2: "(a,b)  \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
    76 apply (rule classical)
    77 apply (simp add:rel_defs fun_upd_apply)
    78 done
    79 
    80 constdefs
    81   -- "Restriction of a relation"
    82   restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"       ("(_/ | _)" [50, 51] 50)
    83   "restr r m == {(x,y). (x,y) \<in> r \<and> \<not> m x}"
    84 
    85 text {* Rewrite rules for the restriction of a relation *}
    86 
    87 lemma restr_identity[simp]:
    88  " (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
    89 by (auto simp add:restr_def)
    90 
    91 lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
    92 by (auto simp add:restr_def elim:converse_rtranclE)
    93 
    94 lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
    95 by (auto simp add:restr_def elim:converse_rtranclE)
    96 
    97 lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
    98 apply (auto simp:restr_def rel_def fun_upd_apply)
    99 apply (rename_tac a b)
   100 apply (case_tac "a=q")
   101  apply auto
   102 done
   103 
   104 lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
   105   by (auto simp add:restr_def)
   106 
   107 lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
   108 apply (rule classical)
   109 apply (simp add:restr_def fun_upd_apply)
   110 done
   111 
   112 constdefs
   113   -- "A short form for the stack mapping function for List"
   114   S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
   115   "S c l r == (\<lambda>x. if c x then r x else l x)"
   116 
   117 text {* Rewrite rules for Lists using S as their mapping *}
   118 
   119 lemma [rule_format,simp]:
   120  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
   121 apply(induct_tac stack)
   122  apply(simp add:fun_upd_apply S_def)+
   123 done
   124 
   125 lemma [rule_format,simp]:
   126  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
   127 apply(induct_tac stack)
   128  apply(simp add:fun_upd_apply S_def)+
   129 done
   130 
   131 lemma [rule_format,simp]:
   132  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
   133 apply(induct_tac stack)
   134  apply(simp add:fun_upd_apply S_def)+
   135 done
   136 
   137 lemma [rule_format,simp]:
   138  "\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
   139 apply(induct_tac stack)
   140  apply(simp add:fun_upd_apply S_def)+
   141 done
   142 
   143 consts
   144   --"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
   145   stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow>  bool"
   146 primrec
   147 stkOk_nil:  "stkOk c l r iL iR t [] = True"
   148 stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
   149                                   iL p = (if c p then l p else t) \<and>
   150                                   iR p = (if c p then t else r p))"
   151 
   152 text {* Rewrite rules for stkOk *}
   153 
   154 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
   155   stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
   156 apply (induct xs)
   157  apply (auto simp:eq_sym_conv)
   158 done
   159 
   160 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
   161  stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
   162 apply (induct xs)
   163  apply (auto simp:eq_sym_conv)
   164 done
   165 
   166 lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
   167  stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
   168 apply (induct xs)
   169  apply (auto simp:eq_sym_conv)
   170 done
   171 
   172 lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
   173   stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
   174 apply (induct xs)
   175  apply (auto simp:eq_sym_conv)
   176 done
   177 
   178 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
   179  stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
   180 apply (induct xs)
   181  apply (auto simp:eq_sym_conv)
   182 done
   183 
   184 lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
   185  stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
   186 apply (induct xs)
   187  apply (auto simp:eq_sym_conv)
   188 done
   189 
   190 
   191 section{*The Schorr-Waite algorithm*}
   192 
   193 
   194 theorem SchorrWaiteAlgorithm: 
   195 "VARS c m l r t p q root
   196  {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l} 
   197  t := root; p := Null;
   198  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
   199  INV {\<exists>stack.
   200           List (S c l r) p stack \<and>                                         (*i1*)
   201           (\<forall>x \<in> set stack. m x) \<and>                                        (*i2*)
   202           R = reachable (relS{l, r}) {t,p} \<and>                           (*i3*)
   203           (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        (*i4*)
   204                  x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
   205           (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         (*i5*)
   206           (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       (*i6*)
   207           (stkOk c l r iL iR t stack)                                    (*i7*) }
   208  DO IF t = Null \<or> t^.m
   209       THEN IF p^.c
   210                THEN q := t; t := p; p := p^.r; t^.r := q               (*pop*)
   211                ELSE q := t; t := p^.r; p^.r := p^.l;                      (*swing*)
   212                         p^.l := q; p^.c := True          FI    
   213       ELSE q := p; p := t; t := t^.l; p^.l := q;                         (*push*)
   214                p^.m := True; p^.c := False            FI       OD
   215  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
   216   (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
   217 proof (vcg)
   218   let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
   219     {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
   220   {
   221 
   222     fix c m l r t p q root
   223     assume "?Pre c m l r root"
   224     thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
   225   next
   226 
   227     fix c m l r t p q
   228     let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
   229     assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"  
   230     then obtain stack where inv: "?Inv stack" by blast
   231     from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
   232     let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
   233     from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
   234     from pNull i1 have stackEmpty: "stack = []" by simp
   235     from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
   236     from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty expand_fun_eq intro:RisMarked)
   237 
   238   next   
   239       fix c m l r t p q root
   240       let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
   241       let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
   242       let "\<exists>stack. ?swInv stack"  =
   243         "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
   244       let "\<exists>stack. ?puInv stack"  =
   245         "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
   246       let "?ifB1"  =  "(t = Null \<or> t^.m)"
   247       let "?ifB2"  =  "p^.c" 
   248 
   249       assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
   250       then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
   251       let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
   252       from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
   253                   and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+        
   254       have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
   255 
   256       show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> 
   257                             (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
   258               (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
   259       proof - 
   260         {
   261           assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
   262           from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
   263           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
   264           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
   265             by auto
   266           with i2 have m_addr_p: "p^.m" by auto
   267           have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
   268           from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
   269           let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
   270           have "?popInv stack_tl"
   271           proof -
   272 
   273             -- {*List property is maintained:*}
   274             from i1 p_notin_stack_tl ifB2
   275             have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" 
   276               by(simp add: addr_p_eq stack_eq, simp add: S_def)
   277 
   278             moreover
   279             -- {*Everything on the stack is marked:*}
   280             from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
   281             moreover
   282 
   283             -- {*Everything is still reachable:*}
   284             let "(R = reachable ?Ra ?A)" = "?I3"
   285             let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
   286             let "?B" = "{p, p^.r}"
   287             -- {*Our goal is @{text"R = reachable ?Rb ?B"}.*}
   288             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
   289             proof
   290               show "?L \<subseteq> ?R"
   291               proof (rule still_reachable)
   292                 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastsimp simp:addrs_def relS_def rel_def addr_p_eq 
   293                      intro:oneStep_reachable Image_iff[THEN iffD2])
   294                 show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) 
   295                      (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
   296               qed
   297               show "?R \<subseteq> ?L"
   298               proof (rule still_reachable)
   299                 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
   300                   by(fastsimp simp:addrs_def rel_defs addr_p_eq 
   301                       intro:oneStep_reachable Image_iff[THEN iffD2])
   302               next
   303                 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
   304                   by (clarsimp simp:relS_def) 
   305                      (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd2)
   306               qed
   307             qed
   308             with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def) 
   309             moreover
   310 
   311             -- "If it is reachable and not marked, it is still reachable using..."
   312             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4        
   313             let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
   314             let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
   315             -- {*Our goal is @{text"\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"}.*}
   316             let ?T = "{t, p^.r}"
   317 
   318             have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
   319             proof (rule still_reachable)
   320               have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
   321                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
   322               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
   323                 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
   324               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
   325                 by (clarsimp simp:restr_def relS_def) 
   326                   (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
   327             qed
   328             -- "We now bring a term from the right to the left of the subset relation."
   329             hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
   330               by blast
   331             have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
   332             proof (rule allI, rule impI)
   333               fix x
   334               assume a: "x \<in> R \<and> \<not> m x"
   335               -- {*First, a disjunction on @{term"p^.r"} used later in the proof*}
   336               have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 
   337                 by auto
   338               -- {*@{term x} belongs to the left hand side of @{thm[source] subset}:*}
   339               have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
   340               have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
   341               -- {*And therefore also belongs to the right hand side of @{thm[source]subset},*}
   342               -- {*which corresponds to our goal.*}
   343               from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
   344             qed
   345             moreover
   346 
   347             -- "If it is marked, then it is reachable"
   348             from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
   349             moreover
   350 
   351             -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
   352             from i7 i6 ifB2 
   353             have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" 
   354               by(auto simp: addr_p_eq stack_eq fun_upd_apply)
   355 
   356             moreover
   357 
   358             -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
   359             from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
   360               by (clarsimp simp:stack_eq addr_p_eq)
   361 
   362             ultimately show "?popInv stack_tl" by simp
   363           qed
   364           hence "\<exists>stack. ?popInv stack" ..
   365         }
   366         moreover
   367 
   368         -- "Proofs of the Swing and Push arm follow."
   369         -- "Since they are in principle simmilar to the Pop arm proof,"
   370         -- "we show fewer comments and use frequent pattern matching."
   371         {
   372           -- "Swing arm"
   373           assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
   374           from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
   375           then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
   376           with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
   377           with i2 have m_addr_p: "p^.m" by clarsimp
   378           from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
   379             by simp
   380           let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
   381           have "?swInv stack"
   382           proof -
   383             
   384             -- {*List property is maintained:*}
   385             from i1 p_notin_stack_tl nifB2
   386             have swI1: "?swI1"
   387               by (simp add:addr_p_eq stack_eq, simp add:S_def)
   388             moreover
   389             
   390             -- {*Everything on the stack is marked:*}
   391             from i2
   392             have swI2: "?swI2" .
   393             moreover
   394             
   395             -- {*Everything is still reachable:*}
   396             let "R = reachable ?Ra ?A" = "?I3"
   397             let "R = reachable ?Rb ?B" = "?swI3"
   398             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
   399             proof (rule still_reachable_eq)
   400               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
   401                 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
   402             next
   403               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
   404                 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
   405             next
   406               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
   407                 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
   408             next
   409               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
   410                 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
   411             qed
   412             with i3
   413             have swI3: "?swI3" by (simp add:reachable_def) 
   414             moreover
   415 
   416             -- "If it is reachable and not marked, it is still reachable using..."
   417             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
   418             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
   419             let ?T = "{t}"
   420             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
   421             proof (rule still_reachable)
   422               have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
   423                 by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
   424               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
   425                 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
   426             next
   427               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
   428                 by (clarsimp simp:relS_def restr_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
   429             qed
   430             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
   431               by blast
   432             have ?swI4
   433             proof (rule allI, rule impI)
   434               fix x
   435               assume a: "x \<in> R \<and>\<not> m x"
   436               with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" 
   437                 by (simp only:reachable_def, clarsimp)
   438               with ifB1 a 
   439               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" 
   440                 by (auto simp add:addrs_def)
   441               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
   442                 by (auto simp add:reachable_def)
   443             qed
   444             moreover
   445             
   446             -- "If it is marked, then it is reachable"
   447             from i5
   448             have "?swI5" .
   449             moreover
   450 
   451             -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
   452             from i6 stack_eq
   453             have "?swI6"
   454               by clarsimp           
   455             moreover
   456 
   457             -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
   458             from stackDist i7 nifB2 
   459             have "?swI7"
   460               by (clarsimp simp:addr_p_eq stack_eq)
   461 
   462             ultimately show ?thesis by auto
   463           qed
   464           then have "\<exists>stack. ?swInv stack" by blast
   465         }
   466         moreover
   467 
   468         {
   469           -- "Push arm"
   470           assume nifB1: "\<not>?ifB1"
   471           from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
   472           then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
   473           with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
   474           from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
   475           with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
   476           let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
   477           have "?puInv new_stack"
   478           proof -
   479             
   480             -- {*List property is maintained:*}
   481             from i1 t_notin_stack
   482             have puI1: "?puI1"
   483               by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
   484             moreover
   485             
   486             -- {*Everything on the stack is marked:*}
   487             from i2
   488             have puI2: "?puI2" 
   489               by (simp add:new_stack_eq fun_upd_apply)
   490             moreover
   491             
   492             -- {*Everything is still reachable:*}
   493             let "R = reachable ?Ra ?A" = "?I3"
   494             let "R = reachable ?Rb ?B" = "?puI3"
   495             have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
   496             proof (rule still_reachable_eq)
   497               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
   498                 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
   499             next
   500               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
   501                 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
   502             next
   503               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
   504                 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
   505             next
   506               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
   507                 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
   508             qed
   509             with i3
   510             have puI3: "?puI3" by (simp add:reachable_def) 
   511             moreover
   512             
   513             -- "If it is reachable and not marked, it is still reachable using..."
   514             let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
   515             let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
   516             let ?T = "{t}"
   517             have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
   518             proof (rule still_reachable)
   519               show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
   520                 by (fastsimp simp:new_stack_eq addrs_def intro:self_reachable)
   521             next
   522               show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
   523                 by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) 
   524                    (fastsimp simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
   525             qed
   526             then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
   527               by blast
   528             have ?puI4
   529             proof (rule allI, rule impI)
   530               fix x
   531               assume a: "x \<in> R \<and> \<not> ?new_m x"
   532               have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
   533               with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
   534                 by (fastsimp simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
   535               have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
   536                 using xDisj a n_m_addr_t
   537                 by (clarsimp simp add:addrs_def addr_t_eq) 
   538               from inc exc subset  show "x \<in> reachable ?Rb ?B" 
   539                 by (auto simp add:reachable_def)
   540             qed  
   541             moreover
   542             
   543             -- "If it is marked, then it is reachable"
   544             from i5
   545             have "?puI5"
   546               by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
   547             moreover
   548             
   549             -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
   550             from i6 
   551             have "?puI6"
   552               by (simp add:new_stack_eq)
   553             moreover
   554 
   555             -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
   556             from stackDist i6 t_notin_stack i7
   557             have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
   558 
   559             ultimately show ?thesis by auto
   560           qed
   561           then have "\<exists>stack. ?puInv stack" by blast
   562 
   563         }
   564         ultimately show ?thesis by blast
   565       qed
   566     }
   567   qed
   568 
   569 end
   570