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