case_tac/induct_tac: use same declarations as cases/induct;
authorwenzelm
Tue Jun 10 19:15:16 2008 +0200 (2008-06-10)
changeset 2712311fcdd5897dd
parent 27122 63d92a5e3784
child 27124 e02d6e655e60
case_tac/induct_tac: use same declarations as cases/induct;
doc-src/IsarRef/Thy/HOL_Specific.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 19:15:14 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 19:15:16 2008 +0200
     1.3 @@ -773,17 +773,18 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -section {* Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac} *}
     1.8 +section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *}
     1.9  
    1.10  text {*
    1.11 -  The following important tactical tools of Isabelle/HOL have been
    1.12 -  ported to Isar.  These should be never used in proper proof texts!
    1.13 +  The following tools of Isabelle/HOL support cases analysis and
    1.14 +  induction in unstructured tactic scripts; see also
    1.15 +  \secref{sec:cases-induct} for proper Isar versions of similar ideas.
    1.16  
    1.17    \begin{matharray}{rcl}
    1.18      @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
    1.19      @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
    1.20      @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
    1.21 -    @{command_def (HOL) "inductive_cases"} & : & \isartrans{theory}{theory} \\
    1.22 +    @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & \isartrans{theory}{theory} \\
    1.23    \end{matharray}
    1.24  
    1.25    \begin{rail}
    1.26 @@ -803,14 +804,18 @@
    1.27    \begin{descr}
    1.28  
    1.29    \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}]
    1.30 -  admit to reason about inductive datatypes only (unless an
    1.31 -  alternative rule is given explicitly).  Furthermore, @{method (HOL)
    1.32 -  case_tac} does a classical case split on booleans; @{method (HOL)
    1.33 -  induct_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 @{attribute cases} and @{attribute
    1.37 +  induct} attributes, cf.\ \secref{sec:cases-induct}.  The @{command
    1.38 +  (HOL) datatype} package already takes care of this.
    1.39 +
    1.40 +  These unstructured tactics feature both goal addressing and dynamic
    1.41    instantiation.  Note that named rule cases are \emph{not} provided
    1.42 -  as would be by the proper @{method induct} and @{method cases} proof
    1.43 -  methods (see \secref{sec:cases-induct}).
    1.44 +  as would be by the proper @{method cases} and @{method induct} proof
    1.45 +  methods (see \secref{sec:cases-induct}).  Unlike the @{method
    1.46 +  induct} method, @{method induct_tac} does not handle structured rule
    1.47 +  statements, only the compact object-logic conclusion of the subgoal
    1.48 +  being addressed.
    1.49    
    1.50    \item [@{method (HOL) ind_cases} and @{command (HOL)
    1.51    "inductive_cases"}] provide an interface to the internal @{ML_text