equal
deleted
inserted
replaced
3080 apply - |
3080 apply - |
3081 by auto |
3081 by auto |
3082 |
3082 |
3083 lemma concat_def: |
3083 lemma concat_def: |
3084 shows"[]@lst=lst" |
3084 shows"[]@lst=lst" |
3085 |
3085 apply auto |
|
3086 done |
|
3087 |
3086 lemma derc_alt: |
3088 lemma derc_alt: |
3087 assumes "bder c (AALTs [] as) >> bs" |
3089 assumes "bder c (AALTs [] as) >> bs" |
3088 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3090 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3089 using assms |
3091 using assms |
3090 apply - |
3092 apply - |
3092 apply - |
3094 apply - |
3093 apply(simp add: bder.simps) |
3095 apply(simp add: bder.simps) |
3094 apply(drule_tac x="[]" in meta_spec) |
3096 apply(drule_tac x="[]" in meta_spec) |
3095 apply(drule_tac x="map (bder c) as" in meta_spec) |
3097 apply(drule_tac x="map (bder c) as" in meta_spec) |
3096 apply(drule_tac x="bs" in meta_spec) |
3098 apply(drule_tac x="bs" in meta_spec) |
|
3099 |
3097 apply(simp add:List.append.simps(1)) |
3100 apply(simp add:List.append.simps(1)) |
3098 apply(rule_tac t="as" and s="list1@[a]@list2" in subst) |
3101 apply(erule bexE) |
3099 |
3102 apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2") |
|
3103 prefer 2 |
|
3104 using split_list_last apply fastforce |
|
3105 apply(erule exE)+ |
|
3106 apply(rule_tac t="as" and s="list1@[a]@list2" in subst) |
|
3107 apply simp |
|
3108 (*find_theorems "map _ _ = _"*) |
|
3109 apply(subst map_append)+ |
|
3110 apply(subst k00)+ |
|
3111 apply(case_tac "flts (map bsimp list1) = Nil") |
|
3112 apply(case_tac "flts (map bsimp list2) = Nil") |
|
3113 apply simp |
|
3114 |
|
3115 |
|
3116 (*find_theorems "flts _ = _ "*) |
3100 (* (*HERE*) |
3117 (* (*HERE*) |
3101 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3118 apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name) |
3102 *) |
3119 *) |
3103 |
3120 |
3104 oops |
3121 oops |