# HG changeset patch # User wenzelm # Date 1306409831 -7200 # Node ID 66b189dc5b83802e138cd58263f7b706eb2503e4 # Parent eb94cfaaf5d496b22b0fe014da861b2bfa9b747d updated and re-unified HOL rep_datatype; diff -r eb94cfaaf5d4 -r 66b189dc5b83 doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Wed May 25 22:21:38 2011 +0200 +++ b/doc-src/HOL/HOL.tex Thu May 26 13:37:11 2011 +0200 @@ -1249,9 +1249,7 @@ shown. The constructions are fairly standard and can be found in the respective theory files. Although the sum and product types are constructed manually for foundational reasons, they are represented as -actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}). -Therefore, the theory \texttt{Datatype} should be used instead of -\texttt{Sum} or \texttt{Prod}. +actual datatypes later. \begin{figure} \begin{constants} @@ -1375,7 +1373,7 @@ the order of the two cases. Both \texttt{primrec} and \texttt{case} are realized by a recursion operator \cdx{nat_rec}, which is available because \textit{nat} is represented as -a datatype (see {\S}\ref{subsec:datatype:rep_datatype}). +a datatype. %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. %Recursion along this relation resembles primitive recursion, but is @@ -1940,32 +1938,6 @@ and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. -\subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype} - -For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt - +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, -but by more primitive means using \texttt{typedef}. To be able to use the -tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by -primitive recursion on these types, such types may be represented as actual -datatypes. This is done by specifying the constructors of the desired type, -plus a proof of the induction rule, as well as theorems -stating the distinctness and injectivity of constructors in a {\tt -rep_datatype} section. For the sum type this works as follows: -\begin{ttbox} -rep_datatype (sum) Inl Inr -proof - - fix P - fix s :: "'a + 'b" - assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)" - then show "P s" by (auto intro: sumE [of s]) -qed simp_all -\end{ttbox} -The datatype package automatically derives additional theorems for recursion -and case combinators from these rules. Any of the basic HOL types mentioned -above are represented as datatypes. Try an induction on \texttt{bool} -today. - - \subsection{Examples} \subsubsection{The datatype $\alpha~mylist$} diff -r eb94cfaaf5d4 -r 66b189dc5b83 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 25 22:21:38 2011 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 13:37:11 2011 +0200 @@ -458,14 +458,26 @@ HOL. \item @{command (HOL) "rep_datatype"} represents existing types as - inductive ones, generating the standard infrastructure of derived - concepts (primitive recursion etc.). + datatypes. + + For foundational reasons, some basic types such as @{typ nat}, @{typ + "'a \ 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are + introduced by more primitive means using @{command_ref typedef}. To + recover the rich infrastructure of @{command datatype} (e.g.\ rules + for @{method cases} and @{method induct} and the primitive recursion + combinators), such types may be represented as actual datatypes + later. This is done by specifying the constructors of the desired + type, and giving a proof of the induction rule, distinctness and + injectivity of constructors. + + For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the + representation of the primitive sum type as fully-featured datatype. \end{description} - The induction and exhaustion theorems generated provide case names - according to the constructors involved, while parameters are named - after the types (see also \secref{sec:cases-induct}). + The generated rules for @{method induct} and @{method cases} provide + case names according to the given constructors, while parameters are + named after the types (see also \secref{sec:cases-induct}). See \cite{isabelle-HOL} for more details on datatypes, but beware of the old-style theory syntax being used there! Apart from proper diff -r eb94cfaaf5d4 -r 66b189dc5b83 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:21:38 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 13:37:11 2011 +0200 @@ -729,14 +729,25 @@ HOL. \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as - inductive ones, generating the standard infrastructure of derived - concepts (primitive recursion etc.). + datatypes. + + For foundational reasons, some basic types such as \isa{nat}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{bool} and \isa{unit} are + introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}. To + recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules + for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion + combinators), such types may be represented as actual datatypes + later. This is done by specifying the constructors of the desired + type, and giving a proof of the induction rule, distinctness and + injectivity of constructors. + + For example, see \verb|~~/src/HOL/Sum_Type.thy| for the + representation of the primitive sum type as fully-featured datatype. \end{description} - The induction and exhaustion theorems generated provide case names - according to the constructors involved, while parameters are named - after the types (see also \secref{sec:cases-induct}). + The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide + case names according to the given constructors, while parameters are + named after the types (see also \secref{sec:cases-induct}). See \cite{isabelle-HOL} for more details on datatypes, but beware of the old-style theory syntax being used there! Apart from proper