# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1564432786 -3600
# Node ID f5ab2f02d148a6d0e05696f8f5b973e8e75175dd
# Parent  cc26b029a86630873d03a1f6cf710a56456ecfed
snapshot

diff -r cc26b029a866 -r f5ab2f02d148 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Jul 29 20:20:32 2019 +0100
+++ b/thys/BitCoded.thy	Mon Jul 29 21:39:46 2019 +0100
@@ -2656,14 +2656,26 @@
   apply(induct as1)
    apply(auto)
   using bder_fuse by blast
-  
+
+lemma WWW5:
+  shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)"
+  apply(induct as1)
+   apply(auto)
+  done
 
 lemma big0:
   shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
          bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
   by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append)
 
-
+lemma bignA:
+  shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) =
+         bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))"
+  apply(simp)
+  apply(subst k0)
+  apply(subst WWW3)
+  apply(simp add: flts_append)
+  done
 
 lemma XXX2a_long_without_good:
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
@@ -2675,7 +2687,15 @@
   prefer 3
     apply(simp)
   (* AALT case *)
-  prefer 2
+   prefer 2
+  apply(simp only:)
+  (* *)
+  apply(simp)
+   apply(subst WWW5)
+  
+
+
+
    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
     apply(clarify)
   apply(simp del: bsimp.simps)