# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1566337348 -7200
# Node ID f139bdc0dcd53c3c2d17ee5f9738b19f83a3a84d
# Parent  f0e876ed43fa98e3edac65de63f7df86345424d2
updated contains

diff -r f0e876ed43fa -r f139bdc0dcd5 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded.thy	Tue Aug 20 23:42:28 2019 +0200
@@ -567,6 +567,9 @@
 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 | "flts (r1 # rs) = r1 # flts rs"
 
+
+
+
 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
   where
   "li _ [] = AZERO"
@@ -574,6 +577,8 @@
 | "li bs as = AALTs bs as"
 
 
+
+
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -1083,6 +1088,8 @@
         apply(auto)
   done
 
+
+
 lemma rt:
   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
   apply(induct rs)
@@ -1783,6 +1790,56 @@
        apply(simp_all)
   done
 
+
+fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
+  where 
+  "flts2 _ [] = []"
+| "flts2 c (AZERO # rs) = flts2 c rs"
+| "flts2 c (AONE _ # rs) = flts2 c rs"
+| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
+| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
+| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 
+    flts2 c rs
+    else ASEQ bs r1 r2 # flts2 c rs)"
+| "flts2 c (r1 # rs) = r1 # flts2 c rs"
+
+lemma  flts2_k0:
+  shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
+  apply(induct r arbitrary: c rs1)
+   apply(auto)
+  done
+
+lemma  flts2_k00:
+  shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
+  apply(induct rs1 arbitrary: rs2 c)
+   apply(auto)
+  by (metis append.assoc flts2_k0)
+
+
+lemma
+  shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
+  apply(induct c rs rule: flts2.induct)
+        apply(simp)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  apply(simp)
+    apply(auto simp add: bder_fuse)[1]
+  defer
+   apply(simp)
+  apply(simp del: flts2.simps)
+  apply(rule conjI)
+   prefer 2
+   apply(auto)[1]
+  apply(rule impI)
+  apply(subst flts2_k0)
+  apply(subst map_append)
+  apply(subst flts2.simps)
+  apply(simp only: flts2.simps)
+  apply(auto)
+
+
+
 lemma XXX2_helper:
   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
           "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2390,130 +2447,13 @@
     apply(auto)
   done
 
-lemma
-  assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
-   "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))" 
-          "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
-   shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
-  using assms
-  apply(induct x52 arbitrary: x51)
-   apply(simp)
-  oops
-  
-
-lemma
-  assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
-  shows "bsimp a = a"
-  using assms
-  apply(induct a taking: asize rule: measure_induct)
-  apply(case_tac x)
-       apply(simp_all)
-   apply(case_tac "(bsimp x42) = AZERO")
-    apply(simp add: asize0)
-  apply(case_tac "(bsimp x43) = AZERO")
-    apply(simp add: asize0)
-    apply (metis bsimp_ASEQ0)
-   apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
-    apply(auto)[1]
-    apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
-  apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
-  (* ALT case *)
-  apply(frule iii)
-  apply(case_tac x52)
-   apply(simp)
-  apply(simp)
-  apply(subst k0)
-  apply(subst (asm) k0)
-  apply(subst (asm) (2) k0)
-  apply(subst (asm) (3) k0)
-  apply(case_tac "(bsimp a) = AZERO")
-   apply(simp)
-  apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
-  apply(simp)
-  apply(case_tac "nonalt  (bsimp a)")
-   prefer 2
-  apply(drule_tac  x="AALTs x51 (bsimp a # list)" in  spec)
-   apply(drule mp)
-  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
-   apply(drule mp)  
-    apply(simp)
-  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
-   apply(drule mp)
-  apply(simp)
-  using bsimp_idem apply auto[1]
-    apply(simp add: bsimp_idem)
-  apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
-  apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
-  apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
-  prefer 2
-  using k0b apply blast
-  apply(clarify)
-  apply(simp only:)
-  apply(simp)
-  apply(case_tac "flts (map bsimp list) = Nil")
-   apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less) 
-  apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) =  AALTs x51 (bsimp a # flts (map bsimp list))")
-   prefer 2
-   apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
-  apply(auto)
-   apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
-  oops
-
-
-
-
-lemma OOO:
-  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
-  apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
-  apply(case_tac x)
-   apply(simp)
-  apply(simp)
-  apply(case_tac "a = AZERO")
-   apply(simp)
-  apply(case_tac "list")
-    apply(simp)
-  apply(simp)
-  apply(case_tac "bsimp a = AZERO")
-   apply(simp)
-  apply(case_tac "list")
-    apply(simp)
-    apply(simp add: bsimp_fuse[symmetric])
-  apply(simp)
-  apply(case_tac "nonalt (bsimp a)")
-  apply(case_tac list)
-  apply(simp)
-    apply(subst k0b)
-      apply(simp)
-     apply(simp)
-    apply(simp add: bsimp_fuse)
-   apply(simp)
-  apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
-   prefer 2
-  using bsimp_size le_neq_implies_less apply blast
-   apply(erule disjE)
-  apply(drule_tac x="(bsimp a) # list" in spec)
-  apply(drule mp)
-    apply(simp)
-   apply(simp)
-  apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
-    apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs  \<and> rs \<noteq> Nil \<and> length rs > 1")
-   prefer 2
-  apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
-  apply(auto)
-  oops
-
-
-lemma  
-  assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
-  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
-  using assms
-  apply(simp)
-  oops
-
-
+lemma CT1_SEQ:
+  shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
+  apply(simp add: bsimp_idem)
+  done
 
 lemma CT1:
-  shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map  bsimp as))"
+  shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map  bsimp as))"
   apply(induct as arbitrary: bs)
    apply(simp)
   apply(simp)
