3086 done |
3086 done |
3087 |
3087 |
3088 lemma derc_alt00: |
3088 lemma derc_alt00: |
3089 assumes " bder c a >> bs" and "bder c (bsimp a) >> bs" |
3089 assumes " bder c a >> bs" and "bder c (bsimp a) >> bs" |
3090 shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs" |
3090 shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs" |
3091 oops |
3091 using assms |
3092 |
3092 apply - |
|
3093 apply(case_tac "bsimp a") |
|
3094 prefer 6 |
|
3095 apply(simp)+ |
|
3096 apply(subst bder_bsimp_AALTs) |
|
3097 by (metis append_Nil contains51c map_bder_fuse map_map) |
|
3098 lemma derc_alt01: |
|
3099 shows "\<And>a list1 list2. |
|
3100 \<lbrakk> bder c (bsimp a) >> bs ; |
|
3101 bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = []; |
|
3102 flts (map bsimp list2) \<noteq> []\<rbrakk> |
|
3103 \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs" |
|
3104 using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce |
|
3105 |
|
3106 lemma derc_alt10: |
|
3107 shows "\<And>a list1 list2. |
|
3108 \<lbrakk> a \<in> set as; bder c (bsimp a) >> bs; |
|
3109 bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> []; |
|
3110 flts(map bsimp list2) = []\<rbrakk> |
|
3111 \<Longrightarrow> bder c (bsimp_AALTs [] |
|
3112 (flts (map bsimp list1) @ |
|
3113 flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs" |
|
3114 apply(subst bder_bsimp_AALTs) |
|
3115 apply simp |
|
3116 using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce |
|
3117 |
|
3118 |
|
3119 (*QUESTION*) |
3093 lemma derc_alt: |
3120 lemma derc_alt: |
3094 assumes "bder c (AALTs [] as) >> bs" |
3121 assumes "bder c (AALTs [] as) >> bs" |
3095 (*QUESTION*) |
3122 and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))" |
3096 and "\<forall> a \<in> as. (bder c a >> bs) \<Rightarrow> (bder c (bsimp a) >> bs)" |
|
3097 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3123 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3098 using assms |
3124 using assms |
3099 apply - |
3125 apply - |
3100 using contains_equiv_def |
3126 using contains_equiv_def |
3101 apply - |
3127 apply - |
3116 apply(subst map_append)+ |
3142 apply(subst map_append)+ |
3117 apply(subst k00)+ |
3143 apply(subst k00)+ |
3118 apply(case_tac "flts (map bsimp list1) = Nil") |
3144 apply(case_tac "flts (map bsimp list1) = Nil") |
3119 apply(case_tac "flts (map bsimp list2) = Nil") |
3145 apply(case_tac "flts (map bsimp list2) = Nil") |
3120 apply simp |
3146 apply simp |
3121 |
3147 using derc_alt00 apply blast |
|
3148 apply simp |
|
3149 using derc_alt01 apply blast |
|
3150 apply(case_tac "flts (map bsimp list2) = Nil") |
|
3151 using derc_alt10 apply blast |
|
3152 by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append) |
3122 |
3153 |
3123 (*find_theorems "flts _ = _ "*) |
3154 (*find_theorems "flts _ = _ "*) |
3124 (* (*HERE*) |
3155 (* (*HERE*) |
3125 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3156 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3126 *) |
3157 *) |
3127 |
|
3128 oops |
|
3129 |
3158 |
3130 lemma transfer: |
3159 lemma transfer: |
3131 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3160 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3132 shows "a \<Rightarrow> b" |
3161 shows "a \<Rightarrow> b" |
3133 |
3162 |