author wenzelm Wed, 23 Nov 2005 18:51:59 +0100 changeset 18232 bc367912603f parent 18231 2eea98bbf650 child 18233 5a124c76e92f
--- 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

\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.
+
\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$
+  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}