Theory Pi_Derivatives

(* Author: Dmitriy Traytel *)

section ‹Derivatives of $\Pi$-Extended Regular Expressions›
(*<*)
theory Pi_Derivatives
imports Pi_Regular_Exp
begin
(*>*)

locale embed = project Σ wf_atom project lookup
  for Σ :: "nat ⇒ 'a set"
  and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
  and project :: "'a ⇒ 'a"
  and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes embed :: "'a ⇒ 'a list"
assumes embed: "⋀a. a ∈ Σ n ⟹ b ∈ set (embed a) = (b ∈ Σ (Suc n) ∧ project b = a)"
begin

subsection ‹Syntactic Derivatives›

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

primrec lderivs where
  "lderivs [] r = r"
| "lderivs (w#ws) r = lderivs ws (lderiv w r)"



subsection ‹Finiteness of ACI-Equivalent Derivatives›

lemma toplevel_summands_lderiv:
  "toplevel_summands (lderiv as r) = (⋃s∈toplevel_summands r. toplevel_summands (lderiv as s))"
  by (induct r) (auto simp: Let_def)

lemma lderivs_Zero[simp]: "lderivs xs Zero = Zero"
  by (induct xs) auto

lemma lderivs_Full[simp]: "lderivs xs Full = Full"
  by (induct xs) auto

lemma lderivs_One: "lderivs xs One ∈ {Zero, One}"
  by (induct xs) auto

lemma lderivs_Atom: "lderivs xs (Atom as) ∈ {Zero, One, Atom as}"
proof (induct xs)
  case (Cons x xs) thus ?case by (auto intro: insertE[OF lderivs_One])
qed simp

lemma lderivs_Plus: "lderivs xs (Plus r s) = Plus (lderivs xs r) (lderivs xs s)"
  by (induct xs arbitrary: r s) auto

lemma lderivs_PLUS: "lderivs xs (PLUS ys) = PLUS (map (lderivs xs) ys)"
  by (induct ys rule: list_singleton_induct) (auto simp: lderivs_Plus)

lemma toplevel_summands_lderivs_Times: "toplevel_summands (lderivs xs (Times r s)) ⊆
  {Times (lderivs xs r) s} ∪
  {r'. ∃ys zs. r' ∈ toplevel_summands (lderivs ys s) ∧ ys ≠ [] ∧ zs @ ys = xs}"
proof (induct xs arbitrary: r s)
  case (Cons x xs)
  thus ?case by (auto simp: Let_def lderivs_Plus) (fastforce intro: exI[of _ "x#xs"])+
qed simp

lemma toplevel_summands_lderivs_Star_nonempty:
  "xs ≠ [] ⟹ toplevel_summands (lderivs xs (Star r)) ⊆
    {Times (lderivs ys r) (Star r) | ys. ∃zs. ys ≠ [] ∧ zs @ ys = xs}"
proof (induct xs rule: length_induct)
  case (1 xs)
  then obtain y ys where "xs = y # ys" by (cases xs) auto
  thus ?case using spec[OF 1(1)]
    by (auto dest!: subsetD[OF toplevel_summands_lderivs_Times] intro: exI[of _ "y#ys"])
       (auto elim!: impE dest!: meta_spec subsetD)
qed

lemma toplevel_summands_lderivs_Star:
  "toplevel_summands (lderivs xs (Star r)) ⊆
    {Star r} ∪ {Times (lderivs ys r) (Star r) | ys. ∃zs. ys ≠ [] ∧ zs @ ys = xs}"
  by (cases "xs = []") (auto dest!: toplevel_summands_lderivs_Star_nonempty)

lemma ex_lderivs_Pr: "∃s. lderivs ass (Pr r) = Pr s"
  by (induct ass arbitrary: r) auto

lemma toplevel_summands_PLUS:
 "xs ≠ [] ⟹ toplevel_summands (PLUS (map f xs)) = (⋃r ∈ set xs. toplevel_summands (f r))"
  by (induct xs rule: list_singleton_induct) simp_all

lemma lderiv_toplevel_summands_Zero:
  "⟦lderivs xs (Pr r) = Pr s; toplevel_summands r = {Zero}⟧ ⟹ toplevel_summands s = {Zero}"
proof (induct xs arbitrary: r s)
  case (Cons y ys)
  from Cons.prems(1) have "toplevel_summands (PLUS (map (λa. lderiv a r) (embed y))) = {Zero}"
  proof (cases "embed y = []")
    case False
    show ?thesis using Cons.prems(2) unfolding toplevel_summands_PLUS[OF False]
      by (subst toplevel_summands_lderiv) (simp add: False)
  qed simp
  with Cons show ?case by simp
qed simp

lemma toplevel_summands_lderivs_Pr:
  "⟦xs ≠ []; lderivs xs (Pr r) = Pr s⟧ ⟹
    toplevel_summands s ⊆ {Zero} ∨ toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
proof (induct xs arbitrary: r s)
  case (Cons y ys) note * = this
  show ?case
  proof (cases "embed y = []")
    case True with Cons show ?thesis by (cases "ys = []") (auto dest: lderiv_toplevel_summands_Zero)
  next
    case False 
    show ?thesis
    proof (cases ys)
      case Nil with * show ?thesis
        by (auto simp: toplevel_summands_PLUS[OF False]) (metis lderivs.simps)
    next
      case (Cons z zs)
      have "toplevel_summands s ⊆ {Zero} ∨ toplevel_summands s ⊆
       (⋃xs. toplevel_summands (lderivs xs (PLUS (map (λa. lderiv a r) (embed y)))))" (is "_ ∨ ?B")
        by (rule *(1)) (auto simp: Cons *(3)[symmetric])
      thus ?thesis
      proof
        assume ?B
        also have "… ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
          by (auto simp: lderivs_PLUS toplevel_summands_PLUS[OF False]) (metis lderivs.simps(2))
        finally show ?thesis ..
      qed blast
    qed
  qed
qed simp

lemma lderivs_Pr:
  "{lderivs xs (Pr r) | xs. True} ⊆
    {Pr s | s. toplevel_summands s ⊆ {Zero} ∨
               toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))}"
  (is "?L ⊆?R")
proof (rule subsetI)
  fix s assume "s ∈ ?L"
  then obtain xs where "s = lderivs xs (Pr r)" by blast
  moreover obtain t where "lderivs xs (Pr r) = Pr t" using ex_lderivs_Pr by blast
  ultimately show "s ∈ ?R"
    by (cases "xs = []") (auto dest!: toplevel_summands_lderivs_Pr elim!: allE[of _ "[]"])
qed

lemma ACI_norm_toplevel_summands_Zero: "toplevel_summands r ⊆ {Zero} ⟹ «r» = Zero"
  by (subst ACI_norm_flatten) (auto dest: subset_singletonD)

lemma ACI_norm_lderivs_Pr:
  "ACI_norm ` {lderivs xs (Pr r) | xs. True} ⊆
    {Pr Zero} ∪ {Pr «s» | s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
proof (intro subset_trans[OF image_mono[OF lderivs_Pr]] subsetI,
       elim imageE CollectE exE conjE disjE)
  fix x x' s :: "'b rexp"
  assume *: "x = «x'»" "x' = Pr s" and "toplevel_summands s ⊆ {Zero}"
  hence "«Pr s» = Pr Zero" using ACI_norm_toplevel_summands_Zero by simp
  thus "x ∈ {Pr Zero} ∪
    {Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
    unfolding * by blast
next
  fix x x' s :: "'b rexp"
  assume *: "x = «x'»" "x' = Pr s" and "toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
  hence "toplevel_summands «s» ⊆ (⋃xs. toplevel_summands «lderivs xs r»)"
    by (fastforce simp: toplevel_summands_ACI_norm)
  moreover have "x = Pr ««s»»" unfolding * ACI_norm_idem ACI_norm.simps(10) ..
  ultimately show "x ∈ {Pr Zero} ∪
    {Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
    by blast
qed

lemma finite_ACI_norm_toplevel_summands: "finite B ⟹ finite {f «s» |s. toplevel_summands s ⊆ B}"
  apply (elim finite_surj [OF iffD2 [OF finite_Pow_iff], of _ _ "f o flatten PLUS o image ACI_norm"])
  apply (subst ACI_norm_flatten)
  apply auto
  done

lemma lderivs_Not: "lderivs xs (Not r) = Not (lderivs xs r)"
  by (induct xs arbitrary: r) auto

lemma lderivs_Inter: "lderivs xs (Inter r s) = Inter (lderivs xs r) (lderivs xs s)"
  by (induct xs arbitrary: r s) auto

theorem finite_lderivs: "finite {«lderivs xs r» | xs . True}"
proof (induct r)
  case Zero show ?case by simp
next
  case Full show ?case by simp
next
  case One show ?case
   by (rule finite_surj[of "{Zero, One}"]) (blast intro: insertE[OF lderivs_One])+
next
  case (Atom as) show ?case
    by (rule finite_surj[of "{Zero, One, Atom as}"]) (blast intro: insertE[OF lderivs_Atom])+
next
  case (Plus r s)
  show ?case by (auto simp: lderivs_Plus intro!: finite_surj[OF finite_cartesian_product[OF Plus]])
next
  case (Times r s)
  hence "finite (⋃ (toplevel_summands ` {«lderivs xs s» | xs . True}))" by auto
  moreover have "{«r'» |r'. ∃ys. r' ∈ toplevel_summands (lderivs ys s)} =
    {r'. ∃ys. r' ∈ toplevel_summands «lderivs ys s»}"
    unfolding toplevel_summands_ACI_norm by auto
  ultimately have fin: "finite {«r'» |r'. ∃ys. r' ∈ toplevel_summands (lderivs ys s)}"
    by (fastforce intro: finite_subset[of _ "⋃ (toplevel_summands ` {«lderivs xs s» | xs . True})"])
  let ?X = "λxs. {Times (lderivs ys r) s | ys. True} ∪ {r'. r' ∈ (⋃ys. toplevel_summands (lderivs ys s))}"
  show ?case
  proof (simp only: ACI_norm_flatten,
      rule finite_surj[of "{X. ∃xs. X ⊆ ACI_norm ` ?X xs}" _ "flatten PLUS"])
    show "finite {X. ∃xs. X ⊆ ACI_norm ` ?X xs}"
      using fin by (fastforce simp: image_Un elim: finite_subset[rotated] intro: finite_surj[OF Times(1), of _ "λr. Times r «s»"])
  qed (fastforce dest!: subsetD[OF toplevel_summands_lderivs_Times] intro!: imageI)
next
  case (Star r)
  let ?f = "λf r'. Times r' (Star (f r))"
  let ?X = "{Star r} ∪ ?f id ` {r'. r' ∈ {lderivs ys r|ys. True}}"
  show ?case
  proof (simp only: ACI_norm_flatten,
      rule finite_surj[of "{X. X ⊆ ACI_norm ` ?X}" _ "flatten PLUS"])
    have *: "⋀X. ACI_norm ` ?f (λx. x) ` X = ?f ACI_norm ` ACI_norm ` X" by (auto simp: image_def)
    show "finite {X. X ⊆ ACI_norm ` ?X}"
      by (rule finite_Collect_subsets)
         (auto simp: * intro!: finite_imageI[of _ "?f ACI_norm"] intro: finite_subset[OF _ Star])
  qed (fastforce dest!: subsetD[OF toplevel_summands_lderivs_Star] intro!: imageI)
next
  case (Not r) thus ?case by (auto simp: lderivs_Not) (blast intro: finite_surj)
next
  case (Inter r s)
  show ?case by (auto simp: lderivs_Inter intro!: finite_surj[OF finite_cartesian_product[OF Inter]])
next
  case (Pr r)
  hence *: "finite (⋃ (toplevel_summands ` {«lderivs xs r» | xs . True}))" by auto
  have "finite (⋃xs. toplevel_summands «lderivs xs r»)" by (rule finite_subset[OF _ *]) auto
  hence fin: "finite {Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
    by (intro finite_ACI_norm_toplevel_summands)
  have "{s. ∃xs. s = «lderivs xs (Pr r)»} = {«s»| s. ∃xs. s = lderivs xs (Pr r)}" by auto
  thus ?case using finite_subset[OF ACI_norm_lderivs_Pr, of r] fin unfolding image_Collect by auto
qed

subsection ‹Wellformedness and language of derivatives›

lemma wf_lderiv[simp]: "wf n r ⟹ wf n (lderiv w r)"
  by (induct r arbitrary: n w) (auto simp add: Let_def)

lemma wf_lderivs[simp]: "wf n r ⟹ wf n (lderivs ws r)"
  by (induct ws arbitrary: r) (auto intro: wf_lderiv)

lemma lQuot_map_project:
assumes "as ∈ Σ n" "A ⊆ lists (Σ (Suc n))"
shows "lQuot as (map project ` A) = map project ` (⋃a ∈ set (embed as). lQuot a A)" (is "?L = ?R")
proof (intro equalityI image_subsetI subsetI)
  fix xss assume "xss ∈ ?L"
  with assms obtain zss
    where zss: "zss ∈ A" "as # xss = map project zss"
    unfolding lQuot_def by fastforce
  hence "xss = map project (tl zss)" by auto
  with zss assms(2) show "xss ∈ ?R" using embed[OF project, of _ n] unfolding lQuot_def by fastforce
next
  fix xss assume "xss ∈ (⋃a ∈ set (embed as). lQuot a A)"
  with assms(1) show "map project xss ∈ lQuot as (map project ` A)" unfolding lQuot_def
    by (fastforce intro!: rev_image_eqI simp: embed)
qed

lemma lang_lderiv: "⟦wf n r; w ∈ Σ n⟧ ⟹ lang n (lderiv w r) = lQuot w (lang n r)"
proof (induct r arbitrary: n w)
  case (Pr r)
  hence *: "wf (Suc n) r" "⋀w'. w' ∈ set (embed w) ⟹  w' ∈ Σ (Suc n)" by (auto simp: embed)
  from Pr(1)[OF *] lQuot_map_project[OF Pr(3) lang_subset_lists[OF *(1)]] show ?case
    by (auto simp: wf_lderiv[OF *(1)])
qed (auto simp: Let_def lang_final[symmetric])

lemma lang_lderivs: "⟦wf n r; wf_word n ws⟧ ⟹ lang n (lderivs ws r) = lQuots ws (lang n r)"
  by (induct ws arbitrary: r) (auto simp: lang_lderiv)

corollary lderivs_final:
assumes "wf n r" "wf_word n ws"
shows "final (lderivs ws r) ⟷ ws ∈ lang n r"
  using lang_lderivs[OF assms] lang_final[of "lderivs ws r" n] by auto

abbreviation "lderivs_set n r s ≡ {(«lderivs w r», «lderivs w s») | w. wf_word n w}"



subsection ‹Deriving preserves ACI-equivalence›

lemma ACI_norm_PLUS:
  "list_all2 (λr s. «r» = «s») xs ys ⟹ «PLUS xs» = «PLUS ys»"
proof (induct rule: list_all2_induct)
  case (Cons x xs y ys)
  hence "length xs = length ys" by (elim list_all2_lengthD)
  thus ?case using Cons by (induct xs ys rule: list_induct2) auto
qed simp

lemma toplevel_summands_ACI_norm_lderiv:
  "(⋃a∈toplevel_summands r. toplevel_summands «lderiv as «a»») = toplevel_summands «lderiv as «r»»"
proof (induct r)
  case (Plus r1 r2) thus ?case
   unfolding toplevel_summands.simps toplevel_summands_ACI_norm
     toplevel_summands_lderiv[of as "«Plus r1 r2»"] image_Un Union_Un_distrib
   by (simp add: image_UN)
qed (auto simp: Let_def)

theorem ACI_norm_lderiv:
  "«lderiv as «r»» = «lderiv as r»"
proof (induct r arbitrary: as)
  case (Plus r1 r2) thus ?case
   unfolding lderiv.simps ACI_norm_flatten[of "lderiv as «Plus r1 r2»"]
     toplevel_summands_lderiv[of as "«Plus r1 r2»"] image_Un image_UN
   by (auto simp: toplevel_summands_ACI_norm toplevel_summands_flatten_ACI_norm_image_Union)
     (auto simp: toplevel_summands_ACI_norm[symmetric] toplevel_summands_ACI_norm_lderiv)
next
  case (Pr r)
  hence "list_all2 (λr s. «r» = «s»)
    (map (λa. lderiv a «r») (embed as)) (map (λa. lderiv a r) (embed as))"
    unfolding list_all2_map1 list_all2_map2 by (intro list_all2_refl)
  thus ?case unfolding lderiv.simps ACI_norm.simps by (blast intro: ACI_norm_PLUS)
qed (simp_all add: Let_def)


corollary lderiv_preserves: "«r» = «s» ⟹ «lderiv as r» = «lderiv as s»"
  by (rule box_equals[OF _ ACI_norm_lderiv ACI_norm_lderiv]) (erule arg_cong)

lemma lderivs_snoc[simp]: "lderivs (ws @ [w]) r = (lderiv w (lderivs ws r))"
  by (induct ws arbitrary: r) auto

theorem ACI_norm_lderivs:
  "«lderivs ws «r»» = «lderivs ws r»"
proof (induct ws arbitrary: r rule: rev_induct)
  case (snoc w ws) thus ?case
    using ACI_norm_lderiv[of w "lderivs ws r"] ACI_norm_lderiv[of w "lderivs ws «r»"] by auto
qed simp

lemma lderivs_alt: "«lderivs w r» = fold (λa r. «lderiv a r») w «r»"
  by (induct w arbitrary: r) (auto simp: ACI_norm_lderiv)

lemma finite_fold_lderiv: "finite {fold (λa r. «lderiv a r») w «s» |w. True}"
  using finite_lderivs unfolding lderivs_alt .

end

(*<*)
end
(*>*)