
theory SizeBound3
  imports "ClosedFormsBounds"
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)"

function
  decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
where
  "decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CH 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) = CH 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)"

fun rerase :: "arexp \<Rightarrow> rrexp"
where
  "rerase AZERO = RZERO"
| "rerase (AONE _) = RONE"
| "rerase (ACHAR _ c) = RCHAR c"
| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
| "rerase (ASTAR _ r) = RSTAR (rerase r)"



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

lemma fuse_Nil:
  shows "fuse [] r = r"
  by (induct r)(simp_all)

(*
lemma map_fuse_Nil:
  shows "map (fuse []) rs = rs"
  by (induct rs)(simp_all add: fuse_Nil)
*)

fun intern :: "rexp \<Rightarrow> arexp" where
  "intern ZERO = AZERO"
| "intern ONE = AONE []"
| "intern (CH 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"

abbreviation
  bnullables :: "arexp list \<Rightarrow> bool"
where
  "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)"

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

lemma bmkepss1:
  assumes "\<not> bnullables rs1"
  shows "bmkepss (rs1 @ rs2) = bmkepss rs2"
  using assms
  by (induct rs1) (auto)

lemma bmkepss2:
  assumes "bnullables rs1"
  shows "bmkepss (rs1 @ rs2) = bmkepss rs1"
  using assms
  by (induct rs1) (auto)


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 rbnullable_correctness:
  shows "rnullable (rerase r) = bnullable r"
  apply(induct r rule: rerase.induct)
       apply simp+
  done


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

lemma rerase_fuse:
  shows "rerase (fuse bs r) = rerase r"
  apply(induct r)
       apply simp+
  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 bnullable_fuse:
  shows "bnullable (fuse bs r) = bnullable r"
  apply(induct r arbitrary: bs)
  apply(auto)
  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 bnullable_Hdbmkeps_Hd:
  assumes "bnullable a" 
  shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
  using assms by simp
*)


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" 
          "bnullables rs"
  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. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
          "bnullables rs"
  shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
 using assms
  apply(induct rs arbitrary: bs)
  apply(auto)
  apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
  apply (metis r3)
  apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
  apply (metis r3)
  done


lemma bmkeps_retrieve:
  assumes "bnullable r"
  shows "bmkeps r = retrieve r (mkeps (erase r))"
  using assms
  apply(induct r)
  apply(auto)
  using t by auto

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 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
      using bnullable_correctness by force 
    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
    by (auto simp add: bnullable_correctness[symmetric])
qed


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

lemma bsimp_ASEQ0[simp]:
  shows "bsimp_ASEQ bs r1 AZERO = AZERO"
  by (case_tac r1)(simp_all)

lemma bsimp_ASEQ1:
  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = 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[simp]:
  shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
  by (case_tac r2) (simp_all)


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 (distinctBy (flts (map bsimp rs)) rerase {}) "
| "bsimp r = r"


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_all)
  done

lemma L_bsimp_ASEQ:
  "L (erase (ASEQ bs r1 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 RL_bsimp_ASEQ:
  "RL (rerase (ASEQ bs r1 r2)) = RL (rerase (bsimp_ASEQ bs r1 r2))"
  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
  apply simp+
  done

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 RL_bsimp_AALTs:
 "RL (rerase (AALTs bs rs)) = RL (rerase (bsimp_AALTs bs rs))"
  apply(induct bs rs rule: bsimp_AALTs.induct)
  apply(simp_all add: rerase_fuse)
  done

lemma RL_rerase_AALTs:
  shows "RL (rerase (AALTs bs rs)) = \<Union> (RL ` rerase ` (set rs))"
  apply(induct rs)
   apply(simp)
  apply(simp)
  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 RL_erase_flts:
  shows "\<Union> (RL ` rerase ` (set (flts rs))) =
         \<Union> (RL ` rerase ` (set rs))"
  apply(induct rs rule: flts.induct)
        apply simp+
      apply auto
  apply (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))
  by (smt (verit, best) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))




lemma L_erase_dB_acc:
  shows "(\<Union> (L ` acc) \<union> (\<Union> (L ` erase ` (set (distinctBy rs erase acc))))) 
            = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"
  apply(induction rs arbitrary: acc)
  apply simp_all
  by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)

