105

1 
%% $Id$

296

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


3 
We now consider how to perform simple proofs using Isabelle. As of this


4 
writing, Isabelle's user interface is \ML. Proofs are conducted by


5 
applying certain \ML{} functions, which update a stored proof state. All


6 
syntax must be expressed using {\sc ascii} characters. Menudriven


7 
graphical interfaces are under construction, but Isabelle users will always


8 
need to know some \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 


18 
\section{Forward proof}


19 
\index{Isabelle!getting started}\index{ML}


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


21 
and demonstrates forward proof.


22 


23 
\subsection{Lexical matters}


24 
\index{identifiersbold}\index{reserved wordsbold}


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


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


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


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


29 
identifiers that appear in Isabelle syntax definitions.


30 


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


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


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


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


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


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


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


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

296

39 
symbols.

105

40 


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


42 
constants. A type identifier consists of an identifier prefixed by a


43 
prime, for example {\tt'a} and \hbox{\tt'hello}. An unknown (or type


44 
unknown) consists of a question mark, an identifier (or type identifier),


45 
and a subscript. The subscript, a nonnegative integer, allows the

296

46 
renaming of unknowns prior to unification.%


47 
%


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


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


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


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


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


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


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


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


56 
part of the identifier!}

105

57 


58 


59 
\subsection{Syntax of types and terms}


60 
\index{Isabelle!syntax of}


61 
\index{classes!builtinbold}


62 
Classes are denoted by identifiers; the builtin class \ttindex{logic}


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

296

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

105

65 


66 
\index{types!syntaxbold}


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


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


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


70 
\[\dquotes


71 
\begin{array}{lll}


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


73 
t "::" C & t :: C & \hbox{class constraint} \\


74 
t "::" "\{" C@1 "," \ldots "," C@n "\}" &


75 
t :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\


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


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


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


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


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


81 
\end{array}


82 
\]


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


84 
\index{terms!syntaxbold}


85 
\[\dquotes


86 
\begin{array}{lll}


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


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


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


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


91 
\hbox{curried abstraction} \\


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


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


94 
\end{array}


95 
\]


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


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


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


99 
are just terms of type~\ttindex{prop}.


100 
\index{metaformulae!syntaxbold}


101 
\[\dquotes


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


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


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


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


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


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


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


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


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


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


112 
\end{array}


113 
\]


114 
Flexflex constraints are metaequalities arising from unification; they


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


116 
\index{flexflex equations}


117 


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


119 
propositions.


120 
\index{Trueprop@{$Trueprop$}}


121 
This could cause an ambiguity: in $P\Imp Q$, do the variables $P$ and $Q$


122 
stand for metaformulae or objectformulae? If the latter, $P\Imp Q$


123 
really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To prevent such


124 
ambiguities, Isabelle's syntax does not allow a metaformula to consist of


125 
a variable. Variables of type~\ttindex{prop} are seldom useful, but you


126 
can make a variable stand for a metaformula by prefixing it with the


127 
keyword \ttindex{PROP}:


128 
\begin{ttbox}


129 
PROP ?psi ==> PROP ?theta


130 
\end{ttbox}


131 


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


133 
as follows:


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


135 
\tt True & $\top$ & true \\


136 
\tt False & $\bot$ & false \\


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


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


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


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


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


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


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


144 
\end{tabular}


145 
\]


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


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


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

296

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

105

150 
{\sc ascii} characters as


151 
\begin{ttbox}


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


153 
\end{ttbox}

296

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


155 
cluttering logic definitions with question marks, Isabelle converts any


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


157 
$({\conj}I)$ as

105

158 
\begin{ttbox}


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


160 
\end{ttbox}


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


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


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


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


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


166 
forth.


167 


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


169 
\begin{ttbox}


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


171 
\end{ttbox}


172 


173 


174 
\subsection{Basic operations on theorems}


175 
\index{theorems!basic operations onbold}


176 
\index{LCF}


177 
Metalevel theorems have type \ttindex{thm} and represent the theorems and


178 
inference rules of objectlogics. Isabelle's metalogic is implemented


179 
using the {\sc lcf} approach: each metalevel inference rule is represented by


180 
a function from theorems to theorems. Objectlevel rules are taken as


181 
axioms.


182 


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


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


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


186 


187 
\index{printing commandsbold}


188 
\begin{description}


189 
\item[\ttindexbold{prth} {\it thm}] prettyprints {\it thm\/} at the terminal.


190 


191 
\item[\ttindexbold{prths} {\it thms}] prettyprints {\it thms}, a list of


192 
theorems.


193 


194 
\item[\ttindexbold{prthq} {\it thmq}] prettyprints {\it thmq}, a sequence of


195 
theorems; this is useful for inspecting the output of a tactic.


196 


197 
\item[\tt$thm1$ RS $thm2$] \indexbold{*RS} resolves the conclusion of $thm1$


198 
with the first premise of~$thm2$.


199 


200 
\item[\tt$thm1$ RSN $(i,thm2)$] \indexbold{*RSN} resolves the conclusion of $thm1$


201 
with the $i$th premise of~$thm2$.


202 


203 
\item[\ttindexbold{standard} $thm$] puts $thm$ into a standard


204 
format. It also renames schematic variables to have subscript zero,


205 
improving readability and reducing subscript growth.


206 
\end{description}


207 
\index{ML}


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


209 
are running an Isabelle session containing natural deduction firstorder


210 
logic. Let us try an example given in~\S\ref{joining}. We first print


211 
\ttindex{mp}, which is the rule~$({\imp}E)$, then resolve it with itself.


212 
\begin{ttbox}


213 
prth mp;


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


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


216 
prth (mp RS mp);


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


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


219 
\end{ttbox}

296

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


221 
{\sltt slanted typewriter characters}. \ML's response {\out val }~\ldots{}


222 
is compilerdependent and will sometimes be suppressed. This session


223 
illustrates two formats for the display of theorems. Isabelle's toplevel


224 
displays theorems as ML values, enclosed in quotes.\footnote{This works


225 
under both Poly/ML and Standard ML of New Jersey.} Printing commands


226 
like {\tt prth} omit the quotes and the surrounding {\tt val \ldots :\


227 
thm}. Ignoring their sideeffects, the commands are identity functions.

105

228 


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


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


231 
\begin{ttbox}


232 
conjunct1 RS mp;


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


234 
conjunct1 RSN (2,mp);


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


236 
\end{ttbox}


237 
These correspond to the following proofs:


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


239 
\qquad


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


241 
\]

296

242 
%


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


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


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


246 
printed.

105

247 
\begin{ttbox}


248 
spec;


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


250 
it RS mp;

296

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


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

105

253 
it RS conjunct1;

296

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


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

105

256 
standard it;

296

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


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

105

259 
\end{ttbox}


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


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


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


263 
rules provide a way of referring to particular assumptions.


264 

296

265 
\subsection{*Flexflex equations} \label{flexflex}

105

266 
\index{flexflex equationsbold}\index{unknowns!of function type}


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


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


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


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


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


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


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


274 
equations as constraints on future unifications. Flexflex constraints


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


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


277 
\begin{ttbox}


278 
refl;


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


280 
exI;


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


282 
refl RS exI;


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


284 
\end{ttbox}


285 


286 
\noindent


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


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


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


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


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


292 
\begin{ttbox}


293 
prthq (flexflex_rule it);


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


295 
\end{ttbox}


296 
Isabelle simplifies flexflex equations to eliminate redundant bound


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


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

296

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

105

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


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


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


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


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


305 


306 
\begin{warn}


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


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


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


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


311 
of \ttindex{refl} containing no schematic variables.


312 
\begin{ttbox}


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


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


315 
\end{ttbox}


316 


317 
\noindent


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


319 
unique unifier:


320 
\begin{ttbox}


321 
reflk RS exI;


322 
{\out uncaught exception THM}


323 
\end{ttbox}


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


325 
four resolvents:


326 
\begin{ttbox}


327 
[reflk] RL [exI];


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


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


330 
\end{ttbox}


331 
\end{warn}


332 


333 


334 
\section{Backward proof}


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


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


337 
conducting a backward proof using tactics.


338 


339 
\subsection{The basic tactics}


340 
\index{tactics!basicbold}


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


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


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


344 
not strictly necessary, they simplify proofs involving elimination and


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


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


347 
tactics try their list of theorems in lefttoright order.


348 


349 
\begin{description}


350 
\item[\ttindexbold{assume_tac} {\it i}] is the tactic that attempts to solve


351 
subgoal~$i$ by assumption. Proof by assumption is not a trivial step; it


352 
can falsify other subgoals by instantiating shared variables. There may be


353 
several ways of solving the subgoal by assumption.


354 


355 
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]


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


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


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


359 
conclusion with the subgoal and inserting instantiated premises in its


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


361 
none of the rules generates next states.


362 


363 
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]


364 
performs elimresolution. Like


365 
\hbox{\tt resolve_tac {\it thms} {\it i}} followed by \hbox{\tt assume_tac


366 
{\it i}}, it applies a rule then solves its first premise by assumption.


367 
But {\tt eresolve_tac} additionally deletes that assumption from any


368 
subgoals arising from the resolution.


369 


370 


371 
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]


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


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


374 
assumptions.


375 
\end{description}


376 


377 
\subsection{Commands for backward proof}


378 
\index{proof!commands forbold}


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


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


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


382 
its many commands, most important are the following:


383 
\begin{description}


384 
\item[\ttindexbold{goal} {\it theory} {\it formula}; ]


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


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


387 


388 
\item[\ttindexbold{by} {\it tactic}; ]


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


390 
state, raising an exception if the tactic fails.


391 

296

392 
\item[\ttindexbold{undo}(); ]


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


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


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

105

396 


397 
\item[\ttindexbold{result}()]


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

296

399 
unproved subgoals are left, etc.

105

400 
\end{description}


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


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


403 
shortcuts:


404 
\begin{center} \tt


405 
\indexbold{*br} \indexbold{*be} \indexbold{*bd} \indexbold{*ba}


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


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


408 


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


410 


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


412 


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


414 
\end{tabular}


415 
\end{center}


416 


417 
\subsection{A trivial example in propositional logic}


418 
\index{examples!propositional}

296

419 


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


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


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


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


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


425 
build firstorder logic.}

105

426 
\begin{ttbox}


427 
goal FOL.thy "PP > P";


428 
{\out Level 0}


429 
{\out P  P > P}


430 
{\out 1. P  P > P}


431 
\end{ttbox}


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


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


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


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


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


437 
\begin{ttbox}


438 
by (resolve_tac [impI] 1);


439 
{\out Level 1}


440 
{\out P  P > P}


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


442 
\end{ttbox}


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


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


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


446 
\begin{ttbox}


447 
by (resolve_tac [disjE] 1);


448 
{\out Level 2}


449 
{\out P  P > P}


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


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


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


453 
\end{ttbox}

296

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


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


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


457 
P}.

105

458 
\begin{ttbox}


459 
by (assume_tac 3);


460 
{\out Level 3}


461 
{\out P  P > P}


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


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


464 
\end{ttbox}

296

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

105

466 
\begin{ttbox}


467 
by (assume_tac 2);


468 
{\out Level 4}


469 
{\out P  P > P}


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


471 
\end{ttbox}


472 
Lastly we prove the remaining subgoal by assumption:


473 
\begin{ttbox}


474 
by (assume_tac 1);


475 
{\out Level 5}


476 
{\out P  P > P}


477 
{\out No subgoals!}


478 
\end{ttbox}


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


480 
complete. Calling \ttindex{result} returns the theorem.


481 
\begin{ttbox}


482 
val mythm = result();


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


484 
\end{ttbox}


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


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


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


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


489 

296

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


491 
instantiations affect the proof state.

105

492 

296

493 


494 
\subsection{Part of a distributive law}

105

495 
\index{examples!propositional}


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

296

497 
and the tactical \ttindex{REPEAT}, let us prove part of the distributive


498 
law


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

105

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


501 
\begin{ttbox}


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


503 
{\out Level 0}


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


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

296

506 
\ttbreak

105

507 
by (resolve_tac [impI] 1);


508 
{\out Level 1}


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


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


511 
\end{ttbox}


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


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


514 
state is simpler.


515 
\begin{ttbox}


516 
by (eresolve_tac [disjE] 1);


517 
{\out Level 2}


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


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


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


521 
\end{ttbox}


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


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


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


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

296

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


527 
may try out {\tt dresolve_tac}.

105

528 
\begin{ttbox}


529 
by (dresolve_tac [conjunct1] 1);


530 
{\out Level 3}


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


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


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


534 
\end{ttbox}


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


536 
\begin{ttbox}


537 
by (resolve_tac [disjI1] 1);


538 
{\out Level 4}


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


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


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


542 
\ttbreak


543 
by (resolve_tac [disjI2] 2);


544 
{\out Level 5}


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


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


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


548 
\end{ttbox}


549 
Two calls of~\ttindex{assume_tac} can finish the proof. The


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


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


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


553 
\begin{ttbox}


554 
by (REPEAT (assume_tac 1));


555 
{\out Level 6}


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


557 
{\out No subgoals!}


558 
\end{ttbox}


559 


560 


561 
\section{Quantifier reasoning}


562 
\index{quantifiers!reasoning about}\index{parameters}\index{unknowns}


563 
This section illustrates how Isabelle enforces quantifier provisos.


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


565 
function unknown and $x$ and~$z$ are parameters. This may be replaced by


566 
any term, possibly containing free occurrences of $x$ and~$z$.


567 

296

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

105

569 
\index{examples!with quantifiers}


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


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


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


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


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


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


576 
equality, and happens automatically.


577 

296

578 
\paragraph{The successful proof.}

105

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


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


581 
\begin{ttbox}


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


583 
{\out Level 0}


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


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


586 
\ttbreak


587 
by (resolve_tac [allI] 1);


588 
{\out Level 1}


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


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


591 
\end{ttbox}


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


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


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

296

595 


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

105

597 
\begin{ttbox}


598 
by (resolve_tac [exI] 1);


599 
{\out Level 2}


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


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


602 
\end{ttbox}


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


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


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


606 
subgoal with the reflexivity axiom.


607 
\begin{ttbox}


608 
by (resolve_tac [refl] 1);


609 
{\out Level 3}


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


611 
{\out No subgoals!}


612 
\end{ttbox}


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


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


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


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


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


618 

296

619 
\paragraph{The unsuccessful proof.}


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

105

621 
try~$(\exists I)$:


622 
\begin{ttbox}


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


624 
{\out Level 0}


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


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


627 
\ttbreak


628 
by (resolve_tac [exI] 1);


629 
{\out Level 1}


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


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


632 
\end{ttbox}


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


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


635 
\begin{ttbox}


636 
by (resolve_tac [allI] 1);


637 
{\out Level 2}


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


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


640 
\end{ttbox}


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


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


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


644 
\begin{ttbox}


645 
by (resolve_tac [refl] 1);


646 
{\out by: tactic returned no results}


647 
\end{ttbox}

296

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


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


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


651 
faults in the implementation.

105

652 


653 


654 
\subsection{Nested quantifiers}


655 
\index{examples!with quantifiers}

296

656 
Multiple quantifiers create complex terms. Proving


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


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


659 
the wrong order, the proof will fail.


660 

105

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


662 
and~{\tt ORELSE}.


663 
\begin{ttbox}


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


665 
{\out Level 0}


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


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


668 
\ttbreak


669 
by (resolve_tac [impI] 1);


670 
{\out Level 1}


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


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


673 
\end{ttbox}


674 

296

675 
\paragraph{The wrong approach.}

105

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


677 
\ML\ identifier \ttindex{spec}. Then we apply $(\forall I)$.


678 
\begin{ttbox}


679 
by (dresolve_tac [spec] 1);


680 
{\out Level 2}


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


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


683 
\ttbreak


684 
by (resolve_tac [allI] 1);


685 
{\out Level 3}


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


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


688 
\end{ttbox}


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

296

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

105

691 
\begin{ttbox}


692 
by (dresolve_tac [spec] 1);


693 
{\out Level 4}


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


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


696 
\ttbreak


697 
by (resolve_tac [allI] 1);


698 
{\out Level 5}


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


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


701 
\end{ttbox}


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


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


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


705 
of {\tt?y3(z)} can only contain~{\tt z}. Because of these restrictions,


706 
proof by assumption will fail.


707 
\begin{ttbox}


708 
by (assume_tac 1);


709 
{\out by: tactic returned no results}


710 
{\out uncaught exception ERROR}


711 
\end{ttbox}


712 

296

713 
\paragraph{The right approach.}

105

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


715 
Eigenvariables should be created before unknowns. The


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


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


718 
\begin{ttbox}


719 
choplev 1;


720 
{\out Level 1}


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


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


723 
\end{ttbox}

296

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

105

725 
\begin{ttbox}


726 
by (resolve_tac [allI] 1);


727 
{\out Level 2}


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


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


730 
\ttbreak


731 
by (resolve_tac [allI] 1);


732 
{\out Level 3}


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


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


735 
\end{ttbox}


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


737 
unknowns:


738 
\begin{ttbox}


739 
by (dresolve_tac [spec] 1);


740 
{\out Level 4}


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


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


743 
\ttbreak


744 
by (dresolve_tac [spec] 1);


745 
{\out Level 5}


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


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


748 
\end{ttbox}


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


750 
z} and~{\tt w}:


751 
\begin{ttbox}


752 
by (assume_tac 1);


753 
{\out Level 6}


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


755 
{\out No subgoals!}


756 
\end{ttbox}


757 

296

758 
\paragraph{A onestep proof using tacticals.}


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


760 


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


762 
attempted in an order that delays the creation of unknowns. Let us return

105

763 
to the original goal using \ttindex{choplev}:


764 
\begin{ttbox}


765 
choplev 0;


766 
{\out Level 0}


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


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


769 
\end{ttbox}

296

770 
As we have just seen, \ttindex{allI} should be attempted


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


772 
attempted first. Such priorities can easily be expressed


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

105

774 
\begin{ttbox}

296

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

105

776 
ORELSE dresolve_tac [spec] 1));


777 
{\out Level 1}


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


779 
{\out No subgoals!}


780 
\end{ttbox}


781 


782 


783 
\subsection{A realistic quantifier proof}


784 
\index{examples!with quantifiers}

296

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


786 
the equivalence


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


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

105

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


790 
use \ttindex{REPEAT}:


791 
\begin{ttbox}


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


793 
{\out Level 0}


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


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


796 
\ttbreak


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


798 
{\out Level 1}


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


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


801 
\end{ttbox}


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


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


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


805 
identifier~\ttindex{exE}.


806 
\begin{ttbox}


807 
by (eresolve_tac [exE] 1);


808 
{\out Level 2}


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


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


811 
\end{ttbox}


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


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


814 
only needed once.


815 
\begin{ttbox}


816 
by (dresolve_tac [spec] 1);


817 
{\out Level 3}


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


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


820 
\end{ttbox}

296

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


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

105

823 


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


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


826 
frequently useful.


827 
\begin{ttbox}


828 
by (eresolve_tac [mp] 1);


829 
{\out Level 4}


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


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


832 
\end{ttbox}


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


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


835 
\begin{ttbox}


836 
by (assume_tac 1);


837 
{\out Level 5}


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


839 
{\out No subgoals!}


840 
\end{ttbox}


841 


842 


843 
\subsection{The classical reasoning package}


844 
\index{classical reasoning package}


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


846 
provides enough automation to tackle substantial examples. The classical


847 
reasoning package can be set up for any classical natural deduction logic


848 
 see the {\em Reference Manual}.


849 


850 
Rules are packaged into bundles called \bfindex{classical sets}. The package


851 
provides several tactics, which apply rules using naive algorithms, using


852 
unification to handle quantifiers. The most useful tactic


853 
is~\ttindex{fast_tac}.


854 


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


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


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


858 
\begin{ttbox}


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


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


861 
{\out Level 0}


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


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


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


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


866 
\end{ttbox}


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


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


869 
\begin{ttbox}


870 
by (fast_tac FOL_cs 1);


871 
{\out Level 1}


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


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


874 
{\out No subgoals!}


875 
\end{ttbox}


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


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


878 
so let us proceed to the next example:


879 
\begin{ttbox}


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


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


882 
{\out Level 0}


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

296

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


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

105

886 
\end{ttbox}


887 
Again, subgoal~1 succumbs immediately.


888 
\begin{ttbox}


889 
by (fast_tac FOL_cs 1);


890 
{\out Level 1}


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


892 
{\out No subgoals!}


893 
\end{ttbox}


894 
The classical reasoning package is not restricted to the usual logical


895 
connectives. The natural deduction rules for unions and intersections in


896 
set theory resemble those for disjunction and conjunction, and in the


897 
infinitary case, for quantifiers. The package is valuable for reasoning in


898 
set theory.


899 


900 


901 
% Local Variables:


902 
% mode: latex


903 
% TeXmaster: t


904 
% End:
