
theory SizeBoundStrong
  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)"

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 nonalt :: "arexp \<Rightarrow> bool"
  where
  "nonalt (AALTs bs2 rs) = False"
| "nonalt 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

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"

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 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 (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 bnullable_Hdbmkeps_Hd)
     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


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

(*filter  (\<lambda>rt. case rt of 
                                      SEQ r1p r2p \<Rightarrow> r2p = (erase r2)
                                      r           \<Rightarrow> False ) allowableTerms*)


lemma dB_single_step: 
  shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
  by simp 

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"


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_ASEQ1 :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
  where
  "bsimp_ASEQ1 _ AZERO _ = AZERO"
| "bsimp_ASEQ1 bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
| "bsimp_ASEQ1 bs r1 r2 = ASEQ  bs r1 r2"


fun collect :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp list" where
  \<open>collect _ [] = []\<close>
|  \<open>collect erasedR2  ((SEQ r1 r2) # rs) = 
       (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\<close>
| \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>


fun pruneRexp where
  "pruneRexp (ASEQ bs r1 r2) allowableTerms = 
          (let termsTruncated = (collect (erase r2) allowableTerms) in 
             (let pruned = pruneRexp r1 termsTruncated in 
                (bsimp_ASEQ1 bs pruned r2)))"
| \<open>pruneRexp (AALTs bs rs) allowableTerms = 
     (let rsp = (filter (\<lambda>r. r \<noteq> AZERO)  (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
\<close>
| \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>


fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where
  \<open> oneSimp (SEQ ONE r) = r \<close>
| \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close>
| \<open> oneSimp r = r \<close>

fun breakIntoTerms where
  \<open>breakIntoTerms (SEQ r1 r2) = map (\<lambda>r1p. SEQ r1p r2) (breakIntoTerms r1)\<close>
| \<open>breakIntoTerms (ALT r1 r2) = (breakIntoTerms r1) @ (breakIntoTerms r2)\<close>
| \<open>breakIntoTerms r = r # [] \<close>

fun addToAcc :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp list"
  where
\<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close>

fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list"
  where
"dBStrong [] acc = []"
| "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
                            else let newSubRexps = (addToAcc r acc) in 
                                 (case (pruneRexp r newSubRexps) of  
                                    AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) |
                                    r1    \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc))
                                 )
                           )
                    "


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


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


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



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)) erase {}) "
| "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"

export_code bders_simp in Scala module_name Example

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 (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_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
  apply simp
  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 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_dB)
  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 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 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 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 bnullable_Hdbmkeps_Hd 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 qq3:
  assumes "bnullable (AALTs bs (rs @ rs1))"
          "bnullable (AALTs bs (rs @ rs2))"
          "\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow> 
               bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"
  shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"
  using assms
  apply(case_tac "\<exists>r \<in> set rs. bnullable r")
  using qq1 apply auto[1]
  by (metis UnE bnullable.simps(4) qq2 set_append)
  

lemma flts_append:
  shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)

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


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


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


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



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 bnullable_Hdbmkeps_Hd)
  apply(case_tac "bnullable a")
   apply (metis append.assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)
  apply(case_tac rs)
  apply(simp)
  apply(simp)
  apply(auto)[1]
   apply (metis bnullable_correctness erase_fuse)+
  done

lemma qq4:
  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: bnullable_Hdbmkeps_Hd)
     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: bnullable_Hdbmkeps_Hd)
   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: qq4)
  apply(simp)
  apply(auto)
   apply(case_tac list)
    apply(simp)
   apply(simp)
   apply (simp add: bnullable_Hdbmkeps_Hd)
  apply(case_tac "bnullable (ASEQ x41 x42 x43)")
   apply(case_tac list)
    apply(simp)
   apply(simp)
   apply (simp add: bnullable_Hdbmkeps_Hd)
  apply(simp)
  using qq4 r1 r2 by auto

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

fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp"
  where
"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
                          case r of (ASEQ bs r1 r2) \<Rightarrow> 
                            bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r1) ( ctx) )) r2   |
                                    (AALTs bs rs) \<Rightarrow> 
                            bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs))    |
                                    r             \<Rightarrow> r
)"



inductive 
  rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
where
  "ASEQ bs AZERO r2 \<leadsto> AZERO"
| "ASEQ bs r1 AZERO \<leadsto> AZERO"
| "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
| "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"
| "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
| "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"


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
  ss1: "[] s\<leadsto>* []"
| ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"


(* rewrites for lists *)
inductive 
  frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
where
  fs1: "[] f\<leadsto>* []"
| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"


lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
  using rrewrites.intros(1) rrewrites.intros(2) by blast
 
lemma real_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  many_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
  by (meson r_in_rstar real_trans)


lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))"
  apply(induct r r' rule: rrewrites.induct)
   apply simp
  by (metis append_Cons append_Nil rrewrite.intros(6) rs2)


lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))"
  apply(induct r r' rule: rrewrites.induct)
   apply simp
  using rrewrite.intros(6) by blast



lemma srewrites_alt: "rs1 s\<leadsto>* rs2 \<Longrightarrow> (AALTs bs (rs@rs1)) \<leadsto>* (AALTs bs (rs@rs2))"

  apply(induct rs1 rs2 arbitrary: bs rs rule: srewrites.induct)
   apply(rule rs1)
  apply(drule_tac x = "bs" in meta_spec)
  apply(drule_tac x = "rsa@[r']" in meta_spec)
  apply simp
  apply(rule real_trans)
   prefer 2
   apply(assumption)
  apply(drule contextrewrites2)
  apply auto
  done

corollary srewrites_alt1: 
  assumes "rs1 s\<leadsto>* rs2"
  shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
using assms
  by (metis append.left_neutral srewrites_alt)


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.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.intros)
done

lemma continuous_rewrite: 
  assumes "r1 \<leadsto>* AZERO"
  shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
using assms
  apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)
  apply(auto intro: rrewrite.intros r_in_rstar star_seq)
  by (meson rrewrite.intros(1) rs2 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 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(rule ss1)
  by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)


lemma bsimp_AALTs_rewrites: 
  "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
  apply(induction rs)
  apply simp
   apply(rule r_in_rstar)
  using rrewrite.intros(9) apply blast
  by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)



lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
  by (metis append_Cons append_Nil flts_single1 flts_append)

lemma fltsfrewrites: "rs f\<leadsto>* (flts rs)"
  apply(induction rs)
  apply simp
   apply(rule fs1)

  apply(case_tac "a = AZERO")

   
  using fs2 apply auto[1]
  apply(case_tac "\<exists>bs rs. a = AALTs bs rs")
   apply(erule exE)+
   
   apply (simp add: fs3)
  apply(subst flts_prepend)
    apply(rule nonalt.elims(2))
  prefer 2
  thm nonalt.elims
   
         apply blast
   
  using bbbbs1 apply blast
       apply(simp)+
   
   apply (meson nonazero.elims(3))
   
  by (meson fs4 nonalt.elims(3) nonazero.elims(3))


lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
  by (metis append_Cons append_Nil rrewrite.intros(7))


lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))"
  apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct)
    apply(rule rs1)
    apply(drule_tac x = "bs" in meta_spec)
  apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec)
    apply(rule real_trans)
     apply simp
  using rrewrite.intros(7) apply auto[1]
    apply(drule_tac x = "bsa" in meta_spec)
  apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec)
   apply(rule real_trans)
    apply simp
  using r_in_rstar rrewrite.intros(8) apply auto[1]
    apply(drule_tac x = "bs" in meta_spec)
  apply(drule_tac x = "rs1@[r]" in meta_spec)
    apply(rule real_trans)
   apply simp
  apply auto
  done

lemma flts_rewrites: "  AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
  apply(induction rs)
   apply simp
  apply(case_tac "a = AZERO")
  apply (metis flts.simps(2) many_steps_later rrewrite0away)

  apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
   apply(erule exE)+
   apply(simp)
   prefer 2

  apply(subst flts_prepend)
   
     apply (meson nonalt.elims(3))
   
    apply (meson nonazero.elims(3))
   apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)")
  apply (metis append_Nil frewritesaalts)
  apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
  by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)

(* TEST *)
lemma r: 
  assumes "AALTs bs rs1 \<leadsto> AALTs bs rs2"
  shows "AALTs bs (x # rs1) \<leadsto>* AALTs bs (x # rs2)"
  using assms
  apply(erule_tac rrewrite.cases)
            apply(auto)
  apply (metis append_Cons append_Nil rrewrite.intros(6) r_in_rstar)
  apply (metis append_Cons append_self_conv2 rrewrite.intros(7) r_in_rstar)
  apply (metis Cons_eq_appendI append_eq_append_conv2 rrewrite.intros(8) self_append_conv r_in_rstar)
   apply(case_tac rs2)
    apply(auto)
  apply(case_tac r)
         apply(auto)
  apply (metis append_Nil2 append_butlast_last_id butlast.simps(2) last.simps list.distinct(1) list.map_disc_iff r_in_rstar rrewrite.intros(8))
     apply(case_tac r)
        apply(auto)
   defer
   apply(rule r_in_rstar)
  apply (metis append_Cons append_Nil rrewrite.intros(11))
  apply(rule real_trans)
   apply(rule r_in_rstar)
  using rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified]
   apply(rule_tac rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified])
  apply(simp add: map_fuse_Nil fuse_Nil)
  done 

lemma alts_simpalts: 
  "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> 
  AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
  apply(induct rs)
   apply(auto)[1]
  using trivialbsimp_srewrites apply auto[1]
  by (simp add: srewrites_alt1 ss2)

lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
  apply auto
  done


lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"
  using split_list by fastforce

lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"
  apply auto
  by (metis split_list)

lemma alts_dBrewrites_withFront: 
  "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
  apply(induction rs arbitrary: rsa)
   apply simp
  apply(drule_tac x = "rsa@[a]" in meta_spec)
  apply(subst threelistsappend)
  apply(rule real_trans)
  apply simp
  apply(case_tac "a \<in> set rsa")
   apply simp
   apply(drule somewhereInside)
   apply(erule exE)+
   apply simp
  apply(subgoal_tac " AALTs bs
            (rs1 @
             a #
             rs2 @
             a #
             distinctBy rs erase
              (insert (erase a)
                (erase `
                 (set rs1 \<union> set rs2)))) \<leadsto> AALTs bs (rs1@ a # rs2 @  distinctBy rs erase
              (insert (erase a)
                (erase `
                 (set rs1 \<union> set rs2)))) ")
  prefer 2
  using rrewrite.intros(11) apply force
  using r_in_rstar apply force
  apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
  prefer 2
    
   apply auto[1]
  apply(case_tac "erase a \<in> erase `set rsa")

   apply simp
  apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>
                     AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")
  apply force
  apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(11) same_append_eq somewhereMapInside)
  by force

 

lemma alts_dBrewrites: "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})"
  apply(induction rs)
   apply simp
  apply simp
  using alts_dBrewrites_withFront
  by (metis append_Nil dB_single_step empty_set image_empty)

lemma bsimp_rewrite: 
  shows "r \<leadsto>* bsimp r"
proof (induction r rule: bsimp.induct)
  case (1 bs1 r1 r2)
  then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"
    apply(simp)
    apply(case_tac "bsimp r1 = AZERO")
        apply simp
  using continuous_rewrite apply blast
       apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
        apply(erule exE)
        apply simp
        apply(subst bsimp_ASEQ2)
        apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
       apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
  done
next
  case (2 bs1 rs)
  then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
    by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites real_trans)  
next
  case "3_1"
  then show "AZERO \<leadsto>* bsimp AZERO"
    by simp
next
  case ("3_2" v)
  then show "AONE v \<leadsto>* bsimp (AONE v)" 
    by simp
next
  case ("3_3" v va)
  then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" 
    by simp
next
  case ("3_4" v va)
  then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" 
    by simp
qed

lemma rewrite_non_nullable_strong: 
  assumes "r1 \<leadsto> r2"
  shows "bnullable r1 = bnullable r2"
using assms
apply(induction r1 r2 rule: rrewrite.induct)
apply(auto)
apply(metis bnullable_correctness erase_fuse)+
apply(metis UnCI bnullable_correctness erase_fuse imageI)
apply(metis bnullable_correctness erase_fuse)+
done

lemma rewrite_nullable: 
  assumes "r1 \<leadsto> r2" "bnullable r1"
  shows "bnullable r2"
using assms rewrite_non_nullable_strong
by auto

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


lemma bnullable_segment: 
  "bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
  by auto

lemma bnullablewhichbmkeps: "\<lbrakk>bnullable  (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
 \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
  
  using qq2 bnullable_Hdbmkeps_Hd by force

lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
    \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
  apply(subst bnullable_Hdbmkeps_Hd)
  
   apply simp
  by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)

lemma third_segment_bnullable: 
  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
   bnullable (AALTs bs rs3)"
  apply(auto)
  done

lemma third_segment_bmkeps:  
  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
   bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
  by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTs_rewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)

lemma rewrite_bmkepsalt: 
  "\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
       \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
  apply(rule qq3)
  apply(simp)
  apply(simp)
  apply(case_tac "bnullable (AALTs bs1 rs1)")
  using spillbmkepslistr apply blast
  apply(subst qq2)
    apply(auto simp add: bnullable_fuse r1)
  done

lemma rewrite_bmkeps_aux: 
  assumes "r1 \<leadsto> r2" "bnullable r1" "bnullable r2"
  shows "bmkeps r1 = bmkeps r2"
  using assms 
proof (induction r1 r2 rule: rrewrite.induct)
  case (1 bs r2)
  then show ?case by simp 
next
  case (2 bs r1)
  then show ?case by simp
next
  case (3 bs bs1 r)
  then show ?case by (simp add: b2) 
next
  case (4 r1 r2 bs r3)
  then show ?case by simp
next
  case (5 r3 r4 bs r1)
  then show ?case by simp
next
  case (6 r r' bs rs1 rs2)
  then show ?case
    by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong)
next
  case (7 bs rsa rsb)
  then show ?case
    by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(9) rrewrite0away third_segment_bmkeps) 
next
  case (8 bs rsa bs1 rs1 rsb)
  then show ?case
    by (simp add: rewrite_bmkepsalt) 
next
  case (9 bs)
  then show ?case
    by fastforce 
next
  case (10 bs r)
  then show ?case
    by (simp add: b2) 
next
  case (11 a1 a2 bs rsa rsb rsc)
  then show ?case
    by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
qed


lemma rewrite_bmkeps: 
  assumes "r1 \<leadsto> r2" "bnullable r1"
  shows "bmkeps r1 = bmkeps r2"
  using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast
  

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 rewrite_bmkeps a3 a4 by simp
  then show "bmkeps r1 = bmkeps r3" using IH by simp
qed

lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
  by (metis append_Cons append_Nil rrewrite.intros(6))

lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto>  AALT bs AZERO r2"
  by (simp add: alts_rewrite_front rrewrite.intros(1))

lemma rewrite_fuse: 
  assumes "r2 \<leadsto> r3"
  shows "fuse bs r2 \<leadsto>* fuse bs r3"
  using assms
proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
  case (1 bs r2)
  then show ?case
    by (simp add: continuous_rewrite) 
next
  case (2 bs r1)
  then show ?case
    using rrewrite.intros(2) by force 
next
  case (3 bs bs1 r)
  then show ?case
    by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3)) 
next
  case (4 r1 r2 bs r3)
  then show ?case
    by (simp add: r_in_rstar star_seq) 
next
  case (5 r3 r4 bs r1)
  then show ?case
    using fuse.simps(5) r_in_rstar star_seq2 by auto  
next
  case (6 r r' bs rs1 rs2)
  then show ?case
    using contextrewrites2 r_in_rstar by force 
next
  case (7 bs rsa rsb)
  then show ?case
    using rrewrite.intros(7) by force  
next
  case (8 bs rsa bs1 rs1 rsb)
  then show ?case
    using rrewrite.intros(8) by force 
next
  case (9 bs)
  then show ?case
    by (simp add: r_in_rstar rrewrite.intros(9))
next
  case (10 bs r)
  then show ?case
    by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(10)) 
next
  case (11 a1 a2 bs rsa rsb rsc)
  then show ?case
    using fuse.simps(4) r_in_rstar rrewrite.intros(11) by auto 
qed

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_fuse real_trans)
done

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_der_altmiddle: 
  "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
   apply simp
   apply(simp add: bder_fuse_list del: append.simps)
  by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)

lemma lock_step_der_removal: 
  shows " erase a1 = erase a2 \<Longrightarrow> 
                                  bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* 
                                  bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
  apply(simp)
  
  using rrewrite.intros(11) by auto

lemma rewrite_after_der: 
  assumes "r1 \<leadsto> r2"
  shows "(bder c r1) \<leadsto>* (bder c r2)"
  using assms
proof(induction r1 r2 rule: rrewrite.induct)
  case (1 bs r2)
  then show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
    by (simp add: continuous_rewrite) 
next
  case (2 bs r1)
  then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
    apply(simp)
    by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(9) rrewrite.intros(2) rrewrite0away)
next
  case (3 bs bs1 r)
  then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)" 
    apply(simp)
    by (metis bder_fuse fuse_append rrewrite.intros(10) rrewrite0away rrewrites.simps to_zero_in_alt)
next
  case (4 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 (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq) 
next
  case (5 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)"
    using bder.simps(5) r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
next
  case (6 r r' bs rs1 rs2)
  have as: "r \<leadsto> r'" by fact
  have IH: "bder c r \<leadsto>* bder c r'" by fact
  from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto>* bder c (AALTs bs (rs1 @ [r'] @ rs2))" 
    apply(simp)
    using contextrewrites2 by force
next
  case (7 bs rsa rsb)
  then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ rsb))" 
    apply(simp)
    using rrewrite.intros(7) by auto
next
  case (8 bs rsa bs1 rs1 rsb)
  then show 
    "bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
    using rewrite_der_altmiddle by auto 
next
  case (9 bs)
  then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
    by (simp add: r_in_rstar rrewrite.intros(9))
next
  case (10 bs r)
  then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
    by (simp add: bder_fuse r_in_rstar rrewrite.intros(10)) 
next
  case (11 a1 a2 bs rsa rsb rsc)
  have as: "erase a1 = erase a2" by fact
  then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
    using lock_step_der_removal by force 
qed


lemma rewrites_after_der: 
  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_after_der real_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_after_der)
  also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
    by (simp add: bsimp_rewrite)
  finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
    by (simp add: bders_simp_append)
qed


  


lemma quasi_main: 
  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_main: 
  shows "blexer r s = blexer_simp r s"
  unfolding blexer_def blexer_simp_def
  using b4 quasi_main by simp


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



export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers


unused_thms


inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
  where
 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "



end
