diff -r 0eaa1851a5b6 -r db0ff630bbb7 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Sat Mar 16 11:15:22 2019 +0000
+++ b/thys/BitCoded.thy	Thu Apr 11 17:37:00 2019 +0100
@@ -98,6 +98,15 @@
 abbreviation
   "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
 
+fun asize :: "arexp \<Rightarrow> nat" where
+  "asize AZERO = 1"
+| "asize (AONE cs) = 1" 
+| "asize (ACHAR cs c) = 1"
+| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
+| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
+| "asize (ASTAR cs r) = Suc (asize r)"
+
+
 
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
@@ -472,17 +481,6 @@
 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 | "flts (r1 # rs) = r1 # flts rs"
 
-(*
-lemma flts_map:
-  assumes "\<forall>r \<in> set rs. f r = r"
-  shows "map f (flts rs) = flts (map f rs)"
-  using assms
-  apply(induct rs rule: flts.induct)
-        apply(simp_all)
-       apply(case_tac rs)
-  apply(simp)
-*)
-
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -515,6 +513,13 @@
                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
 
+lemma asize0:
+  shows "0 < asize r"
+  apply(induct  r)
+       apply(auto)
+  done
+
+
 lemma bders_simp_append:
   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
   apply(induct s1 arbitrary: r s2)
@@ -522,7 +527,78 @@
   apply(simp)
   done
 
+lemma bsimp_ASEQ_size:
+  shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
+  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
 
+lemma fuse_size:
+  shows "asize (fuse bs r) = asize r"
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma flts_size:
+  shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
+  apply(induct rs rule: flts.induct)
+        apply(simp_all)
+  by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong)
+  
+
+lemma bsimp_AALTs_size:
+  shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
+  apply(induct rs rule: bsimp_AALTs.induct)
+  apply(auto simp add: fuse_size)
+  done
+  
+lemma bsimp_size:
+  shows "asize (bsimp r) \<le> asize r"
+  apply(induct r)
+       apply(simp_all)
+   apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
+  apply(rule le_trans)
+   apply(rule bsimp_AALTs_size)
+  apply(simp)
+   apply(rule le_trans)
+   apply(rule flts_size)
+  by (simp add: sum_list_mono)
+
+fun nonalt :: "arexp \<Rightarrow> bool"
+  where
+  "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+
+
+lemma bsimp_AALTs_size2:
+  assumes "\<forall>r \<in> set  rs. nonalt r"
+  shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
+  using assms
+  apply(induct rs rule: bsimp_AALTs.induct)
+    apply(simp_all add: fuse_size)
+  done
+
+lemma qq:
+  shows "map (asize \<circ> fuse bs) rs = map asize rs"
+  apply(induct rs)
+   apply(auto simp add: fuse_size)
+  done
+
+lemma flts_size2:
+  assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"
+  shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
+  using assms
+  apply(induct rs)
+   apply(auto simp add: qq)
+   apply (simp add: flts_size less_Suc_eq_le)
+  apply(case_tac a)
+       apply(auto simp add: qq)
+   prefer 2
+   apply (simp add: flts_size le_imp_less_Suc)
+  using less_Suc_eq by auto
+  
 lemma L_bsimp_ASEQ:
   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -575,6 +651,13 @@
    apply (simp add: L_erase_AALTs)
   using L_erase_AALTs by blast
 
+lemma bsimp_ASEQ0:
+  shows "bsimp_ASEQ bs r1 AZERO = AZERO"
+  apply(induct r1)
+  apply(auto)
+  done
+
+
 
 lemma bsimp_ASEQ1:
   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
@@ -620,7 +703,6 @@
 lemma b4:
   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
-  
 
 lemma q1:
   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
@@ -667,6 +749,427 @@
   apply(simp)
   done
 
