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