summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Intro/getting.tex

author | wenzelm |

Mon Oct 01 21:19:50 2007 +0200 (2007-10-01) | |

changeset 24803 | 38577b4b1fde |

parent 14148 | 6580d374a509 |

child 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

Norbert Schirmer: record improvements;

1 %% $Id$

2 \part{Using Isabelle from the ML Top-Level}\label{chap:getting}

4 Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.

5 Proofs are conducted by

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

7 All syntax can be expressed using plain {\sc ascii}

8 characters, but Isabelle can support

9 alternative syntaxes, for example using mathematical symbols from a

10 special screen font. The meta-logic and main object-logics already

11 provide such fancy output as an option.

13 Object-logics are built upon Pure Isabelle, which implements the

14 meta-logic and provides certain fundamental data structures: types,

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

16 These data structures have the corresponding \ML{} types \texttt{typ},

17 \texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic};

18 tacticals have function types such as \texttt{tactic->tactic}. Isabelle

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

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

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

24 and demonstrates forward proof. The examples are set in first-order logic.

25 The command to start Isabelle running first-order logic is

26 \begin{ttbox}

27 isabelle FOL

28 \end{ttbox}

29 Note that just typing \texttt{isabelle} usually brings up higher-order logic

30 (HOL) by default.

33 \subsection{Lexical matters}

34 \index{identifiers}\index{reserved words}

35 An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)

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

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

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

39 identifiers that appear in Isabelle syntax definitions.

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

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

43 the syntax of the meta-logic.) Such symbols may be run together; thus if

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

45 valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|

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

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

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

49 symbols.

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

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

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

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

55 \index{type identifiers}

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

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

59 a non-negative integer,

60 allows the renaming of unknowns prior to unification.%

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

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

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

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

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

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

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

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

69 part of the identifier!}

72 \subsection{Syntax of types and terms}

73 \index{classes!built-in|bold}\index{syntax!of types and terms}

75 Classes are denoted by identifiers; the built-in class \cldx{logic}

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

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

79 \index{types!syntax of|bold}\index{sort constraints} Types are written

80 with a syntax like \ML's. The built-in type \tydx{prop} is the type

81 of propositions. Type variables can be constrained to particular

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

83 ord, arith\ttrbrace}.

84 \[\dquotes

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

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

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

88 \begin{array}{ll}

89 \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline

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

91 \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &

92 \hbox{sort constraint} \\

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

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

95 & \hbox{$n$-argument function type} \\

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

97 \end{array}

98 \]

99 Terms are those of the typed $\lambda$-calculus.

100 \index{terms!syntax of|bold}\index{type constraints}

101 \[\dquotes

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

103 \index{*:: symbol}

104 \begin{array}{ll}

105 \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline

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

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

108 "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\

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

110 \hbox{application to several arguments (FOL and ZF)} \\

111 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}

112 \end{array}

113 \]

114 Note that HOL uses its traditional ``higher-order'' syntax for application,

115 which differs from that used in FOL.

117 The theorems and rules of an object-logic are represented by theorems in

118 the meta-logic, which are expressed using meta-formulae. Since the

119 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}

120 are just terms of type~\texttt{prop}.

121 \index{meta-implication}

122 \index{meta-quantifiers}\index{meta-equality}

123 \index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}

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

125 \[\dquotes

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

127 \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline

128 a " == " b & a\equiv b & \hbox{meta-equality} \\

129 a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\

130 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\

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

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

133 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\

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

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

136 \end{array}

137 \]

138 Flex-flex constraints are meta-equalities arising from unification; they

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

140 \index{flex-flex constraints}

142 \index{*Trueprop constant}

143 Most logics define the implicit coercion $Trueprop$ from object-formulae to

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

145 variables $P$ and $Q$ stand for meta-formulae or object-formulae? If the

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

147 prevent such ambiguities, Isabelle's syntax does not allow a meta-formula

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

149 useful, but you can make a variable stand for a meta-formula by prefixing

150 it with the symbol \texttt{PROP}:\index{*PROP symbol}

151 \begin{ttbox}

152 PROP ?psi ==> PROP ?theta

153 \end{ttbox}

155 Symbols of object-logics are typically rendered into {\sc ascii} as

156 follows:

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

158 \tt True & $\top$ & true \\

159 \tt False & $\bot$ & false \\

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

161 \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\

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

163 \tt $P$ --> $Q$ & $P\imp Q$ & implication \\

164 \tt $P$ <-> $Q$ & $P\bimp Q$ & bi-implication \\

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

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

167 \end{tabular}

168 \]

169 To illustrate the notation, consider two axioms for first-order logic:

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

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

172 $({\conj}I)$ translates into {\sc ascii} characters as

173 \begin{ttbox}

174 [| ?P; ?Q |] ==> ?P & ?Q

175 \end{ttbox}

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

177 cluttering logic definitions with question marks, Isabelle converts any

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

179 $({\conj}I)$ as

180 \begin{ttbox}

181 [| P; Q |] ==> P & Q

182 \end{ttbox}

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

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

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

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

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

188 forth.

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

191 \begin{ttbox}

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

193 \end{ttbox}

196 \subsection{Basic operations on theorems}

197 \index{theorems!basic operations on|bold}

198 \index{LCF system}

199 Meta-level theorems have the \ML{} type \mltydx{thm}. They represent the

200 theorems and inference rules of object-logics. Isabelle's meta-logic is

201 implemented using the {\sc lcf} approach: each meta-level inference rule is

202 represented by a function from theorems to theorems. Object-level rules

203 are taken as axioms.

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

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

207 and \texttt{RSN}, which perform resolution.

209 \index{theorems!printing of}

210 \begin{ttdescription}

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

212 pretty-prints {\it thm\/} at the terminal.

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

215 pretty-prints {\it thms}, a list of theorems.

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

218 pretty-prints {\it thmq}, a sequence of theorems; this is useful for

219 inspecting the output of a tactic.

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

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

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

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

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

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

229 to have subscript zero, improving readability and reducing subscript

230 growth.

231 \end{ttdescription}

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

233 running an Isabelle session containing theory~FOL, natural deduction

234 first-order logic.\footnote{For a listing of the FOL rules and their \ML{}

235 names, turn to

236 \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%

237 {page~\pageref{fol-rules}}.}

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

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

240 itself.

241 \begin{ttbox}

242 prth mp;

243 {\out [| ?P --> ?Q; ?P |] ==> ?Q}

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

245 prth (mp RS mp);

246 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}

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

248 \end{ttbox}

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

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

251 }~\ldots{} is compiler-dependent and will sometimes be suppressed. This

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

253 top-level displays theorems as \ML{} values, enclosed in quotes. Printing

254 commands like \texttt{prth} omit the quotes and the surrounding \texttt{val

255 \ldots :\ thm}. Ignoring their side-effects, the printing commands are

256 identity functions.

258 To contrast \texttt{RS} with \texttt{RSN}, we resolve

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

260 \begin{ttbox}

261 conjunct1 RS mp;

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

263 conjunct1 RSN (2,mp);

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

265 \end{ttbox}

266 These correspond to the following proofs:

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

268 \qquad

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

270 \]

271 %

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

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

274 conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just

275 printed.

276 \begin{ttbox}

277 spec;

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

279 it RS mp;

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

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

282 it RS conjunct1;

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

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

285 standard it;

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

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

288 \end{ttbox}

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

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

291 P(x)\imp(Q(x)\conj R(x))$. Used with destruct-resolution, such specialized

292 rules provide a way of referring to particular assumptions.

293 \index{assumptions!use of}

295 \subsection{*Flex-flex constraints} \label{flexflex}

296 \index{flex-flex constraints|bold}\index{unknowns!function}

297 In higher-order unification, {\bf flex-flex} equations are those where both

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

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

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

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

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

303 procedure does not enumerate the unifiers; instead, it retains flex-flex

304 equations as constraints on future unifications. Flex-flex constraints

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

306 during use of \texttt{RS} and~\texttt{RSN}:

307 \begin{ttbox}

308 refl;

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

310 exI;

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

312 refl RS exI;

313 {\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm}

314 \end{ttbox}

315 %

316 The mysterious symbol \texttt{[.]} indicates that the result is subject to

317 a meta-level hypothesis. We can make all such hypotheses visible by setting the

318 \ttindexbold{show_hyps} flag:

319 \begin{ttbox}

320 set show_hyps;

321 {\out val it = true : bool}

322 refl RS exI;

323 {\out val it = "EX x. ?a3(x) = ?a2(x)" ["?a3(?x) =?= ?a2(?x)"] : thm}

324 \end{ttbox}

326 \noindent

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

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

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

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

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

332 \begin{ttbox}

333 prthq (flexflex_rule it);

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

335 \end{ttbox}

336 Isabelle simplifies flex-flex equations to eliminate redundant bound

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

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

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

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

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

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

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

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

346 \begin{warn}

347 \ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless

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

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

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

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

352 \begin{ttbox}

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

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

355 \end{ttbox}

357 \noindent

358 A flex-flex constraint is no longer possible; resolution does not find a

359 unique unifier:

360 \begin{ttbox}

361 reflk RS exI;

362 {\out uncaught exception}

363 {\out THM ("RSN: multiple unifiers", 1,}

364 {\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])}

365 \end{ttbox}

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

367 four resolvents:

368 \begin{ttbox}

369 [reflk] RL [exI];

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

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

372 \end{ttbox}

373 \end{warn}

375 \index{forward proof|)}

377 \section{Backward proof}

378 Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning,

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

380 conducting a backward proof using tactics.

382 \subsection{The basic tactics}

383 The tactics \texttt{assume_tac}, {\tt

384 resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most

385 single-step proofs. Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are

386 not strictly necessary, they simplify proofs involving elimination and

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

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

389 tactics try their list of theorems in left-to-right order.

391 \begin{ttdescription}

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

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

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

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

396 subgoal by assumption.

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

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

400 represent object-rules, which are resolved against subgoal~$i$ of the

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

402 conclusion with the subgoal and inserting instantiated premises in its

403 place. A rule can admit many higher-order unifiers. The tactic fails if

404 none of the rules generates next states.

406 \item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}

407 performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}}

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

409 first premise by assumption. But \texttt{eresolve_tac} additionally deletes

410 that assumption from any subgoals arising from the resolution.

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

413 \index{forward proof}\index{destruct-resolution}

414 performs destruct-resolution with the~$thms$, as described

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

416 assumptions.

417 \end{ttdescription}

419 \subsection{Commands for backward proof}

420 \index{proofs!commands for}

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

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

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

424 its many commands, most important are the following:

425 \begin{ttdescription}

426 \item[\ttindex{Goal} {\it formula}; ]

427 begins a new proof, where the {\it formula\/} is written as an \ML\ string.

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

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

431 state, raising an exception if the tactic fails.

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

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

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

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

438 \item[\ttindex{result}();]

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

440 unproved subgoals are left, etc.

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

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

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

446 \end{ttdescription}

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

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

449 shortcuts:

450 \begin{center} \tt

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

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

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

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

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

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

460 \end{tabular}

461 \end{center}

463 \subsection{A trivial example in propositional logic}

464 \index{examples!propositional}

466 Directory \texttt{FOL} of the Isabelle distribution defines the theory of

467 first-order logic. Let us try the example from \S\ref{prop-proof},

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

469 examples, see the file \texttt{FOL/ex/intro.ML}.}

470 \begin{ttbox}

471 Goal "P|P --> P";

472 {\out Level 0}

473 {\out P | P --> P}

474 {\out 1. P | P --> P}

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

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

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

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

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

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

481 \begin{ttbox}

482 by (resolve_tac [impI] 1);

483 {\out Level 1}

484 {\out P | P --> P}

485 {\out 1. P | P ==> P}

486 \end{ttbox}

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

488 (The meta-implication {\tt==>} indicates assumptions.) We apply

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

490 \begin{ttbox}

491 by (resolve_tac [disjE] 1);

492 {\out Level 2}

493 {\out P | P --> P}

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

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

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

497 \end{ttbox}

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

499 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using

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

501 P}.

502 \begin{ttbox}

503 by (assume_tac 3);

504 {\out Level 3}

505 {\out P | P --> P}

506 {\out 1. P | P ==> ?P1 | P}

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

508 \end{ttbox}

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

510 \begin{ttbox}

511 by (assume_tac 2);

512 {\out Level 4}

513 {\out P | P --> P}

514 {\out 1. P | P ==> P | P}

515 \end{ttbox}

516 Lastly we prove the remaining subgoal by assumption:

517 \begin{ttbox}

518 by (assume_tac 1);

519 {\out Level 5}

520 {\out P | P --> P}

521 {\out No subgoals!}

522 \end{ttbox}

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

524 complete. Calling \texttt{qed} stores the theorem.

525 \begin{ttbox}

526 qed "mythm";

527 {\out val mythm = "?P | ?P --> ?P" : thm}

528 \end{ttbox}

529 Isabelle has replaced the free variable~\texttt{P} by the scheme

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

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

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

534 As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how

535 instantiations affect the proof state.

538 \subsection{Part of a distributive law}

539 \index{examples!propositional}

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

541 and the tactical \texttt{REPEAT}, let us prove part of the distributive

542 law

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

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

545 \begin{ttbox}

546 Goal "(P & Q) | R --> (P | R)";

547 {\out Level 0}

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

549 {\out 1. P & Q | R --> P | R}

550 \ttbreak

551 by (resolve_tac [impI] 1);

552 {\out Level 1}

553 {\out P & Q | R --> P | R}

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

555 \end{ttbox}

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

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

558 state is simpler.

559 \begin{ttbox}

560 by (eresolve_tac [disjE] 1);

561 {\out Level 2}

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

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

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

565 \end{ttbox}

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

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

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

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

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

571 may try out \texttt{dresolve_tac}.

572 \begin{ttbox}

573 by (dresolve_tac [conjunct1] 1);

574 {\out Level 3}

575 {\out P & Q | R --> P | R}

576 {\out 1. P ==> P | R}

577 {\out 2. R ==> P | R}

578 \end{ttbox}

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

580 \begin{ttbox}

581 by (resolve_tac [disjI1] 1);

582 {\out Level 4}

583 {\out P & Q | R --> P | R}

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

585 {\out 2. R ==> P | R}

586 \ttbreak

587 by (resolve_tac [disjI2] 2);

588 {\out Level 5}

589 {\out P & Q | R --> P | R}

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

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

592 \end{ttbox}

593 Two calls of \texttt{assume_tac} can finish the proof. The

594 tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1}

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

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

597 \begin{ttbox}

598 by (REPEAT (assume_tac 1));

599 {\out Level 6}

600 {\out P & Q | R --> P | R}

601 {\out No subgoals!}

602 \end{ttbox}

605 \section{Quantifier reasoning}

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

607 This section illustrates how Isabelle enforces quantifier provisos.

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

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

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

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

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

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

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

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

617 \index{examples!with quantifiers}

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

619 attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former

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

621 variables~\cite{paulson-found}. Unification helps even in these trivial

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

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

624 equality, and happens automatically.

626 \paragraph{The successful proof.}

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

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

629 \begin{ttbox}

630 Goal "ALL x. EX y. x=y";

631 {\out Level 0}

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

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

634 \ttbreak

635 by (resolve_tac [allI] 1);

636 {\out Level 1}

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

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

639 \end{ttbox}

640 The variable~\texttt{x} is no longer universally quantified, but is a

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

642 meta-level. The subgoal must be proved for all possible values of~\texttt{x}.

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

645 \begin{ttbox}

646 by (resolve_tac [exI] 1);

647 {\out Level 2}

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

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

650 \end{ttbox}

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

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

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

654 subgoal with the reflexivity axiom.

655 \begin{ttbox}

656 by (resolve_tac [refl] 1);

657 {\out Level 3}

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

659 {\out No subgoals!}

660 \end{ttbox}

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

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

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

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

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

667 \paragraph{The unsuccessful proof.}

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

669 try~$(\exists I)$:

670 \begin{ttbox}

671 Goal "EX y. ALL x. x=y";

672 {\out Level 0}

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

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

675 \ttbreak

676 by (resolve_tac [exI] 1);

677 {\out Level 1}

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

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

680 \end{ttbox}

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

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

683 \begin{ttbox}

684 by (resolve_tac [allI] 1);

685 {\out Level 2}

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

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

688 \end{ttbox}

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

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

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

692 \begin{ttbox}

693 by (resolve_tac [refl] 1);

694 {\out by: tactic failed}

695 \end{ttbox}

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

697 first-order logic. I have elsewhere proved the faithfulness of Isabelle's

698 encoding of first-order logic~\cite{paulson-found}; there could, of course, be

699 faults in the implementation.

702 \subsection{Nested quantifiers}

703 \index{examples!with quantifiers}

704 Multiple quantifiers create complex terms. Proving

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

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

707 the wrong order, the proof will fail.

709 This section concludes with a demonstration of \texttt{REPEAT}

710 and~\texttt{ORELSE}.

711 \begin{ttbox}

712 Goal "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";

713 {\out Level 0}

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

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

716 \ttbreak

717 by (resolve_tac [impI] 1);

718 {\out Level 1}

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

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

721 \end{ttbox}

723 \paragraph{The wrong approach.}

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

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

726 \begin{ttbox}

727 by (dresolve_tac [spec] 1);

728 {\out Level 2}

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

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

731 \ttbreak

732 by (resolve_tac [allI] 1);

733 {\out Level 3}

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

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

736 \end{ttbox}

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

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

739 \begin{ttbox}

740 by (dresolve_tac [spec] 1);

741 {\out Level 4}

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

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

744 \ttbreak

745 by (resolve_tac [allI] 1);

746 {\out Level 5}

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

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

749 \end{ttbox}

750 The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each

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

752 instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances

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

754 proof by assumption will fail.

755 \begin{ttbox}

756 by (assume_tac 1);

757 {\out by: tactic failed}

758 {\out uncaught exception ERROR}

759 \end{ttbox}

761 \paragraph{The right approach.}

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

763 Parameters should be created before unknowns. The

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

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

766 \begin{ttbox}

767 choplev 1;

768 {\out Level 1}

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

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

771 \end{ttbox}

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

773 \begin{ttbox}

774 by (resolve_tac [allI] 1);

775 {\out Level 2}

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

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

778 \ttbreak

779 by (resolve_tac [allI] 1);

780 {\out Level 3}

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

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

783 \end{ttbox}

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

785 unknowns:

786 \begin{ttbox}

787 by (dresolve_tac [spec] 1);

788 {\out Level 4}

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

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

791 \ttbreak

792 by (dresolve_tac [spec] 1);

793 {\out Level 5}

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

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

796 \end{ttbox}

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

798 z} and~\texttt{w}:

799 \begin{ttbox}

800 by (assume_tac 1);

801 {\out Level 6}

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

803 {\out No subgoals!}

804 \end{ttbox}

806 \paragraph{A one-step proof using tacticals.}

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

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

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

811 \ttindex{choplev}:

812 \begin{ttbox}

813 choplev 0;

814 {\out Level 0}

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

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

817 \end{ttbox}

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

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

820 attempted first. Such priorities can easily be expressed

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

822 \begin{ttbox}

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

824 ORELSE dresolve_tac [spec] 1));

825 {\out Level 1}

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

827 {\out No subgoals!}

828 \end{ttbox}

831 \subsection{A realistic quantifier proof}

832 \index{examples!with quantifiers}

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

834 the equivalence

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

836 We state the left-to-right half to Isabelle in the normal way.

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

838 use \texttt{REPEAT}:

839 \begin{ttbox}

840 Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q";

841 {\out Level 0}

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

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

844 \ttbreak

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

846 {\out Level 1}

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

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

849 \end{ttbox}

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

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

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

853 identifier~\tdx{exE}.

854 \begin{ttbox}

855 by (eresolve_tac [exE] 1);

856 {\out Level 2}

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

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

859 \end{ttbox}

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

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

862 only needed once.

863 \begin{ttbox}

864 by (dresolve_tac [spec] 1);

865 {\out Level 3}

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

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

868 \end{ttbox}

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

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

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

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

874 frequently useful.

875 \begin{ttbox}

876 by (eresolve_tac [mp] 1);

877 {\out Level 4}

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

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

880 \end{ttbox}

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

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

883 \begin{ttbox}

884 by (assume_tac 1);

885 {\out Level 5}

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

887 {\out No subgoals!}

888 \end{ttbox}

891 \subsection{The classical reasoner}

892 \index{classical reasoner}

893 Isabelle provides enough automation to tackle substantial examples.

894 The classical

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

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

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

898 It cannot compete with fully automatic theorem provers, but it is

899 competitive with tools found in other interactive provers.

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

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

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

904 is~\ttindex{Blast_tac}.

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

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

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

909 \begin{ttbox}

910 Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback

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

912 {\out Level 0}

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

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

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

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

917 \end{ttbox}

918 \ttindex{Blast_tac} proves subgoal~1 at a stroke.

919 \begin{ttbox}

920 by (Blast_tac 1);

921 {\out Depth = 0}

922 {\out Depth = 1}

923 {\out Level 1}

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

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

926 {\out No subgoals!}

927 \end{ttbox}

928 Sceptics may examine the proof by calling the package's single-step

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

930 so let us proceed to the next example:

931 \begin{ttbox}

932 Goal "ALL x. P(x,f(x)) <-> \ttback

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

934 {\out Level 0}

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

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

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

938 \end{ttbox}

939 Again, subgoal~1 succumbs immediately.

940 \begin{ttbox}

941 by (Blast_tac 1);

942 {\out Depth = 0}

943 {\out Depth = 1}

944 {\out Level 1}

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

946 {\out No subgoals!}

947 \end{ttbox}

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

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

950 disjunction and conjunction. The rules for infinite unions and

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

952 reasoner is effective for reasoning in set theory.