author  wenzelm 
Fri, 16 Jul 1999 22:24:42 +0200  
changeset 7024  44bd3c094fd6 
parent 5205  602354039306 
child 9695  ec7d7f877712 
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. 

5205  15 
These data structures have the corresponding \ML{} types \texttt{typ}, 
16 
\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic}; 

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

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

4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

20 

311  21 
\section{Forward proof}\label{sec:forward} \index{forward proof(} 
105  22 
This section describes the concrete syntax for types, terms and theorems, 
4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

23 
and demonstrates forward proof. The examples are set in firstorder logic. 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

24 
The command to start Isabelle running firstorder logic is 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

25 
\begin{ttbox} 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

26 
isabelle FOL 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

27 
\end{ttbox} 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

28 
Note that just typing \texttt{isabelle} usually brings up higherorder logic 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

29 
(\HOL) by default. 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

30 

105  31 

32 
\subsection{Lexical matters} 

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

5205  36 
regarded as primes; for instance \texttt{x'} is read as~$x'$. Identifiers are 
105  37 
separated by white space and special characters. {\bf Reserved words} are 
38 
identifiers that appear in Isabelle syntax definitions. 

39 

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

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

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

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

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

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

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

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

296  48 
symbols. 
105  49 

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

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

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

54 
\index{type identifiers} 

55 

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

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

58 
a nonnegative integer, 

59 
allows the renaming of unknowns prior to unification.% 

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

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

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

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

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

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

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

68 
part of the identifier!} 

105  69 

70 

71 
\subsection{Syntax of types and terms} 

311  72 
\index{classes!builtinbold}\index{syntax!of types and terms} 
73 

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

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

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

80 
of propositions. Type variables can be constrained to particular 

5205  81 
classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace 
3103  82 
ord, arith\ttrbrace}. 
105  83 
\[\dquotes 
311  84 
\index{*:: symbol}\index{*=> symbol} 
85 
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} 

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

4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

87 
\begin{array}{ll} 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

88 
\multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

89 
\alpha "::" C & \hbox{class constraint} \\ 
3103  90 
\alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & 
4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

91 
\hbox{sort constraint} \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

92 
\sigma " => " \tau & \hbox{function type } \sigma\To\tau \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

93 
"[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

94 
& \hbox{$n$argument function type} \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

95 
"(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction} 
105  96 
\end{array} 
97 
\] 

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

331  99 
\index{terms!syntax ofbold}\index{type constraints} 
105  100 
\[\dquotes 
311  101 
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$abstractions} 
102 
\index{*:: symbol} 

4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

103 
\begin{array}{ll} 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

104 
\multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

105 
t "::" \sigma & \hbox{type constraint} \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

106 
"\%" x "." t & \hbox{abstraction } \lambda x.t \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

107 
"\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

108 
t "(" u@1"," \ldots "," u@n ")" & 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

109 
\hbox{application to several arguments (FOL and ZF)} \\ 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

110 
t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)} 
105  111 
\end{array} 
112 
\] 

4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

113 
Note that \HOL{} uses its traditional ``higherorder'' syntax for application, 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

114 
which differs from that used in \FOL\@. 
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

115 

105  116 
The theorems and rules of an objectlogic are represented by theorems in 
117 
the metalogic, which are expressed using metaformulae. Since the 

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

5205  119 
are just terms of type~\texttt{prop}. 
311  120 
\index{metaimplication} 
121 
\index{metaquantifiers}\index{metaequality} 

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

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

105  124 
\[\dquotes 
125 
\begin{array}{l@{\quad}l@{\quad}l} 

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

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

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

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

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

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

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

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

3103  134 
\Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} 
105  135 
\end{array} 
136 
\] 

137 
Flexflex constraints are metaequalities arising from unification; they 

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

311  139 
\index{flexflex constraints} 
105  140 

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

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

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

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

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

