author  paulson 
Tue, 10 Feb 2004 12:02:11 +0100  
changeset 14378  69c4d5997669 
parent 14148  6580d374a509 
child 42637  381fdcab0f36 
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$. 

14148  51 
These metalevel assumptions are also recorded internally, allowing 
5205  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 

14148  56 
premises, and the second case applies. In this section, many of the 
57 
theorems are subject to metalevel assumptions, so we make them visible by by setting the 

58 
\ttindex{show_hyps} flag: 

59 
\begin{ttbox} 

60 
set show_hyps; 

61 
{\out val it = true : bool} 

62 
\end{ttbox} 

105  63 

14148  64 
Now, we are ready to derive $\conj$ elimination. Until now, calling \texttt{Goal} has 
5205  65 
returned an empty list, which we have ignored. In this example, the list 
66 
contains the two premises of the rule, since one of them involves the $\Imp$ 

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

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

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

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

71 
\xdx{Match}.} 

105  72 
\begin{ttbox} 
5205  73 
val [major,minor] = Goal 
105  74 
"[ P&Q; [ P; Q ] ==> R ] ==> R"; 
75 
{\out Level 0} 

76 
{\out R} 

77 
{\out 1. R} 

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

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

80 
\end{ttbox} 

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

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

85 
by (resolve_tac [minor] 1); 

86 
{\out Level 1} 

87 
{\out R} 

88 
{\out 1. P} 

89 
{\out 2. Q} 

90 
\end{ttbox} 

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

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

93 
\begin{ttbox} 

94 
major RS conjunct1; 

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

96 
\ttbreak 

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

98 
{\out Level 2} 

99 
{\out R} 

100 
{\out 1. Q} 

101 
\end{ttbox} 

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

103 
\begin{ttbox} 

104 
major RS conjunct2; 

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

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

107 
{\out Level 3} 

108 
{\out R} 

109 
{\out No subgoals!} 

110 
\end{ttbox} 

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

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

114 
one  and makes the variables schematic. 

105  115 
\begin{ttbox} 
116 
topthm(); 

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

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

121 

122 

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

310  124 
\index{rules!derived}\index{definitions!and derived rules(} 
125 

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

128 
\begin{eqnarray*} 

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

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

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

132 
\end{eqnarray*} 

331  133 
\index{metarewriting}% 
105  134 
Isabelle permits {\bf metalevel rewriting} using definitions such as 
135 
these. {\bf Unfolding} replaces every instance 

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

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

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

141 

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

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

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

147 
becoming unreadable. 

148 

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

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

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

5205  152 
the \texttt{Goal} command that unfolds the conclusion and premises of the rule 
105  153 
being derived. 
154 

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

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

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

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

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

105  162 

163 

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

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

105  168 
\begin{ttbox} 
5205  169 
val prems = Goal "(P ==> False) ==> ~P"; 
105  170 
{\out Level 0} 
171 
{\out ~P} 

172 
{\out 1. ~P} 

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

174 
\end{ttbox} 

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

178 
\begin{ttbox} 

179 
not_def; 

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

181 
by (rewrite_goals_tac [not_def]); 

182 
{\out Level 1} 

183 
{\out ~P} 

184 
{\out 1. P > False} 

185 
\end{ttbox} 

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

189 
{\out Level 2} 

190 
{\out ~P} 

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

192 
\ttbreak 

193 
by (resolve_tac prems 1); 

194 
{\out Level 3} 

195 
{\out ~P} 

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

197 
\end{ttbox} 

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

201 
{\out Level 4} 

202 
{\out ~P} 

203 
{\out No subgoals!} 

296  204 
\ttbreak 
3103  205 
qed "notI"; 
105  206 
{\out val notI = "(?P ==> False) ==> ~?P" : thm} 
207 
\end{ttbox} 

310  208 
\indexbold{*notI theorem} 
105  209 

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

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

105  214 
\begin{ttbox} 
5205  215 
val prems = Goalw [not_def] 
105  216 
"(P ==> False) ==> ~P"; 
217 
{\out Level 0} 

218 
{\out ~P} 

219 
{\out 1. P > False} 

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

221 
\end{ttbox} 

222 

223 

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

105  229 
\begin{ttbox} 
5205  230 
Goalw [not_def] "[ ~P; P ] ==> R"; 
105  231 
{\out Level 0} 
5205  232 
{\out [ ~ P; P ] ==> R} 
233 
{\out 1. [ P > False; P ] ==> R} 

234 
\end{ttbox} 

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

236 
\begin{ttbox} 

105  237 
by (resolve_tac [FalseE] 1); 
238 
{\out Level 1} 

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

284  241 
\end{ttbox} 
5205  242 
% 
284  243 
Everything follows from falsity. And we can prove falsity using the 
244 
premises and Modus Ponens: 

245 
\begin{ttbox} 

5205  246 
by (eresolve_tac [mp] 1); 
105  247 
{\out Level 2} 
5205  248 
{\out [ ~ P; P ] ==> R} 
249 
{\out 1. P ==> P} 

250 
\ttbreak 

251 
by (assume_tac 1); 

105  252 
{\out Level 3} 
5205  253 
{\out [ ~ P; P ] ==> R} 
105  254 
{\out No subgoals!} 
5205  255 
\ttbreak 
3103  256 
qed "notE"; 
105  257 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm} 
258 
\end{ttbox} 

