author  wenzelm 
Thu, 27 Nov 1997 19:39:02 +0100  
changeset 4317  7264fa2ff2ec 
parent 4276  a770eae2cdb0 
child 4376  407f786d3059 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Theorems and Forward Proof} 

3 
\index{theorems(} 

326  4 

3108  5 
Theorems, which represent the axioms, theorems and rules of 
6 
objectlogics, have type \mltydx{thm}. This chapter begins by 

7 
describing operations that print theorems and that join them in 

8 
forward proof. Most theorem operations are intended for advanced 

9 
applications, such as programming new proof procedures. Many of these 

10 
operations refer to signatures, certified terms and certified types, 

11 
which have the \ML{} types {\tt Sign.sg}, {\tt cterm} and {\tt ctyp} 

12 
and are discussed in Chapter~\ref{theories}. Beginning users should 

13 
ignore such complexities  and skip all but the first section of 

14 
this chapter. 

104  15 

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

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

20 
allI RS mp handle e => print_exn e; 

21 
{\out Exception THM raised:} 

22 
{\out RSN: no unifiers  premise 1} 

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

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

25 
{\out} 

26 
{\out uncaught exception THM} 

27 
\end{ttbox} 

28 

29 

30 
\section{Basic operations on theorems} 

31 
\subsection{Prettyprinting a theorem} 

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

4276  36 
prthq : thm Seq.seq > thm Seq.seq 
326  37 
print_thm : thm > unit 
38 
print_goals : int > thm > unit 

39 
string_of_thm : thm > string 

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

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

44 

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

46 
are convenient for imperative programming. 

47 

48 
\begin{ttdescription} 

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

51 

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

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

54 

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

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

57 
the output of a tactic. 

58 

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

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

61 

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

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

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

65 
to display proof states. 

66 

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

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

326  69 
\end{ttdescription} 
104  70 

71 

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

74 
\index{resolution}\index{forward proof} 

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

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

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

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

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

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

86 
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 

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

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

104  92 

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

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

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

96 

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

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

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

102 
for expressing proof trees. 

103 

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

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

104  108 

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

104  111 

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

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

114 
It too is useful for expressing proof trees. 

326  115 
\end{ttdescription} 
104  116 

117 

118 
\subsection{Expanding definitions in theorems} 

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

122 
rewrite_goals_rule : thm list > thm > thm 

123 
\end{ttbox} 

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

127 

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

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

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

131 
serves little purpose in forward proof. 

326  132 
\end{ttdescription} 
104  133 

134 

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

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

140 
cterm_instantiate : (cterm * cterm) list > thm > thm 

141 
instantiate' : ctyp option list > cterm option list > thm > thm 

104  142 
\end{ttbox} 
143 
These metarules instantiate type and term unknowns in a theorem. They are 

144 
occasionally useful. They can prevent difficulties with higherorder 

145 
unification, and define specialized versions of rules. 

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

149 
thm}. The processing of instantiations is described 

326  150 
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}. 
104  151 

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

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

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

326  155 
associated with the proof state. 
156 

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

158 
incorrectly. 

104  159 

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

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

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

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

165 
sign_of} to get a theory's signature. 

104  166 

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

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

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

4317  170 

171 
\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}] 

172 
instantiates {\it thm} according to the positional arguments {\it 

173 
ctyps} and {\it cterms}. Counting from left to right, schematic 

174 
variables $?x$ are either replaced by $t$ for any argument 

175 
\texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or 

176 
if the end of the argument list is encountered. Types are 

177 
instantiated before terms. 

178 

326  179 
\end{ttdescription} 
104  180 

181 

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

182 
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules} 
326  183 
\index{theorems!standardizing} 
104  184 
\begin{ttbox} 
332  185 
standard : thm > thm 
186 
zero_var_indexes : thm > thm 

187 
make_elim : thm > thm 

104  188 
rule_by_tactic : tactic > thm > thm 
189 
\end{ttbox} 

326  190 
\begin{ttdescription} 
3108  191 
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form 
192 
of objectrules. It discharges all metaassumptions, replaces free 

193 
variables by schematic variables, renames schematic variables to 

194 
have subscript zero, also strips outer (meta) quantifiers and 

195 
removes dangling sort hypotheses. 

104  196 

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

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

199 
clashes. 

200 

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

202 
\index{rules!converting destruction to elimination} 

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

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

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

206 

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

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

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

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

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

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

213 
whatever is left. 

326  214 
\end{ttdescription} 
104  215 

216 

217 
\subsection{Taking a theorem apart} 

326  218 
\index{theorems!taking apart} 
104  219 
\index{flexflex constraints} 
220 
\begin{ttbox} 

4317  221 
cprop_of : thm > cterm 
104  222 
concl_of : thm > term 
223 
prems_of : thm > term list 

4317  224 
cprems_of : thm > cterm list 
104  225 
nprems_of : thm > int 
4317  226 
tpairs_of : thm > (term * term) list 
227 
sign_of_thm : thm > Sign.sg 

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

228 
theory_of_thm : thm > theory 
4317  229 
dest_state : thm * int > (term * term) list * term list * term * term 
230 
rep_thm : thm > {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, 

231 
shyps: sort list, hyps: term list, prop: term\ttrbrace 

232 
crep_thm : thm > {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, 

233 
shyps: sort list, hyps: cterm list, prop: cterm\ttrbrace 

104  234 
\end{ttbox} 
326  235 
\begin{ttdescription} 
4317  236 
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as 
237 
a certified term. 

238 

239 
\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as 

240 
a term. 

241 

242 
\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a 

243 
list of terms. 

244 

245 
\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as 

246 
a list of certified terms. 

104  247 

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

286  249 
returns the number of premises in $thm$, and is equivalent to {\tt 
4317  250 
length~(prems_of~$thm$)}. 
104  251 

4317  252 
\item[\ttindexbold{tpairs_of} $thm$] returns the flexflex constraints 
253 
of $thm$. 

254 

255 
\item[\ttindexbold{sign_of_thm} $thm$] returns the signature 

256 
associated with $thm$. 

257 

258 
\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated 

259 
with $thm$. Note that this does a lookup in Isabelle's global 

260 
database of loaded theories. 

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

261 

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

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

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

266 

4317  267 
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record 
268 
containing the statement of~$thm$ ({\tt prop}), its list of 

269 
metaassumptions ({\tt hyps}), its derivation ({\tt der}), a bound 

270 
on the maximum subscript of its unknowns ({\tt maxidx}), and a 

271 
reference to its signature ({\tt sign_ref}). The {\tt shyps} field 

272 
is discussed below. 

273 

274 
\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns 

275 
the hypotheses and statement as certified terms. 

276 

2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

277 
\end{ttdescription} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

278 

6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

279 

6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

280 
\subsection{*Sort hypotheses} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

281 
\index{sort hypotheses} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

282 
\begin{ttbox} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

283 
force_strip_shyps : bool ref \hfill{\bf initially true} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

284 
\end{ttbox} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

285 

6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

286 
\begin{ttdescription} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

287 
\item[\ttindexbold{force_strip_shyps}] 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

288 
causes sort hypotheses to be deleted, printing a warning. 
326  289 
\end{ttdescription} 
104  290 

2044
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

291 
Isabelle's type variables are decorated with sorts, constraining them to 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

292 
certain ranges of types. This has little impact when sorts only serve for 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

293 
syntactic classification of types  for example, FOL distinguishes between 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

294 
terms and other types. But when type classes are introduced through axioms, 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

295 
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit 
4317  296 
a type belonging to it because certain sets of axioms are unsatisfiable. 
2044
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

297 

3108  298 
If a theorem contains a type variable that is constrained by an empty 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3135
diff
changeset

299 
sort, then that theorem has no instances. It is basically an instance 
3108  300 
of {\em ex falso quodlibet}. But what if it is used to prove another 
301 
theorem that no longer involves that sort? The latter theorem holds 

302 
only if under an additional nonemptiness assumption. 

2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

303 

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

304 
Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt 
2044
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

305 
shyps} field is a list of sorts occurring in type variables in the current 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

306 
{\tt prop} and {\tt hyps} fields. It may also includes sorts used in the 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

307 
theorem's proof that no longer appear in the {\tt prop} or {\tt hyps} 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3135
diff
changeset

308 
fields  socalled {\em dangling\/} sort constraints. These are the 
2044
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

309 
critical ones, asserting nonemptiness of the corresponding sorts. 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

310 

e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

311 
Isabelle tries to remove extraneous sorts from the {\tt shyps} field whenever 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

312 
nonemptiness can be established by looking at the theorem's signature: from 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

313 
the {\tt arities} information, etc. Because its current implementation is 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

314 
highly incomplete, the flag shown above is available. Setting it to true (the 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

315 
default) allows existing proofs to run. 
2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

316 

104  317 

318 
\subsection{Tracing flags for unification} 

326  319 
\index{tracing!of unification} 
104  320 
\begin{ttbox} 
321 
Unify.trace_simp : bool ref \hfill{\bf initially false} 

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

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

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

325 
\end{ttbox} 

326 
Tracing the search may be useful when higherorder unification behaves 

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

328 
though. 

326  329 
\begin{ttdescription} 
4317  330 
\item[set Unify.trace_simp;] 
104  331 
causes tracing of the simplification phase. 
332 

4317  333 
\item[set Unify.trace_types;] 
104  334 
generates warnings of incompleteness, when unification is not considering 
335 
all possible instantiations of type unknowns. 

336 

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

340 
information is almost never printed. 

341 

4317  342 
\item[Unify.search_bound := $n$;] causes unification to limit its 
343 
search to depth~$n$. Because of this bound, higherorder 

344 
unification cannot return an infinite sequence, though it can return 

345 
a very long one. The search rarely approaches the default value 

346 
of~20. If the search is cut off, unification prints a warning 

347 
\texttt{Unification bound exceeded}. 

326  348 
\end{ttdescription} 
104  349 

350 

4317  351 
\section{*Primitive metalevel inference rules} 
104  352 
\index{metarules(} 
4317  353 
These implement the metalogic in the style of the {\sc lcf} system, 
354 
as functions from theorems to theorems. They are, rarely, useful for 

355 
deriving results in the pure theory. Mainly, they are included for 

356 
completeness, and most users should not bother with them. The 

357 
metarules raise exception \xdx{THM} to signal malformed premises, 

358 
incompatible signatures and similar errors. 

104  359 

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

365 
assertions of the form 

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

3108  367 
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. This can be 
368 
also read as a single conclusion sequent $\phi@1,\ldots,\phi@n \vdash 

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

369 
\phi$. Do not confuse metalevel assumptions with the objectlevel 
3108  370 
assumptions in a subgoal, which are represented in the metalogic 
371 
using~$\Imp$. 

104  372 

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

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

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

376 
incompatible. 

377 

326  378 
\index{metaimplication} 
332  379 
The {\bf implication} rules are $({\Imp}I)$ 
104  380 
and $({\Imp}E)$: 
381 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

383 

326  384 
\index{metaequality} 
104  385 
Equality of truth values means logical equivalence: 
3524  386 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi & 
387 
\psi\Imp\phi} 

104  388 
\qquad 
389 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

390 

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

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

395 

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

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

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

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

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

403 

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

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

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

409 

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

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

416 

326  417 
\subsection{Assumption rule} 
418 
\index{metaassumptions} 

104  419 
\begin{ttbox} 
3108  420 
assume: cterm > thm 
104  421 
\end{ttbox} 
326  422 
\begin{ttdescription} 
104  423 
\item[\ttindexbold{assume} $ct$] 
332  424 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  425 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  426 
are not allowed in assumptions. 
326  427 
\end{ttdescription} 
104  428 

326  429 
\subsection{Implication rules} 
430 
\index{metaimplication} 

104  431 
\begin{ttbox} 
3108  432 
implies_intr : cterm > thm > thm 
433 
implies_intr_list : cterm list > thm > thm 

104  434 
implies_intr_hyps : thm > thm 
435 
implies_elim : thm > thm > thm 

436 
implies_elim_list : thm > thm list > thm 

437 
\end{ttbox} 

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

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

443 
type $prop$. 

104  444 

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

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

447 

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

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

104  451 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
452 

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

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

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

456 

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

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

151  459 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  460 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  461 
\end{ttdescription} 
104  462 

326  463 
\subsection{Logical equivalence rules} 
464 
\index{metaequality} 

104  465 
\begin{ttbox} 
326  466 
equal_intr : thm > thm > thm 
467 
equal_elim : thm > thm > thm 

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

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

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

104  475 

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

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

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

326  479 
\end{ttdescription} 
104  480 

481 

482 
\subsection{Equality rules} 

326  483 
\index{metaequality} 
104  484 
\begin{ttbox} 
3108  485 
reflexive : cterm > thm 
104  486 
symmetric : thm > thm 
487 
transitive : thm > thm > thm 

488 
\end{ttbox} 

326  489 
\begin{ttdescription} 
104  490 
\item[\ttindexbold{reflexive} $ct$] 
151  491 
makes the theorem \(ct\equiv ct\). 
104  492 

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

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

495 

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

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

326  498 
\end{ttdescription} 
104  499 

500 

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

326  502 
\index{lambda calc@$\lambda$calculus} 
104  503 
\begin{ttbox} 
3108  504 
beta_conversion : cterm > thm 
104  505 
extensional : thm > thm 
3108  506 
abstract_rule : string > cterm > thm > thm 
104  507 
combination : thm > thm > thm 
508 
\end{ttbox} 

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

511 
\begin{ttdescription} 

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

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

515 

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

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

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

332  519 
variable (provided it does not occur in the assumptions); it must not occur 
104  520 
in $f$ or~$g$. 
521 

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

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

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

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

332  526 
variable (provided it does not occur in the assumptions). In the 
104  527 
conclusion, the bound variable is named~$v$. 
528 

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

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

531 
g(b)$. 

326  532 
\end{ttdescription} 
104  533 

534 

326  535 
\subsection{Forall introduction rules} 
536 
\index{metaquantifiers} 

104  537 
\begin{ttbox} 
3108  538 
forall_intr : cterm > thm > thm 
539 
forall_intr_list : cterm list > thm > thm 

540 
forall_intr_frees : thm > thm 

104  541 
\end{ttbox} 
542 

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

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

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

332  548 
variable (provided it does not occur in the assumptions). 
104  549 

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

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

552 

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

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

555 
of the premise. 

326  556 
\end{ttdescription} 
104  557 

558 

326  559 
\subsection{Forall elimination rules} 
104  560 
\begin{ttbox} 
3108  561 
forall_elim : cterm > thm > thm 
562 
forall_elim_list : cterm list > thm > thm 

563 
forall_elim_var : int > thm > thm 

564 
forall_elim_vars : int > thm > thm 

104  565 
\end{ttbox} 
566 

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

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

571 

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

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

574 

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

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

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

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

579 

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

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

326  582 
\end{ttdescription} 
104  583 

326  584 
\subsection{Instantiation of unknowns} 
585 
\index{instantiation} 

104  586 
\begin{ttbox} 
3135  587 
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list > thm > thm 
104  588 
\end{ttbox} 
326  589 
\begin{ttdescription} 
590 
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 

591 
simultaneously substitutes types for type unknowns (the 

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

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

595 
must be distinct. The rule normalizes its conclusion. 

326  596 
\end{ttdescription} 
104  597 

598 

326  599 
\subsection{Freezing/thawing type unknowns} 
600 
\index{type unknowns!freezing/thawing of} 

104  601 
\begin{ttbox} 
602 
freezeT: thm > thm 

603 
varifyT: thm > thm 

604 
\end{ttbox} 

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

608 

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

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

326  611 
\end{ttdescription} 
104  612 

613 

614 
\section{Derived rules for goaldirected proof} 

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

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

617 

618 
\subsection{Proof by assumption} 

326  619 
\index{metaassumptions} 
104  620 
\begin{ttbox} 
4276  621 
assumption : int > thm > thm Seq.seq 
104  622 
eq_assumption : int > thm > thm 
623 
\end{ttbox} 

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

627 

628 
\item[\ttindexbold{eq_assumption}] 

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

326  630 
\end{ttdescription} 
104  631 

632 

633 
\subsection{Resolution} 

326  634 
\index{resolution} 
104  635 
\begin{ttbox} 
636 
biresolution : bool > (bool*thm)list > int > thm 

4276  637 
> thm Seq.seq 
104  638 
\end{ttbox} 
326  639 
\begin{ttdescription} 
104  640 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  641 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  642 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
643 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

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

326  645 
\end{ttdescription} 
104  646 

647 

648 
\subsection{Composition: resolution without lifting} 

326  649 
\index{resolution!without lifting} 
104  650 
\begin{ttbox} 
651 
compose : thm * int * thm > thm list 

652 
COMP : thm * thm > thm 

653 
bicompose : bool > bool * thm * int > int > thm 

4276  654 
> thm Seq.seq 
104  655 
\end{ttbox} 
656 
In forward proof, a typical use of composition is to regard an assertion of 

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

658 
beware of clashes! 

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

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

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

664 
result list contains the theorem 

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

666 
\] 

667 

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

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

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

677 

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

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

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

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

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

326  685 
\end{ttdescription} 
104  686 

687 

688 
\subsection{Other metarules} 

689 
\begin{ttbox} 

3108  690 
trivial : cterm > thm 
104  691 
lift_rule : (thm * int) > thm > thm 
692 
rename_params_rule : string list * int > thm > thm 

4276  693 
flexflex_rule : thm > thm Seq.seq 
104  694 
\end{ttbox} 
326  695 
\begin{ttdescription} 
104  696 
\item[\ttindexbold{trivial} $ct$] 
697 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

700 

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

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

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

704 

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

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

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

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

709 
ensure that all the parameters are distinct. 

710 
\index{parameters!renaming} 

711 

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

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

326  714 
\end{ttdescription} 
1590  715 
\index{metarules)} 
716 

717 

1846  718 
\section{Proof objects}\label{sec:proofObjects} 
1590  719 
\index{proof objects(} Isabelle can record the full metalevel proof of each 
720 
theorem. The proof object contains all logical inferences in detail, while 

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

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

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

4317  724 
proofchecker, for example. 
1590  725 

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

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

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

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

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

731 
theorem's dependencies. 

732 

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

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

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

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

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

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

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

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

741 
the {\tt Theorem} constructor. 

742 

743 
Proof objects are expressed using a polymorphic type of variablebranching 

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

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

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

747 
\begin{ttbox} 

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

749 
datatype rule = \(\ldots\); 

750 
type deriv = rule mtree; 

751 
\end{ttbox} 

752 
% 

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

754 
record: 

755 
\begin{ttbox} 

756 
#der (rep_thm conjI); 

4317  757 
{\out Join (Theorem "HOL.conjI", [Join (MinProof,[])]) : deriv} 
1590  758 
\end{ttbox} 
4317  759 
This proof object identifies a labelled theorem, {\tt conjI} of theory 
760 
\texttt{HOL}, whose underlying proof has not been recorded; all we 

761 
have is {\tt MinProof}. 

1590  762 

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

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

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

766 
formats, linear or treestructured. 

767 

768 
\begin{ttbox} 

769 
keep_derivs : deriv_kind ref 

770 
Deriv.size : deriv > int 

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

772 
Deriv.linear : deriv > deriv list 

1876  773 
Deriv.tree : deriv > Deriv.orule mtree 
1590  774 
\end{ttbox} 
775 

776 
\begin{ttdescription} 

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

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

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

780 

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

782 
excluding lemmas. 

783 

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

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

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

787 

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

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

790 
reveals the singlestep Isabelle proof that is constructed internally by 

791 
tactics. 

792 

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

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

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

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

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

798 
\end{ttdescription} 

799 

2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

800 
Functions {\tt Deriv.linear} and {\tt Deriv.tree} omit the proof of any named 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

801 
theorems (constructor {\tt Theorem}) they encounter in a derivation. Applying 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

802 
them directly to the derivation of a named theorem is therefore pointless. 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

803 
Use {\tt Deriv.drop} with argument~1 to skip over the initial {\tt Theorem} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

804 
constructor. 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

805 

6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

806 

1590  807 
\index{proof objects)} 
104  808 
\index{theorems)} 