author  paulson 
Wed, 07 Oct 1998 10:31:30 +0200  
changeset 5619  76a8c72e3fd4 
parent 5371  e27558a68b8d 
child 5777  5c0aa825c18e 
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 

4383  135 
\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate} 
326  136 
\index{instantiation} 
286  137 
\begin{ttbox} 
4383  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}] 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4383
diff
changeset

161 
is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads 
326  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 
4607  189 
rotate_prems : int > thm > thm 
104  190 
\end{ttbox} 
326  191 
\begin{ttdescription} 
3108  192 
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form 
193 
of objectrules. It discharges all metaassumptions, replaces free 

194 
variables by schematic variables, renames schematic variables to 

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

196 
removes dangling sort hypotheses. 

104  197 

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

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

200 
clashes. 

201 

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

203 
\index{rules!converting destruction to elimination} 

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

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

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

207 

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

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

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

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

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

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

214 
whatever is left. 

4607  215 

216 
\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to 

217 
the left by~$k$ positions. It requires $0\leq k\leq n$, where $n$ is the 

218 
number of premises; the rotation has no effect if $k$ is at either extreme. 

219 
Used with \texttt{eresolve_tac}\index{*eresolve_tac!on other than first 

220 
premise}, it gives the effect of applying the tactic to some other premise 

221 
of $thm$ than the first. 

326  222 
\end{ttdescription} 
104  223 

224 

225 
\subsection{Taking a theorem apart} 

326  226 
\index{theorems!taking apart} 
104  227 
\index{flexflex constraints} 
228 
\begin{ttbox} 

4317  229 
cprop_of : thm > cterm 
104  230 
concl_of : thm > term 
231 
prems_of : thm > term list 

4317  232 
cprems_of : thm > cterm list 
104  233 
nprems_of : thm > int 
4383  234 
tpairs_of : thm > (term*term) list 
4317  235 
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

236 
theory_of_thm : thm > theory 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4383
diff
changeset

237 
dest_state : thm * int > (term*term) list * term list * term * term 
4317  238 
rep_thm : thm > {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, 
239 
shyps: sort list, hyps: term list, prop: term\ttrbrace 

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

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

104  242 
\end{ttbox} 
326  243 
\begin{ttdescription} 
4317  244 
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as 
245 
a certified term. 

246 

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

248 
a term. 

249 

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

251 
list of terms. 

252 

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

254 
a list of certified terms. 

104  255 

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

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

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

262 

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

264 
associated with $thm$. 

265 

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

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

268 
database of loaded theories. 

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

269 

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

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

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

274 

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

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

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

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

280 
is discussed below. 

281 

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

283 
the hypotheses and statement as certified terms. 

284 

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

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

286 

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

287 

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

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

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

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

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

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

293 

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

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

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

296 
causes sort hypotheses to be deleted, printing a warning. 
326  297 
\end{ttdescription} 
104  298 

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

299 
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

300 
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

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

302 
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

303 
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit 
4317  304 
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

305 

3108  306 
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

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

310 
only if under an additional nonemptiness assumption. 

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

311 

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

312 
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

313 
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

314 
{\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

315 
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

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

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

318 

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

319 
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

320 
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

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

322 
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

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

324 

104  325 

326 
\subsection{Tracing flags for unification} 

326  327 
\index{tracing!of unification} 
104  328 
\begin{ttbox} 
329 
Unify.trace_simp : bool ref \hfill{\bf initially false} 

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

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

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

333 
\end{ttbox} 

334 
Tracing the search may be useful when higherorder unification behaves 

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

336 
though. 

326  337 
\begin{ttdescription} 
4317  338 
\item[set Unify.trace_simp;] 
104  339 
causes tracing of the simplification phase. 
340 

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

344 

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

348 
information is almost never printed. 

349 

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

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

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

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

355 
\texttt{Unification bound exceeded}. 

326  356 
\end{ttdescription} 
104  357 

358 

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

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

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

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

366 
incompatible signatures and similar errors. 

104  367 

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

373 
assertions of the form 

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

3108  375 
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. This can be 
376 
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

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

104  380 

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

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

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

384 
incompatible. 

385 

326  386 
\index{metaimplication} 
332  387 
The {\bf implication} rules are $({\Imp}I)$ 
104  388 
and $({\Imp}E)$: 
389 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

391 

326  392 
\index{metaequality} 
104  393 
Equality of truth values means logical equivalence: 
3524  394 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi & 
395 
\psi\Imp\phi} 

104  396 
\qquad 
397 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

398 

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

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

403 

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

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

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

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

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

411 

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

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

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

417 

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

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

424 

326  425 
\subsection{Assumption rule} 
426 
\index{metaassumptions} 

104  427 
\begin{ttbox} 
3108  428 
assume: cterm > thm 
104  429 
\end{ttbox} 
326  430 
\begin{ttdescription} 
104  431 
\item[\ttindexbold{assume} $ct$] 
332  432 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  433 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  434 
are not allowed in assumptions. 
326  435 
\end{ttdescription} 
104  436 

326  437 
\subsection{Implication rules} 
438 
\index{metaimplication} 

104  439 
\begin{ttbox} 
3108  440 
implies_intr : cterm > thm > thm 
441 
implies_intr_list : cterm list > thm > thm 

104  442 
implies_intr_hyps : thm > thm 
443 
implies_elim : thm > thm > thm 

444 
implies_elim_list : thm > thm list > thm 

445 
\end{ttbox} 

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

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

451 
type $prop$. 

104  452 

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

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

455 

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

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

104  459 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
460 

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

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

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

464 

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

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

151  467 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  468 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  469 
\end{ttdescription} 
104  470 

326  471 
\subsection{Logical equivalence rules} 
472 
\index{metaequality} 

104  473 
\begin{ttbox} 
326  474 
equal_intr : thm > thm > thm 
475 
equal_elim : thm > thm > thm 

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

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

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

104  483 

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

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

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

326  487 
\end{ttdescription} 
104  488 

489 

490 
\subsection{Equality rules} 

326  491 
\index{metaequality} 
104  492 
\begin{ttbox} 
3108  493 
reflexive : cterm > thm 
104  494 
symmetric : thm > thm 
495 
transitive : thm > thm > thm 

496 
\end{ttbox} 

326  497 
\begin{ttdescription} 
104  498 
\item[\ttindexbold{reflexive} $ct$] 
151  499 
makes the theorem \(ct\equiv ct\). 
104  500 

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

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

503 

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

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

326  506 
\end{ttdescription} 
104  507 

508 

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

326  510 
\index{lambda calc@$\lambda$calculus} 
104  511 
\begin{ttbox} 
3108  512 
beta_conversion : cterm > thm 
104  513 
extensional : thm > thm 
3108  514 
abstract_rule : string > cterm > thm > thm 
104  515 
combination : thm > thm > thm 
516 
\end{ttbox} 

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

519 
\begin{ttdescription} 

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

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

523 

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

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

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

332  527 
variable (provided it does not occur in the assumptions); it must not occur 
104  528 
in $f$ or~$g$. 
529 

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

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

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

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

332  534 
variable (provided it does not occur in the assumptions). In the 
104  535 
conclusion, the bound variable is named~$v$. 
536 

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

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

539 
g(b)$. 

326  540 
\end{ttdescription} 
104  541 

542 

326  543 
\subsection{Forall introduction rules} 
544 
\index{metaquantifiers} 

104  545 
\begin{ttbox} 
3108  546 
forall_intr : cterm > thm > thm 
547 
forall_intr_list : cterm list > thm > thm 

548 
forall_intr_frees : thm > thm 

104  549 
\end{ttbox} 
550 

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

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

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

332  556 
variable (provided it does not occur in the assumptions). 
104  557 

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

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

560 

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

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

563 
of the premise. 

326  564 
\end{ttdescription} 
104  565 

566 

326  567 
\subsection{Forall elimination rules} 
104  568 
\begin{ttbox} 
3108  569 
forall_elim : cterm > thm > thm 
570 
forall_elim_list : cterm list > thm > thm 

571 
forall_elim_var : int > thm > thm 

572 
forall_elim_vars : int > thm > thm 

104  573 
\end{ttbox} 
574 

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

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

579 

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

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

582 

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

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

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

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

587 

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

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

326  590 
\end{ttdescription} 
104  591 

326  592 
\subsection{Instantiation of unknowns} 
593 
\index{instantiation} 

104  594 
\begin{ttbox} 
3135  595 
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list > thm > thm 
104  596 
\end{ttbox} 
326  597 
\begin{ttdescription} 
598 
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 

599 
simultaneously substitutes types for type unknowns (the 

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

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

603 
must be distinct. The rule normalizes its conclusion. 

4376  604 

605 
Note that \ttindex{instantiate'} (see \S\ref{sec:instantiate}) 

606 
provides a more convenient interface to this rule. 

326  607 
\end{ttdescription} 
104  608 

609 

326  610 
\subsection{Freezing/thawing type unknowns} 
611 
\index{type unknowns!freezing/thawing of} 

104  612 
\begin{ttbox} 
613 
freezeT: thm > thm 

614 
varifyT: thm > thm 

615 
\end{ttbox} 

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

619 

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

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

326  622 
\end{ttdescription} 
104  623 

624 

625 
\section{Derived rules for goaldirected proof} 

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

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

628 

629 
\subsection{Proof by assumption} 

326  630 
\index{metaassumptions} 
104  631 
\begin{ttbox} 
4276  632 
assumption : int > thm > thm Seq.seq 
104  633 
eq_assumption : int > thm > thm 
634 
\end{ttbox} 

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

638 

639 
\item[\ttindexbold{eq_assumption}] 

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

326  641 
\end{ttdescription} 
104  642 

643 

644 
\subsection{Resolution} 

326  645 
\index{resolution} 
104  646 
\begin{ttbox} 
647 
biresolution : bool > (bool*thm)list > int > thm 

4276  648 
> thm Seq.seq 
104  649 
\end{ttbox} 
326  650 
\begin{ttdescription} 
104  651 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  652 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  653 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
654 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

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

326  656 
\end{ttdescription} 
104  657 

658 

659 
\subsection{Composition: resolution without lifting} 

326  660 
\index{resolution!without lifting} 
104  661 
\begin{ttbox} 
662 
compose : thm * int * thm > thm list 

663 
COMP : thm * thm > thm 

664 
bicompose : bool > bool * thm * int > int > thm 

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

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

669 
beware of clashes! 

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

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

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

675 
result list contains the theorem 

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

677 
\] 

678 

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

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

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

688 

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

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

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

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

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

326  696 
\end{ttdescription} 
104  697 

698 

699 
\subsection{Other metarules} 

700 
\begin{ttbox} 

3108  701 
trivial : cterm > thm 
104  702 
lift_rule : (thm * int) > thm > thm 
703 
rename_params_rule : string list * int > thm > thm 

4276  704 
flexflex_rule : thm > thm Seq.seq 
104  705 
\end{ttbox} 
326  706 
\begin{ttdescription} 
104  707 
\item[\ttindexbold{trivial} $ct$] 
708 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

711 

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

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

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

715 

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

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

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

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

720 
ensure that all the parameters are distinct. 

721 
\index{parameters!renaming} 

722 

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

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

326  725 
\end{ttdescription} 
1590  726 
\index{metarules)} 
727 

728 

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

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

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

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

4317  735 
proofchecker, for example. 
1590  736 

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

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

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

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

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

742 
theorem's dependencies. 

743 

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

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

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

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

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

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

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

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

752 
the {\tt Theorem} constructor. 

753 

754 
Proof objects are expressed using a polymorphic type of variablebranching 

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

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

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

758 
\begin{ttbox} 

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

760 
datatype rule = \(\ldots\); 

761 
type deriv = rule mtree; 

762 
\end{ttbox} 

763 
% 

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

765 
record: 

766 
\begin{ttbox} 

767 
#der (rep_thm conjI); 

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

772 
have is {\tt MinProof}. 

1590  773 

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

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

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

777 
formats, linear or treestructured. 

778 

779 
\begin{ttbox} 

780 
keep_derivs : deriv_kind ref 

781 
Deriv.size : deriv > int 

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

783 
Deriv.linear : deriv > deriv list 

1876  784 
Deriv.tree : deriv > Deriv.orule mtree 
1590  785 
\end{ttbox} 
786 

787 
\begin{ttdescription} 

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

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4383
diff
changeset

789 
specifies one of the options for keeping derivations. They can be 
1590  790 
minimal (oracles only), include theorems and axioms, or be full. 
791 

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

793 
excluding lemmas. 

794 

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

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

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

798 

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

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

801 
reveals the singlestep Isabelle proof that is constructed internally by 

802 
tactics. 

803 

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

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

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

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

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

809 
\end{ttdescription} 

810 

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

811 
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

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

813 
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

814 
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

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

816 

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

817 

1590  818 
\index{proof objects)} 
104  819 
\index{theorems)} 
5371  820 

821 

822 
%%% Local Variables: 

823 
%%% mode: latex 

824 
%%% TeXmaster: "ref" 

825 
%%% End: 