5205  149 
it with the symbol \texttt{PROP}:\index{*PROP symbol} 
105  150 
\begin{ttbox} 
151 
PROP ?psi ==> PROP ?theta 

152 
\end{ttbox} 

153 

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

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

158 
\tt False & $\bot$ & false \\ 

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

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

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

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

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

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

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

166 
\end{tabular} 

167 
\] 

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

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

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

105  172 
\begin{ttbox} 
173 
[ ?P; ?Q ] ==> ?P & ?Q 

174 
\end{ttbox} 

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

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

178 
$({\conj}I)$ as 

105  179 
\begin{ttbox} 
180 
[ P; Q ] ==> P & Q 

181 
\end{ttbox} 

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

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

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

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

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

187 
forth. 

188 

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

190 
\begin{ttbox} 

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

192 
\end{ttbox} 

193 

194 

195 
\subsection{Basic operations on theorems} 

196 
\index{theorems!basic operations onbold} 

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

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

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

202 
are taken as axioms. 

105  203 

5205  204 
The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt 
205 
prthq}. Of the other operations on theorems, most useful are \texttt{RS} 

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

105  207 

311  208 
\index{theorems!printing of} 
209 
\begin{ttdescription} 

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

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

105  212 

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

105  215 

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

218 
inspecting the output of a tactic. 

105  219 

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

105  222 

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

105  225 

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

228 
to have subscript zero, improving readability and reducing subscript 

229 
growth. 

230 
\end{ttdescription} 

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

234 
\ML{} names, turn to 

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

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

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

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

239 
itself. 

105  240 
\begin{ttbox} 
241 
prth mp; 

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

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

244 
prth (mp RS mp); 

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

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

247 
\end{ttbox} 

331  248 
User input appears in {\footnotesize\tt typewriter characters}, and output 
4244  249 
appears in{\out slanted typewriter characters}. \ML's response {\out val 
331  250 
}~\ldots{} is compilerdependent and will sometimes be suppressed. This 
251 
session illustrates two formats for the display of theorems. Isabelle's 

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

5205  253 
commands like \texttt{prth} omit the quotes and the surrounding \texttt{val 
331  254 
\ldots :\ thm}. Ignoring their sideeffects, the commands are identity 
255 
functions. 

105  256 

5205  257 
To contrast \texttt{RS} with \texttt{RSN}, we resolve 
311  258 
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. 
105  259 
\begin{ttbox} 
260 
conjunct1 RS mp; 

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

262 
conjunct1 RSN (2,mp); 

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

264 
\end{ttbox} 

265 
These correspond to the following proofs: 

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

267 
\qquad 

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

269 
\] 

296  270 
% 
271 
Rules can be derived by pasting other rules together. Let us join 

5205  272 
\tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt 
273 
conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just 

296  274 
printed. 
105  275 
\begin{ttbox} 
276 
spec; 

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

278 
it RS mp; 

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

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

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

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

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

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

291 
rules provide a way of referring to particular assumptions. 

311  292 
\index{assumptions!use of} 
105  293 

311  294 
\subsection{*Flexflex constraints} \label{flexflex} 
295 
\index{flexflex constraintsbold}\index{unknowns!function} 

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

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

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

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

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

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

303 
equations as constraints on future unifications. Flexflex constraints 

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

5205  305 
during use of \texttt{RS} and~\texttt{RSN}: 
105  306 
\begin{ttbox} 
307 
refl; 

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

309 
exI; 

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

311 
refl RS exI; 

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

313 
\end{ttbox} 

314 

315 
\noindent 

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

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

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

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

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

321 
\begin{ttbox} 

322 
prthq (flexflex_rule it); 

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

324 
\end{ttbox} 

325 
Isabelle simplifies flexflex equations to eliminate redundant bound 

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

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

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

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

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

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

334 

335 
\begin{warn} 

5205  336 
\ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless 
105  337 
the resolution delivers {\bf exactly one} resolvent. For multiple results, 
338 
use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The 

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

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

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

344 
\end{ttbox} 

345 

346 
\noindent 

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

348 
unique unifier: 

349 
\begin{ttbox} 

350 
reflk RS exI; 

351 
{\out uncaught exception THM} 

352 
\end{ttbox} 

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

354 
four resolvents: 

355 
\begin{ttbox} 

356 
[reflk] RL [exI]; 

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

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

359 
\end{ttbox} 

360 
\end{warn} 

361 

311  362 
\index{forward proof)} 
105  363 

364 
\section{Backward proof} 

5205  365 
Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning, 
105  366 
large proofs require tactics. Isabelle provides a suite of commands for 
367 
conducting a backward proof using tactics. 

368 

369 
\subsection{The basic tactics} 

5205  370 
The tactics \texttt{assume_tac}, {\tt 
371 
resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most 

372 
singlestep proofs. Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are 

105  373 
not strictly necessary, they simplify proofs involving elimination and 
374 
destruction rules. All the tactics act on a subgoal designated by a 

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

376 
tactics try their list of theorems in lefttoright order. 

377 

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

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

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

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

383 
subgoal by assumption. 

105  384 

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

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

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

389 
conclusion with the subgoal and inserting instantiated premises in its 

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

391 
none of the rules generates next states. 

105  392 

311  393 
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elimresolution} 
5205  394 
performs elimresolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}} 
395 
followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its 

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

311  397 
that assumption from any subgoals arising from the resolution. 
105  398 

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

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

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

403 
assumptions. 

404 
\end{ttdescription} 

105  405 

406 
\subsection{Commands for backward proof} 

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

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

411 
its many commands, most important are the following: 

311  412 
\begin{ttdescription} 
5205  413 
\item[\ttindex{Goal} {\it formula}; ] 
105  414 
begins a new proof, where $theory$ is usually an \ML\ identifier 
415 
and the {\it formula\/} is written as an \ML\ string. 

416 

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

420 

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

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

105  425 

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

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

5205  431 
It gets the theorem using \texttt{result}, stores it in Isabelle's 
3103  432 
theorem database and binds it to an \ML{} identifier. 
433 

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

437 
shortcuts: 

438 
\begin{center} \tt 

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

442 

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

444 

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

446 

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

448 
\end{tabular} 

449 
\end{center} 

450 

451 
\subsection{A trivial example in propositional logic} 

452 
\index{examples!propositional} 

296  453 

5205  454 
Directory \texttt{FOL} of the Isabelle distribution defines the theory of 
296  455 
firstorder logic. Let us try the example from \S\ref{propproof}, 
456 
entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these 

5205  457 
examples, see the file \texttt{FOL/ex/intro.ML}.} 
105  458 
\begin{ttbox} 
5205  459 
Goal "PP > P"; 
105  460 
{\out Level 0} 
461 
{\out P  P > P} 

462 
{\out 1. P  P > P} 

311  463 
\end{ttbox}\index{level of a proof} 
105  464 
Isabelle responds by printing the initial proof state, which has $P\disj 
311  465 
P\imp P$ as the main goal and the only subgoal. The {\bf level} of the 
5205  466 
state is the number of \texttt{by} commands that have been applied to reach 
311  467 
it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, 
105  468 
or~$({\imp}I)$, to subgoal~1: 
469 
\begin{ttbox} 

470 
by (resolve_tac [impI] 1); 

471 
{\out Level 1} 

472 
{\out P  P > P} 

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

474 
\end{ttbox} 

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

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

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

480 
{\out Level 2} 

481 
{\out P  P > P} 

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

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

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

485 
\end{ttbox} 

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

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

489 
P}. 

105  490 
\begin{ttbox} 
491 
by (assume_tac 3); 

492 
{\out Level 3} 

493 
{\out P  P > P} 

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

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

496 
\end{ttbox} 

5205  497 
Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1. 
105  498 
\begin{ttbox} 
499 
by (assume_tac 2); 

500 
{\out Level 4} 

501 
{\out P  P > P} 

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

503 
\end{ttbox} 

504 
Lastly we prove the remaining subgoal by assumption: 

505 
\begin{ttbox} 

506 
by (assume_tac 1); 

507 
{\out Level 5} 

508 
{\out P  P > P} 

509 
{\out No subgoals!} 

510 
\end{ttbox} 

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

5205  512 
complete. Calling \texttt{qed} stores the theorem. 
105  513 
\begin{ttbox} 
3103  514 
qed "mythm"; 
105  515 
{\out val mythm = "?P  ?P > ?P" : thm} 
516 
\end{ttbox} 

5205  517 
Isabelle has replaced the free variable~\texttt{P} by the scheme 
105  518 
variable~{\tt?P}\@. Free variables in the proof state remain fixed 
519 
throughout the proof. Isabelle finally converts them to scheme variables 

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

521 

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

105  524 

296  525 

526 
\subsection{Part of a distributive law} 

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

5205  529 
and the tactical \texttt{REPEAT}, let us prove part of the distributive 
296  530 
law 
531 
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] 

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

5205  534 
Goal "(P & Q)  R > (P  R)"; 
105  535 
{\out Level 0} 
536 
{\out P & Q  R > P  R} 

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

296  538 
\ttbreak 
105  539 
by (resolve_tac [impI] 1); 
540 
{\out Level 1} 

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

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

543 
\end{ttbox} 

5205  544 
Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but 
105  545 
\ttindex{eresolve_tac} deletes the assumption after use. The resulting proof 
546 
state is simpler. 

547 
\begin{ttbox} 

548 
by (eresolve_tac [disjE] 1); 

549 
{\out Level 2} 

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

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

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

553 
\end{ttbox} 

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

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

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

5205  557 
and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two 
296  558 
assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we 
5205  559 
may try out \texttt{dresolve_tac}. 
105  560 
\begin{ttbox} 
561 
by (dresolve_tac [conjunct1] 1); 

562 
{\out Level 3} 

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

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

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

566 
\end{ttbox} 

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

568 
\begin{ttbox} 

569 
by (resolve_tac [disjI1] 1); 

570 
{\out Level 4} 

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

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

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

574 
\ttbreak 

575 
by (resolve_tac [disjI2] 2); 

576 
{\out Level 5} 

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

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

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

580 
\end{ttbox} 

5205  581 
Two calls of \texttt{assume_tac} can finish the proof. The 
582 
tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1} 

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

585 
\begin{ttbox} 

586 
by (REPEAT (assume_tac 1)); 

587 
{\out Level 6} 

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

589 
{\out No subgoals!} 

590 
\end{ttbox} 

591 

592 

593 
\section{Quantifier reasoning} 

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

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

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

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

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

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

105  603 

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

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

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

1878  609 
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

610 
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

611 
but we need never say so. This choice is forced by the reflexive law for 
105  612 
equality, and happens automatically. 
613 

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

617 
\begin{ttbox} 

5205  618 
Goal "ALL x. EX y. x=y"; 
105  619 
{\out Level 0} 
620 
{\out ALL x. EX y. x = y} 

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

622 
\ttbreak 

623 
by (resolve_tac [allI] 1); 

624 
{\out Level 1} 

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

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

627 
\end{ttbox} 

5205  628 
The variable~\texttt{x} is no longer universally quantified, but is a 
105  629 
parameter in the subgoal; thus, it is universally quantified at the 
5205  630 
metalevel. The subgoal must be proved for all possible values of~\texttt{x}. 
296  631 

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

105  633 
\begin{ttbox} 
634 
by (resolve_tac [exI] 1); 

635 
{\out Level 2} 

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

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

638 
\end{ttbox} 

5205  639 
The bound variable \texttt{y} has become {\tt?y1(x)}. This term consists of 
640 
the function unknown~{\tt?y1} applied to the parameter~\texttt{x}. 

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

105  642 
subgoal with the reflexivity axiom. 
643 
\begin{ttbox} 

