342 quantification available in HOL.\footnote{Slind already pointed out |
342 quantification available in HOL.\footnote{Slind already pointed out |
343 this problem in an email to the HOL4 mailing list on 21st April |
343 this problem in an email to the HOL4 mailing list on 21st April |
344 2005.} Systems such as Coq permit quantification over types and thus can |
344 2005.} Systems such as Coq permit quantification over types and thus can |
345 state such a definition. This has been recently exploited in an |
345 state such a definition. This has been recently exploited in an |
346 elegant and short formalisation of the Myhill-Nerode theorem in Coq by |
346 elegant and short formalisation of the Myhill-Nerode theorem in Coq by |
347 \citeN{Smolka13}, but as said this is not avaible to us working in Isabelle/HOL. |
347 \citeN{Smolka13}, but as said this is not available to us working in Isabelle/HOL. |
348 |
348 |
349 An alternative, which provides us with a single type for states of automata, |
349 An alternative, which provides us with a single type for states of automata, |
350 is to give every state node an identity, for example a natural number, and |
350 is to give every state node an identity, for example a natural number, and |
351 then be careful to rename these identities apart whenever connecting two |
351 then be careful to rename these identities apart whenever connecting two |
352 automata. This results in clunky proofs establishing that properties are |
352 automata. This results in clunky proofs establishing that properties are |
1739 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set |
1739 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set |
1740 @{text "A"} to @{term "lang r"} and thus complete the proof.\qed |
1740 @{text "A"} to @{term "lang r"} and thus complete the proof.\qed |
1741 \end{proof} |
1741 \end{proof} |
1742 |
1742 |
1743 \begin{rmk} |
1743 \begin{rmk} |
1744 While our proof using tagging functions might seem like a rabbit pulled |
1744 While our proof using tagging functions might seem like a `rabbit pulled |
1745 out of a hat, the intuition behind can be somewhat rationalised by taking the |
1745 out of a hat', the intuition behind can be somewhat rationalised by taking the |
1746 view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the |
1746 view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the |
1747 states of the minimal automaton for the language @{term "lang r"}. The theorem |
1747 states of the minimal automaton for the language @{term "lang r"}. The theorem |
1748 amounts to showing that this minimal automaton has finitely many states. |
1748 amounts to showing that this minimal automaton has finitely many states. |
1749 However, by showing that our @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} relation |
1749 However, by showing that our @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} relation |
1750 refines @{term "\<approx>A"} we do not actually have to show that the minimal automata |
1750 refines @{term "\<approx>A"} we do not actually have to show that the minimal automata |
1966 \noindent |
1966 \noindent |
1967 Carrying this idea through, we must not consider the set of all derivatives, |
1967 Carrying this idea through, we must not consider the set of all derivatives, |
1968 but the one modulo @{text "ACI"}. In principle, this can be done formally, |
1968 but the one modulo @{text "ACI"}. In principle, this can be done formally, |
1969 but it is very painful in a theorem prover---since there is no |
1969 but it is very painful in a theorem prover---since there is no |
1970 direct characterisation of the set of dissimilar derivatives. Therefore |
1970 direct characterisation of the set of dissimilar derivatives. Therefore |
1971 \citeN{CoquandSiles12} who follow through this idea had to `stand on their heads' and |
1971 \citeN{CoquandSiles12} who follow through this idea had to spend extra effort and |
1972 first formalise the quite intricate notion of \emph{inductively finite sets} in |
1972 first formalise the quite intricate notion of \emph{inductively finite sets} in |
1973 order to formalise this property. |
1973 order to formalise this property. |
1974 |
1974 |
1975 |
1975 |
1976 Fortunately, there is a much simpler approach using \emph{partial |
1976 Fortunately, there is a much simpler approach using \emph{partial |
2313 \end{theorem} |
2313 \end{theorem} |
2314 |
2314 |
2315 \noindent |
2315 \noindent |
2316 Our proof follows the one given by \citeN[Pages 92--95]{Shallit08}, except that we use |
2316 Our proof follows the one given by \citeN[Pages 92--95]{Shallit08}, except that we use |
2317 Higman's Lemma, which is already proved in the Isabelle/HOL library by |
2317 Higman's Lemma, which is already proved in the Isabelle/HOL library by |
2318 Sternagel. |
2318 \citeN{Sternagel13}. |
2319 Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying |
2319 Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying |
2320 % |
2320 % |
2321 \begin{equation}\label{higman} |
2321 \begin{equation}\label{higman} |
2322 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"} |
2322 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"} |
2323 \end{equation} |
2323 \end{equation} |