Theory Finite_State_Machines_ZF

(* 
    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:"tid(field(r))  (converse(r^* O r))"
    {
      assume "tid(field(r))"
      then have "tconverse(id(field(r))  (r^* O r))" by auto
    } moreover
    {
      assume "tid(field(r))"
      with t have "tconverse(r^* O r)" by auto
      then have "tconverse(id(field(r))  (r^* O r))" by auto
    }
    ultimately have "tconverse(id(field(r))  (r^* O r))" by auto
  }
  moreover
  {
    fix t assume t:"tconverse(id(field(r))  (r^* O r))"
    then obtain t1 t2 where t12:"t=t1,t2" "t2,t1id(field(r))  (r^* O r)"
      by auto
    {
      assume "t2,t1id(field(r))"
      with t12(1) have "tid(field(r))" by auto
      then have "tid(field(r))  converse(r^* O r)" by auto
    } moreover
    {
      assume "t2,t1id(field(r))"
      with t12(2) have "t2,t1(r^* O r)" by auto
      with t12(1) have "tconverse(r^* O r)" by auto
      then have "tid(field(r))  converse(r^* O r)" by auto
    }
    ultimately have "tid(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:"tid(field(r))  (r^* O r)"
    {
      assume "tid(field(r))"
      then have "t:field(r)*field(r)" by auto
    } moreover
    {
      assume "tid(field(r))"
      with t have "tr^* O r" by auto
      then have "t:field(r)*field(r)" using rtrancl_type unfolding comp_def by auto
    } ultimately
    have "tfield(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,s0,t,F){is an DFSA for alphabet}Σ  Finite(S)  s0  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,s0,t,F){is an DFSA for alphabet}Σ  
  {reduce D-relation}(S,s0,t){in alphabet}Σ  {w,s,Init(w),t`s,Last(w). w,sNELists(Σ)×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,s0,t){in alphabet}Σ)"},
we add the extra condition that @{term "0,s0,0,s0"}
is also a valid transition.›

definition
  DFSASatisfy ("_ <-D '(_,_,_,_'){in alphabet}_") where
  "Finite(Σ)  (S,s0,t,F){is an DFSA for alphabet}Σ  iLists(Σ)  
  i <-D (S,s0,t,F){in alphabet}Σ  (qF. i,s0,0,q ({reduce D-relation}(S,s0,t){in alphabet}Σ)^*)  (i = 0  s0F)"

text‹We define a locale for better notation›

locale DetFinStateAuto =
  fixes S and s0 and t and F and Σ
  assumes finite_alphabet: "Finite(Σ)"
  
  assumes DFSA: "(S,s0,t,F){is an DFSA for alphabet}Σ"

text‹We abbreviate the reduce relation to a single symbol
within this locale.›

abbreviation (in DetFinStateAuto) "rD" where
 "rD  {reduce D-relation}(S,s0,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,s0,t,F){in alphabet}Σ"

text‹Destruction lemma about deterministic finite
state automata.›

lemma (in DetFinStateAuto) DFSA_dest:
  shows "s0S" "FS" "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 "{iLists(Σ). i <-D (S,s0,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  {iLists(Σ). i <-D (S,s0,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(rD)" "function(rD)" 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 "rD:NELists(Σ)×SLists(Σ)×S"
proof-
  from DFSA have T:"t:S×Σ  S" unfolding DFSA_def[OF finite_alphabet] by auto
  {
    fix x assume "xrD"
    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:"rDPow((NELists(Σ)×S)×(Lists(Σ)×S))" by auto moreover
  {
    fix x assume "xNELists(Σ)×S"
    then obtain l s where x:"lNELists(Σ)" "sS" "x=l,s" by auto
    then have "l,s,Init(l),t`s,Last(l)rD" unfolding
      DFSAExecutionRelation_def[OF finite_alphabet DFSA] by auto
    with x(3) have "xdomain(rD)" unfolding domain_def by auto
  }
  then have "NELists(Σ)×S  domain(rD)" 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(rD)  Lists(Σ)×S" "NELists(Σ)×S  field(rD)"
proof-
  from DFSA have T:"t:S×Σ  S" unfolding DFSA_def[OF finite_alphabet] by auto
  {
    fix x assume "xfield(rD)"
    then have E:"y. x,yrD  y,xrD" unfolding domain_def range_def field_def by auto
    {
      assume "y. x,yrD"
      then have "xNELists(Σ)×S" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
        by auto
      then have "xLists(Σ)×S" unfolding Lists_def NELists_def by auto
    } moreover
    {
      assume "¬(y. x,yrD)"
      with E have "y.y,xrD" by auto
      then obtain u v where y:"uNELists(Σ)" "vS" "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 "xLists(Σ)×S" by auto
    }
    ultimately have "xLists(Σ)×S" by auto
  }
  then show "field(rD)  Lists(Σ)×S" by auto
  show "NELists(Σ)×S  field(rD)"
    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,vrD^*"
  shows "restrict(w,domain(u)) = u"
proof-
  from assms have "w,sfield(rD)" using rtrancl_field[of rD] relation_field_times_field[OF relation_rtrancl[of rD]] by auto
  then have "wLists(Σ)" 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  rD^*" "y, z  rD" "restrict(w, domain(fst(y))) = fst(y)"
    from as(1) have "y:field(rD)"  using rtrancl_field[of rD] relation_field_times_field[OF relation_rtrancl[of rD]] by auto
    then obtain y1 y2 where y:"y=y1,y2" "y1Lists(Σ)" "y2S" using reduce_field(1)
      by auto
    with as(2) have z:"z=Init(y1),t`y2,Last(y1)" "y1NELists(Σ)" 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)" "qnat" 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  rD^* 
             (y, z  rD 
             (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" rD "λ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  rD^*" by auto
    {
      fix y z
      assume as:"w, s, y  rD^*" "y, z  rD" "restrict(w, domain(fst(y))) = fst(y)"
      from as(1) have "y:field(rD)"  using rtrancl_field[of rD] relation_field_times_field[OF relation_rtrancl[of rD]] by auto
      then obtain y1 y2 where y:"y=y1,y2" "y1Lists(Σ)" "y2S" using reduce_field(1)
        by auto
      with as(2) have z:"z=Init(y1),t`y2,Last(y1)" "y1NELists(Σ)" 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)" "qnat" 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,vrD^*" "w,s,u,mrD^*"
  shows "v=m"
proof-
  let ?P="λy. q1 q2. w,s,q1,q2rD^*  fst(y) = q1  snd(y) = q2"
  {
    fix q1 q2 assume "w, s, q1, q2  rD^*" "fst(w, ss) = q1" 
    then have "w, s, w, q2  rD^*" by auto
    then have "w, s, w, q2  id(field(rD))  (rD^* O rD)" using rtrancl_rev by auto
    then have A:"s=q2  w, s, w, q2:(rD^* O rD)" by auto
    {
      assume "sq2"
      with A have "w, s, w, q2:(rD^* O rD)" by auto
      then obtain b where b:"w,s,b:rD" "b,w,q2:rD^*" 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:rD^*" "y,z:rD" "?P(y)"
    {
      fix q1 q2 assume z:"w, s, q1, q2  rD^*" "fst(z) = q1"
      from this(1) have "w, s, q1, q2  id(field(rD))  (rD O rD^*)" using rtrancl_unfold by auto
      then have A:"(s=q2  w=q1)  w, s, q1, q2:(rD O rD^*)" by auto
      from y(2) obtain y1 y2 where zz:"y=y1,y2" "y1:NELists(Σ)" "y2S" "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:(rD O rD^*)" by auto
      then obtain pp where pp:"w, s, pp:rD^*" "pp, q1, q2:rD" unfolding compE by auto
      from this(2) obtain ppL ppS where ppl:"ppL:NELists(Σ)" "ppSS" "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)  Σ" "qnat" 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:"onat" "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,yrD^*  y,zrD  ?P(y)  ?P(z)" by auto
  then have "?P(u,v)" using rtrancl_induct[of "w,s" "u,v" rD "λy. q1 q2. w,s,q1,q2:rD^*  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 "wNELists(Σ)"
  shows "q  S. w,s0,0,q  rD^*"
proof-
  let ?P="λk. yLists(Σ). domain(y) = k  y=0  (ssS. (qS. y,ss,0,qrD^*))"
  {
    fix y assume "yLists(Σ)" "domain(y) = 0"
    with assms have "y=0" unfolding Lists_def using domain_of_fun by auto
    then have "y=0  (ssS. (qS. y,ss,0,qrD^*))" by auto
  }
  then have base:"?P(0)" by auto
  {
    fix k assume hyp:"?P(k)" "knat"
    {
      fix y assume as:"yLists(Σ)" "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  (ssS. (qS. Init(y),ss,0,qrD^*))" by auto
      {
        assume iy0:"Init(y) = 0"
        {
          fix ss assume "ssS"
          with iy0 y have "y,ss,0,t`ss,Last(y)rD" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
            by auto
          then have "y,ss,0,t`ss,Last(y)rD^*" using r_into_rtrancl by auto
          moreover from `ssS` have "t`ss,Last(y) S" using apply_type[OF DFSA_dest(3)]
            last_type[OF y] by auto
          ultimately have "qS. y,ss,0,q:rD^*" by auto
        }
        then have "ssS. qS. y,ss,0,q:rD^*" by auto
        then have "y = 0  (ssS. qS. y,ss,0,q:rD^*)" by auto
      } moreover
      {
        assume qS:"ssS. qS. Init(y),ss,0,qrD^*"
        {
          fix ss assume "ssS"
          with y have "y,ss,Init(y),t`ss,Last(y)rD" unfolding DFSAExecutionRelation_def[OF finite_alphabet DFSA]
            by auto
          moreover from `ssS` y have "t`ss,Last(y) S" using apply_type[OF DFSA_dest(3)]
            last_type by auto
          with qS have "qS. Init(y),t`ss,Last(y),0,qrD^*" by auto
          then obtain q where "qS" "Init(y),t`ss,Last(y),0,qrD^*" by auto
          ultimately have "y,ss,0,qrD^*" "qS" using rtrancl_into_trancl2
            trancl_into_rtrancl by auto
          then have "qS. y,ss,0,qrD^*" by auto
        }
        then have "y = 0  (ssS. qS. y,ss,0,q:rD^*)"  by auto
      } ultimately
      have "y = 0  (ssS. qS. y,ss,0,q:rD^*)" using d by auto
    }
    then have "?P(succ(k))" by auto
  }
  then have ind:"k. knat  ?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 "(ssS. qS. w, ss, 0, q  rD^*)" 
    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. x2}
               {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.rD"

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,yr{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" "y1NELists(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),ends0transFun" 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 "wNELists(2)" "w`0 = 0"
  shows "w,starts0,0,starts0r{0.*1}^*" "w,starts1,0,starts0r{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 "qNELists(2)"
    then obtain m where "mnat" "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×2states" 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,starts0r{0.*1}^*  w,starts1,0,starts0r{0.*1}^*)"
    {
      fix y assume y:"yNELists(2)" "y`0 = 0" "domain(y) = succ(ka)"
      from y(1) obtain s where s:"y:succ(s)2" "snat" 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):02" 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,starts0r{0.*1}" by auto
        then have A:"y,starts0,0,starts0r{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,starts0r{0.*1}^*" using r_into_rtrancl by auto
        with A have "y,starts0,0,starts0r{0.*1}^*  y,starts1,0,starts0r{0.*1}^*" by auto
      } moreover
      {
        assume ka:"ka0"
        with kaNat obtain u where u:"ka=succ(u)" "unat" 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):s2" 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,starts0r{0.*1}^*" 
          "Init(y),starts1,0,starts0r{0.*1}^*" by auto
        then have A:"x{starts0, starts1}. Init(y),x,0,starts0r{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),starts0r{0.*1}" by auto
        } moreover
        {
          assume as:"Last(y) = 1"
          with Q t10 have "y,starts0,Init(y),starts1r{0.*1}" by auto
        }
        moreover note last_2 ultimately have
        "(y,starts0,Init(y),starts0r{0.*1})  (y,starts0,Init(y),starts1r{0.*1})" by auto
        with A have B:"y,starts0,0,starts0r{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),starts0r{0.*1}" by auto
        } moreover
        {
          assume as:"Last(y) = 1"
          with Q t11 have "y,starts1,Init(y),starts1r{0.*1}" by auto
        }
        moreover note last_2 ultimately have
        "(y,starts1,Init(y),starts0r{0.*1})  (y,starts1,Init(y),starts1r{0.*1})" by auto
        with A have "y,starts1,0,starts0r{0.*1}^*" using rtrancl_into_trancl2 trancl_into_rtrancl by auto
        with B have rr:"y,starts0,0,starts0r{0.*1}^*  y,starts1,0,starts0r{0.*1}^*" by auto
      }
      ultimately have "y,starts0,0,starts0r{0.*1}^*  y,starts1,0,starts0r{0.*1}^*" by auto
    }
    then have "w. w  NELists(2)  w`0 = 0  domain(w) = succ(ka)  (w,starts0,0,starts0r{0.*1}^*  w,starts1,0,starts0r{0.*1}^*)" by auto
  }
  then have rule:"knat.
       (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. wNELists(2)  w`0 =0  domain(w) = t  (w,starts0,0,starts0r{0.*1}^*  w,starts1,0,starts0r{0.*1}^*)", OF dom base rule]
  show R:"w,starts0,0,starts0r{0.*1}^*" "w,starts1,0,starts0r{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 "iLists(2)" and "i`0=0" and "Last(i) = 1"
  shows "i{reduces in 0.*1}"
proof-
  from assms(1) obtain tt where t:"ttnat" "i:tt2" 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 "i0" by auto
    ultimately have False using t domain_of_fun by auto
  }
  with domNat t(1) obtain y where y:"domain(i) = succ(y)" "ynat" using Nat_ZF_1_L3 by auto
  with domNat t(2) have iList:"iNELists(2)" unfolding NELists_def by auto
  have finA:"Finite(2)" using nat_into_Finite[of 2] by auto  
  have funT:"transFun:states×2states" 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:12" 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 "y0" by auto
  then obtain k where yy:"y= succ(k)" "knat" 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 "0succ(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,starts0r{0.*1}^*" using invariant_state_0_1
    by auto
  with U have "i,empty,0,starts0r{0.*1}^*" using rtrancl_into_trancl2[THEN trancl_into_rtrancl] by auto
  then have "qfinalStates. 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 "iLists(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×2states" 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,qr{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" "q1NELists(2)" "q2states" 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" "knat" unfolding NELists_def by auto
  then have "Init(q1):k2" using init_props(1) by auto
  with A(1) have "k=0" unfolding Pi_def by auto
  with k(1) have qfun:"q1:12" by auto
  from qfun have q10:"Last(q1) = q1`0" unfolding Last_def using domain_of_fun by auto
  from k have "0domain(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`02" 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 "q22" "Last(q1) = 0" by auto
  with `0domain(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 `q22` 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 "zfield(r{0.*1})" using rtrancl_type[of "r{0.*1}"] by auto
  then obtain z1 z2 where zz:"z=z1,z2" "z1Lists(2)" "z2states" 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 `q22` 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 = {iLists(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 "(L1L2) {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 = {iLists(Σ). 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 = {iLists(Σ). 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.rD(?S,?s,?t,Σ)"
  let ?r1 = "DetFinStateAuto.rD(S1,s1,t1,Σ)"
  let ?r2 = "DetFinStateAuto.rD(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,yS1" "t2`x2,yS2" 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. mNELists(Σ)  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^*" "mNELists(Σ)"
      note as(2)
      moreover have "s1S1" "s2S2" 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 "bbfield(?r)" "ccfield(?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"
          "bbLLists(Σ)" "ccLLists(Σ)" "cc1S1" "cc2S2" "bb1S1" "bb2S2"
          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{iLists(Σ). i <-D (?S,?s,?t,?F){in alphabet}Σ}"
    then have M:"mLists(Σ)" "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 "0NELists(Σ)" 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:"m0"
      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 "mNELists(Σ)" 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 "qF1.  m, s1, 0,q?r1^*" "qF2.  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}Σ}  L1L2" using l1(2) l2(2) by auto
  {
    fix m assume "mL1L2"
    with l1(2) l2(2) have M:"mLists(Σ)" "m <-D (S1,s1,t1,F1){in alphabet}Σ" "m <-D (S2,s2,</