src/HOL/UNITY/ELT.thy
 author wenzelm Thu Jul 23 22:13:42 2015 +0200 (2015-07-23) changeset 60773 d09c66a0ea10 parent 59807 22bc39064290 child 61952 546958347e05 permissions -rw-r--r--
more symbols by default, without xsymbols mode;
1 (*  Title:      HOL/UNITY/ELT.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1999  University of Cambridge
5 leadsTo strengthened with a specification of the allowable sets transient parts
7 TRY INSTEAD (to get rid of the {} and to gain strong induction)
9   elt :: "['a set set, 'a program, 'a set] => ('a set) set"
11 inductive "elt CC F B"
12   intros
14     Weaken:  "A <= B ==> A : elt CC F B"
16     ETrans:  "[| F : A ensures A';  A-A' : CC;  A' : elt CC F B |]
17               ==> A : elt CC F B"
19     Union:  "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
21   monos Pow_mono
22 *)
24 section{*Progress Under Allowable Sets*}
26 theory ELT imports Project begin
28 inductive_set
29   (*LEADS-TO constant for the inductive definition*)
30   elt :: "['a set set, 'a program] => ('a set * 'a set) set"
31   for CC :: "'a set set" and F :: "'a program"
32  where
34    Basis:  "[| F : A ensures B;  A-B : (insert {} CC) |] ==> (A,B) : elt CC F"
36  | Trans:  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
38  | Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
41 definition
42   (*the set of all sets determined by f alone*)
43   givenBy :: "['a => 'b] => 'a set set"
44   where "givenBy f = range (%B. f-` B)"
46 definition
47   (*visible version of the LEADS-TO relation*)
48   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
49                                         ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
50   where "leadsETo A CC B = {F. (A,B) : elt CC F}"
52 definition
53   LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
54                                         ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
55   where "LeadsETo A CC B =
56       {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
59 (*** givenBy ***)
61 lemma givenBy_id [simp]: "givenBy id = UNIV"
62 by (unfold givenBy_def, auto)
64 lemma givenBy_eq_all: "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}"
65 apply (unfold givenBy_def, safe)
66 apply (rule_tac  x = "v ` _" in image_eqI, auto)
67 done
69 lemma givenByI: "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v"
70 by (subst givenBy_eq_all, blast)
72 lemma givenByD: "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A"
73 by (unfold givenBy_def, auto)
75 lemma empty_mem_givenBy [iff]: "{} : givenBy v"
76 by (blast intro!: givenByI)
78 lemma givenBy_imp_eq_Collect: "A: givenBy v ==> EX P. A = {s. P(v s)}"
79 apply (rule_tac x = "%n. EX s. v s = n & s : A" in exI)
80 apply (simp (no_asm_use) add: givenBy_eq_all)
81 apply blast
82 done
84 lemma Collect_mem_givenBy: "{s. P(v s)} : givenBy v"
85 by (unfold givenBy_def, best)
87 lemma givenBy_eq_Collect: "givenBy v = {A. EX P. A = {s. P(v s)}}"
88 by (blast intro: Collect_mem_givenBy givenBy_imp_eq_Collect)
90 (*preserving v preserves properties given by v*)
91 lemma preserves_givenBy_imp_stable:
92      "[| F : preserves v;  D : givenBy v |] ==> F : stable D"
93 by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
95 lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
96 apply (simp (no_asm) add: givenBy_eq_Collect)
97 apply best
98 done
100 lemma givenBy_DiffI:
101      "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v"
102 apply (simp (no_asm_use) add: givenBy_eq_Collect)
103 apply safe
104 apply (rule_tac x = "%z. R z & ~ Q z" for R Q in exI)
105 unfolding set_diff_eq
106 apply auto
107 done
110 (** Standard leadsTo rules **)
112 lemma leadsETo_Basis [intro]:
113      "[| F: A ensures B;  A-B: insert {} CC |] ==> F : A leadsTo[CC] B"
114 apply (unfold leadsETo_def)
115 apply (blast intro: elt.Basis)
116 done
119      "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C"
120 apply (unfold leadsETo_def)
121 apply (blast intro: elt.Trans)
122 done
125 (*Useful with cancellation, disjunction*)
127      "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'"
128 by (simp add: Un_ac)
131      "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)"
132 by (simp add: Un_ac)
134 (*The Union introduction rule as we should have liked to state it*)
136     "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
137 apply (unfold leadsETo_def)
138 apply (blast intro: elt.Union)
139 done
142     "(!!i. i : I ==> F : (A i) leadsTo[CC] B)
143      ==> F : (UN i:I. A i) leadsTo[CC] B"
144 apply (subst Union_image_eq [symmetric])
145 apply (blast intro: leadsETo_Union)
146 done
148 (*The INDUCTION rule as we should have liked to state it*)
150   "[| F : za leadsTo[CC] zb;
151       !!A B. [| F : A ensures B;  A-B : insert {} CC |] ==> P A B;
152       !!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |]
153                ==> P A C;
154       !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B
155    |] ==> P za zb"
156 apply (unfold leadsETo_def)
157 apply (drule CollectD)
158 apply (erule elt.induct, blast+)
159 done
162 (** New facts involving leadsETo **)
164 lemma leadsETo_mono: "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)"
165 apply safe
166 apply (erule leadsETo_induct)
167 prefer 3 apply (blast intro: leadsETo_Union)
168 prefer 2 apply (blast intro: leadsETo_Trans)
169 apply blast
170 done
173      "[| F : A leadsTo[CC] B;  F : B leadsTo[DD] C |]
174       ==> F : A leadsTo[CC Un DD] C"
175 by (blast intro: leadsETo_mono [THEN subsetD] leadsETo_Trans)
178  "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B)
179   ==> F : (Union S Int C) leadsTo[CC] B"
180 apply (unfold leadsETo_def)
181 apply (simp only: Int_Union_Union)
182 apply (blast intro: elt.Union)
183 done
185 (*Binary union introduction rule*)
187      "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |]
188       ==> F : (A Un B) leadsTo[CC] C"
189   using leadsETo_Union [of "{A, B}" F CC C] by auto
192      "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
193 by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
196 lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
197 by (simp add: subset_imp_ensures [THEN leadsETo_Basis]
198               Diff_eq_empty_iff [THEN iffD2])
200 lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
204 (** Weakening laws **)
207      "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
211      "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
214 (*Distributes over binary unions*)
216      "F : (A Un B) leadsTo[CC] C  =
217       (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
221      "F : (UN i:I. A i) leadsTo[CC] B  =
222       (ALL i : I. F : (A i) leadsTo[CC] B)"
226      "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
230      "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]
231       ==> F : B leadsTo[CC] B'"
232 apply (drule leadsETo_mono [THEN subsetD], assumption)
233 apply (blast del: subsetCE
235 done
238      "[| F : A leadsTo[CC] A';  CC <= givenBy v |]
239       ==> F : A leadsTo[givenBy v] A'"
240 by (blast intro: leadsETo_weaken)
243 (*Set difference*)
245      "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |]
246       ==> F : A leadsTo[CC] C"
250 (*Binary union version*)
252      "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B' |]
253       ==> F : (A Un B) leadsTo[CC] (A' Un B')"
257 (** The cancellation law **)
260      "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |]
261       ==> F : A leadsTo[CC] (A' Un B')"
265      "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |]
266     ==> F : A leadsTo[CC] (B' Un A')"
267 apply (simp add: Un_commute)
268 apply (blast intro!: leadsETo_cancel2)
269 done
272      "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]
273     ==> F : A leadsTo[CC] (B' Un A')"
274 apply (rule leadsETo_cancel1)
275  prefer 2 apply assumption
276 apply simp_all
277 done
280 (** PSP: Progress-Safety-Progress **)
282 (*Special case of PSP: Misra's "stable conjunction"*)
283 lemma e_psp_stable:
284    "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |]
285     ==> F : (A Int B) leadsTo[CC] (A' Int B)"
286 apply (unfold stable_def)
287 apply (erule leadsETo_induct)
288 prefer 3 apply (blast intro: leadsETo_Union_Int)
289 prefer 2 apply (blast intro: leadsETo_Trans)
290 apply (rule leadsETo_Basis)
291 prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
292 apply (simp add: ensures_def Diff_Int_distrib2 [symmetric]
293                  Int_Un_distrib2 [symmetric])
294 apply (blast intro: transient_strengthen constrains_Int)
295 done
297 lemma e_psp_stable2:
298      "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |]
299       ==> F : (B Int A) leadsTo[CC] (B Int A')"
300 by (simp (no_asm_simp) add: e_psp_stable Int_ac)
302 lemma e_psp:
303      "[| F : A leadsTo[CC] A'; F : B co B';
304          ALL C:CC. C Int B Int B' : CC |]
305       ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
306 apply (erule leadsETo_induct)
307 prefer 3 apply (blast intro: leadsETo_Union_Int)
308 (*Transitivity case has a delicate argument involving "cancellation"*)
309 apply (rule_tac  leadsETo_Un_duplicate2)
310 apply (erule_tac  leadsETo_cancel_Diff1)
311 prefer 2
312  apply (simp add: Int_Diff Diff_triv)
313  apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
314 (*Basis case*)
315 apply (rule leadsETo_Basis)
316 apply (blast intro: psp_ensures)
317 apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
318 apply auto
319 done
321 lemma e_psp2:
322      "[| F : A leadsTo[CC] A'; F : B co B';
323          ALL C:CC. C Int B Int B' : CC |]
324       ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"
325 by (simp add: e_psp Int_ac)
328 (*** Special properties involving the parameter [CC] ***)
330 (*??IS THIS NEEDED?? or is it just an example of what's provable??*)
332      "[| F: (A leadsTo[givenBy v] B);  G : preserves v;
333          F\<squnion>G : stable C |]
334       ==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
335 apply (erule leadsETo_induct)
336   prefer 3
337   apply (subst Int_Union)
338   apply (blast intro: leadsETo_UN)
339 prefer 2
340  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
341 apply (rule leadsETo_Basis)
342 apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
343                       Int_Diff ensures_def givenBy_eq_Collect)
344 prefer 3 apply (blast intro: transient_strengthen)
345 apply (drule_tac  P1 = P in preserves_subset_stable [THEN subsetD])
346 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
347 apply (unfold stable_def)
348 apply (blast intro: constrains_Int [THEN constrains_weaken])+
349 done
351 (**** Relationship with traditional "leadsTo", strong & weak ****)
353 (** strong **)
356 apply safe
357 apply (erule leadsETo_induct)
358   prefer 3 apply (blast intro: leadsTo_Union)
359  prefer 2 apply (blast intro: leadsTo_Trans, blast)
360 done
363 apply safe
365 (*right-to-left case*)
366 apply (erule leadsTo_induct)
367   prefer 3 apply (blast intro: leadsETo_Union)
368  prefer 2 apply (blast intro: leadsETo_Trans, blast)
369 done
371 (**** weak ****)
374      "A LeadsTo[CC] B =
375         {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]
376         (reachable F Int B)}"
377 apply (unfold LeadsETo_def)
378 apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
379 done
381 (*** Introduction rules: Basis, Trans, Union ***)
384      "[| F : A LeadsTo[CC] B;  F : B LeadsTo[CC] C |]
385       ==> F : A LeadsTo[CC] C"
387 apply (blast intro: leadsETo_Trans)
388 done
391      "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
393 apply (subst Int_Union)
394 apply (blast intro: leadsETo_UN)
395 done
398      "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)
399       ==> F : (UN i:I. A i) LeadsTo[CC] B"
400 apply (simp only: Union_image_eq [symmetric])
401 apply (blast intro: LeadsETo_Union)
402 done
404 (*Binary union introduction rule*)
406      "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]
407       ==> F : (A Un B) LeadsTo[CC] C"
408   using LeadsETo_Union [of "{A, B}" F CC C] by auto
410 (*Lets us look at the starting state*)
412      "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
413 by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
416      "A <= B ==> F : A LeadsTo[CC] B"
418 apply (blast intro: subset_imp_leadsETo)
419 done
421 lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
424      "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
426 apply (blast intro: leadsETo_weaken_R)
427 done
430      "[| F : A LeadsTo[CC] A';  B <= A |] ==> F : B LeadsTo[CC] A'"
432 apply (blast intro: leadsETo_weaken_L)
433 done
436      "[| F : A LeadsTo[CC'] A';
437          B <= A;  A' <= B';  CC' <= CC |]
438       ==> F : B LeadsTo[CC] B'"
440 apply (blast intro: leadsETo_weaken)
441 done
445 apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD])
446 done
448 (*Postcondition can be strengthened to (reachable F Int B) *)
449 lemma reachable_ensures:
450      "F : A ensures B ==> F : (reachable F Int A) ensures B"
451 apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto)
452 done
454 lemma lel_lemma:
455      "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
456 apply (erule leadsTo_induct)
457   apply (blast intro: reachable_ensures)
458  apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
459 apply (subst Int_Union)
460 apply (blast intro: leadsETo_UN)
461 done
464 apply safe
466 (*right-to-left case*)
468 apply (blast intro: lel_lemma [THEN leadsETo_weaken])
469 done
472 (**** EXTEND/PROJECT PROPERTIES ****)
474 context Extend
475 begin
477 lemma givenBy_o_eq_extend_set:
478      "givenBy (v o f) = extend_set h ` (givenBy v)"
479 apply (simp add: givenBy_eq_Collect)
480 apply (rule equalityI, best)
481 apply blast
482 done
484 lemma givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
485 by (simp add: givenBy_eq_Collect, best)
487 lemma extend_set_givenBy_I:
488      "D : givenBy v ==> extend_set h D : givenBy (v o f)"
489 apply (simp (no_asm_use) add: givenBy_eq_all, blast)
490 done
493      "F : A leadsTo[CC] B
494       ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
495                        (extend_set h B)"
496 apply (erule leadsETo_induct)
497   apply (force intro: subset_imp_ensures
498                simp add: extend_ensures extend_set_Diff_distrib [symmetric])
499  apply (blast intro: leadsETo_Trans)
501 done
504 (*This version's stronger in the "ensures" precondition
505   BUT there's no ensures_weaken_L*)
506 lemma Join_project_ensures_strong:
507      "[| project h C G ~: transient (project_set h C Int (A-B)) |
508            project_set h C Int (A - B) = {};
509          extend h F\<squnion>G : stable C;
510          F\<squnion>project h C G : (project_set h C Int A) ensures B |]
511       ==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)"
512 apply (subst Int_extend_set_lemma [symmetric])
513 apply (rule Join_project_ensures)
514 apply (auto simp add: Int_Diff)
515 done
517 (*NOT WORKING.  MODIFY AS IN Project.thy
518 lemma pld_lemma:
519      "[| extend h F\<squnion>G : stable C;
520          F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;
521          G : preserves (v o f) |]
522       ==> extend h F\<squnion>G :
523             (C Int extend_set h (project_set h C Int A))
524             leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
525 apply (erule leadsETo_induct)
526   prefer 3
527   apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union)
528  prefer 2
529  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
530 txt{*Base case is hard*}
531 apply auto
532 apply (force intro: leadsETo_Basis subset_imp_ensures)
533 apply (rule leadsETo_Basis)
534  prefer 2
535  apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
536 apply (rule Join_project_ensures_strong)
537 apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
538 apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
539 done
542      "[| extend h F\<squnion>G : stable C;
543          F\<squnion>project h C G :
544              (project_set h C Int A)
545              leadsTo[(%D. project_set h C Int D)`givenBy v] B;
546          G : preserves (v o f) |]
547       ==> extend h F\<squnion>G : (C Int extend_set h A)
548             leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
549 apply (rule pld_lemma [THEN leadsETo_weaken])
550 apply (auto simp add: split_extended_all)
551 done
554      "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;
555          G : preserves (v o f) |]
556       ==> extend h F\<squnion>G : (extend_set h A)
557             leadsTo[givenBy (v o f)] (extend_set h B)"
558 apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto)
559 apply (erule leadsETo_givenBy)
560 apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
561 done
564      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G
565              : A LeadsTo[givenBy v] B;
566          G : preserves (v o f) |]
567       ==> extend h F\<squnion>G :
568             (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
569 apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
571  apply (erule leadsETo_mono [THEN  rev_subsetD])
572  apply (blast intro: extend_set_givenBy_I)
573 apply (simp add: project_set_reachable_extend_eq [symmetric])
574 done
577      "(ALL G. extend h F ok G --> G : preserves (v o f))
578       ==> extending (%G. UNIV) h F
579                 (extend_set h A leadsTo[givenBy (v o f)] extend_set h B)
580                 (A leadsTo[givenBy v] B)"
581 apply (unfold extending_def)
583 done
586      "(ALL G. extend h F ok G --> G : preserves (v o f))
587       ==> extending (%G. reachable (extend h F\<squnion>G)) h F
588                 (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)
589                 (A LeadsTo[givenBy v]  B)"
590 apply (unfold extending_def)
591 apply (blast intro: project_LeadsETo_D)
592 done
593 *)
596 (*** leadsETo in the precondition ***)
598 (*Lemma for the Trans case*)
599 lemma pli_lemma:
600      "[| extend h F\<squnion>G : stable C;
601          F\<squnion>project h C G
602            : project_set h C Int project_set h A leadsTo project_set h B |]
603       ==> F\<squnion>project h C G
604             : project_set h C Int project_set h A leadsTo
605               project_set h C Int project_set h B"
606 apply (rule psp_stable2 [THEN leadsTo_weaken_L])
607 apply (auto simp add: project_stable_project_set extend_stable_project_set)
608 done
611      "[| extend h F\<squnion>G : stable C;
612          extend h F\<squnion>G :
613            (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]
614   ==> F\<squnion>project h C G
615     : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
616 apply (erule leadsETo_induct)
617   prefer 3
618   apply (simp only: Int_UN_distrib project_set_Union)
619   apply (blast intro: leadsTo_UN)
620  prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
621 apply (simp add: givenBy_eq_extend_set)
622 apply (rule leadsTo_Basis)
623 apply (blast intro: ensures_extend_set_imp_project_ensures)
624 done
627      "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
628       ==> F\<squnion>project h UNIV G : A leadsTo B"
629 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
630 done
633      "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)
634       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G
635            : A LeadsTo B"
638 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
639 done
642      "projecting (%G. UNIV) h F
643                  (extend_set h A leadsTo[givenBy f] extend_set h B)
644                  (A leadsTo B)"
645 apply (unfold projecting_def)
646 apply (force dest: project_leadsETo_I)
647 done