105

1 
%% $Id$

296

2 
\part{Getting Started with Isabelle}\label{chap:getting}

311

3 
Let us consider how to perform simple proofs using Isabelle. At present,


4 
Isabelle's user interface is \ML. Proofs are conducted by applying certain


5 
\ML{} functions, which update a stored proof state. All syntax must be


6 
expressed using {\sc ascii} characters. Menudriven graphical interfaces


7 
are under construction, but Isabelle users will always need to know some


8 
\ML, at least to use tacticals.

105

9 


10 
Objectlogics are built upon Pure Isabelle, which implements the metalogic


11 
and provides certain fundamental data structures: types, terms, signatures,


12 
theorems and theories, tactics and tacticals. These data structures have


13 
the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},


14 
{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt


15 
tactic>tactic}. Isabelle users can operate on these data structures by


16 
writing \ML{} programs.


17 

311

18 
\section{Forward proof}\label{sec:forward} \index{forward proof(}

105

19 
This section describes the concrete syntax for types, terms and theorems,


20 
and demonstrates forward proof.


21 


22 
\subsection{Lexical matters}

311

23 
\index{identifiers}\index{reserved words}

105

24 
An {\bf identifier} is a string of letters, digits, underscores~(\verb_)


25 
and single quotes~({\tt'}), beginning with a letter. Single quotes are


26 
regarded as primes; for instance {\tt x'} is read as~$x'$. Identifiers are


27 
separated by white space and special characters. {\bf Reserved words} are


28 
identifiers that appear in Isabelle syntax definitions.


29 


30 
An Isabelle theory can declare symbols composed of special characters, such


31 
as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}. (The latter three are part of


32 
the syntax of the metalogic.) Such symbols may be run together; thus if


33 
\verb} and \verb{ are used for set brackets then \verb{{a},{a,b}} is


34 
valid notation for a set of sets  but only if \verb}} and \verb{{


35 
have not been declared as symbols! The parser resolves any ambiguity by


36 
taking the longest possible symbol that has been declared. Thus the string


37 
{\tt==>} is read as a single symbol. But \hbox{\tt= =>} is read as two

296

38 
symbols.

105

39 


40 
Identifiers that are not reserved words may serve as free variables or

331

41 
constants. A {\bf type identifier} consists of an identifier prefixed by a


42 
prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand


43 
for (free) type variables, which remain fixed during a proof.


44 
\index{type identifiers}


45 


46 
An {\bf unknown}\index{unknowns} (or type unknown) consists of a question


47 
mark, an identifier (or type identifier), and a subscript. The subscript,


48 
a nonnegative integer,


49 
allows the renaming of unknowns prior to unification.%

296

50 
\footnote{The subscript may appear after the identifier, separated by a


51 
dot; this prevents ambiguity when the identifier ends with a digit. Thus


52 
{\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}


53 
has identifier {\tt"a0"} and subscript~5. If the identifier does not


54 
end with a digit, then no dot appears and a subscript of~0 is omitted;


55 
for example, {\tt?hello} has identifier {\tt"hello"} and subscript


56 
zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same


57 
conventions apply to type unknowns. The question mark is {\it not\/}


58 
part of the identifier!}

105

59 


60 


61 
\subsection{Syntax of types and terms}

311

62 
\index{classes!builtinbold}\index{syntax!of types and terms}


63 


64 
Classes are denoted by identifiers; the builtin class \cldx{logic}

105

65 
contains the `logical' types. Sorts are lists of classes enclosed in

296

66 
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.

105

67 

331

68 
\index{types!syntax ofbold}\index{sort constraints}

311

69 
Types are written with a syntax like \ML's. The builtin type \tydx{prop}

105

70 
is the type of propositions. Type variables can be constrained to particular


71 
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.


72 
\[\dquotes

311

73 
\index{*:: symbol}\index{*=> symbol}


74 
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}


75 
\index{*[ symbol}\index{*] symbol}

105

76 
\begin{array}{lll}


77 
\multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline

331

78 
\alpha "::" C & \alpha :: C & \hbox{class constraint} \\


79 
\alpha "::" "\{" C@1 "," \ldots "," C@n "\}" &


80 
\alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\


81 
\sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\

105

82 
"[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &


83 
[\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\


84 
"(" \tau@1"," \ldots "," \tau@n ")" tycon &


85 
(\tau@1, \ldots, \tau@n)tycon & \hbox{type construction}


86 
\end{array}


87 
\]


88 
Terms are those of the typed $\lambda$calculus.

331

89 
\index{terms!syntax ofbold}\index{type constraints}

105

90 
\[\dquotes

311

91 
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$abstractions}


92 
\index{*:: symbol}

105

93 
\begin{array}{lll}


94 
\multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline


95 
t "::" \sigma & t :: \sigma & \hbox{type constraint} \\


96 
"\%" x "." t & \lambda x.t & \hbox{abstraction} \\


97 
"\%" x@1\ldots x@n "." t & \lambda x@1\ldots x@n.t &


98 
\hbox{curried abstraction} \\


99 
t "(" u@1"," \ldots "," u@n ")" &


100 
t (u@1, \ldots, u@n) & \hbox{curried application}


101 
\end{array}


102 
\]


103 
The theorems and rules of an objectlogic are represented by theorems in


104 
the metalogic, which are expressed using metaformulae. Since the


105 
metalogic is higherorder, metaformulae~$\phi$, $\psi$, $\theta$,~\ldots{}

311

106 
are just terms of type~{\tt prop}.


107 
\index{metaimplication}


108 
\index{metaquantifiers}\index{metaequality}


109 
\index{*"!"! symbol}\index{*"[" symbol}\index{*""] symbol}


110 
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}

105

111 
\[\dquotes


112 
\begin{array}{l@{\quad}l@{\quad}l}


113 
\multicolumn{3}{c}{\hbox{ASCII Notation for MetaFormulae}} \\ \hline


114 
a " == " b & a\equiv b & \hbox{metaequality} \\


115 
a " =?= " b & a\qeq b & \hbox{flexflex constraint} \\


116 
\phi " ==> " \psi & \phi\Imp \psi & \hbox{metaimplication} \\


117 
"[" \phi@1 ";" \ldots ";" \phi@n "] ==> " \psi &


118 
\List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\


119 
"!!" x "." \phi & \Forall x.\phi & \hbox{metaquantification} \\


120 
"!!" x@1\ldots x@n "." \phi &


121 
\Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}


122 
\end{array}


123 
\]


124 
Flexflex constraints are metaequalities arising from unification; they


125 
require special treatment. See~\S\ref{flexflex}.

311

126 
\index{flexflex constraints}

105

127 

311

128 
\index{*Trueprop constant}

105

129 
Most logics define the implicit coercion $Trueprop$ from objectformulae to

311

130 
propositions. This could cause an ambiguity: in $P\Imp Q$, do the


131 
variables $P$ and $Q$ stand for metaformulae or objectformulae? If the


132 
latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To


133 
prevent such ambiguities, Isabelle's syntax does not allow a metaformula


134 
to consist of a variable. Variables of type~\tydx{prop} are seldom


135 
useful, but you can make a variable stand for a metaformula by prefixing


136 
it with the symbol {\tt PROP}:\index{*PROP symbol}

105

137 
\begin{ttbox}


138 
PROP ?psi ==> PROP ?theta


139 
\end{ttbox}


140 


141 
Symbols of objectlogics also must be rendered into {\sc ascii}, typically


142 
as follows:


143 
\[ \begin{tabular}{l@{\quad}l@{\quad}l}


144 
\tt True & $\top$ & true \\


145 
\tt False & $\bot$ & false \\


146 
\tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\


147 
\tt $P$  $Q$ & $P\disj Q$ & disjunction \\


148 
\verb'~' $P$ & $\neg P$ & negation \\


149 
\tt $P$ > $Q$ & $P\imp Q$ & implication \\


150 
\tt $P$ <> $Q$ & $P\bimp Q$ & biimplication \\


151 
\tt ALL $x\,y\,z$ .\ $P$ & $\forall x\,y\,z.P$ & for all \\


152 
\tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists


153 
\end{tabular}


154 
\]


155 
To illustrate the notation, consider two axioms for firstorder logic:


156 
$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$


157 
$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$

296

158 
Using the {\tt [\ldots]} shorthand, $({\conj}I)$ translates into

105

159 
{\sc ascii} characters as


160 
\begin{ttbox}


161 
[ ?P; ?Q ] ==> ?P & ?Q


162 
\end{ttbox}

296

163 
The schematic variables let unification instantiate the rule. To avoid


164 
cluttering logic definitions with question marks, Isabelle converts any


165 
free variables in a rule to schematic variables; we normally declare


166 
$({\conj}I)$ as

105

167 
\begin{ttbox}


168 
[ P; Q ] ==> P & Q


169 
\end{ttbox}


170 
This variables convention agrees with the treatment of variables in goals.


171 
Free variables in a goal remain fixed throughout the proof. After the


172 
proof is finished, Isabelle converts them to scheme variables in the


173 
resulting theorem. Scheme variables in a goal may be replaced by terms


174 
during the proof, supporting answer extraction, program synthesis, and so


175 
forth.


176 


177 
For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as


178 
\begin{ttbox}


179 
[ EX x.P(x); !!x. P(x) ==> Q ] ==> Q


180 
\end{ttbox}


181 


182 


183 
\subsection{Basic operations on theorems}


184 
\index{theorems!basic operations onbold}

311

185 
\index{LCF system}

331

186 
Metalevel theorems have the \ML{} type \mltydx{thm}. They represent the


187 
theorems and inference rules of objectlogics. Isabelle's metalogic is


188 
implemented using the {\sc lcf} approach: each metalevel inference rule is


189 
represented by a function from theorems to theorems. Objectlevel rules


190 
are taken as axioms.

105

191 


192 
The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt


193 
prthq}. Of the other operations on theorems, most useful are {\tt RS}


194 
and {\tt RSN}, which perform resolution.


195 

311

196 
\index{theorems!printing of}


197 
\begin{ttdescription}


198 
\item[\ttindex{prth} {\it thm};]


199 
prettyprints {\it thm\/} at the terminal.

105

200 

311

201 
\item[\ttindex{prths} {\it thms};]


202 
prettyprints {\it thms}, a list of theorems.

105

203 

311

204 
\item[\ttindex{prthq} {\it thmq};]


205 
prettyprints {\it thmq}, a sequence of theorems; this is useful for


206 
inspecting the output of a tactic.

105

207 

311

208 
\item[$thm1$ RS $thm2$] \index{*RS}


209 
resolves the conclusion of $thm1$ with the first premise of~$thm2$.

105

210 

311

211 
\item[$thm1$ RSN $(i,thm2)$] \index{*RSN}


212 
resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$.

105

213 

311

214 
\item[\ttindex{standard} $thm$]


215 
puts $thm$ into a standard format. It also renames schematic variables


216 
to have subscript zero, improving readability and reducing subscript


217 
growth.


218 
\end{ttdescription}

105

219 
The rules of a theory are normally bound to \ML\ identifiers. Suppose we

331

220 
are running an Isabelle session containing theory~\FOL, natural deduction


221 
firstorder logic.\footnote{For a listing of the \FOL{} rules and their


222 
\ML{} names, turn to


223 
\iflabelundefined{folrules}{{\em Isabelle's ObjectLogics}}%


224 
{page~\pageref{folrules}}.}


225 
Let us try an example given in~\S\ref{joining}. We


226 
first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with


227 
itself.

105

228 
\begin{ttbox}


229 
prth mp;


230 
{\out [ ?P > ?Q; ?P ] ==> ?Q}


231 
{\out val it = "[ ?P > ?Q; ?P ] ==> ?Q" : thm}


232 
prth (mp RS mp);


233 
{\out [ ?P1 > ?P > ?Q; ?P1; ?P ] ==> ?Q}


234 
{\out val it = "[ ?P1 > ?P > ?Q; ?P1; ?P ] ==> ?Q" : thm}


235 
\end{ttbox}

331

236 
User input appears in {\footnotesize\tt typewriter characters}, and output


237 
appears in {\sltt slanted typewriter characters}. \ML's response {\out val


238 
}~\ldots{} is compilerdependent and will sometimes be suppressed. This


239 
session illustrates two formats for the display of theorems. Isabelle's


240 
toplevel displays theorems as \ML{} values, enclosed in quotes. Printing


241 
commands like {\tt prth} omit the quotes and the surrounding {\tt val


242 
\ldots :\ thm}. Ignoring their sideeffects, the commands are identity


243 
functions.

105

244 


245 
To contrast {\tt RS} with {\tt RSN}, we resolve

311

246 
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.

105

247 
\begin{ttbox}


248 
conjunct1 RS mp;


249 
{\out val it = "[ (?P > ?Q) & ?Q1; ?P ] ==> ?Q" : thm}


250 
conjunct1 RSN (2,mp);


251 
{\out val it = "[ ?P > ?Q; ?P & ?Q1 ] ==> ?Q" : thm}


252 
\end{ttbox}


253 
These correspond to the following proofs:


254 
\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}


255 
\qquad


256 
\infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}}


257 
\]

296

258 
%


259 
Rules can be derived by pasting other rules together. Let us join

311

260 
\tdx{spec}, which stands for~$(\forall E)$, with {\tt mp} and {\tt

296

261 
conjunct1}. In \ML{}, the identifier~{\tt it} denotes the value just


262 
printed.

105

263 
\begin{ttbox}


264 
spec;


265 
{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}


266 
it RS mp;

296

267 
{\out val it = "[ ALL x. ?P3(x) > ?Q2(x); ?P3(?x1) ] ==>}


268 
{\out ?Q2(?x1)" : thm}

105

269 
it RS conjunct1;

296

270 
{\out val it = "[ ALL x. ?P4(x) > ?P6(x) & ?Q5(x); ?P4(?x2) ] ==>}


271 
{\out ?P6(?x2)" : thm}

105

272 
standard it;

296

273 
{\out val it = "[ ALL x. ?P(x) > ?Pa(x) & ?Q(x); ?P(?x) ] ==>}


274 
{\out ?Pa(?x)" : thm}

105

275 
\end{ttbox}


276 
By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have


277 
derived a destruction rule for formulae of the form $\forall x.


278 
P(x)\imp(Q(x)\conj R(x))$. Used with destructresolution, such specialized


279 
rules provide a way of referring to particular assumptions.

311

280 
\index{assumptions!use of}

105

281 

311

282 
\subsection{*Flexflex constraints} \label{flexflex}


283 
\index{flexflex constraintsbold}\index{unknowns!function}

105

284 
In higherorder unification, {\bf flexflex} equations are those where both


285 
sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.


286 
They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and


287 
$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown. They


288 
admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$


289 
and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$. Huet's


290 
procedure does not enumerate the unifiers; instead, it retains flexflex


291 
equations as constraints on future unifications. Flexflex constraints


292 
occasionally become attached to a proof state; more frequently, they appear


293 
during use of {\tt RS} and~{\tt RSN}:


294 
\begin{ttbox}


295 
refl;


296 
{\out val it = "?a = ?a" : thm}


297 
exI;


298 
{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}


299 
refl RS exI;


300 
{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}


301 
\end{ttbox}


302 


303 
\noindent


304 
Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with


305 
the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$. Instances


306 
satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and


307 
$\exists x.x=\Var{u}$. Calling \ttindex{flexflex_rule} removes all


308 
constraints by applying the trivial unifier:\index{*prthq}


309 
\begin{ttbox}


310 
prthq (flexflex_rule it);


311 
{\out EX x. ?a4 = ?a4}


312 
\end{ttbox}


313 
Isabelle simplifies flexflex equations to eliminate redundant bound


314 
variables. In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,


315 
there is no bound occurrence of~$x$ on the right side; thus, there will be

296

316 
none on the left in a common instance of these terms. Choosing a new

105

317 
variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,


318 
simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$


319 
from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda


320 
y.\Var{g}(y)$. By $\eta$conversion, this simplifies to the assignment


321 
$\Var{g}\equiv\lambda y.?h(k(y))$.


322 


323 
\begin{warn}


324 
\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless


325 
the resolution delivers {\bf exactly one} resolvent. For multiple results,


326 
use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The


327 
following example uses \ttindex{read_instantiate} to create an instance

311

328 
of \tdx{refl} containing no schematic variables.

105

329 
\begin{ttbox}


330 
val reflk = read_instantiate [("a","k")] refl;


331 
{\out val reflk = "k = k" : thm}


332 
\end{ttbox}


333 


334 
\noindent


335 
A flexflex constraint is no longer possible; resolution does not find a


336 
unique unifier:


337 
\begin{ttbox}


338 
reflk RS exI;


339 
{\out uncaught exception THM}


340 
\end{ttbox}


341 
Using \ttindex{RL} this time, we discover that there are four unifiers, and


342 
four resolvents:


343 
\begin{ttbox}


344 
[reflk] RL [exI];


345 
{\out val it = ["EX x. x = x", "EX x. k = x",}


346 
{\out "EX x. x = k", "EX x. k = k"] : thm list}


347 
\end{ttbox}


348 
\end{warn}


349 

311

350 
\index{forward proof)}

105

351 


352 
\section{Backward proof}


353 
Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning,


354 
large proofs require tactics. Isabelle provides a suite of commands for


355 
conducting a backward proof using tactics.


356 


357 
\subsection{The basic tactics}


358 
The tactics {\tt assume_tac}, {\tt


359 
resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most


360 
singlestep proofs. Although {\tt eresolve_tac} and {\tt dresolve_tac} are


361 
not strictly necessary, they simplify proofs involving elimination and


362 
destruction rules. All the tactics act on a subgoal designated by a


363 
positive integer~$i$, failing if~$i$ is out of range. The resolution


364 
tactics try their list of theorems in lefttoright order.


365 

311

366 
\begin{ttdescription}


367 
\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}


368 
is the tactic that attempts to solve subgoal~$i$ by assumption. Proof by


369 
assumption is not a trivial step; it can falsify other subgoals by


370 
instantiating shared variables. There may be several ways of solving the


371 
subgoal by assumption.

105

372 

311

373 
\item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}


374 
is the basic resolution tactic, used for most proof steps. The $thms$


375 
represent objectrules, which are resolved against subgoal~$i$ of the


376 
proof state. For each rule, resolution forms next states by unifying the


377 
conclusion with the subgoal and inserting instantiated premises in its


378 
place. A rule can admit many higherorder unifiers. The tactic fails if


379 
none of the rules generates next states.

105

380 

311

381 
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elimresolution}


382 
performs elimresolution. Like {\tt resolve_tac~{\it thms}~{\it i\/}}


383 
followed by {\tt assume_tac~{\it i}}, it applies a rule then solves its


384 
first premise by assumption. But {\tt eresolve_tac} additionally deletes


385 
that assumption from any subgoals arising from the resolution.

105

386 

311

387 
\item[\ttindex{dresolve_tac} {\it thms} {\it i}]


388 
\index{forward proof}\index{destructresolution}


389 
performs destructresolution with the~$thms$, as described


390 
in~\S\ref{destruct}. It is useful for forward reasoning from the


391 
assumptions.


392 
\end{ttdescription}

105

393 


394 
\subsection{Commands for backward proof}

311

395 
\index{proofs!commands for}

105

396 
Tactics are normally applied using the subgoal module, which maintains a


397 
proof state and manages the proof construction. It allows interactive


398 
backtracking through the proof space, going away to prove lemmas, etc.; of


399 
its many commands, most important are the following:

311

400 
\begin{ttdescription}


401 
\item[\ttindex{goal} {\it theory} {\it formula}; ]

105

402 
begins a new proof, where $theory$ is usually an \ML\ identifier


403 
and the {\it formula\/} is written as an \ML\ string.


404 

311

405 
\item[\ttindex{by} {\it tactic}; ]

105

406 
applies the {\it tactic\/} to the current proof


407 
state, raising an exception if the tactic fails.


408 

311

409 
\item[\ttindex{undo}(); ]

296

410 
reverts to the previous proof state. Undo can be repeated but cannot be


411 
undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely


412 
causes \ML\ to echo the value of that function.

105

413 

311

414 
\item[\ttindex{result}()]

105

415 
returns the theorem just proved, in a standard format. It fails if

296

416 
unproved subgoals are left, etc.

311

417 
\end{ttdescription}

105

418 
The commands and tactics given above are cumbersome for interactive use.


419 
Although our examples will use the full commands, you may prefer Isabelle's


420 
shortcuts:


421 
\begin{center} \tt

311

422 
\index{*br} \index{*be} \index{*bd} \index{*ba}

105

423 
\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}


424 
ba {\it i}; & by (assume_tac {\it i}); \\


425 


426 
br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\


427 


428 
be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\


429 


430 
bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i});


431 
\end{tabular}


432 
\end{center}


433 


434 
\subsection{A trivial example in propositional logic}


435 
\index{examples!propositional}

296

436 


437 
Directory {\tt FOL} of the Isabelle distribution defines the theory of


438 
firstorder logic. Let us try the example from \S\ref{propproof},


439 
entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these


440 
examples, see the file {\tt FOL/ex/intro.ML}. The files {\tt README} and


441 
{\tt Makefile} on the directories {\tt Pure} and {\tt FOL} explain how to


442 
build firstorder logic.}

105

443 
\begin{ttbox}


444 
goal FOL.thy "PP > P";


445 
{\out Level 0}


446 
{\out P  P > P}


447 
{\out 1. P  P > P}

311

448 
\end{ttbox}\index{level of a proof}

105

449 
Isabelle responds by printing the initial proof state, which has $P\disj

311

450 
P\imp P$ as the main goal and the only subgoal. The {\bf level} of the

105

451 
state is the number of {\tt by} commands that have been applied to reach

311

452 
it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI},

105

453 
or~$({\imp}I)$, to subgoal~1:


454 
\begin{ttbox}


455 
by (resolve_tac [impI] 1);


456 
{\out Level 1}


457 
{\out P  P > P}


458 
{\out 1. P  P ==> P}


459 
\end{ttbox}


460 
In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.


461 
(The metaimplication {\tt==>} indicates assumptions.) We apply

311

462 
\tdx{disjE}, or~(${\disj}E)$, to that subgoal:

105

463 
\begin{ttbox}


464 
by (resolve_tac [disjE] 1);


465 
{\out Level 2}


466 
{\out P  P > P}


467 
{\out 1. P  P ==> ?P1  ?Q1}


468 
{\out 2. [ P  P; ?P1 ] ==> P}


469 
{\out 3. [ P  P; ?Q1 ] ==> P}


470 
\end{ttbox}

296

471 
At Level~2 there are three subgoals, each provable by assumption. We


472 
deviate from~\S\ref{propproof} by tackling subgoal~3 first, using


473 
\ttindex{assume_tac}. This affects subgoal~1, updating {\tt?Q1} to~{\tt


474 
P}.

105

475 
\begin{ttbox}


476 
by (assume_tac 3);


477 
{\out Level 3}


478 
{\out P  P > P}


479 
{\out 1. P  P ==> ?P1  P}


480 
{\out 2. [ P  P; ?P1 ] ==> P}


481 
\end{ttbox}

296

482 
Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P} in subgoal~1.

105

483 
\begin{ttbox}


484 
by (assume_tac 2);


485 
{\out Level 4}


486 
{\out P  P > P}


487 
{\out 1. P  P ==> P  P}


488 
\end{ttbox}


489 
Lastly we prove the remaining subgoal by assumption:


490 
\begin{ttbox}


491 
by (assume_tac 1);


492 
{\out Level 5}


493 
{\out P  P > P}


494 
{\out No subgoals!}


495 
\end{ttbox}


496 
Isabelle tells us that there are no longer any subgoals: the proof is

311

497 
complete. Calling {\tt result} returns the theorem.

105

498 
\begin{ttbox}


499 
val mythm = result();


500 
{\out val mythm = "?P  ?P > ?P" : thm}


501 
\end{ttbox}


502 
Isabelle has replaced the free variable~{\tt P} by the scheme


503 
variable~{\tt?P}\@. Free variables in the proof state remain fixed


504 
throughout the proof. Isabelle finally converts them to scheme variables


505 
so that the resulting theorem can be instantiated with any formula.


506 

296

507 
As an exercise, try doing the proof as in \S\ref{propproof}, observing how


508 
instantiations affect the proof state.

105

509 

296

510 


511 
\subsection{Part of a distributive law}

105

512 
\index{examples!propositional}


513 
To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}

311

514 
and the tactical {\tt REPEAT}, let us prove part of the distributive

296

515 
law


516 
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \]

105

517 
We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:


518 
\begin{ttbox}


519 
goal FOL.thy "(P & Q)  R > (P  R)";


520 
{\out Level 0}


521 
{\out P & Q  R > P  R}


522 
{\out 1. P & Q  R > P  R}

296

523 
\ttbreak

105

524 
by (resolve_tac [impI] 1);


525 
{\out Level 1}


526 
{\out P & Q  R > P  R}


527 
{\out 1. P & Q  R ==> P  R}


528 
\end{ttbox}


529 
Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but


530 
\ttindex{eresolve_tac} deletes the assumption after use. The resulting proof


531 
state is simpler.


532 
\begin{ttbox}


533 
by (eresolve_tac [disjE] 1);


534 
{\out Level 2}


535 
{\out P & Q  R > P  R}


536 
{\out 1. P & Q ==> P  R}


537 
{\out 2. R ==> P  R}


538 
\end{ttbox}


539 
Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,


540 
replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the


541 
rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule


542 
and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two

296

543 
assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we


544 
may try out {\tt dresolve_tac}.

105

545 
\begin{ttbox}


546 
by (dresolve_tac [conjunct1] 1);


547 
{\out Level 3}


548 
{\out P & Q  R > P  R}


549 
{\out 1. P ==> P  R}


550 
{\out 2. R ==> P  R}


551 
\end{ttbox}


552 
The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.


553 
\begin{ttbox}


554 
by (resolve_tac [disjI1] 1);


555 
{\out Level 4}


556 
{\out P & Q  R > P  R}


557 
{\out 1. P ==> P}


558 
{\out 2. R ==> P  R}


559 
\ttbreak


560 
by (resolve_tac [disjI2] 2);


561 
{\out Level 5}


562 
{\out P & Q  R > P  R}


563 
{\out 1. P ==> P}


564 
{\out 2. R ==> R}


565 
\end{ttbox}

311

566 
Two calls of {\tt assume_tac} can finish the proof. The


567 
tactical~\ttindex{REPEAT} here expresses a tactic that calls {\tt assume_tac~1}

105

568 
as many times as possible. We can restrict attention to subgoal~1 because


569 
the other subgoals move up after subgoal~1 disappears.


570 
\begin{ttbox}


571 
by (REPEAT (assume_tac 1));


572 
{\out Level 6}


573 
{\out P & Q  R > P  R}


574 
{\out No subgoals!}


575 
\end{ttbox}


576 


577 


578 
\section{Quantifier reasoning}

331

579 
\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function}

105

580 
This section illustrates how Isabelle enforces quantifier provisos.

331

581 
Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier


582 
rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function


583 
unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of


584 
replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free


585 
occurrences of~$x$ and~$z$. On the other hand, no instantiation


586 
of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free


587 
occurrences of~$y$, since parameters are bound variables.

105

588 

296

589 
\subsection{Two quantifier proofs: a success and a failure}

105

590 
\index{examples!with quantifiers}


591 
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an


592 
attempted proof of the nontheorem $\exists y.\forall x.x=y$. The former


593 
proof succeeds, and the latter fails, because of the scope of quantified


594 
variables~\cite{paulson89}. Unification helps even in these trivial


595 
proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,


596 
but we need never say so. This choice is forced by the reflexive law for


597 
equality, and happens automatically.


598 

296

599 
\paragraph{The successful proof.}

105

600 
The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules


601 
$(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$:


602 
\begin{ttbox}


603 
goal FOL.thy "ALL x. EX y. x=y";


604 
{\out Level 0}


605 
{\out ALL x. EX y. x = y}


606 
{\out 1. ALL x. EX y. x = y}


607 
\ttbreak


608 
by (resolve_tac [allI] 1);


609 
{\out Level 1}


610 
{\out ALL x. EX y. x = y}


611 
{\out 1. !!x. EX y. x = y}


612 
\end{ttbox}


613 
The variable~{\tt x} is no longer universally quantified, but is a


614 
parameter in the subgoal; thus, it is universally quantified at the


615 
metalevel. The subgoal must be proved for all possible values of~{\tt x}.

296

616 


617 
To remove the existential quantifier, we apply the rule $(\exists I)$:

105

618 
\begin{ttbox}


619 
by (resolve_tac [exI] 1);


620 
{\out Level 2}


621 
{\out ALL x. EX y. x = y}


622 
{\out 1. !!x. x = ?y1(x)}


623 
\end{ttbox}


624 
The bound variable {\tt y} has become {\tt?y1(x)}. This term consists of


625 
the function unknown~{\tt?y1} applied to the parameter~{\tt x}.


626 
Instances of {\tt?y1(x)} may or may not contain~{\tt x}. We resolve the


627 
subgoal with the reflexivity axiom.


628 
\begin{ttbox}


629 
by (resolve_tac [refl] 1);


630 
{\out Level 3}


631 
{\out ALL x. EX y. x = y}


632 
{\out No subgoals!}


633 
\end{ttbox}


634 
Let us consider what has happened in detail. The reflexivity axiom is


635 
lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is


636 
unified with $\Forall x.x=\Var{y@1}(x)$. The function unknowns $\Var{f}$


637 
and~$\Var{y@1}$ are both instantiated to the identity function, and


638 
$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$reduction.


639 

296

640 
\paragraph{The unsuccessful proof.}


641 
We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and

105

642 
try~$(\exists I)$:


643 
\begin{ttbox}


644 
goal FOL.thy "EX y. ALL x. x=y";


645 
{\out Level 0}


646 
{\out EX y. ALL x. x = y}


647 
{\out 1. EX y. ALL x. x = y}


648 
\ttbreak


649 
by (resolve_tac [exI] 1);


650 
{\out Level 1}


651 
{\out EX y. ALL x. x = y}


652 
{\out 1. ALL x. x = ?y}


653 
\end{ttbox}


654 
The unknown {\tt ?y} may be replaced by any term, but this can never


655 
introduce another bound occurrence of~{\tt x}. We now apply~$(\forall I)$:


656 
\begin{ttbox}


657 
by (resolve_tac [allI] 1);


658 
{\out Level 2}


659 
{\out EX y. ALL x. x = y}


660 
{\out 1. !!x. x = ?y}


661 
\end{ttbox}


662 
Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we


663 
have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}.


664 
The reflexivity axiom does not unify with subgoal~1.


665 
\begin{ttbox}


666 
by (resolve_tac [refl] 1);


667 
{\out by: tactic returned no results}


668 
\end{ttbox}

296

669 
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of


670 
firstorder logic. I have elsewhere proved the faithfulness of Isabelle's


671 
encoding of firstorder logic~\cite{paulson89}; there could, of course, be


672 
faults in the implementation.

105

673 


674 


675 
\subsection{Nested quantifiers}


676 
\index{examples!with quantifiers}

296

677 
Multiple quantifiers create complex terms. Proving


678 
\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \]


679 
will demonstrate how parameters and unknowns develop. If they appear in


680 
the wrong order, the proof will fail.


681 

105

682 
This section concludes with a demonstration of {\tt REPEAT}


683 
and~{\tt ORELSE}.


684 
\begin{ttbox}


685 
goal FOL.thy "(ALL x y.P(x,y)) > (ALL z w.P(w,z))";


686 
{\out Level 0}


687 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


688 
{\out 1. (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


689 
\ttbreak


690 
by (resolve_tac [impI] 1);


691 
{\out Level 1}


692 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


693 
{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}


694 
\end{ttbox}


695 

296

696 
\paragraph{The wrong approach.}

311

697 
Using {\tt dresolve_tac}, we apply the rule $(\forall E)$, bound to the


698 
\ML\ identifier \tdx{spec}. Then we apply $(\forall I)$.

105

699 
\begin{ttbox}


700 
by (dresolve_tac [spec] 1);


701 
{\out Level 2}


702 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


703 
{\out 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}


704 
\ttbreak


705 
by (resolve_tac [allI] 1);


706 
{\out Level 3}


707 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


708 
{\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}


709 
\end{ttbox}

311

710 
The unknown {\tt ?x1} and the parameter {\tt z} have appeared. We again

296

711 
apply $(\forall E)$ and~$(\forall I)$.

105

712 
\begin{ttbox}


713 
by (dresolve_tac [spec] 1);


714 
{\out Level 4}


715 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


716 
{\out 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}


717 
\ttbreak


718 
by (resolve_tac [allI] 1);


719 
{\out Level 5}


720 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


721 
{\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}


722 
\end{ttbox}


723 
The unknown {\tt ?y3} and the parameter {\tt w} have appeared. Each


724 
unknown is applied to the parameters existing at the time of its creation;

311

725 
instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances


726 
of {\tt?y3(z)} can only contain~{\tt z}. Due to the restriction on~{\tt ?x1},

105

727 
proof by assumption will fail.


728 
\begin{ttbox}


729 
by (assume_tac 1);


730 
{\out by: tactic returned no results}


731 
{\out uncaught exception ERROR}


732 
\end{ttbox}


733 

296

734 
\paragraph{The right approach.}

105

735 
To do this proof, the rules must be applied in the correct order.

331

736 
Parameters should be created before unknowns. The

105

737 
\ttindex{choplev} command returns to an earlier stage of the proof;


738 
let us return to the result of applying~$({\imp}I)$:


739 
\begin{ttbox}


740 
choplev 1;


741 
{\out Level 1}


742 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


743 
{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}


744 
\end{ttbox}

296

745 
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$.

105

746 
\begin{ttbox}


747 
by (resolve_tac [allI] 1);


748 
{\out Level 2}


749 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


750 
{\out 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}


751 
\ttbreak


752 
by (resolve_tac [allI] 1);


753 
{\out Level 3}


754 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


755 
{\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)}


756 
\end{ttbox}


757 
The parameters {\tt z} and~{\tt w} have appeared. We now create the


758 
unknowns:


759 
\begin{ttbox}


760 
by (dresolve_tac [spec] 1);


761 
{\out Level 4}


762 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


763 
{\out 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}


764 
\ttbreak


765 
by (dresolve_tac [spec] 1);


766 
{\out Level 5}


767 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


768 
{\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}


769 
\end{ttbox}


770 
Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt


771 
z} and~{\tt w}:


772 
\begin{ttbox}


773 
by (assume_tac 1);


774 
{\out Level 6}


775 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


776 
{\out No subgoals!}


777 
\end{ttbox}


778 

296

779 
\paragraph{A onestep proof using tacticals.}


780 
\index{tacticals} \index{examples!of tacticals}


781 


782 
Repeated application of rules can be effective, but the rules should be

331

783 
attempted in the correct order. Let us return to the original goal using


784 
\ttindex{choplev}:

105

785 
\begin{ttbox}


786 
choplev 0;


787 
{\out Level 0}


788 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


789 
{\out 1. (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


790 
\end{ttbox}

311

791 
As we have just seen, \tdx{allI} should be attempted


792 
before~\tdx{spec}, while \ttindex{assume_tac} generally can be

296

793 
attempted first. Such priorities can easily be expressed


794 
using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.

105

795 
\begin{ttbox}

296

796 
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1

105

797 
ORELSE dresolve_tac [spec] 1));


798 
{\out Level 1}


799 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))}


800 
{\out No subgoals!}


801 
\end{ttbox}


802 


803 


804 
\subsection{A realistic quantifier proof}


805 
\index{examples!with quantifiers}

296

806 
To see the practical use of parameters and unknowns, let us prove half of


807 
the equivalence


808 
\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \]


809 
We state the lefttoright half to Isabelle in the normal way.

105

810 
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we

311

811 
use {\tt REPEAT}:

105

812 
\begin{ttbox}


813 
goal FOL.thy "(ALL x.P(x) > Q) > (EX x.P(x)) > Q";


814 
{\out Level 0}


815 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


816 
{\out 1. (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


817 
\ttbreak


818 
by (REPEAT (resolve_tac [impI] 1));


819 
{\out Level 1}


820 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


821 
{\out 1. [ ALL x. P(x) > Q; EX x. P(x) ] ==> Q}


822 
\end{ttbox}


823 
We can eliminate the universal or the existential quantifier. The


824 
existential quantifier should be eliminated first, since this creates a


825 
parameter. The rule~$(\exists E)$ is bound to the

311

826 
identifier~\tdx{exE}.

105

827 
\begin{ttbox}


828 
by (eresolve_tac [exE] 1);


829 
{\out Level 2}


830 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


831 
{\out 1. !!x. [ ALL x. P(x) > Q; P(x) ] ==> Q}


832 
\end{ttbox}


833 
The only possibility now is $(\forall E)$, a destruction rule. We use


834 
\ttindex{dresolve_tac}, which discards the quantified assumption; it is


835 
only needed once.


836 
\begin{ttbox}


837 
by (dresolve_tac [spec] 1);


838 
{\out Level 3}


839 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


840 
{\out 1. !!x. [ P(x); P(?x3(x)) > Q ] ==> Q}


841 
\end{ttbox}

296

842 
Because we applied $(\exists E)$ before $(\forall E)$, the unknown


843 
term~{\tt?x3(x)} may depend upon the parameter~{\tt x}.

105

844 


845 
Although $({\imp}E)$ is a destruction rule, it works with


846 
\ttindex{eresolve_tac} to perform backward chaining. This technique is


847 
frequently useful.


848 
\begin{ttbox}


849 
by (eresolve_tac [mp] 1);


850 
{\out Level 4}


851 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


852 
{\out 1. !!x. P(x) ==> P(?x3(x))}


853 
\end{ttbox}


854 
The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the


855 
implication. The final step is trivial, thanks to the occurrence of~{\tt x}.


856 
\begin{ttbox}


857 
by (assume_tac 1);


858 
{\out Level 5}


859 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q}


860 
{\out No subgoals!}


861 
\end{ttbox}


862 


863 

311

864 
\subsection{The classical reasoner}


865 
\index{classical reasoner}

105

866 
Although Isabelle cannot compete with fully automatic theorem provers, it


867 
provides enough automation to tackle substantial examples. The classical

331

868 
reasoner can be set up for any classical natural deduction logic;


869 
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%


870 
{Chap.\ts\ref{chap:classical}}.

105

871 

331

872 
Rules are packaged into {\bf classical sets}. The classical reasoner


873 
provides several tactics, which apply rules using naive algorithms.


874 
Unification handles quantifiers as shown above. The most useful tactic

105

875 
is~\ttindex{fast_tac}.


876 


877 
Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The


878 
backslashes~\hbox{\verb\\ldots\verb\} are an \ML{} string escape


879 
sequence, to break the long string over two lines.)


880 
\begin{ttbox}


881 
goal FOL.thy "(EX y. ALL x. J(y,x) <> ~J(x,x)) \ttback


882 
\ttback > ~ (ALL x. EX y. ALL z. J(z,y) <> ~ J(z,x))";


883 
{\out Level 0}


884 
{\out (EX y. ALL x. J(y,x) <> ~J(x,x)) >}


885 
{\out ~(ALL x. EX y. ALL z. J(z,y) <> ~J(z,x))}


886 
{\out 1. (EX y. ALL x. J(y,x) <> ~J(x,x)) >}


887 
{\out ~(ALL x. EX y. ALL z. J(z,y) <> ~J(z,x))}


888 
\end{ttbox}


889 
The rules of classical logic are bundled as {\tt FOL_cs}. We may solve


890 
subgoal~1 at a stroke, using~\ttindex{fast_tac}.


891 
\begin{ttbox}


892 
by (fast_tac FOL_cs 1);


893 
{\out Level 1}


894 
{\out (EX y. ALL x. J(y,x) <> ~J(x,x)) >}


895 
{\out ~(ALL x. EX y. ALL z. J(z,y) <> ~J(z,x))}


896 
{\out No subgoals!}


897 
\end{ttbox}


898 
Sceptics may examine the proof by calling the package's singlestep


899 
tactics, such as~{\tt step_tac}. This would take up much space, however,


900 
so let us proceed to the next example:


901 
\begin{ttbox}


902 
goal FOL.thy "ALL x. P(x,f(x)) <> \ttback


903 
\ttback (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))";


904 
{\out Level 0}


905 
{\out ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))}

296

906 
{\out 1. ALL x. P(x,f(x)) <>}


907 
{\out (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))}

105

908 
\end{ttbox}


909 
Again, subgoal~1 succumbs immediately.


910 
\begin{ttbox}


911 
by (fast_tac FOL_cs 1);


912 
{\out Level 1}


913 
{\out ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))}


914 
{\out No subgoals!}


915 
\end{ttbox}

331

916 
The classical reasoner is not restricted to the usual logical connectives.


917 
The natural deduction rules for unions and intersections resemble those for


918 
disjunction and conjunction. The rules for infinite unions and


919 
intersections resemble those for quantifiers. Given such rules, the classical


920 
reasoner is effective for reasoning in set theory.


921 