@@ -2523,6 +2463,21 @@
   shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
   by (metis CT1 list.simps(8) list.simps(9))
 
+lemma WWW2:
+  shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
+         bsimp_AALTs bs1 (flts (map bsimp as1))"
+  by (metis bsimp.simps(2) bsimp_idem)
+
+lemma CT1b:
+  shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
+  apply(induct bs as rule: bsimp_AALTs.induct)
+    apply(auto simp add: bsimp_idem)
+  apply (simp add: bsimp_fuse bsimp_idem)
+  by (metis bsimp_idem comp_apply)
+  
+  
+
+
 (* CT *)
 
 lemma CTU:
@@ -2531,7 +2486,7 @@
     apply(auto)
   done
 
-
+find_theorems "bder _ (bsimp_AALTs _ _)"
 
 lemma CTa:
   assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
@@ -2574,15 +2529,6 @@
   
 
 
-
-lemma 
-  shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
-          = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
-                             (map (fuse bs2) (map (bder c) as2))))"
-  apply(subst  bsimp_idem[symmetric])
-  apply(simp)
-  oops
-
 lemma CT_exp:
   assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
   shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
@@ -2641,10 +2587,6 @@
   using flts2 good1 apply fastforce
   by (smt ex_map_conv list.simps(9) nn1b nn1c)
 
-lemma WWW2:
-  shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
-         bsimp_AALTs bs1 (flts (map bsimp as1))"
-  by (metis bsimp.simps(2) bsimp_idem)
 
 lemma WWW3:
   shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
@@ -3019,12 +2961,17 @@
      apply(simp)
     prefer 3
     apply(simp)
+  (* SEQ case *)
+   apply(simp only:)
+   apply(subst CT1_SEQ)
+  apply(simp only: bsimp.simps)
+
   (* AALT case *)
    prefer 2
    apply(simp only:)
    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
     apply(clarify)
-  apply(simp del: bsimp.simps)
+    apply(simp del: bsimp.simps)
   apply(subst (2) CT1) 
     apply(simp del: bsimp.simps)
   apply(rule_tac t="bsimp (bder c a1)" and  s="bsimp (bder c (bsimp a1))" in subst)
@@ -3032,6 +2979,21 @@
   apply(rule_tac t="bsimp (bder c a2)" and  s="bsimp (bder c (bsimp a2))" in subst)
      apply(simp del: bsimp.simps)
     apply(subst  CT1a[symmetric])
