4 begin

     4 begin

     5 

     5 

     6 declare [[show_question_marks = false]]

     6 declare [[show_question_marks = false]]

     7 

     7 

     8 consts

     8 consts

    10  UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"

    10  UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"

    11 

    11 

    12 abbreviation

    12 abbreviation

    13   "EClass x R \<equiv> R `` {x}"

    13   "EClass x R \<equiv> R `` {x}"

    14 

    14 

   324   an automaton that recognises all its strings (Definition~\ref{baddef}). This

   324   an automaton that recognises all its strings (Definition~\ref{baddef}). This

   325   is because we cannot make a definition in HOL that is only polymorphic in

   325   is because we cannot make a definition in HOL that is only polymorphic in

   326   the state type, but not in the predicate for regularity; and there is no

   326   the state type, but not in the predicate for regularity; and there is no

   327   type quantification available in HOL (unlike in Coq, for

   327   type quantification available in HOL (unlike in Coq, for

   328   example).\footnote{Slind already pointed out this problem in an email to the

   328   example).\footnote{Slind already pointed out this problem in an email to the

   330 

   331 

   331   An alternative, which provides us with a single type for states of automata,

   332   An alternative, which provides us with a single type for states of automata,

   332   is to give every state node an identity, for example a natural number, and

   333   is to give every state node an identity, for example a natural number, and

   333   then be careful to rename these identities apart whenever connecting two

   334   then be careful to rename these identities apart whenever connecting two

   334   automata. This results in clunky proofs establishing that properties are

   335   automata. This results in clunky proofs establishing that properties are

   389   Kozen's proof of the Myhill-Nerode Theorem requires that automata do not

   390   Kozen's proof of the Myhill-Nerode Theorem requires that automata do not

   390   have inaccessible states \cite{Kozen97}. Another subtle side-condition is

   391   have inaccessible states \cite{Kozen97}. Another subtle side-condition is

   391   completeness of automata, that is automata need to have total transition

   392   completeness of automata, that is automata need to have total transition

   392   functions and at most one `sink' state from which there is no connection to

   393   functions and at most one `sink' state from which there is no connection to

   393   a final state (Brzozowski mentions this side-condition in the context of

   394   a final state (Brzozowski mentions this side-condition in the context of

   395   that if we define a regular language as one for which there exists \emph{a}

   397   that if we define a regular language as one for which there exists \emph{a}

   396   finite automaton that recognises all its strings (see

   398   finite automaton that recognises all its strings (see

   397   Definition~\ref{baddef}), then we need a lemma which ensures that another

   399   Definition~\ref{baddef}), then we need a lemma which ensures that another

   398   equivalent one can be found satisfying the side-condition, and also need to

   400   equivalent one can be found satisfying the side-condition, and also need to

   399   make sure our operations on automata preserve them. Unfortunately, such

   401   make sure our operations on automata preserve them. Unfortunately, such

   606 

   608 

   607   \noindent

   609   \noindent

   608   In what follows we shall use this convenient short-hand notation for images of sets 

   610   In what follows we shall use this convenient short-hand notation for images of sets 

   609   also with other functions.

   611   also with other functions.

   610 *}

   612 *}

   612 

   613 

   613 section {* The Myhill-Nerode Theorem, First Part *}

   614 section {* The Myhill-Nerode Theorem, First Part *}

   614 

   615 

   615 text {*

   616 text {*

   616   \noindent

   617   \noindent

  2453   Nipkow of the Gauss-Jordan algorithm \cite{Nipkow11}.

  2454   Nipkow of the Gauss-Jordan algorithm \cite{Nipkow11}.

  2454 

  2455 

  2455   While our formalisation might appear large, it should be seen

  2456   While our formalisation might appear large, it should be seen

  2456   in the context of the work done by Constable at al \cite{Constable00} who

  2457   in the context of the work done by Constable at al \cite{Constable00} who

  2457   formalised the Myhill-Nerode Theorem in Nuprl using automata. They write

  2458   formalised the Myhill-Nerode Theorem in Nuprl using automata. They write

  2460   formalisation in Nurpl, but from what is shown in the Nuprl Math Library

  2462   formalisation in Nurpl, but from what is shown in the Nuprl Math Library

  2461   about their development it seems substantially larger than ours. We attribute

  2463   about their development it seems substantially larger than ours. We attribute

  2462   this to our use of regular expressions, which meant we did not need to `fight' 

  2464   this to our use of regular expressions, which meant we did not need to `fight' 

  2463   the theorem prover.

  2465   the theorem prover.

  2464   Also, Filli\^atre reports that his formalisation in 

  2466   Also, Filli\^atre reports that his formalisation in