author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 11625  74cdf24724ea 
child 30184  37969710e61f 
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 

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

201 
variables by schematic variables, renames schematic variables to 

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

203 
removes dangling sort hypotheses. 

104  204 

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

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

207 
clashes. 

208 

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

210 
\index{rules!converting destruction to elimination} 

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

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

215 

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

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

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

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

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

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

222 
whatever is left. 

4607  223 

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

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

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

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

229 
the first. 

230 

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

232 
leaving the first $j$ premises unchanged. It 

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

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

235 
negative then it rotates the premises to the right. 

11163  236 

237 
\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$ 

238 
where the value at the $i$th position (counting from $0$) in the list $ps$ 

239 
gives the position within the original thm to be transferred to position $i$. 

240 
Any remaining trailing positions are left unchanged. 

326  241 
\end{ttdescription} 
104  242 

243 

244 
\subsection{Taking a theorem apart} 

326  245 
\index{theorems!taking apart} 
104  246 
\index{flexflex constraints} 
247 
\begin{ttbox} 

4317  248 
cprop_of : thm > cterm 
104  249 
concl_of : thm > term 
250 
prems_of : thm > term list 

4317  251 
cprems_of : thm > cterm list 
104  252 
nprems_of : thm > int 
4383  253 
tpairs_of : thm > (term*term) list 
4317  254 
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

255 
theory_of_thm : thm > theory 
8136  256 
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

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

259 
crep_thm : thm > \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int, 
8136  260 
shyps: sort list, hyps: cterm list, prop:{\ts}cterm\} 
104  261 
\end{ttbox} 
326  262 
\begin{ttdescription} 
4317  263 
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as 
264 
a certified term. 

265 

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

267 
a term. 

268 

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

270 
list of terms. 

271 

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

273 
a list of certified terms. 

104  274 

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

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

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

281 

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

283 
associated with $thm$. 

284 

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

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

287 
database of loaded theories. 

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

288 

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

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

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

293 

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

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

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

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

299 
is discussed below. 

300 

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

302 
the hypotheses and statement as certified terms. 

303 

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

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

305 

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

306 

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

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

309 
\begin{ttbox} 
7644  310 
strip_shyps : thm > thm 
311 
strip_shyps_warning : thm > thm 

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

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

313 

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

314 
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

315 
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

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

317 
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

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

320 

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

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

325 
only if under an additional nonemptiness assumption. 

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

326 

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

327 
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

328 
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

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

330 
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

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

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

333 

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

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

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

338 
\texttt{strip_shyps_warning}. 

339 

340 
\begin{ttdescription} 

341 

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

343 
that can be witnessed from the type signature. 

344 

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

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

347 
(syntactic) witness. 

348 

349 
\end{ttdescription} 

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

350 

104  351 

352 
\subsection{Tracing flags for unification} 

326  353 
\index{tracing!of unification} 
104  354 
\begin{ttbox} 
8136  355 
Unify.trace_simp : bool ref \hfill\textbf{initially false} 
356 
Unify.trace_types : bool ref \hfill\textbf{initially false} 

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

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

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

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

362 
though. 

326  363 
\begin{ttdescription} 
4317  364 
\item[set Unify.trace_simp;] 
104  365 
causes tracing of the simplification phase. 
366 

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

370 

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

374 
information is almost never printed. 

375 

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

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

326  382 
\end{ttdescription} 
104  383 

384 

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

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

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

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

392 
incompatible signatures and similar errors. 

104  393 

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

399 
assertions of the form 

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

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

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

104  406 

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

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

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

410 
incompatible. 

411 

5777  412 
\medskip 
413 

414 
The following presentation of primitive rules ignores sort 

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

416 
handled transparently by the logic implementation. 

417 

418 
\bigskip 

419 

326  420 
\index{metaimplication} 
8136  421 
The \textbf{implication} rules are $({\Imp}I)$ 
104  422 
and $({\Imp}E)$: 
423 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

425 

326  426 
\index{metaequality} 
104  427 
Equality of truth values means logical equivalence: 
3524  428 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\phi\Imp\psi & 
429 
\psi\Imp\phi} 

104  430 
\qquad 
431 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

432 

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

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

437 

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

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

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

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

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

445 

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

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

451 

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

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

458 

326  459 
\subsection{Assumption rule} 
460 
\index{metaassumptions} 

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

326  471 
\subsection{Implication rules} 
472 
\index{metaimplication} 

104  473 
\begin{ttbox} 
3108  474 
implies_intr : cterm > thm > thm 
475 
implies_intr_list : cterm list > thm > thm 

104  476 
implies_intr_hyps : thm > thm 
477 
implies_elim : thm > thm > thm 

478 
implies_elim_list : thm > thm list > thm 

479 
\end{ttbox} 

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

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

485 
type $prop$. 

104  486 

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

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

489 

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

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

104  493 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
494 

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

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

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

498 

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

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

151  501 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  502 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  503 
\end{ttdescription} 
104  504 

326  505 
\subsection{Logical equivalence rules} 
506 
\index{metaequality} 

104  507 
\begin{ttbox} 
326  508 
equal_intr : thm > thm > thm 
509 
equal_elim : thm > thm > thm 

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

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

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

104  517 

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

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

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

326  521 
\end{ttdescription} 
104  522 

523 

524 
\subsection{Equality rules} 

326  525 
\index{metaequality} 
104  526 
\begin{ttbox} 
3108  527 
reflexive : cterm > thm 
104  528 
symmetric : thm > thm 
529 
transitive : thm > thm > thm 

530 
\end{ttbox} 

326  531 
\begin{ttdescription} 
104  532 
\item[\ttindexbold{reflexive} $ct$] 
151  533 
makes the theorem \(ct\equiv ct\). 
104  534 

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

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

537 

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

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

326  540 
\end{ttdescription} 
104  541 

542 

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

326  544 
\index{lambda calc@$\lambda$calculus} 
104  545 
\begin{ttbox} 
3108  546 
beta_conversion : cterm > thm 
104  547 
extensional : thm > thm 
3108  548 
abstract_rule : string > cterm > thm > thm 
104  549 
combination : thm > thm > thm 
550 
\end{ttbox} 

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

553 
\begin{ttdescription} 

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

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

557 

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

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

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

332  561 
variable (provided it does not occur in the assumptions); it must not occur 
104  562 
in $f$ or~$g$. 
563 

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

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

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

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

332  568 
variable (provided it does not occur in the assumptions). In the 
104  569 
conclusion, the bound variable is named~$v$. 
570 

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

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

573 
g(b)$. 

326  574 
\end{ttdescription} 
104  575 

576 

326  577 
\subsection{Forall introduction rules} 
578 
\index{metaquantifiers} 

104  579 
\begin{ttbox} 
3108  580 
forall_intr : cterm > thm > thm 
581 
forall_intr_list : cterm list > thm > thm 

582 
forall_intr_frees : thm > thm 

104  583 
\end{ttbox} 
584 

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

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

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

332  590 
variable (provided it does not occur in the assumptions). 
104  591 

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

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

594 

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

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

597 
of the premise. 

326  598 
\end{ttdescription} 
104  599 

600 

326  601 
\subsection{Forall elimination rules} 
104  602 
\begin{ttbox} 
3108  603 
forall_elim : cterm > thm > thm 
604 
forall_elim_list : cterm list > thm > thm 

605 
forall_elim_var : int > thm > thm 

606 
forall_elim_vars : int > thm > thm 

104  607 
\end{ttbox} 
608 

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

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

613 

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

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

616 

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

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

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

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

621 

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

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

326  625 
\end{ttdescription} 
104  626 

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

627 

326  628 
\subsection{Instantiation of unknowns} 
629 
\index{instantiation} 

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

633 
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

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

635 
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

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

637 

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

643 
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

644 
must be distinct. 
4376  645 

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

646 
In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate}) 
4376  647 
provides a more convenient interface to this rule. 
326  648 
\end{ttdescription} 
104  649 

650 

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

651 

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

652 

326  653 
\subsection{Freezing/thawing type unknowns} 
654 
\index{type unknowns!freezing/thawing of} 

104  655 
\begin{ttbox} 
656 
freezeT: thm > thm 

657 
varifyT: thm > thm 

658 
\end{ttbox} 

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

662 

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

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

326  665 
\end{ttdescription} 
104  666 

667 

668 
\section{Derived rules for goaldirected proof} 

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

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

671 

672 
\subsection{Proof by assumption} 

326  673 
\index{metaassumptions} 
104  674 
\begin{ttbox} 
4276  675 
assumption : int > thm > thm Seq.seq 
104  676 
eq_assumption : int > thm > thm 
677 
\end{ttbox} 

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

681 

682 
\item[\ttindexbold{eq_assumption}] 

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

326  684 
\end{ttdescription} 
104  685 

686 

687 
\subsection{Resolution} 

326  688 
\index{resolution} 
104  689 
\begin{ttbox} 
690 
biresolution : bool > (bool*thm)list > int > thm 

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

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

326  699 
\end{ttdescription} 
104  700 

701 

702 
\subsection{Composition: resolution without lifting} 

326  703 
\index{resolution!without lifting} 
104  704 
\begin{ttbox} 
705 
compose : thm * int * thm > thm list 

706 
COMP : thm * thm > thm 

707 
bicompose : bool > bool * thm * int > int > thm 

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

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

712 
beware of clashes! 

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

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

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

718 
result list contains the theorem 

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

720 
\] 

721 

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

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

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

731 

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

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

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

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

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

326  739 
\end{ttdescription} 
104  740 

741 

742 
\subsection{Other metarules} 

743 
\begin{ttbox} 

3108  744 
trivial : cterm > thm 
104  745 
lift_rule : (thm * int) > thm > thm 
746 
rename_params_rule : string list * int > thm > thm 

4276  747 
flexflex_rule : thm > thm Seq.seq 
104  748 
\end{ttbox} 
326  749 
\begin{ttdescription} 
104  750 
\item[\ttindexbold{trivial} $ct$] 
751 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

754 

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

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

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

758 

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

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

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

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

763 
ensure that all the parameters are distinct. 

764 
\index{parameters!renaming} 

765 

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

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

326  768 
\end{ttdescription} 
1590  769 
\index{metarules)} 
770 

771 

11622  772 
\section{Proof terms}\label{sec:proofObjects} 
773 
\index{proof terms(} Isabelle can record the full metalevel proof of each 

774 
theorem. The proof term contains all logical inferences in detail. 

775 
%while 

776 
%omitting bookkeeping steps that have no logical meaning to an outside 

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

778 
%simplifier tracing. 

779 
Resolution and rewriting steps are broken down to primitive rules of the 

780 
metalogic. The proof term can be inspected by a separate proofchecker, 

781 
for example. 

1590  782 

11622  783 
According to the wellknown {\em CurryHoward isomorphism}, a proof can 
784 
be viewed as a $\lambda$term. Following this idea, proofs 

785 
in Isabelle are internally represented by a datatype similar to the one for 

786 
terms described in \S\ref{sec:terms}. 

787 
\begin{ttbox} 

788 
infix 8 % %%; 

789 

790 
datatype proof = 

791 
PBound of int 

792 
 Abst of string * typ option * proof 

793 
 AbsP of string * term option * proof 

794 
 op % of proof * term option 

795 
 op %% of proof * proof 

796 
 Hyp of term 

797 
 PThm of (string * (string * string list) list) * 

798 
proof * term * typ list option 

799 
 PAxm of string * term * typ list option 

800 
 Oracle of string * term * typ list option 

801 
 MinProof of proof list; 

802 
\end{ttbox} 

1590  803 

11622  804 
\begin{ttdescription} 
805 
\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over 

806 
a {\it term variable} of type $\tau$ in the body $prf$. Logically, this 

807 
corresponds to $\bigwedge$ introduction. The name $a$ is used only for 

808 
parsing and printing. 

809 
\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction 

810 
over a {\it proof variable} standing for a proof of proposition $\varphi$ 

811 
in the body $prf$. This corresponds to $\Longrightarrow$ introduction. 

812 
\item[$prf$ \% $t$] \index{\%@{\tt\%}bold} 

813 
is the application of proof $prf$ to term $t$ 

814 
which corresponds to $\bigwedge$ elimination. 

815 
\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}bold} 

816 
is the application of proof $prf@1$ to 

817 
proof $prf@2$ which corresponds to $\Longrightarrow$ elimination. 

818 
\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn 

819 
\cite{debruijn72} index $i$. 

820 
\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level 

821 
hypothesis $\varphi$. 

822 
\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)] 

823 
stands for a preproved theorem, where $name$ is the name of the theorem, 

824 
$prf$ is its actual proof, $\varphi$ is the proven proposition, 

825 
and $\overline{\tau}$ is 

826 
a type assignment for the type variables occurring in the proposition. 

827 
\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)] 

828 
corresponds to the use of an axiom with name $name$ and proposition 

829 
$\varphi$, where $\overline{\tau}$ is a type assignment for the type 

830 
variables occurring in the proposition. 

831 
\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)] 

832 
denotes the invocation of an oracle with name $name$ which produced 

833 
a proposition $\varphi$, where $\overline{\tau}$ is a type assignment 

834 
for the type variables occurring in the proposition. 

835 
\item[\ttindexbold{MinProof} $prfs$] 

836 
represents a {\em minimal proof} where $prfs$ is a list of theorems, 

837 
axioms or oracles. 

838 
\end{ttdescription} 

839 
Note that there are no separate constructors 

840 
for abstraction and application on the level of {\em types}, since 

841 
instantiation of type variables is accomplished via the type assignments 

842 
attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}. 

1590  843 

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

845 
record: 

846 
\begin{ttbox} 

11622  847 
#2 (#der (rep_thm conjI)); 
848 
{\out PThm (("HOL.conjI", []),} 

849 
{\out AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %} 

850 
{\out None % None : Proofterm.proof} 

1590  851 
\end{ttbox} 
11622  852 
This proof term identifies a labelled theorem, {\tt conjI} of theory 
853 
\texttt{HOL}, whose underlying proof is 

854 
{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}. 

855 
The theorem is applied to two (implicit) term arguments, which correspond 

856 
to the two variables occurring in its proposition. 

1590  857 

11622  858 
Isabelle's inference kernel can produce proof objects with different 
859 
levels of detail. This is controlled via the global reference variable 

860 
\ttindexbold{proofs}: 

861 
\begin{ttdescription} 

862 
\item[proofs := 0;] only record uses of oracles 

863 
\item[proofs := 1;] record uses of oracles as well as dependencies 

864 
on other theorems and axioms 

865 
\item[proofs := 2;] record inferences in full detail 

1590  866 
\end{ttdescription} 
11622  867 
Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs} 
868 
will not work for proofs constructed with {\tt proofs} set to 

869 
{\tt 0} or {\tt 1}. 

870 
Theorems involving oracles will be printed with a 

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

5371  872 

7871  873 
\medskip 
874 

11622  875 
The dependencies of theorems can be viewed using the function 
876 
\ttindexbold{thm_deps}\index{theorems!dependencies}: 

7871  877 
\begin{ttbox} 
878 
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)]; 

879 
\end{ttbox} 

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

11622  881 
displays it using Isabelle's graph browser. For this to work properly, 
882 
the theorems in question have to be proved with {\tt proofs} set to a value 

883 
greater than {\tt 0}. You can use 

884 
\begin{ttbox} 

885 
ThmDeps.enable : unit > unit 

886 
ThmDeps.disable : unit > unit 

887 
\end{ttbox} 

888 
to set \texttt{proofs} appropriately. 

889 

890 
\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs} 

891 
\index{proof terms!reconstructing} 

892 
\index{proof terms!checking} 

893 

894 
When looking at the above datatype of proofs more closely, one notices that 

895 
some arguments of constructors are {\it optional}. The reason for this is that 

896 
keeping a full proof term for each theorem would result in enormous memory 

897 
requirements. Fortunately, typical proof terms usually contain quite a lot of 

898 
redundant information that can be reconstructed from the context. Therefore, 

899 
Isabelle's inference kernel creates only {\em partial} (or {\em implicit}) 

900 
\index{proof terms!partial} proof terms, in which 

901 
all typing information in terms, all term and type labels of abstractions 

902 
{\tt AbsP} and {\tt Abst}, and (if possible) some argument terms of 

903 
\verb!%! are omitted. The following functions are available for 

904 
reconstructing and checking proof terms: 

905 
\begin{ttbox} 

906 
Reconstruct.reconstruct_proof : 

907 
Sign.sg > term > Proofterm.proof > Proofterm.proof 

908 
Reconstruct.expand_proof : 

909 
Sign.sg > string list > Proofterm.proof > Proofterm.proof 

910 
ProofChecker.thm_of_proof : theory > Proofterm.proof > thm 

911 
\end{ttbox} 

912 

913 
\begin{ttdescription} 

914 
\item[Reconstruct.reconstruct_proof $sg$ $t$ $prf$] 

915 
turns the partial proof $prf$ into a full proof of the 

916 
proposition denoted by $t$, with respect to signature $sg$. 

917 
Reconstruction will fail with an error message if $prf$ 

918 
is not a proof of $t$, is illformed, or does not contain 

919 
sufficient information for reconstruction by 

920 
{\em higher order pattern unification} 

921 
\cite{nipkowpatterns, BerghoferNipkow:2000:TPHOL}. 

922 
The latter may only happen for proofs 

923 
built up ``by hand'' but not for those produced automatically 

924 
by Isabelle's inference kernel. 

925 
\item[Reconstruct.expand_proof $sg$ 

926 
\ttlbrack$name@1$, $\ldots$, $name@n${\ttrbrack} $prf$] 

927 
expands and reconstructs the proofs of all theorems with names 

928 
$name@1$, $\ldots$, $name@n$ in the (full) proof $prf$. 

929 
\item[ProofChecker.thm_of_proof $thy$ $prf$] turns the (full) proof 

930 
$prf$ into a theorem with respect to theory $thy$ by replaying 

