equal
deleted
inserted
replaced
3078 shows"b" |
3078 shows"b" |
3079 using assms |
3079 using assms |
3080 apply - |
3080 apply - |
3081 by auto |
3081 by auto |
3082 |
3082 |
3083 |
3083 lemma concat_def: |
|
3084 shows"[]@lst=lst" |
|
3085 |
3084 lemma derc_alt: |
3086 lemma derc_alt: |
3085 assumes "bder c (AALTs [] as) >> bs" |
3087 assumes "bder c (AALTs [] as) >> bs" |
3086 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3088 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3087 using assms |
3089 using assms |
3088 apply - |
3090 apply - |
3090 apply - |
3092 apply - |
3091 apply(simp add: bder.simps) |
3093 apply(simp add: bder.simps) |
3092 apply(drule_tac x="[]" in meta_spec) |
3094 apply(drule_tac x="[]" in meta_spec) |
3093 apply(drule_tac x="map (bder c) as" in meta_spec) |
3095 apply(drule_tac x="map (bder c) as" in meta_spec) |
3094 apply(drule_tac x="bs" in meta_spec) |
3096 apply(drule_tac x="bs" in meta_spec) |
3095 (*HERE*) |
3097 apply(simp add:List.append.simps(1)) |
3096 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3098 apply(rule_tac t="as" and s="list1@[a]@list2" in subst) |
|
3099 |
|
3100 (* (*HERE*) |
|
3101 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
|
3102 *) |
|
3103 |
3097 oops |
3104 oops |
3098 |
3105 |
3099 lemma transfer: |
3106 lemma transfer: |
3100 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3107 assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)" |
3101 shows "a \<Rightarrow> b" |
3108 shows "a \<Rightarrow> b" |