author wenzelm Thu, 04 Oct 2001 16:09:12 +0200 changeset 11691 fc9bd420162c parent 11690 cb64368fb405 child 11692 6d15ae4b1123
induct/cases made generic, removed simplified/stripped options;
 doc-src/IsarRef/generic.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/hol.tex file | annotate | diff | comparison | revisions
--- a/doc-src/IsarRef/generic.tex	Thu Oct 04 16:07:43 2001 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Oct 04 16:09:12 2001 +0200
@@ -854,6 +854,182 @@
\end{descr}

+\section{Proof by cases and induction}\label{sec:induct-method}
+
+\subsection{Proof methods}\label{sec:induct-method-proper}
+
+\indexisarmeth{cases}\indexisarmeth{induct}
+\begin{matharray}{rcl}
+  cases & : & \isarmeth \\
+  induct & : & \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 (cf.\
+\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
+
+Note that the full spectrum of this generic functionality is currently only
+supported by Isabelle/HOL, when used in conjunction with advanced definitional
+packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).
+
+\begin{rail}
+  'cases' spec
+  ;
+  'induct' spec
+  ;
+
+  spec: open? args rule? params?
+  ;
+  open: '(' 'open' ')'
+  ;
+  args: (insts * 'and')
+  ;
+  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
+  ;
+  params: 'of' ':' insts
+  ;
+\end{rail}
+
+\begin{descr}
+\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
+  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
+  names are bound according to the rule's local contexts.
+
+  The rule is determined as follows, according to the facts and arguments
+  passed to the $cases$ method:
+  \begin{matharray}{llll}
+    \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$)} \\
+    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
+  \end{matharray}
+
+  Several instantiations may be given, referring to the \emph{suffix} of
+  premises of the case rule; within each premise, the \emph{prefix} of
+  variables is instantiated.  In most situations, only a single term needs to
+  be specified; this refers to the first variable of the last premise (it is
+  usually the same for all cases).
+
+  Additional parameters may be specified as $ps$; these are applied after the
+  primary instantiation in the same manner as by the $of$ attribute (cf.\
+  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
+  typical application would be to specify additional arguments for rules
+  \S\ref{sec:inductive}).
+
+  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~ps$] 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$)} \\
+    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
+  \end{matharray}
+
+  Several instantiations may be given, each referring to some part of a mutual
+  inductive definition or datatype --- only related partial induction rules
+  may be used together, though.  Any of the lists of terms $P, x, \dots$
+  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.
+
+  Additional parameters (including the $open$ option) may be given in the same
+  way as for $cases$, see above.
+\end{descr}
+
+Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
+determined by the instantiated rule \emph{before} it has been applied to the
+internal proof state.\footnote{As a general principle, Isar proof text may
+  never refer to parts of proof states directly.} Thus proper use of symbolic
+cases usually require the rule to be instantiated fully, as far as the
+emerging local contexts and subgoals are concerned.  In particular, for
+induction both the predicates and variables have to be specified.  Otherwise
+the $\CASENAME$ command would refuse to invoke cases containing schematic
+variables.  Furthermore the resulting local goal statement is bound to the
+term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
+fully specified.
+
+The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) 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.
+
+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$.  Also note that local definitions may be expressed as $\All{\vec + x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
+
+\medskip
+
+Facts presented to either method are consumed according to the number of
+major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
+\S\ref{sec:cases}), 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).
+
+Note that whenever facts are present, the default rule selection scheme would
+provide a set'' rule only, with the first fact consumed and the rest
+inserted into the goal.  In order to pass all facts into a type'' rule
+instead, one would have to specify this explicitly, e.g.\ by appending
+$type: name$'' to the method argument.
+
+
+\subsection{Declaring rules}\label{sec:induct-att}
+
+\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
+\begin{matharray}{rcl}
+  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
+  cases & : & \isaratt \\
+  induct & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+  'cases' spec
+  ;
+  'induct' spec
+  ;
+
+  spec: ('type' | 'set') ':' nameref
+  ;
+\end{rail}
+
+The $cases$ and $induct$ attributes augment the corresponding context of rules
+for reasoning about inductive sets and types.  The standard rules are already
+declared by advanced definitional packages.  For special applications, these
+may be replaced manually by variant versions.
+
+Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
+adjust names of cases and parameters of a rule.
+
+The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
+automatically (if none had been given already): $consumes~0$ is specified for
+type'' rules and $consumes~1$ for set'' rules.
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
--- a/doc-src/IsarRef/hol.tex	Thu Oct 04 16:07:43 2001 +0200
+++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 16:09:12 2001 +0200
@@ -43,7 +43,7 @@
\end{descr}

-\section{Primitive types}
+\section{Primitive types}\label{sec:typedef}

\indexisarcmd{typedecl}\indexisarcmd{typedef}
\begin{matharray}{rcl}
@@ -140,7 +140,7 @@
\S\ref{sec:induct_tac}.

-\section{Recursive functions}
+\section{Recursive functions}\label{sec:recursion}

\indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
\begin{matharray}{rcl}
@@ -278,190 +278,33 @@
HOL.

-\section{Proof by cases and induction}\label{sec:induct-method}
-%FIXME move to generic.tex
-
-\subsection{Proof methods}\label{sec:induct-method-proper}
+\section{Arithmetic}

-\indexisarmeth{cases}\indexisarmeth{induct}
+\indexisarmeth{arith}\indexisaratt{arith-split}
\begin{matharray}{rcl}
-  cases & : & \isarmeth \\
-  induct & : & \isarmeth \\
+  arith & : & \isarmeth \\
+  arith_split & : & \isaratt \\
\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 (cf.\
-\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
-
\begin{rail}
-  'cases' ('(' 'simplified' ')')? spec
-  ;
-  'induct' ('(' 'stripped' ')')? spec
-  ;
-
-  spec: open? args rule? params?
-  ;
-  open: '(' 'open' ')'
-  ;
-  args: (insts * 'and')
-  ;
-  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
-  ;
-  params: 'of' ':' insts
+  'arith' '!'?
;
\end{rail}

-\begin{descr}
-\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
-  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
-  names are bound according to the rule's local contexts.
-
-  The rule is determined as follows, according to the facts and arguments
-  passed to the $cases$ method:
-  \begin{matharray}{llll}
-    \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$)} \\
-    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
-  \end{matharray}
-
-  Several instantiations may be given, referring to the \emph{suffix} of
-  premises of the case rule; within each premise, the \emph{prefix} of
-  variables is instantiated.  In most situations, only a single term needs to
-  be specified; this refers to the first variable of the last premise (it is
-  usually the same for all cases).
-
-  Additional parameters may be specified as $ps$; these are applied after the
-  primary instantiation in the same manner as by the $of$ attribute (cf.\
-  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
-  typical application would be to specify additional arguments for rules
-  \S\ref{sec:inductive}).
+The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
+$real$).  Any current facts are inserted into the goal before running the
+procedure.  The !''~argument causes the full context of assumptions to be
+included.  The $arith_split$ attribute declares case split rules to be
+expanded before the arithmetic procedure is invoked.

-  The $simplified$ option causes obvious cases'' of the rule to be solved
-  beforehand, while the others are left unscathed.
-
-  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~ps$] 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$)} \\
-    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
-  \end{matharray}
-
-  Several instantiations may be given, each referring to some part of a mutual
-  inductive definition or datatype --- only related partial induction rules
-  may be used together, though.  Any of the lists of terms $P, x, \dots$
-  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.
-
-  Additional parameters may be given in the same way as for $cases$.
-
-  The $stripped$ option causes implications and (bounded) universal
-  quantifiers to be removed from each new subgoal emerging from the
-  application of the induction rule.  This accommodates special applications
-  of strengthened induction predicates''.  This option is rarely needed, the
-  $induct$ method already handles proper rules appropriately by default.
-
-  The $open$ option has the same effect as for the $cases$ method, see above.
-\end{descr}
-
-Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
-determined by the instantiated rule \emph{before} it has been applied to the
-internal proof state.\footnote{As a general principle, Isar proof text may
-  never refer to parts of proof states directly.} Thus proper use of symbolic
-cases usually require the rule to be instantiated fully, as far as the
-emerging local contexts and subgoals are concerned.  In particular, for
-induction both the predicates and variables have to be specified.  Otherwise
-the $\CASENAME$ command would refuse to invoke cases containing schematic
-variables.  Furthermore the resulting local goal statement is bound to the
-term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
-fully specified.
-
-The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) 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.
-
-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$.  Also note that local definitions may be expressed as $\All{\vec - x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
-
-\medskip
-
-Facts presented to either method are consumed according to the number of
-major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
-\S\ref{sec:cases}), 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).
-
-Note that whenever facts are present, the default rule selection scheme would
-provide a set'' rule only, with the first fact consumed and the rest
-inserted into the goal.  In order to pass all facts into a type'' rule
-instead, one would have to specify this explicitly, e.g.\ by appending
-$type: name$'' to the method argument.
+Note that a simpler (but faster) version of arithmetic reasoning is already
+performed by the Simplifier.

-\subsection{Declaring rules}\label{sec:induct-att}
-
-\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
-\begin{matharray}{rcl}
-  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
-  cases & : & \isaratt \\
-  induct & : & \isaratt \\
-\end{matharray}
-
-\begin{rail}
-  'cases' spec
-  ;
-  'induct' spec
-  ;
+\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}

-  spec: ('type' | 'set') ':' nameref
-  ;
-\end{rail}
-
-The $cases$ and $induct$ attributes augment the corresponding context of rules
-for reasoning about inductive sets and types.  The standard rules are already
-declared by HOL definitional packages.  For special applications, these may be
-replaced manually by variant versions.
-
-Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
-adjust names of cases and parameters of a rule.
-
-The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
-automatically (if none had been given already): $consumes~0$ is specified for
-type'' rules and $consumes~1$ for set'' rules.
-
-
-\subsection{Emulating tactic scripts}\label{sec:induct_tac}
+The following important tactical tools of Isabelle/HOL have been ported to
+Isar.  These should be never used in proper proof texts!

\indexisarmeth{case-tac}\indexisarmeth{induct-tac}
\indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
@@ -510,9 +353,7 @@

\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
-  forward manner, unlike the proper $cases$ method (see
-  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
-  solved completely.
+  forward manner.

While $ind_cases$ is a proof method to apply the result immediately as
elimination rules, $\isarkeyword{inductive_cases}$ provides case split
@@ -520,29 +361,6 @@
\end{descr}

-\section{Arithmetic}
-
-\indexisarmeth{arith}\indexisaratt{arith-split}
-\begin{matharray}{rcl}
-  arith & : & \isarmeth \\
-  arith_split & : & \isaratt \\
-\end{matharray}
-
-\begin{rail}
-  'arith' '!'?
-  ;
-\end{rail}
-
-The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
-$real$).  Any current facts are inserted into the goal before running the
-procedure.  The !''~argument causes the full context of assumptions to be
-included.  The $arith_split$ attribute declares case split rules to be
-expanded before the arithmetic procedure is invoked.
-
-Note that a simpler (but faster) version of arithmetic reasoning is already
-performed by the Simplifier.
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"