author  paulson 
Tue, 04 Feb 2003 18:12:40 +0100  
changeset 13805  3786b2fd6808 
parent 13798  4c1a53627500 
child 13812  91713a1915ee 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/WFair 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
Weak Fairness versions of transient, ensures, leadsTo. 

7 

8 
From Misra, "A Logic for Concurrent Programming", 1994 

9 
*) 

10 

13798  11 
header{*Progress under Weak Fairness*} 
12 

13797  13 
theory WFair = UNITY: 
4776  14 

15 
constdefs 

16 

5155  17 
(*This definition specifies weak fairness. The rest of the theory 
18 
is generic to all forms of fairness.*) 

5648  19 
transient :: "'a set => 'a program set" 
13805  20 
"transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> A}" 
4776  21 

13797  22 
ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) 
13805  23 
"A ensures B == (AB co A \<union> B) \<inter> transient (AB)" 
8006  24 

6536  25 

26 
consts 

27 

28 
(*LEADSTO constant for the inductive definition*) 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

29 
leads :: "'a program => ('a set * 'a set) set" 
5648  30 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

31 

9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

32 
inductive "leads F" 
13797  33 
intros 
4776  34 

13805  35 
Basis: "F \<in> A ensures B ==> (A,B) \<in> leads F" 
4776  36 

13805  37 
Trans: "[ (A,B) \<in> leads F; (B,C) \<in> leads F ] ==> (A,C) \<in> leads F" 
4776  38 

13805  39 
Union: "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F" 
4776  40 

5155  41 

8006  42 
constdefs 
6536  43 

8006  44 
(*visible version of the LEADSTO relation*) 
13797  45 
leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) 
13805  46 
"A leadsTo B == {F. (A,B) \<in> leads F}" 
5648  47 

48 
(*wlt F B is the largest set that leads to B*) 

49 
wlt :: "['a program, 'a set] => 'a set" 

13805  50 
"wlt F B == Union {A. F \<in> A leadsTo B}" 
4776  51 

9685  52 
syntax (xsymbols) 
13797  53 
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60) 
54 

55 

13798  56 
subsection{*transient*} 
13797  57 

58 
lemma stable_transient_empty: 

13805  59 
"[ F \<in> stable A; F \<in> transient A ] ==> A = {}" 
13797  60 
by (unfold stable_def constrains_def transient_def, blast) 
61 

62 
lemma transient_strengthen: 

13805  63 
"[ F \<in> transient A; B \<subseteq> A ] ==> F \<in> transient B" 
13797  64 
apply (unfold transient_def, clarify) 
65 
apply (blast intro!: rev_bexI) 

66 
done 

67 

68 
lemma transientI: 

13805  69 
"[ act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> A ] ==> F \<in> transient A" 
13797  70 
by (unfold transient_def, blast) 
71 

72 
lemma transientE: 

13805  73 
"[ F \<in> transient A; 
74 
!!act. [ act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> A ] ==> P ] 

13797  75 
==> P" 
76 
by (unfold transient_def, blast) 

77 

78 
lemma transient_UNIV [simp]: "transient UNIV = {}" 

79 
by (unfold transient_def, blast) 

80 

81 
lemma transient_empty [simp]: "transient {} = UNIV" 

82 
by (unfold transient_def, auto) 

83 

84 

13798  85 
subsection{*ensures*} 
13797  86 

87 
lemma ensuresI: 

13805  88 
"[ F \<in> (AB) co (A \<union> B); F \<in> transient (AB) ] ==> F \<in> A ensures B" 
13797  89 
by (unfold ensures_def, blast) 
90 

91 
lemma ensuresD: 

13805  92 
"F \<in> A ensures B ==> F \<in> (AB) co (A \<union> B) & F \<in> transient (AB)" 
13797  93 
by (unfold ensures_def, blast) 
94 

95 
lemma ensures_weaken_R: 

13805  96 
"[ F \<in> A ensures A'; A'<=B' ] ==> F \<in> A ensures B'" 
13797  97 
apply (unfold ensures_def) 
98 
apply (blast intro: constrains_weaken transient_strengthen) 

99 
done 

100 

101 
(*The Lversion (precondition strengthening) fails, but we have this*) 

102 
lemma stable_ensures_Int: 

13805  103 
"[ F \<in> stable C; F \<in> A ensures B ] 
104 
==> F \<in> (C \<inter> A) ensures (C \<inter> B)" 

