src/HOL/Hoare/SchorrWaite.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 62042 6c6ccf573479 child 67410 64d928bacddd permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     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 \<open>Machinery for the Schorr-Waite proof\<close>
```
```    12
```
```    13 definition
```
```    14   \<comment> "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 \<open>Rewrite rules for relations induced by a mapping\<close>
```
```    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   \<comment> "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 \<open>Rewrite rules for the restriction of a relation\<close>
```
```    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   \<comment> "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 \<open>Rewrite rules for Lists using S as their mapping\<close>
```
```   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   \<comment>"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 \<open>Rewrite rules for stkOk\<close>
```
```   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\<open>The Schorr-Waite algorithm\<close>
```
```   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             \<comment> \<open>List property is maintained:\<close>
```
```   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             \<comment> \<open>Everything on the stack is marked:\<close>
```
```   286             from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
```
```   287             moreover
```
```   288
```
```   289             \<comment> \<open>Everything is still reachable:\<close>
```
```   290             let "(R = reachable ?Ra ?A)" = "?I3"
```
```   291             let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
```
```   292             let "?B" = "{p, p^.r}"
```
```   293             \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
```
```   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             \<comment> "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             \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
```
```   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             \<comment> "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               \<comment> \<open>First, a disjunction on @{term"p^.r"} used later in the proof\<close>
```
```   342               have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2
```
```   343                 by auto
```
```   344               \<comment> \<open>@{term x} belongs to the left hand side of @{thm[source] subset}:\<close>
```
```   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               \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
```
```   348               \<comment> \<open>which corresponds to our goal.\<close>
```
```   349               from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
```
```   350             qed
```
```   351             moreover
```
```   352
```
```   353             \<comment> "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             \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
```
```   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             \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
```
```   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         \<comment> "Proofs of the Swing and Push arm follow."
```
```   375         \<comment> "Since they are in principle simmilar to the Pop arm proof,"
```
```   376         \<comment> "we show fewer comments and use frequent pattern matching."
```
```   377         {
```
```   378           \<comment> "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             \<comment> \<open>List property is maintained:\<close>
```
```   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             \<comment> \<open>Everything on the stack is marked:\<close>
```
```   397             from i2
```
```   398             have swI2: "?swI2" .
```
```   399             moreover
```
```   400
```
```   401             \<comment> \<open>Everything is still reachable:\<close>
```
```   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             \<comment> "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             \<comment> "If it is marked, then it is reachable"
```
```   453             from i5
```
```   454             have "?swI5" .
```
```   455             moreover
```
```   456
```
```   457             \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
```
```   458             from i6 stack_eq
```
```   459             have "?swI6"
```
```   460               by clarsimp
```
```   461             moreover
```
```   462
```
```   463             \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
```
```   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           \<comment> "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             \<comment> \<open>List property is maintained:\<close>
```
```   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             \<comment> \<open>Everything on the stack is marked:\<close>
```
```   493             from i2
```
```   494             have puI2: "?puI2"
```
```   495               by (simp add:new_stack_eq fun_upd_apply)
```
```   496             moreover
```
```   497
```
```   498             \<comment> \<open>Everything is still reachable:\<close>
```
```   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             \<comment> "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             \<comment> "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             \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close>
```
```   556             from i6
```
```   557             have "?puI6"
```
```   558               by (simp add:new_stack_eq)
```
```   559             moreover
```
```   560
```
```   561             \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close>
```
```   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
```