--- a/thys/BitCoded2.thy Fri Sep 13 17:46:44 2019 +0100
+++ b/thys/BitCoded2.thy Sat Sep 14 13:25:56 2019 +0100
@@ -3503,18 +3503,354 @@
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) \<union> AALTs_subs (AALTs bs rs)"
+
+lemma nonalt_10:
+ assumes "nonalt r" "r \<noteq> AZERO"
+ shows "r \<in> 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 in2:
- assumes "bder c r >> bs2" and
- "AALTs bsX rsX = bsimp r" and
- "XX \<in> set rsX" "nonnested (bsimp r)"
- shows "bder c (fuse bsX XX) >> bs2"
-
- sorry
-
-
-lemma
+
+lemma contains59_2:
+ assumes "AALTs bs rs >> bs2"
+ shows "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2"
+ using assms
+ apply(induct rs arbitrary: bs bs2 taking: "\<lambda>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 "\<exists>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 "\<exists>r \<in> 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 \<in> 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 "\<exists>r \<in> 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) \<subseteq> AALTs_subs (AALTs bs (rs1 @ rs2))"
+ apply(induct rs1)
+ apply(auto)
+ done
+
+lemma H5:
+ shows "AALTs_subs (AALTs bs rs2) \<subseteq> 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) \<union> AALTs_subs (AALTs bs rs2)"
+ apply(induct rs1)
+ apply(auto)
+ done
+
+lemma H10:
+ shows "AALTs_subs (AALTs bs rs) = (\<Union>r \<in> set rs. AALTs_subs (fuse bs r))"
+ apply(induct rs arbitrary: bs)
+ 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 H8:
+ assumes "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
+ 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 \<in> AALTs_subs (AALTs bs rs)"
+ shows "r \<in> 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 HH1:
+ assumes "r \<in> AALTs_subs (fuse bs a)" "r >> bs2"
+ shows "\<exists>bs3. bs2 = bs @ bs3"
+ using assms
+ using H1 f_cont1 by blast
+
+lemma fuse_inj:
+ assumes "fuse bs a = fuse bs b"
+ shows "a = b"
+ using assms
+ apply(induct a arbitrary: bs b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ apply(case_tac b)
+ apply(auto)
+ done
+
+lemma HH11:
+ assumes "r \<in> AALTs_subs (fuse bs1 a)"
+ shows "fuse bs r \<in> AALTs_subs (fuse (bs @ bs1) a)"
+ using assms
+ apply(induct a arbitrary: r bs bs1)
+ apply(auto)
+ apply(subst (asm) H10)
+ apply(auto)
+ apply(drule_tac x="x" in meta_spec)
+ apply(simp)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule_tac x="bs1 @ x1" in meta_spec)
+ apply(simp)
+ apply(subst H10)
+ apply(auto)
+ done
+
+lemma HH12:
+ assumes "r \<in> AALTs_subs a"
+ shows "fuse bs r \<in> AALTs_subs (fuse bs a)"
+ using AALTs_subs_fuse assms by blast
+
+lemma HH13:
+ assumes "r \<in> (\<Union>r \<in> set rs. AALTs_subs r)"
+ shows "fuse bs r \<in> AALTs_subs (AALTs bs rs)"
+ using assms
+ using H10 HH12 by blast
+
+
+lemma contains61a_2:
+ assumes "\<exists>r\<in>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 HK1:
+ assumes "r \<in> AALTs_subs a"
+ shows "bsimp r \<in> AALTs_subs (bsimp a)"
+ using assms
+ apply(induct a arbitrary: r)
+ apply(auto)
+ apply(case_tac "a1 = AZERO")
+ apply(simp)
+ oops
+
+lemma contains_equiv_def2:
+ shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)"
+ by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60)
+
+lemma contains_equiv_def:
+ shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
+ by (meson contains0 contains49 contains59 contains60)
+
+lemma derc_alt00:
+ assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
+ shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
+ using assms
+ apply -
+ apply(case_tac "bsimp a")
+ prefer 6
+ apply(simp)+
+ apply(subst bder_bsimp_AALTs)
+ by (metis append_Nil contains51c map_bder_fuse map_map)
+
+lemma derc_alt01:
+ shows "\<And>a list1 list2.
+ \<lbrakk> bder c (bsimp a) >> bs ;
+ bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = [];
+ flts (map bsimp list2) \<noteq> []\<rbrakk>
+ \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs"
+ using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce
+
+lemma derc_alt10:
+ shows "\<And>a list1 list2.
+ \<lbrakk> a \<in> set as; bder c (bsimp a) >> bs;
+ bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> [];
+flts(map bsimp list2) = []\<rbrakk>
+ \<Longrightarrow> bder c (bsimp_AALTs []
+ (flts (map bsimp list1) @
+ flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs"
+ apply(subst bder_bsimp_AALTs)
+ apply simp
+ using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce
+
+
+lemma derc_alt:
+ assumes "bder c (AALTs [] as) >> bs"
+ and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
+ shows "bder c (bsimp (AALTs [] as)) >> bs"
+ using assms
+ apply -
+ using contains_equiv_def
+ apply -
+ apply(simp)
+ apply(drule_tac x="[]" in meta_spec)
+ apply(drule_tac x="map (bder c) as" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+
+ apply(simp)
+ apply(erule bexE)
+ apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
+ prefer 2
+ using split_list_last apply fastforce
+ apply(erule exE)+
+ apply(rule_tac t="as" and s="list1@[a]@list2" in subst)
+ apply simp
+ (*find_theorems "map _ _ = _"*)
+ apply(subst map_append)+
+ apply(subst k00)+
+ apply(case_tac "flts (map bsimp list1) = Nil")
+ apply(case_tac "flts (map bsimp list2) = Nil")
+ apply simp
+ using derc_alt00 apply blast
+ apply simp
+ using derc_alt01 apply blast
+ apply(case_tac "flts (map bsimp list2) = Nil")
+ using derc_alt10 apply blast
+ by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append)
+
+
+lemma derc_alt2:
+ assumes "bder c (AALTs bs2 as) >> bs2 @ bs"
+ and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
+ shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
+proof -
+ from assms
+ have "bder c (AALTs [] as) >> bs"
+ by (metis bder.simps(4) contains_equiv_def self_append_conv2)
+ then have "bder c (bsimp (AALTs [] as)) >> bs"
+ using assms(2) derc_alt by blast
+ then show "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
+ by (metis bder_fuse bsimp_fuse_AALTs contains0)
+qed
+
+lemma inA:
+ assumes "x \<in> set rs" "bder c (bsimp x) >> bs"
+ shows "\<exists>y. y \<in> set (flts (map bsimp rs))"
+ using assms
+ apply(induct rs arbitrary: x c bs)
+ apply(auto)
+ apply(case_tac "bsimp a = AZERO")
+ apply (metis append.left_neutral bder.simps(1) bsimp_AALTs.simps(1) contains61 in_set_conv_decomp neq_Nil_conv)
+ apply (metis bsimp_AALTs.simps(1) flts4 good1 list.set_intros(1) neq_Nil_conv)
+ by (metis Nil_is_append_conv k0 list.set_intros(1) neq_Nil_conv)
+
+
+lemma inB:
+ assumes "a \<noteq> AZERO" "good a"
+ shows "AALTs_subs a \<noteq> {}"
+ using assms
+ apply(induct a)
+ apply(auto)
+ apply(erule good.elims)
+ apply(auto)
+ by (metis empty_iff good.simps(1) good_fuse nn11a nonalt_10)
+
+lemma bder_simp_contains:
assumes "bder c a >> bs"
shows "bder c (bsimp a) >> bs"
using assms
@@ -3587,43 +3923,14 @@
apply(erule contains.cases)
apply(auto)
(* ALT case *)
- apply(drule contains59)
- apply(auto)
- apply(subst bder_bsimp_AALTs)
- apply(rule contains61a)
+ apply(subgoal_tac "\<exists>bsX. bs = x1 @ bsX")
+ prefer 2
+ using contains59 f_cont1 apply blast
apply(auto)
- apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
- prefer 2
- apply simp
- apply(case_tac "bsimp r = AZERO")
- apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last)
- apply(subgoal_tac "nonnested (bsimp r)")
- prefer 2
- using nn1b apply blast
- apply(case_tac "nonalt (bsimp r)")
- apply(rule_tac x="bsimp r" in bexI)
- apply (metis contains0 contains49 f_cont1)
- apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b)
- (* AALTS case *)
- apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)")
- prefer 2
- apply (metis n0 nonalt.elims(3))
- apply(auto)
- apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
- prefer 2
- apply (metis imageI list.set_map)
- apply(simp)
- apply(simp add: image_def)
- apply(erule bexE)
- apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)")
- prefer 2
- apply simp
- apply(drule in1)
- apply(subgoal_tac "rsX \<noteq> []")
- 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(rule derc_alt2[simplified])
+ apply(simp)
+ by blast
+
lemma CONTAINS1:
assumes "a >> bs"
shows "a >>2 bs"