src/HOL/UNITY/WFair.thy
 author wenzelm Thu Jul 23 22:13:42 2015 +0200 (2015-07-23) changeset 60773 d09c66a0ea10 parent 58889 5b7a9633cfa8 child 61824 dcbe9f756ae0 permissions -rw-r--r--
more symbols by default, without xsymbols mode;
1 (*  Title:      HOL/UNITY/WFair.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1998  University of Cambridge
5 Conditional Fairness versions of transient, ensures, leadsTo.
7 From Misra, "A Logic for Concurrent Programming", 1994
8 *)
10 section{*Progress*}
12 theory WFair imports UNITY begin
14 text{*The original version of this theory was based on weak fairness.  (Thus,
15 the entire UNITY development embodied this assumption, until February 2003.)
16 Weak fairness states that if a command is enabled continuously, then it is
17 eventually executed.  Ernie Cohen suggested that I instead adopt unconditional
18 fairness: every command is executed infinitely often.
20 In fact, Misra's paper on "Progress" seems to be ambiguous about the correct
21 interpretation, and says that the two forms of fairness are equivalent.  They
22 differ only on their treatment of partial transitions, which under
23 unconditional fairness behave magically.  That is because if there are partial
24 transitions then there may be no fair executions, making all leads-to
25 properties hold vacuously.
27 Unconditional fairness has some great advantages.  By distinguishing partial
28 transitions from total ones that are the identity on part of their domain, it
29 is more expressive.  Also, by simplifying the definition of the transient
30 property, it simplifies many proofs.  A drawback is that some laws only hold
31 under the assumption that all transitions are total.  The best-known of these
32 is the impossibility law for leads-to.
33 *}
35 definition
37   --{*This definition specifies conditional fairness.  The rest of the theory
38       is generic to all forms of fairness.  To get weak fairness, conjoin
39       the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies
40       that the action is enabled over all of @{term A}.*}
41   transient :: "'a set => 'a program set" where
42     "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
44 definition
45   ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60) where
46     "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
49 inductive_set
50   leads :: "'a program => ('a set * 'a set) set"
51     --{*LEADS-TO constant for the inductive definition*}
52   for F :: "'a program"
53   where
55     Basis:  "F \<in> A ensures B ==> (A,B) \<in> leads F"
57   | Trans:  "[| (A,B) \<in> leads F;  (B,C) \<in> leads F |] ==> (A,C) \<in> leads F"
59   | Union:  "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
62 definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) where
63      --{*visible version of the LEADS-TO relation*}
64     "A leadsTo B == {F. (A,B) \<in> leads F}"
66 definition wlt :: "['a program, 'a set] => 'a set" where
67      --{*predicate transformer: the largest set that leads to @{term B}*}
68     "wlt F B == Union {A. F \<in> A leadsTo B}"
70 notation leadsTo  (infixl "\<longmapsto>" 60)
73 subsection{*transient*}
75 lemma stable_transient:
76     "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
77 apply (simp add: stable_def constrains_def transient_def, clarify)
78 apply (rule rev_bexI, auto)
79 done
81 lemma stable_transient_empty:
82     "[| F \<in> stable A; F \<in> transient A; all_total F |] ==> A = {}"
83 apply (drule stable_transient, assumption)
84 apply (simp add: all_total_def)
85 done
87 lemma transient_strengthen:
88     "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
89 apply (unfold transient_def, clarify)
90 apply (blast intro!: rev_bexI)
91 done
93 lemma transientI:
94     "[| act: Acts F;  act``A \<subseteq> -A |] ==> F \<in> transient A"
95 by (unfold transient_def, blast)
97 lemma transientE:
98     "[| F \<in> transient A;
99         !!act. [| act: Acts F;  act``A \<subseteq> -A |] ==> P |]
100      ==> P"
101 by (unfold transient_def, blast)
103 lemma transient_empty [simp]: "transient {} = UNIV"
104 by (unfold transient_def, auto)
107 text{*This equation recovers the notion of weak fairness.  A totalized
108       program satisfies a transient assertion just if the original program
109       contains a suitable action that is also enabled.*}
110 lemma totalize_transient_iff:
111    "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
112 apply (simp add: totalize_def totalize_act_def transient_def
113                  Un_Image, safe)
114 apply (blast intro!: rev_bexI)+
115 done
117 lemma totalize_transientI:
118     "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |]
119      ==> totalize F \<in> transient A"
120 by (simp add: totalize_transient_iff, blast)
122 subsection{*ensures*}
124 lemma ensuresI:
125     "[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B"
126 by (unfold ensures_def, blast)
128 lemma ensuresD:
129     "F \<in> A ensures B ==> F \<in> (A-B) co (A \<union> B) & F \<in> transient (A-B)"
130 by (unfold ensures_def, blast)
132 lemma ensures_weaken_R:
133     "[| F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'"
134 apply (unfold ensures_def)
135 apply (blast intro: constrains_weaken transient_strengthen)
136 done
138 text{*The L-version (precondition strengthening) fails, but we have this*}
139 lemma stable_ensures_Int:
140     "[| F \<in> stable C;  F \<in> A ensures B |]
141     ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
142 apply (unfold ensures_def)
143 apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
144 prefer 2 apply (blast intro: transient_strengthen)
145 apply (blast intro: stable_constrains_Int constrains_weaken)
146 done
148 lemma stable_transient_ensures:
149      "[| F \<in> stable A;  F \<in> transient C;  A \<subseteq> B \<union> C |] ==> F \<in> A ensures B"
150 apply (simp add: ensures_def stable_def)
151 apply (blast intro: constrains_weaken transient_strengthen)
152 done
154 lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)"
155 by (simp (no_asm) add: ensures_def unless_def)
160 lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B"
161 apply (unfold leadsTo_def)
162 apply (blast intro: leads.Basis)
163 done
166      "[| F \<in> A leadsTo B;  F \<in> B leadsTo C |] ==> F \<in> A leadsTo C"
167 apply (unfold leadsTo_def)
168 apply (blast intro: leads.Trans)
169 done
172      "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
173 apply (drule_tac B = "A-B" in constrains_weaken_L)
174 apply (drule_tac  B = "A-B" in transient_strengthen)
175 apply (rule_tac  ensuresI [THEN leadsTo_Basis])
176 apply (blast+)
177 done
179 lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
180 by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
182 text{*Useful with cancellation, disjunction*}
183 lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
184 by (simp add: Un_ac)
187      "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
188 by (simp add: Un_ac)
190 text{*The Union introduction rule as we should have liked to state it*}
192     "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
193 apply (unfold leadsTo_def)
194 apply (blast intro: leads.Union)
195 done
198  "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
199 apply (unfold leadsTo_def)
200 apply (simp only: Int_Union_Union)
201 apply (blast intro: leads.Union)
202 done
205     "(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B"
206 apply (subst Union_image_eq [symmetric])
207 apply (blast intro: leadsTo_Union)
208 done
210 text{*Binary union introduction rule*}
212      "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
213   using leadsTo_Union [of "{A, B}" F C] by auto
216      "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
217 by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
220 text{*The INDUCTION rule as we should have liked to state it*}
222   "[| F \<in> za leadsTo zb;
223       !!A B. F \<in> A ensures B ==> P A B;
224       !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]
225                ==> P A C;
226       !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B
227    |] ==> P za zb"
228 apply (unfold leadsTo_def)
229 apply (drule CollectD, erule leads.induct)
230 apply (blast+)
231 done
234 lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
235 by (unfold ensures_def constrains_def transient_def, blast)
237 lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
239 lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo]
241 lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, simp]
243 lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, simp]
247 (** Variant induction rule: on the preconditions for B **)
249 text{*Lemma is the weak version: can't see how to do it in one step*}
251   "[| F \<in> za leadsTo zb;
252       P zb;
253       !!A B. [| F \<in> A ensures B;  P B |] ==> P A;
254       !!S. \<forall>A \<in> S. P A ==> P (Union S)
255    |] ==> P za"
256 txt{*by induction on this formula*}
257 apply (subgoal_tac "P zb --> P za")
258 txt{*now solve first subgoal: this formula is sufficient*}
259 apply (blast intro: leadsTo_refl)
260 apply (erule leadsTo_induct)
261 apply (blast+)
262 done
265   "[| F \<in> za leadsTo zb;
266       P zb;
267       !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P B |] ==> P A;
268       !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)
269    |] ==> P za"
270 apply (subgoal_tac "F \<in> za leadsTo zb & P za")
271 apply (erule conjunct2)
272 apply (erule leadsTo_induct_pre_lemma)
273 prefer 3 apply (blast intro: leadsTo_Union)
274 prefer 2 apply (blast intro: leadsTo_Trans)
275 apply (blast intro: leadsTo_refl)
276 done
279 lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
283      "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
286 text{*Distributes over binary unions*}
288      "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
292      "F \<in> (\<Union>i \<in> I. A i) leadsTo B  =  (\<forall>i \<in> I. F \<in> (A i) leadsTo B)"
296      "F \<in> (Union S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
301      "[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'"
305 text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
307      "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
311    "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))
312     ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
313 apply (simp only: Union_image_eq [symmetric])
315 done
317 text{*Binary union version*}
319      "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]
320       ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
324 (** The cancellation law **)
327      "[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |]
328       ==> F \<in> A leadsTo (A' \<union> B')"
332      "[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |]
333       ==> F \<in> A leadsTo (A' \<union> B')"
334 apply (rule leadsTo_cancel2)
335 prefer 2 apply assumption
336 apply (simp_all (no_asm_simp))
337 done
340      "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |]
341     ==> F \<in> A leadsTo (B' \<union> A')"
342 apply (simp add: Un_commute)
343 apply (blast intro!: leadsTo_cancel2)
344 done
347      "[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |]
348     ==> F \<in> A leadsTo (B' \<union> A')"
349 apply (rule leadsTo_cancel1)
350 prefer 2 apply assumption
351 apply (simp_all (no_asm_simp))
352 done
355 text{*The impossibility law*}
356 lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
357 apply (erule leadsTo_induct_pre)
358 apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
359 apply (drule bspec, assumption)+
360 apply blast
361 done
363 subsection{*PSP: Progress-Safety-Progress*}
365 text{*Special case of PSP: Misra's "stable conjunction"*}
366 lemma psp_stable:
367    "[| F \<in> A leadsTo A'; F \<in> stable B |]
368     ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
369 apply (unfold stable_def)
370 apply (erule leadsTo_induct)
371 prefer 3 apply (blast intro: leadsTo_Union_Int)
372 prefer 2 apply (blast intro: leadsTo_Trans)
373 apply (rule leadsTo_Basis)
374 apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
375 apply (blast intro: transient_strengthen constrains_Int)
376 done
378 lemma psp_stable2:
379    "[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')"
380 by (simp add: psp_stable Int_ac)
382 lemma psp_ensures:
383    "[| F \<in> A ensures A'; F \<in> B co B' |]
384     ==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
385 apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
386 apply (blast intro: transient_strengthen)
387 done
389 lemma psp:
390      "[| F \<in> A leadsTo A'; F \<in> B co B' |]
391       ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
392 apply (erule leadsTo_induct)
393   prefer 3 apply (blast intro: leadsTo_Union_Int)
394  txt{*Basis case*}
395  apply (blast intro: psp_ensures)
396 txt{*Transitivity case has a delicate argument involving "cancellation"*}
397 apply (rule leadsTo_Un_duplicate2)
398 apply (erule leadsTo_cancel_Diff1)
399 apply (simp add: Int_Diff Diff_triv)
400 apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
401 done
403 lemma psp2:
404      "[| F \<in> A leadsTo A'; F \<in> B co B' |]
405     ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
406 by (simp (no_asm_simp) add: psp Int_ac)
408 lemma psp_unless:
409    "[| F \<in> A leadsTo A';  F \<in> B unless B' |]
410     ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
412 apply (unfold unless_def)
413 apply (drule psp, assumption)
414 apply (blast intro: leadsTo_weaken)
415 done
418 subsection{*Proving the induction rules*}
420 (** The most general rule: r is any wf relation; f is any variant function **)
423      "[| wf r;
424          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo
425                     ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
426       ==> F \<in> (A \<inter> f-`{m}) leadsTo B"
427 apply (erule_tac a = m in wf_induct)
428 apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B")
430 apply (subst vimage_eq_UN)
431 apply (simp only: UN_simps [symmetric])
432 apply (blast intro: leadsTo_UN)
433 done
436 (** Meta or object quantifier ? **)
438      "[| wf r;
439          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo
440                     ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
441       ==> F \<in> A leadsTo B"
442 apply (rule_tac t = A in subst)
443  defer 1
444  apply (rule leadsTo_UN)
445  apply (erule leadsTo_wf_induct_lemma)
446  apply assumption
447 apply fast (*Blast_tac: Function unknown's argument not a parameter*)
448 done
451 lemma bounded_induct:
452      "[| wf r;
453          \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo
454                       ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
455       ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)"
456 apply (erule leadsTo_wf_induct, safe)
457 apply (case_tac "m \<in> I")
458 apply (blast intro: leadsTo_weaken)
459 apply (blast intro: subset_imp_leadsTo)
460 done
463 (*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
464 lemma lessThan_induct:
465      "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..<m}) \<union> B) |]
466       ==> F \<in> A leadsTo B"
467 apply (rule wf_less_than [THEN leadsTo_wf_induct])
468 apply (simp (no_asm_simp))
469 apply blast
470 done
472 lemma lessThan_bounded_induct:
473      "!!l::nat. [| \<forall>m \<in> greaterThan l.
474             F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |]
475       ==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
476 apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
477 apply (rule wf_less_than [THEN bounded_induct])
478 apply (simp (no_asm_simp))
479 done
481 lemma greaterThan_bounded_induct:
482      "(!!l::nat. \<forall>m \<in> lessThan l.
483                  F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B))
484       ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
485 apply (rule_tac f = f and f1 = "%k. l - k"
486        in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
487 apply (simp (no_asm) add:Image_singleton)
488 apply clarify
489 apply (case_tac "m<l")
490  apply (blast intro: leadsTo_weaken_R diff_less_mono2)
491 apply (blast intro: not_leE subset_imp_leadsTo)
492 done
495 subsection{*wlt*}
497 text{*Misra's property W3*}
498 lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
499 apply (unfold wlt_def)
500 apply (blast intro!: leadsTo_Union)
501 done
503 lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B"
504 apply (unfold wlt_def)
505 apply (blast intro!: leadsTo_Union)
506 done
508 text{*Misra's property W2*}
509 lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
512 text{*Misra's property W4*}
513 lemma wlt_increasing: "B \<subseteq> wlt F B"
515 done
518 text{*Used in the Trans case below*}
519 lemma lemma1:
520    "[| B \<subseteq> A2;
521        F \<in> (A1 - B) co (A1 \<union> B);
522        F \<in> (A2 - C) co (A2 \<union> C) |]
523     ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
524 by (unfold constrains_def, clarify,  blast)
526 text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
528      "F \<in> A leadsTo A'
529       ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
530 apply (erule leadsTo_induct)
531   txt{*Basis*}
532   apply (blast dest: ensuresD)
533  txt{*Trans*}
534  apply clarify
535  apply (rule_tac x = "Ba \<union> Bb" in exI)
537 txt{*Union*}
538 apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
539 apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
540 apply (auto intro: leadsTo_UN)
541 (*Blast_tac says PROOF FAILED*)
542 apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B"
543        in constrains_UN [THEN constrains_weaken], auto)
544 done
547 text{*Misra's property W5*}
548 lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
549 proof -
550   from wlt_leadsTo [of F B, THEN leadsTo_123]
551   show ?thesis
552   proof (elim exE conjE)
553 (* assumes have to be in exactly the form as in the goal displayed at
554    this point.  Isar doesn't give you any automation. *)
555     fix C
556     assume wlt: "wlt F B \<subseteq> C"
557        and lt:  "F \<in> C leadsTo B"
558        and co:  "F \<in> C - B co C \<union> B"
559     have eq: "C = wlt F B"
560     proof -
561       from lt and wlt show ?thesis
562            by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
563     qed
564     from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
565   qed
566 qed
569 subsection{*Completion: Binary and General Finite versions*}
571 lemma completion_lemma :
572      "[| W = wlt F (B' \<union> C);
573        F \<in> A leadsTo (A' \<union> C);  F \<in> A' co (A' \<union> C);
574        F \<in> B leadsTo (B' \<union> C);  F \<in> B' co (B' \<union> C) |]
575     ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
576 apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ")
577  prefer 2
578  apply (blast intro: wlt_constrains_wlt [THEN  constrains_Un,
579                                          THEN constrains_weaken])
580 apply (subgoal_tac "F \<in> (W-C) co W")
581  prefer 2
582  apply (simp add: wlt_increasing Un_assoc Un_absorb2)
583 apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
584  prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
585 (** LEVEL 6 **)
586 apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
587  prefer 2
588  apply (rule leadsTo_Un_duplicate2)
591 apply (drule leadsTo_Diff)
592 apply (blast intro: subset_imp_leadsTo)
593 apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")
594  prefer 2
595  apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
597 done
599 lemmas completion = completion_lemma [OF refl]
601 lemma finite_completion_lemma:
602      "finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) -->
603                    (\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) -->
604                    F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
605 apply (erule finite_induct, auto)
606 apply (rule completion)
607    prefer 4
608    apply (simp only: INT_simps [symmetric])
609    apply (rule constrains_INT, auto)
610 done
612 lemma finite_completion:
613      "[| finite I;
614          !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C);
615          !!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |]
616       ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
617 by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
619 lemma stable_completion:
620      "[| F \<in> A leadsTo A';  F \<in> stable A';
621          F \<in> B leadsTo B';  F \<in> stable B' |]
622     ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
623 apply (unfold stable_def)
624 apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
625 apply (force+)
626 done
628 lemma finite_stable_completion:
629      "[| finite I;
630          !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i);
631          !!i. i \<in> I ==> F \<in> stable (A' i) |]
632       ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)"
633 apply (unfold stable_def)
634 apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
635 apply (simp_all (no_asm_simp))
636 apply blast+
637 done
639 end