
theory BitCoded2CT
  imports "Lexer" 
begin

section \<open>Bit-Encodings\<close>

datatype bit = Z | S

fun 
  code :: "val \<Rightarrow> bit list"
where
  "code Void = []"
| "code (Char c) = []"
| "code (Left v) = Z # (code v)"
| "code (Right v) = S # (code v)"
| "code (Seq v1 v2) = (code v1) @ (code v2)"
| "code (Stars []) = [S]"
| "code (Stars (v # vs)) =  (Z # code v) @ code (Stars vs)"


fun 
  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)"
where
  "decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CHAR d) = (Char d, ds)"
| "decode' [] (ALT r1 r2) = (Void, [])"
| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
                             let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
| "decode' [] (STAR r) = (Void, [])"
| "decode' (S # ds) (STAR r) = (Stars [], ds)"
| "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in
                                    let (vs, ds'') = decode' ds' (STAR r) 
                                    in (Stars_add v vs, ds''))"
by pat_completeness auto

lemma decode'_smaller:
  assumes "decode'_dom (ds, r)"
  shows "length (snd (decode' ds r)) \<le> length ds"
using assms
apply(induct ds r)
apply(auto simp add: decode'.psimps split: prod.split)
using dual_order.trans apply blast
by (meson dual_order.trans le_SucI)

termination "decode'"  
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 
apply(auto dest!: decode'_smaller)
by (metis less_Suc_eq_le snd_conv)

definition
  decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"
where
  "decode ds r \<equiv> (let (v, ds') = decode' ds r 
                  in (if ds' = [] then Some v else None))"

lemma decode'_code_Stars:
  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" 
  shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
  using assms
  apply(induct vs)
  apply(auto)
  done

lemma decode'_code:
  assumes "\<Turnstile> v : r"
  shows "decode' ((code v) @ ds) r = (v, ds)"
using assms
  apply(induct v r arbitrary: ds) 
  apply(auto)
  using decode'_code_Stars by blast

lemma decode_code:
  assumes "\<Turnstile> v : r"
  shows "decode (code v) r = Some v"
  using assms unfolding decode_def
  by (smt append_Nil2 decode'_code old.prod.case)


section {* Annotated Regular Expressions *}

datatype arexp = 
  AZERO
| AONE "bit list"
| ACHAR "bit list" char
| ASEQ "bit list" arexp arexp
| AALTs "bit list" "arexp list"
| ASTAR "bit list" arexp

abbreviation
  "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"

fun asize :: "arexp \<Rightarrow> nat" where
  "asize AZERO = 1"
| "asize (AONE cs) = 1" 
| "asize (ACHAR cs c) = 1"
| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
| "asize (ASTAR cs r) = Suc (asize r)"

fun 
  erase :: "arexp \<Rightarrow> rexp"
where
  "erase AZERO = ZERO"
| "erase (AONE _) = ONE"
| "erase (ACHAR _ c) = CHAR c"
| "erase (AALTs _ []) = ZERO"
| "erase (AALTs _ [r]) = (erase r)"
| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
| "erase (ASTAR _ r) = STAR (erase r)"

lemma decode_code_erase:
  assumes "\<Turnstile> v : (erase  a)"
  shows "decode (code v) (erase a) = Some v"
  using assms
  by (simp add: decode_code) 


fun nonalt :: "arexp \<Rightarrow> bool"
  where
  "nonalt (AALTs bs2 rs) = False"
| "nonalt r = True"


fun good :: "arexp \<Rightarrow> bool" where
  "good AZERO = False"
| "good (AONE cs) = True" 
| "good (ACHAR cs c) = True"
| "good (AALTs cs []) = False"
| "good (AALTs cs [r]) = False"
| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
| "good (ASEQ _ AZERO _) = False"
| "good (ASEQ _ (AONE _) _) = False"
| "good (ASEQ _ _ AZERO) = False"
| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
| "good (ASTAR cs r) = True"




fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
  "fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)" 
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"

lemma fuse_append:
  shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
  apply(induct r)
  apply(auto)
  done


fun intern :: "rexp \<Rightarrow> arexp" where
  "intern ZERO = AZERO"
| "intern ONE = AONE []"
| "intern (CHAR c) = ACHAR [] c"
| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                (fuse [S]  (intern r2))"
| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
| "intern (STAR r) = ASTAR [] (intern r)"


fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
  "retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
| "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
| "retrieve (ASTAR bs r) (Stars (v#vs)) = 
     bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"



fun
 bnullable :: "arexp \<Rightarrow> bool"
where
  "bnullable (AZERO) = False"
| "bnullable (AONE bs) = True"
| "bnullable (ACHAR bs c) = False"
| "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
| "bnullable (ASTAR bs r) = True"

fun 
  bmkeps :: "arexp \<Rightarrow> bit list"
where
  "bmkeps(AONE bs) = bs"
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
| "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
| "bmkeps(ASTAR bs r) = bs @ [S]"


fun
 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
where
  "bder c (AZERO) = AZERO"
| "bder c (AONE bs) = AZERO"
| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
| "bder c (ASEQ bs r1 r2) = 
     (if bnullable r1
      then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
      else ASEQ bs (bder c r1) r2)"
| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"


fun 
  bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
  "bders r [] = r"
| "bders r (c#s) = bders (bder c r) s"

lemma bders_append:
  "bders r (s1 @ s2) = bders (bders r s1) s2"
  apply(induct s1 arbitrary: r s2)
  apply(simp_all)
  done

lemma bnullable_correctness:
  shows "nullable (erase r) = bnullable r"
  apply(induct r rule: erase.induct)
  apply(simp_all)
  done

lemma erase_fuse:
  shows "erase (fuse bs r) = erase r"
  apply(induct r rule: erase.induct)
  apply(simp_all)
  done

lemma erase_intern [simp]:
  shows "erase (intern r) = r"
  apply(induct r)
  apply(simp_all add: erase_fuse)
  done

lemma erase_bder [simp]:
  shows "erase (bder a r) = der a (erase r)"
  apply(induct r rule: erase.induct)
  apply(simp_all add: erase_fuse bnullable_correctness)
  done

lemma erase_bders [simp]:
  shows "erase (bders r s) = ders s (erase r)"
  apply(induct s arbitrary: r )
  apply(simp_all)
  done

lemma retrieve_encode_STARS:
  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
  shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
  using assms
  apply(induct vs)
  apply(simp_all)
  done

lemma retrieve_fuse2:
  assumes "\<Turnstile> v : (erase r)"
  shows "retrieve (fuse bs r) v = bs @ retrieve r v"
  using assms
  apply(induct r arbitrary: v bs)
         apply(auto elim: Prf_elims)[4]
   defer
  using retrieve_encode_STARS
   apply(auto elim!: Prf_elims)[1]
   apply(case_tac vs)
    apply(simp)
   apply(simp)
  (* AALTs  case *)
  apply(simp)
  apply(case_tac x2a)
   apply(simp)
   apply(auto elim!: Prf_elims)[1]
  apply(simp)
   apply(case_tac list)
   apply(simp)
  apply(auto)
  apply(auto elim!: Prf_elims)[1]
  done

lemma retrieve_fuse:
  assumes "\<Turnstile> v : r"
  shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
  using assms 
  by (simp_all add: retrieve_fuse2)


lemma retrieve_code:
  assumes "\<Turnstile> v : r"
  shows "code v = retrieve (intern r) v"
  using assms
  apply(induct v r )
  apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
  done

lemma r:
  assumes "bnullable (AALTs bs (a # rs))"
  shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
  using assms
  apply(induct rs)
   apply(auto)
  done

lemma r0:
  assumes "bnullable a" 
  shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
  using assms
  by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)

lemma r1:
  assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"
  shows  "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"
  using assms
  apply(induct rs)
   apply(auto)
  done

lemma r2:
  assumes "x \<in> set rs" "bnullable x"
  shows "bnullable (AALTs bs rs)"
  using assms
  apply(induct rs)
   apply(auto)
  done

lemma  r3:
  assumes "\<not> bnullable r" 
          " \<exists> x \<in> set rs. bnullable x"
  shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
         retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
  using assms
  apply(induct rs arbitrary: r bs)
   apply(auto)[1]
  apply(auto)
  using bnullable_correctness apply blast
    apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
   apply(subst retrieve_fuse2[symmetric])
  apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
   apply(simp)
  apply(case_tac "bnullable a")
  apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
  apply(drule_tac x="a" in meta_spec)
  apply(drule_tac x="bs" in meta_spec)
  apply(drule meta_mp)
   apply(simp)
  apply(drule meta_mp)
   apply(auto)
  apply(subst retrieve_fuse2[symmetric])
  apply(case_tac rs)
    apply(simp)
   apply(auto)[1]
      apply (simp add: bnullable_correctness)
  apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
    apply (simp add: bnullable_correctness)
  apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
  apply(simp)
  done


lemma t: 
  assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
          "nullable (erase (AALTs bs rs))"
  shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
  using assms
  apply(induct rs arbitrary: bs)
   apply(simp)
  apply(auto simp add: bnullable_correctness)
   apply(case_tac rs)
     apply(auto simp add: bnullable_correctness)[2]
   apply(subst r1)
     apply(simp)
    apply(rule r2)
     apply(assumption)
    apply(simp)
   apply(drule_tac x="bs" in meta_spec)
   apply(drule meta_mp)
    apply(auto)[1]
   prefer 2
  apply(case_tac "bnullable a")
    apply(subst r0)
     apply blast
    apply(subgoal_tac "nullable (erase a)")
  prefer 2
  using bnullable_correctness apply blast
  apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
  apply(subst r1)
     apply(simp)
  using r2 apply blast
  apply(drule_tac x="bs" in meta_spec)
   apply(drule meta_mp)
    apply(auto)[1]
   apply(simp)
  using r3 apply blast
  apply(auto)
  using r3 by blast

lemma bmkeps_retrieve:
  assumes "nullable (erase r)"
  shows "bmkeps r = retrieve r (mkeps (erase r))"
  using assms
  apply(induct r)
         apply(simp)
        apply(simp)
       apply(simp)
    apply(simp)
   defer
   apply(simp)
  apply(rule t)
   apply(auto)
  done

lemma bder_retrieve:
  assumes "\<Turnstile> v : der c (erase r)"
  shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
  using assms
  apply(induct r arbitrary: v rule: erase.induct)
         apply(simp)
         apply(erule Prf_elims)
        apply(simp)
        apply(erule Prf_elims) 
        apply(simp)
      apply(case_tac "c = ca")
       apply(simp)
       apply(erule Prf_elims)
       apply(simp)
      apply(simp)
       apply(erule Prf_elims)
  apply(simp)
      apply(erule Prf_elims)
     apply(simp)
    apply(simp)
  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
    apply(erule Prf_elims)
     apply(simp)
    apply(simp)
    apply(case_tac rs)
     apply(simp)
    apply(simp)
  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
   apply(simp)
   apply(case_tac "nullable (erase r1)")
    apply(simp)
  apply(erule Prf_elims)
     apply(subgoal_tac "bnullable r1")
  prefer 2
  using bnullable_correctness apply blast
    apply(simp)
     apply(erule Prf_elims)
     apply(simp)
   apply(subgoal_tac "bnullable r1")
  prefer 2
  using bnullable_correctness apply blast
    apply(simp)
    apply(simp add: retrieve_fuse2)
    apply(simp add: bmkeps_retrieve)
   apply(simp)
   apply(erule Prf_elims)
   apply(simp)
  using bnullable_correctness apply blast
  apply(rename_tac bs r v)
  apply(simp)
  apply(erule Prf_elims)
     apply(clarify)
  apply(erule Prf_elims)
  apply(clarify)
  apply(subst injval.simps)
  apply(simp del: retrieve.simps)
  apply(subst retrieve.simps)
  apply(subst retrieve.simps)
  apply(simp)
  apply(simp add: retrieve_fuse2)
  done
  


lemma MAIN_decode:
  assumes "\<Turnstile> v : ders s r"
  shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
  using assms
proof (induct s arbitrary: v rule: rev_induct)
  case Nil
  have "\<Turnstile> v : ders [] r" by fact
  then have "\<Turnstile> v : r" by simp
  then have "Some v = decode (retrieve (intern r) v) r"
    using decode_code retrieve_code by auto
  then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
    by simp
next
  case (snoc c s v)
  have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 
     Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
  have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
  then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 
    by (simp add: Prf_injval ders_append)
  have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
    by (simp add: flex_append)
  also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
    using asm2 IH by simp
  also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
    using asm by (simp_all add: bder_retrieve ders_append)
  finally show "Some (flex r id (s @ [c]) v) = 
                 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
qed


definition blex where
 "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"



definition blexer where
 "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
                decode (bmkeps (bders (intern r) s)) r else None"

lemma blexer_correctness:
  shows "blexer r s = lexer r s"
proof -
  { define bds where "bds \<equiv> bders (intern r) s"
    define ds  where "ds \<equiv> ders s r"
    assume asm: "nullable ds"
    have era: "erase bds = ds" 
      unfolding ds_def bds_def by simp
    have mke: "\<Turnstile> mkeps ds : ds"
      using asm by (simp add: mkeps_nullable)
    have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
      using bmkeps_retrieve
      using asm era by (simp add: bmkeps_retrieve)
    also have "... =  Some (flex r id s (mkeps ds))"
      using mke by (simp_all add: MAIN_decode ds_def bds_def)
    finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" 
      unfolding bds_def ds_def .
  }
  then show "blexer r s = lexer r s"
    unfolding blexer_def lexer_flex
    apply(subst bnullable_correctness[symmetric])
    apply(simp)
    done
qed

lemma asize0:
  shows "0 < asize r"
  apply(induct  r)
  apply(auto)
  done

lemma asize_fuse:
  shows "asize (fuse bs r) = asize r"
  apply(induct r)
  apply(auto)
  done

lemma bder_fuse:
  shows "bder c (fuse bs a) = fuse bs  (bder c a)"
  apply(induct a arbitrary: bs c)
  apply(simp_all)
  done

lemma map_bder_fuse:
  shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
  apply(induct as1)
  apply(auto simp add: bder_fuse)
  done


fun nonnested :: "arexp \<Rightarrow> bool"
  where
  "nonnested (AALTs bs2 []) = True"
| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
| "nonnested r = True"



fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
  where
  "distinctBy [] f acc = []"
| "distinctBy (x#xs) f acc = 
     (if (f x) \<in> acc then distinctBy xs f acc 
      else x # (distinctBy xs f ({f x} \<union> acc)))"

fun flts :: "arexp list \<Rightarrow> arexp list"
  where 
  "flts [] = []"
| "flts (AZERO # rs) = flts rs"
| "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
| "flts (r1 # rs) = r1 # flts rs"


fun spill :: "arexp list \<Rightarrow> arexp list"
  where 
  "spill [] = []"
| "spill ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ spill rs"
| "spill (r1 # rs) = r1 # spill rs"

lemma  spill_Cons:
  shows "spill (r # rs1) = spill [r] @ spill rs1"
  apply(induct r arbitrary: rs1)
   apply(auto)
  done

lemma  spill_append:
  shows "spill (rs1 @ rs2) = spill rs1 @ spill rs2"
  apply(induct rs1 arbitrary: rs2)
   apply(auto)
  by (metis append.assoc spill_Cons)

fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
  where
  "bsimp_ASEQ _ AZERO _ = AZERO"
| "bsimp_ASEQ _ _ AZERO = AZERO"
| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
| "bsimp_ASEQ bs1 r1 r2 = ASEQ  bs1 r1 r2"


fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
  where
  "bsimp_AALTs _ [] = AZERO"
| "bsimp_AALTs bs1 [r] = fuse bs1 r"
| "bsimp_AALTs bs1 rs = AALTs bs1 rs"


fun bsimp :: "arexp \<Rightarrow> arexp" 
  where
  "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
| "bsimp r = r"


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"
| "ACHAR bs c >> bs"
| "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"
| "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
| "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
| "ASTAR bs r >> bs @ [S]"
| "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"

lemma contains0:
  assumes "a >> bs"
  shows "(fuse bs1 a) >> bs1 @ bs"
  using assms
  apply(induct arbitrary: bs1)
  apply(auto intro: contains.intros)
       apply (metis append.assoc contains.intros(3))
     apply (metis append.assoc contains.intros(4))
  apply (metis append.assoc contains.intros(5))
    apply (metis append.assoc contains.intros(6))
   apply (metis append_assoc contains.intros(7))
  done

lemma contains1:
  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> intern r >> code v"
  shows "ASTAR [] (intern r) >> code (Stars vs)"
  using assms
  apply(induct vs)
   apply(simp)
  using contains.simps apply blast
  apply(simp)
   apply(subst (2) append_Nil[symmetric])
  apply(rule contains.intros)
   apply(auto)
  done





lemma contains2:
  assumes "\<Turnstile> v : r"
  shows "(intern r) >> code v"
  using assms
  apply(induct)
       prefer 4
       apply(simp)
       apply(rule contains.intros)
   prefer 4
       apply(simp)
      apply(rule contains.intros)
     apply(simp)
  apply(subst (3) append_Nil[symmetric])
  apply(rule contains.intros)
      apply(simp)
  apply(simp)
    apply(simp)
  apply(subst (9) append_Nil[symmetric])
    apply(rule contains.intros)
    apply (metis append_Cons append_self_conv2 contains0)
    apply(simp)
     apply(subst (9) append_Nil[symmetric])
   apply(rule contains.intros)
   back
   apply(rule contains.intros)
  apply(drule_tac ?bs1.0="[S]" in contains0)
   apply(simp)
  apply(simp)
  apply(case_tac vs)
   apply(simp)
  apply (metis append_Nil contains.intros(6))
  using contains1 by blast

lemma qq1:
  assumes "\<exists>r \<in> set rs. bnullable r"
  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
  using assms
  apply(induct rs arbitrary: rs1 bs)
  apply(simp)
  apply(simp)
  by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)

lemma qq2:
  assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"
  using assms
  apply(induct rs arbitrary: rs1 bs)
  apply(simp)
  apply(simp)
  by (metis append_assoc in_set_conv_decomp r1 r2)

lemma qq2a:
  assumes "\<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
  shows "bmkeps (AALTs bs (r # rs1)) = bmkeps (AALTs bs rs1)"
  using assms
  by (simp add: r1)
  
lemma qq3:
  shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
  apply(induct rs arbitrary: bs)
  apply(simp)
  apply(simp)
  done

lemma qq4:
  assumes "bnullable (AALTs bs rs)"
  shows "bmkeps (AALTs bs rs) = bs @ bmkeps (AALTs [] rs)"
  by (metis append_Nil2 assms bmkeps_retrieve bnullable_correctness erase_fuse fuse.simps(4) mkeps_nullable retrieve_fuse2)


lemma contains3a:
  assumes "AALTs bs lst >> bs @ bs1"
  shows "AALTs bs (a # lst) >> bs @ bs1"
  using assms
  apply -
  by (simp add: contains.intros(5))

  
lemma contains3b:
  assumes "a >> bs1"
  shows "AALTs bs (a # lst) >> bs @ bs1"
  using assms
  apply -
  apply(rule contains.intros)
  apply(simp)
  done   


lemma contains3:
  assumes "\<And>x. \<lbrakk>x \<in> set rs; bnullable x\<rbrakk> \<Longrightarrow> x >> bmkeps x" "x \<in> set rs" "bnullable x"
  shows "AALTs bs rs >> bmkeps (AALTs bs rs)"
  using assms
  apply(induct rs arbitrary: bs x)
   apply simp
  by (metis contains.intros(4) contains.intros(5) list.set_intros(1) list.set_intros(2) qq3 qq4 r r0 r1)

lemma cont1:
  assumes "\<And>v. \<Turnstile> v : erase r \<Longrightarrow> r >> retrieve r v" 
          "\<forall>v\<in>set vs. \<Turnstile> v : erase r \<and> flat v \<noteq> []" 
  shows "ASTAR bs r >> retrieve (ASTAR bs r) (Stars vs)"
  using assms 
  apply(induct vs arbitrary: bs r)
   apply(simp)
  using contains.intros(6) apply auto[1]
  by (simp add: contains.intros(7))
  
lemma contains4:
  assumes "bnullable a"
  shows "a >> bmkeps a"
  using assms
  apply(induct a rule: bnullable.induct)
       apply(auto intro: contains.intros)
  using contains3 by blast

lemma contains5:
  assumes "\<Turnstile> v : r"
  shows "(intern r) >> retrieve (intern r) v"
  using contains2[OF assms] retrieve_code[OF assms]
  by (simp)


lemma contains6:
  assumes "\<Turnstile> v : (erase r)"
  shows "r >> retrieve r v"
  using assms
  apply(induct r arbitrary: v rule: erase.induct)
  apply(auto)[1]
  using Prf_elims(1) apply blast
  using Prf_elims(4) contains.intros(1) apply force
  using Prf_elims(5) contains.intros(2) apply force
  apply(auto)[1]
  using Prf_elims(1) apply blast
  apply(auto)[1]
  using contains3b contains3a apply blast
    prefer 2
  apply(auto)[1]
    apply (metis Prf_elims(2) contains.intros(3) retrieve.simps(6))
   prefer 2
  apply(auto)[1]
   apply (metis Prf_elims(6) cont1)
  apply(simp)
  apply(erule Prf_elims)
   apply(auto)
   apply (simp add: contains3b)
  using retrieve_fuse2 contains3b contains3a
  apply(subst retrieve_fuse2[symmetric])
  apply (metis append_Nil2 erase_fuse fuse.simps(4))
  apply(simp)
  by (metis append_Nil2 erase_fuse fuse.simps(4))

lemma contains7:
  assumes "\<Turnstile> v : der c (erase r)"
  shows "(bder c r) >> retrieve r (injval (erase r) c v)"
  using bder_retrieve[OF assms(1)] retrieve_code[OF assms(1)]
  by (metis assms contains6 erase_bder)


lemma contains7a:
  assumes "\<Turnstile> v : der c (erase r)"
  shows "r >> retrieve r (injval (erase r) c v)"
  using assms
  apply -
  apply(drule Prf_injval)
  apply(drule contains6)
  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
  "bders_simp r [] = r"
| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"

definition blexer_simp where
 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
                decode (bmkeps (bders_simp (intern r) s)) r else None"





lemma bders_simp_append:
  shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
  apply(induct s1 arbitrary: r s2)
   apply(simp)
  apply(simp)
  done

lemma bsimp_ASEQ_size:
  shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
  apply(auto)
  done



lemma flts_size:
  shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
  apply(induct rs rule: flts.induct)
        apply(simp_all)
  by (simp add: asize_fuse comp_def)
  

lemma bsimp_AALTs_size:
  shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
  apply(induct rs rule: bsimp_AALTs.induct)
  apply(auto simp add: asize_fuse)
  done


lemma bsimp_size:
  shows "asize (bsimp r) \<le> asize r"
  apply(induct r)
       apply(simp_all)
   apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
  apply(rule le_trans)
   apply(rule bsimp_AALTs_size)
  apply(simp)
   apply(rule le_trans)
   apply(rule flts_size)
  by (simp add: sum_list_mono)

lemma bsimp_asize0:
  shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
  apply(induct rs)
   apply(auto)
  by (simp add: add_mono bsimp_size)

lemma bsimp_AALTs_size2:
  assumes "\<forall>r \<in> set  rs. nonalt r"
  shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
  using assms
  apply(induct rs rule: bsimp_AALTs.induct)
    apply(simp_all add: asize_fuse)
  done


lemma qq:
  shows "map (asize \<circ> fuse bs) rs = map asize rs"
  apply(induct rs)
   apply(auto simp add: asize_fuse)
  done

lemma flts_size2:
  assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"
  shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
  using assms
  apply(induct rs)
   apply(auto simp add: qq)
   apply (simp add: flts_size less_Suc_eq_le)
  apply(case_tac a)
       apply(auto simp add: qq)
   prefer 2
   apply (simp add: flts_size le_imp_less_Suc)
  using less_Suc_eq by auto

lemma bsimp_AALTs_size3:
  assumes "\<exists>r \<in> set  (map bsimp rs). \<not>nonalt r"
  shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"
  using assms flts_size2
  apply  -
  apply(clarify)
  apply(simp)
  apply(drule_tac x="map bsimp rs" in meta_spec)
  apply(drule meta_mp)
  apply (metis list.set_map nonalt.elims(3))
  apply(simp)
  apply(rule order_class.order.strict_trans1)
   apply(rule bsimp_AALTs_size)
  apply(simp)
  by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)




lemma L_bsimp_ASEQ:
  "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
  apply(simp_all)
  by (metis erase_fuse fuse.simps(4))

lemma L_bsimp_AALTs:
  "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
  apply(induct bs rs rule: bsimp_AALTs.induct)
  apply(simp_all add: erase_fuse)
  done

lemma L_erase_AALTs:
  shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
  apply(induct rs)
   apply(simp)
  apply(simp)
  apply(case_tac rs)
   apply(simp)
  apply(simp)
  done

lemma L_erase_flts:
  shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
  apply(induct rs rule: flts.induct)
        apply(simp_all)
  apply(auto)
  using L_erase_AALTs erase_fuse apply auto[1]
  by (simp add: L_erase_AALTs erase_fuse)


lemma L_bsimp_erase:
  shows "L (erase r) = L (erase (bsimp r))"
  apply(induct r)
  apply(simp)
  apply(simp)
  apply(simp)
  apply(auto simp add: Sequ_def)[1]
  apply(subst L_bsimp_ASEQ[symmetric])
  apply(auto simp add: Sequ_def)[1]
  apply(subst (asm)  L_bsimp_ASEQ[symmetric])
  apply(auto simp add: Sequ_def)[1]
   apply(simp)
   apply(subst L_bsimp_AALTs[symmetric])
   defer
   apply(simp)
  apply(subst (2)L_erase_AALTs)
  apply(subst L_erase_flts)
  apply(auto)
   apply (simp add: L_erase_AALTs)
  using L_erase_AALTs by blast

lemma bsimp_ASEQ0:
  shows "bsimp_ASEQ bs r1 AZERO = AZERO"
  apply(induct r1)
  apply(auto)
  done



lemma bsimp_ASEQ1:
  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
  shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
  using assms
  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
  apply(auto)
  done

lemma bsimp_ASEQ2:
  shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
  apply(induct r2)
  apply(auto)
  done


lemma L_bders_simp:
  shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
  apply(induct s arbitrary: r rule: rev_induct)
   apply(simp)
  apply(simp)
  apply(simp add: ders_append)
  apply(simp add: bders_simp_append)
  apply(simp add: L_bsimp_erase[symmetric])
  by (simp add: der_correctness)

lemma b1:
  "bsimp_ASEQ bs1 (AONE bs) r =  fuse (bs1 @ bs) r" 
  apply(induct r)
       apply(auto)
  done

lemma b2:
  assumes "bnullable r"
  shows "bmkeps (fuse bs r) = bs @ bmkeps r"
  by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)

lemma b3:
  shows "bnullable r = bnullable (bsimp r)"
  using L_bsimp_erase bnullable_correctness nullable_correctness by auto


lemma b4:
  shows "bnullable (bders_simp r s) = bnullable (bders r s)"
  by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))

lemma q1:
  assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
  shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
  using assms
  apply(induct rs)
  apply(simp)
  apply(simp)
  done

lemma q3:
  assumes "\<exists>r \<in> set rs. bnullable r"
  shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"
  using assms
  apply(induct bs rs rule: bsimp_AALTs.induct)
    apply(simp)
   apply(simp)
  apply (simp add: b2)
  apply(simp)
  done


lemma fuse_empty:
  shows "fuse [] r = r"
  apply(induct r)
       apply(auto)
  done

lemma flts_fuse:
  shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
  apply(induct rs arbitrary: bs rule: flts.induct)
        apply(auto simp add: fuse_append)
  done

lemma bsimp_ASEQ_fuse:
  shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
  apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
  apply(auto)
  done

lemma bsimp_AALTs_fuse:
  assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
  shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
  using assms
  apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
  apply(auto)
  done



lemma bsimp_fuse:
  shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
apply(induct r arbitrary: bs)
       apply(simp)
      apply(simp)
     apply(simp)
    prefer 3
    apply(simp)
   apply(simp)
   apply (simp add: bsimp_ASEQ_fuse)
  apply(simp)
  by (simp add: bsimp_AALTs_fuse fuse_append)

lemma bsimp_fuse_AALTs:
  shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
  apply(subst bsimp_fuse) 
  apply(simp)
  done

lemma bsimp_fuse_AALTs2:
  shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
  using bsimp_AALTs_fuse fuse_append by auto
  

lemma bsimp_ASEQ_idem:
  assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
  shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
  using assms
  apply(case_tac "bsimp r1 = AZERO")
    apply(simp)
 apply(case_tac "bsimp r2 = AZERO")
    apply(simp)
  apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))  
  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
    apply(auto)[1]
    apply(subst bsimp_ASEQ2)
   apply(subst bsimp_ASEQ2)
  apply (metis assms(2) bsimp_fuse)
      apply(subst bsimp_ASEQ1)
      apply(auto)
  done



lemma  k0:
  shows "flts (r # rs1) = flts [r] @ flts rs1"
  apply(induct r arbitrary: rs1)
   apply(auto)
  done

lemma  k00:
  shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
  apply(induct rs1 arbitrary: rs2)
   apply(auto)
  by (metis append.assoc k0)

lemma  k0a:
  shows "flts [AALTs bs rs] = map (fuse bs)  rs"
  apply(simp)
  done


lemma  k0b:
  assumes "nonalt r" "r \<noteq> AZERO"
  shows "flts [r] = [r]"
  using assms
  apply(case_tac  r)
  apply(simp_all)
  done

lemma nn1:
  assumes "nonnested (AALTs bs rs)"
  shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
  using assms
  apply(induct rs rule: flts.induct)
  apply(auto)
  done

lemma nn1q:
  assumes "nonnested (AALTs bs rs)"
  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
  using assms
  apply(induct rs rule: flts.induct)
  apply(auto)
  done

lemma nn1qq:
  assumes "nonnested (AALTs bs rs)"
  shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
  using assms
  apply(induct rs rule: flts.induct)
  apply(auto)
  done

lemma nn10:
  assumes "nonnested (AALTs cs rs)" 
  shows "nonnested (AALTs (bs @ cs) rs)"
  using assms
  apply(induct rs arbitrary: cs bs)
   apply(simp_all)
  apply(case_tac a)
       apply(simp_all)
  done

lemma nn11a:
  assumes "nonalt r"
  shows "nonalt (fuse bs r)"
  using assms
  apply(induct r)
       apply(auto)
  done


lemma nn1a:
  assumes "nonnested r"
  shows "nonnested (fuse bs r)"
  using assms
  apply(induct bs r arbitrary: rule: fuse.induct)
       apply(simp_all add: nn10)
  done  

lemma n0:
  shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
  apply(induct rs  arbitrary: bs)
   apply(auto)
    apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
   apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
  by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))

  
  

lemma nn1c:
  assumes "\<forall>r \<in> set rs. nonnested r"
  shows "\<forall>r \<in> set (flts rs). nonalt r"
  using assms
  apply(induct rs rule: flts.induct)
        apply(auto)
  apply(rule nn11a)
  by (metis nn1qq nonalt.elims(3))

lemma nn1bb:
  assumes "\<forall>r \<in> set rs. nonalt r"
  shows "nonnested (bsimp_AALTs bs rs)"
  using assms
  apply(induct bs rs rule: bsimp_AALTs.induct)
    apply(auto)
   apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
  using n0 by auto
    
lemma nn1b:
  shows "nonnested (bsimp r)"
  apply(induct r)
       apply(simp_all)
  apply(case_tac "bsimp r1 = AZERO")
    apply(simp)
 apply(case_tac "bsimp r2 = AZERO")
   apply(simp)
    apply(subst bsimp_ASEQ0)
  apply(simp)
  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
    apply(auto)[1]
    apply(subst bsimp_ASEQ2)
  apply (simp add: nn1a)    
   apply(subst bsimp_ASEQ1)
      apply(auto)
  apply(rule nn1bb)
  apply(auto)
  by (metis (mono_tags, hide_lams) imageE nn1c set_map)

lemma nn1d:
  assumes "bsimp r = AALTs bs rs"
  shows "\<forall>r1 \<in> set rs. \<forall>  bs. r1 \<noteq> AALTs bs  rs2"
  using nn1b assms
  by (metis nn1qq)

lemma nn_flts:
  assumes "nonnested (AALTs bs rs)"
  shows "\<forall>r \<in>  set (flts rs). nonalt r"
  using assms
  apply(induct rs arbitrary: bs rule: flts.induct)
        apply(auto)
  done



lemma rt:
  shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
  apply(induct rs)
   apply(simp)
  apply(simp)
  apply(subst  k0)
  apply(simp)
  by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)

lemma bsimp_AALTs_qq:
  assumes "1 < length rs"
  shows "bsimp_AALTs bs rs = AALTs bs  rs"
  using  assms
  apply(case_tac rs)
   apply(simp)
  apply(case_tac list)
   apply(simp_all)
  done


lemma bsimp_AALTs1:
  assumes "nonalt r"
  shows "bsimp_AALTs bs (flts [r]) = fuse bs r"
  using  assms
  apply(case_tac r)
   apply(simp_all)
  done

lemma bbbbs:
  assumes "good r" "r = AALTs bs1 rs"
  shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
  using  assms
  by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)

lemma bbbbs1:
  shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
  using nonalt.elims(3) by auto
  

lemma good_fuse:
  shows "good (fuse bs r) = good r"
  apply(induct r arbitrary: bs)
       apply(auto)
     apply(case_tac r1)
          apply(simp_all)
  apply(case_tac r2)
          apply(simp_all)
  apply(case_tac r2)
            apply(simp_all)
  apply(case_tac r2)
           apply(simp_all)
  apply(case_tac r2)
          apply(simp_all)
  apply(case_tac r1)
          apply(simp_all)
  apply(case_tac r2)
           apply(simp_all)
  apply(case_tac r2)
           apply(simp_all)
  apply(case_tac r2)
           apply(simp_all)
  apply(case_tac r2)
         apply(simp_all)
  apply(case_tac x2a)
    apply(simp_all)
  apply(case_tac list)
    apply(simp_all)
  apply(case_tac x2a)
    apply(simp_all)
  apply(case_tac list)
    apply(simp_all)
  done

lemma good0:
  assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r"
  shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
  using  assms
  apply(induct bs rs rule: bsimp_AALTs.induct)
  apply(auto simp add: good_fuse)
  done

lemma good0a:
  assumes "flts (map bsimp rs) \<noteq> Nil" "\<forall>r \<in> set (flts (map bsimp rs)). nonalt r"
  shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
  using  assms
  apply(simp)
  apply(auto)
  apply(subst (asm) good0)
   apply(simp)
    apply(auto)
   apply(subst good0)
   apply(simp)
    apply(auto)
  done

lemma flts0:
  assumes "r \<noteq> AZERO" "nonalt r"
  shows "flts [r] \<noteq> []"
  using  assms
  apply(induct r)
       apply(simp_all)
  done

lemma flts1:
  assumes "good r" 
  shows "flts [r] \<noteq> []"
  using  assms
  apply(induct r)
       apply(simp_all)
  apply(case_tac x2a)
   apply(simp)
  apply(simp)
  done

lemma flts2:
  assumes "good r" 
  shows "\<forall>r' \<in> set (flts [r]). good r' \<and> nonalt r'"
  using  assms
  apply(induct r)
       apply(simp)
      apply(simp)
     apply(simp)
    prefer 2
    apply(simp)
    apply(auto)[1]
     apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse)
  apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a)
   apply fastforce
  apply(simp)
  done  


lemma flts3:
  assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO" 
  shows "\<forall>r \<in> set (flts rs). good r"
  using  assms
  apply(induct rs arbitrary: rule: flts.induct)
        apply(simp_all)
  by (metis UnE flts2 k0a set_map)

lemma flts3b:
  assumes "\<exists>r\<in>set rs. good r"
  shows "flts rs \<noteq> []"
  using  assms
  apply(induct rs arbitrary: rule: flts.induct)
        apply(simp)
       apply(simp)
      apply(simp)
      apply(auto)
  done

lemma flts4:
  assumes "bsimp_AALTs bs (flts rs) = AZERO"
  shows "\<forall>r \<in> set rs. \<not> good r"
  using assms
  apply(induct rs arbitrary: bs rule: flts.induct)
        apply(auto)
        defer
  apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
  apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
  apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
  apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject)
    apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
  apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6))
  by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)


lemma flts_nil:
  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
            good (bsimp y) \<or> bsimp y = AZERO"
  and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
  shows "flts (map bsimp rs) = []"
  using assms
  apply(induct rs)
   apply(simp)
  apply(simp)
  apply(subst k0)
  apply(simp)
  by force

lemma flts_nil2:
  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
            good (bsimp y) \<or> bsimp y = AZERO"
  and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
  shows "flts (map bsimp rs) = []"
  using assms
  apply(induct rs arbitrary: bs)
   apply(simp)
  apply(simp)
  apply(subst k0)
  apply(simp)
  apply(subst (asm) k0)
  apply(auto)
  apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
  by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
  
  

lemma good_SEQ:
  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
  shows "good (ASEQ bs r1 r2) = (good r1 \<and> good r2)"
  using assms
  apply(case_tac r1)
       apply(simp_all)
  apply(case_tac r2)
          apply(simp_all)
  apply(case_tac r2)
         apply(simp_all)
  apply(case_tac r2)
        apply(simp_all)
  apply(case_tac r2)
       apply(simp_all)
  done

lemma good1:
  shows "good (bsimp a) \<or> bsimp a = AZERO"
  apply(induct a taking: asize rule: measure_induct)
  apply(case_tac x)
  apply(simp)
  apply(simp)
  apply(simp)
  prefer 3
    apply(simp)
   prefer 2
  (*  AALTs case  *)
  apply(simp only:)
   apply(case_tac "x52")
    apply(simp)
  thm good0a
   (*  AALTs list at least one - case *)
   apply(simp only: )
  apply(frule_tac x="a" in spec)
   apply(drule mp)
    apply(simp)
   (* either first element is good, or AZERO *)
    apply(erule disjE)
     prefer 2
    apply(simp)
   (* in  the AZERO case, the size  is smaller *)
   apply(drule_tac x="AALTs x51 list" in spec)
   apply(drule mp)
     apply(simp add: asize0)
    apply(subst (asm) bsimp.simps)
  apply(subst (asm) bsimp.simps)
    apply(assumption)
   (* in the good case *)
  apply(frule_tac x="AALTs x51 list" in spec)
   apply(drule mp)
    apply(simp add: asize0)
   apply(erule disjE)
    apply(rule disjI1)
  apply(simp add: good0)
    apply(subst good0)
      apply (metis Nil_is_append_conv flts1 k0)
  apply (metis ex_map_conv list.simps(9) nn1b nn1c)
  apply(simp)
    apply(subst k0)
    apply(simp)
    apply(auto)[1]
  using flts2 apply blast
    apply(subst  (asm) good0)
      prefer 3
      apply(auto)[1]
     apply auto[1]
    apply (metis ex_map_conv nn1b nn1c)
  (* in  the AZERO case *)
   apply(simp)
   apply(frule_tac x="a" in spec)
   apply(drule mp)
  apply(simp)
   apply(erule disjE)
    apply(rule disjI1)
    apply(subst good0)
  apply(subst k0)
  using flts1 apply blast
     apply(auto)[1]
  apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c)
    apply(auto)[1]
  apply(subst (asm) k0)
  apply(auto)[1]
  using flts2 apply blast
  apply(frule_tac x="AALTs x51 list" in spec)
   apply(drule mp)
     apply(simp add: asize0)
    apply(erule disjE)
     apply(simp)
    apply(simp)
  apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject)
   apply(subst (2) k0)
  apply(simp)
  (* SEQ case *)
  apply(simp)
  apply(case_tac "bsimp x42 = AZERO")
    apply(simp)
 apply(case_tac "bsimp x43 = AZERO")
   apply(simp)
    apply(subst (2) bsimp_ASEQ0)
  apply(simp)
  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
    apply(auto)[1]
   apply(subst bsimp_ASEQ2)
  using good_fuse apply force
   apply(subst bsimp_ASEQ1)
     apply(auto)
  apply(subst  good_SEQ)
  apply(simp)
    apply(simp)
   apply(simp)
  using less_add_Suc1 less_add_Suc2 by blast

lemma good1a:
  assumes "L(erase a) \<noteq> {}"
  shows "good (bsimp a)"
  using good1 assms
  using L_bsimp_erase by force
  


lemma flts_append:
  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
   apply(auto)
  apply(case_tac xs)
   apply(auto)
   apply(case_tac x)
        apply(auto)
  apply(case_tac x)
        apply(auto)
  done

lemma g1:
  assumes "good (bsimp_AALTs bs rs)"
  shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
using assms
    apply(induct rs arbitrary: bs)
  apply(simp)
  apply(case_tac rs)
  apply(simp only:)
  apply(simp)
  apply(case_tac  list)
  apply(simp)
  by simp

lemma flts_0:
  assumes "nonnested (AALTs bs  rs)"
  shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
  using assms
  apply(induct rs arbitrary: bs rule: flts.induct)
        apply(simp) 
       apply(simp) 
      defer
      apply(simp) 
     apply(simp) 
    apply(simp) 
apply(simp) 
  apply(rule ballI)
  apply(simp)
  done

lemma flts_0a:
  assumes "nonnested (AALTs bs  rs)"
  shows "AZERO \<notin> set (flts rs)"
  using assms
  using flts_0 by blast 
  
lemma qqq1:
  shows "AZERO \<notin> set (flts (map bsimp rs))"
  by (metis ex_map_conv flts3 good.simps(1) good1)


fun nonazero :: "arexp \<Rightarrow> bool"
  where
  "nonazero AZERO = False"
| "nonazero r = True"

lemma flts_concat:
  shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
  apply(induct rs)
   apply(auto)
  apply(subst k0)
  apply(simp)
  done

lemma flts_single1:
  assumes "nonalt r" "nonazero r"
  shows "flts [r] = [r]"
  using assms
  apply(induct r)
  apply(auto)
  done

lemma flts_qq:
  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'"
  shows "flts (map bsimp rs) = rs"
  using assms
  apply(induct rs)
   apply(simp)
  apply(simp)
  apply(subst k0)
  apply(subgoal_tac "flts [bsimp a] =  [a]")
   prefer 2
   apply(drule_tac x="a" in spec)
   apply(drule mp)
    apply(simp)
   apply(auto)[1]
  using good.simps(1) k0b apply blast
  apply(auto)[1]  
  done
  
lemma test:
  assumes "good r"
  shows "bsimp r = r"
  using assms
  apply(induct r taking: "asize" rule: measure_induct)
  apply(erule good.elims)
  apply(simp_all)
  apply(subst k0)
  apply(subst (2) k0)
                apply(subst flts_qq)
                  apply(auto)[1]
                 apply(auto)[1]
                apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b)
               apply force+
  apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2)
  apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2)
         apply force+
  apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2)
  apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2)
    apply force+
  done

