theory BlexerSimp
  imports Blexer 
begin


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"

lemma bmkeps_fuse:
  assumes "bnullable r"
  shows "bmkeps (fuse bs r) = bs @ bmkeps r"
  using assms
  by (induct r rule: bnullable.induct) (auto)

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 bder_fuse:
  shows "bder c (fuse bs a) = fuse bs  (bder c a)"
  apply(induct a arbitrary: bs c)
  apply(simp_all)
  done




fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where
  "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c"

fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and 
   turnIntoTerms :: "rexp \<Rightarrow> rexp list "
   where
  "furtherSEQ ONE r2 =  turnIntoTerms r2 "
| "furtherSEQ r11 r2 = [SEQ r11 r2]"
| "turnIntoTerms (SEQ ONE r2) =  turnIntoTerms r2"
| "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))"
| "turnIntoTerms r = [r]"

abbreviation "tint \<equiv> turnIntoTerms"

fun seqFold :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
  "seqFold acc [] = acc"
| "seqFold ONE (r # rs1) = seqFold r rs1"
| "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1"


fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
  "attachCtx r ctx = set (turnIntoTerms (seqFold (erase r) ctx))"


fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where
  "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"


fun notZero :: "arexp \<Rightarrow> bool" where
  "notZero AZERO = True"
| "notZero _ = False"


fun tset :: "arexp list \<Rightarrow> rexp set" where
  "tset rs = set (concat (map turnIntoTerms (map erase rs)))"


fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
  "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else 
                        (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
                                 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))
                                 | r \<Rightarrow> r
                        )
                      )
            "

abbreviation
  "p6 acc r \<equiv> prune6 (tset acc) r Nil"


fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
  "dB6 [] acc = []"
| "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) 
                       else (let pruned = prune6 acc a [] in 
                              (case pruned of
                                 AZERO \<Rightarrow> dB6 as acc
                               |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc)  ) ) ))   "


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


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

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



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:  "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
| ss7:  " (as @ [a] @ as1) s\<leadsto> (as @ [p6 as a] @ as1)"

thm tset.simps

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 rs_in_rstar: 
  shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<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 srewrites_prepend:
  shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (r # rs1) s\<leadsto>* (r # rs2)"
  by (metis append_Cons append_Nil srewrites1)  

lemma srewrite2: 
  shows  "r1 \<leadsto> r2 \<Longrightarrow> True"
  and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
  apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts)
                apply simp+
  using srewrites_prepend apply force
      apply (simp add: rs_in_rstar ss3)
  using ss4 apply force 
  using rs_in_rstar ss5 apply auto[1]
  using rs_in_rstar ss6 apply auto[1]
  using rs_in_rstar ss7 by force




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

(*harmless sorry*)
lemma existing_preimage :
  shows "f a \<in> f ` set rs1 \<Longrightarrow> \<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> f x = f a "
  apply(induct rs1)
   apply simp
  apply(case_tac "f a = f aa")
  
  sorry


lemma deletes_dB:
  shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)"
  apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a")
  prefer 2
   apply (meson existing_preimage)
  apply(erule exE)+
  apply simp
  apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\<leadsto> (rs1a @ [x] @ rs1b @ rs2)")  
  apply (simp add: rs_in_rstar)
  apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)")
  using ss6 apply presburger
  by simp



lemma ss6_realistic:
  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (tset rs1))"
  apply(induct rs2 arbitrary: rs1)
   apply simp
  apply(rename_tac cc' cc)
  apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))")
   prefer 2
  apply (metis append.assoc append.left_neutral append_Cons)
  apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") 
  sorry




lemma ss6_stronger:
  shows "rs1 s\<leadsto>* dB6 rs1 {}"
  using ss6
  by (metis append_Nil concat.simps(1) list.set(1) list.simps(8) ss6_realistic tset.simps)

 
lemma tint_fuse:
  shows "tint (erase a) = tint (erase (fuse bs a))"
  by (simp add: erase_fuse)

lemma tint_fuse2:
  shows " set (tint (erase a)) =
     set (tint (erase (fuse bs a)))"
  using tint_fuse by auto

lemma fused_bits_at_head:
  shows "fuse bs a = ASEQ bs1 a1 a2 \<Longrightarrow> \<exists>bs2. bs1 = bs @ bs2"
  
(* by (smt (verit) arexp.distinct(13) arexp.distinct(19) arexp.distinct(25) arexp.distinct(27) arexp.distinct(5) arexp.inject(3) fuse.elims)
harmless sorry
*)


  sorry

thm seqFold.simps

lemma seqFold_concats:
  shows "r \<noteq> ONE \<Longrightarrow> seqFold r [r1] = SEQ r r1"
  apply(case_tac r)
       apply simp+
done


lemma tint_seqFold_eq: shows
"set (tint (seqFold (erase x42) [erase x43])) = 
           set (tint (SEQ (erase x42) (erase x43)))"
  apply(case_tac "erase x42 = ONE")
   apply simp
  using seqFold_concats
  apply simp
  done

fun top :: "arexp \<Rightarrow> bit list" where
  "top AZERO = []"
| "top (AONE bs) = bs"
| "top (ASEQ bs r1 r2) = bs"
| "top (ACHAR v va) = v"
| "top (AALTs v va) = v"
| "top (ASTAR v va) = v "




lemma p6fa_aux:
  shows " fuse bs
            (bsimp_AALTs bs\<^sub>0 as) = 
           
            (bsimp_AALTs (bs @ bs\<^sub>0) as)"
  by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv)


lemma p6pfuse_alts:
  shows 
" \<And>bs\<^sub>0 as\<^sub>0.     
       \<lbrakk>\<And>a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\<rbrakk>
       \<Longrightarrow> \<not> set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<longrightarrow>
           fuse bs
            (case a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
             | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
             | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa) 
              =
           (case fuse bs a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
            | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
            | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)"
  apply simp
  using p6fa_aux by presburger




lemma prune6_preserves_fuse:
  shows "fuse bs (p6 as a) = p6 as (fuse bs a)"
  using tint_fuse2
  apply simp
  apply(case_tac a)
       apply simp
  apply simp
     apply simp

  using fused_bits_at_head

    apply simp
  using tint_seqFold_eq
  apply simp
    apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append)
  using p6pfuse_alts apply presburger
  by simp


(*
The top-level bitlist stays the same:
\<^sub>b\<^sub>sa ------pruning----->  \<^sub>b\<^sub>s\<^sub>' b  \<Longrightarrow>        \<exists>bs3. bs' = bs @ bs3 
*)
lemma top_bitcodes_preserved_p6:
  shows "top r = bs \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)"
  

  apply(induct r arbitrary: as)

(*this sorry requires more care *)
  
  sorry



corollary prune6_preserves_fuse_srewrite:
  shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)"
  apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]")
  apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)")
  using prune6_preserves_fuse apply auto[1]
  using rs_in_rstar ss7 apply presburger
  by simp

lemma prune6_invariant_fuse:
  shows "p6 as a = p6 (map (fuse bs) as) a"
  apply simp
  using erase_fuse by presburger


lemma p6pfs_cor:
  shows "(map (fuse bs) as @ map (fuse bs) [a] @ map (fuse bs) as1) s\<leadsto>* (map (fuse bs) as @ map (fuse bs) [p6 as a] @ map (fuse bs) as1)"
  by (metis prune6_invariant_fuse prune6_preserves_fuse_srewrite)

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, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
next
  case (ss7 as a as1)
  then show ?case
    apply(simp only: map_append)
    using p6pfs_cor by presburger
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 bsimp_aalts_simpcases: 
  shows "AONE bs \<leadsto>* bsimpStrong6 (AONE bs)"  
  and   "AZERO \<leadsto>* bsimpStrong6 AZERO" 
  and   "ACHAR bs c \<leadsto>* bsimpStrong6 (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 simp
             apply simp
              apply (simp add: bnullable_fuse)
  using bnullable.simps(5) apply presburger
          apply simp
         apply simp
  sorry   



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 presburger

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
    using bmkepss.simps bnullable0(1) by presburger
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 (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD)
next
           prefer 10
  case (ss7 as a as1)
  then show ?case
    
(*this sorry requires more effort*)
  sorry
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 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 map1:
  shows "(map f [a]) = [f a]"
  by (simp)

lemma "set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<Longrightarrow>
       set (tint (erase (bder c a))) \<subseteq> (\<Union>x\<in>set (map (bder c) as). set (tint (erase x)))"
  
  sorry


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 map1)
    apply(rule srewrites_trans)
    apply(rule rs_in_rstar)
    apply(rule_tac rrewrite_srewrite.ss6)
    using Der_def der_correctness apply auto[1]
    by blast
next
  case (ss7 as a as1)
  then show ?case
    apply simp
    sorry
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 bders_simp_appendStrong :
  shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
  apply(induct s1 arbitrary: s2 rule: rev_induct)
   apply simp
  apply auto
  done




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




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

lemma mainStrong: 
  assumes "bnullable (bders r s)"
  shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
proof -
  have "bders r s \<leadsto>* bdersStrong6 r s" 
    using centralStrong by force
  then 
  show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" 
    using assms rewrites_bmkeps by blast
qed




theorem blexerStrong_correct :
  shows "blexerStrong r s = blexer r s"
  unfolding blexerStrong_def blexer_def
  by (metis centralStrong mainStrong rewritesnullable)



end
