# HG changeset patch # User wenzelm # Date 1275931260 -7200 # Node ID dfca6c4cd1e8df3f4f716ee23bf1c9b2903df3ed # Parent ca260a17e01340caec10cd2bf4c885aaedfd3194 more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros; diff -r ca260a17e013 -r dfca6c4cd1e8 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 18:09:18 2010 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 07 19:21:00 2010 +0200 @@ -1320,9 +1320,9 @@ of premises of the case rule; within each premise, the \emph{prefix} 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). + last premise (it is usually the same for all cases). The @{text + "(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 @@ -1344,28 +1344,28 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations @{text "x \ t"} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the 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. - + @{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 @{text + "(no_simp)"} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the @{attribute_def induct_simp} attribute. + The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' specification generalizes variables @{text "x\<^sub>1, \, x\<^sub>m"} of the original goal before applying induction. Thus diff -r ca260a17e013 -r dfca6c4cd1e8 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 18:09:18 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 07 19:21:00 2010 +0200 @@ -1317,9 +1317,8 @@ of premises of the case rule; within each premise, the \emph{prefix} 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). + last premise (it is usually the same for all cases). The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} 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 @@ -1341,28 +1340,27 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the 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. - + \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 \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}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 induction hypotheses may become sufficiently general to get the