13797  105 
apply (unfold ensures_def) 
106 
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) 

107 
prefer 2 apply (blast intro: transient_strengthen) 

108 
apply (blast intro: stable_constrains_Int constrains_weaken) 

109 
done 

110 

111 
lemma stable_transient_ensures: 

13805  112 
"[ F \<in> stable A; F \<in> transient C; A \<subseteq> B \<union> C ] ==> F \<in> A ensures B" 
13797  113 
apply (simp add: ensures_def stable_def) 
114 
apply (blast intro: constrains_weaken transient_strengthen) 

115 
done 

116 

13805  117 
lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (AB)" 
13797  118 
by (simp (no_asm) add: ensures_def unless_def) 
119 

120 

13798  121 
subsection{*leadsTo*} 
13797  122 

13805  123 
lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B" 
13797  124 
apply (unfold leadsTo_def) 
125 
apply (blast intro: leads.Basis) 

126 
done 

127 

128 
lemma leadsTo_Trans: 

13805  129 
"[ F \<in> A leadsTo B; F \<in> B leadsTo C ] ==> F \<in> A leadsTo C" 
13797  130 
apply (unfold leadsTo_def) 
131 
apply (blast intro: leads.Trans) 

132 
done 

133 

13805  134 
lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (A)" 
13797  135 
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) 
136 

137 
(*Useful with cancellation, disjunction*) 

13805  138 
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'" 
13797  139 
by (simp add: Un_ac) 
140 

141 
lemma leadsTo_Un_duplicate2: 

13805  142 
"F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)" 
13797  143 
by (simp add: Un_ac) 
144 

145 
(*The Union introduction rule as we should have liked to state it*) 

146 
lemma leadsTo_Union: 

13805  147 
"(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B" 
13797  148 
apply (unfold leadsTo_def) 
149 
apply (blast intro: leads.Union) 

150 
done 

151 

152 
lemma leadsTo_Union_Int: 

13805  153 
"(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B" 
13797  154 
apply (unfold leadsTo_def) 
155 
apply (simp only: Int_Union_Union) 

156 
apply (blast intro: leads.Union) 

157 
done 

158 

159 
lemma leadsTo_UN: 

13805  160 
"(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B" 
13797  161 
apply (subst Union_image_eq [symmetric]) 
162 
apply (blast intro: leadsTo_Union) 

163 
done 

164 

165 
(*Binary union introduction rule*) 

166 
lemma leadsTo_Un: 

13805  167 
"[ F \<in> A leadsTo C; F \<in> B leadsTo C ] ==> F \<in> (A \<union> B) leadsTo C" 
13797  168 
apply (subst Un_eq_Union) 
169 
apply (blast intro: leadsTo_Union) 

170 
done 

171 

172 
lemma single_leadsTo_I: 

13805  173 
"(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B" 
13797  174 
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) 
175 

176 

177 
(*The INDUCTION rule as we should have liked to state it*) 

178 
lemma leadsTo_induct: 

13805  179 
"[ F \<in> za leadsTo zb; 
180 
!!A B. F \<in> A ensures B ==> P A B; 

181 
!!A B C. [ F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C ] 

13797  182 
==> P A C; 
13805  183 
!!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B 
13797  184 
] ==> P za zb" 
185 
apply (unfold leadsTo_def) 

186 
apply (drule CollectD, erule leads.induct) 

187 
apply (blast+) 

188 
done 

189 

190 

13805  191 
lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B" 
13797  192 
by (unfold ensures_def constrains_def transient_def, blast) 
193 

194 
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard] 

195 

196 
lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard] 

197 

198 
lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp] 

199 

200 
lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp] 

201 

202 

203 

204 
(** Variant induction rule: on the preconditions for B **) 

205 

206 
(*Lemma is the weak version: can't see how to do it in one step*) 

207 
lemma leadsTo_induct_pre_lemma: 

13805  208 
"[ F \<in> za leadsTo zb; 
13797  209 
P zb; 
13805  210 
!!A B. [ F \<in> A ensures B; P B ] ==> P A; 
211 
!!S. \<forall>A \<in> S. P A ==> P (Union S) 

13797  212 
] ==> P za" 
213 
(*by induction on this formula*) 

214 
apply (subgoal_tac "P zb > P za") 

215 
(*now solve first subgoal: this formula is sufficient*) 

216 
apply (blast intro: leadsTo_refl) 

217 
apply (erule leadsTo_induct) 

218 
apply (blast+) 

219 
done 

220 

221 
lemma leadsTo_induct_pre: 

13805  222 
"[ F \<in> za leadsTo zb; 
13797  223 
P zb; 
13805  224 
!!A B. [ F \<in> A ensures B; F \<in> B leadsTo zb; P B ] ==> P A; 
225 
!!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S) 

13797  226 
] ==> P za" 
13805  227 
apply (subgoal_tac "F \<in> za leadsTo zb & P za") 
13797  228 
apply (erule conjunct2) 
229 
apply (erule leadsTo_induct_pre_lemma) 

230 
prefer 3 apply (blast intro: leadsTo_Union) 

231 
prefer 2 apply (blast intro: leadsTo_Trans) 

232 
apply (blast intro: leadsTo_refl) 

233 
done 

234 

235 

13805  236 
lemma leadsTo_weaken_R: "[ F \<in> A leadsTo A'; A'<=B' ] ==> F \<in> A leadsTo B'" 
13797  237 
by (blast intro: subset_imp_leadsTo leadsTo_Trans) 
238 

13798  239 
lemma leadsTo_weaken_L [rule_format]: 
13805  240 
"[ F \<in> A leadsTo A'; B \<subseteq> A ] ==> F \<in> B leadsTo A'" 
13797  241 
by (blast intro: leadsTo_Trans subset_imp_leadsTo) 
242 

243 
(*Distributes over binary unions*) 

244 
lemma leadsTo_Un_distrib: 

13805  245 
"F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)" 
13797  246 
by (blast intro: leadsTo_Un leadsTo_weaken_L) 
247 

248 
lemma leadsTo_UN_distrib: 

13805  249 
"F \<in> (\<Union>i \<in> I. A i) leadsTo B = (\<forall>i \<in> I. F \<in> (A i) leadsTo B)" 
13797  250 
by (blast intro: leadsTo_UN leadsTo_weaken_L) 
251 

252 
lemma leadsTo_Union_distrib: 

13805  253 
"F \<in> (Union S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)" 
13797  254 
by (blast intro: leadsTo_Union leadsTo_weaken_L) 
255 

256 

257 
lemma leadsTo_weaken: 

13805  258 
"[ F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' ] ==> F \<in> B leadsTo B'" 
13797  259 
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans) 
260 

261 

262 
(*Set difference: maybe combine with leadsTo_weaken_L?*) 

263 
lemma leadsTo_Diff: 

13805  264 
"[ F \<in> (AB) leadsTo C; F \<in> B leadsTo C ] ==> F \<in> A leadsTo C" 
13797  265 
by (blast intro: leadsTo_Un leadsTo_weaken) 
266 

267 
lemma leadsTo_UN_UN: 

13805  268 
"(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i)) 
269 
==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)" 

13797  270 
apply (simp only: Union_image_eq [symmetric]) 
271 
apply (blast intro: leadsTo_Union leadsTo_weaken_R) 

272 
done 

273 

274 
(*Binary union version*) 

275 
lemma leadsTo_Un_Un: 

13805  276 
"[ F \<in> A leadsTo A'; F \<in> B leadsTo B' ] 
277 
==> F \<in> (A \<union> B) leadsTo (A' \<union> B')" 

13797  278 
by (blast intro: leadsTo_Un leadsTo_weaken_R) 
279 

280 

281 
(** The cancellation law **) 

282 

283 
lemma leadsTo_cancel2: 

13805  284 
"[ F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' ] 
285 
==> F \<in> A leadsTo (A' \<union> B')" 

13797  286 
by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans) 
287 

288 
lemma leadsTo_cancel_Diff2: 

13805  289 
"[ F \<in> A leadsTo (A' \<union> B); F \<in> (BA') leadsTo B' ] 
290 
==> F \<in> A leadsTo (A' \<union> B')" 

13797  291 
apply (rule leadsTo_cancel2) 
292 
prefer 2 apply assumption 

293 
apply (simp_all (no_asm_simp)) 

294 
done 

295 

296 
lemma leadsTo_cancel1: 

13805  297 
"[ F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' ] 
298 
==> F \<in> A leadsTo (B' \<union> A')" 

13797  299 
apply (simp add: Un_commute) 
300 
apply (blast intro!: leadsTo_cancel2) 

301 
done 

302 

303 
lemma leadsTo_cancel_Diff1: 

13805  304 
"[ F \<in> A leadsTo (B \<union> A'); F \<in> (BA') leadsTo B' ] 
305 
==> F \<in> A leadsTo (B' \<union> A')" 

13797  306 
apply (rule leadsTo_cancel1) 
307 
prefer 2 apply assumption 

308 
apply (simp_all (no_asm_simp)) 

309 
done 

310 

311 

312 

313 
(** The impossibility law **) 

314 

13805  315 
lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}" 
13797  316 
apply (erule leadsTo_induct_pre) 
317 
apply (simp_all add: ensures_def constrains_def transient_def, blast) 

318 
done 

319 

320 

321 
(** PSP: ProgressSafetyProgress **) 

322 

323 
(*Special case of PSP: Misra's "stable conjunction"*) 

324 
lemma psp_stable: 

13805  325 
"[ F \<in> A leadsTo A'; F \<in> stable B ] 
326 
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)" 

13797  327 
apply (unfold stable_def) 
328 
apply (erule leadsTo_induct) 

329 
prefer 3 apply (blast intro: leadsTo_Union_Int) 

330 
prefer 2 apply (blast intro: leadsTo_Trans) 

331 
apply (rule leadsTo_Basis) 

332 
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric]) 

333 
apply (blast intro: transient_strengthen constrains_Int) 

334 
done 

335 

336 
lemma psp_stable2: 

13805  337 
"[ F \<in> A leadsTo A'; F \<in> stable B ] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')" 
13797  338 
by (simp add: psp_stable Int_ac) 
339 

340 
lemma psp_ensures: 

13805  341 
"[ F \<in> A ensures A'; F \<in> B co B' ] 
342 
==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B'  B))" 

13797  343 
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*) 
344 
apply (blast intro: transient_strengthen) 

345 
done 

346 

347 
lemma psp: 

13805  348 
"[ F \<in> A leadsTo A'; F \<in> B co B' ] 
349 
==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B'  B))" 

13797  350 
apply (erule leadsTo_induct) 
351 
prefer 3 apply (blast intro: leadsTo_Union_Int) 

352 
txt{*Basis case*} 

353 
apply (blast intro: psp_ensures) 

354 
txt{*Transitivity case has a delicate argument involving "cancellation"*} 

355 
apply (rule leadsTo_Un_duplicate2) 

356 
apply (erule leadsTo_cancel_Diff1) 

357 
apply (simp add: Int_Diff Diff_triv) 

358 
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset) 

359 
done 

360 

361 
lemma psp2: 

13805  362 
"[ F \<in> A leadsTo A'; F \<in> B co B' ] 
363 
==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B'  B))" 

13797  364 
by (simp (no_asm_simp) add: psp Int_ac) 
365 

366 
lemma psp_unless: 

13805  367 
"[ F \<in> A leadsTo A'; F \<in> B unless B' ] 
368 
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')" 

13797  369 

370 
apply (unfold unless_def) 

371 
apply (drule psp, assumption) 

372 
apply (blast intro: leadsTo_weaken) 

373 
done 

374 

375 

13798  376 
subsection{*Proving the induction rules*} 
13797  377 

378 
(** The most general rule: r is any wf relation; f is any variant function **) 

379 

380 
lemma leadsTo_wf_induct_lemma: 

381 
"[ wf r; 

13805  382 
\<forall>m. F \<in> (A \<inter> f`{m}) leadsTo 
383 
((A \<inter> f`(r^1 `` {m})) \<union> B) ] 

384 
==> F \<in> (A \<inter> f`{m}) leadsTo B" 

13797  385 
apply (erule_tac a = m in wf_induct) 
13805  386 
apply (subgoal_tac "F \<in> (A \<inter> (f ` (r^1 `` {x}))) leadsTo B") 
13797  387 
apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) 
388 
apply (subst vimage_eq_UN) 

389 
apply (simp only: UN_simps [symmetric]) 

390 
apply (blast intro: leadsTo_UN) 

391 
done 

392 

393 

394 
(** Meta or object quantifier ? **) 

395 
lemma leadsTo_wf_induct: 

396 
"[ wf r; 

13805  397 
\<forall>m. F \<in> (A \<inter> f`{m}) leadsTo 
398 
((A \<inter> f`(r^1 `` {m})) \<union> B) ] 

399 
==> F \<in> A leadsTo B" 

13797  400 
apply (rule_tac t = A in subst) 
401 
defer 1 

