diff -r e29812ea4427 -r e4e507292bd8 thys/BitCoded2.thy --- a/thys/BitCoded2.thy Mon Sep 09 09:37:33 2019 +0100 +++ b/thys/BitCoded2.thy Thu Sep 12 18:06:01 2019 +0100 @@ -3503,166 +3503,6 @@ apply(induct r) apply(auto) by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2)) - - -lemma [simp]: - shows "size (fuse bs r) = size r" - by (induct r) (auto) - -fun AALTs_subs where - "AALTs_subs (AZERO) = {}" -| "AALTs_subs (AONE bs) = {AONE bs}" -| "AALTs_subs (ACHAR bs c) = {ACHAR bs c}" -| "AALTs_subs (ASEQ bs r1 r2) = {ASEQ bs r1 r2}" -| "AALTs_subs (ASTAR bs r) = {ASTAR bs r}" -| "AALTs_subs (AALTs bs []) = {}" -| "AALTs_subs (AALTs bs (r#rs)) = AALTs_subs (fuse bs r) \ AALTs_subs (AALTs bs rs)" - -lemma nonalt_10: - assumes "nonalt r" "r \ AZERO" - shows "r \ AALTs_subs r" - using assms - apply(induct r) - apply(auto) - done - -lemma flt_fuse: - shows "flts (map (fuse bs) rs) = map (fuse bs) (flts rs)" - apply(induct rs arbitrary: bs rule: flts.induct) - apply(auto) - by (simp add: fuse_append) - -lemma AALTs_subs_fuse: - shows "AALTs_subs (fuse bs r) = (fuse bs) ` (AALTs_subs r)" - apply(induct r arbitrary: bs rule: AALTs_subs.induct) - apply(auto) - apply (simp add: fuse_append) - apply blast - by (simp add: fuse_append) - -lemma AALTs_subs_fuse2: - shows "AALTs_subs (AALTs bs rs) = AALTs_subs (AALTs [] (map (fuse bs) rs))" - apply(induct rs arbitrary: bs) - apply(auto) - apply (auto simp add: fuse_empty) - done - -lemma fuse_map: - shows "map (fuse (bs1 @ bs2)) rs = map (fuse bs1) (map (fuse bs2) rs)" - apply(induct rs) - apply(auto) - using fuse_append by blast - - - -lemma contains59_2: - assumes "AALTs bs rs >> bs2" - shows "\r\AALTs_subs (AALTs bs rs). r >> bs2" - using assms - apply(induct rs arbitrary: bs bs2 taking: "\rs. sum_list (map asize rs)" rule: measure_induct) - apply(case_tac x) - apply(auto) - using contains59 apply force - apply(erule contains.cases) - apply(auto) - apply(case_tac "r = AZERO") - apply(simp) - apply (metis bsimp_AALTs.simps(1) contains61 empty_iff empty_set) - apply(case_tac "nonalt r") - apply (metis UnCI bsimp_AALTs.simps(1) contains0 contains61 empty_iff empty_set nn11a nonalt_10) - apply(subgoal_tac "\bsX rsX. r = AALTs bsX rsX") - prefer 2 - using bbbbs1 apply blast - apply(auto) - apply (metis UnCI contains0 fuse.simps(4) less_add_Suc1) - apply(drule_tac x="rs" in spec) - apply(drule mp) - apply(simp add: asize0) - apply(drule_tac x="bsa" in spec) - apply(drule_tac x="bsa @ bs1" in spec) - apply(auto) - done - -lemma TEMPLATE_contains61a: - assumes "\r \ set rs. (fuse bs r) >> bs2" - shows "bsimp_AALTs bs rs >> bs2" - using assms - apply(induct rs arbitrary: bs2 bs) - apply(auto) - apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1)) - by (metis append_Cons append_Nil contains50 f_cont2) - - - - -lemma H1: - assumes "r >> bs2" "r \ AALTs_subs a" - shows "a >> bs2" - using assms - apply(induct a arbitrary: r bs2 rule: AALTs_subs.induct) - apply(auto) - apply (simp add: contains60) - by (simp add: contains59 contains60) - -lemma H3: - assumes "a >> bs" - shows "\r \ AALTs_subs a. r >> bs" - using assms - apply(induct a bs) - apply(auto intro: contains.intros) - using contains.intros(4) contains59_2 by fastforce - -lemma H4: - shows "AALTs_subs (AALTs bs rs1) \ AALTs_subs (AALTs bs (rs1 @ rs2))" - apply(induct rs1) - apply(auto) - done - -lemma H5: - shows "AALTs_subs (AALTs bs rs2) \ AALTs_subs (AALTs bs (rs1 @ rs2))" - apply(induct rs1) - apply(auto) - done - -lemma H7: - shows "AALTs_subs (AALTs bs (rs1 @ rs2)) = AALTs_subs (AALTs bs rs1) \ AALTs_subs (AALTs bs rs2)" - apply(induct rs1) - apply(auto) - done - -lemma H6: - shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)" - apply(induct rs arbitrary: bs rule: flts.induct) - apply(auto) - apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map) - apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map) - by (simp add: H7) - - -lemma H2: - assumes "r >> bs2" "r \ AALTs_subs (AALTs bs rs)" - shows "r \ AALTs_subs (AALTs bs (flts rs))" - using assms - apply(induct rs arbitrary: r bs bs2 rule: flts.induct) - apply(auto) - apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono) - using H7 by blast - -lemma H00: - shows " (\ (AALTs_subs ` (set (map (bder c o fuse bs) rs)))) \ ((bder c) ` (AALTs_subs (AALTs bs rs)))" - apply(induct rs arbitrary: bs c) - apply(auto simp add: image_def) - - - -lemma contains61a_2: - assumes "\r\AALTs_subs (AALTs bs rs). r >> bs2" - shows "bsimp_AALTs bs rs >> bs2" - using assms - apply(induct rs arbitrary: bs2 bs) - apply(auto) - apply (simp add: H1 TEMPLATE_contains61a) - by (metis append_Cons append_Nil contains50 f_cont2) lemma in2: @@ -3670,11 +3510,8 @@ "AALTs bsX rsX = bsimp r" and "XX \ set rsX" "nonnested (bsimp r)" shows "bder c (fuse bsX XX) >> bs2" - using assms - apply(induct r arbitrary: c bs2 bsX rsX XX) - apply(auto) - prefer 2 - oops + + sorry lemma @@ -3750,22 +3587,6 @@ apply(erule contains.cases) apply(auto) (* ALT case *) - apply(drule contains59_2) - apply(auto) - apply(subst bder_bsimp_AALTs) - thm contains61a_2 contains61a - apply(rule contains61a_2) - apply(case_tac x2a) - apply(simp) - apply(simp) - apply(auto) - - - -(* HERE HERE *) - -(* old *) -(* apply(drule contains59) apply(auto) apply(subst bder_bsimp_AALTs) @@ -3801,21 +3622,7 @@ apply(subgoal_tac "rsX \ []") prefer 2 apply (metis arexp.distinct(7) good.simps(4) good1) - apply(subgoal_tac "\XX. XX \ set rsX") - prefer 2 - using neq_Nil_conv apply fastforce - apply(erule exE) - apply(rule_tac x="fuse bsX XX" in bexI) - prefer 2 - apply blast - apply(frule f_cont1) - apply(auto) - apply(rule contains0) - apply(drule contains49) - - by (simp add: in2) -*) - + by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1)) lemma CONTAINS1: assumes "a >> bs"