# HG changeset patch # User Christian Urban # Date 1567775891 -3600 # Node ID 390e429c1676e73cee85dc9c87a0f04d3ce6413b # Parent f1feb44adfe142c6a152b4781957e1070ad55fdf updaed with AALTs_subs definition diff -r f1feb44adfe1 -r 390e429c1676 thys/BitCoded2.thy --- a/thys/BitCoded2.thy Thu Aug 22 09:40:48 2019 +0100 +++ b/thys/BitCoded2.thy Fri Sep 06 14:18:11 2019 +0100 @@ -3503,6 +3503,162 @@ 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 H00: + shows "((bder c) ` (AALTs_subs (AALTs bs rs))) = AALTs_subs (map (bder c) rs)" +*) + +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) + by (metis AALTs_subs_fuse2 H7 UnE fuse_map subset_iff) + + +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 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: @@ -3510,7 +3666,11 @@ "AALTs bsX rsX = bsimp r" and "XX \ set rsX" "nonnested (bsimp r)" shows "bder c (fuse bsX XX) >> bs2" - sorry + using assms + apply(induct r arbitrary: c bs2 bsX rsX XX) + apply(auto) + prefer 2 + oops lemma @@ -3586,6 +3746,21 @@ 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) @@ -3621,7 +3796,21 @@ apply(subgoal_tac "rsX \ []") prefer 2 apply (metis arexp.distinct(7) good.simps(4) good1) - by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1)) + 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) +*) + lemma CONTAINS1: assumes "a >> bs"