Theory Finite_State_Machines_ZF
section ‹Formal languages›
theory Finite_State_Machines_ZF imports FiniteSeq_ZF Finite1 ZF.CardinalArith
begin
subsection‹Introduction›
text‹This file deals with finite state machines. The goal
is to define regular languages and show that they are closed
by finite union, finite intersection, complements and
concatenation.
We show that the languages defined by deterministic, non-deterministic
and non-deterministic with $\epsilon$ moves are equivalent.›
text‹First, a transitive closure variation on @{thm rtrancl_unfold}.›
theorem rtrancl_rev:
shows "r^* = id(field(r)) ∪ (r^* O r)"
proof-
have "converse(r)^* = id(field(converse(r))) ∪ (converse(r) O converse(r)^*)"
using rtrancl_unfold[of "converse(r)"] by auto
then have "converse(r^*) = id(field(r)) ∪ (converse(r) O converse(r^*))"
using rtrancl_converse by auto
then have "converse(r^*) = id(field(r)) ∪ (converse(r^* O r))"
using converse_comp by auto moreover
{
fix t assume t:"t∈id(field(r)) ∪ (converse(r^* O r))"
{
assume "t∈id(field(r))"
then have "t∈converse(id(field(r)) ∪ (r^* O r))" by auto
} moreover
{
assume "t∉id(field(r))"
with t have "t∈converse(r^* O r)" by auto
then have "t∈converse(id(field(r)) ∪ (r^* O r))" by auto
}
ultimately have "t∈converse(id(field(r)) ∪ (r^* O r))" by auto
}
moreover
{
fix t assume t:"t∈converse(id(field(r)) ∪ (r^* O r))"
then obtain t1 t2 where t12:"t=⟨t1,t2⟩" "⟨t2,t1⟩∈id(field(r)) ∪ (r^* O r)"
by auto
{
assume "⟨t2,t1⟩∈id(field(r))"
with t12(1) have "t∈id(field(r))" by auto
then have "t∈id(field(r)) ∪ converse(r^* O r)" by auto
} moreover
{
assume "⟨t2,t1⟩∉id(field(r))"
with t12(2) have "⟨t2,t1⟩∈(r^* O r)" by auto
with t12(1) have "t∈converse(r^* O r)" by auto
then have "t∈id(field(r)) ∪ converse(r^* O r)" by auto
}
ultimately have "t∈id(field(r)) ∪ converse(r^* O r)" by auto
}
ultimately have "converse(id(field(r)) ∪ (r^* O r)) = converse(r^*)" by auto
then have "converse(converse(id(field(r)) ∪ (r^* O r))) = r^*" using converse_converse[OF rtrancl_type]
by auto moreover
{
fix t assume t:"t∈id(field(r)) ∪ (r^* O r)"
{
assume "t∈id(field(r))"
then have "t:field(r)*field(r)" by auto
} moreover
{
assume "t∉id(field(r))"
with t have "t∈r^* O r" by auto
then have "t:field(r)*field(r)" using rtrancl_type unfolding comp_def by auto
} ultimately
have "t∈field(r)*field(r)" by auto
}
ultimately show ?thesis using converse_converse[of "id(field(r))∪(r^* O r)" "field(r)" "λ_. field(r)"] by auto
qed
text‹A language is a subset of words.›
definition
IsALanguage ("_{is a language with alphabet}_") where
"Finite(Σ) ⟹ L {is a language with alphabet} Σ ≡ L ⊆ Lists(Σ)"
text‹The set of all words, and the set of no words are languages.›
lemma full_empty_language:
assumes "Finite(Σ)"
shows "Lists(Σ) {is a language with alphabet} Σ"
and "0 {is a language with alphabet} Σ"
unfolding IsALanguage_def[OF assms] by auto
subsection‹Deterministic Finite Automata›
text‹A deterministic finite state automaton is defined
as a finite set of states, an initial state,
a transition function from state to state based on
the word and a set of final states.›
definition
DFSA ("'(_,_,_,_'){is an DFSA for alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an DFSA for alphabet}Σ ≡ Finite(S) ∧ s⇩0 ∈ S ∧ F ⊆ S ∧ t:S×Σ → S"
text‹A finite automaton defines transitions on pairs of
words and states. Two pairs are transition related
if the second word is equal to the first except it is
missing the last symbol, and the second state is
generated by this symbol and the first state by way
of the transition function.›
definition
DFSAExecutionRelation ("{reduce D-relation}'(_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an DFSA for alphabet}Σ ⟹
{reduce D-relation}(S,s⇩0,t){in alphabet}Σ ≡ {⟨⟨w,s⟩,⟨Init(w),t`⟨s,Last(w)⟩⟩⟩. ⟨w,s⟩∈NELists(Σ)×S}"
text‹We define a word to be fully reducible by a finite
state automaton if in the transitive closure of the previous
relation it is related to the pair of the empty word and a final state.
Since the empty word with the initial state need not be in
@{term "field({reduce D-relation}(S,s⇩0,t){in alphabet}Σ)"},
we add the extra condition that @{term "⟨⟨0,s⇩0⟩,⟨0,s⇩0⟩⟩"}
is also a valid transition.›
definition
DFSASatisfy ("_ <-D '(_,_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an DFSA for alphabet}Σ ⟹ i∈Lists(Σ) ⟹
i <-D (S,s⇩0,t,F){in alphabet}Σ ≡ (∃q∈F. ⟨⟨i,s⇩0⟩,⟨0,q⟩⟩∈ ({reduce D-relation}(S,s⇩0,t){in alphabet}Σ)^*) ∨ (i = 0 ∧ s⇩0∈F)"
text‹We define a locale for better notation›
locale DetFinStateAuto =
fixes S and s⇩0 and t and F and Σ
assumes finite_alphabet: "Finite(Σ)"
assumes DFSA: "(S,s⇩0,t,F){is an DFSA for alphabet}Σ"
text‹We abbreviate the reduce relation to a single symbol
within this locale.›
abbreviation (in DetFinStateAuto) "r⇩D" where
"r⇩D ≡ {reduce D-relation}(S,s⇩0,t){in alphabet}Σ"
text‹We abbreviate the full reduction condition to a single symbol
within this locale.›
abbreviation (in DetFinStateAuto) reduce ("_{reduces}") where
"i{reduces} ≡ i <-D (S,s⇩0,t,F){in alphabet}Σ"
text‹Destruction lemma about deterministic finite
state automata.›
lemma (in DetFinStateAuto) DFSA_dest:
shows "s⇩0∈S" "F⊆S" "t:S×Σ → S" "Finite(S)" using DFSA unfolding DFSA_def[OF finite_alphabet] by auto
text‹The set of words that reduce to final states forms a language.
This is by definition.›
lemma (in DetFinStateAuto) DFSA_language:
shows "{i∈Lists(Σ). i <-D (S,s⇩0,t,F){in alphabet}Σ} {is a language with alphabet}Σ"
unfolding IsALanguage_def[OF finite_alphabet] by auto
text‹Define this language as an abbreviation
to reduce terms›
abbreviation (in DetFinStateAuto) LanguageDFSA
where "LanguageDFSA ≡ {i∈Lists(Σ). i <-D (S,s⇩0,t,F){in alphabet}Σ}"
text‹The relation is an actual relation, but even
more it is a function (hence the adjective deterministic).›
lemma (in DetFinStateAuto) reduce_is_relation_function:
shows "relation(r⇩D)" "function(r⇩D)" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
relation_def function_def by auto
text‹The relation, that is actually a function
has the following domain and range:›
lemma (in DetFinStateAuto) reduce_function:
shows "r⇩D:NELists(Σ)×S→Lists(Σ)×S"
proof-
from DFSA have T:"t:S×Σ → S" unfolding DFSA_def[OF finite_alphabet] by auto
{
fix x assume "x∈r⇩D"
then obtain l s where x:"l ∈ NELists(Σ)" "s ∈ S" "x = ⟨⟨l,s⟩,⟨Init(l),t`⟨s,Last(l)⟩⟩⟩" unfolding
DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
from x(1) have "Init(l) ∈ Lists(Σ)" using init_NElist(1) by auto moreover
from x(1) have "Last(l) ∈ Σ" using last_type by auto
with x(2) have "t`⟨s,Last(l)⟩ ∈ S" using apply_type[OF T] by auto
moreover note x
ultimately have "x∈(NELists(Σ)×S)×(Lists(Σ)×S)" by auto
}
then have r:"r⇩D∈Pow((NELists(Σ)×S)×(Lists(Σ)×S))" by auto moreover
{
fix x assume "x∈NELists(Σ)×S"
then obtain l s where x:"l∈NELists(Σ)" "s∈S" "x=⟨l,s⟩" by auto
then have "⟨⟨l,s⟩,⟨Init(l),t`⟨s,Last(l)⟩⟩⟩∈r⇩D" unfolding
DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
with x(3) have "x∈domain(r⇩D)" unfolding domain_def by auto
}
then have "NELists(Σ)×S ⊆ domain(r⇩D)" by auto moreover
note reduce_is_relation_function(2)
ultimately show ?thesis unfolding Pi_def by auto
qed
text‹The field of the relation contains all pairs
with non-empty
words, but we cannot assume that it contains all pairs.›
corollary (in DetFinStateAuto) reduce_field:
shows "field(r⇩D) ⊆ Lists(Σ)×S" "NELists(Σ)×S ⊆ field(r⇩D)"
proof-
from DFSA have T:"t:S×Σ → S" unfolding DFSA_def[OF finite_alphabet] by auto
{
fix x assume "x∈field(r⇩D)"
then have E:"∃y. ⟨x,y⟩∈r⇩D ∨ ⟨y,x⟩∈r⇩D" unfolding domain_def range_def field_def by auto
{
assume "∃y. ⟨x,y⟩∈r⇩D"
then have "x∈NELists(Σ)×S" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
by auto
then have "x∈Lists(Σ)×S" unfolding Lists_def NELists_def by auto
} moreover
{
assume "¬(∃y. ⟨x,y⟩∈r⇩D)"
with E have "∃y.⟨y,x⟩∈r⇩D" by auto
then obtain u v where y:"u∈NELists(Σ)" "v∈S" "x=⟨Init(u),t`⟨v,Last(u)⟩⟩"
unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
from y(1) have "Init(u) ∈ Lists(Σ)" using init_NElist(1) by auto moreover
from y(1) have "Last(u) ∈ Σ" using last_type by auto
with y(2) have "t`⟨v,Last(u)⟩ ∈ S" using apply_type[OF T] by auto
moreover note y(3) ultimately have "x∈Lists(Σ)×S" by auto
}
ultimately have "x∈Lists(Σ)×S" by auto
}
then show "field(r⇩D) ⊆ Lists(Σ)×S" by auto
show "NELists(Σ)×S ⊆ field(r⇩D)"
using domain_of_fun[OF reduce_function] unfolding field_def by auto
qed
text‹If a word is a reduced version of an other,
then it can be encoded as a restriction.›
lemma (in DetFinStateAuto) seq_is_restriction:
fixes w s u v
assumes "⟨⟨w,s⟩,⟨u,v⟩⟩∈r⇩D^*"
shows "restrict(w,domain(u)) = u"
proof-
from assms have "⟨w,s⟩∈field(r⇩D)" using rtrancl_field[of r⇩D] relation_field_times_field[OF relation_rtrancl[of r⇩D]] by auto
then have "w∈Lists(Σ)" using reduce_field(1) by auto
then obtain n where "w:n→Σ" unfolding Lists_def by auto
then have "restrict(w,n) = w" "w:n→Σ" using restrict_idem unfolding Pi_def by auto
then have base:"restrict(w,domain(w)) = w" using domain_of_fun by auto
{
fix y z
assume as:"⟨⟨w, s⟩, y⟩ ∈ r⇩D^*" "⟨y, z⟩ ∈ r⇩D" "restrict(w, domain(fst(y))) = fst(y)"
from as(1) have "y:field(r⇩D)" using rtrancl_field[of r⇩D] relation_field_times_field[OF relation_rtrancl[of r⇩D]] by auto
then obtain y1 y2 where y:"y=⟨y1,y2⟩" "y1∈Lists(Σ)" "y2∈S" using reduce_field(1)
by auto
with as(2) have z:"z=⟨Init(y1),t`⟨y2,Last(y1)⟩⟩" "y1∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
by auto
then have "fst(z) = Init(y1)" by auto
with z(2) have S:"succ(domain(fst(z))) = domain(y1)" using init_NElist(2) by auto
from as(3) y(1) have "restrict(w,domain(y1)) = y1" by auto
then have "restrict(restrict(w,domain(y1)),pred(domain(y1))) = Init(y1)" unfolding Init_def by auto
then have w:"restrict(w,domain(y1)∩pred(domain(y1))) = Init(y1)" using restrict_restrict by auto
from z(2) obtain q where q:"domain(y1) = succ(q)" "q∈nat" using domain_of_fun unfolding NELists_def by auto
then have "pred(domain(y1)) ⊆ domain(y1)" using pred_succ_eq by auto
then have "domain(y1) ∩ pred(domain(y1)) = pred(domain(y1))" by auto
with w have "restrict(w,pred(domain(y1))) = Init(y1)" by auto moreover
from q z(2) init_props(1)[of _ y1 Σ] have "domain(Init(y1)) = pred(domain(y1))"
using domain_of_fun[of y1 _ "λ_. Σ"] domain_of_fun[of "Init(y1)" _ "λ_. Σ"]
unfolding NELists_def by auto ultimately
have "restrict(w,domain(Init(y1))) = Init(y1)" by auto
with z(1) have "restrict(w,domain(fst(z))) = fst(z)" by auto
}
then have reg:"∀y z. ⟨⟨w, s⟩, y⟩ ∈ r⇩D^* ⟶
(⟨y, z⟩ ∈ r⇩D ⟶
(restrict(w, domain(fst(y))) = fst(y) ⟶
restrict(w, domain(fst(z))) = fst(z)))" by auto
have "restrict(w, domain(fst(⟨u, v⟩))) = fst(⟨u, v⟩)"
proof(rule rtrancl_induct[of "⟨w,s⟩" "⟨u,v⟩" r⇩D "λq. restrict(w,domain(fst(q))) = fst(q)"])
from base show "restrict(w,domain(fst(⟨w,s⟩))) = fst(⟨w,s⟩)" by auto
from assms show "⟨⟨w, s⟩, u, v⟩ ∈ r⇩D^*" by auto
{
fix y z
assume as:"⟨⟨w, s⟩, y⟩ ∈ r⇩D^*" "⟨y, z⟩ ∈ r⇩D" "restrict(w, domain(fst(y))) = fst(y)"
from as(1) have "y:field(r⇩D)" using rtrancl_field[of r⇩D] relation_field_times_field[OF relation_rtrancl[of r⇩D]] by auto
then obtain y1 y2 where y:"y=⟨y1,y2⟩" "y1∈Lists(Σ)" "y2∈S" using reduce_field(1)
by auto
with as(2) have z:"z=⟨Init(y1),t`⟨y2,Last(y1)⟩⟩" "y1∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
by auto
then have "fst(z) = Init(y1)" by auto
with z(2) have S:"succ(domain(fst(z))) = domain(y1)" using init_NElist(2) by auto
from as(3) y(1) have "restrict(w,domain(y1)) = y1" by auto
then have "restrict(restrict(w,domain(y1)),pred(domain(y1))) = Init(y1)" unfolding Init_def by auto
then have w:"restrict(w,domain(y1)∩pred(domain(y1))) = Init(y1)" using restrict_restrict by auto
from z(2) obtain q where q:"domain(y1) = succ(q)" "q∈nat" using domain_of_fun unfolding NELists_def by auto
then have "pred(domain(y1)) ⊆ domain(y1)" using pred_succ_eq by auto
then have "domain(y1) ∩ pred(domain(y1)) = pred(domain(y1))" by auto
with w have "restrict(w,pred(domain(y1))) = Init(y1)" by auto moreover
from q z(2) init_props(1)[of _ y1 Σ] have "domain(Init(y1)) = pred(domain(y1))"
using domain_of_fun[of y1 _ "λ_. Σ"] domain_of_fun[of "Init(y1)" _ "λ_. Σ"]
unfolding NELists_def by auto ultimately
have "restrict(w,domain(Init(y1))) = Init(y1)" by auto
with z(1) show "restrict(w,domain(fst(z))) = fst(z)" by auto
}
qed
then show ?thesis by auto
qed
lemma (in DetFinStateAuto) relation_deteministic:
assumes "⟨⟨w,s⟩,⟨u,v⟩⟩∈r⇩D^*" "⟨⟨w,s⟩,⟨u,m⟩⟩∈r⇩D^*"
shows "v=m"
proof-
let ?P="λy. ∀q1 q2. ⟨⟨w,s⟩,⟨q1,q2⟩⟩∈r⇩D^* ⟶ fst(y) = q1 ⟶ snd(y) = q2"
{
fix q1 q2 assume "⟨⟨w, s⟩, q1, q2⟩ ∈ r⇩D^*" "fst(⟨w, ss⟩) = q1"
then have "⟨⟨w, s⟩, w, q2⟩ ∈ r⇩D^*" by auto
then have "⟨⟨w, s⟩, w, q2⟩ ∈ id(field(r⇩D)) ∪ (r⇩D^* O r⇩D)" using rtrancl_rev by auto
then have A:"s=q2 ∨ ⟨⟨w, s⟩, w, q2⟩:(r⇩D^* O r⇩D)" by auto
{
assume "s≠q2"
with A have "⟨⟨w, s⟩, w, q2⟩:(r⇩D^* O r⇩D)" by auto
then obtain b where b:"⟨⟨w,s⟩,b⟩:r⇩D" "⟨b,w,q2⟩:r⇩D^*" unfolding compE by auto
from b(1) have "b=⟨Init(w),t`⟨s,Last(w)⟩⟩" and w:"w:NELists(Σ)" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
with b(2) have "restrict(Init(w),domain(w)) = w" using seq_is_restriction by auto
then have "domain(Init(w))∩domain(w) = domain(w)" using domain_restrict[of "Init(w)" "domain(w)"] by auto
with w have e:"domain(Init(w))∩domain(w) = succ(domain(Init(w)))" using init_NElist(2)[of w] by auto
{
fix tt assume t:"tt:succ(domain(Init(w)))"
with e have "tt:domain(Init(w))∩domain(w)" by auto
then have "tt:domain(Init(w))" by auto
}
then have "succ(domain(Init(w)))⊆domain(Init(w))" by auto
then have "domain(Init(w)) ∈ domain(Init(w))" by auto
then have False using mem_irrefl[of "domain(Init(w))"] by auto
}
then have "s=q2" by auto
then have "snd(⟨w,s⟩) = q2" by auto
}
then have P0:"?P(⟨w,s⟩)" by auto
{
fix y z assume y:"⟨⟨w,s⟩,y⟩:r⇩D^*" "⟨y,z⟩:r⇩D" "?P(y)"
{
fix q1 q2 assume z:"⟨⟨w, s⟩, q1, q2⟩ ∈ r⇩D^*" "fst(z) = q1"
from this(1) have "⟨⟨w, s⟩, q1, q2⟩ ∈ id(field(r⇩D)) ∪ (r⇩D O r⇩D^*)" using rtrancl_unfold by auto
then have A:"(s=q2 ∧ w=q1) ∨ ⟨⟨w, s⟩, q1, q2⟩:(r⇩D O r⇩D^*)" by auto
from y(2) obtain y1 y2 where zz:"y=⟨y1,y2⟩" "y1:NELists(Σ)" "y2∈S" "z=⟨Init(y1),t`⟨y2,Last(y1)⟩⟩"
unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
{
assume w:"w=q1"
with z(2) zz(4) have "w=Init(y1)" by auto
with y(1) zz(1) have "restrict(Init(y1),domain(y1)) = y1" using seq_is_restriction
by auto
then have "domain(Init(y1))∩domain(y1) = domain(y1)" using domain_restrict[of "Init(y1)" "domain(y1)"] by auto
with zz(2) have e:"domain(Init(y1))∩domain(y1) = succ(domain(Init(y1)))" using init_NElist(2)[of y1] by auto
{
fix tt assume t:"tt:succ(domain(Init(y1)))"
with e have "tt:domain(Init(y1))∩domain(y1)" by auto
then have "tt:domain(Init(y1))" by auto
}
then have "succ(domain(Init(y1)))⊆ domain(Init(y1))" by auto
then have "domain(Init(y1)) ∈ domain(Init(y1))" by auto
then have False using mem_irrefl[of "domain(Init(y1))"] by auto
}
with A have "⟨⟨w, s⟩, q1, q2⟩:(r⇩D O r⇩D^*)" by auto
then obtain pp where pp:"⟨⟨w, s⟩, pp⟩:r⇩D^*" "⟨pp, q1, q2⟩:r⇩D" unfolding compE by auto
from this(2) obtain ppL ppS where ppl:"ppL:NELists(Σ)" "ppS∈S" "pp=⟨ppL,ppS⟩"
"q1=Init(ppL)" "q2=t`⟨ppS,Last(ppL)⟩" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
from this(3) pp(1) have rr:"restrict(w,domain(ppL)) = ppL" using seq_is_restriction by auto
then have r:"restrict(w,domain(ppL))`pred(domain(ppL)) = Last(ppL)" unfolding Last_def by auto
from ppl(1) obtain q where q:"ppL:succ(q) → Σ" "q∈nat" unfolding NELists_def by blast
from q(1) have D:"domain(ppL) = succ(q)" using func1_1_L1[of ppL] by auto moreover
from D have "pred(domain(ppL)) = q" using pred_succ_eq by auto
then have "pred(domain(ppL)) ∈ succ(q)" by auto
ultimately have "pred(domain(ppL)) ∈ domain(ppL)" by auto
with restrict r have W:"w`pred(domain(ppL)) = Last(ppL)" by auto
from y(1) zz(1) have "restrict(w,domain(y1)) = y1" using seq_is_restriction by auto
moreover note rr moreover
from q have "Init(ppL):q → Σ" using init_props(1) by auto
then have DInit:"domain(Init(ppL)) = q" using func1_1_L1 by auto
from zz(4) z(2) have "q1=Init(y1)" by auto
with ppl(4) have "Init(ppL) = Init(y1)" by auto
with DInit have Dy1:"domain(Init(y1)) = q" by auto
from zz(2) obtain o where o:"o∈nat" "y1:succ(o) → Σ" unfolding NELists_def by auto
then have "Init(y1):o→Σ" using init_props(1) by auto
with Dy1 have "q=o" using func1_1_L1 by auto
with o(2) have "y1:succ(q)→Σ" by auto moreover
note q(1) ultimately have "y1=ppL" using func1_1_L1 by auto moreover
then have "fst(y) = ppL" using zz(1) by auto
with y(3) pp(1) ppl(3) have "snd(y) = ppS" by auto
with zz(1) have "y2= ppS" by auto moreover
note zz(4) ultimately have "z=⟨Init(ppL),t`⟨ppS,Last(ppL)⟩⟩" by auto
then have "snd(z) = t`⟨ppS,Last(ppL)⟩" by auto
with ppl(5) have "snd(z) = q2" by auto
}
then have "?P(z)" by auto
}
then have R:"⋀y z. ⟨⟨w,s⟩,y⟩∈r⇩D^* ⟹ ⟨y,z⟩∈r⇩D ⟹ ?P(y) ⟹ ?P(z)" by auto
then have "?P(⟨u,v⟩)" using rtrancl_induct[of "⟨w,s⟩" "⟨u,v⟩" r⇩D "λy. ∀q1 q2. ⟨⟨w,s⟩,⟨q1,q2⟩⟩:r⇩D^* ⟶ fst(y) = q1 ⟶ snd(y) = q2"]
P0 assms(1) by auto
then show ?thesis using assms(2) by auto
qed
text‹Any non-empty word can be reduced to the empty
string, but it does not always end in a final state.›
lemma (in DetFinStateAuto) endpoint_exists:
assumes "w∈NELists(Σ)"
shows "∃q ∈ S. ⟨⟨w,s⇩0⟩,⟨0,q⟩⟩ ∈ r⇩D^*"
proof-
let ?P="λk. ∀y∈Lists(Σ). domain(y) = k ⟶ y=0 ∨ (∀ss∈S. (∃q∈S. ⟨⟨y,ss⟩,⟨0,q⟩⟩∈r⇩D^*))"
{
fix y assume "y∈Lists(Σ)" "domain(y) = 0"
with assms have "y=0" unfolding Lists_def using domain_of_fun by auto
then have "y=0 ∨ (∀ss∈S. (∃q∈S. ⟨⟨y,ss⟩,⟨0,q⟩⟩∈r⇩D^*))" by auto
}
then have base:"?P(0)" by auto
{
fix k assume hyp:"?P(k)" "k∈nat"
{
fix y assume as:"y∈Lists(Σ)" "domain(y) = succ(k)"
from as have "y:succ(k)→Σ" unfolding Lists_def using domain_of_fun by auto
with hyp(2) have y:"y:NELists(Σ)" unfolding NELists_def by auto
then have "Init(y):Lists(Σ)" "succ(domain(Init(y))) = domain(y)" using init_NElist by auto
with as(2) have D:"Init(y):Lists(Σ)" "domain(Init(y)) = k" using pred_succ_eq by auto
with hyp(1) have d:"Init(y) = 0 ∨ (∀ss∈S. (∃q∈S. ⟨⟨Init(y),ss⟩,⟨0,q⟩⟩∈r⇩D^*))" by auto
{
assume iy0:"Init(y) = 0"
{
fix ss assume "ss∈S"
with iy0 y have "⟨⟨y,ss⟩,0,t`⟨ss,Last(y)⟩⟩∈r⇩D" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
by auto
then have "⟨⟨y,ss⟩,0,t`⟨ss,Last(y)⟩⟩∈r⇩D^*" using r_into_rtrancl by auto
moreover from `ss∈S` have "t`⟨ss,Last(y)⟩ ∈S" using apply_type[OF DFSA_dest(3)]
last_type[OF y] by auto
ultimately have "∃q∈S. ⟨⟨y,ss⟩,0,q⟩:r⇩D^*" by auto
}
then have "∀ss∈S. ∃q∈S. ⟨⟨y,ss⟩,0,q⟩:r⇩D^*" by auto
then have "y = 0 ∨ (∀ss∈S. ∃q∈S. ⟨⟨y,ss⟩,0,q⟩:r⇩D^*)" by auto
} moreover
{
assume qS:"∀ss∈S. ∃q∈S. ⟨⟨Init(y),ss⟩,⟨0,q⟩⟩∈r⇩D^*"
{
fix ss assume "ss∈S"
with y have "⟨⟨y,ss⟩,Init(y),t`⟨ss,Last(y)⟩⟩∈r⇩D" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
by auto
moreover from `ss∈S` y have "t`⟨ss,Last(y)⟩ ∈S" using apply_type[OF DFSA_dest(3)]
last_type by auto
with qS have "∃q∈S. ⟨⟨Init(y),t`⟨ss,Last(y)⟩⟩,⟨0,q⟩⟩∈r⇩D^*" by auto
then obtain q where "q∈S" "⟨⟨Init(y),t`⟨ss,Last(y)⟩⟩,⟨0,q⟩⟩∈r⇩D^*" by auto
ultimately have "⟨⟨y,ss⟩,⟨0,q⟩⟩∈r⇩D^*" "q∈S" using rtrancl_into_trancl2
trancl_into_rtrancl by auto
then have "∃q∈S. ⟨⟨y,ss⟩,⟨0,q⟩⟩∈r⇩D^*" by auto
}
then have "y = 0 ∨ (∀ss∈S. ∃q∈S. ⟨⟨y,ss⟩,0,q⟩:r⇩D^*)" by auto
} ultimately
have "y = 0 ∨ (∀ss∈S. ∃q∈S. ⟨⟨y,ss⟩,0,q⟩:r⇩D^*)" using d by auto
}
then have "?P(succ(k))" by auto
}
then have ind:"⋀k. k∈nat ⟹ ?P(k) ⟹ ?P(succ(k))" by blast
have dom:"domain(w) ∈ nat" using assms unfolding NELists_def using domain_of_fun by auto
from ind have "?P(domain(w))" using nat_induct[of _ ?P, OF dom base] by auto
with assms have "(∀ss∈S. ∃q∈S. ⟨⟨w, ss⟩, 0, q⟩ ∈ r⇩D^*)"
using non_zero_List_func_is_NEList by auto
then show ?thesis using DFSA_dest(1) by auto
qed
text‹Example of Finite Automaton of binary lists
starting with $0$ and ending with $1$›
locale ListFrom0To1
begin
text‹Empty state›
definition empty where
"empty ≡ 2"
text‹The string starts with $0$ state›
definition ends0 where
"ends0 ≡ succ(2)"
text‹The string ends with $1$ state›
definition starts1 where
"starts1 ≡ 1"
text‹The string ends with $0$ state›
definition starts0 where
"starts0 ≡ 0"
text‹The states are the previous 4 states.
They are encoded as natural numbers to make
it easier to reason about them, and as human
readable variable names to make it easier to
understand.›
definition states where
"states ≡ {empty, starts0, starts1, ends0}"
text‹The final state is @{term starts0}›
definition finalStates where
"finalStates ≡ {starts0}"
text‹The transition function is defined as follows:
From the @{term empty} state,
we transition to state @{term starts1} in case there is a $1$
and to state @{term ends0} in case there is a $0$.
From the state @{term ends0} we stay in it.
From the states @{term starts1} and @{term starts0}
we transition to @{term starts0} in case there is a $0$,
and to @{term starts1} in case there is a $1$.›
definition transFun where
"transFun ≡ {⟨⟨empty,1⟩,starts1⟩,⟨⟨empty,0⟩,ends0⟩}∪
{⟨⟨ends0,x⟩,ends0⟩. x∈2}∪
{⟨⟨starts1,0⟩,starts0⟩,⟨⟨starts1,1⟩,starts1⟩,
⟨⟨starts0,0⟩,starts0⟩,⟨⟨starts0,1⟩,starts1⟩}"
text‹Add lemmas to simplify›
lemmas from0To1[simp] = states_def empty_def transFun_def finalStates_def
ends0_def starts1_def starts0_def
text‹Interpret the example as a deterministic finite state automaton›
interpretation dfsaFrom0To1: DetFinStateAuto states empty transFun finalStates 2 unfolding DetFinStateAuto_def apply safe
using Finite_0 apply simp
proof-
have finA:"Finite(2)" using nat_into_Finite[of 2] by auto
have finS:"Finite(states)" using nat_into_Finite by auto
moreover have funT:"transFun:states×2 → states" unfolding Pi_def function_def by auto
moreover have "finalStates ⊆ states" by auto
moreover have "empty∈ states" by auto
ultimately show "(states,empty,transFun,finalStates){is an DFSA for alphabet}2"
unfolding DFSA_def[OF finA] by auto
qed
text‹Abbreviate the relation to something
readable.›
abbreviation r0to1 ("r{0.*1}") where
"r{0.*1} ≡ dfsaFrom0To1.r⇩D"
text‹If a word reaches the state @{term starts0},
it does not move from it.›
lemma invariant_state_3:
fixes w u y
assumes "⟨⟨w,ends0⟩,⟨u,y⟩⟩∈r{0.*1}^*"
shows "y = ends0"
proof-
have finA:"Finite(2)" by auto
have funT:"transFun:states×2→ states"
using dfsaFrom0To1.DFSA_dest(3) .
have "snd(⟨u,y⟩) = ends0"
proof(rule rtrancl_induct[of "⟨w,ends0⟩"
"⟨u,y⟩" "r{0.*1}" "λt. snd(t) = ends0"])
show "snd(⟨w, ends0⟩) = ends0" by auto
from assms show "⟨⟨w, ends0⟩, u, y⟩ ∈ r{0.*1}^*" .
{
fix y z assume as:"⟨⟨w, ends0⟩, y⟩ ∈ r{0.*1}^*" "⟨y, z⟩ ∈ r{0.*1}" "snd(y) = ends0"
from as(3,2) obtain y1 where yy:"y=⟨y1,ends0⟩" "y1∈NELists(2)"
"z=⟨Init(y1),transFun`⟨ends0,Last(y1)⟩⟩"
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA]
by auto
from yy(2) have "Last(y1)∈2" using last_type by auto
then have "⟨⟨ends0,Last(y1)⟩,ends0⟩∈transFun" by auto
then have "transFun`⟨ends0,Last(y1)⟩ = ends0"
using apply_equality[OF _ funT, of _ ends0] by auto
with yy(3) have "z=⟨Init(y1),ends0⟩" by auto
then show "snd(z) = ends0" by auto
}
qed
then show ?thesis by auto
qed
text‹If the string starts in $0$ and has
reached states @{term starts0} or @{term starts1};
then it reduces to @{term starts0}.›
lemma invariant_state_0_1:
fixes w
assumes "w∈NELists(2)" "w`0 = 0"
shows "⟨⟨w,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" "⟨⟨w,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*"
proof-
from assms(1) obtain n where w:"n:nat" "w:succ(n)→2" unfolding NELists_def by auto
then have dom:"domain(w)∈nat" using domain_of_fun by auto
{
fix q assume "q∈NELists(2)"
then obtain m where "m∈nat" "q:succ(m)→2" unfolding NELists_def by auto
then have "domain(q)≠0" using domain_of_fun by auto
}
then have base:"∀w. w ∈ NELists(2) ∧ w`0 = 0 ∧ domain(w) = 0 ⟶
⟨⟨w, starts0⟩, 0, starts0⟩ ∈ r{0.*1}^* ∧ ⟨⟨w, starts1⟩, 0, starts0⟩ ∈ r{0.*1}^*" by auto
from w(2) have domN0:"domain(w)≠ 0" using domain_of_fun by auto
have finA:"Finite(2)" using nat_into_Finite[of 2] by auto
have funT:"transFun:states×2→states" unfolding Pi_def function_def by auto
have t00:"transFun`⟨starts0,0⟩ = starts0" using funT apply_equality[of "⟨starts0,0⟩" starts0 transFun "states×2" "λ_. states"] by auto
have t01:"transFun`⟨starts1,0⟩ = starts0" using funT apply_equality[of "⟨starts1,0⟩" starts0 transFun "states×2" "λ_. states"] by auto
have t10:"transFun`⟨starts0,1⟩ = starts1" using funT apply_equality[of "⟨starts0,1⟩" starts1 transFun "states×2" "λ_. states"] by auto
have t11:"transFun`⟨starts1,1⟩ = starts1" using funT apply_equality[of "⟨starts1,1⟩" starts1 transFun "states×2" "λ_. states"] by auto
{
fix ka assume kaNat:"ka:nat"
assume k:"∀w. w ∈ NELists(2) ∧ w`0 = 0 ∧ domain(w) = ka ⟶ (⟨⟨w,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨w,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*)"
{
fix y assume y:"y∈NELists(2)" "y`0 = 0" "domain(y) = succ(ka)"
from y(1) obtain s where s:"y:succ(s)→2" "s∈nat" unfolding NELists_def by auto
then have L:"Last(y) = y`s" using last_seq_elem by auto
then have last_2:"Last(y) ∈ 2" using apply_type[OF s(1), of s] by auto
{
assume ka:"ka =0"
with y(3) have "pred(domain(y)) = 0" using pred_succ_eq by auto
then have y00:"y`0 = 0" using y(2) unfolding Last_def by auto
then have "⟨⟨y,starts0⟩,⟨Init(y),transFun`⟨starts0,Last(y)⟩⟩⟩∈r{0.*1}" unfolding
DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA]
using y(1) by auto
with last_2 t00 t10 have "⟨⟨y,starts0⟩,⟨Init(y),Last(y)⟩⟩∈r{0.*1}" by auto moreover
from ka y(3) s(1) have "Init(y):0→2" using init_props(1)[OF s(2,1)]
domain_of_fun[OF s(1)] by auto
then have y0:"Init(y) = 0" unfolding Pi_def by auto moreover
from ka s(1) y(3) have "s=0" using domain_of_fun by auto
with L have LL:"y`0 = Last(y)" by auto moreover note y(2)
ultimately have "⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}" by auto
then have A:"⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using r_into_rtrancl by auto
note t01 moreover have "⟨⟨y,starts1⟩,⟨Init(y),transFun`⟨starts1,Last(y)⟩⟩⟩ ∈ r{0.*1}"
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] using y(1,2) by auto
moreover note t11 last_2 y0 LL y(2) ultimately have "⟨⟨y,starts1⟩,⟨0,starts0⟩⟩ ∈ r{0.*1}" by auto
then have B:"⟨⟨y,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using r_into_rtrancl by auto
with A have "⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨y,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" by auto
} moreover
{
assume ka:"ka≠0"
with kaNat obtain u where u:"ka=succ(u)" "u∈nat" using Nat_ZF_1_L3 by auto
from y(3) s(1) kaNat s(2) have "s=ka" using domain_of_fun succ_inject by auto
with u(1) have "s=succ(u)" by auto moreover
have "Init(y):s→2" using init_props(1)[OF s(2,1)].
ultimately have yu:"Init(y):succ(u)→2" by auto
with u have "Init(y)∈NELists(2)" "domain(Init(y)) = ka"
using domain_of_fun unfolding NELists_def by auto
moreover from yu have "Init(y)`0 = 0" using init_props(2)[OF nat_succI[OF u(2)], of y 2]
s(1) `s=succ(u)` empty_in_every_succ[OF u(2)] y(2) by auto
moreover note k ultimately have "⟨⟨Init(y),starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^*"
"⟨⟨Init(y),starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" by auto
then have A:"∀x∈{starts0, starts1}. ⟨⟨Init(y),x⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" by auto
have Q:"⟨⟨y,starts0⟩,⟨Init(y),transFun`⟨starts0,Last(y)⟩⟩⟩∈r{0.*1}" using y(2)
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] using y(1) by auto
{
assume as:"Last(y) = 0"
with Q t00 have "⟨⟨y,starts0⟩,⟨Init(y),starts0⟩⟩∈r{0.*1}" by auto
} moreover
{
assume as:"Last(y) = 1"
with Q t10 have "⟨⟨y,starts0⟩,⟨Init(y),starts1⟩⟩∈r{0.*1}" by auto
}
moreover note last_2 ultimately have
"(⟨⟨y,starts0⟩,⟨Init(y),starts0⟩⟩∈r{0.*1}) ∨ (⟨⟨y,starts0⟩,⟨Init(y),starts1⟩⟩∈r{0.*1})" by auto
with A have B:"⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using rtrancl_into_trancl2 trancl_into_rtrancl by auto
have Q:"⟨⟨y,starts1⟩,⟨Init(y),transFun`⟨starts1,Last(y)⟩⟩⟩∈r{0.*1}" using y(2)
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] using y(1) by auto
{
assume as:"Last(y) = 0"
with Q t01 have "⟨⟨y,starts1⟩,⟨Init(y),starts0⟩⟩∈r{0.*1}" by auto
} moreover
{
assume as:"Last(y) = 1"
with Q t11 have "⟨⟨y,starts1⟩,⟨Init(y),starts1⟩⟩∈r{0.*1}" by auto
}
moreover note last_2 ultimately have
"(⟨⟨y,starts1⟩,⟨Init(y),starts0⟩⟩∈r{0.*1}) ∨ (⟨⟨y,starts1⟩,⟨Init(y),starts1⟩⟩∈r{0.*1})" by auto
with A have "⟨⟨y,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using rtrancl_into_trancl2 trancl_into_rtrancl by auto
with B have rr:"⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨y,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" by auto
}
ultimately have "⟨⟨y,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨y,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" by auto
}
then have "∀w. w ∈ NELists(2) ∧ w`0 = 0 ∧ domain(w) = succ(ka) ⟶ (⟨⟨w,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨w,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*)" by auto
}
then have rule:"∀k∈nat.
(∀w. w ∈ NELists(2) ∧ w`0 = 0 ∧ domain(w) = k ⟶
⟨⟨w, starts0⟩, 0, starts0⟩ ∈ r{0.*1}^* ∧ ⟨⟨w, starts1⟩, 0, starts0⟩ ∈ r{0.*1}^*) ⟶
(∀w. w ∈ NELists(2) ∧ w`0 = 0 ∧ domain(w) = succ(k) ⟶
⟨⟨w, starts0⟩, 0, starts0⟩ ∈ r{0.*1}^* ∧ ⟨⟨w, starts1⟩, 0, starts0⟩ ∈ r{0.*1}^*)" by blast
from ind_on_nat[of "domain(w)" "λt . ∀w. w∈NELists(2) ∧ w`0 =0 ∧ domain(w) = t ⟶ (⟨⟨w,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^* ∧ ⟨⟨w,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*)", OF dom base rule]
show R:"⟨⟨w,starts0⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" "⟨⟨w,starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using assms(2,1) by auto
qed
text‹A more readable reduction statement›
abbreviation red ("_{reduces in 0.*1}") where
"i{reduces in 0.*1} ≡ dfsaFrom0To1.reduce(i)"
text‹Any list starting with $0$ and ending in $1$
reduces.›
theorem starts1ends0_DFSA_reduce:
fixes i
assumes "i∈Lists(2)" and "i`0=0" and "Last(i) = 1"
shows "i{reduces in 0.*1}"
proof-
from assms(1) obtain tt where t:"tt∈nat" "i:tt→2" unfolding Lists_def by auto
then have domNat:"domain(i) = tt" using domain_of_fun by auto
{
assume "domain(i) = 0" moreover
from assms(3) have "⋃(i``{Arith.pred(domain(i))})=1" unfolding Last_def apply_def by auto
then have "i≠0" by auto
ultimately have False using t domain_of_fun by auto
}
with domNat t(1) obtain y where y:"domain(i) = succ(y)" "y∈nat" using Nat_ZF_1_L3 by auto
with domNat t(2) have iList:"i∈NELists(2)" unfolding NELists_def by auto
have finA:"Finite(2)" using nat_into_Finite[of 2] by auto
have funT:"transFun:states×2→states" unfolding Pi_def function_def by auto
have "⟨⟨i,empty⟩,⟨Init(i),transFun`⟨empty,Last(i)⟩⟩⟩:r{0.*1}" using iList unfolding
DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] by auto
moreover have "transFun`⟨empty,Last(i)⟩ = 1" using apply_equality[OF _ funT] assms(3)
by auto
ultimately have U:"⟨⟨i,empty⟩,⟨Init(i),starts1⟩⟩:r{0.*1}" by auto
{
assume "y = 0"
with y(1) t(2) have iFun:"i:1→2" using domain_of_fun by auto
then have "i = {⟨0,i`0⟩}" using fun_is_set_of_pairs[of i 1 2] by auto
with assms(2) have ii:"i={⟨0,0⟩}" by auto
then have "∀y. ∃x∈{Arith.pred(domain(i))}. ⟨x, y⟩ ∈ i ⟶ y=0" by auto
moreover from assms(3) have eq:"1 = i`pred(domain(i))" unfolding Last_def by auto
from iFun have "domain(i) = 1" using domain_of_fun by auto
then have "pred(domain(i)) = 0" using pred_succ_eq by auto
then have "i`pred(domain(i)) = i`0" by auto
with eq have "1 = i`0" by auto
then have False using assms(2) by auto
}
then have "y≠0" by auto
then obtain k where yy:"y= succ(k)" "k∈nat" using Nat_ZF_1_L3 y(2) by auto
with iList y(1) have iss:"i:succ(succ(k)) → 2" unfolding NELists_def using domain_of_fun by auto
then have "Init(i):succ(k) → 2" using init_props(1) nat_succI[OF yy(2)] by auto
then have "Init(i)∈NELists(2)" unfolding NELists_def using yy(2) by auto moreover
have "0∈succ(k)" using empty_in_every_succ yy(2) by auto
with iss assms(2) have "Init(i)`0 = 0" using init_props(2)[of "succ(k)" i 2] nat_succI[OF yy(2)]
by auto
ultimately have "⟨⟨Init(i),starts1⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using invariant_state_0_1
by auto
with U have "⟨⟨i,empty⟩,⟨0,starts0⟩⟩∈r{0.*1}^*" using rtrancl_into_trancl2[THEN trancl_into_rtrancl] by auto
then have "∃q∈finalStates. ⟨⟨i,empty⟩,⟨0,q⟩⟩ ∈ r{0.*1}^*" by auto
then show ?thesis using DFSASatisfy_def[OF finA dfsaFrom0To1.DFSA assms(1)] by auto
qed
text‹Any list that reduces starts with 0 and ends in 1›
theorem starts1ends0_DFSA_reduce_rev:
fixes i
assumes "i∈Lists(2)" and "i {reduces in 0.*1}"
shows "i`0=0" and "Last(i) = 1"
proof-
have finA:"Finite(2)" using nat_into_Finite[of 2] by auto
have funT:"transFun:states×2→states" unfolding Pi_def function_def by auto
from assms(2) have "⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ r{0.*1}^*"
unfolding DFSASatisfy_def[OF finA dfsaFrom0To1.DFSA assms(1)]
by auto
then have "⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ id(field(r{0.*1})) ∪ (r{0.*1} O r{0.*1}^*)" using rtrancl_unfold[of "r{0.*1}"] by auto
then have k:"⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ id(field(r{0.*1})) ∨ ⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ (r{0.*1} O r{0.*1}^*)" by auto
have d:"domain(r{0.*1}) = NELists(2)×states"
using domainI[of _ _ "r{0.*1}"]
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA]
by auto
from k have "⟨i,empty⟩ = ⟨0,starts0⟩ ∨ ⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ (r{0.*1} O r{0.*1}^*)" using id_iff by auto
then have "(i=0 ∧ empty=starts0) ∨ (⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ r{0.*1} O r{0.*1}^*)" by auto
then have "⟨⟨i,empty⟩,⟨0,starts0⟩⟩ ∈ r{0.*1} O r{0.*1}^*" by auto
then obtain q where q:"⟨q,⟨0,starts0⟩⟩ ∈ r{0.*1}" "⟨⟨i,empty⟩,q⟩∈r{0.*1}^*" unfolding comp_def by auto
from q(1) have "q ∈ domain(r{0.*1})" unfolding domain_def by auto
with d have "q ∈ NELists(2)×states" by auto
then obtain q1 q2 where qq:"q=⟨q1,q2⟩" "q1∈NELists(2)" "q2∈states" by auto
from q(1) qq(1) have A:"0 = Init(q1)" "0 = transFun`⟨q2,Last(q1)⟩"
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] by auto
from qq(1) q(2) have "restrict(i,domain(q1)) = q1"
using dfsaFrom0To1.seq_is_restriction
by auto
then have iRes:"restrict(i,domain(q1))`0 = q1`0" by auto
from qq(2) obtain k where k:"q1:succ(k)→2" "k∈nat" unfolding NELists_def by auto
then have "Init(q1):k→2" using init_props(1) by auto
with A(1) have "k=0" unfolding Pi_def by auto
with k(1) have qfun:"q1:1→2" by auto
from qfun have q10:"Last(q1) = q1`0" unfolding Last_def using domain_of_fun by auto
from k have "0∈domain(q1)" using domain_of_fun empty_in_every_succ by auto
with iRes have "i`0 = q1`0" using restrict by auto
from qfun have "q1`0∈2" using apply_type[of q1 1 "λ_. 2"] empty_in_every_succ[OF nat_0I] by auto
with qq(3) A(2) have "⟨⟨q2,Last(q1)⟩,0⟩ ∈ transFun" using apply_Pair[OF funT, of "⟨q2,Last(q1)⟩"] q10 by auto
then have "q2∈2" "Last(q1) = 0" by auto
with `0∈domain(q1)` iRes q10 show "i`0 = 0" using restrict by auto
from q(2) qq(1) have "⟨⟨i,empty⟩,⟨q1,q2⟩⟩ ∈ r{0.*1}^*" by auto
then have "⟨⟨i,2⟩,⟨q1,q2⟩⟩ ∈ id(field(r{0.*1})) ∪ (r{0.*1}^* O r{0.*1})" using rtrancl_rev by auto
moreover
{
assume "⟨⟨i,2⟩,⟨q1,q2⟩⟩ ∈ id(field(r{0.*1}))"
then have "i=q1 ∧ q2=2" by auto
with `q2∈2` have False by auto
} ultimately
have "⟨⟨i,2⟩,⟨q1,q2⟩⟩ ∈ (r{0.*1}^* O r{0.*1})" by auto
then obtain z where z:"⟨⟨i,2⟩,z⟩ :r{0.*1}" "⟨z,⟨q1,q2⟩⟩:r{0.*1}^*" unfolding comp_def by auto
from z(2) have "z∈field(r{0.*1})" using rtrancl_type[of "r{0.*1}"] by auto
then obtain z1 z2 where zz:"z=⟨z1,z2⟩" "z1∈Lists(2)" "z2∈states" using dfsaFrom0To1.reduce_field(1)
by blast
from zz(1) z(1) have zzz:"z1=Init(i)" "z2=transFun`⟨2,Last(i)⟩"
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA] by auto
{
assume "Last(i) = 0"
with zzz(2) have "z2 = succ(2)" using apply_equality[OF _ funT] by auto
with zz(1) z(2) have "q2= succ(2)" using invariant_state_3 by auto
with `q2∈2` have False by auto
}
with z(1) show "Last(i) = 1" using last_type[of i 2]
unfolding DFSAExecutionRelation_def[OF finA dfsaFrom0To1.DFSA]
by auto
qed
text‹We conclude that this example constitutes
the language of binary strings starting in $0$
and ending in $1$›
theorem determine_strings:
shows "dfsaFrom0To1.LanguageDFSA = {i∈Lists(2). i`0 = 0 ∧ Last(i) = 1}"
using starts1ends0_DFSA_reduce_rev
starts1ends0_DFSA_reduce by blast
end
text‹We define the languages determined by a deterministic
finite state automaton as \textbf{regular}.›
definition
IsRegularLanguage ("_{is a regular language on}_") where
"Finite(Σ) ⟹ L{is a regular language on}Σ ≡ ∃S s t F. ((S,s,t,F){is an DFSA for alphabet}Σ) ∧ L=DetFinStateAuto.LanguageDFSA(S,s,t,F,Σ)"
text‹By definition, the language in the locale
is regular.›
corollary (in DetFinStateAuto) regular_intersect:
shows "LanguageDFSA{is a regular language on}Σ"
using IsRegularLanguage_def finite_alphabet DFSA by auto
text‹A regular language is a language.›
lemma regular_is_language:
assumes "Finite(Σ)"
and "L{is a regular language on}Σ"
shows "L{is a language with alphabet}Σ" unfolding IsALanguage_def[OF assms(1)]
proof-
from assms(2) obtain S s t F where "(S,s,t,F){is an DFSA for alphabet}Σ" "L=DetFinStateAuto.LanguageDFSA(S,s,t,F,Σ)"
unfolding IsRegularLanguage_def[OF assms(1)] by auto
then show "L⊆ Lists(Σ)"
unfolding DetFinStateAuto_def using assms(1) by auto
qed
subsection‹Operations on regular languages›
text‹The intersection of two regular languages
is a regular language.›
theorem regular_intersect:
assumes "Finite(Σ)"
and "L1{is a regular language on}Σ"
and "L2{is a regular language on}Σ"
shows "(L1∩L2) {is a regular language on}Σ"
proof-
from assms(1,2) obtain S1 s1 t1 F1 where l1:"(S1,s1,t1,F1){is an DFSA for alphabet}Σ"
"L1 = DetFinStateAuto.LanguageDFSA(S1,s1,t1,F1,Σ)"
using IsRegularLanguage_def by auto
then have l1:"(S1,s1,t1,F1){is an DFSA for alphabet}Σ"
"L1 = {i∈Lists(Σ). i <-D (S1,s1,t1,F1){in alphabet}Σ}"
using DetFinStateAuto_def assms(1) l1(1) by auto
from assms(1,3) obtain S2 s2 t2 F2 where l2:"(S2,s2,t2,F2){is an DFSA for alphabet}Σ"
"L2= DetFinStateAuto.LanguageDFSA(S2,s2,t2,F2,Σ)"
using IsRegularLanguage_def by auto
then have l2:"(S2,s2,t2,F2){is an DFSA for alphabet}Σ"
"L2 = {i∈Lists(Σ). i <-D (S2,s2,t2,F2){in alphabet}Σ}"
using DetFinStateAuto_def assms(1) l2(1) by auto
let ?S = "S1×S2"
let ?s = "⟨s1,s2⟩"
let ?t = "{⟨⟨⟨x1,x2⟩,y⟩,⟨t1`⟨x1,y⟩,t2`⟨x2,y⟩⟩⟩. ⟨⟨x1,x2⟩,y⟩ ∈ ?S×Σ}"
let ?F = "F1×F2"
let ?r = "DetFinStateAuto.r⇩D(?S,?s,?t,Σ)"
let ?r1 = "DetFinStateAuto.r⇩D(S1,s1,t1,Σ)"
let ?r2 = "DetFinStateAuto.r⇩D(S2,s2,t2,Σ)"
have D:"(?S,?s,?t,?F){is an DFSA for alphabet}Σ"
proof-
have A:"?s∈?S" using l1(1) l2(1) unfolding DFSA_def[OF assms(1)] by auto
have B:"?F ⊆ ?S" using l1(1) l2(1) unfolding DFSA_def[OF assms(1)] by auto
have "function(?t)" unfolding function_def by auto
moreover have "?S×Σ ⊆ domain(?t)" by auto
moreover
{
fix x1 x2 y assume as:"⟨⟨x1,x2⟩,y⟩ ∈ ?S × Σ"
then have "t1`⟨x1,y⟩∈S1" "t2`⟨x2,y⟩∈S2" using apply_type
l1(1) l2(1) unfolding DFSA_def[OF assms(1)] by auto
then have "⟨t1`⟨x1,y⟩,t2`⟨x2,y⟩⟩∈?S" by auto
}
then have "{⟨⟨⟨x1,x2⟩,y⟩,⟨t1`⟨x1,y⟩,t2`⟨x2,y⟩⟩⟩. ⟨⟨x1,x2⟩,y⟩ ∈ (S1 × S2) × Σ} ∈ Pow((?S×Σ)×?S)" by auto
ultimately have C:"?t:?S×Σ → ?S" unfolding Pi_def by auto
have "Finite(?S)" using Finite1_L12[of S1 S2] Fin_into_Finite Finite_into_Fin
l1(1) l2(1) unfolding DFSA_def[OF assms(1)] by auto
with A B C show ?thesis unfolding DFSA_def[OF assms(1)] by auto
qed
then have DFSA0:"DetFinStateAuto(?S,?s,?t,?F,Σ)" unfolding DetFinStateAuto_def using assms(1) by auto
have RR:"⋀m yy zz. m∈NELists(Σ) ⟹ ⟨⟨m,s1,s2⟩,⟨0,yy,zz⟩⟩:?r^* ⟹ ⟨⟨m,s1⟩,⟨0,yy⟩⟩:?r1^* ∧ ⟨⟨m,s2⟩,⟨0,zz⟩⟩:?r2^*"
proof
fix m yy zz
assume as:"⟨⟨m,s1,s2⟩,⟨0,yy,zz⟩⟩:?r^*" "m∈NELists(Σ)"
note as(2)
moreover have "s1∈S1" "s2∈S2" using l1(1) l2(1) unfolding DFSA_def[OF assms(1)] by auto
ultimately have "⟨m,s1⟩ : field(?r1)" "⟨m,s2⟩ : field(?r2)" using DetFinStateAuto.reduce_field(2)[of S1 s1 t1 F1 Σ] assms(1) l1(1) l2(1)
DetFinStateAuto.reduce_field(2)[of S2 s2 t2 F2 Σ] unfolding DetFinStateAuto_def by auto
then have "⟨⟨m,s1⟩,⟨m,s1⟩⟩:?r1^*" "⟨⟨m,s2⟩,⟨m,s2⟩⟩:?r2^*" using rtrancl_refl by auto moreover
{
fix bb cc assume as:"⟨⟨m,s1,s2⟩,bb⟩:?r^*" "⟨bb,cc⟩:?r" "⟨⟨m,s1⟩,fst(bb),fst(snd(bb))⟩:?r1^* ∧ ⟨⟨m,s2⟩,fst(bb),snd(snd(bb))⟩:?r2^*"
from this(2) have "bb∈field(?r)" "cc∈field(?r)" using
fieldI1[of bb cc ?r] fieldI2[of bb cc ?r] by auto
then obtain bbL bb1 bb2 ccL cc1 cc2 where bbcc:"bb=⟨bbL,bb1,bb2⟩" "cc=⟨ccL,cc1,cc2⟩"
"bbL∈Lists(Σ)" "ccL∈Lists(Σ)" "cc1∈S1" "cc2∈S2" "bb1∈S1" "bb2∈S2"
using DetFinStateAuto.reduce_field(1)[OF DFSA0] by blast
with as(3) have "⟨⟨m,s1⟩,bbL,bb1⟩:?r1^*" by auto
from as(2) bbcc have C:"ccL=Init(bbL)" "⟨cc1,cc2⟩=?t`⟨⟨bb1,bb2⟩,Last(bbL)⟩" "bbL:NELists(Σ)"
unfolding DFSAExecutionRelation_def[OF assms(1) D] by auto
from this(2,3) bbcc(8,7) have "⟨cc1,cc2⟩=⟨t1`⟨bb1,Last(bbL)⟩,t2`⟨bb2,Last(bbL)⟩⟩" using last_type[of bbL Σ]
apply_equality[of "⟨⟨bb1,bb2⟩,Last(bbL)⟩" _ ?t] D
unfolding DFSA_def[OF assms(1)] by auto
then have "cc1=t1`⟨bb1,Last(bbL)⟩" "cc2=t2`⟨bb2,Last(bbL)⟩" by auto
with C(1,3) bbcc(8,7) have "⟨⟨bbL,bb1⟩,⟨ccL,cc1⟩⟩:?r1" "⟨⟨bbL,bb2⟩,⟨ccL,cc2⟩⟩:?r2"
unfolding DFSAExecutionRelation_def[OF assms(1) l1(1)]
DFSAExecutionRelation_def[OF assms(1) l2(1)] by auto
with as(3) bbcc(1,2) have "⟨⟨m,s1⟩,⟨ccL,cc1⟩⟩∈?r1^*" "⟨⟨m,s2⟩,⟨ccL,cc2⟩⟩∈?r2^*"
using rtrancl_into_trancl1[of _ _ ?r2, THEN trancl_into_rtrancl]
rtrancl_into_trancl1[of _ _ ?r1, THEN trancl_into_rtrancl]
by auto
then have "⟨⟨m,s1⟩,⟨fst(cc),fst(snd(cc))⟩⟩:?r1^* ∧ ⟨⟨m,s2⟩,⟨fst(cc),snd(snd(cc))⟩⟩:?r2^*"
using bbcc(2) by auto
} moreover note as
rtrancl_induct[of "⟨m,s1,s2⟩" "⟨0,yy,zz⟩" "?r" "λb. ⟨⟨m,s1⟩,⟨fst(b),fst(snd(b))⟩⟩:?r1^* ∧ ⟨⟨m,s2⟩,⟨fst(b),snd(snd(b))⟩⟩:?r2^*"]
ultimately show "⟨⟨m, s1⟩, 0, yy⟩ ∈ ?r1^*" "⟨⟨m, s2⟩, 0, zz⟩ ∈ ?r2^*" by auto
qed
{
fix m assume "m∈{i∈Lists(Σ). i <-D (?S,?s,?t,?F){in alphabet}Σ}"
then have M:"m∈Lists(Σ)" "m <-D (?S,?s,?t,?F){in alphabet}Σ" by auto
{
assume m0:"m=0"
from m0 M have "0 <-D (?S,?s,?t,?F){in alphabet}Σ" by auto
then obtain yy zz where "⟨⟨0,s1,s2⟩,⟨0,yy,zz⟩⟩:?r^* ∨ ?s:?F" "⟨yy,zz⟩:?F" using m0
DFSASatisfy_def[OF assms(1) D M(1)] by auto moreover
{
fix y z
assume "⟨⟨0,s1,s2⟩,y⟩ ∈ ?r^*" "⟨y,z⟩ ∈ ?r" "y = ⟨0,s1,s2⟩"
from this(2,3) have "0∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF assms(1) D]
by auto
then have False unfolding NELists_def Pi_def by auto
then have "z=⟨0,s1,s2⟩" by auto
}
ultimately have "?s:?F" using rtrancl_induct[of "⟨0,?s⟩" "⟨0,yy,zz⟩" ?r
"λq. q=⟨0,?s⟩"] by auto
then have "m <-D (S1,s1,t1,F1){in alphabet}Σ" "m <-D (S2,s2,t2,F2){in alphabet}Σ"
using DFSASatisfy_def[OF assms(1) l1(1) M(1)] DFSASatisfy_def[OF assms(1) l2(1) M(1)]
using m0 by auto
} moreover
{
assume m0:"m≠0"
with M(2) obtain yy zz where F:"⟨⟨m,s1,s2⟩,⟨0,yy,zz⟩⟩:?r^*" "⟨yy,zz⟩:?F" using
DFSASatisfy_def[OF assms(1) D M(1)] by auto
from m0 M(1) have "m∈NELists(Σ)" using non_zero_List_func_is_NEList by auto
then have RR:"⋀yy zz. ⟨⟨m,s1,s2⟩,⟨0,yy,zz⟩⟩:?r^* ⟹ ⟨⟨m,s1⟩,⟨0,yy⟩⟩:?r1^* ∧ ⟨⟨m,s2⟩,⟨0,zz⟩⟩:?r2^*"
using RR by auto
with F have "∃q∈F1. ⟨⟨m, s1⟩, 0,q⟩∈?r1^*" "∃q∈F2. ⟨⟨m, s2⟩, 0,q⟩∈?r2^*" by auto
then have "m <-D (S1,s1,t1,F1){in alphabet}Σ" "m <-D (S2,s2,t2,F2){in alphabet}Σ"
using DFSASatisfy_def[OF assms(1) l1(1) M(1)] DFSASatisfy_def[OF assms(1) l2(1) M(1)]
using m0 by auto
}
ultimately have "m <-D (S1,s1,t1,F1){in alphabet}Σ" "m <-D (S2,s2,t2,F2){in alphabet}Σ" by auto
}
then have S1:"{i ∈ Lists(Σ). i <-D (?S,?s,?t,?F){in alphabet}Σ} ⊆ L1∩L2" using l1(2) l2(2) by auto
{
fix m assume "m∈L1∩L2"
with l1(2) l2(2) have M:"m∈Lists(Σ)" "m <-D (S1,s1,t1,F1){in alphabet}Σ" "m <-D (S2,s2,t2,F2){in alphabet}Σ"
by auto
then obtain f1 f2 where ff:"f1∈F1" "f2∈F2" "⟨⟨m,s1⟩,0,f1⟩∈?r1^* ∨ (m=0 ∧ s1∈F1)" "⟨⟨m,s2⟩,0,f2⟩∈?r2^* ∨ (m=0 ∧ s2∈F2)"
unfolding DFSASatisfy_def[OF assms(1) l1(1) M(1)] DFSASatisfy_def[OF assms(1) l2(1) M(1)] by auto
{
fix y z
assume "⟨⟨0,s1⟩,y⟩ ∈ ?r1^*" "⟨y,z⟩ ∈ ?r1" "y = ⟨0,s1⟩"
from this(2,3) have "0∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF assms(1) l1(1)]
by auto
then have False unfolding NELists_def Pi_def by auto
then have "z=⟨0,s1⟩" by auto
}
with ff(1,3) have "m=0 ⟶ s1∈F1" using rtrancl_induct[of "⟨m,s1⟩" "⟨0,f1⟩" ?r1 "λq. q=⟨0,s1⟩"] by auto
moreover
{
fix y z
assume "⟨⟨0,s2⟩,y⟩ ∈ ?r2^*" "⟨y,z⟩ ∈ ?r2" "y = ⟨0,s2⟩"
from this(2,3) have "0∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF assms(1) l2(1)]
by auto
then have False unfolding NELists_def Pi_def by auto
then have "z=⟨0,s2⟩" by auto
}
with ff(2,4) have "m=0 ⟶ s2∈F2" using rtrancl_induct[of "⟨m,s2⟩" "⟨0,f2⟩" ?r2 "λq. q=⟨0,s2⟩"] by auto
moreover
{
assume m0:"m≠0"
with ff(3,4) have A:"⟨⟨m,s1⟩,0,f1⟩:?r1^*" "⟨⟨m,s2⟩,0,f2⟩:?r2^*" by auto
from this(1) have "⟨m,s1⟩:field(?r1)" using rtrancl_type by auto
then have "⟨m,s1⟩:Lists(Σ)×S1" using DetFinStateAuto.reduce_field(1)[of S1 s1 t1 F1 Σ] l1(1) unfolding DetFinStateAuto_def
using assms(1) by auto
with m0 have "m∈NELists(Σ)" "s1∈S1" "s2∈S2" using l1(1) l2(1) non_zero_List_func_is_NEList
unfolding DFSA_def[OF assms(1)] by auto
then have "⟨m,s1,s2⟩:NELists(Σ)×?S" by auto
then have "⟨m,s1,s2⟩:field(?r)" using DetFinStateAuto.reduce_field(2)[OF DFSA0] by auto
then have K:"⟨⟨m,s1,s2⟩,⟨m,s1,s2⟩⟩:?r^*" using rtrancl_refl by auto
with `s2∈S2` have "∃f2∈S2. ⟨⟨m,s1,s2⟩,⟨m,s1,f2⟩⟩:?r^*" by auto moreover
{
fix y z
assume as:"⟨⟨m,s1⟩,y⟩:?r1^*" "⟨y,z⟩:?r1" "∃f2∈S2. ⟨⟨m,s1,s2⟩,⟨fst(y),snd(y),f2⟩⟩:?r^*"
from as(2) obtain yL y1 where y:"y=⟨yL,y1⟩" "z=⟨Init(yL),t1`⟨y1,Last(yL)⟩⟩"
"yL∈NELists(Σ)" "y1:S1" unfolding DFSAExecutionRelation_def[OF assms(1) l1(1)] by auto
with as(3) obtain ff2 where sf:"ff2∈S2" "⟨⟨m,s1,s2⟩,⟨yL,y1,ff2⟩⟩:?r^*" by auto
from this(1) y(3,4) have "⟨⟨yL,y1,ff2⟩,⟨Init(yL),?t`⟨⟨y1,ff2⟩,Last(yL)⟩⟩⟩ ∈ ?r"
unfolding DFSAExecutionRelation_def[OF assms(1) D] by auto moreover
have funT:"?t:?S×Σ → ?S" using D unfolding DFSA_def[OF assms(1)] by auto
with y(3,4) sf(1) have "?t`⟨⟨y1,ff2⟩,Last(yL)⟩ =⟨t1`⟨y1,Last(yL)⟩,t2`⟨ff2,Last(yL)⟩⟩"
using apply_equality[of "⟨⟨y1,ff2⟩,Last(yL)⟩" _ ?t "?S×Σ" "λ_. ?S"] last_type by auto
ultimately have "⟨⟨yL,y1,ff2⟩,⟨Init(yL),⟨t1`⟨y1,Last(yL)⟩,t2`⟨ff2,Last(yL)⟩⟩⟩⟩ ∈ ?r" by auto
with y(2) have "⟨⟨yL,y1,ff2⟩,⟨fst(z),⟨snd(z),t2`⟨ff2,Last(yL)⟩⟩⟩⟩ ∈ ?r" by auto
with sf(2) have "⟨⟨m,s1,s2⟩,⟨fst(z),⟨snd(z),t2`⟨ff2,Last(yL)⟩⟩⟩⟩:?r^*" using
rtrancl_into_rtrancl by auto
moreover from sf(1) have "t2`⟨ff2,Last(yL)⟩ ∈ S2" using l2(1)
apply_type[of t2 "S2×Σ" "λ_. S2"] last_type[OF y(3)] unfolding DFSA_def[OF assms(1)]
by auto
ultimately have "∃f2∈S2. ⟨⟨m,s1,s2⟩,⟨fst(z),⟨snd(z),f2⟩⟩⟩:?r^*"
using sf(1) by auto
} moreover note A(1)
ultimately have "∃f2∈S2. ⟨⟨m,s1,s2⟩,⟨0,⟨f1,f2⟩⟩⟩:?r^*"
using rtrancl_induct[of "⟨m,s1⟩" "⟨0,f1⟩" ?r1 "λq. ∃f2∈S2. ⟨⟨m,s1,s2⟩,⟨fst(q),snd(q),f2⟩⟩:?r^*"]
by auto
then obtain uu where uu:"uu∈S2" "⟨⟨m,s1,s2⟩,⟨0,⟨f1,uu⟩⟩⟩:?r^*" by auto
from K `s1∈S1` have "∃f1∈S1. ⟨⟨m,s1,s2⟩,⟨m,f1,s2⟩⟩:?r^*" by auto moreover
{
fix y z
assume as:"⟨⟨m,s2⟩,y⟩:?r2^*" "⟨y,z⟩:?r2" "∃f1∈S1. ⟨⟨m,s1,s2⟩,⟨fst(y),f1,snd(y)⟩⟩:?r^*"
from as(2) obtain yL y1 where y:"y=⟨yL,y1⟩" "z=⟨Init(yL),t2`⟨y1,Last(yL)⟩⟩"
"yL∈NELists(Σ)" "y1:S2" unfolding DFSAExecutionRelation_def[OF assms(1) l2(1)] by auto
with as(3) obtain ff2 where sf:"ff2∈S1" "⟨⟨m,s1,s2⟩,⟨yL,ff2,y1⟩⟩:?r^*" by auto
from this(1) y(3,4) have "⟨⟨yL,ff2,y1⟩,⟨Init(yL),?t`⟨⟨ff2,y1⟩,Last(yL)⟩⟩⟩ ∈ ?r"
unfolding DFSAExecutionRelation_def[OF assms(1) D] by auto moreover
have funT:"?t:?S×Σ → ?S" using D unfolding DFSA_def[OF assms(1)] by auto
with y(3,4) sf(1) have "?t`⟨⟨ff2,y1⟩,Last(yL)⟩ =⟨t1`⟨ff2,Last(yL)⟩,t2`⟨y1,Last(yL)⟩⟩"
using apply_equality[of "⟨⟨ff2,y1⟩,Last(yL)⟩" _ ?t "?S×Σ" "λ_. ?S"] last_type by auto
ultimately have "⟨⟨yL,ff2,y1⟩,⟨Init(yL),⟨t1`⟨ff2,Last(yL)⟩,t2`⟨y1,Last(yL)⟩⟩⟩⟩ ∈ ?r" by auto
with y(2) have "⟨⟨yL,ff2,y1⟩,⟨fst(z),⟨t1`⟨ff2,Last(yL)⟩,snd(z)⟩⟩⟩ ∈ ?r" by auto
with sf(2) have "⟨⟨m,s1,s2⟩,⟨fst(z),⟨t1`⟨ff2,Last(yL)⟩,snd(z)⟩⟩⟩:?r^*" using
rtrancl_into_rtrancl by auto
moreover from sf(1) have "t1`⟨ff2,Last(yL)⟩ ∈ S1" using l1(1)
apply_type[of t1 "S1×Σ" "λ_. S1"] last_type[OF y(3)] unfolding DFSA_def[OF assms(1)]
by auto
ultimately have "∃f2∈S1. ⟨⟨m,s1,s2⟩,⟨fst(z),⟨f2,snd(z)⟩⟩⟩:?r^*"
using sf(1) by auto
} moreover note A(2)
ultimately have "∃f1∈S1. ⟨⟨m,s1,s2⟩,⟨0,⟨f1,f2⟩⟩⟩:?r^*"
using rtrancl_induct[of "⟨m,s2⟩" "⟨0,f2⟩" ?r2 "λq. ∃f1∈S1. ⟨⟨m,s1,s2⟩,⟨fst(q),f1,snd(q)⟩⟩:?r^*"]
by auto
then obtain vv where vv:"vv∈S1" "⟨⟨m,s1,s2⟩,⟨0,⟨vv,f2⟩⟩⟩:?r^*" by auto
from uu(2) vv(2) have "f1=vv" "uu=f2" using DetFinStateAuto.relation_deteministic[OF DFSA0,
of m ?s 0 ] by auto
from this(1) vv(2) ff(1,2) have "m <-D (?S,?s,?t,?F){in alphabet}Σ"
unfolding DFSASatisfy_def[OF assms(1) D M(1)] by auto
}
ultimately have "m <-D (?S,?s,?t,?F){in alphabet}Σ"
unfolding DFSASatisfy_def[OF assms(1) D M(1)] by auto
}
with l1(2) l2(2) have "L1∩L2 ⊆ {i ∈ Lists(Σ). i <-D (?S,?s,?t,?F){in alphabet}Σ}" by auto
with S1 have "{i ∈ Lists(Σ). i <-D (?S,?s,?t,?F){in alphabet}Σ} = L1∩L2" by auto
then have "L1∩L2 = DetFinStateAuto.LanguageDFSA(?S,?s,?t,?F,Σ)" by auto
with D have "∃S s t F. ((S,s,t,F){is an DFSA for alphabet}Σ) ∧ L1∩L2 = DetFinStateAuto.LanguageDFSA(S,s,t,F,Σ)"
using exI[of "λh. ((?S,?s,?t,h){is an DFSA for alphabet}Σ) ∧ L1∩L2 = DetFinStateAuto.LanguageDFSA(?S,?s,?t,h,Σ)" ?F]
using exI[of "λm. ∃h. ((?S,?s,m,h){is an DFSA for alphabet}Σ) ∧ L1∩L2 = DetFinStateAuto.LanguageDFSA(?S,?s,m,h,Σ)" ?t]
using exI[of "λn. ∃m h. ((?S,n,m,h){is an DFSA for alphabet}Σ) ∧ L1∩L2 = DetFinStateAuto.LanguageDFSA(?S,n,m,h,Σ)" ?s]
using exI[of "λp. ∃n m h. ((p,n,m,h){is an DFSA for alphabet}Σ) ∧ L1∩L2 = DetFinStateAuto.LanguageDFSA(p,n,m,h,Σ)" ?S]
by auto
with assms(2,3) show ?thesis unfolding IsRegularLanguage_def[OF assms(1)] IsALanguage_def[OF assms(1)] by auto
qed
text‹The complement of a regular language
is a regular language.›
theorem regular_opp:
assumes "Finite(Σ)"
and "L{is a regular language on}Σ"
shows "(Lists(Σ)-L) {is a regular language on}Σ"
proof-
from assms(1,2) obtain S s t F where l:"(S,s,t,F){is an DFSA for alphabet}Σ"
"L=DetFinStateAuto.LanguageDFSA(S,s,t,F,Σ)" unfolding IsRegularLanguage_def[OF assms(1)] by auto
then have l:"(S,s,t,F){is an DFSA for alphabet}Σ"
"L={i∈Lists(Σ). i <-D (S,s,t,F){in alphabet}Σ}"
using DetFinStateAuto_def assms(1) l(1) by auto
have "Lists(Σ)-L ⊆ Lists(Σ)" by auto
then have "(Lists(Σ)-L) {is a language with alphabet} Σ"
unfolding IsALanguage_def[OF assms(1)] by auto
let ?F = "S-F"
let ?r = "DetFinStateAuto.r⇩D(S,s,t,Σ)"
from l(1) have D:"(S,s,t,?F){is an DFSA for alphabet}Σ" unfolding DFSA_def[OF assms(1)]
by auto
with assms(1) have D0:"DetFinStateAuto(S,s,t,?F,Σ)" unfolding DetFinStateAuto_def by auto
{
fix m assume "m∈{i∈Lists(Σ). i <-D (S,s,t,?F){in alphabet}Σ}"
then have M:"m∈Lists(Σ)" "m <-D (S,s,t,?F){in alphabet}Σ" by auto
{
assume "m∈L"
with l(2) have MM:"m <-D (S,s,t,F){in alphabet}Σ" by auto
{
assume as:"m=0"
from MM(1) as(1) obtain yy where "⟨⟨0,s⟩,⟨0,yy⟩⟩:?r^* ∨ s:F" "yy∈F" unfolding
DFSASatisfy_def[OF assms(1) l(1) M(1)] by auto moreover
{
fix y z
assume "⟨⟨0,s⟩,y⟩ ∈ ?r^*" "⟨y,z⟩ ∈ ?r" "y = ⟨0,s⟩"
from this(2,3) have "0∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF assms(1) l(1)]
by auto
then have False unfolding NELists_def Pi_def by auto
then have "z=⟨0,s⟩" by auto
}
ultimately have sf:"s:F" using rtrancl_induct[of "⟨0,s⟩" "⟨0,yy⟩" ?r "λq. q=⟨0,s⟩"] by auto
from M(2) as(1) obtain yy where "⟨⟨0,s⟩,⟨0,yy⟩⟩:?r^* ∨ s:S-F" "yy∈S-F" unfolding
DFSASatisfy_def[OF assms(1) D M(1)] by auto moreover
{
fix y z
assume "⟨⟨0,s⟩,y⟩ ∈ ?r^*" "⟨y,z⟩ ∈ ?r" "y = ⟨0,s⟩"
from this(2,3) have "0∈NELists(Σ)" unfolding DFSAExecutionRelation_def[OF assms(1) D]
by auto
then have False unfolding NELists_def Pi_def by auto
then have "z=⟨0,s⟩" by auto
}
ultimately have "s:S-F" using rtrancl_induct[of "⟨0,s⟩" "⟨0,yy⟩" ?r "λq. q=⟨0,s⟩"] by auto
with sf have False by auto
}
then have m0:"m≠0" by auto
with MM obtain q1 where q1:"q1∈F" "⟨⟨m, s⟩, 0, q1⟩ ∈ ?r^*"
unfolding DFSASatisfy_def[OF assms(1) l(1) M(1)] by auto
from m0 M(2) obtain q2 where q2:"q2∈S-F" "⟨⟨m, s⟩, 0, q2⟩ ∈ ?r^*"
unfolding DFSASatisfy_def[OF assms(1) D M(1)] by auto
from q1(2) q2(2) have "q1=q2" using DetFinStateAuto.relation_deteministic[OF D0,
of m s 0] by auto
with q1(1) q2(1) have False by auto
}
then have "m∈Lists(Σ) - L" using M(1) by auto
}
then have S:"{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ} ⊆ Lists(Σ) - L" by auto
{
fix m assume "m∈Lists(Σ)-L"
then have m:"m∈Lists(Σ)" "m <-D (S,s,t,F){in alphabet}Σ ⟹ False" using l(2)
by auto
from this(1) have R:"m = 0 ∨ (∃q∈S. ⟨⟨m,s⟩,0,q⟩ ∈ ?r^*)"
using non_zero_List_func_is_NEList
DetFinStateAuto.endpoint_exists[OF D0] by auto
{
assume as:"m=0" "s∈F"
with m(1) have "m <-D (S,s,t,F){in alphabet}Σ" unfolding
DFSASatisfy_def[OF assms(1) l(1) m(1)] by auto
with m(2) have False by auto
then have "m∈{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
} moreover
{
assume as:"m=0" "s∉F"
then have "m=0" "s∈S-F" using DetFinStateAuto.DFSA_dest(1)[OF D0] by auto
then have "m <-D (S,s,t,S - F){in alphabet}Σ" unfolding DFSASatisfy_def[OF assms(1) D m(1)] by auto
with m(1) have "m∈{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
} ultimately
have "m =0 ⟶ m∈{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto moreover
{
assume "∃q∈S. ⟨⟨m,s⟩,0,q⟩ ∈ ?r^*"
then obtain q where q:"⟨⟨m,s⟩,0,q⟩ ∈ ?r^*" "q∈S" by auto
{
assume "q∈F"
with q(1) have "m <-D (S,s,t,F){in alphabet}Σ" unfolding DFSASatisfy_def[OF assms(1) l(1) m(1)] by auto
with m(2) have False by auto
}
with q have "∃q∈S-F. ⟨⟨m,s⟩,0,q⟩ ∈ ?r^*" by auto
then have "m <-D (S,s,t,S-F){in alphabet}Σ" unfolding DFSASatisfy_def[OF assms(1) D m(1)] by auto
with m(1) have "m∈{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
} moreover note R
ultimately have "m∈{i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
}
then have "Lists(Σ) -L ⊆ {i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
with S have "Lists(Σ) -L = {i ∈ Lists(Σ) . i <-D (S,s,t,S - F){in alphabet}Σ}" by auto
then have "Lists(Σ) -L = DetFinStateAuto.LanguageDFSA(S,s,t,S-F,Σ)" .
then show ?thesis unfolding IsRegularLanguage_def[OF assms(1)] using D by auto
qed
text‹The union of two regular languages
is a regular language.›
theorem regular_union:
assumes "Finite(Σ)"
and "L1{is a regular language on}Σ"
and "L2{is a regular language on}Σ"
shows "(L1∪L2) {is a regular language on}Σ"
proof-
have "L1∪L2 = Lists(Σ)-((Lists(Σ)-L1)∩(Lists(Σ)-L2))" using regular_is_language[OF assms(1)]
assms(2,3) unfolding IsALanguage_def[OF assms(1)] by auto
moreover
have A:"(Lists(Σ)-L1) {is a regular language on}Σ" using regular_opp[OF assms(1,2)].
have B:"(Lists(Σ)-L2) {is a regular language on}Σ" using regular_opp[OF assms(1,3)].
from A B have "((Lists(Σ)-L1)∩(Lists(Σ)-L2)) {is a regular language on}Σ" using regular_intersect[OF assms(1)] by auto
then have "(Lists(Σ)-((Lists(Σ)-L1)∩(Lists(Σ)-L2))) {is a regular language on}Σ" using regular_opp[OF assms(1)] by auto
ultimately show ?thesis by auto
qed
text‹Another natural operation on words is concatenation,
hence we can defined the concatenated language as
the set of concatenations of words of one language
with words of another.›
definition concat where
"L1 {is a language with alphabet}Σ ⟹ L2 {is a language with alphabet}Σ
⟹ concat(L1,L2) = {Concat(w1,w2). ⟨w1,w2⟩∈L1×L2}"
text‹The result of concatenating two languages is a language.›
lemma concat_language:
assumes "Finite(Σ)"
and "L1 {is a language with alphabet}Σ"
and "L2 {is a language with alphabet}Σ"
shows "concat(L1,L2) {is a language with alphabet}Σ"
proof-
{
fix w assume "w∈concat(L1,L2)"
then obtain w1 w2 where w:"w=Concat(w1,w2)" "w1∈L1" "w2∈L2" unfolding concat_def[OF assms(2,3)]
by auto
from this(2,3) assms(2,3) obtain n1 n2 where "n1∈nat" "n2∈nat" "w1:n1→Σ" "w2:n2→Σ"
unfolding IsALanguage_def[OF assms(1)] Lists_def by blast
then have "Concat(w1,w2):n1#+n2 → Σ" "n1#+n2 ∈nat" using concat_props(1) by auto
with w(1) have "w∈Lists(Σ)" unfolding Lists_def by auto
}
then show ?thesis unfolding IsALanguage_def[OF assms(1)] by auto
qed
subsection‹Non-deterministic finite state automata›
text‹We have reached a point where it is not easy
to realize a concatenated language of two regular
languages as a regular language. Nevertheless,
if we extend our instruments to allow non-determinism
it is much easier.
The cost, a priori, is that our class of languages
would be larger since our automata are more generic.›
text‹The non-determinism is introduced by allowing
the transition function to return not just a state,
but more than one or even none.›
definition
NFSA ("'(_,_,_,_'){is an NFSA for alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an NFSA for alphabet}Σ ≡ Finite(S) ∧ s⇩0∈S ∧ F⊆S ∧ t:S×Σ→Pow(S)"
text‹The transition relation is then realized by considering
all possible steps the transition function returns.›
definition
NFSAExecutionRelation ("{reduce N-relation} '(_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an NFSA for alphabet}Σ ⟹
{reduce N-relation}(S,s⇩0,t){in alphabet}Σ ≡ {⟨⟨w,Q⟩,⟨Init(w),⋃{t`⟨s,Last(w)⟩. s∈Q}⟩⟩. ⟨w,Q⟩∈NELists(Σ)×Pow(S)}"
text‹The full reduction is conceived as one of those possible
paths reaching a final state.›
definition
NFSASatisfy ("_ <-N '(_,_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an NFSA for alphabet}Σ ⟹ i∈Lists(Σ) ⟹
i <-N (S,s⇩0,t,F){in alphabet}Σ ≡ (∃q∈Pow(S). (q∩F≠0 ∧ ⟨⟨i,{s⇩0}⟩,⟨0,q⟩⟩∈ ({reduce N-relation}(S,s⇩0,t){in alphabet}Σ)^*)) ∨ (i = 0 ∧ s⇩0∈F)"
text‹An extra generalization can be consider
if we allow the transition relation to go forward
without consuming elements from the word. This
is implemented as allowing @{term Σ} to symbolize
an step without the word being touched. We might
call it a @{term Σ} transition or a $\varepsilon$-transition.›
definition
FullNFSA ("'(_,_,_,_'){is an ε-NFSA for alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an ε-NFSA for alphabet}Σ ≡ Finite(S) ∧ s⇩0∈S ∧ F⊆S ∧ t:S×succ(Σ)→Pow(S)"
text‹The closure of a set of states can then be
viewed as all the states reachable from that set
with a transition of type @{term Σ}.›
definition
EpsilonClosure ("ε-cl") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an ε-NFSA for alphabet}Σ ⟹ E⊆S
⟹ ε-cl(S,t,Σ,E) ≡ ⋃{P∈Pow(S). ⟨E,P⟩∈({⟨Q,{s∈S. ∃q∈Q. t`⟨q,Σ⟩ = s}⟩. Q∈Pow(S)}^*)}"
text‹The reduction relation is then extended
by considering any such transitions.›
definition
FullNFSAExecutionRelation ("{reduce ε-N-relation} '(_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an ε-NFSA for alphabet}Σ ⟹
{reduce ε-N-relation}(S,s⇩0,t){in alphabet}Σ ≡ {⟨⟨w,Q⟩,⟨Init(w),ε-cl(S,t,Σ,⋃{t`⟨s,Last(w)⟩. s∈Q})⟩⟩. ⟨w,Q⟩∈NELists(Σ)×Pow(S)}"
text‹The full reduction of a word is similar to that
of the automata without $\varepsilon$-transitions.›
definition
FullNFSASatisfy ("_ <-ε-N '(_,_,_,_'){in alphabet}_") where
"Finite(Σ) ⟹ (S,s⇩0,t,F){is an ε-NFSA for alphabet}Σ ⟹ i∈Lists(Σ) ⟹
i <-ε-N (S,s⇩0,t,F){in alphabet}Σ ≡ (∃q∈Pow(S). (q∩F≠0 ∧ ⟨⟨i,{s⇩0}⟩,⟨0,q⟩⟩∈ ({reduce ε-N-relation}(S,s⇩0,t){in alphabet}Σ)^*)) ∨ (i = 0 ∧ s⇩0∈F)"
text‹We define a locale to create some notation›
locale NonDetFinStateAuto =
fixes S and s⇩0 and t and F and Σ
assumes finite_alphabet: "Finite(Σ)"
assumes NFSA: "(S,s⇩0,t,F){is an NFSA for alphabet}Σ"
text‹Notation for the transition relation›
abbreviation (in NonDetFinStateAuto) nd_rel ("r⇩N")
where "r⇩N ≡ {reduce N-relation}(S,s⇩0,t){in alphabet}Σ"
text‹Notation for the language generated by the
non-deterministic automaton›
abbreviation (in NonDetFinStateAuto) LanguageNFSA
where "LanguageNFSA ≡ {i∈Lists(Σ). i<-N (S,s⇩0,t,F){in alphabet}Σ}"
subsection‹Equivalence of Non-deterministic and Deterministic
Finite State Automata›
text‹We will show that the non-deterministic
automata generate languages that are regular
in the sense that there is a deterministic automaton
that generates the same language.›
text‹The transition function of the deterministic
automata we will construct›
definition (in NonDetFinStateAuto) tPow where
"tPow ≡ {⟨⟨U,u⟩,(⋃v∈U. t ` ⟨v, u⟩)⟩. ⟨U,u⟩∈Pow(S)×Σ}"
text‹The transition relation of the deterministic
automata we will construct›
definition (in NonDetFinStateAuto) rPow where
"rPow ≡ DetFinStateAuto.r⇩D(Pow(S),{s⇩0},tPow,Σ)"
text‹We show that we do have a deterministic automaton›
sublocale NonDetFinStateAuto < dfsa:DetFinStateAuto "Pow(S)" "{s⇩0}" tPow "{Q∈Pow(S). Q∩F ≠ 0}" Σ
unfolding DetFinStateAuto_def DFSA_def[OF finite_alphabet] unfolding tPow_def
apply safe using finite_alphabet apply simp
using NFSA unfolding NFSA_def[OF finite_alphabet]
apply simp using NFSA unfolding NFSA_def[OF finite_alphabet]
apply simp unfolding Pi_def function_def apply auto
proof-
fix b y x v assume as:"y ∈ Σ" "b ⊆ S" "v ∈ b" "x ∈ t ` ⟨v, y⟩"
from as(2,3) have v:"v∈S" by auto
have "t ∈ S × Σ → Pow(S)" using NFSA
unfolding NFSA_def[OF finite_alphabet] by auto
with as(1,4) v show "x∈S" using apply_type[of t "S×Σ" "λ_. Pow(S)" "⟨v,y⟩"]
by auto
qed
text‹The two automata have the same relations
associated with them. ›
text‹First, we show that if the non-deterministic
automaton produces a reduction step to a word, then the deterministic one
we constructed does the same reduction step.›
lemma (in NonDetFinStateAuto) nd_impl_det:
assumes "⟨⟨w,Q⟩,⟨u,G⟩⟩∈r⇩N"
shows "⟨⟨w,Q⟩,⟨u,G⟩⟩∈rPow"
proof-
from assms have w:"w∈NELists(Σ)" "u=Init(w)" "Q∈Pow(S)" "G=(⋃s∈Q. t`⟨s,Last(w)⟩)"
unfolding NFSAExecutionRelation_def[OF finite_alphabet NFSA] by auto
then have "tPow`⟨Q,Last(w)⟩ = (⋃s∈Q. t`⟨s,Last(w)⟩) ⟹ ?thesis"
unfolding DFSAExecutionRelation_def[OF finite_alphabet dfsa.DFSA] rPow_def
by auto
moreover have "⟨⟨Q,Last(w)⟩,⋃s∈Q. t`⟨s,Last(w)⟩⟩:tPow" using last_type[OF w(1)] w(3)
unfolding tPow_def by auto
ultimately show ?thesis using apply_equality[OF _ dfsa.DFSA_dest(3), of "⟨Q,Last(w)⟩" "⋃s∈Q. t`⟨s,Last(w)⟩"]
by blast
qed
text‹Next, we show that if the deterministic
automaton produces a reduction step to a word, then the non-deterministic one
we constructed does the same reduction step.›
lemma (in NonDetFinStateAuto) det_impl_nd:
assumes "⟨⟨w,Q⟩,⟨u,G⟩⟩∈rPow"
shows "⟨⟨w,Q⟩,⟨u,G⟩⟩∈r⇩N"
proof-
from assms have w:"w∈NELists(Σ)" "u=Init(w)" "Q∈Pow(S)" "G=tPow ` ⟨Q, Last(w)⟩"
unfolding DFSAExecutionRelation_def[OF finite_alphabet dfsa.DFSA] rPow_def by auto
then have "tPow`⟨Q,Last(w)⟩ = (⋃s∈Q. t`⟨s,Last(w)⟩) ⟹ ?thesis"
unfolding NFSAExecutionRelation_def[OF finite_alphabet NFSA] by auto
moreover have "⟨⟨Q,Last(w)⟩,⋃s∈Q. t`⟨s,Last(w)⟩⟩:tPow" unfolding tPow_def using last_type[OF w(1)] w(3) by auto
ultimately show ?thesis using apply_equality[OF _ dfsa.DFSA_dest(3), of "⟨Q,Last(w)⟩" "⋃s∈Q. t`⟨s,Last(w)⟩"]
by blast
qed
text‹Since both are relations, they are equal›
corollary (in NonDetFinStateAuto) relation_NFSA_to_DFSA:
shows "r⇩N = rPow" using nd_impl_det det_impl_nd
unfolding DFSAExecutionRelation_def[OF finite_alphabet dfsa.DFSA]
NFSAExecutionRelation_def[OF finite_alphabet NFSA] rPow_def
by auto
text‹As a consequence, by the definition of a language
generated by an automaton, both languages are equal.›
theorem (in NonDetFinStateAuto) language_nfsa:
shows "dfsa.LanguageDFSA = LanguageNFSA"
proof-
let ?S = "Pow(S)"
let ?s = "{s⇩0}"
let ?f = "{⟨⟨U, u⟩, ⋃v∈U. t ` ⟨v, u⟩⟩ . ⟨U, u⟩ ∈ Pow(S) × Σ}"
let ?F = "{Q ∈ Pow(S) . Q ∩ F ≠ 0}"
{
fix i assume i:"i∈Lists(Σ)" "i <-D (?S,?s,?f,?F){in alphabet}Σ"
{
assume "i=0" "?s∈?F"
then have "i=0" "s⇩0∈F" by auto
then have "i <-N (S,s⇩0,t,F){in alphabet}Σ"
unfolding NFSASatisfy_def[OF finite_alphabet NFSA i(1)] by auto
} moreover
{
assume "¬(i=0 ∧ ?s∈?F)"
with i(2) obtain q where q:"q∈?F" "⟨⟨i,?s⟩,⟨0,q⟩⟩∈rPow^*"
using DFSASatisfy_def[OF finite_alphabet dfsa.DFSA i(1)]
unfolding rPow_def tPow_def by auto
then have "⟨⟨i,?s⟩,⟨0,q⟩⟩∈r⇩N^*" using relation_NFSA_to_DFSA
by auto
with q(1) have "i <-N (S,s⇩0,t,F){in alphabet}Σ"
unfolding NFSASatisfy_def[OF finite_alphabet NFSA i(1)] by auto
} ultimately
have "i <-N (S,s⇩0,t,F){in alphabet}Σ" by auto
}
then have A:"{i ∈ Lists(Σ) . dfsa.reduce(i)} ⊆ {i ∈ Lists(Σ) . i <-N (S,s⇩0,t,F){in alphabet}Σ}"
unfolding rPow_def tPow_def by auto
{
fix i assume i:"i∈Lists(Σ)" "i <-N (S,s⇩0,t,F){in alphabet}Σ"
{
assume "i=0" "s⇩0∈F"
then have "i=0" "?s∈?F" using NFSA
unfolding NFSA_def[OF finite_alphabet] by auto
then have "i <-D (?S,?s,?f,?F){in alphabet}Σ"
using DFSASatisfy_def[OF finite_alphabet dfsa.DFSA i(1)]
unfolding tPow_def rPow_def by auto
} moreover
{
assume "¬(i=0 ∧ s⇩0∈F)"
with i(2) obtain q where q:"q∈Pow(S)" "q∩F≠0" "⟨⟨i,?s⟩,⟨0,q⟩⟩∈r⇩N^*"
unfolding NFSASatisfy_def[OF finite_alphabet NFSA i(1)] by auto
then have "⟨⟨i,?s⟩,⟨0,q⟩⟩∈rPow^*" using relation_NFSA_to_DFSA
by auto
with q(1,2) have "i <-D (?S,?s,?f,?F){in alphabet}Σ"
using DFSASatisfy_def[OF finite_alphabet dfsa.DFSA i(1)]
unfolding tPow_def rPow_def by auto
} ultimately
have "i <-D (?S,?s,?f,?F){in alphabet}Σ" by auto
}
then have B:"{i ∈ Lists(Σ) . i <-N (S,s⇩0,t,F){in alphabet}Σ}⊆
{i ∈ Lists(Σ) . dfsa.reduce(i)}" unfolding tPow_def rPow_def by auto
with A show "dfsa.LanguageDFSA = LanguageNFSA" by auto
qed
text‹The language of a non-deterministic finite
state automaton is regular.›
corollary (in NonDetFinStateAuto) lang_is_regular:
shows "LanguageNFSA{is a regular language on}Σ"
unfolding IsRegularLanguage_def[OF finite_alphabet]
apply (rule exI[of _ "Pow(S)"],
rule exI[of _ "{s⇩0}"],
rule exI[of _ tPow],
rule exI[of _ "{Q ∈ Pow(S). Q ∩ F ≠ 0}"])
using language_nfsa dfsa.DFSA by auto
end