--- a/doc-src/Logics/FOL.tex Thu Jul 16 10:35:31 1998 +0200
+++ b/doc-src/Logics/FOL.tex Thu Jul 16 11:50:01 1998 +0200
@@ -7,16 +7,16 @@
\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is
obtained by adding the double negation rule. Basic proof procedures are
provided. The intuitionistic prover works with derived rules to simplify
-implications in the assumptions. Classical~{\tt FOL} employs Isabelle's
+implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's
classical reasoner, which simulates a sequent calculus.
\section{Syntax and rules of inference}
The logic is many-sorted, using Isabelle's type classes. The class of
-first-order terms is called \cldx{term} and is a subclass of {\tt logic}.
+first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
No types of individuals are provided, but extensions can define types such
-as {\tt nat::term} and type constructors such as {\tt list::(term)term}
-(see the examples directory, {\tt FOL/ex}). Below, the type variable
-$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
+as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
+(see the examples directory, \texttt{FOL/ex}). Below, the type variable
+$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax.
Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
@@ -45,8 +45,8 @@
conj_impE}, etc., support the intuitionistic proof procedure
(see~\S\ref{fol-int-prover}).
-See the files {\tt FOL/IFOL.thy}, {\tt FOL/IFOL.ML} and
-{\tt FOL/intprover.ML} for complete listings of the rules and
+See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
+\texttt{FOL/intprover.ML} for complete listings of the rules and
derived rules.
\begin{figure}
@@ -68,7 +68,7 @@
universal quantifier ($\forall$) \\
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
existential quantifier ($\exists$) \\
- {\tt EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
+ \texttt{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
unique existence ($\exists!$)
\end{tabular}
\index{*"E"X"! symbol}
@@ -108,7 +108,7 @@
\end{array}
\]
\subcaption{Grammar}
-\caption{Syntax of {\tt FOL}} \label{fol-syntax}
+\caption{Syntax of \texttt{FOL}} \label{fol-syntax}
\end{figure}
@@ -197,12 +197,12 @@
\begin{itemize}
\item
It instantiates the simplifier. Both equality ($=$) and the biconditional
-($\bimp$) may be used for rewriting. Tactics such as {\tt Asm_simp_tac} and
-{\tt Full_simp_tac} refer to the default simpset ({\tt simpset()}), which works for
+($\bimp$) may be used for rewriting. Tactics such as \texttt{Asm_simp_tac} and
+\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
most purposes. Named simplification sets include \ttindexbold{IFOL_ss},
for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
for classical logic. See the file
-{\tt FOL/simpdata.ML} for a complete listing of the simplification
+\texttt{FOL/simpdata.ML} for a complete listing of the simplification
rules%
\iflabelundefined{sec:setting-up-simp}{}%
{, and \S\ref{sec:setting-up-simp} for discussion}.
@@ -225,7 +225,7 @@
\section{Intuitionistic proof procedures} \label{fol-int-prover}
-Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose
+Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
difficulties for automated proof. In intuitionistic logic, the assumption
$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may
use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
@@ -239,7 +239,7 @@
\[ \infer[({\imp}E)]{Q}{P\imp Q &
\infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}
\]
-The theorem prover for intuitionistic logic does not use~{\tt impE}.\@
+The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
Instead, it simplifies implications using derived rules
(Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
@@ -264,7 +264,7 @@
IntPr.fast_tac : int -> tactic
IntPr.best_tac : int -> tactic
\end{ttbox}
-Most of these belong to the structure {\tt IntPr} and resemble the
+Most of these belong to the structure \texttt{IntPr} and resemble the
tactics of Isabelle's classical reasoner.
\begin{ttdescription}
@@ -277,30 +277,30 @@
produce multiple outcomes, enumerating all suitable pairs of assumptions.
\item[\ttindexbold{eq_mp_tac} {\it i}]
-is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
+is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
is safe.
\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
-care not to instantiate unknowns), or {\tt hyp_subst_tac}.
+care not to instantiate unknowns), or \texttt{hyp_subst_tac}.
\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
subgoals. It is deterministic, with at most one outcome.
-\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like {\tt safe_step_tac},
+\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
but allows unknowns to be instantiated.
-\item[\ttindexbold{IntPr.step_tac} $i$] tries {\tt safe_tac} or {\tt
+\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
inst_step_tac}, or applies an unsafe rule. This is the basic step of
the intuitionistic proof procedure.
-\item[\ttindexbold{IntPr.fast_tac} $i$] applies {\tt step_tac}, using
+\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
depth-first search, to solve subgoal~$i$.
-\item[\ttindexbold{IntPr.best_tac} $i$] applies {\tt step_tac}, using
+\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
best-first search (guided by the size of the proof state) to solve subgoal~$i$.
\end{ttdescription}
-Here are some of the theorems that {\tt IntPr.fast_tac} proves
+Here are some of the theorems that \texttt{IntPr.fast_tac} proves
automatically. The latter three date from {\it Principia Mathematica}
(*11.53, *11.55, *11.61)~\cite{principia}.
\begin{ttbox}
@@ -337,11 +337,11 @@
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule (see Fig.\ts\ref{fol-cla-derived}).
-The classical reasoner is installed. Tactics such as {\tt Blast_tac} and {\tt
-Best_tac} refer to the default claset ({\tt claset()}), which works for most
+The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
+Best_tac} refer to the default claset (\texttt{claset()}), which works for most
purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
-rules. See the file {\tt FOL/cladata.ML} for lists of the
+rules. See the file \texttt{FOL/cladata.ML} for lists of the
classical rules, and
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chap.\ts\ref{chap:classical}}
@@ -351,11 +351,15 @@
\section{An intuitionistic example}
Here is a session similar to one in {\em Logic and Computation}
\cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently
-from {\sc lcf}-based theorem provers such as {\sc hol}. The proof begins
-by entering the goal in intuitionistic logic, then applying the rule
-$({\imp}I)$.
+from {\sc lcf}-based theorem provers such as {\sc hol}.
+
+First, we specify that we are working in intuitionistic logic:
\begin{ttbox}
-goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+context IFOL.thy;
+\end{ttbox}
+The proof begins by entering the goal, then applying the rule $({\imp}I)$.
+\begin{ttbox}
+Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
{\out Level 0}
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
@@ -375,7 +379,7 @@
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
\end{ttbox}
-Applying $({\forall}I)$ replaces the \hbox{\tt ALL x} by \hbox{\tt!!x},
+Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
changing the universal quantifier from object~($\forall$) to
meta~($\Forall$). The bound variable is a {\bf parameter} of the
subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What
@@ -387,8 +391,8 @@
{\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
\end{ttbox}
The new subgoal~1 contains the function variable {\tt?y2}. Instantiating
-{\tt?y2} can replace~{\tt?y2(x)} by a term containing~{\tt x}, even
-though~{\tt x} is a bound variable. Now we analyse the assumption
+{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
+though~\texttt{x} is a bound variable. Now we analyse the assumption
\(\exists y.\forall x. Q(x,y)\) using elimination rules:
\begin{ttbox}
by (eresolve_tac [exE] 1);
@@ -396,10 +400,10 @@
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
\end{ttbox}
-Applying $(\exists E)$ has produced the parameter {\tt y} and stripped the
+Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
existential quantifier from the assumption. But the subgoal is unprovable:
-there is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}.
-Using {\tt choplev} we can return to the critical point. This time we
+there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
+Using \texttt{choplev} we can return to the critical point. This time we
apply $({\exists}E)$:
\begin{ttbox}
choplev 2;
@@ -427,9 +431,9 @@
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
\end{ttbox}
-The subgoal has variables {\tt ?y3} and {\tt ?x4} applied to both
+The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
-x} and \verb|?y3(x,y)| with~{\tt y}.
+x} and \verb|?y3(x,y)| with~\texttt{y}.
\begin{ttbox}
by (assume_tac 1);
{\out Level 6}
@@ -440,7 +444,7 @@
ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
theorem in one step.
\begin{ttbox}
-goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
{\out Level 0}
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
@@ -469,7 +473,7 @@
negations to implications using the definition $\neg P\equiv P\imp\bot$.
This allows use of the special implication rules.
\begin{ttbox}
-goalw IFOL.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))";
+Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
{\out Level 0}
{\out ~ ~ ((P --> Q) | (Q --> P))}
{\out 1. ((P --> Q) | (Q --> P) --> False) --> False}
@@ -525,20 +529,24 @@
{\out ~ ~ ((P --> Q) | (Q --> P))}
{\out No subgoals!}
\end{ttbox}
-This proof is also trivial for {\tt IntPr.fast_tac}.
+This proof is also trivial for \texttt{IntPr.fast_tac}.
\section{A classical example} \label{fol-cla-example}
To illustrate classical logic, we shall prove the theorem
$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
-$\all{x}P(x)$ is true. Either way the theorem holds.
+$\all{x}P(x)$ is true. Either way the theorem holds. First, we switch to
+classical logic:
+\begin{ttbox}
+context FOL.thy;
+\end{ttbox}
The formal proof does not conform in any obvious way to the sketch given
above. The key inference is the first one, \tdx{exCI}; this classical
version of~$(\exists I)$ allows multiple instantiation of the quantifier.
\begin{ttbox}
-goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
+Goal "EX y. ALL x. P(y)-->P(x)";
{\out Level 0}
{\out EX y. ALL x. P(y) --> P(x)}
{\out 1. EX y. ALL x. P(y) --> P(x)}
@@ -582,7 +590,7 @@
{\out EX y. ALL x. P(y) --> P(x)}
{\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
\end{ttbox}
-The previous conclusion, {\tt P(x)}, has become a negated assumption.
+The previous conclusion, \texttt{P(x)}, has become a negated assumption.
\begin{ttbox}
by (resolve_tac [impI] 1);
{\out Level 6}
@@ -603,15 +611,16 @@
{\out EX y. ALL x. P(y) --> P(x)}
{\out No subgoals!}
\end{ttbox}
-The civilised way to prove this theorem is through \ttindex{deepen_tac},
+The civilised way to prove this theorem is through \ttindex{Blast_tac},
which automatically uses the classical version of~$(\exists I)$:
\begin{ttbox}
-goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
+Goal "EX y. ALL x. P(y)-->P(x)";
{\out Level 0}
{\out EX y. ALL x. P(y) --> P(x)}
{\out 1. EX y. ALL x. P(y) --> P(x)}
-by (Deepen_tac 0 1);
+by (Blast_tac 1);
{\out Depth = 0}
+{\out Depth = 1}
{\out Depth = 2}
{\out Level 1}
{\out EX y. ALL x. P(y) --> P(x)}
@@ -644,7 +653,7 @@
& \infer*{S}{[\neg P,R]}}
\]
Having made these plans, we get down to work with Isabelle. The theory of
-classical logic, {\tt FOL}, is extended with the constant
+classical logic, \texttt{FOL}, is extended with the constant
$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the
equation~$(if)$.
\begin{ttbox}
@@ -653,25 +662,33 @@
rules if_def "if(P,Q,R) == P&Q | ~P&R"
end
\end{ttbox}
-The derivations of the introduction and elimination rules demonstrate the
-methods for rewriting with definitions. Classical reasoning is required,
-so we use {\tt blast_tac}.
+We create the file \texttt{If.thy} containing these declarations. (This file
+is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing
+\begin{ttbox}
+use_thy "If";
+\end{ttbox}
+loads that theory and sets it to be the current context.
\subsection{Deriving the introduction rule}
+
+The derivations of the introduction and elimination rules demonstrate the
+methods for rewriting with definitions. Classical reasoning is required,
+so we use \texttt{blast_tac}.
+
The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
concludes $if(P,Q,R)$. We propose the conclusion as the main goal
-using~\ttindex{goalw}, which uses {\tt if_def} to rewrite occurrences
+using~\ttindex{goalw}, which uses \texttt{if_def} to rewrite occurrences
of $if$ in the subgoal.
\begin{ttbox}
-val prems = goalw If.thy [if_def]
+val prems = Goalw [if_def]
"[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
{\out Level 0}
{\out if(P,Q,R)}
{\out 1. P & Q | ~ P & R}
\end{ttbox}
-The premises (bound to the {\ML} variable {\tt prems}) are passed as
-introduction rules to \ttindex{blast_tac}. Remember that {\tt claset()} refers
+The premises (bound to the {\ML} variable \texttt{prems}) are passed as
+introduction rules to \ttindex{blast_tac}. Remember that \texttt{claset()} refers
to the default classical set.
\begin{ttbox}
by (blast_tac (claset() addIs prems) 1);
@@ -686,15 +703,15 @@
The elimination rule has three premises, two of which are themselves rules.
The conclusion is simply $S$.
\begin{ttbox}
-val major::prems = goalw If.thy [if_def]
+val major::prems = Goalw [if_def]
"[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
{\out Level 0}
{\out S}
{\out 1. S}
\end{ttbox}
The major premise contains an occurrence of~$if$, but the version returned
-by \ttindex{goalw} (and bound to the {\ML} variable~{\tt major}) has the
-definition expanded. Now \ttindex{cut_facts_tac} inserts~{\tt major} as an
+by \ttindex{goalw} (and bound to the {\ML} variable~\texttt{major}) has the
+definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
\begin{ttbox}
by (cut_facts_tac [major] 1);
@@ -712,8 +729,8 @@
\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
{\S\ref{definitions}}, there are other
ways of treating definitions when deriving a rule. We can start the
-proof using {\tt goal}, which does not expand definitions, instead of
-{\tt goalw}. We can use \ttindex{rew_tac}
+proof using \texttt{goal}, which does not expand definitions, instead of
+\texttt{goalw}. We can use \ttindex{rew_tac}
to expand definitions in the subgoals --- perhaps after calling
\ttindex{cut_facts_tac} to insert the rule's premises. We can use
\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
@@ -729,12 +746,11 @@
if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))
\end{eqnarray*}
Proofs also require the classical reasoning rules and the $\bimp$
-introduction rule (called~\tdx{iffI}: do not confuse with~{\tt ifI}).
+introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}).
To display the $if$-rules in action, let us analyse a proof step by step.
\begin{ttbox}
-goal If.thy
- "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
+Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
{\out Level 0}
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
@@ -808,7 +824,7 @@
\end{ttbox}
This tactic also solves the other example.
\begin{ttbox}
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
{\out Level 0}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
@@ -839,8 +855,8 @@
{\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
\end{ttbox}
We are left with a subgoal in pure first-order logic, which is why the
-classical reasoner can prove it given {\tt FOL_cs} alone. (We could, of
-course, have used {\tt Blast_tac}.)
+classical reasoner can prove it given \texttt{FOL_cs} alone. (We could, of
+course, have used \texttt{Blast_tac}.)
\begin{ttbox}
by (blast_tac FOL_cs 1);
{\out Level 2}
@@ -851,7 +867,7 @@
approach has its merits --- especially if the prover for the base logic is
good --- but can be slow. In these examples, proofs using the default
claset (which includes the derived rules) run about six times faster
-than proofs using {\tt FOL_cs}.
+than proofs using \texttt{FOL_cs}.
Expanding definitions also complicates error diagnosis. Suppose we are having
difficulties in proving some goal. If by expanding definitions we have
@@ -860,7 +876,7 @@
Attempts at program verification often yield invalid assertions.
Let us try to prove one:
\begin{ttbox}
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
{\out Level 0}
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}