2 \part{Advanced Methods}
3 Before continuing, it might be wise to try some of your own examples in
4 Isabelle, reinforcing your knowledge of the basic functions.
6 Look through {\em Isabelle's Object-Logics\/} and try proving some
7 simple theorems. You probably should begin with first-order logic
8 (\texttt{FOL} or~\texttt{LK}). Try working some of the examples provided,
9 and others from the literature. Set theory~(\texttt{ZF}) and
10 Constructive Type Theory~(\texttt{CTT}) form a richer world for
11 mathematical reasoning and, again, many examples are in the
12 literature. Higher-order logic~(\texttt{HOL}) is Isabelle's most
13 elaborate logic. Its types and functions are identified with those of
16 Choose a logic that you already understand. Isabelle is a proof
17 tool, not a teaching tool; if you do not know how to do a particular proof
18 on paper, then you certainly will not be able to do it on the machine.
19 Even experienced users plan large proofs on paper.
21 We have covered only the bare essentials of Isabelle, but enough to perform
22 substantial proofs. By occasionally dipping into the {\em Reference
23 Manual}, you can learn additional tactics, subgoal commands and tacticals.
26 \section{Deriving rules in Isabelle}
28 A mathematical development goes through a progression of stages. Each
29 stage defines some concepts and derives rules about them. We shall see how
30 to derive rules, perhaps involving definitions, using Isabelle. The
31 following section will explain how to declare types, constants, rules and
35 \subsection{Deriving a rule using tactics and meta-level assumptions}
36 \label{deriving-example}
37 \index{examples!of deriving rules}\index{assumptions!of main goal}
39 The subgoal module supports the derivation of rules, as discussed in
40 \S\ref{deriving}. When the \ttindex{Goal} command is supplied a formula of
41 the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two
44 \item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple
45 formulae{} (they do not involve the meta-connectives $\Forall$ or
46 $\Imp$) then the command sets the goal to be
47 $\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list.
48 \item If one or more premises involves the meta-connectives $\Forall$ or
49 $\Imp$, then the command sets the goal to be $\phi$ and returns a list
50 consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
51 These meta-level assumptions are also recorded internally, allowing
52 \texttt{result} (which is called by \texttt{qed}) to discharge them in the
55 Rules that discharge assumptions or introduce eigenvariables have complex
56 premises, and the second case applies. In this section, many of the
57 theorems are subject to meta-level assumptions, so we make them visible by by setting the
58 \ttindex{show_hyps} flag:
61 {\out val it = true : bool}
64 Now, we are ready to derive $\conj$ elimination. Until now, calling \texttt{Goal} has
65 returned an empty list, which we have ignored. In this example, the list
66 contains the two premises of the rule, since one of them involves the $\Imp$
67 connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt
68 minor}:\footnote{Some ML compilers will print a message such as {\em binding
69 not exhaustive}. This warns that \texttt{Goal} must return a 2-element
70 list. Otherwise, the pattern-match will fail; ML will raise exception
73 val [major,minor] = Goal
74 "[| P&Q; [| P; Q |] ==> R |] ==> R";
78 {\out val major = "P & Q [P & Q]" : thm}
79 {\out val minor = "[| P; Q |] ==> R [[| P; Q |] ==> R]" : thm}
81 Look at the minor premise, recalling that meta-level assumptions are
82 shown in brackets. Using \texttt{minor}, we reduce $R$ to the subgoals
85 by (resolve_tac [minor] 1);
91 Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
92 assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
95 {\out val it = "P [P & Q]" : thm}
97 by (resolve_tac [major RS conjunct1] 1);
102 Similarly, we solve the subgoal involving~$Q$.
105 {\out val it = "Q [P & Q]" : thm}
106 by (resolve_tac [major RS conjunct2] 1);
111 Calling \ttindex{topthm} returns the current proof state as a theorem.
112 Note that it contains assumptions. Calling \ttindex{qed} discharges
113 the assumptions --- both occurrences of $P\conj Q$ are discharged as
114 one --- and makes the variables schematic.
117 {\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
119 {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
123 \subsection{Definitions and derived rules} \label{definitions}
124 \index{rules!derived}\index{definitions!and derived rules|(}
126 Definitions are expressed as meta-level equalities. Let us define negation
127 and the if-and-only-if connective:
129 \neg \Var{P} & \equiv & \Var{P}\imp\bot \\
130 \Var{P}\bimp \Var{Q} & \equiv &
131 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
133 \index{meta-rewriting}%
134 Isabelle permits {\bf meta-level rewriting} using definitions such as
135 these. {\bf Unfolding} replaces every instance
136 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For
137 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
138 \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \]
139 {\bf Folding} a definition replaces occurrences of the right-hand side by
140 the left. The occurrences need not be free in the entire formula.
142 When you define new concepts, you should derive rules asserting their
143 abstract properties, and then forget their definitions. This supports
144 modularity: if you later change the definitions without affecting their
145 abstract properties, then most of your proofs will carry through without
146 change. Indiscriminate unfolding makes a subgoal grow exponentially,
149 Taking this point of view, Isabelle does not unfold definitions
150 automatically during proofs. Rewriting must be explicit and selective.
151 Isabelle provides tactics and meta-rules for rewriting, and a version of
152 the \texttt{Goal} command that unfolds the conclusion and premises of the rule
155 For example, the intuitionistic definition of negation given above may seem
156 peculiar. Using Isabelle, we shall derive pleasanter negation rules:
157 \[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad
158 \infer[({\neg}E)]{Q}{\neg P & P} \]
159 This requires proving the following meta-formulae:
160 $$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$
161 $$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$
164 \subsection{Deriving the $\neg$ introduction rule}
165 To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
166 Again, the rule's premises involve a meta-connective, and \texttt{Goal}
167 returns one-element list. We bind this list to the \ML\ identifier \texttt{prems}.
169 val prems = Goal "(P ==> False) ==> ~P";
173 {\out val prems = ["P ==> False [P ==> False]"] : thm list}
175 Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
176 definition of negation, unfolds that definition in the subgoals. It leaves
180 {\out val it = "~?P == ?P --> False" : thm}
181 by (rewrite_goals_tac [not_def]);
184 {\out 1. P --> False}
186 Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
188 by (resolve_tac [impI] 1);
191 {\out 1. P ==> False}
193 by (resolve_tac prems 1);
198 The rest of the proof is routine. Note the form of the final result.
206 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
208 \indexbold{*notI theorem}
210 There is a simpler way of conducting this proof. The \ttindex{Goalw}
211 command starts a backward proof, as does \texttt{Goal}, but it also
212 unfolds definitions. Thus there is no need to call
213 \ttindex{rewrite_goals_tac}:
215 val prems = Goalw [not_def]
216 "(P ==> False) ==> ~P";
219 {\out 1. P --> False}
220 {\out val prems = ["P ==> False [P ==> False]"] : thm list}
224 \subsection{Deriving the $\neg$ elimination rule}
225 Let us derive the rule $(\neg E)$. The proof follows that of~\texttt{conjE}
226 above, with an additional step to unfold negation in the major premise.
227 The \texttt{Goalw} command is best for this: it unfolds definitions not only
228 in the conclusion but the premises.
230 Goalw [not_def] "[| ~P; P |] ==> R";
232 {\out [| ~ P; P |] ==> R}
233 {\out 1. [| P --> False; P |] ==> R}
235 As the first step, we apply \tdx{FalseE}:
237 by (resolve_tac [FalseE] 1);
239 {\out [| ~ P; P |] ==> R}
240 {\out 1. [| P --> False; P |] ==> False}
243 Everything follows from falsity. And we can prove falsity using the
244 premises and Modus Ponens:
246 by (eresolve_tac [mp] 1);
248 {\out [| ~ P; P |] ==> R}
253 {\out [| ~ P; P |] ==> R}
257 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
262 \texttt{Goalw} unfolds definitions in the premises even when it has to return
263 them as a list. Another way of unfolding definitions in a theorem is by
264 applying the function \ttindex{rewrite_rule}.
266 \index{definitions!and derived rules|)}
269 \section{Defining theories}\label{sec:defining-theories}
270 \index{theories!defining|(}
272 Isabelle makes no distinction between simple extensions of a logic ---
273 like specifying a type~$bool$ with constants~$true$ and~$false$ ---
274 and defining an entire logic. A theory definition has a form like
276 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
277 classes {\it class declarations}
279 types {\it type declarations and synonyms}
280 arities {\it type arity declarations}
281 consts {\it constant declarations}
282 syntax {\it syntactic constant declarations}
283 translations {\it ast translation rules}
284 defs {\it meta-logical definitions}
285 rules {\it rule declarations}
289 This declares the theory $T$ to extend the existing theories
290 $S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities
291 (of existing types), constants and rules; it can specify the default
292 sort for type variables. A constant declaration can specify an
293 associated concrete syntax. The translations section specifies
294 rewrite rules on abstract syntax trees, handling notations and
295 abbreviations. \index{*ML section} The \texttt{ML} section may contain
296 code to perform arbitrary syntactic transformations. The main
297 declaration forms are discussed below. There are some more sections
298 not presented here, the full syntax can be found in
299 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
300 Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that
301 object-logics may add further theory sections, for example
302 \texttt{typedef}, \texttt{datatype} in HOL.
304 All the declaration parts can be omitted or repeated and may appear in
305 any order, except that the {\ML} section must be last (after the {\tt
306 end} keyword). In the simplest case, $T$ is just the union of
307 $S@1$,~\ldots,~$S@n$. New theories always extend one or more other
308 theories, inheriting their types, constants, syntax, etc. The theory
309 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
310 \thydx{CPure} offers the more usual higher-order function application
311 syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
313 Each theory definition must reside in a separate file, whose name is
314 the theory's with {\tt.thy} appended. Calling
315 \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
316 T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
317 T}.thy.ML}, reads the latter file, and deletes it if no errors
318 occurred. This declares the {\ML} structure~$T$, which contains a
319 component \texttt{thy} denoting the new theory, a component for each
320 rule, and everything declared in {\it ML code}.
322 Errors may arise during the translation to {\ML} (say, a misspelled
323 keyword) or during creation of the new theory (say, a type error in a
324 rule). But if all goes well, \texttt{use_thy} will finally read the file
325 {\it T}{\tt.ML} (if it exists). This file typically contains proofs
326 that refer to the components of~$T$. The structure is automatically
327 opened, so its components may be referred to by unqualified names,
328 e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}.
330 \ttindexbold{use_thy} automatically loads a theory's parents before
331 loading the theory itself. When a theory file is modified, many
332 theories may have to be reloaded. Isabelle records the modification
333 times and dependencies of theory files. See
334 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
335 {\S\ref{sec:reloading-theories}}
339 \subsection{Declaring constants, definitions and rules}
340 \indexbold{constants!declaring}\index{rules!declaring}
342 Most theories simply declare constants, definitions and rules. The {\bf
343 constant declaration part} has the form
345 consts \(c@1\) :: \(\tau@1\)
347 \(c@n\) :: \(\tau@n\)
349 where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
350 types. The types must be enclosed in quotation marks if they contain
351 user-declared infix type constructors like \texttt{*}. Each
352 constant must be enclosed in quotation marks unless it is a valid
353 identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
354 the $n$ declarations may be abbreviated to a single line:
356 \(c@1\), \ldots, \(c@n\) :: \(\tau\)
358 The {\bf rule declaration part} has the form
360 rules \(id@1\) "\(rule@1\)"
362 \(id@n\) "\(rule@n\)"
364 where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
365 $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
366 enclosed in quotation marks. Rules are simply axioms; they are
367 called \emph{rules} because they are mainly used to specify the inference
368 rules when defining a new logic.
370 \indexbold{definitions} The {\bf definition part} is similar, but with
371 the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are
372 rules of the form $s \equiv t$, and should serve only as
373 abbreviations. The simplest form of a definition is $f \equiv t$,
374 where $f$ is a constant. Also allowed are $\eta$-equivalent forms of
375 this, where the arguments of~$f$ appear applied on the left-hand side
376 of the equation instead of abstracted on the right-hand side.
378 Isabelle checks for common errors in definitions, such as extra
379 variables on the right-hand side and cyclic dependencies, that could
380 least to inconsistency. It is still essential to take care:
381 theorems proved on the basis of incorrect definitions are useless,
382 your system can be consistent and yet still wrong.
384 \index{examples!of theories} This example theory extends first-order
385 logic by declaring and defining two constants, {\em nand} and {\em
389 consts nand,xor :: [o,o] => o
390 defs nand_def "nand(P,Q) == ~(P & Q)"
391 xor_def "xor(P,Q) == P & ~Q | ~P & Q"
395 Declaring and defining constants can be combined:
398 constdefs nand :: [o,o] => o
399 "nand(P,Q) == ~(P & Q)"
401 "xor(P,Q) == P & ~Q | ~P & Q"
404 \texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}
405 automatically, which is why it is restricted to alphanumeric identifiers. In
406 general it has the form
408 constdefs \(id@1\) :: \(\tau@1\)
409 "\(id@1 \equiv \dots\)"
411 \(id@n\) :: \(\tau@n\)
412 "\(id@n \equiv \dots\)"
417 A common mistake when writing definitions is to introduce extra free variables
418 on the right-hand side as in the following fictitious definition:
420 defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
422 Isabelle rejects this ``definition'' because of the extra \texttt{m} on the
423 right-hand side, which would introduce an inconsistency. What you should have
426 defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
430 \subsection{Declaring type constructors}
431 \indexbold{types!declaring}\indexbold{arities!declaring}
433 Types are composed of type variables and {\bf type constructors}. Each
434 type constructor takes a fixed number of arguments. They are declared
435 with an \ML-like syntax. If $list$ takes one type argument, $tree$ takes
436 two arguments and $nat$ takes no arguments, then these type constructors
444 The {\bf type declaration part} has the general form
446 types \(tids@1\) \(id@1\)
450 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
451 are type argument lists as shown in the example above. It declares each
452 $id@i$ as a type constructor with the specified number of argument places.
454 The {\bf arity declaration part} has the form
456 arities \(tycon@1\) :: \(arity@1\)
458 \(tycon@n\) :: \(arity@n\)
460 where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
461 $arity@n$ are arities. Arity declarations add arities to existing
462 types; they do not declare the types themselves.
463 In the simplest case, for an 0-place type constructor, an arity is simply
464 the type's class. Let us declare a type~$bool$ of class $term$, with
465 constants $tt$ and~$ff$. (In first-order logic, booleans are
466 distinct from formulae, which have type $o::logic$.)
467 \index{examples!of theories}
475 A $k$-place type constructor may have arities of the form
476 $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
477 Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
478 where $c@1$, \dots,~$c@m$ are classes. Mostly we deal with singleton
479 sorts, and may abbreviate them by dropping the braces. The arity
480 $(term)term$ is short for $(\{term\})term$. Recall the discussion in
483 A type constructor may be overloaded (subject to certain conditions) by
484 appearing in several arity declarations. For instance, the function type
485 constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
486 logic, it is declared also to have arity $(term,term)term$.
488 Theory \texttt{List} declares the 1-place type constructor $list$, gives
489 it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with
491 \footnote{In the \texttt{consts} part, type variable {\tt'a} has the default
492 sort, which is \texttt{term}. See the {\em Reference Manual\/}
493 \iflabelundefined{sec:ref-defining-theories}{}%
494 {(\S\ref{sec:ref-defining-theories})} for more information.}
495 \index{examples!of theories}
499 arities list :: (term)term
500 consts Nil :: 'a list
501 Cons :: ['a, 'a list] => 'a list
504 Multiple arity declarations may be abbreviated to a single line:
506 arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
510 %Arity declarations resemble constant declarations, but there are {\it no\/}
511 %quotation marks! Types and rules must be quoted because the theory
512 %translator passes them verbatim to the {\ML} output file.
515 \subsection{Type synonyms}\indexbold{type synonyms}
516 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
517 to those found in \ML. Such synonyms are defined in the type declaration part
518 and are fairly self explanatory:
520 types gate = [o,o] => o
522 ('a,'b)nuf = 'b => 'a
524 Type declarations and synonyms can be mixed arbitrarily:
527 'a stream = nat => 'a
531 A synonym is merely an abbreviation for some existing type expression.
532 Hence synonyms may not be recursive! Internally all synonyms are
533 fully expanded. As a consequence Isabelle output never contains
534 synonyms. Their main purpose is to improve the readability of theory
535 definitions. Synonyms can be used just like any other type:
537 consts and,or :: gate
538 negate :: signal => signal
541 \subsection{Infix and mixfix operators}
542 \index{infixes}\index{examples!of theories}
544 Infix or mixfix syntax may be attached to constants. Consider the
548 consts "~&" :: [o,o] => o (infixl 35)
549 "#" :: [o,o] => o (infixl 30)
550 defs nand_def "P ~& Q == ~(P & Q)"
551 xor_def "P # Q == P & ~Q | ~P & Q"
554 The constant declaration part declares two left-associating infix operators
555 with their priorities, or precedences; they are $\nand$ of priority~35 and
556 $\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
557 \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation
558 marks in \verb|"~&"| and \verb|"#"|.
560 The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
561 automatically, just as in \ML. Hence you may write propositions like
562 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
563 Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
565 \medskip Infix syntax and constant names may be also specified
566 independently. For example, consider this version of $\nand$:
568 consts nand :: [o,o] => o (infixl "~&" 35)
571 \bigskip\index{mixfix declarations}
572 {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
573 add a line to the constant declaration part:
575 If :: [o,o,o] => o ("if _ then _ else _")
577 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
578 if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}. Underscores
579 denote argument positions.
581 The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt
582 else} construct to be printed split across several lines, even if it
583 is too long to fit on one line. Pretty-printing information can be
584 added to specify the layout of mixfix operators. For details, see
585 \iflabelundefined{Defining-Logics}%
586 {the {\it Reference Manual}, chapter `Defining Logics'}%
587 {Chap.\ts\ref{Defining-Logics}}.
589 Mixfix declarations can be annotated with priorities, just like
590 infixes. The example above is just a shorthand for
592 If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000)
594 The numeric components determine priorities. The list of integers
595 defines, for each argument position, the minimal priority an expression
596 at that position must have. The final integer is the priority of the
597 construct itself. In the example above, any argument expression is
598 acceptable because priorities are non-negative, and conditionals may
599 appear everywhere because 1000 is the highest priority. On the other
600 hand, the declaration
602 If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99)
604 defines concrete syntax for a conditional whose first argument cannot have
605 the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority
606 of at least~100. We may of course write
608 if (if $P$ then $Q$ else $R$) then $S$ else $T$
610 because expressions in parentheses have maximal priority.
612 Binary type constructors, like products and sums, may also be declared as
613 infixes. The type declaration below introduces a type constructor~$*$ with
614 infix notation $\alpha*\beta$, together with the mixfix notation
615 ${<}\_,\_{>}$ for pairs. We also see a rule declaration part.
616 \index{examples!of theories}\index{mixfix declarations}
619 types ('a,'b) "*" (infixl 20)
620 arities "*" :: (term,term)term
621 consts fst :: "'a * 'b => 'a"
622 snd :: "'a * 'b => 'b"
623 Pair :: "['a,'b] => 'a * 'b" ("(1<_,/_>)")
624 rules fst "fst(<a,b>) = a"
630 The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as
631 it would be in the case of an infix constant. Only infix type
632 constructors can have symbolic names like~\texttt{*}. General mixfix
633 syntax for types may be introduced via appropriate \texttt{syntax}
638 \subsection{Overloading}
639 \index{overloading}\index{examples!of theories}
640 The {\bf class declaration part} has the form
642 classes \(id@1\) < \(c@1\)
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:
651 \(id\) < \(c@1\), \ldots, \(c@k\)
653 Type classes allow constants to be overloaded. As suggested in
654 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
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.
658 \index{examples!of theories}\index{constants!overloaded}
662 consts "0" :: 'a::arith ("0")
663 "1" :: 'a::arith ("1")
664 "+" :: ['a::arith,'a] => 'a (infixl 60)
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.
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 0-place type constructors $bool$ and $nat$:
675 \index{examples!of theories}
679 arities bool, nat :: arith
680 consts Suc :: nat=>nat
682 rules add0 "0 + n = n::nat"
683 addS "Suc(m)+n = Suc(m+n)"
685 or0l "0 + x = x::bool"
686 or0r "x + 0 = x::bool"
687 or1l "1 + x = 1::bool"
688 or1r "x + 1 = 1::bool"
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 = 1$ (axiom \texttt{or1l})
694 would have type $\alpha{::}arith$
695 and the axiom would hold for any type of class $arith$. This would
696 collapse $nat$ to a trivial type:
697 \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
700 \section{Theory example: the natural numbers}
702 We shall now work through a small example of formalized mathematics
703 demonstrating many of the theory extension features.
706 \subsection{Extending first-order logic with the natural numbers}
707 \index{examples!of theories}
709 Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
710 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
711 Let us introduce the Peano axioms for mathematical induction and the
712 freeness of $0$ and~$Suc$:\index{axioms!Peano}
713 \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
714 \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
716 \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
717 \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
719 Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
720 provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
721 Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
722 To avoid making induction require the presence of other connectives, we
723 formalize mathematical induction as
724 $$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
727 Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
728 and~$\neg$, we take advantage of the meta-logic;\footnote
729 {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
730 and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
731 better with Isabelle's simplifier.}
733 an elimination rule for $Suc(m)=0$:
734 $$ Suc(m)=Suc(n) \Imp m=n \eqno(Suc\_inject) $$
735 $$ Suc(m)=0 \Imp R \eqno(Suc\_neq\_0) $$
738 We shall also define a primitive recursion operator, $rec$. Traditionally,
739 primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
740 and obeys the equations
742 rec(0,a,f) & = & a \\
743 rec(Suc(m),a,f) & = & f(m, rec(m,a,f))
745 Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
749 Suc(m)+n & = & Suc(m+n)
751 Primitive recursion appears to pose difficulties: first-order logic has no
752 function-valued expressions. We again take advantage of the meta-logic,
753 which does have functions. We also generalise primitive recursion to be
754 polymorphic over any type of class~$term$, and declare the addition
757 rec & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
758 + & :: & [nat,nat]\To nat
762 \subsection{Declaring the theory to Isabelle}
763 \index{examples!of theories}
764 Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
765 which contains only classical logic with no natural numbers. We declare
766 the 0-place type constructor $nat$ and the associated constants. Note that
767 the constant~0 requires a mixfix annotation because~0 is not a legal
768 identifier, and could not otherwise be written in terms:
769 \begin{ttbox}\index{mixfix declarations}
773 consts "0" :: nat ("0")
775 rec :: [nat, 'a, [nat,'a]=>'a] => 'a
776 "+" :: [nat, nat] => nat (infixl 60)
777 rules Suc_inject "Suc(m)=Suc(n) ==> m=n"
778 Suc_neq_0 "Suc(m)=0 ==> R"
779 induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
780 rec_0 "rec(0,a,f) = a"
781 rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
782 add_def "m+n == rec(m, n, \%x y. Suc(y))"
785 In axiom \texttt{add_def}, recall that \verb|%| stands for~$\lambda$.
786 Loading this theory file creates the \ML\ structure \texttt{Nat}, which
787 contains the theory and axioms.
789 \subsection{Proving some recursion equations}
790 Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the
791 natural numbers. As a trivial example, let us derive recursion equations
792 for \verb$+$. Here is the zero case:
794 Goalw [add_def] "0+n = n";
797 {\out 1. rec(0,n,\%x y. Suc(y)) = n}
799 by (resolve_tac [rec_0] 1);
805 And here is the successor case:
807 Goalw [add_def] "Suc(m)+n = Suc(m+n)";
809 {\out Suc(m) + n = Suc(m + n)}
810 {\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
812 by (resolve_tac [rec_Suc] 1);
814 {\out Suc(m) + n = Suc(m + n)}
818 The induction rule raises some complications, which are discussed next.
819 \index{theories!defining|)}
822 \section{Refinement with explicit instantiation}
823 \index{resolution!with instantiation}
824 \index{instantiation|(}
826 In order to employ mathematical induction, we need to refine a subgoal by
827 the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$,
828 which is highly ambiguous in higher-order unification. It matches every
829 way that a formula can be regarded as depending on a subterm of type~$nat$.
830 To get round this problem, we could make the induction rule conclude
831 $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
832 refinement by~$(\forall E)$, which is equally hard!
834 The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by
835 a rule. But it also accepts explicit instantiations for the rule's
838 \item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
839 instantiates the rule {\it thm} with the instantiations {\it insts}, and
840 then performs resolution on subgoal~$i$.
842 \item[\ttindex{eres_inst_tac}]
843 and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
844 and destruct-resolution, respectively.
846 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
847 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
848 with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
849 expressions giving their instantiations. The expressions are type-checked
850 in the context of a particular subgoal: free variables receive the same
851 types as they have in the subgoal, and parameters may appear. Type
852 variable instantiations may appear in~{\it insts}, but they are seldom
853 required: \texttt{res_inst_tac} instantiates type variables automatically
854 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
856 \subsection{A simple proof by induction}
857 \index{examples!of induction}
858 Let us prove that no natural number~$k$ equals its own successor. To
859 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
860 instantiation for~$\Var{P}$.
862 Goal "~ (Suc(k) = k)";
865 {\out 1. Suc(k) ~= k}
867 by (res_inst_tac [("n","k")] induct 1);
870 {\out 1. Suc(0) ~= 0}
871 {\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
873 We should check that Isabelle has correctly applied induction. Subgoal~1
874 is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,
875 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
876 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
877 other rules of theory \texttt{Nat}. The base case holds by~\ttindex{Suc_neq_0}:
879 by (resolve_tac [notI] 1);
882 {\out 1. Suc(0) = 0 ==> False}
883 {\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
885 by (eresolve_tac [Suc_neq_0] 1);
888 {\out 1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
890 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
891 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
892 $Suc(Suc(x)) = Suc(x)$:
894 by (resolve_tac [notI] 1);
897 {\out 1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
899 by (eresolve_tac [notE] 1);
902 {\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
904 by (eresolve_tac [Suc_inject] 1);
911 \subsection{An example of ambiguity in \texttt{resolve_tac}}
912 \index{examples!of induction}\index{unification!higher-order}
913 If you try the example above, you may observe that \texttt{res_inst_tac} is
914 not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right
915 instantiation for~$(induct)$ to yield the desired next state. With more
916 complex formulae, our luck fails.
918 Goal "(k+m)+n = k+(m+n)";
920 {\out k + m + n = k + (m + n)}
921 {\out 1. k + m + n = k + (m + n)}
923 by (resolve_tac [induct] 1);
925 {\out k + m + n = k + (m + n)}
926 {\out 1. k + m + n = 0}
927 {\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
929 This proof requires induction on~$k$. The occurrence of~0 in subgoal~1
930 indicates that induction has been applied to the term~$k+(m+n)$; this
931 application is sound but will not lead to a proof here. Fortunately,
932 Isabelle can (lazily!) generate all the valid applications of induction.
933 The \ttindex{back} command causes backtracking to an alternative outcome of
938 {\out k + m + n = k + (m + n)}
939 {\out 1. k + m + n = k + 0}
940 {\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
942 Now induction has been applied to~$m+n$. This is equally useless. Let us
943 call \ttindex{back} again.
947 {\out k + m + n = k + (m + n)}
948 {\out 1. k + m + 0 = k + (m + 0)}
949 {\out 2. !!x. k + m + x = k + (m + x) ==>}
950 {\out k + m + Suc(x) = k + (m + Suc(x))}
952 Now induction has been applied to~$n$. What is the next alternative?
956 {\out k + m + n = k + (m + n)}
957 {\out 1. k + m + n = k + (m + 0)}
958 {\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
960 Inspecting subgoal~1 reveals that induction has been applied to just the
961 second occurrence of~$n$. This perfectly legitimate induction is useless
964 The main goal admits fourteen different applications of induction. The
965 number is exponential in the size of the formula.
967 \subsection{Proving that addition is associative}
968 Let us invoke the induction rule properly, using~{\tt
969 res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's
970 simplification tactics, which are described in
971 \iflabelundefined{simp-chap}%
972 {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
974 \index{simplification}\index{examples!of simplification}
976 Isabelle's simplification tactics repeatedly apply equations to a subgoal,
977 perhaps proving it. For efficiency, the rewrite rules must be packaged into a
978 {\bf simplification set},\index{simplification sets} or {\bf simpset}. We
979 augment the implicit simpset of FOL with the equations proved in the previous
980 section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
982 Addsimps [add_0, add_Suc];
984 We state the goal for associativity of addition, and
985 use \ttindex{res_inst_tac} to invoke induction on~$k$:
987 Goal "(k+m)+n = k+(m+n)";
989 {\out k + m + n = k + (m + n)}
990 {\out 1. k + m + n = k + (m + n)}
992 by (res_inst_tac [("n","k")] induct 1);
994 {\out k + m + n = k + (m + n)}
995 {\out 1. 0 + m + n = 0 + (m + n)}
996 {\out 2. !!x. x + m + n = x + (m + n) ==>}
997 {\out Suc(x) + m + n = Suc(x) + (m + n)}
999 The base case holds easily; both sides reduce to $m+n$. The
1000 tactic~\ttindex{Simp_tac} rewrites with respect to the current
1001 simplification set, applying the rewrite rules for addition:
1005 {\out k + m + n = k + (m + n)}
1006 {\out 1. !!x. x + m + n = x + (m + n) ==>}
1007 {\out Suc(x) + m + n = Suc(x) + (m + n)}
1009 The inductive step requires rewriting by the equations for addition
1010 and with the induction hypothesis, which is also an equation. The
1011 tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
1012 simplification set and any useful assumptions:
1014 by (Asm_simp_tac 1);
1016 {\out k + m + n = k + (m + n)}
1019 \index{instantiation|)}
1022 \section{A Prolog interpreter}
1023 \index{Prolog interpreter|bold}
1024 To demonstrate the power of tacticals, let us construct a Prolog
1025 interpreter and execute programs involving lists.\footnote{To run these
1026 examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program
1027 consists of a theory. We declare a type constructor for lists, with an
1028 arity declaration to say that $(\tau)list$ is of class~$term$
1031 list & :: & (term)term
1033 We declare four constants: the empty list~$Nil$; the infix list
1034 constructor~{:}; the list concatenation predicate~$app$; the list reverse
1035 predicate~$rev$. (In Prolog, functions on lists are expressed as
1038 Nil & :: & \alpha list \\
1039 {:} & :: & [\alpha,\alpha list] \To \alpha list \\
1040 app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
1041 rev & :: & [\alpha list,\alpha list] \To o
1043 The predicate $app$ should satisfy the Prolog-style rules
1044 \[ {app(Nil,ys,ys)} \qquad
1045 {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
1046 We define the naive version of $rev$, which calls~$app$:
1047 \[ {rev(Nil,Nil)} \qquad
1048 {rev(xs,ys)\quad app(ys, x:Nil, zs) \over
1052 \index{examples!of theories}
1053 Theory \thydx{Prolog} extends first-order logic in order to make use
1054 of the class~$term$ and the type~$o$. The interpreter does not use the
1055 rules of~\texttt{FOL}.
1059 arities list :: (term)term
1060 consts Nil :: 'a list
1061 ":" :: ['a, 'a list]=> 'a list (infixr 60)
1062 app :: ['a list, 'a list, 'a list] => o
1063 rev :: ['a list, 'a list] => o
1064 rules appNil "app(Nil,ys,ys)"
1065 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
1066 revNil "rev(Nil,Nil)"
1067 revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
1070 \subsection{Simple executions}
1071 Repeated application of the rules solves Prolog goals. Let us
1072 append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the
1073 answer builds up in~\texttt{?x}.
1075 Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
1077 {\out app(a : b : c : Nil, d : e : Nil, ?x)}
1078 {\out 1. app(a : b : c : Nil, d : e : Nil, ?x)}
1080 by (resolve_tac [appNil,appCons] 1);
1082 {\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
1083 {\out 1. app(b : c : Nil, d : e : Nil, ?zs1)}
1085 by (resolve_tac [appNil,appCons] 1);
1087 {\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
1088 {\out 1. app(c : Nil, d : e : Nil, ?zs2)}
1090 At this point, the first two elements of the result are~$a$ and~$b$.
1092 by (resolve_tac [appNil,appCons] 1);
1094 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
1095 {\out 1. app(Nil, d : e : Nil, ?zs3)}
1097 by (resolve_tac [appNil,appCons] 1);
1099 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
1103 Prolog can run functions backwards. Which list can be appended
1104 with $[c,d]$ to produce $[a,b,c,d]$?
1105 Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
1107 Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
1109 {\out app(?x, c : d : Nil, a : b : c : d : Nil)}
1110 {\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)}
1112 by (REPEAT (resolve_tac [appNil,appCons] 1));
1114 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
1119 \subsection{Backtracking}\index{backtracking!Prolog style}
1120 Prolog backtracking can answer questions that have multiple solutions.
1121 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This
1122 question has five solutions. Using \ttindex{REPEAT} to apply the rules, we
1123 quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
1125 Goal "app(?x, ?y, a:b:c:d:Nil)";
1127 {\out app(?x, ?y, a : b : c : d : Nil)}
1128 {\out 1. app(?x, ?y, a : b : c : d : Nil)}
1130 by (REPEAT (resolve_tac [appNil,appCons] 1));
1132 {\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
1135 Isabelle can lazily generate all the possibilities. The \ttindex{back}
1136 command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
1140 {\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
1143 The other solutions are generated similarly.
1147 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
1152 {\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
1157 {\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
1162 \subsection{Depth-first search}
1163 \index{search!depth-first}
1164 Now let us try $rev$, reversing a list.
1165 Bundle the rules together as the \ML{} identifier \texttt{rules}. Naive
1166 reverse requires 120 inferences for this 14-element list, but the tactic
1167 terminates in a few seconds.
1169 Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
1171 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
1172 {\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
1175 val rules = [appNil,appCons,revNil,revCons];
1177 by (REPEAT (resolve_tac rules 1));
1179 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
1180 {\out n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
1183 We may execute $rev$ backwards. This, too, should reverse a list. What
1184 is the reverse of $[a,b,c]$?
1186 Goal "rev(?x, a:b:c:Nil)";
1188 {\out rev(?x, a : b : c : Nil)}
1189 {\out 1. rev(?x, a : b : c : Nil)}
1191 by (REPEAT (resolve_tac rules 1));
1193 {\out rev(?x1 : Nil, a : b : c : Nil)}
1194 {\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
1196 The tactic has failed to find a solution! It reached a dead end at
1197 subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
1198 equals~$[a,b,c]$. Backtracking explores other outcomes.
1202 {\out rev(?x1 : a : Nil, a : b : c : Nil)}
1203 {\out 1. app(Nil, ?x1 : Nil, b : c : Nil)}
1205 This too is a dead end, but the next outcome is successful.
1209 {\out rev(c : b : a : Nil, a : b : c : Nil)}
1212 \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
1213 search tactical. \texttt{REPEAT} stops when it cannot continue, regardless of
1214 which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a
1215 satisfactory state, as specified by an \ML{} predicate. Below,
1216 \ttindex{has_fewer_prems} specifies that the proof state should have no
1219 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)
1220 (resolve_tac rules 1);
1222 Since Prolog uses depth-first search, this tactic is a (slow!)
1223 Prolog interpreter. We return to the start of the proof using
1224 \ttindex{choplev}, and apply \texttt{prolog_tac}:
1228 {\out rev(?x, a : b : c : Nil)}
1229 {\out 1. rev(?x, a : b : c : Nil)}
1233 {\out rev(c : b : a : Nil, a : b : c : Nil)}
1236 Let us try \texttt{prolog_tac} on one more example, containing four unknowns:
1238 Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
1240 {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
1241 {\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
1245 {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
1248 Although Isabelle is much slower than a Prolog system, Isabelle
1249 tactics can exploit logic programming techniques.