--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 17:13:36 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 17:52:30 2010 +0200
@@ -1275,16 +1275,16 @@
``strengthened'' inductive statements within the object-logic.
\begin{rail}
- 'cases' (insts * 'and') rule?
+ 'cases' '(no_simp)'? (insts * 'and') rule?
;
- 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
+ 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
;
'coinduct' insts taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
;
- definst: name ('==' | equiv) term | inst
+ definst: name ('==' | equiv) term | '(' term ')' | inst
;
definsts: ( definst *)
;
@@ -1318,6 +1318,8 @@
of variables is instantiated. In most situations, only a single
term needs to be specified; this refers to the first variable of the
last premise (it is usually the same for all cases).
+ The \texttt{no\_simp} option can be used to disable pre-simplification
+ of cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
\item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
\hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
@@ -1347,6 +1349,19 @@
induction principle being involved here. In order to achieve
practically useful induction hypotheses, some variables occurring in
\isa{t} need to be fixed (see below).
+ Instantiations of the form \isa{t}, where \isa{t} is not a variable,
+ are taken as a shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is
+ a fresh variable. If this is not intended, \isa{t} has to be enclosed in
+ parentheses.
+ By default, the equalities generated by definitional instantiations
+ are pre-simplified using a specific set of rules, usually consisting
+ of distinctness and injectivity theorems for datatypes. This pre-simplification
+ may cause some of the parameters of an inductive case to disappear,
+ or may even completely delete some of the inductive cases, if one of
+ the equalities occurring in their premises can be simplified to \isa{False}.
+ The \texttt{no\_simp} option can be used to disable pre-simplification.
+ Additional rules to be used in pre-simplification can be declared using the
+ \texttt{induct\_simp} attribute.
The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus