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 


6 
Look through {\em Isabelle's ObjectLogics\/} and try proving some simple


7 
theorems. You probably should begin with firstorder logic ({\tt FOL}


8 
or~{\tt LK}). Try working some of the examples provided, and others from


9 
the literature. Set theory~({\tt ZF}) and Constructive Type Theory~({\tt


10 
CTT}) form a richer world for mathematical reasoning and, again, many


11 
examples are in the literature. Higherorder logic~({\tt HOL}) is

331

12 
Isabelle's most sophisticated logic because its types and functions are


13 
identified with those of 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


39 
\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the


40 
form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$


41 
as the initial proof state and returns a list consisting of the theorems


42 
${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These metaassumptions

310

43 
are also recorded internally, allowing {\tt result} to discharge them

307

44 
in the original order.

105

45 

307

46 
Let us derive $\conj$ elimination using Isabelle.

310

47 
Until now, calling {\tt goal} has returned an empty list, which we have

105

48 
thrown away. In this example, the list contains the two premises of the


49 
rule. We bind them to the \ML\ identifiers {\tt major} and {\tt


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


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


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

310

53 
raise exception \xdx{Match}.}

105

54 
\begin{ttbox}


55 
val [major,minor] = goal FOL.thy


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


57 
{\out Level 0}


58 
{\out R}


59 
{\out 1. R}


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


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


62 
\end{ttbox}


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


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


65 
$P$ and~$Q$:


66 
\begin{ttbox}


67 
by (resolve_tac [minor] 1);


68 
{\out Level 1}


69 
{\out R}


70 
{\out 1. P}


71 
{\out 2. Q}


72 
\end{ttbox}


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


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


75 
\begin{ttbox}


76 
major RS conjunct1;


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


78 
\ttbreak


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


80 
{\out Level 2}


81 
{\out R}


82 
{\out 1. Q}


83 
\end{ttbox}


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


85 
\begin{ttbox}


86 
major RS conjunct2;


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


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


89 
{\out Level 3}


90 
{\out R}


91 
{\out No subgoals!}


92 
\end{ttbox}


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


94 
Note that it contains assumptions. Calling \ttindex{result} discharges the


95 
assumptions  both occurrences of $P\conj Q$ are discharged as one 


96 
and makes the variables schematic.


97 
\begin{ttbox}


98 
topthm();


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


100 
val conjE = result();


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


102 
\end{ttbox}


103 


104 


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

310

106 
\index{rules!derived}\index{definitions!and derived rules(}


107 

105

108 
Definitions are expressed as metalevel equalities. Let us define negation


109 
and the ifandonlyif connective:


110 
\begin{eqnarray*}


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


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


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


114 
\end{eqnarray*}

331

115 
\index{metarewriting}%

105

116 
Isabelle permits {\bf metalevel rewriting} using definitions such as


117 
these. {\bf Unfolding} replaces every instance

331

118 
of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For

105

119 
example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to


120 
\[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \]


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


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


123 


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


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

331

126 
modularity: if you later change the definitions without affecting their

105

127 
abstract properties, then most of your proofs will carry through without


128 
change. Indiscriminate unfolding makes a subgoal grow exponentially,


129 
becoming unreadable.


130 


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


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


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


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


135 
being derived.


136 


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


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


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


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

296

141 
This requires proving the following metaformulae:

105

142 
$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I)$$


143 
$$ \List{\neg P; P} \Imp Q. \eqno(\neg E)$$


144 


145 

296

146 
\subsection{Deriving the $\neg$ introduction rule}

310

147 
To derive $(\neg I)$, we may call {\tt goal} with the appropriate

105

148 
formula. Again, {\tt goal} returns a list consisting of the rule's

296

149 
premises. We bind this oneelement list to the \ML\ identifier {\tt


150 
prems}.

105

151 
\begin{ttbox}


152 
val prems = goal FOL.thy "(P ==> False) ==> ~P";


153 
{\out Level 0}


154 
{\out ~P}


155 
{\out 1. ~P}


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


157 
\end{ttbox}

310

158 
Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the

105

159 
definition of negation, unfolds that definition in the subgoals. It leaves


160 
the main goal alone.


161 
\begin{ttbox}


162 
not_def;


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


164 
by (rewrite_goals_tac [not_def]);


165 
{\out Level 1}


166 
{\out ~P}


167 
{\out 1. P > False}


168 
\end{ttbox}

310

169 
Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:

105

170 
\begin{ttbox}


171 
by (resolve_tac [impI] 1);


172 
{\out Level 2}


173 
{\out ~P}


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


175 
\ttbreak


176 
by (resolve_tac prems 1);


177 
{\out Level 3}


178 
{\out ~P}


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


180 
\end{ttbox}

296

181 
The rest of the proof is routine. Note the form of the final result.

105

182 
\begin{ttbox}


183 
by (assume_tac 1);


184 
{\out Level 4}


185 
{\out ~P}


186 
{\out No subgoals!}

296

187 
\ttbreak

105

188 
val notI = result();


189 
{\out val notI = "(?P ==> False) ==> ~?P" : thm}


190 
\end{ttbox}

310

191 
\indexbold{*notI theorem}

105

192 


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

310

194 
command starts a backward proof, as does {\tt goal}, but it also

296

195 
unfolds definitions. Thus there is no need to call


196 
\ttindex{rewrite_goals_tac}:

105

197 
\begin{ttbox}


198 
val prems = goalw FOL.thy [not_def]


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


200 
{\out Level 0}


201 
{\out ~P}


202 
{\out 1. P > False}


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


204 
\end{ttbox}


205 


206 

296

207 
\subsection{Deriving the $\neg$ elimination rule}

284

208 
Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE}

296

209 
above, with an additional step to unfold negation in the major premise.


210 
Although the {\tt goalw} command is best for this, let us

310

211 
try~{\tt goal} to see another way of unfolding definitions. After


212 
binding the premises to \ML\ identifiers, we apply \tdx{FalseE}:

105

213 
\begin{ttbox}


214 
val [major,minor] = goal FOL.thy "[ ~P; P ] ==> R";


215 
{\out Level 0}


216 
{\out R}


217 
{\out 1. R}


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


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


220 
\ttbreak


221 
by (resolve_tac [FalseE] 1);


222 
{\out Level 1}


223 
{\out R}


224 
{\out 1. False}

284

225 
\end{ttbox}


226 
Everything follows from falsity. And we can prove falsity using the


227 
premises and Modus Ponens:


228 
\begin{ttbox}

105

229 
by (resolve_tac [mp] 1);


230 
{\out Level 2}


231 
{\out R}


232 
{\out 1. ?P1 > False}


233 
{\out 2. ?P1}


234 
\end{ttbox}


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


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

296

237 
definitions, unfolds them in a theorem. Rewriting does not

105

238 
affect the theorem's hypothesis, which remains~$\neg P$:


239 
\begin{ttbox}


240 
rewrite_rule [not_def] major;


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


242 
by (resolve_tac [it] 1);


243 
{\out Level 3}


244 
{\out R}


245 
{\out 1. P}


246 
\end{ttbox}

296

247 
The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove

284

248 
using the minor premise:

105

249 
\begin{ttbox}


250 
by (resolve_tac [minor] 1);


251 
{\out Level 4}


252 
{\out R}


253 
{\out No subgoals!}


254 
val notE = result();


255 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm}


256 
\end{ttbox}

310

257 
\indexbold{*notE theorem}

105

258 


259 
\medskip

284

260 
Again, there is a simpler way of conducting this proof. Recall that


261 
the \ttindex{goalw} command unfolds definitions the conclusion; it also


262 
unfolds definitions in the premises:

105

263 
\begin{ttbox}


264 
val [major,minor] = goalw FOL.thy [not_def]


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


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


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


268 
\end{ttbox}

296

269 
Observe the difference in {\tt major}; the premises are unfolded without


270 
calling~\ttindex{rewrite_rule}. Incidentally, the four calls to


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

284

272 
of~\ttindex{RS}; this is a typical example of forward reasoning from a


273 
complex premise.

105

274 
\begin{ttbox}


275 
minor RS (major RS mp RS FalseE);


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


277 
by (resolve_tac [it] 1);


278 
{\out Level 1}


279 
{\out R}


280 
{\out No subgoals!}


281 
\end{ttbox}

310

282 
\index{definitions!and derived rules)}

105

283 

310

284 
\goodbreak\medskip\index{*"!"! symbol!in main goal}

284

285 
Finally, here is a trick that is sometimes useful. If the goal

105

286 
has an outermost metaquantifier, then \ttindex{goal} and \ttindex{goalw}

284

287 
do not return the rule's premises in the list of theorems; instead, the


288 
premises become assumptions in subgoal~1.


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

105

290 
\begin{ttbox}


291 
goalw FOL.thy [not_def] "!!P R. [ ~P; P ] ==> R";


292 
{\out Level 0}


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


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


295 
val it = [] : thm list


296 
\end{ttbox}


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

310

298 
identifiers, we refer to assumptions using {\tt eresolve_tac} or


299 
{\tt assume_tac}:

105

300 
\begin{ttbox}


301 
by (resolve_tac [FalseE] 1);


302 
{\out Level 1}


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


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


305 
\ttbreak


306 
by (eresolve_tac [mp] 1);


307 
{\out Level 2}


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


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


310 
\ttbreak


311 
by (assume_tac 1);


312 
{\out Level 3}


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


314 
{\out No subgoals!}


315 
\end{ttbox}


316 
Calling \ttindex{result} strips the metaquantifiers, so the resulting


317 
theorem is the same as before.


318 
\begin{ttbox}


319 
val notE = result();


320 
{\out val notE = "[ ~?P; ?P ] ==> ?R" : thm}


321 
\end{ttbox}


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


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


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


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


326 


327 

284

328 
\section{Defining theories}\label{sec:definingtheories}

105

329 
\index{theories!defining(}

310

330 

105

331 
Isabelle makes no distinction between simple extensions of a logic  like


332 
defining a type~$bool$ with constants~$true$ and~$false$  and defining


333 
an entire logic. A theory definition has the form


334 
\begin{ttbox}


335 
\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +


336 
classes {\it class declarations}


337 
default {\it sort}

331

338 
types {\it type declarations and synonyms}

105

339 
arities {\it arity declarations}


340 
consts {\it constant declarations}


341 
rules {\it rule declarations}


342 
translations {\it translation declarations}


343 
end


344 
ML {\it ML code}


345 
\end{ttbox}


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


347 
$S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities


348 
(overloadings of existing types), constants and rules; it can specify the


349 
default sort for type variables. A constant declaration can specify an


350 
associated concrete syntax. The translations section specifies rewrite


351 
rules on abstract syntax trees, for defining notations and abbreviations.

310

352 
\index{*ML section}


353 
The {\tt ML} section contains code to perform arbitrary syntactic

284

354 
transformations. The main declaration forms are discussed below.

303

355 
The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the

307

356 
appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.

105

357 


358 
All the declaration parts can be omitted. In the simplest case, $T$ is


359 
just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one


360 
or more other theories, inheriting their types, constants, syntax, etc.

310

361 
The theory \thydx{Pure} contains nothing but Isabelle's metalogic.

105

362 

331

363 
Each theory definition must reside in a separate file, whose name is the


364 
theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides


365 
on a file named {\tt ListFn.thy}. Isabelle uses this convention to locate the


366 
file containing a given theory; \ttindexbold{use_thy} automatically loads a


367 
theory's parents before loading the theory itself.

105

368 

331

369 
Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the


370 
file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file


371 
{\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors


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

109

373 
{\tt thy} denoting the new theory, a component for each rule, and everything


374 
declared in {\it ML code}.

105

375 


376 
Errors may arise during the translation to {\ML} (say, a misspelled keyword)


377 
or during creation of the new theory (say, a type error in a rule). But if

331

378 
all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if

105

379 
it exists. This file typically begins with the {\ML} declaration {\tt


380 
open}~$T$ and contains proofs that refer to the components of~$T$.


381 

296

382 
When a theory file is modified, many theories may have to be reloaded.


383 
Isabelle records the modification times and dependencies of theory files.

331

384 
See


385 
\iflabelundefined{sec:reloadingtheories}{the {\em Reference Manual\/}}%


386 
{\S\ref{sec:reloadingtheories}}

296

387 
for more details.


388 

105

389 


390 
\subsection{Declaring constants and rules}

310

391 
\indexbold{constants!declaring}\index{rules!declaring}


392 

296

393 
Most theories simply declare constants and rules. The {\bf constant

105

394 
declaration part} has the form


395 
\begin{ttbox}


396 
consts \(c@1\) :: "\(\tau@1\)"


397 
\vdots


398 
\(c@n\) :: "\(\tau@n\)"


399 
\end{ttbox}


400 
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are


401 
types. Each type {\em must\/} be enclosed in quotation marks. Each


402 
constant must be enclosed in quotation marks unless it is a valid


403 
identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,


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


405 
\begin{ttbox}


406 
\(c@1\), \ldots, \(c@n\) :: "\(\tau\)"


407 
\end{ttbox}


408 
The {\bf rule declaration part} has the form


409 
\begin{ttbox}


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


411 
\vdots


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


413 
\end{ttbox}


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

284

415 
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be


416 
enclosed in quotation marks.


417 

310

418 
\indexbold{definitions}

284

419 
{\bf Definitions} are rules of the form $t\equiv u$. Normally definitions


420 
should be conservative, serving only as abbreviations. As of this writing,


421 
Isabelle does not provide a separate declaration part for definitions; it


422 
is your responsibility to ensure that your definitions are conservative.


423 
However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all


424 
variables free in~$u$ are also free in~$t$.

105

425 


426 
\index{examples!of theories}


427 
This theory extends firstorder logic with two constants {\em nand} and

284

428 
{\em xor}, and declares rules to define them:


429 
\begin{ttbox}

105

430 
Gate = FOL +


431 
consts nand,xor :: "[o,o] => o"


432 
rules nand_def "nand(P,Q) == ~(P & Q)"


433 
xor_def "xor(P,Q) == P & ~Q  ~P & Q"


434 
end


435 
\end{ttbox}


436 


437 


438 
\subsection{Declaring type constructors}

303

439 
\indexbold{types!declaring}\indexbold{arities!declaring}

284

440 
%

105

441 
Types are composed of type variables and {\bf type constructors}. Each

284

442 
type constructor takes a fixed number of arguments. They are declared


443 
with an \MLlike syntax. If $list$ takes one type argument, $tree$ takes


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


445 
can be declared by

105

446 
\begin{ttbox}

284

447 
types 'a list


448 
('a,'b) tree


449 
nat

105

450 
\end{ttbox}

284

451 


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


453 
\begin{ttbox}


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


455 
\vdots


456 
\(tids@1\) \(id@n\)


457 
\end{ttbox}


458 
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$


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


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

105

461 


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


463 
\begin{ttbox}


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


465 
\vdots


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


467 
\end{ttbox}


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


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

296

470 
types; they do not declare the types themselves.

105

471 
In the simplest case, for an 0place type constructor, an arity is simply


472 
the type's class. Let us declare a type~$bool$ of class $term$, with

284

473 
constants $tt$ and~$ff$. (In firstorder logic, booleans are


474 
distinct from formulae, which have type $o::logic$.)

105

475 
\index{examples!of theories}

284

476 
\begin{ttbox}

105

477 
Bool = FOL +

284

478 
types bool

105

479 
arities bool :: term


480 
consts tt,ff :: "bool"


481 
end


482 
\end{ttbox}

296

483 
A $k$place type constructor may have arities of the form


484 
$(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.


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


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


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


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


489 
\S\ref{polymorphic}.

105

490 


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

296

492 
appearing in several arity declarations. For instance, the function type

331

493 
constructor~$fun$ has the arity $(logic,logic)logic$; in higherorder

105

494 
logic, it is declared also to have arity $(term,term)term$.


495 


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

284

497 
it arity $(term)term$, and declares constants $Nil$ and $Cons$ with

296

498 
polymorphic types:%


499 
\footnote{In the {\tt consts} part, type variable {\tt'a} has the default


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


501 
\iflabelundefined{sec:refdefiningtheories}{}%


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

105

503 
\index{examples!of theories}

284

504 
\begin{ttbox}

105

505 
List = FOL +

284

506 
types 'a list

105

507 
arities list :: (term)term


508 
consts Nil :: "'a list"


509 
Cons :: "['a, 'a list] => 'a list"


510 
end


511 
\end{ttbox}

284

512 
Multiple arity declarations may be abbreviated to a single line:

105

513 
\begin{ttbox}


514 
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)


515 
\end{ttbox}


516 


517 
\begin{warn}


518 
Arity declarations resemble constant declarations, but there are {\it no\/}


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


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


521 
\end{warn}


522 

331

523 
\subsection{Type synonyms}\indexbold{type synonyms}

303

524 
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar

307

525 
to those found in \ML. Such synonyms are defined in the type declaration part

303

526 
and are fairly self explanatory:


527 
\begin{ttbox}

307

528 
types gate = "[o,o] => o"


529 
'a pred = "'a => o"

303

530 
('a,'b)nuf = "'b => 'a"


531 
\end{ttbox}


532 
Type declarations and synonyms can be mixed arbitrarily:


533 
\begin{ttbox}


534 
types nat


535 
'a stream = "nat => 'a"

307

536 
signal = "nat stream"

303

537 
'a list


538 
\end{ttbox}

307

539 
A synonym is merely an abbreviation for some existing type expression. Hence


540 
synonyms may not be recursive! Internally all synonyms are fully expanded. As


541 
a consequence Isabelle output never contains synonyms. Their main purpose is


542 
to improve the readability of theories. Synonyms can be used just like any

303

543 
other type:


544 
\begin{ttbox}


545 
consts and,or :: "gate"


546 
negate :: "signal => signal"


547 
\end{ttbox}


548 

348

549 
\subsection{Infix and mixfix operators}

310

550 
\index{infixes}\index{examples!of theories}


551 


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


553 
following theory:

284

554 
\begin{ttbox}

105

555 
Gate2 = FOL +


556 
consts "~&" :: "[o,o] => o" (infixl 35)


557 
"#" :: "[o,o] => o" (infixl 30)


558 
rules nand_def "P ~& Q == ~(P & Q)"


559 
xor_def "P # Q == P & ~Q  ~P & Q"


560 
end


561 
\end{ttbox}

310

562 
The constant declaration part declares two leftassociating infix operators


563 
with their priorities, or precedences; they are $\nand$ of priority~35 and


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


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


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

105

567 


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


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


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


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


572 

310

573 
\bigskip\index{mixfix declarations}


574 
{\bf Mixfix} operators may have arbitrary contextfree syntaxes. Let us


575 
add a line to the constant declaration part:

284

576 
\begin{ttbox}


577 
If :: "[o,o,o] => o" ("if _ then _ else _")

105

578 
\end{ttbox}

310

579 
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt

296

580 
if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores

310

581 
denote argument positions.

105

582 

310

583 
The declaration above does not allow the {\tt if}{\tt then}{\tt else}


584 
construct to be split across several lines, even if it is too long to fit


585 
on one line. Prettyprinting information can be added to specify the


586 
layout of mixfix operators. For details, see


587 
\iflabelundefined{DefiningLogics}%


588 
{the {\it Reference Manual}, chapter `Defining Logics'}%


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


590 


591 
Mixfix declarations can be annotated with priorities, just like

105

592 
infixes. The example above is just a shorthand for

284

593 
\begin{ttbox}


594 
If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)

105

595 
\end{ttbox}

310

596 
The numeric components determine priorities. The list of integers


597 
defines, for each argument position, the minimal priority an expression


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

105

599 
construct itself. In the example above, any argument expression is

310

600 
acceptable because priorities are nonnegative, and conditionals may


601 
appear everywhere because 1000 is the highest priority. On the other


602 
hand, the declaration

284

603 
\begin{ttbox}


604 
If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)

105

605 
\end{ttbox}

284

606 
defines concrete syntax for a conditional whose first argument cannot have

310

607 
the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority


608 
of at least~100. We may of course write

284

609 
\begin{quote}\tt


610 
if (if $P$ then $Q$ else $R$) then $S$ else $T$

156

611 
\end{quote}

310

612 
because expressions in parentheses have maximal priority.

105

613 


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


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


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


617 
${<}\_,\_{>}$ for pairs.

310

618 
\index{examples!of theories}\index{mixfix declarations}

105

619 
\begin{ttbox}


620 
Prod = FOL +

284

621 
types ('a,'b) "*" (infixl 20)

105

622 
arities "*" :: (term,term)term


623 
consts fst :: "'a * 'b => 'a"


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


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


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


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


628 
end


629 
\end{ttbox}


630 


631 
\begin{warn}


632 
The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would


633 
be in the case of an infix constant. Only infix type constructors can have


634 
symbolic names like~{\tt *}. There is no general mixfix syntax for types.


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


662 
consts "0" :: "'a::arith" ("0")


663 
"1" :: "'a::arith" ("1")


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


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

105

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


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


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

296

772 
consts "0" :: "nat" ("0")

105

773 
Suc :: "nat=>nat"


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

296

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


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}


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

296

785 
Loading this theory file creates the \ML\ structure {\tt Nat}, which


786 
contains the theory and axioms. Opening structure {\tt Nat} lets us write


787 
{\tt induct} instead of {\tt Nat.induct}, and so forth.

105

788 
\begin{ttbox}


789 
open Nat;


790 
\end{ttbox}

296

791 


792 
\subsection{Proving some recursion equations}

331

793 
File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the

105

794 
natural numbers. As a trivial example, let us derive recursion equations


795 
for \verb$+$. Here is the zero case:

284

796 
\begin{ttbox}

105

797 
goalw Nat.thy [add_def] "0+n = n";


798 
{\out Level 0}


799 
{\out 0 + n = n}

284

800 
{\out 1. rec(0,n,\%x y. Suc(y)) = n}

105

801 
\ttbreak


802 
by (resolve_tac [rec_0] 1);


803 
{\out Level 1}


804 
{\out 0 + n = n}


805 
{\out No subgoals!}


806 
val add_0 = result();

284

807 
\end{ttbox}

105

808 
And here is the successor case:

284

809 
\begin{ttbox}

105

810 
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";


811 
{\out Level 0}


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

284

813 
{\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}

105

814 
\ttbreak


815 
by (resolve_tac [rec_Suc] 1);


816 
{\out Level 1}


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


818 
{\out No subgoals!}


819 
val add_Suc = result();

284

820 
\end{ttbox}

105

821 
The induction rule raises some complications, which are discussed next.


822 
\index{theories!defining)}


823 


824 


825 
\section{Refinement with explicit instantiation}

310

826 
\index{resolution!with instantiation}


827 
\index{instantiation(}


828 

105

829 
In order to employ mathematical induction, we need to refine a subgoal by


830 
the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$,


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


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


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


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


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


836 


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


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


839 
schematic variables.


840 
\begin{description}

310

841 
\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]

105

842 
instantiates the rule {\it thm} with the instantiations {\it insts}, and


843 
then performs resolution on subgoal~$i$.


844 

310

845 
\item[\ttindex{eres_inst_tac}]


846 
and \ttindex{dres_inst_tac} are similar, but perform elimresolution

105

847 
and destructresolution, respectively.


848 
\end{description}


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


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

307

851 
with no leading question marks!  and $e@1$, \ldots, $e@n$ are

105

852 
expressions giving their instantiations. The expressions are typechecked


853 
in the context of a particular subgoal: free variables receive the same


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


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


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


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


858 


859 
\subsection{A simple proof by induction}

310

860 
\index{examples!of induction}

105

861 
Let us prove that no natural number~$k$ equals its own successor. To


862 
use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good


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

284

864 
\begin{ttbox}

105

865 
goal Nat.thy "~ (Suc(k) = k)";


866 
{\out Level 0}


867 
{\out ~Suc(k) = k}


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


869 
\ttbreak


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


871 
{\out Level 1}


872 
{\out ~Suc(k) = k}


873 
{\out 1. ~Suc(0) = 0}


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

284

875 
\end{ttbox}

105

876 
We should check that Isabelle has correctly applied induction. Subgoal~1


877 
is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,


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

310

879 
The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the


880 
other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}:

284

881 
\begin{ttbox}

105

882 
by (resolve_tac [notI] 1);


883 
{\out Level 2}


884 
{\out ~Suc(k) = k}


885 
{\out 1. Suc(0) = 0 ==> False}


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


887 
\ttbreak


888 
by (eresolve_tac [Suc_neq_0] 1);


889 
{\out Level 3}


890 
{\out ~Suc(k) = k}


891 
{\out 1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}

284

892 
\end{ttbox}

105

893 
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.

284

894 
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from


895 
$Suc(Suc(x)) = Suc(x)$:


896 
\begin{ttbox}

105

897 
by (resolve_tac [notI] 1);


898 
{\out Level 4}


899 
{\out ~Suc(k) = k}


900 
{\out 1. !!x. [ ~Suc(x) = x; Suc(Suc(x)) = Suc(x) ] ==> False}


901 
\ttbreak


902 
by (eresolve_tac [notE] 1);


903 
{\out Level 5}


904 
{\out ~Suc(k) = k}


905 
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}


906 
\ttbreak


907 
by (eresolve_tac [Suc_inject] 1);


908 
{\out Level 6}


909 
{\out ~Suc(k) = k}


910 
{\out No subgoals!}

284

911 
\end{ttbox}

105

912 


913 


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


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


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


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


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


919 
complex formulae, our luck fails.

284

920 
\begin{ttbox}

105

921 
goal Nat.thy "(k+m)+n = k+(m+n)";


922 
{\out Level 0}


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


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


925 
\ttbreak


926 
by (resolve_tac [induct] 1);


927 
{\out Level 1}


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


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


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

284

931 
\end{ttbox}


932 
This proof requires induction on~$k$. The occurrence of~0 in subgoal~1


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


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


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


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


937 
the tactic.


938 
\begin{ttbox}

105

939 
back();


940 
{\out Level 1}


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


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


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

284

944 
\end{ttbox}


945 
Now induction has been applied to~$m+n$. This is equally useless. Let us


946 
call \ttindex{back} again.


947 
\begin{ttbox}

105

948 
back();


949 
{\out Level 1}


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


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

284

952 
{\out 2. !!x. k + m + x = k + (m + x) ==>}


953 
{\out k + m + Suc(x) = k + (m + Suc(x))}


954 
\end{ttbox}

105

955 
Now induction has been applied to~$n$. What is the next alternative?

284

956 
\begin{ttbox}

105

957 
back();


958 
{\out Level 1}


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


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


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

284

962 
\end{ttbox}

105

963 
Inspecting subgoal~1 reveals that induction has been applied to just the


964 
second occurrence of~$n$. This perfectly legitimate induction is useless

310

965 
here.


966 


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


968 
number is exponential in the size of the formula.

105

969 


970 
\subsection{Proving that addition is associative}

331

971 
Let us invoke the induction rule properly, using~{\tt

310

972 
res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's


973 
simplification tactics, which are described in


974 
\iflabelundefined{simpchap}%


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

284

976 

310

977 
\index{simplification}\index{examples!of simplification}


978 


979 
Isabelle's simplification tactics repeatedly apply equations to a subgoal,


980 
perhaps proving it. For efficiency, the rewrite rules must be


981 
packaged into a {\bf simplification set},\index{simplification sets}


982 
or {\bf simpset}. We take the standard simpset for firstorder logic and

331

983 
insert the equations proved in the previous section, namely

310

984 
$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:

284

985 
\begin{ttbox}

105

986 
val add_ss = FOL_ss addrews [add_0, add_Suc];

284

987 
\end{ttbox}

105

988 
We state the goal for associativity of addition, and


989 
use \ttindex{res_inst_tac} to invoke induction on~$k$:

284

990 
\begin{ttbox}

105

991 
goal Nat.thy "(k+m)+n = k+(m+n)";


992 
{\out Level 0}


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


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


995 
\ttbreak


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


997 
{\out Level 1}


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


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

284

1000 
{\out 2. !!x. x + m + n = x + (m + n) ==>}


1001 
{\out Suc(x) + m + n = Suc(x) + (m + n)}


1002 
\end{ttbox}

105

1003 
The base case holds easily; both sides reduce to $m+n$. The


1004 
tactic~\ttindex{simp_tac} rewrites with respect to the given simplification

331

1005 
set, applying the rewrite rules for addition:

284

1006 
\begin{ttbox}

105

1007 
by (simp_tac add_ss 1);


1008 
{\out Level 2}


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

284

1010 
{\out 1. !!x. x + m + n = x + (m + n) ==>}


1011 
{\out Suc(x) + m + n = Suc(x) + (m + n)}


1012 
\end{ttbox}

331

1013 
The inductive step requires rewriting by the equations for addition

105

1014 
together the induction hypothesis, which is also an equation. The


1015 
tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any


1016 
useful assumptions:

284

1017 
\begin{ttbox}

105

1018 
by (asm_simp_tac add_ss 1);


1019 
{\out Level 3}


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


1021 
{\out No subgoals!}

284

1022 
\end{ttbox}

310

1023 
\index{instantiation)}

105

1024 


1025 

284

1026 
\section{A Prolog interpreter}

105

1027 
\index{Prolog interpreterbold}

284

1028 
To demonstrate the power of tacticals, let us construct a Prolog

105

1029 
interpreter and execute programs involving lists.\footnote{To run these

331

1030 
examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program

105

1031 
consists of a theory. We declare a type constructor for lists, with an


1032 
arity declaration to say that $(\tau)list$ is of class~$term$


1033 
provided~$\tau$ is:


1034 
\begin{eqnarray*}


1035 
list & :: & (term)term


1036 
\end{eqnarray*}


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


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

284

1039 
predicate~$rev$. (In Prolog, functions on lists are expressed as

105

1040 
predicates.)


1041 
\begin{eqnarray*}


1042 
Nil & :: & \alpha list \\


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


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


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


1046 
\end{eqnarray*}

284

1047 
The predicate $app$ should satisfy the Prologstyle rules

105

1048 
\[ {app(Nil,ys,ys)} \qquad


1049 
{app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]


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


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


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


1053 
rev(x:xs, zs)}


1054 
\]


1055 


1056 
\index{examples!of theories}

310

1057 
Theory \thydx{Prolog} extends firstorder logic in order to make use

105

1058 
of the class~$term$ and the type~$o$. The interpreter does not use the

310

1059 
rules of~{\tt FOL}.

105

1060 
\begin{ttbox}


1061 
Prolog = FOL +

296

1062 
types 'a list

105

1063 
arities list :: (term)term


1064 
consts Nil :: "'a list"


1065 
":" :: "['a, 'a list]=> 'a list" (infixr 60)


1066 
app :: "['a list, 'a list, 'a list] => o"


1067 
rev :: "['a list, 'a list] => o"


1068 
rules appNil "app(Nil,ys,ys)"


1069 
appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"


1070 
revNil "rev(Nil,Nil)"


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


1072 
end


1073 
\end{ttbox}


1074 
\subsection{Simple executions}

284

1075 
Repeated application of the rules solves Prolog goals. Let us

105

1076 
append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the


1077 
answer builds up in~{\tt ?x}.


1078 
\begin{ttbox}


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


1080 
{\out Level 0}


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


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


1083 
\ttbreak


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


1085 
{\out Level 1}


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


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


1088 
\ttbreak


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


1090 
{\out Level 2}


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


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


1093 
\end{ttbox}


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


1095 
\begin{ttbox}


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


1097 
{\out Level 3}


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


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


1100 
\ttbreak


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


1102 
{\out Level 4}


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


1104 
{\out No subgoals!}


1105 
\end{ttbox}


1106 

284

1107 
Prolog can run functions backwards. Which list can be appended

105

1108 
with $[c,d]$ to produce $[a,b,c,d]$?


1109 
Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:


1110 
\begin{ttbox}


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


1112 
{\out Level 0}


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


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


1115 
\ttbreak


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


1117 
{\out Level 1}


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


1119 
{\out No subgoals!}


1120 
\end{ttbox}


1121 


1122 

310

1123 
\subsection{Backtracking}\index{backtracking!Prolog style}

296

1124 
Prolog backtracking can answer questions that have multiple solutions.


1125 
Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This


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


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

105

1128 
\begin{ttbox}


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


1130 
{\out Level 0}


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


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


1133 
\ttbreak


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


1135 
{\out Level 1}


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


1137 
{\out No subgoals!}


1138 
\end{ttbox}

284

1139 
Isabelle can lazily generate all the possibilities. The \ttindex{back}


1140 
command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:

105

1141 
\begin{ttbox}


1142 
back();


1143 
{\out Level 1}


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


1145 
{\out No subgoals!}


1146 
\end{ttbox}


1147 
The other solutions are generated similarly.


1148 
\begin{ttbox}


1149 
back();


1150 
{\out Level 1}


1151 
{\out app(a : b : Nil, c : 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 : Nil, d : Nil, a : b : c : d : Nil)}


1157 
{\out No subgoals!}


1158 
\ttbreak


1159 
back();


1160 
{\out Level 1}


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


1162 
{\out No subgoals!}


1163 
\end{ttbox}


1164 


1165 


1166 
\subsection{Depthfirst search}


1167 
\index{search!depthfirst}


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


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


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


1171 
terminates in a few seconds.


1172 
\begin{ttbox}


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


1174 
{\out Level 0}


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

284

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


1177 
{\out ?w)}


1178 
\ttbreak

105

1179 
val rules = [appNil,appCons,revNil,revCons];


1180 
\ttbreak


1181 
by (REPEAT (resolve_tac rules 1));


1182 
{\out Level 1}


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


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


1185 
{\out No subgoals!}


1186 
\end{ttbox}


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


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


1189 
\begin{ttbox}


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


1191 
{\out Level 0}


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


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


1194 
\ttbreak


1195 
by (REPEAT (resolve_tac rules 1));


1196 
{\out Level 1}


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


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


1199 
\end{ttbox}


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

331

1201 
subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$

105

1202 
equals~$[a,b,c]$. Backtracking explores other outcomes.


1203 
\begin{ttbox}


1204 
back();


1205 
{\out Level 1}


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


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


1208 
\end{ttbox}


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


1210 
\begin{ttbox}


1211 
back();


1212 
{\out Level 1}


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


1214 
{\out No subgoals!}


1215 
\end{ttbox}

310

1216 
\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a


1217 
search tactical. {\tt REPEAT} stops when it cannot continue, regardless of


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


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

105

1220 
\ttindex{has_fewer_prems} specifies that the proof state should have no

310

1221 
subgoals.

105

1222 
\begin{ttbox}


1223 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)


1224 
(resolve_tac rules 1);


1225 
\end{ttbox}

284

1226 
Since Prolog uses depthfirst search, this tactic is a (slow!)

296

1227 
Prolog interpreter. We return to the start of the proof using


1228 
\ttindex{choplev}, and apply {\tt prolog_tac}:

105

1229 
\begin{ttbox}


1230 
choplev 0;


1231 
{\out Level 0}


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


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


1234 
\ttbreak


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


1236 
{\out Level 1}


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


1238 
{\out No subgoals!}


1239 
\end{ttbox}


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


1241 
\begin{ttbox}


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


1243 
{\out Level 0}


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


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


1246 
\ttbreak


1247 
by prolog_tac;


1248 
{\out Level 1}


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


1250 
{\out No subgoals!}


1251 
\end{ttbox}

284

1252 
Although Isabelle is much slower than a Prolog system, Isabelle

156

1253 
tactics can exploit logic programming techniques.


1254 
