author  boehmes 
Tue, 07 Dec 2010 15:44:38 +0100  
changeset 41064  0c447a17770a 
parent 14148  6580d374a509 
child 42637  381fdcab0f36 
permissions  rwrr 
105  1 
%% $Id$ 
14148  2 
\part{Using Isabelle from the ML TopLevel}\label{chap:getting} 
3 

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{} toplevel  is still available, however. 

5 
Proofs are conducted by 

3103  6 
applying certain \ML{} functions, which update a stored proof state. 
14148  7 
All syntax can be expressed using plain {\sc ascii} 
8 
characters, but Isabelle can support 

3103  9 
alternative syntaxes, for example using mathematical symbols from a 
14148  10 
special screen font. The metalogic and main objectlogics already 
3103  11 
provide such fancy output as an option. 
105  12 

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

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

5205  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 

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

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

21 

311  22 
\section{Forward proof}\label{sec:forward} \index{forward proof(} 
105  23 
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

24 
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

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

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

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

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

29 
Note that just typing \texttt{isabelle} usually brings up higherorder logic 
9695  30 
(HOL) by default. 
4802
c15f46833f7a
Simplified the syntax description; mentioned FOL vs HOL
paulson
parents:
4244
diff
changeset

31 

105  32 

33 
\subsection{Lexical matters} 

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

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

40 

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 metalogic.) 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 

296  49 
symbols. 
105  50 

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

331  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} 

56 

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 nonnegative integer, 

60 
allows the renaming of unknowns prior to unification.% 

296  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!} 

105  70 

71 

72 
\subsection{Syntax of types and terms} 

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

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

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

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

81 
of propositions. Type variables can be constrained to particular 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

108 
"\%" 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

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

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

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

9695  114 
Note that HOL uses its traditional ``higherorder'' syntax for application, 
115 
which differs from that used in FOL. 

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

116 

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

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

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

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

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

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

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

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

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

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

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{metaquantification} \\ 

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

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

138 
Flexflex constraints are metaequalities arising from unification; they 

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

311  140 
\index{flexflex constraints} 
105  141 

311  142 
\index{*Trueprop constant} 
105  143 
Most logics define the implicit coercion $Trueprop$ from objectformulae to 
311  144 
propositions. This could cause an ambiguity: in $P\Imp Q$, do the 
145 
variables $P$ and $Q$ stand for metaformulae or objectformulae? 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 metaformula 

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

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

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

153 
\end{ttbox} 

154 

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

105  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$ & biimplication \\ 

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 firstorder logic: 

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

14148  171 
$$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ 
3103  172 
$({\conj}I)$ translates into {\sc ascii} characters as 
105  173 
\begin{ttbox} 
174 
[ ?P; ?Q ] ==> ?P & ?Q 

175 
\end{ttbox} 

296  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 

105  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. 

189 

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

191 
\begin{ttbox} 

14148  192 
[ EX x. P(x); !!x. P(x) ==> Q ] ==> Q 
105  193 
\end{ttbox} 
194 

195 

196 
\subsection{Basic operations on theorems} 

197 
\index{theorems!basic operations onbold} 

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

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

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

203 
are taken as axioms. 

105  204 

5205  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. 

105  208 

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

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

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

105  213 

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

105  216 

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

219 
inspecting the output of a tactic. 

105  220 

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

105  223 

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

105  226 

311  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} 

9695  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 
firstorder logic.\footnote{For a listing of the FOL rules and their \ML{} 

235 
names, turn to 

331  236 
\iflabelundefined{folrules}{{\em Isabelle's ObjectLogics}}% 
237 
{page~\pageref{folrules}}.} 

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. 

105  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} 

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

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

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

105  257 

5205  258 
To contrast \texttt{RS} with \texttt{RSN}, we resolve 
311  259 
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. 
105  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 
\] 

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

5205  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 

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

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

279 
it RS mp; 

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

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

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

105  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 destructresolution, such specialized 

292 
rules provide a way of referring to particular assumptions. 

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

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

105  297 
In higherorder unification, {\bf flexflex} 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 flexflex 

