# Theory Automaton

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section "Regular Expressions Equivalence Framework"

(*<*)
theory Automaton
imports "Regular-Sets.Regular_Exp" "HOL-Library.While_Combinator"
begin
(*>*)

primrec add_atoms :: "'a rexp ⇒ 'a list ⇒ 'a list"
where
| "add_atoms (Atom a) = List.insert a"

lemma set_add_atoms: "set (add_atoms r as) = atoms r ∪ set as"
by (induction r arbitrary: as) auto

lemma rtrancl_fold_product:
shows "{((r,s),(f a r,f a s))| r s a. a : A}^* =
{((r,s),(fold f w r,fold f w s))| r s w. w : lists A}" (is "?L = ?R")
proof-
{ fix r s r' s'
have "((r,s),(r',s')) : ?L ⟹ ((r,s),(r',s')) : ?R"
proof(induction rule: converse_rtrancl_induct2)
case refl show ?case by(force intro!: fold_simps(1)[symmetric])
next
case step thus ?case by(force intro!: fold_simps(2)[symmetric])
qed
} moreover
{ fix r s r' s'
{ fix w have "∀x∈set w. x ∈ A ⟹ ((r, s), fold f w r, fold f w s) :?L"
proof(induction w rule: rev_induct)
case Nil show ?case by simp
next
case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
qed
}
hence "((r,s),(r',s')) : ?R ⟹ ((r,s),(r',s')) : ?L" by auto
} ultimately show ?thesis by (auto simp: in_lists_conv_set) blast
qed

lemma rtrancl_fold_product1:
shows "{(r,s). ∃a ∈ A. s = f a r}^* =
{(r,fold f w r) | r w. w : lists A}" (is "?L = ?R")
proof-
{ fix r s
have "(r,s) : ?L ⟹ (r,s) : ?R"
proof(induction rule: converse_rtrancl_induct)
case base show ?case by(force intro!: fold_simps(1)[symmetric])
next
case step thus ?case by(force intro!: fold_simps(2)[symmetric])
qed
} moreover
{ fix r s
{ fix w have "∀x∈set w. x ∈ A ⟹ (r, fold f w r) :?L"
proof(induction w rule: rev_induct)
case Nil show ?case by simp
next
case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
qed
}
hence "(r,s) : ?R ⟹ (r,s) : ?L" by auto
} ultimately show ?thesis by (auto simp: in_lists_conv_set) blast
qed

lemma lang_eq_ext_Nil_fold_Deriv:
fixes r s
defines "𝔅 ≡ {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w∈lists (atoms r ∪ atoms s)}"
shows "lang r = lang s ⟷ (∀(K, L) ∈ 𝔅. [] ∈ K ⟷ [] ∈ L)"
unfolding lang_eq_ext 𝔅_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto

locale rexp_DA =
fixes init :: "'a rexp ⇒ 's"
fixes delta :: "'a ⇒ 's ⇒ 's"
fixes final :: "'s ⇒ bool"
fixes L :: "'s ⇒ 'a lang"
assumes L_init: "L (init r) = lang r"
assumes L_delta: "L(delta a s) = Deriv a (L s)"
assumes final_iff_Nil: "final s ⟷ [] ∈ L s"
begin

lemma L_deltas: "L (fold delta w s) = fold Deriv w (L s)"
by (induction w arbitrary: s) (auto simp add: L_delta)

definition closure :: "'a list ⇒ 's * 's ⇒ (('s * 's) list * ('s * 's) set) option"
where
"closure as = rtrancl_while (λ(p,q). final p = final q)
(λ(p,q). map (λa. (delta a p, delta a q)) as)"
(* stop when same opti? *)

theorem closure_sound_complete:
assumes result: "closure as (init r,init s) = Some(ws,R)"
and atoms: "set as = atoms r ∪ atoms s"
shows "ws = [] ⟷ lang r = lang s"
proof -
have leq: "(lang r = lang s) =
(∀(r',s') ∈ {((r0,s0),(delta a r0,delta a s0))| r0 s0 a. a : set as}^*  {(init r,init s)}.
final r' = final s')"
by (simp add: atoms rtrancl_fold_product Ball_def lang_eq_ext_Nil_fold_Deriv imp_ex
L_deltas L_init final_iff_Nil del: Un_iff)
have "{(x,y). y ∈ set ((λ(p,q). map (λa. (delta a p, delta a q)) as) x)} =
{((r,s), delta a r, delta a s) |r s a. a ∈ set as}"
by auto
with atoms rtrancl_while_Some[OF result[unfolded closure_def]]
show ?thesis by (auto simp add: leq Ball_def split: if_splits)
qed

subsection ‹The overall procedure›

definition check_eqv :: "'a rexp ⇒ 'a rexp ⇒ bool" where
"check_eqv r s =
in case closure as (init r, init s) of
Some([],_) ⇒ True | _ ⇒ False)"

lemma soundness:
assumes "check_eqv r s" shows "lang r = lang s"
proof -
obtain R where 1: "closure ?as (init r, init s) = Some([],R)"
using assms by (auto simp: check_eqv_def Let_def split:option.splits list.splits)
from closure_sound_complete[OF this]
qed

(* completeness needs termination of closure, otherwise result could be None *)

text‹Auxiliary functions:›
definition reachable :: "'a list ⇒ 'a rexp ⇒ 's set" where
"reachable as s =
snd(the(rtrancl_while (λ_. True) (λs. map (λa. delta a s) as) (init s)))"

definition automaton :: "'a list ⇒ 'a rexp ⇒ (('s * 'a) * 's) set" where
"automaton as s =
snd (the
(let i = init s;
start = (([i], {i}), {});
test = λ((ws, Z), A). ws ≠ [];
step = λ((ws, Z), A).
(let s = hd ws;
new_edges = map (λa. ((s, a), delta a s)) as;
new = remdups (filter (λss. ss ∉ Z) (map snd new_edges))
in ((new @ tl ws, set new ∪ Z), set new_edges ∪ A))
in while_option test step start))"

definition match :: "'a rexp ⇒ 'a list ⇒ bool" where
"match s w = final (fold delta w (init s))"

lemma match_correct: "match s w ⟷ w ∈ lang s"
unfolding match_def
by (induct w arbitrary: s)
(auto simp: L_init L_delta in_fold_Deriv final_iff_Nil L_deltas Deriv_def)

end

locale rexp_DFA = rexp_DA +
assumes fin: "finite {fold delta w (init s) | w. True}"
begin

lemma finite_rtrancl_delta_Image:
"finite ({((r,s),(delta a r,delta a s))| r s a. a : A}^*  {(init r, init s)})"
unfolding rtrancl_fold_product Image_singleton
by (auto intro: finite_subset[OF _ finite_cartesian_product[OF fin fin]])

lemma "termination": "∃st. closure as (init r,init s) = Some st" (is "∃_. closure as ?i = _")
unfolding closure_def proof (rule rtrancl_while_finite_Some)
show "finite ({(x, st). st ∈ set ((λ(p,q). map (λa. (delta a p, delta a q)) as) x)}⇧*  {?i})"
by (rule finite_subset[OF Image_mono[OF rtrancl_mono] finite_rtrancl_delta_Image]) auto
qed

lemma completeness:
assumes "lang r = lang s" shows "check_eqv r s"
proof -
obtain ws R where 1: "closure ?as (init r, init s) = Some(ws,R)"
using "termination" by fastforce
with closure_sound_complete[OF this] assms
qed

lemma finite_rtrancl_delta_Image1:
"finite ({(r,s). ∃a ∈ A. s = delta a r}^*  {init r})"
unfolding rtrancl_fold_product1 by (auto intro: finite_subset[OF _ fin])

lemma reachable: "reachable as r = {fold delta w (init r) | w. w ∈ lists (set as)}"
and finite_reachable: "finite (reachable as r)"
proof -
obtain wsZ where *: "rtrancl_while (λ_. True) (λs. map (λa. delta a s) as) (init r) = Some wsZ"
by (atomize_elim,intro rtrancl_while_finite_Some Image_mono rtrancl_mono
finite_subset[OF _ finite_rtrancl_delta_Image1[of "set as" r]]) auto
then show "reachable as r = {fold delta w (init r) | w. w ∈ lists (set as)}"
unfolding reachable_def by (cases wsZ)
(auto dest!: rtrancl_while_Some split: if_splits simp: rtrancl_fold_product1 image_iff)
then show "finite (reachable as r)" by (auto intro: finite_subset[OF _ fin])
qed

end

(*<*)
end
(*>*)


# Theory Derivatives_Finite

(* Author: Dmitriy Traytel, ported by Tobias Nipkow *)

section ‹Finiteness of Derivatives Modulo ACI›

(*<*)
(* split into Norm and Fin theories *)
theory Derivatives_Finite
imports "Regular-Sets.Derivatives"
begin
(*>*)

text ‹Lifting constructors to lists›

fun rexp_of_list where
"rexp_of_list OP N [] = N"
| "rexp_of_list OP N [r] = r"
| "rexp_of_list OP N (r # rs) = OP r (rexp_of_list OP N rs)"

abbreviation "PLUS ≡ rexp_of_list Plus Zero"
abbreviation "TIMES ≡ rexp_of_list Times One"

lemma list_singleton_induct [case_names nil single cons]:
assumes "P []" and "⋀x. P [x]" and "⋀x y xs. P (y # xs) ⟹ P (x # (y # xs))"
shows "P xs"
using assms by induction_schema (pat_completeness, lexicographic_order)

subsection ‹ACI normalization›

fun toplevel_summands :: "'a rexp ⇒ 'a rexp set" where
"toplevel_summands (Plus r s) = toplevel_summands r ∪ toplevel_summands s"
| "toplevel_summands r = {r}"

abbreviation "flatten LISTOP X ≡ LISTOP (sorted_list_of_set X)"

lemma toplevel_summands_nonempty[simp]:
"toplevel_summands r ≠ {}"
by (induct r) auto

lemma toplevel_summands_finite[simp]:
"finite (toplevel_summands r)"
by (induct r) auto

primrec ACI_norm :: "('a::linorder) rexp ⇒ 'a rexp"  ("«_»") where
"«Zero» = Zero"
| "«One» = One"
| "«Atom a» = Atom a"
| "«Plus r s» = flatten PLUS (toplevel_summands (Plus «r» «s»))"
| "«Times r s» = Times «r» «s»"
| "«Star r» = Star «r»"

lemma Plus_toplevel_summands: "Plus r s ∈ toplevel_summands t ⟹ False"
by (induction t) auto

lemma toplevel_summands_not_Plus[simp]:
"(∀r s. x ≠ Plus r s) ⟹ toplevel_summands x = {x}"
by (induction x) auto

lemma toplevel_summands_PLUS_strong:
"⟦xs ≠ []; list_all (λx. ¬(∃r s. x = Plus r s)) xs⟧ ⟹ toplevel_summands (PLUS xs) = set xs"
by (induct xs rule: list_singleton_induct) auto

lemma toplevel_summands_flatten:
"⟦X ≠ {}; finite X; ∀x ∈ X. ¬(∃r s. x = Plus r s)⟧ ⟹ toplevel_summands (flatten PLUS X) = X"
using toplevel_summands_PLUS_strong[of "sorted_list_of_set X"]
unfolding list_all_iff by fastforce

lemma ACI_norm_Plus: "«r» = Plus s t ⟹ ∃s t. r = Plus s t"
by (induction r) auto

lemma toplevel_summands_flatten_ACI_norm_image:
"toplevel_summands (flatten PLUS (ACI_norm  toplevel_summands r)) = ACI_norm  toplevel_summands r"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_Plus intro: Plus_toplevel_summands)

lemma toplevel_summands_flatten_ACI_norm_image_Union:
"toplevel_summands (flatten PLUS (ACI_norm  toplevel_summands r ∪ ACI_norm  toplevel_summands s)) =
ACI_norm  toplevel_summands r ∪ ACI_norm  toplevel_summands s"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_Plus[OF sym] intro: Plus_toplevel_summands)

lemma toplevel_summands_ACI_norm:
"toplevel_summands «r» = ACI_norm  toplevel_summands r"
by (induction r) (auto simp: toplevel_summands_flatten_ACI_norm_image_Union)

lemma ACI_norm_flatten:
"«r» = flatten PLUS (ACI_norm  toplevel_summands r)"
by (induction r) (auto simp: image_Un toplevel_summands_flatten_ACI_norm_image)

theorem ACI_norm_idem[simp]: "««r»» = «r»"
proof (induct r)
case (Plus r s)
have "««Plus r s»» = «flatten PLUS (toplevel_summands «r» ∪ toplevel_summands «s»)»"
(is "_ = «flatten PLUS ?U»") by simp
also have "… = flatten PLUS (ACI_norm  toplevel_summands (flatten PLUS ?U))"
by (simp only: ACI_norm_flatten)
also have "toplevel_summands (flatten PLUS ?U) = ?U"
by (intro toplevel_summands_flatten) (auto intro: Plus_toplevel_summands)
also have "flatten PLUS (ACI_norm  ?U) = flatten PLUS (toplevel_summands «r» ∪ toplevel_summands «s»)"
by (simp only: image_Un toplevel_summands_ACI_norm[symmetric] Plus)
finally show ?case by simp
qed auto

subsection "Atoms"

lemma atoms_toplevel_summands:
"atoms s = (⋃r∈toplevel_summands s. atoms r)"
by (induct s) auto

lemma wf_PLUS: "atoms (PLUS xs) ⊆ Σ ⟷ (∀r ∈ set xs. atoms r ⊆ Σ)"
by (induct xs rule: list_singleton_induct) auto

lemma atoms_PLUS: "atoms (PLUS xs) = (⋃r ∈ set xs. atoms r)"
by (induct xs rule: list_singleton_induct) auto

lemma atoms_flatten_PLUS:
"finite X ⟹ atoms (flatten PLUS X) = (⋃r ∈ X. atoms r)"
using wf_PLUS[of "sorted_list_of_set X"] by auto

theorem atoms_ACI_norm: "atoms «r» = atoms r"
proof (induct r)
case (Plus r1 r2) thus ?case
using atoms_toplevel_summands[of "«r1»"] atoms_toplevel_summands[of "«r2»"]
qed auto

subsection "Language"

lemma toplevel_summands_lang: "r ∈ toplevel_summands s ⟹ lang r ⊆ lang s"
by (induct s) auto

lemma toplevel_summands_lang_UN:
"lang s = (⋃r∈toplevel_summands s. lang r)"
by (induct s) auto

lemma toplevel_summands_in_lang:
"w ∈ lang s = (∃r∈toplevel_summands s. w ∈ lang r)"
by (induct s) auto

lemma lang_PLUS: "lang (PLUS xs) = (⋃r ∈ set xs. lang r)"
by (induct xs rule: list_singleton_induct) auto

lemma lang_PLUS_map[simp]:
"lang (PLUS (map f xs)) = (⋃a∈set xs. lang (f a))"
by (induct xs rule: list_singleton_induct) auto

lemma lang_flatten_PLUS[simp]:
"finite X ⟹ lang (flatten PLUS X) = (⋃r ∈ X. lang r)"
using lang_PLUS[of "sorted_list_of_set X"] by fastforce

theorem lang_ACI_norm[simp]: "lang «r» = lang r"
proof (induct r)
case (Plus r1 r2)
moreover
from Plus[symmetric] have "lang (Plus r1 r2) ⊆ lang «Plus r1 r2»"
using toplevel_summands_in_lang[of _ "«r1»"] toplevel_summands_in_lang[of _ "«r2»"]
by auto
ultimately show ?case by (fastforce dest!: toplevel_summands_lang)
qed auto

subsection ‹Finiteness of ACI-Equivalent Derivatives›

lemma toplevel_summands_deriv:
"toplevel_summands (deriv as r) = (⋃s∈toplevel_summands r. toplevel_summands (deriv as s))"
by (induction r) (auto simp: Let_def)

lemma derivs_Zero[simp]: "derivs xs Zero = Zero"
by (induction xs) auto

lemma derivs_One: "derivs xs One ∈ {Zero, One}"
by (induction xs) auto

lemma derivs_Atom: "derivs xs (Atom as) ∈ {Zero, One, Atom as}"
proof (induction xs)
case Cons thus ?case by (auto intro: insertE[OF derivs_One])
qed simp

lemma derivs_Plus: "derivs xs (Plus r s) = Plus (derivs xs r) (derivs xs s)"
by (induction xs arbitrary: r s) auto

lemma derivs_PLUS: "derivs xs (PLUS ys) = PLUS (map (derivs xs) ys)"
by (induction ys rule: list_singleton_induct) (auto simp: derivs_Plus)

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

lemma toplevel_summands_derivs_Star_nonempty:
"xs ≠ [] ⟹ toplevel_summands (derivs xs (Star r)) ⊆
{Times (derivs ys r) (Star r) | ys. ∃zs. ys ≠ [] ∧ zs @ ys = xs}"
proof (induction 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_derivs_Times] intro: exI[of _ "y#ys"])
(auto elim!: impE dest!: meta_spec subsetD)
qed

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

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

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

lemma finite_ACI_norm_toplevel_summands:
"finite {f «s» |s. toplevel_summands s ⊆ B}" if "finite B"
proof -
have *: "{f «s» | s.
toplevel_summands s ⊆ B} ⊆ (f ∘ flatten PLUS ∘ () ACI_norm)  Pow B"
by (subst ACI_norm_flatten) auto
with that show ?thesis
by (rule finite_surj [OF iffD2 [OF finite_Pow_iff]])
qed

theorem finite_derivs: "finite {«derivs xs r» | xs . True}"
proof (induct r)
case Zero show ?case by simp
next
case One show ?case
by (rule finite_surj[of "{Zero, One}"]) (blast intro: insertE[OF derivs_One])+
next
case (Atom as) show ?case
by (rule finite_surj[of "{Zero, One, Atom as}"]) (blast intro: insertE[OF derivs_Atom])+
next
case (Plus r s)
show ?case by (auto simp: derivs_Plus intro!: finite_surj[OF finite_cartesian_product[OF Plus]])
next
case (Times r s)
hence "finite (⋃ (toplevel_summands  {«derivs xs s» | xs . True}))" by auto
moreover have "{«r'» |r'. ∃ys. r' ∈ toplevel_summands (derivs ys s)} =
{r'. ∃ys. r' ∈ toplevel_summands «derivs ys s»}"
by (auto simp: toplevel_summands_ACI_norm)
ultimately have fin: "finite {«r'» |r'. ∃ys. r' ∈ toplevel_summands (derivs ys s)}"
by (fastforce intro: finite_subset[of _ "⋃ (toplevel_summands  {«derivs xs s» | xs . True})"])
let ?X = "λxs. {Times (derivs ys r) s | ys. True} ∪ {r'. r' ∈ (⋃ys. toplevel_summands (derivs 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_derivs_Times] intro!: imageI)
next
case (Star r)
let ?f = "λf r'. Times r' (Star (f r))"
let ?X = "{Star r} ∪ ?f id  {r'. r' ∈ {derivs 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_derivs_Star] intro!: imageI)
qed

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_deriv:
"(⋃a∈toplevel_summands r. toplevel_summands «deriv as «a»») = toplevel_summands «deriv as «r»»"
proof (induct r)
case (Plus r1 r2) thus ?case
unfolding toplevel_summands.simps toplevel_summands_ACI_norm
toplevel_summands_deriv[of as "«Plus r1 r2»"] image_Un Union_Un_distrib
qed (auto simp: Let_def)

lemma toplevel_summands_nullable:
"nullable s = (∃r∈toplevel_summands s. nullable r)"
by (induction s) auto

lemma nullable_PLUS:
"nullable (PLUS xs) = (∃r ∈ set xs. nullable r)"
by (induction xs rule: list_singleton_induct) auto

theorem ACI_norm_nullable: "nullable «r» = nullable r"
proof (induction r)
case (Plus r1 r2) thus ?case using toplevel_summands_nullable
by (auto simp: nullable_PLUS)
qed auto

theorem ACI_norm_deriv: "«deriv as «r»» = «deriv as r»"
proof (induction r arbitrary: as)
case (Plus r1 r2) thus ?case
unfolding deriv.simps ACI_norm_flatten[of "deriv as «Plus r1 r2»"]
toplevel_summands_deriv[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_deriv)

corollary deriv_preserves: "«r» = «s» ⟹ «deriv as r» = «deriv as s»"
by (rule box_equals[OF _ ACI_norm_deriv ACI_norm_deriv]) (erule arg_cong)

lemma derivs_snoc[simp]: "derivs (xs @ [x]) r = (deriv x (derivs xs r))"
by (induction xs arbitrary: r) auto

theorem ACI_norm_derivs: "«derivs xs «r»» = «derivs xs r»"
proof (induction xs arbitrary: r rule: rev_induct)
case (snoc x xs) thus ?case
using ACI_norm_deriv[of x "derivs xs r"] ACI_norm_deriv[of x "derivs xs «r»"] by auto
qed simp

subsection ‹Alternative ACI defintions›

text ‹Not necessary but conceptually nicer (and seems also to be faster?!)›

fun ACI_nPlus :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp"
where
"ACI_nPlus (Plus r1 r2) s = ACI_nPlus r1 (ACI_nPlus r2 s)"
| "ACI_nPlus r (Plus s1 s2) =
(if r = s1 then Plus s1 s2
else if r < s1 then Plus r (Plus s1 s2)
else Plus s1 (ACI_nPlus r s2))"
| "ACI_nPlus r s =
(if r = s then r
else if r < s then Plus r s
else Plus s r)"

primrec ACI_norm_alt where
"ACI_norm_alt Zero = Zero"
| "ACI_norm_alt One = One"
| "ACI_norm_alt (Atom a) = Atom a"
| "ACI_norm_alt (Plus r s) = ACI_nPlus (ACI_norm_alt r) (ACI_norm_alt s)"
| "ACI_norm_alt (Times r s) = Times (ACI_norm_alt r) (ACI_norm_alt s)"
| "ACI_norm_alt (Star r) = Star (ACI_norm_alt r)"

lemma toplevel_summands_ACI_nPlus:
"toplevel_summands (ACI_nPlus r s) = toplevel_summands (Plus r s)"
by (induct r s rule: ACI_nPlus.induct) auto

lemma toplevel_summands_ACI_norm_alt:
"toplevel_summands (ACI_norm_alt r) = ACI_norm_alt  toplevel_summands r"
by (induct r) (auto simp: toplevel_summands_ACI_nPlus)

lemma ACI_norm_alt_Plus:
"ACI_norm_alt r = Plus s t ⟹ ∃s t. r = Plus s t"
by (induct r) auto

lemma toplevel_summands_flatten_ACI_norm_alt_image:
"toplevel_summands (flatten PLUS (ACI_norm_alt  toplevel_summands r)) = ACI_norm_alt  toplevel_summands r"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_alt_Plus intro: Plus_toplevel_summands)

lemma ACI_norm_ACI_norm_alt: "«ACI_norm_alt r» = «r»"
proof (induction r)
case (Plus r s) show ?case
using ACI_norm_flatten [of r] ACI_norm_flatten [of s]
(metis ACI_norm_flatten Plus.IH(1) Plus.IH(2) image_Un toplevel_summands.simps(1) toplevel_summands_ACI_nPlus toplevel_summands_ACI_norm)
qed auto

lemma ACI_nPlus_singleton_PLUS:
"⟦xs ≠ []; sorted xs; distinct xs; ∀x ∈ {x} ∪ set xs. ¬(∃r s. x = Plus r s)⟧ ⟹
ACI_nPlus x (PLUS xs) = (if x ∈ set xs then PLUS xs else PLUS (insort x xs))"
proof (induct xs rule: list_singleton_induct)
case (single y)
thus ?case
by (cases x y rule: linorder_cases) (induct x y rule: ACI_nPlus.induct, auto)+
next
case (cons y1 y2 ys) thus ?case by (cases x) (auto)
qed simp

lemma ACI_nPlus_PLUS:
"⟦xs1 ≠ []; xs2 ≠ []; ∀x ∈ set (xs1 @ xs2). ¬(∃r s. x = Plus r s); sorted xs2; distinct xs2⟧⟹
ACI_nPlus (PLUS xs1) (PLUS xs2) = flatten PLUS (set (xs1 @ xs2))"
proof (induct xs1 arbitrary: xs2 rule: list_singleton_induct)
case (single x1)
thus ?case
apply (auto intro!: trans[OF ACI_nPlus_singleton_PLUS] simp del: sorted_list_of_set_insert)
apply (simp only: insert_absorb)
apply (metis List.finite_set finite_sorted_distinct_unique sorted_list_of_set)
apply (rule arg_cong[of _ _ PLUS])
apply (metis remdups_id_iff_distinct sorted_list_of_set_sort_remdups sorted_sort_id)
done
next
case (cons x11 x12 xs1) thus ?case
apply (simp del: sorted_list_of_set_insert)
apply (rule trans[OF ACI_nPlus_singleton_PLUS])
apply (auto simp del: sorted_list_of_set_insert simp add: insert_commute[of x11])
apply (auto simp only: Un_insert_left[of x11, symmetric] insert_absorb) []
apply (auto simp only: Un_insert_right[of _ x11, symmetric] insert_absorb) []
apply (auto simp add: insert_commute[of x12])
done
qed simp

lemma ACI_nPlus_flatten_PLUS:
"⟦X1 ≠ {}; X2 ≠ {}; finite X1; finite X2; ∀x ∈ X1 ∪ X2. ¬(∃r s. x = Plus r s)⟧⟹
ACI_nPlus (flatten PLUS X1) (flatten PLUS X2) = flatten PLUS (X1 ∪ X2)"
by (rule trans[OF ACI_nPlus_PLUS]) auto

lemma ACI_nPlus_ACI_norm [simp]: "ACI_nPlus «r» «s» = «Plus r s»"
by (auto simp: image_Un Un_assoc ACI_norm_flatten [of r] ACI_norm_flatten [of s] ACI_norm_flatten [of "Plus r s"]
toplevel_summands_flatten_ACI_norm_image
intro!: trans [OF ACI_nPlus_flatten_PLUS])
(metis ACI_norm_Plus Plus_toplevel_summands)+

lemma ACI_norm_alt:
"ACI_norm_alt r = «r»"
by (induct r) auto

declare ACI_norm_alt[symmetric, code]

inductive ACI where
ACI_refl:       "ACI r r" |
ACI_sym:        "ACI r s ⟹ ACI s r" |
ACI_trans:      "ACI r s ⟹ ACI s t ⟹ ACI r t" |
ACI_Plus_cong:  "⟦ACI r1 s1; ACI r2 s2⟧ ⟹ ACI (Plus r1 r2) (Plus s1 s2)" |
ACI_Times_cong: "⟦ACI r1 s1; ACI r2 s2⟧ ⟹ ACI (Times r1 r2) (Times s1 s2)" |
ACI_Star_cong:  "ACI r s ⟹ ACI (Star r) (Star s)" |
ACI_assoc:      "ACI (Plus (Plus r s) t) (Plus r (Plus s t))" |
ACI_comm:       "ACI (Plus r s) (Plus s r)" |
ACI_idem:       "ACI (Plus r r) r"

lemma ACI_atoms: "ACI r s ⟹ atoms r = atoms s"
by (induct rule: ACI.induct) auto

lemma ACI_nullable: "ACI r s ⟹ nullable r = nullable s"
by (induct rule: ACI.induct) auto

lemma ACI_lang: "ACI r s ⟹ lang r = lang s"
by (induct rule: ACI.induct) auto

lemma ACI_deriv: "ACI r s ⟹ ACI (deriv a r) (deriv a s)"
proof (induct arbitrary: a rule: ACI.induct)
case (ACI_Times_cong r1 s1 r2 s2) thus ?case
by (auto simp: Let_def intro: ACI.intros dest: ACI_nullable)
(metis ACI.ACI_Times_cong ACI_Plus_cong)
qed (auto intro: ACI.intros)

lemma ACI_Plus_assocI[intro]:
"ACI (Plus r1 r2) s2 ⟹ ACI (Plus r1 (Plus s1 r2)) (Plus s1 s2)"
"ACI (Plus r1 r2) s2 ⟹ ACI (Plus r1 (Plus r2 s1)) (Plus s1 s2)"
by (metis ACI_assoc ACI_comm ACI_Plus_cong ACI_refl ACI_trans)+

lemma ACI_Plus_idemI[intro]: "⟦ACI r s1; ACI r s2⟧ ⟹ ACI r (Plus s1 s2)"
by (metis ACI_Plus_cong ACI_idem ACI_sym ACI_trans)

lemma ACI_Plus_idemI'[intro]:
"⟦ACI r1 s1; ACI (Plus r1 r2) s2⟧ ⟹ ACI (Plus r1 r2) (Plus s1 s2)"
by (rule ACI_trans[OF ACI_Plus_cong[OF ACI_sym[OF ACI_idem] ACI_refl]
ACI_trans[OF ACI_assoc ACI_trans[OF ACI_Plus_cong ACI_refl]]])

lemma ACI_ACI_nPlus: "⟦ACI r1 s1; ACI r2 s2⟧ ⟹ ACI (ACI_nPlus r1 r2) (Plus s1 s2)"
proof (induct r1 r2 arbitrary: s1 s2 rule: ACI_nPlus.induct)
case 1
from 1(2)[OF ACI_refl 1(1)[OF ACI_refl 1(4)]] 1(3) show ?case by (auto intro: ACI_comm ACI_trans)
next
case ("2_1" r1 r2)
with ACI_Plus_cong[OF ACI_refl "2_1"(1)[OF _ _ "2_1"(2) ACI_refl], of r1]
show ?case by (auto intro: ACI.intros)
next
case ("2_2" r1 r2)
with ACI_Plus_cong[OF ACI_refl "2_2"(1)[OF _ _ "2_2"(2) ACI_refl], of r1]
show ?case by (auto intro: ACI.intros)
next
case ("2_3" _ r1 r2)
with ACI_Plus_cong[OF ACI_refl "2_3"(1)[OF _ _ "2_3"(2) ACI_refl], of r1]
show ?case by (auto intro: ACI.intros)
next
case ("2_4" _ _ r1 r2)
with ACI_Plus_cong[OF ACI_refl "2_4"(1)[OF _ _ "2_4"(2) ACI_refl], of r1]
show ?case by (auto intro: ACI.intros)
next
case ("2_5" _ r1 r2)
with ACI_Plus_cong[OF ACI_refl "2_5"(1)[OF _ _ "2_5"(2) ACI_refl], of r1]
show ?case by (auto intro: ACI.intros)
qed (auto intro: ACI.intros)

lemma ACI_ACI_norm: "ACI «r» r"
unfolding ACI_norm_alt[symmetric]
by (induct r) (auto intro: ACI.intros simp: ACI_ACI_nPlus)

lemma ACI_norm_eqI: "ACI r s ⟹ «r» = «s»"
by (induct rule: ACI.induct) (auto simp: toplevel_summands_ACI_norm ACI_norm_flatten[symmetric]
toplevel_summands_flatten_ACI_norm_image_Union ac_simps)

lemma ACI_I: "«r» = «s» ⟹ ACI r s"
by (metis ACI_ACI_norm ACI_sym ACI_trans)

lemma ACI_decidable: "ACI r s = («r» = «s»)"
by (metis ACI_I ACI_norm_eqI)

(*<*)
end
(*>*)


# Theory Deriv_PDeriv

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section "Connection Between Derivatives and Partial Derivatives"

(*<*)
theory Deriv_PDeriv
imports Derivatives_Finite
begin
(*>*)

lemma pderiv_not_is_Zero_is_Plus[simp]: "∀x ∈ pderiv a r. ¬ is_Zero x ∧ ¬ is_Plus x"
by (induct r) auto

lemma finite_pderiv[simp]: "finite (pderiv a r)"
by (induct r) auto

lemma PLUS_inject: "⟦∀x ∈ set xs ∪ set ys. ¬ is_Zero x ∧ ¬ is_Plus x; sorted xs; sorted ys⟧ ⟹
(PLUS xs = PLUS ys) ⟷ xs = ys"
proof (induct xs arbitrary: ys rule: list_singleton_induct)
case nil then show ?case by (induct ys rule: list_singleton_induct) auto
next
case single then show ?case by (induct ys rule: list_singleton_induct) auto
next
case cons then show ?case by (induct ys rule: list_singleton_induct) auto
qed

lemma sorted_list_of_set_inject: "⟦finite R; finite S⟧ ⟹
(sorted_list_of_set R = sorted_list_of_set S) ⟷ R = S"
proof (induct R arbitrary: S rule: finite_linorder_min_induct)
case empty then show ?case
proof (induct S rule: finite_linorder_min_induct)
case (insert b S) then show ?case by simp (metis insort_not_Nil)
qed simp
next
case (insert a R) from this(4,1-3) show ?case
proof (induct S rule: finite_linorder_min_induct)
case (insert b S)
show ?case
proof
assume "sorted_list_of_set (insert a R) = sorted_list_of_set (insert b S)"
with insert(1,2,4,5) have "insort a (sorted_list_of_set R) = insort b (sorted_list_of_set S)"
by (elim box_equals[OF _ sorted_list_of_set.insert sorted_list_of_set.insert]) auto
with insert(2,5) have "a # sorted_list_of_set R = b # sorted_list_of_set S"
apply (cases "sorted_list_of_set R" "sorted_list_of_set S" rule: list.exhaust[case_product list.exhaust])
apply (auto split: if_splits simp add: not_le)
using insort_not_Nil apply metis
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
done
with insert show "insert a R = insert b S" by auto
next
assume "insert a R = insert b S"
then show "sorted_list_of_set (insert a R) = sorted_list_of_set (insert b S)" by simp
qed
qed simp
qed

lemma flatten_PLUS_inject: "⟦∀x ∈ R ∪ S. ¬ is_Zero x ∧ ¬ is_Plus x; finite R; finite S⟧ ⟹
(flatten PLUS R = flatten PLUS S) = (R = S)"
by (rule trans[OF PLUS_inject sorted_list_of_set_inject]) auto

primrec pset where
"pset Zero = {}"
| "pset One = {One}"
| "pset (Atom a) = {Atom a}"
| "pset (Plus r s) = pset r ∪ pset s"
| "pset (Times r s) = Timess (pset r) s"
| "pset (Star r) = {Star r}"

lemma pset_not_is_Zero_is_Plus[simp]: "∀x ∈ pset r. ¬ is_Zero x ∧ ¬ is_Plus x"
by (induct r) auto

lemma finite_pset[simp]: "finite (pset r)"
by (induct r) auto

lemma pset_deriv: "pset (deriv a r) = pderiv a r"
by (induct r) auto

definition pnorm where
"pnorm = flatten PLUS o pset"

lemma pnorm_deriv_eq_iff_pderiv_eq:
"pnorm (deriv a r) = pnorm (deriv a s) ⟷ pderiv a r = pderiv a s"
unfolding pnorm_def o_apply pset_deriv
by (rule flatten_PLUS_inject) auto

fun pnPlus :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnPlus Zero r = r"
| "pnPlus r Zero = r"
| "pnPlus (Plus r s) t = pnPlus r (pnPlus s t)"
| "pnPlus r (Plus s t) =
(if r = s then (Plus s t)
else if le_rexp r s then Plus r (Plus s t)
else Plus s (pnPlus r t))"
| "pnPlus r s =
(if r = s then r
else if le_rexp r s then Plus r s
else Plus s r)"

fun pnTimes :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnTimes Zero r = Zero"
| "pnTimes (Plus r s) t = pnPlus (pnTimes r t) (pnTimes s t)"
| "pnTimes r s = Times r s"

primrec pnorm_alt :: "'a::linorder rexp ⇒ 'a rexp" where
"pnorm_alt Zero = Zero"
| "pnorm_alt One = One"
| "pnorm_alt (Atom a) = Atom a"
| "pnorm_alt (Plus r s) = pnPlus (pnorm_alt r) (pnorm_alt s)"
| "pnorm_alt (Times r s) = pnTimes (pnorm_alt r) s"
| "pnorm_alt (Star r) = Star r"

lemma pset_pnPlus:
"pset (pnPlus r s) = pset (Plus r s)"
by (induct r s rule: pnPlus.induct) auto

lemma pset_pnTimes:
"pset (pnTimes r s) = pset (Times r s)"
by (induct r s rule: pnTimes.induct) (auto simp: pset_pnPlus)

lemma pset_pnorm_alt_Times: "s ∈ pset r ⟹ pnTimes (pnorm_alt s) t = Times (pnorm_alt s) t"
by (induct r arbitrary: s t) auto

lemma pset_pnorm_alt:
"pset (pnorm_alt r) = pnorm_alt  pset r"
by (induct r) (auto simp: pset_pnPlus pset_pnTimes pset_pnorm_alt_Times image_iff)

lemma pset_pnTimes_Times: "s ∈ pset r ⟹ pnTimes s t = Times s t"
by (induct r arbitrary: s t) auto

lemma pset_pnorm_alt_id: "s ∈ pset r ⟹ pnorm_alt s = s"
by (induct r arbitrary: s) (auto simp: pset_pnTimes_Times)

lemma pnorm_alt_image_pset: "pnorm_alt  pset r = pset r"
by (induction r) (auto, auto simp add: pset_pnorm_alt_id pset_pnTimes_Times image_iff)

lemma pnorm_pnorm_alt: "pnorm (pnorm_alt r) = pnorm r"
by (induct r) (auto simp: pnorm_def pset_pnPlus pset_pnTimes pset_pnorm_alt pnorm_alt_image_pset)

lemma pnPlus_singleton_PLUS:
"⟦xs ≠ []; sorted xs; distinct xs; ∀x ∈ {x} ∪ set xs. ¬is_Zero x ∧ ¬is_Plus x⟧ ⟹
pnPlus x (PLUS xs) = (if x ∈ set xs then PLUS xs else PLUS (insort x xs))"
proof (induct xs rule: list_singleton_induct)
case (single y)
thus ?case unfolding is_Zero_def is_Plus_def
apply (cases x y rule: linorder_cases)
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
apply (cases y)
apply auto
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
done
next
case (cons y1 y2 ys) thus ?case unfolding is_Zero_def is_Plus_def
apply (cases x)
apply (metis UnCI insertI1)
apply simp apply (metis antisym less_eq_rexp_def)
apply simp apply (metis antisym less_eq_rexp_def)
apply (metis UnCI insertI1)
apply simp apply (metis antisym less_eq_rexp_def)
apply simp apply (metis antisym less_eq_rexp_def)
done
qed simp

lemma pnPlus_PlusL[simp]: "t ≠ Zero ⟹ pnPlus (Plus r s) t = pnPlus r (pnPlus s t)"
by (induct t) auto

lemma pnPlus_ZeroR[simp]: "pnPlus r Zero = r"
by (induct r) auto

lemma PLUS_eq_Zero: "PLUS xs = Zero ⟷ xs = [] ∨ xs = [Zero]"
by (induct xs rule: list_singleton_induct) auto

lemma pnPlus_PLUS:
"⟦xs1 ≠ []; xs2 ≠ []; ∀x ∈ set (xs1 @ xs2). ¬is_Zero x ∧ ¬is_Plus x; sorted xs2; distinct xs2⟧⟹
pnPlus (PLUS xs1) (PLUS xs2) = flatten PLUS (set (xs1 @ xs2))"
proof (induct xs1 arbitrary: xs2 rule: list_singleton_induct)
case (single x1)
thus ?case
apply (auto intro!: trans[OF pnPlus_singleton_PLUS]
simp: insert_absorb simp del: sorted_list_of_set_insert)
apply (metis List.finite_set finite_sorted_distinct_unique sorted_list_of_set)
apply (rule arg_cong[of _ _ PLUS])
apply (metis remdups_id_iff_distinct sorted_list_of_set_sort_remdups sorted_sort_id)
done
next
case (cons x11 x12 xs1)
then show ?case unfolding rexp_of_list.simps
apply (subst pnPlus_PlusL)
apply (unfold PLUS_eq_Zero) []
apply (metis in_set_conv_decomp rexp.disc(1))
apply (subst cons(1))
apply (simp_all del: sorted_list_of_set_insert)
apply (rule trans[OF pnPlus_singleton_PLUS])
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert)
apply safe
unfolding insert_commute[of x11]
apply (auto simp only: Un_insert_left[of x11, symmetric] insert_absorb) []
apply (auto simp only: Un_insert_right[of _ x11, symmetric] insert_absorb) []
done
qed simp

lemma pnPlus_flatten_PLUS:
"⟦X1 ≠ {}; X2 ≠ {}; finite X1; finite X2; ∀x ∈ X1 ∪ X2.  ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnPlus (flatten PLUS X1) (flatten PLUS X2) = flatten PLUS (X1 ∪ X2)"
by (rule trans[OF pnPlus_PLUS]) auto

lemma pnPlus_pnorm: "pnPlus (pnorm r) (pnorm s) = pnorm (Plus r s)"
by (cases "pset r = {} ∨ pset s = {}")
(auto simp: pnorm_def pset_pnPlus pset_pnorm_alt intro: pnPlus_flatten_PLUS)

lemma pnTimes_not_Zero_or_Plus[simp]: "⟦¬ is_Zero x; ¬ is_Plus x⟧ ⟹ pnTimes x r = Times x r"
by (cases x) auto

lemma pnTimes_PLUS:
"⟦xs ≠ []; ∀x ∈ set xs. ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnTimes (PLUS xs) r = flatten PLUS (Timess (set xs) r)"
proof (induct xs arbitrary: r rule: list_singleton_induct)
case (cons x y xs) then show ?case unfolding rexp_of_list.simps pnTimes.simps
apply (subst pnTimes_not_Zero_or_Plus)
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert)
apply (subst pnPlus_singleton_PLUS)
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert)
unfolding insert_commute[of "Times y r"]
apply (simp del: sorted_list_of_set_insert)
apply safe
apply (subst insert_absorb[of "Times x r"])
apply simp_all
done
qed auto

lemma pnTimes_flatten_PLUS:
"⟦X1 ≠ {}; finite X1; ∀x ∈ X1. ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnTimes (flatten PLUS X1) r = flatten PLUS (Timess X1 r)"
by (rule trans[OF pnTimes_PLUS]) auto

lemma pnTimes_pnorm: "pnTimes (pnorm r1) r2 = pnorm (Times r1 r2)"
by (cases "pset r1 = {}")
(auto simp: pnorm_def pset_pnTimes pset_pnorm_alt intro: pnTimes_flatten_PLUS)

lemma pnorm_alt[symmetric]: "pnorm_alt r = pnorm r"
by (induct r) (simp_all only: pnorm_alt.simps pnPlus_pnorm pnTimes_pnorm, auto simp: pnorm_def)

lemma insort_eq_Cons: "⟦∀a ∈ set xs. b < a; sorted xs⟧ ⟹ insort b xs = b # xs"
by (cases xs) auto

lemma pderiv_PLUS: "pderiv a (PLUS (x # xs)) = pderiv a x ∪ pderiv a (PLUS xs)"
by (cases xs) auto

lemma pderiv_set_flatten_PLUS:
"finite X ⟹ pderiv (a :: 'a :: linorder) (flatten PLUS X) = pderiv_set a X"
proof (induction X rule: finite_linorder_min_induct)
case (insert b X)
then have "b ∉ X" by auto
then have "pderiv a (flatten PLUS (insert b X)) = pderiv a b ∪ pderiv a (flatten PLUS X)"
by (simp add: pderiv_PLUS insort_eq_Cons insert.hyps)
also from insert.IH have "… = pderiv a b ∪ pderiv_set a X" by simp
finally show ?case by simp
qed simp

lemma fold_pderiv_set_flatten_PLUS:
"⟦w ≠ []; finite X⟧ ⟹ fold pderiv_set w {flatten PLUS X} = fold pderiv_set w X"
by (induct w arbitrary: X) (simp_all add: pderiv_set_flatten_PLUS)

lemma fold_pnorm_deriv:
"fold (λa r. pnorm (deriv a r)) w s = flatten PLUS (fold pderiv_set w {s})"
proof (induction w arbitrary: s)
case (Cons x w) then show ?case
proof (cases "w = []")
case False
show ?thesis using fold_pderiv_set_flatten_PLUS[OF False] Cons.IH
by (auto simp: pnorm_def pset_deriv)
qed simp

primrec
pnderiv :: "'a :: linorder ⇒ 'a rexp ⇒ 'a rexp"
where
"pnderiv c (Zero) = Zero"
| "pnderiv c (One) = Zero"
| "pnderiv c (Atom c') = (if c = c' then One else Zero)"
| "pnderiv c (Plus r1 r2) = pnPlus (pnderiv c r1) (pnderiv c r2)"
| "pnderiv c (Times r1 r2) =
(if nullable r1 then pnPlus (pnTimes (pnderiv c r1) r2) (pnderiv c r2) else pnTimes (pnderiv c r1) r2)"
| "pnderiv c (Star r) = pnTimes (pnderiv c r) (Star r)"

lemma pnderiv_alt[code]: "pnderiv a r = pnorm (deriv a r)"
by (induct r) (auto simp: pnorm_alt)

lemma pnderiv_pderiv: "pnderiv a r = flatten PLUS (pderiv a r)"
unfolding pnderiv_alt pnorm_def o_apply pset_deriv ..

(*<*)
end
(*>*)


# Theory Deriv_Autos

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section "Framework Instantiations using (Partial) Derivatives"

(*<*)
theory Deriv_Autos
imports
Automaton
"Regular-Sets.NDerivative"
Deriv_PDeriv
begin
(*>*)

subsection ‹Brzozowski Derivatives Modulo ACI›

lemma ACI_norm_derivs_alt: "«derivs w r» = fold (λa r. «deriv a r») w «r»"
by (induct w arbitrary: r) (auto simp: ACI_norm_deriv)

global_interpretation brzozowski: rexp_DFA "λr. «r»" "λa r. «deriv a r»" nullable lang
defines brzozowski_closure = brzozowski.closure
and check_eqv_brz = brzozowski.check_eqv
and reachable_brz = brzozowski.reachable
and automaton_brz = brzozowski.automaton
and match_brz = brzozowski.match
proof (unfold_locales, goal_cases)
case 1 show ?case by (rule lang_ACI_norm)
next
case 2 show ?case by (rule trans[OF lang_ACI_norm lang_deriv])
next
case 3 show ?case by (rule nullable_iff)
next
case 4 show ?case by (simp only: ACI_norm_derivs_alt[symmetric] finite_derivs)
qed

subsection ‹Brzozowski Derivatives Modulo ACI Operating on the Quotient Type›

lemma derivs_alt: "derivs = fold deriv"
proof
fix w :: "'a list" show "derivs w = fold deriv w" by (induct w) auto
qed

functor map_rexp by (simp_all only: o_def id_def map_map_rexp map_rexp_ident)

quotient_type 'a ACI_rexp = "'a rexp" / ACI
morphisms rep_ACI_rexp ACI_class
by (intro equivpI reflpI sympI transpI) (blast intro: ACI_refl ACI_sym ACI_trans)+

instantiation ACI_rexp :: ("{equal, linorder}") "{equal, linorder}"
begin
lift_definition less_eq_ACI_rexp :: "'a ACI_rexp ⇒ 'a ACI_rexp ⇒ bool" is "λr s. less_eq «r» «s»"
lift_definition less_ACI_rexp :: "'a ACI_rexp ⇒ 'a ACI_rexp ⇒ bool" is "λr s. less «r» «s»"
lift_definition equal_ACI_rexp :: "'a ACI_rexp ⇒ 'a ACI_rexp ⇒ bool" is "λr s. «r» = «s»"
instance by intro_classes (transfer, force simp: ACI_decidable)+
end

lift_definition ACI_deriv :: "'a :: linorder ⇒ 'a ACI_rexp ⇒ 'a ACI_rexp" is deriv
by (rule ACI_deriv)
lift_definition ACI_nullable :: "'a :: linorder ACI_rexp ⇒ bool" is nullable
by (rule ACI_nullable)
lift_definition ACI_lang :: "'a :: linorder ACI_rexp ⇒ 'a lang" is lang
by (rule ACI_lang)

lemma [transfer_rule]: "rel_fun (rel_set (pcr_ACI_rexp (=))) (=) (finite o image ACI_norm) finite"
unfolding rel_fun_def rel_set_def cr_ACI_rexp_def ACI_rexp.pcr_cr_eq
apply (auto simp: elim!: finite_surj[of _ _ ACI_class] finite_surj[of _ _ "ACI_norm o rep_ACI_rexp"])
apply (metis (hide_lams, no_types) ACI_norm_idem ACI_rexp.abs_eq_iff ACI_decidable imageI)
apply (rule image_eqI)
apply (subst ACI_decidable[symmetric])
apply (rule ACI_sym)
apply (rule Quotient_rep_abs[OF Quotient_ACI_rexp, OF ACI_refl])
apply blast
done

global_interpretation brzozowski_quotient: rexp_DFA ACI_class ACI_deriv ACI_nullable ACI_lang
defines brzozowski_quotient_closure = brzozowski_quotient.closure
and check_eqv_brzq = brzozowski_quotient.check_eqv
and reachable_brzq = brzozowski_quotient.reachable
and automaton_brzq = brzozowski_quotient.automaton
and match_brzq = brzozowski_quotient.match
proof (unfold_locales, goal_cases)
case 1 show ?case by transfer (rule refl)
next
case 2 show ?case by transfer (rule lang_deriv)
next
case 3 show ?case by transfer (rule nullable_iff)
next
case 4 show ?case by transfer
(auto simp: ACI_decidable derivs_alt intro!: finite_subset[OF _ finite_derivs])
qed

subsection ‹Brzozowski Derivatives Modulo ACI++ (Only Soundness)›

global_interpretation nderiv: rexp_DA "λx. norm x" nderiv nullable lang
defines nderiv_closure = nderiv.closure
and check_eqv_n = nderiv.check_eqv
and reachable_n = nderiv.reachable
and automaton_n = nderiv.automaton
and match_n = nderiv.match
proof (unfold_locales, goal_cases)
case 1 show ?case by simp
next
case 2 show ?case by (rule lang_nderiv)
next
case 3 show ?case by (rule nullable_iff)
qed

subsection ‹Partial Derivatives›

global_interpretation pderiv: rexp_DFA "λr. {r}" pderiv_set "λP. ∃p∈P. nullable p" "λP. ⋃(lang  P)"
defines pderiv_closure = pderiv.closure
and check_eqv_p = pderiv.check_eqv
and reachable_p = pderiv.reachable
and automaton_p = pderiv.automaton
and match_p = pderiv.match
proof (unfold_locales, goal_cases)
case 1 show ?case by simp
next
case 2 show ?case by (simp add: Deriv_pderiv)
next
case 3 show ?case by (simp add: nullable_iff)
next
case (4 s) note pderivs_lang_def[simp]
{ fix w :: "'a list"
have "fold pderiv_set w = Union o image (pderivs_lang {w})" by (induct w) auto
}
hence "{fold pderiv_set w {s} |w. True} ⊆ Pow (pderivs_lang UNIV s)" by auto
then show ?case by (rule finite_subset) (auto simp only: finite_pderivs_lang)
qed

global_interpretation pnderiv: rexp_DFA "λr. r" pnderiv nullable lang
defines pnderiv_closure = pnderiv.closure
and check_eqv_pn = pnderiv.check_eqv
and reachable_pn = pnderiv.reachable
and automaton_pn = pnderiv.automaton
and match_pn = pnderiv.match
proof (unfold_locales, goal_cases)
case 1 show ?case by simp
next
case 2 show ?case by (simp add: pnorm_def pset_deriv Deriv_pderiv pnderiv_alt)
next
case 3 show ?case by (simp add: nullable_iff)
next
case (4 s)
then show ?case unfolding pnderiv_alt[abs_def]
by (rule finite_surj[OF pderiv.fin, of _ "flatten PLUS" s]) (auto simp: fold_pnorm_deriv)
qed

subsection ‹Languages as States›

text ‹Not executable but still instructive.›

lemma Derivs_alt_def: "Derivs w L = fold Deriv w L"
by (induct w arbitrary: L) simp_all

interpretation language: rexp_DFA lang Deriv "λL. [] ∈ L" id
proof (unfold_locales, goal_cases)
case (4 s)
have "{fold Deriv w (lang s) |w. True} ⊆ (λX. ⋃(lang  X))  Pow (pderivs_lang UNIV s)"
by (auto simp: sym[OF Derivs_alt_def] Derivs_pderivs pderivs_lang_def)
then show ?case by (rule finite_surj[OF iffD2[OF finite_Pow_iff finite_pderivs_lang_UNIV]])
qed simp_all

definition str_eq :: "'a lang => ('a list × 'a list) set" ("≈_" [100] 100)
where "≈A ≡ {(x, y).  (∀z. x @ z ∈ A ⟷ y @ z ∈ A)}"

lemma str_eq_alt: "≈A = {(x, y). fold Deriv x A = fold Deriv y A}"
unfolding str_eq_def set_eq_iff in_fold_Deriv by simp

lemma Myhill_Nerode2: "finite (UNIV // ≈lang r)"
unfolding str_eq_alt quotient_def Image_def
by (rule finite_surj[OF language.fin, of _ "λX. {y. X = fold Deriv y (lang r)}" r]) auto

(*<*)
end
(*>*)


# Theory Position_Autos

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section ‹Framework Instantiations using Marked Regular Expressions›

(*<*)
theory Position_Autos
imports
Automaton
begin
(*>*)

subsection ‹Marked Regular Expressions›

type_synonym 'a mrexp = "(bool * 'a) rexp"

abbreviation "strip ≡ map_rexp snd"

primrec mrexps :: "'a rexp ⇒ ('a mrexp) set" where
"mrexps Zero = {Zero}"
| "mrexps One = {One}"
| "mrexps (Atom a) = {Atom (True, a), Atom (False, a)}"
| "mrexps (Plus r s) = case_prod Plus  (mrexps r × mrexps s)"
| "mrexps (Times r s) = case_prod Times  (mrexps r × mrexps s)"
| "mrexps (Star r) = Star  mrexps r"

lemma finite_mrexps[simp]: "finite (mrexps r)"
by (induction r) auto

lemma strip_mrexps: "strip  mrexps r = {r}"
by (induction r) (auto simp: set_eq_subset subset_iff image_iff)

fun Lm :: "'a mrexp ⇒ 'a lang" where
"Lm Zero = {}" |
"Lm One = {}" |
"Lm (Atom(m,a)) = (if m then {[a]} else {})" |
"Lm (Plus r s) = Lm r ∪ Lm s" |
"Lm (Times r s) = Lm r @@ lang(strip s) ∪ Lm s" |
"Lm (Star r) = Lm r @@ star(lang(strip r))"

fun final :: "'a mrexp ⇒ bool" where
"final Zero = False" |
"final One = False" |
"final (Atom(m,a)) = m" |
"final (Plus r s) = (final r ∨ final s)" |
"final (Times r s) = (final s ∨ nullable s ∧ final r)" |
"final (Star r) = final r"

abbreviation read :: "'a ⇒ 'a mrexp ⇒ 'a mrexp" where
"read a ≡ map_rexp (λ(m,x). (m ∧ a=x, x))"

lemma read_mrexps[simp]: "r ∈ mrexps s ⟹ read a r ∈ mrexps s"
by (induction s arbitrary: a r) (auto simp: image_iff)

fun follow :: "bool ⇒ 'a mrexp ⇒ 'a mrexp" where
"follow m Zero = Zero" |
"follow m One = One" |
"follow m (Atom(_,a)) = Atom(m,a)" |
"follow m (Times r s) =
Times (follow m r) (follow (final r ∨ m ∧ nullable r) s)" |

lemma follow_mrexps[simp]: "r ∈ mrexps s ⟹ follow b r ∈ mrexps s"
by (induction s arbitrary: b r) (auto simp: image_iff)

lemma Nil_notin_Lm[simp]: "[] ∉ Lm r"
by (induction r) (auto split: if_splits)

lemma Nil_in_lang_strip[simp]: "[] ∈ lang(r) ⟷ [] ∈ lang(strip r)"
by (induction r) auto

lemma strip_follow[simp]: "strip(follow m r) = strip r"
by (induction r arbitrary: m) (auto split: if_splits)

lemma conc_lemma: "[] ∉ A ⟹ {w : A @@ B. w ≠ [] ∧ P(hd w)} = {w : A. w ≠ [] ∧ P(hd w)} @@ B"
unfolding conc_def by auto (metis hd_append2)+

lemma Lm_read: "Lm (read a r) = {w : Lm r. w ≠ [] ∧ hd w = a}"
proof (induction r)
case (Times r1 r2) thus ?case
using conc_lemma[OF Nil_notin_Lm, where P = "λx. x=a" and r1 = r1] by auto
next
case Star thus ?case using conc_lemma[OF Nil_notin_Lm, where P = "λx. x=a"] by simp
qed (auto split: if_splits)

lemma tl_conc[simp]: "[] ∉ A ⟹tl  (A @@ B) = tl  A @@ B"
by (fastforce simp: image_def Bex_def tl_append split: list.split)

lemma Nil_in_tl_Lm_if_final[simp]: "final r ⟹ [] : tl  Lm r"
by (induction r) (auto simp: nullable_iff image_Un)

lemma Nil_notin_tl_if_not_final: "¬ final r ⟹ [] ∉ tl  Lm r"
by (induction r) (auto simp: nullable_iff Nil_tl singleton_in_conc intro!: image_eqI[rotated])

lemma Lm_follow: "Lm (follow m r) = tl  Lm r ∪ (if m then lang(strip r) else {}) - {[]}"
proof (induction r arbitrary: m)
case (Atom mb) thus ?case by (cases mb) auto
next
case (Times r s) thus ?case
by (simp add: Un_Diff image_Un conc_Un_distrib nullable_iff
conc_Diff_if_Nil1 Nil_notin_tl_if_not_final Un_ac)
next
case (Star r) thus ?case
conc_Diff_if_Nil1 Nil_notin_tl_if_not_final star_Diff_Nil_fold)
qed auto

subsection ‹Mark Before Atom›

text‹Position automaton where mark is placed before atoms.›

abbreviation "empty_mrexp ≡ map_rexp (λa. (False,a))"

lemma empty_mrexp_mrexps[simp]: "empty_mrexp r ∈ mrexps r"
by (induction r) auto

lemma nullable_empty_mrexp[simp]: "nullable (empty_mrexp r) = nullable r"
by (induct r) auto

definition "init_b r = (follow True (empty_mrexp r), nullable r)"

lemma init_b_mrexps[simp]: "init_b r ∈ mrexps r × UNIV"
unfolding init_b_def by auto

fun delta_b where
"delta_b a (r,b) = (let r' = read a r in (follow False r', final r'))"

lemma delta_b_mrexps[simp]: "rb ∈ mrexps r × UNIV ⟹ delta_b a rb ∈ mrexps r × UNIV"
by (auto simp: Let_def)

lemma fold_delta_b_init_b_mrexps[simp]: "fold delta_b w (init_b s) ∈ mrexps s × UNIV"
by (induction w arbitrary: s rule: rev_induct) auto

fun L_b where
"L_b (r,b) = Lm r ∪ (if b then {[]} else {})"

abbreviation "final_b ≡ snd"

lemma Lm_empty: "Lm (empty_mrexp r) = {}"
by (induction r) auto

by (induction r) (auto simp: nullable_iff concI_if_Nil2 singleton_in_conc split: if_splits)

global_interpretation before: rexp_DFA init_b delta_b final_b L_b
defines before_closure = before.closure
and check_eqv_b = before.check_eqv
and reachable_b = before.reachable
and automaton_b = before.automaton
and match_b = before.match
proof (standard, goal_cases)
case (1 r) show "L_b (init_b r) = lang r"
next
case (2 a rb) show "L_b (delta_b a rb) = Deriv a (L_b rb)"
next
case (3 rb) show  "final_b rb ⟷ [] ∈ L_b rb" by (cases rb) simp
next
case (4 s)
have "{fold delta_b w (init_b s) |w. True} ⊆ mrexps s × UNIV"
by (intro subsetI, elim CollectE exE) (simp only: fold_delta_b_init_b_mrexps)
then show "finite {fold delta_b w (init_b s) |w. True}" by (rule finite_subset) simp
qed

subsection ‹Mark After Atom›

text‹Position automaton where mark is placed after atoms. This is the

definition "init_a r = (True, empty_mrexp r)"

lemma init_a_mrexps[simp]: "init_a r ∈ UNIV × mrexps r"
unfolding init_a_def by auto

fun delta_a where

lemma delta_a_mrexps[simp]: "br ∈ UNIV × mrexps r ⟹ delta_a a br ∈ UNIV × mrexps r"
by auto

lemma fold_delta_a_init_a_mrexps[simp]: "fold delta_a w (init_a s) ∈ UNIV × mrexps s"
by (induction w arbitrary: s rule: rev_induct) auto

fun final_a where
"final_a (b,r) ⟷ final r ∨ b ∧ nullable r"

fun L_a where
"L_a (b,r) = Lm (follow b r) ∪ (if final_a(b,r)  then {[]} else {})"

lemma nonfinal_empty_mrexp: "¬ final (empty_mrexp r)"
by (induction r) auto

lemma Cons_eq_tl_iff[simp]: "x # xs = tl ys ⟷ (∃y. ys = y # x # xs)"
by (cases ys) auto

lemma tl_eq_Cons_iff[simp]: "tl ys = x # xs ⟷ (∃y. ys = y # x # xs)"
by (cases ys) auto

global_interpretation after: rexp_DFA init_a delta_a final_a L_a
defines after_closure = after.closure
and check_eqv_a = after.check_eqv
and reachable_a = after.reachable
and automaton_a = after.automaton
and match_a = after.match
proof (standard, goal_cases)
case (1 r) show "L_a (init_a r) = lang r"
by (auto simp: init_a_def nonfinal_empty_mrexp Lm_follow Lm_empty map_map_rexp nullable_iff)
next
case (2 a br) show "L_a (delta_a a br) = Deriv a (L_a br)"
fastforce simp: image_def neq_Nil_conv)
next
case (3 br) show  "final_a br ⟷ [] ∈ L_a br" by (cases br) simp
next
case (4 s)
have "{fold delta_a w (init_a s) |w. True} ⊆ UNIV × mrexps s"
by (intro subsetI, elim CollectE exE) (simp only: fold_delta_a_init_a_mrexps)
then show "finite {fold delta_a w (init_a s) |w. True}" by (rule finite_subset) simp
qed

text ‹
The before'' atomaton is a quotient of the after'' automaton.

The proof below follows an informal proof given by Helmut Seidl in personal communication.
›

fun hom_ab where
"hom_ab (b, r) = (follow b r, final_a (b, r))"

lemma hom_delta: "hom_ab (delta_a x br) = delta_b x (hom_ab br)"
by(cases br) (auto simp add: Let_def)

lemma hom_deltas: "hom_ab (fold delta_a w br) = fold delta_b w (hom_ab br)"
by (induct w arbitrary: br) (auto simp add: hom_delta)

lemma hom_init: "hom_ab (init_a r) = init_b r"
unfolding init_a_def init_b_def hom_ab.simps by (simp add: nonfinal_empty_mrexp)

lemma reachable_ab: "reachable_b as r = hom_ab  reachable_a as r"
unfolding after.reachable before.reachable by (force simp: hom_init hom_deltas)

theorem card_reachable_ab: "card (reachable_b as r) ≤ card (reachable_a as r)"
unfolding reachable_ab using after.finite_reachable by (rule card_image_le)

text‹The implementation by Fischer et al.:›

(* better: shift b m r and move m b r *)
fun shift :: "bool ⇒ 'a mrexp ⇒ 'a ⇒ 'a mrexp" where
"shift _ One _ = One" |
"shift _ Zero _ = Zero" |
"shift m (Atom (_,x)) c = Atom (m ∧ (x=c),x)" |
"shift m (Plus r s) c = Plus (shift m r c) (shift m s c)" |
"shift m (Times r s) c =
Times (shift m r c) (shift (final r ∨ m ∧ nullable r) s c)" |
"shift m (Star r) c = Star (shift (final r ∨ m) r c)"

by (induction m r x rule: shift.induct) auto

text‹In the spirit of Asperti, and similarly quadratic because of need
to call final1 in move.›

fun final1 :: "'a mrexp ⇒ 'a ⇒ bool" where
"final1 Zero _ = False" |
"final1 One _ = False" |
"final1 (Atom(m,a)) x = (m ∧ a=x)" |
"final1 (Plus r s) x = (final1 r x ∨ final1 s x)" |
"final1 (Times r s) x = (final1 s x ∨ nullable s ∧ final1 r x)" |
"final1 (Star r) x = final1 r x"

fun move :: "'a ⇒ 'a mrexp ⇒ bool ⇒ 'a mrexp" where
"move _ One _ = One" |
"move _ Zero _ = Zero" |
"move c (Atom (_,a)) m = Atom (m, a)" |
"move c (Plus r s) m = Plus (move c r m) (move c s m)" |
"move c (Times r s) m =
Times (move c r m) (move c s (final1 r c ∨ m ∧ nullable r))" |
"move c (Star r) m = Star (move c r (final1 r c ∨ m))"

by (induction r) auto

by (induction r) auto

by (induction c r m rule: move.induct) (auto simp: final_read_final1)

(*<*)
end
(*>*)



# Theory After2

(* Author: Tobias Nipkow, Dmitriy Traytel *)

section ‹Linear Time Optimization for Mark After Atom''›

(*<*)
theory After2
imports
Position_Autos
begin
(*>*)

datatype 'a mrexp2 =
Zero2 |
One2 |
Atom2 (fin: bool) 'a |
Plus2 "'a mrexp2" "'a mrexp2" (fin: bool) (nul: bool) |
Times2 "'a mrexp2" "'a mrexp2" (fin: bool) (nul: bool) |
Star2 "'a mrexp2" (fin: bool)
where
"fin Zero2 = False"
| "nul Zero2 = False"
| "fin One2 = False"
| "nul One2 = True"
| "nul (Atom2 _ _) = False"
| "nul (Star2 _ _) = True"

primrec mrexps2 :: "'a rexp ⇒ ('a mrexp2) set" where
"mrexps2 Zero = {Zero2}"
| "mrexps2 One = {One2} "
| "mrexps2 (Atom a) = {Atom2 True a, Atom2 False a}"
| "mrexps2 (Plus r s) = (λ(r, s, f, n). Plus2 r s f n)  (mrexps2 r × mrexps2 s × UNIV)"
| "mrexps2 (Times r s) = (λ(r, s, f, n). Times2 r s f n)  (mrexps2 r × mrexps2 s  × UNIV)"
| "mrexps2 (Star r) = (λ(r, f). Star2 r f)  (mrexps2 r × UNIV)"

lemma finite_mrexps3[simp]: "finite (mrexps2 r)"
by (induction r) auto

definition[simp]: "plus2 r s == Plus2 r s (fin r ∨ fin s) (nul r ∨ nul s)"
definition[simp]: "times2 r s == Times2 r s (fin r ∧ nul s ∨ fin s) (nul r ∧ nul s)"
definition[simp]: "star2 r == Star2 r (fin r)"

primrec empty_mrexp2 :: "'a rexp ⇒ 'a mrexp2" where
"empty_mrexp2 Zero = Zero2" |
"empty_mrexp2 One = One2" |
"empty_mrexp2 (Atom x) = Atom2 False x" |
"empty_mrexp2 (Plus r s) = plus2 (empty_mrexp2 r) (empty_mrexp2 s)" |
"empty_mrexp2 (Times r s) = times2 (empty_mrexp2 r) (empty_mrexp2 s)" |
"empty_mrexp2 (Star r) = star2 (empty_mrexp2 r)"

primrec shift2 :: "bool ⇒ 'a mrexp2 ⇒ 'a ⇒ 'a mrexp2" where
"shift2 _ One2 _ = One2" |
"shift2 _ Zero2 _ = Zero2" |
"shift2 m (Atom2 _ x) c = Atom2 (m ∧ (x=c)) x" |
"shift2 m (Plus2 r s _ _) c = plus2 (shift2 m r c) (shift2 m s c)" |
"shift2 m (Times2 r s _ _) c = times2 (shift2 m r c) (shift2 (m ∧ nul r ∨ fin r) s c)" |
"shift2 m (Star2 r _) c =  star2 (shift2 (m ∨ fin r) r c)"

primrec strip2 where
"strip2 Zero2 = Zero" |
"strip2 One2 = One" |
"strip2 (Atom2 m x) = Atom (m, x)" |
"strip2 (Plus2 r s _ _) = Plus (strip2 r) (strip2 s)" |
"strip2 (Times2 r s _ _) = Times (strip2 r) (strip2 s)" |
"strip2 (Star2 r _) = Star (strip2 r)"

lemma strip_mrexps2: "(strip o strip2)  mrexps2 r = {r}"
by (induction r) (auto simp: set_eq_subset subset_iff image_iff)

primrec ok2 :: "'a mrexp2 ⇒ bool" where
"ok2 Zero2 = True" |
"ok2 One2 = True" |
"ok2 (Atom2 _ _) = True" |
"ok2 (Plus2 r s f n) = (ok2 r ∧ ok2 s ∧
(let rs = Plus (strip2 r) (strip2 s) in f = final rs ∧ n = nullable rs))" |
"ok2 (Times2 r s f n) = (ok2 r ∧ ok2 s ∧
(let rs = Times (strip2 r) (strip2 s) in f = final rs ∧ n = nullable rs))" |
"ok2 (Star2 r f) = (ok2 r ∧ f = final (strip2 r))"

lemma ok2_fin_final[simp]: "ok2 r ⟹ fin r = final (strip2 r)"
by (induct r) auto

lemma ok2_nul_nullable[simp]: "ok2 r ⟹ nul r = nullable (strip2 r)"
by (induct r) auto

lemma strip2_shift2: "ok2 r ⟹ strip2(shift2 m r c) = shift m (strip2 r) c"
apply(induction r arbitrary: m)
apply (auto simp: disj_commute)
done

lemma ok2_empty_mrexp2: "ok2 (empty_mrexp2 r)"
apply(induction r)
apply auto
done

lemma ok2_shift2: "ok2 r ⟹ ok2(shift2 m r c)"
apply(induction r arbitrary: m)
apply auto
done

lemma strip2_empty_mrexp2[simp]: "strip2 (empty_mrexp2 r) = empty_mrexp r"
by (induct r) auto

lemma nul_empty_mrexp2[simp]: "nul (empty_mrexp2 r) = nullable r"
by (induct r) auto

lemma nonfin_empty_mrexp2[simp]: "¬ fin (empty_mrexp2 r)"
by (induct r) auto

lemma empty_mrexp2_mrexps2[simp]: "empty_mrexp2 s ∈ mrexps2 s"
by (induct s) (auto simp: image_iff)

lemma shift2_mrexps2[simp]: "r ∈ mrexps2 s ⟹ shift2 x r a ∈ mrexps2 s"
by (induct s arbitrary: r x) (auto simp: image_iff)

typedef 'a ok_mrexp2 = "{(b :: bool, r :: 'a mrexp2). ok2 r}"
unfolding mem_Collect_eq split_beta by (metis snd_eqD ok2_empty_mrexp2)

setup_lifting type_definition_ok_mrexp2

lift_definition init_okm :: "'a rexp ⇒ 'a ok_mrexp2" is "λr. (True, empty_mrexp2 r)"
by (simp add: ok2_empty_mrexp2 del: ok2.simps)
lift_definition delta_okm :: "'a ⇒ 'a ok_mrexp2 ⇒ 'a ok_mrexp2" is
"λa (m, r). (False, shift2 m r a)"
unfolding mem_Collect_eq split_beta snd_conv by (intro ok2_shift2) simp
lift_definition nullable_okm :: "'a ok_mrexp2 ⇒ bool" is "λ(m, r). fin r ∨ m ∧ nul r" .
lift_definition lang_okm :: "'a ok_mrexp2 ⇒ 'a lang" is "λ(m, r). L_a (m, strip2 r)" .

instantiation ok_mrexp2 :: (equal) "equal"
begin

fun eq_mrexp2 where
"eq_mrexp2 Zero2 Zero2 = True"
| "eq_mrexp2 One2 One2 = True"
| "eq_mrexp2 (Atom2 m x) (Atom2 m' y) = (m = m' ∧ x = y)"
| "eq_mrexp2 (Plus2 r1 s1 _ _) (Plus2 r2 s2 _ _) = (eq_mrexp2 r1 r2 ∧ eq_mrexp2 s1 s2)"
| "eq_mrexp2 (Times2 r1 s1 _ _) (Times2 r2 s2 _ _) = (eq_mrexp2 r1 r2 ∧ eq_mrexp2 s1 s2)"
| "eq_mrexp2 (Star2 r1 _) (Star2 r2 _) = (eq_mrexp2 r1 r2)"
| "eq_mrexp2 r s = False"

lemma eq_mrexp2_imp_eq: "⟦eq_mrexp2 r s; ok2 r; ok2 s⟧ ⟹ (r = s)"
by (induct rule: eq_mrexp2.induct) auto

lemma eq_mrexp2_refl[simplified, simp]: "r = s ⟹ eq_mrexp2 r s"
by (induct rule: eq_mrexp2.induct) auto

lemma eq_mrexp2_eq: "⟦ok2 r; ok2 s⟧ ⟹ eq_mrexp2 r s = (r = s)"
by (metis eq_mrexp2_imp_eq eq_mrexp2_refl)

lift_definition equal_ok_mrexp2 :: "'a ok_mrexp2 ⇒ 'a ok_mrexp2 ⇒ bool"
is "λ(b1,r1) (b2, r2). b1 = b2 ∧ eq_mrexp2 r1 r2" .

instance by intro_classes (transfer, auto simp: eq_mrexp2_eq)

end

global_interpretation after2: rexp_DFA init_okm delta_okm nullable_okm lang_okm
defines after2_closure = after2.closure
and check_eqv_a2 = after2.check_eqv
and reachable_a2 = after2.reachable
and automaton_a2 = after2.automaton
and match_a2 = after2.match
proof (standard, goal_cases)
case (1 r) show "lang_okm (init_okm r) = lang r"
by transfer (auto simp: split_beta init_a_def nonfinal_empty_mrexp Lm_follow Lm_empty
map_map_rexp nullable_iff)
next
case (2 a br) show "lang_okm (delta_okm a br) = Deriv a (lang_okm br)"
apply transfer
unfolding split_beta fst_conv snd_conv mem_Collect_eq after.L_delta[symmetric] delta_a.simps
by (subst strip2_shift2) simp_all
next
case (3 br) show  "nullable_okm br = ([] ∈ lang_okm br)"
next
case (4 s)
have "{fold (λa (m, r). (False, shift2 m r a)) w (True, empty_mrexp2 s) |w. True} ⊆
UNIV × mrexps2 s"
proof (intro subsetI, elim CollectE exE conjE, hypsubst)
fix w show "fold (λa (m, r). (False, shift2 m r a)) w (True, empty_mrexp2 s) ∈
UNIV × mrexps2 s"
by (induct w rule: rev_induct) (auto simp: split: prod.splits intro!: shift2_mrexps2)
qed
then show "finite {fold delta_okm w (init_okm s) |w. True}"
by transfer (erule finite_subset[OF subset_trans[rotated]], auto)
qed

(*<*)
end
(*>*)


# Theory Before2

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section ‹Linear Time Optimization for Mark Before Atom'' (for a Fixed Alphabet)›

(*<*)
theory Before2
imports
Position_Autos
begin
(*>*)

declare Let_def[simp]

datatype 'a mrexp3 =
Zero3 |
One3 |
Atom3 bool 'a |
Plus3 "'a mrexp3" "'a mrexp3" (fin1: "'a set") (nul: bool) |
Times3 "'a mrexp3" "'a mrexp3" (fin1: "'a set") (nul: bool) |
Star3 "'a mrexp3" (fin1: "'a set")
where
"fin1 Zero3 = {}"
| "nul Zero3 = False"
| "fin1 One3 = {}"
| "nul One3 = True"
| "fin1 (Atom3 m a) = (if m then {a} else {})"
| "nul (Atom3 _ _) = False"
| "nul (Star3 _ _) = True"

primrec final3 where
"final3 Zero3 = False"
| "final3 One3 = False"
| "final3 (Atom3 m a) = m"
| "final3 (Plus3 r s _ _) = (final3 r ∨ final3 s)"
| "final3 (Times3 r s _ _) = (final3 s ∨ nul s ∧ final3 r)"
| "final3 (Star3 r _) = final3 r"

primrec mrexps3 :: "'a rexp ⇒ ('a mrexp3) set" where
"mrexps3 Zero = {Zero3}"
| "mrexps3 One = {One3} "
| "mrexps3 (Atom a) = {Atom3 True a, Atom3 False a}"
| "mrexps3 (Plus r s) = (λ(r, s, f1, n). Plus3 r s f1 n)  (mrexps3 r × mrexps3 s × Pow (atoms (Plus r s)) × UNIV)"
| "mrexps3 (Times r s) = (λ(r, s, f1, n). Times3 r s f1 n)  (mrexps3 r × mrexps3 s × Pow (atoms (Times r s))  × UNIV)"
| "mrexps3 (Star r) = (λ(r, f1). Star3 r f1)  (mrexps3 r × Pow (atoms (Star r)))"

lemma finite_atoms[simp]: "finite (atoms r)"
by (induct r) auto

lemma finite_mrexps3[simp]: "finite (mrexps3 r)"
by (induct r) auto

definition[simp]: "plus3 r s == Plus3 r s (fin1 r ∪ fin1 s) (nul r ∨ nul s)"
definition[simp]: "times3 r s ==
let ns = nul s in Times3 r s (fin1 s ∪ (if ns then fin1 r else {})) (nul r ∧ ns)"
definition[simp]: "star3 r == Star3 r (fin1 r)"

primrec follow3 :: "bool ⇒ 'a mrexp3 ⇒ 'a mrexp3" where
"follow3 m Zero3 = Zero3" |
"follow3 m One3 = One3" |
"follow3 m (Atom3 _ a) = Atom3 m a" |
"follow3 m (Plus3 r s _ _) = plus3 (follow3 m r) (follow3 m s)" |
"follow3 m (Times3 r s _ _) =
times3 (follow3 m r) (follow3 (final3 r ∨ m ∧ nul r) s)" |
"follow3 m (Star3 r _) = star3(follow3 (final3 r ∨ m) r)"

primrec empty_mrexp3 :: "'a rexp ⇒ 'a mrexp3" where
"empty_mrexp3 Zero = Zero3" |
"empty_mrexp3 One = One3" |
"empty_mrexp3 (Atom x) = Atom3 False x" |
"empty_mrexp3 (Plus r s) = plus3 (empty_mrexp3 r) (empty_mrexp3 s)" |
"empty_mrexp3 (Times r s) = times3 (empty_mrexp3 r) (empty_mrexp3 s)" |
"empty_mrexp3 (Star r) = star3 (empty_mrexp3 r)"

primrec move3 :: "'a ⇒ 'a mrexp3 ⇒ bool ⇒ 'a mrexp3" where
"move3 _ One3 _ = One3" |
"move3 _ Zero3 _ = Zero3" |
"move3 c (Atom3 _ a) m = Atom3 m a" |
"move3 c (Plus3 r s _ _) m = plus3 (move3 c r m) (move3 c s m)" |
"move3 c (Times3 r s _ _) m =
times3 (move3 c r m) (move3 c s (c ∈ fin1 r ∨ m ∧ nul r))" |
"move3 c (Star3 r _) m = star3 (move3 c r (c ∈ fin1 r ∨ m))"

primrec strip3 where
"strip3 Zero3 = Zero" |
"strip3 One3 = One" |
"strip3 (Atom3 m x) = Atom (m, x)" |
"strip3 (Plus3 r s _ _) = Plus (strip3 r) (strip3 s)" |
"strip3 (Times3 r s _ _) = Times (strip3 r) (strip3 s)" |
"strip3 (Star3 r _) = Star (strip3 r)"

lemma strip_mrexps3: "(strip o strip3)  mrexps3 r = {r}"
by (induction r) (auto simp: set_eq_subset subset_iff image_iff)

primrec ok3 :: "'a mrexp3 ⇒ bool" where
"ok3 Zero3 = True" |
"ok3 One3 = True" |
"ok3 (Atom3 _ _) = True" |
"ok3 (Plus3 r s f1 n) = (ok3 r ∧ ok3 s ∧
(let rs = Plus (strip3 r) (strip3 s) in f1 = Collect (final1 rs) ∧ n = nullable rs))" |
"ok3 (Times3 r s f1 n) = (ok3 r ∧ ok3 s ∧
(let rs = Times (strip3 r) (strip3 s) in f1 = Collect (final1 rs) ∧ n = nullable rs))" |
"ok3 (Star3 r f1) = (ok3 r ∧ f1 = Collect (final1 (strip3 r)))"

lemma ok3_fin1_final1[simp]: "ok3 r ⟹ fin1 r = Collect (final1 (strip3 r))"
by (induct r) (auto simp add: set_eq_iff)

lemma ok3_nul_nullable[simp]: "ok3 r ⟹ nul r = nullable (strip3 r)"
by (induct r) auto

lemma ok3_final3_final[simp]: "ok3 r ⟹ final3 r = final (strip3 r)"
by (induct r) auto

lemma follow3_follow[simp]: "ok3 r ⟹ strip3 (follow3 m r) = follow m (strip3 r)"
by (induct r arbitrary: m) auto

lemma nul_follow3[simp]: "ok3 r ⟹ nul (follow3 m r) = nul r"
by (induct r arbitrary: m) auto

lemma ok3_follow3[simp]: "ok3 r ⟹ ok3 (follow3 m r)"
by (induct r arbitrary: m) auto

lemma fin1_atoms: "⟦x ∈ fin1 mr; mr ∈ mrexps3 r⟧ ⟹ x ∈ atoms r"
by (induct r) auto

lemma follow3_mrexps3[simp]: "r ∈ mrexps3 s ⟹ follow3 m r ∈ mrexps3 s"
by (induct s arbitrary: m r) (fastforce simp add: image_iff dest: fin1_atoms)+

lemma empty_mrexp3_mrexps[simp]: "empty_mrexp3 r ∈ mrexps3 r"
by (induct r) (auto simp: image_iff dest: fin1_atoms)

lemma strip3_empty_mrexp3[simp]: "strip3 (empty_mrexp3 r) = empty_mrexp r"
by (induct r) auto

lemma strip3_move3: "ok3 r ⟹ strip3(move3 m r c) = move m (strip3 r) c"
apply(induction r arbitrary: c)
apply (auto simp: disj_commute)
done

lemma nul_empty_mrexp3[simp]: "nul (empty_mrexp3 r) = nullable r"
apply(induction r)
apply auto
done

lemma ok3_empty_mrexp3: "ok3 (empty_mrexp3 r)"
apply(induction r)
apply auto
done

lemma ok3_move3: "ok3 r ⟹ ok3(move3 m r c)"
apply(induction r arbitrary: c)
apply auto
done

lemma nonfin1_empty_mrexp3[simp]: "c ∉ fin1 (empty_mrexp3 r)"
by (induct r) auto

lemma move3_mrexps3[simp]: "r ∈ mrexps3 s ⟹ move3 x r a ∈ mrexps3 s"
by (induct s arbitrary: r x a) (fastforce simp: image_iff dest: fin1_atoms)+

typedef 'a ok_mrexp3 = "{(r :: 'a mrexp3, b :: bool). ok3 r}"
unfolding mem_Collect_eq split_beta by (metis fst_eqD ok3_empty_mrexp3)

setup_lifting type_definition_ok_mrexp3

abbreviation "init_m r ≡ let mr = follow3 True (empty_mrexp3 r) in (mr, nul mr)"

lift_definition init_okm :: "'a rexp ⇒ 'a ok_mrexp3" is init_m
lift_definition delta_okm :: "'a ⇒ 'a ok_mrexp3 ⇒ 'a ok_mrexp3" is
"λa (r, m). (move3 a r False, a ∈ fin1 r)"
unfolding mem_Collect_eq split_beta fst_conv by (intro ok3_move3) simp
lift_definition nullable_okm :: "'a ok_mrexp3 ⇒ bool" is "snd" .
lift_definition lang_okm :: "'a ok_mrexp3 ⇒ 'a lang" is "λ(r, m). L_b (strip3 r, m)" .

instantiation ok_mrexp3 :: (equal) "equal"
begin

fun eq_mrexp3 where
"eq_mrexp3 Zero3 Zero3 = True"
| "eq_mrexp3 One3 One3 = True"
| "eq_mrexp3 (Atom3 m x) (Atom3 m' y) = (m = m' ∧ x = y)"
| "eq_mrexp3 (Plus3 r1 s1 _ _) (Plus3 r3 s3 _ _) = (eq_mrexp3 r1 r3 ∧ eq_mrexp3 s1 s3)"
| "eq_mrexp3 (Times3 r1 s1 _ _) (Times3 r3 s3 _ _) = (eq_mrexp3 r1 r3 ∧ eq_mrexp3 s1 s3)"
| "eq_mrexp3 (Star3 r1 _) (Star3 r3 _) = (eq_mrexp3 r1 r3)"
| "eq_mrexp3 r s = False"

lemma eq_mrexp3_imp_eq: "⟦eq_mrexp3 r s; ok3 r; ok3 s⟧ ⟹ (r = s)"
by (induct rule: eq_mrexp3.induct) auto

lemma eq_mrexp3_refl[simplified, simp]: "r = s ⟹ eq_mrexp3 r s"
by (induct rule: eq_mrexp3.induct) auto

lemma eq_mrexp3_eq: "⟦ok3 r; ok3 s⟧ ⟹ eq_mrexp3 r s = (r = s)"
by (metis eq_mrexp3_imp_eq eq_mrexp3_refl)

lift_definition equal_ok_mrexp3 :: "'a ok_mrexp3 ⇒ 'a ok_mrexp3 ⇒ bool"
is "λ(r1, b1) (r3, b3). b1 = b3 ∧ eq_mrexp3 r1 r3" .

instance by intro_classes (transfer, auto simp: eq_mrexp3_eq)

end

global_interpretation before2: rexp_DFA init_okm delta_okm nullable_okm lang_okm
defines before2_closure = before2.closure
and check_eqv_b2 = before2.check_eqv
and reachable_b2 = before2.reachable
and automaton_b2 = before2.automaton
and match_b2 = before2.match
proof (standard, goal_cases)
case (1 r) show "lang_okm (init_okm r) = lang r"
by transfer (auto simp: split_beta init_a_def nonfinal_empty_mrexp Lm_follow Lm_empty
map_map_rexp nullable_iff ok3_empty_mrexp3)
next
case (2 a br) show "lang_okm (delta_okm a br) = Deriv a (lang_okm br)"
apply transfer
unfolding split_beta fst_conv snd_conv mem_Collect_eq before.L_delta[symmetric] delta_b.simps
by (subst strip3_move3) simp_all
next
case (3 br) show  "nullable_okm br = ([] ∈ lang_okm br)"
next
case (4 s)
have "{fold (λa (r, m). (move3 a r False, a ∈ fin1 r)) w (init_m s) |w. True} ⊆
mrexps3 s × UNIV"
proof (intro subsetI, elim CollectE exE conjE, hypsubst)
fix w show "fold (λa (r, m). (move3 a r False, a ∈ fin1 r)) w (init_m s) ∈
mrexps3 s × UNIV"
by (induct w rule: rev_induct) (auto simp: split: prod.splits intro!: move3_mrexps3)
qed
then show "finite {fold delta_okm w (init_okm s) |w. True}"
by transfer (erule finite_subset[OF subset_trans[rotated]], auto)
qed

(*<*)
end
(*>*)


# Theory Regex_Equivalence

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section ‹Various Algorithms for Regular Expression Equivalence›

(*<*)
theory Regex_Equivalence
imports
Deriv_Autos
Position_Autos
After2
Before2
"HOL-Library.Code_Target_Nat"
"Efficient-Mergesort.Efficient_Sort"
begin
(*>*)

export_code
check_eqv_brz
check_eqv_brzq
check_eqv_n
check_eqv_p
check_eqv_pn
check_eqv_b
check_eqv_b2
check_eqv_a
check_eqv_a2
match_brz
match_brzq
match_n
match_p
match_pn
match_b
match_b2
match_a
match_a2
in SML module_name Rexp

(*<*)
end
(*>*)


# Theory Examples

(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section ‹Some Tests›

(*<*)
theory Examples
imports Regex_Equivalence
begin
(*>*)

section ‹Examples›

(*<*)
text‹Test: ‹B(n) = (One + a + aa + ⋯ + a⇧n⇧-⇧1) (a⇧n)⇧* = a⇧*› (see Asperti)›
(*>*)

fun pow where
"pow 0 = One"
| "pow (Suc 0) = Atom True"
| "pow (Suc n) = Times (Atom True) (pow n)"

fun pow_left where
"pow_left 0 = One"
| "pow_left (Suc 0) = Atom True"
| "pow_left (Suc n) = Times (pow_left n) (Atom True)"

fun Sum where
"Sum f 0 = f 0"
| "Sum f (Suc n) = Plus (f (Suc n)) (Sum f n)"

definition "B n = (Times (Sum pow (n - 1)) (Star (pow n)), Star (Atom True))"
definition "B_left n = (Times (Sum pow_left (n - 1)) (Star (pow_left n)), Star (Atom True))"

definition "seq_left n r = foldr (λr s. Times s r) (replicate n r) One"
definition "seq n r = foldr Times (replicate n r) One"
definition "re_left n = Times (seq_left n (Plus (Atom True) One)) (seq_left n (Atom True))"
definition "re n = Times (seq n (Plus (Atom True) One)) (seq n (Atom True))"
definition "M n = (re_left n, replicate n True)"

lemma "case_prod match_brz (M 128)" by eval
lemma "case_prod match_brzq (M 128)" by eval
lemma "case_prod match_n (M 64)" by eval
lemma "case_prod match_p (M 64)" by eval
lemma "case_prod match_pn (M 64)" by eval
lemma "case_prod match_a (M 512)" by eval
lemma "case_prod match_b (M 512)" by eval
lemma "case_prod match_a2 (M 2048)" by eval
lemma "case_prod match_b2 (M 2048)" by eval

lemma "case_prod check_eqv_brz (B 32)" by eval
lemma "case_prod check_eqv_brzq (B 16)" by eval
lemma "case_prod check_eqv_n (B 256)" by eval
lemma "case_prod check_eqv_p (B 256)" by eval
lemma "case_prod check_eqv_b (B 256)" by eval
lemma "case_prod check_eqv_a (B 256)" by eval
lemma "case_prod check_eqv_b2 (B 256)" by eval
lemma "case_prod check_eqv_a2 (B 256)" by eval

(*<*)
end
(*>*)


# Theory Benchmark

theory Benchmark
imports Regex_Equivalence Spec_Check.Spec_Check
begin

definition bool_checkers :: "(string * (bool rexp ⇒ bool rexp ⇒ bool)) list" where
"bool_checkers = [
(''D '', check_eqv_brz),
⌦‹(''DQ'', check_eqv_brzq),›
(''N '', check_eqv_n),
(''P '', check_eqv_p),
(''PN'', check_eqv_pn),
(''B '', check_eqv_b),
(''B2'', check_eqv_b2),
(''A '', check_eqv_a),
(''A2'', check_eqv_a2)
]"

definition bool_matchers :: "(string * (bool rexp ⇒ bool list ⇒ bool)) list" where
"bool_matchers = [
(''D '', match_brz),
⌦‹(''DQ'', match_brzq),›
(''N '', match_n),
(''P '', match_p),
(''PN'', match_pn),
(''B '', match_b),
(''B2'', match_b2),
(''A '', match_a),
(''A2'', match_a2)
]"

ML ‹
structure Rexp =
struct
val Zero = @{code Zero};
val One = @{code One};
val Atom = @{code Atom};
val Plus = @{code Plus};
val Times = @{code Times};
val Star = @{code Star};
val bool_checkers = @{code bool_checkers};
val bool_matchers = @{code bool_matchers};
end
›

ML ‹

val timeout = Time.fromSeconds 10;
datatype res = Res of bool * Time.time | TO

fun sum [] = Time.fromSeconds 0
| sum (TO :: xs) = timeout + sum xs
| sum (Res (_, t) :: xs) = t + sum xs

fun average xs = Time.fromReal (Time.toReal (sum xs) / real (length xs));

fun time f x =
let
val timer = Timer.startRealTimer ();
val res = Timeout.apply timeout (fn () => uncurry f x) ();
val time = Timer.checkRealTimer timer;
in
Res (res, time)
end handle Timeout.TIMEOUT _ => TO;
›

ML ‹
fun list_n 0 _ r = ([], r)
| list_n n g r =
let
val (x,r) = g r
val (xs,r) = list_n (n - 1) g r
in (x::xs, r) end;
fun join g r =
let val (g', r') = g r;
in g' r' end;

fun regex 0 = Generator.map Rexp.Atom Generator.flip
| regex n =
let
val m = Generator.selectL (0 upto n - 1);
val plus = join (Generator.map (fn m =>
Generator.map2 Rexp.Plus (regex m, regex (n - 1 - m))) m);
val times = join (Generator.map (fn m =>
Generator.map2 Rexp.Times (regex m, regex (n - 1 - m))) m);
val star = join (Generator.map (Generator.map Rexp.Star o regex) (Generator.lift (n - 1)));
in
Generator.chooseL [plus, times, star]
end;
›

(*
ML {*
val checkers = drop 2 Rexp.bool_checkers
val sizes = [50,100,150,200,250];
val regexes = fst (fold_map (fn f => fn r => f r) (map (list_n 100 o regex) sizes)
(Generator.new ()));
*}

declare [[ML_print_depth 100000]]
ML {*
fun alph Rexp.Zero = 0
| alph Rexp.One = 0
| alph (Rexp.Atom _) = 1
| alph (Rexp.Plus (r, s)) = alph r + alph s
| alph (Rexp.Times (r, s)) = alph r + alph s
| alph (Rexp.Star r) = alph r;
map (map alph) regexes
*}
declare [[ML_print_depth 10]]
*)

ML ‹

warning ("n     " ^  space_implode "    " (map (String.implode o fst) checkers))
fun pad i = if i < 10 then 4
else if i < 100 then 3
else if i < 1000 then 2
else if i < 10000 then 1
else 0;
fun round n ts =
warning (string_of_int n ^ implode (replicate (1 + pad n) " ") ^
space_implode " " (map Time.toString ts))

fun run checkers sizes =
let
val regexes = fst (fold_map (fn f => fn r => f r) (map (list_n 100 o regex) sizes)
(Generator.new ()));
val _ = map_index (fn (i, rs) =>
let
val n = nth sizes i;
val ts = map (fn (_, ch) => average (map (fn r => time ch (r, r)) rs)) checkers
in
round n ts
end) regexes;
in
()
end;

fun run_re mk_eq checkers sizes =
let
val _ = map (fn n =>
let
val eq = mk_eq n;
val ts = map (fn (_, ch) => case time ch eq of Res (_, t) => t | TO => timeout) checkers;
in
round n ts
end) sizes;
in
()
end;
›

(*
ML {* run Rexp.bool_checkers [10,20,30,40,50,100] *}
n     D     N     P     PN    B     B2    A     A2
10    0.070 0.000 0.000 0.000 0.000 0.000 0.000 0.000
20    1.401 0.000 0.001 0.000 0.000 0.000 0.000 0.000
30    4.235 0.005 0.002 0.002 0.000 0.000 0.000 0.000
40    5.080 0.089 0.005 0.004 0.000 0.000 0.000 0.000
50    6.916 0.222 0.012 0.010 0.001 0.000 0.001 0.001
100   9.587 2.593 0.137 0.116 0.002 0.002 0.003 0.002
*)

(*
ML {* run (drop 2 Rexp.bool_checkers) [50,100,150,200,250] *}
n     P     PN    B     B2    A     A2
50    0.011 0.009 0.001 0.000 0.001 0.001
100   0.136 0.112 0.002 0.002 0.004 0.003
150   0.635 0.499 0.009 0.008 0.013 0.010
200   2.029 1.744 0.016 0.013 0.025 0.019
250   4.490 3.719 0.028 0.024 0.040 0.030
*)

(*
ML {* run (drop 4 Rexp.bool_checkers) [100,200,300,400,500,600,700,800,900,1000]
n     B     B2    A     A2
100   0.003 0.002 0.005 0.003
200   0.023 0.019 0.033 0.025
300   0.090 0.078 0.119 0.094
400   0.215 0.213 0.278 0.222
500   0.443 0.450 0.555 0.477
600   0.710 0.806 0.948 0.776
700   1.304 1.382 1.575 1.335
800   1.696 1.902 2.151 1.848
900   2.388 2.643 2.878 2.567
1000  2.985 3.280 3.498 3.137
*)

text ‹Asperti's example›

ML ‹
fun pow 0 = Rexp.One
| pow 1 = Rexp.Atom true
| pow n = Rexp.Times (Rexp.Atom true, pow (n - 1));

fun powl 0 = Rexp.One
| powl 1 = Rexp.Atom true
| powl n = Rexp.Times (powl (n - 1), Rexp.Atom true);

fun sum f 0 = f 0
| sum f n = Rexp.Plus (f n, sum f (n - 1));

fun b n = (Rexp.Times (sum pow (n - 1), Rexp.Star (pow n)), Rexp.Star (Rexp.Atom true));
fun bl n = (Rexp.Times (sum powl (n - 1), Rexp.Star (powl n)), Rexp.Star (Rexp.Atom true));

›

(*
ML {* run_re b Rexp.bool_checkers [30,40,50,70,100,200] *}
ML {* run_re bl Rexp.bool_checkers [30,40,50,70,100,200] *}
ML {* run_re b (drop 1 Rexp.bool_checkers) [100,200,300,400,500] *}
ML {* run_re bl (drop 1 Rexp.bool_checkers) [100,200,300,400,500] *}
ML {* run_re b (take 3 (drop 1 Rexp.bool_checkers)) [500,600,700,800] *}
ML {* run_re bl (take 3 (drop 1 Rexp.bool_checkers)) [500,600,700,800] *}
*)
text ‹Fischer's example (matching)›

ML ‹
fun seq n = Library.foldr1 Rexp.Times o replicate n;
fun seql n = Library.foldr1 (Rexp.Times o swap) o replicate n;
fun re n = (Rexp.Times (seq n (Rexp.Plus (Rexp.Atom true, Rexp.One)), seq n (Rexp.Atom true)),
replicate n true);
fun rel n = (Rexp.Times (seql n (Rexp.Plus (Rexp.Atom true, Rexp.One)), seql n (Rexp.Atom true)),
replicate n true);

›

(*
ML {* run_re re Rexp.bool_matchers [30,40,50,70,100] *}
ML {* run_re rel Rexp.bool_matchers [30,40,50,70,100] *}
ML {* run_re re (drop 4 Rexp.bool_matchers) [100,300,500,700,1000,1300,1600,2000,2500,3000,4000,5000] *}
ML {* run_re rel (drop 4 Rexp.bool_matchers) [100,300,500,700,1000,1300,1600,2000,2500,3000,4000,5000] *}
*)
ML ‹
val monster =
curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Times (curry
Rexp.Times Rexp.One (curry Rexp.Plus (Rexp.Atom false) (Rexp.Star (curry
Rexp.Times Rexp.Zero (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus (Rexp.Star
Rexp.Zero) (curry Rexp.Plus Rexp.Zero (Rexp.Star (curry Rexp.Plus Rexp.Zero
(Rexp.Atom false))))) (curry Rexp.Plus Rexp.One (Rexp.Star (curry Rexp.Times
(curry Rexp.Times (Rexp.Atom false) Rexp.Zero) (Rexp.Star Rexp.Zero))))))))))
(curry Rexp.Times (curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus (curry
Rexp.Times (curry Rexp.Times (curry Rexp.Times (Rexp.Atom false) Rexp.One)
Rexp.One) (Rexp.Star (Rexp.Star (curry Rexp.Times Rexp.One Rexp.One))))
Rexp.Zero) (curry Rexp.Times (Rexp.Star (curry Rexp.Times Rexp.One (Rexp.Star
(curry Rexp.Times Rexp.One (Rexp.Star (Rexp.Atom true)))))) (curry Rexp.Times
(Rexp.Star (curry Rexp.Times (curry Rexp.Times Rexp.Zero Rexp.One) Rexp.Zero))
(curry Rexp.Times (curry Rexp.Plus (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus
Rexp.Zero Rexp.Zero) (Rexp.Atom false))) (curry Rexp.Times (curry Rexp.Plus
(curry Rexp.Times (Rexp.Atom false) (Rexp.Atom true)) (Rexp.Star Rexp.Zero))
(curry Rexp.Plus (curry Rexp.Times (Rexp.Atom true) Rexp.One) Rexp.Zero)))
(Rexp.Star (curry Rexp.Plus (Rexp.Star Rexp.One) (curry Rexp.Plus (curry
Rexp.Plus (Rexp.Atom true) Rexp.Zero) (Rexp.Atom true)))))))) (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus Rexp.One (curry Rexp.Times
(curry Rexp.Times (curry Rexp.Times Rexp.One (Rexp.Atom false)) Rexp.One) (curry
Rexp.Plus (curry Rexp.Plus Rexp.One (curry Rexp.Plus Rexp.Zero Rexp.Zero))
(curry Rexp.Times (Rexp.Star Rexp.Zero) (curry Rexp.Times (Rexp.Atom false)
Rexp.Zero))))) (curry Rexp.Plus (Rexp.Star Rexp.Zero) (curry Rexp.Plus Rexp.One
(curry Rexp.Times (Rexp.Atom true) (curry Rexp.Plus Rexp.Zero Rexp.One)))))
(Rexp.Star (curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Times (Rexp.Star
Rexp.Zero) (curry Rexp.Times (curry Rexp.Times Rexp.Zero Rexp.One) Rexp.One))
(Rexp.Atom false)) (curry Rexp.Times (Rexp.Star (curry Rexp.Plus (curry
Rexp.Times Rexp.Zero Rexp.One) Rexp.Zero)) (Rexp.Star (Rexp.Atom false))))))
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus Rexp.One (Rexp.Atom true)) (curry
Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (Rexp.Star (Rexp.Atom true))
(Rexp.Star (Rexp.Star (Rexp.Atom true)))) (curry Rexp.Times Rexp.One (curry
Rexp.Plus Rexp.Zero Rexp.Zero))) Rexp.One))))) (curry Rexp.Plus (Rexp.Star
(curry Rexp.Plus (Rexp.Star (curry Rexp.Plus (curry Rexp.Times (Rexp.Star
(Rexp.Star Rexp.Zero)) (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Times
(Rexp.Atom false) (Rexp.Atom true)) Rexp.One) (Rexp.Star (Rexp.Atom false))))
(curry Rexp.Plus (curry Rexp.Plus Rexp.One (curry Rexp.Plus (curry Rexp.Times
(Rexp.Atom false) Rexp.One) (Rexp.Atom false))) (curry Rexp.Plus (curry
Rexp.Plus (Rexp.Star Rexp.Zero) (Rexp.Atom false)) (Rexp.Star (Rexp.Atom
true)))))) (curry Rexp.Times (Rexp.Star (Rexp.Star (Rexp.Atom true))) (Rexp.Star
(curry Rexp.Plus (Rexp.Star (curry Rexp.Times (Rexp.Atom true) (Rexp.Atom
false))) (curry Rexp.Times (Rexp.Star (Rexp.Star (Rexp.Atom false))) (Rexp.Atom
false))))))) (curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus (Rexp.Star
(Rexp.Star (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus (Rexp.Atom false)
(Rexp.Atom false)) Rexp.Zero)))) Rexp.One) (Rexp.Star (curry Rexp.Times
(Rexp.Star (curry Rexp.Plus Rexp.One (Rexp.Star (Rexp.Star Rexp.One)))) (curry
Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Plus Rexp.Zero
(Rexp.Atom true)) (Rexp.Atom true)) (Rexp.Atom true)) Rexp.Zero)))) Rexp.One))))
(Rexp.Star (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus (Rexp.Star Rexp.One) (Rexp.Atom
true)) (curry Rexp.Times (Rexp.Star Rexp.One) (curry Rexp.Plus (curry Rexp.Times
Rexp.One Rexp.One) (curry Rexp.Plus (curry Rexp.Plus Rexp.One (Rexp.Atom true))
(Rexp.Star (Rexp.Atom true))))))) (curry Rexp.Plus (curry Rexp.Plus (curry
Rexp.Times Rexp.One (Rexp.Star (curry Rexp.Times (curry Rexp.Times (Rexp.Atom
true) Rexp.One) (curry Rexp.Plus Rexp.One Rexp.Zero)))) (curry Rexp.Times (curry
Rexp.Times (Rexp.Atom false) (Rexp.Star Rexp.One)) (curry Rexp.Plus Rexp.One
(curry Rexp.Times (curry Rexp.Times Rexp.One Rexp.One) (curry Rexp.Times
Rexp.Zero Rexp.Zero))))) (curry Rexp.Plus (Rexp.Star (Rexp.Star (Rexp.Atom
false))) (Rexp.Star (Rexp.Star (Rexp.Star (Rexp.Atom false))))))) (curry
Rexp.Plus (curry Rexp.Times (Rexp.Star (Rexp.Star (curry Rexp.Times (curry
Rexp.Plus (curry Rexp.Times (Rexp.Atom true) Rexp.Zero) (Rexp.Star (Rexp.Atom
true))) (curry Rexp.Plus (Rexp.Atom false) (curry Rexp.Plus (Rexp.Atom true)
Rexp.One))))) (curry Rexp.Times (curry Rexp.Plus (Rexp.Star Rexp.One) (curry
Rexp.Plus (curry Rexp.Plus Rexp.One Rexp.Zero) (curry Rexp.Times Rexp.One (curry
Rexp.Plus (Rexp.Atom false) Rexp.One)))) (curry Rexp.Times (curry Rexp.Plus
(curry Rexp.Plus (curry Rexp.Plus (Rexp.Atom false) Rexp.One) (curry Rexp.Plus
(Rexp.Atom true) (Rexp.Atom false))) Rexp.Zero) (curry Rexp.Plus (curry
Rexp.Times Rexp.Zero (curry Rexp.Times Rexp.One (Rexp.Atom true))) (curry
Rexp.Plus (Rexp.Star Rexp.Zero) (curry Rexp.Plus (Rexp.Atom false)
Rexp.Zero)))))) (curry Rexp.Plus (Rexp.Star (curry Rexp.Times (curry Rexp.Times
(Rexp.Star (Rexp.Star Rexp.Zero)) (curry Rexp.Times (curry Rexp.Plus Rexp.Zero
(Rexp.Atom false)) (curry Rexp.Times Rexp.Zero Rexp.Zero))) (curry Rexp.Times
(curry Rexp.Plus (Rexp.Star Rexp.Zero) (Rexp.Atom false)) (curry Rexp.Plus
(curry Rexp.Plus Rexp.One Rexp.Zero) Rexp.One)))) (curry Rexp.Plus Rexp.One
(curry Rexp.Plus (curry Rexp.Times (Rexp.Star (curry Rexp.Times Rexp.One
Rexp.Zero)) (Rexp.Atom true)) (curry Rexp.Plus (Rexp.Star (Rexp.Atom true))
(curry Rexp.Plus Rexp.Zero (curry Rexp.Times Rexp.One Rexp.One)))))))) (curry
Rexp.Plus (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (Rexp.Star
(Rexp.Star (curry Rexp.Plus (curry Rexp.Times Rexp.Zero (Rexp.Atom true))
(Rexp.Star (Rexp.Atom false))))) (curry Rexp.Plus Rexp.One (curry Rexp.Plus
(Rexp.Star Rexp.One) (Rexp.Atom true)))) (curry Rexp.Times (curry Rexp.Times
(Rexp.Star (Rexp.Star (Rexp.Atom true))) (Rexp.Atom false)) (Rexp.Star (curry
Rexp.Times (curry Rexp.Plus Rexp.One Rexp.One) (curry Rexp.Times (Rexp.Star
Rexp.One) (Rexp.Star Rexp.One)))))) (curry Rexp.Times (Rexp.Star Rexp.Zero)
Rexp.One)) (curry Rexp.Times (Rexp.Star (curry Rexp.Times (Rexp.Star (Rexp.Star
(Rexp.Star (curry Rexp.Times Rexp.One Rexp.One)))) (Rexp.Star (Rexp.Star
Rexp.One)))) (curry Rexp.Times (curry Rexp.Plus (Rexp.Star (Rexp.Atom false))
(curry Rexp.Plus (curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus Rexp.One
(Rexp.Atom false)) Rexp.Zero) Rexp.Zero) Rexp.One)) (Rexp.Star (Rexp.Star (curry
Rexp.Plus (Rexp.Star (curry Rexp.Times (Rexp.Atom true) Rexp.One)) (Rexp.Star
(Rexp.Atom true))))))))) (curry Rexp.Plus (Rexp.Star (Rexp.Star (curry
Rexp.Times (curry Rexp.Plus (Rexp.Star (Rexp.Star Rexp.One)) (Rexp.Star
(Rexp.Star (Rexp.Star Rexp.Zero)))) (Rexp.Atom true)))) (Rexp.Atom false)))))
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus (Rexp.Star (curry Rexp.Times
(curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times
(Rexp.Star (curry Rexp.Times (Rexp.Star Rexp.Zero) (curry Rexp.Times Rexp.Zero
Rexp.Zero))) (curry Rexp.Plus (curry Rexp.Times Rexp.Zero Rexp.Zero) (Rexp.Star
Rexp.Zero))) Rexp.One) (Rexp.Star (Rexp.Star (Rexp.Atom true)))) Rexp.Zero)
(curry Rexp.Times (Rexp.Star (curry Rexp.Times Rexp.Zero (Rexp.Star (Rexp.Star
(curry Rexp.Plus Rexp.One (Rexp.Star Rexp.Zero)))))) (curry Rexp.Times (curry
Rexp.Plus (curry Rexp.Times Rexp.One Rexp.One) (Rexp.Star Rexp.One)) (curry
Rexp.Plus Rexp.One (curry Rexp.Times (Rexp.Atom true) (Rexp.Atom false)))))))
(curry Rexp.Times (Rexp.Star (Rexp.Star (Rexp.Star (curry Rexp.Plus (curry
Rexp.Plus (curry Rexp.Plus Rexp.One (Rexp.Star (Rexp.Atom true))) (curry
Rexp.Plus (curry Rexp.Times Rexp.Zero Rexp.Zero) (Rexp.Star Rexp.Zero))) (curry
Rexp.Plus (curry Rexp.Times (curry Rexp.Times Rexp.Zero Rexp.One) (curry
Rexp.Plus Rexp.One (Rexp.Atom false))) (Rexp.Star Rexp.One)))))) (Rexp.Star
(curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (Rexp.Star (Rexp.Star
(Rexp.Atom true))) (curry Rexp.Plus (curry Rexp.Plus Rexp.Zero (curry Rexp.Plus
Rexp.Zero Rexp.One)) (curry Rexp.Times (Rexp.Atom true) Rexp.One))) (Rexp.Star
(curry Rexp.Plus Rexp.One (curry Rexp.Times (Rexp.Atom true) (curry Rexp.Plus
Rexp.One (Rexp.Star Rexp.Zero)))))) (curry Rexp.Times Rexp.Zero (Rexp.Star
(Rexp.Star (curry Rexp.Times Rexp.Zero (curry Rexp.Times (Rexp.Atom false)
(curry Rexp.Times (Rexp.Atom true) (Rexp.Atom true))))))))))) (curry Rexp.Times
(curry Rexp.Plus Rexp.Zero (Rexp.Star (Rexp.Star (curry Rexp.Times (Rexp.Atom
false) (curry Rexp.Plus (curry Rexp.Plus (Rexp.Star (Rexp.Atom true)) (Rexp.Star
(curry Rexp.Times (curry Rexp.Times Rexp.Zero Rexp.One) (Rexp.Atom false))))
(Rexp.Star (curry Rexp.Plus (Rexp.Atom true) (curry Rexp.Times (curry Rexp.Times
Rexp.Zero Rexp.Zero) (Rexp.Star (Rexp.Atom false)))))))))) (curry Rexp.Times
(curry Rexp.Times (Rexp.Star (curry Rexp.Plus (curry Rexp.Times (curry
Rexp.Times (curry Rexp.Plus (curry Rexp.Times Rexp.Zero (Rexp.Star Rexp.One))
(curry Rexp.Plus Rexp.One Rexp.Zero)) (curry Rexp.Plus (curry Rexp.Plus (curry
Rexp.Plus Rexp.One (Rexp.Atom false)) (curry Rexp.Plus Rexp.Zero Rexp.Zero))
Rexp.One)) Rexp.One) (Rexp.Star (curry Rexp.Times (Rexp.Star Rexp.Zero)
(Rexp.Star (curry Rexp.Plus (Rexp.Atom true) Rexp.Zero)))))) (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Times (Rexp.Atom false) (Rexp.Star (Rexp.Star
(Rexp.Star Rexp.Zero)))) (curry Rexp.Plus (Rexp.Star (curry Rexp.Plus Rexp.Zero
Rexp.Zero)) (curry Rexp.Plus (Rexp.Atom false) (curry Rexp.Plus (Rexp.Star
(curry Rexp.Plus Rexp.One (Rexp.Atom true))) (curry Rexp.Plus (curry Rexp.Times
(Rexp.Atom true) Rexp.Zero) Rexp.One))))) (curry Rexp.Times (curry Rexp.Plus
(curry Rexp.Plus Rexp.Zero (Rexp.Star (curry Rexp.Times (Rexp.Atom false) (curry
Rexp.Plus Rexp.Zero Rexp.One)))) (curry Rexp.Times (curry Rexp.Times (curry
Rexp.Plus (Rexp.Star Rexp.Zero) (curry Rexp.Times Rexp.Zero (Rexp.Atom false)))
(curry Rexp.Plus Rexp.Zero Rexp.One)) Rexp.Zero)) (curry Rexp.Plus (Rexp.Star
(curry Rexp.Times Rexp.Zero (curry Rexp.Plus Rexp.Zero Rexp.Zero))) (Rexp.Star
Rexp.One))))) (curry Rexp.Times (Rexp.Star (curry Rexp.Plus (Rexp.Star Rexp.One)
(curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times (curry
Rexp.Times (Rexp.Atom false) (Rexp.Atom false)) (Rexp.Atom true)) (curry
Rexp.Times (Rexp.Atom true) (curry Rexp.Times Rexp.Zero (Rexp.Atom true))))
Rexp.One) (curry Rexp.Times (curry Rexp.Times (Rexp.Atom true) (Rexp.Star
Rexp.Zero)) Rexp.Zero)))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times (Rexp.Atom
false) Rexp.Zero) Rexp.Zero) (Rexp.Star (Rexp.Star Rexp.One)))) (curry Rexp.Plus
(curry Rexp.Plus (Rexp.Star Rexp.Zero) Rexp.One) Rexp.One)) (Rexp.Star (curry
Rexp.Plus (curry Rexp.Plus (Rexp.Atom false) (curry Rexp.Plus Rexp.Zero (curry
Rexp.Plus Rexp.One (Rexp.Atom false)))) (curry Rexp.Plus (curry Rexp.Times
(curry Rexp.Plus Rexp.Zero (Rexp.Atom true)) (curry Rexp.Times (Rexp.Atom true)
Rexp.One)) (curry Rexp.Plus (curry Rexp.Plus Rexp.One Rexp.One) (Rexp.Atom
true)))))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (Rexp.Atom false)
(Rexp.Star (Rexp.Star (curry Rexp.Times Rexp.Zero Rexp.One)))) Rexp.Zero)
Rexp.Zero)))))))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (Rexp.Atom
false) (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Plus (Rexp.Star Rexp.One) (Rexp.Star Rexp.Zero))
(curry Rexp.Times Rexp.Zero (Rexp.Atom false))) (curry Rexp.Times (Rexp.Star
(Rexp.Star (Rexp.Atom false))) Rexp.One)) Rexp.One) (curry Rexp.Plus (Rexp.Star
(curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus Rexp.One (curry Rexp.Plus
Rexp.One (Rexp.Atom false))) Rexp.One) (curry Rexp.Times (curry Rexp.Plus
Rexp.One Rexp.One) (Rexp.Star (curry Rexp.Times (curry Rexp.Plus (Rexp.Star
Rexp.Zero) (curry Rexp.Times (Rexp.Atom true) (Rexp.Atom true))) Rexp.Zero)))))
(curry Rexp.Plus Rexp.One (curry Rexp.Times (curry Rexp.Times (curry Rexp.Plus
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus Rexp.One (Rexp.Atom true))
Rexp.One)) (Rexp.Star (Rexp.Star Rexp.Zero))) Rexp.Zero) (Rexp.Star (curry
Rexp.Plus Rexp.Zero (Rexp.Star (curry Rexp.Times (curry Rexp.Times (Rexp.Atom
false) Rexp.Zero) (curry Rexp.Times Rexp.Zero Rexp.Zero))))))))) (curry
Rexp.Times (curry Rexp.Times (curry Rexp.Times (curry Rexp.Times Rexp.One
(Rexp.Star (curry Rexp.Plus (curry Rexp.Times (Rexp.Star (curry Rexp.Plus
(Rexp.Atom false) Rexp.Zero)) Rexp.One) (curry Rexp.Times (curry Rexp.Plus
(Rexp.Atom true) (curry Rexp.Times (Rexp.Atom true) Rexp.One)) (Rexp.Atom
false))))) (curry Rexp.Times (Rexp.Star (Rexp.Star (curry Rexp.Plus (curry
Rexp.Plus (Rexp.Star (Rexp.Atom false)) Rexp.Zero) Rexp.One))) (Rexp.Star (curry
Rexp.Plus (curry Rexp.Plus Rexp.One (curry Rexp.Times (curry Rexp.Plus
(Rexp.Atom true) (Rexp.Atom true)) (curry Rexp.Times Rexp.One (Rexp.Atom
true)))) (curry Rexp.Plus (Rexp.Atom true) (curry Rexp.Times Rexp.One (curry
Rexp.Plus (Rexp.Atom true) Rexp.One))))))) (curry Rexp.Times (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Plus (Rexp.Star (Rexp.Star (Rexp.Atom false)))
(Rexp.Star (curry Rexp.Times Rexp.One (Rexp.Star (Rexp.Atom true))))) (Rexp.Star
(Rexp.Atom true))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (curry
Rexp.Plus Rexp.One (curry Rexp.Times Rexp.One Rexp.One)) (Rexp.Atom false))
(Rexp.Atom false)) (curry Rexp.Times (Rexp.Star (Rexp.Star Rexp.One)) (Rexp.Star
(curry Rexp.Times (Rexp.Star Rexp.One) Rexp.One))))) (curry Rexp.Times
(Rexp.Atom false) (Rexp.Atom false)))) (Rexp.Star (curry Rexp.Plus (curry
Rexp.Times (curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Times Rexp.One (curry
Rexp.Times Rexp.Zero (Rexp.Atom false))) (Rexp.Star (Rexp.Star (Rexp.Atom
true)))) (Rexp.Star (curry Rexp.Times (curry Rexp.Plus (Rexp.Star (Rexp.Atom
true)) (curry Rexp.Plus Rexp.One Rexp.Zero)) Rexp.Zero))) (Rexp.Star (curry
Rexp.Plus Rexp.Zero (Rexp.Atom false)))) (curry Rexp.Times (curry Rexp.Times
(Rexp.Star (Rexp.Star (Rexp.Atom false))) (Rexp.Star Rexp.Zero)) (curry
Rexp.Plus (curry Rexp.Plus (Rexp.Star (Rexp.Star Rexp.One)) Rexp.One) (Rexp.Star
(curry Rexp.Plus (curry Rexp.Plus (Rexp.Atom false) Rexp.One) (curry Rexp.Plus
(Rexp.Star (Rexp.Atom true)) (curry Rexp.Plus Rexp.One Rexp.Zero)))))))))))
(Rexp.Star (curry Rexp.Times (Rexp.Atom false) (Rexp.Star (curry Rexp.Plus
(Rexp.Star (curry Rexp.Times Rexp.Zero (curry Rexp.Times (Rexp.Star (curry
Rexp.Plus (curry Rexp.Plus (curry Rexp.Times Rexp.One Rexp.Zero) (curry
Rexp.Plus Rexp.Zero Rexp.One)) (curry Rexp.Times (curry Rexp.Plus Rexp.One
Rexp.Zero) (curry Rexp.Plus Rexp.Zero Rexp.Zero)))) (Rexp.Star (curry Rexp.Times
(curry Rexp.Plus (curry Rexp.Plus Rexp.Zero Rexp.Zero) (curry Rexp.Times
(Rexp.Atom true) (Rexp.Atom true))) (curry Rexp.Times (curry Rexp.Plus
(Rexp.Atom true) Rexp.One) Rexp.Zero)))))) (curry Rexp.Times Rexp.One (curry
Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times Rexp.One (curry
Rexp.Times (Rexp.Atom true) (Rexp.Atom true))) (Rexp.Star Rexp.One)) (curry
Rexp.Times Rexp.One (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus Rexp.Zero
Rexp.One) (Rexp.Star Rexp.Zero))))) (curry Rexp.Times (curry Rexp.Times
Rexp.Zero (curry Rexp.Times Rexp.One (curry Rexp.Plus (curry Rexp.Times
(Rexp.Atom true) (Rexp.Atom false)) (Rexp.Atom false)))) (curry Rexp.Times
(Rexp.Star (curry Rexp.Times (curry Rexp.Times (Rexp.Atom true) (Rexp.Atom
false)) (curry Rexp.Times (Rexp.Atom true) Rexp.Zero))) (curry Rexp.Times
Rexp.Zero Rexp.One)))))))))) (curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Plus
Rexp.Zero (curry Rexp.Times (Rexp.Star Rexp.One) (curry Rexp.Times (Rexp.Star
(curry Rexp.Times (Rexp.Star Rexp.Zero) (Rexp.Atom true))) (Rexp.Star (curry
Rexp.Plus (Rexp.Atom true) (curry Rexp.Times (Rexp.Atom true) (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Plus (Rexp.Atom false) Rexp.Zero) (curry
Rexp.Times Rexp.One (Rexp.Atom true))) (Rexp.Star (curry Rexp.Times (curry
Rexp.Times (Rexp.Atom false) (Rexp.Atom false)) Rexp.Zero))))))))) (curry
Rexp.Times (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times (Rexp.Star
(curry Rexp.Plus (Rexp.Star (Rexp.Star (curry Rexp.Plus (Rexp.Atom false)
(Rexp.Star Rexp.One)))) (curry Rexp.Plus (Rexp.Atom true) (curry Rexp.Times
(Rexp.Star Rexp.Zero) (Rexp.Atom false))))) (Rexp.Atom true)) (curry Rexp.Times
(curry Rexp.Plus (curry Rexp.Plus Rexp.One (Rexp.Star (Rexp.Star Rexp.One)))
(curry Rexp.Plus (Rexp.Star (curry Rexp.Times (curry Rexp.Times (curry
Rexp.Times Rexp.One Rexp.One) (Rexp.Atom false)) (Rexp.Star (Rexp.Atom true))))
(Rexp.Atom false))) Rexp.One)) (curry Rexp.Times (curry Rexp.Times (curry
Rexp.Plus (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times
Rexp.One (curry Rexp.Times (Rexp.Atom false) (Rexp.Atom false))) (Rexp.Star
(Rexp.Star Rexp.Zero))) (Rexp.Star (curry Rexp.Times (Rexp.Atom true)
Rexp.Zero))) (curry Rexp.Plus (Rexp.Star Rexp.Zero) (curry Rexp.Times (Rexp.Star
Rexp.Zero) Rexp.Zero))) (Rexp.Star (curry Rexp.Plus Rexp.One (curry Rexp.Times
Rexp.One (curry Rexp.Plus (Rexp.Atom true) (Rexp.Atom true)))))) (curry
Rexp.Plus (Rexp.Star (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Times (curry
Rexp.Plus Rexp.Zero Rexp.Zero) (Rexp.Atom false)) Rexp.Zero) (Rexp.Atom false)))
(curry Rexp.Times (curry Rexp.Times Rexp.Zero (Rexp.Star (Rexp.Star (Rexp.Atom
true)))) (curry Rexp.Plus (curry Rexp.Times (curry Rexp.Times Rexp.One Rexp.One)
(Rexp.Star Rexp.Zero)) (Rexp.Star (curry Rexp.Plus (Rexp.Atom true)
Rexp.One)))))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times (Rexp.Star
(curry Rexp.Plus (curry Rexp.Plus Rexp.Zero (Rexp.Atom true)) Rexp.Zero))
Rexp.Zero) (Rexp.Star (curry Rexp.Plus (Rexp.Star (curry Rexp.Times (curry
Rexp.Plus Rexp.Zero (Rexp.Atom true)) (Rexp.Star Rexp.One))) Rexp.One)))
Rexp.Zero))) (curry Rexp.Plus (curry Rexp.Plus (curry Rexp.Plus (Rexp.Star
(curry Rexp.Times (Rexp.Star (curry Rexp.Times (curry Rexp.Plus Rexp.Zero
Rexp.One) (curry Rexp.Times (curry Rexp.Plus Rexp.Zero Rexp.One) (Rexp.Atom
true)))) (curry Rexp.Times (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus Rexp.One
(Rexp.Atom false)) (curry Rexp.Plus Rexp.Zero (Rexp.Atom true)))) (Rexp.Star
(Rexp.Star Rexp.Zero))))) (curry Rexp.Times Rexp.Zero (curry Rexp.Times Rexp.One
Rexp.Zero))) (curry Rexp.Times (curry Rexp.Times (curry Rexp.Times (Rexp.Star
(curry Rexp.Plus (curry Rexp.Plus (Rexp.Star Rexp.Zero) Rexp.Zero) (Rexp.Atom
true))) (curry Rexp.Times (Rexp.Star (Rexp.Atom true)) Rexp.One)) (curry
Rexp.Times (curry Rexp.Times (curry Rexp.Times (Rexp.Star (Rexp.Star (Rexp.Atom
false))) (curry Rexp.Times (curry Rexp.Times (Rexp.Atom true) (Rexp.Atom false))
(Rexp.Atom true))) (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Plus
(Rexp.Atom true) Rexp.One) Rexp.Zero) (curry Rexp.Times Rexp.One Rexp.Zero)))
(Rexp.Star Rexp.Zero))) (curry Rexp.Plus (Rexp.Star (Rexp.Atom false))
(Rexp.Star (curry Rexp.Times (curry Rexp.Plus (curry Rexp.Times Rexp.One (curry
Rexp.Plus (Rexp.Atom false) Rexp.Zero)) Rexp.Zero) (curry Rexp.Plus (curry
Rexp.Times Rexp.One (Rexp.Atom false)) (Rexp.Atom true))))))) (curry Rexp.Times
(Rexp.Star (Rexp.Atom false)) (Rexp.Star (curry Rexp.Times (Rexp.Star (Rexp.Atom
true)) (curry Rexp.Plus (Rexp.Star (curry Rexp.Plus (Rexp.Star (curry Rexp.Times
Rexp.One (Rexp.Atom false))) (curry Rexp.Plus Rexp.One (curry Rexp.Times
Rexp.One Rexp.Zero)))) (Rexp.Star (Rexp.Star (curry Rexp.Times (Rexp.Atom false)
(Rexp.Star Rexp.Zero))))))))))) (Rexp.Star (curry Rexp.Plus (curry Rexp.Plus
(curry Rexp.Times (curry Rexp.Plus (Rexp.Star (curry Rexp.Times (curry
Rexp.Times (Rexp.Atom false) (Rexp.Star (curry Rexp.Plus (Rexp.Star Rexp.Zero)
(curry Rexp.Times Rexp.Zero (Rexp.Atom false))))) (curry Rexp.Times (curry
Rexp.Times Rexp.One (curry Rexp.Plus (Rexp.Star Rexp.Zero) (curry Rexp.Plus
Rexp.Zero Rexp.One))) Rexp.One))) (Rexp.Atom true)) Rexp.Zero) (Rexp.Star (curry
Rexp.Plus (Rexp.Star (curry Rexp.Times (curry Rexp.Times (Rexp.Atom false)
(curry Rexp.Plus (Rexp.Star (curry Rexp.Times Rexp.Zero (Rexp.Atom false)))
Rexp.Zero)) (curry Rexp.Times (Rexp.Star Rexp.Zero) (curry Rexp.Times Rexp.Zero
(Rexp.Star (curry Rexp.Times (Rexp.Atom false) Rexp.One)))))) (curry Rexp.Plus
Rexp.One (curry Rexp.Times (curry Rexp.Plus (Rexp.Star (curry Rexp.Times (curry
Rexp.Times Rexp.One Rexp.Zero) (Rexp.Star Rexp.One))) (curry Rexp.Plus (curry
Rexp.Plus (Rexp.Atom true) (Rexp.Star Rexp.Zero)) Rexp.Zero)) (Rexp.Star (curry
Rexp.Plus Rexp.One (curry Rexp.Plus (curry Rexp.Times Rexp.Zero Rexp.One) (curry
Rexp.Plus (Rexp.Atom true) (Rexp.Atom false)))))))))) (Rexp.Star (Rexp.Star
(Rexp.Star (Rexp.Star (Rexp.Atom true)))))))));
›

(*
ML {* run_re (K (monster, monster)) Rexp.bool_checkers [1] *}
*)

ML ‹
fun runTO checker sizes =
let
val regexes = fst (fold_map (fn f => fn r => f r) (map (list_n 1000 o regex) sizes)
(Generator.new ()));
val _ = map (fn rs =>
let
fun print (TO, i) = (warning (@{make_string} (nth rs i)); TO)
| print (t, i) = (warning (string_of_int i); t);
val ts = map_index (fn (i, r) => print (time (snd checker) (r, r), i)) rs
val _ = warning (String.implode (fst checker))
in
warning (Time.toString (average ts))
end) regexes;
in
()
end;
›

ML ‹local open Rexp in

val evil =

Star (Star (Star (Times (Times (Star (Star (Atom false)), Plus (Star (Star (Plus (Times (Atom
false, Plus (Atom false, Atom true)), Times (Times (Times (Atom false, Plus (Atom true, Atom
false)), Times (Atom true, Atom false)), Times (Star (Times (Times (Atom true, Atom false), Atom
true)), Atom false))))), Times (Times (Plus (Atom false, Plus (Atom true, Atom true)), Atom true),
Star (Plus (Atom false, Atom true))))), Plus (Atom false, Star (Atom false))))))

end
›
(*
ML {* snd (nth Rexp.bool_checkers 1) evil evil *}

ML {*
runTO (nth Rexp.bool_checkers 1) [28]
*}
*)

end
`