# HG changeset patch # User haftmann # Date 1215076565 -7200 # Node ID 5c1fb7d262bfc701bed886022d5dd02207d8fc38 # Parent 85d546d2ebe87dd8c60ac38991ebd711cef5fdc6 adjusted rep_datatype diff -r 85d546d2ebe8 -r 5c1fb7d262bf doc-src/HOL/HOL.tex --- 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 diff -r 85d546d2ebe8 -r 5c1fb7d262bf doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r 85d546d2ebe8 -r 5c1fb7d262bf doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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