644 
by (resolve_tac [refl] 1); 

645 
{\out Level 3} 

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

647 
{\out No subgoals!} 

648 
\end{ttbox} 

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

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

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

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

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

654 

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

105  657 
try~$(\exists I)$: 
658 
\begin{ttbox} 

5205  659 
Goal "EX y. ALL x. x=y"; 
105  660 
{\out Level 0} 
661 
{\out EX y. ALL x. x = y} 

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

663 
\ttbreak 

664 
by (resolve_tac [exI] 1); 

665 
{\out Level 1} 

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

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

668 
\end{ttbox} 

5205  669 
The unknown \texttt{?y} may be replaced by any term, but this can never 
670 
introduce another bound occurrence of~\texttt{x}. We now apply~$(\forall I)$: 

105  671 
\begin{ttbox} 
672 
by (resolve_tac [allI] 1); 

673 
{\out Level 2} 

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

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

676 
\end{ttbox} 

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

5205  678 
have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}. 
105  679 
The reflexivity axiom does not unify with subgoal~1. 
680 
\begin{ttbox} 

681 
by (resolve_tac [refl] 1); 

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

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

689 

690 
\subsection{Nested quantifiers} 

691 
\index{examples!with quantifiers} 

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

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

695 
the wrong order, the proof will fail. 

696 

5205  697 
This section concludes with a demonstration of \texttt{REPEAT} 
698 
and~\texttt{ORELSE}. 

105  699 
\begin{ttbox} 
5205  700 
Goal "(ALL x y.P(x,y)) > (ALL z w.P(w,z))"; 
105  701 
{\out Level 0} 
702 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))} 

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

704 
\ttbreak 

705 
by (resolve_tac [impI] 1); 

706 
{\out Level 1} 

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

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

709 
\end{ttbox} 

710 

296  711 
\paragraph{The wrong approach.} 
5205  712 
Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the 
311  713 
\ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. 
105  714 
\begin{ttbox} 
715 
by (dresolve_tac [spec] 1); 

716 
{\out Level 2} 

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

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

719 
\ttbreak 

720 
by (resolve_tac [allI] 1); 

721 
{\out Level 3} 

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

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

724 
\end{ttbox} 

5205  725 
The unknown \texttt{?x1} and the parameter \texttt{z} have appeared. We again 
296  726 
apply $(\forall E)$ and~$(\forall I)$. 
105  727 
\begin{ttbox} 
728 
by (dresolve_tac [spec] 1); 

729 
{\out Level 4} 

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

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

732 
\ttbreak 

733 
by (resolve_tac [allI] 1); 

734 
{\out Level 5} 

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

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

737 
\end{ttbox} 

5205  738 
The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each 
105  739 
unknown is applied to the parameters existing at the time of its creation; 
5205  740 
instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances 
741 
of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1}, 

105  742 
proof by assumption will fail. 
743 
\begin{ttbox} 

744 
by (assume_tac 1); 

3103  745 
{\out by: tactic failed} 
105  746 
{\out uncaught exception ERROR} 
747 
\end{ttbox} 

748 

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

754 
\begin{ttbox} 

755 
choplev 1; 

756 
{\out Level 1} 

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

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

759 
\end{ttbox} 

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

763 
{\out Level 2} 

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

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

766 
\ttbreak 

767 
by (resolve_tac [allI] 1); 

768 
{\out Level 3} 

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

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

771 
\end{ttbox} 

5205  772 
The parameters \texttt{z} and~\texttt{w} have appeared. We now create the 
105  773 
unknowns: 
774 
\begin{ttbox} 

775 
by (dresolve_tac [spec] 1); 

776 
{\out Level 4} 

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

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

779 
\ttbreak 

780 
by (dresolve_tac [spec] 1); 

781 
{\out Level 5} 

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

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

784 
\end{ttbox} 

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

5205  786 
z} and~\texttt{w}: 
105  787 
\begin{ttbox} 
788 
by (assume_tac 1); 

