author  wenzelm 
Fri, 16 Jul 1999 22:24:42 +0200  
changeset 7024  44bd3c094fd6 
parent 6592  c120262044b6 
child 9695  ec7d7f877712 
permissions  rwrr 
105  1 
%% $Id$ 
3106  2 

105  3 
\part{Foundations} 
296  4 
The following sections discuss Isabelle's logical foundations in detail: 
105  5 
representing logical syntax in the typed $\lambda$calculus; expressing 
6 
inference rules in Isabelle's metalogic; combining rules by resolution. 

296  7 

8 
If you wish to use Isabelle immediately, please turn to 

9 
page~\pageref{chap:getting}. You can always read about foundations later, 

10 
either by returning to this point or by looking up particular items in the 

11 
index. 

105  12 

13 
\begin{figure} 

14 
\begin{eqnarray*} 

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

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

17 
\end{eqnarray*} 

18 
\vskip 4ex 

19 

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

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

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

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

24 

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

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

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

28 

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

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

31 

32 
& 

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

34 

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

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

37 

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

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

40 

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

42 
\end{array} \) 

43 

44 
\bigskip\bigskip 

45 
*{\em Eigenvariable conditions\/}: 

46 

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

48 

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

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

51 
\end{figure} 

52 

296  53 
\section{Formalizing logical syntax in Isabelle}\label{sec:logicalsyntax} 
331  54 
\index{firstorder logic} 
55 

105  56 
Figure~\ref{folfig} presents intuitionistic firstorder logic, 
296  57 
including equality. Let us see how to formalize 
105  58 
this logic in Isabelle, illustrating the main features of Isabelle's 
59 
polymorphic metalogic. 

60 

331  61 
\index{lambda calc@$\lambda$calculus} 
312  62 
Isabelle represents syntax using the simply typed $\lambda$calculus. We 
63 
declare a type for each syntactic category of the logic. We declare a 

64 
constant for each symbol of the logic, giving each $n$place operation an 

65 
$n$argument curried function type. Most importantly, 

66 
$\lambda$abstraction represents variable binding in quantifiers. 

105  67 

331  68 
\index{types!syntax of}\index{types!function}\index{*fun type} 
69 
\index{type constructors} 

70 
Isabelle has \MLstyle polymorphic types such as~$(\alpha)list$, where 

71 
$list$ is a type constructor and $\alpha$ is a type variable; for example, 

105  72 
$(bool)list$ is the type of lists of booleans. Function types have the 
312  73 
form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are 
74 
types. Curried function types may be abbreviated: 

105  75 
\[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad 
3103  76 
[\sigma@1, \ldots, \sigma@n] \To \tau \] 
105  77 

3103  78 
\index{terms!syntax of} The syntax for terms is summarised below. 
79 
Note that there are two versions of function application syntax 

80 
available in Isabelle: either $t\,u$, which is the usual form for 

81 
higherorder languages, or $t(u)$, trying to look more like 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3106
diff
changeset

82 
firstorder. The latter syntax is used throughout the manual. 
105  83 
\[ 
312  84 
\index{lambda abs@$\lambda$abstractions}\index{function applications} 
105  85 
\begin{array}{ll} 
296  86 
t :: \tau & \hbox{type constraint, on a term or bound variable} \\ 
105  87 
\lambda x.t & \hbox{abstraction} \\ 
88 
\lambda x@1\ldots x@n.t 

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

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

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

92 
\end{array} 

93 
\] 

94 

95 

296  96 
\subsection{Simple types and constants}\index{types!simplebold} 
97 

98 
The syntactic categories of our logic (Fig.\ts\ref{folfig}) are {\bf 

99 
formulae} and {\bf terms}. Formulae denote truth values, so (following 

100 
tradition) let us call their type~$o$. To allow~0 and~$Suc(t)$ as terms, 

101 
let us declare a type~$nat$ of natural numbers. Later, we shall see 

102 
how to admit terms of other types. 

105  103 

312  104 
\index{constants}\index{*nat type}\index{*o type} 
105  105 
After declaring the types~$o$ and~$nat$, we may declare constants for the 
106 
symbols of our logic. Since $\bot$ denotes a truth value (falsity) and 0 

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

108 
\bot & :: & o \\ 

109 
0 & :: & nat. 

110 
\end{eqnarray*} 

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

112 
function type. In our logic, the successor function 

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

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

115 
curried functions taking two truth values as arguments: 

116 
\begin{eqnarray*} 

117 
Suc & :: & nat\To nat \\ 

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

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

120 
\end{eqnarray*} 

296  121 
The binary connectives can be declared as infixes, with appropriate 
122 
precedences, so that we write $P\conj Q\disj R$ instead of 

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

105  124 

331  125 
Section~\ref{sec:definingtheories} below describes the syntax of Isabelle 
126 
theory files and illustrates it by extending our logic with mathematical 

127 
induction. 

105  128 

129 

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

131 
\index{types!polymorphicbold} 

296  132 
\index{equality!polymorphic} 
312  133 
\index{constants!polymorphic} 
296  134 

105  135 
Which type should we assign to the equality symbol? If we tried 
136 
$[nat,nat]\To o$, then equality would be restricted to the natural 

312  137 
numbers; we should have to declare different equality symbols for each 
105  138 
type. Isabelle's type system is polymorphic, so we could declare 
139 
\begin{eqnarray*} 

296  140 
{=} & :: & [\alpha,\alpha]\To o, 
105  141 
\end{eqnarray*} 
296  142 
where the type variable~$\alpha$ ranges over all types. 
105  143 
But this is also wrong. The declaration is too polymorphic; $\alpha$ 
296  144 
includes types like~$o$ and $nat\To nat$. Thus, it admits 
105  145 
$\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in 
146 
higherorder logic but not in firstorder logic. 

147 

296  148 
Isabelle's {\bf type classes}\index{classes} control 
149 
polymorphism~\cite{nipkowprehofer}. Each type variable belongs to a 

150 
class, which denotes a set of types. Classes are partially ordered by the 

151 
subclass relation, which is essentially the subset relation on the sets of 

152 
types. They closely resemble the classes of the functional language 

153 
Haskell~\cite{haskelltutorial,haskellreport}. 

105  154 

312  155 
\index{*logic class}\index{*term class} 
105  156 
Isabelle provides the builtin class $logic$, which consists of the logical 
157 
types: the ones we want to reason about. Let us declare a class $term$, to 

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

159 
is now $term\le logic$. 

160 

312  161 
\index{*nat type} 
296  162 
We put $nat$ in class $term$ by declaring $nat{::}term$. We declare the 
163 
equality constant by 

105  164 
\begin{eqnarray*} 
165 
{=} & :: & [\alpha{::}term,\alpha]\To o 

166 
\end{eqnarray*} 

296  167 
where $\alpha{::}term$ constrains the type variable~$\alpha$ to class 
168 
$term$. Such type variables resemble Standard~\ML's equality type 

169 
variables. 

170 

312  171 
We give~$o$ and function types the class $logic$ rather than~$term$, since 
105  172 
they are not legal types for terms. We may introduce new types of class 
173 
$term$  for instance, type $string$ or $real$  at any time. We can 

331  174 
even declare type constructors such as~$list$, and state that type 
296  175 
$(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality 
105  176 
applies to lists of natural numbers but not to lists of formulae. We may 
177 
summarize this paragraph by a set of {\bf arity declarations} for type 

312  178 
constructors:\index{arities!declaring} 
179 
\begin{eqnarray*}\index{*o type}\index{*fun type} 

180 
o & :: & logic \\ 

181 
fun & :: & (logic,logic)logic \\ 

105  182 
nat, string, real & :: & term \\ 
312  183 
list & :: & (term)term 
105  184 
\end{eqnarray*} 
312  185 
(Recall that $fun$ is the type constructor for function types.) 
331  186 
In \rmindex{higherorder logic}, equality does apply to truth values and 
296  187 
functions; this requires the arity declarations ${o::term}$ 
312  188 
and ${fun::(term,term)term}$. The class system can also handle 
105  189 
overloading.\index{overloadingbold} We could declare $arith$ to be the 
190 
subclass of $term$ consisting of the `arithmetic' types, such as~$nat$. 

191 
Then we could declare the operators 

192 
\begin{eqnarray*} 

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

194 
\end{eqnarray*} 

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

331  196 
in effect have three sets of operators: 
105  197 
\begin{eqnarray*} 
198 
{+},{},{\times},{/} & :: & [nat,nat]\To nat \\ 

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

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

201 
\end{eqnarray*} 

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

296  203 
separately. We could even introduce the type $(\alpha)vector$ and declare 
204 
its arity as $(arith)arith$. Then we could declare the constant 

105  205 
\begin{eqnarray*} 
296  206 
{+} & :: & [(\alpha)vector,(\alpha)vector]\To (\alpha)vector 
105  207 
\end{eqnarray*} 
296  208 
and specify it in terms of ${+} :: [\alpha,\alpha]\To \alpha$. 
105  209 

296  210 
A type variable may belong to any finite number of classes. Suppose that 
211 
we had declared yet another class $ord \le term$, the class of all 

105  212 
`ordered' types, and a constant 
213 
\begin{eqnarray*} 

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

215 
\end{eqnarray*} 

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

296  217 
$\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and 
218 
$ord$. Semantically the set $\{arith,ord\}$ should be understood as the 

219 
intersection of the sets of types represented by $arith$ and $ord$. Such 

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

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

222 
universal sort}. 

105  223 

296  224 
Even with overloading, each term has a unique, most general type. For this 
225 
to be possible, the class and type declarations must satisfy certain 

331  226 
technical constraints; see 
227 
\iflabelundefined{sec:refdefiningtheories}% 

228 
{Sect.\ Defining Theories in the {\em Reference Manual}}% 

229 
{\S\ref{sec:refdefiningtheories}}. 

105  230 

