Theory Finite_Automata_Not_HF
theory Finite_Automata_Not_HF
imports Finite_Automata_HF.Finite_Automata_HF
begin
text‹This file contains a version of the dfa and nfa definition from
Lawrence C. Paulson's ‹Finite_Automata_Hf› but with ‹'b set› as states set,
instead of forcing ‹hf set›.
It is intended to be used for easier constructions of explicitly given languages,
not for abstract constructions such as the intersection of 2 automaton languages.
The locale below adds a converter from this dfa/nfa to the hf version dfa/nfa,
to show that regularity also holds for the language of this dfa/nfa.›
lemma embed_finite_set_into_hf:
fixes B::‹'b set›
assumes ‹finite B›
shows ‹∃(f:: 'b ⇒ hf). inj_on f B ›
by (meson assms comp_inj_on finite_imp_inj_to_nat_seg inj_ord_of)
section‹Deterministic Finite Automata›
text‹First, the record for DFAs›
record ('a, 'b) dfa' =
states :: "'b set"
init :: "'b"
final :: "'b set"
nxt :: "'b ⇒ 'a ⇒ 'b"
locale dfa' =
fixes M :: "('a, 'b) dfa'"
assumes init [simp]: "init M ∈ states M"
and final: "final M ⊆ states M"
and nxt[simp]: "⋀q x. q ∈ states M ⟹ nxt M q x ∈ states M"
and finite: "finite (states M)"
begin
text‹Transition function for a given starting state and word.›
primrec nextl :: "['b, 'a list] ⇒ 'b" where
"nextl q [] = q"
| "nextl q (x#xs) = nextl (nxt M q x) xs"
definition language :: "'a list set" where
"language ≡ {xs. nextl (init M) xs ∈ final M}"
lemma nextl_app: "nextl q (xs@ys) = nextl (nextl q xs) ys"
by (induct xs arbitrary: q) auto
lemma nextl_snoc [simp]: "nextl q (xs@[x]) = nxt M (nextl q xs) x"
by (simp add: nextl_app)
definition f :: "'b ⇒ hf" where
"f = (SOME f. inj_on f (states M))"
lemma f_inj_on: "inj_on f (states M)"
unfolding f_def using embed_finite_set_into_hf[OF finite]
by (metis someI_ex)
abbreviation f_inv :: "hf ⇒ 'b" where
‹f_inv ≡ the_inv_into (states M) f›
abbreviation f_M :: "'a dfa" where
‹f_M ≡ ⦇dfa.states = f ` (states M),
init = f (init M),
final = f ` (final M),
nxt = λq x. f( nxt M (f_inv q) x) ⦈›
lemma f_f_inv[simp]: ‹h ∈ dfa.states f_M ⟹ f (f_inv h) = h›
by (simp add: f_inj_on f_the_inv_into_f)
lemma f_in_final: ‹q ∈ dfa'.final M ⟹ f q ∈ dfa.final f_M›
by simp
lemma f_inv_f[simp]: ‹q ∈ dfa'.states M ⟹ f_inv (f q) = q›
by (meson f_inj_on the_inv_into_f_f)
lemma f_inv_in: ‹h ∈ dfa.states f_M ⟹ f_inv h ∈ dfa'.states M›
by fastforce
lemma f_inv_in_final: ‹h ∈ dfa.final f_M ⟹ f_inv h ∈ dfa'.final M›
using final by auto
lemma f_inv_f_init: ‹f_inv( f( dfa'.init M) ) = dfa'.init M›
by (simp add: dfa'.init)
interpretation f_M: dfa f_M
proof(standard, goal_cases)
case 1
then show ?case using dfa'.init by auto
next
case 2
then show ?case by (simp add: final image_mono)
next
case (3 q x)
then show ?case by (simp add: f_inv_in)
next
case 4
then show ?case by (simp add: finite)
qed
lemma nxt_M_f_inv: ‹h ∈ dfa.states f_M ⟹ dfa'.nxt M (f_inv h) x = f_inv (dfa.nxt f_M h x)›
by (simp add: f_inv_in)
lemma nextl_M_f_inv: ‹h ∈ dfa.states f_M ⟹ nextl (f_inv h) xs = f_inv (f_M.nextl h xs)›
proof(induction xs arbitrary: h)
case Nil
then show ?case by simp
next
case (Cons a xs)
then have ‹nextl (dfa'.nxt M (f_inv h) a) xs = f_inv (f_M.nextl (f (dfa'.nxt M (f_inv h) a)) xs)›
using f_f_inv f_M.nxt nxt_M_f_inv by presburger
then show ?case by simp
qed
lemma nextl_f_M_f: ‹q ∈ dfa'.states M ⟹ f_M.nextl (f q) xs = f (nextl q xs)›
proof(induction xs arbitrary: q)
case Nil
then show ?case by simp
next
case (Cons a xs)
then have ‹f_M.nextl (f (dfa'.nxt M q a)) xs = f (nextl (dfa'.nxt M q a) xs)›
using nxt by blast
then show ?case by (simp add: Cons.prems)
qed
lemma M_lang_eq_f_M_lang: ‹language = f_M.language›
unfolding language_def f_M.language_def
by (metis dfa.select_convs(2) f_M.init f_in_final f_inv_f_init f_inv_in_final init nextl_M_f_inv
nextl_f_M_f)
corollary ex_hf_M:
‹∃f_M. dfa f_M ∧ dfa'.language M = dfa.language f_M›
using M_lang_eq_f_M_lang f_M.dfa_axioms by blast
text‹Now we have the result, that our dfas also produce regular languages.›
corollary regular:
assumes "dfa'.language M = L"
shows ‹regular L›
using ex_hf_M assms unfolding regular_def by blast
end
section‹Non-Deterministic Finite Automata›
text‹These NFAs may include epsilon-transitions and multiple start states.›
subsection‹Basic Definitions›
record ('a, 'b) nfa' =
states :: "'b set"
init :: "'b set"
final :: "'b set"
nxt :: "'b ⇒ 'a ⇒ 'b set"
eps :: "('b * 'b) set"
locale nfa' =
fixes M :: "('a, 'b) nfa'"
assumes init: "init M ⊆ states M"
and final: "final M ⊆ states M"
and finite: "finite (states M)"
begin
definition epsclo :: "'b set ⇒ 'b set" where
"epsclo Q ≡ states M ∩ (⋃q∈Q. {q'. (q,q') ∈ (eps M)⇧*})"
lemma epsclo_idem: "epsclo (epsclo Q) = epsclo Q"
by (auto simp: epsclo_def)
lemma epsclo_increasing: "Q ∩ states M ⊆ epsclo Q"
by (auto simp: epsclo_def)
lemma epsclo_UN: "epsclo (⋃x∈A. B x) = (⋃x∈A. epsclo (B x))"
by (auto simp: epsclo_def)
lemma epsclo_subset [simp]: "epsclo Q ⊆ states M"
by (auto simp: epsclo_def)
text‹Transition function for a given starting state and word.›
primrec nextl :: "['b set, 'a list] ⇒ 'b set" where
"nextl Q [] = epsclo Q"
| "nextl Q (x#xs) = nextl (⋃q ∈ epsclo Q. nxt M q x) xs"
definition language :: "'a list set" where
"language ≡ {xs. nextl (init M) xs ∩ final M ≠ {}}"
lemma nextl_epsclo: "nextl (epsclo Q) xs = nextl Q xs"
by (induct xs) (auto simp: epsclo_idem)
lemma epsclo_nextl: "epsclo (nextl Q xs) = nextl Q xs"
by (induct xs arbitrary: Q) (auto simp: epsclo_idem)
lemma nextl_app: "nextl Q (xs@ys) = nextl (nextl Q xs) ys"
by (induct xs arbitrary: Q) (auto simp: nextl_epsclo)
lemma nextl_snoc: "nextl Q (xs@[x]) = (⋃q ∈ nextl Q xs. epsclo (nxt M q x))"
by (simp add: nextl_app epsclo_UN epsclo_nextl)
lemma nextl_state: "nextl Q xs ⊆ states M"
by (induct xs arbitrary: Q) auto
subsection‹The Powerset Construction›
definition Power_dfa' :: "('a, 'b set) dfa'" where
"Power_dfa' = ⦇dfa'.states = {(epsclo q) | q. q ∈ Pow (states M)},
init = (epsclo (init M)),
final = {(epsclo Q) | Q. Q ⊆ states M ∧ Q ∩ final M ≠ {}},
nxt = λQ x. (⋃q ∈ epsclo Q. epsclo (nxt M q x))⦈"
lemma states_Power_dfa' [simp]: "dfa'.states Power_dfa' = epsclo ` Pow (states M)"
by (auto simp add: Power_dfa'_def)
lemma init_Power_dfa' [simp]: "dfa'.init Power_dfa' = (epsclo (nfa'.init M))"
by (simp add: Power_dfa'_def)
lemma final_Power_dfa [simp]: "dfa'.final Power_dfa' = {(epsclo Q) | Q. Q ⊆ states M ∧ Q ∩ final M ≠ {}}"
by (simp add: Power_dfa'_def)
lemma nxt_Power_dfa [simp]: "dfa'.nxt Power_dfa' = (λQ x. (⋃q ∈ epsclo Q. epsclo (nxt M q x)))"
by (simp add: Power_dfa'_def)
interpretation Power: dfa' Power_dfa'
proof (unfold_locales, goal_cases)
case 1 show ?case
by (force simp add: init)
next
case 2 show ?case
by auto
next
case (3 q a)
then show ?case
by (metis (no_types, lifting) Pow_iff epsclo_subset image_iff nextl_snoc nfa'.epsclo_nextl
nfa'.nextl.simps(1) nfa'_axioms nxt_Power_dfa states_Power_dfa')
next
show "finite (dfa'.states Power_dfa')"
by (force simp: finite)
qed
text‹The Power DFA accepts the same language as the NFA.›
theorem Power_language [simp]: "Power.language = language"
proof -
{ fix u
have "(Power.nextl (dfa'.init Power_dfa') u) = (nextl (init M) u)"
proof (induct u rule: List.rev_induct)
case Nil show ?case
using Power.nextl.simps
by (auto simp: hinsert_def)
next
case (snoc x u) then show ?case
by (simp add: epsclo_nextl nextl_snoc init nextl_state [THEN subsetD])
qed
then have "u ∈ Power.language ⟷ u ∈ language" using epsclo_increasing nextl_state
by (fastforce simp add: Power.language_def language_def disjoint_iff_not_equal epsclo_nextl)
}
then show ?thesis
by blast
qed
text‹Every language accepted by an ‹nfa'› is also regular.›
corollary regular: "regular language"
using Power_language Power.regular by blast
end
end