author  oheimb 
Wed, 12 Nov 1997 18:58:50 +0100  
changeset 4223  f60e3d2c81d3 
parent 3485  f27a30a18a17 
child 4244  f50dace8be9f 
permissions  rwrr 
105  1 
%% $Id$ 
296  2 
\part{Getting Started with Isabelle}\label{chap:getting} 
3103  3 
Let us consider how to perform simple proofs using Isabelle. At 
4 
present, Isabelle's user interface is \ML. Proofs are conducted by 

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

6 
Basically, all syntax must be expressed using plain {\sc ascii} 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3199
diff
changeset

7 
characters. There are also mechanisms built into Isabelle that support 
3103  8 
alternative syntaxes, for example using mathematical symbols from a 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3199
diff
changeset

9 
special screen font. The metalogic and major objectlogics already 
3103  10 
provide such fancy output as an option. 
105  11 

3103  12 
Objectlogics are built upon Pure Isabelle, which implements the 
13 
metalogic and provides certain fundamental data structures: types, 

14 
terms, signatures, theorems and theories, tactics and tacticals. 

15 
These data structures have the corresponding \ML{} types {\tt typ}, 

16 
{\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic}; 

17 
tacticals have function types such as {\tt tactic>tactic}. Isabelle 

18 
users can operate on these data structures by writing \ML{} programs. 

105  19 

