author  wenzelm 
Fri, 16 Jul 1999 22:24:42 +0200  
changeset 7024  44bd3c094fd6 
parent 6924  7e166f8d412e 
child 7644  054ecaf3ca22 
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 

5777  288 
\subsection{*Sort hypotheses} \label{sec:sorthyps} 
2040
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 

5777  386 
\medskip 
387 

388 
The following presentation of primitive rules ignores sort 

389 
hypotheses\index{sort hypotheses} (see also \S\ref{sec:sorthyps}). These are 

390 
handled transparently by the logic implementation. 

391 

392 
\bigskip 

393 

326  394 
\index{metaimplication} 
332  395 
The {\bf implication} rules are $({\Imp}I)$ 
104  396 
and $({\Imp}E)$: 
397 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

399 

326  400 
\index{metaequality} 
104  401 
Equality of truth values means logical equivalence: 
3524  402 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi & 
403 
\psi\Imp\phi} 

104  404 
\qquad 
405 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

406 

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

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

411 

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

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

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

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

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

419 

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

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

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

425 

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

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

432 

326  433 
\subsection{Assumption rule} 
434 
\index{metaassumptions} 

104  435 
\begin{ttbox} 
3108  436 
assume: cterm > thm 
104  437 
\end{ttbox} 
326  438 
\begin{ttdescription} 
104  439 
\item[\ttindexbold{assume} $ct$] 
332  440 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  441 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  442 
are not allowed in assumptions. 
326  443 
\end{ttdescription} 
104  444 

326  445 
\subsection{Implication rules} 
446 
\index{metaimplication} 

104  447 
\begin{ttbox} 
3108  448 
implies_intr : cterm > thm > thm 
449 
implies_intr_list : cterm list > thm > thm 

104  450 
implies_intr_hyps : thm > thm 
451 
implies_elim : thm > thm > thm 

452 
implies_elim_list : thm > thm list > thm 

453 
\end{ttbox} 

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

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

459 
type $prop$. 

104  460 

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

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

463 

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

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

104  467 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
468 

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

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

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

472 

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

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

151  475 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  476 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  477 
\end{ttdescription} 
104  478 

326  479 
\subsection{Logical equivalence rules} 
480 
\index{metaequality} 

104  481 
\begin{ttbox} 
326  482 
equal_intr : thm > thm > thm 
483 
equal_elim : thm > thm > thm 

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

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

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

104  491 

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

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

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

326  495 
\end{ttdescription} 
104  496 

497 

498 
\subsection{Equality rules} 

326  499 
\index{metaequality} 
104  500 
\begin{ttbox} 
3108  501 
reflexive : cterm > thm 
104  502 
symmetric : thm > thm 
503 
transitive : thm > thm > thm 

504 
\end{ttbox} 

326  505 
\begin{ttdescription} 
104  506 
\item[\ttindexbold{reflexive} $ct$] 
151  507 
makes the theorem \(ct\equiv ct\). 
104  508 

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

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

511 

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

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

326  514 
\end{ttdescription} 
104  515 

516 

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

326  518 
\index{lambda calc@$\lambda$calculus} 
104  519 
\begin{ttbox} 
3108  520 
beta_conversion : cterm > thm 
104  521 
extensional : thm > thm 
3108  522 
abstract_rule : string > cterm > thm > thm 
104  523 
combination : thm > thm > thm 
524 
\end{ttbox} 

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

527 
\begin{ttdescription} 

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

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

531 

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

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

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

332  535 
variable (provided it does not occur in the assumptions); it must not occur 
104  536 
in $f$ or~$g$. 
537 

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

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

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

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

332  542 
variable (provided it does not occur in the assumptions). In the 
104  543 
conclusion, the bound variable is named~$v$. 
544 

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

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

547 
g(b)$. 

326  548 
\end{ttdescription} 
104  549 

550 

326  551 
\subsection{Forall introduction rules} 
552 
\index{metaquantifiers} 

104  553 
\begin{ttbox} 
3108  554 
forall_intr : cterm > thm > thm 
555 
forall_intr_list : cterm list > thm > thm 

556 
forall_intr_frees : thm > thm 

104  557 
\end{ttbox} 
558 

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

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

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

332  564 
variable (provided it does not occur in the assumptions). 
104  565 

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

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

568 

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

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

571 
of the premise. 

326  572 
\end{ttdescription} 
104  573 

574 

326  575 
\subsection{Forall elimination rules} 
104  576 
\begin{ttbox} 
3108  577 
forall_elim : cterm > thm > thm 
578 
forall_elim_list : cterm list > thm > thm 

579 
forall_elim_var : int > thm > thm 

580 
forall_elim_vars : int > thm > thm 

104  581 
\end{ttbox} 
582 

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

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

587 

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

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

590 

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

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

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

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

595 

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

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

326  598 
\end{ttdescription} 
104  599 

326  600 
\subsection{Instantiation of unknowns} 
601 
\index{instantiation} 

104  602 
\begin{ttbox} 
3135  603 
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list > thm > thm 
104  604 
\end{ttbox} 
326  605 
\begin{ttdescription} 
606 
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 

607 
simultaneously substitutes types for type unknowns (the 

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

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

611 
must be distinct. The rule normalizes its conclusion. 

4376  612 

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

614 
provides a more convenient interface to this rule. 

326  615 
\end{ttdescription} 
104  616 

617 

326  618 
\subsection{Freezing/thawing type unknowns} 
619 
\index{type unknowns!freezing/thawing of} 

104  620 
\begin{ttbox} 
621 
freezeT: thm > thm 

622 
varifyT: thm > thm 

623 
\end{ttbox} 

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

627 

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

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

326  630 
\end{ttdescription} 
104  631 

632 

633 
\section{Derived rules for goaldirected proof} 

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

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

636 

637 
\subsection{Proof by assumption} 

326  638 
\index{metaassumptions} 
104  639 
\begin{ttbox} 
4276  640 
assumption : int > thm > thm Seq.seq 
104  641 
eq_assumption : int > thm > thm 
642 
\end{ttbox} 

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

646 

647 
\item[\ttindexbold{eq_assumption}] 

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

326  649 
\end{ttdescription} 
104  650 

651 

652 
\subsection{Resolution} 

326  653 
\index{resolution} 
104  654 
\begin{ttbox} 
655 
biresolution : bool > (bool*thm)list > int > thm 

4276  656 
> thm Seq.seq 
104  657 
\end{ttbox} 
326  658 
\begin{ttdescription} 
104  659 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  660 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  661 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
662 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

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

326  664 
\end{ttdescription} 
104  665 

666 

667 
\subsection{Composition: resolution without lifting} 

326  668 
\index{resolution!without lifting} 
104  669 
\begin{ttbox} 
670 
compose : thm * int * thm > thm list 

671 
COMP : thm * thm > thm 

672 
bicompose : bool > bool * thm * int > int > thm 

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

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

677 
beware of clashes! 

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

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

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

683 
result list contains the theorem 

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

685 
\] 

686 

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

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

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

696 

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

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

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

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

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

326  704 
\end{ttdescription} 
104  705 

706 

707 
\subsection{Other metarules} 

708 
\begin{ttbox} 

3108  709 
trivial : cterm > thm 
104  710 
lift_rule : (thm * int) > thm > thm 
711 
rename_params_rule : string list * int > thm > thm 

4276  712 
flexflex_rule : thm > thm Seq.seq 
104  713 
\end{ttbox} 
326  714 
\begin{ttdescription} 
104  715 
\item[\ttindexbold{trivial} $ct$] 
716 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

719 

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

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

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

723 

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

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

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

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

728 
ensure that all the parameters are distinct. 

729 
\index{parameters!renaming} 

730 

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

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

326  733 
\end{ttdescription} 
1590  734 
\index{metarules)} 
735 

736 

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

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

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

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

4317  743 
proofchecker, for example. 
1590  744 

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

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

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

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

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

6924
7e166f8d412e
Theorems involving oracles will be printed with a suffixed \verb[!];
wenzelm
parents:
6097
diff
changeset

750 
theorem's dependencies. Theorems involving oracles will be printed with a 
7e166f8d412e
Theorems involving oracles will be printed with a suffixed \verb[!];
wenzelm
parents:
6097
diff
changeset

751 
suffixed \verb[!] to point out the different quality of confidence achieved. 
1590  752 

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

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

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

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

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

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

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

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

761 
the {\tt Theorem} constructor. 

762 

763 
Proof objects are expressed using a polymorphic type of variablebranching 

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

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

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

767 
\begin{ttbox} 

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

769 
datatype rule = \(\ldots\); 

770 
type deriv = rule mtree; 

771 
\end{ttbox} 

772 
% 

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

774 
record: 

775 
\begin{ttbox} 

776 
#der (rep_thm conjI); 

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

781 
have is {\tt MinProof}. 

1590  782 

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

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

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

786 
formats, linear or treestructured. 

787 

788 
\begin{ttbox} 

789 
keep_derivs : deriv_kind ref 

790 
Deriv.size : deriv > int 

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

792 
Deriv.linear : deriv > deriv list 

1876  793 
Deriv.tree : deriv > Deriv.orule mtree 
1590  794 
\end{ttbox} 
795 

796 
\begin{ttdescription} 

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

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

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

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

802 
excluding lemmas. 

803 

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

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

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

807 

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

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

810 
reveals the singlestep Isabelle proof that is constructed internally by 

811 
tactics. 

812 

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

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

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

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

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

818 
\end{ttdescription} 

819 

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

820 
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

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

822 
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

823 
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

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

825 

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

826 

1590  827 
\index{proof objects)} 
104  828 
\index{theorems)} 
5371  829 

830 

831 
%%% Local Variables: 

832 
%%% mode: latex 

833 
%%% TeXmaster: "ref" 

834 
%%% End: 