--- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 17:13:36 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 17:52:30 2010 +0200
@@ -1277,16 +1277,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 *)
;
@@ -1321,6 +1321,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 @{method induct} below for details).
\item @{method induct}~@{text "insts R"} is analogous to the
@{method cases} method, but refers to induction rules, which are
@@ -1350,6 +1352,19 @@
induction principle being involved here. In order to achieve
practically useful induction hypotheses, some variables occurring in
@{text t} need to be fixed (see below).
+ Instantiations of the form @{text t}, where @{text t} is not a variable,
+ are taken as a shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is
+ a fresh variable. If this is not intended, @{text 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 @{text 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 ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
specification generalizes variables @{text "x\<^sub>1, \<dots>,