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
`