789 
{\out Level 6} 

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

791 
{\out No subgoals!} 

792 
\end{ttbox} 

793 

296  794 
\paragraph{A onestep proof using tacticals.} 
795 
\index{tacticals} \index{examples!of tacticals} 

796 

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

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

105  800 
\begin{ttbox} 
801 
choplev 0; 

802 
{\out Level 0} 

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

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

805 
\end{ttbox} 

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

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

105  810 
\begin{ttbox} 
296  811 
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 
105  812 
ORELSE dresolve_tac [spec] 1)); 
813 
{\out Level 1} 

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

815 
{\out No subgoals!} 

816 
\end{ttbox} 

817 

818 

819 
\subsection{A realistic quantifier proof} 

820 
\index{examples!with quantifiers} 

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

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

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

105  825 
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we 
5205  826 
use \texttt{REPEAT}: 
105  827 
\begin{ttbox} 
5205  828 
Goal "(ALL x.P(x) > Q) > (EX x.P(x)) > Q"; 
105  829 
{\out Level 0} 
830 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q} 

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

832 
\ttbreak 

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

834 
{\out Level 1} 

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

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

837 
\end{ttbox} 

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

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

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

311  841 
identifier~\tdx{exE}. 
105  842 
\begin{ttbox} 
843 
by (eresolve_tac [exE] 1); 

844 
{\out Level 2} 

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

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

847 
\end{ttbox} 

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

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

850 
only needed once. 

851 
\begin{ttbox} 

852 
by (dresolve_tac [spec] 1); 

853 
{\out Level 3} 

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

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

856 
\end{ttbox} 

296  857 
Because we applied $(\exists E)$ before $(\forall E)$, the unknown 
5205  858 
term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}. 
105  859 

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

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

862 
frequently useful. 

863 
\begin{ttbox} 

864 
by (eresolve_tac [mp] 1); 

865 
{\out Level 4} 

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

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

868 
\end{ttbox} 

5205  869 
The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the 
870 
implication. The final step is trivial, thanks to the occurrence of~\texttt{x}. 

105  871 
\begin{ttbox} 
872 
by (assume_tac 1); 

873 
{\out Level 5} 

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

875 
{\out No subgoals!} 

876 
\end{ttbox} 

877 

878 

311  879 
\subsection{The classical reasoner} 
880 
\index{classical reasoner} 

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

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

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

105  886 

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

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

3127  890 
is~\ttindex{Blast_tac}. 
105  891 

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

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

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

895 
\begin{ttbox} 

5205  896 
Goal "(EX y. ALL x. J(y,x) <> ~J(x,x)) \ttback 
105  897 
\ttback > ~ (ALL x. EX y. ALL z. J(z,y) <> ~ J(z,x))"; 
898 
{\out Level 0} 

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

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

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

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

903 
\end{ttbox} 

3127  904 
\ttindex{Blast_tac} proves subgoal~1 at a stroke. 
105  905 
\begin{ttbox} 
3127  906 
by (Blast_tac 1); 
907 
{\out Depth = 0} 

908 
{\out Depth = 1} 

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

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

912 
{\out No subgoals!} 

913 
\end{ttbox} 

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

5205  915 
tactics, such as~\texttt{step_tac}. This would take up much space, however, 
105  916 
so let us proceed to the next example: 
917 
\begin{ttbox} 

5205  918 
Goal "ALL x. P(x,f(x)) <> \ttback 
105  919 
\ttback (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"; 
920 
{\out Level 0} 

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

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

105  924 
\end{ttbox} 
925 
Again, subgoal~1 succumbs immediately. 

926 
\begin{ttbox} 

3127  927 
by (Blast_tac 1); 
928 
{\out Depth = 0} 

929 
{\out Depth = 1} 

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

932 
{\out No subgoals!} 

933 
\end{ttbox} 

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

936 
disjunction and conjunction. The rules for infinite unions and 

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

938 
reasoner is effective for reasoning in set theory. 

939 