3506   

  3506 

  3507 

  3507 

  3508 lemma in2:

  3508 lemma [simp]:

  3509   assumes "bder c r >> bs2" and

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

  3510           "AALTs bsX rsX = bsimp r" and

  3510   by (induct r) (auto)

  3511           "XX \<in> set rsX" "nonnested (bsimp r)"

  3511 

  3512         shows "bder c (fuse bsX XX) >> bs2"

  3512 fun AALTs_subs where

  3513 

  3513   "AALTs_subs (AZERO) = {}"

  3514   sorry  

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

  3515 

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

  3516 

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

  3517 lemma

  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 

  3598 lemma H1:

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

  3600   shows "a >> bs2"

  3601   using assms

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

  3603         apply(auto)

  3604    apply (simp add: contains60)

  3605   by (simp add: contains59 contains60)

  3606 

  3607 lemma H3:

  3608   assumes "a >> bs"

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

  3610   using assms

  3611   apply(induct a bs)

  3612         apply(auto intro: contains.intros)

  3613   using contains.intros(4) contains59_2 by fastforce

  3614 

  3615 lemma H4:

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

  3617   apply(induct rs1)

  3618    apply(auto)

  3619   done

  3620 

  3621 lemma H5:

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

  3623   apply(induct rs1)

  3624    apply(auto)

  3625   done

  3626 

  3627 lemma H7:

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

  3629   apply(induct rs1)

  3630    apply(auto)

  3631   done

  3632 

  3633 lemma H10:

  3634   shows "AALTs_subs (AALTs bs rs) = (\<Union>r \<in> set rs. AALTs_subs (fuse bs r))"

  3635   apply(induct rs arbitrary: bs)

  3636    apply(auto)

  3637   done

  3638 

  3639 lemma H6:

  3640   shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"

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

  3642         apply(auto)

  3643   apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)

  3644   apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)

  3645   by (simp add: H7)

  3646 

  3647 (*

  3648 lemma H8:

  3649   assumes "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"

  3650   shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"

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

  3652         apply(auto)

  3653   apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)

  3654   apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)

  3655   by (simp add: H7)

  3656 *)

  3657 

  3658 lemma H2:

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

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

  3661   using assms

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

  3663         apply(auto)

  3664    apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono)

  3665   using H7 by blast

  3666   

  3667 lemma HH1:

  3668   assumes "r \<in> AALTs_subs (fuse bs a)" "r >> bs2"

  3669   shows "\<exists>bs3. bs2 = bs @ bs3"

  3670   using assms

  3671   using H1 f_cont1 by blast

  3672 

  3673 lemma fuse_inj:

  3674   assumes "fuse bs a = fuse bs b"

  3675   shows "a = b"

  3676   using assms

  3677   apply(induct a arbitrary: bs b)

  3678        apply(auto)

  3679        apply(case_tac b)

  3680             apply(auto)

  3681          apply(case_tac b)

  3682            apply(auto)

  3683        apply(case_tac b)

  3684           apply(auto)

  3685        apply(case_tac b)

  3686          apply(auto)

  3687        apply(case_tac b)

  3688         apply(auto)

  3689          apply(case_tac b)

  3690        apply(auto)

  3691   done

  3692 

  3693 lemma HH11:

  3694   assumes "r \<in> AALTs_subs (fuse bs1 a)"

  3695   shows "fuse bs r \<in> AALTs_subs (fuse (bs @ bs1) a)"

  3696   using assms

  3697   apply(induct a arbitrary: r bs bs1)

  3698        apply(auto)

  3699   apply(subst (asm) H10)

  3700   apply(auto)

  3701   apply(drule_tac x="x" in meta_spec)

  3702   apply(simp)

  3703   apply(drule_tac x="r" in meta_spec)

  3704   apply(drule_tac x="bs" in meta_spec)

  3705   apply(drule_tac x="bs1 @ x1" in meta_spec)

  3706   apply(simp)

  3707   apply(subst H10)

  3708   apply(auto)

  3709   done

  3710 

  3711 lemma HH12:

  3712   assumes "r \<in> AALTs_subs a"

  3713   shows "fuse bs r \<in> AALTs_subs (fuse bs a)"

  3714   using AALTs_subs_fuse assms by blast

  3715 

  3716 lemma HH13:

  3717   assumes "r \<in> (\<Union>r \<in> set rs. AALTs_subs r)"

  3718   shows "fuse bs r \<in> AALTs_subs (AALTs bs rs)"

  3719   using assms

  3720   using H10 HH12 by blast

  3721   

  3722 

  3723 lemma contains61a_2:

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

  3725   shows "bsimp_AALTs bs rs >> bs2" 

  3726   using assms

  3727  apply(induct rs arbitrary: bs2 bs)

  3728    apply(auto)

  3729   apply (simp add: H1 TEMPLATE_contains61a)

  3730   by (metis append_Cons append_Nil contains50 f_cont2)

  3731 

  3732 lemma HK1:

  3733   assumes "r \<in> AALTs_subs a"

  3734   shows "bsimp r \<in> AALTs_subs (bsimp a)"

  3735   using assms

  3736   apply(induct a arbitrary: r)

  3737        apply(auto)

  3738    apply(case_tac "a1 = AZERO")

  3739     apply(simp)

  3740   oops  

  3741 

  3742 lemma contains_equiv_def2:

  3743   shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)"

  3744   by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60)

  3745     

  3746 lemma contains_equiv_def:

  3747   shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"

  3748   by (meson contains0 contains49 contains59 contains60)

  3749 

  3750 lemma derc_alt00:

  3751   assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"

  3752   shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"

  3753   using assms

  3754   apply -

  3755   apply(case_tac "bsimp a")

  3756   prefer 6

  3757        apply(simp)+

  3758   apply(subst bder_bsimp_AALTs)

  3759   by (metis append_Nil contains51c map_bder_fuse map_map)

  3760 

  3761 lemma derc_alt01:

  3762   shows "\<And>a list1 list2.

  3763        \<lbrakk> bder c (bsimp a) >> bs ;

  3764         bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = [];

  3765         flts (map bsimp list2) \<noteq> []\<rbrakk>

  3766        \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs"

  3767   using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce

  3768 

  3769 lemma derc_alt10:

  3770   shows "\<And>a list1 list2.

  3771        \<lbrakk>  a \<in> set as; bder c (bsimp a) >> bs;

  3772         bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> [];

  3773 flts(map bsimp list2) = []\<rbrakk>

  3774        \<Longrightarrow> bder c (bsimp_AALTs []

  3775               (flts (map bsimp list1) @

  3776                flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs"

  3777   apply(subst bder_bsimp_AALTs)

  3778   apply simp

  3779   using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce

  3780 

  3781 

  3782 lemma derc_alt:

  3783   assumes "bder c (AALTs [] as) >> bs" 

  3784    and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"

  3785   shows "bder c (bsimp (AALTs [] as)) >> bs"

  3786   using assms

  3787   apply -

  3788   using contains_equiv_def

  3789   apply -

  3790   apply(simp)

  3791   apply(drule_tac  x="[]" in meta_spec)

  3792   apply(drule_tac x="map (bder c) as" in meta_spec)

  3793   apply(drule_tac x="bs" in meta_spec)

  3794   

  3795   apply(simp)

  3796   apply(erule bexE)

  3797   apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")

  3798    prefer 2

  3799   using split_list_last apply fastforce

  3800   apply(erule exE)+

  3801   apply(rule_tac t="as" and  s="list1@[a]@list2" in subst)

  3802    apply simp

  3803   (*find_theorems "map _ _ = _"*)

  3804   apply(subst map_append)+

  3805   apply(subst k00)+

  3806   apply(case_tac "flts (map bsimp list1) = Nil")

  3807   apply(case_tac "flts (map bsimp list2) = Nil")

  3808   apply simp

  3809   using derc_alt00 apply blast

  3810   apply simp

  3811   using derc_alt01 apply blast

  3812   apply(case_tac "flts (map bsimp list2) = Nil")

  3813   using derc_alt10 apply blast

  3814   by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append)

  3815 

  3816   

  3817 lemma derc_alt2:

  3818   assumes "bder c (AALTs bs2 as) >> bs2 @ bs" 

  3819    and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"

  3820  shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"

  3821 proof -

  3822   from assms

  3823   have "bder c (AALTs [] as) >> bs"

  3824     by (metis bder.simps(4) contains_equiv_def self_append_conv2)

  3825   then have "bder c (bsimp (AALTs [] as)) >> bs"

  3826     using assms(2) derc_alt by blast

  3827   then show "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"

  3828     by (metis bder_fuse bsimp_fuse_AALTs contains0) 

  3829 qed  

  3830 

  3831 lemma inA:

  3832   assumes "x \<in> set rs" "bder c (bsimp x) >> bs"

  3833   shows "\<exists>y. y \<in> set (flts (map bsimp rs))"

  3834   using assms

  3835   apply(induct rs arbitrary: x c bs)

  3836    apply(auto)

  3837    apply(case_tac "bsimp a = AZERO")

  3838   apply (metis append.left_neutral bder.simps(1) bsimp_AALTs.simps(1) contains61 in_set_conv_decomp neq_Nil_conv)

  3839   apply (metis bsimp_AALTs.simps(1) flts4 good1 list.set_intros(1) neq_Nil_conv)

  3840   by (metis Nil_is_append_conv k0 list.set_intros(1) neq_Nil_conv)

  3841 

  3842 

  3843 lemma inB:

  3844   assumes "a \<noteq> AZERO" "good a"

  3845   shows "AALTs_subs a \<noteq> {}"

  3846   using assms

  3847   apply(induct a)

  3848        apply(auto)

  3849   apply(erule good.elims)

  3850                       apply(auto)

  3851   by (metis empty_iff good.simps(1) good_fuse nn11a nonalt_10)

  3852 

  3853 lemma bder_simp_contains:

  3590   apply(drule contains59)

  3926   apply(subgoal_tac "\<exists>bsX. bs = x1 @ bsX")

  3927   prefer 2

  3928   using contains59 f_cont1 apply blast

  3592   apply(subst bder_bsimp_AALTs)

  3930   apply(rule derc_alt2[simplified])

  3593   apply(rule contains61a)

  3931    apply(simp)

  3594   apply(auto)

  3932   by blast

  3595   apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")

  3933   

  3596    prefer 2

  3597    apply simp

  3598   apply(case_tac "bsimp r = AZERO")

  3599   apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last)

  3600   apply(subgoal_tac "nonnested (bsimp r)")  

  3601    prefer 2

  3602   using nn1b apply blast

  3603   apply(case_tac "nonalt (bsimp r)")

  3604    apply(rule_tac x="bsimp r" in bexI)

  3605     apply (metis contains0 contains49 f_cont1)

  3606    apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b)

  3607   (* AALTS case *)

  3608   apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)")

  3609    prefer 2

  3610   apply (metis n0 nonalt.elims(3))

  3611   apply(auto)

  3612  apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")

  3613    prefer 2

  3614   apply (metis imageI list.set_map)

  3615   apply(simp)

  3616   apply(simp add: image_def)

  3617   apply(erule bexE)

  3618   apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)")

  3619    prefer 2

  3620   apply simp

  3621   apply(drule in1)

  3622   apply(subgoal_tac "rsX \<noteq> []")

  3623    prefer 2

  3624    apply (metis arexp.distinct(7) good.simps(4) good1)

  3625   by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))

  3626