# HG changeset patch # User wenzelm # Date 1191614411 -7200 # Node ID 9b9b1599fb8978f3a7817ffa9acd51dfc3f7c7c3 # Parent a3a81e73f552a9f192d119cfa8c5111f8b6ba19d tuned induct etc.; diff -r a3a81e73f552 -r 9b9b1599fb89 NEWS --- a/NEWS Fri Oct 05 20:10:35 2007 +0200 +++ b/NEWS Fri Oct 05 22:00:11 2007 +0200 @@ -458,7 +458,7 @@ definition specification element in the context of locale partial_order. -* Provers/induct: improved internal context management to support +* Method "induct": improved internal context management to support local fixes and defines on-the-fly. Thus explicit meta-level connectives !! and ==> are rarely required anymore in inductive goals (using object-logic connectives for this purpose has been long @@ -466,28 +466,32 @@ HOL/Induct/Common_Patterns.thy, see also HOL/Isar_examples/Puzzle.thy and src/HOL/Lambda for realistic examples. -* Provers/induct: improved handling of simultaneous goals. Instead of +* Method "induct": improved handling of simultaneous goals. Instead of introducing object-level conjunction, the statement is now split into several conclusions, while the corresponding symbolic cases are nested accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, see HOL/Induct/Common_Patterns.thy, for example. -* Provers/induct: mutual induction rules are now specified as a list +* Method "induct": mutual induction rules are now specified as a list of rule sharing the same induction cases. HOL packages usually provide foo_bar.inducts for mutually defined items foo and bar (e.g. inductive -sets or datatypes). INCOMPATIBILITY, users need to specify mutual -induction rules differently, i.e. like this: +predicates/sets or datatypes). INCOMPATIBILITY, users need to specify +mutual induction rules differently, i.e. like this: (induct rule: foo_bar.inducts) (induct set: foo bar) + (induct pred: foo bar) (induct type: foo bar) The ML function ProjectRule.projections turns old-style rules into the new format. -* Provers/induct: support coinduction as well. See +* Method "coinduct": dual of induction, see src/HOL/Library/Coinductive_List.thy for various examples. +* Method "cases", "induct", "coinduct": the ``(open)'' option is +considered a legacy feature. + * Attribute "symmetric" produces result with standardized schematic variables (index 0). Potential INCOMPATIBILITY. diff -r a3a81e73f552 -r 9b9b1599fb89 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Fri Oct 05 20:10:35 2007 +0200 +++ b/doc-src/IsarRef/generic.tex Fri Oct 05 22:00:11 2007 +0200 @@ -1660,13 +1660,14 @@ coinduct & : & \isarmeth \\ \end{matharray} -The $cases$, $induct$, and $coinduct$ methods provide a uniform interface to -common proof techniques over datatypes, inductive sets, recursive functions -etc. The corresponding rules may be specified and instantiated in a casual -manner. Furthermore, these methods provide named local contexts that may be -invoked via the $\CASENAME$ proof command within the subsequent proof text. -This accommodates compact proof texts even when reasoning about large -specifications. +The $cases$, $induct$, and $coinduct$ methods provide a uniform +interface to common proof techniques over datatypes, inductive +predicates (or sets), recursive functions etc. The corresponding +rules may be specified and instantiated in a casual manner. +Furthermore, these methods provide named local contexts that may be +invoked via the $\CASENAME$ proof command within the subsequent proof +text. This accommodates compact proof texts even when reasoning about +large specifications. The $induct$ method also provides some additional infrastructure in order to be applicable to structure statements (either using explicit meta-level @@ -1675,16 +1676,14 @@ object-logic. \begin{rail} - 'cases' open? (insts * 'and') rule? + 'cases' (insts * 'and') rule? ; - 'induct' open? (definsts * 'and') \\ arbitrary? taking? rule? + 'induct' (definsts * 'and') \\ arbitrary? taking? rule? ; - 'coinduct' open? insts taking rule? + 'coinduct' insts taking rule? ; - open: '(' 'open' ')' - ; - rule: ('type' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) + rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) ; definst: name ('==' | equiv) term | inst ; @@ -1708,7 +1707,7 @@ \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline & cases & & \Text{classical case split} \\ & cases & t & \Text{datatype exhaustion (type of $t$)} \\ - \edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\ + \edrv A\; t & cases & \dots & \Text{inductive predicate/set elimination (of $A$)} \\ \dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ \end{matharray} @@ -1718,19 +1717,12 @@ be specified; this refers to the first variable of the last premise (it is usually the same for all cases). - The ``$(open)$'' option causes the parameters of the new local contexts to - be exposed to the current proof context. Thus local variables stemming from - distant parts of the theory development may be introduced in an implicit - manner, which can be quite confusing to the reader. Furthermore, this - option may cause unwanted hiding of existing local variables, resulting in - less robust proof texts. - \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to induction rules, which are determined as follows: \begin{matharray}{llll} \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ - \edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\ + \edrv A\; x & induct & \dots & \Text{predicate/set induction (of $A$)} \\ \dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ \end{matharray} @@ -1758,30 +1750,28 @@ instantiations of a prefix of pending variables in the rule. Such schematic induction rules rarely occur in practice, though. - The ``$(open)$'' option works the same way as for $cases$. - \item [$coinduct~inst~R$] is analogous to the $induct$ method, but refers to coinduction rules, which are determined as follows: \begin{matharray}{llll} \Text{goal} & & \Text{arguments} & \Text{rule} \\\hline & coinduct & x ~ \dots & \Text{type coinduction (type of $x$)} \\ - x \in A & coinduct & \dots & \Text{set coinduction (of $A$)} \\ + A\; x & coinduct & \dots & \Text{predicate/set coinduction (of $A$)} \\ \dots & coinduct & \dots ~ R & \Text{explicit rule $R$} \\ \end{matharray} - Coinduction is the dual of induction. Induction essentially eliminates $x - \in A$ towards a generic result $P ~ x$, while coinduction introduces $x \in - A$ starting with $x \in B$, for a suitable ``bisimulation'' $B$. The cases - of a coinduct rule are typically named after the sets being covered, while - the conclusions consist of several alternatives being named after the + Coinduction is the dual of induction. Induction essentially + eliminates $A\; x$ towards a generic result $P\; x$, while + coinduction introduces $A\; x$ starting with $B\; x$, for a suitable + ``bisimulation'' $B$. The cases of a coinduct rule are typically + named after the predicates or sets being covered, while the + conclusions consist of several alternatives being named after the individual destructor patterns. - The given instantiation refers to the \emph{prefix} of variables occurring - in the rule's conclusion. An additional ``$taking: \vec t$'' specification - may be required in order to specify the bisimulation to be used in the - coinduction step. - - The ``$(open)$'' option works the same way as for $cases$. + The given instantiation refers to the \emph{suffix} of variables + occurring in the rule's major premise, or conclusion if unavailable. + An additional ``$taking: \vec t$'' specification may be required in + order to specify the bisimulation to be used in the coinduction + step. \end{descr} @@ -1819,11 +1809,12 @@ \medskip -Facts presented to either method are consumed according to the number of -``major premises'' of the rule involved, which is usually $0$ for plain cases -and induction rules of datatypes etc.\ and $1$ for rules of inductive sets and -the like. The remaining facts are inserted into the goal verbatim before the -actual $cases$, $induct$, or $coinduct$ rule is applied. +Facts presented to either method are consumed according to the number +of ``major premises'' of the rule involved, which is usually $0$ for +plain cases and induction rules of datatypes etc.\ and $1$ for rules +of inductive predicates or sets and the like. The remaining facts are +inserted into the goal verbatim before the actual $cases$, $induct$, +or $coinduct$ rule is applied. \subsubsection{Declaring rules} @@ -1844,25 +1835,27 @@ 'coinduct' spec ; - spec: ('type' | 'set') ':' nameref + spec: ('type' | 'pred' | 'set') ':' nameref ; \end{rail} \begin{descr} -\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for - sets and types of the current context. +\item [$\isarkeyword{print_induct_rules}$] prints cases and induct + rules for predicates (or sets) and types of the current context. \item [$cases$, $induct$, and $coinduct$] (as attributes) augment the - corresponding context of rules for reasoning about (co)inductive sets and - types, using the corresponding methods of the same name. Certain - definitional packages of object-logics usually declare emerging cases and - induction rules as expected, so users rarely need to intervene. + corresponding context of rules for reasoning about (co)inductive + predicates (or sets) and types, using the corresponding methods of + the same name. Certain definitional packages of object-logics + usually declare emerging cases and induction rules as expected, so + users rarely need to intervene. - Manual rule declarations usually refer to the $case_names$ and $params$ - attributes to adjust names of cases and parameters of a rule; the $consumes$ - declaration is taken care of automatically: $consumes~0$ is specified for - ``type'' rules and $consumes~1$ for ``set'' rules. + Manual rule declarations usually refer to the $case_names$ and + $params$ attributes to adjust names of cases and parameters of a + rule; the $consumes$ declaration is taken care of automatically: + $consumes~0$ is specified for ``type'' rules and $consumes~1$ for + ``predicate'' / ``set'' rules. \end{descr}