# HG changeset patch # User wenzelm # Date 1275926958 -7200 # Node ID ca260a17e01340caec10cd2bf4c885aaedfd3194 # Parent a2cde14de4001255fe70ef131481dfd8620222ef# Parent 017146b7d139952ab1c51a3fecb8a4ccc9a1add2 merged; diff -r a2cde14de400 -r ca260a17e013 NEWS --- a/NEWS Mon Jun 07 17:51:26 2010 +0200 +++ b/NEWS Mon Jun 07 18:09:18 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 a2cde14de400 -r ca260a17e013 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 17:51:26 2010 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 18:09:18 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 a2cde14de400 -r ca260a17e013 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 17:51:26 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 18:09:18 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 diff -r a2cde14de400 -r ca260a17e013 src/HOL/Nominal/Examples/CK_Machine.thy --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 07 17:51:26 2010 +0200 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 07 18:09:18 2010 +0200 @@ -491,11 +491,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_VAR y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r a2cde14de400 -r ca260a17e013 src/HOL/Nominal/Examples/Type_Preservation.thy --- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 07 17:51:26 2010 +0200 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 07 18:09:18 2010 +0200 @@ -141,11 +141,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_Var y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique)