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