lemma RL_rerase_dB_acc:
  shows "(\<Union> (RL ` acc) \<union> (\<Union> (RL ` rerase ` (set (distinctBy rs rerase acc)))))
           = \<Union> (RL ` acc) \<union> \<Union> (RL ` rerase ` (set rs))"
  apply(induction rs arbitrary: acc)
   apply simp_all
    by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)




lemma L_erase_dB:
  shows "(\<Union> (L ` erase ` (set (distinctBy rs erase {})))) = \<Union> (L ` erase ` (set rs))"
  by (metis L_erase_dB_acc Un_commute Union_image_empty)

lemma RL_rerase_dB:
  shows "(\<Union> (RL ` rerase ` (set (distinctBy rs rerase {})))) = \<Union> (RL ` rerase ` (set rs))"
  by (metis RL_rerase_dB_acc Un_commute Union_image_empty)


lemma RL_bsimp_rerase:
  shows "RL (rerase r) = RL (rerase (bsimp r))"
  apply(induct r)
  apply(simp)
  apply(simp)
  apply(simp)
  apply(auto simp add: Sequ_def)[1]
  apply(subst RL_bsimp_ASEQ[symmetric])
  apply(auto simp add: Sequ_def)[1]
  apply(subst (asm)  RL_bsimp_ASEQ[symmetric])
  apply(auto simp add: Sequ_def)[1]
  apply(simp)
  apply(subst RL_bsimp_AALTs[symmetric])
  defer
  apply(simp)
  using RL_erase_flts RL_rerase_dB by force

lemma rder_correctness:
  shows "RL (rder c r) = Der c (RL r)"
  by (simp add: RL_rder)




lemma asize_rsize:
  shows "rsize (rerase r) = asize r"
  apply(induct r)
       apply simp+
  
  apply (metis (mono_tags, lifting) comp_apply map_eq_conv)
  by simp

lemma rb_nullability:
  shows " rnullable (rerase a) = bnullable a"
  apply(induct a)
       apply simp+
  done

lemma fuse_anything_doesnt_matter:
  shows "rerase a = rerase (fuse bs a)"
  by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))



lemma rder_bder_rerase:
  shows "rder c (rerase r ) = rerase (bder c r)"
  apply (induct r)
       apply simp+
    apply(case_tac "bnullable r1")
     apply simp
  apply (simp add: rb_nullability rerase_fuse)
  using rb_nullability apply presburger
   apply simp
  apply simp
  using rerase_fuse by presburger




lemma RL_bder_preserved:
  shows "RL (rerase a1) = RL (rerase a2) \<Longrightarrow> RL (rerase (bder c a1 )) = RL (rerase (bder c a2))"
  by (metis rder_bder_rerase rder_correctness)


lemma RL_bders_simp:
  shows "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))"
  apply(induct s arbitrary: r rule: rev_induct)
  apply(simp)
  apply(simp add: bders_append)
  apply(simp add: bders_simp_append)
  apply(simp add: RL_bsimp_rerase[symmetric])
  using RL_bder_preserved by blast



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

lemma bmkepss_fuse: 
  assumes "bnullables rs"
  shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
  using assms
  apply(induct rs arbitrary: bs)
  apply(auto simp add: bmkeps_fuse bnullable_fuse)
  done


lemma b4:
  shows "bnullable (bders_simp r s) = bnullable (bders r s)"
proof -
  have "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))"
    by (simp add: RL_bders_simp)
  then show "bnullable (bders_simp r s) = bnullable (bders r s)"
    using RL_rnullable rb_nullability by blast
qed


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




inductive 
  rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
and 
  srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)
where
  bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"
| bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"
| bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| bs6: "AALTs bs [] \<leadsto> AZERO"
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
| ss1:  "[] s\<leadsto> []"
| ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
| ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
| ss4:  "(AZERO # rs) s\<leadsto> rs"
| ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
| ss6:  "rerase a1 = rerase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"


inductive 
  rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
where 
  rs1[intro, simp]:"r \<leadsto>* r"
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"

inductive 
  srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100)
where 
  sss1[intro, simp]:"rs s\<leadsto>* rs"
| sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"


lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
  using rrewrites.intros(1) rrewrites.intros(2) by blast
 
lemma rrewrites_trans[trans]: 
  assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
  shows "r1 \<leadsto>* r3"
  using a2 a1
  apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) 
  apply(auto)
  done

lemma srewrites_trans[trans]: 
  assumes a1: "r1 s\<leadsto>* r2"  and a2: "r2 s\<leadsto>* r3"
  shows "r1 s\<leadsto>* r3"
  using a1 a2
  apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) 
   apply(auto)
  done



lemma contextrewrites0: 
  "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
  apply(induct rs1 rs2 rule: srewrites.inducts)
   apply simp
  using bs10 r_in_rstar rrewrites_trans by blast

lemma contextrewrites1: 
  "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
  apply(induct r r' rule: rrewrites.induct)
   apply simp
  using bs10 ss3 by blast

lemma srewrite1: 
  shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
  apply(induct rs)
   apply(auto)
  using ss2 by auto

lemma srewrites1: 
  shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"
  apply(induct rs1 rs2 rule: srewrites.induct)
   apply(auto)
  using srewrite1 by blast

lemma srewrite2: 
  shows  "r1 \<leadsto> r2 \<Longrightarrow> True"
  and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
  apply(induct rule: rrewrite_srewrite.inducts)
               apply(auto)
     apply (metis append_Cons append_Nil srewrites1)
    apply(meson srewrites.simps ss3)
  apply (meson srewrites.simps ss4)
  apply (meson srewrites.simps ss5)
  by (metis append_Cons append_Nil srewrites.simps ss6)
  

lemma srewrites3: 
  shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
  apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct)
   apply(auto)
  by (meson srewrite2(2) srewrites_trans)

(*
lemma srewrites4:
  assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" 
  shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"
  using assms
  apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)
  apply (simp add: srewrites3)
  using srewrite1 by blast
*)

lemma srewrites6:
  assumes "r1 \<leadsto>* r2" 
  shows "[r1] s\<leadsto>* [r2]"
  using assms
  apply(induct r1 r2 rule: rrewrites.induct)
   apply(auto)
  by (meson srewrites.simps srewrites_trans ss3)

lemma srewrites7:
  assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" 
  shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
  using assms
  by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)

lemma ss6_stronger_aux:
  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 rerase (set (map rerase rs1)))"
  apply(induct rs2 arbitrary: rs1)
   apply(auto)
  apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
  apply(drule_tac x="rs1 @ [a]" in meta_spec)
  apply(simp)
  done



lemma ss6_stronger:
  shows "rs1 s\<leadsto>* distinctBy rs1 rerase {}"
  by (metis append_Nil list.set(1) list.simps(8) ss6_stronger_aux)


lemma rewrite_preserves_fuse: 
  shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
  and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
proof(induct rule: rrewrite_srewrite.inducts)
  case (bs3 bs1 bs2 r)
  then show ?case
    by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) 
next
  case (bs7 bs r)
  then show ?case
    by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) 
next
  case (ss2 rs1 rs2 r)
  then show ?case
    using srewrites7 by force 
next
  case (ss3 r1 r2 rs)
  then show ?case by (simp add: r_in_rstar srewrites7)
next
  case (ss5 bs1 rs1 rsb)
  then show ?case 
    apply(simp)
    by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
next
  case (ss6 a1 a2 rsa rsb rsc)
  then show ?case 
    apply(simp only: map_append)
    by (smt (verit, ccfv_threshold) rerase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)  
qed (auto intro: rrewrite_srewrite.intros)


lemma rewrites_fuse:  
  assumes "r1 \<leadsto>* r2"
  shows "fuse bs r1 \<leadsto>* fuse bs r2"
using assms
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
done


lemma star_seq:  
  assumes "r1 \<leadsto>* r2"
  shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
using assms
apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
apply(auto intro: rrewrite_srewrite.intros)
done

lemma star_seq2:  
  assumes "r3 \<leadsto>* r4"
  shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
  using assms
apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
apply(auto intro: rrewrite_srewrite.intros)
done

lemma continuous_rewrite: 
  assumes "r1 \<leadsto>* AZERO"
  shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
using assms bs1 star_seq by blast

(*
lemma continuous_rewrite2: 
  assumes "r1 \<leadsto>* AONE bs"
  shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"
  using assms  by (meson bs3 rrewrites.simps star_seq)
*)

lemma bsimp_aalts_simpcases: 
  shows "AONE bs \<leadsto>* bsimp (AONE bs)"  
  and   "AZERO \<leadsto>* bsimp AZERO" 
  and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
  by (simp_all)

lemma bsimp_AALTs_rewrites: 
  shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
  by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)

lemma trivialbsimp_srewrites: 
  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
  apply(induction rs)
   apply simp
  apply(simp)
  using srewrites7 by auto



lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
  apply(induction rs rule: flts.induct)
  apply(auto intro: rrewrite_srewrite.intros)
  apply (meson srewrites.simps srewrites1 ss5)
  using rs1 srewrites7 apply presburger
  using srewrites7 apply force
  apply (simp add: srewrites7)
  by (simp add: srewrites7)

lemma bnullable0:
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" 
  and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" 
  apply(induct rule: rrewrite_srewrite.inducts)
  apply(auto simp add:  bnullable_fuse)
   apply (meson UnCI bnullable_fuse imageI)
  by (metis rb_nullability)


lemma rewritesnullable: 
  assumes "r1 \<leadsto>* r2" 
  shows "bnullable r1 = bnullable r2"
using assms 
  apply(induction r1 r2 rule: rrewrites.induct)
  apply simp
  using bnullable0(1) by auto

lemma rewrite_bmkeps_aux: 
  shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"
  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" 
proof (induct rule: rrewrite_srewrite.inducts)
  case (bs3 bs1 bs2 r)
  then show ?case by (simp add: bmkeps_fuse) 
next
  case (bs7 bs r)
  then show ?case by (simp add: bmkeps_fuse) 
next
  case (ss3 r1 r2 rs)
  then show ?case
    by (metis bmkepss.simps(2) bnullable0(1))
next
  case (ss5 bs1 rs1 rsb)
  then show ?case
    by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
next
  case (ss6 a1 a2 rsa rsb rsc)
  then show ?case
    by (smt (z3) append_is_Nil_conv bmkepss1 bmkepss2 in_set_conv_decomp_first list.set_intros(1) rb_nullability set_ConsD)
qed (auto)

lemma rewrites_bmkeps: 
  assumes "r1 \<leadsto>* r2" "bnullable r1" 
  shows "bmkeps r1 = bmkeps r2"
  using assms
proof(induction r1 r2 rule: rrewrites.induct)
  case (rs1 r)
  then show "bmkeps r = bmkeps r" by simp
next
  case (rs2 r1 r2 r3)
  then have IH: "bmkeps r1 = bmkeps r2" by simp
  have a1: "bnullable r1" by fact
  have a2: "r1 \<leadsto>* r2" by fact
  have a3: "r2 \<leadsto> r3" by fact
  have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) 
  then have "bmkeps r2 = bmkeps r3"
    using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast 
  then show "bmkeps r1 = bmkeps r3" using IH by simp
qed


lemma rewrites_to_bsimp: 
  shows "r \<leadsto>* bsimp r"
proof (induction r rule: bsimp.induct)
  case (1 bs1 r1 r2)
  have IH1: "r1 \<leadsto>* bsimp r1" by fact
  have IH2: "r2 \<leadsto>* bsimp r2" by fact
  { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO"
    with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
    then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
      by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)  
    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto
  }
  moreover
  { assume "\<exists>bs. bsimp r1 = AONE bs"
    then obtain bs where as: "bsimp r1 = AONE bs" by blast
    with IH1 have "r1 \<leadsto>* AONE bs" by simp
    then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
    with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)"
      using rewrites_fuse by (meson rrewrites_trans) 
    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp
    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) 
  } 
  moreover
  { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" 
    then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" 
      by (simp add: bsimp_ASEQ1) 
    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2
      by (metis rrewrites_trans star_seq star_seq2) 
    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp
  } 
  ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast
next
  case (2 bs1 rs)
  have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact
  then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)
  also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) 
  also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) rerase {}" by (simp add: ss6_stronger) 
  finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {})"
    using contextrewrites0 by auto
  also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctBy (flts (map bsimp rs)) rerase {})"
    by (simp add: bsimp_AALTs_rewrites)     
  finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp
qed (simp_all)


lemma to_zero_in_alt: 
  shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
  by (simp add: bs1 bs10 ss3)



lemma  bder_fuse_list: 
  shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
  apply(induction rs1)
  apply(simp_all add: bder_fuse)
  done


lemma rewrite_preserves_bder: 
  shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
proof(induction rule: rrewrite_srewrite.inducts)
  case (bs1 bs r2)
  then show ?case
    by (simp add: continuous_rewrite) 
next
  case (bs2 bs r1)
  then show ?case 
    apply(auto)
    apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
    by (simp add: r_in_rstar rrewrite_srewrite.bs2)
next
  case (bs3 bs1 bs2 r)
  then show ?case 
    apply(simp)
    
    by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
next
  case (bs4 r1 r2 bs r3)
  have as: "r1 \<leadsto> r2" by fact
  have IH: "bder c r1 \<leadsto>* bder c r2" by fact
  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
    by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
next
  case (bs5 r3 r4 bs r1)
  have as: "r3 \<leadsto> r4" by fact 
  have IH: "bder c r3 \<leadsto>* bder c r4" by fact 
  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
    apply(simp)
    apply(auto)
    using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
    using star_seq2 by blast
next
  case (bs6 bs)
  then show ?case
    using rrewrite_srewrite.bs6 by force 
next
  case (bs7 bs r)
  then show ?case
    by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 
next
  case (bs10 rs1 rs2 bs)
  then show ?case
    using contextrewrites0 by force    
next
  case ss1
  then show ?case by simp
next
  case (ss2 rs1 rs2 r)
  then show ?case
    by (simp add: srewrites7) 
next
  case (ss3 r1 r2 rs)
  then show ?case
    by (simp add: srewrites7) 
next
  case (ss4 rs)
  then show ?case
    using rrewrite_srewrite.ss4 by fastforce 
next
  case (ss5 bs1 rs1 rsb)
  then show ?case 
    apply(simp)
    using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
next
  case (ss6 a1 a2 bs rsa rsb)
  then show ?case
    apply(simp only: map_append)
    by (smt (verit, best) rder_bder_rerase list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps)
qed

lemma rewrites_preserves_bder: 
  assumes "r1 \<leadsto>* r2"
  shows "bder c r1 \<leadsto>* bder c r2"
using assms  
apply(induction r1 r2 rule: rrewrites.induct)
apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
done


lemma central:  
  shows "bders r s \<leadsto>* bders_simp r s"
proof(induct s arbitrary: r rule: rev_induct)
  case Nil
  then show "bders r [] \<leadsto>* bders_simp r []" by simp
next
  case (snoc x xs)
  have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
  have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
  also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
    by (simp add: rewrites_preserves_bder)
  also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
    by (simp add: rewrites_to_bsimp)
  finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
    by (simp add: bders_simp_append)
qed

lemma main_aux: 
  assumes "bnullable (bders r s)"
  shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
proof -
  have "bders r s \<leadsto>* bders_simp r s" by (rule central)
  then 
  show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
    by (rule rewrites_bmkeps)
qed  




theorem main_blexer_simp: 
  shows "blexer r s = blexer_simp r s"
  unfolding blexer_def blexer_simp_def
  using b4 main_aux by simp


theorem blexersimp_correctness: 
  shows "lexer r s = blexer_simp r s"
  using blexer_correctness main_blexer_simp by simp



lemma rerase_preimage:
  shows "rerase r = RZERO \<Longrightarrow> r = AZERO"
  apply(case_tac r)
       apply simp+
  done

lemma rerase_preimage2:
  shows "rerase r = RONE \<Longrightarrow> \<exists>bs. r = AONE bs"
  apply(case_tac r)
       apply simp+
  done

lemma rerase_preimage3:
  shows "rerase r= RCHAR c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
  apply(case_tac r)
       apply simp+
  done

lemma rerase_preimage4:
  shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2"
  apply(case_tac r)
       apply(simp)+
  done

lemma rerase_preimage5:
  shows "rerase r = RALTS rs \<Longrightarrow> \<exists>bs as. r = AALTs bs as \<and> map rerase as = rs"
  apply(case_tac r)
       apply(simp)+
  done

lemma rerase_preimage6:
  shows "rerase r = RSTAR r0 \<Longrightarrow> \<exists>bs a0. r = ASTAR bs a0 \<and> rerase a0 = r0 "
  apply(case_tac r)
       apply(simp)+
  done

lemma map_rder_bder:
  shows "\<lbrakk> \<And>xa a. \<lbrakk>xa \<in> set x; rerase a = xa\<rbrakk> \<Longrightarrow> rerase (bder c a) = rder c xa;
         map rerase as = x\<rbrakk> \<Longrightarrow>
        map rerase (map (bder c) as) = map (rder c) x"
  apply(induct x arbitrary: as)
   apply simp+
  by force


lemma der_rerase:
  shows "rerase a = r \<Longrightarrow> rerase (bder c a) = rder c r"
  apply(induct r arbitrary: a)
       apply simp
  using rerase_preimage apply fastforce
  using rerase_preimage2 apply force
     apply (metis bder.simps(3) rder.simps(3) rerase.simps(1) rerase.simps(2) rerase_preimage3)
    apply(insert rerase_preimage4)[1]
    apply(subgoal_tac " \<exists>bs a1 a2. a = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2")
  prefer 2
     apply presburger
    apply(erule exE)+
    apply(erule conjE)+
    apply(subgoal_tac " rerase (bder c a1) = rder c r1")
  prefer 2
     apply blast
    apply(subgoal_tac " rerase (bder c a2) = rder c r2")
  prefer 2
     apply blast
    apply(case_tac "rnullable r1")
     apply(subgoal_tac "bnullable a1")
  apply simp
  using fuse_anything_doesnt_matter apply presburger
  using rb_nullability apply blast
    apply (metis bder.simps(5) rb_nullability rder.simps(5) rerase.simps(5))
  apply simp
   apply(insert rerase_preimage5)[1]
   apply(subgoal_tac "\<exists>bs as. a = AALTs bs as \<and> map rerase as = x")
  prefer 2
  
    apply blast
   apply(erule exE)+
   apply(erule conjE)+
  apply(subgoal_tac "map rerase (map (bder c) as) = map (rder c) x")
  using bder.simps(4) rerase.simps(4) apply presburger
  using map_rder_bder apply blast
  using fuse_anything_doesnt_matter rerase_preimage6 by force

lemma der_rerase2:
  shows "rerase (bder c a) = rder c (rerase a)"
  using der_rerase by force

lemma ders_rerase:
  shows "rerase (bders a s) = rders (rerase a) s"
  apply(induct s rule: rev_induct)
   apply simp
  by (simp add: bders_append der_rerase rders_append)

lemma rerase_bsimp_ASEQ:
  shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"
  by (smt (verit, ccfv_SIG) SizeBound3.bsimp_ASEQ0 SizeBound3.bsimp_ASEQ2 basic_rsimp_SEQ_property1 basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 bsimp_ASEQ.simps(1) bsimp_ASEQ1 fuse_anything_doesnt_matter rerase.simps(1) rerase.simps(2) rerase.simps(5) rerase_preimage rerase_preimage2 rsimp_SEQ.simps(1))

lemma rerase_bsimp_AALTs:
  shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"
  apply(induct rs arbitrary: bs)
   apply simp+
  by (smt (verit, ccfv_threshold) Cons_eq_map_conv bsimp_AALTs.elims fuse_anything_doesnt_matter list.discI list.inject list.simps(9) rerase.simps(4) rsimp_ALTs.elims)


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


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


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


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 bbbbs:
  assumes "agood r" "r = AALTs bs1 rs"
  shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
  using  assms
  by (smt (verit, ccfv_SIG) Cons_eq_map_conv agood.simps(4) agood.simps(5) append.right_neutral bsimp_AALTs.elims flts.simps(1) flts.simps(3) list.map_disc_iff)

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



lemma good_fuse:
  shows "agood (fuse bs r) = agood 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. anonalt r" "distinct (map rerase rs)"
  shows "agood (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. agood r)"
  using  assms
  apply(induct bs rs rule: bsimp_AALTs.induct)
    apply simp+
   apply (simp add: good_fuse)
  apply(subgoal_tac "bsimp_AALTs bs1 (v # vb # vc) = AALTs bs1 (v # vb # vc)")
   prefer 2

  
  using bsimp_AALTs.simps(3) apply presburger
  apply(simp only:)
  apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\<forall>r \<in> (set (v # vb # vc)). agood r \<and> anonalt r) \<and> distinct (map rerase (v # vb # vc)))")
  prefer 2
  using agood.simps(6) apply blast
  apply(simp only:)
  apply(subgoal_tac "((\<forall>r\<in>set (v # vb # vc). agood r \<and> anonalt r) \<and> distinct (map rerase (v # vb # vc))) = ((\<forall>r\<in>set (v # vb # vc). agood r) \<and> distinct (map rerase (v # vb # vc)))")
  prefer 2
  apply blast
  apply(simp only:)
  apply(subgoal_tac "((\<forall>r \<in> set (v # vb # vc). agood r) \<and> distinct (map rerase (v # vb # vc))) = (\<forall> r \<in> set (v # vb # vc). agood r) ")
  prefer 2
   apply(subgoal_tac "distinct (map rerase (v # vb # vc)) = True")
    prefer 2
    apply blast
  prefer 2
   apply force
  apply simp
  done


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




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

lemma flts1:
  assumes "agood 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 "agood r" 
  shows "\<forall>r' \<in> set (flts [r]). agood r' \<and> anonalt r'"
  using  assms
  apply(induct r)
       apply(simp)
      apply(simp)
     apply(simp)
    prefer 2
    apply(simp)
    apply(auto)[1]
     apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) good_fuse)
  apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) nn11a)
   apply fastforce
  apply(simp)
  done  


lemma flts3:
  assumes "\<forall>r \<in> set rs. agood r \<or> r = AZERO" 
  shows "\<forall>r \<in> set (flts rs). agood r"
  using  assms
  apply(induct rs arbitrary: rule: flts.induct)
        apply(simp_all)
  by (metis SizeBound3.flts2 UnE append.right_neutral flts.simps(1) flts.simps(3) list.set_map)


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

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


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

lemma flts4_nogood:
  shows "bsimp_AALTs bs0 rs = AZERO \<Longrightarrow> \<forall>r \<in> set rs. \<not> agood r"
  by (metis SizeBound3.flts3b arexp.distinct(7) bsimp_AALTs.elims flts.simps(1) flts.simps(2) fuse_anything_doesnt_matter rerase.simps(1) rerase_preimage)

lemma flts4_append:
  shows "bsimp_AALTs bs0 (rs @ flts rsa) = AZERO \<Longrightarrow> bsimp_AALTs bs0 rs = AZERO"
  by (metis append_is_Nil_conv arexp.simps(13) bsimp_AALTs.elims bsimp_AALTs.simps(1) butlast_append butlast_snoc)

lemma flts4:
  assumes "bsimp_AALTs bs (flts rs) = AZERO"
  shows "\<forall>r \<in> set rs. \<not> agood 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 anonalt.simps(1) anonalt.simps(2))
       apply (metis agood.simps(1) agood.simps(2) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
      apply (metis agood.simps(1) agood.simps(3) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
     apply (metis agood.simps(1) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
    apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
  apply (metis agood.simps(1) agood.simps(33) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
  by (metis SizeBound3.bbbbs SizeBound3.k0a arexp.simps(13) flts4_append)

  
lemma flts_nil:
  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
            agood (bsimp y) \<or> bsimp y = AZERO"
  and "\<forall>r\<in>set rs. \<not> agood (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>
            agood (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 "agood (ASEQ bs r1 r2) = (agood r1 \<and> agood 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 asize0:
  shows "0 < asize r"
  apply(induct  r)
       apply(auto)
  done

lemma nn1qq:
  assumes "anonnested (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 nn1c:
  assumes "\<forall>r \<in> set rs. anonnested r"
  shows "\<forall>r \<in> set (flts rs). anonalt r"
  using assms
  apply(induct rs rule: flts.induct)
        apply(auto)
  apply(rule nn11a)
  by (metis nn1qq anonalt.elims(3))

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

  

lemma nn1bb:
  assumes "\<forall>r \<in> set rs. anonalt r"
  shows "anonnested (bsimp_AALTs bs rs)"
  using assms
  apply(induct bs rs rule: bsimp_AALTs.induct)
    apply(auto)
   apply (metis nn11a anonalt.simps(1) anonnested.elims(3))
  using n0 by auto

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

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

lemma dB_keeps_property:
  shows "(\<forall>r \<in> set rs. P r) \<longrightarrow> (\<forall>r \<in> set (distinctBy rs rerase rset). P r)"
  apply(induct rs arbitrary: rset)
   apply simp+
  done

lemma dB_filters_out:
  shows "rerase a \<in> rset \<Longrightarrow> a \<notin> set (distinctBy rs rerase (rset))"
  apply(induct rs arbitrary: rset)
   apply simp
  apply(case_tac "a = aa")
   apply simp+
  done

lemma dB_will_be_distinct:
  shows "distinct (distinctBy rs rerase (insert (rerase a) rset)) \<Longrightarrow> distinct (a #  (distinctBy rs rerase (insert (rerase a) rset)))"
  using dB_filters_out by force
  

lemma dB_does_the_job2:
  shows "distinct (distinctBy rs rerase rset)"
  apply(induct rs arbitrary: rset)
   apply simp
  apply(case_tac "rerase a \<in> rset")
   apply simp
  apply(drule_tac x = "insert (rerase a) rset" in meta_spec)
  apply(subgoal_tac "distinctBy (a # rs) rerase rset = a # distinctBy rs rerase (insert (rerase a ) rset)")
   apply(simp only:)
  using dB_will_be_distinct apply presburger
  by auto

lemma dB_does_more_job:
  shows "distinct (map rerase (distinctBy rs rerase rset))"
  apply(induct rs arbitrary:rset)
   apply simp
  apply(case_tac "rerase a \<in> rset")
   apply simp+
  using dB_filters_out by force

lemma dB_mono2:
  shows "rset \<subseteq> rset' \<Longrightarrow> distinctBy rs rerase rset = [] \<Longrightarrow> distinctBy rs rerase rset' = []"
  apply(induct rs arbitrary: rset rset')
   apply simp+
  by (meson in_mono list.discI)


lemma nn1b:
  shows "anonnested (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(case_tac "\<exists>bs. bsimp r1 = AONE bs")
    apply(auto)[1]
  apply (simp add: nn1a)    
   apply(subst bsimp_ASEQ1)
      apply(auto)
  apply(rule nn1bb)
  apply(auto)
  apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r")
  prefer 2
  apply (metis (mono_tags, lifting) SizeBound3.nn1c image_iff list.set_map)
  apply(subgoal_tac "\<forall>r \<in> set (distinctBy (flts (map bsimp x2a)) rerase {}). anonalt r")
   prefer 2
  using dB_keeps_property apply presburger
  by blast

lemma induct_smaller_elem_list:
  shows  "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))"
  apply(induct list)
   apply simp+
  by fastforce

lemma no0s_fltsbsimp:
  shows "\<forall>r \<in> set (flts (map bsimp rs)).  r \<noteq> AZERO"
  oops

lemma flts_all0s:
  shows "\<forall>r \<in> set rs. r = AZERO \<Longrightarrow> flts rs = []"
  apply(induct rs)
   apply simp+
  done





lemma good1:
  shows "agood (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)
   (*  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 agood, 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 agood 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)  
  using SizeBound3.flts3b distinctBy.elims apply force
  apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt")
       prefer 2
  apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
  using dB_keeps_property apply presburger
  

  using dB_does_more_job apply presburger
  apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood")
  using dB_keeps_property apply presburger
    apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)")
  using SizeBound3.flts3 apply blast

    apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (asize a + sum_list (map asize list))")
  
  apply simp

    apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))")
  
     apply fastforce
  using induct_smaller_elem_list apply blast


  

   apply simp
   apply(subgoal_tac "agood (bsimp a)")
  prefer 2
    apply blast
   apply(subgoal_tac "\<forall>r \<in> (set (map bsimp list)). r = AZERO \<or> agood r")
    prefer 2
  apply (metis add_Suc_right image_iff induct_smaller_elem_list list.set_map trans_less_add2)
   apply(subgoal_tac "\<not>(\<exists> r\<in>set (map bsimp list). agood r)")
  prefer 2
    apply (metis SizeBound3.flts3 SizeBound3.flts3b distinctBy.elims empty_iff flts4_nogood list.set_intros(1))
   apply(subgoal_tac "\<forall>r \<in> set (map bsimp list). r = AZERO")
  prefer 2
    apply blast
  apply(subgoal_tac "flts (map bsimp list) = []")
  prefer 2
  using flts_all0s apply presburger
  apply (smt (verit, del_insts) SizeBound3.flts2 SizeBound3.good0 SizeBound3.k0 dB_does_more_job dB_keeps_property distinctBy.simps(1) flts.simps(1))
  apply(subgoal_tac "agood (bsimp x42) \<or> bsimp x42 = AZERO")
   apply(subgoal_tac "agood (bsimp x43) \<or> bsimp x43 = AZERO")
    apply(case_tac "bsimp x42 = AZERO")
     apply simp
    apply(case_tac "bsimp x43 = AZERO")
     apply simp
    apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
  apply(erule exE)
  apply simp
  using good_fuse apply presburger
  apply simp
    apply(subgoal_tac "bsimp_ASEQ x41 (bsimp x42) (bsimp x43) = ASEQ x41 (bsimp x42) (bsimp x43)")
  prefer 2
  using bsimp_ASEQ1 apply presburger
  using SizeBound3.good_SEQ apply presburger
  using asize.simps(5) less_add_Suc2 apply presburger
  by simp

  




lemma good1a:
  assumes "RL (rerase a) \<noteq> {}"
  shows "agood (bsimp a)"
  using good1 assms
  using RL_bsimp_rerase 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 "agood (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 "anonnested (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 "anonnested (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 agood.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 "anonalt 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> agood y \<longrightarrow> bsimp y = y" 
          "\<forall>r'\<in>set rs. agood r' \<and> anonalt 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 agood.simps(1) k0b apply blast
  apply(auto)[1]  
  done
  





lemma nonalt_flts : shows 
  "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO"
  using SizeBound3.qqq1 by force


lemma rerase_map_bsimp:
  assumes "\<And> r. r \<in> set x2a \<Longrightarrow> rerase (bsimp r) = (rsimp \<circ> rerase) r"
  shows "  map rerase (map bsimp x2a) =  map (rsimp \<circ> rerase) x2a "
  using assms
  
  apply(induct x2a)
   apply simp
  apply(subgoal_tac "a \<in> set (a # x2a)")
  prefer 2
  apply (meson list.set_intros(1))
  apply(subgoal_tac "rerase (bsimp a ) = (rsimp \<circ> rerase) a")
  apply simp
  by presburger



lemma rerase_flts:
  shows "map rerase (flts rs) = rflts (map rerase rs)"
  apply(induct rs)
   apply simp+
  apply(case_tac a)
       apply simp+
   apply(simp add: rerase_fuse)
  apply simp
  done

lemma rerase_dB:
  shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc"
  apply(induct rs arbitrary: acc)
   apply simp+
  done
  



lemma rerase_earlier_later_same:
  assumes " \<And>r. r \<in> set x2a \<Longrightarrow> rerase (bsimp r) = rsimp (rerase r)"
  shows " (map rerase (distinctBy (flts (map bsimp x2a)) rerase {})) =
          (rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {})"
  apply(subst rerase_dB)
  apply(subst rerase_flts)
  apply(subst rerase_map_bsimp)
   apply auto
  using assms
  apply simp
  done



lemma simp_rerase:
  shows "rerase (bsimp a) = rsimp (rerase a)"
  apply(induct  a)
  apply simp+
  using rerase_bsimp_ASEQ apply presburger
  apply simp
   apply(subst rerase_bsimp_AALTs)
  apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) rerase {}) =  rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {}")  
    apply simp
  using rerase_earlier_later_same apply presburger
  apply simp
  done



lemma rders_simp_size:
  shows " rders_simp (rerase r) s  = rerase (bders_simp r s)"
  apply(induct s rule: rev_induct)
   apply simp
  apply(subst rders_simp_append)
  apply(subst bders_simp_append)
  apply(subgoal_tac "rders_simp (rerase r ) xs = rerase (bders_simp r xs)")
   apply(simp only:)
   apply simp
  apply (simp add: der_rerase2 simp_rerase)
  by simp




corollary aders_simp_finiteness:
  assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
  shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
  using assms
  apply(subgoal_tac "\<forall>s. asize (bders_simp r s) = rsize (rerase (bders_simp r s))")
   apply(erule exE)
   apply(rule_tac x = "N" in exI)
  using rders_simp_size apply auto[1]
  using asize_rsize by auto
  
theorem annotated_size_bound:
  shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
  apply(insert aders_simp_finiteness)
  by (simp add: rders_simp_bounded)

unused_thms


end
