(* Title: HOL/Hoare/SchorrWaite.thy
Author: Farhad Mehta
Copyright 2003 TUM
*)
section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
theory SchorrWaite
imports HeapSyntax
begin
subsection \<open>Machinery for the Schorr-Waite proof\<close>
definition
\<comment> \<open>Relations induced by a mapping\<close>
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\<^sup>* `` addrs P)"
lemmas rel_defs = relS_def rel_def
text \<open>Rewrite rules for relations induced by a mapping\<close>
lemma self_reachable: "b \ B \ b \ R\<^sup>* `` B"
apply blast
done
lemma oneStep_reachable: "b \ R``B \ b \ R\<^sup>* `` B"
apply blast
done
lemma still_reachable: "\B\Ra\<^sup>*``A; \ (x,y) \ Rb-Ra. y\ (Ra\<^sup>*``A)\ \ Rb\<^sup>* `` B \ Ra\<^sup>* `` 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\<^sup>*``B; B\Ra\<^sup>*``A; \ (x,y) \ Ra-Rb. y \(Rb\<^sup>*``B); \ (x,y) \ Rb-Ra. y\ (Ra\<^sup>*``A)\ \ Ra\<^sup>*``A = Rb\<^sup>*``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\<^sup>* `` 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
\<comment> \<open>Restriction of a relation\<close>
restr ::"('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" ("(_/ | _)" [50, 51] 50)
where "restr r m = {(x,y). (x,y) \ r \ \ m x}"
text \<open>Rewrite rules for the restriction of a relation\<close>
lemma restr_identity[simp]:
" (\x. \ m x) \ (R |m) = R"
by (auto simp add:restr_def)
lemma restr_rtrancl[simp]: " \m l\ \ (R | m)\<^sup>* `` {l} = {l}"
by (auto simp add:restr_def elim:converse_rtranclE)
lemma [simp]: " \m l\ \ (l,x) \ (R | m)\<^sup>* = (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
\<comment> \<open>A short form for the stack mapping function for List\<close>
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 \<open>Rewrite rules for Lists using S as their mapping\<close>
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
\<comment> \<open>Recursive definition of what is means for a the graph/stack structure to be reconstructible\<close>
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) \<and>
iR p = (if c p then t else r p))"
text \<open>Rewrite rules for stkOk\<close>
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
subsection \<open>The Schorr-Waite algorithm\<close>
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}
t := root; p := Null;
WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
INV {\<exists>stack.
List (S c l r) p stack \<and> \<comment> \<open>\<open>i1\<close>\<close>
(\<forall>x \<in> set stack. m x) \<and> \<comment> \<open>\<open>i2\<close>\<close>
R = reachable (relS{l, r}) {t,p} \<and> \<comment> \<open>\<open>i3\<close>\<close>
(\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow> \<comment> \<open>\<open>i4\<close>\<close>
x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
(\<forall>x. m x \<longrightarrow> x \<in> R) \<and> \<comment> \<open>\<open>i5\<close>\<close>
(\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and> \<comment> \<open>\<open>i6\<close>\<close>
(stkOk c l r iL iR t stack) \<comment> \<open>\<open>i7\<close>\<close>}
DO IF t = Null \<or> t^.m
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
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) }"
(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)) \
(\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
(\<not>?ifB1 \<longrightarrow> (\<exists>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 -
\<comment> \<open>List property is maintained:\<close>
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
\<comment> \<open>Everything on the stack is marked:\<close>
from i2 have poI2: "\ x \ set stack_tl. m x" by (simp add:stack_eq)
moreover
\<comment> \<open>Everything is still reachable:\<close>
let "(R = reachable ?Ra ?A)" = "?I3"
let "?Rb" = "(relS {l, r(p \ 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 \ ?R"
proof (rule still_reachable)
show "addrs ?A \ ?Rb\<^sup>* `` 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\<^sup>* `` 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\<^sup>* `` 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\<^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>If it is reachable and not marked, it is still reachable using...\<close>
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)"
\<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 \ ?Rb\<^sup>* `` (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\<^sup>* `` (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\<^sup>*``(addrs ?B \ 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 \ ?Rb\<^sup>* `` 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"
\<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close>
have pDisj:"p^.r = Null \ (p^.r \ Null \ 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 \ ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp)
have excl: "x \ ?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 \ 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: "\x. m x \ x \ 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: "\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
\<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 \ 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
\<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: "\?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 -
\<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 \ ?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 \ ?Ra\<^sup>* `` 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\<^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 "\(x, y)\?Rb-?Ra. y\(?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 "\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\<^sup>*``addrs ?A \ ?Rb\<^sup>*``(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\<^sup>* `` (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\<^sup>*``(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\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \ ?Rb\<^sup>*``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\<^sup>*``addrs ?A"
by (simp only:reachable_def, clarsimp)
with ifB1 a
have exc: "x \ ?Rb\<^sup>*`` 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
\<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 "\stack. ?swInv stack" by blast
}
moreover
{
\<comment> \<open>Push arm\<close>
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 -
\<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 \ ?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 \ ?Ra\<^sup>* `` 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\<^sup>*``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\<^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 "\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\<^sup>*``addrs ?A \ ?Rb\<^sup>*``(addrs ?B \ addrs ?T)"
proof (rule still_reachable)
show "addrs ?A \ ?Rb\<^sup>* `` (addrs ?B \ addrs ?T)"
by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
next
show "\(x, y)\?Ra-?Rb. y\(?Rb\<^sup>*``(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\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \ ?Rb\<^sup>*``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\<^sup>*``addrs ?A"
by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
have exc: "x \ ?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 \ 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 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 "\stack. ?puInv stack" by blast
}
ultimately show ?thesis by blast
qed
}
qed
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
