13820
|
1 |
(* Title: HOL/Hoare/SchorrWaite.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Farhad Mehta
|
|
4 |
Copyright 2003 TUM
|
|
5 |
|
|
6 |
Proof of the Schorr-Waite graph marking algorithm.
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
13875
|
10 |
theory SchorrWaite = HeapSyntax:
|
13820
|
11 |
|
|
12 |
section {* Machinery for the Schorr-Waite proof*}
|
|
13 |
|
|
14 |
constdefs
|
|
15 |
-- "Relations induced by a mapping"
|
|
16 |
rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
|
|
17 |
"rel m == {(x,y). m x = Ref y}"
|
|
18 |
relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
|
|
19 |
"relS M == (\<Union> m \<in> M. rel m)"
|
|
20 |
addrs :: "'a ref set \<Rightarrow> 'a set"
|
|
21 |
"addrs P == {a. Ref a \<in> P}"
|
|
22 |
reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
|
|
23 |
"reachable r P == (r\<^sup>* `` addrs P)"
|
|
24 |
|
|
25 |
lemmas rel_defs = relS_def rel_def
|
|
26 |
|
|
27 |
text {* Rewrite rules for relations induced by a mapping*}
|
|
28 |
|
|
29 |
lemma self_reachable: "b \<in> B \<Longrightarrow> b \<in> R\<^sup>* `` B"
|
|
30 |
apply blast
|
|
31 |
done
|
|
32 |
|
|
33 |
lemma oneStep_reachable: "b \<in> R``B \<Longrightarrow> b \<in> R\<^sup>* `` B"
|
|
34 |
apply blast
|
|
35 |
done
|
|
36 |
|
|
37 |
lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
|
|
38 |
apply (clarsimp simp only:Image_iff intro:subsetI)
|
|
39 |
apply (erule rtrancl_induct)
|
|
40 |
apply blast
|
|
41 |
apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
|
|
42 |
apply (erule UnE)
|
|
43 |
apply (auto intro:rtrancl_into_rtrancl)
|
|
44 |
apply blast
|
|
45 |
done
|
|
46 |
|
|
47 |
lemma still_reachable_eq: "\<lbrakk> A\<subseteq>Rb\<^sup>*``B; B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Ra-Rb. y \<in>(Rb\<^sup>*``B); \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Ra\<^sup>*``A = Rb\<^sup>*``B "
|
|
48 |
apply (rule equalityI)
|
|
49 |
apply (erule still_reachable ,assumption)+
|
|
50 |
done
|
|
51 |
|
|
52 |
lemma reachable_null: "reachable mS {Null} = {}"
|
|
53 |
apply (simp add: reachable_def addrs_def)
|
|
54 |
done
|
|
55 |
|
|
56 |
lemma reachable_empty: "reachable mS {} = {}"
|
|
57 |
apply (simp add: reachable_def addrs_def)
|
|
58 |
done
|
|
59 |
|
|
60 |
lemma reachable_union: "(reachable mS aS \<union> reachable mS bS) = reachable mS (aS \<union> bS)"
|
|
61 |
apply (simp add: reachable_def rel_defs addrs_def)
|
|
62 |
apply blast
|
|
63 |
done
|
|
64 |
|
|
65 |
lemma reachable_union_sym: "reachable r (insert a aS) = (r\<^sup>* `` addrs {a}) \<union> reachable r aS"
|
|
66 |
apply (simp add: reachable_def rel_defs addrs_def)
|
|
67 |
apply blast
|
|
68 |
done
|
|
69 |
|
|
70 |
lemma rel_upd1: "(a,b) \<notin> rel (r(q:=t)) \<Longrightarrow> (a,b) \<in> rel r \<Longrightarrow> a=q"
|
|
71 |
apply (rule classical)
|
|
72 |
apply (simp add:rel_defs fun_upd_apply)
|
|
73 |
done
|
|
74 |
|
|
75 |
lemma rel_upd2: "(a,b) \<notin> rel r \<Longrightarrow> (a,b) \<in> rel (r(q:=t)) \<Longrightarrow> a=q"
|
|
76 |
apply (rule classical)
|
|
77 |
apply (simp add:rel_defs fun_upd_apply)
|
|
78 |
done
|
|
79 |
|
|
80 |
constdefs
|
|
81 |
-- "Restriction of a relation"
|
|
82 |
restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set" ("(_/ | _)" [50, 51] 50)
|
|
83 |
"restr r m == {(x,y). (x,y) \<in> r \<and> \<not> m x}"
|
|
84 |
|
|
85 |
text {* Rewrite rules for the restriction of a relation *}
|
|
86 |
|
|
87 |
lemma restr_identity[simp]:
|
|
88 |
" (\<forall>x. \<not> m x) \<Longrightarrow> (R |m) = R"
|
|
89 |
by (auto simp add:restr_def)
|
|
90 |
|
|
91 |
lemma restr_rtrancl[simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (R | m)\<^sup>* `` {l} = {l}"
|
|
92 |
by (auto simp add:restr_def elim:converse_rtranclE)
|
|
93 |
|
|
94 |
lemma [simp]: " \<lbrakk>m l\<rbrakk> \<Longrightarrow> (l,x) \<in> (R | m)\<^sup>* = (l=x)"
|
|
95 |
by (auto simp add:restr_def elim:converse_rtranclE)
|
|
96 |
|
|
97 |
lemma restr_upd: "((rel (r (q := t)))|(m(q := True))) = ((rel (r))|(m(q := True))) "
|
|
98 |
apply (auto simp:restr_def rel_def fun_upd_apply)
|
|
99 |
apply (rename_tac a b)
|
|
100 |
apply (case_tac "a=q")
|
|
101 |
apply auto
|
|
102 |
done
|
|
103 |
|
|
104 |
lemma restr_un: "((r \<union> s)|m) = (r|m) \<union> (s|m)"
|
|
105 |
by (auto simp add:restr_def)
|
|
106 |
|
|
107 |
lemma rel_upd3: "(a, b) \<notin> (r|(m(q := t))) \<Longrightarrow> (a,b) \<in> (r|m) \<Longrightarrow> a = q "
|
|
108 |
apply (rule classical)
|
|
109 |
apply (simp add:restr_def fun_upd_apply)
|
|
110 |
done
|
|
111 |
|
|
112 |
constdefs
|
|
113 |
-- "A short form for the stack mapping function for List"
|
|
114 |
S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
|
|
115 |
"S c l r == (\<lambda>x. if c x then r x else l x)"
|
|
116 |
|
|
117 |
text {* Rewrite rules for Lists using S as their mapping *}
|
|
118 |
|
|
119 |
lemma [rule_format,simp]:
|
|
120 |
"\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l r) p stack = List (S (c(a:=x)) (l(a:=y)) (r(a:=z))) p stack"
|
|
121 |
apply(induct_tac stack)
|
|
122 |
apply(simp add:fun_upd_apply S_def)+
|
|
123 |
done
|
|
124 |
|
|
125 |
lemma [rule_format,simp]:
|
|
126 |
"\<forall>p. a \<notin> set stack \<longrightarrow> List (S c l (r(a:=z))) p stack = List (S c l r) p stack"
|
|
127 |
apply(induct_tac stack)
|
|
128 |
apply(simp add:fun_upd_apply S_def)+
|
|
129 |
done
|
|
130 |
|
|
131 |
lemma [rule_format,simp]:
|
|
132 |
"\<forall>p. a \<notin> set stack \<longrightarrow> List (S c (l(a:=z)) r) p stack = List (S c l r) p stack"
|
|
133 |
apply(induct_tac stack)
|
|
134 |
apply(simp add:fun_upd_apply S_def)+
|
|
135 |
done
|
|
136 |
|
|
137 |
lemma [rule_format,simp]:
|
|
138 |
"\<forall>p. a \<notin> set stack \<longrightarrow> List (S (c(a:=z)) l r) p stack = List (S c l r) p stack"
|
|
139 |
apply(induct_tac stack)
|
|
140 |
apply(simp add:fun_upd_apply S_def)+
|
|
141 |
done
|
|
142 |
|
|
143 |
consts
|
|
144 |
--"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
|
|
145 |
stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow> bool"
|
|
146 |
primrec
|
|
147 |
stkOk_nil: "stkOk c l r iL iR t [] = True"
|
|
148 |
stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and>
|
|
149 |
iL p = (if c p then l p else t) \<and>
|
|
150 |
iR p = (if c p then t else r p))"
|
|
151 |
|
|
152 |
text {* Rewrite rules for stkOk *}
|
|
153 |
|
|
154 |
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
|
|
155 |
stkOk (c(x := f)) l r iL iR t xs = stkOk c l r iL iR t xs"
|
|
156 |
apply (induct xs)
|
|
157 |
apply (auto simp:eq_sym_conv)
|
|
158 |
done
|
|
159 |
|
|
160 |
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
|
|
161 |
stkOk c (l(x := g)) r iL iR t xs = stkOk c l r iL iR t xs"
|
|
162 |
apply (induct xs)
|
|
163 |
apply (auto simp:eq_sym_conv)
|
|
164 |
done
|
|
165 |
|
|
166 |
lemma [simp]: "\<And>t. \<lbrakk> x \<notin> set xs; Ref x\<noteq>t \<rbrakk> \<Longrightarrow>
|
|
167 |
stkOk c l (r(x := g)) iL iR t xs = stkOk c l r iL iR t xs"
|
|
168 |
apply (induct xs)
|
|
169 |
apply (auto simp:eq_sym_conv)
|
|
170 |
done
|
|
171 |
|
|
172 |
lemma stkOk_r_rewrite [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
|
|
173 |
stkOk c l (r(x := g)) iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
|
|
174 |
apply (induct xs)
|
|
175 |
apply (auto simp:eq_sym_conv)
|
|
176 |
done
|
|
177 |
|
|
178 |
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
|
|
179 |
stkOk c (l(x := g)) r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
|
|
180 |
apply (induct xs)
|
|
181 |
apply (auto simp:eq_sym_conv)
|
|
182 |
done
|
|
183 |
|
|
184 |
lemma [simp]: "\<And>x. x \<notin> set xs \<Longrightarrow>
|
|
185 |
stkOk (c(x := g)) l r iL iR (Ref x) xs = stkOk c l r iL iR (Ref x) xs"
|
|
186 |
apply (induct xs)
|
|
187 |
apply (auto simp:eq_sym_conv)
|
|
188 |
done
|
|
189 |
|
|
190 |
|
|
191 |
section{*The Schorr-Waite algorithm*}
|
|
192 |
|
|
193 |
|
|
194 |
theorem SchorrWaiteAlgorithm:
|
|
195 |
"VARS c m l r t p q root
|
|
196 |
{R = reachable (relS {l, r}) {root} \<and> (\<forall>x. \<not> m x) \<and> iR = r \<and> iL = l}
|
|
197 |
t := root; p := Null;
|
|
198 |
WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
|
|
199 |
INV {\<exists>stack.
|
13875
|
200 |
List (S c l r) p stack \<and> (*i1*)
|
|
201 |
(\<forall>x \<in> set stack. m x) \<and> (*i2*)
|
|
202 |
R = reachable (relS{l, r}) {t,p} \<and> (*i3*)
|
|
203 |
(\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow> (*i4*)
|
13820
|
204 |
x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
|
13875
|
205 |
(\<forall>x. m x \<longrightarrow> x \<in> R) \<and> (*i5*)
|
|
206 |
(\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and> (*i6*)
|
|
207 |
(stkOk c l r iL iR t stack) (*i7*) }
|
13820
|
208 |
DO IF t = Null \<or> t^.m
|
|
209 |
THEN IF p^.c
|
13875
|
210 |
THEN q := t; t := p; p := p^.r; t^.r := q (*pop*)
|
|
211 |
ELSE q := t; t := p^.r; p^.r := p^.l; (*swing*)
|
13820
|
212 |
p^.l := q; p^.c := True FI
|
13875
|
213 |
ELSE q := p; p := t; t := t^.l; p^.l := q; (*push*)
|
13820
|
214 |
p^.m := True; p^.c := False FI OD
|
|
215 |
{(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
|
13875
|
216 |
(is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
|
13820
|
217 |
proof (vcg)
|
|
218 |
let "While {(c, m, l, r, t, p, q, root). ?whileB m t p}
|
|
219 |
{(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3
|
|
220 |
{
|
|
221 |
|
|
222 |
fix c m l r t p q root
|
|
223 |
assume "?Pre c m l r root"
|
|
224 |
thus "?inv c m l r root Null" by (auto simp add: reachable_def addrs_def)
|
|
225 |
next
|
|
226 |
|
|
227 |
fix c m l r t p q
|
|
228 |
let "\<exists>stack. ?Inv stack" = "?inv c m l r t p"
|
|
229 |
assume a: "?inv c m l r t p \<and> \<not>(p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)"
|
|
230 |
then obtain stack where inv: "?Inv stack" by blast
|
|
231 |
from a have pNull: "p = Null" and tDisj: "t=Null \<or> (t\<noteq>Null \<and> t^.m )" by auto
|
|
232 |
let "?I1 \<and> _ \<and> _ \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> _" = "?Inv stack"
|
|
233 |
from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
|
|
234 |
from pNull i1 have stackEmpty: "stack = []" by simp
|
|
235 |
from tDisj i4 have RisMarked[rule_format]: "\<forall>x. x \<in> R \<longrightarrow> m x" by(auto simp: reachable_def addrs_def stackEmpty)
|
|
236 |
from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL" by(auto simp: stackEmpty expand_fun_eq intro:RisMarked)
|
|
237 |
|
|
238 |
next
|
|
239 |
fix c m l r t p q root
|
|
240 |
let "\<exists>stack. ?Inv stack" = "?inv c m l r t p"
|
|
241 |
let "\<exists>stack. ?popInv stack" = "?inv c m l (r(p \<rightarrow> t)) p (p^.r)"
|
|
242 |
let "\<exists>stack. ?swInv stack" =
|
|
243 |
"?inv (c(p \<rightarrow> True)) m (l(p \<rightarrow> t)) (r(p \<rightarrow> p^.l)) (p^.r) p"
|
|
244 |
let "\<exists>stack. ?puInv stack" =
|
|
245 |
"?inv (c(t \<rightarrow> False)) (m(t \<rightarrow> True)) (l(t \<rightarrow> p)) r (t^.l) t"
|
|
246 |
let "?ifB1" = "(t = Null \<or> t^.m)"
|
|
247 |
let "?ifB2" = "p^.c"
|
|
248 |
|
|
249 |
assume "(\<exists>stack.?Inv stack) \<and> (p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m)" (is "_ \<and> ?whileB")
|
|
250 |
then obtain stack where inv: "?Inv stack" and whileB: "?whileB" by blast
|
|
251 |
let "?I1 \<and> ?I2 \<and> ?I3 \<and> ?I4 \<and> ?I5 \<and> ?I6 \<and> ?I7" = "?Inv stack"
|
|
252 |
from inv have i1: "?I1" and i2: "?I2" and i3: "?I3" and i4: "?I4"
|
|
253 |
and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+
|
|
254 |
have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
|
|
255 |
|
|
256 |
show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and>
|
|
257 |
(\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and>
|
|
258 |
(\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))"
|
|
259 |
proof -
|
|
260 |
{
|
|
261 |
assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c"
|
|
262 |
from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto
|
|
263 |
then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto
|
|
264 |
with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl"
|
|
265 |
by auto
|
|
266 |
with i2 have m_addr_p: "p^.m" by auto
|
|
267 |
have stackDist: "distinct (stack)" using i1 by (rule List_distinct)
|
|
268 |
from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp
|
|
269 |
let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl"
|
|
270 |
have "?popInv stack_tl"
|
|
271 |
proof -
|
|
272 |
|
|
273 |
-- {*List property is maintained:*}
|
|
274 |
from i1 p_notin_stack_tl ifB2
|
|
275 |
have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl"
|
|
276 |
by(simp add: addr_p_eq stack_eq, simp add: S_def)
|
|
277 |
|
|
278 |
moreover
|
|
279 |
-- {*Everything on the stack is marked:*}
|
|
280 |
from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq)
|
|
281 |
moreover
|
|
282 |
|
|
283 |
-- {*Everything is still reachable:*}
|
|
284 |
let "(R = reachable ?Ra ?A)" = "?I3"
|
|
285 |
let "?Rb" = "(relS {l, r(p \<rightarrow> t)})"
|
|
286 |
let "?B" = "{p, p^.r}"
|
|
287 |
-- {*Our goal is @{text"R = reachable ?Rb ?B"}.*}
|
|
288 |
have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R")
|
|
289 |
proof
|
|
290 |
show "?L \<subseteq> ?R"
|
|
291 |
proof (rule still_reachable)
|
|
292 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastsimp simp:addrs_def relS_def rel_def addr_p_eq
|
|
293 |
intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
294 |
show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def)
|
|
295 |
(fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
|
|
296 |
qed
|
|
297 |
show "?R \<subseteq> ?L"
|
|
298 |
proof (rule still_reachable)
|
|
299 |
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
|
|
300 |
by(fastsimp simp:addrs_def rel_defs addr_p_eq
|
|
301 |
intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
302 |
next
|
|
303 |
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
|
|
304 |
by (clarsimp simp:relS_def)
|
|
305 |
(fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd2)
|
|
306 |
qed
|
|
307 |
qed
|
|
308 |
with i3 have poI3: "R = reachable ?Rb ?B" by (simp add:reachable_def)
|
|
309 |
moreover
|
|
310 |
|
|
311 |
-- "If it is reachable and not marked, it is still reachable using..."
|
|
312 |
let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
|
|
313 |
let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m"
|
|
314 |
let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)"
|
|
315 |
-- {*Our goal is @{text"\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"}.*}
|
|
316 |
let ?T = "{t, p^.r}"
|
|
317 |
|
|
318 |
have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
|
|
319 |
proof (rule still_reachable)
|
|
320 |
have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
|
|
321 |
by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
|
|
322 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
|
|
323 |
by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
|
|
324 |
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
|
|
325 |
by (clarsimp simp:restr_def relS_def)
|
|
326 |
(fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
|
|
327 |
qed
|
|
328 |
-- "We now bring a term from the right to the left of the subset relation."
|
|
329 |
hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
|
|
330 |
by blast
|
|
331 |
have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"
|
|
332 |
proof (rule allI, rule impI)
|
|
333 |
fix x
|
|
334 |
assume a: "x \<in> R \<and> \<not> m x"
|
|
335 |
-- {*First, a disjunction on @{term"p^.r"} used later in the proof*}
|
|
336 |
have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2
|
|
337 |
by auto
|
|
338 |
-- {*@{term x} belongs to the left hand side of @{thm[source] subset}:*}
|
|
339 |
have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp)
|
|
340 |
have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def)
|
|
341 |
-- {*And therefore also belongs to the right hand side of @{thm[source]subset},*}
|
|
342 |
-- {*which corresponds to our goal.*}
|
|
343 |
from incl excl subset show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def)
|
|
344 |
qed
|
|
345 |
moreover
|
|
346 |
|
|
347 |
-- "If it is marked, then it is reachable"
|
|
348 |
from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" .
|
|
349 |
moreover
|
|
350 |
|
|
351 |
-- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
|
|
352 |
from i7 i6 ifB2
|
|
353 |
have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x"
|
|
354 |
by(auto simp: addr_p_eq stack_eq fun_upd_apply)
|
|
355 |
|
|
356 |
moreover
|
|
357 |
|
|
358 |
-- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
|
|
359 |
from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl"
|
|
360 |
by (clarsimp simp:stack_eq addr_p_eq)
|
|
361 |
|
|
362 |
ultimately show "?popInv stack_tl" by simp
|
|
363 |
qed
|
|
364 |
hence "\<exists>stack. ?popInv stack" ..
|
|
365 |
}
|
|
366 |
moreover
|
|
367 |
|
|
368 |
-- "Proofs of the Swing and Push arm follow."
|
|
369 |
-- "Since they are in principle simmilar to the Pop arm proof,"
|
|
370 |
-- "we show fewer comments and use frequent pattern matching."
|
|
371 |
{
|
|
372 |
-- "Swing arm"
|
|
373 |
assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2"
|
|
374 |
from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp
|
|
375 |
then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp
|
|
376 |
with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp
|
|
377 |
with i2 have m_addr_p: "p^.m" by clarsimp
|
|
378 |
from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl"
|
|
379 |
by simp
|
|
380 |
let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack"
|
|
381 |
have "?swInv stack"
|
|
382 |
proof -
|
|
383 |
|
|
384 |
-- {*List property is maintained:*}
|
|
385 |
from i1 p_notin_stack_tl nifB2
|
|
386 |
have swI1: "?swI1"
|
|
387 |
by (simp add:addr_p_eq stack_eq, simp add:S_def)
|
|
388 |
moreover
|
|
389 |
|
|
390 |
-- {*Everything on the stack is marked:*}
|
|
391 |
from i2
|
|
392 |
have swI2: "?swI2" .
|
|
393 |
moreover
|
|
394 |
|
|
395 |
-- {*Everything is still reachable:*}
|
|
396 |
let "R = reachable ?Ra ?A" = "?I3"
|
|
397 |
let "R = reachable ?Rb ?B" = "?swI3"
|
|
398 |
have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
|
|
399 |
proof (rule still_reachable_eq)
|
|
400 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
|
|
401 |
by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
402 |
next
|
|
403 |
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
|
|
404 |
by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
405 |
next
|
|
406 |
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
|
|
407 |
by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
|
|
408 |
next
|
|
409 |
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
|
|
410 |
by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
|
|
411 |
qed
|
|
412 |
with i3
|
|
413 |
have swI3: "?swI3" by (simp add:reachable_def)
|
|
414 |
moreover
|
|
415 |
|
|
416 |
-- "If it is reachable and not marked, it is still reachable using..."
|
|
417 |
let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
|
|
418 |
let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4
|
|
419 |
let ?T = "{t}"
|
|
420 |
have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
|
|
421 |
proof (rule still_reachable)
|
|
422 |
have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
|
|
423 |
by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
|
|
424 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
|
|
425 |
by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
|
|
426 |
next
|
|
427 |
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
|
|
428 |
by (clarsimp simp:relS_def restr_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
|
|
429 |
qed
|
|
430 |
then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
|
|
431 |
by blast
|
|
432 |
have ?swI4
|
|
433 |
proof (rule allI, rule impI)
|
|
434 |
fix x
|
|
435 |
assume a: "x \<in> R \<and>\<not> m x"
|
|
436 |
with i4 addr_p_eq stack_eq have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
|
|
437 |
by (simp only:reachable_def, clarsimp)
|
|
438 |
with ifB1 a
|
|
439 |
have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
|
|
440 |
by (auto simp add:addrs_def)
|
|
441 |
from inc exc subset show "x \<in> reachable ?Rb ?B"
|
|
442 |
by (auto simp add:reachable_def)
|
|
443 |
qed
|
|
444 |
moreover
|
|
445 |
|
|
446 |
-- "If it is marked, then it is reachable"
|
|
447 |
from i5
|
|
448 |
have "?swI5" .
|
|
449 |
moreover
|
|
450 |
|
|
451 |
-- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
|
|
452 |
from i6 stack_eq
|
|
453 |
have "?swI6"
|
|
454 |
by clarsimp
|
|
455 |
moreover
|
|
456 |
|
|
457 |
-- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
|
|
458 |
from stackDist i7 nifB2
|
|
459 |
have "?swI7"
|
|
460 |
by (clarsimp simp:addr_p_eq stack_eq)
|
|
461 |
|
|
462 |
ultimately show ?thesis by auto
|
|
463 |
qed
|
|
464 |
then have "\<exists>stack. ?swInv stack" by blast
|
|
465 |
}
|
|
466 |
moreover
|
|
467 |
|
|
468 |
{
|
|
469 |
-- "Push arm"
|
|
470 |
assume nifB1: "\<not>?ifB1"
|
|
471 |
from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp
|
|
472 |
then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp
|
|
473 |
with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp
|
|
474 |
from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp
|
|
475 |
with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast
|
|
476 |
let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack"
|
|
477 |
have "?puInv new_stack"
|
|
478 |
proof -
|
|
479 |
|
|
480 |
-- {*List property is maintained:*}
|
|
481 |
from i1 t_notin_stack
|
|
482 |
have puI1: "?puI1"
|
|
483 |
by (simp add:addr_t_eq new_stack_eq, simp add:S_def)
|
|
484 |
moreover
|
|
485 |
|
|
486 |
-- {*Everything on the stack is marked:*}
|
|
487 |
from i2
|
|
488 |
have puI2: "?puI2"
|
|
489 |
by (simp add:new_stack_eq fun_upd_apply)
|
|
490 |
moreover
|
|
491 |
|
|
492 |
-- {*Everything is still reachable:*}
|
|
493 |
let "R = reachable ?Ra ?A" = "?I3"
|
|
494 |
let "R = reachable ?Rb ?B" = "?puI3"
|
|
495 |
have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
|
|
496 |
proof (rule still_reachable_eq)
|
|
497 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
|
|
498 |
by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
499 |
next
|
|
500 |
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
|
|
501 |
by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
|
|
502 |
next
|
|
503 |
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
|
|
504 |
by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
|
|
505 |
next
|
|
506 |
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
|
|
507 |
by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
|
|
508 |
qed
|
|
509 |
with i3
|
|
510 |
have puI3: "?puI3" by (simp add:reachable_def)
|
|
511 |
moreover
|
|
512 |
|
|
513 |
-- "If it is reachable and not marked, it is still reachable using..."
|
|
514 |
let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4
|
|
515 |
let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4
|
|
516 |
let ?T = "{t}"
|
|
517 |
have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
|
|
518 |
proof (rule still_reachable)
|
|
519 |
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
|
|
520 |
by (fastsimp simp:new_stack_eq addrs_def intro:self_reachable)
|
|
521 |
next
|
|
522 |
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
|
|
523 |
by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
|
|
524 |
(fastsimp simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
|
|
525 |
qed
|
|
526 |
then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
|
|
527 |
by blast
|
|
528 |
have ?puI4
|
|
529 |
proof (rule allI, rule impI)
|
|
530 |
fix x
|
|
531 |
assume a: "x \<in> R \<and> \<not> ?new_m x"
|
|
532 |
have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
|
|
533 |
with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
|
|
534 |
by (fastsimp simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
|
|
535 |
have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
|
|
536 |
using xDisj a n_m_addr_t
|
|
537 |
by (clarsimp simp add:addrs_def addr_t_eq)
|
|
538 |
from inc exc subset show "x \<in> reachable ?Rb ?B"
|
|
539 |
by (auto simp add:reachable_def)
|
|
540 |
qed
|
|
541 |
moreover
|
|
542 |
|
|
543 |
-- "If it is marked, then it is reachable"
|
|
544 |
from i5
|
|
545 |
have "?puI5"
|
|
546 |
by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable)
|
|
547 |
moreover
|
|
548 |
|
|
549 |
-- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*}
|
|
550 |
from i6
|
|
551 |
have "?puI6"
|
|
552 |
by (simp add:new_stack_eq)
|
|
553 |
moreover
|
|
554 |
|
|
555 |
-- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*}
|
|
556 |
from stackDist i6 t_notin_stack i7
|
|
557 |
have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq)
|
|
558 |
|
|
559 |
ultimately show ?thesis by auto
|
|
560 |
qed
|
|
561 |
then have "\<exists>stack. ?puInv stack" by blast
|
|
562 |
|
|
563 |
}
|
|
564 |
ultimately show ?thesis by blast
|
|
565 |
qed
|
|
566 |
}
|
|
567 |
qed
|
|
568 |
|
|
569 |
end
|
|
570 |
|