105

1 
%% $Id$


2 
\part{Foundations}


3 
This Part presents Isabelle's logical foundations in detail:


4 
representing logical syntax in the typed $\lambda$calculus; expressing


5 
inference rules in Isabelle's metalogic; combining rules by resolution.


6 
Readers wishing to use Isabelle immediately may prefer to skip straight to


7 
Part~II, using this Part (via the index) for reference only.


8 


9 
\begin{figure}


10 
\begin{eqnarray*}


11 
\neg P & \hbox{abbreviates} & P\imp\bot \\


12 
P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P)


13 
\end{eqnarray*}


14 
\vskip 4ex


15 


16 
\(\begin{array}{c@{\qquad\qquad}c}


17 
\infer[({\conj}I)]{P\conj Q}{P & Q} &


18 
\infer[({\conj}E1)]{P}{P\conj Q} \qquad


19 
\infer[({\conj}E2)]{Q}{P\conj Q} \\[4ex]


20 


21 
\infer[({\disj}I1)]{P\disj Q}{P} \qquad


22 
\infer[({\disj}I2)]{P\disj Q}{Q} &


23 
\infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex]


24 


25 
\infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} &


26 
\infer[({\imp}E)]{Q}{P\imp Q & P} \\[4ex]


27 


28 
&


29 
\infer[({\bot}E)]{P}{\bot}\\[4ex]


30 


31 
\infer[({\forall}I)*]{\forall x.P}{P} &


32 
\infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex]


33 


34 
\infer[({\exists}I)]{\exists x.P}{P[t/x]} &


35 
\infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex]


36 


37 
{t=t} \,(refl) & \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}}


38 
\end{array} \)


39 


40 
\bigskip\bigskip


41 
*{\em Eigenvariable conditions\/}:


42 


43 
$\forall I$: provided $x$ is not free in the assumptions


44 


45 
$\exists E$: provided $x$ is not free in $Q$ or any assumption except $P$


46 
\caption{Intuitionistic firstorder logic} \label{folfig}


47 
\end{figure}


48 


49 
\section{Formalizing logical syntax in Isabelle}


50 
\index{Isabelle!formalizing syntaxbold}


51 
Figure~\ref{folfig} presents intuitionistic firstorder logic,


52 
including equality and the natural numbers. Let us see how to formalize


53 
this logic in Isabelle, illustrating the main features of Isabelle's


54 
polymorphic metalogic.


55 


56 
Isabelle represents syntax using the typed $\lambda$calculus. We declare


57 
a type for each syntactic category of the logic. We declare a constant for


58 
each symbol of the logic, giving each $n$ary operation an $n$argument


59 
curried function type. Most importantly, $\lambda$abstraction represents


60 
variable binding in quantifiers.


61 


62 
\index{$\To$bold}\index{types}


63 
Isabelle has \MLstyle type constructors such as~$(\alpha)list$, where


64 
$(bool)list$ is the type of lists of booleans. Function types have the


65 
form $\sigma\To\tau$, where $\sigma$ and $\tau$ are types. Functions


66 
taking $n$~arguments require curried function types; we may abbreviate


67 
\[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad


68 
[\sigma@1, \ldots, \sigma@n] \To \tau. $$


69 


70 
The syntax for terms is summarised below. Note that function application is


71 
written $t(u)$ rather than the usual $t\,u$.


72 
\[


73 
\begin{array}{ll}


74 
t :: \sigma & \hbox{type constraint, on a term or variable} \\


75 
\lambda x.t & \hbox{abstraction} \\


76 
\lambda x@1\ldots x@n.t


77 
& \hbox{curried abstraction, $\lambda x@1. \ldots \lambda x@n.t$} \\


78 
t(u) & \hbox{application} \\


79 
t (u@1, \ldots, u@n) & \hbox{curried application, $t(u@1)\ldots(u@n)$}


80 
\end{array}


81 
\]


82 


83 


84 
\subsection{Simple types and constants}


85 
\index{types!simplebold}


86 
The syntactic categories of our logic (Figure~\ref{folfig}) are


87 
{\bf formulae} and {\bf terms}. Formulae denote truth


88 
values, so (following logical tradition) we call their type~$o$. Terms can


89 
be constructed using~0 and~$Suc$, requiring a type~$nat$ of natural


90 
numbers. Later, we shall see how to admit terms of other types.


91 


92 
After declaring the types~$o$ and~$nat$, we may declare constants for the


93 
symbols of our logic. Since $\bot$ denotes a truth value (falsity) and 0


94 
denotes a number, we put \begin{eqnarray*}


95 
\bot & :: & o \\


96 
0 & :: & nat.


97 
\end{eqnarray*}


98 
If a symbol requires operands, the corresponding constant must have a


99 
function type. In our logic, the successor function


100 
($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a


101 
function from truth values to truth values, and the binary connectives are


102 
curried functions taking two truth values as arguments:


103 
\begin{eqnarray*}


104 
Suc & :: & nat\To nat \\


105 
{\neg} & :: & o\To o \\


106 
\conj,\disj,\imp,\bimp & :: & [o,o]\To o


107 
\end{eqnarray*}


108 


109 
Isabelle allows us to declare the binary connectives as infixes, with


110 
appropriate precedences, so that we write $P\conj Q\disj R$ instead of


111 
$\disj(\conj(P,Q), R)$.


112 


113 


114 
\subsection{Polymorphic types and constants} \label{polymorphic}


115 
\index{types!polymorphicbold}


116 
Which type should we assign to the equality symbol? If we tried


117 
$[nat,nat]\To o$, then equality would be restricted to the natural


118 
numbers; we would have to declare different equality symbols for each


119 
type. Isabelle's type system is polymorphic, so we could declare


120 
\begin{eqnarray*}


121 
{=} & :: & [\alpha,\alpha]\To o.


122 
\end{eqnarray*}


123 
But this is also wrong. The declaration is too polymorphic; $\alpha$


124 
ranges over all types, including~$o$ and $nat\To nat$. Thus, it admits


125 
$\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in


126 
higherorder logic but not in firstorder logic.


127 


128 
Isabelle's \bfindex{classes} control polymorphism. Each type variable


129 
belongs to a class, which denotes a set of types. Classes are partially


130 
ordered by the subclass relation, which is essentially the subset relation


131 
on the sets of types. They closely resemble the classes of the functional


132 
language Haskell~\cite{haskelltutorial,haskellreport}. Nipkow and


133 
Prehofer discuss type inference for type classes~\cite{nipkowprehofer}.


134 


135 
Isabelle provides the builtin class $logic$, which consists of the logical


136 
types: the ones we want to reason about. Let us declare a class $term$, to


137 
consist of all legal types of terms in our logic. The subclass structure


138 
is now $term\le logic$.


139 


140 
We declare $nat$ to be in class $term$. Type variables of class~$term$


141 
should resemble Standard~\ML's equality type variables, which range over


142 
those types that possess an equality test. Thus, we declare the equality


143 
constant by


144 
\begin{eqnarray*}


145 
{=} & :: & [\alpha{::}term,\alpha]\To o


146 
\end{eqnarray*}


147 
We give function types and~$o$ the class $logic$ rather than~$term$, since


148 
they are not legal types for terms. We may introduce new types of class


149 
$term$  for instance, type $string$ or $real$  at any time. We can


150 
even declare type constructors such as $(\alpha)list$, and state that type


151 
$(\sigma)list$ belongs to class~$term$ provided $\sigma$ does; equality


152 
applies to lists of natural numbers but not to lists of formulae. We may


153 
summarize this paragraph by a set of {\bf arity declarations} for type


154 
constructors:


155 
\index{$\To$bold}\index{arities!declaring}


156 
\begin{eqnarray*}


157 
o & :: & logic \\


158 
{\To} & :: & (logic,logic)logic \\


159 
nat, string, real & :: & term \\


160 
list & :: & (term)term


161 
\end{eqnarray*}


162 
Higherorder logic, where equality does apply to truth values and


163 
functions, would require different arity declarations, namely ${o::term}$


164 
and ${{\To}::(term,term)term}$. The class system can also handle


165 
overloading.\index{overloadingbold} We could declare $arith$ to be the


166 
subclass of $term$ consisting of the `arithmetic' types, such as~$nat$.


167 
Then we could declare the operators


168 
\begin{eqnarray*}


169 
{+},{},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha


170 
\end{eqnarray*}


171 
If we declare new types $real$ and $complex$ of class $arith$, then we


172 
effectively have three sets of operators:


173 
\begin{eqnarray*}


174 
{+},{},{\times},{/} & :: & [nat,nat]\To nat \\


175 
{+},{},{\times},{/} & :: & [real,real]\To real \\


176 
{+},{},{\times},{/} & :: & [complex,complex]\To complex


177 
\end{eqnarray*}


178 
Isabelle will regard these as distinct constants, each of which can be defined


179 
separately. We could even introduce the type $(\alpha)vector$, make


180 
$(\sigma)vector$ belong to $arith$ provided $\sigma$ is in $arith$, and define


181 
\begin{eqnarray*}


182 
{+} & :: & [(\sigma)vector,(\sigma)vector]\To (\sigma)vector


183 
\end{eqnarray*}


184 
in terms of ${+} :: [\sigma,\sigma]\To \sigma$.


185 


186 
Although we have pretended so far that a type variable belongs to only one


187 
class  Isabelle's concrete syntax helps to uphold this illusion  it


188 
may in fact belong to any finite number of classes. For example suppose


189 
that we had declared yet another class $ord \le term$, the class of all


190 
`ordered' types, and a constant


191 
\begin{eqnarray*}


192 
{\le} & :: & [\alpha{::}ord,\alpha]\To o.


193 
\end{eqnarray*}


194 
In this context the variable $x$ in $x \le (x+x)$ will be assigned type


195 
$\alpha{::}\{arith,ord\}$, i.e.\ $\alpha$ belongs to both $arith$ and $ord$.


196 
Semantically the set $\{arith,ord\}$ should be understood


197 
as the intersection of the sets of types represented by $arith$ and $ord$.


198 
Such intersections of classes are called \bfindex{sorts}. The empty


199 
intersection of classes, $\{\}$, contains all types and is thus the


200 
{\bf universal sort}.


201 


202 
The type checker handles overloading, assigning each term a unique type. For


203 
this to be possible, the class and type declarations must satisfy certain


204 
technical constraints~\cite{nipkowprehofer}.


205 


206 
\subsection{Higher types and quantifiers}


207 
\index{types!higherbold}


208 
Quantifiers are regarded as operations upon functions. Ignoring polymorphism


209 
for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges


210 
over type~$nat$. This is true if $P(x)$ is true for all~$x$. Abstracting


211 
$P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$


212 
returns true for all arguments. Thus, the universal quantifier can be


213 
represented by a constant


214 
\begin{eqnarray*}


215 
\forall & :: & (nat\To o) \To o,


216 
\end{eqnarray*}


217 
which is essentially an infinitary truth table. The representation of $\forall


218 
x. P(x)$ is $\forall(\lambda x. P(x))$.


219 


220 
The existential quantifier is treated


221 
in the same way. Other binding operators are also easily handled; for


222 
instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as


223 
$\Sigma(i,j,\lambda k.f(k))$, where


224 
\begin{eqnarray*}


225 
\Sigma & :: & [nat,nat, nat\To nat] \To nat.


226 
\end{eqnarray*}


227 
Quantifiers may be polymorphic. We may define $\forall$ and~$\exists$ over


228 
all legal types of terms, not just the natural numbers, and


229 
allow summations over all arithmetic types:


230 
\begin{eqnarray*}


231 
\forall,\exists & :: & (\alpha{::}term\To o) \To o \\


232 
\Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha


233 
\end{eqnarray*}


234 
Observe that the index variables still have type $nat$, while the values


235 
being summed may belong to any arithmetic type.


236 


237 


238 
\section{Formalizing logical rules in Isabelle}


239 
\index{metalogicbold}


240 
\index{Isabelle!formalizing rulesbold}


241 
\index{$\Imp$bold}\index{$\Forall$bold}\index{$\equiv$bold}


242 
\index{implication!metalevelbold}


243 
\index{quantifiers!metalevelbold}


244 
\index{equality!metalevelbold}


245 
Objectlogics are formalized by extending Isabelle's metalogic, which is


246 
intuitionistic higherorder logic. The metalevel connectives are {\bf


247 
implication}, the {\bf universal quantifier}, and {\bf equality}.


248 
\begin{itemize}


249 
\item The implication \(\phi\Imp \psi\) means `\(\phi\) implies


250 
\(\psi\)', and expresses logical {\bf entailment}.


251 


252 
\item The quantification \(\Forall x.\phi\) means `\(\phi\) is true for


253 
all $x$', and expresses {\bf generality} in rules and axiom schemes.


254 


255 
\item The equality \(a\equiv b\) means `$a$ equals $b$', for expressing


256 
\bfindex{definitions} (see~\S\ref{definitions}). Equalities left over


257 
from the unification process, so called \bfindex{flexflex equations},


258 
are written $a\qeq b$. The two equality symbols have the same logical


259 
meaning.


260 


261 
\end{itemize}


262 
The syntax of the metalogic is formalized in precisely in the same manner


263 
as objectlogics, using the typed $\lambda$calculus. Analogous to


264 
type~$o$ above, there is a builtin type $prop$ of metalevel truth values.


265 
Metalevel formulae will have this type. Type $prop$ belongs to


266 
class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$


267 
and $\tau$ do. Here are the types of the builtin connectives:


268 
\begin{eqnarray*}


269 
\Imp & :: & [prop,prop]\To prop \\


270 
\Forall & :: & (\alpha{::}logic\To prop) \To prop \\


271 
{\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\


272 
\qeq & :: & [\alpha{::}\{\},\alpha]\To prop c


273 
\end{eqnarray*}


274 
The restricted polymorphism in $\Forall$ excludes certain types, those used


275 
just for parsing.


276 


277 
In our formalization of firstorder logic, we declared a type~$o$ of


278 
objectlevel truth values, rather than using~$prop$ for this purpose. If


279 
we declared the objectlevel connectives to have types such as


280 
${\neg}::prop\To prop$, then these connectives would be applicable to


281 
metalevel formulae. Keeping $prop$ and $o$ as separate types maintains


282 
the distinction between the metalevel and the objectlevel. To formalize


283 
the inference rules, we shall need to relate the two levels; accordingly,


284 
we declare the constant


285 
\index{Trueprop@{$Trueprop$}}


286 
\begin{eqnarray*}


287 
Trueprop & :: & o\To prop.


288 
\end{eqnarray*}


289 
We may regard $Trueprop$ as a metalevel predicate, reading $Trueprop(P)$ as


290 
`$P$ is true at the objectlevel.' Put another way, $Trueprop$ is a coercion


291 
from $o$ to $prop$.


292 


293 


294 
\subsection{Expressing propositional rules}


295 
\index{rules!propositionalbold}


296 
We shall illustrate the use of the metalogic by formalizing the rules of


297 
Figure~\ref{folfig}. Each objectlevel rule is expressed as a metalevel


298 
axiom.


299 


300 
One of the simplest rules is $(\conj E1)$. Making


301 
everything explicit, its formalization in the metalogic is


302 
$$ \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) $$


303 
This may look formidable, but it has an obvious reading: for all objectlevel


304 
truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The


305 
reading is correct because the metalogic has simple models, where


306 
types denote sets and $\Forall$ really means `for all.'


307 


308 
\index{Trueprop@{$Trueprop$}}


309 
Isabelle adopts notational conventions to ease the writing of rules. We may


310 
hide the occurrences of $Trueprop$ by making it an implicit coercion.


311 
Outer universal quantifiers may be dropped. Finally, the nested implication


312 
\[ \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \]


313 
may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which


314 
formalizes a rule of $n$~premises.


315 


316 
Using these conventions, the conjunction rules become the following axioms.


317 
These fully specify the properties of~$\conj$:


318 
$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$


319 
$$ P\conj Q \Imp P \qquad P\conj Q \Imp Q \eqno(\conj E1,2) $$


320 


321 
\noindent


322 
Next, consider the disjunction rules. The discharge of assumption in


323 
$(\disj E)$ is expressed using $\Imp$:


324 
$$ P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2) $$


325 
$$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E) $$


326 


327 
\noindent


328 
To understand this treatment of assumptions\index{assumptions} in natural


329 
deduction, look at implication. The rule $({\imp}I)$ is the classic


330 
example of natural deduction: to prove that $P\imp Q$ is true, assume $P$


331 
is true and show that $Q$ must then be true. More concisely, if $P$


332 
implies $Q$ (at the metalevel), then $P\imp Q$ is true (at the


333 
objectlevel). Showing the coercion explicitly, this is formalized as


334 
\[ (Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q). \]


335 
The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to


336 
specify $\imp$ are


337 
$$ (P \Imp Q) \Imp P\imp Q \eqno({\imp}I) $$


338 
$$ \List{P\imp Q; P} \Imp Q. \eqno({\imp}E) $$


339 


340 
\noindent


341 
Finally, the intuitionistic contradiction rule is formalized as the axiom


342 
$$ \bot \Imp P. \eqno(\bot E) $$


343 


344 
\begin{warn}


345 
Earlier versions of Isabelle, and certain


346 
papers~\cite{paulson89,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.


347 
\index{Trueprop@{$Trueprop$}}


348 
\end{warn}


349 


350 
\subsection{Quantifier rules and substitution}


351 
\index{rules!quantifierbold}\index{substitutionbold}


352 
\index{variables!bound}


353 
Isabelle expresses variable binding using $\lambda$abstraction; for instance,


354 
$\forall x.P$ is formalized as $\forall(\lambda x.P)$. Recall that $F(t)$


355 
is Isabelle's syntax for application of the function~$F$ to the argument~$t$;


356 
it is not a metanotation for substitution. On the other hand, a substitution


357 
will take place if $F$ has the form $\lambda x.P$; Isabelle transforms


358 
$(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$conversion. Thus, we can express


359 
inference rules that involve substitution for bound variables.


360 


361 
\index{parametersbold}\index{eigenvariablessee{parameters}}


362 
A logic may attach provisos to certain of its rules, especially quantifier


363 
rules. We cannot hope to formalize arbitrary provisos. Fortunately, those


364 
typical of quantifier rules always have the same form, namely `$x$ not free in


365 
\ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf


366 
parameter} or {\bf eigenvariable}) in some premise. Isabelle treats


367 
provisos using~$\Forall$, its inbuilt notion of `for all'.


368 


369 
\index{$\Forall$}


370 
The purpose of the proviso `$x$ not free in \ldots' is


371 
to ensure that the premise may not make assumptions about the value of~$x$,


372 
and therefore holds for all~$x$. We formalize $(\forall I)$ by


373 
\[ \left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)). \]


374 
This means, `if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.'


375 
The $\forall E$ rule exploits $\beta$conversion. Hiding $Trueprop$, the


376 
$\forall$ axioms are


377 
$$ \left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I) $$


378 
$$ \forall x.P(x) \Imp P(t). \eqno(\forall E)$$


379 


380 
\noindent


381 
We have defined the objectlevel universal quantifier~($\forall$)


382 
using~$\Forall$. But we do not require metalevel counterparts of all the


383 
connectives of the objectlogic! Consider the existential quantifier:


384 
$$ P(t) \Imp \exists x.P(x) \eqno(\exists I)$$


385 
$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$


386 
Let us verify $(\exists E)$ semantically. Suppose that the premises


387 
hold; since $\exists x.P(x)$ is true, we may choose $a$ such that $P(a)$ is


388 
true. Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and


389 
we obtain the desired conclusion, $Q$.


390 


391 
The treatment of substitution deserves mention. The rule


392 
\[ \infer{P[u/t]}{t=u & P} \]


393 
would be hard to formalize in Isabelle. It calls for replacing~$t$ by $u$


394 
throughout~$P$, which cannot be expressed using $\beta$conversion. Our


395 
rule~$(subst)$ uses the occurrences of~$x$ in~$P$ as a template for


396 
substitution, inferring $P[u/x]$ from~$P[t/x]$. When we formalize this as


397 
an axiom, the template becomes a function variable:


398 
$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst)$$


399 


400 


401 
\subsection{Signatures and theories}


402 
\index{signaturesbold}\index{theoriesbold}


403 
A {\bf signature} contains the information necessary for type checking,


404 
parsing and pretty printing. It specifies classes and their


405 
relationships; types, with their arities, and constants, with


406 
their types. It also contains syntax rules, specified using mixfix


407 
declarations.


408 


409 
Two signatures can be merged provided their specifications are compatible 


410 
they must not, for example, assign different types to the same constant.


411 
Under similar conditions, a signature can be extended. Signatures are


412 
managed internally by Isabelle; users seldom encounter them.


413 


414 
A {\bf theory} consists of a signature plus a collection of axioms. The


415 
{\bf pure} theory contains only the metalogic. Theories can be combined


416 
provided their signatures are compatible. A theory definition extends an


417 
existing theory with further signature specifications  classes, types,


418 
constants and mixfix declarations  plus a list of axioms, expressed as


419 
strings to be parsed. A theory can formalize a small piece of mathematics,


420 
such as lists and their operations, or an entire logic. A mathematical


421 
development typically involves many theories in a hierarchy. For example,


422 
the pure theory could be extended to form a theory for


423 
Figure~\ref{folfig}; this could be extended in two separate ways to form a


424 
theory for natural numbers and a theory for lists; the union of these two


425 
could be extended into a theory defining the length of a list:


426 
\[ \bf


427 
\begin{array}{c@{}c@{}c@{}c@{}c}


428 
{} & {} & \hbox{Length} & {} & {} \\


429 
{} & {} & \uparrow & {} & {} \\


430 
{} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\


431 
{} & \nearrow & {} & \nwarrow & {} \\


432 
\hbox{Nat} & {} & {} & {} & \hbox{List} \\


433 
{} & \nwarrow & {} & \nearrow & {} \\


434 
{} & {} &\hbox{FOL} & {} & {} \\


435 
{} & {} & \uparrow & {} & {} \\


436 
{} & {} &\hbox{Pure}& {} & {}


437 
\end{array}


438 
\]


439 
Each Isabelle proof typically works within a single theory, which is


440 
associated with the proof state. However, many different theories may


441 
coexist at the same time, and you may work in each of these during a single


442 
session.


443 


444 


445 
\section{Proof construction in Isabelle}


446 
\index{Isabelle!proof construction inbold}


447 
There is a onetoone correspondence between metalevel proofs and


448 
objectlevel proofs~\cite{paulson89}. To each use of a metalevel axiom,


449 
such as $(\forall I)$, there is a use of the corresponding objectlevel


450 
rule. Objectlevel assumptions and parameters have metalevel


451 
counterparts. The metalevel formalization is {\bf faithful}, admitting no


452 
incorrect objectlevel inferences, and {\bf adequate}, admitting all


453 
correct objectlevel inferences. These properties must be demonstrated


454 
separately for each objectlogic.


455 


456 
The metalogic is defined by a collection of inference rules, including


457 
equational rules for the $\lambda$calculus, and logical rules. The rules


458 
for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in


459 
Figure~\ref{folfig}. Proofs performed using the primitive metarules


460 
would be lengthy; Isabelle proofs normally use certain derived rules.


461 
{\bf Resolution}, in particular, is convenient for backward proof.


462 


463 
Unification is central to theorem proving. It supports quantifier


464 
reasoning by allowing certain `unknown' terms to be instantiated later,


465 
possibly in stages. When proving that the time required to sort $n$


466 
integers is proportional to~$n^2$, we need not state the constant of


467 
proportionality; when proving that a hardware adder will deliver the sum of


468 
its inputs, we need not state how many clock ticks will be required. Such


469 
quantities often emerge from the proof.


470 


471 
\index{variables!schematicsee{unknowns}}


472 
Isabelle provides {\bf schematic variables}, or \bfindex{unknowns}, for


473 
unification. Logically, unknowns are free variables. Pragmatically, they


474 
may be instantiated during a proof, while ordinary variables remain fixed.


475 
Unknowns are written with a ?\ prefix and are frequently subscripted:


476 
$\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots, $\Var{P}$, $\Var{P@1}$, \ldots.


477 


478 
Recall that an inference rule of the form


479 
\[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \]


480 
is formalized in Isabelle's metalogic as the axiom


481 
$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.


482 
Such axioms resemble {\sc Prolog}'s Horn clauses, and can be combined by


483 
resolution  Isabelle's principal proof method. Resolution yields both


484 
forward and backward proof. Backward proof works by unifying a goal with


485 
the conclusion of a rule, whose premises become new subgoals. Forward proof


486 
works by unifying theorems with the premises of a rule, deriving a new theorem.


487 


488 
Isabelle axioms will require an extended notion of resolution, because


489 
they differ from Horn clauses in two major respects:


490 
\begin{itemize}


491 
\item They are written in the typed $\lambda$calculus, and therefore must be


492 
resolved using higherorder unification.


493 


494 
\item Horn clauses are composed of atomic formulae. Any formula of the form


495 
$Trueprop(\cdots)$ is atomic, but axioms such as ${\imp}I$ and $\forall I$


496 
contain nonatomic formulae.


497 
\index{Trueprop@{$Trueprop$}}


498 
\end{itemize}


499 
Isabelle should not be confused with classical resolution theorem provers


500 
such as Otter~\cite{wosbledsoe}. At the metalevel, Isabelle proves


501 
theorems in their positive form, not by refutation. However, an


502 
objectlogic that includes a contradiction rule may employ a refutation


503 
proof procedure.


504 


505 


506 
\subsection{Higherorder unification}


507 
\index{unification!higherorderbold}


508 
Unification is equation solving. The solution of $f(\Var{x},c) \qeq


509 
f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$. {\bf


510 
Higherorder unification} is equation solving for typed $\lambda$terms.


511 
To handle $\beta$conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$.


512 
That is easy  in the typed $\lambda$calculus, all reduction sequences


513 
terminate at a normal form. But it must guess the unknown


514 
function~$\Var{f}$ in order to solve the equation


515 
\begin{equation} \label{houeqn}


516 
\Var{f}(t) \qeq g(u@1,\ldots,u@k).


517 
\end{equation}


518 
Huet's~\cite{huet75} search procedure solves equations by imitation and


519 
projection. {\bf Imitation}\index{imitationbold} makes~$\Var{f}$ apply


520 
leading symbol (if a constant) of the righthand side. To solve


521 
equation~(\ref{houeqn}), it guesses


522 
\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \]


523 
where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns. Assuming there are no


524 
other occurrences of~$\Var{f}$, equation~(\ref{houeqn}) simplifies to the


525 
set of equations


526 
\[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \]


527 
If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots,


528 
$\Var{h@k}$, then it yields an instantiation for~$\Var{f}$.


529 


530 
\index{projectionbold}


531 
{\bf Projection} makes $\Var{f}$ apply one of its arguments. To solve


532 
equation~(\ref{houeqn}), if $t$ expects~$m$ arguments and delivers a


533 
result of suitable type, it guesses


534 
\[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \]


535 
where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no


536 
other occurrences of~$\Var{f}$, equation~(\ref{houeqn}) simplifies to the


537 
equation


538 
\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$


539 


540 
\begin{warn}


541 
Huet's unification procedure is complete. Isabelle's polymorphic version,


542 
which solves for type unknowns as well as for term unknowns, is incomplete.


543 
The problem is that projection requires type information. In


544 
equation~(\ref{houeqn}), if the type of~$t$ is unknown, then projections


545 
are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be


546 
similarly unconstrained. Therefore, Isabelle never attempts such


547 
projections, and may fail to find unifiers where a type unknown turns out


548 
to be a function type.


549 
\end{warn}


550 


551 
\index{unknowns!of function typebold}


552 
Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to


553 
$n+1$ guesses. The search tree and set of unifiers may be infinite. But


554 
higherorder unification can work effectively, provided you are careful


555 
with {\bf function unknowns}:


556 
\begin{itemize}


557 
\item Equations with no function unknowns are solved using firstorder


558 
unification, extended to treat bound variables. For example, $\lambda x.x


559 
\qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would


560 
capture the free variable~$x$.


561 


562 
\item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are


563 
distinct bound variables, causes no difficulties. Its projections can only


564 
match the corresponding variables.


565 


566 
\item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right. It has


567 
four solutions, but Isabelle evaluates them lazily, trying projection before


568 
imitation. The first solution is usually the one desired:


569 
\[ \Var{f}\equiv \lambda x. x+x \quad


570 
\Var{f}\equiv \lambda x. a+x \quad


571 
\Var{f}\equiv \lambda x. x+a \quad


572 
\Var{f}\equiv \lambda x. a+a \]


573 
\item Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and


574 
$\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be


575 
avoided.


576 
\end{itemize}


577 
In problematic cases, you may have to instantiate some unknowns before


578 
invoking unification.


579 


580 


581 
\subsection{Joining rules by resolution} \label{joining}


582 
\index{resolutionbold}


583 
Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots;


584 
\phi@n} \Imp \phi$ be two Isabelle theorems, representing objectlevel rules.


585 
Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a


586 
higherorder unifier. Writing $Xs$ for the application of substitution~$s$ to


587 
expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$.


588 
By resolution, we may conclude


589 
\[ (\List{\phi@1; \ldots; \phi@{i1}; \psi@1; \ldots; \psi@m;


590 
\phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.


591 
\]


592 
The substitution~$s$ may instantiate unknowns in both rules. In short,


593 
resolution is the following rule:


594 
\[ \infer[(\psi s\equiv \phi@i s)]


595 
{(\List{\phi@1; \ldots; \phi@{i1}; \psi@1; \ldots; \psi@m;


596 
\phi@{i+1}; \ldots; \phi@n} \Imp \phi)s}


597 
{\List{\psi@1; \ldots; \psi@m} \Imp \psi & &


598 
\List{\phi@1; \ldots; \phi@n} \Imp \phi}


599 
\]


600 
It operates at the metalevel, on Isabelle theorems, and is justified by


601 
the properties of $\Imp$ and~$\Forall$. It takes the number~$i$ (for


602 
$1\leq i\leq n$) as a parameter and may yield infinitely many conclusions,


603 
one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these


604 
conclusions as a sequence (lazy list).


605 


606 
Resolution expects the rules to have no outer quantifiers~($\Forall$). It


607 
may rename or instantiate any schematic variables, but leaves free


608 
variables unchanged. When constructing a theory, Isabelle puts the rules


609 
into a standard form containing no free variables; for instance, $({\imp}E)$


610 
becomes


611 
\[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}.


612 
\]


613 
When resolving two rules, the unknowns in the first rule are renamed, by


614 
subscripting, to make them distinct from the unknowns in the second rule. To


615 
resolve $({\imp}E)$ with itself, the first copy of the rule would become


616 
\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}. \]


617 
Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with


618 
$\Var{P}\imp \Var{Q}$, is the metalevel inference


619 
\[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}}


620 
\Imp\Var{Q}.}


621 
{\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1} & &


622 
\List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}}


623 
\]


624 
Renaming the unknowns in the resolvent, we have derived the


625 
objectlevel rule


626 
\[ \infer{Q.}{R\imp (P\imp Q) & R & P} \]


627 
\index{rules!derived}


628 
Joining rules in this fashion is a simple way of proving theorems. The


629 
derived rules are conservative extensions of the objectlogic, and may permit


630 
simpler proofs. Let us consider another example. Suppose we have the axiom


631 
$$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$


632 


633 
\noindent


634 
The standard form of $(\forall E)$ is


635 
$\forall x.\Var{P}(x) \Imp \Var{P}(\Var{t})$.


636 
Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by


637 
$\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$


638 
unchanged, yielding


639 
\[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \]


640 
Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$


641 
and yields


642 
\[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \]


643 
Resolving this with $({\imp}E)$ increases the subscripts and yields


644 
\[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}.


645 
\]


646 
We have derived the rule


647 
\[ \infer{m=n,}{Suc(m)=Suc(n)} \]


648 
which goes directly from $Suc(m)=Suc(n)$ to $m=n$. It is handy for simplifying


649 
an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$.


650 


651 


652 
\subsection{Lifting a rule into a context}


653 
The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for


654 
resolution. They have nonatomic premises, namely $P\Imp Q$ and $\Forall


655 
x.P(x)$, while the conclusions of all the rules are atomic (they have the form


656 
$Trueprop(\cdots)$). Isabelle gets round the problem through a metainference


657 
called \bfindex{lifting}. Let us consider how to construct proofs such as


658 
\[ \infer[({\imp}I)]{P\imp(Q\imp R)}


659 
{\infer[({\imp}I)]{Q\imp R}


660 
{\infer*{R}{[P] & [Q]}}}


661 
\qquad


662 
\infer[(\forall I)]{\forall x\,y.P(x,y)}


663 
{\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}}


664 
\]


665 


666 
\subsubsection{Lifting over assumptions}


667 
\index{lifting!over assumptionsbold}


668 
Lifting over $\theta\Imp{}$ is the following metainference rule:


669 
\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp


670 
(\theta \Imp \phi)}


671 
{\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]


672 
This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and


673 
$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$, $\theta$ are all true then


674 
$\phi$ must be true. Iterated lifting over a series of metaformulae


675 
$\theta@k$, \ldots, $\theta@1$ yields an objectrule whose conclusion is


676 
$\List{\theta@1; \ldots; \theta@k} \Imp \phi$. Typically the $\theta@i$ are


677 
the assumptions in a natural deduction proof; lifting copies them into a rule's


678 
premises and conclusion.


679 


680 
When resolving two rules, Isabelle lifts the first one if necessary. The


681 
standard form of $({\imp}I)$ is


682 
\[ (\Var{P} \Imp \Var{Q}) \Imp \Var{P}\imp \Var{Q}. \]


683 
To resolve this rule with itself, Isabelle modifies one copy as follows: it


684 
renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over


685 
$\Var{P}\Imp{}$:


686 
\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}}


687 
\Imp \Var{P@1}\imp \Var{Q@1}. \]


688 
Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp


689 
\Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$.


690 
Resolution yields


691 
\[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp


692 
\Var{P}\imp(\Var{P@1}\imp\Var{Q@1}). \]


693 
This represents the derived rule


694 
\[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \]


695 


696 
\subsubsection{Lifting over parameters}


697 
\index{lifting!over parametersbold}


698 
An analogous form of lifting handles premises of the form $\Forall x\ldots\,$.


699 
Here, lifting prefixes an objectrule's premises and conclusion with $\Forall


700 
x$. At the same time, lifting introduces a dependence upon~$x$. It replaces


701 
each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new


702 
unknown (by subscripting) of suitable type  necessarily a function type. In


703 
short, lifting is the metainference


704 
\[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x}


705 
\Imp \Forall x.\phi^x,}


706 
{\List{\phi@1; \ldots; \phi@n} \Imp \phi} \]


707 
where $\phi^x$ stands for the result of lifting unknowns over~$x$ in $\phi$.


708 
It is not hard to verify that this metainference is sound.


709 
For example, $(\disj I)$ might be lifted to


710 
\[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\]


711 
and $(\forall I)$ to


712 
\[ (\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)). \]


713 
Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$,


714 
avoiding a clash. Resolving the above with $(\forall I)$ is the metainference


715 
\[ \infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) }


716 
{(\Forall x\,y.\Var{P@1}(x,y)) \Imp


717 
(\Forall x. \forall y.\Var{P@1}(x,y)) &


718 
(\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \]


719 
Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the


720 
resolvent expresses the derived rule


721 
\[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }


722 
\quad\hbox{provided $x$, $y$ not free in the assumptions}


723 
\]


724 
I discuss lifting and parameters at length elsewhere~\cite{paulson89}.


725 
Miller goes into even greater detail~\cite{millerjsc}.


726 


727 


728 
\section{Backward proof by resolution}


729 
\index{resolution!in backward proof}\index{proof!backwardbold}


730 
Resolution is convenient for deriving simple rules and for reasoning


731 
forward from facts. It can also support backward proof, where we start


732 
with a goal and refine it to progressively simpler subgoals until all have


733 
been solved. {\sc lcf} (and its descendants {\sc hol} and Nuprl) provide


734 
tactics and tacticals, which constitute a highlevel language for


735 
expressing proof searches. \bfindex{Tactics} perform primitive refinements


736 
while \bfindex{tacticals} combine tactics.


737 


738 
\index{LCF}


739 
Isabelle's tactics and tacticals work differently from {\sc lcf}'s. An


740 
Isabelle rule is {\bf bidirectional}: there is no distinction between


741 
inputs and outputs. {\sc lcf} has a separate tactic for each rule;


742 
Isabelle performs refinement by any rule in a uniform fashion, using


743 
resolution.


744 


745 
\index{subgoalsbold}\index{main goalbold}


746 
Isabelle works with metalevel theorems of the form


747 
\( \List{\phi@1; \ldots; \phi@n} \Imp \phi \).


748 
We have viewed this as the {\bf rule} with premises


749 
$\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$. It can also be viewed as


750 
the \bfindex{proof state} with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main


751 
goal~$\phi$.


752 


753 
To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof


754 
state. This assertion is, trivially, a theorem. At a later stage in the


755 
backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n}


756 
\Imp \phi$. This proof state is a theorem, guaranteeing that the subgoals


757 
$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$. If $m=0$ then we have


758 
proved~$\phi$ outright. If $\phi$ contains unknowns, they may become


759 
instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;


760 
\phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$.


761 


762 
\subsection{Refinement by resolution}


763 
\index{refinementbold}


764 
To refine subgoal~$i$ of a proof state by a rule, perform the following


765 
resolution:


766 
\[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \]


767 
If the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after lifting


768 
over subgoal~$i$, and the proof state is $\List{\phi@1; \ldots; \phi@n}


769 
\Imp \phi$, then the new proof state is (for~$1\leq i\leq n$)


