%% $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.

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

simple theorems.  You probably should begin with first-order logic

(\texttt{FOL} or~\texttt{LK}).  Try working some of the examples provided,

and others from the literature.  Set theory~(\texttt{ZF}) and

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

mathematical reasoning and, again, many examples are in the

literature.  Higher-order logic~(\texttt{HOL}) is Isabelle's most

elaborate logic.  Its types and functions are identified with those of

the meta-logic.

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.

\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, rules and

definitions.

\subsection{Deriving a rule using tactics and meta-level assumptions} 

\label{deriving-example}

\index{examples!of deriving rules}\index{assumptions!of main goal}

The subgoal module supports the derivation of rules, as discussed in

\S\ref{deriving}.  When the \ttindex{Goal} command is supplied a formula of

the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two

possibilities:

\begin{itemize}

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

  formulae{} (they do not involve the meta-connectives $\Forall$ or

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

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

\item If one or more premises involves the meta-connectives $\Forall$ or

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

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

  These meta-assumptions are also recorded internally, allowing

  \texttt{result} (which is called by \texttt{qed}) to discharge them in the

  original order.

\end{itemize}

Rules that discharge assumptions or introduce eigenvariables have complex

premises, and the second case applies.

Let us derive $\conj$ elimination.  Until now, calling \texttt{Goal} has

returned an empty list, which we have ignored.  In this example, the list

contains the two premises of the rule, since one of them involves the $\Imp$

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

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

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

  list.  Otherwise, the pattern-match will fail; ML will raise exception

  \xdx{Match}.}

\begin{ttbox}

val [major,minor] = Goal

    "[| 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 \texttt{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{qed} 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}

qed "conjE";

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

\end{ttbox}

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

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

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{meta-rewriting}%

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.

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 \texttt{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 meta-formulae:

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

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

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

To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.

Again, the rule's premises involve a meta-connective, and \texttt{Goal}

returns one-element list.  We bind this list to the \ML\ identifier \texttt{prems}.

\begin{ttbox}

val prems = Goal "(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 \tdx{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 \tdx{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.  Note the form of the final result.

\begin{ttbox}

by (assume_tac 1);

{\out Level 4}

{\out ~P}

{\out No subgoals!}

\ttbreak

qed "notI";

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

\end{ttbox}

\indexbold{*notI theorem}

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

command starts a backward proof, as does \texttt{Goal}, but it also

unfolds definitions.  Thus there is no need to call

\ttindex{rewrite_goals_tac}:

\begin{ttbox}

val prems = Goalw [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}

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

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

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

The \texttt{Goalw} command is best for this: it unfolds definitions not only

in the conclusion but the premises.

\begin{ttbox}

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

{\out Level 0}

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

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

\end{ttbox}

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

\begin{ttbox}

by (resolve_tac [FalseE] 1);

{\out Level 1}

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

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

\end{ttbox}

%

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

premises and Modus Ponens:

\begin{ttbox}

by (eresolve_tac [mp] 1);

{\out Level 2}

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

{\out  1. P ==> P}

\ttbreak

by (assume_tac 1);

{\out Level 3}

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

{\out No subgoals!}

\ttbreak

qed "notE";

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

\end{ttbox}

\medskip

\texttt{Goalw} unfolds definitions in the premises even when it has to return

them as a list.  Another way of unfolding definitions in a theorem is by

applying the function \ttindex{rewrite_rule}.

\index{definitions!and derived rules|)}

\section{Defining theories}\label{sec:defining-theories}

\index{theories!defining|(}

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

like specifying a type~$bool$ with constants~$true$ and~$false$ ---

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

\begin{ttbox}

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

classes      {\it class declarations}

default      {\it sort}

types        {\it type declarations and synonyms}

arities      {\it type arity declarations}

consts       {\it constant declarations}

syntax       {\it syntactic constant declarations}

translations {\it ast translation rules}

defs         {\it meta-logical definitions}

rules        {\it rule 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 introduce new classes, types, arities

(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, handling notations and

abbreviations.  \index{*ML section} The \texttt{ML} section may contain

code to perform arbitrary syntactic transformations.  The main

declaration forms are discussed below.  There are some more sections

not presented here, the full syntax can be found in

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

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

object-logics may add further theory sections, for example

\texttt{typedef}, \texttt{datatype} in HOL.

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

any order, except that the {\ML} section must be last (after the {\tt

  end} keyword).  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

\thydx{Pure} contains nothing but Isabelle's meta-logic.  The variant

\thydx{CPure} offers the more usual higher-order function application

syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.

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

the theory's with {\tt.thy} appended.  Calling

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

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

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

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

component \texttt{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, \texttt{use_thy} will finally read the file

{\it T}{\tt.ML} (if it exists).  This file typically contains proofs

that refer to the components of~$T$.  The structure is automatically

opened, so its components may be referred to by unqualified names,

e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}.

\ttindexbold{use_thy} automatically loads a theory's parents before

loading the theory itself.  When a theory file is modified, many

theories may have to be reloaded.  Isabelle records the modification

times and dependencies of theory files.  See

\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%

                 {\S\ref{sec:reloading-theories}}

for more details.

\subsection{Declaring constants, definitions and rules}

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

Most theories simply declare constants, definitions and 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.  The types must be enclosed in quotation marks if they contain

user-declared infix type constructors like \texttt{*}.  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$.  Each rule {\em must\/} be

enclosed in quotation marks.

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

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

rules of the form $s \equiv t$, and should serve only as

abbreviations.  The simplest form of a definition is $f \equiv t$,

where $f$ is a constant.  Also allowed are $\eta$-equivalent forms of

this, where the arguments of~$f$ appear applied on the left-hand side

of the equation instead of abstracted on the right-hand side.

Isabelle checks for common errors in definitions, such as extra

variables on the right-hand side, but currently does not a complete

test of well-formedness.  Thus determined users can write

non-conservative `definitions' by using mutual recursion, for example;

the consequences of such actions are their responsibility.

\index{examples!of theories} This example theory extends first-order

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

  xor}:

\begin{ttbox}

Gate = FOL +

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

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

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

end

\end{ttbox}

Declaring and defining constants can be combined:

\begin{ttbox}

Gate = FOL +

constdefs  nand :: [o,o] => o

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

           xor  :: [o,o] => o

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

end

\end{ttbox}

\texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}

automatically, which is why it is restricted to alphanumeric identifiers.  In

general it has the form

\begin{ttbox}

constdefs  \(id@1\) :: \(\tau@1\)

           "\(id@1 \equiv \dots\)"

           \vdots

           \(id@n\) :: \(\tau@n\)

           "\(id@n \equiv \dots\)"

\end{ttbox}

\begin{warn}

A common mistake when writing definitions is to introduce extra free variables

on the right-hand side as in the following fictitious definition:

\begin{ttbox}

defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"

\end{ttbox}

Isabelle rejects this ``definition'' because of the extra \texttt{m} on the

right-hand side, which would introduce an inconsistency.  What you should have

written is

\begin{ttbox}

defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"

\end{ttbox}

\end{warn}

\subsection{Declaring type constructors}

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

%

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

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

with an \ML-like syntax.  If $list$ takes one type argument, $tree$ takes

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

can be declared by

\begin{ttbox}

types 'a list

      ('a,'b) tree

      nat

\end{ttbox}

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

\begin{ttbox}

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

        \vdots

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

\end{ttbox}

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

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

$id@i$ as a type constructor with the specified number of 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 do not declare the types themselves.

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$.  (In first-order logic, booleans are

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

\index{examples!of theories}

\begin{ttbox}

Bool = FOL +

types   bool

arities bool    :: term

consts  tt,ff   :: bool

end

\end{ttbox}

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

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

\S\ref{polymorphic}.

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

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

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

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

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

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

polymorphic types:%

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

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

\iflabelundefined{sec:ref-defining-theories}{}%

{(\S\ref{sec:ref-defining-theories})} for more information.}

\index{examples!of theories}

\begin{ttbox}

List = FOL +

types   'a list

arities list    :: (term)term

consts  Nil     :: 'a list

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

end

\end{ttbox}

Multiple arity declarations may be abbreviated to a single line:

\begin{ttbox}

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{Type synonyms}\indexbold{type synonyms}

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

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

and are fairly self explanatory:

\begin{ttbox}

types gate       = [o,o] => o

      'a pred    = 'a => o

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

\end{ttbox}

Type declarations and synonyms can be mixed arbitrarily:

\begin{ttbox}

types nat

      'a stream = nat => 'a

      signal    = nat stream

      'a list

\end{ttbox}

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

Hence synonyms may not be recursive!  Internally all synonyms are

fully expanded.  As a consequence Isabelle output never contains

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

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

\begin{ttbox}

consts and,or :: gate

       negate :: signal => signal

\end{ttbox}

\subsection{Infix and mixfix operators}

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

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

following theory:

\begin{ttbox}

Gate2 = FOL +

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

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

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

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

end

\end{ttbox}

The constant declaration part declares two left-associating infix operators

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

$\xor$ of priority~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.

\medskip Infix syntax and constant names may be also specified

independently.  For example, consider this version of $\nand$:

\begin{ttbox}

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

\end{ttbox}

\bigskip\index{mixfix declarations}

{\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us

add a line to the constant declaration part:

\begin{ttbox}

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

\end{ttbox}

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

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

denote argument positions.  

The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt

  else} construct to be printed split across several lines, even if it

is too long to fit on one line.  Pretty-printing information can be

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

\iflabelundefined{Defining-Logics}%

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

    {Chap.\ts\ref{Defining-Logics}}.

Mixfix declarations can be annotated with priorities, 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 priorities.  The list of integers

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

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

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

acceptable because priorities are non-negative, and conditionals may

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

hand, the declaration

\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 \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority

of at least~100.  We may of course write

\begin{quote}\tt

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

\end{quote}

because expressions in parentheses have maximal priority.  

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.  We also see a rule declaration part.

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

\begin{ttbox}

Prod = FOL +

types   ('a,'b) "*"                           (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~\texttt{*} and not \texttt{op~*}, as

  it would be in the case of an infix constant.  Only infix type

  constructors can have symbolic names like~\texttt{*}.  General mixfix

  syntax for types may be introduced via appropriate \texttt{syntax}

  declarations.

\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.  As suggested in

\S\ref{polymorphic}, let us 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}\index{constants!overloaded}

\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

arities bool, nat   :: arith

consts  Suc         :: nat=>nat

\ttbreak

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$ to a trivial type:

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

\section{Theory example: the natural numbers}

We shall 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}

Section\ts\ref{sec:logical-syntax} has formalized 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$:\index{axioms!Peano}

\[ \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*}

Primitive recursion appears to pose difficulties: first-order logic has no

function-valued expressions.  We again 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 \thydx{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 associated constants.  Note that

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

identifier, and could not otherwise be written in terms:

\begin{ttbox}\index{mixfix declarations}

Nat = FOL +

types   nat

arities nat         :: term

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

        Suc         :: nat=>nat

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

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

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

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

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

        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 \texttt{add_def}, recall that \verb|%| stands for~$\lambda$.

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

contains the theory and axioms.

\subsection{Proving some recursion equations}

Theory \texttt{FOL/ex/Nat} 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 [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!}

qed "add_0";

\end{ttbox}

And here is the successor case:

\begin{ttbox}

Goalw [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!}

qed "add_Suc";

\end{ttbox}

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

\index{theories!defining|)}

\section{Refinement with explicit instantiation}

\index{resolution!with instantiation}

\index{instantiation|(}

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 \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by

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

schematic variables.  

\begin{description}

\item[\ttindex{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[\ttindex{eres_inst_tac}] 

and \ttindex{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 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: \texttt{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{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 "~ (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~\tdx{notI}, \tdx{notE} and the

other rules of theory \texttt{Nat}.  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}.

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

$Suc(Suc(x)) = Suc(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 \texttt{resolve_tac}}

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

If you try the example above, you may observe that \texttt{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 "(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$.  The occurrence of~0 in subgoal~1

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

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

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

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$.  This is equally useless.  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) ==>}

{\out          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}

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

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

simplification tactics, which are described in 

\iflabelundefined{simp-chap}%

    {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.

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

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

perhaps proving it.  For efficiency, the rewrite rules must be packaged into a

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

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

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

\begin{ttbox}

Addsimps [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 "(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) ==>}

{\out          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 current

simplification set, applying the rewrite rules for addition:

\begin{ttbox}