5205  259 

105  260 

261 
\medskip 

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

264 
applying the function \ttindex{rewrite_rule}. 

105  265 

5205  266 
\index{definitions!and derived rules)} 
105  267 

268 

284  269 
\section{Defining theories}\label{sec:definingtheories} 
105  270 
\index{theories!defining(} 
310  271 

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

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

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

277 
classes {\it class declarations} 

278 
default {\it sort} 

331  279 
types {\it type declarations and synonyms} 
3103  280 
arities {\it type arity declarations} 
105  281 
consts {\it constant declarations} 
3103  282 
syntax {\it syntactic constant declarations} 
283 
translations {\it ast translation rules} 

284 
defs {\it metalogical definitions} 

105  285 
rules {\it rule declarations} 
286 
end 

287 
ML {\it ML code} 

288 
\end{ttbox} 

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

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

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

293 
associated concrete syntax. The translations section specifies 

294 
rewrite rules on abstract syntax trees, handling notations and 

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

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

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

301 
objectlogics may add further theory sections, for example 

9695  302 
\texttt{typedef}, \texttt{datatype} in HOL. 
105  303 

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

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

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

308 
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

309 
\thydx{Pure} contains nothing but Isabelle's metalogic. The variant 
3103  310 
\thydx{CPure} offers the more usual higherorder function application 
9695  311 
syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure. 
105  312 

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

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

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

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

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

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

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

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

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

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

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

333 
times and dependencies of theory files. See 

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

296  336 
for more details. 
337 

105  338 

1084  339 
\subsection{Declaring constants, definitions and rules} 
310  340 
\indexbold{constants!declaring}\index{rules!declaring} 
341 

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

105  344 
\begin{ttbox} 
1387  345 
consts \(c@1\) :: \(\tau@1\) 
105  346 
\vdots 
1387  347 
\(c@n\) :: \(\tau@n\) 
105  348 
\end{ttbox} 
349 
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are 

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

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

355 
\begin{ttbox} 

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

359 
\begin{ttbox} 

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

361 
\vdots 

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

363 
\end{ttbox} 

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

284  365 
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be 
14148  366 
enclosed in quotation marks. Rules are simply axioms; they are 
367 
called \emph{rules} because they are mainly used to specify the inference 

368 
rules when defining a new logic. 

284  369 

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

373 
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

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

1084  377 

3103  378 
Isabelle checks for common errors in definitions, such as extra 
14148  379 
variables on the righthand side and cyclic dependencies, that could 
380 
least to inconsistency. It is still essential to take care: 

381 
theorems proved on the basis of incorrect definitions are useless, 

382 
your system can be consistent and yet still wrong. 

3103  383 

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

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

386 
xor}: 

284  387 
\begin{ttbox} 
105  388 
Gate = FOL + 
1387  389 
consts nand,xor :: [o,o] => o 
1084  390 
defs nand_def "nand(P,Q) == ~(P & Q)" 
105  391 
xor_def "xor(P,Q) == P & ~Q  ~P & Q" 
392 
end 

393 
\end{ttbox} 

394 

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

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

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

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

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

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

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

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

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

403 
\end{ttbox} 
5205  404 
\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

405 
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

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

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

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

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

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

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

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

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

414 

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

415 

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

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

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

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

420 
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

421 
\end{ttbox} 
5205  422 
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

423 
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

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

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

426 
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

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

428 
\end{warn} 
105  429 

430 
\subsection{Declaring type constructors} 

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

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

437 
can be declared by 

105  438 
\begin{ttbox} 
284  439 
types 'a list 
440 
('a,'b) tree 

441 
nat 