402 
apply (rule leadsTo_UN) 

403 
apply (erule leadsTo_wf_induct_lemma) 

404 
apply assumption 

405 
apply fast (*Blast_tac: Function unknown's argument not a parameter*) 

406 
done 

407 

408 

409 
lemma bounded_induct: 

410 
"[ wf r; 

13805  411 
\<forall>m \<in> I. F \<in> (A \<inter> f`{m}) leadsTo 
412 
((A \<inter> f`(r^1 `` {m})) \<union> B) ] 

413 
==> F \<in> A leadsTo ((A  (f`I)) \<union> B)" 

13797  414 
apply (erule leadsTo_wf_induct, safe) 
13805  415 
apply (case_tac "m \<in> I") 
13797  416 
apply (blast intro: leadsTo_weaken) 
417 
apply (blast intro: subset_imp_leadsTo) 

418 
done 

419 

420 

13805  421 
(*Alternative proof is via the lemma F \<in> (A \<inter> f`(lessThan m)) leadsTo B*) 
13797  422 
lemma lessThan_induct: 
13805  423 
"[ !!m::nat. F \<in> (A \<inter> f`{m}) leadsTo ((A \<inter> f`{..m(}) \<union> B) ] 
424 
==> F \<in> A leadsTo B" 

13797  425 
apply (rule wf_less_than [THEN leadsTo_wf_induct]) 
426 
apply (simp (no_asm_simp)) 

427 
apply blast 

428 
done 

429 

430 
lemma lessThan_bounded_induct: 

13805  431 
"!!l::nat. [ \<forall>m \<in> greaterThan l. 
432 
F \<in> (A \<inter> f`{m}) leadsTo ((A \<inter> f`(lessThan m)) \<union> B) ] 

433 
==> F \<in> A leadsTo ((A \<inter> (f`(atMost l))) \<union> B)" 

13797  434 
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) 
435 
apply (rule wf_less_than [THEN bounded_induct]) 

436 
apply (simp (no_asm_simp)) 

437 
done 

438 

439 
lemma greaterThan_bounded_induct: 

13805  440 
"(!!l::nat. \<forall>m \<in> lessThan l. 
441 
F \<in> (A \<inter> f`{m}) leadsTo ((A \<inter> f`(greaterThan m)) \<union> B)) 

442 
==> F \<in> A leadsTo ((A \<inter> (f`(atLeast l))) \<union> B)" 

13797  443 
apply (rule_tac f = f and f1 = "%k. l  k" 
444 
in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct]) 

445 
apply (simp (no_asm) add: inv_image_def Image_singleton) 

446 
apply clarify 

447 
apply (case_tac "m<l") 

13805  448 
apply (blast intro: leadsTo_weaken_R diff_less_mono2) 
449 
apply (blast intro: not_leE subset_imp_leadsTo) 

13797  450 
done 
451 

452 

13798  453 
subsection{*wlt*} 
13797  454 

455 
(*Misra's property W3*) 

13805  456 
lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B" 
13797  457 
apply (unfold wlt_def) 
458 
apply (blast intro!: leadsTo_Union) 

459 
done 

460 

13805  461 
lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B" 
13797  462 
apply (unfold wlt_def) 
463 
apply (blast intro!: leadsTo_Union) 

464 
done 

465 

466 
(*Misra's property W2*) 

13805  467 
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)" 
13797  468 
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) 
469 

470 
(*Misra's property W4*) 

13805  471 
lemma wlt_increasing: "B \<subseteq> wlt F B" 
13797  472 
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) 
473 
done 

474 

475 

476 
(*Used in the Trans case below*) 

477 
lemma lemma1: 

13805  478 
"[ B \<subseteq> A2; 
479 
F \<in> (A1  B) co (A1 \<union> B); 

480 
F \<in> (A2  C) co (A2 \<union> C) ] 

481 
==> F \<in> (A1 \<union> A2  C) co (A1 \<union> A2 \<union> C)" 

13797  482 
by (unfold constrains_def, clarify, blast) 
483 

484 
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) 

485 
lemma leadsTo_123: 

13805  486 
"F \<in> A leadsTo A' 
487 
==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (BA') co (B \<union> A')" 

13797  488 
apply (erule leadsTo_induct) 
489 
(*Basis*) 

490 
apply (blast dest: ensuresD) 

491 
(*Trans*) 

492 
apply clarify 

