author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
permissions  rwrr 
284  1 
\part{Advanced Methods} 
105  2 
Before continuing, it might be wise to try some of your own examples in 
3 
Isabelle, reinforcing your knowledge of the basic functions. 

4 

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

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

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

3103  10 
mathematical reasoning and, again, many examples are in the 
5205  11 
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

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

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

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

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

18 
Even experienced users plan large proofs on paper. 

19 

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

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

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

23 

24 

25 
\section{Deriving rules in Isabelle} 

26 
\index{rules!derived} 

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

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

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

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

33 

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

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

307  38 
The subgoal module supports the derivation of rules, as discussed in 
5205  39 
\S\ref{deriving}. When the \ttindex{Goal} command is supplied a formula of 
40 
the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two 

41 
possibilities: 

42 
\begin{itemize} 

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

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

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

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

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

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

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

14148  50 
These metalevel assumptions are also recorded internally, allowing 
5205  51 
\texttt{result} (which is called by \texttt{qed}) to discharge them in the 
52 
original order. 

53 
\end{itemize} 

54 
Rules that discharge assumptions or introduce eigenvariables have complex 

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

57 
\ttindex{show_hyps} flag: 

58 
\begin{ttbox} 

59 
set show_hyps; 

60 
{\out val it = true : bool} 

61 
\end{ttbox} 

105  62 

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

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

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

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

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

70 
\xdx{Match}.} 

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

75 
{\out R} 

76 
{\out 1. R} 

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

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

79 
\end{ttbox} 

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

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

84 
by (resolve_tac [minor] 1); 

85 
{\out Level 1} 

86 
{\out R} 

87 
{\out 1. P} 

88 
{\out 2. Q} 

89 
\end{ttbox} 

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

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

92 
\begin{ttbox} 

93 
major RS conjunct1; 

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

95 
\ttbreak 

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

97 
{\out Level 2} 

98 
{\out R} 

99 
{\out 1. Q} 

100 
\end{ttbox} 

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

102 
\begin{ttbox} 

103 
major RS conjunct2; 

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

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

106 
{\out Level 3} 

107 
{\out R} 

108 
{\out No subgoals!} 

109 
\end{ttbox} 

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

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

113 
one  and makes the variables schematic. 

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

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

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

120 

121 

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

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

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

127 
\begin{eqnarray*} 

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

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

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

131 
\end{eqnarray*} 

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

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

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

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

140 

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

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

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

146 
becoming unreadable. 

147 

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

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

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

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

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

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

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

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

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

105  161 

162 

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

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

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

171 
{\out 1. ~P} 

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

173 
\end{ttbox} 

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

177 
\begin{ttbox} 

178 
not_def; 

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

180 
by (rewrite_goals_tac [not_def]); 

181 
{\out Level 1} 

182 
{\out ~P} 

183 
{\out 1. P > False} 

184 
\end{ttbox} 

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

188 
{\out Level 2} 

189 
{\out ~P} 

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

191 
\ttbreak 

192 
by (resolve_tac prems 1); 

193 
{\out Level 3} 

194 
{\out ~P} 

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

196 
\end{ttbox} 

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

200 
{\out Level 4} 

201 
{\out ~P} 

202 
{\out No subgoals!} 

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

310  207 
\indexbold{*notI theorem} 
105  208 

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

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

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

217 
{\out ~P} 

218 
{\out 1. P > False} 

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

220 
\end{ttbox} 

221 

222 

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

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

233 
\end{ttbox} 

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

235 
\begin{ttbox} 

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

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

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

244 
\begin{ttbox} 

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

249 
\ttbreak 

250 
by (assume_tac 1); 

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

5205  258 

105  259 

260 
\medskip 

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

263 
applying the function \ttindex{rewrite_rule}. 

105  264 

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

267 

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

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

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

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

276 
classes {\it class declarations} 

277 
default {\it sort} 

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

283 
defs {\it metalogical definitions} 

105  284 
rules {\it rule declarations} 
285 
end 

286 
ML {\it ML code} 

287 
\end{ttbox} 

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

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

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

292 
associated concrete syntax. The translations section specifies 

293 
rewrite rules on abstract syntax trees, handling notations and 

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

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

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

300 
objectlogics may add further theory sections, for example 

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

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

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

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

307 
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

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

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

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

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

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

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

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

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

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

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

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

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

332 
times and dependencies of theory files. See 

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

296  335 
for more details. 
336 

105  337 

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

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

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

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

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

354 
\begin{ttbox} 

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

358 
\begin{ttbox} 

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

360 
\vdots 

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

362 
\end{ttbox} 

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

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

367 
rules when defining a new logic. 

284  368 

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

372 
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

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

1084  376 

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

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

381 
your system can be consistent and yet still wrong. 

3103  382 

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

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

385 
xor}: 

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

392 
\end{ttbox} 

393 

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

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

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

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

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

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

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

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

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

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

404 
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

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

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

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

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

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

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

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

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

413 

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

414 

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

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

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

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

419 
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

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

422 
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

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

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

425 
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

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

427 
\end{warn} 
105  428 

429 
\subsection{Declaring type constructors} 

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

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

436 
can be declared by 

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

440 
nat 

105  441 
\end{ttbox} 
284  442 

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

444 
\begin{ttbox} 

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

446 
\vdots 

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

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

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

105  452 

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

454 
\begin{ttbox} 

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

456 
\vdots 

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

458 
\end{ttbox} 

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

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

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

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

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

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

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

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

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

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

480 
\S\ref{polymorphic}. 

105  481 

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

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

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

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

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

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

105  501 
end 
502 
\end{ttbox} 

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

506 
\end{ttbox} 

507 

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

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

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

512 
%\end{warn} 

105  513 

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

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

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

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

524 
\begin{ttbox} 

525 
types nat 

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

303  528 
'a list 
529 
\end{ttbox} 

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

532 
fully expanded. As a consequence Isabelle output never contains 

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

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

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

303  538 
\end{ttbox} 
539 

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

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

544 
following theory: 

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

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

552 
\end{ttbox} 

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

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

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

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

105  558 

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

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

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

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

563 

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

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

568 
\end{ttbox} 

569 

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

572 
add a line to the constant declaration part: 

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

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

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

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

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

587 

588 
Mixfix declarations can be annotated with priorities, just like 

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

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

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

599 
hand, the declaration 

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

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

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

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

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

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

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

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

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

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

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

625 
end 

626 
\end{ttbox} 

627 

628 
\begin{warn} 

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

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

636 

637 
\subsection{Overloading} 

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

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

640 
\begin{ttbox} 

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

642 
\vdots 

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

644 
\end{ttbox} 

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

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

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

648 
subclass of $k$ existing classes: 

649 
\begin{ttbox} 

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

651 
\end{ttbox} 

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

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

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

660 
classes arith < term 

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

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

105  664 
end 
665 
\end{ttbox} 

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

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

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

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

670 

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

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

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

674 
\index{examples!of theories} 

675 
\begin{ttbox} 

676 
BoolNat = Arith + 

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

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

683 
nat1 "1 = Suc(0)" 

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

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

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

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

688 
end 

689 
\end{ttbox} 

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

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

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

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

105  698 

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

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

105  702 
demonstrating many of the theory extension features. 
703 

704 

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

706 
\index{examples!of theories} 

707 

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

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

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

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

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

717 
\] 

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

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

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

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

722 
formalize mathematical induction as 

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

724 

725 
\noindent 

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

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

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

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

730 
better with Isabelle's simplifier.} 

731 
$(Suc\_neq\_0)$ is 

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

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

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

735 

736 
\noindent 

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

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

739 
and obeys the equations 

740 
\begin{eqnarray*} 

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

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

743 
\end{eqnarray*} 

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

745 
should satisfy 

746 
\begin{eqnarray*} 

747 
0+n & = & n \\ 

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

749 
\end{eqnarray*} 

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

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

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

755 
\begin{eqnarray*} 

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

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

758 
\end{eqnarray*} 

759 

760 

761 
\subsection{Declaring the theory to Isabelle} 

762 
\index{examples!of theories} 

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

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

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

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

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

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

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

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

3103  786 
contains the theory and axioms. 
296  787 

788 
\subsection{Proving some recursion equations} 

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

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

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

799 
{\out Level 1} 

800 
{\out 0 + n = n} 

801 
{\out No subgoals!} 

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

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

812 
{\out Level 1} 

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

814 
{\out No subgoals!} 

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

819 

820 

821 
\section{Refinement with explicit instantiation} 

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

824 

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

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

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

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

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

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

832 

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

836 
\begin{description} 

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

840 

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

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

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

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

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

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

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

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

855 
\subsection{A simple proof by induction} 

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

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

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

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

867 
{\out Level 1} 

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

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

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

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

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

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

885 
{\out Level 3} 

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

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

892 
\begin{ttbox} 

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

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

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

899 
{\out Level 5} 

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

903 
by (eresolve_tac [Suc_inject] 1); 

904 
{\out Level 6} 

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

909 

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

915 
complex formulae, our luck fails. 

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

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

921 
\ttbreak 

922 
by (resolve_tac [induct] 1); 

923 
{\out Level 1} 

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

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

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

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

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

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

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

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

933 
the tactic. 

934 
\begin{ttbox} 

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

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

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

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

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

942 
call \ttindex{back} again. 

943 
\begin{ttbox} 

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

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

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

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

950 
\end{ttbox} 

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

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

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

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

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

310  961 
here. 
962 

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

964 
number is exponential in the size of the formula. 

105  965 

966 
\subsection{Proving that addition is associative} 

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

970 
\iflabelundefined{simpchap}% 

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

284  972 

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

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

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

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

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

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

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

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

990 
\ttbreak 

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

992 
{\out Level 1} 

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

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

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

997 
\end{ttbox} 

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

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

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

1007 
\end{ttbox} 

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

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

1016 
{\out No subgoals!} 

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

1020 

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

1028 
provided~$\tau$ is: 

1029 
\begin{eqnarray*} 

1030 
list & :: & (term)term 

1031 
\end{eqnarray*} 

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

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

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

1037 
Nil & :: & \alpha list \\ 

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

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

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

1041 
\end{eqnarray*} 

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

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

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

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

1048 
rev(x:xs, zs)} 

1049 
\] 

1050 

1051 
\index{examples!of theories} 

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

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

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

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

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

1065 
revNil "rev(Nil,Nil)" 

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

1067 
end 

1068 
\end{ttbox} 

1069 
\subsection{Simple executions} 

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

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

1078 
\ttbreak 

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

1080 
{\out Level 1} 

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

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

1083 
\ttbreak 

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

1085 
{\out Level 2} 

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

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

1088 
\end{ttbox} 

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

1090 
\begin{ttbox} 

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

1092 
{\out Level 3} 

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

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

1095 
\ttbreak 

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

1097 
{\out Level 4} 

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

1099 
{\out No subgoals!} 

1100 
\end{ttbox} 

1101 

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

1105 
\begin{ttbox} 

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

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

1110 
\ttbreak 

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

1112 
{\out Level 1} 

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

1114 
{\out No subgoals!} 

1115 
\end{ttbox} 

1116 

1117 

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

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

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

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

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

1128 
\ttbreak 

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

1130 
{\out Level 1} 

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

1132 
{\out No subgoals!} 

1133 
\end{ttbox} 

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

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

1138 
{\out Level 1} 

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

1140 
{\out No subgoals!} 

1141 
\end{ttbox} 

1142 
The other solutions are generated similarly. 

1143 
\begin{ttbox} 

1144 
back(); 

1145 
{\out Level 1} 

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

1147 
{\out No subgoals!} 

1148 
\ttbreak 

1149 
back(); 

1150 
{\out Level 1} 

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

1152 
{\out No subgoals!} 

1153 
\ttbreak 

1154 
back(); 

1155 
{\out Level 1} 

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

1157 
{\out No subgoals!} 

1158 
\end{ttbox} 

1159 

1160 

1161 
\subsection{Depthfirst search} 

1162 
\index{search!depthfirst} 

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

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

1167 
\begin{ttbox} 

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

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

1173 
\ttbreak 

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

1176 
by (REPEAT (resolve_tac rules 1)); 

1177 
{\out Level 1} 

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

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

1180 
{\out No subgoals!} 

1181 
\end{ttbox} 

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

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

1184 
\begin{ttbox} 

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

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

1189 
\ttbreak 

1190 
by (REPEAT (resolve_tac rules 1)); 

1191 
{\out Level 1} 

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

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

1194 
\end{ttbox} 

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

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

1199 
back(); 

1200 
{\out Level 1} 

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

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

1203 
\end{ttbox} 

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

1205 
\begin{ttbox} 

1206 
back(); 

1207 
{\out Level 1} 

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

1209 
{\out No subgoals!} 

1210 
\end{ttbox} 

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

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

1219 
(resolve_tac rules 1); 

1220 
\end{ttbox} 

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

1226 
{\out Level 0} 

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

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

1229 
\ttbreak 

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

1233 
{\out No subgoals!} 

1234 
\end{ttbox} 

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

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

1241 
\ttbreak 

1242 
by prolog_tac; 

1243 
{\out Level 1} 

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

1245 
{\out No subgoals!} 

1246 
\end{ttbox} 

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