# HG changeset patch
# User wenzelm
# Date 1729262573 -7200
# Node ID 60fedd5b7c5813621ae4a6d026aa3dcca88ecf49
# Parent  47a0dfee26eaadd565b98349aa1f83a8a53f22cd
tuned whitespace;

diff -r 47a0dfee26ea -r 60fedd5b7c58 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Fri Oct 18 16:37:39 2024 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Fri Oct 18 16:42:53 2024 +0200
@@ -153,7 +153,7 @@
 where
   stkOk_nil:  "stkOk c l r iL iR t [] = True"
 | stkOk_cons:
-    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and> 
+    "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and>
       iL p = (if c p then l p else t) \<and>
       iR p = (if c p then t else r p))"
 
@@ -198,9 +198,9 @@
 
 subsection \<open>The Schorr-Waite algorithm\<close>
 
-theorem SchorrWaiteAlgorithm: 
+theorem SchorrWaiteAlgorithm:
 "VARS c m l r t p q root
- {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l} 
+ {R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l}
  t := root; p := Null;
  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
  INV {\<exists>stack.
@@ -216,7 +216,7 @@
       THEN IF p^.c
                THEN q := t; t := p; p := p^.r; t^.r := q                \<comment> \<open>\<open>pop\<close>\<close>
                ELSE q := t; t := p^.r; p^.r := p^.l;                    \<comment> \<open>\<open>swing\<close>\<close>
-                        p^.l := q; p^.c := True          FI    
+                        p^.l := q; p^.c := True          FI
       ELSE q := p; p := t; t := t^.l; p^.l := q;                        \<comment> \<open>\<open>push\<close>\<close>
                p^.m := True; p^.c := False            FI       OD
  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
@@ -226,15 +226,13 @@
          (Aseq _ (Aseq _ (Awhile {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ _))) _")
 proof (vcg)
   {
-
     fix c m l r t p q root
     assume "?Pre c m l r root"
     thus "?inv c m l r root Null"  by (auto simp add: reachable_def addrs_def)
   next
-
     fix c m l r t p q
     let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
-    assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"  
+    assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"
     then obtain stack where inv: "?Inv stack" by blast
     from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
     let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _"  =  "?Inv stack"
@@ -242,336 +240,335 @@
     from pNull i1 have stackEmpty: "stack = []" by simp
     from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
     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)
-
-  next   
-      fix c m l r t p q root
-      let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
-      let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
-      let "\<exists>stack. ?swInv stack"  =
-        "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
-      let "\<exists>stack. ?puInv stack"  =
-        "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
-      let "?ifB1"  =  "(t = Null \<or> t^.m)"
-      let "?ifB2"  =  "p^.c" 
-
-      assume "(\<exists>stack.?Inv stack) \<and> ?whileB m t p"
-      then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
-      let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
-      from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
-                  and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+        
-      have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
+  next
+    fix c m l r t p q root
+    let "\<exists>stack. ?Inv stack"  =  "?inv c m l r t p"
+    let "\<exists>stack. ?popInv stack"  =  "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
+    let "\<exists>stack. ?swInv stack"  =
+      "?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
+    let "\<exists>stack. ?puInv stack"  =
+      "?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
+    let "?ifB1"  =  "(t = Null \<or> t^.m)"
+    let "?ifB2"  =  "p^.c"
 
-      show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> 
-                            (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
-              (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
-      proof - 
-        {
-          assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
-          from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
-          then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
-          with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
-            by auto
-          with i2 have m_addr_p: "p^.m" by auto
-          have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
-          from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
-          let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
-          have "?popInv stack_tl"
-          proof -
-
-            \<comment> \<open>List property is maintained:\<close>
-            from i1 p_notin_stack_tl ifB2
-            have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" 
-              by(simp add: addr_p_eq stack_eq, simp add: S_def)
+    assume "(\<exists>stack.?Inv stack) \<and> ?whileB m t p"
+    then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
+    let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
+    from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
+                and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+
+    have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
 
-            moreover
-            \<comment> \<open>Everything on the stack is marked:\<close>
-            from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
-            moreover
+    show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and>
+                          (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
+            (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
+    proof -
+      {
+        assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
+        from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
+        then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
+        with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
+          by auto
+        with i2 have m_addr_p: "p^.m" by auto
+        have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
+        from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
+        let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
+        have "?popInv stack_tl"
+        proof -
 
-            \<comment> \<open>Everything is still reachable:\<close>
-            let "(R = reachable ?Ra ?A)" = "?I3"
-            let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
-            let "?B" = "{p, p^.r}"
-            \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
-            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
-            proof
-              show "?L \<subseteq> ?R"
-              proof (rule still_reachable)
-                show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq 
-                     intro:oneStep_reachable Image_iff[THEN iffD2])
-                show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) 
-                     (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
-              qed
-              show "?R \<subseteq> ?L"
-              proof (rule still_reachable)
-                show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
-                  by(fastforce simp:addrs_def rel_defs addr_p_eq 
-                      intro:oneStep_reachable Image_iff[THEN iffD2])
-              next
-                show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
-                  by (clarsimp simp:relS_def) 
-                     (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
-              qed
-            qed
-            with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def) 
-            moreover
+          \<comment> \<open>List property is maintained:\<close>
+          from i1 p_notin_stack_tl ifB2
+          have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl"
+            by(simp add: addr_p_eq stack_eq, simp add: S_def)
 
-            \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
-            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4        
-            let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
-            let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
-            \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
-            let ?T = "{t, p^.r}"
+          moreover
+          \<comment> \<open>Everything on the stack is marked:\<close>
+          from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
+          moreover
 
-            have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
+          \<comment> \<open>Everything is still reachable:\<close>
+          let "(R = reachable ?Ra ?A)" = "?I3"
+          let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
+          let "?B" = "{p, p^.r}"
+          \<comment> \<open>Our goal is \<open>R = reachable ?Rb ?B\<close>.\<close>
+          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
+          proof
+            show "?L \<subseteq> ?R"
             proof (rule still_reachable)
-              have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
-                by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
-              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
-                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
-              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
-                by (clarsimp simp:restr_def relS_def) 
-                  (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
-            qed
-            \<comment> \<open>We now bring a term from the right to the left of the subset relation.\<close>
-            hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
-              by blast
-            have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
-            proof (rule allI, rule impI)
-              fix x
-              assume a: "x \<in> R \<and> \<not> m x"
-              \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
-              have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 
-                by auto
-              \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close>
-              have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
-              have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
-              \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
-              \<comment> \<open>which corresponds to our goal.\<close>
-              from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
+              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq
+                   intro:oneStep_reachable Image_iff[THEN iffD2])
+              show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def)
+                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
             qed
-            moreover
-
-            \<comment> \<open>If it is marked, then it is reachable\<close>
-            from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
-            moreover
-
-            \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
-            from i7 i6 ifB2 
-            have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" 
-              by(auto simp: addr_p_eq stack_eq fun_upd_apply)
-
-            moreover
-
-            \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
-            from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
-              by (clarsimp simp:stack_eq addr_p_eq)
-
-            ultimately show "?popInv stack_tl" by simp
-          qed
-          hence "\<exists>stack. ?popInv stack" ..
-        }
-        moreover
-
-        \<comment> \<open>Proofs of the Swing and Push arm follow.\<close>
-        \<comment> \<open>Since they are in principle simmilar to the Pop arm proof,\<close>
-        \<comment> \<open>we show fewer comments and use frequent pattern matching.\<close>
-        {
-          \<comment> \<open>Swing arm\<close>
-          assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
-          from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
-          then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
-          with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
-          with i2 have m_addr_p: "p^.m" by clarsimp
-          from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
-            by simp
-          let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
-          have "?swInv stack"
-          proof -
-            
-            \<comment> \<open>List property is maintained:\<close>
-            from i1 p_notin_stack_tl nifB2
-            have swI1: "?swI1"
-              by (simp add:addr_p_eq stack_eq, simp add:S_def)
-            moreover
-            
-            \<comment> \<open>Everything on the stack is marked:\<close>
-            from i2
-            have swI2: "?swI2" .
-            moreover
-            
-            \<comment> \<open>Everything is still reachable:\<close>
-            let "R = reachable ?Ra ?A" = "?I3"
-            let "R = reachable ?Rb ?B" = "?swI3"
-            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
-            proof (rule still_reachable_eq)
-              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
-                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
-            next
+            show "?R \<subseteq> ?L"
+            proof (rule still_reachable)
               show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
-                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
-            next
-              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
-                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+                by(fastforce simp:addrs_def rel_defs addr_p_eq
+                    intro:oneStep_reachable Image_iff[THEN iffD2])
             next
               show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
-                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
-            qed
-            with i3
-            have swI3: "?swI3" by (simp add:reachable_def) 
-            moreover
-
-            \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
-            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
-            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
-            let ?T = "{t}"
-            have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
-            proof (rule still_reachable)
-              have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
-                by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
-              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
-                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
-            next
-              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
-                by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+                by (clarsimp simp:relS_def)
+                   (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
             qed
-            then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
-              by blast
-            have ?swI4
-            proof (rule allI, rule impI)
-              fix x
-              assume a: "x \<in> R \<and>\<not> m x"
-              with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" 
-                by (simp only:reachable_def, clarsimp)
-              with ifB1 a 
-              have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" 
-                by (auto simp add:addrs_def)
-              from inc exc subset  show "x \<in> reachable ?Rb ?B" 
-                by (auto simp add:reachable_def)
-            qed
-            moreover
-            
-            \<comment> \<open>If it is marked, then it is reachable\<close>
-            from i5
-            have "?swI5" .
-            moreover
+          qed
+          with i3 have poI3: "R = reachable ?Rb ?B"  by (simp add:reachable_def)
+          moreover
+
+          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
+          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A"  =  ?I4
+          let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
+          let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
+          \<comment> \<open>Our goal is \<open>\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B\<close>.\<close>
+          let ?T = "{t, p^.r}"
+
+          have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
+          proof (rule still_reachable)
+            have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
+              by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
+            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
+              by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
+            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
+              by (clarsimp simp:restr_def relS_def)
+                (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
+          qed
+          \<comment> \<open>We now bring a term from the right to the left of the subset relation.\<close>
+          hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
+            by blast
+          have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
+          proof (rule allI, rule impI)
+            fix x
+            assume a: "x \<in> R \<and> \<not> m x"
+            \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
+            have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2
+              by auto
+            \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close>
+            have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
+            have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
+            \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close>
+            \<comment> \<open>which corresponds to our goal.\<close>
+            from incl excl subset  show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
+          qed
+          moreover
+
+          \<comment> \<open>If it is marked, then it is reachable\<close>
+          from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
+          moreover
+
+          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
+          from i7 i6 ifB2
+          have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x"
+            by(auto simp: addr_p_eq stack_eq fun_upd_apply)
+
+          moreover
 
-            \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
-            from i6 stack_eq
-            have "?swI6"
-              by clarsimp           
-            moreover
+          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
+          from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
+            by (clarsimp simp:stack_eq addr_p_eq)
+
+          ultimately show "?popInv stack_tl" by simp
+        qed
+        hence "\<exists>stack. ?popInv stack" ..
+      }
+      moreover
+
+      \<comment> \<open>Proofs of the Swing and Push arm follow.\<close>
+      \<comment> \<open>Since they are in principle simmilar to the Pop arm proof,\<close>
+      \<comment> \<open>we show fewer comments and use frequent pattern matching.\<close>
+      {
+        \<comment> \<open>Swing arm\<close>
+        assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
+        from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
+        then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
+        with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
+        with i2 have m_addr_p: "p^.m" by clarsimp
+        from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
+          by simp
+        let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
+        have "?swInv stack"
+        proof -
 
-            \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
-            from stackDist i7 nifB2 
-            have "?swI7"
-              by (clarsimp simp:addr_p_eq stack_eq)
+          \<comment> \<open>List property is maintained:\<close>
+          from i1 p_notin_stack_tl nifB2
+          have swI1: "?swI1"
+            by (simp add:addr_p_eq stack_eq, simp add:S_def)
+          moreover
+
+          \<comment> \<open>Everything on the stack is marked:\<close>
+          from i2
+          have swI2: "?swI2" .
+          moreover
 
-            ultimately show ?thesis by auto
+          \<comment> \<open>Everything is still reachable:\<close>
+          let "R = reachable ?Ra ?A" = "?I3"
+          let "R = reachable ?Rb ?B" = "?swI3"
+          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
+          proof (rule still_reachable_eq)
+            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
+              by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+          next
+            show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
+              by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+          next
+            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
+              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+          next
+            show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
+              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
           qed
-          then have "\<exists>stack. ?swInv stack" by blast
-        }
-        moreover
+          with i3
+          have swI3: "?swI3" by (simp add:reachable_def)
+          moreover
 
-        {
-          \<comment> \<open>Push arm\<close>
-          assume nifB1: "\<not>?ifB1"
-          from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
-          then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
-          with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
-          from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
-          with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
-          let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
-          have "?puInv new_stack"
-          proof -
-            
-            \<comment> \<open>List property is maintained:\<close>
-            from i1 t_notin_stack
-            have puI1: "?puI1"
-              by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
-            moreover
-            
-            \<comment> \<open>Everything on the stack is marked:\<close>
-            from i2
-            have puI2: "?puI2" 
-              by (simp add:new_stack_eq fun_upd_apply)
-            moreover
-            
-            \<comment> \<open>Everything is still reachable:\<close>
-            let "R = reachable ?Ra ?A" = "?I3"
-            let "R = reachable ?Rb ?B" = "?puI3"
-            have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
-            proof (rule still_reachable_eq)
-              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
-                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
-            next
-              show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
-                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
-            next
-              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
-                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
-            next
-              show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
-                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
-            qed
-            with i3
-            have puI3: "?puI3" by (simp add:reachable_def) 
-            moreover
-            
-            \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
-            let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
-            let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
-            let ?T = "{t}"
-            have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
-            proof (rule still_reachable)
-              show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
-                by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
-            next
-              show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
-                by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) 
-                   (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
-            qed
-            then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
-              by blast
-            have ?puI4
-            proof (rule allI, rule impI)
-              fix x
-              assume a: "x \<in> R \<and> \<not> ?new_m x"
-              have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
-              with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
-                by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
-              have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
-                using xDisj a n_m_addr_t
-                by (clarsimp simp add:addrs_def addr_t_eq) 
-              from inc exc subset  show "x \<in> reachable ?Rb ?B" 
-                by (auto simp add:reachable_def)
-            qed  
-            moreover
-            
-            \<comment> \<open>If it is marked, then it is reachable\<close>
-            from i5
-            have "?puI5"
-              by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
-            moreover
-            
-            \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
-            from i6 
-            have "?puI6"
-              by (simp add:new_stack_eq)
-            moreover
+          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
+          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
+          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
+          let ?T = "{t}"
+          have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
+          proof (rule still_reachable)
+            have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
+              by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
+            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
+              by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
+          next
+            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
+              by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+          qed
+          then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
+            by blast
+          have ?swI4
+          proof (rule allI, rule impI)
+            fix x
+            assume a: "x \<in> R \<and>\<not> m x"
+            with i4 addr_p_eq stack_eq  have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
+              by (simp only:reachable_def, clarsimp)
+            with ifB1 a
+            have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
+              by (auto simp add:addrs_def)
+            from inc exc subset  show "x \<in> reachable ?Rb ?B"
+              by (auto simp add:reachable_def)
+          qed
+          moreover
+
+          \<comment> \<open>If it is marked, then it is reachable\<close>
+          from i5
+          have "?swI5" .
+          moreover
+
+          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
+          from i6 stack_eq
+          have "?swI6"
+            by clarsimp
+          moreover
+
+          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
+          from stackDist i7 nifB2
+          have "?swI7"
+            by (clarsimp simp:addr_p_eq stack_eq)
+
+          ultimately show ?thesis by auto
+        qed
+        then have "\<exists>stack. ?swInv stack" by blast
+      }
+      moreover
+
+      {
+        \<comment> \<open>Push arm\<close>
+        assume nifB1: "\<not>?ifB1"
+        from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
+        then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
+        with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
+        from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
+        with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
+        let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
+        have "?puInv new_stack"
+        proof -
+
+          \<comment> \<open>List property is maintained:\<close>
+          from i1 t_notin_stack
+          have puI1: "?puI1"
+            by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
+          moreover
+
+          \<comment> \<open>Everything on the stack is marked:\<close>
+          from i2
+          have puI2: "?puI2"
+            by (simp add:new_stack_eq fun_upd_apply)
+          moreover
 
-            \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
-            from stackDist i6 t_notin_stack i7
-            have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
+          \<comment> \<open>Everything is still reachable:\<close>
+          let "R = reachable ?Ra ?A" = "?I3"
+          let "R = reachable ?Rb ?B" = "?puI3"
+          have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
+          proof (rule still_reachable_eq)
+            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
+              by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+          next
+            show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
+              by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+          next
+            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
+              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
+          next
+            show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
+              by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
+          qed
+          with i3
+          have puI3: "?puI3" by (simp add:reachable_def)
+          moreover
 
-            ultimately show ?thesis by auto
+          \<comment> \<open>If it is reachable and not marked, it is still reachable using...\<close>
+          let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
+          let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
+          let ?T = "{t}"
+          have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
+          proof (rule still_reachable)
+            show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
+              by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
+          next
+            show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
+              by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
+                 (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
           qed
-          then have "\<exists>stack. ?puInv stack" by blast
+          then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
+            by blast
+          have ?puI4
+          proof (rule allI, rule impI)
+            fix x
+            assume a: "x \<in> R \<and> \<not> ?new_m x"
+            have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
+            with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
+              by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
+            have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
+              using xDisj a n_m_addr_t
+              by (clarsimp simp add:addrs_def addr_t_eq)
+            from inc exc subset  show "x \<in> reachable ?Rb ?B"
+              by (auto simp add:reachable_def)
+          qed
+          moreover
 
-        }
-        ultimately show ?thesis by blast
-      qed
-    }
-  qed
+          \<comment> \<open>If it is marked, then it is reachable\<close>
+          from i5
+          have "?puI5"
+            by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
+          moreover
+
+          \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close>
+          from i6
+          have "?puI6"
+            by (simp add:new_stack_eq)
+          moreover
+
+          \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close>
+          from stackDist i6 t_notin_stack i7
+          have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
+
+          ultimately show ?thesis by auto
+        qed
+        then have "\<exists>stack. ?puInv stack" by blast
+
+      }
+      ultimately show ?thesis by blast
+    qed
+  }
+qed
 
 end