--- a/thys/BitCoded2.thy Sun Aug 11 00:28:14 2019 +0100
+++ b/thys/BitCoded2.thy Mon Aug 19 11:14:38 2019 +0200
@@ -23,6 +23,7 @@
Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
where
"Stars_add v (Stars vs) = Stars (v # vs)"
+| "Stars_add v _ = Stars [v]"
function
decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
@@ -2718,7 +2719,1353 @@
apply(auto)
using le_add2 le_less_trans not_less_eq by blast
-lemma PPP:
+lemma L_erase_bder_simp:
+ shows "L (erase (bsimp (bder a r))) = L (der a (erase (bsimp r)))"
+ using L_bsimp_erase der_correctness by auto
+
+lemma PPP0:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "(bders (intern r) s) >> code v"
+ using assms
+ by (smt L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code)
+
+thm L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code
+
+
+lemma PPP0_isar:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "(bders (intern r) s) >> code v"
+proof -
+ from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp
+
+ from assms have "s \<in> L r" using Posix1(1) by auto
+ then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)
+ then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"
+ by (simp add: mkeps_nullable nullable_correctness)
+
+ have "retrieve (bders (intern r) s) (mkeps (ders s r)) =
+ retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA LB bder_retrieve by simp
+ also have "... = retrieve (intern r) v"
+ using LB assms by auto
+ also have "... = code v" using a1 by (simp add: retrieve_code)
+ finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp
+ moreover
+ have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp
+ then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"
+ by (rule contains6)
+ ultimately
+ show "(bders (intern r) s) >> code v" by simp
+qed
+
+lemma PPP0b:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "(intern r) >> code v"
+ using assms
+ using Posix_Prf contains2 by auto
+
+lemma PPP0_eq:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "(intern r >> code v) = (bders (intern r) s >> code v)"
+ using assms
+ using PPP0_isar PPP0b by blast
+
+lemma f_cont1:
+ assumes "fuse bs1 a >> bs"
+ shows "\<exists>bs2. bs = bs1 @ bs2"
+ using assms
+ apply(induct a arbitrary: bs1 bs)
+ apply(auto elim: contains.cases)
+ done
+
+
+lemma f_cont2:
+ assumes "bsimp_AALTs bs1 as >> bs"
+ shows "\<exists>bs2. bs = bs1 @ bs2"
+ using assms
+ apply(induct bs1 as arbitrary: bs rule: bsimp_AALTs.induct)
+ apply(auto elim: contains.cases f_cont1)
+ done
+
+lemma contains_SEQ1:
+ assumes "bsimp_ASEQ bs r1 r2 >> bsX"
+ shows "\<exists>bs1 bs2. r1 >> bs1 \<and> r2 >> bs2 \<and> bsX = bs @ bs1 @ bs2"
+ using assms
+ apply(auto)
+ apply(case_tac "r1 = AZERO")
+ apply(auto)
+ using contains.simps apply blast
+ apply(case_tac "r2 = AZERO")
+ apply(auto)
+ apply(simp add: bsimp_ASEQ0)
+ using contains.simps apply blast
+ apply(case_tac "\<exists>bsX. r1 = AONE bsX")
+ apply(auto)
+ apply(simp add: bsimp_ASEQ2)
+ apply (metis append_assoc contains.intros(1) contains49 f_cont1)
+ apply(simp add: bsimp_ASEQ1)
+ apply(erule contains.cases)
+ apply(auto)
+ done
+
+lemma contains59:
+ assumes "AALTs bs rs >> bs2"
+ shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
+ using assms
+ apply(induct rs arbitrary: bs bs2)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto)
+ using contains0 by blast
+
+lemma contains60:
+ assumes "\<exists>r \<in> set rs. fuse bs r >> bs2"
+ shows "AALTs bs rs >> bs2"
+ using assms
+ apply(induct rs arbitrary: bs bs2)
+ apply(auto)
+ apply (metis contains3b contains49 f_cont1)
+ using contains.intros(5) f_cont1 by blast
+
+
+
+lemma contains61:
+ assumes "bsimp_AALTs bs rs >> bs2"
+ shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
+ using assms
+ apply(induct arbitrary: bs2 rule: bsimp_AALTs.induct)
+ apply(auto)
+ using contains.simps apply blast
+ using contains59 by fastforce
+
+lemma contains61b:
+ assumes "bsimp_AALTs bs rs >> bs2"
+ shows "\<exists>r \<in> set (flts rs). (fuse bs r) >> bs2"
+ using assms
+ apply(induct bs rs arbitrary: bs2 rule: bsimp_AALTs.induct)
+ apply(auto)
+ using contains.simps apply blast
+ using contains51d contains61 f_cont1 apply blast
+ by (metis bsimp_AALTs.simps(3) contains52 contains61 f_cont2)
+
+
+
+lemma contains61a:
+ assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
+ shows "bsimp_AALTs bs rs >> bs2"
+ using assms
+ apply(induct rs arbitrary: bs2 bs)
+ apply(auto)
+ apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1))
+ by (metis append_Cons append_Nil contains50 f_cont2)
+
+lemma contains62:
+ assumes "bsimp_AALTs bs (rs1 @ rs2) >> bs2"
+ shows "bsimp_AALTs bs rs1 >> bs2 \<or> bsimp_AALTs bs rs2 >> bs2"
+ using assms
+ apply -
+ apply(drule contains61)
+ apply(auto)
+ apply(case_tac rs1)
+ apply(auto)
+ apply(case_tac list)
+ apply(auto)
+ apply (simp add: contains60)
+ apply(case_tac list)
+ apply(auto)
+ apply (simp add: contains60)
+ apply (meson contains60 list.set_intros(2))
+ apply(case_tac rs2)
+ apply(auto)
+ apply(case_tac list)
+ apply(auto)
+ apply (simp add: contains60)
+ apply(case_tac list)
+ apply(auto)
+ apply (simp add: contains60)
+ apply (meson contains60 list.set_intros(2))
+ done
+
+lemma contains63:
+ assumes "AALTs bs (map (fuse bs1) rs) >> bs3"
+ shows "AALTs (bs @ bs1) rs >> bs3"
+ using assms
+ apply(induct rs arbitrary: bs bs1 bs3)
+ apply(auto elim: contains.cases)
+ apply(erule contains.cases)
+ apply(auto)
+ apply (simp add: contains0 contains60 fuse_append)
+ by (metis contains.intros(5) contains59 f_cont1)
+
+lemma contains64:
+ assumes "bsimp_AALTs bs (flts rs1 @ flts rs2) >> bs2" "\<forall>r \<in> set rs2. \<not> fuse bs r >> bs2"
+ shows "bsimp_AALTs bs (flts rs1) >> bs2"
+ using assms
+ apply(induct rs2 arbitrary: rs1 bs bs2)
+ apply(auto)
+ apply(drule_tac x="rs1" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
+ apply(drule_tac x="bs2" in meta_spec)
+ apply(drule meta_mp)
+ apply(drule contains61)
+ apply(auto)
+ using contains51b contains61a f_cont1 apply blast
+ apply(subst (asm) k0)
+ apply(auto)
+ prefer 2
+ using contains50 contains61a f_cont1 apply blast
+ apply(case_tac a)
+ apply(auto)
+ by (metis contains60 fuse_append)
+
+
+
+lemma contains65:
+ assumes "bsimp_AALTs bs (flts rs) >> bs2"
+ shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
+ using assms
+ apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+ apply(case_tac x)
+ apply(auto elim: contains.cases)
+ apply(case_tac list)
+ apply(auto elim: contains.cases)
+ apply(case_tac a)
+ apply(auto elim: contains.cases)
+ apply(drule contains61)
+ apply(auto)
+ apply (metis contains60 fuse_append)
+ apply(case_tac lista)
+ apply(auto elim: contains.cases)
+ apply(subst (asm) k0)
+ apply(drule contains62)
+ apply(auto)
+ apply(case_tac a)
+ apply(auto elim: contains.cases)
+ apply(case_tac x52)
+ apply(auto elim: contains.cases)
+ apply(case_tac list)
+ apply(auto elim: contains.cases)
+ apply (simp add: contains60 fuse_append)
+ apply(erule contains.cases)
+ apply(auto)
+ apply (metis append.left_neutral contains0 contains60 fuse.simps(4) in_set_conv_decomp)
+ apply(erule contains.cases)
+ apply(auto)
+ apply (metis contains0 contains60 fuse.simps(4) list.set_intros(1) list.set_intros(2))
+ apply (simp add: contains.intros(5) contains63)
+ apply(case_tac aa)
+ apply(auto)
+ apply (meson contains60 contains61 contains63)
+ apply(subst (asm) k0)
+ apply(drule contains64)
+ apply(auto)[1]
+ by (metis append_Nil2 bsimp_AALTs.simps(2) contains50 contains61a contains64 f_cont2 flts.simps(1))
+
+
+lemma contains55a:
+ assumes "bsimp r >> bs"
+ shows "r >> bs"
+ using assms
+ apply(induct r arbitrary: bs)
+ apply(auto)
+ apply(frule contains_SEQ1)
+ apply(auto)
+ apply (simp add: contains.intros(3))
+ apply(frule f_cont2)
+ apply(auto)
+ apply(drule contains65)
+ apply(auto)
+ using contains0 contains49 contains60 by blast
+
+
+lemma PPP1_eq:
+ shows "bsimp r >> bs \<longleftrightarrow> r >> bs"
+ using contains55 contains55a by blast
+
+lemma retrieve_code_bder:
+ assumes "\<Turnstile> v : der c r"
+ shows "code (injval r c v) = retrieve (bder c (intern r)) v"
+ using assms
+ by (simp add: Prf_injval bder_retrieve retrieve_code)
+
+lemma Etrans:
+ assumes "a >> s" "s = t"
+ shows "a >> t"
+ using assms by simp
+
+
+
+lemma retrieve_code_bders:
+ assumes "\<Turnstile> v : ders s r"
+ shows "code (flex r id s v) = retrieve (bders (intern r) s) v"
+ using assms
+ apply(induct s arbitrary: v r rule: rev_induct)
+ apply(auto simp add: ders_append flex_append bders_append)
+ apply (simp add: retrieve_code)
+ apply(frule Prf_injval)
+ apply(drule_tac meta_spec)+
+ apply(drule meta_mp)
+ apply(assumption)
+ apply(simp)
+ apply(subst bder_retrieve)
+ apply(simp)
+ apply(simp)
+ done
+
+thm LA LB
+
+lemma contains70:
+ assumes "s \<in> L(r)"
+ shows "bders (intern r) s >> code (flex r id s (mkeps (ders s r)))"
+ apply(subst PPP0_eq[symmetric])
+ apply (meson assms lexer_correct_None lexer_correctness(1) lexer_flex)
+ by (metis L07XX PPP0b assms erase_intern)
+
+
+
+
+definition PV where
+ "PV r s v = flex r id s v"
+
+definition PX where
+ "PX r s = PV r s (mkeps (ders s r))"
+
+lemma PV_id[simp]:
+ shows "PV r [] v = v"
+ by (simp add: PV_def)
+
+lemma PX_id[simp]:
+ shows "PX r [] = mkeps r"
+ by (simp add: PX_def)
+
+lemma PV_cons:
+ shows "PV r (c # s) v = injval r c (PV (der c r) s v)"
+ apply(simp add: PV_def flex_fun_apply)
+ done
+
+lemma PX_cons:
+ shows "PX r (c # s) = injval r c (PX (der c r) s)"
+ apply(simp add: PX_def PV_cons)
+ done
+
+lemma PV_append:
+ shows "PV r (s1 @ s2) v = PV r s1 (PV (ders s1 r) s2 v)"
+ apply(simp add: PV_def flex_append)
+ by (simp add: flex_fun_apply2)
+
+lemma PX_append:
+ shows "PX r (s1 @ s2) = PV r s1 (PX (ders s1 r) s2)"
+ by (simp add: PV_append PX_def ders_append)
+
+lemma code_PV0:
+ shows "PV r (c # s) v = injval r c (PV (der c r) s v)"
+ unfolding PX_def PV_def
+ apply(simp)
+ by (simp add: flex_injval)
+
+lemma code_PX0:
+ shows "PX r (c # s) = injval r c (PX (der c r) s)"
+ unfolding PX_def
+ apply(simp add: code_PV0)
+ done
+
+lemma Prf_PV:
+ assumes "\<Turnstile> v : ders s r"
+ shows "\<Turnstile> PV r s v : r"
+ using assms unfolding PX_def PV_def
+ apply(induct s arbitrary: v r)
+ apply(simp)
+ apply(simp)
+ by (simp add: Prf_injval flex_injval)
+
+
+lemma Prf_PX:
+ assumes "s \<in> L r"
+ shows "\<Turnstile> PX r s : r"
+ using assms unfolding PX_def PV_def
+ using L1 LX0 Posix_Prf lexer_correct_Some by fastforce
+
+lemma PV1:
+ assumes "\<Turnstile> v : ders s r"
+ shows "(intern r) >> code (PV r s v)"
+ using assms
+ by (simp add: Prf_PV contains2)
+
+lemma PX1:
+ assumes "s \<in> L r"
+ shows "(intern r) >> code (PX r s)"
+ using assms
+ by (simp add: Prf_PX contains2)
+
+lemma PX2:
+ assumes "s \<in> L (der c r)"
+ shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"
+ using assms
+ by (simp add: Prf_PX contains6 retrieve_code_bder)
+
+lemma PX2a:
+ assumes "c # s \<in> L r"
+ shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"
+ using assms
+ using PX2 lexer_correct_None by force
+
+lemma PX2b:
+ assumes "c # s \<in> L r"
+ shows "bder c (intern r) >> code (PX r (c # s))"
+ using assms unfolding PX_def PV_def
+ by (metis Der_def L07XX PV_def PX2a PX_def Posix_determ Posix_injval der_correctness erase_intern mem_Collect_eq)
+
+lemma PV3:
+ assumes "\<Turnstile> v : ders s r"
+ shows "bders (intern r) s >> code (PV r s v)"
+ using assms
+ using PX_def PV_def contains70
+ by (simp add: contains6 retrieve_code_bders)
+
+lemma PX3:
+ assumes "s \<in> L r"
+ shows "bders (intern r) s >> code (PX r s)"
+ using assms
+ using PX_def PV_def contains70 by auto
+
+lemma PV_bders_iff:
+ assumes "\<Turnstile> v : ders s r"
+ shows "bders (intern r) s >> code (PV r s v) \<longleftrightarrow> (intern r) >> code (PV r s v)"
+ by (simp add: PV1 PV3 assms)
+
+lemma PX_bders_iff:
+ assumes "s \<in> L r"
+ shows "bders (intern r) s >> code (PX r s) \<longleftrightarrow> (intern r) >> code (PX r s)"
+ by (simp add: PX1 PX3 assms)
+
+lemma PX4:
+ assumes "(s1 @ s2) \<in> L r"
+ shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2))"
+ using assms
+ by (simp add: PX3)
+
+lemma PX_bders_iff2:
+ assumes "(s1 @ s2) \<in> L r"
+ shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>
+ (intern r) >> code (PX r (s1 @ s2))"
+ by (simp add: PX1 PX3 assms)
+
+lemma PV_bders_iff3:
+ assumes "\<Turnstile> v : ders (s1 @ s2) r"
+ shows "bders (intern r) (s1 @ s2) >> code (PV r (s1 @ s2) v) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PV r (s1 @ s2) v)"
+ by (metis PV3 PV_append Prf_PV assms ders_append)
+
+
+
+lemma PX_bders_iff3:
+ assumes "(s1 @ s2) \<in> L r"
+ shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PX r (s1 @ s2))"
+ by (metis Ders_def L07XX PV_append PV_def PX4 PX_def Posix_Prf assms contains6 ders_append ders_correctness erase_bders erase_intern mem_Collect_eq retrieve_code_bders)
+
+lemma PV_bder_iff:
+ assumes "\<Turnstile> v : ders (s1 @ [c]) r"
+ shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ [c]) v) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PV r (s1 @ [c]) v)"
+ by (simp add: PV_bders_iff3 assms bders_snoc)
+
+lemma PV_bder_IFF:
+ assumes "\<Turnstile> v : ders (s1 @ c # s2) r"
+ shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ c # s2) v) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PV r (s1 @ c # s2) v)"
+ by (metis LA PV3 PV_def Prf_PV assms bders_append code_PV0 contains7 ders.simps(2) erase_bders erase_intern retrieve_code_bders)
+
+
+lemma PX_bder_iff:
+ assumes "(s1 @ [c]) \<in> L r"
+ shows "bder c (bders (intern r) s1) >> code (PX r (s1 @ [c])) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PX r (s1 @ [c]))"
+ by (simp add: PX_bders_iff3 assms bders_snoc)
+
+lemma PV_bder_iff2:
+ assumes "\<Turnstile> v : ders (c # s1) r"
+ shows "bders (bder c (intern r)) s1 >> code (PV r (c # s1) v) \<longleftrightarrow>
+ bder c (intern r) >> code (PV r (c # s1) v)"
+ by (metis PV3 Prf_PV assms bders.simps(2) code_PV0 contains7 ders.simps(2) erase_intern retrieve_code)
+
+
+lemma PX_bder_iff2:
+ assumes "(c # s1) \<in> L r"
+ shows "bders (bder c (intern r)) s1 >> code (PX r (c # s1)) \<longleftrightarrow>
+ bder c (intern r) >> code (PX r (c # s1))"
+ using PX2b PX3 assms by force
+
+
+
+
+
+
+definition EQ where
+ "EQ a1 a2 \<equiv> (\<forall>bs. a1 >> bs \<longleftrightarrow> a2 >> bs)"
+
+lemma EQ1:
+ assumes "EQ (intern r1) (intern r2)"
+ "bders (intern r1) s >> code (PX r1 s)"
+ "s \<in> L r1" "s \<in> L r2"
+ shows "bders (intern r2) s >> code (PX r1 s)"
+ using assms unfolding EQ_def
+ thm PX_bders_iff
+ apply(subst (asm) PX_bders_iff)
+ apply(assumption)
+ apply(subgoal_tac "intern r2 >> code (PX r1 s)")
+ prefer 2
+ apply(auto)
+
+
+lemma AA1:
+ assumes "[c] \<in> L r"
+ assumes "bder c (intern r) >> code (PX r [c])"
+ shows "bder c (bsimp (intern r)) >> code (PX r [c])"
+ using assms
+
+ apply(induct a arbitrary: c bs1 bs2 rs)
+ apply(auto elim: contains.cases)
+ apply(case_tac "c = x2a")
+ apply(simp)
+ apply(case_tac rs)
+ apply(auto)
+ using contains0 apply fastforce
+ apply(case_tac list)
+ apply(auto)
+
+ prefer 2
+ apply(erule contains.cases)
+ apply(auto)
+
+
+
+lemma TEST:
+ assumes "bder c a >> bs"
+ shows "bder c (bsimp a) >> bs"
+ using assms
+ apply(induct a arbitrary: c bs)
+ apply(auto elim: contains.cases)
+ prefer 2
+ apply(erule contains.cases)
+ apply(auto)
+
+
+
+
+
+lemma PX_bder_simp_iff:
+ assumes "\<Turnstile> v: ders (s1 @ s2) r"
+ shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow>
+ bders (intern r) s1 >> code (PV r (s1 @ s2) v)"
+ using assms
+ apply(induct s2 arbitrary: r s1 v)
+ apply(simp)
+ apply (simp add: PV3 contains55)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule_tac x="s1 @ [a]" in meta_spec)
+ apply(drule_tac x="v" in meta_spec)
+ apply(simp)
+ apply(simp add: bders_append)
+ apply(subst (asm) PV_bder_IFF)
+
+definition EXs where
+ "EXs a s \<equiv> \<forall>v \<in> \<lbrace>= v : ders s (erase a).
+
+lemma
+ assumes "s \<in> L r"
+ shows "(bders_simp (intern r) s >> code (PX r s)) \<longleftrightarrow> ((intern r) >> code (PX r s))"
+ using assms
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_simp_append)
+ apply(simp add: PPP1_eq)
+
+
+find_theorems "retrieve (bders _ _) _"
+find_theorems "_ >> retrieve _ _"
+find_theorems "bsimp _ >> _"
+
+
+
+lemma PX4a:
+ assumes "(s1 @ s2) \<in> L r"
+ shows "bders (intern r) (s1 @ s2) >> code (PV r s1 (PX (ders s1 r) s2))"
+ using PX4[OF assms]
+ apply(simp add: PX_append)
+ done
+
+lemma PV5:
+ assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+ shows "bders (intern r) (s1 @ s2) >> code (PV r s1 v)"
+ by (simp add: PPP0_isar PV_def Posix_flex assms)
+
+lemma PV6:
+ assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+ shows "bders (bders (intern r) s1) s2 >> code (PV r s1 v)"
+ using PV5 assms bders_append by auto
+
+find_theorems "retrieve (bders _ _) _"
+find_theorems "_ >> retrieve _ _"
+find_theorems "bder _ _ >> _"
+
+
+
+lemma PV6:
+ assumes "s @[c] \<in> L r"
+ shows"bder s1 (bders (intern r) s2) >> code (PX r (c # s))"
+ apply(subst PX_bders_iff)
+ apply(rule contains7)
+ apply(simp)
+ apply(rule assms)
+ apply(subst retrieve_code)
+
+ apply(simp add: PV_def)
+ apply(simp)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule_tac x="s1 @ [a]" in meta_spec)
+ apply(simp add: bders_append)
+ apply(subst PV_cons)
+ apply(drule_tac x="injval r a v" in meta_spec)
+ apply(drule meta_mp)
+
+
+lemma PV8:
+ assumes "(s1 @ s2) \<in> L r"
+ shows "bders (bders_simp (intern r) s1) s2 >> code (PX r (s1 @ s2))"
+ using assms
+ apply(induct s1 arbitrary: r s2 rule: rev_induct)
+ apply(simp add: PX3)
+ apply(simp)
+ apply(simp add: bders_simp_append)
+ apply(drule_tac x="r" in meta_spec)
+ apply(drule_tac x="x # s2" in meta_spec)
+ apply(simp add: bders_simp_append)
+ apply(rule iffI)
+ defer
+
+ apply(simp add: PX_append)
+ apply(simp add: bders_append)
+
+lemma PV6:
+ assumes "\<Turnstile> v : ders s r"
+ shows "bders (intern r) s >> code (PV r s v)"
+ using assms
+ by (simp add: PV_def contains6 retrieve_code_bders)
+
+lemma OO0_PX:
+ assumes "s \<in> L r"
+ shows "bders (intern r) s >> code (PX r s)"
+ using assms
+ by (simp add: PX3)
+
+
+lemma OO1:
+ assumes "[c] \<in> r \<rightarrow> v"
+ shows "bder c (intern r) >> code v"
+ using assms
+ using PPP0_isar by force
+
+lemma OO1a:
+ assumes "[c] \<in> L r"
+ shows "bder c (intern r) >> code (PX r [c])"
+ using assms unfolding PX_def PV_def
+ using contains70 by fastforce
+
+lemma OO12:
+ assumes "[c1, c2] \<in> L r"
+ shows "bders (intern r) [c1, c2] >> code (PX r [c1, c2])"
+ using assms
+ using PX_def PV_def contains70 by presburger
+
+lemma OO2:
+ assumes "[c] \<in> L r"
+ shows "bders_simp (intern r) [c] >> code (PX r [c])"
+ using assms
+ using OO1a Posix1(1) contains55 by auto
+
+
+lemma OO22:
+ assumes "[c1, c2] \<in> L r"
+ shows "bders_simp (intern r) [c1, c2] >> code (PX r [c1, c2])"
+ using assms
+ apply(simp)
+ apply(rule contains55)
+ apply(rule Etrans)
+ thm contains7
+ apply(rule contains7)
+
+
+
+lemma contains70:
+ assumes "s \<in> L(r)"
+ shows "bders_simp (intern r) s >> code (flex r id s (mkeps (ders s r)))"
+ using assms
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply (simp add: contains2 mkeps_nullable nullable_correctness)
+ apply(simp add: bders_simp_append flex_append)
+ apply(simp add: PPP1_eq)
+ apply(rule Etrans)
+ apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7)
+
+
+
+thm L07XX PPP0b erase_intern
+
+find_theorems "retrieve (bders _ _) _"
+find_theorems "_ >> retrieve _ _"
+find_theorems "bder _ _ >> _"
+
+
+proof -
+ from assms have "\<Turnstile> v : erase (bder c r)" by simp
+ then have "bder c r >> retrieve (bder c r) v"
+ by (simp add: contains6)
+ moreover have "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
+ using assms bder_retrieve by blast
+ ultimately have "bder c r >> code (injval (erase r) c v)"
+ apply -
+ apply(subst retrieve_code_bder)
+ apply(simp add: assms)
+ oops
+
+find_theorems "code _ = retrieve _ _"
+find_theorems "_ >> retrieve _ _"
+find_theorems "bder _ _ >> _"
+
+lemma
+ assumes "s \<in> r \<rightarrow> v" "s = [c1, c2]"
+ shows "bders_simp (intern r) s >> bs \<longleftrightarrow> bders (intern r) s >> bs"
+ using assms
+ apply(simp add: PPP1_eq)
+
+
+
+lemma PPP10:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "bders_simp (intern r) s >> retrieve (intern r) v \<longleftrightarrow> bders (intern r) s >> retrieve (intern r) v"
+ using assms
+ apply(induct s arbitrary: r v rule: rev_induct)
+ apply(auto)
+ apply(simp_all add: PPP1_eq bders_append bders_simp_append)
+
+ find_theorems "bder _ _ >> _"
+
+lemma
+ shows "bder
+
+
+find_theorems "bsimp _ >> _"
+
+fun get where
+ "get (Some v) = v"
+
+
+lemma decode9:
+ assumes "decode' bs (STAR r) = (v, bsX)" "bs \<noteq> []"
+ shows "\<exists>vs. v = Stars vs"
+ using assms
+ apply(induct bs\<equiv>"bs" r\<equiv>"STAR r" arbitrary: bs r v bsX rule: decode'.induct)
+ apply(auto)
+ apply(case_tac "decode' ds r")
+ apply(auto)
+ apply(case_tac "decode' b (STAR r)")
+ apply(auto)
+ apply(case_tac aa)
+ apply(auto)
+ done
+
+lemma decode10_Stars:
+ assumes "decode' bs (STAR r) = (Stars vs, bs1)" "\<Turnstile> Stars vs : (STAR r)" "vs \<noteq> []"
+ shows "decode' (bs @ bsX) (STAR r) = (Stars vs, bs1 @ bsX)"
+ using assms
+ apply(induct vs arbitrary: bs r bs1 bsX)
+ apply(auto elim!: Prf_elims)
+ apply(case_tac vs)
+ apply(auto)
+ apply(case_tac bs)
+ apply(auto)
+ apply(case_tac aa)
+ apply(auto)
+ apply(case_tac "decode' list r")
+ apply(auto)
+ apply(case_tac "decode' b (STAR r)")
+ apply(auto)
+ apply(case_tac "decode' (list @ bsX) r")
+ apply(auto)
+ apply(case_tac "decode' ba (STAR r)")
+ apply(auto)
+ apply(case_tac ba)
+ apply(auto)
+ oops
+
+lemma decode10:
+ assumes "decode' bs r = (v, bs1)" "\<Turnstile> v : r"
+ shows "decode' (bs @ bsX) r = (v, bs1 @ bsX)"
+ using assms
+ apply(induct bs r arbitrary: v bs1 bsX rule: decode'.induct)
+ apply(auto elim: Prf_elims)[7]
+ apply(case_tac "decode' ds r1")
+ apply(auto)[3]
+ apply(case_tac "decode' (ds @ bsX) r1")
+ apply(auto)[3]
+ apply(auto elim: Prf_elims)[4]
+ apply(case_tac "decode' ds r2")
+ apply(auto)[1]
+ apply(case_tac "decode' (ds @ bsX) r2")
+ apply(auto)[1]
+ apply(auto elim: Prf_elims)[2]
+ apply(case_tac "decode' ds r1")
+ apply(auto)[1]
+ apply(case_tac "decode' b r2")
+ apply(auto)[1]
+ apply(auto elim: Prf_elims)[1]
+ apply(auto elim: Prf_elims)[1]
+ apply(auto elim: Prf_elims)[1]
+ apply(erule Prf_elims)
+(* STAR case *)
+ apply(auto)
+ apply(case_tac "decode' ds r")
+ apply(auto)
+ apply(case_tac "decode' b (STAR r)")
+ apply(auto)
+ apply(case_tac aa)
+ apply(auto)
+ apply(case_tac "decode' (b @ bsX) (STAR r)")
+ apply(auto)
+ oops
+
+
+lemma contains100:
+ assumes "(intern r) >> bs"
+ shows "\<exists>v bsV. decode' bs r = (v, bsV) \<and> \<Turnstile> v : r"
+ using assms
+ apply(induct r arbitrary: bs)
+ apply(auto)
+apply(erule contains.cases)
+ apply(auto)
+ apply(erule contains.cases)
+ apply(auto intro: Prf.intros)
+apply(erule contains.cases)
+ apply(auto)
+ apply(drule_tac x="bs1" in meta_spec)
+ apply(drule_tac x="bs2" in meta_spec)
+ apply(auto)[1]
+ apply(rule_tac x="Seq v va" in exI)
+ apply(auto)
+ apply(case_tac "decode' (bs1 @ bs2) r1")
+ apply(auto)
+ apply(case_tac "decode' b r2")
+ apply(auto)
+ oops
+
+lemma contains101:
+ assumes "(intern r) >> code v"
+ shows "\<Turnstile> v : r"
+ using assms
+ apply(induct r arbitrary: v)
+ apply(auto elim: contains.cases)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac v)
+ apply(auto intro: Prf.intros)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac v)
+ apply(auto intro: Prf.intros)
+
+(*
+ using contains.simps apply blast
+ apply(erule contains.cases)
+ apply(auto)
+ using L1 Posix_ONE Prf.intros(4) apply force
+ apply(erule contains.cases)
+ apply(auto)
+ apply (metis Prf.intros(5) code.simps(2) decode_code get.simps)
+ apply(erule contains.cases)
+ apply(auto)
+ prefer 2
+ apply(erule contains.cases)
+ apply(auto)
+ apply(frule f_cont1)
+ apply(auto)
+ apply(case_tac "decode' bs2 r1")
+ apply(auto)
+ apply(rule Prf.intros)
+ apply (metis Cons_eq_append_conv contains49 f_cont1 fst_conv list.inject self_append_conv2)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(frule f_cont1)
+ apply(auto)
+ apply(case_tac "decode' bs2 r2")
+ apply(auto)
+ apply(rule Prf.intros)
+ apply (metis (full_types) append_Cons contains49 append_Nil fst_conv)
+ apply(erule contains.cases)
+ apply(auto)
+ apply(case_tac "decode' (bs1 @ bs2) r1")
+ apply(auto)
+ apply(case_tac "decode' b r2")
+ apply(auto)
+ apply(rule Prf.intros)
+
+ apply (metis fst_conv)
+ apply(subgoal_tac "b = bs2 @ bsX")
+ apply(auto)
+ apply (metis fst_conv)
+ apply(subgoal_tac "decode' (bs1 @ bs2 @ bsX) r1 = (a, bs2 @ bsX)")
+ apply simp
+*)
+
+
+ apply(case_tac ba)
+ apply(auto)
+ apply(drule meta_spec)
+ apply(drule meta_mp)
+ apply(assumption)
+ prefer 2
+
+
+ apply(case_tac v)
+ apply(auto)
+
+
+
+find_theorems "bder _ _ >> _"
+
+lemma PPP0_isar:
+ assumes "bders r s >> code v"
+ shows "bders_simp r s >> code v"
+ using assms
+ apply(induct s arbitrary: r v)
+ apply(simp)
+ apply(auto)
+ apply(drule_tac x="bsimp (bder a r)" in meta_spec)
+ apply(drule_tac x="v" in meta_spec)
+ apply(drule_tac meta_mp)
+
+ prefer 2
+ apply(simp)
+
+ using bnullable_correctness nullable_correctness apply fastforce
+ apply(simp add: bders_append)
+
+
+
+
+
+lemma PPP0_isar:
+ assumes "s \<in> r \<rightarrow> v"
+ shows "(bders (intern r) s) >> code v"
+proof -
+ from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp
+
+ from assms have "s \<in> L r" using Posix1(1) by auto
+ then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)
+ then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"
+ by (simp add: mkeps_nullable nullable_correctness)
+
+ have "retrieve (bders (intern r) s) (mkeps (ders s r)) =
+ retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA by simp
+ also have "... = retrieve (intern r) v"
+ using LB assms by auto
+ also have "... = code v" using a1 by (simp add: retrieve_code)
+ finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp
+ moreover
+ have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp
+ then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"
+ by (rule contains6)
+ ultimately
+ show "(bders (intern r) s) >> code v" by simp
+qed
+
+
+
+
+
+
+
+
+
+lemma A0:
+ assumes "r \<in> set (flts rs)"
+ shows "r \<in> set rs"
+ using assms
+ apply(induct rs arbitrary: r rule: flts.induct)
+ apply(auto)
+ oops
+
+lemma A1:
+ assumes "r \<in> set (flts (map (bder c) (flts rs)))" "\<forall>r \<in> set rs. nonnested r \<and> good r"
+ shows "r \<in> set (flts (map (bder c) rs))"
+ using assms
+ apply(induct rs arbitrary: r c rule: flts.induct)
+ apply(auto)
+ apply(subst (asm) map_bder_fuse)
+ apply(simp add: flts_append)
+ apply(auto)
+ apply(auto simp add: comp_def)
+ apply(subgoal_tac "\<forall>r \<in> set rs1. nonalt r \<and> good r")
+ prefer 2
+ apply (metis Nil_is_append_conv good.simps(5) good.simps(6) in_set_conv_decomp neq_Nil_conv)
+ apply(case_tac rs1)
+ apply(auto)
+ apply(subst (asm) k0)
+ apply(auto)
+
+ oops
+
+
+lemma bsimp_comm2:
+ assumes "bder c a >> bs"
+ shows "bder c (bsimp a) >> bs"
+ using assms
+ apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)
+ apply(case_tac x)
+ apply(auto)
+ prefer 2
+ apply(erule contains.cases)
+ apply(auto)
+ apply(subst bder_bsimp_AALTs)
+ apply(rule contains61a)
+ apply(rule bexI)
+ apply(rule contains0)
+ apply(assumption)
+
+
+lemma bsimp_comm:
+ assumes "bder c (bsimp a) >> bs"
+ shows "bsimp (bder c a) >> bs"
+ using assms
+ apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)
+ apply(case_tac x)
+ apply(auto)
+ prefer 4
+ apply(erule contains.cases)
+ apply(auto)
+ using contains.intros(3) contains55 apply fastforce
+ prefer 3
+ apply(subst (asm) bder_bsimp_AALTs)
+ apply(drule contains61b)
+ apply(auto)
+ apply(rule contains61a)
+ apply(rule bexI)
+ apply(assumption)
+ apply(rule_tac t="set (flts (map (bsimp \<circ> bder c) x52))"
+ and s="set (flts (map (bder c \<circ> bsimp) x52))" in subst)
+ prefer 2
+ find_theorems "map (_ \<circ> _) _ = _"
+ apply(simp add: comp_def)
+
+
+ find_theorems "bder _ (bsimp_AALTs _ _) = _"
+ apply(drule contains_SEQ1)
+ apply(auto)[1]
+ apply(rule contains.intros)
+ prefer 2
+ apply(assumption)
+
+
+ apply(case_tac "bnullable x42")
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(case_tac "bsimp x42 = AZERO")
+ apply (me tis L_erase_bder_simp bder.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) good.simps(1) good1a xxx_bder2)
+ apply(case_tac "bsimp x43 = AZERO")
+ apply (simp add: bsimp_ASEQ0)
+ apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")
+ using b3 apply force
+ apply(subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(auto)[1]
+ using b3 apply blast
+ apply(case_tac "bsimp (bder c x42) = AZERO")
+ apply(simp)
+ using contains.simps apply blast
+ apply(case_tac "\<exists>bs2. bsimp (bder c x42) = AONE bs2")
+ apply(auto)[1]
+ apply(subst (asm) bsimp_ASEQ2)
+ apply(subgoal_tac "\<exists>bsX. bs = x41 @ bs2 @ bsX")
+ apply(auto)[1]
+ apply(rule contains.intros)
+ apply (simp add: contains.intros(1))
+ apply (metis append_assoc contains49)
+ using append_assoc f_cont1 apply blast
+ apply(subst (asm) bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(erule contains.cases)
+ apply(auto)
+ using contains.intros(3) less_add_Suc1 apply blast
+ apply(case_tac "bsimp x42 = AZERO")
+ using b3 apply force
+ apply(case_tac "bsimp x43 = AZERO")
+ apply (metis LLLL(1) L_erase_bder_simp bder.simps(1) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) good.simps(1) good1a xxx_bder2)
+ apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")
+ apply(auto)[1]
+ apply(subst bsimp_ASEQ2)
+ apply(drule_tac x="fuse (x41 @ bs1) x43" in spec)
+ apply(drule mp)
+ apply (simp add: asize_fuse)
+ apply(drule_tac x="bs" in spec)
+ apply(drule_tac x="c" in spec)
+ apply(drule mp)
+ prefer 2
+ apply (simp add: bsimp_fuse)
+ apply(subst (asm) k0)
+ apply(subgoal_tac "\<exists>bsX. bs = x41 @ bsX")
+ prefer 2
+ using f_cont2 apply blast
+ apply(clarify)
+ apply(drule contains62)
+ apply(auto)[1]
+ apply(case_tac "bsimp (bder c x42) = AZERO")
+ apply (metis append_is_Nil_conv bsimp_ASEQ.simps(1) contains61 flts.simps(1) flts.simps(2) in_set_conv_decomp list.distinct(1))
+ apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX")
+ apply(clarify)
+ apply (simp add: L_erase_bder_simp xxx_bder2)
+ using L_erase_bder_simp xxx_bder2 apply auto[1]
+ apply(drule contains65)
+ apply(auto)[1]
+ apply (simp add: bder_fuse bmkeps_simp bsimp_fuse fuse_append)
+ apply(subst bsimp_ASEQ1)
+ apply(auto)[3]
+ apply(auto)[1]
+ apply(case_tac "bsimp (bder c x42) = AZERO")
+ apply(simp add: bsimp_ASEQ0)
+ apply(drule contains65)
+ apply(auto)[1]
+ apply (metis asize_fuse bder_fuse bmkeps_simp bsimp_fuse contains.intros(4) contains.intros(5) contains49 f_cont1 less_add_Suc2)
+
+ apply(frule f_cont1)
+ apply(auto)
+
+ apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX")
+ apply(auto)[1]
+ apply(subst (asm) bsimp_ASEQ2)
+ apply(auto)
+ apply(drule contains65)
+ apply(auto)[1]
+ apply(frule f_cont1)
+ apply(auto)
+ apply(rule contains.intros)
+ apply (metis (no_types, lifting) append_Nil2 append_eq_append_conv2 contains.intros(1) contains.intros(3) contains49 f_cont1 less_add_Suc1 same_append_eq)
+ apply(frule f_cont1)
+ apply(auto)
+ apply(rule contains.intros)
+ apply(drule contains49)
+ apply(subst (asm) bsimp_fuse[symmetric])
+ apply(frule f_cont1)
+ apply(auto)
+ apply(subst (3) append_Nil[symmetric])
+ apply(rule contains.intros)
+ apply(drule contains49)
+
+ prefer 2
+
+ apply(simp)
+ find_theorems "fuse _ _ >> _"
+
+
+ apply(erule contains.cases)
+ apply(auto)
+
+
+
+
+
+
+
+
+
+thm bder_retrieve
+find_theorems "_ >> retrieve _ _"
+
+lemma TEST:
+ assumes "\<Turnstile> v : ders s (erase r)"
+ shows "bders r s >> retrieve r (flex (erase r) id s v)"
+ using assms
+ apply(induct s arbitrary: v r rule: rev_induct)
+ apply(simp)
+ apply (simp add: contains6)
+ apply(simp add: bders_append ders_append)
+ apply(rule Etrans)
+ apply(rule contains7)
+ apply(simp)
+ by (metis LA bder_retrieve bders_snoc ders_snoc erase_bders)
+
+
+lemma TEST1:
+ assumes "bder c r >> retrieve r (injval (erase r) c v)"
+ shows "r >> retrieve r v"
+ oops
+
+lemma TEST2:
+ assumes "bders (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))" "s = [c1, c2]"
+ shows "bders_simp (intern r) s >> retrieve (intern r) (flex r id s (mkeps (ders s r)))"
+ using assms
+ apply(simp)
+
+
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_simp_append ders_append flex_append bders_append)
+ apply(rule contains55)
+
+ apply(drule_tac x="bsimp (bder a r)" in meta_spec)
+ thm L02_bders
+ apply(subst L02_bders)
+ find_theorems "retrieve (bsimp _) _ = _"
+ apply(drule_tac "" in Etrans)
+
+lemma TEST2:
+ assumes "bders r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+ shows "bders_simp r s >> retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+ using assms
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_simp_append ders_append flex_append bders_append)
+ apply(subgoal_tac "bder x (bders r xs) >> retrieve r (flex (erase r) id xs (injval (ders xs (erase r)) x (mkeps (ders xs (erase r)))))")
+ find_theorems "bders _ _ >> _"
+ apply(drule_tac x="bsimp (bder a r)" in meta_spec)
+ thm L02_bders
+ apply(subst L02_bders)
+ find_theorems "retrieve (bsimp _) _ = _"
+ apply(drule_tac "" in Etrans)
+ apply(rule contains55)
+ apply(rule Etrans)
+ apply(rule contains7)
+ apply(subgoal_tac "\<Turnstile> v : der x (erase (bders_simp r xs))")
+ apply(assumption)
+ prefer 2
+
+
+ apply(simp)
+ by (m etis LA bder_retrieve bders_snoc ders_snoc erase_bders)
+
+
+
+
+lemma PPP0A:
+ assumes "s \<in> L (r)"
+ shows "(bders (intern r) s) >> code (flex r id s (mkeps (ders s r)))"
+ using assms
+ by (metis L07XX PPP0 erase_intern)
+
+
+
+
+lemma PPP1:
+ assumes "bder c (intern r) >> code v" "\<Turnstile> v : der c r"
+ shows "(intern r) >> code (injval r c v)"
+ using assms
+ by (simp add: Prf_injval contains2)
+
+
+(*
+lemma PPP1:
+ assumes "bder c r >> code v" "\<Turnstile> v : der c (erase r)"
+ shows "r >> code (injval (erase r) c v)"
+ using assms contains7[OF assms(2)] retrieve_code[OF assms(2)]
+ find_theorems "bder _ _ >> _"
+ by (simp add: Prf_injval contains2)
+*)
+
+lemma PPP3:
+ assumes "\<Turnstile> v : ders s (erase a)"
+ shows "bders a s >> retrieve a (flex (erase a) id s v)"
+ using LA[OF assms] contains6 erase_bders assms by metis
+
+
+find_theorems "bder _ _ >> _"
+
+lemma QQQ0:
+ assumes "bder c a >> code v"
+ shows "a >> code (injval (erase a) c v)"
+ using assms
+ apply(induct a arbitrary: c v)
+ apply(auto)
+ using contains.simps apply blast
+ using contains.simps apply blast
+ apply(case_tac "c = x2a")
+ apply(simp)
+ apply(erule contains.cases)
+ apply(auto)
+
+
+lemma PPP4:
+ assumes "bders (intern a) [c1, c2] >> bs"
+ shows "bders_simp (intern a) [c1, c2] >> bs"
+ using assms
+ apply(simp)
+ apply(rule contains55)
+
+ find_theorems "bder _ _ >> _"
+
+
+ apply(induct s arbitrary: a v rule: rev_induct)
+ apply(simp)
+ apply (simp add: contains6)
+ apply(simp add: bders_append bders_simp_append ders_append flex_append)
+ (*apply(rule contains55)*)
+ apply(drule Prf_injval)
+ apply(drule_tac x="a" in meta_spec)
+ apply(drule_tac x="injval (ders xs (erase a)) x v" in meta_spec)
+ apply(drule meta_mp)
+ apply(assumption)
+
+ apply(thin_tac "\<Turnstile> injval (ders xs (erase a)) x v : ders xs (erase a)")
+
+ apply(thin_tac "bders a xs >> retrieve a (flex (erase a) id xs (injval (ders xs (erase a)) x v))")
+
+ apply(rule Etrans)
+ apply(rule contains7)
+
+lemma PPP4:
+ assumes "bders a s >> code v" "\<Turnstile> v : ders s (erase a)"
+ shows "bders_simp a s >> code v"
+ using assms
+ apply(induct s arbitrary: a v rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_append bders_simp_append ders_append)
+ apply(rule contains55)
+ find_theorems "bder _ _ >> _"
+
+
+lemma PPP0:
+ assumes "s \<in> L (r)"
+ shows "(bders (intern r) s) >> code (flex r id s (mkeps (ders s r)))"
+ using assms
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply (simp add: contains2 mkeps_nullable nullable_correctness)
+ apply(simp add: bders_simp_append flex_append)
+ apply(rule contains55)
+ apply(rule Etrans)
+ apply(rule contains7)
+ defer
+
+ find_theorems "_ >> _"
+ apply(drule_tac x="der a r" in meta_spec)
+ apply(drule meta_mp)
+ find_theorems "bder _ _ >> _"
+ apply(subgoal_tac "s \<in> L(der a r)")
+ prefer 2
+
+ apply (simp add: Posix_Prf contains2)
+ apply(simp add: bders_simp_append)
+ apply(rule contains55)
+ apply(frule PPP0)
+ apply(simp add: bders_append)
+ using Posix_injval contains7
+ apply(subgoal_tac "retrieve r (injval (erase r) x v)")
+ find_theorems "bders _ _ >> _"
+
+
+
+lemma PPP1:
assumes "\<Turnstile> v : ders s r"
shows "bders (intern r) s >> code v"
using assms
@@ -2735,6 +4082,7 @@
apply(assumption)
apply(subst (asm) retrieve_code)
apply(assumption)
+
using contains7 contains7a contains6 retrieve_code
apply(rule contains7)