1\part{Foundations} 2The following sections discuss Isabelle's logical foundations in detail: 3representing logical syntax in the typed $\lambda$-calculus; expressing 4inference rules in Isabelle's meta-logic; combining rules by resolution. 5 6If you wish to use Isabelle immediately, please turn to 7page~\pageref{chap:getting}. You can always read about foundations later, 8either by returning to this point or by looking up particular items in the 9index. 10 11\begin{figure} 12\begin{eqnarray*} 13 \neg P & \hbox{abbreviates} & P\imp\bot \\ 14 P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P) 15\end{eqnarray*} 16\vskip 4ex 17 18\(\begin{array}{c@{\qquad\qquad}c} 19 \infer[({\conj}I)]{P\conj Q}{P & Q} & 20 \infer[({\conj}E1)]{P}{P\conj Q} \qquad 21 \infer[({\conj}E2)]{Q}{P\conj Q} \\[4ex] 22 23 \infer[({\disj}I1)]{P\disj Q}{P} \qquad 24 \infer[({\disj}I2)]{P\disj Q}{Q} & 25 \infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex] 26 27 \infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} & 28 \infer[({\imp}E)]{Q}{P\imp Q & P} \\[4ex] 29 30 & 31 \infer[({\bot}E)]{P}{\bot}\\[4ex] 32 33 \infer[({\forall}I)*]{\forall x.P}{P} & 34 \infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex] 35 36 \infer[({\exists}I)]{\exists x.P}{P[t/x]} & 37 \infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex] 38 39 {t=t} \,(refl) & \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}} 40\end{array} \) 41 42\bigskip\bigskip 43*{\em Eigenvariable conditions\/}: 44 45$\forall I$: provided $x$ is not free in the assumptions 46 47$\exists E$: provided $x$ is not free in $Q$ or any assumption except $P$ 48\caption{Intuitionistic first-order logic} \label{fol-fig} 49\end{figure} 50 51\section{Formalizing logical syntax in Isabelle}\label{sec:logical-syntax} 52\index{first-order logic} 53 54Figure~\ref{fol-fig} presents intuitionistic first-order logic, 55including equality. Let us see how to formalize 56this logic in Isabelle, illustrating the main features of Isabelle's 57polymorphic meta-logic. 58 59\index{lambda calc@$\lambda$-calculus} 60Isabelle represents syntax using the simply typed $\lambda$-calculus. We 61declare a type for each syntactic category of the logic. We declare a 62constant for each symbol of the logic, giving each $n$-place operation an 63$n$-argument curried function type. Most importantly, 64$\lambda$-abstraction represents variable binding in quantifiers. 65 66\index{types!syntax of}\index{types!function}\index{*fun type} 67\index{type constructors} 68Isabelle has \ML-style polymorphic types such as~$(\alpha)list$, where 69$list$ is a type constructor and $\alpha$ is a type variable; for example, 70$(bool)list$ is the type of lists of booleans. Function types have the 71form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are 72types. Curried function types may be abbreviated: 73\[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad 74[\sigma@1, \ldots, \sigma@n] \To \tau \] 75 76\index{terms!syntax of} The syntax for terms is summarised below. 77Note that there are two versions of function application syntax 78available in Isabelle: either $t\,u$, which is the usual form for 79higher-order languages, or $t(u)$, trying to look more like 80first-order. The latter syntax is used throughout the manual. 81\[ 82\index{lambda abs@$\lambda$-abstractions}\index{function applications} 83\begin{array}{ll} 84 t :: \tau & \hbox{type constraint, on a term or bound variable} \\ 85 \lambda x.t & \hbox{abstraction} \\ 86 \lambda x@1\ldots x@n.t 87 & \hbox{curried abstraction, $\lambda x@1. \ldots \lambda x@n.t$} \\ 88 t(u) & \hbox{application} \\ 89 t (u@1, \ldots, u@n) & \hbox{curried application, $t(u@1)\ldots(u@n)$} 90\end{array} 91\] 92 93 94\subsection{Simple types and constants}\index{types!simple|bold} 95 96The syntactic categories of our logic (Fig.\ts\ref{fol-fig}) are {\bf 97 formulae} and {\bf terms}. Formulae denote truth values, so (following 98tradition) let us call their type~$o$. To allow~0 and~$Suc(t)$ as terms, 99let us declare a type~$nat$ of natural numbers. Later, we shall see 100how to admit terms of other types. 101 102\index{constants}\index{*nat type}\index{*o type} 103After declaring the types~$o$ and~$nat$, we may declare constants for the 104symbols of our logic. Since $\bot$ denotes a truth value (falsity) and 0 105denotes a number, we put \begin{eqnarray*} 106 \bot & :: & o \\ 107 0 & :: & nat. 108\end{eqnarray*} 109If a symbol requires operands, the corresponding constant must have a 110function type. In our logic, the successor function 111($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a 112function from truth values to truth values, and the binary connectives are 113curried functions taking two truth values as arguments: 114\begin{eqnarray*} 115 Suc & :: & nat\To nat \\ 116 {\neg} & :: & o\To o \\ 117 \conj,\disj,\imp,\bimp & :: & [o,o]\To o 118\end{eqnarray*} 119The binary connectives can be declared as infixes, with appropriate 120precedences, so that we write $P\conj Q\disj R$ instead of 121$\disj(\conj(P,Q), R)$. 122 123Section~\ref{sec:defining-theories} below describes the syntax of Isabelle 124theory files and illustrates it by extending our logic with mathematical 125induction. 126 127 128\subsection{Polymorphic types and constants} \label{polymorphic} 129\index{types!polymorphic|bold} 130\index{equality!polymorphic} 131\index{constants!polymorphic} 132 133Which type should we assign to the equality symbol? If we tried 134$[nat,nat]\To o$, then equality would be restricted to the natural 135numbers; we should have to declare different equality symbols for each 136type. Isabelle's type system is polymorphic, so we could declare 137\begin{eqnarray*} 138 {=} & :: & [\alpha,\alpha]\To o, 139\end{eqnarray*} 140where the type variable~$\alpha$ ranges over all types. 141But this is also wrong. The declaration is too polymorphic; $\alpha$ 142includes types like~$o$ and $nat\To nat$. Thus, it admits 143$\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in 144higher-order logic but not in first-order logic. 145 146Isabelle's {\bf type classes}\index{classes} control 147polymorphism~\cite{nipkow-prehofer}. Each type variable belongs to a 148class, which denotes a set of types. Classes are partially ordered by the 149subclass relation, which is essentially the subset relation on the sets of 150types. They closely resemble the classes of the functional language 151Haskell~\cite{haskell-tutorial,haskell-report}. 152 153\index{*logic class}\index{*term class} 154Isabelle provides the built-in class $logic$, which consists of the logical 155types: the ones we want to reason about. Let us declare a class $term$, to 156consist of all legal types of terms in our logic. The subclass structure 157is now $term\le logic$. 158 159\index{*nat type} 160We put $nat$ in class $term$ by declaring $nat{::}term$. We declare the 161equality constant by 162\begin{eqnarray*} 163 {=} & :: & [\alpha{::}term,\alpha]\To o 164\end{eqnarray*} 165where $\alpha{::}term$ constrains the type variable~$\alpha$ to class 166$term$. Such type variables resemble Standard~\ML's equality type 167variables. 168 169We give~$o$ and function types the class $logic$ rather than~$term$, since 170they are not legal types for terms. We may introduce new types of class 171$term$ --- for instance, type $string$ or $real$ --- at any time. We can 172even declare type constructors such as~$list$, and state that type 173$(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality 174applies to lists of natural numbers but not to lists of formulae. We may 175summarize this paragraph by a set of {\bf arity declarations} for type 176constructors:\index{arities!declaring} 177\begin{eqnarray*}\index{*o type}\index{*fun type} 178 o & :: & logic \\ 179 fun & :: & (logic,logic)logic \\ 180 nat, string, real & :: & term \\ 181 list & :: & (term)term 182\end{eqnarray*} 183(Recall that $fun$ is the type constructor for function types.) 184In \rmindex{higher-order logic}, equality does apply to truth values and 185functions; this requires the arity declarations ${o::term}$ 186and ${fun::(term,term)term}$. The class system can also handle 187overloading.\index{overloading|bold} We could declare $arith$ to be the 188subclass of $term$ consisting of the `arithmetic' types, such as~$nat$. 189Then we could declare the operators 190\begin{eqnarray*} 191 {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha 192\end{eqnarray*} 193If we declare new types $real$ and $complex$ of class $arith$, then we 194in effect have three sets of operators: 195\begin{eqnarray*} 196 {+},{-},{\times},{/} & :: & [nat,nat]\To nat \\ 197 {+},{-},{\times},{/} & :: & [real,real]\To real \\ 198 {+},{-},{\times},{/} & :: & [complex,complex]\To complex 199\end{eqnarray*} 200Isabelle will regard these as distinct constants, each of which can be defined 201separately. We could even introduce the type $(\alpha)vector$ and declare 202its arity as $(arith)arith$. Then we could declare the constant 203\begin{eqnarray*} 204 {+} & :: & [(\alpha)vector,(\alpha)vector]\To (\alpha)vector 205\end{eqnarray*} 206and specify it in terms of ${+} :: [\alpha,\alpha]\To \alpha$. 207 208A type variable may belong to any finite number of classes. Suppose that 209we had declared yet another class $ord \le term$, the class of all 210`ordered' types, and a constant 211\begin{eqnarray*} 212 {\le} & :: & [\alpha{::}ord,\alpha]\To o. 213\end{eqnarray*} 214In this context the variable $x$ in $x \le (x+x)$ will be assigned type 215$\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and 216$ord$. Semantically the set $\{arith,ord\}$ should be understood as the 217intersection of the sets of types represented by $arith$ and $ord$. Such 218intersections of classes are called \bfindex{sorts}. The empty 219intersection of classes, $\{\}$, contains all types and is thus the {\bf 220 universal sort}. 221 222Even with overloading, each term has a unique, most general type. For this 223to be possible, the class and type declarations must satisfy certain 224technical constraints; see 225\iflabelundefined{sec:ref-defining-theories}% 226 {Sect.\ Defining Theories in the {\em Reference Manual}}% 227 {\S\ref{sec:ref-defining-theories}}. 228 229 230\subsection{Higher types and quantifiers} 231\index{types!higher|bold}\index{quantifiers} 232Quantifiers are regarded as operations upon functions. Ignoring polymorphism 233for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges 234over type~$nat$. This is true if $P(x)$ is true for all~$x$. Abstracting 235$P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$ 236returns true for all arguments. Thus, the universal quantifier can be 237represented by a constant 238\begin{eqnarray*} 239 \forall & :: & (nat\To o) \To o, 240\end{eqnarray*} 241which is essentially an infinitary truth table. The representation of $\forall 242x. P(x)$ is $\forall(\lambda x. P(x))$. 243 244The existential quantifier is treated 245in the same way. Other binding operators are also easily handled; for 246instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as 247$\Sigma(i,j,\lambda k.f(k))$, where 248\begin{eqnarray*} 249 \Sigma & :: & [nat,nat, nat\To nat] \To nat. 250\end{eqnarray*} 251Quantifiers may be polymorphic. We may define $\forall$ and~$\exists$ over 252all legal types of terms, not just the natural numbers, and 253allow summations over all arithmetic types: 254\begin{eqnarray*} 255 \forall,\exists & :: & (\alpha{::}term\To o) \To o \\ 256 \Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha 257\end{eqnarray*} 258Observe that the index variables still have type $nat$, while the values 259being summed may belong to any arithmetic type. 260 261 262\section{Formalizing logical rules in Isabelle} 263\index{meta-implication|bold} 264\index{meta-quantifiers|bold} 265\index{meta-equality|bold} 266 267Object-logics are formalized by extending Isabelle's 268meta-logic~\cite{paulson-found}, which is intuitionistic higher-order logic. 269The meta-level connectives are {\bf implication}, the {\bf universal 270 quantifier}, and {\bf equality}. 271\begin{itemize} 272 \item The implication \(\phi\Imp \psi\) means `\(\phi\) implies 273\(\psi\)', and expresses logical {\bf entailment}. 274 275 \item The quantification \(\Forall x.\phi\) means `\(\phi\) is true for 276all $x$', and expresses {\bf generality} in rules and axiom schemes. 277 278\item The equality \(a\equiv b\) means `$a$ equals $b$', for expressing 279 {\bf definitions} (see~\S\ref{definitions}).\index{definitions} 280 Equalities left over from the unification process, so called {\bf 281 flex-flex constraints},\index{flex-flex constraints} are written $a\qeq 282 b$. The two equality symbols have the same logical meaning. 283 284\end{itemize} 285The syntax of the meta-logic is formalized in the same manner 286as object-logics, using the simply typed $\lambda$-calculus. Analogous to 287type~$o$ above, there is a built-in type $prop$ of meta-level truth values. 288Meta-level formulae will have this type. Type $prop$ belongs to 289class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$ 290and $\tau$ do. Here are the types of the built-in connectives: 291\begin{eqnarray*}\index{*prop type}\index{*logic class} 292 \Imp & :: & [prop,prop]\To prop \\ 293 \Forall & :: & (\alpha{::}logic\To prop) \To prop \\ 294 {\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\ 295 \qeq & :: & [\alpha{::}\{\},\alpha]\To prop 296\end{eqnarray*} 297The polymorphism in $\Forall$ is restricted to class~$logic$ to exclude 298certain types, those used just for parsing. The type variable 299$\alpha{::}\{\}$ ranges over the universal sort. 300 301In our formalization of first-order logic, we declared a type~$o$ of 302object-level truth values, rather than using~$prop$ for this purpose. If 303we declared the object-level connectives to have types such as 304${\neg}::prop\To prop$, then these connectives would be applicable to 305meta-level formulae. Keeping $prop$ and $o$ as separate types maintains 306the distinction between the meta-level and the object-level. To formalize 307the inference rules, we shall need to relate the two levels; accordingly, 308we declare the constant 309\index{*Trueprop constant} 310\begin{eqnarray*} 311 Trueprop & :: & o\To prop. 312\end{eqnarray*} 313We may regard $Trueprop$ as a meta-level predicate, reading $Trueprop(P)$ as 314`$P$ is true at the object-level.' Put another way, $Trueprop$ is a coercion 315from $o$ to $prop$. 316 317 318\subsection{Expressing propositional rules} 319\index{rules!propositional} 320We shall illustrate the use of the meta-logic by formalizing the rules of 321Fig.\ts\ref{fol-fig}. Each object-level rule is expressed as a meta-level 322axiom. 323 324One of the simplest rules is $(\conj E1)$. Making 325everything explicit, its formalization in the meta-logic is 326$$ 327\Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) 328$$ 329This may look formidable, but it has an obvious reading: for all object-level 330truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The 331reading is correct because the meta-logic has simple models, where 332types denote sets and $\Forall$ really means `for all.' 333 334\index{*Trueprop constant} 335Isabelle adopts notational conventions to ease the writing of rules. We may 336hide the occurrences of $Trueprop$ by making it an implicit coercion. 337Outer universal quantifiers may be dropped. Finally, the nested implication 338\index{meta-implication} 339\[ \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \] 340may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which 341formalizes a rule of $n$~premises. 342 343Using these conventions, the conjunction rules become the following axioms. 344These fully specify the properties of~$\conj$: 345$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ 346$$ P\conj Q \Imp P \qquad P\conj Q \Imp Q \eqno(\conj E1,2) $$ 347 348\noindent 349Next, consider the disjunction rules. The discharge of assumption in 350$(\disj E)$ is expressed using $\Imp$: 351\index{assumptions!discharge of}% 352$$ P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2) $$ 353$$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E) $$ 354% 355To understand this treatment of assumptions in natural 356deduction, look at implication. The rule $({\imp}I)$ is the classic 357example of natural deduction: to prove that $P\imp Q$ is true, assume $P$ 358is true and show that $Q$ must then be true. More concisely, if $P$ 359implies $Q$ (at the meta-level), then $P\imp Q$ is true (at the 360object-level). Showing the coercion explicitly, this is formalized as 361\[ (Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q). \] 362The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to 363specify $\imp$ are 364$$ (P \Imp Q) \Imp P\imp Q \eqno({\imp}I) $$ 365$$ \List{P\imp Q; P} \Imp Q. \eqno({\imp}E) $$ 366 367\noindent 368Finally, the intuitionistic contradiction rule is formalized as the axiom 369$$ \bot \Imp P. \eqno(\bot E) $$ 370 371\begin{warn} 372Earlier versions of Isabelle, and certain 373papers~\cite{paulson-found,paulson700}, use $\List{P}$ to mean $Trueprop(P)$. 374\end{warn} 375 376\subsection{Quantifier rules and substitution} 377\index{quantifiers}\index{rules!quantifier}\index{substitution|bold} 378\index{variables!bound}\index{lambda abs@$\lambda$-abstractions} 379\index{function applications} 380 381Isabelle expresses variable binding using $\lambda$-abstraction; for instance, 382$\forall x.P$ is formalized as $\forall(\lambda x.P)$. Recall that $F(t)$ 383is Isabelle's syntax for application of the function~$F$ to the argument~$t$; 384it is not a meta-notation for substitution. On the other hand, a substitution 385will take place if $F$ has the form $\lambda x.P$; Isabelle transforms 386$(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$-conversion. Thus, we can express 387inference rules that involve substitution for bound variables. 388 389\index{parameters|bold}\index{eigenvariables|see{parameters}} 390A logic may attach provisos to certain of its rules, especially quantifier 391rules. We cannot hope to formalize arbitrary provisos. Fortunately, those 392typical of quantifier rules always have the same form, namely `$x$ not free in 393\ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf 394parameter} or {\bf eigenvariable}) in some premise. Isabelle treats 395provisos using~$\Forall$, its inbuilt notion of `for all'. 396\index{meta-quantifiers} 397 398The purpose of the proviso `$x$ not free in \ldots' is 399to ensure that the premise may not make assumptions about the value of~$x$, 400and therefore holds for all~$x$. We formalize $(\forall I)$ by 401\[ \left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)). \] 402This means, `if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.' 403The $\forall E$ rule exploits $\beta$-conversion. Hiding $Trueprop$, the 404$\forall$ axioms are 405$$ \left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I) $$ 406$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E) $$ 407 408\noindent 409We have defined the object-level universal quantifier~($\forall$) 410using~$\Forall$. But we do not require meta-level counterparts of all the 411connectives of the object-logic! Consider the existential quantifier: 412$$ P(t) \Imp \exists x.P(x) \eqno(\exists I) $$ 413$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$ 414Let us verify $(\exists E)$ semantically. Suppose that the premises 415hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is 416true. Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and 417we obtain the desired conclusion, $Q$. 418 419The treatment of substitution deserves mention. The rule 420\[ \infer{P[u/t]}{t=u & P} \] 421would be hard to formalize in Isabelle. It calls for replacing~$t$ by $u$ 422throughout~$P$, which cannot be expressed using $\beta$-conversion. Our 423rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$ 424from~$P[t/x]$. When we formalize this as an axiom, the template becomes a 425function variable: 426$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst) $$ 427 428 429\subsection{Signatures and theories} 430\index{signatures|bold} 431 432A {\bf signature} contains the information necessary for type-checking, 433parsing and pretty printing a term. It specifies type classes and their 434relationships, types and their arities, constants and their types, etc. It 435also contains grammar rules, specified using mixfix declarations. 436 437Two signatures can be merged provided their specifications are compatible --- 438they must not, for example, assign different types to the same constant. 439Under similar conditions, a signature can be extended. Signatures are 440managed internally by Isabelle; users seldom encounter them. 441 442\index{theories|bold} A {\bf theory} consists of a signature plus a collection 443of axioms. The Pure theory contains only the meta-logic. Theories can be 444combined provided their signatures are compatible. A theory definition 445extends an existing theory with further signature specifications --- classes, 446types, constants and mixfix declarations --- plus lists of axioms and 447definitions etc., expressed as strings to be parsed. A theory can formalize a 448small piece of mathematics, such as lists and their operations, or an entire 449logic. A mathematical development typically involves many theories in a 450hierarchy. For example, the Pure theory could be extended to form a theory 451for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form 452a theory for natural numbers and a theory for lists; the union of these two 453could be extended into a theory defining the length of a list: 454\begin{tt} 455\[ 456\begin{array}{c@{}c@{}c@{}c@{}c} 457 {} & {} &\hbox{Pure}& {} & {} \\ 458 {} & {} & \downarrow & {} & {} \\ 459 {} & {} &\hbox{FOL} & {} & {} \\ 460 {} & \swarrow & {} & \searrow & {} \\ 461 \hbox{Nat} & {} & {} & {} & \hbox{List} \\ 462 {} & \searrow & {} & \swarrow & {} \\ 463 {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\ 464 {} & {} & \downarrow & {} & {} \\ 465 {} & {} & \hbox{Length} & {} & {} 466\end{array} 467\] 468\end{tt}% 469Each Isabelle proof typically works within a single theory, which is 470associated with the proof state. However, many different theories may 471coexist at the same time, and you may work in each of these during a single 472session. 473 474\begin{warn}\index{constants!clashes with variables}% 475 Confusing problems arise if you work in the wrong theory. Each theory 476 defines its own syntax. An identifier may be regarded in one theory as a 477 constant and in another as a variable, for example. 478\end{warn} 479 480\section{Proof construction in Isabelle} 481I have elsewhere described the meta-logic and demonstrated it by 482formalizing first-order logic~\cite{paulson-found}. There is a one-to-one 483correspondence between meta-level proofs and object-level proofs. To each 484use of a meta-level axiom, such as $(\forall I)$, there is a use of the 485corresponding object-level rule. Object-level assumptions and parameters 486have meta-level counterparts. The meta-level formalization is {\bf 487 faithful}, admitting no incorrect object-level inferences, and {\bf 488 adequate}, admitting all correct object-level inferences. These 489properties must be demonstrated separately for each object-logic. 490 491The meta-logic is defined by a collection of inference rules, including 492equational rules for the $\lambda$-calculus and logical rules. The rules 493for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in 494Fig.\ts\ref{fol-fig}. Proofs performed using the primitive meta-rules 495would be lengthy; Isabelle proofs normally use certain derived rules. 496{\bf Resolution}, in particular, is convenient for backward proof. 497 498Unification is central to theorem proving. It supports quantifier 499reasoning by allowing certain `unknown' terms to be instantiated later, 500possibly in stages. When proving that the time required to sort $n$ 501integers is proportional to~$n^2$, we need not state the constant of 502proportionality; when proving that a hardware adder will deliver the sum of 503its inputs, we need not state how many clock ticks will be required. Such 504quantities often emerge from the proof. 505 506Isabelle provides {\bf schematic variables}, or {\bf 507 unknowns},\index{unknowns} for unification. Logically, unknowns are free 508variables. But while ordinary variables remain fixed, unification may 509instantiate unknowns. Unknowns are written with a ?\ prefix and are 510frequently subscripted: $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots, 511$\Var{P}$, $\Var{P@1}$, \ldots. 512 513Recall that an inference rule of the form 514\[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \] 515is formalized in Isabelle's meta-logic as the axiom 516$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.\index{resolution} 517Such axioms resemble Prolog's Horn clauses, and can be combined by 518resolution --- Isabelle's principal proof method. Resolution yields both 519forward and backward proof. Backward proof works by unifying a goal with 520the conclusion of a rule, whose premises become new subgoals. Forward proof 521works by unifying theorems with the premises of a rule, deriving a new theorem. 522 523Isabelle formulae require an extended notion of resolution. 524They differ from Horn clauses in two major respects: 525\begin{itemize} 526 \item They are written in the typed $\lambda$-calculus, and therefore must be 527resolved using higher-order unification. 528 529\item The constituents of a clause need not be atomic formulae. Any 530 formula of the form $Trueprop(\cdots)$ is atomic, but axioms such as 531 ${\imp}I$ and $\forall I$ contain non-atomic formulae. 532\end{itemize} 533Isabelle has little in common with classical resolution theorem provers 534such as Otter~\cite{wos-bledsoe}. At the meta-level, Isabelle proves 535theorems in their positive form, not by refutation. However, an 536object-logic that includes a contradiction rule may employ a refutation 537proof procedure. 538 539 540\subsection{Higher-order unification} 541\index{unification!higher-order|bold} 542Unification is equation solving. The solution of $f(\Var{x},c) \qeq 543f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$. {\bf 544Higher-order unification} is equation solving for typed $\lambda$-terms. 545To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$. 546That is easy --- in the typed $\lambda$-calculus, all reduction sequences 547terminate at a normal form. But it must guess the unknown 548function~$\Var{f}$ in order to solve the equation 549\begin{equation} \label{hou-eqn} 550 \Var{f}(t) \qeq g(u@1,\ldots,u@k). 551\end{equation} 552Huet's~\cite{huet75} search procedure solves equations by imitation and 553projection. {\bf Imitation} makes~$\Var{f}$ apply the leading symbol (if a 554constant) of the right-hand side. To solve equation~(\ref{hou-eqn}), it 555guesses 556\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \] 557where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns. Assuming there are no 558other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the 559set of equations 560\[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \] 561If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots, 562$\Var{h@k}$, then it yields an instantiation for~$\Var{f}$. 563 564{\bf Projection} makes $\Var{f}$ apply one of its arguments. To solve 565equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a 566result of suitable type, it guesses 567\[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \] 568where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no 569other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the 570equation 571\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). \] 572 573\begin{warn}\index{unification!incompleteness of}% 574Huet's unification procedure is complete. Isabelle's polymorphic version, 575which solves for type unknowns as well as for term unknowns, is incomplete. 576The problem is that projection requires type information. In 577equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections 578are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be 579similarly unconstrained. Therefore, Isabelle never attempts such 580projections, and may fail to find unifiers where a type unknown turns out 581to be a function type. 582\end{warn} 583 584\index{unknowns!function|bold} 585Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to 586$n+1$ guesses. The search tree and set of unifiers may be infinite. But 587higher-order unification can work effectively, provided you are careful 588with {\bf function unknowns}: 589\begin{itemize} 590 \item Equations with no function unknowns are solved using first-order 591unification, extended to treat bound variables. For example, $\lambda x.x 592\qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would 593capture the free variable~$x$. 594 595 \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are 596distinct bound variables, causes no difficulties. Its projections can only 597match the corresponding variables. 598 599 \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right. It has 600four solutions, but Isabelle evaluates them lazily, trying projection before 601imitation. The first solution is usually the one desired: 602\[ \Var{f}\equiv \lambda x. x+x \quad 603 \Var{f}\equiv \lambda x. a+x \quad 604 \Var{f}\equiv \lambda x. x+a \quad 605 \Var{f}\equiv \lambda x. a+a \] 606 \item Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and 607$\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be 608avoided. 609\end{itemize} 610In problematic cases, you may have to instantiate some unknowns before 611invoking unification. 612 613 614\subsection{Joining rules by resolution} \label{joining} 615\index{resolution|bold} 616Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots; 617\phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules. 618Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a 619higher-order unifier. Writing $Xs$ for the application of substitution~$s$ to 620expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$. 621By resolution, we may conclude 622\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m; 623 \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. 624\] 625The substitution~$s$ may instantiate unknowns in both rules. In short, 626resolution is the following rule: 627\[ \infer[(\psi s\equiv \phi@i s)] 628 {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m; 629 \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s} 630 {\List{\psi@1; \ldots; \psi@m} \Imp \psi & & 631 \List{\phi@1; \ldots; \phi@n} \Imp \phi} 632\] 633It operates at the meta-level, on Isabelle theorems, and is justified by 634the properties of $\Imp$ and~$\Forall$. It takes the number~$i$ (for 635$1\leq i\leq n$) as a parameter and may yield infinitely many conclusions, 636one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these 637conclusions as a sequence (lazy list). 638 639Resolution expects the rules to have no outer quantifiers~($\Forall$). 640It may rename or instantiate any schematic variables, but leaves free 641variables unchanged. When constructing a theory, Isabelle puts the 642rules into a standard form with all free variables converted into 643schematic ones; for instance, $({\imp}E)$ becomes 644\[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}. 645\] 646When resolving two rules, the unknowns in the first rule are renamed, by 647subscripting, to make them distinct from the unknowns in the second rule. To 648resolve $({\imp}E)$ with itself, the first copy of the rule becomes 649\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}. \] 650Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with 651$\Var{P}\imp \Var{Q}$, is the meta-level inference 652\[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}} 653 \Imp\Var{Q}.} 654 {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1} & & 655 \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}} 656\] 657Renaming the unknowns in the resolvent, we have derived the 658object-level rule\index{rules!derived} 659\[ \infer{Q.}{R\imp (P\imp Q) & R & P} \] 660Joining rules in this fashion is a simple way of proving theorems. The 661derived rules are conservative extensions of the object-logic, and may permit 662simpler proofs. Let us consider another example. Suppose we have the axiom 663$$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$ 664 665\noindent 666The standard form of $(\forall E)$ is 667$\forall x.\Var{P}(x) \Imp \Var{P}(\Var{t})$. 668Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by 669$\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$ 670unchanged, yielding 671\[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \] 672Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$ 673and yields 674\[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \] 675Resolving this with $({\imp}E)$ increases the subscripts and yields 676\[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}. 677\] 678We have derived the rule 679\[ \infer{m=n,}{Suc(m)=Suc(n)} \] 680which goes directly from $Suc(m)=Suc(n)$ to $m=n$. It is handy for simplifying 681an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$. 682 683 684\section{Lifting a rule into a context} 685The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for 686resolution. They have non-atomic premises, namely $P\Imp Q$ and $\Forall 687x.P(x)$, while the conclusions of all the rules are atomic (they have the form 688$Trueprop(\cdots)$). Isabelle gets round the problem through a meta-inference 689called \bfindex{lifting}. Let us consider how to construct proofs such as 690\[ \infer[({\imp}I)]{P\imp(Q\imp R)} 691 {\infer[({\imp}I)]{Q\imp R} 692 {\infer*{R}{[P,Q]}}} 693 \qquad 694 \infer[(\forall I)]{\forall x\,y.P(x,y)} 695 {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}} 696\] 697 698\subsection{Lifting over assumptions} 699\index{assumptions!lifting over} 700Lifting over $\theta\Imp{}$ is the following meta-inference rule: 701\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp 702 (\theta \Imp \phi)} 703 {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \] 704This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and 705$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$ and $\theta$ are all true then 706$\phi$ must be true. Iterated lifting over a series of meta-formulae 707$\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is 708$\List{\theta@1; \ldots; \theta@k} \Imp \phi$. Typically the $\theta@i$ are 709the assumptions in a natural deduction proof; lifting copies them into a rule's 710premises and conclusion. 711 712When resolving two rules, Isabelle lifts the first one if necessary. The 713standard form of $({\imp}I)$ is 714\[ (\Var{P} \Imp \Var{Q}) \Imp \Var{P}\imp \Var{Q}. \] 715To resolve this rule with itself, Isabelle modifies one copy as follows: it 716renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over 717$\Var{P}\Imp{}$ to obtain 718\[ (\Var{P}\Imp (\Var{P@1} \Imp \Var{Q@1})) \Imp (\Var{P} \Imp 719 (\Var{P@1}\imp \Var{Q@1})). \] 720Using the $\List{\cdots}$ abbreviation, this can be written as 721\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} 722 \Imp \Var{P@1}\imp \Var{Q@1}. \] 723Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp 724\Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$. 725Resolution yields 726\[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp 727\Var{P}\imp(\Var{P@1}\imp\Var{Q@1}). \] 728This represents the derived rule 729\[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \] 730 731\subsection{Lifting over parameters} 732\index{parameters!lifting over} 733An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. 734Here, lifting prefixes an object-rule's premises and conclusion with $\Forall 735x$. At the same time, lifting introduces a dependence upon~$x$. It replaces 736each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new 737unknown (by subscripting) of suitable type --- necessarily a function type. In 738short, lifting is the meta-inference 739\[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x} 740 \Imp \Forall x.\phi^x,} 741 {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \] 742% 743where $\phi^x$ stands for the result of lifting unknowns over~$x$ in 744$\phi$. It is not hard to verify that this meta-inference is sound. If 745$\phi\Imp\psi$ then $\phi^x\Imp\psi^x$ for all~$x$; so if $\phi^x$ is true 746for all~$x$ then so is $\psi^x$. Thus, from $\phi\Imp\psi$ we conclude 747$(\Forall x.\phi^x) \Imp (\Forall x.\psi^x)$. 748 749For example, $(\disj I)$ might be lifted to 750\[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\] 751and $(\forall I)$ to 752\[ (\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)). \] 753Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$, 754avoiding a clash. Resolving the above with $(\forall I)$ is the meta-inference 755\[ \infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) } 756 {(\Forall x\,y.\Var{P@1}(x,y)) \Imp 757 (\Forall x. \forall y.\Var{P@1}(x,y)) & 758 (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \] 759Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the 760resolvent expresses the derived rule 761\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} } 762 \quad\hbox{provided $x$, $y$ not free in the assumptions} 763\] 764I discuss lifting and parameters at length elsewhere~\cite{paulson-found}. 765Miller goes into even greater detail~\cite{miller-mixed}. 766 767 768\section{Backward proof by resolution} 769\index{resolution!in backward proof} 770 771Resolution is convenient for deriving simple rules and for reasoning 772forward from facts. It can also support backward proof, where we start 773with a goal and refine it to progressively simpler subgoals until all have 774been solved. {\sc lcf} and its descendants {\sc hol} and Nuprl provide 775tactics and tacticals, which constitute a sophisticated language for 776expressing proof searches. {\bf Tactics} refine subgoals while {\bf 777 tacticals} combine tactics. 778 779\index{LCF system} 780Isabelle's tactics and tacticals work differently from {\sc lcf}'s. An 781Isabelle rule is bidirectional: there is no distinction between 782inputs and outputs. {\sc lcf} has a separate tactic for each rule; 783Isabelle performs refinement by any rule in a uniform fashion, using 784resolution. 785 786Isabelle works with meta-level theorems of the form 787\( \List{\phi@1; \ldots; \phi@n} \Imp \phi \). 788We have viewed this as the {\bf rule} with premises 789$\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$. It can also be viewed as 790the {\bf proof state}\index{proof state} 791with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main 792goal~$\phi$. 793 794To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof 795state. This assertion is, trivially, a theorem. At a later stage in the 796backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n} 797\Imp \phi$. This proof state is a theorem, ensuring that the subgoals 798$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$. If $n=0$ then we have 799proved~$\phi$ outright. If $\phi$ contains unknowns, they may become 800instantiated during the proof; a proof state may be $\List{\phi@1; \ldots; 801\phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$. 802 803\subsection{Refinement by resolution} 804To refine subgoal~$i$ of a proof state by a rule, perform the following 805resolution: 806\[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \] 807Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after 808lifting over subgoal~$i$'s assumptions and parameters. If the proof state 809is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is 810(for~$1\leq i\leq n$) 811\[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1; 812 \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \] 813Substitution~$s$ unifies $\psi'$ with~$\phi@i$. In the proof state, 814subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises. 815If some of the rule's unknowns are left un-instantiated, they become new 816unknowns in the proof state. Refinement by~$(\exists I)$, namely 817\[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \] 818inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting. 819We do not have to specify an `existential witness' when 820applying~$(\exists I)$. Further resolutions may instantiate unknowns in 821the proof state. 822 823\subsection{Proof by assumption} 824\index{assumptions!use of} 825In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and 826assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for 827each subgoal. Repeated lifting steps can lift a rule into any context. To 828aid readability, Isabelle puts contexts into a normal form, gathering the 829parameters at the front: 830\begin{equation} \label{context-eqn} 831\Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta. 832\end{equation} 833Under the usual reading of the connectives, this expresses that $\theta$ 834follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary 835$x@1$,~\ldots,~$x@l$. It is trivially true if $\theta$ equals any of 836$\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them. This 837models proof by assumption in natural deduction. 838 839Isabelle automates the meta-inference for proof by assumption. Its arguments 840are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$ 841from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}). Its results 842are meta-theorems of the form 843\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s \] 844for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$ 845with $\lambda x@1 \ldots x@l. \theta$. Isabelle supplies the parameters 846$x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which 847regards them as unique constants with a limited scope --- this enforces 848parameter provisos~\cite{paulson-found}. 849 850The premise represents a proof state with~$n$ subgoals, of which the~$i$th 851is to be solved by assumption. Isabelle searches the subgoal's context for 852an assumption~$\theta@j$ that can solve it. For each unifier, the 853meta-inference returns an instantiated proof state from which the $i$th 854subgoal has been removed. Isabelle searches for a unifying assumption; for 855readability and robustness, proofs do not refer to assumptions by number. 856 857Consider the proof state 858\[ (\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x}). \] 859Proof by assumption (with $i=1$, the only possibility) yields two results: 860\begin{itemize} 861 \item $Q(a)$, instantiating $\Var{x}\equiv a$ 862 \item $Q(b)$, instantiating $\Var{x}\equiv b$ 863\end{itemize} 864Here, proof by assumption affects the main goal. It could also affect 865other subgoals; if we also had the subgoal ${\List{P(b); P(c)} \Imp 866 P(\Var{x})}$, then $\Var{x}\equiv a$ would transform it to ${\List{P(b); 867 P(c)} \Imp P(a)}$, which might be unprovable. 868 869 870\subsection{A propositional proof} \label{prop-proof} 871\index{examples!propositional} 872Our first example avoids quantifiers. Given the main goal $P\disj P\imp 873P$, Isabelle creates the initial state 874\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \] 875% 876Bear in mind that every proof state we derive will be a meta-theorem, 877expressing that the subgoals imply the main goal. Our aim is to reach the 878state $P\disj P\imp P$; this meta-theorem is the desired result. 879 880The first step is to refine subgoal~1 by (${\imp}I)$, creating a new state 881where $P\disj P$ is an assumption: 882\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \] 883The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. 884Because of lifting, each subgoal contains a copy of the context --- the 885assumption $P\disj P$. (In fact, this assumption is now redundant; we shall 886shortly see how to get rid of it!) The new proof state is the following 887meta-theorem, laid out for clarity: 888\[ \begin{array}{l@{}l@{\qquad\qquad}l} 889 \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\ 890 & \List{P\disj P; \Var{P@1}} \Imp P; & \hbox{(subgoal 2)} \\ 891 & \List{P\disj P; \Var{Q@1}} \Imp P & \hbox{(subgoal 3)} \\ 892 \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)} 893 \end{array} 894\] 895Notice the unknowns in the proof state. Because we have applied $(\disj E)$, 896we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$. Of course, 897subgoal~1 is provable by assumption. This instantiates both $\Var{P@1}$ and 898$\Var{Q@1}$ to~$P$ throughout the proof state: 899\[ \begin{array}{l@{}l@{\qquad\qquad}l} 900 \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\ 901 & \List{P\disj P; P} \Imp P & \hbox{(subgoal 2)} \\ 902 \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)} 903 \end{array} \] 904Both of the remaining subgoals can be proved by assumption. After two such 905steps, the proof state is $P\disj P\imp P$. 906 907 908\subsection{A quantifier proof} 909\index{examples!with quantifiers} 910To illustrate quantifiers and $\Forall$-lifting, let us prove 911$(\exists x.P(f(x)))\imp(\exists x.P(x))$. The initial proof 912state is the trivial meta-theorem 913\[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp 914 (\exists x.P(f(x)))\imp(\exists x.P(x)). \] 915As above, the first step is refinement by (${\imp}I)$: 916\[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp 917 (\exists x.P(f(x)))\imp(\exists x.P(x)) 918\] 919The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals. 920Both have the assumption $\exists x.P(f(x))$. The new proof 921state is the meta-theorem 922\[ \begin{array}{l@{}l@{\qquad\qquad}l} 923 \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\ 924 & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp 925 \exists x.P(x) & \hbox{(subgoal 2)} \\ 926 \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) & \hbox{(main goal)} 927 \end{array} 928\] 929The unknown $\Var{P@1}$ appears in both subgoals. Because we have applied 930$(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may 931become any formula possibly containing~$x$. Proving subgoal~1 by assumption 932instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$: 933\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 934 \exists x.P(x)\right) 935 \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 936\] 937The next step is refinement by $(\exists I)$. The rule is lifted into the 938context of the parameter~$x$ and the assumption $P(f(x))$. This copies 939the context to the subgoal and allows the existential witness to 940depend upon~$x$: 941\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 942 P(\Var{x@2}(x))\right) 943 \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) 944\] 945The existential witness, $\Var{x@2}(x)$, consists of an unknown 946applied to a parameter. Proof by assumption unifies $\lambda x.P(f(x))$ 947with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$. The final 948proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$. 949 950 951\subsection{Tactics and tacticals} 952\index{tactics|bold}\index{tacticals|bold} 953{\bf Tactics} perform backward proof. Isabelle tactics differ from those 954of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states, 955rather than on individual subgoals. An Isabelle tactic is a function that 956takes a proof state and returns a sequence (lazy list) of possible 957successor states. Lazy lists are coded in ML as functions, a standard 958technique~\cite{paulson-ml2}. Isabelle represents proof states by theorems. 959 960Basic tactics execute the meta-rules described above, operating on a 961given subgoal. The {\bf resolution tactics} take a list of rules and 962return next states for each combination of rule and unifier. The {\bf 963assumption tactic} examines the subgoal's assumptions and returns next 964states for each combination of assumption and unifier. Lazy lists are 965essential because higher-order resolution may return infinitely many 966unifiers. If there are no matching rules or assumptions then no next 967states are generated; a tactic application that returns an empty list is 968said to {\bf fail}. 969 970Sequences realize their full potential with {\bf tacticals} --- operators 971for combining tactics. Depth-first search, breadth-first search and 972best-first search (where a heuristic function selects the best state to 973explore) return their outcomes as a sequence. Isabelle provides such 974procedures in the form of tacticals. Simpler procedures can be expressed 975directly using the basic tacticals {\tt THEN}, {\tt ORELSE} and {\tt REPEAT}: 976\begin{ttdescription} 977\item[$tac1$ THEN $tac2$] is a tactic for sequential composition. Applied 978to a proof state, it returns all states reachable in two steps by applying 979$tac1$ followed by~$tac2$. 980 981\item[$tac1$ ORELSE $tac2$] is a choice tactic. Applied to a state, it 982tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$. 983 984\item[REPEAT $tac$] is a repetition tactic. Applied to a state, it 985returns all states reachable by applying~$tac$ as long as possible --- until 986it would fail. 987\end{ttdescription} 988For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving 989$tac1$ priority: 990\begin{center} \tt 991REPEAT($tac1$ ORELSE $tac2$) 992\end{center} 993 994 995\section{Variations on resolution} 996In principle, resolution and proof by assumption suffice to prove all 997theorems. However, specialized forms of resolution are helpful for working 998with elimination rules. Elim-resolution applies an elimination rule to an 999assumption; destruct-resolution is similar, but applies a rule in a forward 1000style. 1001 1002The last part of the section shows how the techniques for proving theorems 1003can also serve to derive rules. 1004 1005\subsection{Elim-resolution} 1006\index{elim-resolution|bold}\index{assumptions!deleting} 1007 1008Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By 1009$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$. 1010Applying $(\disj E)$ to this assumption yields two subgoals, one that 1011assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj 1012R)\disj R$. This subgoal admits another application of $(\disj E)$. Since 1013natural deduction never discards assumptions, we eventually generate a 1014subgoal containing much that is redundant: 1015\[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \] 1016In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new 1017subgoals with the additional assumption $P$ or~$Q$. In these subgoals, 1018$P\disj Q$ is redundant. Other elimination rules behave 1019similarly. In first-order logic, only universally quantified 1020assumptions are sometimes needed more than once --- say, to prove 1021$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$. 1022 1023Many logics can be formulated as sequent calculi that delete redundant 1024assumptions after use. The rule $(\disj E)$ might become 1025\[ \infer[\disj\hbox{-left}] 1026 {\Gamma,P\disj Q,\Delta \turn \Theta} 1027 {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta} \] 1028In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$ 1029(that is, as an assumption) splits into two subgoals, replacing $P\disj Q$ 1030by $P$ or~$Q$. But the sequent calculus, with its explicit handling of 1031assumptions, can be tiresome to use. 1032 1033Elim-resolution is Isabelle's way of getting sequent calculus behaviour 1034from natural deduction rules. It lets an elimination rule consume an 1035assumption. Elim-resolution combines two meta-theorems: 1036\begin{itemize} 1037 \item a rule $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ 1038 \item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ 1039\end{itemize} 1040The rule must have at least one premise, thus $m>0$. Write the rule's 1041lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$. Suppose we 1042wish to change subgoal number~$i$. 1043 1044Ordinary resolution would attempt to reduce~$\phi@i$, 1045replacing subgoal~$i$ by $m$ new ones. Elim-resolution tries 1046simultaneously to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it 1047returns a sequence of next states. Each of these replaces subgoal~$i$ by 1048instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected 1049assumption has been deleted. Suppose $\phi@i$ has the parameter~$x$ and 1050assumptions $\theta@1$,~\ldots,~$\theta@k$. Then $\psi'@1$, the rule's first 1051premise after lifting, will be 1052\( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \). 1053Elim-resolution tries to unify $\psi'\qeq\phi@i$ and 1054$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$ simultaneously, for 1055$j=1$,~\ldots,~$k$. 1056 1057Let us redo the example from~\S\ref{prop-proof}. The elimination rule 1058is~$(\disj E)$, 1059\[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}} 1060 \Imp \Var{R} \] 1061and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$. The 1062lifted rule is 1063\[ \begin{array}{l@{}l} 1064 \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\ 1065 & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\ 1066 & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1} \\ 1067 \rbrakk\;& \Imp (P\disj P \Imp \Var{R@1}) 1068 \end{array} 1069\] 1070Unification takes the simultaneous equations 1071$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding 1072$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state 1073is simply 1074\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). 1075\] 1076Elim-resolution's simultaneous unification gives better control 1077than ordinary resolution. Recall the substitution rule: 1078$$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u}) 1079\eqno(subst) $$ 1080Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many 1081unifiers, $(subst)$ works well with elim-resolution. It deletes some 1082assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal 1083formula. The simultaneous unification instantiates $\Var{u}$ to~$y$; if 1084$y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another 1085formula. 1086 1087In logical parlance, the premise containing the connective to be eliminated 1088is called the \bfindex{major premise}. Elim-resolution expects the major 1089premise to come first. The order of the premises is significant in 1090Isabelle. 1091 1092\subsection{Destruction rules} \label{destruct} 1093\index{rules!destruction}\index{rules!elimination} 1094\index{forward proof} 1095 1096Looking back to Fig.\ts\ref{fol-fig}, notice that there are two kinds of 1097elimination rule. The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and 1098$({\forall}E)$ extract the conclusion from the major premise. In Isabelle 1099parlance, such rules are called {\bf destruction rules}; they are readable 1100and easy to use in forward proof. The rules $({\disj}E)$, $({\bot}E)$ and 1101$({\exists}E)$ work by discharging assumptions; they support backward proof 1102in a style reminiscent of the sequent calculus. 1103 1104The latter style is the most general form of elimination rule. In natural 1105deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or 1106$({\exists}E)$ as destruction rules. But we can write general elimination 1107rules for $\conj$, $\imp$ and~$\forall$: 1108\[ 1109\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad 1110\infer{R}{P\imp Q & P & \infer*{R}{[Q]}} \qquad 1111\infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}} 1112\] 1113Because they are concise, destruction rules are simpler to derive than the 1114corresponding elimination rules. To facilitate their use in backward 1115proof, Isabelle provides a means of transforming a destruction rule such as 1116\[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} 1117 \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} 1118\] 1119{\bf Destruct-resolution}\index{destruct-resolution} combines this 1120transformation with elim-resolution. It applies a destruction rule to some 1121assumption of a subgoal. Given the rule above, it replaces the 1122assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$, 1123\ldots,~$P@m$. Destruct-resolution works forward from a subgoal's 1124assumptions. Ordinary resolution performs forward reasoning from theorems, 1125as illustrated in~\S\ref{joining}. 1126 1127 1128\subsection{Deriving rules by resolution} \label{deriving} 1129\index{rules!derived|bold}\index{meta-assumptions!syntax of} 1130The meta-logic, itself a form of the predicate calculus, is defined by a 1131system of natural deduction rules. Each theorem may depend upon 1132meta-assumptions. The theorem that~$\phi$ follows from the assumptions 1133$\phi@1$, \ldots, $\phi@n$ is written 1134\[ \phi \quad [\phi@1,\ldots,\phi@n]. \] 1135A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$, 1136but Isabelle's notation is more readable with large formulae. 1137 1138Meta-level natural deduction provides a convenient mechanism for deriving 1139new object-level rules. To derive the rule 1140\[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \] 1141assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the 1142meta-level. Then prove $\phi$, possibly using these assumptions. 1143Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate, 1144reaching a final state such as 1145\[ \phi \quad [\theta@1,\ldots,\theta@k]. \] 1146The meta-rule for $\Imp$ introduction discharges an assumption. 1147Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the 1148meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no 1149assumptions. This represents the desired rule. 1150Let us derive the general $\conj$ elimination rule: 1151$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E) $$ 1152We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in 1153the state $R\Imp R$. Resolving this with the second assumption yields the 1154state 1155\[ \phantom{\List{P\conj Q;\; P\conj Q}} 1156 \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \] 1157Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$, 1158respectively, yields the state 1159\[ \List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R 1160 \quad [\,\List{P;Q}\Imp R\,]. 1161\] 1162The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained 1163subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$. Resolving 1164both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield 1165\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \] 1166The proof may use the meta-assumptions in any order, and as often as 1167necessary; when finished, we discharge them in the correct order to 1168obtain the desired form: 1169\[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \] 1170We have derived the rule using free variables, which prevents their 1171premature instantiation during the proof; we may now replace them by 1172schematic variables. 1173 1174\begin{warn} 1175 Schematic variables are not allowed in meta-assumptions, for a variety of 1176 reasons. Meta-assumptions remain fixed throughout a proof. 1177\end{warn} 1178 1179