lemma test2:
  assumes "good r"
  shows "bsimp r = r"
  using assms
  apply(induct r taking: "asize" rule: measure_induct)
  apply(case_tac x)
       apply(simp_all)
   defer  
  (* AALT case *)
   apply(subgoal_tac "1 < length x52")
    prefer 2
    apply(case_tac x52)
     apply(simp)
    apply(simp)
    apply(case_tac list)
     apply(simp)
  apply(simp)
    apply(subst bsimp_AALTs_qq)
    prefer 2
    apply(subst flts_qq)
      apply(auto)[1]
     apply(auto)[1]
   apply(case_tac x52)
     apply(simp)
    apply(simp)
    apply(case_tac list)
     apply(simp)
      apply(simp)
      apply(auto)[1]
  apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff)
  apply(simp)  
  apply(case_tac x52)
     apply(simp)
    apply(simp)
    apply(case_tac list)
     apply(simp)
   apply(simp)
   apply(subst k0)
   apply(simp)
   apply(subst (2) k0)
   apply(simp)
  apply (simp add: Suc_lessI flts1 one_is_add)
  (* SEQ case *)
  apply(case_tac "bsimp x42 = AZERO")
   apply simp
  apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1)  
   apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
   apply(auto)[1]
  defer
  apply(case_tac "bsimp x43 = AZERO")
    apply(simp)
  apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2)
  apply(auto)  
   apply (subst bsimp_ASEQ1)
      apply(auto)[3]
   apply(auto)[1]
    apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1)
   apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2)
  apply (subst bsimp_ASEQ2)
  apply(drule_tac x="x42" in spec)
  apply(drule mp)
   apply(simp)
  apply(drule mp)
   apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ)
  apply(simp)
  done


lemma bsimp_idem:
  shows "bsimp (bsimp r) = bsimp r"
  using test good1
  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" 
          "AALTs (bs @ x1) x2a >> bs @ bs1"
        shows "AALTs x1 x2a >> bs1"
  using assms
  apply(induct x2a arbitrary: bs x1 bs1)
   apply(auto)
   apply(erule contains.cases)
         apply(auto)
  apply(erule contains.cases)
        apply(auto)
  apply (simp add: contains.intros(4))
  using contains.intros(5) by blast


lemma contains49:
  assumes "fuse bs a >> bs @ bs1"
  shows "a >> bs1"
  using assms
  apply(induct a arbitrary: bs bs1)
       apply(auto)
  using contains.simps apply blast
      apply(erule contains.cases)
            apply(auto)
  apply(rule contains.intros)
    apply(erule contains.cases)
            apply(auto)
     apply(rule contains.intros)
  apply(erule contains.cases)
            apply(auto)
  apply(rule contains.intros)
     apply(auto)[2]
  prefer 2
  apply(erule contains.cases)
         apply(auto)
  apply (simp add: contains.intros(6))
  using contains.intros(7) apply blast
  using contains48 by blast

lemma contains50:
  assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
  shows "bsimp_AALTs bs (rs1 @ rs2) >> bs @ bs1"
  using assms
  apply(induct rs1 arbitrary: bs rs2 bs1)
   apply(simp)
  apply(auto)
  apply(case_tac rs1)
   apply(simp)
   apply(case_tac rs2)
    apply(simp)
  using contains.simps apply blast
  apply(simp)
  apply(case_tac list)
    apply(simp)
    apply(rule contains.intros)
    back
    apply(rule contains.intros)
  using contains49 apply blast
   apply(simp)
  using contains.intros(5) apply blast
  apply(simp)
  by (metis bsimp_AALTs.elims contains.intros(4) contains.intros(5) contains49 list.distinct(1))

lemma contains51:
  assumes "bsimp_AALTs bs [r] >> bs @ bs1"
  shows "bsimp_AALTs bs ([r] @ rs2) >> bs @ bs1"
  using assms
  apply(induct rs2 arbitrary: bs r bs1)
   apply(simp)
  apply(auto)
  using contains.intros(4) contains49 by blast

lemma contains51a:
  assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
  shows "bsimp_AALTs bs (rs2 @ [r]) >> bs @ bs1"
  using assms
  apply(induct rs2 arbitrary: bs r bs1)
   apply(simp)
   apply(auto)
  using contains.simps apply blast
  apply(case_tac rs2)
   apply(auto)
  using contains3b contains49 apply blast
  apply(case_tac list)
   apply(auto)
  apply(erule contains.cases)
         apply(auto)
  using contains.intros(4) apply auto[1]
   apply(erule contains.cases)
         apply(auto)
    apply (simp add: contains.intros(4) contains.intros(5))
   apply (simp add: contains.intros(5))
  apply(erule contains.cases)
        apply(auto)
   apply (simp add: contains.intros(4))
   apply(erule contains.cases)
        apply(auto)
  using contains.intros(4) contains.intros(5) apply blast
  using contains.intros(5) by blast  
  
lemma contains51b:
  assumes "bsimp_AALTs bs rs >> bs @ bs1"
  shows "bsimp_AALTs bs (rs @ rs2) >> bs @ bs1"
  using assms
  apply(induct rs2 arbitrary: bs rs bs1)
   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"
  using assms
  apply(induct rs arbitrary: bs bs1 bs2)
       apply(auto)
  apply(erule contains.cases)
        apply(auto)
  apply(erule contains.cases)
        apply(auto)
  using contains0 contains51 apply auto[1]
  by (metis append.left_neutral append_Cons contains50 list.simps(9))
  

lemma contains51d:
  assumes "fuse bs r >> bs @ bs1"
  shows "bsimp_AALTs bs (flts [r]) >> bs @ bs1"
  using assms
  apply(induct r arbitrary: bs bs1)
       apply(auto)
  by (simp add: contains51c)

lemma contains52:
  assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs @ bs1"
  shows "bsimp_AALTs bs (flts rs) >> bs @ bs1"
  using assms
  apply(induct rs arbitrary: bs bs1)
   apply(simp)
  apply(auto)
   defer
   apply (metis contains50 k0)
  apply(subst k0)
  apply(rule contains51b)
  using contains51d by blast

lemma contains55:
  assumes "a >> bs" 
  shows "bsimp a >> bs"
  using assms
  apply(induct a bs arbitrary:)
        apply(auto intro: contains.intros)
    apply(case_tac "bsimp a1 = AZERO")
     apply(simp)
  using contains.simps apply blast
  apply(case_tac "bsimp a2 = AZERO")
     apply(simp)
  using contains.simps apply blast
  apply(case_tac "\<exists>bs. bsimp a1 = AONE bs")
     apply(auto)[1]
     apply(rotate_tac 1)
     apply(erule contains.cases)
           apply(auto)
     apply (simp add: b1 contains0 fuse_append)
    apply (simp add: bsimp_ASEQ1 contains.intros(3))
   prefer 2
   apply(case_tac rs)
    apply(simp)
  using contains.simps apply blast
   apply (metis contains50 k0)
  (* AALTS case *)
  apply(rule contains52)
  apply(rule_tac x="bsimp r" in bexI)
   apply(auto)
  using contains0 by blast


lemma q3a:
  assumes "\<exists>r \<in> set rs. bnullable r"
  shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
  using assms
  apply(induct rs arbitrary: bs bs1)
   apply(simp)
  apply(simp)
  apply(auto)
   apply (metis append_assoc b2 bnullable_correctness erase_fuse r0)
  apply(case_tac "bnullable a")
   apply (metis append.assoc b2 bnullable_correctness erase_fuse r0)
  apply(case_tac rs)
  apply(simp)
  apply(simp)
  apply(auto)[1]
   apply (metis bnullable_correctness erase_fuse)+
  done



lemma qq4a:
  assumes "\<exists>x\<in>set list. bnullable x"
  shows "\<exists>x\<in>set (flts list). bnullable x"
  using assms
  apply(induct list rule: flts.induct)
        apply(auto)
  by (metis UnCI bnullable_correctness erase_fuse imageI)
  

lemma qs3:
  assumes "\<exists>r \<in> set rs. bnullable r"
  shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"
  using assms
  apply(induct rs arbitrary: bs taking: size rule: measure_induct)
  apply(case_tac x)
  apply(simp)
  apply(simp)
  apply(case_tac a)
       apply(simp)
       apply (simp add: r1)
      apply(simp)
      apply (simp add: r0)
     apply(simp)
     apply(case_tac "flts list")
      apply(simp)
  apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)
     apply(simp)
     apply (simp add: r1)
    prefer 3
    apply(simp)
    apply (simp add: r0)
   prefer 2
   apply(simp)
  apply(case_tac "\<exists>x\<in>set x52. bnullable x")
  apply(case_tac "list")
    apply(simp)
    apply (metis b2 fuse.simps(4) q3a r2)
   apply(erule disjE)
    apply(subst qq1)
     apply(auto)[1]
     apply (metis bnullable_correctness erase_fuse)
    apply(simp)
     apply (metis b2 fuse.simps(4) q3a r2)
    apply(simp)
    apply(auto)[1]
     apply(subst qq1)
      apply (metis bnullable_correctness erase_fuse image_eqI set_map)
     apply (metis b2 fuse.simps(4) q3a r2)
  apply(subst qq1)
      apply (metis bnullable_correctness erase_fuse image_eqI set_map)
    apply (metis b2 fuse.simps(4) q3a r2)
   apply(simp)
   apply(subst qq2)
     apply (metis bnullable_correctness erase_fuse imageE set_map)
  prefer 2
  apply(case_tac "list")
     apply(simp)
    apply(simp)
   apply (simp add: qq4a)
  apply(simp)
  apply(auto)
   apply(case_tac list)
    apply(simp)
   apply(simp)
   apply (simp add: r0)
  apply(case_tac "bnullable (ASEQ x41 x42 x43)")
   apply(case_tac list)
    apply(simp)
   apply(simp)
   apply (simp add: r0)
  apply(simp)
  using qq4a r1 r2 by auto