770 
\[ (\List{\phi@1; \ldots; \phi@{i1}; \psi'@1;


771 
\ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \]


772 
Substitution~$s$ unifies $\psi'$ with~$\phi@i$. In the proof state,


773 
subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises.


774 
If some of the rule's unknowns are left uninstantiated, they become new


775 
unknowns in the proof state. Refinement by~$(\exists I)$, namely


776 
\[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \]


777 
inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting.


778 
We do not have to specify an `existential witness' when


779 
applying~$(\exists I)$. Further resolutions may instantiate unknowns in


780 
the proof state.


781 


782 
\subsection{Proof by assumption}


783 
\index{proof!by assumptionbold}


784 
In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and


785 
assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for


786 
each subgoal. Repeated lifting steps can lift a rule into any context. To


787 
aid readability, Isabelle puts contexts into a normal form, gathering the


788 
parameters at the front:


789 
\begin{equation} \label{contexteqn}


790 
\Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta.


791 
\end{equation}


792 
Under the usual reading of the connectives, this expresses that $\theta$


793 
follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary


794 
$x@1$,~\ldots,~$x@l$. It is trivially true if $\theta$ equals any of


795 
$\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them. This


796 
models proof by assumption in natural deduction.


797 


798 
Isabelle automates the metainference for proof by assumption. Its arguments


799 
are the metatheorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$


800 
from~1 to~$n$, where $\phi@i$ has the form~(\ref{contexteqn}). Its results


801 
are metatheorems of the form


802 
\[ (\List{\phi@1; \ldots; \phi@{i1}; \phi@{i+1}; \phi@n} \Imp \phi)s \]


803 
for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$


804 
with $\lambda x@1 \ldots x@l. \theta$. Isabelle supplies the parameters


805 
$x@1$,~\ldots,~$x@l$ to higherorder unification as bound variables, which


806 
regards them as unique constants with a limited scope  this enforces


807 
parameter provisos~\cite{paulson89}.


808 


809 
The premise represents a proof state with~$n$ subgoals, of which the~$i$th is


810 
to be solved by assumption. Isabelle searches the subgoal's context for an


811 
assumption, say $\theta@j$, that can solve it by unification. For each


812 
unifier, the metainference returns an instantiated proof state from which the


813 
$i$th subgoal has been removed. Isabelle searches for a unifying assumption;


814 
for readability and robustness, proofs do not refer to assumptions by number.


815 


816 
Consider the proof state $(\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x})$.


817 
Proof by assumption (with $i=1$, the only possibility) yields two results:


818 
\begin{itemize}


819 
\item $Q(a)$, instantiating $\Var{x}\equiv a$


820 
\item $Q(b)$, instantiating $\Var{x}\equiv b$


821 
\end{itemize}


822 
Here, proof by assumption affects the main goal. It could also affect


823 
other subgoals. Consider the effect of having the


824 
additional subgoal ${\List{P(b); P(c)} \Imp P(\Var{x})}$.


825 


826 
\subsection{A propositional proof} \label{propproof}


827 
\index{examples!propositional}


828 
Our first example avoids quantifiers. Given the main goal $P\disj P\imp


829 
P$, Isabelle creates the initial state


830 
\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \]


831 
Bear in mind that every proof state we derive will be a metatheorem,


832 
expressing that the subgoals imply the main goal. The first step is to refine


833 
subgoal~1 by (${\imp}I)$, creating a new state where $P\disj P$ is an


834 
assumption:


835 
\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \]


836 
The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals.


837 
Because of lifting, each subgoal contains a copy of the context  the


838 
assumption $P\disj P$. (In fact, this assumption is now redundant; we shall


839 
shortly see how to get rid of it!) The new proof state is the following


840 
metatheorem, laid out for clarity:


841 
\[ \begin{array}{l@{}l@{\qquad\qquad}l}


842 
\lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\


843 
& \List{P\disj P; \Var{P@1}} \Imp P; & \hbox{(subgoal 2)} \\


844 
& \List{P\disj P; \Var{Q@1}} \Imp P & \hbox{(subgoal 3)} \\


845 
\rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)}


846 
\end{array}


847 
\]


848 
Notice the unknowns in the proof state. Because we have applied $(\disj E)$,


849 
we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$. Of course,


850 
subgoal~1 is provable by assumption. This instantiates both $\Var{P@1}$ and


851 
$\Var{Q@1}$ to~$P$ throughout the proof state:


852 
\[ \begin{array}{l@{}l@{\qquad\qquad}l}


853 
\lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\


854 
& \List{P\disj P; P} \Imp P & \hbox{(subgoal 2)} \\


855 
\rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)}


856 
\end{array} \]


857 
Both of the remaining subgoals can be proved by assumption. After two such


858 
steps, the proof state is simply the metatheorem $P\disj P\imp P$. This is


859 
our desired result.


860 


861 
\subsection{A quantifier proof}


862 
\index{examples!with quantifiers}


863 
To illustrate quantifiers and $\Forall$lifting, let us prove


864 
$(\exists x.P(f(x)))\imp(\exists x.P(x))$. The initial proof


865 
state is the trivial metatheorem


866 
\[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp


867 
(\exists x.P(f(x)))\imp(\exists x.P(x)). \]


868 
As above, the first step is refinement by (${\imp}I)$:


869 
\[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp


870 
(\exists x.P(f(x)))\imp(\exists x.P(x))


871 
\]


872 
The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals.


873 
Both have the assumption $\exists x.P(f(x))$. The new proof


874 
state is the metatheorem


875 
\[ \begin{array}{l@{}l@{\qquad\qquad}l}


876 
\lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\


877 
& \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp


878 
\exists x.P(x) & \hbox{(subgoal 2)} \\


879 
\rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) & \hbox{(main goal)}


880 
\end{array}


881 
\]


882 
The unknown $\Var{P@1}$ appears in both subgoals. Because we have applied


883 
$(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may


884 
become any formula possibly containing~$x$. Proving subgoal~1 by assumption


885 
instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$:


886 
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp


887 
\exists x.P(x)\right)


888 
\Imp (\exists x.P(f(x)))\imp(\exists x.P(x))


889 
\]


890 
The next step is refinement by $(\exists I)$. The rule is lifted into the


891 
context of the parameter~$x$ and the assumption $P(f(x))$. This ensures that


892 
the context is copied to the subgoal and allows the existential witness to


893 
depend upon~$x$:


894 
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp


895 
P(\Var{x@2}(x))\right)


896 
\Imp (\exists x.P(f(x)))\imp(\exists x.P(x))


897 
\]


898 
The existential witness, $\Var{x@2}(x)$, consists of an unknown


899 
applied to a parameter. Proof by assumption unifies $\lambda x.P(f(x))$


900 
with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$. The final


901 
proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.


902 


903 


904 
\subsection{Tactics and tacticals}


905 
\index{tacticsbold}\index{tacticalsbold}


906 
{\bf Tactics} perform backward proof. Isabelle tactics differ from those


907 
of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,


908 
rather than on individual subgoals. An Isabelle tactic is a function that


909 
takes a proof state and returns a sequence (lazy list) of possible


910 
successor states. Sequences are coded in ML as functions, a standard


911 
technique~\cite{paulson91}. Isabelle represents proof states by theorems.


912 


913 
Basic tactics execute the metarules described above, operating on a


914 
given subgoal. The {\bf resolution tactics} take a list of rules and


915 
return next states for each combination of rule and unifier. The {\bf


916 
assumption tactic} examines the subgoal's assumptions and returns next


917 
states for each combination of assumption and unifier. Lazy lists are


918 
essential because higherorder resolution may return infinitely many


919 
unifiers. If there are no matching rules or assumptions then no next


920 
states are generated; a tactic application that returns an empty list is


921 
said to {\bf fail}.


922 


923 
Sequences realize their full potential with {\bf tacticals}  operators


924 
for combining tactics. Depthfirst search, breadthfirst search and


925 
bestfirst search (where a heuristic function selects the best state to


926 
explore) return their outcomes as a sequence. Isabelle provides such


927 
procedures in the form of tacticals. Simpler procedures can be expressed


928 
directly using the basic tacticals {\it THEN}, {\it ORELSE} and {\it REPEAT}:


929 
\begin{description}


930 
\item[$tac1\;THEN\;tac2$] is a tactic for sequential composition. Applied


931 
to a proof state, it returns all states reachable in two steps by applying


932 
$tac1$ followed by~$tac2$.


933 


934 
\item[$tac1\;ORELSE\;tac2$] is a choice tactic. Applied to a state, it


935 
tries~$tac1$ and returns the result if nonempty; otherwise, it uses~$tac2$.


936 


937 
\item[$REPEAT\;tac$] is a repetition tactic. Applied to a state, it


938 
returns all states reachable by applying~$tac$ as long as possible (until


939 
it would fail). $REPEAT$ can be expressed in a few lines of \ML{} using


940 
{\it THEN} and~{\it ORELSE}.


941 
\end{description}


942 
For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving


943 
$tac1$ priority:


944 
\[ REPEAT(tac1\;ORELSE\;tac2) \]


945 


946 


947 
\section{Variations on resolution}


948 
In principle, resolution and proof by assumption suffice to prove all


949 
theorems. However, specialized forms of resolution are helpful for working


950 
with elimination rules. Elimresolution applies an elimination rule to an


951 
assumption; destructresolution is similar, but applies a rule in a forward


952 
style.


953 


954 
The last part of the section shows how the techniques for proving theorems


955 
can also serve to derive rules.


956 


957 
\subsection{Elimresolution}


958 
\index{elimresolutionbold}


959 
Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By


960 
$({\imp}I)$, we prove $R$ from the assumption $((R\disj R)\disj R)\disj R$.


961 
Applying $(\disj E)$ to this assumption yields two subgoals, one that


962 
assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj


963 
R)\disj R$. This subgoal admits another application of $(\disj E)$. Since


964 
natural deduction never discards assumptions, we eventually generate a


965 
subgoal containing much that is redundant:


966 
\[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \]


967 
In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new


968 
subgoals with the additional assumption $P$ or~$Q$. In these subgoals,


969 
$P\disj Q$ is redundant. It wastes space; worse, it could make a theorem


970 
prover repeatedly apply~$(\disj E)$, looping. Other elimination rules pose


971 
similar problems. In firstorder logic, only universally quantified


972 
assumptions are sometimes needed more than once  say, to prove


973 
$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$.


974 


975 
Many logics can be formulated as sequent calculi that delete redundant


976 
assumptions after use. The rule $(\disj E)$ might become


977 
\[ \infer[\disj\hbox{left}]


978 
{\Gamma,P\disj Q,\Delta \turn \Theta}


979 
{\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta} \]


980 
In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$


981 
(that is, as an assumption) splits into two subgoals, replacing $P\disj Q$


982 
by $P$ or~$Q$. But the sequent calculus, with its explicit handling of


983 
assumptions, can be tiresome to use.


984 


985 
Elimresolution is Isabelle's way of getting sequent calculus behaviour


986 
from natural deduction rules. It lets an elimination rule consume an


987 
assumption. Elimresolution takes a rule $\List{\psi@1; \ldots; \psi@m}


988 
\Imp \psi$ a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and a


989 
subgoal number~$i$. The rule must have at least one premise, thus $m>0$.


990 
Write the rule's lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp


991 
\psi'$. Ordinary resolution would attempt to reduce~$\phi@i$,


992 
replacing subgoal~$i$ by $m$ new ones. Elimresolution tries {\bf


993 
simultaneously} to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it


994 
returns a sequence of next states. Each of these replaces subgoal~$i$ by


995 
instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected


996 
assumption has been deleted. Suppose $\phi@i$ has the parameter~$x$ and


997 
assumptions $\theta@1$,~\ldots,~$\theta@k$. Then $\psi'@1$, the rule's first


998 
premise after lifting, will be


999 
\( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \).


1000 
Elimresolution tries to unify simultaneously $\psi'\qeq\phi@i$ and


1001 
$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$, for $j=1$,~\ldots,~$k$.


1002 


1003 
Let us redo the example from~\S\ref{propproof}. The elimination rule


1004 
is~$(\disj E)$,


1005 
\[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}}


1006 
\Imp \Var{R} \]


1007 
and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$. The


1008 
lifted rule would be


1009 
\[ \begin{array}{l@{}l}


1010 
\lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\


1011 
& \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\


1012 
& \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1} \\


1013 
\rbrakk\;& \Imp \Var{R@1}


1014 
\end{array}


1015 
\]


1016 
Unification would take the simultaneous equations


1017 
$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding


1018 
$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state


1019 
would be simply


1020 
\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P).


1021 
\]


1022 
Elimresolution's simultaneous unification gives better control


1023 
than ordinary resolution. Recall the substitution rule:


1024 
$$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u})


1025 
\eqno(subst) $$


1026 
Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many


1027 
unifiers, $(subst)$ works well with elimresolution. It deletes some


1028 
assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal


1029 
formula. The simultaneous unification instantiates $\Var{u}$ to~$y$; if


1030 
$y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another


1031 
formula.


1032 


1033 
In logical parlance, the premise containing the connective to be eliminated


1034 
is called the \bfindex{major premise}. Elimresolution expects the major


1035 
premise to come first. The order of the premises is significant in


1036 
Isabelle.


1037 


1038 
\subsection{Destruction rules} \label{destruct}


1039 
\index{destruction rulesbold}\index{proof!forward}


1040 
Looking back to Figure~\ref{folfig}, notice that there are two kinds of


1041 
elimination rule. The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and


1042 
$({\forall}E)$ extract the conclusion from the major premise. In Isabelle


1043 
parlance, such rules are called \bfindex{destruction rules}; they are readable


1044 
and easy to use in forward proof. The rules $({\disj}E)$, $({\bot}E)$ and


1045 
$({\exists}E)$ work by discharging assumptions; they support backward proof


1046 
in a style reminiscent of the sequent calculus.


1047 


1048 
The latter style is the most general form of elimination rule. In natural


1049 
deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or


1050 
$({\exists}E)$ as destruction rules. But we can write general elimination


1051 
rules for $\conj$, $\imp$ and~$\forall$:


1052 
\[


1053 
\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad


1054 
\infer{R}{P\imp Q & P & \infer*{R}{[Q]}} \qquad


1055 
\infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}}


1056 
\]


1057 
Because they are concise, destruction rules are simpler to derive than the


1058 
corresponding elimination rules. To facilitate their use in backward


1059 
proof, Isabelle provides a means of transforming a destruction rule such as


1060 
\[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m}


1061 
\infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}}


1062 
\]


1063 
\index{destructresolutionbold}


1064 
{\bf Destructresolution} combines this transformation with


1065 
elimresolution. It applies a destruction rule to some assumption of a


1066 
subgoal. Given the rule above, it replaces the assumption~$P@1$ by~$Q$,


1067 
with new subgoals of showing instances of $P@2$, \ldots,~$P@m$.


1068 
Destructresolution works forward from a subgoal's assumptions. Ordinary


1069 
resolution performs forward reasoning from theorems, as illustrated


1070 
in~\S\ref{joining}.


1071 


1072 


1073 
\subsection{Deriving rules by resolution} \label{deriving}


1074 
\index{rules!derivedbold}


1075 
The metalogic, itself a form of the predicate calculus, is defined by a


1076 
system of natural deduction rules. Each theorem may depend upon


1077 
metaassumptions. The theorem that~$\phi$ follows from the assumptions


1078 
$\phi@1$, \ldots, $\phi@n$ is written


1079 
\[ \phi \quad [\phi@1,\ldots,\phi@n]. \]


1080 
A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$,


1081 
but Isabelle's notation is more readable with large formulae.


1082 


1083 
Metalevel natural deduction provides a convenient mechanism for deriving


1084 
new objectlevel rules. To derive the rule


1085 
\[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \]


1086 
assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the


1087 
metalevel. Then prove $\phi$, possibly using these assumptions.


1088 
Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,


1089 
reaching a final state such as


1090 
\[ \phi \quad [\theta@1,\ldots,\theta@k]. \]


1091 
The metarule for $\Imp$ introduction discharges an assumption.


1092 
Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the


1093 
metatheorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no


1094 
assumptions. This represents the desired rule.


1095 
Let us derive the general $\conj$ elimination rule:


1096 
$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E)$$


1097 
We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in


1098 
the state $R\Imp R$. Resolving this with the second assumption yields the


1099 
state


1100 
\[ \phantom{\List{P\conj Q;\; P\conj Q}}


1101 
\llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]


1102 
Resolving subgoals~1 and~2 with $({\conj}E1)$ and $({\conj}E2)$,


1103 
respectively, yields the state


1104 
\[ \List{P\conj Q;\; P\conj Q}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \]


1105 
Resolving both subgoals with the assumption $P\conj Q$ yields


1106 
\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \]


1107 
The proof may use the metaassumptions in any order, and as often as


1108 
necessary; when finished, we discharge them in the correct order to


1109 
obtain the desired form:


1110 
\[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \]


1111 
We have derived the rule using free variables, which prevents their


1112 
premature instantiation during the proof; we may now replace them by


1113 
schematic variables.


1114 


1115 
\begin{warn}


1116 
Schematic variables are not allowed in (meta) assumptions because they would


1117 
complicate lifting. Assumptions remain fixed throughout a proof.


1118 
\end{warn}


1119 


1120 
% Local Variables:


1121 
% mode: latex


1122 
% TeXmaster: t


1123 
% End:
