author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
permissions  rwrr 
14148  1 
\part{Using Isabelle from the ML TopLevel}\label{chap:getting} 
2 

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

4 
Proofs are conducted by 

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

3103  8 
alternative syntaxes, for example using mathematical symbols from a 
14148  9 
special screen font. The metalogic and main 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 
9695  29 
(HOL) by default. 
4802
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 
\] 

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

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

43077
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42637
diff
changeset

122 
\index{*"!"! symbol} 
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42637
diff
changeset

123 

7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42637
diff
changeset

124 
\index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because  stopped working 
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42637
diff
changeset

125 
\index{"!]@{\tt\char124]} symbol} % so these are [ and ] 
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42637
diff
changeset

126 

311  127 
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol} 
105  128 
\[\dquotes 
129 
\begin{array}{l@{\quad}l@{\quad}l} 

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

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

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

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

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

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

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

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

3103  138 
\Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} 
105  139 
\end{array} 
140 
\] 

141 
Flexflex constraints are metaequalities arising from unification; they 

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

311  143 
\index{flexflex constraints} 
105  144 

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

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

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

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

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

5205  153 
it with the symbol \texttt{PROP}:\index{*PROP symbol} 
105  154 
\begin{ttbox} 
155 
PROP ?psi ==> PROP ?theta 

156 
\end{ttbox} 

157 

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

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

162 
\tt False & $\bot$ & false \\ 

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

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

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

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

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

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

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

170 
\end{tabular} 

171 
\] 

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

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

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

178 
\end{ttbox} 

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

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

182 
$({\conj}I)$ as 

105  183 
\begin{ttbox} 
184 
[ P; Q ] ==> P & Q 

185 
\end{ttbox} 

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

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

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

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

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

191 
forth. 

192 

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

194 
\begin{ttbox} 

14148  195 
[ EX x. P(x); !!x. P(x) ==> Q ] ==> Q 
105  196 
\end{ttbox} 
197 

198 

199 
\subsection{Basic operations on theorems} 

200 
\index{theorems!basic operations onbold} 

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

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

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

206 
are taken as axioms. 

105  207 

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

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

105  211 

311  212 
\index{theorems!printing of} 
213 
\begin{ttdescription} 

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

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

105  216 

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

105  219 

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

222 
inspecting the output of a tactic. 

105  223 

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

105  226 

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

105  229 

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

232 
to have subscript zero, improving readability and reducing subscript 

233 
growth. 

234 
\end{ttdescription} 

9695  235 
The rules of a theory are normally bound to \ML\ identifiers. Suppose we are 
236 
running an Isabelle session containing theory~FOL, natural deduction 

237 
firstorder logic.\footnote{For a listing of the FOL rules and their \ML{} 

238 
names, turn to 

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

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

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

243 
itself. 

105  244 
\begin{ttbox} 
245 
prth mp; 

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

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

248 
prth (mp RS mp); 

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

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

251 
\end{ttbox} 

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

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

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

105  260 

5205  261 
To contrast \texttt{RS} with \texttt{RSN}, we resolve 
311  262 
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. 
105  263 
\begin{ttbox} 
264 
conjunct1 RS mp; 

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

266 
conjunct1 RSN (2,mp); 

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

268 
\end{ttbox} 

269 
These correspond to the following proofs: 

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

271 
\qquad 

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

273 
\] 

296  274 
% 
275 
Rules can be derived by pasting other rules together. Let us join 

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

296  278 
printed. 
105  279 
\begin{ttbox} 
280 
spec; 

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

282 
it RS mp; 

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

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

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

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

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

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

295 
rules provide a way of referring to particular assumptions. 

311  296 
\index{assumptions!use of} 
105  297 

311  298 
\subsection{*Flexflex constraints} \label{flexflex} 
299 
\index{flexflex constraintsbold}\index{unknowns!function} 

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

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

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

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

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

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

307 
equations as constraints on future unifications. Flexflex constraints 

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

5205  309 
during use of \texttt{RS} and~\texttt{RSN}: 
105  310 
\begin{ttbox} 
311 
refl; 

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

313 
exI; 

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

315 
refl RS exI; 

14148  316 
{\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm} 
317 
\end{ttbox} 

318 
% 

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

320 
a metalevel hypothesis. We can make all such hypotheses visible by setting the 

321 
\ttindexbold{show_hyps} flag: 

322 
\begin{ttbox} 

323 
set show_hyps; 

324 
{\out val it = true : bool} 

325 
refl RS exI; 

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

105  327 
\end{ttbox} 
328 

329 
\noindent 

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

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

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

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

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

335 
\begin{ttbox} 

336 
prthq (flexflex_rule it); 

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

338 
\end{ttbox} 

339 
Isabelle simplifies flexflex equations to eliminate redundant bound 

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

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

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

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

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

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

348 

349 
\begin{warn} 

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

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

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

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

358 
\end{ttbox} 

359 

360 
\noindent 

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

362 
unique unifier: 

363 
\begin{ttbox} 

364 
reflk RS exI; 

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

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

105  368 
\end{ttbox} 
369 
Using \ttindex{RL} this time, we discover that there are four unifiers, and 

370 
four resolvents: 

371 
\begin{ttbox} 

372 
[reflk] RL [exI]; 

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

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

375 
\end{ttbox} 

376 
\end{warn} 

377 

311  378 
\index{forward proof)} 
105  379 

380 
\section{Backward proof} 

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

384 

385 
\subsection{The basic tactics} 

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

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

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

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

392 
tactics try their list of theorems in lefttoright order. 

393 

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

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

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

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

399 
subgoal by assumption. 

105  400 

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

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

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

405 
conclusion with the subgoal and inserting instantiated premises in its 

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

407 
none of the rules generates next states. 

105  408 

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

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

311  413 
that assumption from any subgoals arising from the resolution. 
105  414 

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

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

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

419 
assumptions. 

420 
\end{ttdescription} 

105  421 

422 
\subsection{Commands for backward proof} 

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

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

427 
its many commands, most important are the following: 

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

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

435 

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

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

105  440 

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

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

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

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

452 
shortcuts: 

453 
\begin{center} \tt 

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

457 

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

459 

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

461 

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

463 
\end{tabular} 

464 
\end{center} 

465 

466 
\subsection{A trivial example in propositional logic} 

467 
\index{examples!propositional} 

296  468 

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

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

477 
{\out 1. P  P > P} 

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

485 
by (resolve_tac [impI] 1); 

486 
{\out Level 1} 

487 
{\out P  P > P} 

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

489 
\end{ttbox} 

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

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

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

495 
{\out Level 2} 

496 
{\out P  P > P} 

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

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

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

500 
\end{ttbox} 

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

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

504 
P}. 

105  505 
\begin{ttbox} 
506 
by (assume_tac 3); 

507 
{\out Level 3} 

508 
{\out P  P > P} 

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

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

511 
\end{ttbox} 

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

515 
{\out Level 4} 

516 
{\out P  P > P} 

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

518 
\end{ttbox} 

519 
Lastly we prove the remaining subgoal by assumption: 

520 
\begin{ttbox} 

521 
by (assume_tac 1); 

522 
{\out Level 5} 

523 
{\out P  P > P} 

524 
{\out No subgoals!} 

525 
\end{ttbox} 

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

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

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

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

536 

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

105  539 

296  540 

541 
\subsection{Part of a distributive law} 

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

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

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

5205  549 
Goal "(P & Q)  R > (P  R)"; 
105  550 
{\out Level 0} 
551 
{\out P & Q  R > P  R} 

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

296  553 
\ttbreak 
105  554 
by (resolve_tac [impI] 1); 
555 
{\out Level 1} 

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

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

558 
\end{ttbox} 

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

562 
\begin{ttbox} 

563 
by (eresolve_tac [disjE] 1); 

564 
{\out Level 2} 

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

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

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

568 
\end{ttbox} 

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

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

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

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

577 
{\out Level 3} 

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

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

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

581 
\end{ttbox} 

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

583 
\begin{ttbox} 

584 
by (resolve_tac [disjI1] 1); 

585 
{\out Level 4} 

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

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

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

589 
\ttbreak 

590 
by (resolve_tac [disjI2] 2); 

591 
{\out Level 5} 

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

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

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

595 
\end{ttbox} 

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

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

600 
\begin{ttbox} 

601 
by (REPEAT (assume_tac 1)); 

602 
{\out Level 6} 

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

604 
{\out No subgoals!} 

605 
\end{ttbox} 

606 

607 

608 
\section{Quantifier reasoning} 

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

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

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

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

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

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

105  618 

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

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

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

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

625 
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

626 
but we need never say so. This choice is forced by the reflexive law for 
105  627 
equality, and happens automatically. 
628 

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

632 
\begin{ttbox} 

5205  633 
Goal "ALL x. EX y. x=y"; 
105  634 
{\out Level 0} 
635 
{\out ALL x. EX y. x = y} 

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

637 
\ttbreak 

638 
by (resolve_tac [allI] 1); 

639 
{\out Level 1} 

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

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

642 
\end{ttbox} 

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

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

105  648 
\begin{ttbox} 
649 
by (resolve_tac [exI] 1); 

650 
{\out Level 2} 

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

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

653 
\end{ttbox} 

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

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

105  657 
subgoal with the reflexivity axiom. 
658 
\begin{ttbox} 

659 
by (resolve_tac [refl] 1); 

660 
{\out Level 3} 

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

662 
{\out No subgoals!} 

663 
\end{ttbox} 

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

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

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

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

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

669 

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

105  672 
try~$(\exists I)$: 
673 
\begin{ttbox} 

5205  674 
Goal "EX y. ALL x. x=y"; 
105  675 
{\out Level 0} 
676 
{\out EX y. ALL x. x = y} 

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

678 
\ttbreak 

679 
by (resolve_tac [exI] 1); 

680 
{\out Level 1} 

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

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

683 
\end{ttbox} 

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

105  686 
\begin{ttbox} 
687 
by (resolve_tac [allI] 1); 

688 
{\out Level 2} 

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

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

691 
\end{ttbox} 

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

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

696 
by (resolve_tac [refl] 1); 

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

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

704 

705 
\subsection{Nested quantifiers} 

706 
\index{examples!with quantifiers} 

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

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

710 
the wrong order, the proof will fail. 

711 

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

105  714 
\begin{ttbox} 
5205  715 
Goal "(ALL x y.P(x,y)) > (ALL z w.P(w,z))"; 
105  716 
{\out Level 0} 
717 
{\out (ALL x y. P(x,y)) > (ALL z w. P(w,z))} 

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

719 
\ttbreak 

720 
by (resolve_tac [impI] 1); 

721 
{\out Level 1} 

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

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

724 
\end{ttbox} 

725 

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

731 
{\out Level 2} 

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

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

734 
\ttbreak 

735 
by (resolve_tac [allI] 1); 

736 
{\out Level 3} 

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

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

739 
\end{ttbox} 

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

744 
{\out Level 4} 

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

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

747 
\ttbreak 

748 
by (resolve_tac [allI] 1); 

749 
{\out Level 5} 

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

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

752 
\end{ttbox} 

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

105  757 
proof by assumption will fail. 
758 
\begin{ttbox} 

759 
by (assume_tac 1); 

3103  760 
{\out by: tactic failed} 
105  761 
{\out uncaught exception ERROR} 
762 
\end{ttbox} 

763 

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

769 
\begin{ttbox} 

770 
choplev 1; 

771 
{\out Level 1} 

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

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

774 
\end{ttbox} 

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

778 
{\out Level 2} 

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

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

781 
\ttbreak 

782 
by (resolve_tac [allI] 1); 

783 
{\out Level 3} 

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

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

786 
\end{ttbox} 

5205  787 
The parameters \texttt{z} and~\texttt{w} have appeared. We now create the 
105  788 
unknowns: 
789 
\begin{ttbox} 

790 
by (dresolve_tac [spec] 1); 

791 
{\out Level 4} 

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

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

794 
\ttbreak 

795 
by (dresolve_tac [spec] 1); 

796 
{\out Level 5} 

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

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

799 
\end{ttbox} 

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

5205  801 
z} and~\texttt{w}: 
105  802 
\begin{ttbox} 
803 
by (assume_tac 1); 

804 
{\out Level 6} 

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

806 
{\out No subgoals!} 

807 
\end{ttbox} 

808 

296  809 
\paragraph{A onestep proof using tacticals.} 
810 
\index{tacticals} \index{examples!of tacticals} 

811 

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

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

105  815 
\begin{ttbox} 
816 
choplev 0; 

817 
{\out Level 0} 

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

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

820 
\end{ttbox} 

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

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

105  825 
\begin{ttbox} 
296  826 
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 
105  827 
ORELSE dresolve_tac [spec] 1)); 
828 
{\out Level 1} 

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

830 
{\out No subgoals!} 

831 
\end{ttbox} 

832 

833 

834 
\subsection{A realistic quantifier proof} 

835 
\index{examples!with quantifiers} 

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

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

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

105  840 
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we 
5205  841 
use \texttt{REPEAT}: 
105  842 
\begin{ttbox} 
14148  843 
Goal "(ALL x. P(x) > Q) > (EX x. P(x)) > Q"; 
105  844 
{\out Level 0} 
845 
{\out (ALL x. P(x) > Q) > (EX x. P(x)) > Q} 

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

847 
\ttbreak 

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

849 
{\out Level 1} 

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

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

852 
\end{ttbox} 

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

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

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

311  856 
identifier~\tdx{exE}. 
105  857 
\begin{ttbox} 
858 
by (eresolve_tac [exE] 1); 

859 
{\out Level 2} 

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

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

862 
\end{ttbox} 

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

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

865 
only needed once. 

866 
\begin{ttbox} 

867 
by (dresolve_tac [spec] 1); 

868 
{\out Level 3} 

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

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

871 
\end{ttbox} 

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

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

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

877 
frequently useful. 

878 
\begin{ttbox} 

879 
by (eresolve_tac [mp] 1); 

880 
{\out Level 4} 

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

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

883 
\end{ttbox} 

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

105  886 
\begin{ttbox} 
887 
by (assume_tac 1); 

888 
{\out Level 5} 

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

890 
{\out No subgoals!} 

891 
\end{ttbox} 

892 

893 

311  894 
\subsection{The classical reasoner} 
895 
\index{classical reasoner} 

14148  896 
Isabelle provides enough automation to tackle substantial examples. 
897 
The classical 

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

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

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

105  903 

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

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

3127  907 
is~\ttindex{Blast_tac}. 
105  908 

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

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

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

912 
\begin{ttbox} 

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

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

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

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

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

920 
\end{ttbox} 

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

925 
{\out Depth = 1} 

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

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

929 
{\out No subgoals!} 

930 
\end{ttbox} 

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

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

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

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

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

105  941 
\end{ttbox} 
942 
Again, subgoal~1 succumbs immediately. 

943 
\begin{ttbox} 

3127  944 
by (Blast_tac 1); 
945 
{\out Depth = 0} 

946 
{\out Depth = 1} 

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

949 
{\out No subgoals!} 

950 
\end{ttbox} 

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

953 
disjunction and conjunction. The rules for infinite unions and 

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

955 
reasoner is effective for reasoning in set theory. 

956 