--- a/doc-src/Logics/LK.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Logics/LK.tex Mon Aug 28 13:52:38 2000 +0200
@@ -18,8 +18,8 @@
are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
belongs to class {\tt logic}.
-\LK{} implements a classical logic theorem prover that is nearly as powerful
-as the generic classical reasoner. The simplifier is now available too.
+LK implements a classical logic theorem prover that is nearly as powerful as
+the generic classical reasoner. The simplifier is now available too.
To work in LK, start up Isabelle specifying \texttt{Sequents} as the
object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:
@@ -179,17 +179,17 @@
of formulae.
The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
-satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{}
-denote something, a description is always meaningful, but we do not know
-its value unless $P[x]$ defines it uniquely. The Isabelle notation is
-\hbox{\tt THE $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules})
-does not entail the Axiom of Choice because it requires uniqueness.
+satisfying~$P[a]$, if one exists and is unique. Since all terms in LK denote
+something, a description is always meaningful, but we do not know its value
+unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE
+ $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not
+entail the Axiom of Choice because it requires uniqueness.
Conditional expressions are available with the notation
\[ \dquotes
"if"~formula~"then"~term~"else"~term. \]
-Figure~\ref{lk-grammar} presents the grammar of \LK. Traditionally,
+Figure~\ref{lk-grammar} presents the grammar of LK. Traditionally,
\(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's
notation, the prefix~\verb|$| on a term makes it range over sequences.
In a sequent, anything not prefixed by \verb|$| is taken as a formula.
@@ -272,13 +272,13 @@
\section{Automatic Proof}
-\LK{} instantiates Isabelle's simplifier. Both equality ($=$) and the
+LK instantiates Isabelle's simplifier. Both equality ($=$) and the
biconditional ($\bimp$) may be used for rewriting. The tactic
\texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With
sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
-required; all the formulae{} in the sequent will be simplified. The
-left-hand formulae{} are taken as rewrite rules. (Thus, the behaviour is what
-you would normally expect from calling \texttt{Asm_full_simp_tac}.)
+required; all the formulae{} in the sequent will be simplified. The left-hand
+formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would
+normally expect from calling \texttt{Asm_full_simp_tac}.)
For classical reasoning, several tactics are available:
\begin{ttbox}
@@ -325,15 +325,13 @@
These tactics refine a subgoal into two by applying the cut rule. The cut
formula is given as a string, and replaces some other formula in the sequent.
\begin{ttdescription}
-\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}]
-reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It
-then deletes some formula from the right side of subgoal~$i$, replacing
-that formula by~$P$.
-
-\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}]
-reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It
-then deletes some formula from the left side of the new subgoal $i+1$,
-replacing that formula by~$P$.
+\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
+ applies the cut rule to subgoal~$i$. It then deletes some formula from the
+ right side of subgoal~$i$, replacing that formula by~$P$.
+
+\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
+ applies the cut rule to subgoal~$i$. It then deletes some formula from the
+ left side of the new subgoal $i+1$, replacing that formula by~$P$.
\end{ttdescription}
All the structural rules --- cut, contraction, and thinning --- can be
applied to particular formulae using {\tt res_inst_tac}.
@@ -378,11 +376,11 @@
\section{A simple example of classical reasoning}
The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
-classical treatment of the existential quantifier. Classical reasoning
-is easy using~{\LK}, as you can see by comparing this proof with the one
-given in the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the
-proofs are essentially the same; the key step here is to use \tdx{exR}
-rather than the weaker~\tdx{exR_thin}.
+classical treatment of the existential quantifier. Classical reasoning is
+easy using~LK, as you can see by comparing this proof with the one given in
+the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs
+are essentially the same; the key step here is to use \tdx{exR} rather than
+the weaker~\tdx{exR_thin}.
\begin{ttbox}
Goal "|- EX y. ALL x. P(y)-->P(x)";
{\out Level 0}
@@ -405,10 +403,10 @@
{\out |- EX y. ALL x. P(y) --> P(x)}
{\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
\end{ttbox}
-Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
-become an assumption; instead, it moves to the left side. The
-resulting subgoal cannot be instantiated to a basic sequent: the bound
-variable~$x$ is not unifiable with the unknown~$\Var{x}$.
+Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
+assumption; instead, it moves to the left side. The resulting subgoal cannot
+be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
+with the unknown~$\Var{x}$.
\begin{ttbox}
by (resolve_tac [basic] 1);
{\out by: tactic failed}
@@ -548,10 +546,10 @@
Multiple unifiers occur whenever this is resolved against a goal containing
more than one conjunction on the left.
-\LK{} exploits this representation of lists. As an alternative, the
-sequent calculus can be formalized using an ordinary representation of
-lists, with a logic program for removing a formula from a list. Amy Felty
-has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
+LK exploits this representation of lists. As an alternative, the sequent
+calculus can be formalized using an ordinary representation of lists, with a
+logic program for removing a formula from a list. Amy Felty has applied this
+technique using the language $\lambda$Prolog~\cite{felty91a}.
Explicit formalization of sequents can be tiresome. But it gives precise
control over contraction and weakening, and is essential to handle relevant
@@ -575,10 +573,10 @@
rules require a search strategy, such as backtracking.
A \textbf{pack} is a pair whose first component is a list of safe rules and
-whose second is a list of unsafe rules. Packs can be extended in an
-obvious way to allow reasoning with various collections of rules. For
-clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is
-essentially a type synonym:
+whose second is a list of unsafe rules. Packs can be extended in an obvious
+way to allow reasoning with various collections of rules. For clarity, LK
+declares \mltydx{pack} as an \ML{} datatype, although is essentially a type
+synonym:
\begin{ttbox}
datatype pack = Pack of thm list * thm list;
\end{ttbox}
@@ -628,8 +626,7 @@
\section{*Proof procedures}\label{sec:sequent-provers}
-The \LK{} proof procedure is similar to the classical reasoner
-described in
+The LK proof procedure is similar to the classical reasoner described in
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chap.\ts\ref{chap:classical}}.
%