1\part{Using Isabelle from the ML Top-Level}\label{chap:getting} 2 3Most 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. 4Proofs are conducted by 5applying certain \ML{} functions, which update a stored proof state. 6All syntax can be expressed using plain {\sc ascii} 7characters, but Isabelle can support 8alternative syntaxes, for example using mathematical symbols from a 9special screen font. The meta-logic and main object-logics already 10provide such fancy output as an option. 11 12Object-logics are built upon Pure Isabelle, which implements the 13meta-logic and provides certain fundamental data structures: types, 14terms, signatures, theorems and theories, tactics and tacticals. 15These data structures have the corresponding \ML{} types \texttt{typ}, 16\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic}; 17tacticals have function types such as \texttt{tactic->tactic}. Isabelle 18users can operate on these data structures by writing \ML{} programs. 19 20 21\section{Forward proof}\label{sec:forward} \index{forward proof|(} 22This section describes the concrete syntax for types, terms and theorems, 23and demonstrates forward proof. The examples are set in first-order logic. 24The command to start Isabelle running first-order logic is 25\begin{ttbox} 26isabelle FOL 27\end{ttbox} 28Note that just typing \texttt{isabelle} usually brings up higher-order logic 29(HOL) by default. 30 31 32\subsection{Lexical matters} 33\index{identifiers}\index{reserved words} 34An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|) 35and single quotes~({\tt'}), beginning with a letter. Single quotes are 36regarded as primes; for instance \texttt{x'} is read as~$x'$. Identifiers are 37separated by white space and special characters. {\bf Reserved words} are 38identifiers that appear in Isabelle syntax definitions. 39 40An Isabelle theory can declare symbols composed of special characters, such 41as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}. (The latter three are part of 42the syntax of the meta-logic.) Such symbols may be run together; thus if 43\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is 44valid notation for a set of sets --- but only if \verb|}}| and \verb|{{| 45have not been declared as symbols! The parser resolves any ambiguity by 46taking the longest possible symbol that has been declared. Thus the string 47{\tt==>} is read as a single symbol. But \hbox{\tt= =>} is read as two 48symbols. 49 50Identifiers that are not reserved words may serve as free variables or 51constants. A {\bf type identifier} consists of an identifier prefixed by a 52prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand 53for (free) type variables, which remain fixed during a proof. 54\index{type identifiers} 55 56An {\bf unknown}\index{unknowns} (or type unknown) consists of a question 57mark, an identifier (or type identifier), and a subscript. The subscript, 58a non-negative integer, 59allows the renaming of unknowns prior to unification.% 60\footnote{The subscript may appear after the identifier, separated by a 61 dot; this prevents ambiguity when the identifier ends with a digit. Thus 62 {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5} 63 has identifier {\tt"a0"} and subscript~5. If the identifier does not 64 end with a digit, then no dot appears and a subscript of~0 is omitted; 65 for example, {\tt?hello} has identifier {\tt"hello"} and subscript 66 zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same 67 conventions apply to type unknowns. The question mark is {\it not\/} 68 part of the identifier!} 69 70 71\subsection{Syntax of types and terms} 72\index{classes!built-in|bold}\index{syntax!of types and terms} 73 74Classes are denoted by identifiers; the built-in class \cldx{logic} 75contains the `logical' types. Sorts are lists of classes enclosed in 76braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. 77 78\index{types!syntax of|bold}\index{sort constraints} Types are written 79with a syntax like \ML's. The built-in type \tydx{prop} is the type 80of propositions. Type variables can be constrained to particular 81classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace 82 ord, arith\ttrbrace}. 83\[\dquotes 84\index{*:: symbol}\index{*=> symbol} 85\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} 86\index{*[ symbol}\index{*] symbol} 87\begin{array}{ll} 88 \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline 89 \alpha "::" C & \hbox{class constraint} \\ 90 \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & 91 \hbox{sort constraint} \\ 92 \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\ 93 "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 94 & \hbox{$n$-argument function type} \\ 95 "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction} 96\end{array} 97\] 98Terms are those of the typed $\lambda$-calculus. 99\index{terms!syntax of|bold}\index{type constraints} 100\[\dquotes 101\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions} 102\index{*:: symbol} 103\begin{array}{ll} 104 \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline 105 t "::" \sigma & \hbox{type constraint} \\ 106 "\%" x "." t & \hbox{abstraction } \lambda x.t \\ 107 "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\ 108 t "(" u@1"," \ldots "," u@n ")" & 109 \hbox{application to several arguments (FOL and ZF)} \\ 110 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)} 111\end{array} 112\] 113Note that HOL uses its traditional ``higher-order'' syntax for application, 114which differs from that used in FOL. 115 116The theorems and rules of an object-logic are represented by theorems in 117the meta-logic, which are expressed using meta-formulae. Since the 118meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{} 119are just terms of type~\texttt{prop}. 120\index{meta-implication} 121\index{meta-quantifiers}\index{meta-equality} 122\index{*"!"! symbol} 123 124\index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working 125\index{"!]@{\tt\char124]} symbol} % so these are [| and |] 126 127\index{*== symbol}\index{*=?= symbol}\index{*==> symbol} 128\[\dquotes 129 \begin{array}{l@{\quad}l@{\quad}l} 130 \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline 131 a " == " b & a\equiv b & \hbox{meta-equality} \\ 132 a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\ 133 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\ 134 "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & 135 \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ 136 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ 137 "!!" x@1\ldots x@n "." \phi & 138 \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} 139 \end{array} 140\] 141Flex-flex constraints are meta-equalities arising from unification; they 142require special treatment. See~\S\ref{flexflex}. 143\index{flex-flex constraints} 144 145\index{*Trueprop constant} 146Most logics define the implicit coercion $Trueprop$ from object-formulae to 147propositions. This could cause an ambiguity: in $P\Imp Q$, do the 148variables $P$ and $Q$ stand for meta-formulae or object-formulae? If the 149latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To 150prevent such ambiguities, Isabelle's syntax does not allow a meta-formula 151to consist of a variable. Variables of type~\tydx{prop} are seldom 152useful, but you can make a variable stand for a meta-formula by prefixing 153it with the symbol \texttt{PROP}:\index{*PROP symbol} 154\begin{ttbox} 155PROP ?psi ==> PROP ?theta 156\end{ttbox} 157 158Symbols of object-logics are typically rendered into {\sc ascii} as 159follows: 160\[ \begin{tabular}{l@{\quad}l@{\quad}l} 161 \tt True & $\top$ & true \\ 162 \tt False & $\bot$ & false \\ 163 \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\ 164 \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\ 165 \verb'~' $P$ & $\neg P$ & negation \\ 166 \tt $P$ --> $Q$ & $P\imp Q$ & implication \\ 167 \tt $P$ <-> $Q$ & $P\bimp Q$ & bi-implication \\ 168 \tt ALL $x\,y\,z$ .\ $P$ & $\forall x\,y\,z.P$ & for all \\ 169 \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists 170 \end{tabular} 171\] 172To illustrate the notation, consider two axioms for first-order logic: 173$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ 174$$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ 175$({\conj}I)$ translates into {\sc ascii} characters as 176\begin{ttbox} 177[| ?P; ?Q |] ==> ?P & ?Q 178\end{ttbox} 179The schematic variables let unification instantiate the rule. To avoid 180cluttering logic definitions with question marks, Isabelle converts any 181free variables in a rule to schematic variables; we normally declare 182$({\conj}I)$ as 183\begin{ttbox} 184[| P; Q |] ==> P & Q 185\end{ttbox} 186This variables convention agrees with the treatment of variables in goals. 187Free variables in a goal remain fixed throughout the proof. After the 188proof is finished, Isabelle converts them to scheme variables in the 189resulting theorem. Scheme variables in a goal may be replaced by terms 190during the proof, supporting answer extraction, program synthesis, and so 191forth. 192 193For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as 194\begin{ttbox} 195[| EX x. P(x); !!x. P(x) ==> Q |] ==> Q 196\end{ttbox} 197 198 199\subsection{Basic operations on theorems} 200\index{theorems!basic operations on|bold} 201\index{LCF system} 202Meta-level theorems have the \ML{} type \mltydx{thm}. They represent the 203theorems and inference rules of object-logics. Isabelle's meta-logic is 204implemented using the {\sc lcf} approach: each meta-level inference rule is 205represented by a function from theorems to theorems. Object-level rules 206are taken as axioms. 207 208The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt 209 prthq}. Of the other operations on theorems, most useful are \texttt{RS} 210and \texttt{RSN}, which perform resolution. 211 212\index{theorems!printing of} 213\begin{ttdescription} 214\item[\ttindex{prth} {\it thm};] 215 pretty-prints {\it thm\/} at the terminal. 216 217\item[\ttindex{prths} {\it thms};] 218 pretty-prints {\it thms}, a list of theorems. 219 220\item[\ttindex{prthq} {\it thmq};] 221 pretty-prints {\it thmq}, a sequence of theorems; this is useful for 222 inspecting the output of a tactic. 223 224\item[$thm1$ RS $thm2$] \index{*RS} 225 resolves the conclusion of $thm1$ with the first premise of~$thm2$. 226 227\item[$thm1$ RSN $(i,thm2)$] \index{*RSN} 228 resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$. 229 230\item[\ttindex{standard} $thm$] 231 puts $thm$ into a standard format. It also renames schematic variables 232 to have subscript zero, improving readability and reducing subscript 233 growth. 234\end{ttdescription} 235The rules of a theory are normally bound to \ML\ identifiers. Suppose we are 236running an Isabelle session containing theory~FOL, natural deduction 237first-order logic.\footnote{For a listing of the FOL rules and their \ML{} 238 names, turn to 239\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}% 240 {page~\pageref{fol-rules}}.} 241Let us try an example given in~\S\ref{joining}. We 242first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with 243itself. 244\begin{ttbox} 245prth mp; 246{\out [| ?P --> ?Q; ?P |] ==> ?Q} 247{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm} 248prth (mp RS mp); 249{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} 250{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} 251\end{ttbox} 252User input appears in {\footnotesize\tt typewriter characters}, and output 253appears in{\out slanted typewriter characters}. \ML's response {\out val 254 }~\ldots{} is compiler-dependent and will sometimes be suppressed. This 255session illustrates two formats for the display of theorems. Isabelle's 256top-level displays theorems as \ML{} values, enclosed in quotes. Printing 257commands like \texttt{prth} omit the quotes and the surrounding \texttt{val 258 \ldots :\ thm}. Ignoring their side-effects, the printing commands are 259identity functions. 260 261To contrast \texttt{RS} with \texttt{RSN}, we resolve 262\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. 263\begin{ttbox} 264conjunct1 RS mp; 265{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm} 266conjunct1 RSN (2,mp); 267{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm} 268\end{ttbox} 269These correspond to the following proofs: 270\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P} 271 \qquad 272 \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} 273\] 274% 275Rules can be derived by pasting other rules together. Let us join 276\tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt 277 conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just 278printed. 279\begin{ttbox} 280spec; 281{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm} 282it RS mp; 283{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>} 284{\out ?Q2(?x1)" : thm} 285it RS conjunct1; 286{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>} 287{\out ?P6(?x2)" : thm} 288standard it; 289{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>} 290{\out ?Pa(?x)" : thm} 291\end{ttbox} 292By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have 293derived a destruction rule for formulae of the form $\forall x. 294P(x)\imp(Q(x)\conj R(x))$. Used with destruct-resolution, such specialized 295rules provide a way of referring to particular assumptions. 296\index{assumptions!use of} 297 298\subsection{*Flex-flex constraints} \label{flexflex} 299\index{flex-flex constraints|bold}\index{unknowns!function} 300In higher-order unification, {\bf flex-flex} equations are those where both 301sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$. 302They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and 303$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown. They 304admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$ 305and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$. Huet's 306procedure does not enumerate the unifiers; instead, it retains flex-flex 307equations as constraints on future unifications. Flex-flex constraints 308occasionally become attached to a proof state; more frequently, they appear 309during use of \texttt{RS} and~\texttt{RSN}: 310\begin{ttbox} 311refl; 312{\out val it = "?a = ?a" : thm} 313exI; 314{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm} 315refl RS exI; 316{\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm} 317\end{ttbox} 318% 319The mysterious symbol \texttt{[.]} indicates that the result is subject to 320a meta-level hypothesis. We can make all such hypotheses visible by setting the 321\ttindexbold{show_hyps} flag: 322\begin{ttbox} 323set show_hyps; 324{\out val it = true : bool} 325refl RS exI; 326{\out val it = "EX x. ?a3(x) = ?a2(x)" ["?a3(?x) =?= ?a2(?x)"] : thm} 327\end{ttbox} 328 329\noindent 330Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with 331the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$. Instances 332satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and 333$\exists x.x=\Var{u}$. Calling \ttindex{flexflex_rule} removes all 334constraints by applying the trivial unifier:\index{*prthq} 335\begin{ttbox} 336prthq (flexflex_rule it); 337{\out EX x. ?a4 = ?a4} 338\end{ttbox} 339Isabelle simplifies flex-flex equations to eliminate redundant bound 340variables. In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$, 341there is no bound occurrence of~$x$ on the right side; thus, there will be 342none on the left in a common instance of these terms. Choosing a new 343variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$, 344simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$ 345from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda 346y.\Var{g}(y)$. By $\eta$-conversion, this simplifies to the assignment 347$\Var{g}\equiv\lambda y.?h(k(y))$. 348 349\begin{warn} 350\ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless 351the resolution delivers {\bf exactly one} resolvent. For multiple results, 352use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The 353following example uses \ttindex{read_instantiate} to create an instance 354of \tdx{refl} containing no schematic variables. 355\begin{ttbox} 356val reflk = read_instantiate [("a","k")] refl; 357{\out val reflk = "k = k" : thm} 358\end{ttbox} 359 360\noindent 361A flex-flex constraint is no longer possible; resolution does not find a 362unique unifier: 363\begin{ttbox} 364reflk RS exI; 365{\out uncaught exception} 366{\out THM ("RSN: multiple unifiers", 1,} 367{\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])} 368\end{ttbox} 369Using \ttindex{RL} this time, we discover that there are four unifiers, and 370four resolvents: 371\begin{ttbox} 372[reflk] RL [exI]; 373{\out val it = ["EX x. x = x", "EX x. k = x",} 374{\out "EX x. x = k", "EX x. k = k"] : thm list} 375\end{ttbox} 376\end{warn} 377 378\index{forward proof|)} 379 380\section{Backward proof} 381Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning, 382large proofs require tactics. Isabelle provides a suite of commands for 383conducting a backward proof using tactics. 384 385\subsection{The basic tactics} 386The tactics \texttt{assume_tac}, {\tt 387resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most 388single-step proofs. Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are 389not strictly necessary, they simplify proofs involving elimination and 390destruction rules. All the tactics act on a subgoal designated by a 391positive integer~$i$, failing if~$i$ is out of range. The resolution 392tactics try their list of theorems in left-to-right order. 393 394\begin{ttdescription} 395\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption} 396 is the tactic that attempts to solve subgoal~$i$ by assumption. Proof by 397 assumption is not a trivial step; it can falsify other subgoals by 398 instantiating shared variables. There may be several ways of solving the 399 subgoal by assumption. 400 401\item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution} 402 is the basic resolution tactic, used for most proof steps. The $thms$ 403 represent object-rules, which are resolved against subgoal~$i$ of the 404 proof state. For each rule, resolution forms next states by unifying the 405 conclusion with the subgoal and inserting instantiated premises in its 406 place. A rule can admit many higher-order unifiers. The tactic fails if 407 none of the rules generates next states. 408 409\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution} 410 performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}} 411 followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its 412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes 413 that assumption from any subgoals arising from the resolution. 414 415\item[\ttindex{dresolve_tac} {\it thms} {\it i}] 416 \index{forward proof}\index{destruct-resolution} 417 performs destruct-resolution with the~$thms$, as described 418 in~\S\ref{destruct}. It is useful for forward reasoning from the 419 assumptions. 420\end{ttdescription} 421 422\subsection{Commands for backward proof} 423\index{proofs!commands for} 424Tactics are normally applied using the subgoal module, which maintains a 425proof state and manages the proof construction. It allows interactive 426backtracking through the proof space, going away to prove lemmas, etc.; of 427its many commands, most important are the following: 428\begin{ttdescription} 429\item[\ttindex{Goal} {\it formula}; ] 430begins a new proof, where the {\it formula\/} is written as an \ML\ string. 431 432\item[\ttindex{by} {\it tactic}; ] 433applies the {\it tactic\/} to the current proof 434state, raising an exception if the tactic fails. 435 436\item[\ttindex{undo}(); ] 437 reverts to the previous proof state. Undo can be repeated but cannot be 438 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely 439 causes \ML\ to echo the value of that function. 440 441\item[\ttindex{result}();] 442returns the theorem just proved, in a standard format. It fails if 443unproved subgoals are left, etc. 444 445\item[\ttindex{qed} {\it name};] is the usual way of ending a proof. 446 It gets the theorem using \texttt{result}, stores it in Isabelle's 447 theorem database and binds it to an \ML{} identifier. 448 449\end{ttdescription} 450The commands and tactics given above are cumbersome for interactive use. 451Although our examples will use the full commands, you may prefer Isabelle's 452shortcuts: 453\begin{center} \tt 454\index{*br} \index{*be} \index{*bd} \index{*ba} 455\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l} 456 ba {\it i}; & by (assume_tac {\it i}); \\ 457 458 br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\ 459 460 be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\ 461 462 bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); 463\end{tabular} 464\end{center} 465 466\subsection{A trivial example in propositional logic} 467\index{examples!propositional} 468 469Directory \texttt{FOL} of the Isabelle distribution defines the theory of 470first-order logic. Let us try the example from \S\ref{prop-proof}, 471entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these 472 examples, see the file \texttt{FOL/ex/intro.ML}.} 473\begin{ttbox} 474Goal "P|P --> P"; 475{\out Level 0} 476{\out P | P --> P} 477{\out 1. P | P --> P} 478\end{ttbox}\index{level of a proof} 479Isabelle responds by printing the initial proof state, which has $P\disj 480P\imp P$ as the main goal and the only subgoal. The {\bf level} of the 481state is the number of \texttt{by} commands that have been applied to reach 482it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, 483or~$({\imp}I)$, to subgoal~1: 484\begin{ttbox} 485by (resolve_tac [impI] 1); 486{\out Level 1} 487{\out P | P --> P} 488{\out 1. P | P ==> P} 489\end{ttbox} 490In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$. 491(The meta-implication {\tt==>} indicates assumptions.) We apply 492\tdx{disjE}, or~(${\disj}E)$, to that subgoal: 493\begin{ttbox} 494by (resolve_tac [disjE] 1); 495{\out Level 2} 496{\out P | P --> P} 497{\out 1. P | P ==> ?P1 | ?Q1} 498{\out 2. [| P | P; ?P1 |] ==> P} 499{\out 3. [| P | P; ?Q1 |] ==> P} 500\end{ttbox} 501At Level~2 there are three subgoals, each provable by assumption. We 502deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using 503\ttindex{assume_tac}. This affects subgoal~1, updating {\tt?Q1} to~{\tt 504 P}. 505\begin{ttbox} 506by (assume_tac 3); 507{\out Level 3} 508{\out P | P --> P} 509{\out 1. P | P ==> ?P1 | P} 510{\out 2. [| P | P; ?P1 |] ==> P} 511\end{ttbox} 512Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1. 513\begin{ttbox} 514by (assume_tac 2); 515{\out Level 4} 516{\out P | P --> P} 517{\out 1. P | P ==> P | P} 518\end{ttbox} 519Lastly we prove the remaining subgoal by assumption: 520\begin{ttbox} 521by (assume_tac 1); 522{\out Level 5} 523{\out P | P --> P} 524{\out No subgoals!} 525\end{ttbox} 526Isabelle tells us that there are no longer any subgoals: the proof is 527complete. Calling \texttt{qed} stores the theorem. 528\begin{ttbox} 529qed "mythm"; 530{\out val mythm = "?P | ?P --> ?P" : thm} 531\end{ttbox} 532Isabelle has replaced the free variable~\texttt{P} by the scheme 533variable~{\tt?P}\@. Free variables in the proof state remain fixed 534throughout the proof. Isabelle finally converts them to scheme variables 535so that the resulting theorem can be instantiated with any formula. 536 537As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how 538instantiations affect the proof state. 539 540 541\subsection{Part of a distributive law} 542\index{examples!propositional} 543To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} 544and the tactical \texttt{REPEAT}, let us prove part of the distributive 545law 546\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] 547We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it: 548\begin{ttbox} 549Goal "(P & Q) | R --> (P | R)"; 550{\out Level 0} 551{\out P & Q | R --> P | R} 552{\out 1. P & Q | R --> P | R} 553\ttbreak 554by (resolve_tac [impI] 1); 555{\out Level 1} 556{\out P & Q | R --> P | R} 557{\out 1. P & Q | R ==> P | R} 558\end{ttbox} 559Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but 560\ttindex{eresolve_tac} deletes the assumption after use. The resulting proof 561state is simpler. 562\begin{ttbox} 563by (eresolve_tac [disjE] 1); 564{\out Level 2} 565{\out P & Q | R --> P | R} 566{\out 1. P & Q ==> P | R} 567{\out 2. R ==> P | R} 568\end{ttbox} 569Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1, 570replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the 571rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule 572and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two 573assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we 574may try out \texttt{dresolve_tac}. 575\begin{ttbox} 576by (dresolve_tac [conjunct1] 1); 577{\out Level 3} 578{\out P & Q | R --> P | R} 579{\out 1. P ==> P | R} 580{\out 2. R ==> P | R} 581\end{ttbox} 582The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner. 583\begin{ttbox} 584by (resolve_tac [disjI1] 1); 585{\out Level 4} 586{\out P & Q | R --> P | R} 587{\out 1. P ==> P} 588{\out 2. R ==> P | R} 589\ttbreak 590by (resolve_tac [disjI2] 2); 591{\out Level 5} 592{\out P & Q | R --> P | R} 593{\out 1. P ==> P} 594{\out 2. R ==> R} 595\end{ttbox} 596Two calls of \texttt{assume_tac} can finish the proof. The 597tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1} 598as many times as possible. We can restrict attention to subgoal~1 because 599the other subgoals move up after subgoal~1 disappears. 600\begin{ttbox} 601by (REPEAT (assume_tac 1)); 602{\out Level 6} 603{\out P & Q | R --> P | R} 604{\out No subgoals!} 605\end{ttbox} 606 607 608\section{Quantifier reasoning} 609\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function} 610This section illustrates how Isabelle enforces quantifier provisos. 611Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier 612rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function 613unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of 614replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free 615occurrences of~$x$ and~$z$. On the other hand, no instantiation 616of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free 617occurrences of~$y$, since parameters are bound variables. 618 619\subsection{Two quantifier proofs: a success and a failure} 620\index{examples!with quantifiers} 621Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an 622attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former 623proof succeeds, and the latter fails, because of the scope of quantified 624variables~\cite{paulson-found}. Unification helps even in these trivial 625proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, 626but we need never say so. This choice is forced by the reflexive law for 627equality, and happens automatically. 628 629\paragraph{The successful proof.} 630The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules 631$(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: 632\begin{ttbox} 633Goal "ALL x. EX y. x=y"; 634{\out Level 0} 635{\out ALL x. EX y. x = y} 636{\out 1. ALL x. EX y. x = y} 637\ttbreak 638by (resolve_tac [allI] 1); 639{\out Level 1} 640{\out ALL x. EX y. x = y} 641{\out 1. !!x. EX y. x = y} 642\end{ttbox} 643The variable~\texttt{x} is no longer universally quantified, but is a 644parameter in the subgoal; thus, it is universally quantified at the 645meta-level. The subgoal must be proved for all possible values of~\texttt{x}. 646 647To remove the existential quantifier, we apply the rule $(\exists I)$: 648\begin{ttbox} 649by (resolve_tac [exI] 1); 650{\out Level 2} 651{\out ALL x. EX y. x = y} 652{\out 1. !!x. x = ?y1(x)} 653\end{ttbox} 654The bound variable \texttt{y} has become {\tt?y1(x)}. This term consists of 655the function unknown~{\tt?y1} applied to the parameter~\texttt{x}. 656Instances of {\tt?y1(x)} may or may not contain~\texttt{x}. We resolve the 657subgoal with the reflexivity axiom. 658\begin{ttbox} 659by (resolve_tac [refl] 1); 660{\out Level 3} 661{\out ALL x. EX y. x = y} 662{\out No subgoals!} 663\end{ttbox} 664Let us consider what has happened in detail. The reflexivity axiom is 665lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is 666unified with $\Forall x.x=\Var{y@1}(x)$. The function unknowns $\Var{f}$ 667and~$\Var{y@1}$ are both instantiated to the identity function, and 668$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction. 669 670\paragraph{The unsuccessful proof.} 671We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and 672try~$(\exists I)$: 673\begin{ttbox} 674Goal "EX y. ALL x. x=y"; 675{\out Level 0} 676{\out EX y. ALL x. x = y} 677{\out 1. EX y. ALL x. x = y} 678\ttbreak 679by (resolve_tac [exI] 1); 680{\out Level 1} 681{\out EX y. ALL x. x = y} 682{\out 1. ALL x. x = ?y} 683\end{ttbox} 684The unknown \texttt{?y} may be replaced by any term, but this can never 685introduce another bound occurrence of~\texttt{x}. We now apply~$(\forall I)$: 686\begin{ttbox} 687by (resolve_tac [allI] 1); 688{\out Level 2} 689{\out EX y. ALL x. x = y} 690{\out 1. !!x. x = ?y} 691\end{ttbox} 692Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we 693have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}. 694The reflexivity axiom does not unify with subgoal~1. 695\begin{ttbox} 696by (resolve_tac [refl] 1); 697{\out by: tactic failed} 698\end{ttbox} 699There can be no proof of $\exists y.\forall x.x=y$ by the soundness of 700first-order logic. I have elsewhere proved the faithfulness of Isabelle's 701encoding of first-order logic~\cite{paulson-found}; there could, of course, be 702faults in the implementation. 703 704 705\subsection{Nested quantifiers} 706\index{examples!with quantifiers} 707Multiple quantifiers create complex terms. Proving 708\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] 709will demonstrate how parameters and unknowns develop. If they appear in 710the wrong order, the proof will fail. 711 712This section concludes with a demonstration of \texttt{REPEAT} 713and~\texttt{ORELSE}. 714\begin{ttbox} 715Goal "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; 716{\out Level 0} 717{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 718{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 719\ttbreak 720by (resolve_tac [impI] 1); 721{\out Level 1} 722{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 723{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} 724\end{ttbox} 725 726\paragraph{The wrong approach.} 727Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the 728\ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. 729\begin{ttbox} 730by (dresolve_tac [spec] 1); 731{\out Level 2} 732{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 733{\out 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)} 734\ttbreak 735by (resolve_tac [allI] 1); 736{\out Level 3} 737{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 738{\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)} 739\end{ttbox} 740The unknown \texttt{?x1} and the parameter \texttt{z} have appeared. We again 741apply $(\forall E)$ and~$(\forall I)$. 742\begin{ttbox} 743by (dresolve_tac [spec] 1); 744{\out Level 4} 745{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 746{\out 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)} 747\ttbreak 748by (resolve_tac [allI] 1); 749{\out Level 5} 750{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 751{\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)} 752\end{ttbox} 753The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each 754unknown is applied to the parameters existing at the time of its creation; 755instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances 756of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1}, 757proof by assumption will fail. 758\begin{ttbox} 759by (assume_tac 1); 760{\out by: tactic failed} 761{\out uncaught exception ERROR} 762\end{ttbox} 763 764\paragraph{The right approach.} 765To do this proof, the rules must be applied in the correct order. 766Parameters should be created before unknowns. The 767\ttindex{choplev} command returns to an earlier stage of the proof; 768let us return to the result of applying~$({\imp}I)$: 769\begin{ttbox} 770choplev 1; 771{\out Level 1} 772{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 773{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} 774\end{ttbox} 775Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$. 776\begin{ttbox} 777by (resolve_tac [allI] 1); 778{\out Level 2} 779{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 780{\out 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)} 781\ttbreak 782by (resolve_tac [allI] 1); 783{\out Level 3} 784{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 785{\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)} 786\end{ttbox} 787The parameters \texttt{z} and~\texttt{w} have appeared. We now create the 788unknowns: 789\begin{ttbox} 790by (dresolve_tac [spec] 1); 791{\out Level 4} 792{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 793{\out 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)} 794\ttbreak 795by (dresolve_tac [spec] 1); 796{\out Level 5} 797{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 798{\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)} 799\end{ttbox} 800Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt 801z} and~\texttt{w}: 802\begin{ttbox} 803by (assume_tac 1); 804{\out Level 6} 805{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 806{\out No subgoals!} 807\end{ttbox} 808 809\paragraph{A one-step proof using tacticals.} 810\index{tacticals} \index{examples!of tacticals} 811 812Repeated application of rules can be effective, but the rules should be 813attempted in the correct order. Let us return to the original goal using 814\ttindex{choplev}: 815\begin{ttbox} 816choplev 0; 817{\out Level 0} 818{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 819{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 820\end{ttbox} 821As we have just seen, \tdx{allI} should be attempted 822before~\tdx{spec}, while \ttindex{assume_tac} generally can be 823attempted first. Such priorities can easily be expressed 824using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. 825\begin{ttbox} 826by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 827 ORELSE dresolve_tac [spec] 1)); 828{\out Level 1} 829{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} 830{\out No subgoals!} 831\end{ttbox} 832 833 834\subsection{A realistic quantifier proof} 835\index{examples!with quantifiers} 836To see the practical use of parameters and unknowns, let us prove half of 837the equivalence 838\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \] 839We state the left-to-right half to Isabelle in the normal way. 840Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we 841use \texttt{REPEAT}: 842\begin{ttbox} 843Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q"; 844{\out Level 0} 845{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 846{\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 847\ttbreak 848by (REPEAT (resolve_tac [impI] 1)); 849{\out Level 1} 850{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 851{\out 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q} 852\end{ttbox} 853We can eliminate the universal or the existential quantifier. The 854existential quantifier should be eliminated first, since this creates a 855parameter. The rule~$(\exists E)$ is bound to the 856identifier~\tdx{exE}. 857\begin{ttbox} 858by (eresolve_tac [exE] 1); 859{\out Level 2} 860{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 861{\out 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q} 862\end{ttbox} 863The only possibility now is $(\forall E)$, a destruction rule. We use 864\ttindex{dresolve_tac}, which discards the quantified assumption; it is 865only needed once. 866\begin{ttbox} 867by (dresolve_tac [spec] 1); 868{\out Level 3} 869{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 870{\out 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q} 871\end{ttbox} 872Because we applied $(\exists E)$ before $(\forall E)$, the unknown 873term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}. 874 875Although $({\imp}E)$ is a destruction rule, it works with 876\ttindex{eresolve_tac} to perform backward chaining. This technique is 877frequently useful. 878\begin{ttbox} 879by (eresolve_tac [mp] 1); 880{\out Level 4} 881{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 882{\out 1. !!x. P(x) ==> P(?x3(x))} 883\end{ttbox} 884The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the 885implication. The final step is trivial, thanks to the occurrence of~\texttt{x}. 886\begin{ttbox} 887by (assume_tac 1); 888{\out Level 5} 889{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} 890{\out No subgoals!} 891\end{ttbox} 892 893 894\subsection{The classical reasoner} 895\index{classical reasoner} 896Isabelle provides enough automation to tackle substantial examples. 897The classical 898reasoner can be set up for any classical natural deduction logic; 899see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 900 {Chap.\ts\ref{chap:classical}}. 901It cannot compete with fully automatic theorem provers, but it is 902competitive with tools found in other interactive provers. 903 904Rules are packaged into {\bf classical sets}. The classical reasoner 905provides several tactics, which apply rules using naive algorithms. 906Unification handles quantifiers as shown above. The most useful tactic 907is~\ttindex{Blast_tac}. 908 909Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The 910backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape 911sequence, to break the long string over two lines.) 912\begin{ttbox} 913Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback 914\ttback --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; 915{\out Level 0} 916{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} 917{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} 918{\out 1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} 919{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} 920\end{ttbox} 921\ttindex{Blast_tac} proves subgoal~1 at a stroke. 922\begin{ttbox} 923by (Blast_tac 1); 924{\out Depth = 0} 925{\out Depth = 1} 926{\out Level 1} 927{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} 928{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} 929{\out No subgoals!} 930\end{ttbox} 931Sceptics may examine the proof by calling the package's single-step 932tactics, such as~\texttt{step_tac}. This would take up much space, however, 933so let us proceed to the next example: 934\begin{ttbox} 935Goal "ALL x. P(x,f(x)) <-> \ttback 936\ttback (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; 937{\out Level 0} 938{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} 939{\out 1. ALL x. P(x,f(x)) <->} 940{\out (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} 941\end{ttbox} 942Again, subgoal~1 succumbs immediately. 943\begin{ttbox} 944by (Blast_tac 1); 945{\out Depth = 0} 946{\out Depth = 1} 947{\out Level 1} 948{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} 949{\out No subgoals!} 950\end{ttbox} 951The classical reasoner is not restricted to the usual logical connectives. 952The natural deduction rules for unions and intersections resemble those for 953disjunction and conjunction. The rules for infinite unions and 954intersections resemble those for quantifiers. Given such rules, the classical 955reasoner is effective for reasoning in set theory. 956 957