equal
deleted
inserted
replaced
3591 apply(auto) |
3591 apply(auto) |
3592 apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1)) |
3592 apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1)) |
3593 by (metis append_Cons append_Nil contains50 f_cont2) |
3593 by (metis append_Cons append_Nil contains50 f_cont2) |
3594 |
3594 |
3595 |
3595 |
3596 (* |
3596 |
3597 lemma H00: |
|
3598 shows "((bder c) ` (AALTs_subs (AALTs bs rs))) = AALTs_subs (map (bder c) rs)" |
|
3599 *) |
|
3600 |
3597 |
3601 lemma H1: |
3598 lemma H1: |
3602 assumes "r >> bs2" "r \<in> AALTs_subs a" |
3599 assumes "r >> bs2" "r \<in> AALTs_subs a" |
3603 shows "a >> bs2" |
3600 shows "a >> bs2" |
3604 using assms |
3601 using assms |
3632 apply(induct rs1) |
3629 apply(induct rs1) |
3633 apply(auto) |
3630 apply(auto) |
3634 done |
3631 done |
3635 |
3632 |
3636 lemma H6: |
3633 lemma H6: |
3637 shows "AALTs_subs (AALTs bs (flts rs)) \<subseteq> AALTs_subs (AALTs bs rs)" |
3634 shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)" |
3638 apply(induct rs arbitrary: bs rule: flts.induct) |
3635 apply(induct rs arbitrary: bs rule: flts.induct) |
3639 apply(auto) |
3636 apply(auto) |
3640 by (metis AALTs_subs_fuse2 H7 UnE fuse_map subset_iff) |
3637 apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map) |
|
3638 apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map) |
|
3639 by (simp add: H7) |
3641 |
3640 |
3642 |
3641 |
3643 lemma H2: |
3642 lemma H2: |
3644 assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)" |
3643 assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)" |
3645 shows "r \<in> AALTs_subs (AALTs bs (flts rs))" |
3644 shows "r \<in> AALTs_subs (AALTs bs (flts rs))" |
3647 apply(induct rs arbitrary: r bs bs2 rule: flts.induct) |
3646 apply(induct rs arbitrary: r bs bs2 rule: flts.induct) |
3648 apply(auto) |
3647 apply(auto) |
3649 apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono) |
3648 apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono) |
3650 using H7 by blast |
3649 using H7 by blast |
3651 |
3650 |
3652 |
3651 lemma H00: |
|
3652 shows " (\<Union> (AALTs_subs ` (set (map (bder c o fuse bs) rs)))) \<subseteq> ((bder c) ` (AALTs_subs (AALTs bs rs)))" |
|
3653 apply(induct rs arbitrary: bs c) |
|
3654 apply(auto simp add: image_def) |
|
3655 |
|
3656 |
3653 |
3657 |
3654 lemma contains61a_2: |
3658 lemma contains61a_2: |
3655 assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" |
3659 assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" |
3656 shows "bsimp_AALTs bs rs >> bs2" |
3660 shows "bsimp_AALTs bs rs >> bs2" |
3657 using assms |
3661 using assms |
3755 apply(simp) |
3759 apply(simp) |
3756 apply(simp) |
3760 apply(simp) |
3757 apply(auto) |
3761 apply(auto) |
3758 |
3762 |
3759 |
3763 |
|
3764 |
3760 (* HERE HERE *) |
3765 (* HERE HERE *) |
3761 |
3766 |
3762 (* old *) |
3767 (* old *) |
3763 (* |
3768 (* |
3764 apply(drule contains59) |
3769 apply(drule contains59) |