author  paulson 
Wed, 20 Mar 1996 18:36:59 +0100  
changeset 1590  1547174673e1 
parent 1119  49ed9a415637 
child 1846  763f08fb194f 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Theorems and Forward Proof} 

3 
\index{theorems(} 

326  4 

104  5 
Theorems, which represent the axioms, theorems and rules of objectlogics, 
326  6 
have type \mltydx{thm}. This chapter begins by describing operations that 
7 
print theorems and that join them in forward proof. Most theorem 

8 
operations are intended for advanced applications, such as programming new 

9 
proof procedures. Many of these operations refer to signatures, certified 

10 
terms and certified types, which have the \ML{} types {\tt Sign.sg}, {\tt 

11 
Sign.cterm} and {\tt Sign.ctyp} and are discussed in 

104  12 
Chapter~\ref{theories}. Beginning users should ignore such complexities 
13 
 and skip all but the first section of this chapter. 

14 

15 
The theorem operations do not print error messages. Instead, they raise 

326  16 
exception~\xdx{THM}\@. Use \ttindex{print_exn} to display 
104  17 
exceptions nicely: 
18 
\begin{ttbox} 

19 
allI RS mp handle e => print_exn e; 

20 
{\out Exception THM raised:} 

21 
{\out RSN: no unifiers  premise 1} 

22 
{\out (!!x. ?P(x)) ==> ALL x. ?P(x)} 

23 
{\out [ ?P > ?Q; ?P ] ==> ?Q} 

24 
{\out} 

25 
{\out uncaught exception THM} 

26 
\end{ttbox} 

27 

28 

29 
\section{Basic operations on theorems} 

30 
\subsection{Prettyprinting a theorem} 

326  31 
\index{theorems!printing of} 
104  32 
\begin{ttbox} 
326  33 
prth : thm > thm 
34 
prths : thm list > thm list 

35 
prthq : thm Sequence.seq > thm Sequence.seq 

36 
print_thm : thm > unit 

37 
print_goals : int > thm > unit 

38 
string_of_thm : thm > string 

104  39 
\end{ttbox} 
326  40 
The first three commands are for interactive use. They are identity 
41 
functions that display, then return, their argument. The \ML{} identifier 

42 
{\tt it} will refer to the value just displayed. 

43 

44 
The others are for use in programs. Functions with result type {\tt unit} 

45 
are convenient for imperative programming. 

46 

47 
\begin{ttdescription} 

104  48 
\item[\ttindexbold{prth} {\it thm}] 
49 
prints {\it thm\/} at the terminal. 

50 

51 
\item[\ttindexbold{prths} {\it thms}] 

52 
prints {\it thms}, a list of theorems. 

53 

54 
\item[\ttindexbold{prthq} {\it thmq}] 

55 
prints {\it thmq}, a sequence of theorems. It is useful for inspecting 

56 
the output of a tactic. 

57 

58 
\item[\ttindexbold{print_thm} {\it thm}] 

59 
prints {\it thm\/} at the terminal. 

60 

61 
\item[\ttindexbold{print_goals} {\it limit\/} {\it thm}] 

62 
prints {\it thm\/} in goal style, with the premises as subgoals. It prints 

63 
at most {\it limit\/} subgoals. The subgoal module calls {\tt print_goals} 

64 
to display proof states. 

65 

66 
\item[\ttindexbold{string_of_thm} {\it thm}] 

67 
converts {\it thm\/} to a string. 

326  68 
\end{ttdescription} 
104  69 

70 

326  71 
\subsection{Forward proof: joining rules by resolution} 
72 
\index{theorems!joining by resolution} 

73 
\index{resolution}\index{forward proof} 

104  74 
\begin{ttbox} 
75 
RSN : thm * (int * thm) > thm \hfill{\bf infix} 

76 
RS : thm * thm > thm \hfill{\bf infix} 

77 
MRS : thm list * thm > thm \hfill{\bf infix} 

78 
RLN : thm list * (int * thm list) > thm list \hfill{\bf infix} 

79 
RL : thm list * thm list > thm list \hfill{\bf infix} 

326  80 
MRL : thm list list * thm list > thm list \hfill{\bf infix} 
104  81 
\end{ttbox} 
326  82 
Joining rules together is a simple way of deriving new rules. These 
876  83 
functions are especially useful with destruction rules. To store 
84 
the result in the theorem database, use \ttindex{bind_thm} 

85 
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 

326  86 
\begin{ttdescription} 
104  87 
\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} 
326  88 
resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$. 
89 
Unless there is precisely one resolvent it raises exception 

90 
\xdx{THM}; in that case, use {\tt RLN}. 

104  91 

92 
\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS} 

93 
abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}. Thus, it resolves the 

94 
conclusion of $thm@1$ with the first premise of~$thm@2$. 

95 

96 
\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS} 

332  97 
uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for 
104  98 
$i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$ 
99 
premises of $thm$. Because the theorems are used from right to left, it 

100 
does not matter if the $thm@i$ create new premises. {\tt MRS} is useful 

101 
for expressing proof trees. 

102 

151  103 
\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN} 
326  104 
joins lists of theorems. For every $thm@1$ in $thms@1$ and $thm@2$ in 
105 
$thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise 

106 
of~$thm@2$, accumulating the results. 

104  107 

151  108 
\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL} 
109 
abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}. 

104  110 

111 
\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL} 

112 
is analogous to {\tt MRS}, but combines theorem lists rather than theorems. 

113 
It too is useful for expressing proof trees. 

326  114 
\end{ttdescription} 
104  115 

116 

117 
\subsection{Expanding definitions in theorems} 

326  118 
\index{metarewriting!in theorems} 
104  119 
\begin{ttbox} 
120 
rewrite_rule : thm list > thm > thm 

121 
rewrite_goals_rule : thm list > thm > thm 

122 
\end{ttbox} 

326  123 
\begin{ttdescription} 
104  124 
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}] 
125 
unfolds the {\it defs} throughout the theorem~{\it thm}. 

126 

127 
\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}] 

128 
unfolds the {\it defs} in the premises of~{\it thm}, but leaves the 

129 
conclusion unchanged. This rule underlies \ttindex{rewrite_goals_tac}, but 

130 
serves little purpose in forward proof. 

326  131 
\end{ttdescription} 
104  132 

133 

326  134 
\subsection{Instantiating a theorem} 
135 
\index{instantiation} 

286  136 
\begin{ttbox} 
104  137 
read_instantiate : (string*string)list > thm > thm 
138 
read_instantiate_sg : Sign.sg > (string*string)list > thm > thm 

139 
cterm_instantiate : (Sign.cterm*Sign.cterm)list > thm > thm 

140 
\end{ttbox} 

141 
These metarules instantiate type and term unknowns in a theorem. They are 

142 
occasionally useful. They can prevent difficulties with higherorder 

143 
unification, and define specialized versions of rules. 

326  144 
\begin{ttdescription} 
104  145 
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}] 
146 
processes the instantiations {\it insts} and instantiates the rule~{\it 

147 
thm}. The processing of instantiations is described 

326  148 
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}. 
104  149 

150 
Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule 

151 
and refine a particular subgoal. The tactic allows instantiation by the 

152 
subgoal's parameters, and reads the instantiations using the signature 

326  153 
associated with the proof state. 
154 

155 
Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated 

156 
incorrectly. 

104  157 

326  158 
\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}] 
159 
resembles \hbox{\tt read_instantiate {\it insts} {\it thm}}, but reads 

160 
the instantiations under signature~{\it sg}. This is necessary to 

161 
instantiate a rule from a general theory, such as firstorder logic, 

162 
using the notation of some specialized theory. Use the function {\tt 

163 
sign_of} to get a theory's signature. 

104  164 

165 
\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}] 

166 
is similar to {\tt read_instantiate}, but the instantiations are provided 

167 
as pairs of certified terms, not as strings to be read. 

326  168 
\end{ttdescription} 
104  169 

170 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

171 
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules} 
326  172 
\index{theorems!standardizing} 
104  173 
\begin{ttbox} 
332  174 
standard : thm > thm 
175 
zero_var_indexes : thm > thm 

176 
make_elim : thm > thm 

104  177 
rule_by_tactic : tactic > thm > thm 
178 
\end{ttbox} 

326  179 
\begin{ttdescription} 
104  180 
\item[\ttindexbold{standard} $thm$] 
181 
puts $thm$ into the standard form of objectrules. It discharges all 

332  182 
metaassumptions, replaces free variables by schematic variables, and 
104  183 
renames schematic variables to have subscript zero. 
184 

185 
\item[\ttindexbold{zero_var_indexes} $thm$] 

186 
makes all schematic variables have subscript zero, renaming them to avoid 

187 
clashes. 

188 

189 
\item[\ttindexbold{make_elim} $thm$] 

190 
\index{rules!converting destruction to elimination} 

191 
converts $thm$, a destruction rule of the form $\List{P@1;\ldots;P@m}\Imp 

192 
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This 

193 
is the basis for destructresolution: {\tt dresolve_tac}, etc. 

194 

195 
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}] 

196 
applies {\it tac\/} to the {\it thm}, freezing its variables first, then 

197 
yields the proof state returned by the tactic. In typical usage, the 

198 
{\it thm\/} represents an instance of a rule with several premises, some 

199 
with contradictory assumptions (because of the instantiation). The 

200 
tactic proves those subgoals and does whatever else it can, and returns 

201 
whatever is left. 

326  202 
\end{ttdescription} 
104  203 

204 

205 
\subsection{Taking a theorem apart} 

326  206 
\index{theorems!taking apart} 
104  207 
\index{flexflex constraints} 
208 
\begin{ttbox} 

209 
concl_of : thm > term 

210 
prems_of : thm > term list 

211 
nprems_of : thm > int 

212 
tpairs_of : thm > (term*term)list 

213 
stamps_of_thy : thm > string ref list 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

214 
theory_of_thm : thm > theory 
286  215 
dest_state : thm*int > (term*term)list*term list*term*term 
1590  216 
rep_thm : thm > \{prop: term, hyps: term list, 
217 
maxidx: int, der: deriv, sign: Sign.sg\} 

104  218 
\end{ttbox} 
326  219 
\begin{ttdescription} 
104  220 
\item[\ttindexbold{concl_of} $thm$] 
221 
returns the conclusion of $thm$ as a term. 

222 

223 
\item[\ttindexbold{prems_of} $thm$] 

224 
returns the premises of $thm$ as a list of terms. 

225 

226 
\item[\ttindexbold{nprems_of} $thm$] 

286  227 
returns the number of premises in $thm$, and is equivalent to {\tt 
228 
length(prems_of~$thm$)}. 

104  229 

230 
\item[\ttindexbold{tpairs_of} $thm$] 

231 
returns the flexflex constraints of $thm$. 

232 

233 
\item[\ttindexbold{stamps_of_thm} $thm$] 

332  234 
returns the \rmindex{stamps} of the signature associated with~$thm$. 
104  235 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

236 
\item[\ttindexbold{theory_of_thm} $thm$] 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

237 
returns the theory associated with $thm$. 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

238 

104  239 
\item[\ttindexbold{dest_state} $(thm,i)$] 
240 
decomposes $thm$ as a tuple containing a list of flexflex constraints, a 

241 
list of the subgoals~1 to~$i1$, subgoal~$i$, and the rest of the theorem 

242 
(this will be an implication if there are more than $i$ subgoals). 

243 

244 
\item[\ttindexbold{rep_thm} $thm$] 

245 
decomposes $thm$ as a record containing the statement of~$thm$, its list of 

332  246 
metaassumptions, the maximum subscript of its unknowns, and its signature. 
326  247 
\end{ttdescription} 
104  248 

249 

250 
\subsection{Tracing flags for unification} 

326  251 
\index{tracing!of unification} 
104  252 
\begin{ttbox} 
253 
Unify.trace_simp : bool ref \hfill{\bf initially false} 

254 
Unify.trace_types : bool ref \hfill{\bf initially false} 

255 
Unify.trace_bound : int ref \hfill{\bf initially 10} 

256 
Unify.search_bound : int ref \hfill{\bf initially 20} 

257 
\end{ttbox} 

258 
Tracing the search may be useful when higherorder unification behaves 

259 
unexpectedly. Letting {\tt res_inst_tac} circumvent the problem is easier, 

260 
though. 

326  261 
\begin{ttdescription} 
262 
\item[Unify.trace_simp := true;] 

104  263 
causes tracing of the simplification phase. 
264 

326  265 
\item[Unify.trace_types := true;] 
104  266 
generates warnings of incompleteness, when unification is not considering 
267 
all possible instantiations of type unknowns. 

268 

326  269 
\item[Unify.trace_bound := $n$;] 
104  270 
causes unification to print tracing information once it reaches depth~$n$. 
271 
Use $n=0$ for full tracing. At the default value of~10, tracing 

272 
information is almost never printed. 

273 

326  274 
\item[Unify.search_bound := $n$;] 
104  275 
causes unification to limit its search to depth~$n$. Because of this 
276 
bound, higherorder unification cannot return an infinite sequence, though 

277 
it can return a very long one. The search rarely approaches the default 

278 
value of~20. If the search is cut off, unification prints {\tt 

279 
***Unification bound exceeded}. 

326  280 
\end{ttdescription} 
104  281 

282 

283 
\section{Primitive metalevel inference rules} 

284 
\index{metarules(} 

285 
These implement the metalogic in {\sc lcf} style, as functions from theorems 

286 
to theorems. They are, rarely, useful for deriving results in the pure 

287 
theory. Mainly, they are included for completeness, and most users should 

326  288 
not bother with them. The metarules raise exception \xdx{THM} to signal 
104  289 
malformed premises, incompatible signatures and similar errors. 
290 

326  291 
\index{metaassumptions} 
104  292 
The metalogic uses natural deduction. Each theorem may depend on 
332  293 
metalevel assumptions. Certain rules, such as $({\Imp}I)$, 
104  294 
discharge assumptions; in most other rules, the conclusion depends on all 
295 
of the assumptions of the premises. Formally, the system works with 

296 
assertions of the form 

297 
\[ \phi \quad [\phi@1,\ldots,\phi@n], \] 

332  298 
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. Do not confuse 
104  299 
metalevel assumptions with the objectlevel assumptions in a subgoal, 
300 
which are represented in the metalogic using~$\Imp$. 

301 

302 
Each theorem has a signature. Certified terms have a signature. When a 

303 
rule takes several premises and certified terms, it merges the signatures 

304 
to make a signature for the conclusion. This fails if the signatures are 

305 
incompatible. 

306 

326  307 
\index{metaimplication} 
332  308 
The {\bf implication} rules are $({\Imp}I)$ 
104  309 
and $({\Imp}E)$: 
310 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

311 
\infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi} \] 

312 

326  313 
\index{metaequality} 
104  314 
Equality of truth values means logical equivalence: 
315 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} & 

286  316 
\infer*{\phi}{[\psi]}} 
104  317 
\qquad 
318 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

319 

332  320 
The {\bf equality} rules are reflexivity, symmetry, and transitivity: 
104  321 
\[ {a\equiv a}\,(refl) \qquad 
322 
\infer[(sym)]{b\equiv a}{a\equiv b} \qquad 

323 
\infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c} \] 

324 

326  325 
\index{lambda calc@$\lambda$calculus} 
104  326 
The $\lambda$conversions are $\alpha$conversion, $\beta$conversion, and 
327 
extensionality:\footnote{$\alpha$conversion holds if $y$ is not free 

328 
in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.} 

329 
\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])} \qquad 

330 
{((\lambda x.a)(b)) \equiv a[b/x]} \qquad 

331 
\infer[(ext)]{f\equiv g}{f(x) \equiv g(x)} \] 

332 

332  333 
The {\bf abstraction} and {\bf combination} rules let conversions be 
334 
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the 

104  335 
assumptions.} 
336 
\[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad 

337 
\infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b} \] 

338 

326  339 
\index{metaquantifiers} 
332  340 
The {\bf universal quantification} rules are $(\Forall I)$ and $(\Forall 
104  341 
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.} 
342 
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad 

286  343 
\infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi} \] 
104  344 

345 

326  346 
\subsection{Assumption rule} 
347 
\index{metaassumptions} 

104  348 
\begin{ttbox} 
349 
assume: Sign.cterm > thm 

350 
\end{ttbox} 

326  351 
\begin{ttdescription} 
104  352 
\item[\ttindexbold{assume} $ct$] 
332  353 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  354 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  355 
are not allowed in assumptions. 
326  356 
\end{ttdescription} 
104  357 

326  358 
\subsection{Implication rules} 
359 
\index{metaimplication} 

104  360 
\begin{ttbox} 
361 
implies_intr : Sign.cterm > thm > thm 

362 
implies_intr_list : Sign.cterm list > thm > thm 

363 
implies_intr_hyps : thm > thm 

364 
implies_elim : thm > thm > thm 

365 
implies_elim_list : thm > thm list > thm 

366 
\end{ttbox} 

326  367 
\begin{ttdescription} 
104  368 
\item[\ttindexbold{implies_intr} $ct$ $thm$] 
369 
is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$. It 

332  370 
maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all 
371 
occurrences of~$\phi$ from the assumptions. The rule checks that $ct$ has 

372 
type $prop$. 

104  373 

374 
\item[\ttindexbold{implies_intr_list} $cts$ $thm$] 

375 
applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$. 

376 

377 
\item[\ttindexbold{implies_intr_hyps} $thm$] 

332  378 
applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$. 
379 
It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion 

104  380 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
381 

382 
\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] 

383 
applies $({\Imp}E)$ to $thm@1$ and~$thm@2$. It maps the premises $\phi\Imp 

384 
\psi$ and $\phi$ to the conclusion~$\psi$. 

385 

386 
\item[\ttindexbold{implies_elim_list} $thm$ $thms$] 

387 
applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in 

151  388 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  389 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  390 
\end{ttdescription} 
104  391 

326  392 
\subsection{Logical equivalence rules} 
393 
\index{metaequality} 

104  394 
\begin{ttbox} 
326  395 
equal_intr : thm > thm > thm 
396 
equal_elim : thm > thm > thm 

104  397 
\end{ttbox} 
326  398 
\begin{ttdescription} 
104  399 
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] 
332  400 
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$ 
401 
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of 

402 
the first premise with~$\phi$ removed, plus those of 

403 
the second premise with~$\psi$ removed. 

104  404 

405 
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] 

406 
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises 

407 
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$. 

326  408 
\end{ttdescription} 
104  409 

410 

411 
\subsection{Equality rules} 

326  412 
\index{metaequality} 
104  413 
\begin{ttbox} 
414 
reflexive : Sign.cterm > thm 

415 
symmetric : thm > thm 

416 
transitive : thm > thm > thm 

417 
\end{ttbox} 

326  418 
\begin{ttdescription} 
104  419 
\item[\ttindexbold{reflexive} $ct$] 
151  420 
makes the theorem \(ct\equiv ct\). 
104  421 

422 
\item[\ttindexbold{symmetric} $thm$] 

423 
maps the premise $a\equiv b$ to the conclusion $b\equiv a$. 

424 

425 
\item[\ttindexbold{transitive} $thm@1$ $thm@2$] 

426 
maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$. 

326  427 
\end{ttdescription} 
104  428 

429 

430 
\subsection{The $\lambda$conversion rules} 

326  431 
\index{lambda calc@$\lambda$calculus} 
104  432 
\begin{ttbox} 
433 
beta_conversion : Sign.cterm > thm 

434 
extensional : thm > thm 

435 
abstract_rule : string > Sign.cterm > thm > thm 

436 
combination : thm > thm > thm 

437 
\end{ttbox} 

326  438 
There is no rule for $\alpha$conversion because Isabelle regards 
439 
$\alpha$convertible theorems as equal. 

440 
\begin{ttdescription} 

104  441 
\item[\ttindexbold{beta_conversion} $ct$] 
442 
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the 

443 
term $(\lambda x.a)(b)$. 

444 

445 
\item[\ttindexbold{extensional} $thm$] 

446 
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$. 

447 
Parameter~$x$ is taken from the premise. It may be an unknown or a free 

332  448 
variable (provided it does not occur in the assumptions); it must not occur 
104  449 
in $f$ or~$g$. 
450 

451 
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] 

452 
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv 

453 
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$. 

454 
Parameter~$x$ is supplied as a cterm. It may be an unknown or a free 

332  455 
variable (provided it does not occur in the assumptions). In the 
104  456 
conclusion, the bound variable is named~$v$. 
457 

458 
\item[\ttindexbold{combination} $thm@1$ $thm@2$] 

459 
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv 

460 
g(b)$. 

326  461 
\end{ttdescription} 
104  462 

463 

326  464 
\subsection{Forall introduction rules} 
465 
\index{metaquantifiers} 

104  466 
\begin{ttbox} 
467 
forall_intr : Sign.cterm > thm > thm 

468 
forall_intr_list : Sign.cterm list > thm > thm 

469 
forall_intr_frees : thm > thm 

470 
\end{ttbox} 

471 

326  472 
\begin{ttdescription} 
104  473 
\item[\ttindexbold{forall_intr} $x$ $thm$] 
474 
applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$. 

475 
The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$. 

476 
Parameter~$x$ is supplied as a cterm. It may be an unknown or a free 

332  477 
variable (provided it does not occur in the assumptions). 
104  478 

479 
\item[\ttindexbold{forall_intr_list} $xs$ $thm$] 

480 
applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$. 

481 

482 
\item[\ttindexbold{forall_intr_frees} $thm$] 

483 
applies $({\Forall}I)$ repeatedly, generalizing over all the free variables 

484 
of the premise. 

326  485 
\end{ttdescription} 
104  486 

487 

326  488 
\subsection{Forall elimination rules} 
104  489 
\begin{ttbox} 
490 
forall_elim : Sign.cterm > thm > thm 

491 
forall_elim_list : Sign.cterm list > thm > thm 

492 
forall_elim_var : int > thm > thm 

493 
forall_elim_vars : int > thm > thm 

494 
\end{ttbox} 

495 

326  496 
\begin{ttdescription} 
104  497 
\item[\ttindexbold{forall_elim} $ct$ $thm$] 
498 
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion 

499 
$\phi[ct/x]$. The rule checks that $ct$ and $x$ have the same type. 

500 

501 
\item[\ttindexbold{forall_elim_list} $cts$ $thm$] 

502 
applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$. 

503 

504 
\item[\ttindexbold{forall_elim_var} $k$ $thm$] 

505 
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion 

506 
$\phi[\Var{x@k}/x]$. Thus, it replaces the outermost $\Forall$bound 

507 
variable by an unknown having subscript~$k$. 

508 

509 
\item[\ttindexbold{forall_elim_vars} $ks$ $thm$] 

510 
applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$. 

326  511 
\end{ttdescription} 
104  512 

326  513 
\subsection{Instantiation of unknowns} 
514 
\index{instantiation} 

104  515 
\begin{ttbox} 
286  516 
instantiate: (indexname*Sign.ctyp)list * 
517 
(Sign.cterm*Sign.cterm)list > thm > thm 

104  518 
\end{ttbox} 
326  519 
\begin{ttdescription} 
520 
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 

521 
simultaneously substitutes types for type unknowns (the 

104  522 
$tyinsts$) and terms for term unknowns (the $insts$). Instantiations are 
523 
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the 

524 
same type as $v$) or a type (of the same sort as~$v$). All the unknowns 

525 
must be distinct. The rule normalizes its conclusion. 

326  526 
\end{ttdescription} 
104  527 

528 

326  529 
\subsection{Freezing/thawing type unknowns} 
530 
\index{type unknowns!freezing/thawing of} 

104  531 
\begin{ttbox} 
532 
freezeT: thm > thm 

533 
varifyT: thm > thm 

534 
\end{ttbox} 

326  535 
\begin{ttdescription} 
104  536 
\item[\ttindexbold{freezeT} $thm$] 
537 
converts all the type unknowns in $thm$ to free type variables. 

538 

539 
\item[\ttindexbold{varifyT} $thm$] 

540 
converts all the free type variables in $thm$ to type unknowns. 

326  541 
\end{ttdescription} 
104  542 

543 

544 
\section{Derived rules for goaldirected proof} 

545 
Most of these rules have the sole purpose of implementing particular 

546 
tactics. There are few occasions for applying them directly to a theorem. 

547 

548 
\subsection{Proof by assumption} 

326  549 
\index{metaassumptions} 
104  550 
\begin{ttbox} 
551 
assumption : int > thm > thm Sequence.seq 

552 
eq_assumption : int > thm > thm 

553 
\end{ttbox} 

326  554 
\begin{ttdescription} 
104  555 
\item[\ttindexbold{assumption} {\it i} $thm$] 
556 
attempts to solve premise~$i$ of~$thm$ by assumption. 

557 

558 
\item[\ttindexbold{eq_assumption}] 

559 
is like {\tt assumption} but does not use unification. 

326  560 
\end{ttdescription} 
104  561 

562 

563 
\subsection{Resolution} 

326  564 
\index{resolution} 
104  565 
\begin{ttbox} 
566 
biresolution : bool > (bool*thm)list > int > thm 

567 
> thm Sequence.seq 

568 
\end{ttbox} 

326  569 
\begin{ttdescription} 
104  570 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  571 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  572 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
573 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

574 
is~{\tt true}, the $state$ is not instantiated. 

326  575 
\end{ttdescription} 
104  576 

577 

578 
\subsection{Composition: resolution without lifting} 

326  579 
\index{resolution!without lifting} 
104  580 
\begin{ttbox} 
581 
compose : thm * int * thm > thm list 

582 
COMP : thm * thm > thm 

583 
bicompose : bool > bool * thm * int > int > thm 

584 
> thm Sequence.seq 

585 
\end{ttbox} 

586 
In forward proof, a typical use of composition is to regard an assertion of 

587 
the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so 

588 
beware of clashes! 

326  589 
\begin{ttdescription} 
104  590 
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)] 
591 
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$ 

592 
of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots; 

593 
\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the 

594 
result list contains the theorem 

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

596 
\] 

597 

1119  598 
\item[$thm@1$ \ttindexbold{COMP} $thm@2$] 
104  599 
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if 
326  600 
unique; otherwise, it raises exception~\xdx{THM}\@. It is 
104  601 
analogous to {\tt RS}\@. 
602 

603 
For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and 

332  604 
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the 
104  605 
principle of contrapositives. Then the result would be the 
606 
derived rule $\neg(b=a)\Imp\neg(a=b)$. 

607 

608 
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$] 

609 
refines subgoal~$i$ of $state$ using $rule$, without lifting. The $rule$ 

610 
is taken to have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where 

326  611 
$\psi$ need not be atomic; thus $m$ determines the number of new 
104  612 
subgoals. If $flag$ is {\tt true} then it performs elimresolution  it 
613 
solves the first premise of~$rule$ by assumption and deletes that 

614 
assumption. If $match$ is~{\tt true}, the $state$ is not instantiated. 

326  615 
\end{ttdescription} 
104  616 

617 

618 
\subsection{Other metarules} 

619 
\begin{ttbox} 

620 
trivial : Sign.cterm > thm 

621 
lift_rule : (thm * int) > thm > thm 

622 
rename_params_rule : string list * int > thm > thm 

623 
rewrite_cterm : thm list > Sign.cterm > thm 

624 
flexflex_rule : thm > thm Sequence.seq 

625 
\end{ttbox} 

326  626 
\begin{ttdescription} 
104  627 
\item[\ttindexbold{trivial} $ct$] 
628 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

629 
This is the initial state for a goaldirected proof of~$\phi$. The rule 

630 
checks that $ct$ has type~$prop$. 

631 

632 
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting} 

633 
prepares $rule$ for resolution by lifting it over the parameters and 

634 
assumptions of subgoal~$i$ of~$state$. 

635 

636 
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$] 

637 
uses the $names$ to rename the parameters of premise~$i$ of $thm$. The 

638 
names must be distinct. If there are fewer names than parameters, then the 

639 
rule renames the innermost parameters and may modify the remaining ones to 

640 
ensure that all the parameters are distinct. 

641 
\index{parameters!renaming} 

642 

643 
\item[\ttindexbold{rewrite_cterm} $defs$ $ct$] 

644 
transforms $ct$ to $ct'$ by repeatedly applying $defs$ as rewrite rules; it 

645 
returns the conclusion~$ct\equiv ct'$. This underlies the metarewriting 

646 
tactics and rules. 

326  647 
\index{metarewriting!in terms} 
104  648 

649 
\item[\ttindexbold{flexflex_rule} $thm$] \index{flexflex constraints} 

650 
removes all flexflex pairs from $thm$ using the trivial unifier. 

326  651 
\end{ttdescription} 
1590  652 
\index{metarules)} 
653 

654 

655 
\section{Proof objects} 

656 
\index{proof objects(} Isabelle can record the full metalevel proof of each 

657 
theorem. The proof object contains all logical inferences in detail, while 

658 
omitting bookkeeping steps that have no logical meaning to an outside 

659 
observer. Rewriting steps are recorded in similar detail as the output of 

660 
simplifier tracing. The proof object can be inspected by a separate 

661 
proofchecker, or used to generate humanreadable proof digests. 

662 

663 
Full proof objects are large. They multiply storage requirements by about 

664 
seven; attempts to build large logics (such as {\sc zf} and {\sc hol}) may 

665 
fail. Isabelle normally builds minimal proof objects, which include only uses 

666 
of oracles. You can also request an intermediate level of detail, containing 

667 
uses of oracles, axioms and theorems. These smaller proof objects indicate a 

668 
theorem's dependencies. 

669 

670 
Isabelle provides proof objects for the sake of transparency. Their aim is to 

671 
increase your confidence in Isabelle. They let you inspect proofs constructed 

672 
by the classical reasoner or simplifier, and inform you of all uses of 

673 
oracles. Seldom will proof objects be given whole to an automatic 

674 
proofchecker: none has been written. It is up to you to examine and 

675 
interpret them sensibly. For example, when scrutinizing a theorem's 

676 
derivation for dependence upon some oracle or axiom, remember to scrutinize 

677 
all of its lemmas. Their proofs are included in the main derivation, through 

678 
the {\tt Theorem} constructor. 

679 

680 
Proof objects are expressed using a polymorphic type of variablebranching 

681 
trees. Proof objects (formally known as {\em derivations\/}) are trees 

682 
labelled by rules, where {\tt rule} is a complicated datatype declared in the 

683 
file {\tt Pure/thm.ML}. 

684 
\begin{ttbox} 

685 
datatype 'a mtree = Join of 'a * 'a mtree list; 

686 
datatype rule = \(\ldots\); 

687 
type deriv = rule mtree; 

688 
\end{ttbox} 

689 
% 

690 
Each theorem's derivation is stored as the {\tt der} field of its internal 

691 
record: 

692 
\begin{ttbox} 

693 
#der (rep_thm conjI); 

694 
{\out Join (Theorem ({ProtoPure, CPure, HOL},"conjI"),} 

695 
{\out [Join (MinProof,[])]) : deriv} 

696 
\end{ttbox} 

697 
This proof object identifies a labelled theorem, {\tt conjI}, whose underlying 

698 
proof has not been recorded; all we have is {\tt MinProof}. 

699 

700 
Nontrivial proof objects are unreadably large and complex. Isabelle provides 

701 
several functions to help you inspect them informally. These functions omit 

702 
the more obscure inferences and attempt to restructure the others into natural 

703 
formats, linear or treestructured. 

704 

705 
\begin{ttbox} 

706 
keep_derivs : deriv_kind ref 

707 
Deriv.size : deriv > int 

708 
Deriv.drop : 'a mtree * int > 'a mtree 

709 
Deriv.linear : deriv > deriv list 

710 
Deriv.linear : deriv > Deriv.orule mtree 

711 
\end{ttbox} 

712 

713 
\begin{ttdescription} 

714 
\item[\ttindexbold{keep_derivs} := MinDeriv $$ ThmDeriv $$ FullDeriv;] 

715 
specifies one of the three options for keeping derivations. They can be 

716 
minimal (oracles only), include theorems and axioms, or be full. 

717 

718 
\item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation, 

719 
excluding lemmas. 

720 

721 
\item[\ttindexbold{Deriv.drop} ($tree$,$n$)] returns the subtree $n$ levels 

722 
down, always following the first child. It is good for stripping off 

723 
outer level inferences that are used to put a theorem into standard form. 

724 

725 
\item[\ttindexbold{Deriv.linear} $der$] converts a derivation into a linear 

726 
format, replacing the deep nesting by a list of rules. Intuitively, this 

727 
reveals the singlestep Isabelle proof that is constructed internally by 

728 
tactics. 

729 

730 
\item[\ttindexbold{Deriv.tree} $der$] converts a derivation into an 

731 
objectlevel proof tree. A resolution by an objectrule is converted to a 

732 
tree node labelled by that rule. Complications arise if the objectrule is 

733 
itself derived in some way. Nested resolutions are unravelled, but other 

734 
operations on rules (such as rewriting) are left asis. 

735 
\end{ttdescription} 

736 

737 
\index{proof objects)} 

104  738 
\index{theorems)} 