(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2023 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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,</