diff -r c470f792022b -r 76397aa190dc thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Jul 29 12:32:28 2019 +0100
+++ b/thys/BitCoded.thy	Mon Jul 29 14:27:17 2019 +0100
@@ -2620,13 +2620,135 @@
   apply(simp)
   oops
 
-lemma big:
+lemma YY:
+  assumes "flts (map bsimp as1) = xs"
+  shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs"
+  using assms
+  apply(induct as1 arbitrary: bs1 xs)
+   apply(simp)
+  apply(auto)
+  by (metis bsimp_fuse flts_fuse k0 list.simps(9))
+  
+
+
+lemma big0:
+  assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" 
+      and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'"
   shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
          bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
-  apply(simp add: comp_def bder_fuse)
-  apply(simp add: flts_append)
-   
-  sorry    
+  apply -
+  apply(subst CT1a)
+  apply(subst (2) bsimp.simps)
+  apply(subst (2) bsimp.simps)
+  apply(subst (2) bsimp_idem[symmetric])
+  apply(subst (2) bsimp.simps)
+  using as1p as2p
+  apply -
+  apply(erule exE)+
+  apply(simp del: bsimp.simps)
+  apply(simp only: flts_append)
+  apply(case_tac "flts (map bsimp as1)")
+   apply(subgoal_tac "flts (map bsimp as1') = []")
+    prefer 2
+  using YY apply auto[1]  
+    apply(simp only:)
+   apply(simp del: bsimp_AALTs.simps bsimp.simps)
+    apply(subst bsimp_AALTs.simps)
+    apply(case_tac "flts (map bsimp as2)")
+    apply(subgoal_tac "flts (map bsimp as2') = []")
+     prefer 2
+  using YY apply auto[1]
+    apply(simp)
+   apply(case_tac list)
+    apply(simp)
+    apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]")
+     prefer 2
+  using YY apply blast
+     apply(simp)
+  (* HERE TODAY *)
+  
+  
+  sorry
+(*  
+  
+  
+  using as1 apply auto[1]
+  apply(case_tac list)
+   apply(simp)
+  apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less)
+  apply(simp only:)  
+  apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)")
+   prefer 2
+  apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2)
+  apply(simp only:)
+  apply(simp only: bsimp_AALTs.simps)
+  apply(simp del: bsimp_AALTs.simps bsimp.simps)
+  apply(subst bsimp_AALTs.simps)
+   apply(case_tac "flts (map bsimp as2)")
+   apply(simp)
+  using as2 apply auto[1]
+   apply(case_tac listb)
+   apply(simp)
+  apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less)
+  apply(simp only:)
+  apply(simp only: bsimp_AALTs.simps)
+   apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)")  
+   prefer 2
+   apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2)
+  apply(simp only:)
+  apply(simp del: bsimp.simps)
+  by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9))
+*) 
+
+(*
+lemma big:
+  assumes as1: "(AALTs bs1 as1) = bsimp (AALTs bs1 as1)" 
+      and as2: "(AALTs bs2 as2) = bsimp (AALTs bs2 as2)"
+      and as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" 
+      and as2p: "\<exists>as2'. map (fuse bs2) as2 = as2'"
+  shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
+         bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
+  apply -
+  apply(subst as1)
+  apply(subst as2)
+  apply(subst (2) bsimp.simps)
+  apply(subst (2) bsimp.simps)
+  apply(subst (2) bsimp_idem[symmetric])
+  apply(subst (2) bsimp.simps)
+  using as1p as2p
+  apply -
+  apply(erule exE)+
+  apply(simp del: bsimp.simps)
+  apply(simp only: flts_append)
+  apply(case_tac "flts (map bsimp as1)")
+   apply(simp)
+  using as1 apply auto[1]
+  apply(case_tac list)
+   apply(simp)
+  apply (metis as1 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less)
+  apply(simp only:)  
+  apply(subgoal_tac "flts (map bsimp as1') = map (fuse bs1) (a # aa # lista)")
+   prefer 2
+  apply (metis CTa arexp.distinct(7) as1 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 good.simps(1) good1 k0a map_idI test2)
+  apply(simp only:)
+  apply(simp only: bsimp_AALTs.simps)
+  apply(simp del: bsimp_AALTs.simps bsimp.simps)
+  apply(subst bsimp_AALTs.simps)
+   apply(case_tac "flts (map bsimp as2)")
+   apply(simp)
+  using as2 apply auto[1]
+   apply(case_tac listb)
+   apply(simp)
+  apply (metis as2 bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs_size3 bsimp_size list.set_intros(1) n0 nn11a nn_flts nonalt.simps(1) not_less)
+  apply(simp only:)
+  apply(simp only: bsimp_AALTs.simps)
+   apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) (ab # ac # listc)")  
+   prefer 2
+   apply (metis arexp.distinct(7) as2 bsimp.simps(2) bsimp_AALTs.simps(3) flts2 flts_qq good1 k0a test2)
+  apply(simp only:)
+  apply(simp del: bsimp.simps)
+  by (smt append_Cons bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem k0 k0a list.simps(8) list.simps(9))
+*) 
 
 lemma XXX2a_long_without_good:
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
@@ -2659,10 +2781,13 @@
       apply(subst bsimp_AALTs_qq)
        prefer 2
        apply(simp del: bsimp.simps)
-       apply(subst big)
-       prefer 2
-  apply (metis (no_types, lifting) Nil_is_append_conv Nil_is_map_conv One_nat_def Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_0_conv length_append length_greater_0_conv less_Suc0 less_add_same_cancel1)
-      apply(simp add: comp_def bder_fuse)
+       apply(subst big0)
+           prefer 2
+           apply(blast)
+  prefer 2
+          apply(blast)  
+        prefer 2
+  
   
   oops