author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9499  7e6988210488 
child 11163  14732e3eaa6e 
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} 
8136  76 
RSN : thm * (int * thm) > thm \hfill\textbf{infix} 
77 
RS : thm * thm > thm \hfill\textbf{infix} 

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

9288
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9258
diff
changeset

79 
OF : thm * thm list > thm \hfill\textbf{infix} 
8136  80 
RLN : thm list * (int * thm list) > thm list \hfill\textbf{infix} 
81 
RL : thm list * thm list > thm list \hfill\textbf{infix} 

82 
MRL : thm list list * thm list > thm list \hfill\textbf{infix} 

104  83 
\end{ttbox} 
326  84 
Joining rules together is a simple way of deriving new rules. These 
876  85 
functions are especially useful with destruction rules. To store 
86 
the result in the theorem database, use \ttindex{bind_thm} 

87 
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 

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

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

104  93 

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

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

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

97 

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

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

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

103 
for expressing proof trees. 

9288
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9258
diff
changeset

104 

06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9258
diff
changeset

105 
\item[\tt {$thm$ OF $[thm@1,\ldots,thm@n]$}] \indexbold{*OF} is the same as 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9258
diff
changeset

106 
\texttt{$[thm@1,\ldots,thm@n]$ MRS $thm$}, with slightly more readable 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9258
diff
changeset

107 
argument order, though. 
104  108 

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

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

104  113 

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

104  116 

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

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

119 
It too is useful for expressing proof trees. 

326  120 
\end{ttdescription} 
104  121 

122 

123 
\subsection{Expanding definitions in theorems} 

326  124 
\index{metarewriting!in theorems} 
104  125 
\begin{ttbox} 
126 
rewrite_rule : thm list > thm > thm 

127 
rewrite_goals_rule : thm list > thm > thm 

128 
\end{ttbox} 

326  129 
\begin{ttdescription} 
104  130 
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}] 
131 
unfolds the {\it defs} throughout the theorem~{\it thm}. 

132 

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

8136  134 
unfolds the {\it defs} in the premises of~{\it thm}, but it leaves the 
135 
conclusion unchanged. This rule is the basis for \ttindex{rewrite_goals_tac}, 

136 
but it serves little purpose in forward proof. 

326  137 
\end{ttdescription} 
104  138 

139 

4383  140 
\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate} 
326  141 
\index{instantiation} 
8136  142 
\begin{alltt}\footnotesize 
4383  143 
read_instantiate : (string*string) list > thm > thm 
144 
read_instantiate_sg : Sign.sg > (string*string) list > thm > thm 

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

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

8136  147 
\end{alltt} 
104  148 
These metarules instantiate type and term unknowns in a theorem. They are 
149 
occasionally useful. They can prevent difficulties with higherorder 

150 
unification, and define specialized versions of rules. 

326  151 
\begin{ttdescription} 
104  152 
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}] 
153 
processes the instantiations {\it insts} and instantiates the rule~{\it 

154 
thm}. The processing of instantiations is described 

326  155 
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}. 
104  156 

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

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

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

326  160 
associated with the proof state. 
161 

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

163 
incorrectly. 

104  164 

326  165 
\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

166 
is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads 
326  167 
the instantiations under signature~{\it sg}. This is necessary to 
168 
instantiate a rule from a general theory, such as firstorder logic, 

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

170 
sign_of} to get a theory's signature. 

104  171 

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

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

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

4317  175 

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

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

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

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

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

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

182 
instantiated before terms. 

183 

326  184 
\end{ttdescription} 
104  185 

186 

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

187 
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules} 
326  188 
\index{theorems!standardizing} 
104  189 
\begin{ttbox} 
8969  190 
standard : thm > thm 
191 
zero_var_indexes : thm > thm 

192 
make_elim : thm > thm 

193 
rule_by_tactic : tactic > thm > thm 

194 
rotate_prems : int > thm > thm 

195 
permute_prems : int > int > thm > thm 

104  196 
\end{ttbox} 
326  197 
\begin{ttdescription} 
3108  198 
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form 
199 
of objectrules. It discharges all metaassumptions, replaces free 

200 
variables by schematic variables, renames schematic variables to 

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