105  442 
\end{ttbox} 
284  443 

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

445 
\begin{ttbox} 

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

447 
\vdots 

841  448 
\(tids@n\) \(id@n\) 
284  449 
\end{ttbox} 
450 
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$ 

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

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

105  453 

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

455 
\begin{ttbox} 

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

457 
\vdots 

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

459 
\end{ttbox} 

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

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

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

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

105  467 
\index{examples!of theories} 
284  468 
\begin{ttbox} 
105  469 
Bool = FOL + 
284  470 
types bool 
105  471 
arities bool :: term 
1387  472 
consts tt,ff :: bool 
105  473 
end 
474 
\end{ttbox} 

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

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

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

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

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

481 
\S\ref{polymorphic}. 

105  482 

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

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

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

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

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

105  495 
\index{examples!of theories} 
284  496 
\begin{ttbox} 
105  497 
List = FOL + 
284  498 
types 'a list 
105  499 
arities list :: (term)term 
1387  500 
consts Nil :: 'a list 
501 
Cons :: ['a, 'a list] => 'a list 

105  502 
end 
503 
\end{ttbox} 

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

507 
\end{ttbox} 

508 

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

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

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

513 
%\end{warn} 

105  514 

331  515 
\subsection{Type synonyms}\indexbold{type synonyms} 
303  516 
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar 
307  517 
to those found in \ML. Such synonyms are defined in the type declaration part 
303  518 
and are fairly self explanatory: 
519 
\begin{ttbox} 

1387  520 
types gate = [o,o] => o 
521 
'a pred = 'a => o 

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

303  523 
\end{ttbox} 
524 
Type declarations and synonyms can be mixed arbitrarily: 

525 
\begin{ttbox} 

526 
types nat 

1387  527 
'a stream = nat => 'a 
528 
signal = nat stream 

303  529 
'a list 
530 
\end{ttbox} 

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

533 
fully expanded. As a consequence Isabelle output never contains 

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

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

303  536 
\begin{ttbox} 
1387  537 
consts and,or :: gate 
538 
negate :: signal => signal 

303  539 
\end{ttbox} 
540 

348  541 
\subsection{Infix and mixfix operators} 
310  542 
\index{infixes}\index{examples!of theories} 
543 

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

545 
following theory: 

284  546 
\begin{ttbox} 
105  547 
Gate2 = FOL + 
1387  548 
consts "~&" :: [o,o] => o (infixl 35) 
549 
"#" :: [o,o] => o (infixl 30) 

1084  550 
defs nand_def "P ~& Q == ~(P & Q)" 
105  551 
xor_def "P # Q == P & ~Q  ~P & Q" 
552 
end 

553 
\end{ttbox} 

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

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

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

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

105  559 

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

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

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

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

564 

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

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

569 
\end{ttbox} 

570 

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

573 
add a line to the constant declaration part: 

284  574 
\begin{ttbox} 
1387  575 
If :: [o,o,o] => o ("if _ then _ else _") 
105  576 
\end{ttbox} 
310  577 
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt 
5205  578 
if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}. Underscores 
310  579 
denote argument positions. 
105  580 

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

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

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

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

588 

589 
Mixfix declarations can be annotated with priorities, just like 

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

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

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

600 
hand, the declaration 

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

156  609 
\end{quote} 
310  610 
because expressions in parentheses have maximal priority. 
105  611 

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

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

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

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

284  619 
types ('a,'b) "*" (infixl 20) 
105  620 
arities "*" :: (term,term)term 
621 
consts fst :: "'a * 'b => 'a" 

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

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

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

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

626 
end 

627 
\end{ttbox} 

628 

629 
\begin{warn} 

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

3103  634 
declarations. 
105  635 
\end{warn} 
636 

637 

638 
\subsection{Overloading} 

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

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

641 
\begin{ttbox} 

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

643 
\vdots 

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

645 
\end{ttbox} 

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

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

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

649 
subclass of $k$ existing classes: 

650 
\begin{ttbox} 

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

652 
\end{ttbox} 

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

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

310  658 
\index{examples!of theories}\index{constants!overloaded} 
105  659 
\begin{ttbox} 
660 
Arith = FOL + 

661 
classes arith < term 

1387  662 
consts "0" :: 'a::arith ("0") 
663 
"1" :: 'a::arith ("1") 

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

105  665 
end 
666 
\end{ttbox} 

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

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

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

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

671 

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

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

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

675 
\index{examples!of theories} 

676 
\begin{ttbox} 

677 
BoolNat = Arith + 

348  678 
types bool nat 
679 
arities bool, nat :: arith 

1387  680 
consts Suc :: nat=>nat 
284  681 
\ttbreak 
105  682 
rules add0 "0 + n = n::nat" 
683 
addS "Suc(m)+n = Suc(m+n)" 

684 
nat1 "1 = Suc(0)" 

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

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

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

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

689 
end 

690 
\end{ttbox} 

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

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

14148  693 
constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l}) 
694 
would have type $\alpha{::}arith$ 

105  695 
and the axiom would hold for any type of class $arith$. This would 
284  696 
collapse $nat$ to a trivial type: 
105  697 
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \] 
296  698 

105  699 

296  700 
\section{Theory example: the natural numbers} 
701 

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

105  703 
demonstrating many of the theory extension features. 
704 

705 

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

707 
\index{examples!of theories} 

708 

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

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

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

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

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

718 
\] 

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

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

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

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

723 
formalize mathematical induction as 

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

725 

726 
\noindent 

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

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

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

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

731 
better with Isabelle's simplifier.} 

732 
$(Suc\_neq\_0)$ is 

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

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

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

736 

737 
\noindent 

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

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

740 
and obeys the equations 

741 
\begin{eqnarray*} 

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

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

744 
\end{eqnarray*} 

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

746 
should satisfy 

747 
\begin{eqnarray*} 

748 
0+n & = & n \\ 

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

750 
\end{eqnarray*} 

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

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

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

756 
\begin{eqnarray*} 

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

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

759 
\end{eqnarray*} 

760 

761 

762 
\subsection{Declaring the theory to Isabelle} 

763 
\index{examples!of theories} 

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

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

310  769 
\begin{ttbox}\index{mixfix declarations} 
105  770 
Nat = FOL + 
284  771 
types nat 
105  772 
arities nat :: term 
1387  773 
consts "0" :: nat ("0") 
774 
Suc :: nat=>nat 

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

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

296  777 
rules Suc_inject "Suc(m)=Suc(n) ==> m=n" 
105  778 
Suc_neq_0 "Suc(m)=0 ==> R" 
296  779 
induct "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)" 
105  780 
rec_0 "rec(0,a,f) = a" 
781 
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" 

296  782 
add_def "m+n == rec(m, n, \%x y. Suc(y))" 
105  783 
end 
784 
\end{ttbox} 

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

3103  787 
contains the theory and axioms. 
296  788 

789 
\subsection{Proving some recursion equations} 

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

284  793 
\begin{ttbox} 
5205  794 
Goalw [add_def] "0+n = n"; 
105  795 
{\out Level 0} 
796 
{\out 0 + n = n} 

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

800 
{\out Level 1} 

801 
{\out 0 + n = n} 

802 
{\out No subgoals!} 

3103  803 
qed "add_0"; 
284  804 
\end{ttbox} 
105  805 
And here is the successor case: 
284  806 
\begin{ttbox} 
5205  807 
Goalw [add_def] "Suc(m)+n = Suc(m+n)"; 
105  808 
{\out Level 0} 
809 
{\out Suc(m) + n = Suc(m + n)} 

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

813 
{\out Level 1} 

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

815 
{\out No subgoals!} 

3103  816 
qed "add_Suc"; 
284  817 
\end{ttbox} 
105  818 
The induction rule raises some complications, which are discussed next. 
819 
\index{theories!defining)} 

820 

821 

822 
\section{Refinement with explicit instantiation} 

310  823 
\index{resolution!with instantiation} 
824 
\index{instantiation(} 

825 

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

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

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

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

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

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

833 

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

837 
\begin{description} 

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

841 

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

105  844 
and destructresolution, respectively. 
845 
\end{description} 

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

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

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

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

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

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

856 
\subsection{A simple proof by induction} 

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

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

284  861 
\begin{ttbox} 
5205  862 
Goal "~ (Suc(k) = k)"; 
105  863 
{\out Level 0} 
459  864 
{\out Suc(k) ~= k} 
865 
{\out 1. Suc(k) ~= k} 

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

868 
{\out Level 1} 

459  869 
{\out Suc(k) ~= k} 
870 
{\out 1. Suc(0) ~= 0} 

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

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

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

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

459  881 
{\out Suc(k) ~= k} 
105  882 
{\out 1. Suc(0) = 0 ==> False} 
459  883 
{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} 
105  884 
\ttbreak 
885 
by (eresolve_tac [Suc_neq_0] 1); 

886 
{\out Level 3} 

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

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

893 
\begin{ttbox} 

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

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

105  898 
\ttbreak 
899 
by (eresolve_tac [notE] 1); 

900 
{\out Level 5} 

459  901 
{\out Suc(k) ~= k} 
105  902 
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x} 
903 
\ttbreak 

