doc-src/Intro/advanced.tex
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14)
changeset 16842 5979c46853d1
parent 14148 6580d374a509
child 42637 381fdcab0f36
permissions -rw-r--r--
tuned;
     1 %% $Id$
     2 \part{Advanced Methods}
     3 Before continuing, it might be wise to try some of your own examples in
     4 Isabelle, reinforcing your knowledge of the basic functions.
     5 
     6 Look through {\em Isabelle's Object-Logics\/} and try proving some
     7 simple theorems.  You probably should begin with first-order logic
     8 (\texttt{FOL} or~\texttt{LK}).  Try working some of the examples provided,
     9 and others from the literature.  Set theory~(\texttt{ZF}) and
    10 Constructive Type Theory~(\texttt{CTT}) form a richer world for
    11 mathematical reasoning and, again, many examples are in the
    12 literature.  Higher-order logic~(\texttt{HOL}) is Isabelle's most
    13 elaborate logic.  Its types and functions are identified with those of
    14 the meta-logic.
    15 
    16 Choose a logic that you already understand.  Isabelle is a proof
    17 tool, not a teaching tool; if you do not know how to do a particular proof
    18 on paper, then you certainly will not be able to do it on the machine.
    19 Even experienced users plan large proofs on paper.
    20 
    21 We have covered only the bare essentials of Isabelle, but enough to perform
    22 substantial proofs.  By occasionally dipping into the {\em Reference
    23 Manual}, you can learn additional tactics, subgoal commands and tacticals.
    24 
    25 
    26 \section{Deriving rules in Isabelle}
    27 \index{rules!derived}
    28 A mathematical development goes through a progression of stages.  Each
    29 stage defines some concepts and derives rules about them.  We shall see how
    30 to derive rules, perhaps involving definitions, using Isabelle.  The
    31 following section will explain how to declare types, constants, rules and
    32 definitions.
    33 
    34 
    35 \subsection{Deriving a rule using tactics and meta-level assumptions} 
    36 \label{deriving-example}
    37 \index{examples!of deriving rules}\index{assumptions!of main goal}
    38 
    39 The subgoal module supports the derivation of rules, as discussed in
    40 \S\ref{deriving}.  When the \ttindex{Goal} command is supplied a formula of
    41 the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two
    42 possibilities:
    43 \begin{itemize}
    44 \item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple
    45   formulae{} (they do not involve the meta-connectives $\Forall$ or
    46   $\Imp$) then the command sets the goal to be 
    47   $\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list.
    48 \item If one or more premises involves the meta-connectives $\Forall$ or
    49   $\Imp$, then the command sets the goal to be $\phi$ and returns a list
    50   consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
    51   These meta-level assumptions are also recorded internally, allowing
    52   \texttt{result} (which is called by \texttt{qed}) to discharge them in the
    53   original order.
    54 \end{itemize}
    55 Rules that discharge assumptions or introduce eigenvariables have complex
    56 premises, and the second case applies.  In this section, many of the
    57 theorems are subject to meta-level assumptions, so we make them visible by by setting the 
    58 \ttindex{show_hyps} flag:
    59 \begin{ttbox} 
    60 set show_hyps;
    61 {\out val it = true : bool}
    62 \end{ttbox}
    63 
    64 Now, we are ready to derive $\conj$ elimination.  Until now, calling \texttt{Goal} has
    65 returned an empty list, which we have ignored.  In this example, the list
    66 contains the two premises of the rule, since one of them involves the $\Imp$
    67 connective.  We bind them to the \ML\ identifiers \texttt{major} and {\tt
    68   minor}:\footnote{Some ML compilers will print a message such as {\em binding
    69     not exhaustive}.  This warns that \texttt{Goal} must return a 2-element
    70   list.  Otherwise, the pattern-match will fail; ML will raise exception
    71   \xdx{Match}.}
    72 \begin{ttbox}
    73 val [major,minor] = Goal
    74     "[| P&Q;  [| P; Q |] ==> R |] ==> R";
    75 {\out Level 0}
    76 {\out R}
    77 {\out  1. R}
    78 {\out val major = "P & Q  [P & Q]" : thm}
    79 {\out val minor = "[| P; Q |] ==> R  [[| P; Q |] ==> R]" : thm}
    80 \end{ttbox}
    81 Look at the minor premise, recalling that meta-level assumptions are
    82 shown in brackets.  Using \texttt{minor}, we reduce $R$ to the subgoals
    83 $P$ and~$Q$:
    84 \begin{ttbox}
    85 by (resolve_tac [minor] 1);
    86 {\out Level 1}
    87 {\out R}
    88 {\out  1. P}
    89 {\out  2. Q}
    90 \end{ttbox}
    91 Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
    92 assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
    93 \begin{ttbox}
    94 major RS conjunct1;
    95 {\out val it = "P  [P & Q]" : thm}
    96 \ttbreak
    97 by (resolve_tac [major RS conjunct1] 1);
    98 {\out Level 2}
    99 {\out R}
   100 {\out  1. Q}
   101 \end{ttbox}
   102 Similarly, we solve the subgoal involving~$Q$.
   103 \begin{ttbox}
   104 major RS conjunct2;
   105 {\out val it = "Q  [P & Q]" : thm}
   106 by (resolve_tac [major RS conjunct2] 1);
   107 {\out Level 3}
   108 {\out R}
   109 {\out No subgoals!}
   110 \end{ttbox}
   111 Calling \ttindex{topthm} returns the current proof state as a theorem.
   112 Note that it contains assumptions.  Calling \ttindex{qed} discharges
   113 the assumptions --- both occurrences of $P\conj Q$ are discharged as
   114 one --- and makes the variables schematic.
   115 \begin{ttbox}
   116 topthm();
   117 {\out val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
   118 qed "conjE";
   119 {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
   120 \end{ttbox}
   121 
   122 
   123 \subsection{Definitions and derived rules} \label{definitions}
   124 \index{rules!derived}\index{definitions!and derived rules|(}
   125 
   126 Definitions are expressed as meta-level equalities.  Let us define negation
   127 and the if-and-only-if connective:
   128 \begin{eqnarray*}
   129   \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
   130   \Var{P}\bimp \Var{Q}  & \equiv & 
   131                 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
   132 \end{eqnarray*}
   133 \index{meta-rewriting}%
   134 Isabelle permits {\bf meta-level rewriting} using definitions such as
   135 these.  {\bf Unfolding} replaces every instance
   136 of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
   137 example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
   138 \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
   139 {\bf Folding} a definition replaces occurrences of the right-hand side by
   140 the left.  The occurrences need not be free in the entire formula.
   141 
   142 When you define new concepts, you should derive rules asserting their
   143 abstract properties, and then forget their definitions.  This supports
   144 modularity: if you later change the definitions without affecting their
   145 abstract properties, then most of your proofs will carry through without
   146 change.  Indiscriminate unfolding makes a subgoal grow exponentially,
   147 becoming unreadable.
   148 
   149 Taking this point of view, Isabelle does not unfold definitions
   150 automatically during proofs.  Rewriting must be explicit and selective.
   151 Isabelle provides tactics and meta-rules for rewriting, and a version of
   152 the \texttt{Goal} command that unfolds the conclusion and premises of the rule
   153 being derived.
   154 
   155 For example, the intuitionistic definition of negation given above may seem
   156 peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
   157 \[  \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}}   \qquad
   158     \infer[({\neg}E)]{Q}{\neg P & P}  \]
   159 This requires proving the following meta-formulae:
   160 $$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I) $$
   161 $$ \List{\neg P; P} \Imp Q.       \eqno(\neg E) $$
   162 
   163 
   164 \subsection{Deriving the $\neg$ introduction rule}
   165 To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
   166 Again, the rule's premises involve a meta-connective, and \texttt{Goal}
   167 returns one-element list.  We bind this list to the \ML\ identifier \texttt{prems}.
   168 \begin{ttbox}
   169 val prems = Goal "(P ==> False) ==> ~P";
   170 {\out Level 0}
   171 {\out ~P}
   172 {\out  1. ~P}
   173 {\out val prems = ["P ==> False  [P ==> False]"] : thm list}
   174 \end{ttbox}
   175 Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
   176 definition of negation, unfolds that definition in the subgoals.  It leaves
   177 the main goal alone.
   178 \begin{ttbox}
   179 not_def;
   180 {\out val it = "~?P == ?P --> False" : thm}
   181 by (rewrite_goals_tac [not_def]);
   182 {\out Level 1}
   183 {\out ~P}
   184 {\out  1. P --> False}
   185 \end{ttbox}
   186 Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
   187 \begin{ttbox}
   188 by (resolve_tac [impI] 1);
   189 {\out Level 2}
   190 {\out ~P}
   191 {\out  1. P ==> False}
   192 \ttbreak
   193 by (resolve_tac prems 1);
   194 {\out Level 3}
   195 {\out ~P}
   196 {\out  1. P ==> P}
   197 \end{ttbox}
   198 The rest of the proof is routine.  Note the form of the final result.
   199 \begin{ttbox}
   200 by (assume_tac 1);
   201 {\out Level 4}
   202 {\out ~P}
   203 {\out No subgoals!}
   204 \ttbreak
   205 qed "notI";
   206 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
   207 \end{ttbox}
   208 \indexbold{*notI theorem}
   209 
   210 There is a simpler way of conducting this proof.  The \ttindex{Goalw}
   211 command starts a backward proof, as does \texttt{Goal}, but it also
   212 unfolds definitions.  Thus there is no need to call
   213 \ttindex{rewrite_goals_tac}:
   214 \begin{ttbox}
   215 val prems = Goalw [not_def]
   216     "(P ==> False) ==> ~P";
   217 {\out Level 0}
   218 {\out ~P}
   219 {\out  1. P --> False}
   220 {\out val prems = ["P ==> False  [P ==> False]"] : thm list}
   221 \end{ttbox}
   222 
   223 
   224 \subsection{Deriving the $\neg$ elimination rule}
   225 Let us derive the rule $(\neg E)$.  The proof follows that of~\texttt{conjE}
   226 above, with an additional step to unfold negation in the major premise.
   227 The \texttt{Goalw} command is best for this: it unfolds definitions not only
   228 in the conclusion but the premises.
   229 \begin{ttbox}
   230 Goalw [not_def] "[| ~P;  P |] ==> R";
   231 {\out Level 0}
   232 {\out [| ~ P; P |] ==> R}
   233 {\out  1. [| P --> False; P |] ==> R}
   234 \end{ttbox}
   235 As the first step, we apply \tdx{FalseE}:
   236 \begin{ttbox}
   237 by (resolve_tac [FalseE] 1);
   238 {\out Level 1}
   239 {\out [| ~ P; P |] ==> R}
   240 {\out  1. [| P --> False; P |] ==> False}
   241 \end{ttbox}
   242 %
   243 Everything follows from falsity.  And we can prove falsity using the
   244 premises and Modus Ponens:
   245 \begin{ttbox}
   246 by (eresolve_tac [mp] 1);
   247 {\out Level 2}
   248 {\out [| ~ P; P |] ==> R}
   249 {\out  1. P ==> P}
   250 \ttbreak
   251 by (assume_tac 1);
   252 {\out Level 3}
   253 {\out [| ~ P; P |] ==> R}
   254 {\out No subgoals!}
   255 \ttbreak
   256 qed "notE";
   257 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
   258 \end{ttbox}
   259 
   260 
   261 \medskip
   262 \texttt{Goalw} unfolds definitions in the premises even when it has to return
   263 them as a list.  Another way of unfolding definitions in a theorem is by
   264 applying the function \ttindex{rewrite_rule}.
   265 
   266 \index{definitions!and derived rules|)}
   267 
   268 
   269 \section{Defining theories}\label{sec:defining-theories}
   270 \index{theories!defining|(}
   271 
   272 Isabelle makes no distinction between simple extensions of a logic ---
   273 like specifying a type~$bool$ with constants~$true$ and~$false$ ---
   274 and defining an entire logic.  A theory definition has a form like
   275 \begin{ttbox}
   276 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
   277 classes      {\it class declarations}
   278 default      {\it sort}
   279 types        {\it type declarations and synonyms}
   280 arities      {\it type arity declarations}
   281 consts       {\it constant declarations}
   282 syntax       {\it syntactic constant declarations}
   283 translations {\it ast translation rules}
   284 defs         {\it meta-logical definitions}
   285 rules        {\it rule declarations}
   286 end
   287 ML           {\it ML code}
   288 \end{ttbox}
   289 This declares the theory $T$ to extend the existing theories
   290 $S@1$,~\ldots,~$S@n$.  It may introduce new classes, types, arities
   291 (of existing types), constants and rules; it can specify the default
   292 sort for type variables.  A constant declaration can specify an
   293 associated concrete syntax.  The translations section specifies
   294 rewrite rules on abstract syntax trees, handling notations and
   295 abbreviations.  \index{*ML section} The \texttt{ML} section may contain
   296 code to perform arbitrary syntactic transformations.  The main
   297 declaration forms are discussed below.  There are some more sections
   298 not presented here, the full syntax can be found in
   299 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
   300     Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
   301 object-logics may add further theory sections, for example
   302 \texttt{typedef}, \texttt{datatype} in HOL.
   303 
   304 All the declaration parts can be omitted or repeated and may appear in
   305 any order, except that the {\ML} section must be last (after the {\tt
   306   end} keyword).  In the simplest case, $T$ is just the union of
   307 $S@1$,~\ldots,~$S@n$.  New theories always extend one or more other
   308 theories, inheriting their types, constants, syntax, etc.  The theory
   309 \thydx{Pure} contains nothing but Isabelle's meta-logic.  The variant
   310 \thydx{CPure} offers the more usual higher-order function application
   311 syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
   312 
   313 Each theory definition must reside in a separate file, whose name is
   314 the theory's with {\tt.thy} appended.  Calling
   315 \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
   316   T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
   317     T}.thy.ML}, reads the latter file, and deletes it if no errors
   318 occurred.  This declares the {\ML} structure~$T$, which contains a
   319 component \texttt{thy} denoting the new theory, a component for each
   320 rule, and everything declared in {\it ML code}.
   321 
   322 Errors may arise during the translation to {\ML} (say, a misspelled
   323 keyword) or during creation of the new theory (say, a type error in a
   324 rule).  But if all goes well, \texttt{use_thy} will finally read the file
   325 {\it T}{\tt.ML} (if it exists).  This file typically contains proofs
   326 that refer to the components of~$T$.  The structure is automatically
   327 opened, so its components may be referred to by unqualified names,
   328 e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}.
   329 
   330 \ttindexbold{use_thy} automatically loads a theory's parents before
   331 loading the theory itself.  When a theory file is modified, many
   332 theories may have to be reloaded.  Isabelle records the modification
   333 times and dependencies of theory files.  See
   334 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
   335                  {\S\ref{sec:reloading-theories}}
   336 for more details.
   337 
   338 
   339 \subsection{Declaring constants, definitions and rules}
   340 \indexbold{constants!declaring}\index{rules!declaring}
   341 
   342 Most theories simply declare constants, definitions and rules.  The {\bf
   343   constant declaration part} has the form
   344 \begin{ttbox}
   345 consts  \(c@1\) :: \(\tau@1\)
   346         \vdots
   347         \(c@n\) :: \(\tau@n\)
   348 \end{ttbox}
   349 where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
   350 types.  The types must be enclosed in quotation marks if they contain
   351 user-declared infix type constructors like \texttt{*}.  Each
   352 constant must be enclosed in quotation marks unless it is a valid
   353 identifier.  To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
   354 the $n$ declarations may be abbreviated to a single line:
   355 \begin{ttbox}
   356         \(c@1\), \ldots, \(c@n\) :: \(\tau\)
   357 \end{ttbox}
   358 The {\bf rule declaration part} has the form
   359 \begin{ttbox}
   360 rules   \(id@1\) "\(rule@1\)"
   361         \vdots
   362         \(id@n\) "\(rule@n\)"
   363 \end{ttbox}
   364 where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
   365 $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
   366 enclosed in quotation marks.  Rules are simply axioms; they are 
   367 called \emph{rules} because they are mainly used to specify the inference
   368 rules when defining a new logic.
   369 
   370 \indexbold{definitions} The {\bf definition part} is similar, but with
   371 the keyword \texttt{defs} instead of \texttt{rules}.  {\bf Definitions} are
   372 rules of the form $s \equiv t$, and should serve only as
   373 abbreviations.  The simplest form of a definition is $f \equiv t$,
   374 where $f$ is a constant.  Also allowed are $\eta$-equivalent forms of
   375 this, where the arguments of~$f$ appear applied on the left-hand side
   376 of the equation instead of abstracted on the right-hand side.
   377 
   378 Isabelle checks for common errors in definitions, such as extra
   379 variables on the right-hand side and cyclic dependencies, that could
   380 least to inconsistency.  It is still essential to take care:
   381 theorems proved on the basis of incorrect definitions are useless,
   382 your system can be consistent and yet still wrong.
   383 
   384 \index{examples!of theories} This example theory extends first-order
   385 logic by declaring and defining two constants, {\em nand} and {\em
   386   xor}:
   387 \begin{ttbox}
   388 Gate = FOL +
   389 consts  nand,xor :: [o,o] => o
   390 defs    nand_def "nand(P,Q) == ~(P & Q)"
   391         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   392 end
   393 \end{ttbox}
   394 
   395 Declaring and defining constants can be combined:
   396 \begin{ttbox}
   397 Gate = FOL +
   398 constdefs  nand :: [o,o] => o
   399            "nand(P,Q) == ~(P & Q)"
   400            xor  :: [o,o] => o
   401            "xor(P,Q)  == P & ~Q | ~P & Q"
   402 end
   403 \end{ttbox}
   404 \texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}
   405 automatically, which is why it is restricted to alphanumeric identifiers.  In
   406 general it has the form
   407 \begin{ttbox}
   408 constdefs  \(id@1\) :: \(\tau@1\)
   409            "\(id@1 \equiv \dots\)"
   410            \vdots
   411            \(id@n\) :: \(\tau@n\)
   412            "\(id@n \equiv \dots\)"
   413 \end{ttbox}
   414 
   415 
   416 \begin{warn}
   417 A common mistake when writing definitions is to introduce extra free variables
   418 on the right-hand side as in the following fictitious definition:
   419 \begin{ttbox}
   420 defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
   421 \end{ttbox}
   422 Isabelle rejects this ``definition'' because of the extra \texttt{m} on the
   423 right-hand side, which would introduce an inconsistency.  What you should have
   424 written is
   425 \begin{ttbox}
   426 defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
   427 \end{ttbox}
   428 \end{warn}
   429 
   430 \subsection{Declaring type constructors}
   431 \indexbold{types!declaring}\indexbold{arities!declaring}
   432 %
   433 Types are composed of type variables and {\bf type constructors}.  Each
   434 type constructor takes a fixed number of arguments.  They are declared
   435 with an \ML-like syntax.  If $list$ takes one type argument, $tree$ takes
   436 two arguments and $nat$ takes no arguments, then these type constructors
   437 can be declared by
   438 \begin{ttbox}
   439 types 'a list
   440       ('a,'b) tree
   441       nat
   442 \end{ttbox}
   443 
   444 The {\bf type declaration part} has the general form
   445 \begin{ttbox}
   446 types   \(tids@1\) \(id@1\)
   447         \vdots
   448         \(tids@n\) \(id@n\)
   449 \end{ttbox}
   450 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
   451 are type argument lists as shown in the example above.  It declares each
   452 $id@i$ as a type constructor with the specified number of argument places.
   453 
   454 The {\bf arity declaration part} has the form
   455 \begin{ttbox}
   456 arities \(tycon@1\) :: \(arity@1\)
   457         \vdots
   458         \(tycon@n\) :: \(arity@n\)
   459 \end{ttbox}
   460 where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
   461 $arity@n$ are arities.  Arity declarations add arities to existing
   462 types; they do not declare the types themselves.
   463 In the simplest case, for an 0-place type constructor, an arity is simply
   464 the type's class.  Let us declare a type~$bool$ of class $term$, with
   465 constants $tt$ and~$ff$.  (In first-order logic, booleans are
   466 distinct from formulae, which have type $o::logic$.)
   467 \index{examples!of theories}
   468 \begin{ttbox}
   469 Bool = FOL +
   470 types   bool
   471 arities bool    :: term
   472 consts  tt,ff   :: bool
   473 end
   474 \end{ttbox}
   475 A $k$-place type constructor may have arities of the form
   476 $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
   477 Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
   478 where $c@1$, \dots,~$c@m$ are classes.  Mostly we deal with singleton
   479 sorts, and may abbreviate them by dropping the braces.  The arity
   480 $(term)term$ is short for $(\{term\})term$.  Recall the discussion in
   481 \S\ref{polymorphic}.
   482 
   483 A type constructor may be overloaded (subject to certain conditions) by
   484 appearing in several arity declarations.  For instance, the function type
   485 constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
   486 logic, it is declared also to have arity $(term,term)term$.
   487 
   488 Theory \texttt{List} declares the 1-place type constructor $list$, gives
   489 it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with
   490 polymorphic types:%
   491 \footnote{In the \texttt{consts} part, type variable {\tt'a} has the default
   492   sort, which is \texttt{term}.  See the {\em Reference Manual\/}
   493 \iflabelundefined{sec:ref-defining-theories}{}%
   494 {(\S\ref{sec:ref-defining-theories})} for more information.}
   495 \index{examples!of theories}
   496 \begin{ttbox}
   497 List = FOL +
   498 types   'a list
   499 arities list    :: (term)term
   500 consts  Nil     :: 'a list
   501         Cons    :: ['a, 'a list] => 'a list
   502 end
   503 \end{ttbox}
   504 Multiple arity declarations may be abbreviated to a single line:
   505 \begin{ttbox}
   506 arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
   507 \end{ttbox}
   508 
   509 %\begin{warn}
   510 %Arity declarations resemble constant declarations, but there are {\it no\/}
   511 %quotation marks!  Types and rules must be quoted because the theory
   512 %translator passes them verbatim to the {\ML} output file.
   513 %\end{warn}
   514 
   515 \subsection{Type synonyms}\indexbold{type synonyms}
   516 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
   517 to those found in \ML.  Such synonyms are defined in the type declaration part
   518 and are fairly self explanatory:
   519 \begin{ttbox}
   520 types gate       = [o,o] => o
   521       'a pred    = 'a => o
   522       ('a,'b)nuf = 'b => 'a
   523 \end{ttbox}
   524 Type declarations and synonyms can be mixed arbitrarily:
   525 \begin{ttbox}
   526 types nat
   527       'a stream = nat => 'a
   528       signal    = nat stream
   529       'a list
   530 \end{ttbox}
   531 A synonym is merely an abbreviation for some existing type expression.
   532 Hence synonyms may not be recursive!  Internally all synonyms are
   533 fully expanded.  As a consequence Isabelle output never contains
   534 synonyms.  Their main purpose is to improve the readability of theory
   535 definitions.  Synonyms can be used just like any other type:
   536 \begin{ttbox}
   537 consts and,or :: gate
   538        negate :: signal => signal
   539 \end{ttbox}
   540 
   541 \subsection{Infix and mixfix operators}
   542 \index{infixes}\index{examples!of theories}
   543 
   544 Infix or mixfix syntax may be attached to constants.  Consider the
   545 following theory:
   546 \begin{ttbox}
   547 Gate2 = FOL +
   548 consts  "~&"     :: [o,o] => o         (infixl 35)
   549         "#"      :: [o,o] => o         (infixl 30)
   550 defs    nand_def "P ~& Q == ~(P & Q)"    
   551         xor_def  "P # Q  == P & ~Q | ~P & Q"
   552 end
   553 \end{ttbox}
   554 The constant declaration part declares two left-associating infix operators
   555 with their priorities, or precedences; they are $\nand$ of priority~35 and
   556 $\xor$ of priority~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
   557 \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the quotation
   558 marks in \verb|"~&"| and \verb|"#"|.
   559 
   560 The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
   561 automatically, just as in \ML.  Hence you may write propositions like
   562 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
   563 Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
   564 
   565 \medskip Infix syntax and constant names may be also specified
   566 independently.  For example, consider this version of $\nand$:
   567 \begin{ttbox}
   568 consts  nand     :: [o,o] => o         (infixl "~&" 35)
   569 \end{ttbox}
   570 
   571 \bigskip\index{mixfix declarations}
   572 {\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us
   573 add a line to the constant declaration part:
   574 \begin{ttbox}
   575         If :: [o,o,o] => o       ("if _ then _ else _")
   576 \end{ttbox}
   577 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
   578   if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}.  Underscores
   579 denote argument positions.  
   580 
   581 The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt
   582   else} construct to be printed split across several lines, even if it
   583 is too long to fit on one line.  Pretty-printing information can be
   584 added to specify the layout of mixfix operators.  For details, see
   585 \iflabelundefined{Defining-Logics}%
   586     {the {\it Reference Manual}, chapter `Defining Logics'}%
   587     {Chap.\ts\ref{Defining-Logics}}.
   588 
   589 Mixfix declarations can be annotated with priorities, just like
   590 infixes.  The example above is just a shorthand for
   591 \begin{ttbox}
   592         If :: [o,o,o] => o       ("if _ then _ else _" [0,0,0] 1000)
   593 \end{ttbox}
   594 The numeric components determine priorities.  The list of integers
   595 defines, for each argument position, the minimal priority an expression
   596 at that position must have.  The final integer is the priority of the
   597 construct itself.  In the example above, any argument expression is
   598 acceptable because priorities are non-negative, and conditionals may
   599 appear everywhere because 1000 is the highest priority.  On the other
   600 hand, the declaration
   601 \begin{ttbox}
   602         If :: [o,o,o] => o       ("if _ then _ else _" [100,0,0] 99)
   603 \end{ttbox}
   604 defines concrete syntax for a conditional whose first argument cannot have
   605 the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority
   606 of at least~100.  We may of course write
   607 \begin{quote}\tt
   608 if (if $P$ then $Q$ else $R$) then $S$ else $T$
   609 \end{quote}
   610 because expressions in parentheses have maximal priority.  
   611 
   612 Binary type constructors, like products and sums, may also be declared as
   613 infixes.  The type declaration below introduces a type constructor~$*$ with
   614 infix notation $\alpha*\beta$, together with the mixfix notation
   615 ${<}\_,\_{>}$ for pairs.  We also see a rule declaration part.
   616 \index{examples!of theories}\index{mixfix declarations}
   617 \begin{ttbox}
   618 Prod = FOL +
   619 types   ('a,'b) "*"                           (infixl 20)
   620 arities "*"     :: (term,term)term
   621 consts  fst     :: "'a * 'b => 'a"
   622         snd     :: "'a * 'b => 'b"
   623         Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
   624 rules   fst     "fst(<a,b>) = a"
   625         snd     "snd(<a,b>) = b"
   626 end
   627 \end{ttbox}
   628 
   629 \begin{warn}
   630   The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as
   631   it would be in the case of an infix constant.  Only infix type
   632   constructors can have symbolic names like~\texttt{*}.  General mixfix
   633   syntax for types may be introduced via appropriate \texttt{syntax}
   634   declarations.
   635 \end{warn}
   636 
   637 
   638 \subsection{Overloading}
   639 \index{overloading}\index{examples!of theories}
   640 The {\bf class declaration part} has the form
   641 \begin{ttbox}
   642 classes \(id@1\) < \(c@1\)
   643         \vdots
   644         \(id@n\) < \(c@n\)
   645 \end{ttbox}
   646 where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are
   647 existing classes.  It declares each $id@i$ as a new class, a subclass
   648 of~$c@i$.  In the general case, an identifier may be declared to be a
   649 subclass of $k$ existing classes:
   650 \begin{ttbox}
   651         \(id\) < \(c@1\), \ldots, \(c@k\)
   652 \end{ttbox}
   653 Type classes allow constants to be overloaded.  As suggested in
   654 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
   655 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
   656 \alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
   657 $term$ and add the three polymorphic constants of this class.
   658 \index{examples!of theories}\index{constants!overloaded}
   659 \begin{ttbox}
   660 Arith = FOL +
   661 classes arith < term
   662 consts  "0"     :: 'a::arith                  ("0")
   663         "1"     :: 'a::arith                  ("1")
   664         "+"     :: ['a::arith,'a] => 'a       (infixl 60)
   665 end
   666 \end{ttbox}
   667 No rules are declared for these constants: we merely introduce their
   668 names without specifying properties.  On the other hand, classes
   669 with rules make it possible to prove {\bf generic} theorems.  Such
   670 theorems hold for all instances, all types in that class.
   671 
   672 We can now obtain distinct versions of the constants of $arith$ by
   673 declaring certain types to be of class $arith$.  For example, let us
   674 declare the 0-place type constructors $bool$ and $nat$:
   675 \index{examples!of theories}
   676 \begin{ttbox}
   677 BoolNat = Arith +
   678 types   bool  nat
   679 arities bool, nat   :: arith
   680 consts  Suc         :: nat=>nat
   681 \ttbreak
   682 rules   add0        "0 + n = n::nat"
   683         addS        "Suc(m)+n = Suc(m+n)"
   684         nat1        "1 = Suc(0)"
   685         or0l        "0 + x = x::bool"
   686         or0r        "x + 0 = x::bool"
   687         or1l        "1 + x = 1::bool"
   688         or1r        "x + 1 = 1::bool"
   689 end
   690 \end{ttbox}
   691 Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
   692 either type.  The type constraints in the axioms are vital.  Without
   693 constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
   694 would have type $\alpha{::}arith$
   695 and the axiom would hold for any type of class $arith$.  This would
   696 collapse $nat$ to a trivial type:
   697 \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
   698 
   699 
   700 \section{Theory example: the natural numbers}
   701 
   702 We shall now work through a small example of formalized mathematics
   703 demonstrating many of the theory extension features.
   704 
   705 
   706 \subsection{Extending first-order logic with the natural numbers}
   707 \index{examples!of theories}
   708 
   709 Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
   710 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
   711 Let us introduce the Peano axioms for mathematical induction and the
   712 freeness of $0$ and~$Suc$:\index{axioms!Peano}
   713 \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
   714  \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
   715 \]
   716 \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
   717    \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
   718 \]
   719 Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
   720 provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
   721 Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
   722 To avoid making induction require the presence of other connectives, we
   723 formalize mathematical induction as
   724 $$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
   725 
   726 \noindent
   727 Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
   728 and~$\neg$, we take advantage of the meta-logic;\footnote
   729 {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
   730 and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
   731 better with Isabelle's simplifier.} 
   732 $(Suc\_neq\_0)$ is
   733 an elimination rule for $Suc(m)=0$:
   734 $$ Suc(m)=Suc(n) \Imp m=n  \eqno(Suc\_inject) $$
   735 $$ Suc(m)=0      \Imp R    \eqno(Suc\_neq\_0) $$
   736 
   737 \noindent
   738 We shall also define a primitive recursion operator, $rec$.  Traditionally,
   739 primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
   740 and obeys the equations
   741 \begin{eqnarray*}
   742   rec(0,a,f)            & = & a \\
   743   rec(Suc(m),a,f)       & = & f(m, rec(m,a,f))
   744 \end{eqnarray*}
   745 Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
   746 should satisfy
   747 \begin{eqnarray*}
   748   0+n      & = & n \\
   749   Suc(m)+n & = & Suc(m+n)
   750 \end{eqnarray*}
   751 Primitive recursion appears to pose difficulties: first-order logic has no
   752 function-valued expressions.  We again take advantage of the meta-logic,
   753 which does have functions.  We also generalise primitive recursion to be
   754 polymorphic over any type of class~$term$, and declare the addition
   755 function:
   756 \begin{eqnarray*}
   757   rec   & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
   758   +     & :: & [nat,nat]\To nat 
   759 \end{eqnarray*}
   760 
   761 
   762 \subsection{Declaring the theory to Isabelle}
   763 \index{examples!of theories}
   764 Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
   765 which contains only classical logic with no natural numbers.  We declare
   766 the 0-place type constructor $nat$ and the associated constants.  Note that
   767 the constant~0 requires a mixfix annotation because~0 is not a legal
   768 identifier, and could not otherwise be written in terms:
   769 \begin{ttbox}\index{mixfix declarations}
   770 Nat = FOL +
   771 types   nat
   772 arities nat         :: term
   773 consts  "0"         :: nat                              ("0")
   774         Suc         :: nat=>nat
   775         rec         :: [nat, 'a, [nat,'a]=>'a] => 'a
   776         "+"         :: [nat, nat] => nat                (infixl 60)
   777 rules   Suc_inject  "Suc(m)=Suc(n) ==> m=n"
   778         Suc_neq_0   "Suc(m)=0      ==> R"
   779         induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
   780         rec_0       "rec(0,a,f) = a"
   781         rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   782         add_def     "m+n == rec(m, n, \%x y. Suc(y))"
   783 end
   784 \end{ttbox}
   785 In axiom \texttt{add_def}, recall that \verb|%| stands for~$\lambda$.
   786 Loading this theory file creates the \ML\ structure \texttt{Nat}, which
   787 contains the theory and axioms.
   788 
   789 \subsection{Proving some recursion equations}
   790 Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the
   791 natural numbers.  As a trivial example, let us derive recursion equations
   792 for \verb$+$.  Here is the zero case:
   793 \begin{ttbox}
   794 Goalw [add_def] "0+n = n";
   795 {\out Level 0}
   796 {\out 0 + n = n}
   797 {\out  1. rec(0,n,\%x y. Suc(y)) = n}
   798 \ttbreak
   799 by (resolve_tac [rec_0] 1);
   800 {\out Level 1}
   801 {\out 0 + n = n}
   802 {\out No subgoals!}
   803 qed "add_0";
   804 \end{ttbox}
   805 And here is the successor case:
   806 \begin{ttbox}
   807 Goalw [add_def] "Suc(m)+n = Suc(m+n)";
   808 {\out Level 0}
   809 {\out Suc(m) + n = Suc(m + n)}
   810 {\out  1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
   811 \ttbreak
   812 by (resolve_tac [rec_Suc] 1);
   813 {\out Level 1}
   814 {\out Suc(m) + n = Suc(m + n)}
   815 {\out No subgoals!}
   816 qed "add_Suc";
   817 \end{ttbox}
   818 The induction rule raises some complications, which are discussed next.
   819 \index{theories!defining|)}
   820 
   821 
   822 \section{Refinement with explicit instantiation}
   823 \index{resolution!with instantiation}
   824 \index{instantiation|(}
   825 
   826 In order to employ mathematical induction, we need to refine a subgoal by
   827 the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
   828 which is highly ambiguous in higher-order unification.  It matches every
   829 way that a formula can be regarded as depending on a subterm of type~$nat$.
   830 To get round this problem, we could make the induction rule conclude
   831 $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
   832 refinement by~$(\forall E)$, which is equally hard!
   833 
   834 The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by
   835 a rule.  But it also accepts explicit instantiations for the rule's
   836 schematic variables.  
   837 \begin{description}
   838 \item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
   839 instantiates the rule {\it thm} with the instantiations {\it insts}, and
   840 then performs resolution on subgoal~$i$.
   841 
   842 \item[\ttindex{eres_inst_tac}] 
   843 and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
   844 and destruct-resolution, respectively.
   845 \end{description}
   846 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
   847 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
   848 with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
   849 expressions giving their instantiations.  The expressions are type-checked
   850 in the context of a particular subgoal: free variables receive the same
   851 types as they have in the subgoal, and parameters may appear.  Type
   852 variable instantiations may appear in~{\it insts}, but they are seldom
   853 required: \texttt{res_inst_tac} instantiates type variables automatically
   854 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
   855 
   856 \subsection{A simple proof by induction}
   857 \index{examples!of induction}
   858 Let us prove that no natural number~$k$ equals its own successor.  To
   859 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
   860 instantiation for~$\Var{P}$.
   861 \begin{ttbox}
   862 Goal "~ (Suc(k) = k)";
   863 {\out Level 0}
   864 {\out Suc(k) ~= k}
   865 {\out  1. Suc(k) ~= k}
   866 \ttbreak
   867 by (res_inst_tac [("n","k")] induct 1);
   868 {\out Level 1}
   869 {\out Suc(k) ~= k}
   870 {\out  1. Suc(0) ~= 0}
   871 {\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   872 \end{ttbox}
   873 We should check that Isabelle has correctly applied induction.  Subgoal~1
   874 is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
   875 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
   876 The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
   877 other rules of theory \texttt{Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
   878 \begin{ttbox}
   879 by (resolve_tac [notI] 1);
   880 {\out Level 2}
   881 {\out Suc(k) ~= k}
   882 {\out  1. Suc(0) = 0 ==> False}
   883 {\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   884 \ttbreak
   885 by (eresolve_tac [Suc_neq_0] 1);
   886 {\out Level 3}
   887 {\out Suc(k) ~= k}
   888 {\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
   889 \end{ttbox}
   890 The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
   891 Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
   892 $Suc(Suc(x)) = Suc(x)$:
   893 \begin{ttbox}
   894 by (resolve_tac [notI] 1);
   895 {\out Level 4}
   896 {\out Suc(k) ~= k}
   897 {\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
   898 \ttbreak
   899 by (eresolve_tac [notE] 1);
   900 {\out Level 5}
   901 {\out Suc(k) ~= k}
   902 {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
   903 \ttbreak
   904 by (eresolve_tac [Suc_inject] 1);
   905 {\out Level 6}
   906 {\out Suc(k) ~= k}
   907 {\out No subgoals!}
   908 \end{ttbox}
   909 
   910 
   911 \subsection{An example of ambiguity in \texttt{resolve_tac}}
   912 \index{examples!of induction}\index{unification!higher-order}
   913 If you try the example above, you may observe that \texttt{res_inst_tac} is
   914 not actually needed.  Almost by chance, \ttindex{resolve_tac} finds the right
   915 instantiation for~$(induct)$ to yield the desired next state.  With more
   916 complex formulae, our luck fails.  
   917 \begin{ttbox}
   918 Goal "(k+m)+n = k+(m+n)";
   919 {\out Level 0}
   920 {\out k + m + n = k + (m + n)}
   921 {\out  1. k + m + n = k + (m + n)}
   922 \ttbreak
   923 by (resolve_tac [induct] 1);
   924 {\out Level 1}
   925 {\out k + m + n = k + (m + n)}
   926 {\out  1. k + m + n = 0}
   927 {\out  2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
   928 \end{ttbox}
   929 This proof requires induction on~$k$.  The occurrence of~0 in subgoal~1
   930 indicates that induction has been applied to the term~$k+(m+n)$; this
   931 application is sound but will not lead to a proof here.  Fortunately,
   932 Isabelle can (lazily!) generate all the valid applications of induction.
   933 The \ttindex{back} command causes backtracking to an alternative outcome of
   934 the tactic.
   935 \begin{ttbox}
   936 back();
   937 {\out Level 1}
   938 {\out k + m + n = k + (m + n)}
   939 {\out  1. k + m + n = k + 0}
   940 {\out  2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
   941 \end{ttbox}
   942 Now induction has been applied to~$m+n$.  This is equally useless.  Let us
   943 call \ttindex{back} again.
   944 \begin{ttbox}
   945 back();
   946 {\out Level 1}
   947 {\out k + m + n = k + (m + n)}
   948 {\out  1. k + m + 0 = k + (m + 0)}
   949 {\out  2. !!x. k + m + x = k + (m + x) ==>}
   950 {\out          k + m + Suc(x) = k + (m + Suc(x))}
   951 \end{ttbox}
   952 Now induction has been applied to~$n$.  What is the next alternative?
   953 \begin{ttbox}
   954 back();
   955 {\out Level 1}
   956 {\out k + m + n = k + (m + n)}
   957 {\out  1. k + m + n = k + (m + 0)}
   958 {\out  2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
   959 \end{ttbox}
   960 Inspecting subgoal~1 reveals that induction has been applied to just the
   961 second occurrence of~$n$.  This perfectly legitimate induction is useless
   962 here.  
   963 
   964 The main goal admits fourteen different applications of induction.  The
   965 number is exponential in the size of the formula.
   966 
   967 \subsection{Proving that addition is associative}
   968 Let us invoke the induction rule properly, using~{\tt
   969   res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
   970 simplification tactics, which are described in 
   971 \iflabelundefined{simp-chap}%
   972     {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
   973 
   974 \index{simplification}\index{examples!of simplification} 
   975 
   976 Isabelle's simplification tactics repeatedly apply equations to a subgoal,
   977 perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
   978 {\bf simplification set},\index{simplification sets} or {\bf simpset}.  We
   979 augment the implicit simpset of FOL with the equations proved in the previous
   980 section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
   981 \begin{ttbox}
   982 Addsimps [add_0, add_Suc];
   983 \end{ttbox}
   984 We state the goal for associativity of addition, and
   985 use \ttindex{res_inst_tac} to invoke induction on~$k$:
   986 \begin{ttbox}
   987 Goal "(k+m)+n = k+(m+n)";
   988 {\out Level 0}
   989 {\out k + m + n = k + (m + n)}
   990 {\out  1. k + m + n = k + (m + n)}
   991 \ttbreak
   992 by (res_inst_tac [("n","k")] induct 1);
   993 {\out Level 1}
   994 {\out k + m + n = k + (m + n)}
   995 {\out  1. 0 + m + n = 0 + (m + n)}
   996 {\out  2. !!x. x + m + n = x + (m + n) ==>}
   997 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
   998 \end{ttbox}
   999 The base case holds easily; both sides reduce to $m+n$.  The
  1000 tactic~\ttindex{Simp_tac} rewrites with respect to the current
  1001 simplification set, applying the rewrite rules for addition:
  1002 \begin{ttbox}
  1003 by (Simp_tac 1);
  1004 {\out Level 2}
  1005 {\out k + m + n = k + (m + n)}
  1006 {\out  1. !!x. x + m + n = x + (m + n) ==>}
  1007 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
  1008 \end{ttbox}
  1009 The inductive step requires rewriting by the equations for addition
  1010 and with the induction hypothesis, which is also an equation.  The
  1011 tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
  1012 simplification set and any useful assumptions:
  1013 \begin{ttbox}
  1014 by (Asm_simp_tac 1);
  1015 {\out Level 3}
  1016 {\out k + m + n = k + (m + n)}
  1017 {\out No subgoals!}
  1018 \end{ttbox}
  1019 \index{instantiation|)}
  1020 
  1021 
  1022 \section{A Prolog interpreter}
  1023 \index{Prolog interpreter|bold}
  1024 To demonstrate the power of tacticals, let us construct a Prolog
  1025 interpreter and execute programs involving lists.\footnote{To run these
  1026 examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program
  1027 consists of a theory.  We declare a type constructor for lists, with an
  1028 arity declaration to say that $(\tau)list$ is of class~$term$
  1029 provided~$\tau$ is:
  1030 \begin{eqnarray*}
  1031   list  & :: & (term)term
  1032 \end{eqnarray*}
  1033 We declare four constants: the empty list~$Nil$; the infix list
  1034 constructor~{:}; the list concatenation predicate~$app$; the list reverse
  1035 predicate~$rev$.  (In Prolog, functions on lists are expressed as
  1036 predicates.)
  1037 \begin{eqnarray*}
  1038     Nil         & :: & \alpha list \\
  1039     {:}         & :: & [\alpha,\alpha list] \To \alpha list \\
  1040     app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
  1041     rev & :: & [\alpha list,\alpha list] \To o 
  1042 \end{eqnarray*}
  1043 The predicate $app$ should satisfy the Prolog-style rules
  1044 \[ {app(Nil,ys,ys)} \qquad
  1045    {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
  1046 We define the naive version of $rev$, which calls~$app$:
  1047 \[ {rev(Nil,Nil)} \qquad
  1048    {rev(xs,ys)\quad  app(ys, x:Nil, zs) \over
  1049     rev(x:xs, zs)} 
  1050 \]
  1051 
  1052 \index{examples!of theories}
  1053 Theory \thydx{Prolog} extends first-order logic in order to make use
  1054 of the class~$term$ and the type~$o$.  The interpreter does not use the
  1055 rules of~\texttt{FOL}.
  1056 \begin{ttbox}
  1057 Prolog = FOL +
  1058 types   'a list
  1059 arities list    :: (term)term
  1060 consts  Nil     :: 'a list
  1061         ":"     :: ['a, 'a list]=> 'a list            (infixr 60)
  1062         app     :: ['a list, 'a list, 'a list] => o
  1063         rev     :: ['a list, 'a list] => o
  1064 rules   appNil  "app(Nil,ys,ys)"
  1065         appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
  1066         revNil  "rev(Nil,Nil)"
  1067         revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
  1068 end
  1069 \end{ttbox}
  1070 \subsection{Simple executions}
  1071 Repeated application of the rules solves Prolog goals.  Let us
  1072 append the lists $[a,b,c]$ and~$[d,e]$.  As the rules are applied, the
  1073 answer builds up in~\texttt{?x}.
  1074 \begin{ttbox}
  1075 Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
  1076 {\out Level 0}
  1077 {\out app(a : b : c : Nil, d : e : Nil, ?x)}
  1078 {\out  1. app(a : b : c : Nil, d : e : Nil, ?x)}
  1079 \ttbreak
  1080 by (resolve_tac [appNil,appCons] 1);
  1081 {\out Level 1}
  1082 {\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
  1083 {\out  1. app(b : c : Nil, d : e : Nil, ?zs1)}
  1084 \ttbreak
  1085 by (resolve_tac [appNil,appCons] 1);
  1086 {\out Level 2}
  1087 {\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
  1088 {\out  1. app(c : Nil, d : e : Nil, ?zs2)}
  1089 \end{ttbox}
  1090 At this point, the first two elements of the result are~$a$ and~$b$.
  1091 \begin{ttbox}
  1092 by (resolve_tac [appNil,appCons] 1);
  1093 {\out Level 3}
  1094 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
  1095 {\out  1. app(Nil, d : e : Nil, ?zs3)}
  1096 \ttbreak
  1097 by (resolve_tac [appNil,appCons] 1);
  1098 {\out Level 4}
  1099 {\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
  1100 {\out No subgoals!}
  1101 \end{ttbox}
  1102 
  1103 Prolog can run functions backwards.  Which list can be appended
  1104 with $[c,d]$ to produce $[a,b,c,d]$?
  1105 Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
  1106 \begin{ttbox}
  1107 Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
  1108 {\out Level 0}
  1109 {\out app(?x, c : d : Nil, a : b : c : d : Nil)}
  1110 {\out  1. app(?x, c : d : Nil, a : b : c : d : Nil)}
  1111 \ttbreak
  1112 by (REPEAT (resolve_tac [appNil,appCons] 1));
  1113 {\out Level 1}
  1114 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
  1115 {\out No subgoals!}
  1116 \end{ttbox}
  1117 
  1118 
  1119 \subsection{Backtracking}\index{backtracking!Prolog style}
  1120 Prolog backtracking can answer questions that have multiple solutions.
  1121 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?  This
  1122 question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
  1123 quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
  1124 \begin{ttbox}
  1125 Goal "app(?x, ?y, a:b:c:d:Nil)";
  1126 {\out Level 0}
  1127 {\out app(?x, ?y, a : b : c : d : Nil)}
  1128 {\out  1. app(?x, ?y, a : b : c : d : Nil)}
  1129 \ttbreak
  1130 by (REPEAT (resolve_tac [appNil,appCons] 1));
  1131 {\out Level 1}
  1132 {\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
  1133 {\out No subgoals!}
  1134 \end{ttbox}
  1135 Isabelle can lazily generate all the possibilities.  The \ttindex{back}
  1136 command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
  1137 \begin{ttbox}
  1138 back();
  1139 {\out Level 1}
  1140 {\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
  1141 {\out No subgoals!}
  1142 \end{ttbox}
  1143 The other solutions are generated similarly.
  1144 \begin{ttbox}
  1145 back();
  1146 {\out Level 1}
  1147 {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
  1148 {\out No subgoals!}
  1149 \ttbreak
  1150 back();
  1151 {\out Level 1}
  1152 {\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
  1153 {\out No subgoals!}
  1154 \ttbreak
  1155 back();
  1156 {\out Level 1}
  1157 {\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
  1158 {\out No subgoals!}
  1159 \end{ttbox}
  1160 
  1161 
  1162 \subsection{Depth-first search}
  1163 \index{search!depth-first}
  1164 Now let us try $rev$, reversing a list.
  1165 Bundle the rules together as the \ML{} identifier \texttt{rules}.  Naive
  1166 reverse requires 120 inferences for this 14-element list, but the tactic
  1167 terminates in a few seconds.
  1168 \begin{ttbox}
  1169 Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
  1170 {\out Level 0}
  1171 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
  1172 {\out  1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
  1173 {\out         ?w)}
  1174 \ttbreak
  1175 val rules = [appNil,appCons,revNil,revCons];
  1176 \ttbreak
  1177 by (REPEAT (resolve_tac rules 1));
  1178 {\out Level 1}
  1179 {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
  1180 {\out     n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
  1181 {\out No subgoals!}
  1182 \end{ttbox}
  1183 We may execute $rev$ backwards.  This, too, should reverse a list.  What
  1184 is the reverse of $[a,b,c]$?
  1185 \begin{ttbox}
  1186 Goal "rev(?x, a:b:c:Nil)";
  1187 {\out Level 0}
  1188 {\out rev(?x, a : b : c : Nil)}
  1189 {\out  1. rev(?x, a : b : c : Nil)}
  1190 \ttbreak
  1191 by (REPEAT (resolve_tac rules 1));
  1192 {\out Level 1}
  1193 {\out rev(?x1 : Nil, a : b : c : Nil)}
  1194 {\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
  1195 \end{ttbox}
  1196 The tactic has failed to find a solution!  It reached a dead end at
  1197 subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
  1198 equals~$[a,b,c]$.  Backtracking explores other outcomes.
  1199 \begin{ttbox}
  1200 back();
  1201 {\out Level 1}
  1202 {\out rev(?x1 : a : Nil, a : b : c : Nil)}
  1203 {\out  1. app(Nil, ?x1 : Nil, b : c : Nil)}
  1204 \end{ttbox}
  1205 This too is a dead end, but the next outcome is successful.
  1206 \begin{ttbox}
  1207 back();
  1208 {\out Level 1}
  1209 {\out rev(c : b : a : Nil, a : b : c : Nil)}
  1210 {\out No subgoals!}
  1211 \end{ttbox}
  1212 \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
  1213 search tactical.  \texttt{REPEAT} stops when it cannot continue, regardless of
  1214 which state is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a
  1215 satisfactory state, as specified by an \ML{} predicate.  Below,
  1216 \ttindex{has_fewer_prems} specifies that the proof state should have no
  1217 subgoals.
  1218 \begin{ttbox}
  1219 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 
  1220                              (resolve_tac rules 1);
  1221 \end{ttbox}
  1222 Since Prolog uses depth-first search, this tactic is a (slow!) 
  1223 Prolog interpreter.  We return to the start of the proof using
  1224 \ttindex{choplev}, and apply \texttt{prolog_tac}:
  1225 \begin{ttbox}
  1226 choplev 0;
  1227 {\out Level 0}
  1228 {\out rev(?x, a : b : c : Nil)}
  1229 {\out  1. rev(?x, a : b : c : Nil)}
  1230 \ttbreak
  1231 by prolog_tac;
  1232 {\out Level 1}
  1233 {\out rev(c : b : a : Nil, a : b : c : Nil)}
  1234 {\out No subgoals!}
  1235 \end{ttbox}
  1236 Let us try \texttt{prolog_tac} on one more example, containing four unknowns:
  1237 \begin{ttbox}
  1238 Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
  1239 {\out Level 0}
  1240 {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
  1241 {\out  1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
  1242 \ttbreak
  1243 by prolog_tac;
  1244 {\out Level 1}
  1245 {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
  1246 {\out No subgoals!}
  1247 \end{ttbox}
  1248 Although Isabelle is much slower than a Prolog system, Isabelle
  1249 tactics can exploit logic programming techniques.  
  1250