# Theory SchorrWaite

theory SchorrWaite
imports HeapSyntax
```(*  Title:      HOL/Hoare/SchorrWaite.thy

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

theory SchorrWaite imports HeapSyntax begin

section ‹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: "⟦B⊆Ra⇧*``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: "⟦ 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} = {}"
done

lemma reachable_empty: "reachable mS {} = {}"
done

lemma reachable_union: "(reachable mS aS ∪ reachable mS bS) = reachable mS (aS ∪ bS)"
apply blast
done

lemma reachable_union_sym: "reachable r (insert a aS) = (r⇧* `` addrs {a}) ∪ reachable r aS"
apply blast
done

lemma rel_upd1: "(a,b) ∉ rel (r(q:=t)) ⟹ (a,b) ∈ rel r ⟹ a=q"
apply (rule classical)
done

lemma rel_upd2: "(a,b)  ∉ rel r ⟹ (a,b) ∈ rel (r(q:=t)) ⟹ a=q"
apply (rule classical)
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"

lemma restr_rtrancl[simp]: " ⟦m l⟧ ⟹ (R | m)⇧* `` {l} = {l}"

lemma [simp]: " ⟦m l⟧ ⟹ (l,x) ∈ (R | m)⇧* = (l=x)"

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)"

lemma rel_upd3: "(a, b) ∉ (r|(m(q := t))) ⟹ (a,b) ∈ (r|m) ⟹ a = q "
apply (rule classical)
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)
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)
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)
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)
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 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 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) ∧ (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
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"

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)
intro:oneStep_reachable Image_iff[THEN iffD2])
show "∀(x,y) ∈ ?Ra-?Rb. y ∈ (?Rb⇧* `` addrs ?B)" by (clarsimp simp:relS_def)
qed
show "?R ⊆ ?L"
proof (rule still_reachable)
intro:oneStep_reachable Image_iff[THEN iffD2])
next
by (clarsimp simp:relS_def)
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}"

proof (rule still_reachable)
have rewrite: "∀s∈set stack_tl. (r(p → t)) s = r s"
by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
by (clarsimp simp:restr_def relS_def)
qed
― ‹We now bring a term from the right to the left of the subset relation.›
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)
― ‹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"

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"

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
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"
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"
proof (rule still_reachable_eq)
next
next
next
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}"
proof (rule still_reachable)
have rewrite: "(∀s∈set stack_tl. (r(addr p := l(addr p))) s = r s)"
by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
next
qed
by blast
have ?swI4
proof (rule allI, rule impI)
fix x
assume a: "x ∈ R ∧¬ m x"
by (simp only:reachable_def, clarsimp)
with ifB1 a
have exc: "x ∉ ?Rb⇧*`` addrs ?T"
from inc exc subset  show "x ∈ reachable ?Rb ?B"
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"

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
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"
moreover

― ‹Everything on the stack is marked:›
from i2
have puI2: "?puI2"
moreover

― ‹Everything is still reachable:›
let "R = reachable ?Ra ?A" = "?I3"
let "R = reachable ?Rb ?B" = "?puI3"
proof (rule still_reachable_eq)
next
next
next
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}"
proof (rule still_reachable)
next
by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
qed
by blast
have ?puI4
proof (rule allI, rule impI)
fix x
assume a: "x ∈ R ∧ ¬ ?new_m x"
with i4 a have inc: "x ∈ ?Ra⇧*``addrs ?A"
have exc: "x ∉ ?Rb⇧*`` addrs ?T"
from inc exc subset  show "x ∈ reachable ?Rb ?B"
qed
moreover

― ‹If it is marked, then it is reachable›
from i5
have "?puI5"
moreover

― ‹If it is not on the stack, then its @{term l} and @{term r} fields are unchanged›
from i6
have "?puI6"
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

```