311  20 
\section{Forward proof}\label{sec:forward} \index{forward proof(} 
105  21 
This section describes the concrete syntax for types, terms and theorems, 
22 
and demonstrates forward proof. 

23 

24 
\subsection{Lexical matters} 

311  25 
\index{identifiers}\index{reserved words} 
105  26 
An {\bf identifier} is a string of letters, digits, underscores~(\verb_) 
27 
and single quotes~({\tt'}), beginning with a letter. Single quotes are 

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

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

30 
identifiers that appear in Isabelle syntax definitions. 

31 

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

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

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

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

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

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

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

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

296  40 
symbols. 
105  41 

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

331  43 
constants. A {\bf type identifier} consists of an identifier prefixed by a 
44 
prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand 

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

46 
\index{type identifiers} 

47 

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

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

50 
a nonnegative integer, 

51 
allows the renaming of unknowns prior to unification.% 

296  52 
\footnote{The subscript may appear after the identifier, separated by a 
53 
dot; this prevents ambiguity when the identifier ends with a digit. Thus 

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

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

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

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

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

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

60 
part of the identifier!} 

105  61 

62 

63 
\subsection{Syntax of types and terms} 

311  64 
\index{classes!builtinbold}\index{syntax!of types and terms} 
65 

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

105  67 
contains the `logical' types. Sorts are lists of classes enclosed in 
296  68 
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. 
105  69 

3103  70 
\index{types!syntax ofbold}\index{sort constraints} Types are written 
71 
with a syntax like \ML's. The builtin type \tydx{prop} is the type 

72 
of propositions. Type variables can be constrained to particular 

73 
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace 

74 
ord, arith\ttrbrace}. 

105  75 
\[\dquotes 
311  76 
\index{*:: symbol}\index{*=> symbol} 
77 
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} 

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

105  79 
\begin{array}{lll} 
80 
\multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline 

331  81 
\alpha "::" C & \alpha :: C & \hbox{class constraint} \\ 
3103  82 
\alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & 
331  83 
\alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ 
84 
\sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\ 

105  85 
"[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & 
86 
[\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\ 

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

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

89 
\end{array} 

90 
\] 

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

331  92 
\index{terms!syntax ofbold}\index{type constraints} 
105  93 
\[\dquotes 
311  94 
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$abstractions} 
95 
\index{*:: symbol} 

105  96 
\begin{array}{lll} 
97 
\multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline 

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

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

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

101 
\hbox{curried abstraction} \\ 

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

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

104 
\end{array} 

105 
\] 

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

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

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

311  109 
are just terms of type~{\tt prop}. 
110 
\index{metaimplication} 

111 
\index{metaquantifiers}\index{metaequality} 

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

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

105  114 
\[\dquotes 
115 
\begin{array}{l@{\quad}l@{\quad}l} 

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

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

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

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

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

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

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

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

3103  124 
\Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} 
105  125 
\end{array} 
126 
\] 

127 
Flexflex constraints are metaequalities arising from unification; they 

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

311  129 
\index{flexflex constraints} 
105  130 

311  131 
\index{*Trueprop constant} 
105  132 
Most logics define the implicit coercion $Trueprop$ from objectformulae to 
311  133 
propositions. This could cause an ambiguity: in $P\Imp Q$, do the 
134 
variables $P$ and $Q$ stand for metaformulae or objectformulae? If the 

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

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

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

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

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

105  140 
\begin{ttbox} 
141 
PROP ?psi ==> PROP ?theta 

142 
\end{ttbox} 

143 

3103  144 
Symbols of objectlogics are typically rendered into {\sc ascii} as 
145 
follows: 

105  146 
\[ \begin{tabular}{l@{\quad}l@{\quad}l} 
147 
\tt True & $\top$ & true \\ 

148 
\tt False & $\bot$ & false \\ 

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

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

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

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

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

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

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

156 
\end{tabular} 

157 
\] 

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

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

3103  160 
$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ 
161 
$({\conj}I)$ translates into {\sc ascii} characters as 

105  162 
\begin{ttbox} 
163 
[ ?P; ?Q ] ==> ?P & ?Q 

164 
\end{ttbox} 

296  165 
The schematic variables let unification instantiate the rule. To avoid 
166 
cluttering logic definitions with question marks, Isabelle converts any 

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

168 
$({\conj}I)$ as 

105  169 
\begin{ttbox} 
170 
[ P; Q ] ==> P & Q 

171 
\end{ttbox} 

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

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

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

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

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

177 
forth. 

178 

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

180 
\begin{ttbox} 

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

182 
\end{ttbox} 

183 

184 

185 
\subsection{Basic operations on theorems} 

186 
\index{theorems!basic operations onbold} 

311  187 
\index{LCF system} 
331  188 
Metalevel theorems have the \ML{} type \mltydx{thm}. They represent the 
189 
theorems and inference rules of objectlogics. Isabelle's metalogic is 

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

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

192 
are taken as axioms. 

105  193 

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

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

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

197 

311  198 
\index{theorems!printing of} 
199 
\begin{ttdescription} 

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

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

105  202 

311  203 
\item[\ttindex{prths} {\it thms};] 
204 
prettyprints {\it thms}, a list of theorems. 

105  205 

311  206 
\item[\ttindex{prthq} {\it thmq};] 
207 
prettyprints {\it thmq}, a sequence of theorems; this is useful for 

208 
inspecting the output of a tactic. 

105  209 

311  210 
\item[$thm1$ RS $thm2$] \index{*RS} 
211 
resolves the conclusion of $thm1$ with the first premise of~$thm2$. 

105  212 

311  213 
\item[$thm1$ RSN $(i,thm2)$] \index{*RSN} 
214 
resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$. 

105  215 

311  216 
\item[\ttindex{standard} $thm$] 
217 
puts $thm$ into a standard format. It also renames schematic variables 

218 
to have subscript zero, improving readability and reducing subscript 

219 
growth. 

220 
\end{ttdescription} 

105  221 
The rules of a theory are normally bound to \ML\ identifiers. Suppose we 
331  222 
are running an Isabelle session containing theory~\FOL, natural deduction 
223 
firstorder logic.\footnote{For a listing of the \FOL{} rules and their 

224 
\ML{} names, turn to 

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

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

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

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

229 
itself. 

105  230 
\begin{ttbox} 
231 
prth mp; 

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

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

234 
prth (mp RS mp); 

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

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

237 
\end{ttbox} 

331  238 
User input appears in {\footnotesize\tt typewriter characters}, and output 
239 
appears in {\sltt slanted typewriter characters}. \ML's response {\out val 

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

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

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

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

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

245 
functions. 

105  246 

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

311  248 
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. 
105  249 
\begin{ttbox} 
250 
conjunct1 RS mp; 

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

252 
conjunct1 RSN (2,mp); 

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

254 
\end{ttbox} 

255 
These correspond to the following proofs: 

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

257 
\qquad 

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

259 
\] 

296  260 
% 
261 
Rules can be derived by pasting other rules together. Let us join 

311  262 
\tdx{spec}, which stands for~$(\forall E)$, with {\tt mp} and {\tt 
296  263 
conjunct1}. In \ML{}, the identifier~{\tt it} denotes the value just 
264 
printed. 

105  265 
\begin{ttbox} 
266 
spec; 

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

268 
it RS mp; 

296  269 
{\out val it = "[ ALL x. ?P3(x) > ?Q2(x); ?P3(?x1) ] ==>} 
270 
{\out ?Q2(?x1)" : thm} 

105  271 
it RS conjunct1; 
296  272 
{\out val it = "[ ALL x. ?P4(x) > ?P6(x) & ?Q5(x); ?P4(?x2) ] ==>} 
273 
{\out ?P6(?x2)" : thm} 

105  274 
standard it; 
296  275 
{\out val it = "[ ALL x. ?P(x) > ?Pa(x) & ?Q(x); ?P(?x) ] ==>} 
276 
{\out ?Pa(?x)" : thm} 

105  277 
\end{ttbox} 
278 
By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have 

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

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

281 
rules provide a way of referring to particular assumptions. 

311  282 
\index{assumptions!use of} 
105  283 

311  284 
\subsection{*Flexflex constraints} \label{flexflex} 
285 
\index{flexflex constraintsbold}\index{unknowns!function} 

105  286 
In higherorder unification, {\bf flexflex} equations are those where both 
287 
sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$. 

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

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

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

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

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

293 
equations as constraints on future unifications. Flexflex constraints 

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

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

296 
\begin{ttbox} 

297 
refl; 

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

299 
exI; 

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

301 
refl RS exI; 

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

303 
\end{ttbox} 

304 

305 
\noindent 

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

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

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

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

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

311 
\begin{ttbox} 

312 
prthq (flexflex_rule it); 

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

314 
\end{ttbox} 

315 
Isabelle simplifies flexflex equations to eliminate redundant bound 

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

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

296  318 
none on the left in a common instance of these terms. Choosing a new 
105  319 
variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$, 
320 
simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$ 

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

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

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

324 

325 
\begin{warn} 

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

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

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

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

311  330 
of \tdx{refl} containing no schematic variables. 
105  331 
\begin{ttbox} 
332 
val reflk = read_instantiate [("a","k")] refl; 

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

334 
\end{ttbox} 

335 

336 
\noindent 

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

338 
unique unifier: 

339 
\begin{ttbox} 

340 
reflk RS exI; 

341 
{\out uncaught exception THM} 

342 
\end{ttbox} 

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

344 
four resolvents: 

345 
\begin{ttbox} 

346 
[reflk] RL [exI]; 

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

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

349 
\end{ttbox} 

350 
\end{warn} 

351 

311  352 
\index{forward proof)} 
105  353 

354 
\section{Backward proof} 

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

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

357 
conducting a backward proof using tactics. 

358 

359 
\subsection{The basic tactics} 

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

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

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

363 
not strictly necessary, they simplify proofs involving elimination and 

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

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

366 
tactics try their list of theorems in lefttoright order. 

367 

311  368 
\begin{ttdescription} 
369 
\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption} 

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

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

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

373 
subgoal by assumption. 

105  374 

311  375 
\item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution} 
376 
is the basic resolution tactic, used for most proof steps. The $thms$ 

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

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

379 
conclusion with the subgoal and inserting instantiated premises in its 

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

381 
none of the rules generates next states. 

105  382 

311  383 
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elimresolution} 
384 
performs elimresolution. Like {\tt resolve_tac~{\it thms}~{\it i\/}} 

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

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

387 
that assumption from any subgoals arising from the resolution. 

105  388 

311  389 
\item[\ttindex{dresolve_tac} {\it thms} {\it i}] 
390 
\index{forward proof}\index{destructresolution} 

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

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

393 
assumptions. 

394 
\end{ttdescription} 

105  395 

396 
\subsection{Commands for backward proof} 

311  397 
\index{proofs!commands for} 
105  398 
Tactics are normally applied using the subgoal module, which maintains a 
399 
proof state and manages the proof construction. It allows interactive 

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

401 
its many commands, most important are the following: 

311  402 
\begin{ttdescription} 
403 
\item[\ttindex{goal} {\it theory} {\it formula}; ] 

105  404 
begins a new proof, where $theory$ is usually an \ML\ identifier 
405 
and the {\it formula\/} is written as an \ML\ string. 

406 

311  407 
\item[\ttindex{by} {\it tactic}; ] 
105  408 
applies the {\it tactic\/} to the current proof 
409 
state, raising an exception if the tactic fails. 

410 

3103  411 
\item[\ttindex{undo}(); ] 
296  412 
reverts to the previous proof state. Undo can be repeated but cannot be 
413 
undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely 

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

105  415 

3103  416 
\item[\ttindex{result}();] 
105  417 
returns the theorem just proved, in a standard format. It fails if 
296  418 
unproved subgoals are left, etc. 
3103  419 

420 
\item[\ttindex{qed} {\it name};] is the usual way of ending a proof. 

421 
It gets the theorem using {\tt result}, stores it in Isabelle's 

422 
theorem database and binds it to an \ML{} identifier. 

423 

311  424 
\end{ttdescription} 
105  425 
The commands and tactics given above are cumbersome for interactive use. 
426 
Although our examples will use the full commands, you may prefer Isabelle's 

427 
shortcuts: 

428 
\begin{center} \tt 

311  429 
\index{*br} \index{*be} \index{*bd} \index{*ba} 
105  430 
\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l} 
431 
ba {\it i}; & by (assume_tac {\it i}); \\ 

432 

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

434 

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

436 

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

438 
\end{tabular} 

439 
\end{center} 

440 

441 
\subsection{A trivial example in propositional logic} 

442 
\index{examples!propositional} 

296  443 

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

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

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

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

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

449 
build firstorder logic.} 

105  450 
\begin{ttbox} 
451 
goal FOL.thy "PP > P"; 

452 
{\out Level 0} 

453 
{\out P  P > P} 

454 
{\out 1. P  P > P} 

311  455 
\end{ttbox}\index{level of a proof} 
105  456 
Isabelle responds by printing the initial proof state, which has $P\disj 
311  457 
P\imp P$ as the main goal and the only subgoal. The {\bf level} of the 
105  458 
state is the number of {\tt by} commands that have been applied to reach 
311  459 
it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, 
105  460 
or~$({\imp}I)$, to subgoal~1: 
461 
\begin{ttbox} 

462 
by (resolve_tac [impI] 1); 

463 
{\out Level 1} 

464 
{\out P  P > P} 

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

466 
\end{ttbox} 

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

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

311  469 
\tdx{disjE}, or~(${\disj}E)$, to that subgoal: 
105  470 
\begin{ttbox} 
471 
by (resolve_tac [disjE] 1); 

472 
{\out Level 2} 

473 
{\out P  P > P} 

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

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

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

477 
\end{ttbox} 

296  478 
At Level~2 there are three subgoals, each provable by assumption. We 
479 
deviate from~\S\ref{propproof} by tackling subgoal~3 first, using 

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

481 
P}. 

105  482 
\begin{ttbox} 
483 
by (assume_tac 3); 

484 
{\out Level 3} 

485 
{\out P  P > P} 

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

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

488 
\end{ttbox} 

296  489 
Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P} in subgoal~1. 
105  490 
\begin{ttbox} 
491 
by (assume_tac 2); 

492 
{\out Level 4} 

493 
{\out P  P > P} 

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

495 
\end{ttbox} 

496 
Lastly we prove the remaining subgoal by assumption: 

497 
\begin{ttbox} 

498 
by (assume_tac 1); 

499 
{\out Level 5} 

500 
{\out P  P > P} 

501 
{\out No subgoals!} 

502 
\end{ttbox} 

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

3103  504 
complete. Calling {\tt qed} stores the theorem. 
105  505 
\begin{ttbox} 
3103  506 
qed "mythm"; 
105  507 
{\out val mythm = "?P  ?P > ?P" : thm} 
508 
\end{ttbox} 

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

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

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

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

513 

296  514 
As an exercise, try doing the proof as in \S\ref{propproof}, observing how 
515 
instantiations affect the proof state. 

105  516 

296  517 

518 
\subsection{Part of a distributive law} 

105  519 
\index{examples!propositional} 
520 
To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} 

311  521 
and the tactical {\tt REPEAT}, let us prove part of the distributive 
296  522 
law 
523 
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] 

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

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

527 
{\out Level 0} 

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

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

296  530 
\ttbreak 
105  531 
by (resolve_tac [impI] 1); 
532 
{\out Level 1} 

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

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

535 
\end{ttbox} 

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

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

538 
state is simpler. 

539 
\begin{ttbox} 

540 
by (eresolve_tac [disjE] 1); 

541 
{\out Level 2} 

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

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

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

545 
\end{ttbox} 

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

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

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

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

296  550 
assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we 
551 
may try out {\tt dresolve_tac}. 

105  552 
\begin{ttbox} 
553 
by (dresolve_tac [conjunct1] 1); 

554 
{\out Level 3} 

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

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

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

558 
\end{ttbox} 

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

560 
\begin{ttbox} 

561 
by (resolve_tac [disjI1] 1); 

562 
{\out Level 4} 

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

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

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

566 
\ttbreak 

567 
by (resolve_tac [disjI2] 2); 

568 
{\out Level 5} 

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

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

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

572 
\end{ttbox} 

311  573 
Two calls of {\tt assume_tac} can finish the proof. The 
574 
tactical~\ttindex{REPEAT} here expresses a tactic that calls {\tt assume_tac~1} 

105  575 
as many times as possible. We can restrict attention to subgoal~1 because 
576 
the other subgoals move up after subgoal~1 disappears. 

577 
\begin{ttbox} 

578 
by (REPEAT (assume_tac 1)); 

579 
{\out Level 6} 

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

581 
{\out No subgoals!} 

582 
\end{ttbox} 

583 

584 

585 
\section{Quantifier reasoning} 

331  586 
\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function} 
105  587 
This section illustrates how Isabelle enforces quantifier provisos. 
331  588 
Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier 
589 
rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function 

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

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

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

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

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

105  595 

296  596 
\subsection{Two quantifier proofs: a success and a failure} 
105  597 
\index{examples!with quantifiers} 
598 
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an 

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

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

1878  601 
variables~\cite{paulsonfound}. Unification helps even in these trivial 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3199
diff
changeset

602 
proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3199
diff
changeset

603 
but we need never say so. This choice is forced by the reflexive law for 
105  604 
equality, and happens automatically. 
605 

296  606 
\paragraph{The successful proof.} 
105  607 
The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules 
608 
$(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: 

609 
\begin{ttbox} 

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

611 
{\out Level 0} 

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

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

614 
\ttbreak 

615 
by (resolve_tac [allI] 1); 

616 
{\out Level 1} 

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

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

619 
\end{ttbox} 

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

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

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

296  623 

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

105  625 
\begin{ttbox} 
626 
by (resolve_tac [exI] 1); 

627 
{\out Level 2} 

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

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

630 
\end{ttbox} 

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

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

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

634 
subgoal with the reflexivity axiom. 

635 
\begin{ttbox} 

636 
by (resolve_tac [refl] 1); 

637 
{\out Level 3} 

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

639 
{\out No subgoals!} 

640 
\end{ttbox} 

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

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

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

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

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

646 

296  647 
\paragraph{The unsuccessful proof.} 
648 
We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and 

105  649 
try~$(\exists I)$: 
650 
\begin{ttbox} 

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

652 
{\out Level 0} 

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

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

655 
\ttbreak 

656 
by (resolve_tac [exI] 1); 

657 
{\out Level 1} 

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

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

660 
\end{ttbox} 

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

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

663 
\begin{ttbox} 

664 
by (resolve_tac [allI] 1); 

665 
{\out Level 2} 

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

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

668 
\end{ttbox} 

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

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

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

672 
\begin{ttbox} 

673 
by (resolve_tac [refl] 1); 

3103  674 
{\out by: tactic failed} 
105  675 
\end{ttbox} 
296  676 
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of 
677 
firstorder logic. I have elsewhere proved the faithfulness of Isabelle's 

1878  678 
encoding of firstorder logic~\cite{paulsonfound}; there could, of course, be 
296  679 
faults in the implementation. 
105  680 

681 

682 
\subsection{Nested quantifiers} 

683 
\index{examples!with quantifiers} 

296  684 
Multiple quantifiers create complex terms. Proving 
685 
\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] 

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

687 
the wrong order, the proof will fail. 

688 

105  689 
This section concludes with a demonstration of {\tt REPEAT} 
690 
and~{\tt ORELSE}. 

691 
\begin{ttbox} 

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

693 
{\out Level 0} 

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

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

696 
\ttbreak 

697 
by (resolve_tac [impI] 1); 

698 
{\out Level 1} 

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

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

701 
\end{ttbox} 

702 

296  703 
\paragraph{The wrong approach.} 
311  704 
Using {\tt dresolve_tac}, we apply the rule $(\forall E)$, bound to the 
705 
\ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. 

105  706 
\begin{ttbox} 
707 
by (dresolve_tac [spec] 1); 

708 
{\out Level 2} 

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

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

711 
\ttbreak 

712 
by (resolve_tac [allI] 1); 

713 
{\out Level 3} 

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

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

716 
\end{ttbox} 

311  717 
The unknown {\tt ?x1} and the parameter {\tt z} have appeared. We again 
296  718 
apply $(\forall E)$ and~$(\forall I)$. 
105  719 
\begin{ttbox} 
720 
by (dresolve_tac [spec] 1); 

721 
{\out Level 4} 

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

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

724 
\ttbreak 

725 
by (resolve_tac [allI] 1); 

726 
{\out Level 5} 

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

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

729 
\end{ttbox} 

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

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

311  732 
instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances 
733 
of {\tt?y3(z)} can only contain~{\tt z}. Due to the restriction on~{\tt ?x1}, 

105  734 
proof by assumption will fail. 
735 
\begin{ttbox} 

736 
by (assume_tac 1); 

3103  737 
{\out by: tactic failed} 
105  738 
{\out uncaught exception ERROR} 
739 
\end{ttbox} 

740 

296  741 
\paragraph{The right approach.} 
105  742 
To do this proof, the rules must be applied in the correct order. 
331  743 
Parameters should be created before unknowns. The 
105  744 
\ttindex{choplev} command returns to an earlier stage of the proof; 
745 
let us return to the result of applying~$({\imp}I)$: 

746 
\begin{ttbox} 

747 
choplev 1; 

748 
{\out Level 1} 

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

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

751 
\end{ttbox} 

296  752 
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$. 
105  753 
\begin{ttbox} 
754 
by (resolve_tac [allI] 1); 

755 
{\out Level 2} 

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

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

758 
\ttbreak 

759 
by (resolve_tac [allI] 1); 

760 
{\out Level 3} 

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

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

763 
\end{ttbox} 

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

765 
unknowns: 

766 
\begin{ttbox} 

767 
by (dresolve_tac [spec] 1); 

768 
{\out Level 4} 

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

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

771 
\ttbreak 

772 
by (dresolve_tac [spec] 1); 

773 
{\out Level 5} 

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

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

776 
\end{ttbox} 

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

778 
z} and~{\tt w}: 

779 
\begin{ttbox} 

780 
by (assume_tac 1); 

781 
{\out Level 6} 

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

783 
{\out No subgoals!} 

784 
\end{ttbox} 

785 

296  786 
\paragraph{A onestep proof using tacticals.} 
787 
\index{tacticals} \index{examples!of tacticals} 

788 

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

331  790 
attempted in the correct order. Let us return to the original goal using 
791 
\ttindex{choplev}: 

105  792 
\begin{ttbox} 
793 
choplev 0; 

794 
{\out Level 0} 

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

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

797 
\end{ttbox} 

311  798 
As we have just seen, \tdx{allI} should be attempted 
799 
before~\tdx{spec}, while \ttindex{assume_tac} generally can be 

296  800 
attempted first. Such priorities can easily be expressed 
801 
using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. 

105  802 
\begin{ttbox} 
296  803 
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 
105  804 
ORELSE dresolve_tac [spec] 1)); 
805 
{\out Level 1} 

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

807 
{\out No subgoals!} 

808 
\end{ttbox} 

809 

810 

811 
\subsection{A realistic quantifier proof} 

812 
\index{examples!with quantifiers} 

296  813 
To see the practical use of parameters and unknowns, let us prove half of 
814 
the equivalence 

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

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

105  817 
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we 
311  818 
use {\tt REPEAT}: 
105  819 
\begin{ttbox} 
820 
goal FOL.thy "(ALL x.P(x) > Q) > (EX x.P(x)) > Q"; 

821 
{\out Level 0} 

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

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

824 
\ttbreak 

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

826 
{\out Level 1} 

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

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

829 
\end{ttbox} 

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

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

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

311  833 
identifier~\tdx{exE}. 
105  834 
\begin{ttbox} 
835 
by (eresolve_tac [exE] 1); 

836 
{\out Level 2} 

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

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

839 
\end{ttbox} 

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

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

842 
only needed once. 

843 
\begin{ttbox} 

844 
by (dresolve_tac [spec] 1); 

845 
{\out Level 3} 

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

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

848 
\end{ttbox} 

296  849 
Because we applied $(\exists E)$ before $(\forall E)$, the unknown 
850 
term~{\tt?x3(x)} may depend upon the parameter~{\tt x}. 

105  851 

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

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

854 
frequently useful. 

855 
\begin{ttbox} 

856 
by (eresolve_tac [mp] 1); 

857 
{\out Level 4} 

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

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

860 
\end{ttbox} 

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

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

863 
\begin{ttbox} 

864 
by (assume_tac 1); 

865 
{\out Level 5} 

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

867 
{\out No subgoals!} 

868 
\end{ttbox} 

869 

870 

311  871 
\subsection{The classical reasoner} 
872 
\index{classical reasoner} 

105  873 
Although Isabelle cannot compete with fully automatic theorem provers, it 
874 
provides enough automation to tackle substantial examples. The classical 

331  875 
reasoner can be set up for any classical natural deduction logic; 
876 
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 

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

105  878 

331  879 
Rules are packaged into {\bf classical sets}. The classical reasoner 
880 
provides several tactics, which apply rules using naive algorithms. 

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

3127  882 
is~\ttindex{Blast_tac}. 
105  883 

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

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

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

887 
\begin{ttbox} 

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

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

890 
{\out Level 0} 

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

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

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

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

895 
\end{ttbox} 

3127  896 
\ttindex{Blast_tac} proves subgoal~1 at a stroke. 
105  897 
\begin{ttbox} 
3127  898 
by (Blast_tac 1); 
899 
{\out Depth = 0} 

900 
{\out Depth = 1} 

105  901 
{\out Level 1} 
902 
{\out (EX y. ALL x. J(y,x) <> ~J(x,x)) >} 

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

904 
{\out No subgoals!} 

905 
\end{ttbox} 

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

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

908 
so let us proceed to the next example: 

909 
\begin{ttbox} 

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

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

912 
{\out Level 0} 

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

296  914 
{\out 1. ALL x. P(x,f(x)) <>} 
915 
{\out (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))} 

105  916 
\end{ttbox} 
917 
Again, subgoal~1 succumbs immediately. 

918 
\begin{ttbox} 

3127  919 
by (Blast_tac 1); 
920 
{\out Depth = 0} 

921 
{\out Depth = 1} 

105  922 
{\out Level 1} 
923 
{\out ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))} 

924 
{\out No subgoals!} 

925 
\end{ttbox} 

331  926 
The classical reasoner is not restricted to the usual logical connectives. 
927 
The natural deduction rules for unions and intersections resemble those for 

928 
disjunction and conjunction. The rules for infinite unions and 

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

930 
reasoner is effective for reasoning in set theory. 

931 