Documented changes in induct, cases, and nominal_induct method.
--- a/NEWS Mon Jun 07 17:13:36 2010 +0200
+++ b/NEWS Mon Jun 07 17:52:30 2010 +0200
@@ -469,6 +469,17 @@
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
- Removed "nitpick_intro" attribute. INCOMPATIBILITY.
+* Method "induct" now takes instantiations of the form t, where t is not
+ a variable, as a shorthand for "x == t", where x is a fresh variable.
+ If this is not intended, t has to be enclosed in parentheses.
+ By default, the equalities generated by definitional instantiations
+ are pre-simplified, which may cause parameters of inductive cases
+ to disappear, or may even delete some of the inductive cases.
+ Use "induct (no_simp)" instead of "induct" to restore the old
+ behaviour. The (no_simp) option is also understood by the "cases"
+ and "nominal_induct" methods, which now perform pre-simplification, too.
+ INCOMPATIBILITY.
+
*** HOLCF ***
--- 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>,
--- 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