304 
equations as constraints on future unifications. Flexflex constraints 

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

5205  306 
during use of \texttt{RS} and~\texttt{RSN}: 
105  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; 

14148  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 metalevel 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} 

105  324 
\end{ttbox} 
325 

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 flexflex 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 

296  339 
none on the left in a common instance of these terms. Choosing a new 
105  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))$. 

345 

346 
\begin{warn} 

5205  347 
\ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless 
105  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 

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

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

355 
\end{ttbox} 

356 

357 
\noindent 

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

359 
unique unifier: 

360 
\begin{ttbox} 

361 
reflk RS exI; 

14148  362 
{\out uncaught exception} 
363 
{\out THM ("RSN: multiple unifiers", 1,} 

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

105  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} 

374 

311  375 
\index{forward proof)} 
105  376 

377 
\section{Backward proof} 

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

381 

382 
\subsection{The basic tactics} 

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

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

105  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 lefttoright order. 

390 

311  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. 

105  397 

311  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 objectrules, 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 higherorder unifiers. The tactic fails if 

404 
none of the rules generates next states. 

105  405 

311  406 
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elimresolution} 
5205  407 
performs elimresolution. 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 

311  410 
that assumption from any subgoals arising from the resolution. 
105  411 

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

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

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

416 
assumptions. 

417 
\end{ttdescription} 

105  418 

419 
\subsection{Commands for backward proof} 

311  420 
\index{proofs!commands for} 
105  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: 

311  425 
\begin{ttdescription} 
5205  426 
\item[\ttindex{Goal} {\it formula}; ] 
14148  427 
begins a new proof, where the {\it formula\/} is written as an \ML\ string. 
105  428 

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

432 

3103  433 
\item[\ttindex{undo}(); ] 
296  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. 

105  437 

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

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

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

311  446 
\end{ttdescription} 
105  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 

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

454 

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

456 

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

458 

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

460 
\end{tabular} 

461 
\end{center} 

462 

463 
\subsection{A trivial example in propositional logic} 

464 
\index{examples!propositional} 

296  465 

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

5205  469 
examples, see the file \texttt{FOL/ex/intro.ML}.} 
105  470 
\begin{ttbox} 
5205  471 
Goal "PP > P"; 
105  472 
{\out Level 0} 
473 
{\out P  P > P} 

474 
{\out 1. P  P > P} 

311  475 
\end{ttbox}\index{level of a proof} 
105  476 
Isabelle responds by printing the initial proof state, which has $P\disj 
311  477 
P\imp P$ as the main goal and the only subgoal. The {\bf level} of the 
5205  478 
state is the number of \texttt{by} commands that have been applied to reach 
311  479 
it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, 
105  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 metaimplication {\tt==>} indicates assumptions.) We apply 

311  489 
\tdx{disjE}, or~(${\disj}E)$, to that subgoal: 
105  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} 

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

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

501 
P}. 

105  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} 

5205  509 
Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1. 
105  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 

5205  524 
complete. Calling \texttt{qed} stores the theorem. 
105  525 
\begin{ttbox} 
3103  526 
qed "mythm"; 
105  527 
{\out val mythm = "?P  ?P > ?P" : thm} 
528 
\end{ttbox} 

5205  529 
Isabelle has replaced the free variable~\texttt{P} by the scheme 
105  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. 

533 

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

105  536 

296  537 

538 
\subsection{Part of a distributive law} 

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

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

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

5205  546 
Goal "(P & Q)  R > (P  R)"; 
105  547 
{\out Level 0} 
548 
{\out P & Q  R > P  R} 

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

296  550 
\ttbreak 
105  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} 

5205  556 
Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but 
105  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 

5205  569 
and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two 
296  570 
assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we 
5205  571 
may try out \texttt{dresolve_tac}. 
105  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} 

5205  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} 

105  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} 

603 

604 

605 
\section{Quantifier reasoning} 

331  606 
\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function} 
105  607 
This section illustrates how Isabelle enforces quantifier provisos. 
331  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. 

105  615 

296  616 
\subsection{Two quantifier proofs: a success and a failure} 
105  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 nontheorem $\exists y.\forall x.x=y$. The former 

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

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

622 
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

623 
but we need never say so. This choice is forced by the reflexive law for 
105  624 
equality, and happens automatically. 
625 

296  626 
\paragraph{The successful proof.} 
105  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} 

5205  630 
Goal "ALL x. EX y. x=y"; 
105  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} 

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

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

105  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} 

5205  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 

105  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. 

666 

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

105  669 
try~$(\exists I)$: 
670 
\begin{ttbox} 

5205  671 
Goal "EX y. ALL x. x=y"; 
105  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} 

5205  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)$: 

105  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 

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

693 
by (resolve_tac [refl] 1); 

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

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

701 

702 
\subsection{Nested quantifiers} 

703 
\index{examples!with quantifiers} 

296  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. 

708 

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

105  711 
\begin{ttbox} 
5205  712 
Goal "(ALL x y.P(x,y)) > (ALL z w.P(w,z))"; 
105  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} 

722 

296  723 
\paragraph{The wrong approach.} 
5205  724 
Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the 
311  725 
\ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. 
105  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} 

5205  737 
The unknown \texttt{?x1} and the parameter \texttt{z} have appeared. We again 
296  738 
apply $(\forall E)$ and~$(\forall I)$. 
105  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} 

5205  750 
The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each 
105  751 
unknown is applied to the parameters existing at the time of its creation; 
5205  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}, 

105  754 
proof by assumption will fail. 
755 
\begin{ttbox} 

756 
by (assume_tac 1); 

3103  757 
{\out by: tactic failed} 
105  758 
{\out uncaught exception ERROR} 
759 
\end{ttbox} 

760 

296  761 
\paragraph{The right approach.} 
105  762 
To do this proof, the rules must be applied in the correct order. 
331  763 
Parameters should be created before unknowns. The 
105  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} 

296  772 
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$. 
105  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} 

5205  784 
The parameters \texttt{z} and~\texttt{w} have appeared. We now create the 
105  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 

5205  798 
z} and~\texttt{w}: 
105  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} 

805 

296  806 
\paragraph{A onestep proof using tacticals.} 
807 
\index{tacticals} \index{examples!of tacticals} 

808 

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

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

105  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} 

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

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

105  822 
\begin{ttbox} 
296  823 
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 
105  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} 

829 

830 

831 
\subsection{A realistic quantifier proof} 

832 
\index{examples!with quantifiers} 

296  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 lefttoright half to Isabelle in the normal way. 

105  837 
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we 
5205  838 
use \texttt{REPEAT}: 
105  839 
\begin{ttbox} 
14148  840 
Goal "(ALL x. P(x) > Q) > (EX x. P(x)) > Q"; 
105  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 

311  853 
identifier~\tdx{exE}. 
105  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} 

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

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} 

5205  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}. 

105  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} 

889 

890 

311  891 
\subsection{The classical reasoner} 
892 
\index{classical reasoner} 

14148  893 
Isabelle provides enough automation to tackle substantial examples. 
894 
The classical 

331  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}}. 

14148  898 
It cannot compete with fully automatic theorem provers, but it is 
899 
competitive with tools found in other interactive provers. 

105  900 

331  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 

3127  904 
is~\ttindex{Blast_tac}. 
105  905 

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} 

5205  910 
Goal "(EX y. ALL x. J(y,x) <> ~J(x,x)) \ttback 
105  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} 

3127  918 
\ttindex{Blast_tac} proves subgoal~1 at a stroke. 
105  919 
\begin{ttbox} 
3127  920 
by (Blast_tac 1); 
921 
{\out Depth = 0} 

922 
{\out Depth = 1} 

105  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 singlestep 

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

5205  932 
Goal "ALL x. P(x,f(x)) <> \ttback 
105  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))} 

296  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))} 

105  938 
\end{ttbox} 
939 
Again, subgoal~1 succumbs immediately. 

940 
\begin{ttbox} 

3127  941 
by (Blast_tac 1); 
942 
{\out Depth = 0} 

943 
{\out Depth = 1} 

105  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} 

331  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. 

953 