202 
removes dangling sort hypotheses. 

104  203 

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

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

206 
clashes. 

207 

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

209 
\index{rules!converting destruction to elimination} 

8136  210 
converts $thm$, which should be a destruction rule of the form 
211 
$\List{P@1;\ldots;P@m}\Imp 

104  212 
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This 
213 
is the basis for destructresolution: {\tt dresolve_tac}, etc. 

214 

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

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

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

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

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

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

221 
whatever is left. 

4607  222 

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

8969  224 
the left by~$k$ positions (to the right if $k<0$). It simply calls 
225 
\texttt{permute_prems}, below, with $j=0$. Used with 

226 
\texttt{eresolve_tac}\index{*eresolve_tac!on other than first premise}, it 

227 
gives the effect of applying the tactic to some other premise of $thm$ than 

228 
the first. 

229 

230 
\item[\ttindexbold{permute_prems} $j$ $k$ $thm$] rotates the premises of $thm$ 

231 
leaving the first $j$ premises unchanged. It 

232 
requires $0\leq j\leq n$, where $n$ is the number of premises. If $k$ is 

233 
positive then it rotates the remaining $nj$ premises to the left; if $k$ is 

234 
negative then it rotates the premises to the right. 

326  235 
\end{ttdescription} 
104  236 

237 

238 
\subsection{Taking a theorem apart} 

326  239 
\index{theorems!taking apart} 
104  240 
\index{flexflex constraints} 
241 
\begin{ttbox} 

4317  242 
cprop_of : thm > cterm 
104  243 
concl_of : thm > term 
244 
prems_of : thm > term list 

4317  245 
cprems_of : thm > cterm list 
104  246 
nprems_of : thm > int 
4383  247 
tpairs_of : thm > (term*term) list 
4317  248 
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

249 
theory_of_thm : thm > theory 
8136  250 
dest_state : thm * int > (term*term) list * term list * term * term 
9499
7e6988210488
rep_thm: 'der' field has additional bool for oracles;
wenzelm
parents:
9288
diff
changeset

251 
rep_thm : thm > \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int, 
8136  252 
shyps: sort list, hyps: term list, prop: term\} 
9499
7e6988210488
rep_thm: 'der' field has additional bool for oracles;
wenzelm
parents:
9288
diff
changeset

253 
crep_thm : thm > \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int, 
8136  254 
shyps: sort list, hyps: cterm list, prop:{\ts}cterm\} 
104  255 
\end{ttbox} 
326  256 
\begin{ttdescription} 
4317  257 
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as 
258 
a certified term. 

259 

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

261 
a term. 

262 

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

264 
list of terms. 

265 

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

267 
a list of certified terms. 

104  268 

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

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

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

275 

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

277 
associated with $thm$. 

278 

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

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

281 
database of loaded theories. 

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

282 

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

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

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

287 

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

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

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

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

293 
is discussed below. 

294 

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

296 
the hypotheses and statement as certified terms. 

297 

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

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

299 

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

300 

5777  301 
\subsection{*Sort hypotheses} \label{sec:sorthyps} 
2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

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

303 
\begin{ttbox} 
7644  304 
strip_shyps : thm > thm 
305 
strip_shyps_warning : thm > thm 

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

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

307 

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

308 
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

309 
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

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

311 
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

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

314 

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

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

319 
only if under an additional nonemptiness assumption. 

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

320 

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

321 
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

322 
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

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

324 
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

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

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

327 

7644  328 
Isabelle automatically removes extraneous sorts from the {\tt shyps} field at 
329 
the end of a proof, provided that nonemptiness can be established by looking 

330 
at the theorem's signature: from the {\tt classes} and {\tt arities} 

331 
information. This operation is performed by \texttt{strip_shyps} and 

332 
\texttt{strip_shyps_warning}. 

333 

334 
\begin{ttdescription} 

335 

336 
\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses 

337 
that can be witnessed from the type signature. 

338 

339 
\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but 

340 
issues a warning message of any pending sort hypotheses that do not have a 

341 
(syntactic) witness. 

342 

343 
\end{ttdescription} 

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

344 

104  345 

346 
\subsection{Tracing flags for unification} 

