diff -r 3b8e3a156200 -r 20a57552d722 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Sat Feb 23 21:52:06 2019 +0000
+++ b/thys/BitCoded.thy	Wed Mar 13 10:36:29 2019 +0000
@@ -87,7 +87,7 @@
 
 section {* Annotated Regular Expressions *}
 
-datatype arexp =
+datatype arexp = 
   AZERO
 | AONE "bit list"
 | ACHAR "bit list" char
@@ -107,6 +107,13 @@
 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
 
+lemma fuse_append:
+  shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
+  apply(induct r)
+  apply(auto)
+  done
+
+
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
@@ -451,5 +458,901 @@
 qed
 
 
+fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
+  where
+  "distinctBy [] f acc = []"
+| "distinctBy (x#xs) f acc = 
+     (if (f x) \<in> acc then distinctBy xs f acc 
+      else x # (distinctBy xs f ({f x} \<union> acc)))"
+
+fun flts :: "arexp list \<Rightarrow> arexp list"
+  where 
+  "flts [] = []"
+| "flts (AZERO # rs) = flts rs"
+| "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"
+| "bsimp_ASEQ _ _ AZERO = AZERO"
+| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
+| "bsimp_ASEQ bs1 r1 r2 = ASEQ  bs1 r1 r2"
+
+
+fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
+  where
+  "bsimp_AALTs _ [] = AZERO"
+| "bsimp_AALTs bs1 [r] = fuse bs1 r"
+| "bsimp_AALTs bs1 rs = AALTs bs1 rs"
+
+
+fun bsimp :: "arexp \<Rightarrow> arexp" 
+  where
+  "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
+| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
+| "bsimp r = r"
+
+fun 
+  bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+where
+  "bders_simp r [] = r"
+| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
+
+definition blexer_simp where
+ "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
+                decode (bmkeps (bders_simp (intern r) s)) r else None"
+
+
+lemma bders_simp_append:
+  shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
+  apply(induct s1 arbitrary: r s2)
+   apply(simp)
+  apply(simp)
+  done
+
+
+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)
+  apply(simp_all)
+  by (metis erase_fuse fuse.simps(4))
+
+lemma L_bsimp_AALTs:
+  "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+  apply(simp_all add: erase_fuse)
+  done
+
+lemma L_erase_AALTs:
+  shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(case_tac rs)
+   apply(simp)
+  apply(simp)
+  done
+
+lemma L_erase_flts:
+  shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
+  apply(induct rs rule: flts.induct)
+        apply(simp_all)
+  apply(auto)
+  using L_erase_AALTs erase_fuse apply auto[1]
+  by (simp add: L_erase_AALTs erase_fuse)
+
+
+lemma L_bsimp_erase:
+  shows "L (erase r) = L (erase (bsimp r))"
+  apply(induct r)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(auto simp add: Sequ_def)[1]
+  apply(subst L_bsimp_ASEQ[symmetric])
+  apply(auto simp add: Sequ_def)[1]
+  apply(subst (asm)  L_bsimp_ASEQ[symmetric])
+  apply(auto simp add: Sequ_def)[1]
+   apply(simp)
+   apply(subst L_bsimp_AALTs[symmetric])
+   defer
+   apply(simp)
+  apply(subst (2)L_erase_AALTs)
+  apply(subst L_erase_flts)
+  apply(auto)
+   apply (simp add: L_erase_AALTs)
+  using L_erase_AALTs by blast
+
+
+lemma bsimp_ASEQ1:
+  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+  shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
+  using assms
+  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
+
+lemma bsimp_ASEQ2:
+  shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
+  apply(induct r2)
+  apply(auto)
+  done
+
+
+lemma L_bders_simp:
+  shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply(simp)
+  apply(simp)
+  apply(simp add: ders_append)
+  apply(simp add: bders_simp_append)
+  apply(simp add: L_bsimp_erase[symmetric])
+  by (simp add: der_correctness)
+
+lemma b1:
+  "bsimp_ASEQ bs1 (AONE bs) r =  fuse (bs1 @ bs) r" 
+  apply(induct r)
+       apply(auto)
+  done
+
+lemma b2:
+  assumes "bnullable r"
+  shows "bmkeps (fuse bs r) = bs @ bmkeps r"
+  by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+
+lemma b3:
+  shows "bnullable r = bnullable (bsimp r)"
+  using L_bsimp_erase bnullable_correctness nullable_correctness by auto
+
+
+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"
+  shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
+  using assms
+  apply(induct rs)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma q3:
+  assumes "\<exists>r \<in> set rs. bnullable r"
+  shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"
+  using assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply(simp)
+   apply(simp)
+  apply (simp add: b2)
+  apply(simp)
+  done
+
+lemma qq1:
+  assumes "\<exists>r \<in> set rs. bnullable r"
+  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
+  using assms
+  apply(induct rs arbitrary: rs1 bs)
+  apply(simp)
+  apply(simp)
+  by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)
+
+lemma qq2:
+  assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
+  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"
+  using assms
+  apply(induct rs arbitrary: rs1 bs)
+  apply(simp)
+  apply(simp)
+  by (metis append_assoc in_set_conv_decomp r1 r2)
+  
+lemma qq3:
+  shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
+  apply(induct rs arbitrary: bs)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma q3a:
+  assumes "\<exists>r \<in> set rs. bnullable r"
+  shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
+  using assms
+  apply(induct rs arbitrary: bs bs1)
+   apply(simp)
+  apply(simp)
+  apply(auto)
+   apply (metis append_assoc b2 bnullable_correctness erase_fuse r0)
+  apply(case_tac "bnullable a")
+   apply (metis append.assoc b2 bnullable_correctness erase_fuse r0)
+  apply(case_tac rs)
+  apply(simp)
+  apply(simp)
+  apply(auto)[1]
+   apply (metis bnullable_correctness erase_fuse)+
+  done
+
+lemma qq4:
+  assumes "\<exists>x\<in>set list. bnullable x"
+  shows "\<exists>x\<in>set (flts list). bnullable x"
+  using assms
+  apply(induct list rule: flts.induct)
+        apply(auto)
+  by (metis UnCI bnullable_correctness erase_fuse imageI)
+  
+
+lemma qs3:
+  assumes "\<exists>r \<in> set rs. bnullable r"
+  shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"
+  using assms
+  apply(induct rs arbitrary: bs taking: size rule: measure_induct)
+  apply(case_tac x)
+  apply(simp)
+  apply(simp)
+  apply(case_tac a)
+       apply(simp)
+       apply (simp add: r1)
+      apply(simp)
+      apply (simp add: r0)
+     apply(simp)
+     apply(case_tac "flts list")
+      apply(simp)
+  apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)
+     apply(simp)
+     apply (simp add: r1)
+    prefer 3
+    apply(simp)
+    apply (simp add: r0)
+   prefer 2
+   apply(simp)
+  apply(case_tac "\<exists>x\<in>set x52. bnullable x")
+  apply(case_tac "list")
+    apply(simp)
+    apply (metis b2 fuse.simps(4) q3a r2)
+   apply(erule disjE)
+    apply(subst qq1)
+     apply(auto)[1]
+     apply (metis bnullable_correctness erase_fuse)
+    apply(simp)
+     apply (metis b2 fuse.simps(4) q3a r2)
+    apply(simp)
+    apply(auto)[1]
+     apply(subst qq1)
+      apply (metis bnullable_correctness erase_fuse image_eqI set_map)
+     apply (metis b2 fuse.simps(4) q3a r2)
+  apply(subst qq1)
+      apply (metis bnullable_correctness erase_fuse image_eqI set_map)
+    apply (metis b2 fuse.simps(4) q3a r2)
+   apply(simp)
+   apply(subst qq2)
+     apply (metis bnullable_correctness erase_fuse imageE set_map)
+  prefer 2
+  apply(case_tac "list")
+     apply(simp)
+    apply(simp)
+   apply (simp add: qq4)
+  apply(simp)
+  apply(auto)
+   apply(case_tac list)
+    apply(simp)
+   apply(simp)
+   apply (simp add: r0)
+  apply(case_tac "bnullable (ASEQ x41 x42 x43)")
+   apply(case_tac list)
+    apply(simp)
+   apply(simp)
+   apply (simp add: r0)
+  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)"
+          "\<exists>x\<in>set x2a. bnullable x"
+        shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
+  using assms
+  apply(induct x2a)
+  apply fastforce
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0)
+  apply(auto)[1]
+  apply (metis b3 k0 list.set_intros(1) qs3 r0)
+  by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map)
+  
+  
+  
+lemma bmkeps_simp:
+  assumes "bnullable r"
+  shows "bmkeps r = bmkeps (bsimp r)"
+  using  assms
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+    prefer 3
+  apply(simp)
+   apply(case_tac "bsimp r1 = AZERO")
+    apply(simp)
+    apply(auto)[1]
+  apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
+ apply(case_tac "bsimp r2 = AZERO")
+    apply(simp)  
+    apply(auto)[1]
+  apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+    apply(auto)[1]
+    apply(subst b1)
+    apply(subst b2)
+  apply(simp add: b3[symmetric])
+    apply(simp)
+   apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)")
+    prefer 2
+  apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
+   apply(simp)
+  apply(simp)
+  apply(subst q3[symmetric])
+   apply simp
+  using b3 qq4 apply auto[1]
+  apply(subst qs3)
+   apply simp
+  using k1 by blast
+
+thm bmkeps_retrieve bmkeps_simp bder_retrieve
+
+lemma bmkeps_bder_AALTs:
+  assumes "\<exists>r \<in> set rs. bnullable (bder c r)" 
+  shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(auto)
+  apply(case_tac rs)
+    apply(simp)
+  apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2)
+   apply(simp)
+  apply(case_tac  rs)
+   apply(simp_all)
+  done
+
+
+
+
+lemma MAIN_decode:
+  assumes "\<Turnstile> v : ders s r"
+  shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"
+  using assms
+proof (induct s arbitrary: v rule: rev_induct)
+  case Nil
+  have "\<Turnstile> v : ders [] r" by fact
+  then have "\<Turnstile> v : r" by simp
+  then have "Some v = decode (retrieve (intern r) v) r"
+    using decode_code retrieve_code by auto
+  then show "Some (flex r id [] v) = decode (retrieve (bders_simp (intern r) []) v) r"
+    by simp
+next
+  case (snoc c s v)
+  have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 
+     Some (flex r id s v) = decode (retrieve (bders_simp (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)
+  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_simp (intern r) s) (injval (ders s r) c v)) r"
+    using asm2 IH by simp
+  also have "... = decode (retrieve (bder c (bders_simp (intern r) s)) v) r"
+    using asm bder_retrieve ders_append 
+    apply -
+    apply(drule_tac x="v" in meta_spec)
+    apply(drule_tac x="c" in meta_spec)
+    apply(drule_tac x="bders_simp (intern r) s" in meta_spec)
+    apply(drule_tac  meta_mp)
+     apply(simp add: ders_append)
+     defer
+    apply(simp)
+    oops
+
+function (sequential) bretrieve :: "arexp \<Rightarrow> bit list \<Rightarrow> (bit list) * (bit list)" where
+  "bretrieve (AZERO) bs1 = ([], bs1)"
+| "bretrieve (AONE bs) bs1 = (bs, bs1)"
+| "bretrieve (ACHAR bs c) bs1 = (bs, bs1)"
+| "bretrieve (AALTs bs rs) [] = (bs, [])"
+| "bretrieve (AALTs bs [r]) bs1 = 
+     (let (bs2, bs3) = bretrieve r bs1 in (bs @ bs2, bs3))"
+| "bretrieve (AALTs bs (r#rs)) (Z#bs1) = 
+     (let (bs2, bs3) = bretrieve r bs1 in (bs @ [Z] @ bs2, bs3))"
+| "bretrieve (AALTs bs (r#rs)) (S#bs1) = 
+     (let (bs2, bs3) = bretrieve (AALTs [] rs) bs1 in (bs @ [S] @ bs2, bs3))"
+| "bretrieve (ASEQ bs r1 r2) bs1 = 
+     (let (bs2, bs3) = bretrieve r1 bs1 in 
+      let (bs4, bs5) = bretrieve r2 bs3 in (bs @ bs2 @ bs4, bs5))"
+| "bretrieve (ASTAR bs r) [] = (bs, [])"
+| "bretrieve (ASTAR bs r) (S#bs1) = (bs @ [S], bs1)"
+| "bretrieve (ASTAR bs r) (Z#bs1) = 
+     (let (bs2, bs3) = bretrieve r bs1 in 
+      let (bs4, bs5) = bretrieve (ASTAR [] r) bs3 in (bs @ bs2 @ [Z] @ bs4, bs5))"
+  by (pat_completeness) (auto)
+
+termination
+  sorry
+
+thm Prf.intros
+
+
+lemma retrieve_XXX:
+  assumes "\<Turnstile> v : erase r" 
+  shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r)  \<and> retrieve (bsimp r) v' = retrieve r v"
+  using assms
+  apply(induct r arbitrary: v)
+       apply(simp)
+  using Prf_elims(1) apply blast
+      apply(simp)
+  using Prf_elims(4) apply fastforce
+    apply(simp)
+  apply blast
+  apply simp
+   apply(case_tac  "r1 = AZERO")
+     apply(simp)
+  apply (meson Prf_elims(1) Prf_elims(2))
+  apply(case_tac  "r2 = AZERO")
+     apply(simp)
+     apply (meson Prf_elims(1) Prf_elims(2))
+  apply(erule Prf_elims)
+  apply(simp)
+   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+     apply(clarify)
+     apply(simp)
+    apply(subst bsimp_ASEQ2)
+     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 fastforce
+      apply(simp)
+    apply(simp)
+  apply(drule_tac  x="v1" in meta_spec)
+  apply(drule_tac  x="v2" in meta_spec)
+     apply(simp)
+  apply(clarify)
+     apply(rule_tac x="Seq v' v'a" in exI)
+     apply(simp)
+  apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
+    prefer 3
+  apply(drule_tac  x="v1" in meta_spec)
+  apply(drule_tac  x="v2" in meta_spec)
+     apply(simp)
+    apply(clarify)
+    apply(rule_tac x="v'a" in exI)
+    apply(subst bsimp_ASEQ2)
+    apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
+   prefer 2  
+   apply(auto)
+  apply(case_tac "x2a")
+   apply(simp)
+  using Prf_elims(1) apply blast
+  apply(simp)
+  apply(case_tac "list")
+   apply(simp)
+  sorry
+
+
+lemma TEST:
+  assumes "\<Turnstile> v : ders s r"
+  shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v"
+  using assms
+  apply(induct s arbitrary: r v rule: rev_induct)
+   apply(simp)
+   defer
+   apply(simp add: ders_append)
+   apply(frule Prf_injval)
+  apply(drule_tac x="r" in meta_spec)
+   apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+   apply(simp)
+   apply(simp add: bders_append)
+   apply(subst bder_retrieve)
+    apply(simp)
+   apply(simp)
+  thm bder_retrieve
+  thm bmkeps_retrieve
+
+
+lemma bmkeps_simp2:
+  assumes "bnullable (bder c r)"
+  shows "bmkeps (bder c (bsimp r)) = bmkeps (bder c r)"
+  using  assms
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  prefer 3
+    apply(simp)
+   apply(simp)
+   apply(auto)[1]
+     prefer 2
+     apply(case_tac "r1 = AZERO")
+      apply(simp)
+   apply(case_tac "r2 = AZERO")
+      apply(simp)
+     apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
+      apply(clarify)
+      apply(simp)
+      apply(subst bsimp_ASEQ2)
+  
+   apply(simp add: bmkeps_simp)
+  apply(simp add: bders_append)
+  apply(drule_tac x="bder a r" in meta_spec)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   prefer 2
+   apply(simp)
+   apply(case_tac x2a)
+    apply(simp)
+  apply(simp add: )
+  apply(subst k0)
+   apply(auto)[1]
+    apply(case_tac list)
+     apply(simp)
+  
+
+   apply(case_tac  "r1=AZERO")
+    apply(simp)
+   apply(case_tac  "r2=AZERO")
+    apply(simp)
+    apply(auto)[1]
+   apply(case_tac  "\<exists>bs. r1=AONE bs")
+  apply(simp)
+    apply(auto)[1]
+     apply(subst bsimp_ASEQ2)
+
+  
+   prefer 2
+   apply(simp)
+  apply(subst  bmkeps_bder_AALTs)
+   apply(case_tac x2a)
+    apply(simp)
+   apply(simp)
+   apply(auto)[1]
+    apply(subst  bmkeps_bder_AALTs)
+  
+   apply(case_tac a)
+  apply(simp_all)
+   apply(auto)[1]
+    apply(case_tac list)
+         apply(simp)
+        apply(simp)
+  
+     prefer 2
+  apply(simp)
+
+
+lemma bbs0:
+  shows "blexer_simp r [] = blexer r []"
+  apply(simp add: blexer_def blexer_simp_def)
+  done
+
+lemma bbs1:
+  shows "blexer_simp r [c] = blexer r [c]"
+  apply(simp add: blexer_def blexer_simp_def)
+  apply(auto)
+    defer
+  using b3 apply auto[1]
+  using b3 apply auto[1]  
+  apply(subst bmkeps_simp[symmetric])
+   apply(simp)
+  apply(simp)
+  done
+  
+lemma bbs1:
+  shows "blexer_simp r [c1, c2] = blexer r [c1, c2]"
+  apply(simp add: blexer_def blexer_simp_def)
+  apply(auto)
+    defer
+  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
+  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
+  apply(subst bmkeps_simp[symmetric])
+  using b3 apply auto[1]
+  apply(subst bmkeps_retrieve)
+  using b3 bnullable_correctness apply blast
+  apply(subst bder_retrieve)
+  using b3 bnullable_correctness mkeps_nullable apply fastforce
+  apply(subst bmkeps_retrieve)
+  using bnullable_correctness apply blast
+  apply(subst bder_retrieve)
+  using bnullable_correctness mkeps_nullable apply force
+  
+  using bder_retrieve bmkeps_simp bmkeps_retrieve
+
+  
+
+lemma bsimp_retrieve_bder:
+  assumes "\<Turnstile> v : der c (erase r)"
+  shows "retrieve (bder c r) v = retrieve (bsimp (bder c r)) v"
+  thm bder_retrieve bmkeps_simp
+  apply(induct  r arbitrary: c v)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(auto)[1]
+     apply(case_tac "bsimp (bder c r1) = AZERO")
+      apply(simp)
+  
+    prefer 3
+    apply(simp)
+  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(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs")
+     apply(clarify)
+     apply(subgoal_tac "L (der c (erase r)) = {[]}")
+      prefer 2
+      apply (metis L.simps(2) L_bsimp_erase erase.simps(2) erase_bder erase_fuse)
+     apply(simp)
+  
+  
+  
+    apply(subst bsimp_ASEQ1)
+       apply(simp)
+      apply(simp)
+  apply(auto)[1]
+  
+     prefer 2
+  
+
+lemma oo:
+  shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
+  apply(simp add: blexer_correctness)
+  done
+
+lemma oo2a:
+  assumes "\<forall>r. bmkeps (bders_simp r s) = bmkeps (bders r s)" "c # s \<in> L r"
+          "bnullable (bders_simp (bsimp (bder c (intern r))) s)"
+  shows "(case (blexer_simp (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer_simp r (c # s)"
+  using assms
+  apply(simp add: blexer_simp_def)
+  apply(auto  split: option.split)
+    apply (metis blexer_correctness blexer_def lexer.simps(2) lexer_correct_None option.simps(4))
+   prefer 2
+  apply (metis L_bders_simp L_bsimp_erase Posix1(1) Posix_mkeps bnullable_correctness ders_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None)
+  apply(subst bmkeps_retrieve)
+  using L_bders_simp bnullable_correctness nullable_correctness apply blast
+  
+  thm bder_retrieve
+  
+  
+  apply(subst bder_retrieve[symmetric])
+  
+  
+
+  apply(drule_tac x="bsimp (bder c (intern r))" in  spec)
+  apply(drule sym)
+   apply(simp)
+   apply(subst blexer_simp_def)
+  apply(case_tac "bnullable (bders_simp (intern (der c r)) s)")
+   apply(simp)
+  apply(auto split: option.split)
+  apply(subst oo)
+  apply(simp)
+  done
+
+
+
+lemma oo3:
+  assumes "\<forall>r. bders r s = bders_simp r s"
+  shows "blexer_simp r (s @ [c]) = blexer r (s @ [c])"
+  using assms
+  apply(simp (no_asm) add: blexer_simp_def)
+  apply(auto)
+   prefer 2
+  apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
+  apply(simp add: bders_simp_append)
+  apply(subst bmkeps_simp[symmetric])
+  using b3 apply auto[1]
+  apply(simp add: blexer_def)
+  apply(auto)[1]
+   prefer 2
+  apply (metis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
+  apply(simp add: bders_append)     
+  done
+
+lemma oo4:
+  assumes "\<forall>r. bmkeps (bders r s) = bmkeps (bders_simp r s)" "bnullable (bder c (bders r s))"
+  shows "bmkeps (bders_simp r (s @ [c])) = bmkeps (bders r (s @ [c]))"
+  using assms
+  apply(simp add: bders_simp_append)
+  apply(subst bmkeps_simp[symmetric])
+  apply (metis L_bders_simp bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
+  apply(simp add: bders_append)
+  done
+
+lemma oo4:
+  shows "blexer_simp r s = blexer r s"
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply(simp only: blexer_simp_def blexer_def)
+   apply(simp)
+  apply(simp only: blexer_simp_def blexer_def)
+  apply(subgoal_tac "bnullable (bders_simp (intern r) (xs @ [x])) = bnullable (bders (intern r) (xs @ [x]))")
+   prefer 2
+   apply (simp add: b4)
+  apply(simp)
+  apply(rule impI)
+  apply(simp add: bders_simp_append)
+  apply(subst bmkeps_simp[symmetric])
+  using b3 apply auto[1]
+  apply(subst bmkeps_retrieve)
+  using b3 bnullable_correctness apply blast
+  apply(subst bder_retrieve)
+  using b3 bnullable_correctness mkeps_nullable apply fastforce
+  apply(simp add: bders_append)
+  apply(subst bmkeps_retrieve)
+  using bnullable_correctness apply blast
+  apply(subst bder_retrieve)
+  using bnullable_correctness mkeps_nullable apply fastforce
+  apply(subst erase_bder)
+  apply(case_tac "xs \<in> L")
+  apply(subst (asm) (2) bmkeps_retrieve)
+  
+  
+  thm bmkeps_retrieve bmkeps_retrieve
+  apply(subst bmkeps_retrieve[symmetric])
+  
+   apply (simp add: bnullable_correctness)
+  apply(simp add: bders_simp_append)
+   
+  
+  apply(induct s arbitrary: r rule: rev_induct) 
+   apply(simp add: blexer_def blexer_simp_def)
+  apply(rule oo3)
+  apply(simp (no_asm) add: blexer_simp_def)
+  apply(auto)
+   prefer 2
+  apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
+  apply(simp add: bders_simp_append)
+  apply(subst bmkeps_simp[symmetric])
+  using b3 apply auto[1]
+  apply(simp add: blexer_def)
+  apply(auto)[1]
+   prefer 2
+  apply (m etis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
+  apply(simp add: bders_append)     
+  oops
+
+
+lemma bnullable_simp:
+  assumes "s \<in> L (erase r)"
+  shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
+  using assms
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply(simp)
+  apply(simp add: bders_append bders_simp_append)
+  apply(subst bmkeps_simp[symmetric])
+  apply (metis L_bders_simp b3 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correct_Some lexer_correctness(1))
+  apply(subst bmkeps_retrieve)
+  apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer_correct_Some option.distinct(1))
+  apply(subst bmkeps_retrieve)
+  apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2))
+  apply(subst bder_retrieve)
+  apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer_correct_Some mkeps_nullable option.distinct(1))
+  apply(subst bder_retrieve)
+  apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2) mkeps_nullable)
+    
+  apply(drule_tac x="bder a r" in meta_spec)
+  apply(drule_tac  meta_mp)
+  apply (me tis erase_bder lexer.simps(2) lexer_correct_None option.simps(4))
+  apply(simp)
+  oops
+
+
+lemma
+  shows "blexer r s = blexer_simp r s"
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply(simp add: blexer_def blexer_simp_def)
+  apply(case_tac "xs @ [x] \<in> L r")
+   defer
+   apply(subgoal_tac "blexer (ders xs r) [x] = None")
+    prefer 2
+    apply(subst blexer_correctness)
+    apply(simp (no_asm) add: lexer_correct_None)
+    apply(simp add: nullable_correctness)
+    apply(simp add: der_correctness ders_correctness)
+  apply(simp add: Der_def Ders_def)
+apply(subgoal_tac "blexer r (xs @ [x]) = None")
+    prefer 2
+    apply (simp add: blexer_correctness)
+  using lexer_correct_None apply auto[1]
+  apply(simp)
+   apply(subgoal_tac "blexer_simp (ders xs r) [x] = None")
+    prefer 2
+  apply (metis L_bders_simp Posix_injval Posix_mkeps bders.simps(2) blexer_correctness blexer_simp_def bnullable_correctness ders.simps(1) erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
+   apply(subgoal_tac "[] \<notin> L (erase (bders_simp (intern r) (xs @ [x])))")
+  prefer 2
+  apply(metis L_bders_simp Posix_injval bders.simps(2) blexer_correctness ders.simps(1) ders_append erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
+  using blexer_simp_def bnullable_correctness lexer_correct_None apply auto[1]
+(* case xs @ [x] \<in> L r *)
+  apply(subgoal_tac "\<exists>v. blexer (ders xs r) [x] = Some v \<and> [x] \<in> (ders xs r) \<rightarrow> v")
+   prefer 2  
+  using blexer_correctness lexer_correct_Some apply auto[1]
+    apply (simp add: Posix_injval Posix_mkeps)
+  apply (metis ders.simps(1) ders.simps(2) ders_append lexer_correct_None lexer_flex)    
+  apply(clarify)
+  apply(subgoal_tac "blexer_simp (ders xs r) [x] = Some v")
+   prefer 2
+   apply(simp add: blexer_simp_def)
+   apply(auto)[1]
+    apply (metis bders.simps(1) bders.simps(2) blexer_def bmkeps_simp option.simps(3))
+  using b3 blexer_def apply fastforce
+  apply(subgoal_tac "blexer_simp (ders xs r) [x] = blexer_simp r (xs @ [x])")
+   prefer 2
+   apply(simp add: blexer_simp_def)
+  
+   apply(simp)
+  
+  
+  
+   apply(simp)
+  apply(subst blexer_simp_def)
+  apply(simp)
+  apply(auto)
+  apply(drule_tac x="der a r" in meta_spec)
+  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(simp)
+  
+
+
+lemma
+  shows "blexer r s = blexer_simp r s"
+  apply(induct s arbitrary: r)
+   apply(simp add: blexer_def blexer_simp_def)
+  apply(case_tac "s \<in> L (der a r)")
+   defer
+   apply(subgoal_tac "blexer (der a r) s = None")
+    prefer 2
+    apply (simp add: blexer_correctness lexer_correct_None)
+apply(subgoal_tac "blexer r (a # s) = None")
+    prefer 2
+    apply (simp add: blexer_correctness)
+   apply(simp)
+  
+   apply(subst blexer_simp_def)
+   apply(simp)
+  apply(drule_tac  x="der a r" in  meta_spec)
+   apply(subgoal_tac "s \<notin> L(erase (bder a (intern  r)))")
+  prefer 2
+    apply simp
+   
+   apply(simp only:)
+   apply(subst blexer_simp_def)
+   apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))")
+    apply(simp)
+   apply(subst bnullable_correctness[symmetric])
+  apply(simp)
+  
+
 
 end
\ No newline at end of file