# HG changeset patch # User berghofe # Date 1275925950 -7200 # Node ID 250f487b3034698152f515393a01c8b971d763d5 # Parent 7b0ccc20cddc26edde73d341beeeffd4a6b702e3 Documented changes in induct, cases, and nominal_induct method. diff -r 7b0ccc20cddc -r 250f487b3034 NEWS --- 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 *** diff -r 7b0ccc20cddc -r 250f487b3034 doc-src/IsarRef/Thy/Proof.thy --- 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 \ 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 \ x\<^sub>m"}'' specification generalizes variables @{text "x\<^sub>1, \, diff -r 7b0ccc20cddc -r 250f487b3034 doc-src/IsarRef/Thy/document/Proof.tex --- 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