--- 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