+  (* \<rightarrow> *)
+  apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
+            and  s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
+     apply(simp)
+     apply(subst bsimp.simps)
+    apply(simp del: bsimp.simps bder.simps)
+
+    apply(subst bder_bsimp_AALTs)
+    apply(subst bsimp.simps)
+    apply(subst WWW2[symmetric])
+    apply(subst bsimp_AALTs_qq)
+  defer 
+    apply(subst bsimp.simps)
+    
+  (* <- *)
     apply(subst bsimp.simps)
     apply(simp del: bsimp.simps)
 (*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
@@ -3046,7 +3008,7 @@
        apply(simp del: bsimp.simps)
        apply(subst big0)
        apply(simp add: WWW4)
-  apply (metis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
+  apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
   oops
 
 lemma XXX2a_long_without_good:
diff -r f0e876ed43fa -r f139bdc0dcd5 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/BitCoded2.thy	Tue Aug 20 23:42:28 2019 +0200
@@ -641,6 +641,19 @@
 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
 | "bsimp r = r"
 
+
+inductive contains2 :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >>2 _" [51, 50] 50)
+  where
+  "AONE bs >>2 bs"
+| "ACHAR bs c >>2 bs"
+| "\<lbrakk>a1 >>2 bs1; a2 >>2 bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >>2 bs @ bs1 @ bs2"
+| "r >>2 bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
+| "AALTs bs rs >>2 bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
+| "ASTAR bs r >>2 bs @ [S]"
+| "\<lbrakk>r >>2 bs1; ASTAR [] r >>2 bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >>2 bs @ Z # bs1 @ bs2"
+| "r >>2 bs \<Longrightarrow> (bsimp r) >>2 bs"
+
+
 inductive contains :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >> _" [51, 50] 50)
   where
   "AONE bs >> bs"
@@ -678,6 +691,9 @@
   done
 
 
+
+
+
 lemma contains2:
   assumes "\<Turnstile> v : r"
   shows "(intern r) >> code v"
@@ -798,6 +814,7 @@
   using contains2[OF assms] retrieve_code[OF assms]
   by (simp)
 
+
 lemma contains6:
   assumes "\<Turnstile> v : (erase r)"
   shows "r >> retrieve r v"
@@ -844,6 +861,37 @@
   apply(simp)
   done
 
+lemma contains7b:
+  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: r v)
+   apply(simp)
+   apply (simp add: contains6)
+  apply(simp add: bders_append flex_append ders_append)
+  apply(drule_tac x="bder a r" in meta_spec)
+  apply(drule meta_spec)
+  apply(drule meta_mp)
+   apply(simp)
+  apply(simp)
+  apply(subst (asm) bder_retrieve)
+   defer
+  apply (simp add: flex_injval)
+  by (simp add: Prf_flex)
+
+lemma contains7_iff:
+  assumes "\<Turnstile> v : der c (erase r)"
+  shows "(bder c r) >> retrieve r (injval (erase r) c v) \<longleftrightarrow>
+                  r >> retrieve r (injval (erase r) c v)"
+  by (simp add: assms contains7 contains7a)
+
+lemma contains8_iff:
+  assumes "\<Turnstile> v : ders s (erase r)"
+  shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>
+                  r >> retrieve r (flex (erase r) id s v)"
+  using Prf_flex assms contains6 contains7b by blast
+
+
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -1826,13 +1874,13 @@
         apply(auto)
   apply(erule contains.cases)
          apply(auto)
-  apply (metis append.left_neutral contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
+  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 append.left_neutral contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
+  apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
       apply(erule contains.cases)
          apply(auto)
 apply(erule contains.cases)
@@ -2354,7 +2402,7 @@
 lemma L0:
   assumes "bnullable a"
   shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
-  using assms
+  using assms b3 bmkeps_retrieve bmkeps_simp bnullable_correctness
   by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)
 
 thm bmkeps_retrieve
@@ -3013,8 +3061,6 @@
   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)))"
@@ -3024,6 +3070,17 @@
 
 
 
+  
+  
+  
+  
+
+
+definition FC where
+ "FC a s v = retrieve a (flex (erase a) id s v)"
+
+definition FE where
+ "FE a s = retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))"
 
 definition PV where
   "PV r s v = flex r id s v"
@@ -3031,6 +3088,18 @@
 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)
+
+lemma FE_PX_code:
+  assumes "s \<in> L r"
+  shows "FE (intern r) s = code (PX r s)"
+  unfolding FE_def PX_def PV_def 
+  using assms
+  by (metis L07XX Posix_Prf erase_intern retrieve_code)
+  
+
 lemma PV_id[simp]:
   shows "PV r [] v = v"
   by (simp add: PV_def)
@@ -3129,6 +3198,7 @@
   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)"
@@ -3197,64 +3267,211 @@
          bder c (intern r) >> code (PX r (c # s1))"
   using PX2b PX3 assms by force
 
+
+lemma FC_id:
+  shows "FC r [] v = retrieve r v"
+  by (simp add: FC_def)
+
+lemma FC_char:
+  shows "FC r [c] v = retrieve r (injval (erase r) c v)"
+  by (simp add: FC_def)
+
+lemma FC_char2:
+  assumes "\<Turnstile> v : der c (erase r)"
+  shows "FC r [c] v = FC (bder c r) [] v"
+  using assms
+  by (simp add: FC_char FC_id bder_retrieve)
   
-  
+
+lemma FC_bders_iff:
+  assumes "\<Turnstile> v : ders s (erase r)"
+  shows "bders r s >> FC r s v \<longleftrightarrow> r >> FC r s v"
+  unfolding FC_def
+  by (simp add: assms contains8_iff)
+
+
+lemma FC_bder_iff:
+  assumes "\<Turnstile> v : der c (erase r)"
+  shows "bder c r >> FC r [c] v \<longleftrightarrow> r >> FC r [c] v"
+  apply(subst FC_bders_iff[symmetric])
+   apply(simp add: assms)
+  apply(simp)
+  done
+
+lemma FC_bnullable0:
+  assumes "bnullable r"
+  shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))"
+  unfolding FC_def 
+  by (simp add: L0 assms)
+
+
+lemma FC_nullable2:
+  assumes "bnullable (bders a s)"
+  shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = 
+         FC (bders (bsimp a) s) [] (mkeps (erase (bders (bsimp a) s)))"
+  unfolding FC_def
+  using L02_bders assms by auto
+
+lemma FC_nullable3:
+  assumes "bnullable (bders a s)"
+  shows "FC a s (mkeps (erase (bders a s))) = 
+         FC (bders a s) [] (mkeps (erase (bders a s)))"
+  unfolding FC_def
+  using LA assms bnullable_correctness mkeps_nullable by fastforce
+
+
+lemma FE_contains0:
+  assumes "bnullable r"
+  shows "r >> FE r []"
+  by (simp add: FE_def assms bnullable_correctness contains6 mkeps_nullable)
+
+lemma FE_contains1:
+  assumes "bnullable (bders r s)"
+  shows "r >> FE r s"
+  by (metis FE_def Prf_flex assms bnullable_correctness contains6 erase_bders mkeps_nullable)
+
+lemma FE_bnullable0:
+  assumes "bnullable r"
+  shows "FE r [] = FE (bsimp r) []"
+  unfolding FE_def 
+  by (simp add: L0 assms)
+
+
+lemma FE_nullable1:
+  assumes "bnullable (bders r s)"
+  shows "FE r s = FE (bders r s) []"
+  unfolding FE_def
+  using LA assms bnullable_correctness mkeps_nullable by fastforce
+
+lemma FE_contains2:
+  assumes "bnullable (bders r s)"
+  shows "r >> FE (bders r s) []"
+  by (metis FE_contains1 FE_nullable1 assms)
+
+lemma FE_contains3:
+  assumes "bnullable (bder c r)"
+  shows "r >> FE (bsimp (bder c r)) []"
+  by (metis FE_def L0 assms bder_retrieve bders.simps(1) bnullable_correctness contains7a erase_bder erase_bders flex.simps(1) id_apply mkeps_nullable)
+
+lemma FE_contains4:
+  assumes "bnullable (bders r s)"
+  shows "r >> FE (bsimp (bders r s)) []"
+  using FE_bnullable0 FE_contains2 assms by auto
   
 
-
-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 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"
+  unfolding FC_def by (simp add: LA assms)
+
+lemma FC5:
+  assumes "nullable (erase a)"
+  shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))"
+  unfolding FC_def
+  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 "[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"
+  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(induct a arbitrary: c bs)
-       apply(auto elim: contains.cases)
-   prefer 2
-   apply(erule contains.cases)
-         apply(auto)
+  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>
@@ -3269,9 +3486,183 @@
   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).   
+  oops
+
+lemma in1:
+  assumes "AALTs bsX rsX \<in> set rs"
+  shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)"
+  using assms
+  apply(induct rs arbitrary: bsX rsX)
+   apply(auto)
+  by (metis append_assoc in_set_conv_decomp k0)
+
+lemma in2a:
+  assumes "nonnested (bsimp r)" "\<not>nonalt(bsimp r)" 
+  shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)"
+  using assms
+  apply(induct r)
+       apply(auto)
+  by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2))
+  
+
+lemma in2:
+  assumes "bder c r >> bs2" and
+          "AALTs bsX rsX = bsimp r" and
+          "XX \<in> set rsX" "nonnested (bsimp r)"
+        shows "bder c (fuse bsX XX) >> bs2"
+  sorry  
+
+
+lemma
+  assumes "bder c a >> bs"
+  shows "bder c (bsimp a) >> bs"
+  using assms
+  apply(induct a arbitrary: c bs)
+       apply(auto elim: contains.cases)
+   apply(case_tac "bnullable a1")
+    apply(simp)
+  prefer 2
+    apply(simp)
+    apply(erule contains.cases)
+          apply(auto)
+    apply(case_tac "(bsimp a1) = AZERO")
+     apply(simp)
+     apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
+   apply(case_tac "(bsimp a2a) = AZERO")
+     apply(simp)
+  apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
+    apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+     apply(auto)[1]
+  using b3 apply fastforce
+    apply(subst bsimp_ASEQ1)
+  apply(auto)[3]
+    apply(simp)
+    apply(subgoal_tac  "\<not> bnullable (bsimp a1)")
+     prefer 2
+  using b3 apply blast
+    apply(simp)
+    apply (simp add: contains.intros(3) contains55)
+  (* SEQ nullable case *)
+   apply(erule contains.cases)
+         apply(auto)
+   apply(erule contains.cases)
+          apply(auto)
+   apply(case_tac "(bsimp a1) = AZERO")
+     apply(simp)
+     apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
+   apply(case_tac "(bsimp a2a) = AZERO")
+     apply(simp)
+  apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
+    apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+     apply(auto)[1]
+  using contains.simps apply blast
+    apply(subst bsimp_ASEQ1)
+  apply(auto)[3]
+    apply(simp)
+  apply(subgoal_tac  "bnullable (bsimp a1)")
+     prefer 2
+  using b3 apply blast
+    apply(simp)
+  apply (metis contains.intros(3) contains.intros(4) contains55 self_append_conv2)
+   apply(erule contains.cases)
+         apply(auto)
+  apply(case_tac "(bsimp a1) = AZERO")
+     apply(simp)
+  using b3 apply force
+   apply(case_tac "(bsimp a2) = AZERO")
+     apply(simp)
+  apply (metis bder.simps(1) bsimp_ASEQ0 bsimp_ASEQ_fuse contains0 contains49 f_cont1)    
+  apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
+     apply(auto)[1]
+  apply (metis append_assoc bder_fuse bmkeps.simps(1) bmkeps_simp bsimp_ASEQ2 contains0 contains49 f_cont1)
+   apply(subst bsimp_ASEQ1)
+       apply(auto)[3]
+    apply(simp)
+   apply(subgoal_tac  "bnullable (bsimp a1)")
+     prefer 2
+  using b3 apply blast
+    apply(simp)
+  apply (metis bmkeps_simp contains.intros(4) contains.intros(5) contains0 contains49 f_cont1)
+       apply(erule contains.cases)
+         apply(auto)
+  (* ALT case *)
+  apply(drule contains59)
+  apply(auto)
+  apply(subst bder_bsimp_AALTs)
+  apply(rule contains61a)
+  apply(auto)
+  apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
+   prefer 2
+   apply simp
+  apply(case_tac "bsimp r = AZERO")
+  apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last)
+  apply(subgoal_tac "nonnested (bsimp r)")  
+   prefer 2
+  using nn1b apply blast
+  apply(case_tac "nonalt (bsimp r)")
+   apply(rule_tac x="bsimp r" in bexI)
+    apply (metis contains0 contains49 f_cont1)
+   apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b)
+  (* AALTS case *)
+  apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)")
+   prefer 2
+  apply (metis n0 nonalt.elims(3))
+  apply(auto)
+ apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
+   prefer 2
+  apply (metis imageI list.set_map)
+  apply(simp)
+  apply(simp add: image_def)
+  apply(erule bexE)
+  apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)")
+   prefer 2
+  apply simp
+  apply(drule in1)
+  apply(subgoal_tac "rsX \<noteq> []")
+   prefer 2
+   apply (metis arexp.distinct(7) good.simps(4) good1)
+  apply(subgoal_tac "\<exists>XX. XX \<in> set rsX")
+   prefer 2
+  using neq_Nil_conv apply fastforce
+  apply(erule exE)
+  apply(rule_tac x="fuse bsX XX" in bexI)
+   prefer 2
+   apply blast
+  apply(frule f_cont1)
+  apply(auto)
+  apply(rule contains0)
+  apply(drule contains49)
+  by (simp add: in2)
+
+lemma CONTAINS1:
+  assumes "a >> bs"
+  shows "a >>2 bs"
+  using assms
+  apply(induct a bs)
+  apply(auto intro: contains2.intros)
+  done
+
+lemma CONTAINS2:
+  assumes "a >>2 bs"
+  shows "a >> bs"
+  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
+
+lemma
+  assumes "bders (intern r) s >>2 bs"
+  shows   "bders_simp (intern r) s >>2 bs"
+  using assms
+  apply(induct s arbitrary: r bs)
+   apply(simp)
+  apply(simp)
+  oops
+
 
 lemma
   assumes "s \<in> L r"
@@ -3286,7 +3677,7 @@
 find_theorems "retrieve (bders _ _) _"
 find_theorems "_ >> retrieve _ _"
 find_theorems "bsimp _ >> _"
-
+  oops
 
 
 lemma PX4a: 
@@ -3311,49 +3702,6 @@
 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)"
@@ -3395,7 +3743,7 @@
   apply(rule Etrans)
   thm contains7
   apply(rule contains7)
-
+  oops
 
 
 lemma contains70:
@@ -3409,7 +3757,7 @@
   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
@@ -3419,560 +3767,6 @@
 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)"
@@ -3981,158 +3775,6 @@
 
 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
-  apply(induct s arbitrary: r v rule: rev_induct)
-   apply(simp)
-   apply (simp add: Posix_Prf contains2)
-  apply(simp add: bders_append ders_append flex_append)
-  apply(frule Prf_injval)
-  apply(drule meta_spec)
-  apply(drule meta_spec)
-  apply(drule meta_mp)
-   apply(assumption)
-  apply(subst retrieve_code)
-   apply(assumption)
-  apply(subst (asm) retrieve_code)
-   apply(assumption)
-
-  using contains7 contains7a contains6 retrieve_code
-  apply(rule contains7)
-  
-  find_theorems "bder _ _ >> _"
-  find_theorems "code _ = _"
-  find_theorems "\<Turnstile> _ : der _ _"
-  
-  
-
-  find_theorems "_ >> (code _)"
-  apply(induct s arbitrary: a bs rule: rev_induct)
-   apply(simp)
-  apply(simp add: bders_simp_append bders_append)
-  apply(rule contains55)
-  find_theorems "bder _ _ >> _"
-  apply(drule_tac x="bder a aa" in meta_spec)
-  apply(drule_tac x="bs" in meta_spec)
-  apply(simp)
-  apply(rule contains55)
-  find_theorems "bsimp _ >> _"
-
-lemma XXX4:
-  assumes "good a"
-  shows "bders_simp a s = bsimp (bders a s)"
-  using  assms
-  apply(induct s arbitrary: a rule: rev_induct)
-   apply(simp)
-   apply (simp add: test2)
-  apply(simp add: bders_append bders_simp_append)
-  oops
-
-
-lemma MAINMAIN:
-  "blexer r s = blexer_simp r s"
-  apply(induct s arbitrary: r)
-  apply(simp add: blexer_def blexer_simp_def)
-  apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps)
-  apply(auto simp del: bders.simps bders_simp.simps)
-    prefer 2
-  apply (metis b4 bders.simps(2) bders_simp.simps(2))
-   prefer 2
-  apply (metis b4 bders.simps(2))
-  apply(subst bmkeps_simp)
-   apply(simp)
-  apply(case_tac s)
-   apply(simp only: bders.simps)
-   apply(subst bders_simp.simps)
-  apply(simp)
-  oops   
-
 
 lemma
   fixes n :: nat
diff -r f0e876ed43fa -r f139bdc0dcd5 thys/Lexer.thy
--- a/thys/Lexer.thy	Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/Lexer.thy	Tue Aug 20 23:42:28 2019 +0200
@@ -286,6 +286,11 @@
   apply(simp_all add: comp_def)
   by meson
 
+lemma flex_fun_apply2:
+  shows "g (flex r id s v) = flex r g s v"
+  by (simp add: flex_fun_apply)
+
+
 lemma flex_append:
   shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
   apply(induct s1 arbitrary: s2 r f)
@@ -397,7 +402,14 @@
   shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"
   by (simp add: flex_fun_apply)
   
-
-
+lemma Prf_flex:
+  assumes "\<Turnstile> v : ders s r"
+  shows "\<Turnstile> flex r id s v : r"
+  using assms
+  apply(induct s arbitrary: v r)
+  apply(simp)
+  apply(simp)
+  by (simp add: Prf_injval flex_injval)
+  
 
 end
\ No newline at end of file