equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../Myhill" "LaTeXsugar" |
3 imports "../Myhill_2" "~~/src/HOL/Library/LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 declare [[show_question_marks = false]] |
6 declare [[show_question_marks = false]] |
7 |
7 |
8 consts |
8 consts |
876 the base cases are straightforward. |
876 the base cases are straightforward. |
877 |
877 |
878 |
878 |
879 \begin{proof}[Base Cases] |
879 \begin{proof}[Base Cases] |
880 The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because |
880 The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because |
881 we can easily establish |
881 we can easily establish that |
882 |
882 |
883 \begin{center} |
883 \begin{center} |
884 \begin{tabular}{l} |
884 \begin{tabular}{l} |
885 @{thm quot_null_eq}\\ |
885 @{thm quot_null_eq}\\ |
886 @{thm quot_empty_subset}\\ |
886 @{thm quot_empty_subset}\\ |
935 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have |
935 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have |
936 @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be |
936 @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be |
937 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"}, |
937 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"}, |
938 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the |
938 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the |
939 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}. |
939 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}. |
940 From the assumption we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with |
940 From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with |
941 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in |
941 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in |
942 turn means that the equivalence classes @{text X} |
942 turn means that the equivalence classes @{text X} |
943 and @{text Y} must be equal.\qed |
943 and @{text Y} must be equal.\qed |
944 \end{proof} |
944 \end{proof} |
945 |
945 |
1316 whose correctness has been formally established, we refer the reader to |
1316 whose correctness has been formally established, we refer the reader to |
1317 Owens and Slind \cite{OwensSlind08}. |
1317 Owens and Slind \cite{OwensSlind08}. |
1318 |
1318 |
1319 |
1319 |
1320 Our formalisation consists of 780 lines of Isabelle/Isar code for the first |
1320 Our formalisation consists of 780 lines of Isabelle/Isar code for the first |
1321 direction and 475 for the second, plus around 300 lines of standard material about |
1321 direction and 460 for the second, plus around 300 lines of standard material about |
1322 regular languages. While this might be seen as too large to count as a |
1322 regular languages. While this might be seen as too large to count as a |
1323 concise proof pearl, this should be seen in the context of the work done by |
1323 concise proof pearl, this should be seen in the context of the work done by |
1324 Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem |
1324 Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem |
1325 in Nuprl using automata. They write that their four-member team needed |
1325 in Nuprl using automata. They write that their four-member team needed |
1326 something on the magnitude of 18 months for their formalisation. The |
1326 something on the magnitude of 18 months for their formalisation. The |