diff -r f0e876ed43fa -r f139bdc0dcd5 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded.thy	Tue Aug 20 23:42:28 2019 +0200
@@ -567,6 +567,9 @@
 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 | "flts (r1 # rs) = r1 # flts rs"
 
+
+
+
 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
   where
   "li _ [] = AZERO"
@@ -574,6 +577,8 @@
 | "li bs as = AALTs bs as"
 
 
+
+
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -1083,6 +1088,8 @@
         apply(auto)
   done
 
+
+
 lemma rt:
   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
   apply(induct rs)
@@ -1783,6 +1790,56 @@
        apply(simp_all)
   done
 
+
+fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
+  where 
+  "flts2 _ [] = []"
+| "flts2 c (AZERO # rs) = flts2 c rs"
+| "flts2 c (AONE _ # rs) = flts2 c rs"
+| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
+| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
+| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 
+    flts2 c rs
+    else ASEQ bs r1 r2 # flts2 c rs)"
+| "flts2 c (r1 # rs) = r1 # flts2 c rs"
+
+lemma  flts2_k0:
+  shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
+  apply(induct r arbitrary: c rs1)
+   apply(auto)
+  done
+
+lemma  flts2_k00:
+  shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
+  apply(induct rs1 arbitrary: rs2 c)
+   apply(auto)
+  by (metis append.assoc flts2_k0)
+
+
+lemma
+  shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
+  apply(induct c rs rule: flts2.induct)
+        apply(simp)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  apply(simp)
+    apply(auto simp add: bder_fuse)[1]
+  defer
+   apply(simp)
+  apply(simp del: flts2.simps)
+  apply(rule conjI)
+   prefer 2
+   apply(auto)[1]
+  apply(rule impI)
+  apply(subst flts2_k0)
+  apply(subst map_append)
+  apply(subst flts2.simps)
+  apply(simp only: flts2.simps)
+  apply(auto)
+
+
+
 lemma XXX2_helper:
   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
           "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2390,130 +2447,13 @@
     apply(auto)
   done
 
-lemma
-  assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
-   "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))" 
-          "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
-   shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
-  using assms
-  apply(induct x52 arbitrary: x51)
-   apply(simp)
-  oops
-  
-
-lemma
-  assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
-  shows "bsimp a = a"
-  using assms
-  apply(induct a taking: asize rule: measure_induct)
-  apply(case_tac x)
-       apply(simp_all)
-   apply(case_tac "(bsimp x42) = AZERO")
-    apply(simp add: asize0)
-  apply(case_tac "(bsimp x43) = AZERO")
-    apply(simp add: asize0)
-    apply (metis bsimp_ASEQ0)
-   apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
-    apply(auto)[1]
-    apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
-  apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
-  (* ALT case *)
-  apply(frule iii)
-  apply(case_tac x52)
-   apply(simp)
-  apply(simp)
-  apply(subst k0)
-  apply(subst (asm) k0)
-  apply(subst (asm) (2) k0)
-  apply(subst (asm) (3) k0)
-  apply(case_tac "(bsimp a) = AZERO")
-   apply(simp)
-  apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
-  apply(simp)
-  apply(case_tac "nonalt  (bsimp a)")
-   prefer 2
-  apply(drule_tac  x="AALTs x51 (bsimp a # list)" in  spec)
-   apply(drule mp)
-  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
-   apply(drule mp)  
-    apply(simp)
-  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
-   apply(drule mp)
-  apply(simp)
-  using bsimp_idem apply auto[1]
-    apply(simp add: bsimp_idem)
-  apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
-  apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
-  apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
-  prefer 2
-  using k0b apply blast
-  apply(clarify)
-  apply(simp only:)
-  apply(simp)
-  apply(case_tac "flts (map bsimp list) = Nil")
-   apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less) 
-  apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) =  AALTs x51 (bsimp a # flts (map bsimp list))")
-   prefer 2
-   apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
-  apply(auto)
-   apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
-  oops
-
-
-
-
-lemma OOO:
-  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
-  apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
-  apply(case_tac x)
-   apply(simp)
-  apply(simp)
-  apply(case_tac "a = AZERO")
-   apply(simp)
-  apply(case_tac "list")
-    apply(simp)
-  apply(simp)
-  apply(case_tac "bsimp a = AZERO")
-   apply(simp)
-  apply(case_tac "list")
-    apply(simp)
-    apply(simp add: bsimp_fuse[symmetric])
-  apply(simp)
-  apply(case_tac "nonalt (bsimp a)")
-  apply(case_tac list)
-  apply(simp)
-    apply(subst k0b)
-      apply(simp)
-     apply(simp)
-    apply(simp add: bsimp_fuse)
-   apply(simp)
-  apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
-   prefer 2
-  using bsimp_size le_neq_implies_less apply blast
-   apply(erule disjE)
-  apply(drule_tac x="(bsimp a) # list" in spec)
-  apply(drule mp)
-    apply(simp)
-   apply(simp)
-  apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
-    apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs  \<and> rs \<noteq> Nil \<and> length rs > 1")
-   prefer 2
-  apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
-  apply(auto)
-  oops
-
-
-lemma  
-  assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
-  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
-  using assms
-  apply(simp)
-  oops
-
-
+lemma CT1_SEQ:
+  shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
+  apply(simp add: bsimp_idem)
+  done
 
 lemma CT1:
-  shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map  bsimp as))"
+  shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map  bsimp as))"
   apply(induct as arbitrary: bs)
    apply(simp)
   apply(simp)
@@ -2523,6 +2463,21 @@
   shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
   by (metis CT1 list.simps(8) list.simps(9))
 
+lemma WWW2:
+  shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
+         bsimp_AALTs bs1 (flts (map bsimp as1))"
+  by (metis bsimp.simps(2) bsimp_idem)
+
+lemma CT1b:
+  shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
+  apply(induct bs as rule: bsimp_AALTs.induct)
+    apply(auto simp add: bsimp_idem)
+  apply (simp add: bsimp_fuse bsimp_idem)
+  by (metis bsimp_idem comp_apply)
+  
+  
+
+
 (* CT *)
 
 lemma CTU:
@@ -2531,7 +2486,7 @@
     apply(auto)
   done
 
-
+find_theorems "bder _ (bsimp_AALTs _ _)"
 
 lemma CTa:
   assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
@@ -2574,15 +2529,6 @@
   
 
 
-
-lemma 
-  shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
-          = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
-                             (map (fuse bs2) (map (bder c) as2))))"
-  apply(subst  bsimp_idem[symmetric])
-  apply(simp)
-  oops
-
 lemma CT_exp:
   assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
   shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
@@ -2641,10 +2587,6 @@
   using flts2 good1 apply fastforce
   by (smt ex_map_conv list.simps(9) nn1b nn1c)
 
-lemma WWW2:
-  shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
-         bsimp_AALTs bs1 (flts (map bsimp as1))"
-  by (metis bsimp.simps(2) bsimp_idem)
 
 lemma WWW3:
   shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
@@ -3019,12 +2961,17 @@
      apply(simp)
     prefer 3
     apply(simp)
+  (* SEQ case *)
+   apply(simp only:)
+   apply(subst CT1_SEQ)
+  apply(simp only: bsimp.simps)
+
   (* AALT case *)
    prefer 2
    apply(simp only:)
    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
     apply(clarify)
-  apply(simp del: bsimp.simps)
+    apply(simp del: bsimp.simps)
   apply(subst (2) CT1) 
     apply(simp del: bsimp.simps)
   apply(rule_tac t="bsimp (bder c a1)" and  s="bsimp (bder c (bsimp a1))" in subst)
@@ -3032,6 +2979,21 @@
   apply(rule_tac t="bsimp (bder c a2)" and  s="bsimp (bder c (bsimp a2))" in subst)
      apply(simp del: bsimp.simps)
     apply(subst  CT1a[symmetric])
+  (* \<rightarrow> *)
+  apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
+            and  s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
+     apply(simp)
+     apply(subst bsimp.simps)
+    apply(simp del: bsimp.simps bder.simps)
+
+    apply(subst bder_bsimp_AALTs)
+    apply(subst bsimp.simps)
+    apply(subst WWW2[symmetric])
+    apply(subst bsimp_AALTs_qq)
+  defer 
+    apply(subst bsimp.simps)
+    
+  (* <- *)
     apply(subst bsimp.simps)
     apply(simp del: bsimp.simps)
 (*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
@@ -3046,7 +3008,7 @@
        apply(simp del: bsimp.simps)
        apply(subst big0)
        apply(simp add: WWW4)
-  apply (metis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
+  apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
   oops
 
 lemma XXX2a_long_without_good: