Paper/Paper.thy
changeset 149 e122cb146ecc
parent 145 099e20f25b25
child 154 7c68b9ad4486
equal deleted inserted replaced
148:3b7477db3462 149:e122cb146ecc
     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