diff -r 04391e303101 -r 8f9ea6453ba2 thys/BitCoded2.thy
--- 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"