--- a/doc-src/IsarRef/generic.tex Sat Oct 30 20:41:30 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Sun Oct 31 15:20:35 1999 +0100
@@ -37,9 +37,9 @@
becomes a (generalized) \emph{elimination}.
Note that the classical reasoner introduces another version of $rule$ that
- is able to pick appropriate rules automatically, whenever explicit $thms$
- are omitted (see \S\ref{sec:classical-basic}); that method is the default
- for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
+ is able to pick appropriate rules automatically, whenever $thms$ are omitted
+ (see \S\ref{sec:classical-basic}); that method is the default for
+ $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
$\BY{default}$.
\item [$erule~thms$] is similar to $rule$, but applies rules by
elim-resolution. This is an improper method, mainly for experimentation and
@@ -47,11 +47,11 @@
$rule$ (single step, involving facts) or $elim$ (repeated steps, see
\S\ref{sec:classical-basic}).
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
- meta-level definitions throughout all goals; any facts provided are
- \emph{ignored}.
-\item [$succeed$] yields a single (unchanged) result; it is the identify of
+ meta-level definitions throughout all goals; any facts provided are inserted
+ into the goal and subject to rewriting as well.
+\item [$succeed$] yields a single (unchanged) result; it is the identity of
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
-\item [$fail$] yields an empty result sequence; it is the identify of the
+\item [$fail$] yields an empty result sequence; it is the identity of the
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
\end{descr}
@@ -98,12 +98,12 @@
result).
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
- the reversed order). Note that premises may be skipped by including $\_$
- (underscore) as argument.
+ the reversed order). Note that premises may be skipped by including
+ ``$\_$'' (underscore) as argument.
$RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
- that does not include the automatic lifting process that is normally
- intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
+ that skips the automatic lifting process that is normally intended (cf.\
+ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively. The terms given in $of$ are substituted for
@@ -180,9 +180,10 @@
\item [$\FINALLY~(thms)$] 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}$. Typical proof
- idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
- ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
+ $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
+ ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
+ ``$\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).
@@ -204,12 +205,12 @@
intro_classes & : & \isarmeth \\
\end{matharray}
-Axiomatic type classes are provided by Isabelle/Pure as a purely
-\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
-any object logic may make use of this light-weight mechanism for 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.
+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.
%FIXME cite
\begin{rail}
@@ -225,21 +226,22 @@
holding. Class axioms may not contain more than one type variable. The
class axioms (with implicit sort constraints added) are bound to the given
names. Furthermore a class introduction rule is generated, which is
- employed by method $intro_classes$ in support instantiation proofs of this
+ employed by method $intro_classes$ to support instantiation proofs of this
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 the $intro_classes$ method, 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.
-\item [$intro_classes$] repeatedly expands the class introduction rules of
+ 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.
+\item [$intro_classes$] repeatedly expands all class introduction rules of
this theory.
\end{descr}
-See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
-axiomatic type classes, including instantiation proofs.
+%FIXME
+%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
+%axiomatic type classes, including instantiation proofs.
\section{The Simplifier}
@@ -345,7 +347,7 @@
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 proof.
+ 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
@@ -388,7 +390,10 @@
Any of above methods support additional modifiers of the context of classical
rules. There semantics is analogous to the attributes given in
-\S\ref{sec:classical-mod}.
+\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}).}
\subsection{Combined automated methods}
@@ -403,7 +408,7 @@
('force' | 'auto') ('!' ?) (clasimpmod * )
;
- clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
+ clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
(('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
\end{rail}
@@ -414,8 +419,13 @@
modifier arguments correspond to those given in \S\ref{sec:simp} and
\S\ref{sec:classical-auto}. Just note that the ones related to the
Simplifier are prefixed by \railtoken{simp} here.
+
+ 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.
\end{descr}
+
\subsection{Modifying the context}\label{sec:classical-mod}
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
--- a/doc-src/IsarRef/hol.tex Sat Oct 30 20:41:30 1999 +0200
+++ b/doc-src/IsarRef/hol.tex Sun Oct 31 15:20:35 1999 +0100
@@ -146,8 +146,8 @@
\end{descr}
See \cite{isabelle-HOL} for more information. Note that
-$\isarkeyword{inductive_cases}$ corresponds to the ML function
-\texttt{mk_cases}.
+$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML
+function.
\section{Proof by induction}
--- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:41:30 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Sun Oct 31 15:20:35 1999 +0100
@@ -149,7 +149,7 @@
\end{tabular}
\end{center}
-See \texttt{HOL/Isar_examples} for a collection of introductory examples.
+See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
browsable HTML sources, both sessions provide actual documents (in PDF).
--- a/doc-src/IsarRef/pure.tex Sat Oct 30 20:41:30 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Sun Oct 31 15:20:35 1999 +0100
@@ -370,10 +370,9 @@
afterwards. Thus $text$ may actually change the theory as a side effect.
\item [$\isarkeyword{setup}~text$] changes the current theory context by
- applying setup functions from $text$, which refers to an ML expression of
- type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the
- canonical way to initialize object-logic specific tools and packages written
- in ML.
+ applying $text$, which refers to an ML expression of type $(theory \to
+ theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to
+ initialize object-logic specific tools and packages written in ML.
\end{descr}
@@ -424,7 +423,7 @@
\section{Proof commands}
-Proof commands provide transitions of Isar/VM machine configurations, which
+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
@@ -434,16 +433,18 @@
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.
\item [$proof(state)$] is like an internal theory mode: the context may be
- augmented by \emph{stating} additional assumptions, intermediate result etc.
+ augmented by \emph{stating} additional assumptions, intermediate results
+ etc.
\item [$proof(chain)$] is intermediate between $proof(state)$ and
- $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
- picked up in order to be used when refining the goal claimed next.
+ $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
+ register) have been just picked up in order to be used when refining the
+ goal claimed next.
\end{descr}
\subsection{Proof markup commands}\label{sec:markup-prf}
-\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
+\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
\indexisarcmd{txt}\indexisarcmd{txt-raw}
\begin{matharray}{rcl}
\isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
@@ -480,10 +481,10 @@
former closely correspond to Skolem constants, or meta-level universal
quantification as provided by the Isabelle/Pure logical framework.
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
-a local object that may be used in the subsequent proof as any other variable
+a local value that may be used in the subsequent proof as any other variable
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the
-current context will be universally closed wrt.\ $x$ at the outermost level:
-$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
+context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
+\All x \phi$ (this is expressed using Isabelle's meta-variables).
Similarly, introducing some assumption $\chi$ has two effects. On the one
hand, a local theorem is created that may be used as a fact in subsequent
@@ -497,9 +498,9 @@
user.
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
-combining $\FIX x$ with another kind of assumption that causes any
-hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus,
-exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
+combining $\FIX x$ with another version of assumption that causes any
+hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
+Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
\begin{rail}
'fix' (vars + 'and') comment?
@@ -530,7 +531,7 @@
these concatenated.
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
In results exported from the context, $x$ is replaced by $t$. Basically,
- $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
+ $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
resulting hypothetical equation solved by reflexivity.
The default name for the definitional equation is $x_def$.
@@ -554,7 +555,7 @@
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
$\THEN$ (and variants). Note that the special theorem name
-$this$.\indexisarthm{this} refers to the most recently established facts.
+$this$\indexisarthm{this} refers to the most recently established facts.
\begin{rail}
'note' thmdef? thmrefs comment?
;
@@ -596,8 +597,8 @@
\begin{matharray}{rcl}
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
- \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
\end{matharray}
@@ -605,7 +606,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 and whether forward chaining is employed.
+some pending goal or whether forward chaining is employed.
\begin{rail}
('theorem' | 'lemma') goal
@@ -620,7 +621,7 @@
\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.
-\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
+\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
theorem with the current assumption context as hypotheses.
@@ -655,8 +656,8 @@
goal to a number of sub-goals that are to be solved later. Facts are passed
to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
-\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
- completely. No facts are passed to $m@2$.
+\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
+ remaining goals. No facts are passed to $m@2$.
\end{enumerate}
The only other proper way to affect pending goals is by $\SHOWNAME$ (or
@@ -668,17 +669,19 @@
or constitute some well-understood reduction to new sub-goals. Arbitrary
automatic proof tools that are prone leave a large number of badly structured
sub-goals are no help in continuing the proof document in any intelligible
-way. A much better technique would be to $\SHOWNAME$ some non-trivial
-reduction as an explicit rule, which is solved completely by some automated
-method, and then applied to some pending goal.
+way.
+%FIXME
+%A more appropriate technique would be to $\SHOWNAME$ some non-trivial
+%reduction as an explicit rule, which is solved completely by some automated
+%method, and then applied to some pending goal.
\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 the final step is to solve all
-remaining goals by assumption, though.
+separate default terminal method. In any case, any goals left after that are
+solved by assumption as the very last step.
\begin{rail}
'proof' interest? meth? comment?
@@ -708,8 +711,8 @@
$\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
- abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
- methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
+ abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
+ though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
by expanding its definition; in many cases $\PROOF{m@1}$ is already
sufficient to see what is going wrong.
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
@@ -717,12 +720,12 @@
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
abbreviates $\BY{assumption}$.
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
- provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
- pretends to solve the goal without further ado. Of course, the result is a
- fake theorem only, involving some oracle in its internal derivation object
- (this is indicated as ``$[!]$'' in the printed result). The main
- application of $\isarkeyword{sorry}$ is to support experimentation and
- top-down proof development.
+ provided that the \texttt{quick_and_dirty} flag is enabled,
+ $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of
+ course, the result is a fake theorem only, involving some oracle in its
+ internal derivation object (this is indicated as ``$[!]$'' in the printed
+ result). The main application of $\isarkeyword{sorry}$ is to support
+ experimentation and top-down proof development.
\end{descr}
@@ -772,13 +775,13 @@
\end{matharray}
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
-or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
-etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases,
-higher-order matching is invoked to bind extra-logical term variables, which
-may be either named schematic variables of the form $\Var{x}$, or nameless
-dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
-the $\LETNAME$ form the patterns occur on the left-hand side, while the
-$\ISNAME$ patterns are in postfix position.
+or by annotating assumptions or goal statements with a list of patterns
+$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to
+bind extra-logical term variables, which may be either named schematic
+variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
+(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
+patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
+postfix position.
Term abbreviations are quite different from actual local definitions as
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
@@ -807,7 +810,7 @@
(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
-parameters bound by $\Forall$.
+parameters.
Fact statements resulting from assumptions or finished goals are bound as
$\Var{this_prop}$\indexisarvar{this-prop},
@@ -816,7 +819,7 @@
$\Var{this}$ refers to an object-logic statement that is an application
$f(t)$, then $t$ is bound to the special text variable
``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
-this feature are calculational proofs (see \S\ref{sec:calculation}).
+the latter are calculational proofs (see \S\ref{sec:calculation}).
\subsection{Block structure}
@@ -834,8 +837,8 @@
again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
different context within a sub-proof may be switched via $\isarkeyword{next}$,
which is just a single block-close followed by block-open again. Thus the
-effect of $\isarkeyword{next}$ is a local reset the proof
-context.\footnote{There is no goal focus involved here!}
+effect of $\isarkeyword{next}$ to reset the local proof context. There is no
+goal focus involved here!
For slightly more advanced applications, there are explicit block parentheses
as well. These typically achieve a stronger forward style of reasoning.
@@ -887,8 +890,8 @@
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.
-\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
- and print terms or propositions according to the current theory or proof
+\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
commands are also useful in inspecting the current environment of term
abbreviations.
@@ -915,17 +918,16 @@
process.
\item [$\isarkeyword{pwd}~$] prints the current working directory.
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
- $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
+ $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
theory given as $name$ argument. These commands are basically the same as
- the corresponding ML functions\footnote{For historic reasons, the original
- ML versions also change the theory context to that of the theory loaded.}
- (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar
- versions may load new- and old-style theories alike.
+ the corresponding ML functions\footnote{The ML versions also change the
+ implicit theory context to that of the theory loaded.} (see also
+ \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may
+ load new- and old-style theories alike.
\end{descr}
-Note that these system commands are scarcely used when working with the
-Proof~General interface, since loading of theories is done fully
-transparently.
+These system commands are scarcely used when working with the Proof~General
+interface, since loading of theories is done fully transparently.
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/refcard.tex Sat Oct 30 20:41:30 1999 +0200
+++ b/doc-src/IsarRef/refcard.tex Sun Oct 31 15:20:35 1999 +0100
@@ -14,13 +14,13 @@
$\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
$\BG~\dots~\EN$ & declare explicit blocks \\
$\isarcmd{next}$ & switch implicit blocks \\
- $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
- $\LET{p = t}$ & \text{abbreviate terms by matching} \\
+ $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
+ $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
\end{tabular}
\begin{matharray}{rcl}
- theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
- & \Or & \LEMMA{name}{form}~proof \\
+ theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
+ & \Or & \LEMMA{name}{prop}~proof \\
& \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
stmt & = & \BG~stmt^*~\EN \\
@@ -28,11 +28,11 @@
& \Or & \NOTE{name}{name^+} \\
& \Or & \LET{term = term} \\[0.5ex]
& \Or & \FIX{var^+} \\
- & \Or & \ASSUME{name}{form^+}\\
+ & \Or & \ASSUME{name}{prop^+}\\
& \Or & \THEN~goal{\dsh}stmt \\
& \Or & goal{\dsh}stmt \\
- goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
- & \Or & \SHOW{name}{form}~proof \\
+ goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
+ & \Or & \SHOW{name}{prop}~proof \\
\end{matharray}
@@ -44,8 +44,8 @@
\DOT & \equiv & \BY{assumption} \\
\HENCENAME & \equiv & \THEN~\HAVENAME \\
\THUSNAME & \equiv & \THEN~\SHOWNAME \\
- \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
- \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
+ \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
+ \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
\FROM{this} & \equiv & \THEN \\
\FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
\FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
@@ -67,7 +67,7 @@
\subsection{Diagnostic commands}
\begin{matharray}{ll}
- \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
+ \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
\isarcmd{term}~t & \text{print term} \\
\isarcmd{prop}~\phi & \text{print meta-level proposition} \\
\isarcmd{typ}~\tau & \text{print meta-level type} \\
@@ -78,22 +78,22 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
- $assumption$ & apply assumption \\
- $rule~a@1~\dots~a@n$ & apply some rule \\
+ $assumption$ & apply some assumption \\
+ $rule~a@1\;\dots\;a@n$ & apply some rule \\
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
$induct~x$ & apply induction rule \\
- $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
+ $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
\multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
$-$ & \text{no rules} \\
- $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
- $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
- $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
+ $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
+ $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
+ $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
$simp$ & Simplifier \\
- $blast$, $fast$ & Classical reasoner \\
- $force$, $auto$ & Simplifier + Classical reasoner \\
+ $blast$, $fast$ & Classical Reasoner \\
+ $force$, $auto$ & Simplifier + Classical Reasoner \\
$arith$ & Arithmetic procedure \\
\end{tabular}
@@ -102,8 +102,8 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
- $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
- $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
+ $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
+ $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\
$RS~b$ & resolve fact with rule \\
$standard$ & put into standard result form \\
$rulify$ & put into object-rule form \\
@@ -111,12 +111,11 @@
\multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
$simp$ & declare Simplifier rules \\
- $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
- $iff$ & declare Simplifier + Classical reasoner rules \\
- $trans$ & calculational rules (general transitivity) \\
+ $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
+ $iff$ & declare Simplifier + Classical Reasoner rules \\
+ $trans$ & declare calculational rules (general transitivity) \\
\end{tabular}
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"