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

doc-src/Intro/getting.tex

author | boehmes |

Tue, 07 Dec 2010 15:44:38 +0100 | |

changeset 41064 | 0c447a17770a |

parent 14148 | 6580d374a509 |

child 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

updated SMT certificates

%% $Id$ \part{Using Isabelle from the ML Top-Level}\label{chap:getting} Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however. Proofs are conducted by applying certain \ML{} functions, which update a stored proof state. All syntax can be expressed using plain {\sc ascii} characters, but Isabelle can support alternative syntaxes, for example using mathematical symbols from a special screen font. The meta-logic and main object-logics already provide such fancy output as an option. 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 \texttt{typ}, \texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic}; tacticals have function types such as \texttt{tactic->tactic}. Isabelle users can operate on these data structures by writing \ML{} programs. \section{Forward proof}\label{sec:forward} \index{forward proof|(} This section describes the concrete syntax for types, terms and theorems, and demonstrates forward proof. The examples are set in first-order logic. The command to start Isabelle running first-order logic is \begin{ttbox} isabelle FOL \end{ttbox} Note that just typing \texttt{isabelle} usually brings up higher-order logic (HOL) by default. \subsection{Lexical matters} \index{identifiers}\index{reserved words} 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 \texttt{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. Identifiers that are not reserved words may serve as free variables or constants. A {\bf type identifier} consists of an identifier prefixed by a prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand for (free) type variables, which remain fixed during a proof. \index{type identifiers} An {\bf unknown}\index{unknowns} (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.% \footnote{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 {\tt"z6"} and subscript~0, while {\tt?a0.5} has identifier {\tt"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 {\tt"hello"} and subscript zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same conventions apply to type unknowns. The question mark is {\it not\/} part of the identifier!} \subsection{Syntax of types and terms} \index{classes!built-in|bold}\index{syntax!of types and terms} Classes are denoted by identifiers; the built-in class \cldx{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 of|bold}\index{sort constraints} Types are written with a syntax like \ML's. The built-in type \tydx{prop} is the type of propositions. Type variables can be constrained to particular classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace ord, arith\ttrbrace}. \[\dquotes \index{*:: symbol}\index{*=> symbol} \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} \index{*[ symbol}\index{*] symbol} \begin{array}{ll} \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline \alpha "::" C & \hbox{class constraint} \\ \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & \hbox{sort constraint} \\ \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & \hbox{$n$-argument function type} \\ "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction} \end{array} \] Terms are those of the typed $\lambda$-calculus. \index{terms!syntax of|bold}\index{type constraints} \[\dquotes \index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions} \index{*:: symbol} \begin{array}{ll} \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline t "::" \sigma & \hbox{type constraint} \\ "\%" x "." t & \hbox{abstraction } \lambda x.t \\ "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\ t "(" u@1"," \ldots "," u@n ")" & \hbox{application to several arguments (FOL and ZF)} \\ t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)} \end{array} \] Note that HOL uses its traditional ``higher-order'' syntax for application, which differs from that used in FOL. 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~\texttt{prop}. \index{meta-implication} \index{meta-quantifiers}\index{meta-equality} \index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol} \index{*== symbol}\index{*=?= symbol}\index{*==> symbol} \[\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 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 constraints} \index{*Trueprop constant} Most logics define the implicit coercion $Trueprop$ from object-formulae to propositions. 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~\tydx{prop} are seldom useful, but you can make a variable stand for a meta-formula by prefixing it with the symbol \texttt{PROP}:\index{*PROP symbol} \begin{ttbox} PROP ?psi ==> PROP ?theta \end{ttbox} Symbols of object-logics are typically rendered into {\sc ascii} 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) $$ $({\conj}I)$ translates into {\sc ascii} characters as \begin{ttbox} [| ?P; ?Q |] ==> ?P & ?Q \end{ttbox} The schematic variables let unification instantiate the rule. To avoid cluttering logic definitions with question marks, Isabelle converts any free variables in a rule to schematic variables; we normally declare $({\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 system} Meta-level theorems have the \ML{} type \mltydx{thm}. They 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 \texttt{prth}, \texttt{prths} and~{\tt prthq}. Of the other operations on theorems, most useful are \texttt{RS} and \texttt{RSN}, which perform resolution. \index{theorems!printing of} \begin{ttdescription} \item[\ttindex{prth} {\it thm};] pretty-prints {\it thm\/} at the terminal. \item[\ttindex{prths} {\it thms};] pretty-prints {\it thms}, a list of theorems. \item[\ttindex{prthq} {\it thmq};] pretty-prints {\it thmq}, a sequence of theorems; this is useful for inspecting the output of a tactic. \item[$thm1$ RS $thm2$] \index{*RS} resolves the conclusion of $thm1$ with the first premise of~$thm2$. \item[$thm1$ RSN $(i,thm2)$] \index{*RSN} resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$. \item[\ttindex{standard} $thm$] puts $thm$ into a standard format. It also renames schematic variables to have subscript zero, improving readability and reducing subscript growth. \end{ttdescription} The rules of a theory are normally bound to \ML\ identifiers. Suppose we are running an Isabelle session containing theory~FOL, natural deduction first-order logic.\footnote{For a listing of the FOL rules and their \ML{} names, turn to \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}% {page~\pageref{fol-rules}}.} Let us try an example given in~\S\ref{joining}. We first print \tdx{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} User input appears in {\footnotesize\tt typewriter characters}, and output appears in{\out 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. Printing commands like \texttt{prth} omit the quotes and the surrounding \texttt{val \ldots :\ thm}. Ignoring their side-effects, the printing commands are identity functions. To contrast \texttt{RS} with \texttt{RSN}, we resolve \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{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}} \] % Rules can be derived by pasting other rules together. Let us join \tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just printed. \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) |] ==>} {\out ?Q2(?x1)" : thm} it RS conjunct1; {\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>} {\out ?P6(?x2)" : thm} standard it; {\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>} {\out ?Pa(?x)" : thm} \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. \index{assumptions!use of} \subsection{*Flex-flex constraints} \label{flexflex} \index{flex-flex constraints|bold}\index{unknowns!function} 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 \texttt{RS} and~\texttt{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 = "EX x. ?a3(x) = ?a2(x)" [.] : thm} \end{ttbox} % The mysterious symbol \texttt{[.]} indicates that the result is subject to a meta-level hypothesis. We can make all such hypotheses visible by setting the \ttindexbold{show_hyps} flag: \begin{ttbox} set show_hyps; {\out val it = true : bool} refl RS exI; {\out val it = "EX x. ?a3(x) = ?a2(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 \texttt{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 \tdx{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} {\out THM ("RSN: multiple unifiers", 1,} {\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])} \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} \index{forward proof|)} \section{Backward proof} Although \texttt{RS} and \texttt{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} The tactics \texttt{assume_tac}, {\tt resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most single-step proofs. Although \texttt{eresolve_tac} and \texttt{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{ttdescription} \item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption} 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[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution} 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[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution} performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}} followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its first premise by assumption. But \texttt{eresolve_tac} additionally deletes that assumption from any subgoals arising from the resolution. \item[\ttindex{dresolve_tac} {\it thms} {\it i}] \index{forward proof}\index{destruct-resolution} performs destruct-resolution with the~$thms$, as described in~\S\ref{destruct}. It is useful for forward reasoning from the assumptions. \end{ttdescription} \subsection{Commands for backward proof} \index{proofs!commands for} 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{ttdescription} \item[\ttindex{Goal} {\it formula}; ] begins a new proof, where the {\it formula\/} is written as an \ML\ string. \item[\ttindex{by} {\it tactic}; ] applies the {\it tactic\/} to the current proof state, raising an exception if the tactic fails. \item[\ttindex{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[\ttindex{result}();] returns the theorem just proved, in a standard format. It fails if unproved subgoals are left, etc. \item[\ttindex{qed} {\it name};] is the usual way of ending a proof. It gets the theorem using \texttt{result}, stores it in Isabelle's theorem database and binds it to an \ML{} identifier. \end{ttdescription} 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 \index{*br} \index{*be} \index{*bd} \index{*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 \texttt{FOL} of the Isabelle distribution defines 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 \texttt{FOL/ex/intro.ML}.} \begin{ttbox} Goal "P|P --> P"; {\out Level 0} {\out P | P --> P} {\out 1. P | P --> P} \end{ttbox}\index{level of a proof} Isabelle responds by printing the initial proof state, which has $P\disj P\imp P$ as the main goal and the only subgoal. The {\bf level} of the state is the number of \texttt{by} commands that have been applied to reach it. We now use \ttindex{resolve_tac} to apply the rule \tdx{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 \tdx{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 affects subgoal~1, updating {\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~\texttt{P} in subgoal~1. \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 \texttt{qed} stores the theorem. \begin{ttbox} qed "mythm"; {\out val mythm = "?P | ?P --> ?P" : thm} \end{ttbox} Isabelle has replaced the free variable~\texttt{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. As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how instantiations affect the proof state. \subsection{Part of a distributive law} \index{examples!propositional} To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} and the tactical \texttt{REPEAT}, let us prove part of the distributive law \[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it: \begin{ttbox} Goal "(P & Q) | R --> (P | R)"; {\out Level 0} {\out P & Q | R --> P | R} {\out 1. P & Q | R --> P | R} \ttbreak 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 \texttt{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 \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we may try out \texttt{dresolve_tac}. \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 \texttt{assume_tac} can finish the proof. The tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{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}\index{parameters}\index{unknowns}\index{unknowns!function} This section illustrates how Isabelle enforces quantifier provisos. Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free occurrences of~$x$ and~$z$. On the other hand, no instantiation of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free occurrences of~$y$, since parameters are bound variables. \subsection{Two quantifier proofs: a success and a failure} \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{paulson-found}. 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. \paragraph{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 "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~\texttt{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~\texttt{x}. To remove the existential quantifier, 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 \texttt{y} has become {\tt?y1(x)}. This term consists of the function unknown~{\tt?y1} applied to the parameter~\texttt{x}. Instances of {\tt?y1(x)} may or may not contain~\texttt{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. \paragraph{The unsuccessful proof.} We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and try~$(\exists I)$: \begin{ttbox} Goal "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 \texttt{?y} may be replaced by any term, but this can never introduce another bound occurrence of~\texttt{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~\texttt{x}. The reflexivity axiom does not unify with subgoal~1. \begin{ttbox} by (resolve_tac [refl] 1); {\out by: tactic failed} \end{ttbox} There can be no proof of $\exists y.\forall x.x=y$ by the soundness of first-order logic. I have elsewhere proved the faithfulness of Isabelle's encoding of first-order logic~\cite{paulson-found}; there could, of course, be faults in 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 \texttt{REPEAT} and~\texttt{ORELSE}. \begin{ttbox} Goal "(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} \paragraph{The wrong approach.} Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the \ML\ identifier \tdx{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 \texttt{?x1} and the parameter \texttt{z} have appeared. We again apply $(\forall E)$ and~$(\forall I)$. \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 \texttt{?y3} and the parameter \texttt{w} have appeared. Each unknown is applied to the parameters existing at the time of its creation; instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1}, proof by assumption will fail. \begin{ttbox} by (assume_tac 1); {\out by: tactic failed} {\out uncaught exception ERROR} \end{ttbox} \paragraph{The right approach.} To do this proof, the rules must be applied in the correct order. Parameters 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)$ before $(\forall I)$. \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 \texttt{z} and~\texttt{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~\texttt{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} \paragraph{A one-step proof using tacticals.} \index{tacticals} \index{examples!of tacticals} Repeated application of rules can be effective, but the rules should be attempted in the correct order. 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} As we have just seen, \tdx{allI} should be attempted before~\tdx{spec}, while \ttindex{assume_tac} generally can be attempted first. Such priorities can easily be expressed using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. \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} To see the practical use of parameters and unknowns, let us prove half of the equivalence \[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \] We state the left-to-right half to Isabelle in the normal way. Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we use \texttt{REPEAT}: \begin{ttbox} Goal "(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~\tdx{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 we applied $(\exists E)$ before $(\forall E)$, the unknown term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}. 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~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the implication. The final step is trivial, thanks to the occurrence of~\texttt{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 reasoner} \index{classical reasoner} Isabelle provides enough automation to tackle substantial examples. The classical reasoner can be set up for any classical natural deduction logic; see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}}. It cannot compete with fully automatic theorem provers, but it is competitive with tools found in other interactive provers. Rules are packaged into {\bf classical sets}. The classical reasoner provides several tactics, which apply rules using naive algorithms. Unification handles quantifiers as shown above. The most useful tactic is~\ttindex{Blast_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 "(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} \ttindex{Blast_tac} proves subgoal~1 at a stroke. \begin{ttbox} by (Blast_tac 1); {\out Depth = 0} {\out Depth = 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~\texttt{step_tac}. This would take up much space, however, so let us proceed to the next example: \begin{ttbox} Goal "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)) <->} {\out (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} \end{ttbox} Again, subgoal~1 succumbs immediately. \begin{ttbox} by (Blast_tac 1); {\out Depth = 0} {\out Depth = 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 reasoner is not restricted to the usual logical connectives. The natural deduction rules for unions and intersections resemble those for disjunction and conjunction. The rules for infinite unions and intersections resemble those for quantifiers. Given such rules, the classical reasoner is effective for reasoning in set theory.