--- 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) \<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 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 H00:
+  shows "((bder c) ` (AALTs_subs (AALTs bs rs))) =  AALTs_subs (map (bder c) rs)"
+*)
+
+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 H6:
+  shows "AALTs_subs (AALTs bs (flts rs)) \<subseteq> 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 \<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 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 in2:
@@ -3510,7 +3666,11 @@
           "AALTs bsX rsX = bsimp r" and
           "XX \<in> 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 \<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(subgoal_tac "\<exists>XX. XX \<in> 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"