--- 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}