author  wenzelm 
Thu, 17 Jul 1997 15:03:38 +0200  
changeset 3524  c02cb15830de 
parent 3485  f27a30a18a17 
child 5205  602354039306 
permissions  rwrr 
105  1 
%% $Id$ 
284  2 
\part{Advanced Methods} 
105  3 
Before continuing, it might be wise to try some of your own examples in 
4 
Isabelle, reinforcing your knowledge of the basic functions. 

5 

3103  6 
Look through {\em Isabelle's ObjectLogics\/} and try proving some 
7 
simple theorems. You probably should begin with firstorder logic 

8 
({\tt FOL} or~{\tt LK}). Try working some of the examples provided, 

9 
and others from the literature. Set theory~({\tt ZF}) and 

10 
Constructive Type Theory~({\tt CTT}) form a richer world for 

11 
mathematical reasoning and, again, many examples are in the 

12 
literature. Higherorder logic~({\tt HOL}) is Isabelle's most 

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

13 
elaborate logic. Its types and functions are identified with those of 
3103  14 
the metalogic. 
105  15 

16 
Choose a logic that you already understand. Isabelle is a proof 

17 
tool, not a teaching tool; if you do not know how to do a particular proof 

18 
on paper, then you certainly will not be able to do it on the machine. 

19 
Even experienced users plan large proofs on paper. 

20 

21 
We have covered only the bare essentials of Isabelle, but enough to perform 

22 
substantial proofs. By occasionally dipping into the {\em Reference 

23 
Manual}, you can learn additional tactics, subgoal commands and tacticals. 

24 

25 

26 
\section{Deriving rules in Isabelle} 

27 
\index{rules!derived} 

28 
A mathematical development goes through a progression of stages. Each 

29 
stage defines some concepts and derives rules about them. We shall see how 

30 
to derive rules, perhaps involving definitions, using Isabelle. The 

310  31 
following section will explain how to declare types, constants, rules and 
105  32 
definitions. 
33 

34 

296  35 
\subsection{Deriving a rule using tactics and metalevel assumptions} 
36 
\label{derivingexample} 

310  37 
\index{examples!of deriving rules}\index{assumptions!of main goal} 
296  38 

307  39 
The subgoal module supports the derivation of rules, as discussed in 
3103  40 
\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of 
41 
the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates 

42 
$\phi\Imp\phi$ as the initial proof state and returns a list 

43 
consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, 

44 
\ldots,~$k$. These metaassumptions are also recorded internally, 

45 
allowing {\tt result} (which is called by {\tt qed}) to discharge them 

307  46 
in the original order. 
105  47 

307  48 
Let us derive $\conj$ elimination using Isabelle. 
310  49 
Until now, calling {\tt goal} has returned an empty list, which we have 
105  50 
thrown away. In this example, the list contains the two premises of the 
51 
rule. We bind them to the \ML\ identifiers {\tt major} and {\tt 

52 
minor}:\footnote{Some ML compilers will print a message such as {\em 

53 
binding not exhaustive}. This warns that {\tt goal} must return a 

54 
2element list. Otherwise, the patternmatch will fail; ML will 

310  55 
raise exception \xdx{Match}.} 
105  56 
\begin{ttbox} 
57 
val [major,minor] = goal FOL.thy 

58 
"[ P&Q; [ P; Q ] ==> R ] ==> R"; 

59 
{\out Level 0} 

60 
{\out R} 

61 
{\out 1. R} 

62 
{\out val major = "P & Q [P & Q]" : thm} 

63 
{\out val minor = "[ P; Q ] ==> R [[ P; Q ] ==> R]" : thm} 

64 
\end{ttbox} 

65 
Look at the minor premise, recalling that metalevel assumptions are 

66 
shown in brackets. Using {\tt minor}, we reduce $R$ to the subgoals 

67 
$P$ and~$Q$: 

68 
\begin{ttbox} 

69 
by (resolve_tac [minor] 1); 

70 
{\out Level 1} 

71 
{\out R} 

72 
{\out 1. P} 

73 
{\out 2. Q} 

74 
\end{ttbox} 

75 
Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the 

76 
assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$. 

77 
\begin{ttbox} 

78 
major RS conjunct1; 

79 
{\out val it = "P [P & Q]" : thm} 

80 
\ttbreak 

81 
by (resolve_tac [major RS conjunct1] 1); 

82 
{\out Level 2} 

83 
{\out R} 

84 
{\out 1. Q} 

85 
\end{ttbox} 

86 
Similarly, we solve the subgoal involving~$Q$. 

87 
\begin{ttbox} 

88 
major RS conjunct2; 

89 
{\out val it = "Q [P & Q]" : thm} 

90 
by (resolve_tac [major RS conjunct2] 1); 

91 
{\out Level 3} 

92 
{\out R} 

93 
{\out No subgoals!} 

94 
\end{ttbox} 

95 
Calling \ttindex{topthm} returns the current proof state as a theorem. 

3103  96 
Note that it contains assumptions. Calling \ttindex{qed} discharges 
97 
the assumptions  both occurrences of $P\conj Q$ are discharged as 

98 
one  and makes the variables schematic. 

105  99 
\begin{ttbox} 
100 
topthm(); 

101 
{\out val it = "R [P & Q, P & Q, [ P; Q ] ==> R]" : thm} 

3103  102 
qed "conjE"; 
105  103 
{\out val conjE = "[ ?P & ?Q; [ ?P; ?Q ] ==> ?R ] ==> ?R" : thm} 
104 
\end{ttbox} 

105 

106 

107 
\subsection{Definitions and derived rules} \label{definitions} 

310  108 
\index{rules!derived}\index{definitions!and derived rules(} 
109 

105  110 
Definitions are expressed as metalevel equalities. Let us define negation 
111 
and the ifandonlyif connective: 

112 
\begin{eqnarray*} 

113 
\neg \Var{P} & \equiv & \Var{P}\imp\bot \\ 

114 
\Var{P}\bimp \Var{Q} & \equiv & 

115 
(\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P}) 

116 
\end{eqnarray*} 

331  117 
\index{metarewriting}% 
105  118 
Isabelle permits {\bf metalevel rewriting} using definitions such as 
119 
these. {\bf Unfolding} replaces every instance 

331  120 
of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For 
105  121 
example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to 
122 
\[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \] 

123 
{\bf Folding} a definition replaces occurrences of the righthand side by 

124 
the left. The occurrences need not be free in the entire formula. 

125 

126 
When you define new concepts, you should derive rules asserting their 

127 
abstract properties, and then forget their definitions. This supports 

331  128 
modularity: if you later change the definitions without affecting their 
105  129 
abstract properties, then most of your proofs will carry through without 
130 
change. Indiscriminate unfolding makes a subgoal grow exponentially, 

131 
becoming unreadable. 

132 

133 
Taking this point of view, Isabelle does not unfold definitions 

134 
automatically during proofs. Rewriting must be explicit and selective. 

135 
Isabelle provides tactics and metarules for rewriting, and a version of 

136 
the {\tt goal} command that unfolds the conclusion and premises of the rule 

137 
being derived. 

138 

139 
For example, the intuitionistic definition of negation given above may seem 

140 
peculiar. Using Isabelle, we shall derive pleasanter negation rules: 

141 
\[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad 

142 
\infer[({\neg}E)]{Q}{\neg P & P} \] 

296  143 
This requires proving the following metaformulae: 
3103  144 
$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$ 
145 
$$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$ 

105  146 

147 

296  148 
\subsection{Deriving the $\neg$ introduction rule} 
310  149 
To derive $(\neg I)$, we may call {\tt goal} with the appropriate 
105  150 
formula. Again, {\tt goal} returns a list consisting of the rule's 
296  151 
premises. We bind this oneelement list to the \ML\ identifier {\tt 
152 
prems}. 

105  153 
\begin{ttbox} 
154 
val prems = goal FOL.thy "(P ==> False) ==> ~P"; 

155 
{\out Level 0} 

156 
{\out ~P} 

157 
{\out 1. ~P} 

158 
{\out val prems = ["P ==> False [P ==> False]"] : thm list} 

159 
\end{ttbox} 

310  160 
Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the 
105  161 
definition of negation, unfolds that definition in the subgoals. It leaves 
162 
the main goal alone. 

163 
\begin{ttbox} 

164 
not_def; 

165 
{\out val it = "~?P == ?P > False" : thm} 

166 
by (rewrite_goals_tac [not_def]); 

167 
{\out Level 1} 

168 
{\out ~P} 

169 
{\out 1. P > False} 

170 
\end{ttbox} 

310  171 
Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality: 
105  172 
\begin{ttbox} 
173 
by (resolve_tac [impI] 1); 

174 
{\out Level 2} 

175 
{\out ~P} 

176 
{\out 1. P ==> False} 

177 
\ttbreak 

178 
by (resolve_tac prems 1); 

179 
{\out Level 3} 

180 
{\out ~P} 

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

182 
\end{ttbox} 

296  183 
The rest of the proof is routine. Note the form of the final result. 
105  184 
\begin{ttbox} 
185 
by (assume_tac 1); 

186 
{\out Level 4} 

187 
{\out ~P} 

188 
{\out No subgoals!} 

296  189 
\ttbreak 
3103  190 
qed "notI"; 
105  191 
{\out val notI = "(?P ==> False) ==> ~?P" : thm} 
192 
\end{ttbox} 

310  193 
\indexbold{*notI theorem} 
105  194 

195 
There is a simpler way of conducting this proof. The \ttindex{goalw} 

310  196 
command starts a backward proof, as does {\tt goal}, but it also 
296  197 
unfolds definitions. Thus there is no need to call 
198 
\ttindex{rewrite_goals_tac}: 

105  199 
\begin{ttbox} 
200 
val prems = goalw FOL.thy [not_def] 

201 
"(P ==> False) ==> ~P"; 

202 
{\out Level 0} 

203 
{\out ~P} 

204 
{\out 1. P > False} 

205 
{\out val prems = ["P ==> False [P ==> False]"] : thm list} 

206 
\end{ttbox} 

207 

208 

296  209 
\subsection{Deriving the $\neg$ elimination rule} 
284  210 
Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE} 
296  211 
above, with an additional step to unfold negation in the major premise. 
212 
Although the {\tt goalw} command is best for this, let us 

310  213 
try~{\tt goal} to see another way of unfolding definitions. After 
214 
binding the premises to \ML\ identifiers, we apply \tdx{FalseE}: 

105  215 
\begin{ttbox} 
216 
val [major,minor] = goal FOL.thy "[ ~P; P ] ==> R"; 

217 
{\out Level 0} 

218 
{\out R} 

219 
{\out 1. R} 

220 
{\out val major = "~ P [~ P]" : thm} 

221 
{\out val minor = "P [P]" : thm} 

222 
\ttbreak 

223 
by (resolve_tac [FalseE] 1); 

224 
{\out Level 1} 

225 
{\out R} 

226 
{\out 1. False} 

284  227 
\end{ttbox} 
228 
Everything follows from falsity. And we can prove falsity using the 

229 
premises and Modus Ponens: 

230 
\begin{ttbox} 

105  231 
by (resolve_tac [mp] 1); 
232 
{\out Level 2} 

233 
{\out R} 

234 
{\out 1. ?P1 > False} 

235 
{\out 2. ?P1} 

236 
\end{ttbox} 

237 
For subgoal~1, we transform the major premise from~$\neg P$ 

238 
to~${P\imp\bot}$. The function \ttindex{rewrite_rule}, given a list of 

296  239 
definitions, unfolds them in a theorem. Rewriting does not 
105  240 
affect the theorem's hypothesis, which remains~$\neg P$: 
241 
\begin{ttbox} 

242 
rewrite_rule [not_def] major; 

243 
{\out val it = "P > False [~P]" : thm} 

244 
by (resolve_tac [it] 1); 

245 
{\out Level 3} 

246 
{\out R} 

247 
{\out 1. P} 

248 
\end{ttbox} 

296  249 
The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove 
284  250 
using the minor premise: 
105  251 
\begin{ttbox} 
252 
by (resolve_tac [minor] 1); 

253 
{\out Level 4} 

254 
{\out R} 

255 
{\out No subgoals!} 

3103  256 
qed "notE"; 
105  257 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm} 
258 
\end{ttbox} 

310  259 
\indexbold{*notE theorem} 
105  260 

261 
\medskip 

284  262 
Again, there is a simpler way of conducting this proof. Recall that 
263 
the \ttindex{goalw} command unfolds definitions the conclusion; it also 

264 
unfolds definitions in the premises: 

105  265 
\begin{ttbox} 
266 
val [major,minor] = goalw FOL.thy [not_def] 

267 
"[ ~P; P ] ==> R"; 

268 
{\out val major = "P > False [~ P]" : thm} 

269 
{\out val minor = "P [P]" : thm} 

270 
\end{ttbox} 

296  271 
Observe the difference in {\tt major}; the premises are unfolded without 
272 
calling~\ttindex{rewrite_rule}. Incidentally, the four calls to 

273 
\ttindex{resolve_tac} above can be collapsed to one, with the help 

284  274 
of~\ttindex{RS}; this is a typical example of forward reasoning from a 
275 
complex premise. 

105  276 
\begin{ttbox} 
277 
minor RS (major RS mp RS FalseE); 

278 
{\out val it = "?P [P, ~P]" : thm} 

279 
by (resolve_tac [it] 1); 

280 
{\out Level 1} 

281 
{\out R} 

282 
{\out No subgoals!} 

283 
\end{ttbox} 

310  284 
\index{definitions!and derived rules)} 
105  285 

310  286 
\goodbreak\medskip\index{*"!"! symbol!in main goal} 
284  287 
Finally, here is a trick that is sometimes useful. If the goal 
105  288 
has an outermost metaquantifier, then \ttindex{goal} and \ttindex{goalw} 
284  289 
do not return the rule's premises in the list of theorems; instead, the 
290 
premises become assumptions in subgoal~1. 

291 
%%%It does not matter which variables are quantified over. 

105  292 
\begin{ttbox} 
293 
goalw FOL.thy [not_def] "!!P R. [ ~P; P ] ==> R"; 

294 
{\out Level 0} 

295 
{\out !!P R. [ ~ P; P ] ==> R} 

296 
{\out 1. !!P R. [ P > False; P ] ==> R} 

297 
val it = [] : thm list 

298 
\end{ttbox} 

299 
The proof continues as before. But instead of referring to \ML\ 

310  300 
identifiers, we refer to assumptions using {\tt eresolve_tac} or 
301 
{\tt assume_tac}: 

105  302 
\begin{ttbox} 
303 
by (resolve_tac [FalseE] 1); 

304 
{\out Level 1} 

305 
{\out !!P R. [ ~ P; P ] ==> R} 

306 
{\out 1. !!P R. [ P > False; P ] ==> False} 

307 
\ttbreak 

308 
by (eresolve_tac [mp] 1); 

309 
{\out Level 2} 

310 
{\out !!P R. [ ~ P; P ] ==> R} 

311 
{\out 1. !!P R. P ==> P} 

312 
\ttbreak 

313 
by (assume_tac 1); 

314 
{\out Level 3} 

315 
{\out !!P R. [ ~ P; P ] ==> R} 

316 
{\out No subgoals!} 

317 
\end{ttbox} 

3103  318 
Calling \ttindex{qed} strips the metaquantifiers, so the resulting 
105  319 
theorem is the same as before. 
320 
\begin{ttbox} 

3103  321 
qed "notE"; 
105  322 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm} 
323 
\end{ttbox} 

324 
Do not use the {\tt!!}\ trick if the premises contain metalevel 

325 
connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would 

326 
not be able to handle the resulting assumptions. The trick is not suitable 

327 
for deriving the introduction rule~$(\neg I)$. 

328 

329 

284  330 
\section{Defining theories}\label{sec:definingtheories} 
105  331 
\index{theories!defining(} 
310  332 

3103  333 
Isabelle makes no distinction between simple extensions of a logic  
334 
like specifying a type~$bool$ with constants~$true$ and~$false$  

335 
and defining an entire logic. A theory definition has a form like 

105  336 
\begin{ttbox} 
337 
\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) + 

338 
classes {\it class declarations} 

339 
default {\it sort} 

331  340 
types {\it type declarations and synonyms} 
3103  341 
arities {\it type arity declarations} 
105  342 
consts {\it constant declarations} 
3103  343 
syntax {\it syntactic constant declarations} 
344 
translations {\it ast translation rules} 

345 
defs {\it metalogical definitions} 

105  346 
rules {\it rule declarations} 
347 
end 

348 
ML {\it ML code} 

349 
\end{ttbox} 

350 
This declares the theory $T$ to extend the existing theories 

3103  351 
$S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities 
352 
(of existing types), constants and rules; it can specify the default 

353 
sort for type variables. A constant declaration can specify an 

354 
associated concrete syntax. The translations section specifies 

355 
rewrite rules on abstract syntax trees, handling notations and 

356 
abbreviations. \index{*ML section} The {\tt ML} section may contain 

357 
code to perform arbitrary syntactic transformations. The main 

3212  358 
declaration forms are discussed below. There are some more sections 
359 
not presented here, the full syntax can be found in 

360 
\iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference 

361 
Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that 

362 
objectlogics may add further theory sections, for example 

363 
\texttt{typedef}, \texttt{datatype} in \HOL. 

105  364 

3103  365 
All the declaration parts can be omitted or repeated and may appear in 
366 
any order, except that the {\ML} section must be last (after the {\tt 

367 
end} keyword). In the simplest case, $T$ is just the union of 

368 
$S@1$,~\ldots,~$S@n$. New theories always extend one or more other 

369 
theories, inheriting their types, constants, syntax, etc. The theory 

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

370 
\thydx{Pure} contains nothing but Isabelle's metalogic. The variant 
3103  371 
\thydx{CPure} offers the more usual higherorder function application 
3106  372 
syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure. 
105  373 

3103  374 
Each theory definition must reside in a separate file, whose name is 
375 
the theory's with {\tt.thy} appended. Calling 

376 
\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it 

377 
T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it 

378 
T}.thy.ML}, reads the latter file, and deletes it if no errors 

379 
occurred. This declares the {\ML} structure~$T$, which contains a 

380 
component {\tt thy} denoting the new theory, a component for each 

381 
rule, and everything declared in {\it ML code}. 

105  382 

3103  383 
Errors may arise during the translation to {\ML} (say, a misspelled 
384 
keyword) or during creation of the new theory (say, a type error in a 

385 
rule). But if all goes well, {\tt use_thy} will finally read the file 

386 
{\it T}{\tt.ML} (if it exists). This file typically contains proofs 

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

387 
that refer to the components of~$T$. The structure is automatically 
3103  388 
opened, so its components may be referred to by unqualified names, 
389 
e.g.\ just {\tt thy} instead of $T${\tt .thy}. 

105  390 

3103  391 
\ttindexbold{use_thy} automatically loads a theory's parents before 
392 
loading the theory itself. When a theory file is modified, many 

393 
theories may have to be reloaded. Isabelle records the modification 

394 
times and dependencies of theory files. See 

331  395 
\iflabelundefined{sec:reloadingtheories}{the {\em Reference Manual\/}}% 
396 
{\S\ref{sec:reloadingtheories}} 

296  397 
for more details. 
398 

105  399 

1084  400 
\subsection{Declaring constants, definitions and rules} 
310  401 
\indexbold{constants!declaring}\index{rules!declaring} 
402 

1084  403 
Most theories simply declare constants, definitions and rules. The {\bf 
404 
constant declaration part} has the form 

105  405 
\begin{ttbox} 
1387  406 
consts \(c@1\) :: \(\tau@1\) 
105  407 
\vdots 
1387  408 
\(c@n\) :: \(\tau@n\) 
105  409 
\end{ttbox} 
410 
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are 

1387  411 
types. The types must be enclosed in quotation marks if they contain 
412 
userdeclared infix type constructors like {\tt *}. Each 

105  413 
constant must be enclosed in quotation marks unless it is a valid 
414 
identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$, 

415 
the $n$ declarations may be abbreviated to a single line: 

416 
\begin{ttbox} 

1387  417 
\(c@1\), \ldots, \(c@n\) :: \(\tau\) 
105  418 
\end{ttbox} 
419 
The {\bf rule declaration part} has the form 

420 
\begin{ttbox} 

421 
rules \(id@1\) "\(rule@1\)" 

422 
\vdots 

423 
\(id@n\) "\(rule@n\)" 

424 
\end{ttbox} 

425 
where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots, 

284  426 
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be 
427 
enclosed in quotation marks. 

428 

3103  429 
\indexbold{definitions} The {\bf definition part} is similar, but with 
430 
the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are 

431 
rules of the form $s \equiv t$, and should serve only as 

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

432 
abbreviations. The simplest form of a definition is $f \equiv t$, 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3212
diff
changeset

433 
where $f$ is a constant. Also allowed are $\eta$equivalent forms of 
3106  434 
this, where the arguments of~$f$ appear applied on the lefthand side 
435 
of the equation instead of abstracted on the righthand side. 

1084  436 

3103  437 
Isabelle checks for common errors in definitions, such as extra 
438 
variables on the righthand side, but currently does not a complete 

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

