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