# HG changeset patch # User wenzelm # Date 1132768319 -3600 # Node ID bc367912603f9d2dc71788588413a169b16277b7 # Parent 2eea98bbf65081b801eb857bbdd56122d6d8171d added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned; diff -r 2eea98bbf650 -r bc367912603f doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Wed Nov 23 17:16:42 2005 +0100 +++ b/doc-src/IsarRef/generic.tex Wed Nov 23 18:51:59 2005 +0100 @@ -1209,51 +1209,56 @@ \subsubsection{Rule contexts} \indexisarcmd{case}\indexisarcmd{print-cases} -\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} +\indexisaratt{case-names}\indexisaratt{case-conclusion} +\indexisaratt{params}\indexisaratt{consumes} \begin{matharray}{rcl} \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{print_cases}^* & : & \isarkeep{proof} \\ case_names & : & \isaratt \\ + case_conclusion & : & \isaratt \\ params & : & \isaratt \\ consumes & : & \isaratt \\ \end{matharray} -Basically, Isar proof contexts are built up explicitly using commands like -$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical -verification tasks this can become hard to manage, though. In particular, a -large number of local contexts may emerge from case analysis or induction over -inductive sets and types. +The puristic way to build up Isar proof contexts is by explicit language +elements like $\FIXNAME$, $\ASSUMENAME$, $\LET$ (see +\S\ref{sec:proof-context}). This is adequate for plain natural deduction, but +easily becomes unwieldy in concrete verification tasks, which typically +involve big induction rules with several cases. + +The $\CASENAME$ command provides a shorthand to refer to a local context +symbolically: certain proof methods provide an environment of named ``cases'' +of the form $c\colon \vec x, \vec \phi$; the effect of ``$\CASE{c}$'' is then +equivalent to ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term bindings may be +covered as well, notably $\Var{case}$ for the main conclusion. + +By default, the ``terminology'' $\vec x$ of a case value is marked as hidden, +i.e.\ there is no way to refer to such parameters in the subsequent proof +text. After all, original rule parameters stem from somewhere outside of the +current proof text. By using the explicit form ``$\CASE{(c~\vec y)}$'' +instead, the proof author is able to chose local names that fit nicely into +the current context. \medskip -The $\CASENAME$ command provides a shorthand to refer to certain parts of -logical context symbolically. Proof methods may provide an environment of -named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of -``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term -bindings may be covered as well, such as $\Var{case}$ for the intended -conclusion. +It is important to note that proper use of $\CASENAME$ does not provide means +to peek at the current goal state, which is not directly observable in Isar! +Nonetheless, goal refinement commands do provide named cases $goal@i$ for each +subgoal $i = 1, \dots, n$ of the resulting goal state. Using this feature +requires great care, because some bits of the internal tactical machinery +intrude the proof text. In particular, parameter names stemming from the +left-over of automated reasoning tools are usually quite unpredictable. -Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$) -are marked as hidden. Using the explicit form ``$\CASE{(c~\vec x)}$'' enables -proof writers to choose their own names for the subsequent proof text. - -\medskip - -It is important to note that $\CASENAME$ does \emph{not} provide direct means -to peek at the current goal state, which is generally considered -non-observable in Isar. The text of the cases basically emerge from standard -elimination or induction rules, which in turn are derived from previous theory +Under normal circumstances, the text of cases emerge from standard elimination +or induction rules, which in turn are derived from previous theory specifications in a canonical way (say from $\isarkeyword{inductive}$ definitions). -Named cases may be exhibited in the current proof context only if both the -proof method and the rules involved support this. Case names and parameters -of basic rules may be declared by hand as well, by using appropriate -attributes. Thus variant versions of rules that have been derived manually -may be used in advanced case analysis later. - -\railalias{casenames}{case\_names} -\railterm{casenames} +\medskip Proper cases are only available if both the proof method and the +rules involved support this. By using appropriate attributes, case names, +conclusions, and parameters may be also declared by hand. Thus variant +versions of rules that have been derived manually become reasy to use in +advanced case analysis later. \begin{rail} 'case' (caseref | '(' caseref ((name | underscore) +) ')') @@ -1261,7 +1266,9 @@ caseref: nameref attributes? ; - casenames (name +) + 'case\_names' (name +) + ; + 'case\_conclusion' name (name *) ; 'params' ((name *) + 'and') ; @@ -1270,71 +1277,91 @@ \end{rail} \begin{descr} - + \item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x, \vec \phi$, as provided by an appropriate proof method (such as $cases$ and - $induct$, see \S\ref{sec:cases-induct-meth}). The command ``$\CASE{(c~\vec - x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. + $induct$). The command ``$\CASE{(c~\vec x)}$'' abbreviates ``$\FIX{\vec + x}~\ASSUME{c}{\vec\phi}$''. \item [$\isarkeyword{print_cases}$] prints all local contexts of the current state, using Isar proof language notation. This is a diagnostic command; $undo$ does not apply. - + \item [$case_names~\vec c$] declares names for the local contexts of premises - of some theorem; $\vec c$ refers to the \emph{suffix} of the list of - premises. + of a theorem; $\vec c$ refers to the \emph{suffix} of the list of premises. + +\item [$case_conclusion~c~\vec d$] declares names for the conclusions of a + named premise $c$; here $\vec d$ refers to the prefix of arguments of a + logical formula built by nesting a binary connective (e.g.\ $\lor$). + + Note that proof methods such as $induct$ and $coinduct$ already provide a + default name for the conclusion as a whole. The need to name subformulas + only arises with cases that split into several sub-cases, as in common + co-induction rules. \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of premises $1, \dots, n$ of some theorem. An empty list of names may be given to skip positions, leaving the present parameters unchanged. - + Note that the default usage of case rules does \emph{not} directly expose - parameters to the proof context (see also \S\ref{sec:cases-induct-meth}). - + parameters to the proof context. + \item [$consumes~n$] declares the number of ``major premises'' of a rule, i.e.\ the number of facts to be consumed when it is applied by an - appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default - value of $consumes$ is $n = 1$, which is appropriate for the usual kind of - cases and induction rules for inductive sets (cf.\ - \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given - are treated as if $consumes~0$ had been specified. - + appropriate proof method. The default value of $consumes$ is $n = 1$, which + is appropriate for the usual kind of cases and induction rules for inductive + sets (cf.\ \S\ref{sec:hol-inductive}). Rules without any $consumes$ + declaration given are treated as if $consumes~0$ had been specified. + Note that explicit $consumes$ declarations are only rarely needed; this is - already taken care of automatically by the higher-level $cases$ and $induct$ - declarations, see also \S\ref{sec:cases-induct-att}. + already taken care of automatically by the higher-level $cases$, $induct$, + and $coinduct$ declarations. \end{descr} -\subsubsection{Proof methods}\label{sec:cases-induct-meth} +\subsubsection{Proof methods} -\indexisarmeth{cases}\indexisarmeth{induct} +\indexisarmeth{cases}\indexisarmeth{induct}\indexisarmeth{coinduct} \begin{matharray}{rcl} cases & : & \isarmeth \\ induct & : & \isarmeth \\ + coinduct & : & \isarmeth \\ \end{matharray} -The $cases$ and $induct$ methods provide a uniform interface to case analysis -and induction over datatypes, inductive sets, and recursive functions. 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 +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 $induct$ method also provides some additional infrastructure in order to +be applicable to structure statements (either using explicit meta-level +connectives, or including facts and parameters separately). This avoids +cumbersome encoding of ``strengthened'' inductive statements within the +object-logic. + \begin{rail} - 'cases' spec + 'cases' open? (insts * 'and') rule? ; - 'induct' spec + 'induct' open? (definsts * 'and') \\ fixing? taking? rule? + ; + 'coinduct' open? insts taking rule? ; - spec: open? args rule? - ; open: '(' 'open' ')' ; - args: (insts * 'and') + rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref + ; + definst: name ('==' | equiv) term | inst ; - rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref + definsts: ( definst *) + ; + fixing: 'fixing' ':' ((term *) 'and' +) + ; + taking: 'taking' ':' insts ; \end{rail} @@ -1382,40 +1409,76 @@ refers to the \emph{suffix} of variables 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 $x \equiv 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 $t$ need to be fixed (see below). + + The optional ``$fixing\colon \vec x$'' specification generalizes variables + $\vec x$ of the original goal before applying induction. Thus induction + hypotheses may become sufficiently general to get the proof through. + Together with definitional instantiations, one may effectively perform + induction over expressions of a certain structure. + + The optional ``$taking\colon \vec t$'' specification provides additional + 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$)} \\ + \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 + 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$. \end{descr} Above methods produce named local contexts, as determined by the instantiated -rule as specified in the text. Beyond that, the $induct$ method guesses -further instantiations from the goal specification itself. Any persisting -unresolved schematic variables of the resulting rule will render the the -corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case} -for the conclusion will be provided with each case, provided that term is -fully specified. +rule as given in the text. Beyond that, the $induct$ and $coinduct$ methods +guess further instantiations from the goal specification itself. Any +persisting unresolved schematic variables of the resulting rule will render +the the corresponding case invalid. The term binding +$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each +case, provided that term is fully specified. The $\isarkeyword{print_cases}$ command prints all named cases present in the current proof state. \medskip -It is important to note that there is a fundamental difference of the $cases$ -and $induct$ methods in handling of non-atomic goal statements: $cases$ just -applies a certain rule in backward fashion, splitting the result into new -goals with the local contexts being augmented in a purely monotonic manner. +Despite the additional infrastructure, both $cases$ and $coinduct$ merely +apply a certain rule, after instantiation, while conforming due to the usual +way of monotonic natural deduction: the context of a structured statement +$\All{\vec x} \vec\phi \Imp \dots$ reappears unchanged after the case split. -In contrast, $induct$ passes the full goal statement through the -``recursive'' course involved in the induction. Thus the original statement -is basically replaced by separate copies, corresponding to the induction -hypotheses and conclusion; the original goal context is no longer available. -This behavior allows \emph{strengthened induction predicates} to be expressed -concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp -\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive'' -assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs -``$\FIX{\vec x}$''. Also note that local definitions may be expressed as -$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. - +The $induct$ method is significantly different in this respect: the meta-level +structure is passed through the ``recursive'' course involved in the +induction. Thus the original statement is basically replaced by separate +copies, corresponding to the induction hypotheses and conclusion; the original +goal context is no longer available. Thus local assumptions, fixed parameters +and definitions effectively participate in the inductive rephrasing of the +original statement. In induction proofs, local assumptions introduced by cases are split into two different kinds: $hyps$ stemming from the rule and $prems$ from the goal @@ -1426,20 +1489,20 @@ \medskip Facts presented to either method are consumed according to the number of -``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}), -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$ or $induct$ rule is -applied (thus facts may be even passed through an induction). +``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. -\subsubsection{Declaring rules}\label{sec:cases-induct-att} +\subsubsection{Declaring rules} -\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} +\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}\indexisaratt{coinduct} \begin{matharray}{rcl} \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ cases & : & \isaratt \\ induct & : & \isaratt \\ + coinduct & : & \isaratt \\ \end{matharray} \begin{rail} @@ -1447,6 +1510,8 @@ ; 'induct' spec ; + 'coinduct' spec + ; spec: ('type' | 'set') ':' nameref ; @@ -1456,18 +1521,17 @@ \item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for sets and types of the current context. - -\item [$cases$ and $induct$] (as attributes) augment the corresponding context - of rules for reasoning about 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. - Manual rule declarations usually include the the $case_names$ and $ps$ - attributes to adjust names of cases and parameters of a rule (see - \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of - automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$ - for ``set'' rules. +\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. + + 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. \end{descr}