Session Regex_Equivalence

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 Zero = id"
| "add_atoms One = id"
| "add_atoms (Atom a) = List.insert a"
| "add_atoms (Plus r s) = add_atoms s o add_atoms r"
| "add_atoms (Times r s) = add_atoms s o add_atoms r"
| "add_atoms (Star r) = add_atoms r"

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 "xset 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 "xset 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. wlists (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 =
  (let as = add_atoms r (add_atoms 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 -
  let ?as = "add_atoms r (add_atoms s [])"
  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]
  show "lang r = lang s" by (simp add: set_add_atoms)
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 -
  let ?as = "add_atoms r (add_atoms s [])"
  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
  show "check_eqv r s" by (simp add: check_eqv_def set_add_atoms)
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 = (rtoplevel_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»"]
   by(simp add: atoms_flatten_PLUS ball_Un Un_commute)
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 = (rtoplevel_summands s. lang r)"
by (induct s) auto

lemma toplevel_summands_in_lang:
  "w  lang s = (rtoplevel_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)) = (aset 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) = (stoplevel_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:
  "(atoplevel_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
   by (simp add: image_UN)
qed (auto simp: Let_def)


lemma toplevel_summands_nullable:
  "nullable s = (rtoplevel_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)
qed (simp_all add: ACI_norm_nullable)

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]
    by (auto simp add: toplevel_summands_ACI_nPlus)
      (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 add: 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»"
   by (simp add: ACI_decidable)
lift_definition less_ACI_rexp :: "'a ACI_rexp  'a ACI_rexp  bool" is "λr s. less «r» «s»"
   by (simp add: ACI_decidable)
lift_definition equal_ACI_rexp :: "'a ACI_rexp  'a ACI_rexp  bool" is "λr s. «r» = «s»"
   by (simp add: ACI_decidable)
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. pP. 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 (Plus r s) = Plus (follow m r) (follow m s)" |
"follow m (Times r s) =
  Times (follow m r) (follow (final r  m  nullable r) s)" |
"follow m (Star r) = Star(follow (final r  m) r)"

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

lemma strip_read[simp]: "strip (read a r) = strip r"
by (simp add: map_map_rexp split_def)

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
    by (simp add: Un_Diff conc_Un_distrib
          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

lemma final_read_Lm: "final(read a r)  [a]  Lm r"
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"
    by(auto simp add: init_b_def Lm_follow Lm_empty map_map_rexp nullable_iff)
next
  case (2 a rb) show "L_b (delta_b a rb) = Deriv a (L_b rb)"
    by (cases rb) (auto simp add: Deriv_def final_read_Lm image_def Lm_read Lm_follow)
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
Glushkov and McNaughton/Yamada construction.›

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
"delta_a a (b,r) = (False, read a (follow b r))"

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)"
    by (cases br) (simp add: Deriv_def final_read_Lm Lm_read Lm_follow,
      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)"

lemma shift_read_follow: "shift m r x = read x (follow m r)"
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))"

lemma nullable_read[simp]: "nullable (read c r) = nullable r"
by (induction r) auto

lemma final_read_final1: "final (read c r) = final1 r c"
by (induction r) auto

lemma move_follow_read: "move c r m = follow m (read c r)"
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
      shift_read_follow[symmetric]
    by (subst strip2_shift2) simp_all
next
  case (3 br) show  "nullable_okm br = ([]  lang_okm br)"
    by transfer (simp add: split_beta)
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
  by (simp add: ok3_empty_mrexp3)
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
      move_follow_read[symmetric] final_read_final1 Let_def
    by (subst strip3_move3) simp_all
next
  case (3 br) show  "nullable_okm br = ([]  lang_okm br)"
    by transfer (simp add: split_beta)
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 + ⋯ + an-1) (an)* = 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 fun header checkers =
  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 _ = header checkers;
    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 _ = header checkers;
    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