author | wenzelm |
Wed, 07 May 1997 17:21:24 +0200 | |
changeset 3135 | 233aba197bf2 |
parent 3108 | 335efc3f5632 |
child 3485 | f27a30a18a17 |
permissions | -rw-r--r-- |
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 |
object-logics, 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{Pretty-printing 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{meta-rewriting!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 meta-rules instantiate type and term unknowns in a theorem. They are |
|
143 |
occasionally useful. They can prevent difficulties with higher-order |
|
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 first-order 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 object-rules. It discharges all meta-assumptions, 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 destruct-resolution: {\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{flex-flex 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 flex-flex 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 flex-flex constraints, a |
|
243 |
list of the subgoals~1 to~$i-1$, 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 meta-assumptions ({\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 non-emptiness 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 --- so-called {\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 non-emptiness 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 |
non-emptiness 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 higher-order 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, higher-order 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 meta-level inference rules} |
|
326 |
\index{meta-rules|(} |
|
327 |
These implement the meta-logic 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 meta-rules raise exception \xdx{THM} to signal |
104 | 331 |
malformed premises, incompatible signatures and similar errors. |
332 |
||
326 | 333 |
\index{meta-assumptions} |
104 | 334 |
The meta-logic uses natural deduction. Each theorem may depend on |
332 | 335 |
meta-level 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 meta-level assumptions with the object-level |
|
343 |
assumptions in a subgoal, which are represented in the meta-logic |
|
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{meta-implication} |
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{meta-equality} |
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{meta-quantifiers} |
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{meta-assumptions} |
|
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{meta-implication} |
|
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{meta-equality} |
|
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{meta-equality} |
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{meta-quantifiers} |
|
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} |
3135 | 560 |
instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}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 goal-directed 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{meta-assumptions} |
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 bi-resolution 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 elim-resolution 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@{i-1}; \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 elim-resolution --- 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 meta-rules} |
|
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 goal-directed 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 meta-rewriting |
|
689 |
tactics and rules. |
|
326 | 690 |
\index{meta-rewriting!in terms} |
104 | 691 |
|
692 |
\item[\ttindexbold{flexflex_rule} $thm$] \index{flex-flex constraints} |
|
693 |
removes all flex-flex pairs from $thm$ using the trivial unifier. |
|
326 | 694 |
\end{ttdescription} |
1590 | 695 |
\index{meta-rules|)} |
696 |
||
697 |
||
1846 | 698 |
\section{Proof objects}\label{sec:proofObjects} |
1590 | 699 |
\index{proof objects|(} Isabelle can record the full meta-level 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 |
proof-checker, or used to generate human-readable 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 |
proof-checker: 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 variable-branching |
|
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 tree-structured. |
|
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 single-step Isabelle proof that is constructed internally by |
|
770 |
tactics. |
|
771 |
||
772 |
\item[\ttindexbold{Deriv.tree} $der$] converts a derivation into an |
|
773 |
object-level proof tree. A resolution by an object-rule is converted to a |
|
774 |
tree node labelled by that rule. Complications arise if the object-rule is |
|
775 |
itself derived in some way. Nested resolutions are unravelled, but other |
|
776 |
operations on rules (such as rewriting) are left as-is. |
|
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|)} |