diff -r 8f9ea6453ba2 -r 533765dc71cc thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Sat Sep 14 13:25:56 2019 +0100
+++ b/thys/BitCoded2.thy	Tue Sep 17 08:42:13 2019 +0100
@@ -566,11 +566,18 @@
   done
 
 lemma bder_fuse:
-  shows "bder c (fuse bs a) = fuse bs  (bder c a)"
+  shows "bder c (fuse bs a) = fuse bs (bder c a)"
   apply(induct a arbitrary: bs c)
   apply(simp_all)
   done
 
+lemma bders_fuse:
+  shows "bders (fuse bs a) s = fuse bs (bders a s)"
+  apply(induct s arbitrary: bs a)
+   apply(simp_all)
+  by (simp add: bder_fuse)
+
+
 lemma map_bder_fuse:
   shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
   apply(induct as1)
@@ -1846,46 +1853,6 @@
   by force
 
 
-lemma contains_ex1:
-  assumes "a = AALTs bs1 [AZERO, AONE bs2]" "a >> bs" 
-  shows "bsimp a >> bs"
-  using assms
-  apply(simp)
-  apply(erule contains.cases)
-        apply(auto)
-  using contains.simps apply blast
-  apply(erule contains.cases)
-        apply(auto)
-  using contains0 apply fastforce
-  using contains.simps by blast
-    
-lemma contains_ex2:
-  assumes "a = AALTs bs1 [AZERO, AONE bs2, AALTs bs5 [AONE bs3, AZERO, AONE bs4]]" "a >> bs" 
-  shows "bsimp a >> bs"
-  using assms
-  apply(simp)
-  apply(erule contains.cases)
-        apply(auto)
-  using contains.simps apply blast
-  apply(erule contains.cases)
-        apply(auto)
-  using contains3b apply blast
-   apply(erule contains.cases)
-        apply(auto)
-  apply(erule contains.cases)
-         apply(auto)
-  apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
-  apply(erule contains.cases)
-         apply(auto)
-  using contains.simps apply blast
-  apply(erule contains.cases)
-         apply(auto)
-  apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
-      apply(erule contains.cases)
-         apply(auto)
-apply(erule contains.cases)
-         apply(auto)
-  done
 
 lemma contains48:
   assumes "\<And>x2aa bs bs1. \<lbrakk>x2aa \<in> set x2a; fuse bs x2aa >> bs @ bs1\<rbrakk> \<Longrightarrow> x2aa >> bs1" 
@@ -1926,6 +1893,39 @@
   using contains.intros(7) apply blast
   using contains48 by blast
 
+
+lemma contains50_IFF2:
+  shows "bsimp_AALTs bs [a] >> bs @ bs1 \<longleftrightarrow> fuse bs a >> bs @ bs1"
+  by simp
+
+lemma contains50_IFF3:
+  shows "bsimp_AALTs bs as >> bs @ bs1  \<longleftrightarrow> (\<exists>a \<in> set as. fuse bs a >> bs @ bs1)"
+apply(induct as arbitrary: bs bs1)
+   apply(simp)
+   apply(auto elim: contains.cases simp add: contains0)
+   apply(case_tac as)
+     apply(auto)
+  apply(case_tac list)
+     apply(auto)
+  apply(erule contains.cases)
+            apply(auto)
+      apply (simp add: contains0)
+apply(erule contains.cases)
+            apply(auto)
+  using contains0 apply auto[1]
+  apply(erule contains.cases)
+           apply(auto)
+ apply(erule contains.cases)
+          apply(auto)
+  using contains0 apply blast
+  apply (metis bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) contains.intros(4) contains49 list.exhaust)
+  by (smt bsimp_AALTs.simps(3) contains.intros(4) contains.intros(5) contains49 list.set_cases)
+  
+lemma contains50_IFF4:
+  shows "bsimp_AALTs bs as >> bs @ bs1  \<longleftrightarrow> (\<exists>a \<in> set as. a >> bs1)"
+  by (meson contains0 contains49 contains50_IFF3)
+  
+  
 lemma contains50:
   assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
   shows "bsimp_AALTs bs (rs1 @ rs2) >> bs @ bs1"
@@ -1995,7 +1995,6 @@
    apply(simp)
   using contains51a by fastforce
 
-
 lemma contains51c:
   assumes "AALTs (bs @ bs2) rs >> bs @ bs1"
   shows "bsimp_AALTs bs (map (fuse bs2) rs) >> bs @ bs1"
@@ -2642,6 +2641,15 @@
   apply(simp)
   done
 
+lemma bders_bsimp_AALTs:
+  shows "bders (bsimp_AALTs bs rs) s = bsimp_AALTs bs (map (\<lambda>a. bders a s) rs)"
+  apply(induct s arbitrary: bs rs rule: rev_induct)
+    apply(simp)
+  apply(simp add: bders_append)
+  apply(simp add: bder_bsimp_AALTs)
+  apply(simp add: comp_def)
+  done
+
 lemma flts_nothing:
   assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
   shows "flts rs = rs"
@@ -3088,6 +3096,7 @@
 definition PX where
   "PX r s = PV r s (mkeps (ders s r))"
 
+
 lemma FE_PX:
   shows "FE r s = retrieve r (PX (erase r) s)"
   unfolding FE_def PX_def PV_def by(simp)
@@ -3298,6 +3307,14 @@
   apply(simp)
   done
 
+lemma FC_bders_iff2:
+  assumes "\<Turnstile> v : ders (c # s) (erase r)"
+  shows "bders r (c # s) >> FC r (c # s) v \<longleftrightarrow> bders (bder c r) s >> FC (bder c r) s v"
+  apply(subst FC_bders_iff)
+  using assms apply simp
+  by (metis FC_def assms contains7b contains8_iff ders.simps(2) erase_bder)
+
+
 lemma FC_bnullable0:
   assumes "bnullable r"
   shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))"
@@ -3358,38 +3375,6 @@
   shows "r >> FE (bsimp (bders r s)) []"
   using FE_bnullable0 FE_contains2 assms by auto
   
-
-(*
-lemma FE_bnullable2:
-  assumes "bnullable (bder c r)"
-  shows "FE r [c] = FE (bsimp r) [c]"
-  unfolding FE_def
-  apply(simp)
-  using L0
-
-  apply(subst FE_nullable1)
-  using assms apply(simp)
-  apply(subst FE_bnullable0)
-  using assms apply(simp)
-  unfolding FE_def
-  apply(simp)
-  apply(subst L0)
-  using assms apply(simp)
-  apply(subst bder_retrieve[symmetric])
-  using LLLL(1) L_erase_bder_simp assms bnullable_correctness mkeps_nullable nullable_correctness apply b last
-  apply(simp)
-  find_theorems "retrieve _ (injval _ _ _)"
-  find_theorems "retrieve (bsimp _) _"
-
-  lemma FE_nullable3:
-  assumes "bnullable (bders a s)"
-  shows "FE (bsimp a) s = FE a s"
-  
-  unfolding FE_def
-  using LA assms bnullable_correctness mkeps_nullable by fas tforce
-*)
-
-
 lemma FC4:
   assumes "\<Turnstile> v : ders s (erase a)"
   shows "FC a s v = FC (bders a s) [] v"
@@ -3402,92 +3387,6 @@
   using L0 assms bnullable_correctness by auto 
 
 
-lemma FC6:
-  assumes "nullable (erase (bders a s))"
-  shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = FC a s (mkeps (erase (bders a s)))"
-  apply(subst (2) FC4)
-  using assms mkeps_nullable apply auto[1]
-  apply(subst FC_nullable2)
-  using assms bnullable_correctness apply blast
-  oops
-(*
-lemma FC_bnullable:
-  assumes "bnullable (bders r s)"
-  shows "FC r s (mkeps (erase r)) = FC (bsimp r) s (mkeps (erase (bsimp r)))"
-  using assms
-  unfolding FC_def
-  using L0 L0a bder_retrieve L02_bders L04
-
-  apply(induct s arbitrary: r)
-   apply(simp add: FC_id)
-  apply (simp add: L0 assms)
-  apply(simp add: bders_append)
-  apply(drule_tac x="bder a r" in meta_spec)
-  apply(drule meta_mp)
-   apply(simp)
-
-  apply(subst bder_retrieve[symmetric])
-  apply(simp)
-*)
-
-
-lemma FC_bnullable:
-  assumes "bnullable (bders r s)"
-  shows "FC r s (mkeps (ders s (erase r))) = FC (bsimp r) s (mkeps (ders s (erase (bsimp r))))"
-  unfolding FC_def
-  oops
-
-lemma AA0:
-  assumes "bnullable (bders r s)"
-  assumes "bders r s >> FC r s (mkeps (erase (bders r s)))"
-  shows "bders (bsimp r) s >> FC (bsimp r) s (mkeps (erase (bders (bsimp r) s)))"
-  using assms
-  apply(subst (asm) FC_bders_iff)
-   apply(simp)
-  using bnullable_correctness mkeps_nullable apply fastforce
-  apply(subst FC_bders_iff)
-   apply(simp)
-  apply (metis LLLL(1) bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
-  apply(simp add: PPP1_eq)
-  unfolding FC_def
-  find_theorems "retrieve (bsimp _) _"
-  using contains7b
-  oops
-
-
-lemma AA1:
-  
-  assumes "\<Turnstile> v : der c (erase r)" "\<Turnstile> v : der c (erase (bsimp r))" 
-  assumes "bder c r >> FC r [c] v"
-  shows "bder c (bsimp r) >> FC (bsimp r) [c] v"
-  using assms
-  apply(subst (asm) FC_bder_iff)
-  apply(rule assms)
-  apply(subst FC_bder_iff)
-   apply(rule assms)
-  apply(simp add: PPP1_eq)
-  unfolding FC_def
-  find_theorems "retrieve (bsimp _) _"
-  using contains7b
-  oops
-
-  
-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)
-  oops
-
 lemma in1:
   assumes "AALTs bsX rsX \<in> set rs"
   shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)"
@@ -3644,16 +3543,7 @@
   apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
   by (simp add: H7)
 
-(*
-lemma H8:
-  assumes "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
-  shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
-  apply(induct rs arbitrary: bs rule: flts.induct)
-        apply(auto)
-  apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)
-  apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
-  by (simp add: H7)
-*)
+
 
 lemma H2:
   assumes "r >> bs2" "r \<in> AALTs_subs (AALTs bs rs)" 
@@ -3729,126 +3619,129 @@
   apply (simp add: H1 TEMPLATE_contains61a)
   by (metis append_Cons append_Nil contains50 f_cont2)
 
-lemma HK1:
-  assumes "r \<in> AALTs_subs a"
-  shows "bsimp r \<in> AALTs_subs (bsimp a)"
-  using assms
-  apply(induct a arbitrary: r)
-       apply(auto)
-   apply(case_tac "a1 = AZERO")
-    apply(simp)
-  oops  
-
 lemma contains_equiv_def2:
   shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>(\<Union> (AALTs_subs ` set as)). a >> bs1)"
   by (metis H1 H3 UN_E UN_I contains0 contains49 contains59 contains60)
     
 lemma contains_equiv_def:
-  shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
+  shows "(AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
   by (meson contains0 contains49 contains59 contains60)
 
-lemma derc_alt00:
-  assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
-  shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
-  using assms
-  apply -
+lemma map_fuse2:
+  shows "map (bder c) (map (fuse bs) as) = map (fuse bs) (map (bder c) as)"
+  by (simp add: map_bder_fuse)
+
+lemma map_fuse3:
+  shows "map (\<lambda>a. bders a s) (map (fuse bs) as) = map (fuse bs) (map (\<lambda>a. bders a s) as)"
+  apply(induct s arbitrary: bs as rule: rev_induct)
+   apply(auto simp add: bders_append map_fuse2)
+  using bder_fuse by blast
+
+lemma bders_AALTs:
+  shows "bders (AALTs bs2 as) s = AALTs bs2 (map (\<lambda>a. bders a s) as)"
+  apply(induct s arbitrary: bs2 as rule: rev_induct)
+  apply(auto simp add: bders_append)
+  done
+
+lemma bders_AALTs_contains:
+  shows "bders (AALTs bs2 as) s >> bs2 @ bs \<longleftrightarrow> 
+         AALTs bs2 (map (\<lambda>a. bders a s) as) >> bs2 @ bs"
+  apply(induct s arbitrary: bs bs2 as)
+   apply(auto)[1]
+  apply(simp)
+  by (smt comp_apply map_eq_conv)
+
+
+lemma derc_alt00_Urb:
+  shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow>
+         fuse bs2 (bder c (bsimp a)) >> bs2 @ bs"
   apply(case_tac "bsimp a")
-  prefer 6
-       apply(simp)+
-  apply(subst bder_bsimp_AALTs)
-  by (metis append_Nil contains51c map_bder_fuse map_map)
-
-lemma derc_alt01:
-  shows "\<And>a list1 list2.
-       \<lbrakk> bder c (bsimp a) >> bs ;
-        bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = [];
-        flts (map bsimp list2) \<noteq> []\<rbrakk>
-       \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs"
-  using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce
-
-lemma derc_alt10:
-  shows "\<And>a list1 list2.
-       \<lbrakk>  a \<in> set as; bder c (bsimp a) >> bs;
-        bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> [];
-flts(map bsimp list2) = []\<rbrakk>
-       \<Longrightarrow> bder c (bsimp_AALTs []
-              (flts (map bsimp list1) @
-               flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs"
-  apply(subst bder_bsimp_AALTs)
-  apply simp
-  using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce
-
-
-lemma derc_alt:
-  assumes "bder c (AALTs [] as) >> bs" 
-   and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
-  shows "bder c (bsimp (AALTs [] as)) >> bs"
+  apply(auto)
+  apply(subst (asm) bder_bsimp_AALTs)
+   apply(subst (asm) map_fuse2)
+  using contains60 contains61 contains63 apply blast
+  by (metis bder_bsimp_AALTs contains51c map_bder_fuse map_map)
+
+lemma ders_alt00_Urb:
+  shows "bders (bsimp_AALTs bs2 (flts [bsimp a])) s >> bs2 @ bs \<longleftrightarrow>
+         fuse bs2 (bders (bsimp a) s) >> bs2 @ bs"
+      apply(case_tac "bsimp a")
+             apply (simp add: bders_AZERO(1))
+  using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(4) apply presburger
+  using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(5) apply presburger
+  using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(6) apply presburger
+   prefer 2
+  using bders_fuse bsimp_AALTs.simps(2) flts.simps(1) flts.simps(7) apply presburger
+  apply(auto simp add: bders_bsimp_AALTs)
+   apply(drule contains61)
+   apply(auto simp add: bders_AALTs) 
+   apply(rule contains63)
+   apply(rule contains60)
+   apply(auto)
+  using bders_fuse apply auto[1]
+  by (metis contains51c map_fuse3 map_map)
+    
+lemma derc_alt00_Urb2a:
+  shows "bder c (bsimp_AALTs bs2 (flts [bsimp a])) >> bs2 @ bs \<longleftrightarrow>
+         bder c (bsimp a) >> bs"
+  using contains0 contains49 derc_alt00_Urb by blast
+
+
+lemma derc_alt00_Urb2:
+  assumes "fuse bs2 (bder c (bsimp a)) >> bs2 @ bs" "a \<in> set as"
+  shows "bder c (bsimp_AALTs bs2 (flts (map bsimp as))) >> bs2 @ bs"
   using assms
-  apply -
-  using contains_equiv_def
-  apply -
-  apply(simp)
-  apply(drule_tac  x="[]" in meta_spec)
-  apply(drule_tac x="map (bder c) as" in meta_spec)
-  apply(drule_tac x="bs" in meta_spec)
-  
-  apply(simp)
-  apply(erule bexE)
   apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
    prefer 2
   using split_list_last apply fastforce
   apply(erule exE)+
-  apply(rule_tac t="as" and  s="list1@[a]@list2" in subst)
-   apply simp
-  (*find_theorems "map _ _ = _"*)
-  apply(subst map_append)+
-  apply(subst k00)+
-  apply(case_tac "flts (map bsimp list1) = Nil")
-  apply(case_tac "flts (map bsimp list2) = Nil")
-  apply simp
-  using derc_alt00 apply blast
-  apply simp
-  using derc_alt01 apply blast
-  apply(case_tac "flts (map bsimp list2) = Nil")
-  using derc_alt10 apply blast
-  by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append)
-
-  
+  apply(simp add: flts_append del: append.simps)
+  using bder_bsimp_AALTs contains50 contains51b derc_alt00_Urb by auto
+
+lemma ders_alt00_Urb2:
+  assumes "fuse bs2 (bders (bsimp a) s) >> bs2 @ bs" "a \<in> set as"
+  shows "bders (bsimp_AALTs bs2 (flts (map bsimp as))) s >> bs2 @ bs"
+  using assms
+  apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
+   prefer 2
+  using split_list_last apply fastforce
+  apply(erule exE)+
+  apply(simp add: flts_append del: append.simps)
+  apply(simp add: bders_bsimp_AALTs)
+  apply(rule contains50)
+  apply(rule contains51b)
+  using bders_bsimp_AALTs ders_alt00_Urb by auto
+
+
 lemma derc_alt2:
   assumes "bder c (AALTs bs2 as) >> bs2 @ bs" 
    and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
  shows "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
-proof -
-  from assms
-  have "bder c (AALTs [] as) >> bs"
-    by (metis bder.simps(4) contains_equiv_def self_append_conv2)
-  then have "bder c (bsimp (AALTs [] as)) >> bs"
-    using assms(2) derc_alt by blast
-  then show "bder c (bsimp (AALTs bs2 as)) >> bs2 @ bs"
-    by (metis bder_fuse bsimp_fuse_AALTs contains0) 
-qed  
-
-lemma inA:
-  assumes "x \<in> set rs" "bder c (bsimp x) >> bs"
-  shows "\<exists>y. y \<in> set (flts (map bsimp rs))"
   using assms
-  apply(induct rs arbitrary: x c bs)
-   apply(auto)
-   apply(case_tac "bsimp a = AZERO")
-  apply (metis append.left_neutral bder.simps(1) bsimp_AALTs.simps(1) contains61 in_set_conv_decomp neq_Nil_conv)
-  apply (metis bsimp_AALTs.simps(1) flts4 good1 list.set_intros(1) neq_Nil_conv)
-  by (metis Nil_is_append_conv k0 list.set_intros(1) neq_Nil_conv)
-
-
-lemma inB:
-  assumes "a \<noteq> AZERO" "good a"
-  shows "AALTs_subs a \<noteq> {}"
+  apply -
+  apply(simp)
+  apply(subst (asm) contains_equiv_def)
+  apply(simp)
+  apply(erule bexE)
+  using contains0 derc_alt00_Urb2 by blast
+
+
+
+lemma ders_alt2:
+  assumes "bders (AALTs bs2 as) s >> bs2 @ bs" 
+   and "\<forall>a \<in> set as. ((bders a s >> bs) \<longrightarrow> (bders (bsimp a) s >> bs))"
+ shows "bders (bsimp (AALTs bs2 as)) s >> bs2 @ bs"
   using assms
-  apply(induct a)
-       apply(auto)
-  apply(erule good.elims)
-                      apply(auto)
-  by (metis empty_iff good.simps(1) good_fuse nn11a nonalt_10)
+  apply -
+  apply(simp add: bders_AALTs)
+  thm contains_equiv_def
+  apply(subst (asm) contains_equiv_def)
+  apply(simp)
+  apply(erule bexE)
+  using contains0 ders_alt00_Urb2 by blast
+
+
+
 
 lemma bder_simp_contains:
   assumes "bder c a >> bs"
@@ -3930,34 +3823,217 @@
   apply(rule derc_alt2[simplified])
    apply(simp)
   by blast
+
   
-lemma CONTAINS1:
-  assumes "a >> bs"
-  shows "a >>2 bs"
+
+lemma bder_simp_containsA:
+  assumes "bder c a >> bs"
+  shows "bsimp (bder c (bsimp a)) >> bs"
+  using assms
+  by (simp add: bder_simp_contains contains55)
+
+lemma bder_simp_containsB:
+  assumes "bsimp (bder c a) >> bs"
+  shows "bder c (bsimp a) >> bs"
+  using assms
+  by (simp add: PPP1_eq bder_simp_contains)
+    
+lemma bder_simp_contains_IFF:
+  assumes "good a"
+  shows "bsimp (bder c a) >> bs \<longleftrightarrow> bder c (bsimp a) >> bs"
+  using assms
+  by (simp add: PPP1_eq test2)  
+
+
+lemma ders_seq:
+  assumes "bders (ASEQ bs a1 a2) s >> bs @ bs2"
+  and "\<And>s bs. bders a1 s >> bs \<Longrightarrow> bders (bsimp a1) s >> bs"
+      "\<And>s bs. bders a2 s >> bs \<Longrightarrow> bders (bsimp a2) s >> bs"
+    shows "bders (ASEQ bs (bsimp a1) (bsimp a2)) s >> bs @ bs2"
+  using assms(1)  
+  apply(induct s arbitrary: a1 a2 bs bs2 rule: rev_induct)
+   apply(auto)[1]
+  thm CT1_SEQ PPP1_eq
+  apply (metis CT1_SEQ PPP1_eq)
+  apply(auto simp add: bders_append)  
+  apply(drule bder_simp_contains)
+  oops
+
+
+lemma bders_simp_contains:
+  assumes "bders a s >> bs"
+  shows "bders (bsimp a) s >> bs"
+ using assms
+  apply(induct a arbitrary: s bs)
+       apply(auto elim: contains.cases)[4]
+   prefer 2  
+   apply(subgoal_tac "\<exists>bsX. bs = x1 @ bsX")
+    prefer 2
+  apply (metis bders_AALTs contains59 f_cont1)
+  apply(clarify)
+  apply(rule ders_alt2)
+    apply(assumption)
+   apply(auto)[1]
+  prefer 2
+  apply simp
+  (* SEQ case *)
+  apply(case_tac "bsimp a1 = AZERO")
+  apply(simp)
+  apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2)
+    apply(case_tac "bsimp a2 = AZERO")
+  apply(simp)
+  apply (metis LLLL(1) bders_AZERO(1) bsimp.simps(1) bsimp.simps(3) bsimp_ASEQ0 contains55 ders_correctness erase_bders good.simps(1) good1a xxx_bder2)
+  apply(case_tac "\<exists>bsX. bsimp a1 = AONE bsX")
+  apply(auto)
+  apply(subst bsimp_ASEQ2)
+  apply(case_tac s)
+   apply(simp)
+   apply (metis b1 bsimp.simps(1) contains55)
+  apply(simp)
+   apply(subgoal_tac "bnullable a1")
+    prefer 2
+  using b3 apply fastforce
+  apply(auto)
+   apply(subst (asm) bders_AALTs)
+  apply(erule contains.cases)
+             apply(auto)
+  prefer 2
+  apply(erule contains.cases)
+          apply(auto)
+  apply(simp add: fuse_append)
+     apply(simp add: bder_fuse bders_fuse)
+apply (metis bders.simps(2) bmkeps.simps(1) bmkeps_simp contains0 contains49 f_cont1)
+  using contains_equiv_def apply auto[1]
+   apply(simp add: bder_fuse bders_fuse fuse_append)
+   apply(rule contains0)
+  oops
+  
+  
+lemma T0:
+  assumes "s = []"
+  shows "bders (bsimp r) s >> bs \<longleftrightarrow> bders r s >> bs"
+  using assms
+  by (simp add: PPP1_eq test2)  
+
+lemma T1:
+  assumes "s = [a]" "bders r s >> bs"
+  shows "bders (bsimp r) s >> bs"
   using assms
-  apply(induct a bs)
-  apply(auto intro: contains2.intros)
-  done
-
-lemma CONTAINS2:
-  assumes "a >>2 bs"
-  shows "a >> bs"
+  apply(simp)
+  by (simp add: bder_simp_contains)
+
+lemma TX:
+  assumes "\<Turnstile> v : ders s (erase r)" "\<Turnstile> v : ders s (erase (bsimp r))"
+  shows "bders r s >>  FC r s v \<longleftrightarrow> bders (bsimp r) s >> FC (bsimp r) s v"
+  using FC_def contains7b 
+  using assms by metis
+
+lemma mkeps1:
+  assumes "s \<in> L (erase r)"
+  shows "\<Turnstile> mkeps (ders s (erase r)) : ders s (erase r)"
+  using assms
+  by (meson lexer_correct_None lexer_flex mkeps_nullable)
+  
+lemma mkeps2:
+  assumes "s \<in> L (erase r)"
+  shows "\<Turnstile> mkeps (ders s (erase (bsimp r))) : ders s (erase (bsimp r))"
+  using assms
+  by (metis LLLL(1) lexer_correct_None lexer_flex mkeps_nullable)
+
+thm FC_def FE_def PX_def PV_def
+
+
+lemma TX2:
+  assumes "s \<in> L (erase r)"
+  shows "bders r s >>  FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bsimp r) s"
+  using assms
+  by (simp add: FE_def contains7b mkeps1 mkeps2)
+
+lemma TX3:
+  assumes "s \<in> L (erase r)"
+  shows "bders r s >>  FE r s \<longleftrightarrow> bders (bsimp r) s >> FE (bders (bsimp r) s) []"
   using assms
-  apply(induct a bs)
-  apply(auto intro: contains.intros)
-  using contains55 by auto
-
-lemma CONTAINS2_IFF:
-  shows "a >> bs \<longleftrightarrow> a >>2 bs"
-  using CONTAINS1 CONTAINS2 by blast
+  by (metis FE_PX FE_def L07 LLLL(1) PX_id TX2)
+  
+find_theorems "FE _ _ = _"
+find_theorems "FC _ _ _ = _"
+find_theorems "(bder _ _ >> _ _ _ _) = _"
+
+
+(* HERE *)
+
+lemma PX:
+  assumes "s \<in> L r" 
+  shows "bders (intern r) s >> code (PX r s) \<Longrightarrow> bders (bsimp (intern r)) s >> code (PX r s)"
+  
+  using FC_def contains7b
+  using assms by me tis
+
+
+
+  
+  apply(simp)
+  (*using FC_bders_iff2[of _ _ "[b]", simplified]*)
+  apply(subst (asm) FC_bders_iff2[of _ _ "[b]", simplified])
+  apply(simp)
+  apply(subst (asm) FC_bder_iff)
+   apply(simp)
+  apply(drule bder_simp_contains)
+  using FC_bder_iff FC_bders_iff2 FC_bders_iff
+  apply(subst (asm) FC_bder_iff[symmetric])
+   apply(subst FC_bder_iff)
+    using FC_bder_iff
+  
+  
+  apply (simp add: bder_simp_contains)
+
+lemma bder_simp_contains_IFF2:
+  assumes "bders r s >> bs"
+  shows ""
+  using assms
+  apply(induct s arbitrary: r bs rule: rev_induct)
+   apply(simp)
+  apply (simp add: contains55)  
+  apply (simp add: bders_append bders_simp_append)
+   apply (simp add: PPP1_eq)
+  find_theorems "(bder _ _ >> _) = _"
+  apply(rule contains50)
+  
+  apply(case_tac "bders a xs = AZERO")
+   apply(simp)
+   apply(subgoal_tac "bders_simp a xs = AZERO")
+    prefer 2
+  apply (metis L_bders_simp XXX4a_good_cons bders.simps(1) bders_simp.simps(1) bsimp.simps(3) good.simps(1) good1a test2 xxx_bder2)
+   apply(simp)
+  apply(case_tac xs)
+  apply(simp)
+  apply (simp add: PPP1_eq)
+  apply(simp)
+  apply(subgoal_tac "good (bders_simp a (aa # list)) \<or> (bders_simp a (aa # list) = AZERO)")
+  apply(auto)
+      apply(subst (asm) bder_simp_contains_IFF)
+       apply(simp)
+  
+  
 
 lemma
-  assumes "bders (intern r) s >>2 bs"
-  shows   "bders_simp (intern r) s >>2 bs"
+  assumes "s \<in> L (erase r)"
+  shows "bders_simp r s >> bs \<longleftrightarrow> bders r s >> bs"
   using assms
   apply(induct s arbitrary: r bs)
    apply(simp)
+  apply(simp add: bders_append bders_simp_append)
+  apply(rule iffI)
+   apply(drule_tac x="bsimp (bder a r)" in meta_spec)
+  apply(drule_tac x="bs" in meta_spec)
+   apply(drule meta_mp)
+  using L_bsimp_erase lexer_correct_None apply fastforce
   apply(simp)
+    
+  
+   prefer 2
+  
+
   oops
 
 
@@ -4031,32 +4107,6 @@
   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)
-  oops
-
-
-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)
-  oops
-
-
 thm L07XX PPP0b erase_intern
 
 find_theorems "retrieve (bders _ _) _"