3506 

  3507 

  3508 lemma [simp]:

  3509   shows "size (fuse bs r) = size r"

  3510   by (induct r) (auto)

  3511 

  3512 fun AALTs_subs where

  3513   "AALTs_subs (AZERO) = {}"

  3514 | "AALTs_subs (AONE bs) = {AONE bs}"

  3515 | "AALTs_subs (ACHAR bs c) = {ACHAR bs c}"

  3516 | "AALTs_subs (ASEQ bs r1 r2) = {ASEQ bs r1 r2}"

  3517 | "AALTs_subs (ASTAR bs r) = {ASTAR bs r}"

  3518 | "AALTs_subs (AALTs bs []) = {}"

  3519 | "AALTs_subs (AALTs bs (r#rs)) = AALTs_subs (fuse bs r) \<union> AALTs_subs (AALTs bs rs)"

  3520 

  3521 lemma nonalt_10:

  3522   assumes "nonalt r" "r \<noteq> AZERO"

  3523   shows "r \<in> AALTs_subs r"

  3524   using assms

  3525   apply(induct r)

  3526        apply(auto)

  3527   done

  3528 

  3529 lemma flt_fuse:

  3530   shows "flts (map (fuse bs) rs) = map (fuse bs) (flts rs)"

  3531   apply(induct rs arbitrary: bs rule: flts.induct)

  3532         apply(auto)

  3533   by (simp add: fuse_append)

  3534 

  3535 lemma AALTs_subs_fuse: 

  3536   shows "AALTs_subs (fuse bs r) = (fuse bs) ` (AALTs_subs r)"

  3537   apply(induct r arbitrary: bs rule: AALTs_subs.induct)

  3538        apply(auto)

  3539    apply (simp add: fuse_append)

  3540   apply blast

  3541   by (simp add: fuse_append)

  3542 

  3543 lemma AALTs_subs_fuse2: 

  3544   shows "AALTs_subs (AALTs bs rs) = AALTs_subs (AALTs [] (map (fuse bs) rs))"

  3545   apply(induct rs arbitrary: bs)

  3546    apply(auto)

  3547    apply (auto simp add: fuse_empty)

  3548   done

  3549 

  3550 lemma fuse_map:

  3551   shows "map (fuse (bs1 @ bs2)) rs = map (fuse bs1) (map (fuse bs2) rs)"

  3552   apply(induct rs)

  3553    apply(auto)

  3554   using fuse_append by blast

  3555   

  3556 

  3557  

  3558 lemma contains59_2:

  3559   assumes "AALTs bs rs >> bs2" 

  3560   shows "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2"

  3561   using assms

  3562   apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list  (map asize rs)" rule: measure_induct)

  3563   apply(case_tac x)

  3564   apply(auto)

  3565   using contains59 apply force

  3566   apply(erule contains.cases)

  3567         apply(auto)

  3568    apply(case_tac "r = AZERO")

  3569     apply(simp)

  3570     apply (metis bsimp_AALTs.simps(1) contains61 empty_iff empty_set)

  3571    apply(case_tac "nonalt r")

  3572   apply (metis UnCI bsimp_AALTs.simps(1) contains0 contains61 empty_iff empty_set nn11a nonalt_10)

  3573    apply(subgoal_tac "\<exists>bsX rsX. r = AALTs bsX rsX")

  3574     prefer 2

  3575   using bbbbs1 apply blast

  3576    apply(auto)

  3577    apply (metis UnCI contains0 fuse.simps(4) less_add_Suc1)

  3578   apply(drule_tac x="rs" in spec)

  3579   apply(drule mp)

  3580    apply(simp add: asize0)

  3581   apply(drule_tac x="bsa" in spec)

  3582   apply(drule_tac x="bsa @ bs1" in spec)

  3583   apply(auto)

  3584   done

  3585 

  3586 lemma TEMPLATE_contains61a:

  3587   assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2"

  3588   shows "bsimp_AALTs bs rs >> bs2" 

  3589   using assms

  3590   apply(induct rs arbitrary: bs2 bs)

  3591    apply(auto)

  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)

  3594 

  3595 

  3596 (*

  3597 lemma H00:

  3598   shows "((bder c) ` (AALTs_subs (AALTs bs rs))) =  AALTs_subs (map (bder c) rs)"

  3599 *)

  3600 

  3601 lemma H1:

  3602   assumes "r >> bs2" "r \<in> AALTs_subs a" 

  3603   shows "a >> bs2"

  3604   using assms

  3605   apply(induct a arbitrary: r bs2 rule: AALTs_subs.induct)

  3606         apply(auto)

  3607    apply (simp add: contains60)

  3608   by (simp add: contains59 contains60)

  3609 

  3610 lemma H3:

  3611   assumes "a >> bs"

  3612   shows "\<exists>r \<in> AALTs_subs a. r >> bs"

  3613   using assms

  3614   apply(induct a bs)

  3615         apply(auto intro: contains.intros)

  3616   using contains.intros(4) contains59_2 by fastforce

  3617 

  3618 lemma H4:

  3619   shows "AALTs_subs (AALTs bs rs1) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))"

  3620   apply(induct rs1)

  3621    apply(auto)

  3622   done

  3623 

  3624 lemma H5:

  3625   shows "AALTs_subs (AALTs bs rs2) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))"

  3626   apply(induct rs1)

  3627    apply(auto)

  3628   done

  3629 

  3630 lemma H7:

  3631   shows "AALTs_subs (AALTs bs (rs1 @ rs2)) = AALTs_subs (AALTs bs rs1) \<union> AALTs_subs (AALTs bs rs2)"

  3632   apply(induct rs1)

  3633    apply(auto)

  3634   done

  3635 

  3636 lemma H6:

  3637   shows "AALTs_subs (AALTs bs (flts rs)) \<subseteq> AALTs_subs (AALTs bs rs)"

  3638   apply(induct rs arbitrary: bs rule: flts.induct)

  3639         apply(auto)

  3640   by (metis AALTs_subs_fuse2 H7 UnE fuse_map subset_iff)

  3641 

  3642 

  3643 lemma H2:

  3644   assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)" 

  3645   shows "r \<in> AALTs_subs (AALTs bs (flts rs))"

  3646   using assms

  3647   apply(induct rs arbitrary: r bs bs2 rule: flts.induct)

  3648         apply(auto)

  3649    apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono)

  3650   using H7 by blast

  3651   

  3652   

  3653   

  3654 lemma contains61a_2:

  3655   assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" 

  3656   shows "bsimp_AALTs bs rs >> bs2" 

  3657   using assms

  3658  apply(induct rs arbitrary: bs2 bs)

  3659    apply(auto)

  3660   apply (simp add: H1 TEMPLATE_contains61a)

  3661   by (metis append_Cons append_Nil contains50 f_cont2)

  3749   apply(drule contains59_2)

  3750   apply(auto)

  3751   apply(subst bder_bsimp_AALTs)

  3752   thm contains61a_2 contains61a

  3753   apply(rule contains61a_2)

  3754   apply(case_tac x2a)

  3755    apply(simp)

  3756   apply(simp)  

  3757   apply(auto)

  3758   

  3759   

  3760 (* HERE HERE *)

  3761 

  3762 (* old *)

  3763 (*