--- a/doc-src/IsarRef/generic.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/generic.tex Tue Mar 21 17:32:43 2000 +0100
@@ -12,10 +12,10 @@
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
-may make use of this light-weight mechanism of abstract theories. See
-\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on
-\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
-Isabelle documentation.
+may make use of this light-weight mechanism of abstract theories
+\cite{Wenzel:1997:TPHOL}. There is also a tutorial on \emph{Using Axiomatic
+ Type Classes in Isabelle} that is part of the standard Isabelle
+documentation.
%FIXME cite
\begin{rail}
@@ -35,8 +35,8 @@
class.
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
- (\vec s)c$] setup up a goal stating the class relation or type arity. The
- proof would usually proceed by $intro_classes$, and then establish the
+ (\vec s)c$] setup a goal stating a class relation or type arity. The proof
+ would usually proceed by $intro_classes$, and then establish the
characteristic theorems of the type classes involved. After finishing the
proof, the theory will be augmented by a type signature declaration
corresponding to the resulting theorem.
@@ -86,15 +86,15 @@
\end{rail}
\begin{descr}
-\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
+\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
follows. The first occurrence of $\ALSO$ in some calculational thread
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
level of block-structure updates $calculation$ by some transitivity rule
applied to $calculation$ and $this$ (in that order). Transitivity rules are
- picked from the current context plus those given as $thms$ (the latter have
- precedence).
+ picked from the current context plus those given as explicit arguments (the
+ latter have precedence).
-\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
+\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
$\ALSO$, and concludes the current calculational thread. The final result
is exhibited as fact for forward chaining towards the next goal. Basically,
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
@@ -102,8 +102,7 @@
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
calculational proofs.
-\item [$trans$] maintains the set of transitivity rules of the theory or proof
- context, by adding or deleting theorems (the default is to add).
+\item [$trans$] declares theorems as transitivity rules.
\end{descr}
@@ -141,10 +140,10 @@
\medskip
Named cases may be exhibited in the current proof context only if both the
-proof method and the corresponding rule 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.
+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}
@@ -157,20 +156,21 @@
'params' ((name * ) + 'and')
;
\end{rail}
+%FIXME bug in rail
\begin{descr}
\item [$\CASE{c}$] 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:induct-method}). The command $\CASE{c}$ abbreviates
- $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
+ as provided by an appropriate proof method (such as $cases$ and $induct$ in
+ Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$
+ abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
- goal context, using Isar proof language notation. This is a diagnostic
- command; $undo$ does not apply.
+ 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 premises).
+ of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
\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 be be given
- to skip positions, leaving the corresponding parameters unchanged.
+ premises $1, \dots, n$ of some theorem. An empty list of names may be given
+ to skip positions, leaving the present parameters unchanged.
\end{descr}
@@ -185,17 +185,17 @@
properties are introduced, together with a soundness proof of that context
change (the rest of the main goal is left unchanged).
-Syntactically, the $\OBTAINNAME$ language element is like a proof method to
-the present goal, followed by a proof of its additional claim, followed by the
-actual context commands (cf.\ $\FIXNAME$ and $\ASSUMENAME$,
-\S\ref{sec:proof-context}).
+Syntactically, the $\OBTAINNAME$ language element is like an initial proof
+method to the present goal, followed by a proof of its additional claim,
+followed by the actual context commands (using the syntax of $\FIXNAME$ and
+$\ASSUMENAME$, see \S\ref{sec:proof-context}).
\begin{rail}
'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
;
\end{rail}
-$\OBTAINNAME$ is defined as a derived Isar command as follows, where the
+$\OBTAINNAME$ is defined as a derived Isar command as follows; here the
preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for
forward chaining.
\begin{matharray}{l}
@@ -212,13 +212,13 @@
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
$\BY{blast}$ (see \S\ref{sec:classical-auto}). Note that the ``$that$''
presumption above is usually declared as simplification and (unsafe)
-introduction rule, somewhat depending on the object-logic's policy,
-though.\footnote{Major object-logics such as HOL and HOLCF do this already.}
+introduction rule, depending on the object-logic's policy,
+though.\footnote{HOL and HOLCF do this already.}
The original goal statement is wrapped into a local definition in order to
avoid any automated tools descending into it. Usually, any statement would
-admit the intended reduction; only in very rare cases $thesis_def$ has to be
-expanded to complete the soundness proof.
+admit the intended reduction anyway; only in very rare cases $thesis_def$ has
+to be expanded to complete the soundness proof.
\medskip
@@ -250,18 +250,18 @@
\end{rail}
\begin{descr}
-\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
meta-level definitions throughout all goals; any facts provided are inserted
into the goal and subject to rewriting as well.
-\item [$erule~thms$, $drule~thms$, and $frule~thms$] are similar to the basic
- $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
+\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
+ basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
elim-resolution, destruct-resolution, and forward-resolution, respectively
\cite{isabelle-ref}. These are improper method, mainly for experimentation
and emulating tactic scripts.
Different modes of basic rule application are usually expressed in Isar at
the proof language level, rather than via implicit proof state
- modifications. For example, a proper single-step elimination would be done
+ manipulations. For example, a proper single-step elimination would be done
using the basic $rule$ method, with forward chaining of current facts.
\item [$succeed$] yields a single (unchanged) result; it is the identity of
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
@@ -312,16 +312,16 @@
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
result). The first string is considered the tag name, the rest its
arguments. Note that untag removes any tags of the same name.
-\item [$RS~n~thm$ and $COMP~n~thm$] compose rules. $RS$ resolves with the
- $n$-th premise of $thm$; $COMP$ is a version of $RS$ that skips the
- automatic lifting process that is normally intended (cf.\ \texttt{RS} and
- \texttt{COMP} in \cite[\S5]{isabelle-ref}).
+\item [$RS~n~a$ and $COMP~n~a$] compose rules. $RS$ resolves with the $n$-th
+ premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting
+ process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
+ \cite[\S5]{isabelle-ref}).
\item [$where~\vec x = \vec t$] perform named instantiation of schematic
variables occurring in a theorem. Unlike instantiation tactics (such as
\texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables
have to be specified (e.g.\ $\Var{x@3}$).
-\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
meta-level definitions throughout a rule.
\item [$standard$] puts a theorem into the standard form of object-rules, just
@@ -332,12 +332,12 @@
\item [$export$] lifts a local result out of the current proof context,
generalizing all fixed variables and discharging all assumptions. Note that
- (partial) export is usually done automatically behind the scenes. This
- attribute is mainly for experimentation.
+ proper incremental export is already done as part of the basic Isar
+ machinery. This attribute is mainly for experimentation.
\item [$transfer$] promotes a theorem to the current theory context, which has
- to enclose the former one. Normally, this is done automatically when rules
- are joined by inference.
+ to enclose the former one. This is done automatically whenever rules are
+ joined by inference.
\end{descr}
@@ -364,32 +364,31 @@
\end{rail}
\begin{descr}
-\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
- adding or deleting rules as specified. The \railtoken{only} modifier first
- removes all other rewrite rules, congruences, and looper tactics (including
- splits), and then behaves like \railtoken{add}.
+\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
+ according to the arguments given. Note that the \railtoken{only} modifier
+ first removes all other rewrite rules, congruences, and looper tactics
+ (including splits), and then behaves like \railtoken{add}.
The \railtoken{split} modifiers add or delete rules for the Splitter (see
also \cite{isabelle-ref}), the default is to add. This works only if the
Simplifier method has been properly setup to include the Splitter (all major
object logics such HOL, HOLCF, FOL, ZF do this already).
- The \railtoken{other} modifier ignores its arguments. Nevertheless there
- may be side-effects on the context via attributes.\footnote{This provides a
- back door for arbitrary context manipulation.}
-
+ The \railtoken{other} modifier ignores its arguments. Nevertheless,
+ additional kinds of rules may be declared by including appropriate
+ attributes in the specification.
\item [$simp_all$] is similar to $simp$, but acts on all goals.
\end{descr}
-The $simp$ methods are based on \texttt{asm_full_simp_tac}
+Internally, the $simp$ method is based on \texttt{asm_full_simp_tac}
\cite[\S10]{isabelle-ref}, but is much better behaved in practice. Just the
local premises of the actual goal are involved by default. Additional facts
may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The
-full context of assumptions is only included in the $simp!$ versions, which
+full context of assumptions is only included in the $simp!$ version, which
should be used with some care, though.
Note that there is no separate $split$ method. The effect of
-\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~thms)$.
+\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$.
\subsection{Declaring rules}
@@ -406,9 +405,8 @@
\end{rail}
\begin{descr}
-\item [$simp$] adds or deletes rules from the theory or proof context (the
- default is to add).
-\item [$split$] is similar to $simp$, but refers to split rules.
+\item [$simp$] declares simplification rules.
+\item [$split$] declares split rules.
\end{descr}
@@ -424,7 +422,7 @@
\end{matharray}
These attributes provide forward rules for simplification, which should be
-used only very rarely. There are no separate options for adding or deleting
+used only very rarely. There are no separate options for declaring
simplification rules locally.
See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
@@ -445,7 +443,7 @@
\end{matharray}
\begin{rail}
- ('rule' | 'intro' | 'elim') thmrefs
+ ('rule' | 'intro' | 'elim') thmrefs?
;
\end{rail}
@@ -460,11 +458,11 @@
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
elim-resolution, after having inserted any facts. Omitting the arguments
- refers to any suitable rules from the context, otherwise only the explicitly
- given ones may be applied. The latter form admits better control of what
- actually happens, thus it is very appropriate as an initial method for
- $\PROOFNAME$ that splits up certain connectives of the goal, before entering
- the actual sub-proof.
+ refers to any suitable rules declared in the context, otherwise only the
+ explicitly given ones may be applied. The latter form admits better control
+ of what actually happens, thus it is very appropriate as an initial method
+ for $\PROOFNAME$ that splits up certain connectives of the goal, before
+ entering the actual sub-proof.
\item [$contradiction$] solves some goal by contradiction, deriving any result
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
@@ -507,10 +505,12 @@
Any of above methods support additional modifiers of the context of classical
rules. Their semantics is analogous to the attributes given in
-\S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted
-into the goal before doing the search. The ``!''~argument causes the full
-context of assumptions to be included as well.\footnote{This is slightly less
- hazardous than for the Simplifier (see \S\ref{sec:simp}).}
+\S\ref{sec:classical-mod}. Facts provided by forward chaining are
+inserted\footnote{These methods usually cannot make proper use of actual rules
+ inserted that way, though.} into the goal before doing the search. The
+``!''~argument causes the full context of assumptions to be included as well.
+This is slightly less hazardous than for the Simplifier (see
+\S\ref{sec:simp}).
\subsection{Combined automated methods}
@@ -568,8 +568,8 @@
\emph{extra} (i.e.\ not applied in the search-oriented automated methods,
but only in single-step methods such as $rule$).
-\item [$iff$] declares equations both as rewrite rules for the simplifier and
- classical reasoning rules.
+\item [$iff$] declares equations both as rules for the Simplifier and
+ Classical Reasoner.
\item [$delrule$] deletes introduction or elimination rules from the context.
Note that destruction rules would have to be turned into elimination rules
--- a/doc-src/IsarRef/hol.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/hol.tex Tue Mar 21 17:32:43 2000 +0100
@@ -182,9 +182,8 @@
\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
(co)inductive sets from the given introduction rules.
-\item [$mono$] adds or deletes monotonicity rules from the theory or proof
- context (the default is to add). These rule are involved in the automated
- monotonicity proof of $\isarkeyword{inductive}$.
+\item [$mono$] declares monotonicity rules. These rule are involved in the
+ automated monotonicity proof of $\isarkeyword{inductive}$.
\item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules
of (co)inductive sets, solving obvious cases by simplification.
@@ -193,10 +192,10 @@
Unlike the \texttt{mk_cases} ML function exported with any inductive
definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does
- \emph{not} modify cases by simplification, apart from trying to solve
- completely (e.g.\ due to contradictory assumptions. Thus
- $\isarkeyword{inductive_cases}$ conforms to way Isar proofs are conducted,
- rather than old-style tactic scripts.
+ \emph{not} modify cases by simplification that are not solved completely
+ anyway (e.g.\ due to contradictory assumptions). Thus
+ $\isarkeyword{inductive_cases}$ conforms to the way Isar proofs are
+ conducted, rather than old-style tactic scripts.
\end{descr}
See \cite{isabelle-HOL} for further information on inductive definitions in
@@ -269,7 +268,8 @@
The $stripped$ option causes implications and (bounded) universal
quantifiers to be removed from each new subgoal emerging from the
- application of the induction rule.
+ application of the induction rule. This accommodates typical
+ ``strengthening of induction'' predicates.
\end{descr}
Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
@@ -279,11 +279,11 @@
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 that contain schematic
+the $\CASENAME$ command would refuse to invoke cases containing schematic
variables.
The $\isarkeyword{print_cases}$ command (\S\ref{sec:diag}) prints all named
-cases present in the current proof context.
+cases present in the current proof state.
\subsection{Declaring rules}
--- a/doc-src/IsarRef/intro.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/intro.tex Tue Mar 21 17:32:43 2000 +0100
@@ -8,7 +8,7 @@
Isar is already part of Isabelle (as of version Isabelle99, or later). The
\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
interaction loop at startup, rather than the plain ML top-level. Thus the
-quickest way to do anything with Isabelle/Isar is as follows:
+quickest way to do \emph{anything} with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
@@ -17,23 +17,23 @@
lemma "0 < foo" by (simp add: foo_def);
end
\end{ttbox}
-Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
+Note that any Isabelle/Isar command may be retracted by \texttt{undo}. The
\texttt{help} command prints a list of available language elements.
\subsection{The Proof~General interface}
Plain TTY-based interaction as above used to be quite feasible with
-traditional tactic based theorem proving, but developing Isar documents
+traditional tactic based theorem proving, but developing Isar documents really
demands some better user-interface support. David Aspinall's
\emph{Proof~General}\index{Proof General} environment
-\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs-based interface
-for interactive theorem provers that does all the cut-and-paste and
+\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
+interactive theorem provers that does all the cut-and-paste and
forward-backward walk through the text in a very neat way. In Isabelle/Isar,
the current position within a partial proof document is equally important than
the actual proof state. Thus Proof~General provides the canonical working
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
-existing Isar documents) and real production work.
+existing Isar documents) and for production work.
\medskip
@@ -50,18 +50,18 @@
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
classic Isabelle tactic scripts.}
-The interface script provides several options, just pass ``\texttt{-?}'' to
-see its usage. Apart from the command line, the defaults for these options
-may be overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For
+The interface script provides several options, just pass \verb,-?, to see its
+usage. Apart from the command line, the defaults for these options may be
+overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For
example, plain FSF Emacs (instead of the default XEmacs) may be configured in
Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p emacs"}.
Occasionally, the user's \verb,~/.emacs, file contains material that is
incompatible with the version of Emacs that Proof~General prefers. Then
proper startup may be still achieved by using the \texttt{-u false} option.
-Also note that any Emacs lisp file \texttt{proofgeneral-settings.el} occurring
-in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
-automatically loaded by the Proof~General interface script as well.
+Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
+occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
+is automatically loaded by the Proof~General interface script as well.
\medskip
@@ -72,8 +72,8 @@
\end{ttbox}
Users of XEmacs may note the tool bar for navigating forward and backward
through the text. Consult the Proof~General documentation \cite{proofgeneral}
-for further basic command sequences, such as ``\texttt{c-c c-return}'' or
-``\texttt{c-c u}''.
+for further basic command sequences, such as ``\texttt{C-c C-return}'' or
+``\texttt{C-c u}''.
\medskip
@@ -88,12 +88,12 @@
according the default set of Isabelle symbols. On the other hand, the
Isabelle document preparation system \cite{isabelle-sys} will be happy to
print non-ASCII symbols properly. It is even possible to invent additional
-notation beyond the display capabilities of XEmacs~/X-Symbol.
+notation beyond the display capabilities of XEmacs and X-Symbol.
\section{Isabelle/Isar theories}
-Isabelle/Isar offers the following main improvements over classic Isabelle:
+Isabelle/Isar offers the following main improvements over classic Isabelle.
\begin{enumerate}
\item A new \emph{theory format}, occasionally referred to as ``new-style
theories'', supporting interactive development and unlimited undo operation.
@@ -101,18 +101,18 @@
semi-automated reasoning. Instead of putting together unreadable tactic
scripts, the author is enabled to express the reasoning in way that is close
to usual mathematical practice.
-\item A simple document preparation system for Isabelle/Isar theories, for
- typesetting formal developments together with informal text. The resulting
- resulting hyper-linked PDF documents are equally well suited for WWW
- presentation and printed copies.
+\item A simple document preparation system, for typesetting formal
+ developments together with informal text. The resulting hyper-linked PDF
+ documents are equally well suited for WWW presentation and as printed
+ copies.
\end{enumerate}
The Isar proof language is embedded into the new theory format as a proper
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
$\LEMMANAME$ at the theory level, and left again with the final conclusion
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
-well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
-the representing sets.
+well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
+representing sets.
New-style theory files may still be associated with separate ML files
consisting of plain old tactic scripts. There is no longer any ML binding
@@ -120,10 +120,11 @@
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
relatively easy. Thus users may start to benefit from interactive theory
-development even before they have any idea of the Isar proof language at all.
+development and document preparation, even before they have any idea of the
+Isar proof language at all.
\begin{warn}
- Currently Proof~General does \emph{not} support mixed interactive
+ Currently, Proof~General does \emph{not} support mixed interactive
development of classic Isabelle theory files or tactic scripts, together
with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
Proof~General are handled as two different theorem proving systems, only one
@@ -146,6 +147,7 @@
but a good understanding of mathematical proof, might cope with Isar even
better. See also \cite{Wenzel:1999:TPHOL} for further background information
on Isar.
+%FIXME cite [HahnBanach-in-Isar]
\medskip This really is a \emph{reference manual}. Nevertheless, we will also
give some clues of how the concepts introduced here may be put into practice.
@@ -162,8 +164,10 @@
\end{center}
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
-\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
-plain HTML sources, these sessions also provide actual documents (in PDF).
+\texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application. Apart
+from plain HTML sources, these sessions also provide actual documents (in
+PDF).
+
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/isar-ref.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Tue Mar 21 17:32:43 2000 +0100
@@ -53,20 +53,20 @@
The current version of Isabelle offers Isar as an alternative proof language
interface layer. The Isabelle/Isar system provides an interpreter for the
- Isar formal proof document language. The input may consist either of proper
- document constructors, or improper auxiliary commands (for diagnostics,
- exploration etc.). Proof texts consisting of proper document constructors
- only, admit a purely static reading, thus being intelligible later without
- requiring dynamic replay that is so typical for traditional proof scripts.
- Any of the Isabelle/Isar commands may be executed in single-steps, so
- basically the interpreter has a proof text debugger already built-in.
+ Isar formal proof language. The input may consist either of proper document
+ constructors, or improper auxiliary commands (for diagnostics, exploration
+ etc.). Proof texts consisting of proper elements only, admit a purely
+ static reading, thus being intelligible later without requiring dynamic
+ replay that is so typical for traditional proof scripts. Any of the
+ Isabelle/Isar commands may be executed in single-steps, so basically the
+ interpreter has a proof text debugger already built-in.
Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
interface for interactive proof assistants, we arrive at a reasonable
environment for \emph{live document editing}. Thus proof texts may be
- developed incrementally by issuing proper document constructors, including
- forward and backward tracing of partial documents; intermediate states may
- be inspected by diagnostic commands.
+ developed incrementally by issuing proof commands, including forward and
+ backward tracing of partial documents; intermediate states may be inspected
+ by diagnostic commands.
The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
implementation. Theories, theorems, proof procedures etc.\ may be used
--- a/doc-src/IsarRef/pure.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Mar 21 17:32:43 2000 +0100
@@ -2,7 +2,7 @@
\chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
Subsequently, we introduce the main part of Pure Isar theory and proof
-commands, together with a few fundamental proof methods and attributes.
+commands, together with fundamental proof methods and attributes.
Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
tools and packages (such as the Simplifier) that are either part of Pure
Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools}
@@ -17,7 +17,7 @@
documents, while their use is discouraged for the final outcome. Typical
examples are diagnostic commands that print terms or theorems according to the
current context; other commands even emulate old-style tactical theorem
-proving, which facilitates porting of legacy proof scripts.
+proving.
\section{Theory commands}
@@ -45,7 +45,7 @@
command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory
context may be also changed by $\CONTEXT$ without creating a new theory. In
both cases, $\END$ concludes the theory development; it has to be the very
-last command in a theory file.
+last command of any theory file.
\begin{rail}
'header' text
@@ -62,7 +62,7 @@
\begin{descr}
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding
- the formal begin of a theory. In actual document preparation the
+ the formal beginning of a theory. In actual document preparation the
corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
produce chapter or section headings. See also \S\ref{sec:markup-thy} and
\S\ref{sec:markup-prf} for further markup commands.
@@ -128,7 +128,7 @@
becomes available. A typical application would be to emit
\verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
parts from the final document.\footnote{This requires the \texttt{comment}
- package to be included in {\LaTeX}.}
+ package to be included in {\LaTeX}, of course.}
\end{descr}
Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
@@ -172,7 +172,7 @@
introduce proven class relations.
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
any type variables given without sort constraints. Usually, the default
- sort would be only changed when defining new logics.
+ sort would be only changed when defining new object-logics.
\end{descr}
@@ -245,8 +245,8 @@
existing constant. See \cite[\S6]{isabelle-ref} for more details on the
form of equations admitted as constant definitions.
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
- definitions of constants, using canonical name $c_def$ for the definitional
- axiom.
+ definitions of constants, using the canonical name $c_def$ for the
+ definitional axiom.
\end{descr}
@@ -272,9 +272,9 @@
except that the actual logical signature extension is omitted. Thus the
context free grammar of Isabelle's inner syntax may be augmented in
arbitrary ways, independently of the logic. The $mode$ argument refers to
- the print mode that the grammar rules belong; unless there is the
- \texttt{output} flag given, all productions are added both to the input and
- output grammar.
+ the print mode that the grammar rules belong; unless the \texttt{output}
+ flag is given, all productions are added both to the input and output
+ grammar.
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
(\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be
@@ -306,10 +306,10 @@
Axioms are usually only introduced when declaring new logical systems.
Everyday work is typically done the hard way, with proper definitions and
- actual theorems.
+ actual proven theorems.
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
- Typical applications would also involve attributes, to augment the
- Simplifier context, for example.
+ Typical applications would also involve attributes, to declare Simplifier
+ rules, for example.
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
tags the results as ``lemma''.
\end{descr}
@@ -324,9 +324,9 @@
\end{matharray}
Isabelle organizes any kind of name declarations (of types, constants,
-theorems etc.) by hierarchically structured name spaces. Normally the user
-never has to control the behavior of name space entry by hand, yet the
-following commands provide some way to do so.
+theorems etc.) by separate hierarchically structured name spaces. Normally
+the user never has to control the behavior of name space entry by hand, yet
+the following commands provide some way to do so.
\begin{descr}
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
@@ -374,8 +374,8 @@
\item [$\isarkeyword{setup}~text$] changes the current theory context by
applying $text$, which refers to an ML expression of type
\texttt{(theory~->~theory)~list}. The $\isarkeyword{setup}$ command is the
- canonical way to initialize object-logic specific tools and packages written
- in ML.
+ canonical way to initialize any object-logic specific tools and packages
+ written in ML.
\end{descr}
@@ -439,12 +439,12 @@
Proof commands perform transitions of Isar/VM machine configurations, which
are block-structured, consisting of a stack of nodes with three main
components: logical proof context, current facts, and open goals. Isar/VM
-transitions are \emph{typed} according to the following three three different
-modes of operation:
+transitions are \emph{typed} according to the following three different modes
+of operation:
\begin{descr}
\item [$proof(prove)$] means that a new goal has just been stated that is now
- to be \emph{proven}; the next command may refine it by some proof method
- (read: tactic), and enter a sub-proof to establish the actual result.
+ to be \emph{proven}; the next command may refine it by some proof method,
+ and enter a sub-proof to establish the actual result.
\item [$proof(state)$] is like an internal theory mode: the context may be
augmented by \emph{stating} additional assumptions, intermediate results
etc.
@@ -532,8 +532,8 @@
\end{rail}
\begin{descr}
-\item [$\FIX{\vec x}$] introduces a local \emph{arbitrary, but fixed}
- variables $\vec x$.
+\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
+ $\vec x$.
\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
theorems $\vec\phi$ by assumption. Subsequent results applied to an
enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
@@ -567,7 +567,7 @@
New facts are established either by assumption or proof of local statements.
Any fact will usually be involved in further proofs, either as explicit
-arguments of proof methods or when forward chaining towards the next goal via
+arguments of proof methods, or when forward chaining towards the next goal via
$\THEN$ (and variants). Note that the special theorem name
$this$\indexisarthm{this} refers to the most recently established facts.
\begin{rail}
@@ -589,7 +589,8 @@
also \S\ref{sec:proof-steps}). For example, method $rule$ (see
\S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
introduction. Automatic methods usually insert the facts into the goal
- state before operation.
+ state before operation. This provides a simple scheme to control relevance
+ of facts in automated proof search.
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
equivalent to $\FROM{this}$.
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
@@ -599,9 +600,10 @@
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
multiple facts to be given in their proper order, corresponding to a prefix of
the premises of the rule involved. Note that positions may be easily skipped
-using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves
-the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be bound in
-Isabelle/Pure as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
+using something like $\FROM{\text{\texttt{_}}~a~b}$, for example. This
+involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
+bound in Isabelle/Pure as ``\texttt{_}''
+(underscore).\indexisarthm{_@\texttt{_}}
\subsection{Goal statements}
@@ -620,7 +622,7 @@
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
and $\LEMMANAME$. New local goals may be claimed within proof mode as well.
Four variants are available, indicating whether the result is meant to solve
-some pending goal or whether forward chaining is employed.
+some pending goal or whether forward chaining is indicated.
\begin{rail}
('theorem' | 'lemma') goal
@@ -634,7 +636,8 @@
\begin{descr}
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
- eventually resulting in some theorem $\turn \phi$ put back into the theory.
+ eventually resulting in some theorem $\turn \phi$ to be put back into the
+ theory.
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
``lemma''.
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
@@ -663,7 +666,7 @@
\isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
\end{matharray}
-Arbitrary goal refinement via tactics is considered harmful. Consequently the
+Arbitrary goal refinement via tactics is considered harmful. Properly, the
Isar framework admits proof methods to be invoked in two places only.
\begin{enumerate}
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
@@ -674,8 +677,8 @@
remaining goals. No facts are passed to $m@2$.
\end{enumerate}
-The only other proper way to affect pending goals is by $\SHOWNAME$ (or
-$\THUSNAME$), which involves an explicit statement of what is to be solved.
+The only other proper way to affect pending goals is by $\SHOWNAME$, which
+involves an explicit statement of what is to be solved.
\medskip
@@ -687,11 +690,10 @@
\medskip
-Unless given explicitly by the user, the default initial method is
-``$default$'', which is usually set up to apply a single standard elimination
-or introduction rule according to the topmost symbol involved. There is no
-separate default terminal method. In any case, any goals left after that are
-solved by assumption as the very last step.
+Unless given explicitly by the user, the default initial method is ``$rule$'',
+which applies a single standard elimination or introduction rule according to
+the topmost symbol involved. There is no separate default terminal method.
+Any remaining goals are always solved by assumption in the very last step.
\begin{rail}
'proof' interest? meth? comment?
@@ -740,10 +742,10 @@
\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
-The following proof methods and attributes refer to some basic logical
-operations of Isar. Further methods and attributes are provided by several
-generic and object-logic specific tools and packages (see chapters
-\ref{ch:gen-tools} and \ref{ch:hol-tools}).
+The following proof methods and attributes refer to basic logical operations
+of Isar. Further methods and attributes are provided by several generic and
+object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
+\ref{ch:hol-tools}).
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
@@ -762,7 +764,7 @@
\end{matharray}
\begin{rail}
- 'rule' thmrefs
+ 'rule' thmrefs?
;
'OF' thmrefs
;
@@ -780,25 +782,26 @@
remaining sub-goals by assumption.
\item [$this$] applies all of the current facts directly as rules. Recall
that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
-\item [$rule~thms$] applies some rule given as argument in backward manner;
+\item [$rule~\vec a$] applies some rule given as argument in backward manner;
facts are used to reduce the rule before applying it to the goal. Thus
$rule$ without facts is plain \emph{introduction}, while with facts it
becomes \emph{elimination}.
- When omitting the $thms$ argument, the $rule$ method tries to pick
- appropriate rules automatically, as declared in the current context using
- the $intro$, $elim$, $dest$ attributes (see below). This is the default
- behavior of $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
+ When no arguments are given, the $rule$ method tries to pick appropriate
+ rules automatically, as declared in the current context using the $intro$,
+ $elim$, $dest$ attributes (see below). This is the default behavior of
+ $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
\S\ref{sec:proof-steps}).
\item [``$-$''] does nothing but insert the forward chaining facts as premises
into the goal. Note that command $\PROOFNAME$ without any method actually
performs a single reduction step using the $rule$ method; thus a plain
\emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
alone.
-\item [$OF~thms$] applies $thms$ in parallel (cf.\ \texttt{MRS} in
- \cite[\S5]{isabelle-ref}, but note the reversed order). Some premises may
- be skipped by including ``$\_$'' (underscore) as argument.
-\item [$of~ts$] performs positional instantiation. The terms $ts$ are
+\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
+ parallel). This corresponds to the \texttt{MRS} operator in ML
+ \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
+ skipped by including ``$\_$'' (underscore) as argument.
+\item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are
substituted for any schematic variables occurring in a theorem from left to
right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments
following a ``$concl\colon$'' specification refer to positions of the
@@ -856,7 +859,7 @@
$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
-object-logical statement. The latter two abstract over any meta-level
+object-level statement. The latter two abstract over any meta-level
parameters.
Fact statements resulting from assumptions or finished goals are bound as
@@ -968,8 +971,8 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial
- position, but retains ``$prove$'' mode (unlike $\PROOFNAME$). Thus
+\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in initial
+ position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus
consecutive method applications may be given just as in tactic scripts. In
order to complete the proof properly, any of the actual structured proof
commands (e.g.\ ``$\DOT$'') has to be given eventually.
@@ -992,7 +995,7 @@
\cite{isabelle-ref}, the Isar command does not search upwards for further
branch points.} Basically, any proof command may return multiple results.
\item [$tactic~text$] produces a proof method from any ML text of type
- \texttt{tactic}. Apart from the usual ML environment, and the current
+ \texttt{tactic}. Apart from the usual ML environment and the current
implicit theory context, the ML code may refer to the following locally
bound values:
%%FIXME ttbox produces too much trailing space (why?)
@@ -1014,7 +1017,7 @@
type-checked according to the dynamic goal state, rather than the static
proof context! In particular, locally fixed variables and term
abbreviations may not be included in the term specifications.
-\item [$subgoal_tac$] emulates the ML tactic of the same name, see
+\item [$subgoal_tac~\phi$] emulates the ML tactic of the same name, see
\cite[\S3]{isabelle-ref}. Syntactically, the given proposition is handled
as the instantiations in $res_inst_tac$ etc.
@@ -1045,15 +1048,9 @@
macros can be easily adapted to print something like ``$\dots$'' instead of an
``$\OOPS$'' keyword.
-\medskip The $\OOPS$ command is undoable, in contrast to $\isarkeyword{kill}$
-(see \S\ref{sec:history}). The effect is to get back to the theory
-\emph{before} the opening of the proof.
-
-%FIXME remove
-% \begin{descr}
-% \item [$\isarkeyword{oops}$] dismisses the current proof, leaving the text in
-% as properly processed.
-% \end{descr}
+\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see
+\S\ref{sec:history}). The effect is to get back to the theory \emph{before}
+the opening of the proof.
\section{Other commands}
@@ -1101,11 +1098,11 @@
current facts and goals. The optional argument $n$ affects the implicit
limit of goals to be displayed, which is initially 10. Omitting the limit
leaves the value unchanged.
-\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
- theory or proof context. Note that any attributes included in the theorem
+\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
+ or proof context. Note that any attributes included in the theorem
specifications are applied to a temporary context derived from the current
- theory or proof; the result is discarded, i.e.\ attributes involved in
- $thms$ do not have any permanent effect.
+ theory or proof; the result is discarded, i.e.\ attributes involved in $\vec
+ a$ do not have any permanent effect.
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
print terms or propositions according to the current theory or proof
context; the inferred type of $t$ is output as well. Note that these
@@ -1124,17 +1121,14 @@
Thus the output behavior may be modified according particular print mode
features.
-\medskip
-
For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would print the
current proof state with mathematical symbols and special characters
represented in {\LaTeX} source, according to the Isabelle style
-\cite{isabelle-sys}. The resulting text can be directly pasted into and
-\verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment.
-
-Note that $\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output,
-if the current Isabelle session has the other modes already activated, say due
-to some particular user interface configuration such as Proof~General
+\cite{isabelle-sys}. The resulting text can be directly pasted into a
+\verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment. Note that
+$\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output, if the
+current Isabelle session has the other modes already activated, say due to
+some particular user interface configuration such as Proof~General
\cite{proofgeneral,Aspinall:TACAS:2000} with X-Symbol mode \cite{x-symbol}.
@@ -1157,9 +1151,9 @@
undoable.
\begin{warn}
- History commands may not be used with user interfaces such as Proof~General
- \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of stepping forth
- and back itself. Interfering with manual $\isarkeyword{undo}$,
+ History commands should never be used with user interfaces such as
+ Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of
+ stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$,
$\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly
result in utter confusion.
\end{warn}
--- a/doc-src/IsarRef/refcard.tex Tue Mar 21 15:32:08 2000 +0100
+++ b/doc-src/IsarRef/refcard.tex Tue Mar 21 17:32:43 2000 +0100
@@ -58,10 +58,14 @@
\ALSO@0 & \approx & \NOTE{calculation}{this} \\
\ALSO@{n+1} & \approx & \NOTE{calculation}{trans~[OF~calculation~this]} \\
\FINALLY & \approx & \ALSO~\FROM{calculation} \\[0.5ex]
- \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi}~~\text{(permissive assumption)} \\
- \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t}~~\text{(definitional assumption)} \\
- \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi}~~\text{(generalized existence)} \\
- \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi}~~\text{(named context)} \\[0.5ex]
+ \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
+% & & \text{(permissive assumption)} \\
+ \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
+% & & \text{(definitional assumption)} \\
+ \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
+% & & \text{(generalized existence)} \\
+ \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
+% & & \text{(named context)} \\[0.5ex]
\SORRY & \approx & \BY{cheating} \\
\end{matharray}
@@ -90,8 +94,8 @@
$rule~\vec a$ & apply some rule \\
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
$contradiction$ & apply $\neg{}$ elimination rule (any order) \\
- $cases~x$ & case analysis (provides cases) \\
- $induct~x$ & proof by induction (provides cases) \\[2ex]
+ $cases~t$ & case analysis (provides cases) \\
+ $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
\multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
$-$ & \text{no rules} \\
@@ -130,17 +134,17 @@
\section{Emulating tactic scripts}
-\subsection{Proof commands}
+\subsection{Commands}
\begin{tabular}{ll}
- $\isarkeyword{apply}~(m)$ & apply proof method (at initial position) \\
- $\isarkeyword{apply_end}~(m)$ & apply proof method (near terminal position) \\
+ $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\
+ $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
$\isarkeyword{defer}~n$ & move subgoal to end \\
$\isarkeyword{prefer}~n$ & move subgoal to beginning \\
$\isarkeyword{back}$ & backtrack last command \\
\end{tabular}
-\subsection{Proof methods}
+\subsection{Methods}
\begin{tabular}{ll}
$tactic~text$ & method from ML tactic \\
@@ -150,7 +154,7 @@
$forw_inst_tac~insts$ & forward-resolution with instantiation \\
$subgoal_tac~\phi$ & insert new claim \\
$case_tac~t$ & datatype exhaustion \\
- $induct_tac~xs$ & datatype induction \\
+ $induct_tac~\vec x$ & datatype induction \\
\end{tabular}