
lcp@105: %% $Id$
lcp@284: \part{Advanced Methods}
lcp@105: Before continuing, it might be wise to try some of your own examples in
lcp@105: Isabelle, reinforcing your knowledge of the basic functions.
lcp@105: 
lcp@105: Look through {\em Isabelle's Object-Logics\/} and try proving some simple
lcp@105: theorems.  You probably should begin with first-order logic ({\tt FOL}
lcp@105: or~{\tt LK}).  Try working some of the examples provided, and others from
lcp@105: the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
lcp@105:   CTT}) form a richer world for mathematical reasoning and, again, many
lcp@105: examples are in the literature.  Higher-order logic~({\tt HOL}) is
lcp@331: Isabelle's most sophisticated logic because its types and functions are
lcp@331: identified with those of the meta-logic.
lcp@105: 
lcp@105: Choose a logic that you already understand.  Isabelle is a proof
lcp@105: tool, not a teaching tool; if you do not know how to do a particular proof
lcp@105: on paper, then you certainly will not be able to do it on the machine.
lcp@105: Even experienced users plan large proofs on paper.
lcp@105: 
lcp@105: We have covered only the bare essentials of Isabelle, but enough to perform
lcp@105: substantial proofs.  By occasionally dipping into the {\em Reference
lcp@105: Manual}, you can learn additional tactics, subgoal commands and tacticals.
lcp@105: 
lcp@105: 
lcp@105: \section{Deriving rules in Isabelle}
lcp@105: \index{rules!derived}
lcp@105: A mathematical development goes through a progression of stages.  Each
lcp@105: stage defines some concepts and derives rules about them.  We shall see how
lcp@105: to derive rules, perhaps involving definitions, using Isabelle.  The
lcp@310: following section will explain how to declare types, constants, rules and
lcp@105: definitions.
lcp@105: 
lcp@105: 
lcp@296: \subsection{Deriving a rule using tactics and meta-level assumptions} 
lcp@296: \label{deriving-example}
lcp@310: \index{examples!of deriving rules}\index{assumptions!of main goal}
lcp@296: 
lcp@307: The subgoal module supports the derivation of rules, as discussed in
lcp@307: \S\ref{deriving}.  The \ttindex{goal} command, when supplied a goal of the
lcp@307: form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
lcp@307: as the initial proof state and returns a list consisting of the theorems
lcp@307: ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.  These meta-assumptions
lcp@310: are also recorded internally, allowing {\tt result} to discharge them
lcp@307: in the original order.
lcp@105: 
lcp@307: Let us derive $\conj$ elimination using Isabelle.
lcp@310: Until now, calling {\tt goal} has returned an empty list, which we have
lcp@105: thrown away.  In this example, the list contains the two premises of the
lcp@105: rule.  We bind them to the \ML\ identifiers {\tt major} and {\tt
lcp@105: minor}:\footnote{Some ML compilers will print a message such as {\em
lcp@105: binding not exhaustive}.  This warns that {\tt goal} must return a
lcp@105: 2-element list.  Otherwise, the pattern-match will fail; ML will
lcp@310: raise exception \xdx{Match}.}
lcp@105: \begin{ttbox}
lcp@105: val [major,minor] = goal FOL.thy
lcp@105:     "[| P&Q;  [| P; Q |] ==> R |] ==> R";
lcp@105: {\out Level 0}
lcp@105: {\out R}
lcp@105: {\out  1. R}
lcp@105: {\out val major = "P & Q  [P & Q]" : thm}
lcp@105: {\out val minor = "[| P; Q |] ==> R  [[| P; Q |] ==> R]" : thm}
lcp@105: \end{ttbox}
lcp@105: Look at the minor premise, recalling that meta-level assumptions are
lcp@105: shown in brackets.  Using {\tt minor}, we reduce $R$ to the subgoals
lcp@105: $P$ and~$Q$:
lcp@105: \begin{ttbox}
lcp@105: by (resolve_tac [minor] 1);
lcp@105: {\out Level 1}
lcp@105: {\out R}
lcp@105: {\out  1. P}
lcp@105: {\out  2. Q}
lcp@105: \end{ttbox}
lcp@105: Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
lcp@105: assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
lcp@105: \begin{ttbox}
lcp@105: major RS conjunct1;
lcp@105: {\out val it = "P  [P & Q]" : thm}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [major RS conjunct1] 1);
lcp@105: {\out Level 2}
lcp@105: {\out R}
lcp@105: {\out  1. Q}
lcp@105: \end{ttbox}
lcp@105: Similarly, we solve the subgoal involving~$Q$.
lcp@105: \begin{ttbox}
lcp@105: major RS conjunct2;
lcp@105: {\out val it = "Q  [P & Q]" : thm}
lcp@105: by (resolve_tac [major RS conjunct2] 1);
lcp@105: {\out Level 3}
lcp@105: {\out R}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: Calling \ttindex{topthm} returns the current proof state as a theorem.
lcp@105: Note that it contains assumptions.  Calling \ttindex{result} discharges the
lcp@105: assumptions --- both occurrences of $P\conj Q$ are discharged as one ---
lcp@105: and makes the variables schematic.
lcp@105: \begin{ttbox}
lcp@105: topthm();
lcp@105: {\out val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
lcp@105: val conjE = result();
lcp@105: {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@105: \subsection{Definitions and derived rules} \label{definitions}
lcp@310: \index{rules!derived}\index{definitions!and derived rules|(}
lcp@310: 
lcp@105: Definitions are expressed as meta-level equalities.  Let us define negation
lcp@105: and the if-and-only-if connective:
lcp@105: \begin{eqnarray*}
lcp@105:   \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
lcp@105:   \Var{P}\bimp \Var{Q}  & \equiv & 
lcp@105:                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
lcp@105: \end{eqnarray*}
lcp@331: \index{meta-rewriting}%
lcp@105: Isabelle permits {\bf meta-level rewriting} using definitions such as
lcp@105: these.  {\bf Unfolding} replaces every instance
lcp@331: of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
lcp@105: example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
lcp@105: \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
lcp@105: {\bf Folding} a definition replaces occurrences of the right-hand side by
lcp@105: the left.  The occurrences need not be free in the entire formula.
lcp@105: 
lcp@105: When you define new concepts, you should derive rules asserting their
lcp@105: abstract properties, and then forget their definitions.  This supports
lcp@331: modularity: if you later change the definitions without affecting their
lcp@105: abstract properties, then most of your proofs will carry through without
lcp@105: change.  Indiscriminate unfolding makes a subgoal grow exponentially,
lcp@105: becoming unreadable.
lcp@105: 
lcp@105: Taking this point of view, Isabelle does not unfold definitions
lcp@105: automatically during proofs.  Rewriting must be explicit and selective.
lcp@105: Isabelle provides tactics and meta-rules for rewriting, and a version of
lcp@105: the {\tt goal} command that unfolds the conclusion and premises of the rule
lcp@105: being derived.
lcp@105: 
lcp@105: For example, the intuitionistic definition of negation given above may seem
lcp@105: peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
lcp@105: \[  \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}}   \qquad
lcp@105:     \infer[({\neg}E)]{Q}{\neg P & P}  \]
lcp@296: This requires proving the following meta-formulae:
lcp@105: $$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I)$$
lcp@105: $$ \List{\neg P; P} \Imp Q.       \eqno(\neg E)$$
lcp@105: 
lcp@105: 
lcp@296: \subsection{Deriving the $\neg$ introduction rule}
lcp@310: To derive $(\neg I)$, we may call {\tt goal} with the appropriate
lcp@105: formula.  Again, {\tt goal} returns a list consisting of the rule's
lcp@296: premises.  We bind this one-element list to the \ML\ identifier {\tt
lcp@296:   prems}.
lcp@105: \begin{ttbox}
lcp@105: val prems = goal FOL.thy "(P ==> False) ==> ~P";
lcp@105: {\out Level 0}
lcp@105: {\out ~P}
lcp@105: {\out  1. ~P}
lcp@105: {\out val prems = ["P ==> False  [P ==> False]"] : thm list}
lcp@105: \end{ttbox}
lcp@310: Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
lcp@105: definition of negation, unfolds that definition in the subgoals.  It leaves
lcp@105: the main goal alone.
lcp@105: \begin{ttbox}
lcp@105: not_def;
lcp@105: {\out val it = "~?P == ?P --> False" : thm}
lcp@105: by (rewrite_goals_tac [not_def]);
lcp@105: {\out Level 1}
lcp@105: {\out ~P}
lcp@105: {\out  1. P --> False}
lcp@105: \end{ttbox}
lcp@310: Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
lcp@105: \begin{ttbox}
lcp@105: by (resolve_tac [impI] 1);
lcp@105: {\out Level 2}
lcp@105: {\out ~P}
lcp@105: {\out  1. P ==> False}
lcp@105: \ttbreak
lcp@105: by (resolve_tac prems 1);
lcp@105: {\out Level 3}
lcp@105: {\out ~P}
lcp@105: {\out  1. P ==> P}
lcp@105: \end{ttbox}
lcp@296: The rest of the proof is routine.  Note the form of the final result.
lcp@105: \begin{ttbox}
lcp@105: by (assume_tac 1);
lcp@105: {\out Level 4}
lcp@105: {\out ~P}
lcp@105: {\out No subgoals!}
lcp@296: \ttbreak
lcp@105: val notI = result();
lcp@105: {\out val notI = "(?P ==> False) ==> ~?P" : thm}
lcp@105: \end{ttbox}
lcp@310: \indexbold{*notI theorem}
lcp@105: 
lcp@105: There is a simpler way of conducting this proof.  The \ttindex{goalw}
lcp@310: command starts a backward proof, as does {\tt goal}, but it also
lcp@296: unfolds definitions.  Thus there is no need to call
lcp@296: \ttindex{rewrite_goals_tac}:
lcp@105: \begin{ttbox}
lcp@105: val prems = goalw FOL.thy [not_def]
lcp@105:     "(P ==> False) ==> ~P";
lcp@105: {\out Level 0}
lcp@105: {\out ~P}
lcp@105: {\out  1. P --> False}
lcp@105: {\out val prems = ["P ==> False  [P ==> False]"] : thm list}
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@296: \subsection{Deriving the $\neg$ elimination rule}
lcp@284: Let us derive the rule $(\neg E)$.  The proof follows that of~{\tt conjE}
lcp@296: above, with an additional step to unfold negation in the major premise.
lcp@296: Although the {\tt goalw} command is best for this, let us
lcp@310: try~{\tt goal} to see another way of unfolding definitions.  After
lcp@310: binding the premises to \ML\ identifiers, we apply \tdx{FalseE}:
lcp@105: \begin{ttbox}
lcp@105: val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
lcp@105: {\out Level 0}
lcp@105: {\out R}
lcp@105: {\out  1. R}
lcp@105: {\out val major = "~ P  [~ P]" : thm}
lcp@105: {\out val minor = "P  [P]" : thm}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [FalseE] 1);
lcp@105: {\out Level 1}
lcp@105: {\out R}
lcp@105: {\out  1. False}
lcp@284: \end{ttbox}
lcp@284: Everything follows from falsity.  And we can prove falsity using the
lcp@284: premises and Modus Ponens:
lcp@284: \begin{ttbox}
lcp@105: by (resolve_tac [mp] 1);
lcp@105: {\out Level 2}
lcp@105: {\out R}
lcp@105: {\out  1. ?P1 --> False}
lcp@105: {\out  2. ?P1}
lcp@105: \end{ttbox}
lcp@105: For subgoal~1, we transform the major premise from~$\neg P$
lcp@105: to~${P\imp\bot}$.  The function \ttindex{rewrite_rule}, given a list of
lcp@296: definitions, unfolds them in a theorem.  Rewriting does not
lcp@105: affect the theorem's hypothesis, which remains~$\neg P$:
lcp@105: \begin{ttbox}
lcp@105: rewrite_rule [not_def] major;
lcp@105: {\out val it = "P --> False  [~P]" : thm}
lcp@105: by (resolve_tac [it] 1);
lcp@105: {\out Level 3}
lcp@105: {\out R}
lcp@105: {\out  1. P}
lcp@105: \end{ttbox}
lcp@296: The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove
lcp@284: using the minor premise:
lcp@105: \begin{ttbox}
lcp@105: by (resolve_tac [minor] 1);
lcp@105: {\out Level 4}
lcp@105: {\out R}
lcp@105: {\out No subgoals!}
lcp@105: val notE = result();
lcp@105: {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
lcp@105: \end{ttbox}
lcp@310: \indexbold{*notE theorem}
lcp@105: 
lcp@105: \medskip
lcp@284: Again, there is a simpler way of conducting this proof.  Recall that
lcp@284: the \ttindex{goalw} command unfolds definitions the conclusion; it also
lcp@284: unfolds definitions in the premises:
lcp@105: \begin{ttbox}
lcp@105: val [major,minor] = goalw FOL.thy [not_def]
lcp@105:     "[| ~P;  P |] ==> R";
lcp@105: {\out val major = "P --> False  [~ P]" : thm}
lcp@105: {\out val minor = "P  [P]" : thm}
lcp@105: \end{ttbox}
lcp@296: Observe the difference in {\tt major}; the premises are unfolded without
lcp@296: calling~\ttindex{rewrite_rule}.  Incidentally, the four calls to
lcp@296: \ttindex{resolve_tac} above can be collapsed to one, with the help
lcp@284: of~\ttindex{RS}; this is a typical example of forward reasoning from a
lcp@284: complex premise.
lcp@105: \begin{ttbox}
lcp@105: minor RS (major RS mp RS FalseE);
lcp@105: {\out val it = "?P  [P, ~P]" : thm}
lcp@105: by (resolve_tac [it] 1);
lcp@105: {\out Level 1}
lcp@105: {\out R}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@310: \index{definitions!and derived rules|)}
lcp@105: 
lcp@310: \goodbreak\medskip\index{*"!"! symbol!in main goal}
lcp@284: Finally, here is a trick that is sometimes useful.  If the goal
lcp@105: has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}
lcp@284: do not return the rule's premises in the list of theorems;  instead, the
lcp@284: premises become assumptions in subgoal~1.  
lcp@284: %%%It does not matter which variables are quantified over.
lcp@105: \begin{ttbox}
lcp@105: goalw FOL.thy [not_def] "!!P R. [| ~P;  P |] ==> R";
lcp@105: {\out Level 0}
lcp@105: {\out !!P R. [| ~ P; P |] ==> R}
lcp@105: {\out  1. !!P R. [| P --> False; P |] ==> R}
lcp@105: val it = [] : thm list
lcp@105: \end{ttbox}
lcp@105: The proof continues as before.  But instead of referring to \ML\
lcp@310: identifiers, we refer to assumptions using {\tt eresolve_tac} or
lcp@310: {\tt assume_tac}: 
lcp@105: \begin{ttbox}
lcp@105: by (resolve_tac [FalseE] 1);
lcp@105: {\out Level 1}
lcp@105: {\out !!P R. [| ~ P; P |] ==> R}
lcp@105: {\out  1. !!P R. [| P --> False; P |] ==> False}
lcp@105: \ttbreak
lcp@105: by (eresolve_tac [mp] 1);
lcp@105: {\out Level 2}
lcp@105: {\out !!P R. [| ~ P; P |] ==> R}
lcp@105: {\out  1. !!P R. P ==> P}
lcp@105: \ttbreak
lcp@105: by (assume_tac 1);
lcp@105: {\out Level 3}
lcp@105: {\out !!P R. [| ~ P; P |] ==> R}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: Calling \ttindex{result} strips the meta-quantifiers, so the resulting
lcp@105: theorem is the same as before.
lcp@105: \begin{ttbox}
lcp@105: val notE = result();
lcp@105: {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
lcp@105: \end{ttbox}
lcp@105: Do not use the {\tt!!}\ trick if the premises contain meta-level
lcp@105: connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would
lcp@105: not be able to handle the resulting assumptions.  The trick is not suitable
lcp@105: for deriving the introduction rule~$(\neg I)$.
lcp@105: 
lcp@105: 
lcp@284: \section{Defining theories}\label{sec:defining-theories}
lcp@105: \index{theories!defining|(}
lcp@310: 
lcp@105: Isabelle makes no distinction between simple extensions of a logic --- like
lcp@105: defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
lcp@105: an entire logic.  A theory definition has the form
lcp@105: \begin{ttbox}
lcp@105: \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
lcp@105: classes      {\it class declarations}
lcp@105: default      {\it sort}
lcp@331: types        {\it type declarations and synonyms}
lcp@105: arities      {\it arity declarations}
lcp@105: consts       {\it constant declarations}
lcp@105: rules        {\it rule declarations}
lcp@105: translations {\it translation declarations}
lcp@105: end
lcp@105: ML           {\it ML code}
lcp@105: \end{ttbox}
lcp@105: This declares the theory $T$ to extend the existing theories
lcp@105: $S@1$,~\ldots,~$S@n$.  It may declare new classes, types, arities
lcp@105: (overloadings of existing types), constants and rules; it can specify the
lcp@105: default sort for type variables.  A constant declaration can specify an
lcp@105: associated concrete syntax.  The translations section specifies rewrite
lcp@105: rules on abstract syntax trees, for defining notations and abbreviations.
lcp@310: \index{*ML section}
lcp@310: The {\tt ML} section contains code to perform arbitrary syntactic
lcp@284: transformations.  The main declaration forms are discussed below.
nipkow@303: The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
lcp@307:   appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
lcp@105: 
lcp@105: All the declaration parts can be omitted.  In the simplest case, $T$ is
lcp@105: just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
lcp@105: or more other theories, inheriting their types, constants, syntax, etc.
lcp@310: The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
lcp@105: 
lcp@331: Each theory definition must reside in a separate file, whose name is the
lcp@331: theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
lcp@331: on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
lcp@331: file containing a given theory; \ttindexbold{use_thy} automatically loads a
lcp@331: theory's parents before loading the theory itself.
lcp@105: 
lcp@331: Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
lcp@331: file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
lcp@331: {\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
lcp@331: occurred.  This declares the {\ML} structure~$T$, which contains a component
clasohm@109: {\tt thy} denoting the new theory, a component for each rule, and everything
clasohm@109: declared in {\it ML code}.
lcp@105: 
lcp@105: Errors may arise during the translation to {\ML} (say, a misspelled keyword)
lcp@105: or during creation of the new theory (say, a type error in a rule).  But if
lcp@331: all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
lcp@105: it exists.  This file typically begins with the {\ML} declaration {\tt
lcp@105: open}~$T$ and contains proofs that refer to the components of~$T$.
lcp@105: 
lcp@296: When a theory file is modified, many theories may have to be reloaded.
lcp@296: Isabelle records the modification times and dependencies of theory files.
lcp@331: See 
lcp@331: \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
lcp@331:                  {\S\ref{sec:reloading-theories}}
lcp@296: for more details.
lcp@296: 
lcp@105: 
lcp@105: \subsection{Declaring constants and rules}
lcp@310: \indexbold{constants!declaring}\index{rules!declaring}
lcp@310: 
lcp@296: Most theories simply declare constants and rules.  The {\bf constant
lcp@105: declaration part} has the form
lcp@105: \begin{ttbox}
lcp@105: consts  \(c@1\) :: "\(\tau@1\)"
lcp@105:         \vdots
lcp@105:         \(c@n\) :: "\(\tau@n\)"
lcp@105: \end{ttbox}
lcp@105: where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
lcp@105: types.  Each type {\em must\/} be enclosed in quotation marks.  Each
lcp@105: constant must be enclosed in quotation marks unless it is a valid
lcp@105: identifier.  To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
lcp@105: the $n$ declarations may be abbreviated to a single line:
lcp@105: \begin{ttbox}
lcp@105:         \(c@1\), \ldots, \(c@n\) :: "\(\tau\)"
lcp@105: \end{ttbox}
lcp@105: The {\bf rule declaration part} has the form
lcp@105: \begin{ttbox}
lcp@105: rules   \(id@1\) "\(rule@1\)"
lcp@105:         \vdots
lcp@105:         \(id@n\) "\(rule@n\)"
lcp@105: \end{ttbox}
lcp@105: where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
lcp@284: $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
lcp@284: enclosed in quotation marks.
lcp@284: 
lcp@310: \indexbold{definitions}
lcp@284: {\bf Definitions} are rules of the form $t\equiv u$.  Normally definitions
lcp@284: should be conservative, serving only as abbreviations.  As of this writing,
lcp@284: Isabelle does not provide a separate declaration part for definitions; it
lcp@284: is your responsibility to ensure that your definitions are conservative.
lcp@284: However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all
lcp@284: variables free in~$u$ are also free in~$t$.
lcp@105: 
lcp@105: \index{examples!of theories}
lcp@105: This theory extends first-order logic with two constants {\em nand} and
lcp@284: {\em xor}, and declares rules to define them:
lcp@284: \begin{ttbox}
lcp@105: Gate = FOL +
lcp@105: consts  nand,xor :: "[o,o] => o"
lcp@105: rules   nand_def "nand(P,Q) == ~(P & Q)"
lcp@105:         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@105: \subsection{Declaring type constructors}
nipkow@303: \indexbold{types!declaring}\indexbold{arities!declaring}
lcp@284: %
lcp@105: Types are composed of type variables and {\bf type constructors}.  Each
lcp@284: type constructor takes a fixed number of arguments.  They are declared
lcp@284: with an \ML-like syntax.  If $list$ takes one type argument, $tree$ takes
lcp@284: two arguments and $nat$ takes no arguments, then these type constructors
lcp@284: can be declared by
lcp@284: \begin{ttbox}
lcp@284: types 'a list
lcp@284:       ('a,'b) tree
lcp@284:       nat
lcp@284: \end{ttbox}
lcp@105: 
lcp@284: The {\bf type declaration part} has the general form
lcp@105: \begin{ttbox}
lcp@284: types   \(tids@1\) \(id@1\)
lcp@105:         \vdots
lcp@284:         \(tids@1\) \(id@n\)
lcp@105: \end{ttbox}
lcp@284: where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
lcp@284: are type argument lists as shown in the example above.  It declares each
lcp@284: $id@i$ as a type constructor with the specified number of argument places.
lcp@105: 
lcp@105: The {\bf arity declaration part} has the form
lcp@105: \begin{ttbox}
lcp@105: arities \(tycon@1\) :: \(arity@1\)
lcp@105:         \vdots
lcp@105:         \(tycon@n\) :: \(arity@n\)
lcp@105: \end{ttbox}
lcp@105: where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
lcp@105: $arity@n$ are arities.  Arity declarations add arities to existing
lcp@296: types; they do not declare the types themselves.
lcp@105: In the simplest case, for an 0-place type constructor, an arity is simply
lcp@105: the type's class.  Let us declare a type~$bool$ of class $term$, with
lcp@284: constants $tt$ and~$ff$.  (In first-order logic, booleans are
lcp@284: distinct from formulae, which have type $o::logic$.)
lcp@105: \index{examples!of theories}
lcp@284: \begin{ttbox}
lcp@105: Bool = FOL +
lcp@284: types   bool
lcp@105: arities bool    :: term
lcp@105: consts  tt,ff   :: "bool"
lcp@105: end
lcp@105: \end{ttbox}
lcp@296: A $k$-place type constructor may have arities of the form
lcp@296: $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
lcp@296: Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
lcp@296: where $c@1$, \dots,~$c@m$ are classes.  Mostly we deal with singleton
lcp@296: sorts, and may abbreviate them by dropping the braces.  The arity
lcp@296: $(term)term$ is short for $(\{term\})term$.  Recall the discussion in
lcp@296: \S\ref{polymorphic}.
lcp@105: 
lcp@105: A type constructor may be overloaded (subject to certain conditions) by
lcp@296: appearing in several arity declarations.  For instance, the function type
lcp@331: constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
lcp@105: logic, it is declared also to have arity $(term,term)term$.
lcp@105: 
lcp@105: Theory {\tt List} declares the 1-place type constructor $list$, gives
lcp@284: it arity $(term)term$, and declares constants $Nil$ and $Cons$ with
lcp@296: polymorphic types:%
lcp@296: \footnote{In the {\tt consts} part, type variable {\tt'a} has the default
lcp@296:   sort, which is {\tt term}.  See the {\em Reference Manual\/}
lcp@296: \iflabelundefined{sec:ref-defining-theories}{}%
lcp@296: {(\S\ref{sec:ref-defining-theories})} for more information.}
lcp@105: \index{examples!of theories}
lcp@284: \begin{ttbox}
lcp@105: List = FOL +
lcp@284: types   'a list
lcp@105: arities list    :: (term)term
lcp@105: consts  Nil     :: "'a list"
lcp@105:         Cons    :: "['a, 'a list] => 'a list" 
lcp@105: end
lcp@105: \end{ttbox}
lcp@284: Multiple arity declarations may be abbreviated to a single line:
lcp@105: \begin{ttbox}
lcp@105: arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: \begin{warn}
lcp@105: Arity declarations resemble constant declarations, but there are {\it no\/}
lcp@105: quotation marks!  Types and rules must be quoted because the theory
lcp@105: translator passes them verbatim to the {\ML} output file.
lcp@105: \end{warn}
lcp@105: 
lcp@331: \subsection{Type synonyms}\indexbold{type synonyms}
nipkow@303: Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
lcp@307: to those found in \ML.  Such synonyms are defined in the type declaration part
nipkow@303: and are fairly self explanatory:
nipkow@303: \begin{ttbox}
lcp@307: types gate       = "[o,o] => o"
lcp@307:       'a pred    = "'a => o"
nipkow@303:       ('a,'b)nuf = "'b => 'a"
nipkow@303: \end{ttbox}
nipkow@303: Type declarations and synonyms can be mixed arbitrarily:
nipkow@303: \begin{ttbox}
nipkow@303: types nat
nipkow@303:       'a stream = "nat => 'a"
lcp@307:       signal    = "nat stream"
nipkow@303:       'a list
nipkow@303: \end{ttbox}
lcp@307: A synonym is merely an abbreviation for some existing type expression.  Hence
lcp@307: synonyms may not be recursive!  Internally all synonyms are fully expanded.  As
lcp@307: a consequence Isabelle output never contains synonyms.  Their main purpose is
lcp@307: to improve the readability of theories.  Synonyms can be used just like any
nipkow@303: other type:
nipkow@303: \begin{ttbox}
nipkow@303: consts and,or :: "gate"
nipkow@303:        negate :: "signal => signal"
nipkow@303: \end{ttbox}
nipkow@303: 
lcp@348: \subsection{Infix and mixfix operators}
lcp@310: \index{infixes}\index{examples!of theories}
lcp@310: 
lcp@310: Infix or mixfix syntax may be attached to constants.  Consider the
lcp@310: following theory:
lcp@284: \begin{ttbox}
lcp@105: Gate2 = FOL +
lcp@105: consts  "~&"     :: "[o,o] => o"         (infixl 35)
lcp@105:         "#"      :: "[o,o] => o"         (infixl 30)
lcp@105: rules   nand_def "P ~& Q == ~(P & Q)"    
lcp@105:         xor_def  "P # Q  == P & ~Q | ~P & Q"
lcp@105: end
lcp@105: \end{ttbox}
lcp@310: The constant declaration part declares two left-associating infix operators
lcp@310: with their priorities, or precedences; they are $\nand$ of priority~35 and
lcp@310: $\xor$ of priority~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
lcp@310: \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the quotation
lcp@310: marks in \verb|"~&"| and \verb|"#"|.
lcp@105: 
lcp@105: The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
lcp@105: automatically, just as in \ML.  Hence you may write propositions like
lcp@105: \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
lcp@105: Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
lcp@105: 
lcp@310: \bigskip\index{mixfix declarations}
lcp@310: {\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us
lcp@310: add a line to the constant declaration part:
lcp@284: \begin{ttbox}
lcp@284:         If :: "[o,o,o] => o"       ("if _ then _ else _")
lcp@105: \end{ttbox}
lcp@310: This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
lcp@296:   if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}.  Underscores
lcp@310: denote argument positions.  
lcp@105: 
lcp@310: The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
lcp@310: construct to be split across several lines, even if it is too long to fit
lcp@310: on one line.  Pretty-printing information can be added to specify the
lcp@310: layout of mixfix operators.  For details, see
lcp@310: \iflabelundefined{Defining-Logics}%
lcp@310:     {the {\it Reference Manual}, chapter `Defining Logics'}%
lcp@310:     {Chap.\ts\ref{Defining-Logics}}.
lcp@310: 
lcp@310: Mixfix declarations can be annotated with priorities, just like
lcp@105: infixes.  The example above is just a shorthand for
lcp@284: \begin{ttbox}
lcp@284:         If :: "[o,o,o] => o"       ("if _ then _ else _" [0,0,0] 1000)
lcp@105: \end{ttbox}
lcp@310: The numeric components determine priorities.  The list of integers
lcp@310: defines, for each argument position, the minimal priority an expression
lcp@310: at that position must have.  The final integer is the priority of the
lcp@105: construct itself.  In the example above, any argument expression is
lcp@310: acceptable because priorities are non-negative, and conditionals may
lcp@310: appear everywhere because 1000 is the highest priority.  On the other
lcp@310: hand, the declaration
lcp@284: \begin{ttbox}
lcp@284:         If :: "[o,o,o] => o"       ("if _ then _ else _" [100,0,0] 99)
lcp@105: \end{ttbox}
lcp@284: defines concrete syntax for a conditional whose first argument cannot have
lcp@310: the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
lcp@310: of at least~100.  We may of course write
lcp@284: \begin{quote}\tt
lcp@284: if (if $P$ then $Q$ else $R$) then $S$ else $T$
lcp@156: \end{quote}
lcp@310: because expressions in parentheses have maximal priority.  
lcp@105: 
lcp@105: Binary type constructors, like products and sums, may also be declared as
lcp@105: infixes.  The type declaration below introduces a type constructor~$*$ with
lcp@105: infix notation $\alpha*\beta$, together with the mixfix notation
lcp@105: ${<}\_,\_{>}$ for pairs.  
lcp@310: \index{examples!of theories}\index{mixfix declarations}
lcp@105: \begin{ttbox}
lcp@105: Prod = FOL +
lcp@284: types   ('a,'b) "*"                           (infixl 20)
lcp@105: arities "*"     :: (term,term)term
lcp@105: consts  fst     :: "'a * 'b => 'a"
lcp@105:         snd     :: "'a * 'b => 'b"
lcp@105:         Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
lcp@105: rules   fst     "fst(<a,b>) = a"
lcp@105:         snd     "snd(<a,b>) = b"
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: \begin{warn}
lcp@105: The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would
lcp@105: be in the case of an infix constant.  Only infix type constructors can have
lcp@105: symbolic names like~{\tt *}.  There is no general mixfix syntax for types.
lcp@105: \end{warn}
lcp@105: 
lcp@105: 
lcp@105: \subsection{Overloading}
lcp@105: \index{overloading}\index{examples!of theories}
lcp@105: The {\bf class declaration part} has the form
lcp@105: \begin{ttbox}
lcp@105: classes \(id@1\) < \(c@1\)
lcp@105:         \vdots
lcp@105:         \(id@n\) < \(c@n\)
lcp@105: \end{ttbox}
lcp@105: where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are
lcp@105: existing classes.  It declares each $id@i$ as a new class, a subclass
lcp@105: of~$c@i$.  In the general case, an identifier may be declared to be a
lcp@105: subclass of $k$ existing classes:
lcp@105: \begin{ttbox}
lcp@105:         \(id\) < \(c@1\), \ldots, \(c@k\)
lcp@105: \end{ttbox}
lcp@296: Type classes allow constants to be overloaded.  As suggested in
lcp@307: \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
lcp@296: types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
lcp@296: \alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
lcp@296: $term$ and add the three polymorphic constants of this class.
lcp@310: \index{examples!of theories}\index{constants!overloaded}
lcp@105: \begin{ttbox}
lcp@105: Arith = FOL +
lcp@105: classes arith < term
lcp@105: consts  "0"     :: "'a::arith"                  ("0")
lcp@105:         "1"     :: "'a::arith"                  ("1")
lcp@105:         "+"     :: "['a::arith,'a] => 'a"       (infixl 60)
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: No rules are declared for these constants: we merely introduce their
lcp@105: names without specifying properties.  On the other hand, classes
lcp@105: with rules make it possible to prove {\bf generic} theorems.  Such
lcp@105: theorems hold for all instances, all types in that class.
lcp@105: 
lcp@105: We can now obtain distinct versions of the constants of $arith$ by
lcp@105: declaring certain types to be of class $arith$.  For example, let us
lcp@105: declare the 0-place type constructors $bool$ and $nat$:
lcp@105: \index{examples!of theories}
lcp@105: \begin{ttbox}
lcp@105: BoolNat = Arith +
lcp@348: types   bool  nat
lcp@348: arities bool, nat   :: arith
lcp@105: consts  Suc         :: "nat=>nat"
lcp@284: \ttbreak
lcp@105: rules   add0        "0 + n = n::nat"
lcp@105:         addS        "Suc(m)+n = Suc(m+n)"
lcp@105:         nat1        "1 = Suc(0)"
lcp@105:         or0l        "0 + x = x::bool"
lcp@105:         or0r        "x + 0 = x::bool"
lcp@105:         or1l        "1 + x = 1::bool"
lcp@105:         or1r        "x + 1 = 1::bool"
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
lcp@105: either type.  The type constraints in the axioms are vital.  Without
lcp@105: constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$
lcp@105: and the axiom would hold for any type of class $arith$.  This would
lcp@284: collapse $nat$ to a trivial type:
lcp@105: \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
lcp@105: 
lcp@296: 
lcp@296: \section{Theory example: the natural numbers}
lcp@296: 
lcp@296: We shall now work through a small example of formalized mathematics
lcp@105: demonstrating many of the theory extension features.
lcp@105: 
lcp@105: 
lcp@105: \subsection{Extending first-order logic with the natural numbers}
lcp@105: \index{examples!of theories}
lcp@105: 
lcp@284: Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
lcp@284: including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
lcp@284: Let us introduce the Peano axioms for mathematical induction and the
lcp@310: freeness of $0$ and~$Suc$:\index{axioms!Peano}
lcp@307: \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
lcp@105:  \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
lcp@105: \]
lcp@105: \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
lcp@105:    \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
lcp@105: \]
lcp@105: Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
lcp@105: provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
lcp@105: Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
lcp@105: To avoid making induction require the presence of other connectives, we
lcp@105: formalize mathematical induction as
lcp@105: $$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
lcp@105: 
lcp@105: \noindent
lcp@105: Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
lcp@105: and~$\neg$, we take advantage of the meta-logic;\footnote
lcp@105: {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
lcp@105: and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
lcp@105: better with Isabelle's simplifier.} 
lcp@105: $(Suc\_neq\_0)$ is
lcp@105: an elimination rule for $Suc(m)=0$:
lcp@105: $$ Suc(m)=Suc(n) \Imp m=n  \eqno(Suc\_inject) $$
lcp@105: $$ Suc(m)=0      \Imp R    \eqno(Suc\_neq\_0) $$
lcp@105: 
lcp@105: \noindent
lcp@105: We shall also define a primitive recursion operator, $rec$.  Traditionally,
lcp@105: primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
lcp@105: and obeys the equations
lcp@105: \begin{eqnarray*}
lcp@105:   rec(0,a,f)            & = & a \\
lcp@105:   rec(Suc(m),a,f)       & = & f(m, rec(m,a,f))
lcp@105: \end{eqnarray*}
lcp@105: Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
lcp@105: should satisfy
lcp@105: \begin{eqnarray*}
lcp@105:   0+n      & = & n \\
lcp@105:   Suc(m)+n & = & Suc(m+n)
lcp@105: \end{eqnarray*}
lcp@296: Primitive recursion appears to pose difficulties: first-order logic has no
lcp@296: function-valued expressions.  We again take advantage of the meta-logic,
lcp@296: which does have functions.  We also generalise primitive recursion to be
lcp@105: polymorphic over any type of class~$term$, and declare the addition
lcp@105: function:
lcp@105: \begin{eqnarray*}
lcp@105:   rec   & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
lcp@105:   +     & :: & [nat,nat]\To nat 
lcp@105: \end{eqnarray*}
lcp@105: 
lcp@105: 
lcp@105: \subsection{Declaring the theory to Isabelle}
lcp@105: \index{examples!of theories}
lcp@310: Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
lcp@105: which contains only classical logic with no natural numbers.  We declare
lcp@307: the 0-place type constructor $nat$ and the associated constants.  Note that
lcp@307: the constant~0 requires a mixfix annotation because~0 is not a legal
lcp@307: identifier, and could not otherwise be written in terms:
lcp@310: \begin{ttbox}\index{mixfix declarations}
lcp@105: Nat = FOL +
lcp@284: types   nat
lcp@105: arities nat         :: term
lcp@296: consts  "0"         :: "nat"                              ("0")
lcp@105:         Suc         :: "nat=>nat"
lcp@105:         rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
lcp@296:         "+"         :: "[nat, nat] => nat"                (infixl 60)
lcp@296: rules   Suc_inject  "Suc(m)=Suc(n) ==> m=n"
lcp@105:         Suc_neq_0   "Suc(m)=0      ==> R"
lcp@296:         induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
lcp@105:         rec_0       "rec(0,a,f) = a"
lcp@105:         rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
lcp@296:         add_def     "m+n == rec(m, n, \%x y. Suc(y))"
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.
lcp@296: Loading this theory file creates the \ML\ structure {\tt Nat}, which
lcp@296: contains the theory and axioms.  Opening structure {\tt Nat} lets us write
lcp@296: {\tt induct} instead of {\tt Nat.induct}, and so forth.
lcp@105: \begin{ttbox}
lcp@105: open Nat;
lcp@105: \end{ttbox}
lcp@296: 
lcp@296: \subsection{Proving some recursion equations}
lcp@331: File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
lcp@105: natural numbers.  As a trivial example, let us derive recursion equations
lcp@105: for \verb$+$.  Here is the zero case:
lcp@284: \begin{ttbox}
lcp@105: goalw Nat.thy [add_def] "0+n = n";
lcp@105: {\out Level 0}
lcp@105: {\out 0 + n = n}
lcp@284: {\out  1. rec(0,n,\%x y. Suc(y)) = n}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [rec_0] 1);
lcp@105: {\out Level 1}
lcp@105: {\out 0 + n = n}
lcp@105: {\out No subgoals!}
lcp@105: val add_0 = result();
lcp@284: \end{ttbox}
lcp@105: And here is the successor case:
lcp@284: \begin{ttbox}
lcp@105: goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
lcp@105: {\out Level 0}
lcp@105: {\out Suc(m) + n = Suc(m + n)}
lcp@284: {\out  1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [rec_Suc] 1);
lcp@105: {\out Level 1}
lcp@105: {\out Suc(m) + n = Suc(m + n)}
lcp@105: {\out No subgoals!}
lcp@105: val add_Suc = result();
lcp@284: \end{ttbox}
lcp@105: The induction rule raises some complications, which are discussed next.
lcp@105: \index{theories!defining|)}
lcp@105: 
lcp@105: 
lcp@105: \section{Refinement with explicit instantiation}
lcp@310: \index{resolution!with instantiation}
lcp@310: \index{instantiation|(}
lcp@310: 
lcp@105: In order to employ mathematical induction, we need to refine a subgoal by
lcp@105: the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
lcp@105: which is highly ambiguous in higher-order unification.  It matches every
lcp@105: way that a formula can be regarded as depending on a subterm of type~$nat$.
lcp@105: To get round this problem, we could make the induction rule conclude
lcp@105: $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
lcp@105: refinement by~$(\forall E)$, which is equally hard!
lcp@105: 
lcp@105: The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by
lcp@105: a rule.  But it also accepts explicit instantiations for the rule's
lcp@105: schematic variables.  
lcp@105: \begin{description}
lcp@310: \item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
lcp@105: instantiates the rule {\it thm} with the instantiations {\it insts}, and
lcp@105: then performs resolution on subgoal~$i$.
lcp@105: 
lcp@310: \item[\ttindex{eres_inst_tac}] 
lcp@310: and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
lcp@105: and destruct-resolution, respectively.
lcp@105: \end{description}
lcp@105: The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
lcp@105: where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
lcp@307: with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
lcp@105: expressions giving their instantiations.  The expressions are type-checked
lcp@105: in the context of a particular subgoal: free variables receive the same
lcp@105: types as they have in the subgoal, and parameters may appear.  Type
lcp@105: variable instantiations may appear in~{\it insts}, but they are seldom
lcp@105: required: {\tt res_inst_tac} instantiates type variables automatically
lcp@105: whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
lcp@105: 
lcp@105: \subsection{A simple proof by induction}
lcp@310: \index{examples!of induction}
lcp@105: Let us prove that no natural number~$k$ equals its own successor.  To
lcp@105: use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
lcp@105: instantiation for~$\Var{P}$.
lcp@284: \begin{ttbox}
lcp@105: goal Nat.thy "~ (Suc(k) = k)";
lcp@105: {\out Level 0}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. ~Suc(k) = k}
lcp@105: \ttbreak
lcp@105: by (res_inst_tac [("n","k")] induct 1);
lcp@105: {\out Level 1}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. ~Suc(0) = 0}
lcp@105: {\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
lcp@284: \end{ttbox}
lcp@105: We should check that Isabelle has correctly applied induction.  Subgoal~1
lcp@105: is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
lcp@105: with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
lcp@310: The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
lcp@310: other rules of theory {\tt Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
lcp@284: \begin{ttbox}
lcp@105: by (resolve_tac [notI] 1);
lcp@105: {\out Level 2}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. Suc(0) = 0 ==> False}
lcp@105: {\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
lcp@105: \ttbreak
lcp@105: by (eresolve_tac [Suc_neq_0] 1);
lcp@105: {\out Level 3}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
lcp@284: \end{ttbox}
lcp@105: The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
lcp@284: Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
lcp@284: $Suc(Suc(x)) = Suc(x)$:
lcp@284: \begin{ttbox}
lcp@105: by (resolve_tac [notI] 1);
lcp@105: {\out Level 4}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
lcp@105: \ttbreak
lcp@105: by (eresolve_tac [notE] 1);
lcp@105: {\out Level 5}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
lcp@105: \ttbreak
lcp@105: by (eresolve_tac [Suc_inject] 1);
lcp@105: {\out Level 6}
lcp@105: {\out ~Suc(k) = k}
lcp@105: {\out No subgoals!}
lcp@284: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@105: \subsection{An example of ambiguity in {\tt resolve_tac}}
lcp@105: \index{examples!of induction}\index{unification!higher-order}
lcp@105: If you try the example above, you may observe that {\tt res_inst_tac} is
lcp@105: not actually needed.  Almost by chance, \ttindex{resolve_tac} finds the right
lcp@105: instantiation for~$(induct)$ to yield the desired next state.  With more
lcp@105: complex formulae, our luck fails.  
lcp@284: \begin{ttbox}
lcp@105: goal Nat.thy "(k+m)+n = k+(m+n)";
lcp@105: {\out Level 0}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + n = k + (m + n)}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [induct] 1);
lcp@105: {\out Level 1}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + n = 0}
lcp@105: {\out  2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
lcp@284: \end{ttbox}
lcp@284: This proof requires induction on~$k$.  The occurrence of~0 in subgoal~1
lcp@284: indicates that induction has been applied to the term~$k+(m+n)$; this
lcp@284: application is sound but will not lead to a proof here.  Fortunately,
lcp@284: Isabelle can (lazily!) generate all the valid applications of induction.
lcp@284: The \ttindex{back} command causes backtracking to an alternative outcome of
lcp@284: the tactic.
lcp@284: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + n = k + 0}
lcp@105: {\out  2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
lcp@284: \end{ttbox}
lcp@284: Now induction has been applied to~$m+n$.  This is equally useless.  Let us
lcp@284: call \ttindex{back} again.
lcp@284: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + 0 = k + (m + 0)}
lcp@284: {\out  2. !!x. k + m + x = k + (m + x) ==>}
lcp@284: {\out          k + m + Suc(x) = k + (m + Suc(x))}
lcp@284: \end{ttbox}
lcp@105: Now induction has been applied to~$n$.  What is the next alternative?
lcp@284: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + n = k + (m + 0)}
lcp@105: {\out  2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
lcp@284: \end{ttbox}
lcp@105: Inspecting subgoal~1 reveals that induction has been applied to just the
lcp@105: second occurrence of~$n$.  This perfectly legitimate induction is useless
lcp@310: here.  
lcp@310: 
lcp@310: The main goal admits fourteen different applications of induction.  The
lcp@310: number is exponential in the size of the formula.
lcp@105: 
lcp@105: \subsection{Proving that addition is associative}
lcp@331: Let us invoke the induction rule properly, using~{\tt
lcp@310:   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
lcp@310: simplification tactics, which are described in 
lcp@310: \iflabelundefined{simp-chap}%
lcp@310:     {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
lcp@105: 
lcp@310: \index{simplification}\index{examples!of simplification} 
lcp@284: 
lcp@310: Isabelle's simplification tactics repeatedly apply equations to a subgoal,
lcp@310: perhaps proving it.  For efficiency, the rewrite rules must be
lcp@310: packaged into a {\bf simplification set},\index{simplification sets} 
lcp@310: or {\bf simpset}.  We take the standard simpset for first-order logic and
lcp@331: insert the equations proved in the previous section, namely
lcp@310: $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
lcp@284: \begin{ttbox}
lcp@105: val add_ss = FOL_ss addrews [add_0, add_Suc];
lcp@284: \end{ttbox}
lcp@105: We state the goal for associativity of addition, and
lcp@105: use \ttindex{res_inst_tac} to invoke induction on~$k$:
lcp@284: \begin{ttbox}
lcp@105: goal Nat.thy "(k+m)+n = k+(m+n)";
lcp@105: {\out Level 0}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. k + m + n = k + (m + n)}
lcp@105: \ttbreak
lcp@105: by (res_inst_tac [("n","k")] induct 1);
lcp@105: {\out Level 1}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out  1. 0 + m + n = 0 + (m + n)}
lcp@284: {\out  2. !!x. x + m + n = x + (m + n) ==>}
lcp@284: {\out          Suc(x) + m + n = Suc(x) + (m + n)}
lcp@284: \end{ttbox}
lcp@105: The base case holds easily; both sides reduce to $m+n$.  The
lcp@105: tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
lcp@331: set, applying the rewrite rules for addition:
lcp@284: \begin{ttbox}
lcp@105: by (simp_tac add_ss 1);
lcp@105: {\out Level 2}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@284: {\out  1. !!x. x + m + n = x + (m + n) ==>}
lcp@284: {\out          Suc(x) + m + n = Suc(x) + (m + n)}
lcp@284: \end{ttbox}
lcp@331: The inductive step requires rewriting by the equations for addition
lcp@105: together the induction hypothesis, which is also an equation.  The
lcp@105: tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
lcp@105: useful assumptions:
lcp@284: \begin{ttbox}
lcp@105: by (asm_simp_tac add_ss 1);
lcp@105: {\out Level 3}
lcp@105: {\out k + m + n = k + (m + n)}
lcp@105: {\out No subgoals!}
lcp@284: \end{ttbox}
lcp@310: \index{instantiation|)}
lcp@105: 
lcp@105: 
lcp@284: \section{A Prolog interpreter}
lcp@105: \index{Prolog interpreter|bold}
lcp@284: To demonstrate the power of tacticals, let us construct a Prolog
lcp@105: interpreter and execute programs involving lists.\footnote{To run these
lcp@331: examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program
lcp@105: consists of a theory.  We declare a type constructor for lists, with an
lcp@105: arity declaration to say that $(\tau)list$ is of class~$term$
lcp@105: provided~$\tau$ is:
lcp@105: \begin{eqnarray*}
lcp@105:   list  & :: & (term)term
lcp@105: \end{eqnarray*}
lcp@105: We declare four constants: the empty list~$Nil$; the infix list
lcp@105: constructor~{:}; the list concatenation predicate~$app$; the list reverse
lcp@284: predicate~$rev$.  (In Prolog, functions on lists are expressed as
lcp@105: predicates.)
lcp@105: \begin{eqnarray*}
lcp@105:     Nil         & :: & \alpha list \\
lcp@105:     {:}         & :: & [\alpha,\alpha list] \To \alpha list \\
lcp@105:     app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
lcp@105:     rev & :: & [\alpha list,\alpha list] \To o 
lcp@105: \end{eqnarray*}
lcp@284: The predicate $app$ should satisfy the Prolog-style rules
lcp@105: \[ {app(Nil,ys,ys)} \qquad
lcp@105:    {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
lcp@105: We define the naive version of $rev$, which calls~$app$:
lcp@105: \[ {rev(Nil,Nil)} \qquad
lcp@105:    {rev(xs,ys)\quad  app(ys, x:Nil, zs) \over
lcp@105:     rev(x:xs, zs)} 
lcp@105: \]
lcp@105: 
lcp@105: \index{examples!of theories}
lcp@310: Theory \thydx{Prolog} extends first-order logic in order to make use
lcp@105: of the class~$term$ and the type~$o$.  The interpreter does not use the
lcp@310: rules of~{\tt FOL}.
lcp@105: \begin{ttbox}
lcp@105: Prolog = FOL +
lcp@296: types   'a list
lcp@105: arities list    :: (term)term
lcp@105: consts  Nil     :: "'a list"
lcp@105:         ":"     :: "['a, 'a list]=> 'a list"            (infixr 60)
lcp@105:         app     :: "['a list, 'a list, 'a list] => o"
lcp@105:         rev     :: "['a list, 'a list] => o"
lcp@105: rules   appNil  "app(Nil,ys,ys)"
lcp@105:         appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
lcp@105:         revNil  "rev(Nil,Nil)"
lcp@105:         revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
lcp@105: end
lcp@105: \end{ttbox}
lcp@105: \subsection{Simple executions}
lcp@284: Repeated application of the rules solves Prolog goals.  Let us
lcp@105: append the lists $[a,b,c]$ and~$[d,e]$.  As the rules are applied, the
lcp@105: answer builds up in~{\tt ?x}.
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";
lcp@105: {\out Level 0}
lcp@105: {\out app(a : b : c : Nil, d : e : Nil, ?x)}
lcp@105: {\out  1. app(a : b : c : Nil, d : e : Nil, ?x)}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [appNil,appCons] 1);
lcp@105: {\out Level 1}
lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
lcp@105: {\out  1. app(b : c : Nil, d : e : Nil, ?zs1)}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [appNil,appCons] 1);
lcp@105: {\out Level 2}
lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
lcp@105: {\out  1. app(c : Nil, d : e : Nil, ?zs2)}
lcp@105: \end{ttbox}
lcp@105: At this point, the first two elements of the result are~$a$ and~$b$.
lcp@105: \begin{ttbox}
lcp@105: by (resolve_tac [appNil,appCons] 1);
lcp@105: {\out Level 3}
lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
lcp@105: {\out  1. app(Nil, d : e : Nil, ?zs3)}
lcp@105: \ttbreak
lcp@105: by (resolve_tac [appNil,appCons] 1);
lcp@105: {\out Level 4}
lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: 
lcp@284: Prolog can run functions backwards.  Which list can be appended
lcp@105: with $[c,d]$ to produce $[a,b,c,d]$?
lcp@105: Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";
lcp@105: {\out Level 0}
lcp@105: {\out app(?x, c : d : Nil, a : b : c : d : Nil)}
lcp@105: {\out  1. app(?x, c : d : Nil, a : b : c : d : Nil)}
lcp@105: \ttbreak
lcp@105: by (REPEAT (resolve_tac [appNil,appCons] 1));
lcp@105: {\out Level 1}
lcp@105: {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@310: \subsection{Backtracking}\index{backtracking!Prolog style}
lcp@296: Prolog backtracking can answer questions that have multiple solutions.
lcp@296: Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?  This
lcp@296: question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
lcp@296: quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
lcp@105: {\out Level 0}
lcp@105: {\out app(?x, ?y, a : b : c : d : Nil)}
lcp@105: {\out  1. app(?x, ?y, a : b : c : d : Nil)}
lcp@105: \ttbreak
lcp@105: by (REPEAT (resolve_tac [appNil,appCons] 1));
lcp@105: {\out Level 1}
lcp@105: {\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@284: Isabelle can lazily generate all the possibilities.  The \ttindex{back}
lcp@284: command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
lcp@105: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: The other solutions are generated similarly.
lcp@105: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \ttbreak
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \ttbreak
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: 
lcp@105: 
lcp@105: \subsection{Depth-first search}
lcp@105: \index{search!depth-first}
lcp@105: Now let us try $rev$, reversing a list.
lcp@105: Bundle the rules together as the \ML{} identifier {\tt rules}.  Naive
lcp@105: reverse requires 120 inferences for this 14-element list, but the tactic
lcp@105: terminates in a few seconds.
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
lcp@105: {\out Level 0}
lcp@105: {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
lcp@284: {\out  1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
lcp@284: {\out         ?w)}
lcp@284: \ttbreak
lcp@105: val rules = [appNil,appCons,revNil,revCons];
lcp@105: \ttbreak
lcp@105: by (REPEAT (resolve_tac rules 1));
lcp@105: {\out Level 1}
lcp@105: {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
lcp@105: {\out     n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: We may execute $rev$ backwards.  This, too, should reverse a list.  What
lcp@105: is the reverse of $[a,b,c]$?
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "rev(?x, a:b:c:Nil)";
lcp@105: {\out Level 0}
lcp@105: {\out rev(?x, a : b : c : Nil)}
lcp@105: {\out  1. rev(?x, a : b : c : Nil)}
lcp@105: \ttbreak
lcp@105: by (REPEAT (resolve_tac rules 1));
lcp@105: {\out Level 1}
lcp@105: {\out rev(?x1 : Nil, a : b : c : Nil)}
lcp@105: {\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
lcp@105: \end{ttbox}
lcp@105: The tactic has failed to find a solution!  It reached a dead end at
lcp@331: subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
lcp@105: equals~$[a,b,c]$.  Backtracking explores other outcomes.
lcp@105: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out rev(?x1 : a : Nil, a : b : c : Nil)}
lcp@105: {\out  1. app(Nil, ?x1 : Nil, b : c : Nil)}
lcp@105: \end{ttbox}
lcp@105: This too is a dead end, but the next outcome is successful.
lcp@105: \begin{ttbox}
lcp@105: back();
lcp@105: {\out Level 1}
lcp@105: {\out rev(c : b : a : Nil, a : b : c : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@310: \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
lcp@310: search tactical.  {\tt REPEAT} stops when it cannot continue, regardless of
lcp@310: which state is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a
lcp@310: satisfactory state, as specified by an \ML{} predicate.  Below,
lcp@105: \ttindex{has_fewer_prems} specifies that the proof state should have no
lcp@310: subgoals.
lcp@105: \begin{ttbox}
lcp@105: val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 
lcp@105:                              (resolve_tac rules 1);
lcp@105: \end{ttbox}
lcp@284: Since Prolog uses depth-first search, this tactic is a (slow!) 
lcp@296: Prolog interpreter.  We return to the start of the proof using
lcp@296: \ttindex{choplev}, and apply {\tt prolog_tac}:
lcp@105: \begin{ttbox}
lcp@105: choplev 0;
lcp@105: {\out Level 0}
lcp@105: {\out rev(?x, a : b : c : Nil)}
lcp@105: {\out  1. rev(?x, a : b : c : Nil)}
lcp@105: \ttbreak
lcp@105: by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));
lcp@105: {\out Level 1}
lcp@105: {\out rev(c : b : a : Nil, a : b : c : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@105: Let us try {\tt prolog_tac} on one more example, containing four unknowns:
lcp@105: \begin{ttbox}
lcp@105: goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
lcp@105: {\out Level 0}
lcp@105: {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
lcp@105: {\out  1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
lcp@105: \ttbreak
lcp@105: by prolog_tac;
lcp@105: {\out Level 1}
lcp@105: {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
lcp@105: {\out No subgoals!}
lcp@105: \end{ttbox}
lcp@284: Although Isabelle is much slower than a Prolog system, Isabelle
lcp@156: tactics can exploit logic programming techniques.  
lcp@156: 