296  231 

105  232 
\subsection{Higher types and quantifiers} 
312  233 
\index{types!higherbold}\index{quantifiers} 
105  234 
Quantifiers are regarded as operations upon functions. Ignoring polymorphism 
235 
for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges 

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

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

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

239 
represented by a constant 

240 
\begin{eqnarray*} 

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

242 
\end{eqnarray*} 

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

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

245 

246 
The existential quantifier is treated 

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

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

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

250 
\begin{eqnarray*} 

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

252 
\end{eqnarray*} 

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

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

255 
allow summations over all arithmetic types: 

256 
\begin{eqnarray*} 

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

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

259 
\end{eqnarray*} 

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

261 
being summed may belong to any arithmetic type. 

262 

263 

264 
\section{Formalizing logical rules in Isabelle} 

312  265 
\index{metaimplicationbold} 
266 
\index{metaquantifiersbold} 

267 
\index{metaequalitybold} 

296  268 

269 
Objectlogics are formalized by extending Isabelle's 

1878  270 
metalogic~\cite{paulsonfound}, which is intuitionistic higherorder logic. 
296  271 
The metalevel connectives are {\bf implication}, the {\bf universal 
272 
quantifier}, and {\bf equality}. 

105  273 
\begin{itemize} 
274 
\item The implication \(\phi\Imp \psi\) means `\(\phi\) implies 

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

276 

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

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

279 

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

312  281 
{\bf definitions} (see~\S\ref{definitions}).\index{definitions} 
282 
Equalities left over from the unification process, so called {\bf 

283 
flexflex constraints},\index{flexflex constraints} are written $a\qeq 

284 
b$. The two equality symbols have the same logical meaning. 

105  285 

286 
\end{itemize} 

312  287 
The syntax of the metalogic is formalized in the same manner 
288 
as objectlogics, using the simply typed $\lambda$calculus. Analogous to 

105  289 
type~$o$ above, there is a builtin type $prop$ of metalevel truth values. 
290 
Metalevel formulae will have this type. Type $prop$ belongs to 

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

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

312  293 
\begin{eqnarray*}\index{*prop type}\index{*logic class} 
105  294 
\Imp & :: & [prop,prop]\To prop \\ 
295 
\Forall & :: & (\alpha{::}logic\To prop) \To prop \\ 

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

312  297 
\qeq & :: & [\alpha{::}\{\},\alpha]\To prop 
105  298 
\end{eqnarray*} 
312  299 
The polymorphism in $\Forall$ is restricted to class~$logic$ to exclude 
300 
certain types, those used just for parsing. The type variable 

301 
$\alpha{::}\{\}$ ranges over the universal sort. 

105  302 

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

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

305 
we declared the objectlevel connectives to have types such as 

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

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

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

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

310 
we declare the constant 

312  311 
\index{*Trueprop constant} 
105  312 
\begin{eqnarray*} 
313 
Trueprop & :: & o\To prop. 

314 
\end{eqnarray*} 

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

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

317 
from $o$ to $prop$. 

318 

319 

320 
\subsection{Expressing propositional rules} 

312  321 
\index{rules!propositional} 
105  322 
We shall illustrate the use of the metalogic by formalizing the rules of 
296  323 
Fig.\ts\ref{folfig}. Each objectlevel rule is expressed as a metalevel 
105  324 
axiom. 
325 

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

327 
everything explicit, its formalization in the metalogic is 

3103  328 
$$ 
329 
\Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) 

330 
$$ 

105  331 
This may look formidable, but it has an obvious reading: for all objectlevel 
332 
truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The 

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

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

335 

312  336 
\index{*Trueprop constant} 
105  337 
Isabelle adopts notational conventions to ease the writing of rules. We may 
338 
hide the occurrences of $Trueprop$ by making it an implicit coercion. 

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

312  340 
\index{metaimplication} 
105  341 
\[ \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \] 
342 
may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which 

343 
formalizes a rule of $n$~premises. 

344 

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

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

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

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

349 

350 
\noindent 

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

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

331  353 
\index{assumptions!discharge of}% 
105  354 
$$ P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2) $$ 
355 
$$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E) $$ 

331  356 
% 
312  357 
To understand this treatment of assumptions in natural 
105  358 
deduction, look at implication. The rule $({\imp}I)$ is the classic 
359 
example of natural deduction: to prove that $P\imp Q$ is true, assume $P$ 

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

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

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

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

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

365 
specify $\imp$ are 

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

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

368 

369 
\noindent 

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

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

372 

373 
\begin{warn} 

374 
Earlier versions of Isabelle, and certain 

1878  375 
papers~\cite{paulsonfound,paulson700}, use $\List{P}$ to mean $Trueprop(P)$. 
105  376 
\end{warn} 
377 

378 
\subsection{Quantifier rules and substitution} 

312  379 
\index{quantifiers}\index{rules!quantifier}\index{substitutionbold} 
380 
\index{variables!bound}\index{lambda abs@$\lambda$abstractions} 

381 
\index{function applications} 

382 

105  383 
Isabelle expresses variable binding using $\lambda$abstraction; for instance, 
384 
$\forall x.P$ is formalized as $\forall(\lambda x.P)$. Recall that $F(t)$ 

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

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

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

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

389 
inference rules that involve substitution for bound variables. 

390 

391 
\index{parametersbold}\index{eigenvariablessee{parameters}} 

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

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

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

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

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

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

312  398 
\index{metaquantifiers} 
105  399 

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

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

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

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

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

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

406 
$\forall$ axioms are 

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

3103  408 
$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E) $$ 
105  409 

410 
\noindent 

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

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

413 
connectives of the objectlogic! Consider the existential quantifier: 

3103  414 
$$ P(t) \Imp \exists x.P(x) \eqno(\exists I) $$ 
105  415 
$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$ 
416 
Let us verify $(\exists E)$ semantically. Suppose that the premises 

312  417 
hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is 
105  418 
true. Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and 
419 
we obtain the desired conclusion, $Q$. 

420 

421 
The treatment of substitution deserves mention. The rule 

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

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

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

312  425 
rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$ 
426 
from~$P[t/x]$. When we formalize this as an axiom, the template becomes a 

427 
function variable: 

3103  428 
$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst) $$ 
105  429 

430 

431 
\subsection{Signatures and theories} 

312  432 
\index{signaturesbold} 
433 

6170  434 
A {\bf signature} contains the information necessary for typechecking, 
3103  435 
parsing and pretty printing a term. It specifies type classes and their 
331  436 
relationships, types and their arities, constants and their types, etc. It 
3103  437 
also contains grammar rules, specified using mixfix declarations. 
105  438 

439 
Two signatures can be merged provided their specifications are compatible  

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

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

442 
managed internally by Isabelle; users seldom encounter them. 

443 

3103  444 
\index{theoriesbold} A {\bf theory} consists of a signature plus a 
445 
collection of axioms. The {\Pure} theory contains only the 

446 
metalogic. Theories can be combined provided their signatures are 

447 
compatible. A theory definition extends an existing theory with 

448 
further signature specifications  classes, types, constants and 

449 
mixfix declarations  plus lists of axioms and definitions etc., 

450 
expressed as strings to be parsed. A theory can formalize a small 

451 
piece of mathematics, such as lists and their operations, or an entire 

452 
logic. A mathematical development typically involves many theories in 

453 
a hierarchy. For example, the {\Pure} theory could be extended to 

454 
form a theory for Fig.\ts\ref{folfig}; this could be extended in two 

455 
separate ways to form a theory for natural numbers and a theory for 

456 
lists; the union of these two could be extended into a theory defining 

457 
the length of a list: 

296  458 
\begin{tt} 
459 
\[ 

105  460 
\begin{array}{c@{}c@{}c@{}c@{}c} 
3103  461 
{} & {} &\hbox{Pure}& {} & {} \\ 
462 
{} & {} & \downarrow & {} & {} \\ 

463 
{} & {} &\hbox{FOL} & {} & {} \\ 

464 
{} & \swarrow & {} & \searrow & {} \\ 

105  465 
\hbox{Nat} & {} & {} & {} & \hbox{List} \\ 
3103  466 
{} & \searrow & {} & \swarrow & {} \\ 
467 
{} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\ 

468 
{} & {} & \downarrow & {} & {} \\ 

469 
{} & {} & \hbox{Length} & {} & {} 

105  470 
\end{array} 
471 
\] 

331  472 
\end{tt}% 
105  473 
Each Isabelle proof typically works within a single theory, which is 
474 
associated with the proof state. However, many different theories may 

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

476 
session. 

477 

331  478 
\begin{warn}\index{constants!clashes with variables}% 
296  479 
Confusing problems arise if you work in the wrong theory. Each theory 
480 
defines its own syntax. An identifier may be regarded in one theory as a 

3103  481 
constant and in another as a variable, for example. 
296  482 
\end{warn} 
105  483 

484 
\section{Proof construction in Isabelle} 

296  485 
I have elsewhere described the metalogic and demonstrated it by 
1878  486 
formalizing firstorder logic~\cite{paulsonfound}. There is a onetoone 
296  487 
correspondence between metalevel proofs and objectlevel proofs. To each 
488 
use of a metalevel axiom, such as $(\forall I)$, there is a use of the 

489 
corresponding objectlevel rule. Objectlevel assumptions and parameters 

490 
have metalevel counterparts. The metalevel formalization is {\bf 

491 
faithful}, admitting no incorrect objectlevel inferences, and {\bf 

492 
adequate}, admitting all correct objectlevel inferences. These 

493 
properties must be demonstrated separately for each objectlogic. 

105  494 

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

331  496 
equational rules for the $\lambda$calculus and logical rules. The rules 
105  497 
for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in 
296  498 
Fig.\ts\ref{folfig}. Proofs performed using the primitive metarules 
105  499 
would be lengthy; Isabelle proofs normally use certain derived rules. 
500 
{\bf Resolution}, in particular, is convenient for backward proof. 

501 

502 
Unification is central to theorem proving. It supports quantifier 

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

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

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

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

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

508 
quantities often emerge from the proof. 

509 

312  510 
Isabelle provides {\bf schematic variables}, or {\bf 
511 
unknowns},\index{unknowns} for unification. Logically, unknowns are free 

512 
variables. But while ordinary variables remain fixed, unification may 

513 
instantiate unknowns. Unknowns are written with a ?\ prefix and are 

514 
frequently subscripted: $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots, 

515 
$\Var{P}$, $\Var{P@1}$, \ldots. 

105  516 

517 
Recall that an inference rule of the form 

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

519 
is formalized in Isabelle's metalogic as the axiom 

312  520 
$\List{\phi@1; \ldots; \phi@n} \Imp \phi$.\index{resolution} 
296  521 
Such axioms resemble Prolog's Horn clauses, and can be combined by 
105  522 
resolution  Isabelle's principal proof method. Resolution yields both 
523 
forward and backward proof. Backward proof works by unifying a goal with 

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

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

526 

312  527 
Isabelle formulae require an extended notion of resolution. 
296  528 
They differ from Horn clauses in two major respects: 
105  529 
\begin{itemize} 
530 
\item They are written in the typed $\lambda$calculus, and therefore must be 

531 
resolved using higherorder unification. 

532 

296  533 
\item The constituents of a clause need not be atomic formulae. Any 
534 
formula of the form $Trueprop(\cdots)$ is atomic, but axioms such as 

535 
${\imp}I$ and $\forall I$ contain nonatomic formulae. 

105  536 
\end{itemize} 
296  537 
Isabelle has little in common with classical resolution theorem provers 
105  538 
such as Otter~\cite{wosbledsoe}. At the metalevel, Isabelle proves 
539 
theorems in their positive form, not by refutation. However, an 

540 
objectlogic that includes a contradiction rule may employ a refutation 

541 
proof procedure. 

542 

543 

544 
\subsection{Higherorder unification} 

545 
\index{unification!higherorderbold} 

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

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

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

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

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

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

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

553 
\begin{equation} \label{houeqn} 

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

555 
\end{equation} 

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

312  557 
projection. {\bf Imitation} makes~$\Var{f}$ apply the leading symbol (if a 
558 
constant) of the righthand side. To solve equation~(\ref{houeqn}), it 

559 
guesses 

105  560 
\[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \] 
561 
where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns. Assuming there are no 

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

563 
set of equations 

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

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

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

567 

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

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

570 
result of suitable type, it guesses 

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

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

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

574 
equation 

3103  575 
\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). \] 
105  576 

331  577 
\begin{warn}\index{unification!incompleteness of}% 
105  578 
Huet's unification procedure is complete. Isabelle's polymorphic version, 
579 
which solves for type unknowns as well as for term unknowns, is incomplete. 

580 
The problem is that projection requires type information. In 

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

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

583 
similarly unconstrained. Therefore, Isabelle never attempts such 

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

585 
to be a function type. 

586 
\end{warn} 

587 

312  588 
\index{unknowns!functionbold} 
105  589 
Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to 
590 
$n+1$ guesses. The search tree and set of unifiers may be infinite. But 

591 
higherorder unification can work effectively, provided you are careful 

592 
with {\bf function unknowns}: 

593 
\begin{itemize} 

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

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

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

597 
capture the free variable~$x$. 

598 

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

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

601 
match the corresponding variables. 

602 

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

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

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3106
diff
changeset

605 
imitation. The first solution is usually the one desired: 
105  606 
\[ \Var{f}\equiv \lambda x. x+x \quad 
607 
\Var{f}\equiv \lambda x. a+x \quad 

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

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

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

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

612 
avoided. 

613 
\end{itemize} 

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

615 
invoking unification. 

616 

617 

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

619 
\index{resolutionbold} 

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

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

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

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

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

625 
By resolution, we may conclude 

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

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

628 
\] 

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

630 
resolution is the following rule: 

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

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

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

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

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

636 
\] 

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

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

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

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

641 
conclusions as a sequence (lazy list). 

642 

3103  643 
Resolution expects the rules to have no outer quantifiers~($\Forall$). 
644 
It may rename or instantiate any schematic variables, but leaves free 

645 
variables unchanged. When constructing a theory, Isabelle puts the 

3106  646 
rules into a standard form with all free variables converted into 
647 
schematic ones; for instance, $({\imp}E)$ becomes 

105  648 
\[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}. 
649 
\] 

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

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

331  652 
resolve $({\imp}E)$ with itself, the first copy of the rule becomes 
105  653 
\[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}. \] 
654 
Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with 

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

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

657 
\Imp\Var{Q}.} 

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

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

660 
\] 

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

331  662 
objectlevel rule\index{rules!derived} 
105  663 
\[ \infer{Q.}{R\imp (P\imp Q) & R & P} \] 
664 
Joining rules in this fashion is a simple way of proving theorems. The 

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

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

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

668 

669 
\noindent 

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

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

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

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

674 
unchanged, yielding 

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

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

677 
and yields 

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

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

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

681 
\] 

682 
We have derived the rule 

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

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

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

686 

687 

296  688 
\section{Lifting a rule into a context} 
105  689 
The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for 
690 
resolution. They have nonatomic premises, namely $P\Imp Q$ and $\Forall 

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

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

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

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

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

296  696 
{\infer*{R}{[P,Q]}}} 
105  697 
\qquad 
698 
\infer[(\forall I)]{\forall x\,y.P(x,y)} 

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

700 
\] 

701 

296  702 
\subsection{Lifting over assumptions} 
312  703 
\index{assumptions!lifting over} 
105  704 
Lifting over $\theta\Imp{}$ is the following metainference rule: 
705 
\[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp 

706 
(\theta \Imp \phi)} 

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

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

296  709 
$\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$ and $\theta$ are all true then 
105  710 
$\phi$ must be true. Iterated lifting over a series of metaformulae 
711 
$\theta@k$, \ldots, $\theta@1$ yields an objectrule whose conclusion is 

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

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

714 
premises and conclusion. 

715 

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

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

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

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

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

296  721 
$\Var{P}\Imp{}$ to obtain 
722 
\[ (\Var{P}\Imp (\Var{P@1} \Imp \Var{Q@1})) \Imp (\Var{P} \Imp 

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

724 
Using the $\List{\cdots}$ abbreviation, this can be written as 

105  725 
\[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} 
726 
\Imp \Var{P@1}\imp \Var{Q@1}. \] 

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

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

729 
Resolution yields 

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

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

732 
This represents the derived rule 

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

734 

296  735 
\subsection{Lifting over parameters} 
312  736 
\index{parameters!lifting over} 
105  737 
An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. 
738 
Here, lifting prefixes an objectrule's premises and conclusion with $\Forall 

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

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

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

742 
short, lifting is the metainference 

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

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

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

296  746 
% 
747 
where $\phi^x$ stands for the result of lifting unknowns over~$x$ in 

748 
$\phi$. It is not hard to verify that this metainference is sound. If 

749 
$\phi\Imp\psi$ then $\phi^x\Imp\psi^x$ for all~$x$; so if $\phi^x$ is true 

750 
for all~$x$ then so is $\psi^x$. Thus, from $\phi\Imp\psi$ we conclude 

751 
$(\Forall x.\phi^x) \Imp (\Forall x.\psi^x)$. 

752 

105  753 
For example, $(\disj I)$ might be lifted to 
754 
\[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\] 

755 
and $(\forall I)$ to 

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

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

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

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

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

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

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

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

764 
resolvent expresses the derived rule 

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

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

767 
\] 

1878  768 
I discuss lifting and parameters at length elsewhere~\cite{paulsonfound}. 
296  769 
Miller goes into even greater detail~\cite{millermixed}. 
105  770 

771 

772 
\section{Backward proof by resolution} 

312  773 
\index{resolution!in backward proof} 
296  774 

105  775 
Resolution is convenient for deriving simple rules and for reasoning 
776 
forward from facts. It can also support backward proof, where we start 

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

296  778 
been solved. {\sc lcf} and its descendants {\sc hol} and Nuprl provide 
3103  779 
tactics and tacticals, which constitute a sophisticated language for 
296  780 
expressing proof searches. {\bf Tactics} refine subgoals while {\bf 
781 
tacticals} combine tactics. 

105  782 

312  783 
\index{LCF system} 
105  784 
Isabelle's tactics and tacticals work differently from {\sc lcf}'s. An 
296  785 
Isabelle rule is bidirectional: there is no distinction between 
105  786 
inputs and outputs. {\sc lcf} has a separate tactic for each rule; 
787 
Isabelle performs refinement by any rule in a uniform fashion, using 

788 
resolution. 

789 

790 
Isabelle works with metalevel theorems of the form 

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

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

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

312  794 
the {\bf proof state}\index{proof state} 
795 
with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main 

105  796 
goal~$\phi$. 
797 

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

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

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

296  801 
\Imp \phi$. This proof state is a theorem, ensuring that the subgoals 
802 
$\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$. If $n=0$ then we have 

105  803 
proved~$\phi$ outright. If $\phi$ contains unknowns, they may become 
804 
instantiated during the proof; a proof state may be $\List{\phi@1; \ldots; 

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

806 

807 
\subsection{Refinement by resolution} 

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

809 
resolution: 

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

331  811 
Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after 
812 
lifting over subgoal~$i$'s assumptions and parameters. If the proof state 

813 
is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is 

814 
(for~$1\leq i\leq n$) 

105  815 
\[ (\List{\phi@1; \ldots; \phi@{i1}; \psi'@1; 
816 
\ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \] 

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

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

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

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

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

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

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

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

825 
the proof state. 

826 

827 
\subsection{Proof by assumption} 

312  828 
\index{assumptions!use of} 
105  829 
In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and 
830 
assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for 

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

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

833 
parameters at the front: 

834 
\begin{equation} \label{contexteqn} 

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

836 
\end{equation} 

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

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

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

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

841 
models proof by assumption in natural deduction. 

842 

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

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

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

846 
are metatheorems of the form 

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

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

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

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

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

1878  852 
parameter provisos~\cite{paulsonfound}. 
105  853 

296  854 
The premise represents a proof state with~$n$ subgoals, of which the~$i$th 
855 
is to be solved by assumption. Isabelle searches the subgoal's context for 

856 
an assumption~$\theta@j$ that can solve it. For each unifier, the 

857 
metainference returns an instantiated proof state from which the $i$th 

858 
subgoal has been removed. Isabelle searches for a unifying assumption; for 

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

105  860 

296  861 
Consider the proof state 
862 
\[ (\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x}). \] 

105  863 
Proof by assumption (with $i=1$, the only possibility) yields two results: 
864 
\begin{itemize} 

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

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

867 
\end{itemize} 

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

296  869 
other subgoals; if we also had the subgoal ${\List{P(b); P(c)} \Imp 
870 
P(\Var{x})}$, then $\Var{x}\equiv a$ would transform it to ${\List{P(b); 

871 
P(c)} \Imp P(a)}$, which might be unprovable. 

872 

105  873 

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

875 
\index{examples!propositional} 

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

877 
P$, Isabelle creates the initial state 

296  878 
\[ (P\disj P\imp P)\Imp (P\disj P\imp P). \] 
879 
% 

105  880 
Bear in mind that every proof state we derive will be a metatheorem, 
296  881 
expressing that the subgoals imply the main goal. Our aim is to reach the 
882 
state $P\disj P\imp P$; this metatheorem is the desired result. 

883 

884 
The first step is to refine subgoal~1 by (${\imp}I)$, creating a new state 

885 
where $P\disj P$ is an assumption: 

105  886 
\[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \] 
887 
The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. 

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

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

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

891 
metatheorem, laid out for clarity: 

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

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

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

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

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

897 
\end{array} 

898 
\] 

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

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

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

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

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

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

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

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

907 
\end{array} \] 

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

296  909 
steps, the proof state is $P\disj P\imp P$. 
910 

105  911 

912 
\subsection{A quantifier proof} 

913 
\index{examples!with quantifiers} 

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

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

916 
state is the trivial metatheorem 

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

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

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

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

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

922 
\] 

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

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

925 
state is the metatheorem 

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

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

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

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

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

931 
\end{array} 

932 
\] 

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

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

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

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

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

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

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

940 
\] 

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

296  942 
context of the parameter~$x$ and the assumption $P(f(x))$. This copies 
943 
the context to the subgoal and allows the existential witness to 

105  944 
depend upon~$x$: 
945 
\[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp 

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

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

948 
\] 

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

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

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

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

953 

954 

955 
\subsection{Tactics and tacticals} 

956 
\index{tacticsbold}\index{tacticalsbold} 

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

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

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

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

296  961 
successor states. Lazy lists are coded in ML as functions, a standard 
6592  962 
technique~\cite{paulsonml2}. Isabelle represents proof states by theorems. 
105  963 

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

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

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

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

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

969 
essential because higherorder resolution may return infinitely many 

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

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

972 
said to {\bf fail}. 

973 

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

975 
for combining tactics. Depthfirst search, breadthfirst search and 

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

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

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

312  979 
directly using the basic tacticals {\tt THEN}, {\tt ORELSE} and {\tt REPEAT}: 
980 
\begin{ttdescription} 

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

105  982 
to a proof state, it returns all states reachable in two steps by applying 
983 
$tac1$ followed by~$tac2$. 

984 

312  985 
\item[$tac1$ ORELSE $tac2$] is a choice tactic. Applied to a state, it 
105  986 
tries~$tac1$ and returns the result if nonempty; otherwise, it uses~$tac2$. 
987 

312  988 
\item[REPEAT $tac$] is a repetition tactic. Applied to a state, it 
331  989 
returns all states reachable by applying~$tac$ as long as possible  until 
990 
it would fail. 

312  991 
\end{ttdescription} 
105  992 
For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving 
993 
$tac1$ priority: 

312  994 
\begin{center} \tt 
995 
REPEAT($tac1$ ORELSE $tac2$) 

996 
\end{center} 

105  997 

998 

999 
\section{Variations on resolution} 

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

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

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

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

1004 
style. 

1005 

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

1007 
can also serve to derive rules. 

1008 

1009 
\subsection{Elimresolution} 

312  1010 
\index{elimresolutionbold}\index{assumptions!deleting} 
1011 

105  1012 
Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By 
331  1013 
$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$. 
105  1014 
Applying $(\disj E)$ to this assumption yields two subgoals, one that 
1015 
assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj 

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

1017 
natural deduction never discards assumptions, we eventually generate a 

1018 
subgoal containing much that is redundant: 

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

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

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

331  1022 
$P\disj Q$ is redundant. Other elimination rules behave 
1023 
similarly. In firstorder logic, only universally quantified 

105  1024 
assumptions are sometimes needed more than once  say, to prove 
1025 
$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$. 

1026 

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

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

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

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

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

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

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

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

1035 
assumptions, can be tiresome to use. 

1036 

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

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

296  1039 
assumption. Elimresolution combines two metatheorems: 
1040 
\begin{itemize} 

1041 
\item a rule $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ 

1042 
\item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ 

1043 
\end{itemize} 

1044 
The rule must have at least one premise, thus $m>0$. Write the rule's 

1045 
lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$. Suppose we 

1046 
wish to change subgoal number~$i$. 

1047 

1048 
Ordinary resolution would attempt to reduce~$\phi@i$, 

1049 
replacing subgoal~$i$ by $m$ new ones. Elimresolution tries 

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

105  1051 
returns a sequence of next states. Each of these replaces subgoal~$i$ by 
1052 
instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected 

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

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

1055 
premise after lifting, will be 

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

296  1057 
Elimresolution tries to unify $\psi'\qeq\phi@i$ and 
1058 
$\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$ simultaneously, for 

1059 
$j=1$,~\ldots,~$k$. 

105  1060 

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

1062 
is~$(\disj E)$, 

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

1064 
\Imp \Var{R} \] 

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

331  1066 
lifted rule is 
105  1067 
\[ \begin{array}{l@{}l} 
1068 
\lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\ 

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

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

1865  1071 
\rbrakk\;& \Imp (P\disj P \Imp \Var{R@1}) 
105  1072 
\end{array} 
1073 
\] 

331  1074 
Unification takes the simultaneous equations 
105  1075 
$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding 
1076 
$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state 

331  1077 
is simply 
105  1078 
\[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). 
1079 
\] 

1080 
Elimresolution's simultaneous unification gives better control 

1081 
than ordinary resolution. Recall the substitution rule: 

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

3103  1083 
\eqno(subst) $$ 
105  1084 
Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many 
1085 
unifiers, $(subst)$ works well with elimresolution. It deletes some 

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

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

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

1089 
formula. 

1090 

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

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

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

1094 
Isabelle. 

1095 

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

312  1097 
\index{rules!destruction}\index{rules!elimination} 
1098 
\index{forward proof} 

1099 

296  1100 
Looking back to Fig.\ts\ref{folfig}, notice that there are two kinds of 
105  1101 
elimination rule. The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and 
1102 
$({\forall}E)$ extract the conclusion from the major premise. In Isabelle 

312  1103 
parlance, such rules are called {\bf destruction rules}; they are readable 
105  1104 
and easy to use in forward proof. The rules $({\disj}E)$, $({\bot}E)$ and 
1105 
$({\exists}E)$ work by discharging assumptions; they support backward proof 

1106 
in a style reminiscent of the sequent calculus. 

1107 

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

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

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

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

1112 
\[ 

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

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

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

1116 
\] 

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

1118 
corresponding elimination rules. To facilitate their use in backward 

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

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

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

1122 
\] 

331  1123 
{\bf Destructresolution}\index{destructresolution} combines this 
1124 
transformation with elimresolution. It applies a destruction rule to some 

1125 
assumption of a subgoal. Given the rule above, it replaces the 

1126 
assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$, 

1127 
\ldots,~$P@m$. Destructresolution works forward from a subgoal's 

1128 
assumptions. Ordinary resolution performs forward reasoning from theorems, 

1129 
as illustrated in~\S\ref{joining}. 

105  1130 

1131 

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

312  1133 
\index{rules!derivedbold}\index{metaassumptions!syntax of} 
105  1134 
The metalogic, itself a form of the predicate calculus, is defined by a 
1135 
system of natural deduction rules. Each theorem may depend upon 

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

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

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

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

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

1141 

1142 
Metalevel natural deduction provides a convenient mechanism for deriving 

1143 
new objectlevel rules. To derive the rule 

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

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

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

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

1148 
reaching a final state such as 

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

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

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

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

1153 
assumptions. This represents the desired rule. 

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

3103  1155 
$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E) $$ 
105  1156 
We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in 
1157 
the state $R\Imp R$. Resolving this with the second assumption yields the 

1158 
state 

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

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

331  1161 
Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$, 
105  1162 
respectively, yields the state 
331  1163 
\[ \List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R 
1164 
\quad [\,\List{P;Q}\Imp R\,]. 

1165 
\] 

1166 
The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained 

1167 
subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$. Resolving 

1168 
both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield 

105  1169 
\[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \] 
1170 
The proof may use the metaassumptions in any order, and as often as 

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

1172 
obtain the desired form: 

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

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

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

1176 
schematic variables. 

1177 

1178 
\begin{warn} 

331  1179 
Schematic variables are not allowed in metaassumptions, for a variety of 
1180 
reasons. Metaassumptions remain fixed throughout a proof. 

105  1181 
\end{warn} 
1182 