# Theory SchorrWaite

Up to index of Isabelle/HOL/Hoare

theory SchorrWaite
imports HeapSyntax
begin

    (*  Title:      HOL/Hoare/SchorrWaite.thy
        ID:         $Id: SchorrWaite.thy,v 1.3 2005/06/17 14:13:07 haftmann Exp $
        Author:     Farhad Mehta
        Copyright   2003 TUM

    Proof of the Schorr-Waite graph marking algorithm.
    *)

    theory SchorrWaite imports HeapSyntax begin

    section {* Machinery for the Schorr-Waite proof*}

    constdefs
      -- "Relations induced by a mapping"
      rel :: "('a => 'a ref) => ('a × 'a) set"
      "rel m == {(x,y). m x = Ref y}"
      relS :: "('a => 'a ref) set => ('a × 'a) set"
      "relS M == (\<Union> m ∈ M. rel m)"
      addrs :: "'a ref set => 'a set"
      "addrs P == {a. Ref a ∈ P}"
      reachable :: "('a × 'a) set => 'a ref set => 'a set"
      "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: "[|B⊆Ra*``A; ∀ (x,y) ∈ Rb-Ra. y∈ (Ra*``A)|] ==> Rb* `` B ⊆ Ra* `` A "
    apply (clarsimp simp only:Image_iff intro:subsetI)
    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: "[| A⊆Rb*``B; B⊆Ra*``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

    constdefs
      -- "Restriction of a relation"
      restr ::"('a × 'a) set => ('a => bool) => ('a × 'a) set"       ("(_/ | _)" [50, 51] 50)
      "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

    constdefs
      -- "A short form for the stack mapping function for List"
      S :: "('a => bool) => ('a => 'a ref) => ('a => 'a ref) => ('a => 'a ref)"
      "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

    consts
      --"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"
    primrec
    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 x≠t |] ==>
      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 x≠t |] ==>
     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 x≠t |] ==>
     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

    section{*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 "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
    proof (vcg)
      let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
        {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
      {

        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 ∨ (t≠Null ∧ 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 expand_fun_eq 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) ∧ (p ≠ Null ∨ t ≠ Null ∧ ¬ t^.m)" (is "_ ∧ ?whileB")
          then obtain stack where inv: "?Inv stack" and whileB: "?whileB" 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 @{text"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(fastsimp 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)
                         (fastsimp 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(fastsimp 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)
                         (fastsimp 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 @{text"∀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: "∀s∈set 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 (fastsimp 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)
                      (fastsimp 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 @{term"p^.r"} used later in the proof*}
                  have pDisj:"p^.r = Null ∨ (p^.r ≠ Null ∧ p^.r^.m)" using poI1 poI2
                    by auto
                  -- {*@{term x} 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 @{term l} and @{term r} 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 @{term l} and @{term r} 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(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
                next
                  show "addrs ?B ⊆ ?Ra* `` addrs ?A"
                    by(fastsimp 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) (fastsimp 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) (fastsimp 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: "(∀s∈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 ⊆ ?Rb* `` (addrs ?B ∪ addrs ?T)"
                    by (fastsimp 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) (fastsimp 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 @{term l} and @{term r} fields are unchanged*}
                from i6 stack_eq
                have "?swI6"
                  by clarsimp
                moreover

                -- {*If it is on the stack, then its @{term l} and @{term r} 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(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
                next
                  show "addrs ?B ⊆ ?Ra* `` addrs ?A"
                    by(fastsimp 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) (fastsimp 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) (fastsimp 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 (fastsimp 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)
                       (fastsimp 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 (fastsimp 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 @{term l} and @{term r} fields are unchanged*}
                from i6
                have "?puI6"
                  by (simp add:new_stack_eq)
                moreover

                -- {*If it is on the stack, then its @{term l} and @{term r} 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

## Machinery for the Schorr-Waite proof

lemmas rel_defs:

      relS M == UN m:M. rel m

      rel m == {(x, y). m x = Ref y}

lemmas rel_defs:

      relS M == UN m:M. rel m

      rel m == {(x, y). m x = Ref y}

lemma self_reachable:

      b ∈ B ==> b ∈ R* `` B

lemma oneStep_reachable:

      b ∈ R `` B ==> b ∈ R* `` B

lemma still_reachable:

      [| B ⊆ Ra* `` A; ∀(x, y)∈Rb - Ra. y ∈ Ra* `` A |] ==> Rb* `` B ⊆ Ra* `` A

lemma still_reachable_eq:

      [| A ⊆ Rb* `` B; B ⊆ Ra* `` A; ∀(x, y)∈Ra - Rb. y ∈ Rb* `` B;
         ∀(x, y)∈Rb - Ra. y ∈ Ra* `` A |]
      ==> Ra* `` A = Rb* `` B

lemma reachable_null:

      reachable mS {Null} = {}

lemma reachable_empty:

      reachable mS {} = {}

lemma reachable_union:

      reachable mS aS ∪ reachable mS bS = reachable mS (aS ∪ bS)

lemma reachable_union_sym:

      reachable r (insert a aS) = r* `` addrs {a} ∪ reachable r aS

lemma rel_upd1:

      [| (a, b) ∉ rel (r(q := t)); (a, b) ∈ rel r |] ==> a = q

lemma rel_upd2:

      [| (a, b) ∉ rel r; (a, b) ∈ rel (r(q := t)) |] ==> a = q

lemma restr_identity:

      ∀x. ¬ m x ==> (R | m) = R

lemma restr_rtrancl:

      m l ==> (R | m)* `` {l} = {l}

lemma

      m l ==> ((l, x) ∈ (R | m)*) = (l = x)

lemma restr_upd:

      (rel (r(q := t)) | m(q := True)) = (rel r | m(q := True))

lemma restr_un:

      (r ∪ s | m) = (r | m) ∪ (s | m)

lemma rel_upd3:

      [| (a, b) ∉ (r | m(q := t)); (a, b) ∈ (r | m) |] ==> a = q

lemma

      a ∉ set stack
      ==> List (S c l r) p stack =
          List (S (c(a := x)) (l(a := y)) (r(a := z))) p stack

lemma

      a ∉ set stack ==> List (S c l (r(a := z))) p stack = List (S c l r) p stack

lemma

      a ∉ set stack ==> List (S c (l(a := z)) r) p stack = List (S c l r) p stack

lemma

      a ∉ set stack ==> List (S (c(a := z)) l r) p stack = List (S c l r) p stack

lemma

      [| x ∉ set xs; Ref x ≠ t |]
      ==> stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs

lemma

      [| x ∉ set xs; Ref x ≠ t |]
      ==> stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs

lemma

      [| x ∉ set xs; Ref x ≠ t |]
      ==> stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs

lemma stkOk_r_rewrite:

      x ∉ set xs
      ==> stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs

lemma

      x ∉ set xs
      ==> stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs

lemma

      x ∉ set xs
      ==> stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs

## The Schorr-Waite algorithm

theorem SchorrWaiteAlgorithm:

      {R = reachable (relS {l, r}) {root} ∧ (∀x. ¬ m x) ∧ iR = r ∧ iL = l}
       t := root;
       p := Null;
       WHILE p ≠ Null ∨ t ≠ Null ∧ ¬ m (addr t)
        INV {∃stack.
                List (S c l r) p stack ∧
                (∀x∈set stack. m x) ∧
                R = reachable (relS {l, r}) {t, p} ∧
                (∀x. x ∈ R ∧ ¬ m x -->
                     x ∈ reachable (relS {l, r} | m) ({t} ∪ set (map r stack))) ∧
                (∀x. m x --> x ∈ R) ∧
                (∀x. x ∉ set stack --> r x = iR x ∧ l x = iL x) ∧
                stkOk c l r iL iR t stack}
        DO IF t = Null ∨ m (addr t)
            THEN IF c (addr p) THEN q := t; t := p; p := r (addr p); r := r(t -> q)
                  ELSE q := t;
                       t := r (addr p);
                       r := r(p -> l (addr p)); l := l(p -> q); c := c(p -> True)
                  FI
            ELSE q := p;
                 p := t;
                 t := l (addr t);
                 l := l(p -> q); m := m(p -> True); c := c(p -> False)
            FI
        OD
       {(∀x. (x ∈ R) = m x) ∧ r = iR ∧ l = iL}