# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1566206078 -7200
# Node ID 9d466b27b05491bb507e256e1a679c9d78144288
# Parent  c40348a77318fdddafc79c1df79ae84168cf83c9
added progress with the contains relation

diff -r c40348a77318 -r 9d466b27b054 thys/BitCoded2.thy
--- 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)