diff -r db0ff630bbb7 -r 43e070803c1c thys/BitCoded.thy
--- a/thys/BitCoded.thy	Thu Apr 11 17:37:00 2019 +0100
+++ b/thys/BitCoded.thy	Fri May 10 11:56:37 2019 +0100
@@ -400,13 +400,65 @@
   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
   using assms
   apply(induct r arbitrary: v rule: erase.induct)
-  apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve)
-  apply(case_tac va)
+         apply(simp)
+         apply(erule Prf_elims)
+        apply(simp)
+        apply(erule Prf_elims) 
+        apply(simp)
+      apply(case_tac "c = ca")
+       apply(simp)
+       apply(erule Prf_elims)
+       apply(simp)
+      apply(simp)
+       apply(erule Prf_elims)
+  apply(simp)
+      apply(erule Prf_elims)
+     apply(simp)
+    apply(simp)
+  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+    apply(erule Prf_elims)
+     apply(simp)
+    apply(simp)
+    apply(case_tac rs)
+     apply(simp)
+    apply(simp)
+  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
    apply(simp)
-  apply(auto)
-  by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
+   apply(case_tac "nullable (erase r1)")
+    apply(simp)
+  apply(erule Prf_elims)
+     apply(subgoal_tac "bnullable r1")
+  prefer 2
+  using bnullable_correctness apply blast
+    apply(simp)
+     apply(erule Prf_elims)
+     apply(simp)
+   apply(subgoal_tac "bnullable r1")
+  prefer 2
+  using bnullable_correctness apply blast
+    apply(simp)
+    apply(simp add: retrieve_fuse2)
+    apply(simp add: bmkeps_retrieve)
+   apply(simp)
+   apply(erule Prf_elims)
+   apply(simp)
+  using bnullable_correctness apply blast
+  apply(rename_tac bs r v)
+  apply(simp)
+  apply(erule Prf_elims)
+     apply(clarify)
+  apply(erule Prf_elims)
+  apply(clarify)
+  apply(subst injval.simps)
+  apply(simp del: retrieve.simps)
+  apply(subst retrieve.simps)
+  apply(subst retrieve.simps)
+  apply(simp)
+  apply(simp add: retrieve_fuse2)
+  done
   
 
+
 lemma MAIN_decode:
   assumes "\<Turnstile> v : ders s r"
   shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
@@ -425,18 +477,23 @@
      Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
   have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
   then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 
-    by(simp add: Prf_injval ders_append)
+    by (simp add: Prf_injval ders_append)
   have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
     by (simp add: flex_append)
   also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
     using asm2 IH by simp
   also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
-    using asm by(simp_all add: bder_retrieve ders_append)
+    using asm by (simp_all add: bder_retrieve ders_append)
   finally show "Some (flex r id (s @ [c]) v) = 
                  decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
 qed
 
 
+definition blex where
+ "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
+
+
+
 definition blexer where
  "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
                 decode (bmkeps (bders (intern r) s)) r else None"
@@ -513,6 +570,9 @@
                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
 
+
+
+
 lemma asize0:
   shows "0 < asize r"
   apply(induct  r)
@@ -964,6 +1024,20 @@
   apply(auto)
   by (metis (mono_tags, hide_lams) imageE nn1c set_map)
 
+lemma nn1d:
+  assumes "bsimp r = AALTs bs rs"
+  shows "\<forall>r1 \<in> set rs. \<forall>  bs. r1 \<noteq> AALTs bs  rs2"
+  using nn1b assms
+  by (metis nn1qq)
+
+lemma nn_flts:
+  assumes "nonnested (AALTs bs rs)"
+  shows "\<forall>r \<in>  set (flts rs). nonalt r"
+  using assms
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(auto)
+  done
+
 lemma rt:
   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
   apply(induct rs)
@@ -973,6 +1047,16 @@
   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 bsimp_AALTs_qq:
+  assumes "1 < length rs"
+  shows "bsimp_AALTs bs rs = AALTs bs  rs"
+  using  assms
+  apply(case_tac rs)
+   apply(simp)
+  apply(case_tac list)
+   apply(simp_all)
+  done
+
 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)"
@@ -1007,7 +1091,7 @@
    apply(simp)
   apply(case_tac a)
   apply(simp_all)
-  sorry
+  oops
 
 lemma bsimp_AALTs_idem:
   (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
@@ -1091,6 +1175,149 @@
     prefer 3
   oops
 
+lemma ww:
+  shows "bsimp_AALTs bs [r] = fuse bs r"
+  by simp
+
+lemma flts_0:
+  assumes "nonnested (AALTs bs  rs)"
+  shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
+  using assms
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(simp) 
+       apply(simp) 
+      defer
+      apply(simp) 
+     apply(simp) 
+    apply(simp) 
+apply(simp) 
+  apply(rule ballI)
+  apply(simp)
+  done
+  
+lemma q1:
+  shows "AZERO \<notin> set (flts (map bsimp rs))"
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp)
+
+lemma cc:
+  assumes "bsimp (fuse bs' r) = (AALTs bs rs)" 
+  shows "\<forall>r \<in> set  rs. r \<noteq> AZERO"
+  using assms
+ apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
+       apply(simp)
+  apply(case_tac "bsimp r1 = AZERO")
+    apply simp
+   apply(case_tac "bsimp r2 = AZERO")
+    apply(simp)
+    apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+     apply(auto)[1]
+  apply (simp add: bsimp_ASEQ0)
+  apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+    apply(auto)[2]
+    apply (simp add: bsimp_ASEQ2)
+  using bsimp_fuse apply fastforce
+    apply (simp add: bsimp_ASEQ1)
+   prefer 2
+      apply(simp)
+     defer
+     apply(simp)
+    apply(simp)
+   apply(simp)
+  (* AALT case *)
+  apply(simp only: fuse.simps)
+  apply(simp)
+  apply(case_tac "flts (map bsimp rs)")
+   apply(simp)
+  apply(simp)
+  apply(case_tac list)
+   apply(simp)
+   apply(case_tac a)
+        apply(simp_all)
+   apply(auto)
+   apply (metis ex_map_conv list.set_intros(1) nn1b nn1c nonalt.simps(1))
+  apply(case_tac rs)
+   apply(simp)
+  apply(simp)
+  apply(case_tac list)
+   apply(simp)  
+  
+  
+  apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO")
+   prefer 2
+   apply(rule_tac bs="bs' @ bs1" in flts_0)
+  
+  
+  thm bsimp_AALTs_qq
+  apply(case_tac "1 < length rs")
+  apply(drule_tac bsimp_AALTs_qq)
+  apply(subgoal_tac "nonnested (AALTs bs rsa)")
+   prefer 2
+   apply (metis nn1b)
+  apply(rule ballI)
+  apply(simp)
+  apply(drule_tac x="r" in meta_spec)
+  apply(simp)
+  (* HERE *)
+  apply(drule flts_0)
+  
+  
+  
+  apply(simp)
+  
+  
+  
+  
+  apply(subst 
+
+  apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
+    
+   prefer 2
+  
+  
+  apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
+       apply(auto)
+  apply(case_tac "bsimp r1 = AZERO")
+    apply simp
+   apply(case_tac "bsimp r2 = AZERO")
+    apply(simp)
+    apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+     apply(auto)
+  apply (simp add: bsimp_ASEQ0)
+  apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
+    apply(auto)
+    apply (simp add: bsimp_ASEQ2)
+  using bsimp_fuse apply fastforce
+   apply (simp add: bsimp_ASEQ1)
+  
+  
+  
+  apply(subst 
+
+  apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
+    
+   prefer 2
+  
+
+
+lemma ww1:
+  assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO"
+  shows  "r1 = r2"
+  using assms
+  apply(case_tac r1)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+   prefer 2
+   apply(simp)
+  apply(simp)
+  apply(auto)
+  oops
+
 lemma bsimp_idem:
   shows "bsimp (bsimp r) = bsimp r"
 apply(induct r taking: "asize" rule: measure_induct)
@@ -1104,8 +1331,87 @@
    apply (simp add: bsimp_ASEQ_idem)
   apply(clarify)
   apply(case_tac x52)
+   apply(simp)
+  (* AALT case where rs is of the form _ # _ *)
+  apply(clarify)
   apply(simp)
-  apply(simp)
+  apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
+   prefer 2
+   apply(subst bsimp_AALTs_qq)
+    apply(auto)[1]
+   apply(simp)
+   prefer 2
+  apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> 
+                     length (flts (bsimp a # map bsimp list)) = 1")
+    prefer 2
+    apply(auto)[1]
+  using le_SucE apply blast
+  apply(erule disjE)
+    apply(simp)
+   apply(simp)
+   apply(subst k0)
+   apply(subst (2)  k0)
+   apply(subst (asm) k0)
+   apply(simp)
+  apply(subgoal_tac "length (flts [bsimp a]) = 1 \<or> 
+                     length (flts (map bsimp list)) = 1")
+    prefer 2
+  apply linarith
+    apply(erule disjE)
+    apply(simp)
+    prefer 2
+    apply(simp)
+    apply(drule_tac x="AALTs x51 list" in  spec)
+    apply(drule mp)
+     apply(simp)
+  using asize0 apply blast
+    apply(simp)
+   apply(frule_tac x="a" in spec)
+  apply(drule mp)
+    apply(simp)
+   apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
+    prefer 2
+  apply (simp add: length_Suc_conv)
+   apply(clarify)
+   apply(simp only: )
+  apply(case_tac "bsimp a = AZERO")
+    apply simp
+  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+    apply(clarify)
+    apply(simp)
+  apply(drule_tac x="AALTs bs rs" in spec)
+  apply(drule mp)
+     apply(simp)
+  apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1)
+    apply(simp)
+  
+    apply(subst ww)
+   apply(subst ww)
+   apply(frule_tac x="fuse x51 r" in spec)
+  apply(drule mp)
+    apply(simp)
+  apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons)
+   apply(case_tac "bsimp a = AZERO")
+    apply simp
+  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+    apply(clarify)
+  
+   defer
+  
+  apply(
+   apply(case_tac a)
+  apply(simp_all)
+   apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
+    prefer 2
+  apply (simp add: length_Suc_conv)
+   apply auto[1]
+  apply(case_tac 
+  apply(clarify)
+  
+  defer
+    apply(auto)[1]
+
+
   apply(subst k0)
   apply(subst (2) k0)
   apply(case_tac "bsimp a = AZERO")
@@ -1480,7 +1786,7 @@
   
      defer
      apply(subst bsimp_ASEQ1)
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
+  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force
   using L_bsimp_erase L_
 
 lemma retrieve_XXX:
@@ -1744,7 +2050,7 @@
   apply(auto elim!: Prf_elims)[1]
     apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO")
      apply(simp)
-     apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)
+     apply (met is L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)
     apply(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs")
      apply(clarify)
      apply(subgoal_tac "L (der c (erase r)) = {[]}")
@@ -1960,7 +2266,7 @@
   apply(subst blexer_def)
    apply(subgoal_tac "bnullable (bders (intern r) (a # s))")
     prefer 2
-    apply (metis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
+    apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
   apply(simp)
   
 
@@ -1992,6 +2298,198 @@
     apply(simp)
    apply(subst bnullable_correctness[symmetric])
   apply(simp)
+  oops
+
+lemma flts_append:
+  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
+   apply(auto)
+  apply(case_tac xs)
+   apply(auto)
+   apply(case_tac x)
+        apply(auto)
+  apply(case_tac x)
+        apply(auto)
+  done
+
+lemma flts_bsimp:
+  "flts (map bsimp rs) = map bsimp (flts rs)"
+apply(induct rs taking: size rule: measure_induct)
+  apply(case_tac x)
+   apply(simp)
+  apply(simp)
+  apply(induct rs rule: flts.induct)
+        apply(simp)
+       apply(simp)
+      defer
+      apply(simp)
+     apply(simp)
+    defer
+    apply(simp)
+  apply(subst List.list.map(2))
+   apply(simp only: flts.simps)
+   apply(subst k0)
+   apply(subst map_append)
+   apply(simp only:)
+   apply(simp del: bsimp.simps)
+   apply(case_tac rs1)
+    apply(simp)
+   apply(simp)
+  apply(case_tac list)
+    apply(simp_all)
+  thm map
+  apply(subst map.simps)
+        apply(auto)
+   defer
+  apply(case_tac "(bsimp va) = AZERO")
+    apply(simp)
+  
+  using b3 apply for ce
+   apply(case_tac "(bsimp a2) = AZERO")
+     apply(simp)
+  apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
+    apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
+     apply(clarify)
+     apply(simp)
+  
+
+lemma XXX:
+  shows "bsimp (bsimp a) = bsimp a"
+  sorry
+
+lemma bder_fuse:
+  shows "bder c (fuse bs a) = fuse bs  (bder c a)"
+  apply(induct a arbitrary: bs c)
+       apply(simp_all)
+  done
+
+lemma XXX2:
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  apply(induct a arbitrary: c)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  prefer 3
+    apply(simp)
+   apply(auto)[1]
+   apply(case_tac "(bsimp a1) = AZERO")
+     apply(simp)
+  using b3 apply force
+   apply(case_tac "(bsimp a2) = AZERO")
+     apply(simp)
+  apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
+    apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
+     apply(clarify)
+     apply(simp)
+  apply(subst bsimp_ASEQ2)  
+     apply(subgoal_tac "bmkeps a1 = bs")
+      prefer 2
+      apply (simp add: bmkeps_simp)
+     apply(simp)
+  apply(subst (1) bsimp_fuse[symmetric])
+     defer
+  apply(subst bsimp_ASEQ1)  
+        apply(simp)
+       apply(simp)
+  apply(simp)
+     apply(auto)[1]
+      apply (metis XXX bmkeps_simp bsimp_fuse)
+  using b3 apply blast
+  apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
+   apply(simp)
+   prefer 2
+   apply(subst bder_fuse)
+  apply(subst bsimp_fuse[symmetric])
+   apply(simp)
+  sorry
+
+
+thm bsimp_AALTs.simps
+thm bsimp.simps
+thm flts.simps
+
+lemma XXX3:
+  "bsimp (bders (bsimp r) s) = bsimp (bders r s)"
+  apply(induct s arbitrary: r rule:  rev_induct)
+   apply(simp)
+   apply (simp add: XXX)
+  apply(simp add: bders_append)
+  apply(subst (2) XXX2[symmetric])
+  apply(subst XXX2[symmetric])
+  apply(drule_tac x="r" in meta_spec)
+  apply(simp)
+  done
+
+lemma XXX4:
+ "bders_simp (bsimp r) s = bsimp (bders r s)"
+  apply(induct s arbitrary: r)
+   apply(simp)
+  apply(simp)
+  by (metis XXX2)
+  
+  
+lemma
+  assumes "bnullable (bder c r)"  "bnullable (bder c (bsimp r))"
+  shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))"
+ using  assms
+  apply(induct r arbitrary: c)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+  prefer 3
+   apply(simp)
+  apply(auto)[1]
+    apply(case_tac "(bsimp r1) = AZERO")
+     apply(simp)
+   apply(case_tac "(bsimp r2) = AZERO")
+     apply(simp)
+  apply (simp add: bsimp_ASEQ0)
+    apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
+     apply(clarify)
+     apply(simp)
+     apply(subgoal_tac "bnullable r1")
+      prefer 2
+  using b3 apply force
+      apply(simp)
+  apply(simp add: bsimp_ASEQ2) 
+      prefer 2
+  
+  
+  
+  apply(subst bsimp_ASEQ2)
+  
+  
+  
+  
+
+
+lemma
+  assumes  "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)"
+  shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)"
+  using  assms
+  apply(induct s2 arbitrary: a s1)
+   apply(simp)
+  using bmkeps_simp apply blast
+  apply(simp add: bders_append)
+  apply(drule_tac x="aa" in meta_spec)
+  apply(drule_tac x="s1 @ [a]" in meta_spec)
+  apply(drule meta_mp)
+   apply(simp add: bders_append)
+  apply(simp add: bders_append)
+  apply(drule meta_mp)
+   apply (metis b4 bders.simps(2) bders_simp.simps(2))
+  apply(simp)
+  
+   apply (met is b4 bders.simps(2) bders_simp.simps(2))
+  
+  
+  
+  using b3 apply blast
+  using b3 apply auto[1]
+  apply(auto simp add: blex_def)
+    prefer 3
+  
+