1.1 --- a/NEWS Mon Jun 07 17:51:26 2010 +0200
1.2 +++ b/NEWS Mon Jun 07 18:09:18 2010 +0200
1.3 @@ -469,6 +469,17 @@
1.4 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
1.5 - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
1.6
1.7 +* Method "induct" now takes instantiations of the form t, where t is not
1.8 + a variable, as a shorthand for "x == t", where x is a fresh variable.
1.9 + If this is not intended, t has to be enclosed in parentheses.
1.10 + By default, the equalities generated by definitional instantiations
1.11 + are pre-simplified, which may cause parameters of inductive cases
1.12 + to disappear, or may even delete some of the inductive cases.
1.13 + Use "induct (no_simp)" instead of "induct" to restore the old
1.14 + behaviour. The (no_simp) option is also understood by the "cases"
1.15 + and "nominal_induct" methods, which now perform pre-simplification, too.
1.16 + INCOMPATIBILITY.
1.17 +
1.18
1.19 *** HOLCF ***
1.20
2.1 --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 17:51:26 2010 +0200
2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 18:09:18 2010 +0200
2.3 @@ -1277,16 +1277,16 @@
2.4 ``strengthened'' inductive statements within the object-logic.
2.5
2.6 \begin{rail}
2.7 - 'cases' (insts * 'and') rule?
2.8 + 'cases' '(no_simp)'? (insts * 'and') rule?
2.9 ;
2.10 - 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
2.11 + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
2.12 ;
2.13 'coinduct' insts taking rule?
2.14 ;
2.15
2.16 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
2.17 ;
2.18 - definst: name ('==' | equiv) term | inst
2.19 + definst: name ('==' | equiv) term | '(' term ')' | inst
2.20 ;
2.21 definsts: ( definst *)
2.22 ;
2.23 @@ -1321,6 +1321,8 @@
2.24 of variables is instantiated. In most situations, only a single
2.25 term needs to be specified; this refers to the first variable of the
2.26 last premise (it is usually the same for all cases).
2.27 + The \texttt{no\_simp} option can be used to disable pre-simplification
2.28 + of cases (see the description of @{method induct} below for details).
2.29
2.30 \item @{method induct}~@{text "insts R"} is analogous to the
2.31 @{method cases} method, but refers to induction rules, which are
2.32 @@ -1350,6 +1352,19 @@
2.33 induction principle being involved here. In order to achieve
2.34 practically useful induction hypotheses, some variables occurring in
2.35 @{text t} need to be fixed (see below).
2.36 + Instantiations of the form @{text t}, where @{text t} is not a variable,
2.37 + are taken as a shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is
2.38 + a fresh variable. If this is not intended, @{text t} has to be enclosed in
2.39 + parentheses.
2.40 + By default, the equalities generated by definitional instantiations
2.41 + are pre-simplified using a specific set of rules, usually consisting
2.42 + of distinctness and injectivity theorems for datatypes. This pre-simplification
2.43 + may cause some of the parameters of an inductive case to disappear,
2.44 + or may even completely delete some of the inductive cases, if one of
2.45 + the equalities occurring in their premises can be simplified to @{text False}.
2.46 + The \texttt{no\_simp} option can be used to disable pre-simplification.
2.47 + Additional rules to be used in pre-simplification can be declared using the
2.48 + \texttt{induct\_simp} attribute.
2.49
2.50 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
2.51 specification generalizes variables @{text "x\<^sub>1, \<dots>,
3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 17:51:26 2010 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 18:09:18 2010 +0200
3.3 @@ -1275,16 +1275,16 @@
3.4 ``strengthened'' inductive statements within the object-logic.
3.5
3.6 \begin{rail}
3.7 - 'cases' (insts * 'and') rule?
3.8 + 'cases' '(no_simp)'? (insts * 'and') rule?
3.9 ;
3.10 - 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
3.11 + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
3.12 ;
3.13 'coinduct' insts taking rule?
3.14 ;
3.15
3.16 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
3.17 ;
3.18 - definst: name ('==' | equiv) term | inst
3.19 + definst: name ('==' | equiv) term | '(' term ')' | inst
3.20 ;
3.21 definsts: ( definst *)
3.22 ;
3.23 @@ -1318,6 +1318,8 @@
3.24 of variables is instantiated. In most situations, only a single
3.25 term needs to be specified; this refers to the first variable of the
3.26 last premise (it is usually the same for all cases).
3.27 + The \texttt{no\_simp} option can be used to disable pre-simplification
3.28 + of cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
3.29
3.30 \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
3.31 \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
3.32 @@ -1347,6 +1349,19 @@
3.33 induction principle being involved here. In order to achieve
3.34 practically useful induction hypotheses, some variables occurring in
3.35 \isa{t} need to be fixed (see below).
3.36 + Instantiations of the form \isa{t}, where \isa{t} is not a variable,
3.37 + are taken as a shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is
3.38 + a fresh variable. If this is not intended, \isa{t} has to be enclosed in
3.39 + parentheses.
3.40 + By default, the equalities generated by definitional instantiations
3.41 + are pre-simplified using a specific set of rules, usually consisting
3.42 + of distinctness and injectivity theorems for datatypes. This pre-simplification
3.43 + may cause some of the parameters of an inductive case to disappear,
3.44 + or may even completely delete some of the inductive cases, if one of
3.45 + the equalities occurring in their premises can be simplified to \isa{False}.
3.46 + The \texttt{no\_simp} option can be used to disable pre-simplification.
3.47 + Additional rules to be used in pre-simplification can be declared using the
3.48 + \texttt{induct\_simp} attribute.
3.49
3.50 The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
3.51 specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
4.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 07 17:51:26 2010 +0200
4.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 07 18:09:18 2010 +0200
4.3 @@ -491,11 +491,11 @@
4.4 and b: "\<Gamma> \<turnstile> e' : T'"
4.5 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
4.6 using a b
4.7 -proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
4.8 +proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
4.9 case (t_VAR y T x e' \<Delta>)
4.10 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
4.11 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
4.12 - and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
4.13 + and a3: "\<Gamma> \<turnstile> e' : T'" .
4.14 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
4.15 { assume eq: "x=y"
4.16 from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
5.1 --- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 07 17:51:26 2010 +0200
5.2 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 07 18:09:18 2010 +0200
5.3 @@ -141,11 +141,11 @@
5.4 and b: "\<Gamma> \<turnstile> e' : T'"
5.5 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
5.6 using a b
5.7 -proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
5.8 +proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
5.9 case (t_Var y T x e' \<Delta>)
5.10 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
5.11 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
5.12 - and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
5.13 + and a3: "\<Gamma> \<turnstile> e' : T'" .
5.14 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
5.15 { assume eq: "x=y"
5.16 from a1 a2 have "T=T'" using eq by (auto intro: context_unique)