+lemma fuse_empty:
+  shows "fuse [] r = r"
+  apply(induct r)
+       apply(auto)
+  done
+
+lemma flts_fuse:
+  shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(auto simp add: fuse_append)
+  done
+
+lemma bsimp_ASEQ_fuse:
+  shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
+  apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
+
+lemma bsimp_AALTs_fuse:
+  assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+  shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+  using assms
+  apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+  apply(auto)
+  done
+
+
+
+lemma bsimp_fuse:
+  shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+apply(induct r arbitrary: bs)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   apply(simp)
+   apply (simp add: bsimp_ASEQ_fuse)
+  apply(simp)
+  by (simp add: bsimp_AALTs_fuse fuse_append)
+
+lemma bsimp_fuse_AALTs:
+  shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
+  apply(subst bsimp_fuse) 
+  apply(simp)
+  done
+
+lemma bsimp_fuse_AALTs2:
+  shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
+  using bsimp_AALTs_fuse fuse_append by auto
+  
+
+lemma bsimp_ASEQ_idem:
+  assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+  shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+  using assms
+  apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+    apply(simp)
+  apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))  
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+   apply(subst bsimp_ASEQ2)
+  apply (metis assms(2) bsimp_fuse)
+      apply(subst bsimp_ASEQ1)
+      apply(auto)
+  done
+
+
+fun nonnested :: "arexp \<Rightarrow> bool"
+  where
+  "nonnested (AALTs bs2 []) = True"
+| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
+| "nonnested r = True"
+
+
+lemma  k0:
+  shows "flts (r # rs1) = flts [r] @ flts rs1"
+  apply(induct r arbitrary: rs1)
+   apply(auto)
+  done
+
+lemma  k00:
+  shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
+  apply(induct rs1 arbitrary: rs2)
+   apply(auto)
+  by (metis append.assoc k0)
+
+lemma  k0a:
+  shows "flts [AALTs bs rs] = map (fuse bs)  rs"
+  apply(simp)
+  done
+
+fun spill where
+ "spill (AALTs bs rs) =  map (fuse bs) rs"
+
+lemma  k0a2:
+  assumes "\<not> nonalt r"  
+  shows "flts [r] = spill r"
+  using  assms
+  apply(case_tac r)
+  apply(simp_all)
+  done
+
+lemma  k0b:
+  assumes "nonalt r" "r \<noteq> AZERO"
+  shows "flts [r] = [r]"
+  using assms
+  apply(case_tac  r)
+  apply(simp_all)
+  done
+
+lemma nn1:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn1q:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn1qq:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
+  using assms
+  apply(induct rs rule: flts.induct)
+  apply(auto)
+  done
+
+lemma nn10:
+  assumes "nonnested (AALTs cs rs)" 
+  shows "nonnested (AALTs (bs @ cs) rs)"
+  using assms
+  apply(induct rs arbitrary: cs bs)
+   apply(simp_all)
+  apply(case_tac a)
+       apply(simp_all)
+  done
+
+lemma nn11a:
+  assumes "nonalt r"
+  shows "nonalt (fuse bs r)"
+  using assms
+  apply(induct r)
+       apply(auto)
+  done
+
+
+lemma nn1a:
+  assumes "nonnested r"
+  shows "nonnested (fuse bs r)"
+  using assms
+  apply(induct bs r arbitrary: rule: fuse.induct)
+       apply(simp_all add: nn10)
+  done  
+
+lemma n0:
+  shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+  apply(induct rs  arbitrary: bs)
+   apply(auto)
+    apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+   apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
+  by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+
+  
+  
+
+lemma nn1c:
+  assumes "\<forall>r \<in> set rs. nonnested r"
+  shows "\<forall>r \<in> set (flts rs). nonalt r"
+  using assms
+  apply(induct rs rule: flts.induct)
+        apply(auto)
+  apply(rule nn11a)
+  by (metis nn1qq nonalt.elims(3))
+
+lemma nn1bb:
+  assumes "\<forall>r \<in> set rs. nonalt r"
+  shows "nonnested (bsimp_AALTs bs rs)"
+  using assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply(auto)
+   apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
+  using n0 by auto
+    
+lemma nn1b:
+  shows "nonnested (bsimp r)"
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+   apply(simp)
+    apply(subst bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+  apply (simp add: nn1a)    
+   apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(rule nn1bb)
+  apply(auto)
+  by (metis (mono_tags, hide_lams) imageE nn1c set_map)
+
+lemma rt:
+  shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst  k0)
+  apply(simp)
+  by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
+
+lemma flts_idem:
+  assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+  shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0) 
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+  thm k0 k0a k0b
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(subst k0)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  apply(simp)
+  apply(simp add: k00)
+  apply(subst k0a2)
+   apply(simp)
+  apply(subst k0a2)
+   apply(simp)
+  apply(case_tac a)
+  apply(simp_all)
+  sorry
+
+lemma bsimp_AALTs_idem:
+  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
+  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
+  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 "\<exists>bs'  rs'. a = AALTs bs' rs'")
+   apply(clarify)
+  apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+
+  apply(drule_tac x="flts (rs' @ list)" in spec)
+  apply(erule impE)
+  prefer 2
+  apply(case_tac a)
+       apply(simp)
+       apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+   apply(case_tac list)
+        apply(simp)
+      apply(simp) 
+   apply(case_tac list)
+        apply(simp)
+     apply(simp) 
+  prefer 3
+   apply(case_tac list)
+        apply(simp)
+       apply(simp) 
+   apply(case_tac list)
+    apply(simp)
+      
+
+       apply(simp) 
+
+      apply(case_tac "flts (map bsimp list)")
+       apply(simp)
+      apply(simp)
+  
+  
+
+   prefer 2
+   apply(simp)
+  
+   apply(subst k0)
+   apply(subst (2) k0)
+  
+  apply(case_tac a)
+       apply(simp_all)
+  
+  prefer 2
+   apply(simp)
+  apply(case_tac r)
+       apply(auto)
+   apply(case_tac "bsimp x42 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp x43 = AZERO")
+   apply(simp)
+   apply(subst bsimp_ASEQ0)
+   apply(subst bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+    apply(auto)[1]
+    apply(subst bsimp_ASEQ2)
+   apply(subst bsimp_ASEQ2)
+  prefer 2
+      apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(subst bsimp_ASEQ1)
+      apply(auto)
+  apply(subst (asm) bsimp_ASEQ2)
+   apply(subst (asm) bsimp_ASEQ2)
+  using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
+    
+   apply(case_tac x43)
+        apply(simp_all)
+    prefer 3
+  oops
+
+lemma bsimp_idem:
+  shows "bsimp (bsimp r) = bsimp r"
+apply(induct r taking: "asize" rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   apply(simp)
+   apply (simp add: bsimp_ASEQ_idem)
+  apply(clarify)
+  apply(case_tac x52)
+  apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0)
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+   apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec)
+   apply(drule mp)
+    apply(simp)
+  apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2)
+  apply(simp)
+    apply(subst (asm) flts_idem)
+     apply(auto)[1]
+     apply(drule_tac  x="r" in spec)
+  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
+  apply(simp)
+  apply(subst flts_idem)
+   apply(auto)[1]
+     apply(drule_tac  x="r" in spec)
+  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
+   apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+   apply(auto)[1]
+  apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec)
+   apply(drule mp)
+    apply(simp)
+    prefer 2
+    apply(simp)
+  apply(subst (asm) k0)
+  apply(subst (asm) flts_idem)
+     apply(auto)[1]
+  apply (simp add: sum_list_map_remove1)
+  apply(subst (asm) k0b)
+     apply(simp)
+    apply(simp)
+    apply(simp)
+   apply(subst k0)
+  apply(subst flts_idem)
+     apply(auto)[1]
+     apply (simp add: sum_list_map_remove1)
+  apply(subst k0b)
+     apply(simp)
+    apply(simp)
+  apply(simp)
+lemma XX_bder:
+  shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r"
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+  prefer 2
+   apply(simp)
+   apply(case_tac x2a)
+    apply(simp)
+  apply(simp)
+  apply(auto)[1]
+
+
 lemma q3a:
   assumes "\<exists>r \<in> set rs. bnullable r"
   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
@@ -758,11 +1261,7 @@
   apply(simp)
   using qq4 r1 r2 by auto
 
-lemma  k0:
-  shows "flts (r # rs1) = flts [r] @ flts rs1"
-  apply(induct r arbitrary: rs1)
-   apply(auto)
-  done
+
 
 lemma k1:
   assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
@@ -836,6 +1335,16 @@
   done
 
 
+fun extr :: "arexp  \<Rightarrow> (bit list) set" where
+  "extr (AONE bs) = {bs}"
+| "extr (ACHAR bs c) = {bs}"
+| "extr (AALTs bs (r#rs)) = 
+     {bs @ bs' | bs'.  bs' \<in> extr r} \<union>
+     {bs @ bs' | bs'.  bs' \<in> extr (AALTs [] rs)}"
+| "extr (ASEQ bs r1 r2) = 
+     {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}"
+| "extr (ASTAR bs r) = {bs @ [S]} \<union>
+     {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR  [] r)}"
 
 
 lemma MAIN_decode:
@@ -959,7 +1468,16 @@
      apply(simp)
      apply(subst bsimp_ASEQ2)
      apply(subst bsimp_ASEQ2)
-  apply(simp add: erase_fuse)
+     apply(simp add: erase_fuse)
+     apply(case_tac r1)
+          apply(simp_all)
+  using Prf_elims(4) apply fastforce
+      apply(erule Prf_elims)
+      apply(simp)
+  
+      apply(simp)
+  
+  
      defer
      apply(subst bsimp_ASEQ1)
   using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce