%% $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 ({\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.

 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}.  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 meta-assumptions

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

 in the original order.

 Let us derive $\conj$ elimination using Isabelle.

 Until now, calling {\tt 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 \xdx{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{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 {\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 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 {\tt goal} with the appropriate

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

 premises.  We bind this one-element list 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 \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

 val notI = result();

 {\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 {\tt goal}, but it also

 unfolds definitions.  Thus there is no need to call

 \ttindex{rewrite_goals_tac}:

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

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

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

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

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

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

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

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

 \end{ttbox}

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

 premises and Modus Ponens:

 \begin{ttbox}

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

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

 using 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 theorem}

 \medskip

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

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

 unfolds definitions in the premises:

 \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 unfolded without

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

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

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

 complex premise.

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

 \index{definitions!and derived rules|)}

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

 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.  

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

 \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 {\tt eresolve_tac} or

 {\tt 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}\label{sec: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 and synonyms}

 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.

 \index{*ML section}

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

 transformations.  The main declaration forms are discussed below.

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

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

 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 \thydx{Pure} contains nothing but Isabelle's meta-logic.

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

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

 on a file named {\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\/}"} reads a theory from the

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

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

 {\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$.

 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 and rules}

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

 Most theories simply declare constants 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.  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$.  Each rule {\em must\/} be

 enclosed in quotation marks.

 \indexbold{definitions}

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

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

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

 is your responsibility to ensure that your definitions are conservative.

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

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

 \index{examples!of theories}

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

 {\em xor}, and declares rules to define 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{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@1\) \(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 {\tt List} declares the 1-place type constructor $list$, gives

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

 polymorphic types:%

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

   sort, which is {\tt 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 theories.  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)

 rules   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.

 \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 {\tt If($P$,$Q$,$R$)}.  Underscores

 denote argument positions.  

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

 construct to be 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 {\tt 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.  

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

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

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

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

 \begin{ttbox}

 open Nat;

 \end{ttbox}

 \subsection{Proving some recursion equations}

 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{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 {\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[\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: {\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{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~\tdx{notI}, \tdx{notE} and the

 other rules of theory {\tt 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 {\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$.  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 take the standard simpset for first-order logic and

 insert the equations 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) ==>}

 {\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 given simplification

 set, applying the rewrite rules for addition:

 \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) ==>}

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

 \end{ttbox}

 The inductive step requires rewriting by the equations for addition

 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}

 \index{instantiation|)}

 \section{A Prolog interpreter}

 \index{Prolog interpreter|bold}

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

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

 examples, see the file {\tt FOL/ex/Prolog.ML}.} The 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 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 

 \end{eqnarray*}

 The predicate $app$ should satisfy the Prolog-style rules

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

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

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

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

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

     rev(x:xs, zs)} 

 \]

 \index{examples!of theories}

 Theory \thydx{Prolog} extends first-order logic in order to make use

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

 rules of~{\tt FOL}.

 \begin{ttbox}

 Prolog = FOL +

 types   'a list

 arities list    :: (term)term

 consts  Nil     :: "'a list"

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

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

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

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

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

         revNil  "rev(Nil,Nil)"

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

 end

 \end{ttbox}

 \subsection{Simple executions}

 Repeated application of the rules solves Prolog goals.  Let us

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

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

 \begin{ttbox}

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

 {\out Level 0}

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

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

 \ttbreak

 by (resolve_tac [appNil,appCons] 1);

 {\out Level 1}

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

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

 \ttbreak

 by (resolve_tac [appNil,appCons] 1);

 {\out Level 2}

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

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

 \end{ttbox}

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

 \begin{ttbox}

 by (resolve_tac [appNil,appCons] 1);

 {\out Level 3}

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

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

 \ttbreak

 by (resolve_tac [appNil,appCons] 1);

 {\out Level 4}

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

 {\out No subgoals!}

 \end{ttbox}

 Prolog can run functions backwards.  Which list can be appended

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

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

 \begin{ttbox}

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

 {\out Level 0}

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

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

 \ttbreak

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

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

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

 Prolog backtracking can answer questions that have multiple solutions.

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

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

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

 \begin{ttbox}

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

 {\out Level 0}

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

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

 \ttbreak

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

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

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

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

 \begin{ttbox}

 back();

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

 The other solutions are generated similarly.

 \begin{ttbox}

 back();

 {\out Level 1}

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

 {\out No subgoals!}

 \ttbreak

 back();

 {\out Level 1}

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

 {\out No subgoals!}

 \ttbreak

 back();

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

 \subsection{Depth-first search}

 \index{search!depth-first}

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

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

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

 terminates in a few seconds.

 \begin{ttbox}

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

 {\out Level 0}

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

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

 {\out         ?w)}

 \ttbreak

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

 \ttbreak

 by (REPEAT (resolve_tac rules 1));

 {\out Level 1}

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

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

 {\out No subgoals!}

 \end{ttbox}

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

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

 \begin{ttbox}

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

 {\out Level 0}

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

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

 \ttbreak

 by (REPEAT (resolve_tac rules 1));

 {\out Level 1}

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

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

 \end{ttbox}

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

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

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

 \begin{ttbox}

 back();

 {\out Level 1}

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

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

 \end{ttbox}

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

 \begin{ttbox}

 back();

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

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

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

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

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

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

 subgoals.

 \begin{ttbox}

 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 

                              (resolve_tac rules 1);

 \end{ttbox}

 Since Prolog uses depth-first search, this tactic is a (slow!) 

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

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

 \begin{ttbox}

 choplev 0;

 {\out Level 0}

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

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

 \ttbreak

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

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

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

 \begin{ttbox}

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

 {\out Level 0}

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

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

 \ttbreak

 by prolog_tac;

 {\out Level 1}

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

 {\out No subgoals!}

 \end{ttbox}

 Although Isabelle is much slower than a Prolog system, Isabelle

 tactics can exploit logic programming techniques.