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