931 
it using only primitive rules from Isabelle's inference kernel. 

932 
\end{ttdescription} 

933 

934 
\subsection{Parsing and printing proof terms} 

935 
\index{proof terms!parsing} 

936 
\index{proof terms!printing} 

937 

938 
Isabelle offers several functions for parsing and printing 

939 
proof terms. The concrete syntax for proof terms is described 

940 
in Fig.\ts\ref{fig:proof_gram}. 

941 
Implicit term arguments in partial proofs are indicated 

942 
by ``{\tt _}''. 

943 
Type arguments for theorems and axioms may be specified using 

944 
\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)} 

945 
(see \S\ref{sec:basic_syntax}). 

946 
They must appear before any other term argument of a theorem 

947 
or axiom. In contrast to term arguments, type arguments may 

948 
be completely omitted. 

7871  949 
\begin{ttbox} 
11625
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset

950 
ProofSyntax.read_proof : theory > bool > string > Proofterm.proof 
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset

951 
ProofSyntax.pretty_proof : Sign.sg > Proofterm.proof > Pretty.T 
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset

952 
ProofSyntax.pretty_proof_of : bool > thm > Pretty.T 
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset

953 
ProofSyntax.print_proof_of : bool > thm > unit 
7871  954 
\end{ttbox} 
11622  955 
\begin{figure} 
956 
\begin{center} 

957 
\begin{tabular}{rcl} 

958 
$proof$ & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$$~~ 

959 
$\Lambda params${\tt .} $proof$ \\ 

960 
& $$ & $proof$ \verb!%! $any$ ~~$$~~ 

961 
$proof$ $\cdot$ $any$ \\ 

962 
& $$ & $proof$ \verb!%%! $proof$ ~~$$~~ 

963 
$proof$ {\boldmath$\cdot$} $proof$ \\ 

964 
& $$ & $id$ ~~$$~~ $longid$ \\\\ 

965 
$param$ & $=$ & $idt$ ~~$$~~ $idt$ {\tt :} $prop$ ~~$$~~ 

966 
{\tt (} $param$ {\tt )} \\\\ 

967 
$params$ & $=$ & $param$ ~~$$~~ $param$ $params$ 

968 
\end{tabular} 

969 
\end{center} 

970 
\caption{Proof term syntax}\label{fig:proof_gram} 

971 
\end{figure} 

972 
The function {\tt read_proof} reads in a proof term with 

973 
respect to a given theory. The boolean flag indicates whether 

974 
the proof term to be parsed contains explicit typing information 

975 
to be taken into account. 

976 
Usually, typing information is left implicit and 

977 
is inferred during proof reconstruction. The pretty printing 

978 
functions operating on theorems take a boolean flag as an 

979 
argument which indicates whether the proof term should 

980 
be reconstructed before printing. 

981 

982 
The following example (based on Isabelle/HOL) illustrates how 

983 
to parse and check proof terms. We start by parsing a partial 

984 
proof term 

985 
\begin{ttbox} 

986 
val prf = ProofSyntax.read_proof Main.thy false 

987 
"impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %% 

988 
(Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))"; 

989 
{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%} 

990 
{\out AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %} 

991 
{\out None % None % None %% PBound 0 %%} 

992 
{\out AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof} 

993 
\end{ttbox} 

994 
The statement to be established by this proof is 

995 
\begin{ttbox} 

996 
val t = term_of 

997 
(read_cterm (sign_of Main.thy) ("A & B > B & A", propT)); 

998 
{\out val t = Const ("Trueprop", "bool => prop") $} 

999 
{\out (Const ("op >", "[bool, bool] => bool") $} 

1000 
{\out \dots $ \dots : Term.term} 

1001 
\end{ttbox} 

1002 
Using {\tt t} we can reconstruct the full proof 

1003 
\begin{ttbox} 

1004 
val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf; 

1005 
{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %} 

1006 
{\out Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %} 

1007 
{\out Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%} 

1008 
{\out AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)} 

1009 
{\out : Proofterm.proof} 

1010 
\end{ttbox} 

1011 
This proof can finally be turned into a theorem 

1012 
\begin{ttbox} 

1013 
val thm = ProofChecker.thm_of_proof Main.thy prf'; 

1014 
{\out val thm = "A & B > B & A" : Thm.thm} 

1015 
\end{ttbox} 

1016 

1017 
\index{proof terms)} 

1018 
\index{theorems)} 

7871  1019 

5371  1020 

1021 
%%% Local Variables: 

1022 
%%% mode: latex 

1023 
%%% TeXmaster: "ref" 

1024 
%%% End: 