--- a/doc-src/HOL/HOL.tex Thu Jul 03 00:58:30 2008 +0200
+++ b/doc-src/HOL/HOL.tex Thu Jul 03 11:16:05 2008 +0200
@@ -2072,14 +2072,18 @@
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 an induction rule, as well as theorems
+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 type \texttt{nat} this works as follows:
+rep_datatype} section. For the sum type this works as follows:
\begin{ttbox}
-rep_datatype nat
- distinct Suc_not_Zero, Zero_not_Suc
- inject Suc_Suc_eq
- induct nat_induct
+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
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 03 00:58:30 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 03 11:16:05 2008 +0200
@@ -362,20 +362,18 @@
text {*
\begin{matharray}{rcl}
@{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\
- @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{proof} \\
\end{matharray}
\begin{rail}
'datatype' (dtspec + 'and')
;
- 'rep\_datatype' (name *) dtrules
+ 'rep\_datatype' ('(' (name +) ')')? (term +)
;
dtspec: parname? typespec infix? '=' (cons + '|')
;
cons: name (type *) mixfix?
- ;
- dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
\begin{descr}
@@ -460,12 +458,16 @@
%FIXME check
- Recursive definitions introduced by both the @{command (HOL)
- "primrec"} and the @{command (HOL) "function"} command accommodate
+ Recursive definitions introduced by the @{command (HOL) "function"}
+ command accommodate
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
"c.induct"} (where @{text c} is the name of the function definition)
refers to a specific induction rule, with parameters named according
- to the user-specified equations. Case names of @{command (HOL)
+ to the user-specified equations.
+ For the @{command (HOL) "primrec"} the induction principle coincides
+ with structural recursion on the datatype the recursion is carried
+ out.
+ Case names of @{command (HOL)
"primrec"} are that of the datatypes involved, while those of
@{command (HOL) "function"} are numbered (starting from 1).
@@ -985,7 +987,7 @@
'code\_modulename' target ( ( string string ) + )
;
- 'code\_exception' ( const + )
+ 'code\_abort' ( const + )
;
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
@@ -1075,13 +1077,13 @@
one module name onto another.
\item [@{command (HOL) "code_abort"}] declares constants which
- are not required to have a definition by a defining equations;
+ are not required to have a definition by means of defining equations;
if needed these are implemented by program abort instead.
\item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
with option ``@{text "del:"}'' deselects) a defining equation for
code generation. Usually packages introducing defining equations
- provide a resonable default setup for selection.
+ provide a reasonable default setup for selection.
\item [@{attribute (HOL) code}@{text inline}] declares (or with
option ``@{text "del:"}'' removes) inlining theorems which are
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 03 00:58:30 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 03 11:16:05 2008 +0200
@@ -365,20 +365,18 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\
\end{matharray}
\begin{rail}
'datatype' (dtspec + 'and')
;
- 'rep\_datatype' (name *) dtrules
+ 'rep\_datatype' ('(' (name +) ')')? (term +)
;
dtspec: parname? typespec infix? '=' (cons + '|')
;
cons: name (type *) mixfix?
- ;
- dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
\begin{descr}
@@ -464,10 +462,15 @@
%FIXME check
- Recursive definitions introduced by both the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} and the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accommodate
+ Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
+ command accommodate
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)
refers to a specific induction rule, with parameters named according
- to the user-specified equations. Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
+ to the user-specified equations.
+ For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
+ with structural recursion on the datatype the recursion is carried
+ out.
+ Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
The equations provided by these packages may be referred later as
@@ -988,7 +991,7 @@
'code\_modulename' target ( ( string string ) + )
;
- 'code\_exception' ( const + )
+ 'code\_abort' ( const + )
;
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
@@ -1075,13 +1078,13 @@
one module name onto another.
\item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
- are not required to have a definition by a defining equations;
+ are not required to have a definition by means of defining equations;
if needed these are implemented by program abort instead.
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
code generation. Usually packages introducing defining equations
- provide a resonable default setup for selection.
+ provide a reasonable default setup for selection.
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are