# Theory Automaton

```(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section "Regular Expressions Equivalence Framework"

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

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

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

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

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

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

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

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

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

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

subsection ‹The overall procedure›

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

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

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

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

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

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

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

end

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

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

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

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

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

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

end

(*<*)
end
(*>*)
```