adjusted rep_datatype
authorhaftmann
Thu Jul 03 11:16:05 2008 +0200 (2008-07-03)
changeset 274525c1fb7d262bf
parent 27451 85d546d2ebe8
child 27453 eecd9d84e41b
adjusted rep_datatype
doc-src/HOL/HOL.tex
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/HOL/HOL.tex	Thu Jul 03 00:58:30 2008 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Thu Jul 03 11:16:05 2008 +0200
     1.3 @@ -2072,14 +2072,18 @@
     1.4  but by more primitive means using \texttt{typedef}. To be able to use the
     1.5  tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
     1.6  primitive recursion on these types, such types may be represented as actual
     1.7 -datatypes.  This is done by specifying an induction rule, as well as theorems
     1.8 +datatypes.  This is done by specifying the constructors of the desired type,
     1.9 +plus a proof of the  induction rule, as well as theorems
    1.10  stating the distinctness and injectivity of constructors in a {\tt
    1.11 -  rep_datatype} section.  For type \texttt{nat} this works as follows:
    1.12 +rep_datatype} section.  For the sum type this works as follows:
    1.13  \begin{ttbox}
    1.14 -rep_datatype nat
    1.15 -  distinct Suc_not_Zero, Zero_not_Suc
    1.16 -  inject   Suc_Suc_eq
    1.17 -  induct   nat_induct
    1.18 +rep_datatype (sum) Inl Inr
    1.19 +proof -
    1.20 +  fix P
    1.21 +  fix s :: "'a + 'b"
    1.22 +  assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)"
    1.23 +  then show "P s" by (auto intro: sumE [of s])
    1.24 +qed simp_all
    1.25  \end{ttbox}
    1.26  The datatype package automatically derives additional theorems for recursion
    1.27  and case combinators from these rules.  Any of the basic HOL types mentioned
     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 03 00:58:30 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 03 11:16:05 2008 +0200
     2.3 @@ -362,20 +362,18 @@
     2.4  text {*
     2.5    \begin{matharray}{rcl}
     2.6      @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\
     2.7 -    @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{theory} \\
     2.8 +  @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{proof} \\
     2.9    \end{matharray}
    2.10  
    2.11    \begin{rail}
    2.12      'datatype' (dtspec + 'and')
    2.13      ;
    2.14 -    'rep\_datatype' (name *) dtrules
    2.15 +    'rep\_datatype' ('(' (name +) ')')? (term +)
    2.16      ;
    2.17  
    2.18      dtspec: parname? typespec infix? '=' (cons + '|')
    2.19      ;
    2.20      cons: name (type *) mixfix?
    2.21 -    ;
    2.22 -    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    2.23    \end{rail}
    2.24  
    2.25    \begin{descr}
    2.26 @@ -460,12 +458,16 @@
    2.27  
    2.28    %FIXME check
    2.29  
    2.30 -  Recursive definitions introduced by both the @{command (HOL)
    2.31 -  "primrec"} and the @{command (HOL) "function"} command accommodate
    2.32 +  Recursive definitions introduced by the @{command (HOL) "function"}
    2.33 +  command accommodate
    2.34    reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
    2.35    "c.induct"} (where @{text c} is the name of the function definition)
    2.36    refers to a specific induction rule, with parameters named according
    2.37 -  to the user-specified equations.  Case names of @{command (HOL)
    2.38 +  to the user-specified equations.
    2.39 +  For the @{command (HOL) "primrec"} the induction principle coincides
    2.40 +  with structural recursion on the datatype the recursion is carried
    2.41 +  out.
    2.42 +  Case names of @{command (HOL)
    2.43    "primrec"} are that of the datatypes involved, while those of
    2.44    @{command (HOL) "function"} are numbered (starting from 1).
    2.45  
    2.46 @@ -985,7 +987,7 @@
    2.47      'code\_modulename' target ( ( string string ) + )
    2.48      ;
    2.49  
    2.50 -    'code\_exception' ( const + )
    2.51 +    'code\_abort' ( const + )
    2.52      ;
    2.53  
    2.54      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
    2.55 @@ -1075,13 +1077,13 @@
    2.56    one module name onto another.
    2.57  
    2.58    \item [@{command (HOL) "code_abort"}] declares constants which
    2.59 -  are not required to have a definition by a defining equations;
    2.60 +  are not required to have a definition by means of defining equations;
    2.61    if needed these are implemented by program abort instead.
    2.62  
    2.63    \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
    2.64    with option ``@{text "del:"}'' deselects) a defining equation for
    2.65    code generation.  Usually packages introducing defining equations
    2.66 -  provide a resonable default setup for selection.
    2.67 +  provide a reasonable default setup for selection.
    2.68  
    2.69    \item [@{attribute (HOL) code}@{text inline}] declares (or with
    2.70    option ``@{text "del:"}'' removes) inlining theorems which are
     3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 03 00:58:30 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 03 11:16:05 2008 +0200
     3.3 @@ -365,20 +365,18 @@
     3.4  \begin{isamarkuptext}%
     3.5  \begin{matharray}{rcl}
     3.6      \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
     3.7 -    \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
     3.8 +  \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\
     3.9    \end{matharray}
    3.10  
    3.11    \begin{rail}
    3.12      'datatype' (dtspec + 'and')
    3.13      ;
    3.14 -    'rep\_datatype' (name *) dtrules
    3.15 +    'rep\_datatype' ('(' (name +) ')')? (term +)
    3.16      ;
    3.17  
    3.18      dtspec: parname? typespec infix? '=' (cons + '|')
    3.19      ;
    3.20      cons: name (type *) mixfix?
    3.21 -    ;
    3.22 -    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    3.23    \end{rail}
    3.24  
    3.25    \begin{descr}
    3.26 @@ -464,10 +462,15 @@
    3.27  
    3.28    %FIXME check
    3.29  
    3.30 -  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
    3.31 +  Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
    3.32 +  command accommodate
    3.33    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)
    3.34    refers to a specific induction rule, with parameters named according
    3.35 -  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
    3.36 +  to the user-specified equations.
    3.37 +  For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
    3.38 +  with structural recursion on the datatype the recursion is carried
    3.39 +  out.
    3.40 +  Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
    3.41    \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
    3.42  
    3.43    The equations provided by these packages may be referred later as
    3.44 @@ -988,7 +991,7 @@
    3.45      'code\_modulename' target ( ( string string ) + )
    3.46      ;
    3.47  
    3.48 -    'code\_exception' ( const + )
    3.49 +    'code\_abort' ( const + )
    3.50      ;
    3.51  
    3.52      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
    3.53 @@ -1075,13 +1078,13 @@
    3.54    one module name onto another.
    3.55  
    3.56    \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which
    3.57 -  are not required to have a definition by a defining equations;
    3.58 +  are not required to have a definition by means of defining equations;
    3.59    if needed these are implemented by program abort instead.
    3.60  
    3.61    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
    3.62    with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
    3.63    code generation.  Usually packages introducing defining equations
    3.64 -  provide a resonable default setup for selection.
    3.65 +  provide a reasonable default setup for selection.
    3.66  
    3.67    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
    3.68    option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are