Theory Pi_Regular_Operators

(* Author: Dmitriy Traytel *)

section "Some Useful Regular Operators"

(*<*)
theory Pi_Regular_Operators
imports Pi_Derivatives "HOL-Library.While_Combinator"
begin
(*>*)

primrec REV :: "'a rexp ⇒ 'a rexp" where
  "REV Zero = Zero"
| "REV Full = Full"
| "REV One = One"
| "REV (Atom a) = Atom a"
| "REV (Plus r s) = Plus (REV r) (REV s)"
| "REV (Times r s) = Times (REV s) (REV r)"
| "REV (Star r) = Star (REV r)"
| "REV (Not r) = Not (REV r)"
| "REV (Inter r s) = Inter (REV r) (REV s)"
| "REV (Pr r) = Pr (REV r)"

lemma REV_REV[simp]: "REV (REV r) = r"
  by (induct r) auto

lemma final_REV[simp]: "final (REV r) = final r"
  by (induct r) auto

lemma REV_PLUS: "REV (PLUS xs) = PLUS (map REV xs)"
  by (induct xs rule: list_singleton_induct) auto

lemma (in alphabet) wf_REV[simp]: "wf n r ⟹ wf n (REV r)"
  by (induct r arbitrary: n) auto

lemma (in project) lang_REV[simp]: "lang n (REV r) = rev ` lang n r"
  by (induct r arbitrary: n) (auto simp: image_image rev_map image_set_diff)

context embed
begin

primrec rderiv :: "'a ⇒ 'b rexp ⇒ 'b rexp" where
  "rderiv _ Zero = Zero"
| "rderiv _ Full = Full"
| "rderiv _ One = Zero"
| "rderiv a (Atom b) = (if lookup b a then One else Zero)"
| "rderiv a (Plus r s) = Plus (rderiv a r) (rderiv a s)"
| "rderiv a (Times r s) =
    (let rs' = Times r (rderiv a s)
     in if final s then Plus rs' (rderiv a r) else rs')"
| "rderiv a (Star r) = Times (Star r) (rderiv a r)"
| "rderiv a (Not r) = Not (rderiv a r)"
| "rderiv a (Inter r s) = Inter (rderiv a r) (rderiv a s)"
| "rderiv a (Pr r) = Pr (PLUS (map (λa'. rderiv a' r) (embed a)))"

primrec rderivs where
  "rderivs [] r = r"
| "rderivs (w#ws) r = rderivs ws (rderiv w r)"

lemma rderivs_snoc: "rderivs (ws @ [w]) r = rderiv w (rderivs ws r)"
  by (induct ws arbitrary: r) auto

lemma rderivs_append: "rderivs (ws @ ws') r = rderivs ws' (rderivs ws r)"
  by (induct ws arbitrary: r) auto

lemma rderiv_lderiv: "rderiv as r = REV (lderiv as (REV r))"
  by (induct r arbitrary: as) (auto simp: Let_def o_def REV_PLUS)

lemma rderivs_lderivs: "rderivs w r = REV (lderivs w (REV r))"
  by (induct w arbitrary: r) (auto simp: rderiv_lderiv)

lemma wf_rderiv[simp]: "wf n r ⟹ wf n (rderiv w r)"
  unfolding rderiv_lderiv by (rule wf_REV[OF wf_lderiv[OF wf_REV]])

lemma wf_rderivs[simp]: "wf n r ⟹ wf n (rderivs ws r)"
  unfolding rderivs_lderivs by (rule wf_REV[OF wf_lderivs[OF wf_REV]])

lemma lang_rderiv: "⟦wf n r; as ∈ Σ n⟧ ⟹ lang n (rderiv as r) = rQuot as (lang n r)"
  unfolding rderiv_lderiv rQuot_rev_lQuot by (simp add: lang_lderiv)

lemma lang_rderivs: "⟦wf n r; wf_word n w⟧ ⟹ lang n (rderivs w r) = rQuots w (lang n r)"
  unfolding rderivs_lderivs rQuots_rev_lQuots by (simp add: lang_lderivs)

corollary rderivs_final:
assumes "wf n r" "wf_word n w"
shows "final (rderivs w r) ⟷ rev w ∈ lang n r"
  using lang_rderivs[OF assms] lang_final[of "rderivs w r" n] by auto

lemma toplevel_summands_REV[simp]: "toplevel_summands (REV r) = REV ` toplevel_summands r"
  by (induct r) auto

lemma ACI_norm_REV: "«REV «r»» = «REV r»"
proof (induct r)
  case (Plus r s)
  show ?case
    using [[unfold_abs_def = false]]
    unfolding REV.simps ACI_norm.simps Plus[symmetric] image_Un[symmetric]
      toplevel_summands.simps(1) toplevel_summands_ACI_norm toplevel_summands_REV
    unfolding toplevel_summands.simps(1)[symmetric] ACI_norm_flatten toplevel_summands_REV
    unfolding ACI_norm_flatten[symmetric] toplevel_summands_ACI_norm
    ..
qed auto

lemma ACI_norm_rderiv: "«rderiv as «r»» = «rderiv as r»"
  unfolding rderiv_lderiv by (metis ACI_norm_REV ACI_norm_lderiv)

lemma ACI_norm_rderivs: "«rderivs w «r»» = «rderivs w r»"
  unfolding rderivs_lderivs by (metis ACI_norm_REV ACI_norm_lderivs)

theorem finite_rderivs: "finite {«rderivs xs r» | xs . True}"
  unfolding rderivs_lderivs
  by (subst ACI_norm_REV[symmetric]) (auto intro: finite_surj[OF finite_lderivs, of _ "λr. «REV r»"])

lemma lderiv_PLUS[simp]: "lderiv a (PLUS xs) = PLUS (map (lderiv a) xs)"
  by (induct xs rule: list_singleton_induct) auto

lemma rderiv_PLUS[simp]: "rderiv a (PLUS xs) = PLUS (map (rderiv a) xs)"
  by (induct xs rule: list_singleton_induct) auto

lemma lang_rderiv_lderiv: "lang n (rderiv a (lderiv b r)) = lang n (lderiv b (rderiv a r))"
  by (induct r arbitrary: n a b) (auto simp: Let_def conc_assoc)

lemma lang_lderiv_rderiv: "lang n (lderiv a (rderiv b r)) = lang n (rderiv b (lderiv a r))"
  by (induct r arbitrary: n a b) (auto simp: Let_def conc_assoc)

lemma lang_rderiv_lderivs[simp]: "⟦wf n r; wf_word n w; a ∈ Σ n⟧ ⟹
  lang n (rderiv a (lderivs w r)) = lang n (lderivs w (rderiv a r))"
  by (induct w arbitrary: n r)
    (auto, auto simp: lang_lderivs lang_lderiv lang_rderiv lQuot_rQuot)

lemma lang_lderiv_rderivs[simp]: "⟦wf n r; wf_word n w; a ∈ Σ n⟧ ⟹
  lang n (lderiv a (rderivs w r)) = lang n (rderivs w (lderiv a r))"
  by (induct w arbitrary: n r)
    (auto, auto simp: lang_rderivs lang_lderiv lang_rderiv lQuot_rQuot)
(*
primrec bideriv :: "'a ⇒ 'a ⇒ 'a rexp ⇒ 'a rexp" where
  "bideriv _ _ Zero = Zero"
| "bideriv _ _ One = Zero"
| "bideriv a b (Atom c) = Zero"
| "bideriv a b (Plus r s) = Plus (bideriv a b r) (bideriv a b s)"
| "bideriv a b (Times r s) =
    (let rs' = Times (lderiv a r) (rderiv b s)
     in if final r ∧ final s then Plus (Plus rs' (bideriv a b r)) (bideriv a b s)
        else if final r then Plus rs' (bideriv a b s)
        else if final s then Plus rs' (bideriv a b r)
        else rs')"
| "bideriv a b (Star r) = Plus (bideriv a b r) (TIMES [lderiv a r, Star r, rderiv b r])"
| "bideriv a b (Not r) = Not (bideriv a b r)"
| "bideriv a b (Inter r s) = Inter (bideriv a b r) (bideriv a b s)"
| "bideriv a b (Pr r) = Pr (PLUS (map (λb. PLUS (map (λa. bideriv a b r) (embed a))) (embed b)))"

lemma wf_bideriv[simp]: "wf n r ⟹ wf n (bideriv a b r)"
  by (induct r arbitrary: n a b) (auto simp: maps_def Let_def)

lemma ACI_norm_bideriv_rderiv_lderiv: "«bideriv a b r» = «rderiv b (lderiv a r)»"
  by (induct r arbitrary: a b)
    (auto simp: Let_def maps_def o_def list_all2_map1 list_all2_map2 intro!: ACI_PLUS list_all2_refl)

lemma bideriv_rderiv_lderiv:
  "lang n (bideriv a b r) = lang n (rderiv b (lderiv a r))"
  by (induct r arbitrary: n a b) (auto simp: Let_def)

lemma lang_bideriv:
  "⟦wf n r; a ∈ Σ n; b ∈ Σ n⟧ ⟹ lang n (bideriv a b r) = biQuot a b (lang n r)"
  by (auto simp: bideriv_rderiv_lderiv lang_lderiv lang_rderiv biQuot_rQuot_lQuot)

lemma ACI_norm_bideriv: "«bideriv a b «r»» = «bideriv a b r»"
  unfolding ACI_norm_bideriv_rderiv_lderiv by (metis ACI_norm_lderiv ACI_norm_rderiv)

fun biderivs where
  "biderivs [] [] r = r"
| "biderivs as [] r = lderivs as r"
| "biderivs [] bs r = rderivs bs r"
| "biderivs (a#as) (b#bs) r = biderivs as bs (bideriv a b r)"

lemma biderivs_rderivs_lderivs: "⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹
  lang n (biderivs w1 w2 r) = lang n (rderivs w2 (lderivs w1 r))"
  by (induct arbitrary: r rule: biderivs.induct)
    (auto simp: lang_rderivs lang_lderivs bideriv_rderiv_lderiv)

lemma lang_biderivs:
  "⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹ lang n (biderivs w1 w2 r) = biQuots w1 w2 (lang n r)"
  by (auto simp: biderivs_rderivs_lderivs lang_lderivs lang_rderivs biQuots_rQuots_lQuots)

lemma wf_biderivs[simp]: "wf n r ⟹ wf n (biderivs w1 w2 r)"
  by (induct arbitrary: r rule: biderivs.induct) auto
*)
definition "biderivs w1 w2 = rderivs w2 o lderivs w1"

lemma lang_biderivs: "⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹
  lang n (biderivs w1 w2 r) = biQuots w1 w2 (lang n r)"
   unfolding biderivs_def by (auto simp: lang_rderivs lang_lderivs in_lists_conv_set)

lemma wf_biderivs[simp]: "wf n r ⟹ wf n (biderivs w1 w2 r)"
  unfolding biderivs_def by simp

corollary biderivs_final:
assumes "wf n r" "wf_word n w1" "wf_word n w2"
shows "final (biderivs w1 w2 r) ⟷ w1 @ rev w2 ∈ lang n r"
  using lang_biderivs[OF assms] lang_final[of "biderivs w1 w2 r" n] by auto

lemma ACI_norm_biderivs: "«biderivs w1 w2 «r»» = «biderivs w1 w2 r»"
  unfolding biderivs_def by (metis ACI_norm_lderivs ACI_norm_rderivs o_apply)

lemma "finite {«biderivs w1 w2 r» | w1 w2 . True}"
proof -
  have "{«biderivs w1 w2 r» | w1 w2 . True} =
    (⋃s ∈ {«lderivs as r» | as . True}. {«rderivs bs s» | bs . True})"
    unfolding biderivs_def by (fastforce simp: ACI_norm_rderivs)
  also have "finite …" by (rule iffD2[OF finite_UN[OF finite_lderivs] ballI[OF finite_rderivs]])
  finally show ?thesis .
qed

end


subsection ‹Quotioning by the same letter›

definition "fin_cut_same x xs = take (LEAST n. drop n xs = replicate (length xs - n) x) xs"

lemma fin_cut_same_Nil[simp]: "fin_cut_same x [] = []"
  unfolding fin_cut_same_def by simp

lemma Least_fin_cut_same: "(LEAST n. drop n xs = replicate (length xs - n) y) =
  length xs - length (takeWhile (λx. x = y) (rev xs))"
  (is "Least ?P = ?min")
proof (rule Least_equality)
  show "?P ?min" by (induct xs rule: rev_induct) (auto simp:  Suc_diff_le replicate_append_same)
next
  fix m assume "?P m"
  have "length xs - m ≤ length (takeWhile (λx. x = y) (rev xs))"
  proof (intro length_takeWhile_less_P_nth)
    fix i assume "i < length xs - m"
    hence "rev xs ! i ∈ set (drop m xs)"
      by (induct xs arbitrary: i rule: rev_induct) (auto simp: nth_Cons')
    with ‹?P m› show "rev xs ! i = y" by simp
  qed simp
  thus "?min ≤ m" by linarith
qed
    

lemma takeWhile_takes_all: "length xs = m ⟹ m ≤ length (takeWhile P xs) ⟷ Ball (set xs) P"
  by hypsubst_thin (induct xs, auto)

lemma fin_cut_same_Cons[simp]: "fin_cut_same x (y # xs) =
  (if fin_cut_same x xs = [] then if x = y then [] else [y] else y # fin_cut_same x xs)"
  unfolding fin_cut_same_def Least_fin_cut_same
  apply auto
  apply (simp add: takeWhile_takes_all)
  apply (simp add: takeWhile_takes_all)
  apply auto
  apply (metis (full_types) Suc_diff_le length_rev length_takeWhile_le take_Suc_Cons)
  apply (simp add: takeWhile_takes_all)
  apply (subst takeWhile_append2)
  apply auto
  apply (simp add: takeWhile_takes_all)
  apply auto
  apply (metis (full_types) Suc_diff_le length_rev length_takeWhile_le take_Suc_Cons)
  done

lemma fin_cut_same_singleton[simp]: "fin_cut_same x (xs @ [x]) = fin_cut_same x xs"
  by (induct xs) auto

lemma fin_cut_same_replicate[simp]: "fin_cut_same x (xs @ replicate n x) = fin_cut_same x xs"
  by (induct n arbitrary: xs)
    (auto simp: replicate_append_same[symmetric] append_assoc[symmetric] simp del: append_assoc)

lemma fin_cut_sameE: "fin_cut_same x xs = ys ⟹ ∃m. xs = ys @ replicate m x"
  apply (induct xs arbitrary: ys)
   apply auto
    apply (metis replicate_Suc)
   apply metis
  apply metis
  done


definition "SAMEQUOT a A = {fin_cut_same a x @ replicate m a| x m. x ∈ A}"

lemma SAMEQUOT_mono: "A ⊆ B ⟹ SAMEQUOT a A ⊆ SAMEQUOT a B"
  unfolding SAMEQUOT_def by auto

locale embed2 = embed Σ wf_atom project lookup embed
  for Σ :: "nat ⇒ 'a set"
  and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
  and project :: "'a ⇒ 'a"
  and lookup :: "'b ⇒ 'a ⇒ bool"
  and embed :: "'a ⇒ 'a list" +
  fixes singleton :: "'a ⇒ 'b"
  assumes wf_singleton[simp]: "a ∈ Σ n ⟹ wf_atom n (singleton a)"
  assumes lookup_singleton[simp]: "lookup (singleton a) a' = (a = a')"
begin

lemma finite_rderivs_same: "finite {«rderivs (replicate m a) r» | m . True}"
  by (auto intro: finite_subset[OF _ finite_rderivs])

lemma wf_word_replicate[simp]: "a ∈ Σ n ⟹ wf_word n (replicate m a)"
  by (induct m) auto

lemma star_singleton[simp]: "star {[x]} = {replicate m x | m . True}"
proof (intro equalityI subsetI)
  fix xs assume "xs ∈ star {[x]}"
  thus "xs ∈ {replicate m x | m . True}" by (induct xs) (auto, metis replicate_Suc)
qed (auto intro: Ball_starI)

definition "samequot a r = Times (flatten PLUS {«rderivs (replicate m a) r» | m . True}) (Star (Atom (singleton a)))"

lemma wf_samequot: "⟦wf n r; a ∈ Σ n⟧ ⟹ wf n (samequot a r)"
  unfolding samequot_def wf.simps wf_flatten_PLUS[OF finite_rderivs_same] by auto

lemma lang_samequot: "⟦wf n r; a ∈ Σ n⟧ ⟹ 
   lang n (samequot a r) = SAMEQUOT a (lang n r)"
   unfolding SAMEQUOT_def samequot_def lang.simps lang_flatten_PLUS[OF finite_rderivs_same]
   apply (rule sym)
   apply (auto simp: lang_rderivs)
   apply (intro concI)
   apply auto
   apply (insert fin_cut_sameE[OF refl, of _ a])
   apply (drule meta_spec)
   apply (erule exE)
   apply (intro exI conjI)
   apply (rule refl)
   apply (auto simp: lang_rderivs)
   apply (erule subst)
   apply assumption
   apply (erule concE)
   apply (auto simp: lang_rderivs)
   apply (drule meta_spec)
   apply (erule exE)
   apply (intro exI conjI)
   defer
   apply assumption
   unfolding fin_cut_same_replicate
   apply (erule trans)
   unfolding fin_cut_same_replicate
   apply (rule refl)
   done

fun rderiv_and_add where
  "rderiv_and_add as (_ :: bool, rs) =
    (let
      r = «rderiv as (hd rs)»
    in if r ∈ set rs then (False, rs) else (True, r # rs))"

definition "invar_rderiv_and_add as r brs ≡
  (if fst brs then True else «rderiv as (hd (snd brs))» ∈ set (snd brs)) ∧
  snd brs ≠ [] ∧ distinct (snd brs) ∧
  (∀i < length (snd brs). snd brs ! i = «rderivs (replicate (length (snd brs) - 1 - i) as) r»)"

lemma invar_rderiv_and_add_init: "invar_rderiv_and_add as r (True, [«r»])"
  unfolding invar_rderiv_and_add_def by auto

lemma invar_rderiv_and_add_step: "invar_rderiv_and_add as r brs ⟹ fst brs ⟹
  invar_rderiv_and_add as r (rderiv_and_add as brs)"
  unfolding invar_rderiv_and_add_def by (cases brs) (auto simp:
    Let_def nth_Cons' ACI_norm_rderiv rderivs_snoc[symmetric] neq_Nil_conv replicate_append_same)

lemma rderivs_replicate_mult: "⟦«rderivs (replicate i as) r» = «r»; i > 0⟧ ⟹
  «rderivs (replicate (m * i) as) r» = «r»"
proof (induct m arbitrary: r)
  case (Suc m)
  hence "«rderivs (replicate (m * i) as) «rderivs (replicate i as) r»» = «r»" 
    by (auto simp: ACI_norm_rderivs)
  thus ?case by (auto simp: ACI_norm_rderivs replicate_add rderivs_append)
qed simp

lemma rderivs_replicate_mult_rest: 
  assumes "«rderivs (replicate i as) r» = «r»" "k < i"
  shows "«rderivs (replicate (m * i + k) as) r» = «rderivs (replicate k as) r»" (is "?L = ?R")
proof -
  have "?L = «rderivs (replicate k as) «rderivs (replicate (m * i) as) r»»"
    by (simp add: ACI_norm_rderivs replicate_add rderivs_append)
  also have "«rderivs (replicate (m * i) as) r» = «r»" using assms
    by (simp add: rderivs_replicate_mult)
  finally show ?thesis by (simp add: ACI_norm_rderivs)
qed

lemma rderivs_replicate_mod: 
  assumes "«rderivs (replicate i as) r» = «r»" "i > 0"
  shows "«rderivs (replicate m as) r» = «rderivs (replicate (m mod i) as) r»" (is "?L = ?R")
  by (subst div_mult_mod_eq[symmetric, of m i])
    (intro rderivs_replicate_mult_rest[OF assms(1)] mod_less_divisor[OF assms(2)])

lemma rderivs_replicate_diff: "⟦«rderivs (replicate i as) r» = «rderivs (replicate j as) r»; i > j⟧ ⟹
  «rderivs (replicate (i - j) as) (rderivs (replicate j as) r)» = «rderivs (replicate j as) r»"
  unfolding rderivs_append[symmetric] replicate_add[symmetric] by auto

lemma samequot_wf:
  assumes "wf n r" "while_option fst (rderiv_and_add as) (True, [«r»]) = Some (b, rs)"
  shows "wf n (PLUS rs)"
proof -
  have "¬ b" using while_option_stop[OF assms(2)] by simp
  from while_option_rule[where P="invar_rderiv_and_add as r",
    OF invar_rderiv_and_add_step assms(2) invar_rderiv_and_add_init]
    have *: "invar_rderiv_and_add as r (b, rs)" by simp
  thus "wf n (PLUS rs)" unfolding invar_rderiv_and_add_def wf_PLUS
    by (auto simp: in_set_conv_nth wf_rderivs[OF assms(1)])
qed

lemma samequot_soundness:
  assumes "while_option fst (rderiv_and_add as) (True, [«r»]) = Some (b, rs)"
  shows "lang n (PLUS rs) = ⋃ (lang n ` {«rderivs (replicate m as) r» | m. True})"
proof -
  have "¬ b" using while_option_stop[OF assms] by simp
  moreover 
  from while_option_rule[where P="invar_rderiv_and_add as r",
    OF invar_rderiv_and_add_step assms invar_rderiv_and_add_init]
    have *: "invar_rderiv_and_add as r (b, rs)" by simp
  ultimately obtain i where i: "i < length rs" and "«rderivs (replicate (length rs - Suc i) as) r» =
       «rderivs (replicate (Suc (length rs - Suc 0)) as) r»" (is "«rderivs ?x r» = _")
    unfolding invar_rderiv_and_add_def by (auto simp: in_set_conv_nth hd_conv_nth ACI_norm_rderiv
      rderivs_snoc[symmetric] replicate_append_same)
  with * have "«rderivs ?x r» = «rderivs (replicate (length rs) as) r»"
    by (auto simp: invar_rderiv_and_add_def)
  with i have cyc: "«rderivs (replicate (Suc i) as) (rderivs ?x r)» = «rderivs ?x r»"
    by (fastforce dest: rderivs_replicate_diff[OF sym])
  { fix m
    have "∃i<length rs. rs ! i = «rderivs (replicate m as) r»"
    proof (cases "m > length rs - Suc i")
      case True
      with i obtain m' where m: "m = m' + length rs - Suc i"
        by atomize_elim (auto intro: exI[of _ "m - (length rs - Suc i)"])
      with i have "«rderivs (replicate m as) r» = «rderivs (replicate m' as) (rderivs ?x r)»"
       unfolding replicate_add[symmetric] rderivs_append[symmetric] by (simp add: add.commute)
      also from cyc have "… = «rderivs (replicate (m' mod (Suc i)) as) (rderivs ?x r)»" 
        by (elim rderivs_replicate_mod) simp
      also from i have "… = «rderivs (replicate (m' mod (Suc i) + length rs - Suc i) as) r»" 
        unfolding rderivs_append[symmetric] replicate_add[symmetric] by (simp add: add.commute)
      also from m i have "… = «rderivs (replicate ((m - (length rs - Suc i)) mod (Suc i) + length rs - Suc i) as) r»"
        by simp
      also have "… = «rderivs (replicate (length rs - Suc (i - (m - (length rs - Suc i)) mod (Suc i))) as) r»"
        by (subst Suc_diff_le[symmetric])
          (metis less_Suc_eq_le mod_less_divisor zero_less_Suc, simp add: add.commute)
      finally have "∃j < length rs. «rderivs (replicate m as) r» = «rderivs (replicate (length rs - Suc j) as) r»"
        using i by (metis less_imp_diff_less)
      with * show ?thesis unfolding invar_rderiv_and_add_def by auto
    next
      case False
      with i have "∃j < length rs. m = length rs - Suc j"
        by (induct m)
          (metis diff_self_eq_0 gr_implies_not0 lessI nat.exhaust,
           metis (no_types) One_nat_def Suc_diff_Suc diff_Suc_1 gr0_conv_Suc less_imp_diff_less
             not_less_eq not_less_iff_gr_or_eq)
      with * show ?thesis unfolding invar_rderiv_and_add_def by auto
    qed
  }
  hence "⋃ (lang n ` {«rderivs (replicate m as) r» |m. True}) ⊆ lang n (PLUS rs)"
    by (fastforce simp: in_set_conv_nth intro!: bexI[rotated])
  moreover from * have "lang n (PLUS rs) ⊆ ⋃ (lang n ` {«rderivs (replicate m as) r» |m. True})"
    unfolding invar_rderiv_and_add_def by (fastforce simp: in_set_conv_nth)
  ultimately show "lang n (PLUS rs) = ⋃ (lang n ` {«rderivs (replicate m as) r» |m. True})" by blast
qed

lemma length_subset_card: "⟦finite X; distinct (x # xs); set (x # xs) ⊆ X⟧ ⟹ length xs < card X"
  by (metis card_mono distinct_card impossible_Cons not_le_imp_less order_trans)

lemma samequot_termination:
  assumes "while_option fst (rderiv_and_add as) (True, [«r»]) = None" (is "?cl = None")
  shows "False"
proof -
  let ?D =  "{«rderivs (replicate m as) r» | m . True}"
  let ?f = "λ(b, rs). card ?D + 1 - length rs + (if b then 1 else 0)"
  have "∃st. ?cl = Some st"
    apply (rule measure_while_option_Some[of "invar_rderiv_and_add as r" _ _ ?f])
     apply (auto simp: invar_rderiv_and_add_init invar_rderiv_and_add_step)
    apply (auto simp: invar_rderiv_and_add_def Let_def neq_Nil_conv in_set_conv_nth
       intro!: diff_less_mono2 length_subset_card[OF finite_rderivs_same, simplified])
      apply auto []
     apply fastforce
    apply (metis Suc_less_eq nth_Cons_Suc)
    done
  with assms show False by auto
qed

definition "samequot_exec a r =
  Times (PLUS (snd (the (while_option fst (rderiv_and_add a) (True, [«r»]))))) (Star (Atom (singleton a)))"

lemma wf_samequot_exec: "⟦wf n r; as ∈ Σ n⟧ ⟹ wf n (samequot_exec as r)"
  unfolding samequot_exec_def
  by (cases "while_option fst (rderiv_and_add as) (True, [«r»])")
    (auto dest: samequot_termination samequot_wf)

lemma samequot_exec_samequot: "lang n (samequot_exec as r) = lang n (samequot as r)"
  unfolding samequot_exec_def samequot_def lang.simps lang_flatten_PLUS[OF finite_rderivs_same]
  by (cases "while_option fst (rderiv_and_add as) (True, [«r»])")
    (auto dest: samequot_termination dest!: samequot_soundness[of _ _ _ _ n] simp del: ACI_norm_lang)

lemma lang_samequot_exec:
  "⟦wf n r; as ∈ Σ n⟧ ⟹ lang n (samequot_exec as r) = SAMEQUOT as (lang n r)"
unfolding samequot_exec_samequot by (rule lang_samequot)

end

subsection ‹Suffix and Prefix Languages›

definition Suffix :: "'a lang ⇒ 'a lang" where
  "Suffix L = {w. ∃u. u @ w ∈ L}"

definition Prefix :: "'a lang ⇒ 'a lang" where
  "Prefix L = {w. ∃u. w @ u ∈ L}"

lemma Prefix_Suffix: "Prefix L = rev ` Suffix (rev ` L)"
  unfolding Prefix_def Suffix_def
  by (auto simp: rev_append_invert
  intro: image_eqI[of _ rev, OF rev_rev_ident[symmetric]]
         image_eqI[of _ rev, OF rev_append[symmetric]])

definition Root :: "'a lang ⇒ 'a lang" where
  "Root L = {x . ∃n > 0. x ^^ n ∈ L}"

definition Cycle :: "'a lang ⇒ 'a lang" where
  "Cycle L = {u @ w | u w. w @ u ∈ L}"

context embed
begin

context
fixes n :: nat
begin

definition SUFFIX :: "'b rexp ⇒ 'b rexp" where
  "SUFFIX r = flatten PLUS {«lderivs w r»| w. wf_word n w}"

lemma finite_lderivs_wf: "finite {«lderivs w r»| w. wf_word n w}"
  by (auto intro: finite_subset[OF _ finite_lderivs])

definition PREFIX :: "'b rexp ⇒ 'b rexp" where
  "PREFIX r = REV (SUFFIX (REV r))"

lemma wf_SUFFIX[simp]: "wf n r ⟹ wf n (SUFFIX r)"
  unfolding SUFFIX_def by (intro iffD2[OF wf_flatten_PLUS[OF finite_lderivs_wf]]) auto
                                            
lemma lang_SUFFIX[simp]: "wf n r ⟹ lang n (SUFFIX r) = Suffix (lang n r)"
  unfolding SUFFIX_def Suffix_def
  using lang_flatten_PLUS[OF finite_lderivs_wf] lang_lderivs wf_lang_wf_word
  by fastforce

lemma wf_PREFIX[simp]: "wf n r ⟹ wf n (PREFIX r)"
  unfolding PREFIX_def by auto

lemma lang_PREFIX[simp]: "wf n r ⟹ lang n (PREFIX r) = Prefix (lang n r)"
  unfolding PREFIX_def by (auto simp: Prefix_Suffix)         

end

lemma take_drop_CycleI[intro!]: "x ∈ L ⟹ drop i x @ take i x ∈ Cycle L"
  unfolding Cycle_def by fastforce

lemma take_drop_CycleI'[intro!]: "drop i x @ take i x ∈ L ⟹ x ∈ Cycle L"
  by (drule take_drop_CycleI[of _ _ "length x - i"]) auto

end

(*<*)
end
(*>*)