Theory SchorrWaite

(*  Title:      HOL/Hoare/SchorrWaite.thy
    Author:     Farhad Mehta
    Copyright   2003 TUM
*)

section ‹Proof of the Schorr-Waite graph marking algorithm›

theory SchorrWaite
  imports HeapSyntax
begin

subsection ‹Machinery for the Schorr-Waite proof›

definition
  ― ‹Relations induced by a mapping›
  rel :: "('a  'a ref)  ('a × 'a) set"
  where "rel m = {(x,y). m x = Ref y}"

definition
  relS :: "('a  'a ref) set  ('a × 'a) set"
  where "relS M = (m  M. rel m)"

definition
  addrs :: "'a ref set  'a set"
  where "addrs P = {a. Ref a  P}"

definition
  reachable :: "('a × 'a) set  'a ref set  'a set"
  where "reachable r P = (r* `` addrs P)"

lemmas rel_defs = relS_def rel_def

text ‹Rewrite rules for relations induced by a mapping›

lemma self_reachable: "b  B  b  R* `` B"
apply blast
done

lemma oneStep_reachable: "b  R``B  b  R* `` B"
apply blast
done

lemma still_reachable: "BRa*``A;  (x,y)  Rb-Ra. y (Ra*``A)  Rb* `` B  Ra* `` A "
apply (clarsimp simp only:Image_iff)
apply (erule rtrancl_induct)
 apply blast
apply (subgoal_tac "(y, z)  Ra(Rb-Ra)")
 apply (erule UnE)
 apply (auto intro:rtrancl_into_rtrancl)
apply blast
done

lemma still_reachable_eq: " ARb*``B; BRa*``A;  (x,y)  Ra-Rb. y (Rb*``B);  (x,y)  Rb-Ra. y (Ra*``A)  Ra*``A =  Rb*``B "
apply (rule equalityI)
 apply (erule still_reachable ,assumption)+
done

lemma reachable_null: "reachable mS {Null} = {}"
apply (simp add: reachable_def addrs_def)
done

lemma reachable_empty: "reachable mS {} = {}"
apply (simp add: reachable_def addrs_def)
done

lemma reachable_union: "(reachable mS aS  reachable mS bS) = reachable mS (aS  bS)"
apply (simp add: reachable_def rel_defs addrs_def)
apply blast
done

lemma reachable_union_sym: "reachable r (insert a aS) = (r* `` addrs {a})  reachable r aS"
apply (simp add: reachable_def rel_defs addrs_def)
apply blast
done

lemma rel_upd1: "(a,b)  rel (r(q:=t))  (a,b)  rel r  a=q"
apply (rule classical)
apply (simp add:rel_defs fun_upd_apply)
done

lemma rel_upd2: "(a,b)   rel r  (a,b)  rel (r(q:=t))  a=q"
apply (rule classical)
apply (simp add:rel_defs fun_upd_apply)
done

definition
  ― ‹Restriction of a relation›
  restr ::"('a × 'a) set  ('a  bool)  ('a × 'a) set"       ("(_/ | _)" [50, 51] 50)
  where "restr r m = {(x,y). (x,y)  r  ¬ m x}"

text ‹Rewrite rules for the restriction of a relation›

lemma restr_identity[simp]:
 " (x. ¬ m x)  (R |m) = R"
by (auto simp add:restr_def)

lemma restr_rtrancl[simp]: " m l  (R | m)* `` {l} = {l}"
by (auto simp add:restr_def elim:converse_rtranclE)

lemma [simp]: " m l  (l,x)  (R | m)* = (l=x)"
by (auto simp add:restr_def elim:converse_rtranclE)

lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
apply (auto simp:restr_def rel_def fun_upd_apply)
apply (rename_tac a b)
apply (case_tac "a=q")
 apply auto
done

lemma restr_un: "((r  s)|m) = (r|m)  (s|m)"
  by (auto simp add:restr_def)

lemma rel_upd3: "(a, b)  (r|(m(q := t)))  (a,b)  (r|m)  a = q "
apply (rule classical)
apply (simp add:restr_def fun_upd_apply)
done

definition
  ― ‹A short form for the stack mapping function for List›
  S :: "('a  bool)  ('a  'a ref)  ('a  'a ref)  ('a  'a ref)"
  where "S c l r = (λx. if c x then r x else l x)"

text ‹Rewrite rules for Lists using S as their mapping›

lemma [rule_format,simp]:
 "p. a  set stack  List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
apply(induct_tac stack)
 apply(simp add:fun_upd_apply S_def)+
done

lemma [rule_format,simp]:
 "p. a  set stack  List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
apply(induct_tac stack)
 apply(simp add:fun_upd_apply S_def)+
done

lemma [rule_format,simp]:
 "p. a  set stack  List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
apply(induct_tac stack)
 apply(simp add:fun_upd_apply S_def)+
done

lemma [rule_format,simp]:
 "p. a  set stack  List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
apply(induct_tac stack)
 apply(simp add:fun_upd_apply S_def)+
done

primrec
  ― ‹Recursive definition of what is means for a the graph/stack structure to be reconstructible›
  stkOk :: "('a  bool)  ('a  'a ref)  ('a  'a ref)  ('a  'a ref)  ('a  'a ref)  'a ref 'a list   bool"
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)  
      iL p = (if c p then l p else t) 
      iR p = (if c p then t else r p))"

text ‹Rewrite rules for stkOk›

lemma [simp]: "t.  x  set xs; Ref xt  
  stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done

lemma [simp]: "t.  x  set xs; Ref xt  
 stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done

lemma [simp]: "t.  x  set xs; Ref xt  
 stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done

lemma stkOk_r_rewrite [simp]: "x. x  set xs 
  stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done

lemma [simp]: "x. x  set xs 
 stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done

lemma [simp]: "x. x  set xs 
 stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
apply (induct xs)
 apply (auto simp:eq_sym_conv)
done


subsection ‹The Schorr-Waite algorithm›

theorem SchorrWaiteAlgorithm: 
"VARS c m l r t p q root
 {R = reachable (relS {l, r}) {root}  (x. ¬ m x)  iR = r  iL = l} 
 t := root; p := Null;
 WHILE p  Null  t  Null  ¬ t^.m
 INV {stack.
          List (S c l r) p stack                                       ― ‹i1›
          (x  set stack. m x)                                        ― ‹i2›
          R = reachable (relS{l, r}) {t,p}                             ― ‹i3›
          (x. x  R  ¬m x                                          ― ‹i4›
                 x  reachable (relS{l,r}|m) ({t}set(map r stack))) 
          (x. m x  x  R)                                          ― ‹i5›
          (x. x  set stack  r x = iR x  l x = iL x)              ― ‹i6›
          (stkOk c l r iL iR t stack)                                   ― ‹i7›}
 DO IF t = Null  t^.m
      THEN IF p^.c
               THEN q := t; t := p; p := p^.r; t^.r := q                ― ‹pop›
               ELSE q := t; t := p^.r; p^.r := p^.l;                    ― ‹swing›
                        p^.l := q; p^.c := True          FI    
      ELSE q := p; p := t; t := t^.l; p^.l := q;                        ― ‹push›
               p^.m := True; p^.c := False            FI       OD
 {(x. (x  R) = m x)  (r = iR  l = iL) }"
  (is "Valid
         {(c, m, l, r, t, p, q, root). ?Pre c m l r root}
         (Seq _ (Seq _ (While {(c, m, l, r, t, p, q, root). ?whileB m t p} _)))
         (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 "stack. ?Inv stack"  =  "?inv c m l r t p"
    assume a: "?inv c m l r t p  ¬(p  Null  t  Null  ¬ t^.m)"  
    then obtain stack where inv: "?Inv stack" by blast
    from a have pNull: "p = Null" and tDisj: "t=Null  (tNull  t^.m )" by auto
    let "?I1  _  _  ?I4  ?I5  ?I6  _"  =  "?Inv stack"
    from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
    from pNull i1 have stackEmpty: "stack = []" by simp
    from tDisj i4 have RisMarked[rule_format]: "x.  x  R  m x"  by(auto simp: reachable_def addrs_def stackEmpty)
    from i5 i6 show "(x.(x  R) = m x)  r = iR  l = iL"  by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)

  next   
      fix c m l r t p q root
      let "stack. ?Inv stack"  =  "?inv c m l r t p"
      let "stack. ?popInv stack"  =  "?inv c m l (r(p  t)) p (p^.r)"
      let "stack. ?swInv stack"  =
        "?inv (c(p  True)) m (l(p  t)) (r(p  p^.l)) (p^.r) p"
      let "stack. ?puInv stack"  =
        "?inv (c(t  False)) (m(t  True)) (l(t  p)) r (t^.l) t"
      let "?ifB1"  =  "(t = Null  t^.m)"
      let "?ifB2"  =  "p^.c" 

      assume "(stack.?Inv stack)  ?whileB m t p"
      then obtain stack where inv: "?Inv stack" and whileB: "?whileB m t p" by blast
      let "?I1  ?I2  ?I3  ?I4  ?I5  ?I6  ?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)

      show "(?ifB1  (?ifB2  (stack.?popInv stack))  
                            (¬?ifB2  (stack.?swInv stack)) ) 
              (¬?ifB1  (stack.?puInv stack))"
      proof - 
        {
          assume ifB1: "t = Null  t^.m" and ifB2: "p^.c"
          from ifB1 whileB have pNotNull: "p  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  set stack_tl" by simp
          let "?poI1 ?poI2 ?poI3 ?poI4 ?poI5 ?poI6 ?poI7" = "?popInv stack_tl"
          have "?popInv stack_tl"
          proof -

            ― ‹List property is maintained:›
            from i1 p_notin_stack_tl ifB2
            have poI1: "List (S c l (r(p  t))) (p^.r) stack_tl" 
              by(simp add: addr_p_eq stack_eq, simp add: S_def)

            moreover
            ― ‹Everything on the stack is marked:›
            from i2 have poI2: " x  set stack_tl. m x" by (simp add:stack_eq)
            moreover

            ― ‹Everything is still reachable:›
            let "(R = reachable ?Ra ?A)" = "?I3"
            let "?Rb" = "(relS {l, r(p  t)})"
            let "?B" = "{p, p^.r}"
            ― ‹Our goal is R = reachable ?Rb ?B›.›
            have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B" (is "?L = ?R")
            proof
              show "?L  ?R"
              proof (rule still_reachable)
                show "addrs ?A  ?Rb* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq 
                     intro:oneStep_reachable Image_iff[THEN iffD2])
                show "(x,y)  ?Ra-?Rb. y  (?Rb* `` addrs ?B)" by (clarsimp simp:relS_def) 
                     (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
              qed
              show "?R  ?L"
              proof (rule still_reachable)
                show "addrs ?B  ?Ra* `` addrs ?A"
                  by(fastforce simp:addrs_def rel_defs addr_p_eq 
                      intro:oneStep_reachable Image_iff[THEN iffD2])
              next
                show "(x, y)?Rb-?Ra. y(?Ra*``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

            ― ‹If it is reachable and not marked, it is still reachable using...›
            let "x. x  R  ¬ m x  x  reachable ?Ra ?A"  =  ?I4        
            let "?Rb" = "relS {l, r(p  t)} | m"
            let "?B" = "{p}  set (map (r(p  t)) stack_tl)"
            ― ‹Our goal is ∀x. x ∈ R ∧ ¬ m x ⟶ x ∈ reachable ?Rb ?B›.›
            let ?T = "{t, p^.r}"

            have "?Ra* `` addrs ?A  ?Rb* `` (addrs ?B  addrs ?T)"
            proof (rule still_reachable)
              have rewrite: "sset stack_tl. (r(p  t)) s = r s"
                by (auto simp add:p_notin_stack_tl intro:fun_upd_other) 
              show "addrs ?A  ?Rb* `` (addrs ?B  addrs ?T)"
                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
              show "(x, y)?Ra-?Rb. y(?Rb*``(addrs ?B  addrs ?T))"
                by (clarsimp simp:restr_def relS_def) 
                  (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
            qed
            ― ‹We now bring a term from the right to the left of the subset relation.›
            hence subset: "?Ra* `` addrs ?A - ?Rb* `` addrs ?T  ?Rb* `` addrs ?B"
              by blast
            have poI4: "x. x  R  ¬ m x  x  reachable ?Rb ?B"
            proof (rule allI, rule impI)
              fix x
              assume a: "x  R  ¬ m x"
              ― ‹First, a disjunction on termp^.r used later in the proof›
              have pDisj:"p^.r = Null  (p^.r  Null  p^.r^.m)" using poI1 poI2 
                by auto
              ― ‹termx belongs to the left hand side of @{thm[source] subset}:›
              have incl: "x  ?Ra*``addrs ?A" using  a i4 by (simp only:reachable_def, clarsimp)
              have excl: "x  ?Rb*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
              ― ‹And therefore also belongs to the right hand side of @{thm[source]subset},›
              ― ‹which corresponds to our goal.›
              from incl excl subset  show "x  reachable ?Rb ?B" by (auto simp add:reachable_def)
            qed
            moreover

            ― ‹If it is marked, then it is reachable›
            from i5 have poI5: "x. m x  x  R" .
            moreover

            ― ‹If it is not on the stack, then its terml and termr fields are unchanged›
            from i7 i6 ifB2 
            have poI6: "x. x  set stack_tl  (r(p  t)) x = iR x  l x = iL x" 
              by(auto simp: addr_p_eq stack_eq fun_upd_apply)

            moreover

            ― ‹If it is on the stack, then its terml and termr fields can be reconstructed›
            from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p  t)) iL iR p stack_tl"
              by (clarsimp simp:stack_eq addr_p_eq)

            ultimately show "?popInv stack_tl" by simp
          qed
          hence "stack. ?popInv stack" ..
        }
        moreover

        ― ‹Proofs of the Swing and Push arm follow.›
        ― ‹Since they are in principle simmilar to the Pop arm proof,›
        ― ‹we show fewer comments and use frequent pattern matching.›
        {
          ― ‹Swing arm›
          assume ifB1: "?ifB1" and nifB2: "¬?ifB2"
          from ifB1 whileB have pNotNull: "p  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)  set stack_tl"
            by simp
          let "?swI1?swI2?swI3?swI4?swI5?swI6?swI7" = "?swInv stack"
          have "?swInv stack"
          proof -
            
            ― ‹List property is maintained:›
            from i1 p_notin_stack_tl nifB2
            have swI1: "?swI1"
              by (simp add:addr_p_eq stack_eq, simp add:S_def)
            moreover
            
            ― ‹Everything on the stack is marked:›
            from i2
            have swI2: "?swI2" .
            moreover
            
            ― ‹Everything is still reachable:›
            let "R = reachable ?Ra ?A" = "?I3"
            let "R = reachable ?Rb ?B" = "?swI3"
            have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B"
            proof (rule still_reachable_eq)
              show "addrs ?A  ?Rb* `` addrs ?B"
                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
            next
              show "addrs ?B  ?Ra* `` addrs ?A"
                by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
            next
              show "(x, y)?Ra-?Rb. y(?Rb*``addrs ?B)"
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
            next
              show "(x, y)?Rb-?Ra. y(?Ra*``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

            ― ‹If it is reachable and not marked, it is still reachable using...›
            let "x. x  R  ¬ m x  x  reachable ?Ra ?A" = ?I4
            let "x. x  R  ¬ m x  x  reachable ?Rb ?B" = ?swI4
            let ?T = "{t}"
            have "?Ra*``addrs ?A  ?Rb*``(addrs ?B  addrs ?T)"
            proof (rule still_reachable)
              have rewrite: "(sset 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  ?Rb* `` (addrs ?B  addrs ?T)"
                by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
            next
              show "(x, y)?Ra-?Rb. y(?Rb*``(addrs ?B  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*``addrs ?A - ?Rb*``addrs ?T  ?Rb*``addrs ?B"
              by blast
            have ?swI4
            proof (rule allI, rule impI)
              fix x
              assume a: "x  R ¬ m x"
              with i4 addr_p_eq stack_eq  have inc: "x  ?Ra*``addrs ?A" 
                by (simp only:reachable_def, clarsimp)
              with ifB1 a 
              have exc: "x  ?Rb*`` addrs ?T" 
                by (auto simp add:addrs_def)
              from inc exc subset  show "x  reachable ?Rb ?B" 
                by (auto simp add:reachable_def)
            qed
            moreover
            
            ― ‹If it is marked, then it is reachable›
            from i5
            have "?swI5" .
            moreover

            ― ‹If it is not on the stack, then its terml and termr fields are unchanged›
            from i6 stack_eq
            have "?swI6"
              by clarsimp           
            moreover

            ― ‹If it is on the stack, then its terml and termr fields can be reconstructed›
            from stackDist i7 nifB2 
            have "?swI7"
              by (clarsimp simp:addr_p_eq stack_eq)

            ultimately show ?thesis by auto
          qed
          then have "stack. ?swInv stack" by blast
        }
        moreover

        {
          ― ‹Push arm›
          assume nifB1: "¬?ifB1"
          from nifB1 whileB have tNotNull: "t  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: "¬ (t^.m)" by clarsimp
          with i2 have t_notin_stack: "(addr t)  set stack" by blast
          let "?puI1?puI2?puI3?puI4?puI5?puI6?puI7" = "?puInv new_stack"
          have "?puInv new_stack"
          proof -
            
            ― ‹List property is maintained:›
            from i1 t_notin_stack
            have puI1: "?puI1"
              by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
            moreover
            
            ― ‹Everything on the stack is marked:›
            from i2
            have puI2: "?puI2" 
              by (simp add:new_stack_eq fun_upd_apply)
            moreover
            
            ― ‹Everything is still reachable:›
            let "R = reachable ?Ra ?A" = "?I3"
            let "R = reachable ?Rb ?B" = "?puI3"
            have "?Ra* `` addrs ?A = ?Rb* `` addrs ?B"
            proof (rule still_reachable_eq)
              show "addrs ?A  ?Rb* `` addrs ?B"
                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
            next
              show "addrs ?B  ?Ra* `` addrs ?A"
                by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
            next
              show "(x, y)?Ra-?Rb. y(?Rb*``addrs ?B)"
                by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
            next
              show "(x, y)?Rb-?Ra. y(?Ra*``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
            
            ― ‹If it is reachable and not marked, it is still reachable using...›
            let "x. x  R  ¬ m x  x  reachable ?Ra ?A" = ?I4
            let "x. x  R  ¬ ?new_m x  x  reachable ?Rb ?B" = ?puI4
            let ?T = "{t}"
            have "?Ra*``addrs ?A  ?Rb*``(addrs ?B  addrs ?T)"
            proof (rule still_reachable)
              show "addrs ?A  ?Rb* `` (addrs ?B  addrs ?T)"
                by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
            next
              show "(x, y)?Ra-?Rb. y(?Rb*``(addrs ?B  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*``addrs ?A - ?Rb*``addrs ?T  ?Rb*``addrs ?B"
              by blast
            have ?puI4
            proof (rule allI, rule impI)
              fix x
              assume a: "x  R  ¬ ?new_m x"
              have xDisj: "x=(addr t)  x(addr t)" by simp
              with i4 a have inc: "x  ?Ra*``addrs ?A"
                by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
              have exc: "x  ?Rb*`` addrs ?T"
                using xDisj a n_m_addr_t
                by (clarsimp simp add:addrs_def addr_t_eq) 
              from inc exc subset  show "x  reachable ?Rb ?B" 
                by (auto simp add:reachable_def)
            qed  
            moreover
            
            ― ‹If it is marked, then it is reachable›
            from i5
            have "?puI5"
              by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
            moreover
            
            ― ‹If it is not on the stack, then its terml and termr fields are unchanged›
            from i6 
            have "?puI6"
              by (simp add:new_stack_eq)
            moreover

            ― ‹If it is on the stack, then its terml and termr fields can be reconstructed›
            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 "stack. ?puInv stack" by blast

        }
        ultimately show ?thesis by blast
      qed
    }
  qed

end