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