469 lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)" |
469 lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)" |
470 apply safe |
470 apply safe |
471 apply (erule LeadsETo_subset_LeadsTo [THEN subsetD]) |
471 apply (erule LeadsETo_subset_LeadsTo [THEN subsetD]) |
472 (*right-to-left case*) |
472 (*right-to-left case*) |
473 apply (unfold LeadsETo_def LeadsTo_def) |
473 apply (unfold LeadsETo_def LeadsTo_def) |
474 apply (fast elim: lel_lemma [THEN leadsETo_weaken]) |
474 apply (blast intro: lel_lemma [THEN leadsETo_weaken]) |
475 done |
475 done |
476 |
476 |
477 |
477 |
478 (**** EXTEND/PROJECT PROPERTIES ****) |
478 (**** EXTEND/PROJECT PROPERTIES ****) |
479 |
479 |
480 lemma (in Extend) givenBy_o_eq_extend_set: |
480 lemma (in Extend) givenBy_o_eq_extend_set: |
481 "givenBy (v o f) = extend_set h ` (givenBy v)" |
481 "givenBy (v o f) = extend_set h ` (givenBy v)" |
|
482 apply (simp add: givenBy_eq_Collect) |
|
483 apply (rule equalityI, best) |
|
484 apply blast |
|
485 done |
|
486 |
|
487 lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)" |
482 by (simp add: givenBy_eq_Collect, best) |
488 by (simp add: givenBy_eq_Collect, best) |
483 |
|
484 lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)" |
|
485 apply (simp (no_asm) add: givenBy_eq_Collect) |
|
486 apply best |
|
487 done |
|
488 |
489 |
489 lemma (in Extend) extend_set_givenBy_I: |
490 lemma (in Extend) extend_set_givenBy_I: |
490 "D : givenBy v ==> extend_set h D : givenBy (v o f)" |
491 "D : givenBy v ==> extend_set h D : givenBy (v o f)" |
491 apply (simp (no_asm_use) add: givenBy_eq_all) |
492 apply (simp (no_asm_use) add: givenBy_eq_all, blast) |
492 apply blast |
|
493 done |
493 done |
494 |
494 |
495 lemma (in Extend) leadsETo_imp_extend_leadsETo: |
495 lemma (in Extend) leadsETo_imp_extend_leadsETo: |
496 "F : A leadsTo[CC] B |
496 "F : A leadsTo[CC] B |
497 ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] |
497 ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] |