lemma k1:
  assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
          "\<exists>x\<in>set x2a. bnullable x"
        shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
  using assms
  apply(induct x2a)
  apply fastforce
  apply(simp)
  apply(subst k0)
  apply(subst (2) k0)
  apply(auto)[1]
  apply (metis b3 k0 list.set_intros(1) qs3 r0)
  by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map)
  
  
  
lemma bmkeps_simp:
  assumes "bnullable r"
  shows "bmkeps r = bmkeps (bsimp r)"
  using  assms
  apply(induct r)
       apply(simp)
      apply(simp)
     apply(simp)
    apply(simp)
    prefer 3
  apply(simp)
   apply(case_tac "bsimp r1 = AZERO")
    apply(simp)
    apply(auto)[1]
  apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
 apply(case_tac "bsimp r2 = AZERO")
    apply(simp)  
    apply(auto)[1]
  apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
    apply(auto)[1]
    apply(subst b1)
    apply(subst b2)
  apply(simp add: b3[symmetric])
    apply(simp)
   apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)")
    prefer 2
  apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
   apply(simp)
  apply(simp)
  thm q3
  apply(subst q3[symmetric])
   apply simp
  using b3 qq4a apply auto[1]
  apply(subst qs3)
   apply simp
  using k1 by blast

thm bmkeps_retrieve bmkeps_simp bder_retrieve

lemma bmkeps_bder_AALTs:
  assumes "\<exists>r \<in> set rs. bnullable (bder c r)" 
  shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))"
  using assms
  apply(induct rs)
   apply(simp)
  apply(simp)
  apply(auto)
  apply(case_tac rs)
    apply(simp)
  apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2)
   apply(simp)
  apply(case_tac  rs)
   apply(simp_all)
  done

lemma bbs0:
  shows "blexer_simp r [] = blexer r []"
  apply(simp add: blexer_def blexer_simp_def)
  done

lemma bbs1:
  shows "blexer_simp r [c] = blexer r [c]"
  apply(simp add: blexer_def blexer_simp_def)
  apply(auto)
    defer
  using b3 apply auto[1]
  using b3 apply auto[1]  
  apply(subst bmkeps_simp[symmetric])
   apply(simp)
  apply(simp)
  done

lemma oo:
  shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
  apply(simp add: blexer_correctness)
  done

lemma 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'"
  shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
  using assms
  apply(induct rs arbitrary: c)
   apply(simp)
  apply(simp)
  apply(subst k0)
  apply(simp add: flts_append)
  apply(subst (2) k0)
  apply(simp add: flts_append)
  apply(subgoal_tac "flts [a] =  [a]")
   prefer 2
  using good.simps(1) k0b apply blast
  apply(simp)
  done

lemma bmkeps_good:
  assumes "good a"
  shows "bmkeps (bsimp a) = bmkeps a"
  using assms
  using test2 by auto


lemma xxx_bder:
  assumes "good r"
  shows "L (erase r) \<noteq> {}"
  using assms
  apply(induct r rule: good.induct)
  apply(auto simp add: Sequ_def)
  done

lemma xxx_bder2:
  assumes "L (erase (bsimp r)) = {}"
  shows "bsimp r = AZERO"
  using assms xxx_bder test2 good1
  by blast

lemma XXX2aa:
  assumes "good a"
  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
  using  assms
  by (simp add: test2)

lemma XXX2aa_ders:
  assumes "good a"
  shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)"
  using  assms
  by (simp add: test2)

lemma XXX4a:
  shows "good (bders_simp (bsimp r) s)  \<or> bders_simp (bsimp r) s = AZERO"
  apply(induct s arbitrary: r rule:  rev_induct)
   apply(simp)
  apply (simp add: good1)
  apply(simp add: bders_simp_append)
  apply (simp add: good1)
  done

lemma XXX4a_good:
  assumes "good a"
  shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
  using assms
  apply(induct s arbitrary: a rule:  rev_induct)
   apply(simp)
  apply(simp add: bders_simp_append)
  apply (simp add: good1)
  done

lemma XXX4a_good_cons:
  assumes "s \<noteq> []"
  shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
  using assms
  apply(case_tac s)
   apply(auto)
  using XXX4a by blast

lemma XXX4b:
  assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}"
  shows "good (bders_simp a s)"
  using assms
  apply(induct s arbitrary: a)
   apply(simp)
  apply(simp)
  apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}")
   prefer 2
   apply(auto)[1]
  apply(erule disjE)
   apply(subgoal_tac "bsimp (bder a aa) = AZERO")
    prefer 2
  using L_bsimp_erase xxx_bder2 apply auto[1]
   apply(simp)
  apply (metis L.simps(1) XXX4a erase.simps(1))  
  apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
  apply(drule meta_mp)
  apply simp
  apply(rule good1a)
  apply(auto)
  done

lemma bders_AZERO:
  shows "bders AZERO s = AZERO"
  and   "bders_simp AZERO s = AZERO"
   apply (induct s)
     apply(auto)
  done

lemma LA:
  assumes "\<Turnstile> v : ders s (erase r)"
  shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)"
  using assms
  apply(induct s arbitrary: r v rule: rev_induct)
   apply(simp)
  apply(simp add: bders_append ders_append)
  apply(subst bder_retrieve)
   apply(simp)
  apply(drule Prf_injval)
  by (simp add: flex_append)


lemma LB:
  assumes "s \<in> (erase r) \<rightarrow> v" 
  shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
  using assms
  apply(induct s arbitrary: r v rule: rev_induct)
   apply(simp)
   apply(subgoal_tac "v = mkeps (erase r)")
    prefer 2
  apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness)
   apply(simp)
  apply(simp add: flex_append ders_append)
  by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex)

lemma LB_sym:
  assumes "s \<in> (erase r) \<rightarrow> v" 
  shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))"
  using assms
  by (simp add: LB)


lemma LC:
  assumes "s \<in> (erase r) \<rightarrow> v" 
  shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))"
  apply(simp)
  by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable)


lemma L0:
  assumes "bnullable a"
  shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
  using assms b3 bmkeps_retrieve bmkeps_simp bnullable_correctness
  by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)

thm bmkeps_retrieve

lemma L0a:
  assumes "s \<in> L(erase a)"
  shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) = 
         retrieve (bders a s) (mkeps (erase (bders a s)))"
  using assms
  by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
  
lemma L0aa:
  assumes "s \<in> L (erase a)"
  shows "[] \<in> erase (bsimp (bders a s)) \<rightarrow> mkeps (erase (bsimp (bders a s)))"
  using assms
  by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex)

lemma L0aaa:
  assumes "[c] \<in> L (erase a)"
  shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bder c a)))"
  using assms
  by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject)

lemma L0aaaa:
  assumes "[c] \<in> L (erase a)"
  shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bders a [c])))"
  using assms
  using L0aaa by auto
    

lemma L02:
  assumes "bnullable (bder c a)"
  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) = 
         retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))"
  using assms
  apply(simp)
  using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0  LA LB
  apply(subst bder_retrieve[symmetric])
  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness)
  apply(simp)
  done

lemma L02_bders:
  assumes "bnullable (bders a s)"
  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = 
         retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))"
  using assms
  by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)


  

lemma L03:
  assumes "bnullable (bder c a)"
  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
         bmkeps (bsimp (bder c (bsimp a)))"
  using assms
  by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)

lemma L04:
  assumes "bnullable (bder c a)"
  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
         retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"     
  using assms
  by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness)
    
lemma L05:
  assumes "bnullable (bder c a)"
  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
         retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" 
  using assms
  using L04 by auto 

lemma L06:
  assumes "bnullable (bder c a)"
  shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))"
  using assms
  by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) 

lemma L07:
  assumes "s \<in> L (erase r)"
  shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) 
            = retrieve (bders r s) (mkeps (erase (bders r s)))"
  using assms
  using LB LC lexer_correct_Some by auto

lemma L06_2:
  assumes "bnullable (bders a [c,d])"
  shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
  using assms
  apply(simp)
  by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness)
  
lemma L06_bders:
  assumes "bnullable (bders a s)"
  shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))"
  using assms
  by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness)

lemma LLLL:
  shows "L (erase a) =  L (erase (bsimp a))"
  and "L (erase a) = {flat v | v. \<Turnstile> v: (erase a)}"
  and "L (erase a) = {flat v | v. \<Turnstile> v: (erase (bsimp a))}"
  using L_bsimp_erase apply(blast)
  apply (simp add: L_flat_Prf)
  using L_bsimp_erase L_flat_Prf apply(auto)[1]
  done  
    


lemma L07XX:
  assumes "s \<in> L (erase a)"
  shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))"
  using assms
  by (meson lexer_correct_None lexer_correctness(1) lexer_flex)

lemma LX0:
  assumes "s \<in> L r"
  shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))"
  by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex)

lemma L1:
  assumes "s \<in> r \<rightarrow> v" 
  shows "decode (bmkeps (bders (intern r) s)) r = Some v"
  using assms
  by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1))

lemma L2:
  assumes "s \<in> (der c r) \<rightarrow> v" 
  shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)"
  using assms
  apply(subst bmkeps_retrieve)
  using Posix1(1) lexer_correct_None lexer_flex apply fastforce
  using MAIN_decode
  apply(subst MAIN_decode[symmetric])
   apply(simp)
   apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable)
  apply(simp)
  apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))")
   prefer 2
   apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1))
  apply(simp)
  apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) =
    (flex (der c r) ((\<lambda>v. injval r c v) o id) s (mkeps (ders s (der c r))))")
   apply(simp)
  using flex_fun_apply by blast
  
lemma L3:
  assumes "s2 \<in> (ders s1 r) \<rightarrow> v" 
  shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)"
  using assms
  apply(induct s1 arbitrary: r s2 v rule: rev_induct)
   apply(simp)
  using L1 apply blast
  apply(simp add: ders_append)
  apply(drule_tac x="r" in meta_spec)
  apply(drule_tac x="x # s2" in meta_spec)
  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
  apply(drule meta_mp)
   defer
   apply(simp)
   apply(simp add:  flex_append)
  by (simp add: Posix_injval)



lemma bders_snoc:
  "bder c (bders a s) = bders a (s @ [c])"
  apply(simp add: bders_append)
  done


lemma QQ1:
  shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
  apply(simp)
  apply(simp add: bsimp_idem)
  done

lemma QQ2:
  shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]"
  apply(simp)
  done

lemma XXX2a_long:
  assumes "good a"
  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
  using  assms
  apply(induct a arbitrary: c taking: asize rule: measure_induct)
  apply(case_tac x)
       apply(simp)
      apply(simp)
     apply(simp)
  prefer 3
    apply(simp)
   apply(simp)
   apply(auto)[1]
apply(case_tac "x42 = AZERO")
     apply(simp)
   apply(case_tac "x43 = AZERO")
     apply(simp)
  using test2 apply force  
  apply(case_tac "\<exists>bs. x42 = AONE bs")
     apply(clarify)
     apply(simp)
    apply(subst bsimp_ASEQ1)
       apply(simp)
  using b3 apply force
  using bsimp_ASEQ0 test2 apply force
  thm good_SEQ test2
     apply (simp add: good_SEQ test2)
    apply (simp add: good_SEQ test2)
  apply(case_tac "x42 = AZERO")
     apply(simp)
   apply(case_tac "x43 = AZERO")
    apply(simp)
  apply (simp add: bsimp_ASEQ0)
  apply(case_tac "\<exists>bs. x42 = AONE bs")
     apply(clarify)
     apply(simp)
    apply(subst bsimp_ASEQ1)
      apply(simp)
  using bsimp_ASEQ0 test2 apply force
     apply (simp add: good_SEQ test2)
    apply (simp add: good_SEQ test2)
  apply (simp add: good_SEQ test2)
  (* AALTs case *)
  apply(simp)
  using test2 by fastforce


lemma bder_bsimp_AALTs:
  shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
  apply(induct bs rs rule: bsimp_AALTs.induct)
    apply(simp)
   apply(simp)
   apply (simp add: bder_fuse)
  apply(simp)
  done

lemma flts_nothing:
  assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
  shows "flts rs = rs"
  using assms
  apply(induct rs rule: flts.induct)
        apply(auto)
  done

lemma flts_flts:
  assumes "\<forall>r \<in> set rs. good r"
  shows "flts (flts rs) = flts rs"
  using assms
  apply(induct rs taking: "\<lambda>rs. sum_list  (map asize rs)" rule: measure_induct)
  apply(case_tac x)
   apply(simp)
  apply(simp)
  apply(case_tac a)
       apply(simp_all  add: bder_fuse flts_append)
  apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO")
   prefer 2
  apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2)
  apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r")
   prefer 2
   apply (metis n0 nn1b test2)
  by (metis flts_fuse flts_nothing)


lemma iii:
  assumes "bsimp_AALTs bs rs \<noteq> AZERO"
  shows "rs \<noteq> []"
  using assms
  apply(induct bs  rs rule: bsimp_AALTs.induct)
    apply(auto)
  done

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))"
  apply(induct as arbitrary: bs)
   apply(simp)
  apply(simp)
  by (simp add: bsimp_idem comp_def)
  
lemma CT1a:
  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 CTa:
  assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
  shows  "flts as = as"
  using assms
  apply(induct as)
   apply(simp)
  apply(case_tac as)
   apply(simp)
  apply (simp add: k0b)
  using flts_nothing by auto

lemma CT0:
  assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" 
  shows "flts [bsimp_AALTs bs1 as1] =  flts (map (fuse bs1) as1)"
  using assms CTa
  apply(induct as1 arbitrary: bs1)
    apply(simp)
   apply(simp)
  apply(case_tac as1)
   apply(simp)
  apply(simp)
proof -
fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list"
  assume a1: "nonalt a \<and> a \<noteq> AZERO \<and> nonalt aa \<and> aa \<noteq> AZERO \<and> (\<forall>r\<in>set list. nonalt r \<and> r \<noteq> AZERO)"
  assume a2: "\<And>as. \<forall>r\<in>set as. nonalt r \<and> r \<noteq> AZERO \<Longrightarrow> flts as = as"
  assume a3: "as1a = aa # list"
  have "flts [a] = [a]"
using a1 k0b by blast
then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)"
  using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9))
qed
  
  
lemma CT01:
  assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" "\<forall>r \<in> set as2. nonalt r \<and> r \<noteq> AZERO" 
  shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] =  flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))"
  using assms CT0
  by (metis k0 k00)
  


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))"
  using assms
  apply(induct as)
   apply(auto)
  done

lemma asize_set:
  assumes "a \<in> set as"
  shows "asize a < Suc (sum_list (map asize as))"
  using assms
  apply(induct as arbitrary: a)
   apply(auto)
  using le_add2 le_less_trans not_less_eq by blast

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

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)


lemma contains_equiv_def:
  shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
  by (meson contains0 contains49 contains59 contains60)

lemma derc_alt:
  assumes "bder c (AALTs [] as) >> bs"
  shows "bder c (bsimp(AALTs [] as)) >> bs"
  using assms
  apply -
  using contains_equiv_def
  apply -
  apply(drule_tac  x="[]" in meta_spec)
  apply(drule_tac x="as" in meta_spec)
  apply(drule_tac x="bs" in meta_spec)
  
  oops

lemma transfer:
  assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)"
  shows "a \<Rightarrow> b"
  
(*if we have proved that a can prove c, to prove a can prove b, we
then have the option to just show that c can prove b *)
(*how to express the above using drule+mp and a lemma*)

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"

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)

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


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
  

(*
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 "\<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)"
  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)
  by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))

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"
  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 _ >> _"
  oops


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 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)
  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 _ _) _"
find_theorems "_ >> retrieve _ _"
find_theorems "bder _ _ >> _"


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
  fixes n :: nat
  shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2"
  apply(induct n)
  apply(simp)
  apply(simp)
  done

lemma COUNTEREXAMPLE:
  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
  shows "bsimp (bder c (bsimp r)) = bsimp (bder c r)"
  apply(simp_all add: assms)
  oops

lemma COUNTEREXAMPLE:
  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
  shows "bsimp r = r"
  apply(simp_all add: assms)
  oops

lemma COUNTEREXAMPLE:
  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
  shows "bsimp r = XXX"
  and   "bder c r = XXX"
  and   "bder c (bsimp r) = XXX"
  and   "bsimp (bder c (bsimp r)) = XXX"
  and   "bsimp (bder c r) = XXX"
  apply(simp_all add: assms)
  oops

lemma COUNTEREXAMPLE_contains1:
  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
  and   "bsimp (bder c r) >> bs"
  shows "bsimp (bder c (bsimp r)) >> bs"
  using assms 
  apply(auto elim!: contains.cases)
   apply(rule Etrans)
    apply(rule contains.intros)
    apply(rule contains.intros)
   apply(simp)
  apply(rule Etrans)
    apply(rule contains.intros)
    apply(rule contains.intros)
  apply(simp)
  done

lemma COUNTEREXAMPLE_contains2:
  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
  and   "bsimp (bder c (bsimp r)) >> bs"
  shows "bsimp (bder c r) >> bs" 
  using assms 
  apply(auto elim!: contains.cases)
   apply(rule Etrans)
    apply(rule contains.intros)
    apply(rule contains.intros)
   apply(simp)
  apply(rule Etrans)
    apply(rule contains.intros)
    apply(rule contains.intros)
  apply(simp)
  done


end