904 
by (eresolve_tac [Suc_inject] 1); 

905 
{\out Level 6} 

459  906 
{\out Suc(k) ~= k} 
105  907 
{\out No subgoals!} 
284  908 
\end{ttbox} 
105  909 

910 

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

916 
complex formulae, our luck fails. 

284  917 
\begin{ttbox} 
5205  918 
Goal "(k+m)+n = k+(m+n)"; 
105  919 
{\out Level 0} 
920 
{\out k + m + n = k + (m + n)} 

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

922 
\ttbreak 

923 
by (resolve_tac [induct] 1); 

924 
{\out Level 1} 

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

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

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

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

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

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

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

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

934 
the tactic. 

935 
\begin{ttbox} 

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

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

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

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

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

943 
call \ttindex{back} again. 

944 
\begin{ttbox} 

105  945 
back(); 
946 
{\out Level 1} 

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

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

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

951 
\end{ttbox} 

105  952 
Now induction has been applied to~$n$. What is the next alternative? 
284  953 
\begin{ttbox} 
105  954 
back(); 
955 
{\out Level 1} 

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

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

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

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

310  962 
here. 
963 

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

965 
number is exponential in the size of the formula. 

105  966 

967 
\subsection{Proving that addition is associative} 

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

971 
\iflabelundefined{simpchap}% 

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

284  973 

310  974 
\index{simplification}\index{examples!of simplification} 
975 

9695  976 
Isabelle's simplification tactics repeatedly apply equations to a subgoal, 
977 
perhaps proving it. For efficiency, the rewrite rules must be packaged into a 

978 
{\bf simplification set},\index{simplification sets} or {\bf simpset}. We 

979 
augment the implicit simpset of FOL with the equations proved in the previous 

980 
section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$: 

284  981 
\begin{ttbox} 
3114  982 
Addsimps [add_0, add_Suc]; 
284  983 
\end{ttbox} 
105  984 
We state the goal for associativity of addition, and 
985 
use \ttindex{res_inst_tac} to invoke induction on~$k$: 

284  986 
\begin{ttbox} 
5205  987 
Goal "(k+m)+n = k+(m+n)"; 
105  988 
{\out Level 0} 
989 
{\out k + m + n = k + (m + n)} 

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

991 
\ttbreak 

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

993 
{\out Level 1} 

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

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

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

998 
\end{ttbox} 

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

284  1002 
\begin{ttbox} 
3114  1003 
by (Simp_tac 1); 
105  1004 
{\out Level 2} 
1005 
{\out k + m + n = k + (m + n)} 

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

1008 
\end{ttbox} 

331  1009 
The inductive step requires rewriting by the equations for addition 
14148  1010 
and with the induction hypothesis, which is also an equation. The 
3114  1011 
tactic~\ttindex{Asm_simp_tac} rewrites using the implicit 
1012 
simplification set and any useful assumptions: 

284  1013 
\begin{ttbox} 
3114  1014 
by (Asm_simp_tac 1); 
105  1015 
{\out Level 3} 
1016 
{\out k + m + n = k + (m + n)} 

1017 
{\out No subgoals!} 

284  1018 
\end{ttbox} 
310  1019 
\index{instantiation)} 
105  1020 

1021 

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

1029 
provided~$\tau$ is: 

1030 
\begin{eqnarray*} 

1031 
list & :: & (term)term 

1032 
\end{eqnarray*} 

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

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

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

1038 
Nil & :: & \alpha list \\ 

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

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

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

1042 
\end{eqnarray*} 

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

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

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

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

1049 
rev(x:xs, zs)} 

1050 
\] 

1051 

1052 
\index{examples!of theories} 

310  1053 
Theory \thydx{Prolog} extends firstorder logic in order to make use 
105  1054 
of the class~$term$ and the type~$o$. The interpreter does not use the 
5205  1055 
rules of~\texttt{FOL}. 
105  1056 
\begin{ttbox} 
1057 
Prolog = FOL + 

296  1058 
types 'a list 
105  1059 
arities list :: (term)term 
1387  1060 
consts Nil :: 'a list 
1061 
":" :: ['a, 'a list]=> 'a list (infixr 60) 

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

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

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

1066 
revNil "rev(Nil,Nil)" 

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

