updated generated file;
authorwenzelm
Tue Jun 10 19:15:17 2008 +0200 (2008-06-10)
changeset 27124e02d6e655e60
parent 27123 11fcdd5897dd
child 27125 0733f575b51e
updated generated file;
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/Proof.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 19:15:16 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jun 10 19:15:17 2008 +0200
     1.3 @@ -779,19 +779,20 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsection{Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac}%
     1.8 +\isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
    1.12  \begin{isamarkuptext}%
    1.13 -The following important tactical tools of Isabelle/HOL have been
    1.14 -  ported to Isar.  These should be never used in proper proof texts!
    1.15 +The following tools of Isabelle/HOL support cases analysis and
    1.16 +  induction in unstructured tactic scripts; see also
    1.17 +  \secref{sec:cases-induct} for proper Isar versions of similar ideas.
    1.18  
    1.19    \begin{matharray}{rcl}
    1.20      \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.21      \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.22      \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    1.23 -    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
    1.24 +    \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{theory} \\
    1.25    \end{matharray}
    1.26  
    1.27    \begin{rail}
    1.28 @@ -811,12 +812,15 @@
    1.29    \begin{descr}
    1.30  
    1.31    \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
    1.32 -  admit to reason about inductive datatypes only (unless an
    1.33 -  alternative rule is given explicitly).  Furthermore, \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} does a classical case split on booleans; \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} allows only variables to be given as instantiation.
    1.34 -  These tactic emulations feature both goal addressing and dynamic
    1.35 +  admit to reason about inductive types.  Rules are selected according
    1.36 +  to the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
    1.37 +
    1.38 +  These unstructured tactics feature both goal addressing and dynamic
    1.39    instantiation.  Note that named rule cases are \emph{not} provided
    1.40 -  as would be by the proper \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} proof
    1.41 -  methods (see \secref{sec:cases-induct}).
    1.42 +  as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof
    1.43 +  methods (see \secref{sec:cases-induct}).  Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} does not handle structured rule
    1.44 +  statements, only the compact object-logic conclusion of the subgoal
    1.45 +  being addressed.
    1.46    
    1.47    \item [\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted
    1.48    forward manner.
     2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Jun 10 19:15:16 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue Jun 10 19:15:17 2008 +0200
     2.3 @@ -349,7 +349,7 @@
     2.4    meaning: (1) during the of this claim they refer to the the local
     2.5    context introductions, (2) the resulting rule is annotated
     2.6    accordingly to support symbolic case splits when used with the
     2.7 -  \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.  \secref{sec:cases-induct}).
     2.8 +  \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} method (cf.\ \secref{sec:cases-induct}).
     2.9  
    2.10    \medskip
    2.11