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

5205  8 
(\texttt{FOL} or~\texttt{LK}). Try working some of the examples provided, 
9 
and others from the literature. Set theory~(\texttt{ZF}) and 

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

3103  11 
mathematical reasoning and, again, many examples are in the 
5205  12 
literature. Higherorder logic~(\texttt{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 
5205  40 
\S\ref{deriving}. When the \ttindex{Goal} command is supplied a formula of 
41 
the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two 

42 
possibilities: 

43 
\begin{itemize} 

44 
\item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple 

45 
formulae{} (they do not involve the metaconnectives $\Forall$ or 

46 
$\Imp$) then the command sets the goal to be 

47 
$\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list. 

48 
\item If one or more premises involves the metaconnectives $\Forall$ or 

49 
$\Imp$, then the command sets the goal to be $\phi$ and returns a list 

50 
consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. 

51 
These metaassumptions are also recorded internally, allowing 

52 
\texttt{result} (which is called by \texttt{qed}) to discharge them in the 

53 
original order. 

54 
\end{itemize} 

55 
Rules that discharge assumptions or introduce eigenvariables have complex 

56 
premises, and the second case applies. 

105  57 

5205  58 
Let us derive $\conj$ elimination. Until now, calling \texttt{Goal} has 
59 
returned an empty list, which we have ignored. In this example, the list 

60 
contains the two premises of the rule, since one of them involves the $\Imp$ 

61 
connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt 

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

63 
not exhaustive}. This warns that \texttt{Goal} must return a 2element 

64 
list. Otherwise, the patternmatch will fail; ML will raise exception 

65 
\xdx{Match}.} 

105  66 
\begin{ttbox} 
5205  67 
val [major,minor] = Goal 
105  68 
"[ P&Q; [ P; Q ] ==> R ] ==> R"; 
69 
{\out Level 0} 

70 
{\out R} 

71 
{\out 1. R} 

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

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

74 
\end{ttbox} 

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

5205  76 
shown in brackets. Using \texttt{minor}, we reduce $R$ to the subgoals 
105  77 
$P$ and~$Q$: 
78 
\begin{ttbox} 

79 
by (resolve_tac [minor] 1); 

80 
{\out Level 1} 

81 
{\out R} 

82 
{\out 1. P} 

83 
{\out 2. Q} 

84 
\end{ttbox} 

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

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

87 
\begin{ttbox} 

88 
major RS conjunct1; 

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

90 
\ttbreak 

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

92 
{\out Level 2} 

93 
{\out R} 

94 
{\out 1. Q} 

95 
\end{ttbox} 

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

97 
\begin{ttbox} 

98 
major RS conjunct2; 

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

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

101 
{\out Level 3} 

102 
{\out R} 

103 
{\out No subgoals!} 

104 
\end{ttbox} 

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

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

108 
one  and makes the variables schematic. 

105  109 
\begin{ttbox} 
110 
topthm(); 

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

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

115 

116 

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

310  118 
\index{rules!derived}\index{definitions!and derived rules(} 
119 

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

122 
\begin{eqnarray*} 

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

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

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

126 
\end{eqnarray*} 

331  127 
\index{metarewriting}% 
105  128 
Isabelle permits {\bf metalevel rewriting} using definitions such as 
129 
these. {\bf Unfolding} replaces every instance 

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

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

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

135 

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

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

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

141 
becoming unreadable. 

142 

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

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

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

5205  146 
the \texttt{Goal} command that unfolds the conclusion and premises of the rule 
105  147 
being derived. 
148 

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

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

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

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

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

105  156 

157 

296  158 
\subsection{Deriving the $\neg$ introduction rule} 
5205  159 
To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula. 
160 
Again, the rule's premises involve a metaconnective, and \texttt{Goal} 

161 
returns oneelement list. We bind this list to the \ML\ identifier \texttt{prems}. 

105  162 
\begin{ttbox} 
5205  163 
val prems = Goal "(P ==> False) ==> ~P"; 
105  164 
{\out Level 0} 
165 
{\out ~P} 

166 
{\out 1. ~P} 

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

168 
\end{ttbox} 

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

172 
\begin{ttbox} 

173 
not_def; 

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

175 
by (rewrite_goals_tac [not_def]); 

176 
{\out Level 1} 

177 
{\out ~P} 

178 
{\out 1. P > False} 

179 
\end{ttbox} 

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

183 
{\out Level 2} 

184 
{\out ~P} 

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

186 
\ttbreak 

187 
by (resolve_tac prems 1); 

188 
{\out Level 3} 

189 
{\out ~P} 

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

191 
\end{ttbox} 

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

195 
{\out Level 4} 

196 
{\out ~P} 

197 
{\out No subgoals!} 

296  198 
\ttbreak 
3103  199 
qed "notI"; 
105  200 
{\out val notI = "(?P ==> False) ==> ~?P" : thm} 
201 
\end{ttbox} 

310  202 
\indexbold{*notI theorem} 
105  203 

5205  204 
There is a simpler way of conducting this proof. The \ttindex{Goalw} 
205 
command starts a backward proof, as does \texttt{Goal}, but it also 

296  206 
unfolds definitions. Thus there is no need to call 
207 
\ttindex{rewrite_goals_tac}: 

105  208 
\begin{ttbox} 
5205  209 
val prems = Goalw [not_def] 
105  210 
"(P ==> False) ==> ~P"; 
211 
{\out Level 0} 

212 
{\out ~P} 

213 
{\out 1. P > False} 

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

215 
\end{ttbox} 

216 

217 

296  218 
\subsection{Deriving the $\neg$ elimination rule} 
5205  219 
Let us derive the rule $(\neg E)$. The proof follows that of~\texttt{conjE} 
296  220 
above, with an additional step to unfold negation in the major premise. 
5205  221 
The \texttt{Goalw} command is best for this: it unfolds definitions not only 
222 
in the conclusion but the premises. 

105  223 
\begin{ttbox} 
5205  224 
Goalw [not_def] "[ ~P; P ] ==> R"; 
105  225 
{\out Level 0} 
5205  226 
{\out [ ~ P; P ] ==> R} 
227 
{\out 1. [ P > False; P ] ==> R} 

228 
\end{ttbox} 

229 
As the first step, we apply \tdx{FalseE}: 

230 
\begin{ttbox} 

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

5205  233 
{\out [ ~ P; P ] ==> R} 
234 
{\out 1. [ P > False; P ] ==> False} 

284  235 
\end{ttbox} 
5205  236 
% 
284  237 
Everything follows from falsity. And we can prove falsity using the 
238 
premises and Modus Ponens: 

239 
\begin{ttbox} 

5205  240 
by (eresolve_tac [mp] 1); 
105  241 
{\out Level 2} 
5205  242 
{\out [ ~ P; P ] ==> R} 
243 
{\out 1. P ==> P} 

244 
\ttbreak 

245 
by (assume_tac 1); 

105  246 
{\out Level 3} 
5205  247 
{\out [ ~ P; P ] ==> R} 
105  248 
{\out No subgoals!} 
5205  249 
\ttbreak 
3103  250 
qed "notE"; 
105  251 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm} 
252 
\end{ttbox} 

5205  253 

105  254 

255 
\medskip 

5205  256 
\texttt{Goalw} unfolds definitions in the premises even when it has to return 
257 
them as a list. Another way of unfolding definitions in a theorem is by 

258 
applying the function \ttindex{rewrite_rule}. 

105  259 

5205  260 
\index{definitions!and derived rules)} 
105  261 

262 

284  263 
\section{Defining theories}\label{sec:definingtheories} 
105  264 
\index{theories!defining(} 
310  265 

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

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

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

271 
classes {\it class declarations} 

272 
default {\it sort} 

331  273 
types {\it type declarations and synonyms} 
3103  274 
arities {\it type arity declarations} 
105  275 
consts {\it constant declarations} 
3103  276 
syntax {\it syntactic constant declarations} 
277 
translations {\it ast translation rules} 

278 
defs {\it metalogical definitions} 

105  279 
rules {\it rule declarations} 
280 
end 

281 
ML {\it ML code} 

282 
\end{ttbox} 

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

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

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

287 
associated concrete syntax. The translations section specifies 

288 
rewrite rules on abstract syntax trees, handling notations and 

5205  289 
abbreviations. \index{*ML section} The \texttt{ML} section may contain 
3103  290 
code to perform arbitrary syntactic transformations. The main 
3212  291 
declaration forms are discussed below. There are some more sections 
292 
not presented here, the full syntax can be found in 

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

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

295 
objectlogics may add further theory sections, for example 

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

105  297 

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

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

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

302 
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

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

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

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

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

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

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

5205  313 
component \texttt{thy} denoting the new theory, a component for each 
3103  314 
rule, and everything declared in {\it ML code}. 
105  315 

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

5205  318 
rule). But if all goes well, \texttt{use_thy} will finally read the file 
3103  319 
{\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

320 
that refer to the components of~$T$. The structure is automatically 
3103  321 
opened, so its components may be referred to by unqualified names, 
5205  322 
e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}. 
105  323 

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

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

327 
times and dependencies of theory files. See 

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

296  330 
for more details. 
331 

105  332 

1084  333 
\subsection{Declaring constants, definitions and rules} 
310  334 
\indexbold{constants!declaring}\index{rules!declaring} 
335 

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

105  338 
\begin{ttbox} 
1387  339 
consts \(c@1\) :: \(\tau@1\) 
105  340 
\vdots 
1387  341 
\(c@n\) :: \(\tau@n\) 
105  342 
\end{ttbox} 
343 
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are 

1387  344 
types. The types must be enclosed in quotation marks if they contain 
5205  345 
userdeclared infix type constructors like \texttt{*}. Each 
105  346 
constant must be enclosed in quotation marks unless it is a valid 
347 
identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$, 

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

349 
\begin{ttbox} 

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

353 
\begin{ttbox} 

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

355 
\vdots 

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

357 
\end{ttbox} 

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

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

361 

3103  362 
\indexbold{definitions} The {\bf definition part} is similar, but with 
5205  363 
the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are 
3103  364 
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

365 
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

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

1084  369 

3103  370 
Isabelle checks for common errors in definitions, such as extra 
371 
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

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

375 

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

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

378 
xor}: 

284  379 
\begin{ttbox} 
105  380 
Gate = FOL + 
1387  381 
consts nand,xor :: [o,o] => o 
1084  382 
defs nand_def "nand(P,Q) == ~(P & Q)" 
105  383 
xor_def "xor(P,Q) == P & ~Q  ~P & Q" 
384 
end 

385 
\end{ttbox} 

386 

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

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

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

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

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

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

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

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

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

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

397 
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

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

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

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

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

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

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

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

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

406 

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

407 

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

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

409 
A common mistake when writing definitions is to introduce extra free variables 
1468  410 
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

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

412 
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

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

415 
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

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

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

418 
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

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

420 
\end{warn} 
105  421 

422 
\subsection{Declaring type constructors} 

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

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

429 
can be declared by 

105  430 
\begin{ttbox} 
284  431 
types 'a list 
432 
('a,'b) tree 

433 
nat 

105  434 
\end{ttbox} 
284  435 

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

437 
\begin{ttbox} 

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

439 
\vdots 

841  440 
\(tids@n\) \(id@n\) 
284  441 
\end{ttbox} 
442 
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$ 

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

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

105  445 

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

447 
\begin{ttbox} 

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

449 
\vdots 

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

451 
\end{ttbox} 

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

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

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

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

105  459 
\index{examples!of theories} 
284  460 
\begin{ttbox} 
105  461 
Bool = FOL + 
284  462 
types bool 
105  463 
arities bool :: term 
1387  464 
consts tt,ff :: bool 
105  465 
end 
466 
\end{ttbox} 

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

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

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

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

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

473 
\S\ref{polymorphic}. 

105  474 

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

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

5205  480 
Theory \texttt{List} declares the 1place type constructor $list$, gives 
481 
it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with 

296  482 
polymorphic types:% 
5205  483 
\footnote{In the \texttt{consts} part, type variable {\tt'a} has the default 
484 
sort, which is \texttt{term}. See the {\em Reference Manual\/} 

296  485 
\iflabelundefined{sec:refdefiningtheories}{}% 
486 
{(\S\ref{sec:refdefiningtheories})} for more information.} 

105  487 
\index{examples!of theories} 
284  488 
\begin{ttbox} 
105  489 
List = FOL + 
284  490 
types 'a list 
105  491 
arities list :: (term)term 
1387  492 
consts Nil :: 'a list 
493 
Cons :: ['a, 'a list] => 'a list 

105  494 
end 
495 
\end{ttbox} 

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

499 
\end{ttbox} 

500 

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

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

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

505 
%\end{warn} 

105  506 

331  507 
\subsection{Type synonyms}\indexbold{type synonyms} 
303  508 
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar 
307  509 
to those found in \ML. Such synonyms are defined in the type declaration part 
303  510 
and are fairly self explanatory: 
511 
\begin{ttbox} 

1387  512 
types gate = [o,o] => o 
513 
'a pred = 'a => o 

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

303  515 
\end{ttbox} 
516 
Type declarations and synonyms can be mixed arbitrarily: 

517 
\begin{ttbox} 

518 
types nat 

1387  519 
'a stream = nat => 'a 
520 
signal = nat stream 

303  521 
'a list 
522 
\end{ttbox} 

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

525 
fully expanded. As a consequence Isabelle output never contains 

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

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

303  528 
\begin{ttbox} 
1387  529 
consts and,or :: gate 
530 
negate :: signal => signal 

303  531 
\end{ttbox} 
532 

348  533 
\subsection{Infix and mixfix operators} 
310  534 
\index{infixes}\index{examples!of theories} 
535 

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

537 
following theory: 

284  538 
\begin{ttbox} 
105  539 
Gate2 = FOL + 
1387  540 
consts "~&" :: [o,o] => o (infixl 35) 
541 
"#" :: [o,o] => o (infixl 30) 

1084  542 
defs nand_def "P ~& Q == ~(P & Q)" 
105  543 
xor_def "P # Q == P & ~Q  ~P & Q" 
544 
end 

545 
\end{ttbox} 

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

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

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

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

105  551 

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

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

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

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

556 

3212  557 
\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

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

561 
\end{ttbox} 

562 

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

565 
add a line to the constant declaration part: 

284  566 
\begin{ttbox} 
1387  567 
If :: [o,o,o] => o ("if _ then _ else _") 
105  568 
\end{ttbox} 
310  569 
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt 
5205  570 
if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}. Underscores 
310  571 
denote argument positions. 
105  572 

5205  573 
The declaration above does not allow the \texttt{if}\texttt{then}{\tt 
3103  574 
else} construct to be printed split across several lines, even if it 
575 
is too long to fit on one line. Prettyprinting information can be 

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

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

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

580 

581 
Mixfix declarations can be annotated with priorities, just like 

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

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

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

592 
hand, the declaration 

284  593 
\begin{ttbox} 
1387  594 
If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99) 
105  595 
\end{ttbox} 
284  596 
defines concrete syntax for a conditional whose first argument cannot have 
5205  597 
the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority 
310  598 
of at least~100. We may of course write 
284  599 
\begin{quote}\tt 
600 
if (if $P$ then $Q$ else $R$) then $S$ else $T$ 

156  601 
\end{quote} 
310  602 
because expressions in parentheses have maximal priority. 
105  603 

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

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

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

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

284  611 
types ('a,'b) "*" (infixl 20) 
105  612 
arities "*" :: (term,term)term 
613 
consts fst :: "'a * 'b => 'a" 

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

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

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

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

618 
end 

619 
\end{ttbox} 

620 

621 
\begin{warn} 

5205  622 
The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as 
3103  623 
it would be in the case of an infix constant. Only infix type 
5205  624 
constructors can have symbolic names like~\texttt{*}. General mixfix 
625 
syntax for types may be introduced via appropriate \texttt{syntax} 

3103  626 
declarations. 
105  627 
\end{warn} 
628 

629 

630 
\subsection{Overloading} 

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

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

633 
\begin{ttbox} 

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

635 
\vdots 

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

637 
\end{ttbox} 

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

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

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

641 
subclass of $k$ existing classes: 

642 
\begin{ttbox} 

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

644 
\end{ttbox} 

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

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

310  650 
\index{examples!of theories}\index{constants!overloaded} 
105  651 
\begin{ttbox} 
652 
Arith = FOL + 

653 
classes arith < term 

1387  654 
consts "0" :: 'a::arith ("0") 
655 
"1" :: 'a::arith ("1") 

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

105  657 
end 
658 
\end{ttbox} 

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

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

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

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

663 

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

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

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

667 
\index{examples!of theories} 

668 
\begin{ttbox} 

669 
BoolNat = Arith + 

348  670 
types bool nat 
671 
arities bool, nat :: arith 

1387  672 
consts Suc :: nat=>nat 
284  673 
\ttbreak 
105  674 
rules add0 "0 + n = n::nat" 
675 
addS "Suc(m)+n = Suc(m+n)" 

676 
nat1 "1 = Suc(0)" 

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

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

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

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

681 
end 

682 
\end{ttbox} 

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

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

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

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

284  687 
collapse $nat$ to a trivial type: 
105  688 
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \] 
296  689 

105  690 

296  691 
\section{Theory example: the natural numbers} 
692 

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

105  694 
demonstrating many of the theory extension features. 
695 

696 

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

698 
\index{examples!of theories} 

699 

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

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

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

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

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

709 
\] 

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

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

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

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

714 
formalize mathematical induction as 

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

716 

717 
\noindent 

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

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

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

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

722 
better with Isabelle's simplifier.} 

723 
$(Suc\_neq\_0)$ is 

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

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

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

727 

728 
\noindent 

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

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

731 
and obeys the equations 

732 
\begin{eqnarray*} 

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

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

735 
\end{eqnarray*} 

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

737 
should satisfy 

738 
\begin{eqnarray*} 

739 
0+n & = & n \\ 

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

741 
\end{eqnarray*} 

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

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

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

747 
\begin{eqnarray*} 

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

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

750 
\end{eqnarray*} 

751 

752 

753 
\subsection{Declaring the theory to Isabelle} 

754 
\index{examples!of theories} 

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

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

310  760 
\begin{ttbox}\index{mixfix declarations} 
105  761 
Nat = FOL + 
284  762 
types nat 
105  763 
arities nat :: term 
1387  764 
consts "0" :: nat ("0") 
765 
Suc :: nat=>nat 

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

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

296  768 
rules Suc_inject "Suc(m)=Suc(n) ==> m=n" 
105  769 
Suc_neq_0 "Suc(m)=0 ==> R" 
296  770 
induct "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)" 
105  771 
rec_0 "rec(0,a,f) = a" 
772 
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" 

296  773 
add_def "m+n == rec(m, n, \%x y. Suc(y))" 
105  774 
end 
775 
\end{ttbox} 

5205  776 
In axiom \texttt{add_def}, recall that \verb% stands for~$\lambda$. 
777 
Loading this theory file creates the \ML\ structure \texttt{Nat}, which 

3103  778 
contains the theory and axioms. 
296  779 

780 
\subsection{Proving some recursion equations} 

5205  781 
Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the 
105  782 
natural numbers. As a trivial example, let us derive recursion equations 
783 
for \verb$+$. Here is the zero case: 

284  784 
\begin{ttbox} 
5205  785 
Goalw [add_def] "0+n = n"; 
105  786 
{\out Level 0} 
787 
{\out 0 + n = n} 

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

791 
{\out Level 1} 

792 
{\out 0 + n = n} 

793 
{\out No subgoals!} 

3103  794 
qed "add_0"; 
284  795 
\end{ttbox} 
105  796 
And here is the successor case: 
284  797 
\begin{ttbox} 
5205  798 
Goalw [add_def] "Suc(m)+n = Suc(m+n)"; 
105  799 
{\out Level 0} 
800 
{\out Suc(m) + n = Suc(m + n)} 

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

804 
{\out Level 1} 

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

806 
{\out No subgoals!} 

3103  807 
qed "add_Suc"; 
284  808 
\end{ttbox} 
105  809 
The induction rule raises some complications, which are discussed next. 
810 
\index{theories!defining)} 

811 

812 

813 
\section{Refinement with explicit instantiation} 

310  814 
\index{resolution!with instantiation} 
815 
\index{instantiation(} 

816 

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

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

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

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

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

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

824 

5205  825 
The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by 
105  826 
a rule. But it also accepts explicit instantiations for the rule's 
827 
schematic variables. 

828 
\begin{description} 

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

832 

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

105  835 
and destructresolution, respectively. 
836 
\end{description} 

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

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

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

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

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

5205  844 
required: \texttt{res_inst_tac} instantiates type variables automatically 
105  845 
whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$. 
846 

847 
\subsection{A simple proof by induction} 

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

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

284  852 
\begin{ttbox} 
5205  853 
Goal "~ (Suc(k) = k)"; 
105  854 
{\out Level 0} 
459  855 
{\out Suc(k) ~= k} 
856 
{\out 1. Suc(k) ~= k} 

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

859 
{\out Level 1} 

459  860 
{\out Suc(k) ~= k} 
861 
{\out 1. Suc(0) ~= 0} 

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

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

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

310  867 
The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the 
5205  868 
other rules of theory \texttt{Nat}. The base case holds by~\ttindex{Suc_neq_0}: 
284  869 
\begin{ttbox} 
105  870 
by (resolve_tac [notI] 1); 
871 
{\out Level 2} 

459  872 
{\out Suc(k) ~= k} 
105  873 
{\out 1. Suc(0) = 0 ==> False} 
459  874 
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} 
105  875 
\ttbreak 
876 
by (eresolve_tac [Suc_neq_0] 1); 

877 
{\out Level 3} 

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

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

884 
\begin{ttbox} 

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

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

105  889 
\ttbreak 
890 
by (eresolve_tac [notE] 1); 

891 
{\out Level 5} 

459  892 
{\out Suc(k) ~= k} 
105  893 
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x} 
894 
\ttbreak 

895 
by (eresolve_tac [Suc_inject] 1); 

896 
{\out Level 6} 

459  897 
{\out Suc(k) ~= k} 
105  898 
{\out No subgoals!} 
284  899 
\end{ttbox} 
105  900 

901 

5205  902 
\subsection{An example of ambiguity in \texttt{resolve_tac}} 
105  903 
\index{examples!of induction}\index{unification!higherorder} 
5205  904 
If you try the example above, you may observe that \texttt{res_inst_tac} is 
105  905 
not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right 
906 
instantiation for~$(induct)$ to yield the desired next state. With more 

907 
complex formulae, our luck fails. 

284  908 
\begin{ttbox} 
5205  909 
Goal "(k+m)+n = k+(m+n)"; 
105  910 
{\out Level 0} 
911 
{\out k + m + n = k + (m + n)} 

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

913 
\ttbreak 

914 
by (resolve_tac [induct] 1); 

915 
{\out Level 1} 

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

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

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

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

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

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

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

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

925 
the tactic. 

926 
\begin{ttbox} 

105  927 
back(); 
928 
{\out Level 1} 

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

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

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

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

934 
call \ttindex{back} again. 

935 
\begin{ttbox} 

105  936 
back(); 
937 
{\out Level 1} 

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

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

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

942 
\end{ttbox} 

105  943 
Now induction has been applied to~$n$. What is the next alternative? 
284  944 
\begin{ttbox} 
105  945 
back(); 
946 
{\out Level 1} 

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

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

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

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

310  953 
here. 
954 

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

956 
number is exponential in the size of the formula. 

105  957 

958 
\subsection{Proving that addition is associative} 

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

962 
\iflabelundefined{simpchap}% 

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

284  964 

310  965 
\index{simplification}\index{examples!of simplification} 
966 

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

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

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

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

5205  972 
$\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$: 
284  973 
\begin{ttbox} 
3114  974 
Addsimps [add_0, add_Suc]; 
284  975 
\end{ttbox} 
105  976 
We state the goal for associativity of addition, and 
977 
use \ttindex{res_inst_tac} to invoke induction on~$k$: 

284  978 
\begin{ttbox} 
5205  979 
Goal "(k+m)+n = k+(m+n)"; 
105  980 
{\out Level 0} 
981 
{\out k + m + n = k + (m + n)} 

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

983 
\ttbreak 

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

985 
{\out Level 1} 

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

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

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

990 
\end{ttbox} 

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

284  994 
\begin{ttbox} 
3114  995 
by (Simp_tac 1); 
105  996 
{\out Level 2} 
997 
{\out k + m + n = k + (m + n)} 

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

1000 
\end{ttbox} 

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

284  1005 
\begin{ttbox} 
3114  1006 
by (Asm_simp_tac 1); 
105  1007 
{\out Level 3} 
1008 
{\out k + m + n = k + (m + n)} 

1009 
{\out No subgoals!} 

284  1010 
\end{ttbox} 
310  1011 
\index{instantiation)} 
105  1012 

1013 

284  1014 
\section{A Prolog interpreter} 
105  1015 
\index{Prolog interpreterbold} 
284  1016 
To demonstrate the power of tacticals, let us construct a Prolog 
105  1017 
interpreter and execute programs involving lists.\footnote{To run these 
5205  1018 
examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program 
105  1019 
consists of a theory. We declare a type constructor for lists, with an 
1020 
arity declaration to say that $(\tau)list$ is of class~$term$ 

1021 
provided~$\tau$ is: 

1022 
\begin{eqnarray*} 

1023 
list & :: & (term)term 

1024 
\end{eqnarray*} 

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

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

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

1030 
Nil & :: & \alpha list \\ 

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

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

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

1034 
\end{eqnarray*} 

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

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

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

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

1041 
rev(x:xs, zs)} 

1042 
\] 

1043 

1044 
\index{examples!of theories} 

310  1045 
Theory \thydx{Prolog} extends firstorder logic in order to make use 
105  1046 
of the class~$term$ and the type~$o$. The interpreter does not use the 
5205  1047 
rules of~\texttt{FOL}. 
105  1048 
\begin{ttbox} 
1049 
Prolog = FOL + 

296  1050 
types 'a list 
105  1051 
arities list :: (term)term 
1387  1052 
consts Nil :: 'a list 
1053 
":" :: ['a, 'a list]=> 'a list (infixr 60) 

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

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

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

1058 
revNil "rev(Nil,Nil)" 

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

1060 
end 

1061 
\end{ttbox} 

1062 
\subsection{Simple executions} 

284  1063 
Repeated application of the rules solves Prolog goals. Let us 
105  1064 
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the 
5205  1065 
answer builds up in~\texttt{?x}. 
105  1066 
\begin{ttbox} 
5205  1067 
Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; 
105  1068 
{\out Level 0} 
1069 
{\out app(a : b : c : Nil, d : e : Nil, ?x)} 

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

1071 
\ttbreak 

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

1073 
{\out Level 1} 

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

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

1076 
\ttbreak 

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

1078 
{\out Level 2} 

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

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

1081 
\end{ttbox} 

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

1083 
\begin{ttbox} 

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

1085 
{\out Level 3} 

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

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

1088 
\ttbreak 

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

1090 
{\out Level 4} 

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

1092 
{\out No subgoals!} 

1093 
\end{ttbox} 

1094 

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

1098 
\begin{ttbox} 

5205  1099 
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; 
105  1100 
{\out Level 0} 
1101 
{\out app(?x, c : d : Nil, a : b : c : d : Nil)} 

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

1103 
\ttbreak 

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

1105 
{\out Level 1} 

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

1107 
{\out No subgoals!} 

1108 
\end{ttbox} 

1109 

1110 

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

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

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

105  1116 
\begin{ttbox} 
5205  1117 
Goal "app(?x, ?y, a:b:c:d:Nil)"; 
105  1118 
{\out Level 0} 
1119 
{\out app(?x, ?y, a : b : c : d : Nil)} 

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

1121 
\ttbreak 

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

1123 
{\out Level 1} 

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

1125 
{\out No subgoals!} 

1126 
\end{ttbox} 

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

105  1129 
\begin{ttbox} 
1130 
back(); 

1131 
{\out Level 1} 

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

1133 
{\out No subgoals!} 

1134 
\end{ttbox} 

1135 
The other solutions are generated similarly. 

1136 
\begin{ttbox} 

1137 
back(); 

1138 
{\out Level 1} 

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

1140 
{\out No subgoals!} 

1141 
\ttbreak 

1142 
back(); 

1143 
{\out Level 1} 

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

1145 
{\out No subgoals!} 

1146 
\ttbreak 

1147 
back(); 

1148 
{\out Level 1} 

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

1150 
{\out No subgoals!} 

1151 
\end{ttbox} 

1152 

1153 

1154 
\subsection{Depthfirst search} 

1155 
\index{search!depthfirst} 

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

5205  1157 
Bundle the rules together as the \ML{} identifier \texttt{rules}. Naive 
105  1158 
reverse requires 120 inferences for this 14element list, but the tactic 
1159 
terminates in a few seconds. 

1160 
\begin{ttbox} 

5205  1161 
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; 
105  1162 
{\out Level 0} 
1163 
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)} 

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

1166 
\ttbreak 

105  1167 
val rules = [appNil,appCons,revNil,revCons]; 
1168 
\ttbreak 

1169 
by (REPEAT (resolve_tac rules 1)); 

1170 
{\out Level 1} 

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

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

1173 
{\out No subgoals!} 

1174 
\end{ttbox} 

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

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

1177 
\begin{ttbox} 

5205  1178 
Goal "rev(?x, a:b:c:Nil)"; 
105  1179 
{\out Level 0} 
1180 
{\out rev(?x, a : b : c : Nil)} 

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

1182 
\ttbreak 

1183 
by (REPEAT (resolve_tac rules 1)); 

1184 
{\out Level 1} 

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

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

1187 
\end{ttbox} 

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

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

1192 
back(); 

1193 
{\out Level 1} 

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

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

1196 
\end{ttbox} 

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

1198 
\begin{ttbox} 

1199 
back(); 

1200 
{\out Level 1} 

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

1202 
{\out No subgoals!} 

1203 
\end{ttbox} 

310  1204 
\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a 
5205  1205 
search tactical. \texttt{REPEAT} stops when it cannot continue, regardless of 
310  1206 
which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a 
1207 
satisfactory state, as specified by an \ML{} predicate. Below, 

105  1208 
\ttindex{has_fewer_prems} specifies that the proof state should have no 
310  1209 
subgoals. 
105  1210 
\begin{ttbox} 
1211 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 

1212 
(resolve_tac rules 1); 

1213 
\end{ttbox} 

284  1214 
Since Prolog uses depthfirst search, this tactic is a (slow!) 
296  1215 
Prolog interpreter. We return to the start of the proof using 
5205  1216 
\ttindex{choplev}, and apply \texttt{prolog_tac}: 
105  1217 
\begin{ttbox} 
1218 
choplev 0; 

1219 
{\out Level 0} 

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

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

1222 
\ttbreak 

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

1224 
{\out Level 1} 

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

1226 
{\out No subgoals!} 

1227 
\end{ttbox} 

5205  1228 
Let us try \texttt{prolog_tac} on one more example, containing four unknowns: 
105  1229 
\begin{ttbox} 
5205  1230 
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; 
105  1231 
{\out Level 0} 
1232 
{\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} 

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

1234 
\ttbreak 

1235 
by prolog_tac; 

1236 
{\out Level 1} 

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

1238 
{\out No subgoals!} 

1239 
\end{ttbox} 

284  1240 
Although Isabelle is much slower than a Prolog system, Isabelle 
156  1241 
tactics can exploit logic programming techniques. 
1242 