equal
deleted
inserted
replaced
3071 |
3071 |
3072 lemma contains_equiv_def: |
3072 lemma contains_equiv_def: |
3073 shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)" |
3073 shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)" |
3074 by (meson contains0 contains49 contains59 contains60) |
3074 by (meson contains0 contains49 contains59 contains60) |
3075 |
3075 |
|
3076 lemma i_know_it_must_be_a_theorem_but_dunno_its_name: |
|
3077 assumes "a \<and> (a=b) " |
|
3078 shows"b" |
|
3079 using assms |
|
3080 apply - |
|
3081 by auto |
|
3082 |
|
3083 |
3076 lemma derc_alt: |
3084 lemma derc_alt: |
3077 assumes "bder c (AALTs [] as) >> bs" |
3085 assumes "bder c (AALTs [] as) >> bs" |
3078 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3086 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3079 using assms |
3087 using assms |
3080 apply - |
3088 apply - |
3081 using contains_equiv_def |
3089 using contains_equiv_def |
3082 apply - |
3090 apply - |
|
3091 apply(simp add: bder.simps) |
3083 apply(drule_tac x="[]" in meta_spec) |
3092 apply(drule_tac x="[]" in meta_spec) |
3084 apply(drule_tac x="as" in meta_spec) |
3093 apply(drule_tac x="map (bder c) as" in meta_spec) |
3085 apply(drule_tac x="bs" in meta_spec) |
3094 apply(drule_tac x="bs" in meta_spec) |
3086 |
3095 (*HERE*) |
|
3096 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3087 oops |
3097 oops |
3088 |
3098 |
3089 lemma transfer: |
3099 lemma transfer: |
3090 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3100 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3091 shows "a \<Rightarrow> b" |
3101 shows "a \<Rightarrow> b" |