326  347 
\index{tracing!of unification} 
104  348 
\begin{ttbox} 
8136  349 
Unify.trace_simp : bool ref \hfill\textbf{initially false} 
350 
Unify.trace_types : bool ref \hfill\textbf{initially false} 

351 
Unify.trace_bound : int ref \hfill\textbf{initially 10} 

352 
Unify.search_bound : int ref \hfill\textbf{initially 20} 

104  353 
\end{ttbox} 
354 
Tracing the search may be useful when higherorder unification behaves 

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

356 
though. 

326  357 
\begin{ttdescription} 
4317  358 
\item[set Unify.trace_simp;] 
104  359 
causes tracing of the simplification phase. 
360 

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

364 

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

368 
information is almost never printed. 

369 

8136  370 
\item[Unify.search_bound := $n$;] prevents unification from 
371 
searching past the depth~$n$. Because of this bound, higherorder 

4317  372 
unification cannot return an infinite sequence, though it can return 
8136  373 
an exponentially long one. The search rarely approaches the default value 
4317  374 
of~20. If the search is cut off, unification prints a warning 
375 
\texttt{Unification bound exceeded}. 

326  376 
\end{ttdescription} 
104  377 

378 

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

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

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

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

386 
incompatible signatures and similar errors. 

104  387 

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

393 
assertions of the form 

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

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

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

104  400 

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

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

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

404 
incompatible. 

405 

5777  406 
\medskip 
407 

408 
The following presentation of primitive rules ignores sort 

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

410 
handled transparently by the logic implementation. 

411 

412 
\bigskip 

413 

326  414 
\index{metaimplication} 
8136  415 
The \textbf{implication} rules are $({\Imp}I)$ 
104  416 
and $({\Imp}E)$: 
417 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

419 

326  420 
\index{metaequality} 
104  421 
Equality of truth values means logical equivalence: 
3524  422 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi & 
423 
\psi\Imp\phi} 

104  424 
\qquad 
425 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

426 

8136  427 
The \textbf{equality} rules are reflexivity, symmetry, and transitivity: 
104  428 
\[ {a\equiv a}\,(refl) \qquad 
429 
\infer[(sym)]{b\equiv a}{a\equiv b} \qquad 

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

431 

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

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

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

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

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

439 

8136  440 
The \textbf{abstraction} and \textbf{combination} rules let conversions be 
332  441 
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the 
104  442 
assumptions.} 
443 
\[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad 

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

445 

326  446 
\index{metaquantifiers} 
8136  447 
The \textbf{universal quantification} rules are $(\Forall I)$ and $(\Forall 
104  448 
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.} 
449 
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad 

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

452 

326  453 
\subsection{Assumption rule} 
454 
\index{metaassumptions} 

104  455 
\begin{ttbox} 
3108  456 
assume: cterm > thm 
104  457 
\end{ttbox} 
326  458 
\begin{ttdescription} 
104  459 
\item[\ttindexbold{assume} $ct$] 
332  460 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  461 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  462 
are not allowed in assumptions. 
326  463 
\end{ttdescription} 
104  464 

326  465 
\subsection{Implication rules} 
466 
\index{metaimplication} 

104  467 
\begin{ttbox} 
3108  468 
implies_intr : cterm > thm > thm 
469 
implies_intr_list : cterm list > thm > thm 

104  470 
implies_intr_hyps : thm > thm 
471 
implies_elim : thm > thm > thm 

472 
implies_elim_list : thm > thm list > thm 

473 
\end{ttbox} 

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

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

479 
type $prop$. 

104  480 

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

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

483 

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

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

104  487 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
488 

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

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

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

492 

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

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

151  495 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  496 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  497 
\end{ttdescription} 
104  498 

326  499 
\subsection{Logical equivalence rules} 
500 
\index{metaequality} 

104  501 
\begin{ttbox} 
326  502 
equal_intr : thm > thm > thm 
503 
equal_elim : thm > thm > thm 

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

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

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

104  511 

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

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

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

326  515 
\end{ttdescription} 
104  516 

517 

518 
\subsection{Equality rules} 

326  519 
\index{metaequality} 
104  520 
\begin{ttbox} 
3108  521 
reflexive : cterm > thm 
104  522 
symmetric : thm > thm 
523 
transitive : thm > thm > thm 

524 
\end{ttbox} 

326  525 
\begin{ttdescription} 
104  526 
\item[\ttindexbold{reflexive} $ct$] 
151  527 
makes the theorem \(ct\equiv ct\). 
104  528 

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

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

531 

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

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

326  534 
\end{ttdescription} 
104  535 

536 

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

326  538 
\index{lambda calc@$\lambda$calculus} 
104  539 
\begin{ttbox} 
3108  540 
beta_conversion : cterm > thm 
104  541 
extensional : thm > thm 
3108  542 
abstract_rule : string > cterm > thm > thm 
104  543 
combination : thm > thm > thm 
544 
\end{ttbox} 

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

547 
\begin{ttdescription} 

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

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

551 

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

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

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

332  555 
variable (provided it does not occur in the assumptions); it must not occur 
104  556 
in $f$ or~$g$. 
557 

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

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

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

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

332  562 
variable (provided it does not occur in the assumptions). In the 
104  563 
conclusion, the bound variable is named~$v$. 
564 

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

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

567 
g(b)$. 

326  568 
\end{ttdescription} 
104  569 

570 

326  571 
\subsection{Forall introduction rules} 
572 
\index{metaquantifiers} 

104  573 
\begin{ttbox} 
3108  574 
forall_intr : cterm > thm > thm 
575 
forall_intr_list : cterm list > thm > thm 

576 
forall_intr_frees : thm > thm 

104  577 
\end{ttbox} 
578 

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

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

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

332  584 
variable (provided it does not occur in the assumptions). 
104  585 

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

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

588 

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

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

591 
of the premise. 

326  592 
\end{ttdescription} 
104  593 

594 

326  595 
\subsection{Forall elimination rules} 
104  596 
\begin{ttbox} 
3108  597 
forall_elim : cterm > thm > thm 
598 
forall_elim_list : cterm list > thm > thm 

599 
forall_elim_var : int > thm > thm 

600 
forall_elim_vars : int > thm > thm 

104  601 
\end{ttbox} 
602 

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

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

607 

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

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

610 

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

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

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

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

615 

9258  616 
\item[\ttindexbold{forall_elim_vars} $k$ $thm$] 
617 
applies {\tt forall_elim_var}~$k$ repeatedly until the theorem no longer has 

618 
the form $\Forall x.\phi$. 

326  619 
\end{ttdescription} 
104  620 

8135
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

621 

326  622 
\subsection{Instantiation of unknowns} 
623 
\index{instantiation} 

8136  624 
\begin{alltt}\footnotesize 
3135  625 
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list > thm > thm 
8136  626 
\end{alltt} 
8135
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

627 
There are two versions of this rule. The primitive one is 
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

628 
\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can 
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

629 
produce a conclusion not in normal form. A derived version is 
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

630 
\ttindexbold{Drule.instantiate}, which normalizes its conclusion. 
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

631 

326  632 
\begin{ttdescription} 
8136  633 
\item[\ttindexbold{instantiate} ($tyinsts$,$insts$) $thm$] 
326  634 
simultaneously substitutes types for type unknowns (the 
104  635 
$tyinsts$) and terms for term unknowns (the $insts$). Instantiations are 
636 
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the 

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

8135
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

638 
must be distinct. 
4376  639 

8135
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

640 
In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate}) 
4376  641 
provides a more convenient interface to this rule. 
326  642 
\end{ttdescription} 
104  643 

644 

8135
ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

645 

ad1c4a678196
Documented Thm.instantiate (not normalizing) and Drule.instantiate
paulson
parents:
7871
diff
changeset

646 

326  647 
\subsection{Freezing/thawing type unknowns} 
648 
\index{type unknowns!freezing/thawing of} 

104  649 
\begin{ttbox} 
650 
freezeT: thm > thm 

651 
varifyT: thm > thm 

652 
\end{ttbox} 

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

656 

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

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

326  659 
\end{ttdescription} 
104  660 

661 

662 
\section{Derived rules for goaldirected proof} 

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

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

665 

666 
\subsection{Proof by assumption} 

326  667 
\index{metaassumptions} 
104  668 
\begin{ttbox} 
4276  669 
assumption : int > thm > thm Seq.seq 
104  670 
eq_assumption : int > thm > thm 
671 
\end{ttbox} 

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

675 

676 
\item[\ttindexbold{eq_assumption}] 

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

326  678 
\end{ttdescription} 
104  679 

680 

681 
\subsection{Resolution} 

326  682 
\index{resolution} 
104  683 
\begin{ttbox} 
684 
biresolution : bool > (bool*thm)list > int > thm 

4276  685 
> thm Seq.seq 
104  686 
\end{ttbox} 
326  687 
\begin{ttdescription} 
104  688 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  689 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  690 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
691 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

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

326  693 
\end{ttdescription} 
104  694 

695 

696 
\subsection{Composition: resolution without lifting} 

326  697 
\index{resolution!without lifting} 
104  698 
\begin{ttbox} 
699 
compose : thm * int * thm > thm list 

700 
COMP : thm * thm > thm 

701 
bicompose : bool > bool * thm * int > int > thm 

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

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

706 
beware of clashes! 

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

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

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

712 
result list contains the theorem 

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

714 
\] 

715 

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

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

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

725 

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

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

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

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

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

326  733 
\end{ttdescription} 
104  734 

735 

736 
\subsection{Other metarules} 

737 
\begin{ttbox} 

3108  738 
trivial : cterm > thm 
104  739 
lift_rule : (thm * int) > thm > thm 
740 
rename_params_rule : string list * int > thm > thm 

4276  741 
flexflex_rule : thm > thm Seq.seq 
104  742 
\end{ttbox} 
326  743 
\begin{ttdescription} 
104  744 
\item[\ttindexbold{trivial} $ct$] 
745 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

748 

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

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

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

752 

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

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

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

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

757 
ensure that all the parameters are distinct. 

758 
\index{parameters!renaming} 

759 

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

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

326  762 
\end{ttdescription} 
1590  763 
\index{metarules)} 
764 

765 

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

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

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

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

4317  772 
proofchecker, for example. 
1590  773 

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

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

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

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

778 
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

779 
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

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

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

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

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

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

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

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

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

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

790 
the {\tt Theorem} constructor. 

791 

792 
Proof objects are expressed using a polymorphic type of variablebranching 

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

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

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

796 
\begin{ttbox} 

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

798 
datatype rule = \(\ldots\); 

799 
type deriv = rule mtree; 

800 
\end{ttbox} 

801 
% 

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

803 
record: 

804 
\begin{ttbox} 

805 
#der (rep_thm conjI); 

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

810 
have is {\tt MinProof}. 

1590  811 

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

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

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

815 
formats, linear or treestructured. 

816 

817 
\begin{ttbox} 

818 
keep_derivs : deriv_kind ref 

819 
Deriv.size : deriv > int 

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

821 
Deriv.linear : deriv > deriv list 

1876  822 
Deriv.tree : deriv > Deriv.orule mtree 
1590  823 
\end{ttbox} 
824 

825 
\begin{ttdescription} 

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

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

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

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

831 
excluding lemmas. 

832 

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

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

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

836 

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

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

839 
reveals the singlestep Isabelle proof that is constructed internally by 

840 
tactics. 

841 

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

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

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

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

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

847 
\end{ttdescription} 

848 

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

849 
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

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

851 
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

852 
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

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

854 

1590  855 
\index{proof objects)} 
104  856 
\index{theorems)} 
5371  857 

7871  858 
\medskip 
859 

860 
The dependencies of theorems can be viewed using the function \ttindexbold{thm_deps}: 

861 
\begin{ttbox} 

862 
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)]; 

863 
\end{ttbox} 

864 
generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and 

865 
displays it using Isabelle's graph browser. This function expects derivations 

866 
to be enabled. The structure \texttt{ThmDeps} contains the two functions 

867 
\begin{ttbox} 

868 
enable : unit > unit 

869 
disable : unit > unit 

870 
\end{ttbox} 

871 
which set \texttt{keep_derivs} appropriately. 

872 

5371  873 

874 
%%% Local Variables: 

875 
%%% mode: latex 

876 
%%% TeXmaster: "ref" 

877 
%%% End: 