13805  493 
apply (rule_tac x = "Ba \<union> Bb" in exI) 
13797  494 
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) 
495 
(*Union*) 

496 
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) 

13805  497 
apply (rule_tac x = "\<Union>A \<in> S. f A" in exI) 
13797  498 
apply (auto intro: leadsTo_UN) 
499 
(*Blast_tac says PROOF FAILED*) 

13805  500 
apply (rule_tac I1=S and A1="%i. f i  B" and A'1="%i. f i \<union> B" 
13798  501 
in constrains_UN [THEN constrains_weaken], auto) 
13797  502 
done 
503 

504 

505 
(*Misra's property W5*) 

13805  506 
lemma wlt_constrains_wlt: "F \<in> (wlt F B  B) co (wlt F B)" 
13798  507 
proof  
508 
from wlt_leadsTo [of F B, THEN leadsTo_123] 

509 
show ?thesis 

510 
proof (elim exE conjE) 

511 
(* assumes have to be in exactly the form as in the goal displayed at 

512 
this point. Isar doesn't give you any automation. *) 

513 
fix C 

514 
assume wlt: "wlt F B \<subseteq> C" 

515 
and lt: "F \<in> C leadsTo B" 

516 
and co: "F \<in> C  B co C \<union> B" 

517 
have eq: "C = wlt F B" 

518 
proof  

519 
from lt and wlt show ?thesis 

520 
by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1]) 

521 
qed 

522 
from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2) 

523 
qed 

524 
qed 

13797  525 

526 

13798  527 
subsection{*Completion: Binary and General Finite versions*} 
13797  528 

529 
lemma completion_lemma : 

13805  530 
"[ W = wlt F (B' \<union> C); 
531 
F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C); 

532 
F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) ] 

533 
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)" 

534 
apply (subgoal_tac "F \<in> (WC) co (W \<union> B' \<union> C) ") 

13797  535 
prefer 2 
536 
apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 

537 
THEN constrains_weaken]) 

13805  538 
apply (subgoal_tac "F \<in> (WC) co W") 
13797  539 
prefer 2 
540 
apply (simp add: wlt_increasing Un_assoc Un_absorb2) 

13805  541 
apply (subgoal_tac "F \<in> (A \<inter> W  C) leadsTo (A' \<inter> W \<union> C) ") 
13797  542 
prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) 
543 
(** LEVEL 6 **) 

13805  544 
apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ") 
13797  545 
prefer 2 
546 
apply (rule leadsTo_Un_duplicate2) 

547 
apply (blast intro: leadsTo_Un_Un wlt_leadsTo 

548 
[THEN psp2, THEN leadsTo_weaken] leadsTo_refl) 

549 
apply (drule leadsTo_Diff) 

550 
apply (blast intro: subset_imp_leadsTo) 

13805  551 
apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W") 
13797  552 
prefer 2 
553 
apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) 

554 
apply (blast intro: leadsTo_Trans subset_imp_leadsTo) 

555 
done 

556 

557 
lemmas completion = completion_lemma [OF refl] 

558 

559 
lemma finite_completion_lemma: 

13805  560 
"finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) > 
561 
(\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) > 

562 
F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 

13797  563 
apply (erule finite_induct, auto) 
564 
apply (rule completion) 

565 
prefer 4 

566 
apply (simp only: INT_simps [symmetric]) 

567 
apply (rule constrains_INT, auto) 

568 
done 

569 

570 
lemma finite_completion: 

571 
"[ finite I; 

13805  572 
!!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C); 
573 
!!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) ] 

574 
==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 

13797  575 
by (blast intro: finite_completion_lemma [THEN mp, THEN mp]) 
576 

577 
lemma stable_completion: 

13805  578 
"[ F \<in> A leadsTo A'; F \<in> stable A'; 
579 
F \<in> B leadsTo B'; F \<in> stable B' ] 

580 
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')" 

13797  581 
apply (unfold stable_def) 
582 
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R]) 

583 
apply (force+) 

584 
done 

585 

586 
lemma finite_stable_completion: 

587 
"[ finite I; 

13805  588 
!!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i); 
589 
!!i. i \<in> I ==> F \<in> stable (A' i) ] 

590 
==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)" 

13797  591 
apply (unfold stable_def) 
592 
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R]) 

593 
apply (simp_all (no_asm_simp)) 

594 
apply blast+ 

595 
done 

9685  596 

4776  597 
end 