439 
test of wellformedness. Thus determined users can write 
3103  440 
nonconservative `definitions' by using mutual recursion, for example; 
441 
the consequences of such actions are their responsibility. 

442 

443 
\index{examples!of theories} This example theory extends firstorder 

444 
logic by declaring and defining two constants, {\em nand} and {\em 

445 
xor}: 

284  446 
\begin{ttbox} 
105  447 
Gate = FOL + 
1387  448 
consts nand,xor :: [o,o] => o 
1084  449 
defs nand_def "nand(P,Q) == ~(P & Q)" 
105  450 
xor_def "xor(P,Q) == P & ~Q  ~P & Q" 
451 
end 

452 
\end{ttbox} 

453 

1649
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

454 
Declaring and defining constants can be combined: 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

455 
\begin{ttbox} 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

456 
Gate = FOL + 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

457 
constdefs nand :: [o,o] => o 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

458 
"nand(P,Q) == ~(P & Q)" 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

459 
xor :: [o,o] => o 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

460 
"xor(P,Q) == P & ~Q  ~P & Q" 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

461 
end 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

462 
\end{ttbox} 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

463 
{\tt constdefs} generates the names {\tt nand_def} and {\tt xor_def} 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3212
diff
changeset

464 
automatically, which is why it is restricted to alphanumeric identifiers. In 
1649
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

465 
general it has the form 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

466 
\begin{ttbox} 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

467 
constdefs \(id@1\) :: \(\tau@1\) 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

468 
"\(id@1 \equiv \dots\)" 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

469 
\vdots 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

470 
\(id@n\) :: \(\tau@n\) 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

471 
"\(id@n \equiv \dots\)" 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

472 
\end{ttbox} 
c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

473 

c4901f7161c5
Added 'constdefs' and extended the section on 'defs'
nipkow
parents:
1468
diff
changeset

474 

1366
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

475 
\begin{warn} 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

476 
A common mistake when writing definitions is to introduce extra free variables 
1468  477 
on the righthand side as in the following fictitious definition: 
1366
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

478 
\begin{ttbox} 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

479 
defs prime_def "prime(p) == (m divides p) > (m=1  m=p)" 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

480 
\end{ttbox} 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

481 
Isabelle rejects this ``definition'' because of the extra {\tt m} on the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3212
diff
changeset

482 
righthand side, which would introduce an inconsistency. What you should have 
1366
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

483 
written is 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

484 
\begin{ttbox} 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

485 
defs prime_def "prime(p) == ALL m. (m divides p) > (m=1  m=p)" 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

486 
\end{ttbox} 
3f3c25d3ec04
Inserted warning about defs with extra vars on rhs.
nipkow
parents:
1185
diff
changeset

487 
\end{warn} 
105  488 

489 
\subsection{Declaring type constructors} 

303  490 
\indexbold{types!declaring}\indexbold{arities!declaring} 
284  491 
% 
105  492 
Types are composed of type variables and {\bf type constructors}. Each 
284  493 
type constructor takes a fixed number of arguments. They are declared 
494 
with an \MLlike syntax. If $list$ takes one type argument, $tree$ takes 

495 
two arguments and $nat$ takes no arguments, then these type constructors 

496 
can be declared by 

105  497 
\begin{ttbox} 
284  498 
types 'a list 
499 
('a,'b) tree 

500 
nat 

105  501 
\end{ttbox} 
284  502 

503 
The {\bf type declaration part} has the general form 

504 
\begin{ttbox} 

505 
types \(tids@1\) \(id@1\) 

506 
\vdots 

841  507 
\(tids@n\) \(id@n\) 
284  508 
\end{ttbox} 
509 
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$ 

510 
are type argument lists as shown in the example above. It declares each 

511 
$id@i$ as a type constructor with the specified number of argument places. 

105  512 

513 
The {\bf arity declaration part} has the form 

514 
\begin{ttbox} 

515 
arities \(tycon@1\) :: \(arity@1\) 

516 
\vdots 

517 
\(tycon@n\) :: \(arity@n\) 

518 
\end{ttbox} 

519 
where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots, 

520 
$arity@n$ are arities. Arity declarations add arities to existing 

296  521 
types; they do not declare the types themselves. 
105  522 
In the simplest case, for an 0place type constructor, an arity is simply 
523 
the type's class. Let us declare a type~$bool$ of class $term$, with 

284  524 
constants $tt$ and~$ff$. (In firstorder logic, booleans are 
525 
distinct from formulae, which have type $o::logic$.) 

105  526 
\index{examples!of theories} 
284  527 
\begin{ttbox} 
105  528 
Bool = FOL + 
284  529 
types bool 
105  530 
arities bool :: term 
1387  531 
consts tt,ff :: bool 
105  532 
end 
533 
\end{ttbox} 

296  534 
A $k$place type constructor may have arities of the form 
535 
$(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class. 

536 
Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$, 

537 
where $c@1$, \dots,~$c@m$ are classes. Mostly we deal with singleton 

538 
sorts, and may abbreviate them by dropping the braces. The arity 

539 
$(term)term$ is short for $(\{term\})term$. Recall the discussion in 

540 
\S\ref{polymorphic}. 

105  541 

542 
A type constructor may be overloaded (subject to certain conditions) by 

296  543 
appearing in several arity declarations. For instance, the function type 
331  544 
constructor~$fun$ has the arity $(logic,logic)logic$; in higherorder 
105  545 
logic, it is declared also to have arity $(term,term)term$. 
546 

547 
Theory {\tt List} declares the 1place type constructor $list$, gives 

284  548 
it arity $(term)term$, and declares constants $Nil$ and $Cons$ with 
296  549 
polymorphic types:% 
550 
\footnote{In the {\tt consts} part, type variable {\tt'a} has the default 

551 
sort, which is {\tt term}. See the {\em Reference Manual\/} 

552 
\iflabelundefined{sec:refdefiningtheories}{}% 

553 
{(\S\ref{sec:refdefiningtheories})} for more information.} 

105  554 
\index{examples!of theories} 
284  555 
\begin{ttbox} 
105  556 
List = FOL + 
284  557 
types 'a list 
105  558 
arities list :: (term)term 
1387  559 
consts Nil :: 'a list 
560 
Cons :: ['a, 'a list] => 'a list 

105  561 
end 
562 
\end{ttbox} 

284  563 
Multiple arity declarations may be abbreviated to a single line: 
105  564 
\begin{ttbox} 
565 
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\) 

566 
\end{ttbox} 

567 

3103  568 
%\begin{warn} 
569 
%Arity declarations resemble constant declarations, but there are {\it no\/} 

570 
%quotation marks! Types and rules must be quoted because the theory 

571 
%translator passes them verbatim to the {\ML} output file. 

572 
%\end{warn} 

105  573 

331  574 
\subsection{Type synonyms}\indexbold{type synonyms} 
303  575 
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar 
307  576 
to those found in \ML. Such synonyms are defined in the type declaration part 
303  577 
and are fairly self explanatory: 
578 
\begin{ttbox} 

1387  579 
types gate = [o,o] => o 
580 
'a pred = 'a => o 

581 
('a,'b)nuf = 'b => 'a 

303  582 
\end{ttbox} 
583 
Type declarations and synonyms can be mixed arbitrarily: 

584 
\begin{ttbox} 

585 
types nat 

1387  586 
'a stream = nat => 'a 
587 
signal = nat stream 

303  588 
'a list 
589 
\end{ttbox} 

3103  590 
A synonym is merely an abbreviation for some existing type expression. 
591 
Hence synonyms may not be recursive! Internally all synonyms are 

592 
fully expanded. As a consequence Isabelle output never contains 

593 
synonyms. Their main purpose is to improve the readability of theory 

594 
definitions. Synonyms can be used just like any other type: 

303  595 
\begin{ttbox} 
1387  596 
consts and,or :: gate 
597 
negate :: signal => signal 

303  598 
\end{ttbox} 
599 

348  600 
\subsection{Infix and mixfix operators} 
310  601 
\index{infixes}\index{examples!of theories} 
602 

603 
Infix or mixfix syntax may be attached to constants. Consider the 

604 
following theory: 

284  605 
\begin{ttbox} 
105  606 
Gate2 = FOL + 
1387  607 
consts "~&" :: [o,o] => o (infixl 35) 
608 
"#" :: [o,o] => o (infixl 30) 

1084  609 
defs nand_def "P ~& Q == ~(P & Q)" 
105  610 
xor_def "P # Q == P & ~Q  ~P & Q" 
611 
end 

612 
\end{ttbox} 

310  613 
The constant declaration part declares two leftassociating infix operators 
614 
with their priorities, or precedences; they are $\nand$ of priority~35 and 

615 
$\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q) 

616 
\xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation 

617 
marks in \verb"~&" and \verb"#". 

105  618 

619 
The constants \hbox{\verbop ~&} and \hbox{\verbop #} are declared 

620 
automatically, just as in \ML. Hence you may write propositions like 

621 
\verbop #(True) == op ~&(True), which asserts that the functions $\lambda 

622 
Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical. 

623 

3212  624 
\medskip Infix syntax and constant names may be also specified 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3212
diff
changeset

625 
independently. For example, consider this version of $\nand$: 
3212  626 
\begin{ttbox} 
627 
consts nand :: [o,o] => o (infixl "~&" 35) 

628 
\end{ttbox} 

629 

310  630 
\bigskip\index{mixfix declarations} 
631 
{\bf Mixfix} operators may have arbitrary contextfree syntaxes. Let us 

632 
add a line to the constant declaration part: 

284  633 
\begin{ttbox} 
1387  634 
If :: [o,o,o] => o ("if _ then _ else _") 
105  635 
\end{ttbox} 
310  636 
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt 
296  637 
if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores 
310  638 
denote argument positions. 
105  639 

3103  640 
The declaration above does not allow the {\tt if}{\tt then}{\tt 
641 
else} construct to be printed split across several lines, even if it 

642 
is too long to fit on one line. Prettyprinting information can be 

643 
added to specify the layout of mixfix operators. For details, see 

310  644 
\iflabelundefined{DefiningLogics}% 
645 
{the {\it Reference Manual}, chapter `Defining Logics'}% 

646 
{Chap.\ts\ref{DefiningLogics}}. 

647 

648 
Mixfix declarations can be annotated with priorities, just like 

105  649 
infixes. The example above is just a shorthand for 
284  650 
\begin{ttbox} 
1387  651 
If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000) 
105  652 
\end{ttbox} 
310  653 
The numeric components determine priorities. The list of integers 
654 
defines, for each argument position, the minimal priority an expression 

655 
at that position must have. The final integer is the priority of the 

105  656 
construct itself. In the example above, any argument expression is 
310  657 
acceptable because priorities are nonnegative, and conditionals may 
658 
appear everywhere because 1000 is the highest priority. On the other 

659 
hand, the declaration 

284  660 
\begin{ttbox} 
1387  661 
If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99) 
105  662 
\end{ttbox} 
284  663 
defines concrete syntax for a conditional whose first argument cannot have 
310  664 
the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority 
665 
of at least~100. We may of course write 

284  666 
\begin{quote}\tt 
667 
if (if $P$ then $Q$ else $R$) then $S$ else $T$ 

156  668 
\end{quote} 
310  669 
because expressions in parentheses have maximal priority. 
105  670 

671 
Binary type constructors, like products and sums, may also be declared as 

672 
infixes. The type declaration below introduces a type constructor~$*$ with 

673 
infix notation $\alpha*\beta$, together with the mixfix notation 

1084  674 
${<}\_,\_{>}$ for pairs. We also see a rule declaration part. 
310  675 
\index{examples!of theories}\index{mixfix declarations} 
105  676 
\begin{ttbox} 
677 
Prod = FOL + 

284  678 
types ('a,'b) "*" (infixl 20) 
105  679 
arities "*" :: (term,term)term 
680 
consts fst :: "'a * 'b => 'a" 

681 
snd :: "'a * 'b => 'b" 

682 
Pair :: "['a,'b] => 'a * 'b" ("(1<_,/_>)") 

683 
rules fst "fst(<a,b>) = a" 

684 
snd "snd(<a,b>) = b" 

685 
end 

686 
\end{ttbox} 

687 

688 
\begin{warn} 

3103  689 
The name of the type constructor is~{\tt *} and not {\tt op~*}, as 
690 
it would be in the case of an infix constant. Only infix type 

691 
constructors can have symbolic names like~{\tt *}. General mixfix 

692 
syntax for types may be introduced via appropriate {\tt syntax} 

693 
declarations. 

105  694 
\end{warn} 
695 

696 

697 
\subsection{Overloading} 

698 
\index{overloading}\index{examples!of theories} 

699 
The {\bf class declaration part} has the form 

700 
\begin{ttbox} 

701 
classes \(id@1\) < \(c@1\) 

702 
\vdots 

703 
\(id@n\) < \(c@n\) 

704 
\end{ttbox} 

705 
where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are 

706 
existing classes. It declares each $id@i$ as a new class, a subclass 

707 
of~$c@i$. In the general case, an identifier may be declared to be a 

708 
subclass of $k$ existing classes: 

709 
\begin{ttbox} 

710 
\(id\) < \(c@1\), \ldots, \(c@k\) 

711 
\end{ttbox} 

296  712 
Type classes allow constants to be overloaded. As suggested in 
307  713 
\S\ref{polymorphic}, let us define the class $arith$ of arithmetic 
296  714 
types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::} 
715 
\alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of 

716 
$term$ and add the three polymorphic constants of this class. 

310  717 
\index{examples!of theories}\index{constants!overloaded} 
105  718 
\begin{ttbox} 
719 
Arith = FOL + 

720 
classes arith < term 

1387  721 
consts "0" :: 'a::arith ("0") 
722 
"1" :: 'a::arith ("1") 

723 
"+" :: ['a::arith,'a] => 'a (infixl 60) 

105  724 
end 
725 
\end{ttbox} 

726 
No rules are declared for these constants: we merely introduce their 

727 
names without specifying properties. On the other hand, classes 

728 
with rules make it possible to prove {\bf generic} theorems. Such 

729 
theorems hold for all instances, all types in that class. 

730 

731 
We can now obtain distinct versions of the constants of $arith$ by 

732 
declaring certain types to be of class $arith$. For example, let us 

733 
declare the 0place type constructors $bool$ and $nat$: 

734 
\index{examples!of theories} 

735 
\begin{ttbox} 

736 
BoolNat = Arith + 

348  737 
types bool nat 
738 
arities bool, nat :: arith 

1387  739 
consts Suc :: nat=>nat 
284  740 
\ttbreak 
105  741 
rules add0 "0 + n = n::nat" 
742 
addS "Suc(m)+n = Suc(m+n)" 

743 
nat1 "1 = Suc(0)" 

744 
or0l "0 + x = x::bool" 

745 
or0r "x + 0 = x::bool" 

746 
or1l "1 + x = 1::bool" 

747 
or1r "x + 1 = 1::bool" 

748 
end 

749 
\end{ttbox} 

750 
Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at 

751 
either type. The type constraints in the axioms are vital. Without 

752 
constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$ 

753 
and the axiom would hold for any type of class $arith$. This would 

284  754 
collapse $nat$ to a trivial type: 
105  755 
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \] 
296  756 

105  757 

296  758 
\section{Theory example: the natural numbers} 
759 

760 
We shall now work through a small example of formalized mathematics 

105  761 
demonstrating many of the theory extension features. 
762 

763 

764 
\subsection{Extending firstorder logic with the natural numbers} 

765 
\index{examples!of theories} 

766 

284  767 
Section\ts\ref{sec:logicalsyntax} has formalized a firstorder logic, 
768 
including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$. 

769 
Let us introduce the Peano axioms for mathematical induction and the 

310  770 
freeness of $0$ and~$Suc$:\index{axioms!Peano} 
307  771 
\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} 
105  772 
\qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$} 
773 
\] 

774 
\[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad 

775 
\infer[(Suc\_neq\_0)]{R}{Suc(m)=0} 

776 
\] 

777 
Mathematical induction asserts that $P(n)$ is true, for any $n::nat$, 

778 
provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$. 

779 
Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$. 

780 
To avoid making induction require the presence of other connectives, we 

781 
formalize mathematical induction as 

782 
$$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$ 

783 

784 
\noindent 

785 
Similarly, to avoid expressing the other rules using~$\forall$, $\imp$ 

786 
and~$\neg$, we take advantage of the metalogic;\footnote 

787 
{On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$ 

788 
and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work 

789 
better with Isabelle's simplifier.} 

790 
$(Suc\_neq\_0)$ is 

791 
an elimination rule for $Suc(m)=0$: 

792 
$$ Suc(m)=Suc(n) \Imp m=n \eqno(Suc\_inject) $$ 

793 
$$ Suc(m)=0 \Imp R \eqno(Suc\_neq\_0) $$ 

794 

795 
\noindent 

796 
We shall also define a primitive recursion operator, $rec$. Traditionally, 

797 
primitive recursion takes a natural number~$a$ and a 2place function~$f$, 

798 
and obeys the equations 

799 
\begin{eqnarray*} 

800 
rec(0,a,f) & = & a \\ 

801 
rec(Suc(m),a,f) & = & f(m, rec(m,a,f)) 

802 
\end{eqnarray*} 

803 
Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$, 

804 
should satisfy 

805 
\begin{eqnarray*} 

806 
0+n & = & n \\ 

807 
Suc(m)+n & = & Suc(m+n) 

808 
\end{eqnarray*} 

296  809 
Primitive recursion appears to pose difficulties: firstorder logic has no 
810 
functionvalued expressions. We again take advantage of the metalogic, 

811 
which does have functions. We also generalise primitive recursion to be 

105  812 
polymorphic over any type of class~$term$, and declare the addition 
813 
function: 

814 
\begin{eqnarray*} 

815 
rec & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\ 

816 
+ & :: & [nat,nat]\To nat 

817 
\end{eqnarray*} 

818 

819 

820 
\subsection{Declaring the theory to Isabelle} 

821 
\index{examples!of theories} 

310  822 
Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$, 
105  823 
which contains only classical logic with no natural numbers. We declare 
307  824 
the 0place type constructor $nat$ and the associated constants. Note that 
825 
the constant~0 requires a mixfix annotation because~0 is not a legal 

826 
identifier, and could not otherwise be written in terms: 

310  827 
\begin{ttbox}\index{mixfix declarations} 
105  828 
Nat = FOL + 
284  829 
types nat 
105  830 
arities nat :: term 
1387  831 
consts "0" :: nat ("0") 
832 
Suc :: nat=>nat 

833 
rec :: [nat, 'a, [nat,'a]=>'a] => 'a 

834 
"+" :: [nat, nat] => nat (infixl 60) 

296  835 
rules Suc_inject "Suc(m)=Suc(n) ==> m=n" 
105  836 
Suc_neq_0 "Suc(m)=0 ==> R" 
296  837 
induct "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)" 
105  838 
rec_0 "rec(0,a,f) = a" 
839 
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" 

296  840 
add_def "m+n == rec(m, n, \%x y. Suc(y))" 
105  841 
end 
842 
\end{ttbox} 

843 
In axiom {\tt add_def}, recall that \verb% stands for~$\lambda$. 

296  844 
Loading this theory file creates the \ML\ structure {\tt Nat}, which 
3103  845 
contains the theory and axioms. 
296  846 

847 
\subsection{Proving some recursion equations} 

331  848 
File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the 
105  849 
natural numbers. As a trivial example, let us derive recursion equations 
850 
for \verb$+$. Here is the zero case: 

284  851 
\begin{ttbox} 
105  852 
goalw Nat.thy [add_def] "0+n = n"; 
853 
{\out Level 0} 

854 
{\out 0 + n = n} 

284  855 
{\out 1. rec(0,n,\%x y. Suc(y)) = n} 
105  856 
\ttbreak 
857 
by (resolve_tac [rec_0] 1); 

858 
{\out Level 1} 

859 
{\out 0 + n = n} 

860 
{\out No subgoals!} 

3103  861 
qed "add_0"; 
284  862 
\end{ttbox} 
105  863 
And here is the successor case: 
284  864 
\begin{ttbox} 
105  865 
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)"; 
866 
{\out Level 0} 

867 
{\out Suc(m) + n = Suc(m + n)} 

284  868 
{\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))} 
105  869 
\ttbreak 
870 
by (resolve_tac [rec_Suc] 1); 

871 
{\out Level 1} 

872 
{\out Suc(m) + n = Suc(m + n)} 

873 
{\out No subgoals!} 

3103  874 
qed "add_Suc"; 
284  875 
\end{ttbox} 
105  876 
The induction rule raises some complications, which are discussed next. 
877 
\index{theories!defining)} 

878 

879 

880 
\section{Refinement with explicit instantiation} 

310  881 
\index{resolution!with instantiation} 
882 
\index{instantiation(} 

883 

105  884 
In order to employ mathematical induction, we need to refine a subgoal by 
885 
the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$, 

886 
which is highly ambiguous in higherorder unification. It matches every 

887 
way that a formula can be regarded as depending on a subterm of type~$nat$. 

888 
To get round this problem, we could make the induction rule conclude 

889 
$\forall n.\Var{P}(n)$  but putting a subgoal into this form requires 

890 
refinement by~$(\forall E)$, which is equally hard! 

891 

892 
The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by 

893 
a rule. But it also accepts explicit instantiations for the rule's 

894 
schematic variables. 

895 
\begin{description} 

310  896 
\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}] 
105  897 
instantiates the rule {\it thm} with the instantiations {\it insts}, and 
898 
then performs resolution on subgoal~$i$. 

899 

310  900 
\item[\ttindex{eres_inst_tac}] 
901 
and \ttindex{dres_inst_tac} are similar, but perform elimresolution 

105  902 
and destructresolution, respectively. 
903 
\end{description} 

904 
The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$, 

905 
where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule  

307  906 
with no leading question marks!  and $e@1$, \ldots, $e@n$ are 
105  907 
expressions giving their instantiations. The expressions are typechecked 
908 
in the context of a particular subgoal: free variables receive the same 

909 
types as they have in the subgoal, and parameters may appear. Type 

910 
variable instantiations may appear in~{\it insts}, but they are seldom 

911 
required: {\tt res_inst_tac} instantiates type variables automatically 

912 
whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$. 

913 

914 
\subsection{A simple proof by induction} 

310  915 
\index{examples!of induction} 
105  916 
Let us prove that no natural number~$k$ equals its own successor. To 
917 
use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good 

918 
instantiation for~$\Var{P}$. 

284  919 
\begin{ttbox} 
105  920 
goal Nat.thy "~ (Suc(k) = k)"; 
921 
{\out Level 0} 

459  922 
{\out Suc(k) ~= k} 
923 
{\out 1. Suc(k) ~= k} 

105  924 
\ttbreak 
925 
by (res_inst_tac [("n","k")] induct 1); 

926 
{\out Level 1} 

459  927 
{\out Suc(k) ~= k} 
928 
{\out 1. Suc(0) ~= 0} 

929 
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} 

284  930 
\end{ttbox} 
105  931 
We should check that Isabelle has correctly applied induction. Subgoal~1 
932 
is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step, 

933 
with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$. 

310  934 
The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the 
935 
other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}: 

284  936 
\begin{ttbox} 
105  937 
by (resolve_tac [notI] 1); 
938 
{\out Level 2} 

459  939 
{\out Suc(k) ~= k} 
105  940 
{\out 1. Suc(0) = 0 ==> False} 
459  941 
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} 
105  942 
\ttbreak 
943 
by (eresolve_tac [Suc_neq_0] 1); 

944 
{\out Level 3} 

459  945 
{\out Suc(k) ~= k} 
946 
{\out 1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} 

284  947 
\end{ttbox} 
105  948 
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}. 
284  949 
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from 
950 
$Suc(Suc(x)) = Suc(x)$: 

951 
\begin{ttbox} 

105  952 
by (resolve_tac [notI] 1); 
953 
{\out Level 4} 

459  954 
{\out Suc(k) ~= k} 
955 
{\out 1. !!x. [ Suc(x) ~= x; Suc(Suc(x)) = Suc(x) ] ==> False} 

105  956 
\ttbreak 
957 
by (eresolve_tac [notE] 1); 

958 
{\out Level 5} 

459  959 
{\out Suc(k) ~= k} 
105  960 
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x} 
961 
\ttbreak 

962 
by (eresolve_tac [Suc_inject] 1); 

963 
{\out Level 6} 

459  964 
{\out Suc(k) ~= k} 
105  965 
{\out No subgoals!} 
284  966 
\end{ttbox} 
105  967 

968 

969 
\subsection{An example of ambiguity in {\tt resolve_tac}} 

970 
\index{examples!of induction}\index{unification!higherorder} 

971 
If you try the example above, you may observe that {\tt res_inst_tac} is 

972 
not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right 

973 
instantiation for~$(induct)$ to yield the desired next state. With more 

974 
complex formulae, our luck fails. 

284  975 
\begin{ttbox} 
105  976 
goal Nat.thy "(k+m)+n = k+(m+n)"; 
977 
{\out Level 0} 

978 
{\out k + m + n = k + (m + n)} 

979 
{\out 1. k + m + n = k + (m + n)} 

980 
\ttbreak 

981 
by (resolve_tac [induct] 1); 

982 
{\out Level 1} 

983 
{\out k + m + n = k + (m + n)} 

984 
{\out 1. k + m + n = 0} 

985 
{\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)} 

284  986 
\end{ttbox} 
987 
This proof requires induction on~$k$. The occurrence of~0 in subgoal~1 

988 
indicates that induction has been applied to the term~$k+(m+n)$; this 

989 
application is sound but will not lead to a proof here. Fortunately, 

990 
Isabelle can (lazily!) generate all the valid applications of induction. 

991 
The \ttindex{back} command causes backtracking to an alternative outcome of 

992 
the tactic. 

993 
\begin{ttbox} 

105  994 
back(); 
995 
{\out Level 1} 

996 
{\out k + m + n = k + (m + n)} 

997 
{\out 1. k + m + n = k + 0} 

998 
{\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)} 

284  999 
\end{ttbox} 
1000 
Now induction has been applied to~$m+n$. This is equally useless. Let us 

1001 
call \ttindex{back} again. 

1002 
\begin{ttbox} 

105  1003 
back(); 
1004 
{\out Level 1} 

1005 
{\out k + m + n = k + (m + n)} 

1006 
{\out 1. k + m + 0 = k + (m + 0)} 

284  1007 
{\out 2. !!x. k + m + x = k + (m + x) ==>} 
1008 
{\out k + m + Suc(x) = k + (m + Suc(x))} 

1009 
\end{ttbox} 

105  1010 
Now induction has been applied to~$n$. What is the next alternative? 
284  1011 
\begin{ttbox} 
105  1012 
back(); 
1013 
{\out Level 1} 

1014 
{\out k + m + n = k + (m + n)} 

1015 
{\out 1. k + m + n = k + (m + 0)} 

1016 
{\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))} 

284  1017 
\end{ttbox} 
105  1018 
Inspecting subgoal~1 reveals that induction has been applied to just the 
1019 
second occurrence of~$n$. This perfectly legitimate induction is useless 

310  1020 
here. 
1021 

1022 
The main goal admits fourteen different applications of induction. The 

1023 
number is exponential in the size of the formula. 

105  1024 

1025 
\subsection{Proving that addition is associative} 

331  1026 
Let us invoke the induction rule properly, using~{\tt 
310  1027 
res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's 
1028 
simplification tactics, which are described in 

1029 
\iflabelundefined{simpchap}% 

1030 
{the {\em Reference Manual}}{Chap.\ts\ref{simpchap}}. 

284  1031 

310  1032 
\index{simplification}\index{examples!of simplification} 
1033 

3114  1034 
Isabelle's simplification tactics repeatedly apply equations to a 
1035 
subgoal, perhaps proving it. For efficiency, the rewrite rules must 

1036 
be packaged into a {\bf simplification set},\index{simplification 

1037 
sets} or {\bf simpset}. We augment the implicit simpset of {\FOL} 

1038 
with the equations proved in the previous section, namely $0+n=n$ and 

1039 
${\tt Suc}(m)+n={\tt Suc}(m+n)$: 

284  1040 
\begin{ttbox} 
3114  1041 
Addsimps [add_0, add_Suc]; 
284  1042 
\end{ttbox} 
105  1043 
We state the goal for associativity of addition, and 
1044 
use \ttindex{res_inst_tac} to invoke induction on~$k$: 

284  1045 
\begin{ttbox} 
105  1046 
goal Nat.thy "(k+m)+n = k+(m+n)"; 
1047 
{\out Level 0} 

1048 
{\out k + m + n = k + (m + n)} 

1049 
{\out 1. k + m + n = k + (m + n)} 

1050 
\ttbreak 

1051 
by (res_inst_tac [("n","k")] induct 1); 

1052 
{\out Level 1} 

1053 
{\out k + m + n = k + (m + n)} 

1054 
{\out 1. 0 + m + n = 0 + (m + n)} 

284  1055 
{\out 2. !!x. x + m + n = x + (m + n) ==>} 
1056 
{\out Suc(x) + m + n = Suc(x) + (m + n)} 

1057 
\end{ttbox} 

105  1058 
The base case holds easily; both sides reduce to $m+n$. The 
3114  1059 
tactic~\ttindex{Simp_tac} rewrites with respect to the current 
1060 
simplification set, applying the rewrite rules for addition: 

284  1061 
\begin{ttbox} 
3114  1062 
by (Simp_tac 1); 
105  1063 
{\out Level 2} 
1064 
{\out k + m + n = k + (m + n)} 

284  1065 
{\out 1. !!x. x + m + n = x + (m + n) ==>} 
1066 
{\out Suc(x) + m + n = Suc(x) + (m + n)} 

1067 
\end{ttbox} 

331  1068 
The inductive step requires rewriting by the equations for addition 
105  1069 
together the induction hypothesis, which is also an equation. The 
3114  1070 
tactic~\ttindex{Asm_simp_tac} rewrites using the implicit 
1071 
simplification set and any useful assumptions: 

284  1072 
\begin{ttbox} 
3114  1073 
by (Asm_simp_tac 1); 
105  1074 
{\out Level 3} 
1075 
{\out k + m + n = k + (m + n)} 

1076 
{\out No subgoals!} 

284  1077 
\end{ttbox} 
310  1078 
\index{instantiation)} 
105  1079 

1080 

284  1081 
\section{A Prolog interpreter} 
105  1082 
\index{Prolog interpreterbold} 
284  1083 
To demonstrate the power of tacticals, let us construct a Prolog 
105  1084 
interpreter and execute programs involving lists.\footnote{To run these 
331  1085 
examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program 
105  1086 
consists of a theory. We declare a type constructor for lists, with an 
1087 
arity declaration to say that $(\tau)list$ is of class~$term$ 

1088 
provided~$\tau$ is: 

1089 
\begin{eqnarray*} 

1090 
list & :: & (term)term 

1091 
\end{eqnarray*} 

1092 
We declare four constants: the empty list~$Nil$; the infix list 

1093 
constructor~{:}; the list concatenation predicate~$app$; the list reverse 

284  1094 
predicate~$rev$. (In Prolog, functions on lists are expressed as 
105  1095 
predicates.) 
1096 
\begin{eqnarray*} 

1097 
Nil & :: & \alpha list \\ 

1098 
{:} & :: & [\alpha,\alpha list] \To \alpha list \\ 

1099 
app & :: & [\alpha list,\alpha list,\alpha list] \To o \\ 

1100 
rev & :: & [\alpha list,\alpha list] \To o 

1101 
\end{eqnarray*} 

284  1102 
The predicate $app$ should satisfy the Prologstyle rules 
105  1103 
\[ {app(Nil,ys,ys)} \qquad 
1104 
{app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \] 

1105 
We define the naive version of $rev$, which calls~$app$: 

1106 
\[ {rev(Nil,Nil)} \qquad 

1107 
{rev(xs,ys)\quad app(ys, x:Nil, zs) \over 

1108 
rev(x:xs, zs)} 

1109 
\] 

1110 

1111 
\index{examples!of theories} 

310  1112 
Theory \thydx{Prolog} extends firstorder logic in order to make use 
105  1113 
of the class~$term$ and the type~$o$. The interpreter does not use the 
310  1114 
rules of~{\tt FOL}. 
105  1115 
\begin{ttbox} 
1116 
Prolog = FOL + 

296  1117 
types 'a list 
105  1118 
arities list :: (term)term 
1387  1119 
consts Nil :: 'a list 
1120 
":" :: ['a, 'a list]=> 'a list (infixr 60) 

1121 
app :: ['a list, 'a list, 'a list] => o 

1122 
rev :: ['a list, 'a list] => o 

105  1123 
rules appNil "app(Nil,ys,ys)" 
1124 
appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" 

1125 
revNil "rev(Nil,Nil)" 

1126 
revCons "[ rev(xs,ys); app(ys,x:Nil,zs) ] ==> rev(x:xs,zs)" 

1127 
end 

1128 
\end{ttbox} 

1129 
\subsection{Simple executions} 

284  1130 
Repeated application of the rules solves Prolog goals. Let us 
105  1131 
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the 
1132 
answer builds up in~{\tt ?x}. 

1133 
\begin{ttbox} 

1134 
goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)"; 

1135 
{\out Level 0} 

1136 
{\out app(a : b : c : Nil, d : e : Nil, ?x)} 

1137 
{\out 1. app(a : b : c : Nil, d : e : Nil, ?x)} 

1138 
\ttbreak 

1139 
by (resolve_tac [appNil,appCons] 1); 

1140 
{\out Level 1} 

1141 
{\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)} 

1142 
{\out 1. app(b : c : Nil, d : e : Nil, ?zs1)} 

1143 
\ttbreak 

1144 
by (resolve_tac [appNil,appCons] 1); 

1145 
{\out Level 2} 

1146 
{\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)} 

1147 
{\out 1. app(c : Nil, d : e : Nil, ?zs2)} 

1148 
\end{ttbox} 

1149 
At this point, the first two elements of the result are~$a$ and~$b$. 

1150 
\begin{ttbox} 

1151 
by (resolve_tac [appNil,appCons] 1); 

1152 
{\out Level 3} 

1153 
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)} 

1154 
{\out 1. app(Nil, d : e : Nil, ?zs3)} 

1155 
\ttbreak 

1156 
by (resolve_tac [appNil,appCons] 1); 

1157 
{\out Level 4} 

1158 
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)} 

1159 
{\out No subgoals!} 

1160 
\end{ttbox} 

1161 

284  1162 
Prolog can run functions backwards. Which list can be appended 
105  1163 
with $[c,d]$ to produce $[a,b,c,d]$? 
1164 
Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$: 

1165 
\begin{ttbox} 

1166 
goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)"; 

1167 
{\out Level 0} 

1168 
{\out app(?x, c : d : Nil, a : b : c : d : Nil)} 

1169 
{\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)} 

1170 
\ttbreak 

1171 
by (REPEAT (resolve_tac [appNil,appCons] 1)); 

1172 
{\out Level 1} 

1173 
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)} 

1174 
{\out No subgoals!} 

1175 
\end{ttbox} 

1176 

1177 

310  1178 
\subsection{Backtracking}\index{backtracking!Prolog style} 
296  1179 
Prolog backtracking can answer questions that have multiple solutions. 
1180 
Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This 

1181 
question has five solutions. Using \ttindex{REPEAT} to apply the rules, we 

1182 
quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$: 

105  1183 
\begin{ttbox} 
1184 
goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)"; 

1185 
{\out Level 0} 

1186 
{\out app(?x, ?y, a : b : c : d : Nil)} 

1187 
{\out 1. app(?x, ?y, a : b : c : d : Nil)} 

1188 
\ttbreak 

1189 
by (REPEAT (resolve_tac [appNil,appCons] 1)); 

1190 
{\out Level 1} 

1191 
{\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)} 

1192 
{\out No subgoals!} 

1193 
\end{ttbox} 

284  1194 
Isabelle can lazily generate all the possibilities. The \ttindex{back} 
1195 
command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$: 

105  1196 
\begin{ttbox} 
1197 
back(); 

1198 
{\out Level 1} 

1199 
{\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)} 

1200 
{\out No subgoals!} 

1201 
\end{ttbox} 

1202 
The other solutions are generated similarly. 

1203 
\begin{ttbox} 

1204 
back(); 

1205 
{\out Level 1} 

1206 
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)} 

1207 
{\out No subgoals!} 

1208 
\ttbreak 

1209 
back(); 

1210 
{\out Level 1} 

1211 
{\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)} 

1212 
{\out No subgoals!} 

1213 
\ttbreak 

1214 
back(); 

1215 
{\out Level 1} 

1216 
{\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)} 

1217 
{\out No subgoals!} 

1218 
\end{ttbox} 

1219 

1220 

1221 
\subsection{Depthfirst search} 

1222 
\index{search!depthfirst} 

1223 
Now let us try $rev$, reversing a list. 

1224 
Bundle the rules together as the \ML{} identifier {\tt rules}. Naive 

1225 
reverse requires 120 inferences for this 14element list, but the tactic 

1226 
terminates in a few seconds. 

1227 
\begin{ttbox} 

1228 
goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; 

1229 
{\out Level 0} 

1230 
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)} 

284  1231 
{\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,} 
1232 
{\out ?w)} 

1233 
\ttbreak 

105  1234 
val rules = [appNil,appCons,revNil,revCons]; 
1235 
\ttbreak 

1236 
by (REPEAT (resolve_tac rules 1)); 

1237 
{\out Level 1} 

1238 
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,} 

1239 
{\out n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)} 

1240 
{\out No subgoals!} 

1241 
\end{ttbox} 

1242 
We may execute $rev$ backwards. This, too, should reverse a list. What 

1243 
is the reverse of $[a,b,c]$? 

1244 
\begin{ttbox} 

1245 
goal Prolog.thy "rev(?x, a:b:c:Nil)"; 

1246 
{\out Level 0} 

1247 
{\out rev(?x, a : b : c : Nil)} 

1248 
{\out 1. rev(?x, a : b : c : Nil)} 

1249 
\ttbreak 

1250 
by (REPEAT (resolve_tac rules 1)); 

1251 
{\out Level 1} 

1252 
{\out rev(?x1 : Nil, a : b : c : Nil)} 

1253 
{\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)} 

1254 
\end{ttbox} 

1255 
The tactic has failed to find a solution! It reached a dead end at 

331  1256 
subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$ 
105  1257 
equals~$[a,b,c]$. Backtracking explores other outcomes. 
1258 
\begin{ttbox} 

1259 
back(); 

1260 
{\out Level 1} 

1261 
{\out rev(?x1 : a : Nil, a : b : c : Nil)} 

1262 
{\out 1. app(Nil, ?x1 : Nil, b : c : Nil)} 

1263 
\end{ttbox} 

1264 
This too is a dead end, but the next outcome is successful. 

1265 
\begin{ttbox} 

1266 
back(); 

1267 
{\out Level 1} 

1268 
{\out rev(c : b : a : Nil, a : b : c : Nil)} 

1269 
{\out No subgoals!} 

1270 
\end{ttbox} 

310  1271 
\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a 
1272 
search tactical. {\tt REPEAT} stops when it cannot continue, regardless of 

1273 
which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a 

1274 
satisfactory state, as specified by an \ML{} predicate. Below, 

105  1275 
\ttindex{has_fewer_prems} specifies that the proof state should have no 
310  1276 
subgoals. 
105  1277 
\begin{ttbox} 
1278 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 

1279 
(resolve_tac rules 1); 

1280 
\end{ttbox} 

284  1281 
Since Prolog uses depthfirst search, this tactic is a (slow!) 
296  1282 
Prolog interpreter. We return to the start of the proof using 
1283 
\ttindex{choplev}, and apply {\tt prolog_tac}: 

105  1284 
\begin{ttbox} 
1285 
choplev 0; 

1286 
{\out Level 0} 

1287 
{\out rev(?x, a : b : c : Nil)} 

1288 
{\out 1. rev(?x, a : b : c : Nil)} 

1289 
\ttbreak 

1290 
by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1)); 

1291 
{\out Level 1} 

1292 
{\out rev(c : b : a : Nil, a : b : c : Nil)} 

1293 
{\out No subgoals!} 

1294 
\end{ttbox} 

1295 
Let us try {\tt prolog_tac} on one more example, containing four unknowns: 

1296 
\begin{ttbox} 

1297 
goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; 

1298 
{\out Level 0} 

1299 
{\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} 

1300 
{\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} 

1301 
\ttbreak 

1302 
by prolog_tac; 

1303 
{\out Level 1} 

1304 
{\out rev(a : b : c : d : Nil, d : c : b : a : Nil)} 

1305 
{\out No subgoals!} 

1306 
\end{ttbox} 

284  1307 
Although Isabelle is much slower than a Prolog system, Isabelle 
156  1308 
tactics can exploit logic programming techniques. 
1309 