author  wenzelm 
Tue, 06 May 1997 12:50:16 +0200  
changeset 3108  335efc3f5632 
parent 2044  e8d52d05530a 
child 3135  233aba197bf2 
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 

36 
prthq : thm Sequence.seq > thm Sequence.seq 

37 
print_thm : thm > unit 

38 
print_goals : int > thm > unit 

39 
string_of_thm : thm > string 

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

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

44 

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

46 
are convenient for imperative programming. 

47 

48 
\begin{ttdescription} 

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

51 

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

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

54 

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

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

57 
the output of a tactic. 

58 

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

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

61 

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

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

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

65 
to display proof states. 

66 

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

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

326  69 
\end{ttdescription} 
104  70 

71 

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

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

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

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

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

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

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

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

86 
(\S\ref{ExtractingAndStoringTheProvedTheorem}). 

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

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

104  92 

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

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

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

96 

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

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

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

102 
for expressing proof trees. 

103 

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

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

104  108 

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

104  111 

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

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

114 
It too is useful for expressing proof trees. 

326  115 
\end{ttdescription} 
104  116 

117 

118 
\subsection{Expanding definitions in theorems} 

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

122 
rewrite_goals_rule : thm list > thm > thm 

123 
\end{ttbox} 

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

127 

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

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

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

131 
serves little purpose in forward proof. 

326  132 
\end{ttdescription} 
104  133 

134 

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

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

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

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

143 
occasionally useful. They can prevent difficulties with higherorder 

144 
unification, and define specialized versions of rules. 

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

148 
thm}. The processing of instantiations is described 

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

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

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

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

326  154 
associated with the proof state. 
155 

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

157 
incorrectly. 

104  158 

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

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

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

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

164 
sign_of} to get a theory's signature. 

104  165 

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

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

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

326  169 
\end{ttdescription} 
104  170 

171 

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

172 
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules} 
326  173 
\index{theorems!standardizing} 
104  174 
\begin{ttbox} 
332  175 
standard : thm > thm 
176 
zero_var_indexes : thm > thm 

177 
make_elim : thm > thm 

104  178 
rule_by_tactic : tactic > thm > thm 
179 
\end{ttbox} 

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

183 
variables by schematic variables, renames schematic variables to 

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

185 
removes dangling sort hypotheses. 

104  186 

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

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

189 
clashes. 

190 

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

192 
\index{rules!converting destruction to elimination} 

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

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

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

196 

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

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

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

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

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

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

203 
whatever is left. 

326  204 
\end{ttdescription} 
104  205 

206 

207 
\subsection{Taking a theorem apart} 

326  208 
\index{theorems!taking apart} 
104  209 
\index{flexflex constraints} 
210 
\begin{ttbox} 

211 
concl_of : thm > term 

212 
prems_of : thm > term list 

213 
nprems_of : thm > int 

214 
tpairs_of : thm > (term*term)list 

215 
stamps_of_thy : thm > string ref list 

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

216 
theory_of_thm : thm > theory 
286  217 
dest_state : thm*int > (term*term)list*term list*term*term 
3108  218 
rep_thm : thm > {\ttlbrace}prop: term, hyps: term list, der: deriv, 
219 
maxidx: int, sign: Sign.sg, shyps: sort list\ttrbrace 

104  220 
\end{ttbox} 
326  221 
\begin{ttdescription} 
104  222 
\item[\ttindexbold{concl_of} $thm$] 
223 
returns the conclusion of $thm$ as a term. 

224 

225 
\item[\ttindexbold{prems_of} $thm$] 

226 
returns the premises of $thm$ as a list of terms. 

227 

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

286  229 
returns the number of premises in $thm$, and is equivalent to {\tt 
230 
length(prems_of~$thm$)}. 

104  231 

232 
\item[\ttindexbold{tpairs_of} $thm$] 

233 
returns the flexflex constraints of $thm$. 

234 

235 
\item[\ttindexbold{stamps_of_thm} $thm$] 

332  236 
returns the \rmindex{stamps} of the signature associated with~$thm$. 
104  237 

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

238 
\item[\ttindexbold{theory_of_thm} $thm$] 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

239 
returns the theory associated with $thm$. 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
332
diff
changeset

240 

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

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

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

245 

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

246 
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record containing the 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

247 
statement of~$thm$ ({\tt prop}), its list of metaassumptions ({\tt hyps}), 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

248 
its derivation ({\tt der}), a bound on the maximum subscript of its 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

249 
unknowns ({\tt maxidx}), and its signature ({\tt sign}). The {\tt shyps} 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

250 
field is discussed below. 
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset

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

252 

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

253 

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

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

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

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

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

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

259 

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

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

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

262 
causes sort hypotheses to be deleted, printing a warning. 
326  263 
\end{ttdescription} 
104  264 

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

265 
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

266 
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

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

268 
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

269 
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

270 
a type belonging to it because certain axioms are unsatisfiable. 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

271 

3108  272 
If a theorem contains a type variable that is constrained by an empty 
273 
sort, then that theorem has no instances. It is basically an instance 

274 
of {\em ex falso quodlibet}. But what if it is used to prove another 

275 
theorem that no longer involves that sort? The latter theorem holds 

276 
only if under an additional nonemptiness assumption. 

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

277 

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

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

279 
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

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

281 
theorem's proof that no longer appear in the {\tt prop} or {\tt hyps} 
e8d52d05530a
Improved discussion of shyps thanks to Markus Wenzel
paulson
parents:
2040
diff
changeset

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

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

284 

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

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

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

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

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

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

290 

104  291 

292 
\subsection{Tracing flags for unification} 

326  293 
\index{tracing!of unification} 
104  294 
\begin{ttbox} 
295 
Unify.trace_simp : bool ref \hfill{\bf initially false} 

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

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

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

299 
\end{ttbox} 

300 
Tracing the search may be useful when higherorder unification behaves 

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

302 
though. 

326  303 
\begin{ttdescription} 
304 
\item[Unify.trace_simp := true;] 

104  305 
causes tracing of the simplification phase. 
306 

326  307 
\item[Unify.trace_types := true;] 
104  308 
generates warnings of incompleteness, when unification is not considering 
309 
all possible instantiations of type unknowns. 

310 

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

314 
information is almost never printed. 

315 

326  316 
\item[Unify.search_bound := $n$;] 
104  317 
causes unification to limit its search to depth~$n$. Because of this 
318 
bound, higherorder unification cannot return an infinite sequence, though 

319 
it can return a very long one. The search rarely approaches the default 

320 
value of~20. If the search is cut off, unification prints {\tt 

321 
***Unification bound exceeded}. 

326  322 
\end{ttdescription} 
104  323 

324 

325 
\section{Primitive metalevel inference rules} 

326 
\index{metarules(} 

327 
These implement the metalogic in {\sc lcf} style, as functions from theorems 

328 
to theorems. They are, rarely, useful for deriving results in the pure 

329 
theory. Mainly, they are included for completeness, and most users should 

326  330 
not bother with them. The metarules raise exception \xdx{THM} to signal 
104  331 
malformed premises, incompatible signatures and similar errors. 
332 

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

338 
assertions of the form 

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

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

342 
\phi$. Do not confuse metalevel assumptions with the objectlevel 

343 
assumptions in a subgoal, which are represented in the metalogic 

344 
using~$\Imp$. 

104  345 

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

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

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

349 
incompatible. 

350 

326  351 
\index{metaimplication} 
332  352 
The {\bf implication} rules are $({\Imp}I)$ 
104  353 
and $({\Imp}E)$: 
354 
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad 

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

356 

326  357 
\index{metaequality} 
104  358 
Equality of truth values means logical equivalence: 
359 
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} & 

286  360 
\infer*{\phi}{[\psi]}} 
104  361 
\qquad 
362 
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \] 

363 

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

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

368 

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

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

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

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

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

376 

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

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

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

382 

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

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

389 

326  390 
\subsection{Assumption rule} 
391 
\index{metaassumptions} 

104  392 
\begin{ttbox} 
3108  393 
assume: cterm > thm 
104  394 
\end{ttbox} 
326  395 
\begin{ttdescription} 
104  396 
\item[\ttindexbold{assume} $ct$] 
332  397 
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$. 
104  398 
The rule checks that $ct$ has type $prop$ and contains no unknowns, which 
332  399 
are not allowed in assumptions. 
326  400 
\end{ttdescription} 
104  401 

326  402 
\subsection{Implication rules} 
403 
\index{metaimplication} 

104  404 
\begin{ttbox} 
3108  405 
implies_intr : cterm > thm > thm 
406 
implies_intr_list : cterm list > thm > thm 

104  407 
implies_intr_hyps : thm > thm 
408 
implies_elim : thm > thm > thm 

409 
implies_elim_list : thm > thm list > thm 

410 
\end{ttbox} 

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

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

416 
type $prop$. 

104  417 

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

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

420 

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

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

104  424 
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$. 
425 

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

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

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

429 

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

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

151  432 
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and 
104  433 
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$. 
326  434 
\end{ttdescription} 
104  435 

326  436 
\subsection{Logical equivalence rules} 
437 
\index{metaequality} 

104  438 
\begin{ttbox} 
326  439 
equal_intr : thm > thm > thm 
440 
equal_elim : thm > thm > thm 

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

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

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

104  448 

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

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

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

326  452 
\end{ttdescription} 
104  453 

454 

455 
\subsection{Equality rules} 

326  456 
\index{metaequality} 
104  457 
\begin{ttbox} 
3108  458 
reflexive : cterm > thm 
104  459 
symmetric : thm > thm 
460 
transitive : thm > thm > thm 

461 
\end{ttbox} 

326  462 
\begin{ttdescription} 
104  463 
\item[\ttindexbold{reflexive} $ct$] 
151  464 
makes the theorem \(ct\equiv ct\). 
104  465 

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

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

468 

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

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

326  471 
\end{ttdescription} 
104  472 

473 

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

326  475 
\index{lambda calc@$\lambda$calculus} 
104  476 
\begin{ttbox} 
3108  477 
beta_conversion : cterm > thm 
104  478 
extensional : thm > thm 
3108  479 
abstract_rule : string > cterm > thm > thm 
104  480 
combination : thm > thm > thm 
481 
\end{ttbox} 

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

484 
\begin{ttdescription} 

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

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

488 

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

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

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

332  492 
variable (provided it does not occur in the assumptions); it must not occur 
104  493 
in $f$ or~$g$. 
494 

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

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

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

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

332  499 
variable (provided it does not occur in the assumptions). In the 
104  500 
conclusion, the bound variable is named~$v$. 
501 

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

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

504 
g(b)$. 

326  505 
\end{ttdescription} 
104  506 

507 

326  508 
\subsection{Forall introduction rules} 
509 
\index{metaquantifiers} 

104  510 
\begin{ttbox} 
3108  511 
forall_intr : cterm > thm > thm 
512 
forall_intr_list : cterm list > thm > thm 

513 
forall_intr_frees : thm > thm 

104  514 
\end{ttbox} 
515 

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

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

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

332  521 
variable (provided it does not occur in the assumptions). 
104  522 

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

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

525 

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

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

528 
of the premise. 

326  529 
\end{ttdescription} 
104  530 

531 

326  532 
\subsection{Forall elimination rules} 
104  533 
\begin{ttbox} 
3108  534 
forall_elim : cterm > thm > thm 
535 
forall_elim_list : cterm list > thm > thm 

536 
forall_elim_var : int > thm > thm 

537 
forall_elim_vars : int > thm > thm 

104  538 
\end{ttbox} 
539 

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

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

544 

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

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

547 

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

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

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

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

552 

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

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

326  555 
\end{ttdescription} 
104  556 

326  557 
\subsection{Instantiation of unknowns} 
558 
\index{instantiation} 

104  559 
\begin{ttbox} 
3108  560 
instantiate: (indexname * ctyp) list * (cterm * cterm) list > thm > thm 
104  561 
\end{ttbox} 
326  562 
\begin{ttdescription} 
563 
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 

564 
simultaneously substitutes types for type unknowns (the 

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

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

568 
must be distinct. The rule normalizes its conclusion. 

326  569 
\end{ttdescription} 
104  570 

571 

326  572 
\subsection{Freezing/thawing type unknowns} 
573 
\index{type unknowns!freezing/thawing of} 

104  574 
\begin{ttbox} 
575 
freezeT: thm > thm 

576 
varifyT: thm > thm 

577 
\end{ttbox} 

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

581 

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

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

326  584 
\end{ttdescription} 
104  585 

586 

587 
\section{Derived rules for goaldirected proof} 

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

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

590 

591 
\subsection{Proof by assumption} 

326  592 
\index{metaassumptions} 
104  593 
\begin{ttbox} 
594 
assumption : int > thm > thm Sequence.seq 

595 
eq_assumption : int > thm > thm 

596 
\end{ttbox} 

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

600 

601 
\item[\ttindexbold{eq_assumption}] 

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

326  603 
\end{ttdescription} 
104  604 

605 

606 
\subsection{Resolution} 

326  607 
\index{resolution} 
104  608 
\begin{ttbox} 
609 
biresolution : bool > (bool*thm)list > int > thm 

610 
> thm Sequence.seq 

611 
\end{ttbox} 

326  612 
\begin{ttdescription} 
104  613 
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$] 
326  614 
performs biresolution on subgoal~$i$ of $state$, using the list of $\it 
104  615 
(flag,rule)$ pairs. For each pair, it applies resolution if the flag 
616 
is~{\tt false} and elimresolution if the flag is~{\tt true}. If $match$ 

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

326  618 
\end{ttdescription} 
104  619 

620 

621 
\subsection{Composition: resolution without lifting} 

326  622 
\index{resolution!without lifting} 
104  623 
\begin{ttbox} 
624 
compose : thm * int * thm > thm list 

625 
COMP : thm * thm > thm 

626 
bicompose : bool > bool * thm * int > int > thm 

627 
> thm Sequence.seq 

628 
\end{ttbox} 

629 
In forward proof, a typical use of composition is to regard an assertion of 

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

631 
beware of clashes! 

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

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

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

637 
result list contains the theorem 

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

639 
\] 

640 

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

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

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

650 

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

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

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

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

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

326  658 
\end{ttdescription} 
104  659 

660 

661 
\subsection{Other metarules} 

662 
\begin{ttbox} 

3108  663 
trivial : cterm > thm 
104  664 
lift_rule : (thm * int) > thm > thm 
665 
rename_params_rule : string list * int > thm > thm 

3108  666 
rewrite_cterm : thm list > cterm > thm 
104  667 
flexflex_rule : thm > thm Sequence.seq 
668 
\end{ttbox} 

326  669 
\begin{ttdescription} 
104  670 
\item[\ttindexbold{trivial} $ct$] 
671 
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$. 

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

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

674 

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

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

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

678 

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

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

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

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

683 
ensure that all the parameters are distinct. 

684 
\index{parameters!renaming} 

685 

686 
\item[\ttindexbold{rewrite_cterm} $defs$ $ct$] 

687 
transforms $ct$ to $ct'$ by repeatedly applying $defs$ as rewrite rules; it 

688 
returns the conclusion~$ct\equiv ct'$. This underlies the metarewriting 

689 
tactics and rules. 

326  690 
\index{metarewriting!in terms} 
104  691 

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

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

326  694 
\end{ttdescription} 
1590  695 
\index{metarules)} 
696 

697 

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

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

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

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

704 
proofchecker, or used to generate humanreadable proof digests. 

705 

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

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

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

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

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

711 
theorem's dependencies. 

712 

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

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

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

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

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

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

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

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

721 
the {\tt Theorem} constructor. 

722 

723 
Proof objects are expressed using a polymorphic type of variablebranching 

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

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

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

727 
\begin{ttbox} 

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

729 
datatype rule = \(\ldots\); 

730 
type deriv = rule mtree; 

731 
\end{ttbox} 

732 
% 

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

734 
record: 

735 
\begin{ttbox} 

736 
#der (rep_thm conjI); 

3108  737 
{\out Join (Theorem "conjI", [Join (MinProof,[])]) : deriv} 
1590  738 
\end{ttbox} 
739 
This proof object identifies a labelled theorem, {\tt conjI}, whose underlying 

740 
proof has not been recorded; all we have is {\tt MinProof}. 

741 

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

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

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

745 
formats, linear or treestructured. 

746 

747 
\begin{ttbox} 

748 
keep_derivs : deriv_kind ref 

749 
Deriv.size : deriv > int 

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

751 
Deriv.linear : deriv > deriv list 

1876  752 
Deriv.tree : deriv > Deriv.orule mtree 
1590  753 
\end{ttbox} 
754 

755 
\begin{ttdescription} 

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

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

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

759 

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

761 
excluding lemmas. 

762 

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

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

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

766 

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

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

769 
reveals the singlestep Isabelle proof that is constructed internally by 

770 
tactics. 

771 

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

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

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

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

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

777 
\end{ttdescription} 

778 

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

779 
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

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

781 
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

782 
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

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

784 

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

785 

1590  786 
\index{proof objects)} 
104  787 
\index{theorems)} 