# 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
(*>*)
```