1068 
end 

1069 
\end{ttbox} 

1070 
\subsection{Simple executions} 

284  1071 
Repeated application of the rules solves Prolog goals. Let us 
105  1072 
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the 
5205  1073 
answer builds up in~\texttt{?x}. 
105  1074 
\begin{ttbox} 
5205  1075 
Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; 
105  1076 
{\out Level 0} 
1077 
{\out app(a : b : c : Nil, d : e : Nil, ?x)} 

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

1079 
\ttbreak 

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

1081 
{\out Level 1} 

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

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

1084 
\ttbreak 

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

1086 
{\out Level 2} 

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

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

1089 
\end{ttbox} 

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

1091 
\begin{ttbox} 

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

1093 
{\out Level 3} 

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

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

1096 
\ttbreak 

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

1098 
{\out Level 4} 

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

1100 
{\out No subgoals!} 

1101 
\end{ttbox} 

1102 

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

1106 
\begin{ttbox} 

5205  1107 
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; 
105  1108 
{\out Level 0} 
1109 
{\out app(?x, c : d : Nil, a : b : c : d : Nil)} 

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

1111 
\ttbreak 

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

1113 
{\out Level 1} 

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

1115 
{\out No subgoals!} 

1116 
\end{ttbox} 

1117 

1118 

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

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

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

105  1124 
\begin{ttbox} 
5205  1125 
Goal "app(?x, ?y, a:b:c:d:Nil)"; 
105  1126 
{\out Level 0} 
1127 
{\out app(?x, ?y, a : b : c : d : Nil)} 

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

1129 
\ttbreak 

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

1131 
{\out Level 1} 

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

1133 
{\out No subgoals!} 

1134 
\end{ttbox} 

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

105  1137 
\begin{ttbox} 
1138 
back(); 

1139 
{\out Level 1} 

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

1141 
{\out No subgoals!} 

1142 
\end{ttbox} 

1143 
The other solutions are generated similarly. 

1144 
\begin{ttbox} 

1145 
back(); 

1146 
{\out Level 1} 

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

1148 
{\out No subgoals!} 

1149 
\ttbreak 

1150 
back(); 

1151 
{\out Level 1} 

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

1153 
{\out No subgoals!} 

1154 
\ttbreak 

1155 
back(); 

1156 
{\out Level 1} 

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

1158 
{\out No subgoals!} 

1159 
\end{ttbox} 

1160 

1161 

1162 
\subsection{Depthfirst search} 

1163 
\index{search!depthfirst} 

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

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

1168 
\begin{ttbox} 

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

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

1174 
\ttbreak 

105  1175 
val rules = [appNil,appCons,revNil,revCons]; 
1176 
\ttbreak 

1177 
by (REPEAT (resolve_tac rules 1)); 

1178 
{\out Level 1} 

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

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

1181 
{\out No subgoals!} 

1182 
\end{ttbox} 

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

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

1185 
\begin{ttbox} 

5205  1186 
Goal "rev(?x, a:b:c:Nil)"; 
105  1187 
{\out Level 0} 
1188 
{\out rev(?x, a : b : c : Nil)} 

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

1190 
\ttbreak 

1191 
by (REPEAT (resolve_tac rules 1)); 

1192 
{\out Level 1} 

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

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

1195 
\end{ttbox} 

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

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

1200 
back(); 

1201 
{\out Level 1} 

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

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

1204 
\end{ttbox} 

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

1206 
\begin{ttbox} 

1207 
back(); 

1208 
{\out Level 1} 

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

1210 
{\out No subgoals!} 

1211 
\end{ttbox} 

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

105  1216 
\ttindex{has_fewer_prems} specifies that the proof state should have no 
310  1217 
subgoals. 
105  1218 
\begin{ttbox} 
1219 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 

1220 
(resolve_tac rules 1); 

1221 
\end{ttbox} 

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

1227 
{\out Level 0} 

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

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

1230 
\ttbreak 

14148  1231 
by prolog_tac; 
105  1232 
{\out Level 1} 
1233 
{\out rev(c : b : a : Nil, a : b : c : Nil)} 

1234 
{\out No subgoals!} 

1235 
\end{ttbox} 

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

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

1242 
\ttbreak 

1243 
by prolog_tac; 

1244 
{\out Level 1} 

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

1246 
{\out No subgoals!} 

1247 
\end{ttbox} 

284  1248 
Although Isabelle is much slower than a Prolog system, Isabelle 
156  1249 
tactics can exploit logic programming techniques. 
1250 