summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/getting.tex

changeset 105 | 216d6ed87399 |

child 296 | e1f6cd9f682e |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Intro/getting.tex Wed Nov 10 05:06:55 1993 +0100 @@ -0,0 +1,896 @@ +%% $Id$ +\part{Getting started with Isabelle} +This Part describes how to perform simple proofs using Isabelle. Although +it frequently refers to concepts from the previous Part, a user can get +started without understanding them in detail. + +As of this writing, Isabelle's user interface is \ML. Proofs are conducted +by applying certain \ML{} functions, which update a stored proof state. +Logics are combined and extended by calling \ML{} functions. All syntax +must be expressed using {\sc ascii} characters. Menu-driven graphical +interfaces are under construction, but Isabelle users will always need to +know some \ML, at least to use tacticals. + +Object-logics are built upon Pure Isabelle, which implements the meta-logic +and provides certain fundamental data structures: types, terms, signatures, +theorems and theories, tactics and tacticals. These data structures have +the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm}, +{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt +tactic->tactic}. Isabelle users can operate on these data structures by +writing \ML{} programs. + +\section{Forward proof} +\index{Isabelle!getting started}\index{ML} +This section describes the concrete syntax for types, terms and theorems, +and demonstrates forward proof. + +\subsection{Lexical matters} +\index{identifiers|bold}\index{reserved words|bold} +An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|) +and single quotes~({\tt'}), beginning with a letter. Single quotes are +regarded as primes; for instance {\tt x'} is read as~$x'$. Identifiers are +separated by white space and special characters. {\bf Reserved words} are +identifiers that appear in Isabelle syntax definitions. + +An Isabelle theory can declare symbols composed of special characters, such +as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}. (The latter three are part of +the syntax of the meta-logic.) Such symbols may be run together; thus if +\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is +valid notation for a set of sets --- but only if \verb|}}| and \verb|{{| +have not been declared as symbols! The parser resolves any ambiguity by +taking the longest possible symbol that has been declared. Thus the string +{\tt==>} is read as a single symbol. But \hbox{\tt= =>} is read as two +symbols, as is \verb|}}|, as discussed above. + +Identifiers that are not reserved words may serve as free variables or +constants. A type identifier consists of an identifier prefixed by a +prime, for example {\tt'a} and \hbox{\tt'hello}. An unknown (or type +unknown) consists of a question mark, an identifier (or type identifier), +and a subscript. The subscript, a non-negative integer, allows the +renaming of unknowns prior to unification. + +The subscript may appear after the identifier, separated by a dot; this +prevents ambiguity when the identifier ends with a digit. Thus {\tt?z6.0} +has identifier \verb|"z6"| and subscript~0, while {\tt?a0.5} has identifier +\verb|"a0"| and subscript~5. If the identifier does not end with a digit, +then no dot appears and a subscript of~0 is omitted; for example, +{\tt?hello} has identifier \verb|"hello"| and subscript zero, while +{\tt?z6} has identifier \verb|"z"| and subscript~6. The same conventions +apply to type unknowns. Note that the question mark is {\bf not} part of the +identifier! + + +\subsection{Syntax of types and terms} +\index{Isabelle!syntax of} +\index{classes!built-in|bold} +Classes are denoted by identifiers; the built-in class \ttindex{logic} +contains the `logical' types. Sorts are lists of classes enclosed in +braces~\{ and \}; singleton sorts may be abbreviated by dropping the braces. + +\index{types!syntax|bold} +Types are written with a syntax like \ML's. The built-in type \ttindex{prop} +is the type of propositions. Type variables can be constrained to particular +classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}. +\[\dquotes +\begin{array}{lll} + \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline + t "::" C & t :: C & \hbox{class constraint} \\ + t "::" "\{" C@1 "," \ldots "," C@n "\}" & + t :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ + \sigma"=>"\tau & \sigma\To\tau & \hbox{function type} \\ + "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & + [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\ + "(" \tau@1"," \ldots "," \tau@n ")" tycon & + (\tau@1, \ldots, \tau@n)tycon & \hbox{type construction} +\end{array} +\] +Terms are those of the typed $\lambda$-calculus. +\index{terms!syntax|bold} +\[\dquotes +\begin{array}{lll} + \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline + t "::" \sigma & t :: \sigma & \hbox{type constraint} \\ + "\%" x "." t & \lambda x.t & \hbox{abstraction} \\ + "\%" x@1\ldots x@n "." t & \lambda x@1\ldots x@n.t & + \hbox{curried abstraction} \\ + t "(" u@1"," \ldots "," u@n ")" & + t (u@1, \ldots, u@n) & \hbox{curried application} +\end{array} +\] +The theorems and rules of an object-logic are represented by theorems in +the meta-logic, which are expressed using meta-formulae. Since the +meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{} +are just terms of type~\ttindex{prop}. +\index{meta-formulae!syntax|bold} +\[\dquotes + \begin{array}{l@{\quad}l@{\quad}l} + \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline + a " == " b & a\equiv b & \hbox{meta-equality} \\ + a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\ + \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\ + "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & + \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ + "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ + "!!" x@1\ldots x@n "." \phi & + \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification} + \end{array} +\] +Flex-flex constraints are meta-equalities arising from unification; they +require special treatment. See~\S\ref{flexflex}. +\index{flex-flex equations} + +Most logics define the implicit coercion $Trueprop$ from object-formulae to +propositions. +\index{Trueprop@{$Trueprop$}} +This could cause an ambiguity: in $P\Imp Q$, do the variables $P$ and $Q$ +stand for meta-formulae or object-formulae? If the latter, $P\Imp Q$ +really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To prevent such +ambiguities, Isabelle's syntax does not allow a meta-formula to consist of +a variable. Variables of type~\ttindex{prop} are seldom useful, but you +can make a variable stand for a meta-formula by prefixing it with the +keyword \ttindex{PROP}: +\begin{ttbox} +PROP ?psi ==> PROP ?theta +\end{ttbox} + +Symbols of object-logics also must be rendered into {\sc ascii}, typically +as follows: +\[ \begin{tabular}{l@{\quad}l@{\quad}l} + \tt True & $\top$ & true \\ + \tt False & $\bot$ & false \\ + \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\ + \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\ + \verb'~' $P$ & $\neg P$ & negation \\ + \tt $P$ --> $Q$ & $P\imp Q$ & implication \\ + \tt $P$ <-> $Q$ & $P\bimp Q$ & bi-implication \\ + \tt ALL $x\,y\,z$ .\ $P$ & $\forall x\,y\,z.P$ & for all \\ + \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists + \end{tabular} +\] +To illustrate the notation, consider two axioms for first-order logic: +$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ +$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ +Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates literally into +{\sc ascii} characters as +\begin{ttbox} +[| ?P; ?Q |] ==> ?P & ?Q +\end{ttbox} +The schematic variables let unification instantiate the rule. To +avoid cluttering rules with question marks, Isabelle converts any free +variables in a rule to schematic variables; we normally write $({\conj}I)$ as +\begin{ttbox} +[| P; Q |] ==> P & Q +\end{ttbox} +This variables convention agrees with the treatment of variables in goals. +Free variables in a goal remain fixed throughout the proof. After the +proof is finished, Isabelle converts them to scheme variables in the +resulting theorem. Scheme variables in a goal may be replaced by terms +during the proof, supporting answer extraction, program synthesis, and so +forth. + +For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as +\begin{ttbox} +[| EX x.P(x); !!x. P(x) ==> Q |] ==> Q +\end{ttbox} + + +\subsection{Basic operations on theorems} +\index{theorems!basic operations on|bold} +\index{LCF} +Meta-level theorems have type \ttindex{thm} and represent the theorems and +inference rules of object-logics. Isabelle's meta-logic is implemented +using the {\sc lcf} approach: each meta-level inference rule is represented by +a function from theorems to theorems. Object-level rules are taken as +axioms. + +The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt + prthq}. Of the other operations on theorems, most useful are {\tt RS} +and {\tt RSN}, which perform resolution. + +\index{printing commands|bold} +\begin{description} +\item[\ttindexbold{prth} {\it thm}] pretty-prints {\it thm\/} at the terminal. + +\item[\ttindexbold{prths} {\it thms}] pretty-prints {\it thms}, a list of +theorems. + +\item[\ttindexbold{prthq} {\it thmq}] pretty-prints {\it thmq}, a sequence of +theorems; this is useful for inspecting the output of a tactic. + +\item[\tt$thm1$ RS $thm2$] \indexbold{*RS} resolves the conclusion of $thm1$ +with the first premise of~$thm2$. + +\item[\tt$thm1$ RSN $(i,thm2)$] \indexbold{*RSN} resolves the conclusion of $thm1$ +with the $i$th premise of~$thm2$. + +\item[\ttindexbold{standard} $thm$] puts $thm$ into a standard +format. It also renames schematic variables to have subscript zero, +improving readability and reducing subscript growth. +\end{description} +\index{ML} +The rules of a theory are normally bound to \ML\ identifiers. Suppose we +are running an Isabelle session containing natural deduction first-order +logic. Let us try an example given in~\S\ref{joining}. We first print +\ttindex{mp}, which is the rule~$({\imp}E)$, then resolve it with itself. +\begin{ttbox} +prth mp; +{\out [| ?P --> ?Q; ?P |] ==> ?Q} +{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm} +prth (mp RS mp); +{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} +{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} +\end{ttbox} +In the Isabelle documentation, user's input appears in {\tt typewriter + characters}, and output appears in {\sltt slanted typewriter characters}. +\ML's response {\out val }~\ldots{} is compiler-dependent and will +sometimes be suppressed. This session illustrates two formats for the +display of theorems. Isabelle's top-level displays theorems as ML values, +enclosed in quotes.\footnote{This works under both Poly/ML and Standard ML + of New Jersey.} Printing functions like {\tt prth} omit the quotes and +the surrounding {\tt val \ldots :\ thm}. + +To contrast {\tt RS} with {\tt RSN}, we resolve +\ttindex{conjunct1}, which stands for~$(\conj E1)$, with~\ttindex{mp}. +\begin{ttbox} +conjunct1 RS mp; +{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm} +conjunct1 RSN (2,mp); +{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm} +\end{ttbox} +These correspond to the following proofs: +\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P} + \qquad + \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} +\] +The printing commands return their argument; the \ML{} identifier~{\tt it} +denotes the value just printed. You may derive a rule by pasting other +rules together. Below, \ttindex{spec} stands for~$(\forall E)$: +\begin{ttbox} +spec; +{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm} +it RS mp; +{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)" : thm} +it RS conjunct1; +{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)"} +standard it; +{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)"} +\end{ttbox} +By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have +derived a destruction rule for formulae of the form $\forall x. +P(x)\imp(Q(x)\conj R(x))$. Used with destruct-resolution, such specialized +rules provide a way of referring to particular assumptions. + +\subsection{Flex-flex equations} \label{flexflex} +\index{flex-flex equations|bold}\index{unknowns!of function type} +In higher-order unification, {\bf flex-flex} equations are those where both +sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$. +They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and +$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown. They +admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$ +and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$. Huet's +procedure does not enumerate the unifiers; instead, it retains flex-flex +equations as constraints on future unifications. Flex-flex constraints +occasionally become attached to a proof state; more frequently, they appear +during use of {\tt RS} and~{\tt RSN}: +\begin{ttbox} +refl; +{\out val it = "?a = ?a" : thm} +exI; +{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm} +refl RS exI; +{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm} +\end{ttbox} + +\noindent +Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with +the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$. Instances +satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and +$\exists x.x=\Var{u}$. Calling \ttindex{flexflex_rule} removes all +constraints by applying the trivial unifier:\index{*prthq} +\begin{ttbox} +prthq (flexflex_rule it); +{\out EX x. ?a4 = ?a4} +\end{ttbox} +Isabelle simplifies flex-flex equations to eliminate redundant bound +variables. In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$, +there is no bound occurrence of~$x$ on the right side; thus, there will be +none on the left, in a common instance of these terms. Choosing a new +variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$, +simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$ +from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda +y.\Var{g}(y)$. By $\eta$-conversion, this simplifies to the assignment +$\Var{g}\equiv\lambda y.?h(k(y))$. + +\begin{warn} +\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless +the resolution delivers {\bf exactly one} resolvent. For multiple results, +use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The +following example uses \ttindex{read_instantiate} to create an instance +of \ttindex{refl} containing no schematic variables. +\begin{ttbox} +val reflk = read_instantiate [("a","k")] refl; +{\out val reflk = "k = k" : thm} +\end{ttbox} + +\noindent +A flex-flex constraint is no longer possible; resolution does not find a +unique unifier: +\begin{ttbox} +reflk RS exI; +{\out uncaught exception THM} +\end{ttbox} +Using \ttindex{RL} this time, we discover that there are four unifiers, and +four resolvents: +\begin{ttbox} +[reflk] RL [exI]; +{\out val it = ["EX x. x = x", "EX x. k = x",} +{\out "EX x. x = k", "EX x. k = k"] : thm list} +\end{ttbox} +\end{warn} + + +\section{Backward proof} +Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning, +large proofs require tactics. Isabelle provides a suite of commands for +conducting a backward proof using tactics. + +\subsection{The basic tactics} +\index{tactics!basic|bold} +The tactics {\tt assume_tac}, {\tt +resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most +single-step proofs. Although {\tt eresolve_tac} and {\tt dresolve_tac} are +not strictly necessary, they simplify proofs involving elimination and +destruction rules. All the tactics act on a subgoal designated by a +positive integer~$i$, failing if~$i$ is out of range. The resolution +tactics try their list of theorems in left-to-right order. + +\begin{description} +\item[\ttindexbold{assume_tac} {\it i}] is the tactic that attempts to solve +subgoal~$i$ by assumption. Proof by assumption is not a trivial step; it +can falsify other subgoals by instantiating shared variables. There may be +several ways of solving the subgoal by assumption. + +\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] +is the basic resolution tactic, used for most proof steps. The $thms$ +represent object-rules, which are resolved against subgoal~$i$ of the proof +state. For each rule, resolution forms next states by unifying the +conclusion with the subgoal and inserting instantiated premises in its +place. A rule can admit many higher-order unifiers. The tactic fails if +none of the rules generates next states. + +\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] +performs elim-resolution. Like +\hbox{\tt resolve_tac {\it thms} {\it i}} followed by \hbox{\tt assume_tac +{\it i}}, it applies a rule then solves its first premise by assumption. +But {\tt eresolve_tac} additionally deletes that assumption from any +subgoals arising from the resolution. + + +\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] +performs destruct-resolution with the~$thms$, as described +in~\S\ref{destruct}. It is useful for forward reasoning from the +assumptions. +\end{description} + +\subsection{Commands for backward proof} +\index{proof!commands for|bold} +Tactics are normally applied using the subgoal module, which maintains a +proof state and manages the proof construction. It allows interactive +backtracking through the proof space, going away to prove lemmas, etc.; of +its many commands, most important are the following: +\begin{description} +\item[\ttindexbold{goal} {\it theory} {\it formula}; ] +begins a new proof, where $theory$ is usually an \ML\ identifier +and the {\it formula\/} is written as an \ML\ string. + +\item[\ttindexbold{by} {\it tactic}; ] +applies the {\it tactic\/} to the current proof +state, raising an exception if the tactic fails. + +\item[\ttindexbold{undo}(); ] +reverts to the previous proof state. Undo can be repeated but cannot be +undone. Do not omit the parentheses; typing {\tt undo;} merely causes \ML\ +to echo the value of that function. + +\item[\ttindexbold{result}()] +returns the theorem just proved, in a standard format. It fails if +unproved subgoals are left or if the main goal does not match the one you +started with. +\end{description} +The commands and tactics given above are cumbersome for interactive use. +Although our examples will use the full commands, you may prefer Isabelle's +shortcuts: +\begin{center} \tt +\indexbold{*br} \indexbold{*be} \indexbold{*bd} \indexbold{*ba} +\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l} + ba {\it i}; & by (assume_tac {\it i}); \\ + + br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\ + + be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\ + + bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); +\end{tabular} +\end{center} + +\subsection{A trivial example in propositional logic} +\index{examples!propositional} +Directory {\tt FOL} of the Isabelle distribution defines the \ML\ +identifier~\ttindex{FOL.thy}, which denotes the theory of first-order +logic. Let us try the example from~\S\ref{prop-proof}, entering the goal +$P\disj P\imp P$ in that theory.\footnote{To run these examples, see the +file {\tt FOL/ex/intro.ML}.} +\begin{ttbox} +goal FOL.thy "P|P --> P"; +{\out Level 0} +{\out P | P --> P} +{\out 1. P | P --> P} +\end{ttbox} +Isabelle responds by printing the initial proof state, which has $P\disj +P\imp P$ as the main goal and the only subgoal. The \bfindex{level} of the +state is the number of {\tt by} commands that have been applied to reach +it. We now use \ttindex{resolve_tac} to apply the rule \ttindex{impI}, +or~$({\imp}I)$, to subgoal~1: +\begin{ttbox} +by (resolve_tac [impI] 1); +{\out Level 1} +{\out P | P --> P} +{\out 1. P | P ==> P} +\end{ttbox} +In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$. +(The meta-implication {\tt==>} indicates assumptions.) We apply +\ttindex{disjE}, or~(${\disj}E)$, to that subgoal: +\begin{ttbox} +by (resolve_tac [disjE] 1); +{\out Level 2} +{\out P | P --> P} +{\out 1. P | P ==> ?P1 | ?Q1} +{\out 2. [| P | P; ?P1 |] ==> P} +{\out 3. [| P | P; ?Q1 |] ==> P} +\end{ttbox} +At Level~2 there are three subgoals, each provable by +assumption. We deviate from~\S\ref{prop-proof} by tackling subgoal~3 +first, using \ttindex{assume_tac}. This updates {\tt?Q1} to~{\tt P}. +\begin{ttbox} +by (assume_tac 3); +{\out Level 3} +{\out P | P --> P} +{\out 1. P | P ==> ?P1 | P} +{\out 2. [| P | P; ?P1 |] ==> P} +\end{ttbox} +Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P}. +\begin{ttbox} +by (assume_tac 2); +{\out Level 4} +{\out P | P --> P} +{\out 1. P | P ==> P | P} +\end{ttbox} +Lastly we prove the remaining subgoal by assumption: +\begin{ttbox} +by (assume_tac 1); +{\out Level 5} +{\out P | P --> P} +{\out No subgoals!} +\end{ttbox} +Isabelle tells us that there are no longer any subgoals: the proof is +complete. Calling \ttindex{result} returns the theorem. +\begin{ttbox} +val mythm = result(); +{\out val mythm = "?P | ?P --> ?P" : thm} +\end{ttbox} +Isabelle has replaced the free variable~{\tt P} by the scheme +variable~{\tt?P}\@. Free variables in the proof state remain fixed +throughout the proof. Isabelle finally converts them to scheme variables +so that the resulting theorem can be instantiated with any formula. + + +\subsection{Proving a distributive law} +\index{examples!propositional} +To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} +and the tactical \ttindex{REPEAT}, we shall prove part of the distributive +law $(P\conj Q)\disj R \iff (P\disj R)\conj (Q\disj R)$. + +We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it: +\begin{ttbox} +goal FOL.thy "(P & Q) | R --> (P | R)"; +{\out Level 0} +{\out P & Q | R --> P | R} +{\out 1. P & Q | R --> P | R} +by (resolve_tac [impI] 1); +{\out Level 1} +{\out P & Q | R --> P | R} +{\out 1. P & Q | R ==> P | R} +\end{ttbox} +Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but +\ttindex{eresolve_tac} deletes the assumption after use. The resulting proof +state is simpler. +\begin{ttbox} +by (eresolve_tac [disjE] 1); +{\out Level 2} +{\out P & Q | R --> P | R} +{\out 1. P & Q ==> P | R} +{\out 2. R ==> P | R} +\end{ttbox} +Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1, +replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the +rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule +and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two +assumptions~$P$ and~$Q$. The present example does not need~$Q$. +\begin{ttbox} +by (dresolve_tac [conjunct1] 1); +{\out Level 3} +{\out P & Q | R --> P | R} +{\out 1. P ==> P | R} +{\out 2. R ==> P | R} +\end{ttbox} +The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner. +\begin{ttbox} +by (resolve_tac [disjI1] 1); +{\out Level 4} +{\out P & Q | R --> P | R} +{\out 1. P ==> P} +{\out 2. R ==> P | R} +\ttbreak +by (resolve_tac [disjI2] 2); +{\out Level 5} +{\out P & Q | R --> P | R} +{\out 1. P ==> P} +{\out 2. R ==> R} +\end{ttbox} +Two calls of~\ttindex{assume_tac} can finish the proof. The +tactical~\ttindex{REPEAT} expresses a tactic that calls {\tt assume_tac~1} +as many times as possible. We can restrict attention to subgoal~1 because +the other subgoals move up after subgoal~1 disappears. +\begin{ttbox} +by (REPEAT (assume_tac 1)); +{\out Level 6} +{\out P & Q | R --> P | R} +{\out No subgoals!} +\end{ttbox} + + +\section{Quantifier reasoning} +\index{quantifiers!reasoning about}\index{parameters}\index{unknowns} +This section illustrates how Isabelle enforces quantifier provisos. +Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a +function unknown and $x$ and~$z$ are parameters. This may be replaced by +any term, possibly containing free occurrences of $x$ and~$z$. + +\subsection{Two quantifier proofs, successful and not} +\index{examples!with quantifiers} +Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an +attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former +proof succeeds, and the latter fails, because of the scope of quantified +variables~\cite{paulson89}. Unification helps even in these trivial +proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, +but we need never say so. This choice is forced by the reflexive law for +equality, and happens automatically. + +\subsubsection{The successful proof} +The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules +$(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: +\begin{ttbox} +goal FOL.thy "ALL x. EX y. x=y"; +{\out Level 0} +{\out ALL x. EX y. x = y} +{\out 1. ALL x. EX y. x = y} +\ttbreak +by (resolve_tac [allI] 1); +{\out Level 1} +{\out ALL x. EX y. x = y} +{\out 1. !!x. EX y. x = y} +\end{ttbox} +The variable~{\tt x} is no longer universally quantified, but is a +parameter in the subgoal; thus, it is universally quantified at the +meta-level. The subgoal must be proved for all possible values of~{\tt x}. +We apply the rule $(\exists I)$: +\begin{ttbox} +by (resolve_tac [exI] 1); +{\out Level 2} +{\out ALL x. EX y. x = y} +{\out 1. !!x. x = ?y1(x)} +\end{ttbox} +The bound variable {\tt y} has become {\tt?y1(x)}. This term consists of +the function unknown~{\tt?y1} applied to the parameter~{\tt x}. +Instances of {\tt?y1(x)} may or may not contain~{\tt x}. We resolve the +subgoal with the reflexivity axiom. +\begin{ttbox} +by (resolve_tac [refl] 1); +{\out Level 3} +{\out ALL x. EX y. x = y} +{\out No subgoals!} +\end{ttbox} +Let us consider what has happened in detail. The reflexivity axiom is +lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is +unified with $\Forall x.x=\Var{y@1}(x)$. The function unknowns $\Var{f}$ +and~$\Var{y@1}$ are both instantiated to the identity function, and +$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction. + +\subsubsection{The unsuccessful proof} +We state the goal $\exists y.\forall x.x=y$, which is {\bf not} a theorem, and +try~$(\exists I)$: +\begin{ttbox} +goal FOL.thy "EX y. ALL x. x=y"; +{\out Level 0} +{\out EX y. ALL x. x = y} +{\out 1. EX y. ALL x. x = y} +\ttbreak +by (resolve_tac [exI] 1); +{\out Level 1} +{\out EX y. ALL x. x = y} +{\out 1. ALL x. x = ?y} +\end{ttbox} +The unknown {\tt ?y} may be replaced by any term, but this can never +introduce another bound occurrence of~{\tt x}. We now apply~$(\forall I)$: +\begin{ttbox} +by (resolve_tac [allI] 1); +{\out Level 2} +{\out EX y. ALL x. x = y} +{\out 1. !!x. x = ?y} +\end{ttbox} +Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we +have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}. +The reflexivity axiom does not unify with subgoal~1. +\begin{ttbox} +by (resolve_tac [refl] 1); +{\out by: tactic returned no results} +\end{ttbox} +No other choice of rules seems likely to complete the proof. Of course, +this is no guarantee that Isabelle cannot prove $\exists y.\forall x.x=y$ +or other invalid assertions. We must appeal to the soundness of +first-order logic and the faithfulness of its encoding in +Isabelle~\cite{paulson89}, and must trust the implementation. + + +\subsection{Nested quantifiers} +\index{examples!with quantifiers} +Multiple quantifiers create complex terms. Proving $(\forall x\,y.P(x,y)) +\imp (\forall z\,w.P(w,z))$, will demonstrate how parameters and +unknowns develop. If they appear in the wrong order, the proof will fail. +This section concludes with a demonstration of {\tt REPEAT} +and~{\tt ORELSE}. + +The start of the proof is routine. +\begin{ttbox} +goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; +{\out Level 0} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +\ttbreak +by (resolve_tac [impI] 1); +{\out Level 1} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} +\end{ttbox} + +\subsubsection{The wrong approach} +Using \ttindex{dresolve_tac}, we apply the rule $(\forall E)$, bound to the +\ML\ identifier \ttindex{spec}. Then we apply $(\forall I)$. +\begin{ttbox} +by (dresolve_tac [spec] 1); +{\out Level 2} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)} +\ttbreak +by (resolve_tac [allI] 1); +{\out Level 3} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)} +\end{ttbox} +The unknown {\tt ?u} and the parameter {\tt z} have appeared. We again +apply $(\forall I)$ and~$(\forall E)$. +\begin{ttbox} +by (dresolve_tac [spec] 1); +{\out Level 4} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)} +\ttbreak +by (resolve_tac [allI] 1); +{\out Level 5} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)} +\end{ttbox} +The unknown {\tt ?y3} and the parameter {\tt w} have appeared. Each +unknown is applied to the parameters existing at the time of its creation; +instances of {\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances +of {\tt?y3(z)} can only contain~{\tt z}. Because of these restrictions, +proof by assumption will fail. +\begin{ttbox} +by (assume_tac 1); +{\out by: tactic returned no results} +{\out uncaught exception ERROR} +\end{ttbox} + +\subsubsection{The right approach} +To do this proof, the rules must be applied in the correct order. +Eigenvariables should be created before unknowns. The +\ttindex{choplev} command returns to an earlier stage of the proof; +let us return to the result of applying~$({\imp}I)$: +\begin{ttbox} +choplev 1; +{\out Level 1} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} +\end{ttbox} +Previously, we made the mistake of applying $(\forall E)$; this time, we +apply $(\forall I)$ twice. +\begin{ttbox} +by (resolve_tac [allI] 1); +{\out Level 2} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)} +\ttbreak +by (resolve_tac [allI] 1); +{\out Level 3} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)} +\end{ttbox} +The parameters {\tt z} and~{\tt w} have appeared. We now create the +unknowns: +\begin{ttbox} +by (dresolve_tac [spec] 1); +{\out Level 4} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)} +\ttbreak +by (dresolve_tac [spec] 1); +{\out Level 5} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)} +\end{ttbox} +Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt +z} and~{\tt w}: +\begin{ttbox} +by (assume_tac 1); +{\out Level 6} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out No subgoals!} +\end{ttbox} + +\subsubsection{A one-step proof using tacticals} +\index{tacticals} +\index{examples!of tacticals} +Repeated application of rules can be an effective theorem-proving +procedure, but the rules should be attempted in an order that delays the +creation of unknowns. As we have just seen, \ttindex{allI} should be +attempted before~\ttindex{spec}, while \ttindex{assume_tac} generally can +be attempted first. Such priorities can easily be expressed +using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. Let us return +to the original goal using \ttindex{choplev}: +\begin{ttbox} +choplev 0; +{\out Level 0} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +\end{ttbox} +A repetitive procedure proves it: +\begin{ttbox} +by (REPEAT (assume_tac 1 + ORELSE resolve_tac [impI,allI] 1 + ORELSE dresolve_tac [spec] 1)); +{\out Level 1} +{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} +{\out No subgoals!} +\end{ttbox} + + +\subsection{A realistic quantifier proof} +\index{examples!with quantifiers} +A proof of $(\forall x. P(x) \imp Q) \imp (\exists x. P(x)) \imp Q$ +demonstrates the practical use of parameters and unknowns. +Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we +use \ttindex{REPEAT}: +\begin{ttbox} +goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q"; +{\out Level 0} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +\ttbreak +by (REPEAT (resolve_tac [impI] 1)); +{\out Level 1} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q} +\end{ttbox} +We can eliminate the universal or the existential quantifier. The +existential quantifier should be eliminated first, since this creates a +parameter. The rule~$(\exists E)$ is bound to the +identifier~\ttindex{exE}. +\begin{ttbox} +by (eresolve_tac [exE] 1); +{\out Level 2} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q} +\end{ttbox} +The only possibility now is $(\forall E)$, a destruction rule. We use +\ttindex{dresolve_tac}, which discards the quantified assumption; it is +only needed once. +\begin{ttbox} +by (dresolve_tac [spec] 1); +{\out Level 3} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q} +\end{ttbox} +Because the parameter~{\tt x} appeared first, the unknown +term~{\tt?x3(x)} may depend upon it. Had we eliminated the universal +quantifier before the existential, this would not be so. + +Although $({\imp}E)$ is a destruction rule, it works with +\ttindex{eresolve_tac} to perform backward chaining. This technique is +frequently useful. +\begin{ttbox} +by (eresolve_tac [mp] 1); +{\out Level 4} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out 1. !!x. P(x) ==> P(?x3(x))} +\end{ttbox} +The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the +implication. The final step is trivial, thanks to the occurrence of~{\tt x}. +\begin{ttbox} +by (assume_tac 1); +{\out Level 5} +{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} +{\out No subgoals!} +\end{ttbox} + + +\subsection{The classical reasoning package} +\index{classical reasoning package} +Although Isabelle cannot compete with fully automatic theorem provers, it +provides enough automation to tackle substantial examples. The classical +reasoning package can be set up for any classical natural deduction logic +--- see the {\em Reference Manual}. + +Rules are packaged into bundles called \bfindex{classical sets}. The package +provides several tactics, which apply rules using naive algorithms, using +unification to handle quantifiers. The most useful tactic +is~\ttindex{fast_tac}. + +Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The +backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape +sequence, to break the long string over two lines.) +\begin{ttbox} +goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback +\ttback --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; +{\out Level 0} +{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} +{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} +{\out 1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} +{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} +\end{ttbox} +The rules of classical logic are bundled as {\tt FOL_cs}. We may solve +subgoal~1 at a stroke, using~\ttindex{fast_tac}. +\begin{ttbox} +by (fast_tac FOL_cs 1); +{\out Level 1} +{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} +{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} +{\out No subgoals!} +\end{ttbox} +Sceptics may examine the proof by calling the package's single-step +tactics, such as~{\tt step_tac}. This would take up much space, however, +so let us proceed to the next example: +\begin{ttbox} +goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback +\ttback (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; +{\out Level 0} +{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} +{\out 1. ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} +\end{ttbox} +Again, subgoal~1 succumbs immediately. +\begin{ttbox} +by (fast_tac FOL_cs 1); +{\out Level 1} +{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} +{\out No subgoals!} +\end{ttbox} +The classical reasoning package is not restricted to the usual logical +connectives. The natural deduction rules for unions and intersections in +set theory resemble those for disjunction and conjunction, and in the +infinitary case, for quantifiers. The package is valuable for reasoning in +set theory. + + +% Local Variables: +% mode: latex +% TeX-master: t +% End: