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}

841

341 
translations {\it translation declarations}

1185

342 
defs {\it definitions}

105

343 
rules {\it rule declarations}


344 
end


345 
ML {\it ML code}


346 
\end{ttbox}


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


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


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


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


351 
associated concrete syntax. The translations section specifies rewrite


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

310

353 
\index{*ML section}


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

284

355 
transformations. The main declaration forms are discussed below.

303

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

307

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

105

358 

1084

359 
All the declaration parts can be omitted or repeated and may appear in any


360 
order, except that the {\ML} section must be last. In the simplest case, $T$


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


362 
more other theories, inheriting their types, constants, syntax, etc. The


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

105

364 

331

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


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


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


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


369 
theory's parents before loading the theory itself.

105

370 

331

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


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


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


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

109

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


376 
declared in {\it ML code}.

105

377 


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


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

331

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

105

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


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


383 

296

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


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

331

386 
See


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


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

296

389 
for more details.


390 

105

391 

1084

392 
\subsection{Declaring constants, definitions and rules}

310

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


394 

1084

395 
Most theories simply declare constants, definitions and rules. The {\bf


396 
constant declaration part} has the form

105

397 
\begin{ttbox}


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


399 
\vdots


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


401 
\end{ttbox}


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


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


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


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


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


407 
\begin{ttbox}


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


409 
\end{ttbox}


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


411 
\begin{ttbox}


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


413 
\vdots


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


415 
\end{ttbox}


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

284

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


418 
enclosed in quotation marks.


419 

1084

420 
\indexbold{definitions} The {\bf definition part} is similar, but with the


421 
keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are rules of the


422 
form $t\equiv u$, and should serve only as abbreviations. Isabelle checks for


423 
common errors in definitions, such as extra variables on the righthard side.


424 
Determined users can write nonconservative `definitions' by using mutual


425 
recursion, for example; the consequences of such actions are their


426 
responsibility.

105

427 

1084

428 


429 
\index{examples!of theories}


430 
This theory extends firstorder logic by declaring and defining two constants,


431 
{\em nand} and {\em xor}:

284

432 
\begin{ttbox}

105

433 
Gate = FOL +


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

1084

435 
defs nand_def "nand(P,Q) == ~(P & Q)"

105

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


437 
end


438 
\end{ttbox}


439 


440 


441 
\subsection{Declaring type constructors}

303

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

284

443 
%

105

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

284

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


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


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


448 
can be declared by

105

449 
\begin{ttbox}

284

450 
types 'a list


451 
('a,'b) tree


452 
nat

105

453 
\end{ttbox}

284

454 


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


456 
\begin{ttbox}


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


458 
\vdots

841

459 
\(tids@n\) \(id@n\)

284

460 
\end{ttbox}


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


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


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

105

464 


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


466 
\begin{ttbox}


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


468 
\vdots


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


470 
\end{ttbox}


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


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

296

473 
types; they do not declare the types themselves.

105

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


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

284

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


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

105

478 
\index{examples!of theories}

284

479 
\begin{ttbox}

105

480 
Bool = FOL +

284

481 
types bool

105

482 
arities bool :: term


483 
consts tt,ff :: "bool"


484 
end


485 
\end{ttbox}

296

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


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


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


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


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


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


492 
\S\ref{polymorphic}.

105

493 


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

296

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

331

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

105

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


498 


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

284

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

296

501 
polymorphic types:%


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


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


504 
\iflabelundefined{sec:refdefiningtheories}{}%


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

105

506 
\index{examples!of theories}

284

507 
\begin{ttbox}

105

508 
List = FOL +

284

509 
types 'a list

105

510 
arities list :: (term)term


511 
consts Nil :: "'a list"


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


513 
end


514 
\end{ttbox}

284

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

105

516 
\begin{ttbox}


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


518 
\end{ttbox}


519 


520 
\begin{warn}


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


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


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


524 
\end{warn}


525 

331

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

303

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

307

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

303

529 
and are fairly self explanatory:


530 
\begin{ttbox}

307

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


532 
'a pred = "'a => o"

303

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


534 
\end{ttbox}


535 
Type declarations and synonyms can be mixed arbitrarily:


536 
\begin{ttbox}


537 
types nat


538 
'a stream = "nat => 'a"

307

539 
signal = "nat stream"

303

540 
'a list


541 
\end{ttbox}

307

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


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


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


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

303

546 
other type:


547 
\begin{ttbox}


548 
consts and,or :: "gate"


549 
negate :: "signal => signal"


550 
\end{ttbox}


551 

348

552 
\subsection{Infix and mixfix operators}

310

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


554 


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


556 
following theory:

284

557 
\begin{ttbox}

105

558 
Gate2 = FOL +


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


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

1084

561 
defs nand_def "P ~& Q == ~(P & Q)"

105

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


563 
end


564 
\end{ttbox}

310

565 
The constant declaration part declares two leftassociating infix operators


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


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


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


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

105

570 


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


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


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


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


575 

310

576 
\bigskip\index{mixfix declarations}


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


578 
add a line to the constant declaration part:

284

579 
\begin{ttbox}


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

105

581 
\end{ttbox}

310

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

296

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

310

584 
denote argument positions.

105

585 

310

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


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


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


589 
layout of mixfix operators. For details, see


590 
\iflabelundefined{DefiningLogics}%


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


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


593 


594 
Mixfix declarations can be annotated with priorities, just like

105

595 
infixes. The example above is just a shorthand for

284

596 
\begin{ttbox}


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

105

598 
\end{ttbox}

310

599 
The numeric components determine priorities. The list of integers


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


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

105

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

310

603 
acceptable because priorities are nonnegative, and conditionals may


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


605 
hand, the declaration

284

606 
\begin{ttbox}


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

105

608 
\end{ttbox}

284

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

310

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


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

284

612 
\begin{quote}\tt


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

156

614 
\end{quote}

310

615 
because expressions in parentheses have maximal priority.

105

616 


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


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


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

1084

620 
${<}\_,\_{>}$ for pairs. We also see a rule declaration part.

310

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

105

622 
\begin{ttbox}


623 
Prod = FOL +

284

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

105

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


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


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


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


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


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


631 
end


632 
\end{ttbox}


633 


634 
\begin{warn}


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


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


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


638 
\end{warn}


639 


640 


641 
\subsection{Overloading}


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


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


644 
\begin{ttbox}


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


646 
\vdots


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


648 
\end{ttbox}


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


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


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


652 
subclass of $k$ existing classes:


653 
\begin{ttbox}


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


655 
\end{ttbox}

296

656 
Type classes allow constants to be overloaded. As suggested in

307

657 
\S\ref{polymorphic}, let us define the class $arith$ of arithmetic

296

658 
types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}


659 
\alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of


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

310

661 
\index{examples!of theories}\index{constants!overloaded}

105

662 
\begin{ttbox}


663 
Arith = FOL +


664 
classes arith < term


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


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


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


668 
end


669 
\end{ttbox}


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


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


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


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


674 


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


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


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


678 
\index{examples!of theories}


679 
\begin{ttbox}


680 
BoolNat = Arith +

348

681 
types bool nat


682 
arities bool, nat :: arith

105

683 
consts Suc :: "nat=>nat"

284

684 
\ttbreak

105

685 
rules add0 "0 + n = n::nat"


686 
addS "Suc(m)+n = Suc(m+n)"


687 
nat1 "1 = Suc(0)"


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


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


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


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


692 
end


693 
\end{ttbox}


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


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


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


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

284

698 
collapse $nat$ to a trivial type:

105

699 
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]

296

700 

105

701 

296

702 
\section{Theory example: the natural numbers}


703 


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

105

705 
demonstrating many of the theory extension features.


706 


707 


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


709 
\index{examples!of theories}


710 

284

711 
Section\ts\ref{sec:logicalsyntax} has formalized a firstorder logic,


712 
including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.


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

310

714 
freeness of $0$ and~$Suc$:\index{axioms!Peano}

307

715 
\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}

105

716 
\qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}


717 
\]


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


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


720 
\]


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


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


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


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


725 
formalize mathematical induction as


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


727 


728 
\noindent


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


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


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


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


733 
better with Isabelle's simplifier.}


734 
$(Suc\_neq\_0)$ is


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


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


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


738 


739 
\noindent


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


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


742 
and obeys the equations


743 
\begin{eqnarray*}


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


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


746 
\end{eqnarray*}


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


748 
should satisfy


749 
\begin{eqnarray*}


750 
0+n & = & n \\


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


752 
\end{eqnarray*}

296

753 
Primitive recursion appears to pose difficulties: firstorder logic has no


754 
functionvalued expressions. We again take advantage of the metalogic,


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

105

756 
polymorphic over any type of class~$term$, and declare the addition


757 
function:


758 
\begin{eqnarray*}


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


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


761 
\end{eqnarray*}


762 


763 


764 
\subsection{Declaring the theory to Isabelle}


765 
\index{examples!of theories}

310

766 
Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,

105

767 
which contains only classical logic with no natural numbers. We declare

307

768 
the 0place type constructor $nat$ and the associated constants. Note that


769 
the constant~0 requires a mixfix annotation because~0 is not a legal


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

310

771 
\begin{ttbox}\index{mixfix declarations}

105

772 
Nat = FOL +

284

773 
types nat

105

774 
arities nat :: term

296

775 
consts "0" :: "nat" ("0")

105

776 
Suc :: "nat=>nat"


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

296

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


779 
rules Suc_inject "Suc(m)=Suc(n) ==> m=n"

105

780 
Suc_neq_0 "Suc(m)=0 ==> R"

296

781 
induct "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)"

105

782 
rec_0 "rec(0,a,f) = a"


783 
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))"

296

784 
add_def "m+n == rec(m, n, \%x y. Suc(y))"

105

785 
end


786 
\end{ttbox}


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

296

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


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


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

105

791 
\begin{ttbox}


792 
open Nat;


793 
\end{ttbox}

296

794 


795 
\subsection{Proving some recursion equations}

331

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

105

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


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

284

799 
\begin{ttbox}

105

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


801 
{\out Level 0}


802 
{\out 0 + n = n}

284

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

105

804 
\ttbreak


805 
by (resolve_tac [rec_0] 1);


806 
{\out Level 1}


807 
{\out 0 + n = n}


808 
{\out No subgoals!}


809 
val add_0 = result();

284

810 
\end{ttbox}

105

811 
And here is the successor case:

284

812 
\begin{ttbox}

105

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


814 
{\out Level 0}


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

284

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

105

817 
\ttbreak


818 
by (resolve_tac [rec_Suc] 1);


819 
{\out Level 1}


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


821 
{\out No subgoals!}


822 
val add_Suc = result();

284

823 
\end{ttbox}

105

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


825 
\index{theories!defining)}


826 


827 


828 
\section{Refinement with explicit instantiation}

310

829 
\index{resolution!with instantiation}


830 
\index{instantiation(}


831 

105

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


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


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


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


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


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


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


839 


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


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


842 
schematic variables.


843 
\begin{description}

310

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

105

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


846 
then performs resolution on subgoal~$i$.


847 

310

848 
\item[\ttindex{eres_inst_tac}]


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

105

850 
and destructresolution, respectively.


851 
\end{description}


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


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

307

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

105

855 
expressions giving their instantiations. The expressions are typechecked


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


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


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


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


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


861 


862 
\subsection{A simple proof by induction}

310

863 
\index{examples!of induction}

105

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


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


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

284

867 
\begin{ttbox}

105

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


869 
{\out Level 0}

459

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


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

105

872 
\ttbreak


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


874 
{\out Level 1}

459

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


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


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

284

878 
\end{ttbox}

105

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


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


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

310

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


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

284

884 
\begin{ttbox}

105

885 
by (resolve_tac [notI] 1);


886 
{\out Level 2}

459

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

105

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

459

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

105

890 
\ttbreak


891 
by (eresolve_tac [Suc_neq_0] 1);


892 
{\out Level 3}

459

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


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

284

895 
\end{ttbox}

105

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

284

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


898 
$Suc(Suc(x)) = Suc(x)$:


899 
\begin{ttbox}

105

900 
by (resolve_tac [notI] 1);


901 
{\out Level 4}

459

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


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

105

904 
\ttbreak


905 
by (eresolve_tac [notE] 1);


906 
{\out Level 5}

459

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

105

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


909 
\ttbreak


910 
by (eresolve_tac [Suc_inject] 1);


911 
{\out Level 6}

459

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

105

913 
{\out No subgoals!}

284

914 
\end{ttbox}

105

915 


916 


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


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


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


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


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


922 
complex formulae, our luck fails.

284

923 
\begin{ttbox}

105

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


925 
{\out Level 0}


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


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


928 
\ttbreak


929 
by (resolve_tac [induct] 1);


930 
{\out Level 1}


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


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


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

284

934 
\end{ttbox}


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


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


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


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


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


940 
the tactic.


941 
\begin{ttbox}

105

942 
back();


943 
{\out Level 1}


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


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


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

284

947 
\end{ttbox}


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


949 
call \ttindex{back} again.


950 
\begin{ttbox}

105

951 
back();


952 
{\out Level 1}


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


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

284

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


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


957 
\end{ttbox}

105

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

284

959 
\begin{ttbox}

105

960 
back();


961 
{\out Level 1}


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


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


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

284

965 
\end{ttbox}

105

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


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

310

968 
here.


969 


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


971 
number is exponential in the size of the formula.

105

972 


973 
\subsection{Proving that addition is associative}

331

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

310

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


976 
simplification tactics, which are described in


977 
\iflabelundefined{simpchap}%


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

284

979 

310

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


981 


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


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


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


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

331

986 
insert the equations proved in the previous section, namely

310

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

284

988 
\begin{ttbox}

459

989 
val add_ss = FOL_ss addsimps [add_0, add_Suc];

284

990 
\end{ttbox}

105

991 
We state the goal for associativity of addition, and


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

284

993 
\begin{ttbox}

105

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


995 
{\out Level 0}


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


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


998 
\ttbreak


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


1000 
{\out Level 1}


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


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

284

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


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


1005 
\end{ttbox}

105

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


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

331

1008 
set, applying the rewrite rules for addition:

284

1009 
\begin{ttbox}

105

1010 
by (simp_tac add_ss 1);


1011 
{\out Level 2}


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

284

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


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


1015 
\end{ttbox}

331

1016 
The inductive step requires rewriting by the equations for addition

105

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


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


1019 
useful assumptions:

284

1020 
\begin{ttbox}

105

1021 
by (asm_simp_tac add_ss 1);


1022 
{\out Level 3}


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


1024 
{\out No subgoals!}

284

1025 
\end{ttbox}

310

1026 
\index{instantiation)}

105

1027 


1028 

284

1029 
\section{A Prolog interpreter}

105

1030 
\index{Prolog interpreterbold}

284

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

105

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

331

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

105

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


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


1036 
provided~$\tau$ is:


1037 
\begin{eqnarray*}


1038 
list & :: & (term)term


1039 
\end{eqnarray*}


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


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

284

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

105

1043 
predicates.)


1044 
\begin{eqnarray*}


1045 
Nil & :: & \alpha list \\


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


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


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


1049 
\end{eqnarray*}

284

1050 
The predicate $app$ should satisfy the Prologstyle rules

105

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


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


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


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


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


1056 
rev(x:xs, zs)}


1057 
\]


1058 


1059 
\index{examples!of theories}

310

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

105

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

310

1062 
rules of~{\tt FOL}.

105

1063 
\begin{ttbox}


1064 
Prolog = FOL +

296

1065 
types 'a list

105

1066 
arities list :: (term)term


1067 
consts Nil :: "'a list"


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


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


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


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


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


1073 
revNil "rev(Nil,Nil)"


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


1075 
end


1076 
\end{ttbox}


1077 
\subsection{Simple executions}

284

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

105

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


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


1081 
\begin{ttbox}


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


1083 
{\out Level 0}


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


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


1086 
\ttbreak


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


1088 
{\out Level 1}


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


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


1091 
\ttbreak


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


1093 
{\out Level 2}


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


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


1096 
\end{ttbox}


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


1098 
\begin{ttbox}


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


1100 
{\out Level 3}


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


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


1103 
\ttbreak


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


1105 
{\out Level 4}


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


1107 
{\out No subgoals!}


1108 
\end{ttbox}


1109 

284

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

105

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


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


1113 
\begin{ttbox}


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


1115 
{\out Level 0}


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


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


1118 
\ttbreak


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


1120 
{\out Level 1}


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


1122 
{\out No subgoals!}


1123 
\end{ttbox}


1124 


1125 

310

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

296

1127 
Prolog backtracking can answer questions that have multiple solutions.


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


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


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

105

1131 
\begin{ttbox}


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


1133 
{\out Level 0}


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


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


1136 
\ttbreak


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


1138 
{\out Level 1}


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


1140 
{\out No subgoals!}


1141 
\end{ttbox}

284

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


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

105

1144 
\begin{ttbox}


1145 
back();


1146 
{\out Level 1}


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


1148 
{\out No subgoals!}


1149 
\end{ttbox}


1150 
The other solutions are generated similarly.


1151 
\begin{ttbox}


1152 
back();


1153 
{\out Level 1}


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


1155 
{\out No subgoals!}


1156 
\ttbreak


1157 
back();


1158 
{\out Level 1}


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


1160 
{\out No subgoals!}


1161 
\ttbreak


1162 
back();


1163 
{\out Level 1}


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


1165 
{\out No subgoals!}


1166 
\end{ttbox}


1167 


1168 


1169 
\subsection{Depthfirst search}


1170 
\index{search!depthfirst}


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


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


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


1174 
terminates in a few seconds.


1175 
\begin{ttbox}


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


1177 
{\out Level 0}


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

284

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


1180 
{\out ?w)}


1181 
\ttbreak

105

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


1183 
\ttbreak


1184 
by (REPEAT (resolve_tac rules 1));


1185 
{\out Level 1}


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


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


1188 
{\out No subgoals!}


1189 
\end{ttbox}


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


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


1192 
\begin{ttbox}


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


1194 
{\out Level 0}


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


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


1197 
\ttbreak


1198 
by (REPEAT (resolve_tac rules 1));


1199 
{\out Level 1}


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


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


1202 
\end{ttbox}


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

331

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

105

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


1206 
\begin{ttbox}


1207 
back();


1208 
{\out Level 1}


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


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


1211 
\end{ttbox}


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


1213 
\begin{ttbox}


1214 
back();


1215 
{\out Level 1}


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


1217 
{\out No subgoals!}


1218 
\end{ttbox}

310

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


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


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


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

105

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

310

1224 
subgoals.

105

1225 
\begin{ttbox}


1226 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)


1227 
(resolve_tac rules 1);


1228 
\end{ttbox}

284

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

296

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


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

105

1232 
\begin{ttbox}


1233 
choplev 0;


1234 
{\out Level 0}


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


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


1237 
\ttbreak


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


1239 
{\out Level 1}


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


1241 
{\out No subgoals!}


1242 
\end{ttbox}


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


1244 
\begin{ttbox}


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


1246 
{\out Level 0}


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


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


1249 
\ttbreak


1250 
by prolog_tac;


1251 
{\out Level 1}


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


1253 
{\out No subgoals!}


1254 
\end{ttbox}

284

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

156

1256 
tactics can exploit logic programming techniques.


1257 
