%% $Id$

\part{Advanced methods}

Before continuing, it might be wise to try some of your own examples in

Isabelle, reinforcing your knowledge of the basic functions.

This paper is merely an introduction to Isabelle.  Two other documents

exist:

\begin{itemize}

  \item {\em The Isabelle Reference Manual\/} contains information about

most of the facilities of Isabelle, apart from particular object-logics.

  \item {\em Isabelle's Object-Logics\/} describes the various logics

distributed with Isabelle.  It also explains how to define new logics in

Isabelle.

\end{itemize}

Look through {\em Isabelle's Object-Logics\/} and try proving some simple

theorems.  You probably should begin with first-order logic ({\tt FOL}

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

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

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

examples are in the literature.  Higher-order logic~({\tt HOL}) is

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

identified with those of the meta-logic; this may cause difficulties for

beginners.

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

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

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

Even experienced users plan large proofs on paper.

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

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

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

Isabelle's simplifier and classical theorem prover are

difficult to learn, and can be ignored at first.

\section{Deriving rules in Isabelle}

\index{rules!derived}

A mathematical development goes through a progression of stages.  Each

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

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

following section will explain how to declare types, constants, axioms and

definitions.

\subsection{Deriving a rule using tactics} \label{deriving-example}

\index{examples!of deriving rules}

The subgoal module supports the derivation of rules.  The \ttindex{goal}

command, when supplied a goal of the form $\List{\theta@1; \ldots;

\theta@k} \Imp \phi$, creates $\phi\Imp\phi$ as the initial proof state and

returns a list consisting of the theorems 

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

also recorded internally, allowing \ttindex{result} to discharge them in the

original order.

Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle.

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

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

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

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

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

2-element list.  Otherwise, the pattern-match will fail; ML will

raise exception \ttindex{Match}.}

\begin{ttbox}

val [major,minor] = goal FOL.thy

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

{\out Level 0}

{\out R}

{\out  1. R}

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

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

\end{ttbox}

Look at the minor premise, recalling that meta-level assumptions are

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

$P$ and~$Q$:

\begin{ttbox}

by (resolve_tac [minor] 1);

{\out Level 1}

{\out R}

{\out  1. P}

{\out  2. Q}

\end{ttbox}

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

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

\begin{ttbox}

major RS conjunct1;

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

\ttbreak

by (resolve_tac [major RS conjunct1] 1);

{\out Level 2}

{\out R}

{\out  1. Q}

\end{ttbox}

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

\begin{ttbox}

major RS conjunct2;

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

by (resolve_tac [major RS conjunct2] 1);

{\out Level 3}

{\out R}

{\out No subgoals!}

\end{ttbox}

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

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

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

and makes the variables schematic.

\begin{ttbox}

topthm();

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

val conjE = result();

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

\end{ttbox}

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

\index{rules!derived}

\index{Isabelle!definitions in}

\index{definitions!reasoning about|bold}

Definitions are expressed as meta-level equalities.  Let us define negation

and the if-and-only-if connective:

\begin{eqnarray*}

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

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

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

\end{eqnarray*}

\index{rewriting!meta-level|bold}

\index{unfolding|bold}\index{folding|bold}

Isabelle permits {\bf meta-level rewriting} using definitions such as

these.  {\bf Unfolding} replaces every instance

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

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

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

{\bf Folding} a definition replaces occurrences of the right-hand side by

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

\begin{warn}

Isabelle does not distinguish sensible definitions, like $1\equiv Suc(0)$, from

equations like $1\equiv Suc(1)$.  However, meta-rewriting fails for

equations like ${f(\Var{x})\equiv g(\Var{x},\Var{y})}$: all variables on

the right-hand side must also be present on the left.

\index{rewriting!meta-level}

\end{warn}

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

abstract properties, and then forget their definitions.  This supports

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

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

change.  Indiscriminate unfolding makes a subgoal grow exponentially,

becoming unreadable.

Taking this point of view, Isabelle does not unfold definitions

automatically during proofs.  Rewriting must be explicit and selective.

Isabelle provides tactics and meta-rules for rewriting, and a version of

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

being derived.

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

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

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

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

This requires proving the following formulae:

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

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

\subsubsection{Deriving the introduction rule}

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

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

premises.  We bind this list, which contains the one element $P\Imp\bot$,

to the \ML\ identifier {\tt prems}.

\begin{ttbox}

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

{\out Level 0}

{\out ~P}

{\out  1. ~P}

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

\end{ttbox}

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

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

the main goal alone.

\begin{ttbox}

not_def;

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

by (rewrite_goals_tac [not_def]);

{\out Level 1}

{\out ~P}

{\out  1. P --> False}

\end{ttbox}

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

\begin{ttbox}

by (resolve_tac [impI] 1);

{\out Level 2}

{\out ~P}

{\out  1. P ==> False}

\ttbreak

by (resolve_tac prems 1);

{\out Level 3}

{\out ~P}

{\out  1. P ==> P}

\end{ttbox}

The rest of the proof is routine.

\begin{ttbox}

by (assume_tac 1);

{\out Level 4}

{\out ~P}

{\out No subgoals!}

val notI = result();

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

\end{ttbox}

\indexbold{*notI}

\medskip

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

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

unfolds definitions:

\begin{ttbox}

val prems = goalw FOL.thy [not_def]

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

{\out Level 0}

{\out ~P}

{\out  1. P --> False}

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

\end{ttbox}

The proof continues as above, but without calling \ttindex{rewrite_goals_tac}.

\subsubsection{Deriving the elimination rule}

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

(\S\ref{deriving-example}), with an additional step to unfold negation in

the major premise.  Although the {\tt goalw} command is best for this, let

us try~\ttindex{goal}.  As usual, we bind the premises to \ML\ identifiers.

We then apply \ttindex{FalseE}, which stands for~$(\bot E)$:

\begin{ttbox}

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

{\out Level 0}

{\out R}

{\out  1. R}

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

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

\ttbreak

by (resolve_tac [FalseE] 1);

{\out Level 1}

{\out R}

{\out  1. False}

\ttbreak

by (resolve_tac [mp] 1);

{\out Level 2}

{\out R}

{\out  1. ?P1 --> False}

{\out  2. ?P1}

\end{ttbox}

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

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

definitions, unfolds them in a theorem.  Rewriting does {\bf not}

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

\begin{ttbox}

rewrite_rule [not_def] major;

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

by (resolve_tac [it] 1);

{\out Level 3}

{\out R}

{\out  1. P}

\end{ttbox}

Now {\tt?P1} has changed to~{\tt P}; we need only use the minor premise:

\begin{ttbox}

by (resolve_tac [minor] 1);

{\out Level 4}

{\out R}

{\out No subgoals!}

val notE = result();

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

\end{ttbox}

\indexbold{*notE}

\medskip

Again, there is a simpler way of conducting this proof.  The

\ttindex{goalw} command unfolds definitions in the premises as well

as the conclusion:

\begin{ttbox}

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

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

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

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

\end{ttbox}

Observe the difference in {\tt major}; the premises are now {\bf unfolded}

and we need not call~\ttindex{rewrite_rule}.  Incidentally, the four calls

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

of~\ttindex{RS}\@:

\begin{ttbox}

minor RS (major RS mp RS FalseE);

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

by (resolve_tac [it] 1);

{\out Level 1}

{\out R}

{\out No subgoals!}

\end{ttbox}

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

has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}

do not return the rule's premises in the list of theorems.  Instead, the

premises become assumptions in subgoal~1:

\begin{ttbox}

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

{\out Level 0}

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

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

val it = [] : thm list

\end{ttbox}

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

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

\ttindex{assume_tac}: 

\begin{ttbox}

by (resolve_tac [FalseE] 1);

{\out Level 1}

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

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

\ttbreak

by (eresolve_tac [mp] 1);

{\out Level 2}

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

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

\ttbreak

by (assume_tac 1);

{\out Level 3}

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

{\out No subgoals!}

\end{ttbox}

Calling \ttindex{result} strips the meta-quantifiers, so the resulting

theorem is the same as before.

\begin{ttbox}

val notE = result();

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

\end{ttbox}

Do not use the {\tt!!}\ trick if the premises contain meta-level

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

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

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

\section{Defining theories}

\index{theories!defining|(}

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

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

an entire logic.  A theory definition has the form

\begin{ttbox}

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

classes      {\it class declarations}

default      {\it sort}

types        {\it type declarations}

arities      {\it arity declarations}

consts       {\it constant declarations}

rules        {\it rule declarations}

translations {\it translation declarations}

end

ML           {\it ML code}

\end{ttbox}

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

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

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

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

associated concrete syntax.  The translations section specifies rewrite

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

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

transformations.  The main declaration forms are discussed below; see {\em

  Isabelle's Object-Logics} for full details and examples.

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

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

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

The theory \ttindexbold{Pure} contains nothing but Isabelle's meta-logic.

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

determined as follows: the theory name, say {\tt ListFn}, is converted to

lower case and {\tt.thy} is appended, yielding the filename {\tt

  listfn.thy}.  Isabelle uses this convention to locate the file containing

a given theory; \ttindexbold{use_thy} automatically loads a theory's

parents before loading the theory itself.

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

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

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

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

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

declared in {\it ML code}.

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

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

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

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

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

Theories can be defined directly by issuing {\ML} declarations to Isabelle,

but the calling sequences are extremely cumbersome.

If theory~$T$ is later redeclared in order to delete an incorrect rule,

bindings to the old rule may persist.  Isabelle ensures that the old and

new versions of~$T$ are not involved in the same proof.  Attempting to

combine different versions of~$T$ yields the fatal error

\begin{ttbox} 

Attempt to merge different versions of theory: \(T\)

\end{ttbox}

\subsection{Declaring constants and rules}

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

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

declaration part} has the form

\begin{ttbox}

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

        \vdots

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

\end{ttbox}

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

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

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

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

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

\begin{ttbox}

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

\end{ttbox}

The {\bf rule declaration part} has the form

\begin{ttbox}

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

        \vdots

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

\end{ttbox}

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

$rule@n$ are expressions of type~$prop$.  {\bf Definitions} are rules of

the form $t\equiv u$.  Each rule {\em must\/} be enclosed in quotation marks.

\index{examples!of theories}

This theory extends first-order logic with two constants {\em nand} and

{\em xor}, and two rules defining them:

\begin{ttbox} 

Gate = FOL +

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

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

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

end

\end{ttbox}

\subsection{Declaring type constructors}

\indexbold{type constructors!declaring}\indexbold{arities!declaring}

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

type constructor has a fixed number of argument places.  For example,

$list$ is a 1-place type constructor and $nat$ is a 0-place type

constructor.

The {\bf type declaration part} has the form

\begin{ttbox}

types   \(id@1\) \(k@1\)

        \vdots

        \(id@n\) \(k@n\)

\end{ttbox}

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

natural numbers.  It declares each $id@i$ as a type constructor with $k@i$

argument places.

The {\bf arity declaration part} has the form

\begin{ttbox}

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

        \vdots

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

\end{ttbox}

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

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

types; they complement type declarations.

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

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

constants $tt$ and~$ff$:\footnote{In first-order logic, booleans are

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

\index{examples!of theories}

\begin{ttbox} 

Bool = FOL +

types   bool 0

arities bool    :: term

consts  tt,ff   :: "bool"

end

\end{ttbox}

In the general case, type constructors take arguments.  Each type

constructor has an {\bf arity} with respect to

classes~(\S\ref{polymorphic}).  A $k$-place type constructor may have

arities of the form $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts

and $c$ is a class.  Each sort specifies a type argument; it has the form

$\{c@1,\ldots,c@m\}$, where $c@1$, \dots,~$c@m$ are classes.  Mostly we

deal with singleton sorts, and may abbreviate them by dropping the braces.

The arity declaration $list{::}(term)term$ is short for

$list{::}(\{term\})term$.

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

appearing in several arity declarations.  For instance, the built-in type

constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order

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

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

it arity $list{::}(term)term$, and declares constants $Nil$ and $Cons$ with

polymorphic types:

\index{examples!of theories}

\begin{ttbox} 

List = FOL +

types   list 1

arities list    :: (term)term

consts  Nil     :: "'a list"

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

end

\end{ttbox}

Multiple type and arity declarations may be abbreviated to a single line:

\begin{ttbox}

types   \(id@1\), \ldots, \(id@n\) \(k\)

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

\end{ttbox}

\begin{warn}

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

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

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

\end{warn}

\subsection{Infixes and Mixfixes}

\indexbold{infix operators}\index{examples!of theories}

The constant declaration part of the theory

\begin{ttbox} 

Gate2 = FOL +

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

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

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

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

end

\end{ttbox}

declares two left-associating infix operators: $\nand$ of precedence~35 and

$\xor$ of precedence~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor

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

quotation marks in \verb|"~&"| and \verb|"#"|.

The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared

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

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

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

\indexbold{mixfix operators}

{\bf Mixfix} operators may have arbitrary context-free syntaxes.  For example

\begin{ttbox} 

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

\end{ttbox}

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

$if~P~then~Q~else~R$ instead of $If(P,Q,R)$.  Underscores denote argument

positions.  Pretty-printing information can be specified in order to

improve the layout of formulae with mixfix operations.  For details, see

{\em Isabelle's Object-Logics}.

Mixfix declarations can be annotated with precedences, just like

infixes.  The example above is just a shorthand for

\begin{ttbox} 

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

\end{ttbox}

The numeric components determine precedences.  The list of integers

defines, for each argument position, the minimal precedence an expression

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

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

acceptable because precedences are non-negative, and conditionals may

appear everywhere because 1000 is the highest precedence.  On the other

hand,

\begin{ttbox} 

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

\end{ttbox}

defines concrete syntax for a

conditional whose first argument cannot have the form $if~P~then~Q~else~R$

because it must have a precedence of at least~100.  Since expressions put in

parentheses have maximal precedence, we may of course write 

\begin{quote}

\it  if (if P then Q else R) then S else T

\end{quote}

Conditional expressions can also be written using the constant {\tt If}.

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

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

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

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

\index{examples!of theories}

\begin{ttbox}

Prod = FOL +

types   "*" 2                                 (infixl 20)

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

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

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

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

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

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

end

\end{ttbox}

\begin{warn}

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

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

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

\end{warn}

\subsection{Overloading}

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

The {\bf class declaration part} has the form

\begin{ttbox}

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

        \vdots

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

\end{ttbox}

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

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

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

subclass of $k$ existing classes:

\begin{ttbox}

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

\end{ttbox}

Type classes allow constants to be overloaded~(\S\ref{polymorphic}).  As an

example, we define the class $arith$ of ``arithmetic'' types with the

constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 :: \alpha$, for

$\alpha{::}arith$.  We introduce $arith$ as a subclass of $term$ and add

the three polymorphic constants of this class.

\index{examples!of theories}

\begin{ttbox}

Arith = FOL +

classes arith < term

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

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

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

end

\end{ttbox}

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

names without specifying properties.  On the other hand, classes

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

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

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

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

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

\index{examples!of theories}

\begin{ttbox}

BoolNat = Arith +

types   bool,nat    0

arities bool,nat    :: arith

consts  Suc         :: "nat=>nat"

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

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

        nat1        "1 = Suc(0)"

        or0l        "0 + x = x::bool"

        or0r        "x + 0 = x::bool"

        or1l        "1 + x = 1::bool"

        or1r        "x + 1 = 1::bool"

end

\end{ttbox}

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

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

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

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

collapse $nat$:

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

The class $arith$ as defined above is more specific than necessary.  Many

types come with a binary operation and identity~(0).  On lists,

$+$ could be concatenation and 0 the empty list --- but what is 1?  Hence it

may be better to define $+$ and 0 on $arith$ and introduce a separate

class, say $k$, containing~1.  Should $k$ be a subclass of $term$ or of

$arith$?  This depends on the structure of your theories; the design of an

appropriate class hierarchy may require some experimentation.

We will now work through a small example of formalized mathematics

demonstrating many of the theory extension features.

\subsection{Extending first-order logic with the natural numbers}

\index{examples!of theories}

The early part of this paper defines a first-order logic, including a

type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.  Let us

introduce the Peano axioms for mathematical induction and the freeness of

$0$ and~$Suc$:

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

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

\]

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

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

\]

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

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

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

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

formalize mathematical induction as

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

\noindent

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

and~$\neg$, we take advantage of the meta-logic;\footnote

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

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

better with Isabelle's simplifier.} 

$(Suc\_neq\_0)$ is

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

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

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

\noindent

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

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

and obeys the equations

\begin{eqnarray*}

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

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

\end{eqnarray*}

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

should satisfy

\begin{eqnarray*}

  0+n      & = & n \\

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

\end{eqnarray*}

This appears to pose difficulties: first-order logic has no functions.

Following the previous examples, we take advantage of the meta-logic, which

does have functions.  We also generalise primitive recursion to be

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

function:

\begin{eqnarray*}

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

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

\end{eqnarray*}

\subsection{Declaring the theory to Isabelle}

\index{examples!of theories}

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

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

the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:

\begin{ttbox}

Nat = FOL +

types   nat 0

arities nat         :: term

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

        Suc         :: "nat=>nat"

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

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

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

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

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

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

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

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

end

\end{ttbox}

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

Opening the \ML\ structure {\tt Nat} permits reference to the axioms by \ML\

identifiers; we may write {\tt induct} instead of {\tt Nat.induct}.

\begin{ttbox}

open Nat;

\end{ttbox}

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

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

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

\begin{ttbox} 

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

{\out Level 0}

{\out 0 + n = n}

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

\ttbreak

by (resolve_tac [rec_0] 1);

{\out Level 1}

{\out 0 + n = n}

{\out No subgoals!}

val add_0 = result();

\end{ttbox} 

And here is the successor case:

\begin{ttbox} 

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

{\out Level 0}

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

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

\ttbreak

by (resolve_tac [rec_Suc] 1);

{\out Level 1}

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

{\out No subgoals!}

val add_Suc = result();

\end{ttbox} 

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

\index{theories!defining|)}

\section{Refinement with explicit instantiation}

\index{refinement!with instantiation|bold}

\index{instantiation!explicit|bold}

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

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

which is highly ambiguous in higher-order unification.  It matches every

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

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

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

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

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

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

schematic variables.  

\begin{description}

\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]

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

then performs resolution on subgoal~$i$.

\item[\ttindexbold{eres_inst_tac}] 

and \ttindexbold{dres_inst_tac} are similar, but perform elim-resolution

and destruct-resolution, respectively.

\end{description}

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

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

with {\bf no} leading question marks!! --- and $e@1$, \ldots, $e@n$ are

expressions giving their instantiations.  The expressions are type-checked

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

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

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

required: {\tt res_inst_tac} instantiates type variables automatically

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

\subsection{A simple proof by induction}

\index{proof!by induction}\index{examples!of induction}

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

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

instantiation for~$\Var{P}$.

\begin{ttbox} 

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

{\out Level 0}

{\out ~Suc(k) = k}

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

\ttbreak

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

{\out Level 1}

{\out ~Suc(k) = k}

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

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

\end{ttbox} 

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

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

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

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

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

\begin{ttbox} 

by (resolve_tac [notI] 1);

{\out Level 2}

{\out ~Suc(k) = k}

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

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

\ttbreak

by (eresolve_tac [Suc_neq_0] 1);

{\out Level 3}

{\out ~Suc(k) = k}

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

\end{ttbox} 

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

Using the negation rule, we assume $Suc(Suc(x)) = Suc(x)$ and prove $Suc(x)=x$:

\begin{ttbox} 

by (resolve_tac [notI] 1);

{\out Level 4}

{\out ~Suc(k) = k}

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

\ttbreak

by (eresolve_tac [notE] 1);

{\out Level 5}

{\out ~Suc(k) = k}

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

\ttbreak

by (eresolve_tac [Suc_inject] 1);

{\out Level 6}

{\out ~Suc(k) = k}

{\out No subgoals!}

\end{ttbox} 

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

\index{examples!of induction}\index{unification!higher-order}

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

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

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

complex formulae, our luck fails.  

\begin{ttbox} 

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

{\out Level 0}

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

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

\ttbreak

by (resolve_tac [induct] 1);

{\out Level 1}

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

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

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

\end{ttbox} 

This proof requires induction on~$k$.  But the 0 in subgoal~1 indicates

that induction has been applied to the term~$k+(m+n)$.  The

\ttindex{back} command causes backtracking to an alternative

outcome of the tactic.  

\begin{ttbox} 

back();

{\out Level 1}

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

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

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

\end{ttbox} 

Now induction has been applied to~$m+n$.  Let us call \ttindex{back}

again.

\begin{ttbox} 

back();

{\out Level 1}

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

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

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

\end{ttbox} 

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

\begin{ttbox} 

back();

{\out Level 1}

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

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

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

\end{ttbox} 

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

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

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

The number is exponential in the size of the formula.

\subsection{Proving that addition is associative}

\index{associativity of addition}

\index{examples!of rewriting}

Let us do the proof properly, using~\ttindex{res_inst_tac}.  At the same

time, we shall have a glimpse at Isabelle's rewriting tactics, which are

described in the {\em Reference Manual}.

\index{rewriting!object-level} 

Isabelle's rewriting tactics repeatedly applies equations to a subgoal,

simplifying or proving it.  For efficiency, the rewriting rules must be

packaged into a \bfindex{simplification set}.  Let us include the equations

for~{\tt add} proved in the previous section, namely $0+n=n$ and ${\tt

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

\begin{ttbox} 

val add_ss = FOL_ss addrews [add_0, add_Suc];

\end{ttbox} 

We state the goal for associativity of addition, and

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

\begin{ttbox} 

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

{\out Level 0}

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

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

\ttbreak

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

{\out Level 1}

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

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

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

\end{ttbox} 

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

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

set, applying the rewrite rules for~{\tt +}:

\begin{ttbox} 

by (simp_tac add_ss 1);

{\out Level 2}

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

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

\end{ttbox} 

The inductive step requires rewriting by the equations for~{\tt add}

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

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

useful assumptions:

\begin{ttbox} 

by (asm_simp_tac add_ss 1);

{\out Level 3}

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

{\out No subgoals!}

\end{ttbox} 

\section{A {\sc Prolog} interpreter}

\index{Prolog interpreter|bold}

To demonstrate the power of tacticals, let us construct a {\sc Prolog}

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

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

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

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

provided~$\tau$ is:

\begin{eqnarray*}

  list  & :: & (term)term

\end{eqnarray*}

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

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

predicate~$rev$.  (In {\sc Prolog}, functions on lists are expressed as

predicates.)

\begin{eqnarray*}

    Nil         & :: & \alpha list \\

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

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

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