lcp@104
|
1 |
%% $Id$
|
lcp@104
|
2 |
\chapter{Theorems and Forward Proof}
|
lcp@104
|
3 |
\index{theorems|(}
|
lcp@326
|
4 |
|
lcp@104
|
5 |
Theorems, which represent the axioms, theorems and rules of object-logics,
|
lcp@326
|
6 |
have type \mltydx{thm}. This chapter begins by describing operations that
|
lcp@326
|
7 |
print theorems and that join them in forward proof. Most theorem
|
lcp@326
|
8 |
operations are intended for advanced applications, such as programming new
|
lcp@326
|
9 |
proof procedures. Many of these operations refer to signatures, certified
|
lcp@326
|
10 |
terms and certified types, which have the \ML{} types {\tt Sign.sg}, {\tt
|
lcp@326
|
11 |
Sign.cterm} and {\tt Sign.ctyp} and are discussed in
|
lcp@104
|
12 |
Chapter~\ref{theories}. Beginning users should ignore such complexities
|
lcp@104
|
13 |
--- and skip all but the first section of this chapter.
|
lcp@104
|
14 |
|
lcp@104
|
15 |
The theorem operations do not print error messages. Instead, they raise
|
lcp@326
|
16 |
exception~\xdx{THM}\@. Use \ttindex{print_exn} to display
|
lcp@104
|
17 |
exceptions nicely:
|
lcp@104
|
18 |
\begin{ttbox}
|
lcp@104
|
19 |
allI RS mp handle e => print_exn e;
|
lcp@104
|
20 |
{\out Exception THM raised:}
|
lcp@104
|
21 |
{\out RSN: no unifiers -- premise 1}
|
lcp@104
|
22 |
{\out (!!x. ?P(x)) ==> ALL x. ?P(x)}
|
lcp@104
|
23 |
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
|
lcp@104
|
24 |
{\out}
|
lcp@104
|
25 |
{\out uncaught exception THM}
|
lcp@104
|
26 |
\end{ttbox}
|
lcp@104
|
27 |
|
lcp@104
|
28 |
|
lcp@104
|
29 |
\section{Basic operations on theorems}
|
lcp@104
|
30 |
\subsection{Pretty-printing a theorem}
|
lcp@326
|
31 |
\index{theorems!printing of}
|
lcp@104
|
32 |
\begin{ttbox}
|
lcp@326
|
33 |
prth : thm -> thm
|
lcp@326
|
34 |
prths : thm list -> thm list
|
lcp@326
|
35 |
prthq : thm Sequence.seq -> thm Sequence.seq
|
lcp@326
|
36 |
print_thm : thm -> unit
|
lcp@326
|
37 |
print_goals : int -> thm -> unit
|
lcp@326
|
38 |
string_of_thm : thm -> string
|
lcp@104
|
39 |
\end{ttbox}
|
lcp@326
|
40 |
The first three commands are for interactive use. They are identity
|
lcp@326
|
41 |
functions that display, then return, their argument. The \ML{} identifier
|
lcp@326
|
42 |
{\tt it} will refer to the value just displayed.
|
lcp@326
|
43 |
|
lcp@326
|
44 |
The others are for use in programs. Functions with result type {\tt unit}
|
lcp@326
|
45 |
are convenient for imperative programming.
|
lcp@326
|
46 |
|
lcp@326
|
47 |
\begin{ttdescription}
|
lcp@104
|
48 |
\item[\ttindexbold{prth} {\it thm}]
|
lcp@104
|
49 |
prints {\it thm\/} at the terminal.
|
lcp@104
|
50 |
|
lcp@104
|
51 |
\item[\ttindexbold{prths} {\it thms}]
|
lcp@104
|
52 |
prints {\it thms}, a list of theorems.
|
lcp@104
|
53 |
|
lcp@104
|
54 |
\item[\ttindexbold{prthq} {\it thmq}]
|
lcp@104
|
55 |
prints {\it thmq}, a sequence of theorems. It is useful for inspecting
|
lcp@104
|
56 |
the output of a tactic.
|
lcp@104
|
57 |
|
lcp@104
|
58 |
\item[\ttindexbold{print_thm} {\it thm}]
|
lcp@104
|
59 |
prints {\it thm\/} at the terminal.
|
lcp@104
|
60 |
|
lcp@104
|
61 |
\item[\ttindexbold{print_goals} {\it limit\/} {\it thm}]
|
lcp@104
|
62 |
prints {\it thm\/} in goal style, with the premises as subgoals. It prints
|
lcp@104
|
63 |
at most {\it limit\/} subgoals. The subgoal module calls {\tt print_goals}
|
lcp@104
|
64 |
to display proof states.
|
lcp@104
|
65 |
|
lcp@104
|
66 |
\item[\ttindexbold{string_of_thm} {\it thm}]
|
lcp@104
|
67 |
converts {\it thm\/} to a string.
|
lcp@326
|
68 |
\end{ttdescription}
|
lcp@104
|
69 |
|
lcp@104
|
70 |
|
lcp@326
|
71 |
\subsection{Forward proof: joining rules by resolution}
|
lcp@326
|
72 |
\index{theorems!joining by resolution}
|
lcp@326
|
73 |
\index{resolution}\index{forward proof}
|
lcp@104
|
74 |
\begin{ttbox}
|
lcp@104
|
75 |
RSN : thm * (int * thm) -> thm \hfill{\bf infix}
|
lcp@104
|
76 |
RS : thm * thm -> thm \hfill{\bf infix}
|
lcp@104
|
77 |
MRS : thm list * thm -> thm \hfill{\bf infix}
|
lcp@104
|
78 |
RLN : thm list * (int * thm list) -> thm list \hfill{\bf infix}
|
lcp@104
|
79 |
RL : thm list * thm list -> thm list \hfill{\bf infix}
|
lcp@326
|
80 |
MRL : thm list list * thm list -> thm list \hfill{\bf infix}
|
lcp@104
|
81 |
\end{ttbox}
|
lcp@326
|
82 |
Joining rules together is a simple way of deriving new rules. These
|
lcp@876
|
83 |
functions are especially useful with destruction rules. To store
|
lcp@876
|
84 |
the result in the theorem database, use \ttindex{bind_thm}
|
lcp@876
|
85 |
(\S\ref{ExtractingAndStoringTheProvedTheorem}).
|
lcp@326
|
86 |
\begin{ttdescription}
|
lcp@104
|
87 |
\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN}
|
lcp@326
|
88 |
resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.
|
lcp@326
|
89 |
Unless there is precisely one resolvent it raises exception
|
lcp@326
|
90 |
\xdx{THM}; in that case, use {\tt RLN}.
|
lcp@104
|
91 |
|
lcp@104
|
92 |
\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS}
|
lcp@104
|
93 |
abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}. Thus, it resolves the
|
lcp@104
|
94 |
conclusion of $thm@1$ with the first premise of~$thm@2$.
|
lcp@104
|
95 |
|
lcp@104
|
96 |
\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS}
|
lcp@332
|
97 |
uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
|
lcp@104
|
98 |
$i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$
|
lcp@104
|
99 |
premises of $thm$. Because the theorems are used from right to left, it
|
lcp@104
|
100 |
does not matter if the $thm@i$ create new premises. {\tt MRS} is useful
|
lcp@104
|
101 |
for expressing proof trees.
|
lcp@104
|
102 |
|
wenzelm@151
|
103 |
\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN}
|
lcp@326
|
104 |
joins lists of theorems. For every $thm@1$ in $thms@1$ and $thm@2$ in
|
lcp@326
|
105 |
$thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise
|
lcp@326
|
106 |
of~$thm@2$, accumulating the results.
|
lcp@104
|
107 |
|
wenzelm@151
|
108 |
\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL}
|
wenzelm@151
|
109 |
abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}.
|
lcp@104
|
110 |
|
lcp@104
|
111 |
\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL}
|
lcp@104
|
112 |
is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
|
lcp@104
|
113 |
It too is useful for expressing proof trees.
|
lcp@326
|
114 |
\end{ttdescription}
|
lcp@104
|
115 |
|
lcp@104
|
116 |
|
lcp@104
|
117 |
\subsection{Expanding definitions in theorems}
|
lcp@326
|
118 |
\index{meta-rewriting!in theorems}
|
lcp@104
|
119 |
\begin{ttbox}
|
lcp@104
|
120 |
rewrite_rule : thm list -> thm -> thm
|
lcp@104
|
121 |
rewrite_goals_rule : thm list -> thm -> thm
|
lcp@104
|
122 |
\end{ttbox}
|
lcp@326
|
123 |
\begin{ttdescription}
|
lcp@104
|
124 |
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]
|
lcp@104
|
125 |
unfolds the {\it defs} throughout the theorem~{\it thm}.
|
lcp@104
|
126 |
|
lcp@104
|
127 |
\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]
|
lcp@104
|
128 |
unfolds the {\it defs} in the premises of~{\it thm}, but leaves the
|
lcp@104
|
129 |
conclusion unchanged. This rule underlies \ttindex{rewrite_goals_tac}, but
|
lcp@104
|
130 |
serves little purpose in forward proof.
|
lcp@326
|
131 |
\end{ttdescription}
|
lcp@104
|
132 |
|
lcp@104
|
133 |
|
lcp@326
|
134 |
\subsection{Instantiating a theorem}
|
lcp@326
|
135 |
\index{instantiation}
|
lcp@286
|
136 |
\begin{ttbox}
|
lcp@104
|
137 |
read_instantiate : (string*string)list -> thm -> thm
|
lcp@104
|
138 |
read_instantiate_sg : Sign.sg -> (string*string)list -> thm -> thm
|
lcp@104
|
139 |
cterm_instantiate : (Sign.cterm*Sign.cterm)list -> thm -> thm
|
lcp@104
|
140 |
\end{ttbox}
|
lcp@104
|
141 |
These meta-rules instantiate type and term unknowns in a theorem. They are
|
lcp@104
|
142 |
occasionally useful. They can prevent difficulties with higher-order
|
lcp@104
|
143 |
unification, and define specialized versions of rules.
|
lcp@326
|
144 |
\begin{ttdescription}
|
lcp@104
|
145 |
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}]
|
lcp@104
|
146 |
processes the instantiations {\it insts} and instantiates the rule~{\it
|
lcp@104
|
147 |
thm}. The processing of instantiations is described
|
lcp@326
|
148 |
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}.
|
lcp@104
|
149 |
|
lcp@104
|
150 |
Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
|
lcp@104
|
151 |
and refine a particular subgoal. The tactic allows instantiation by the
|
lcp@104
|
152 |
subgoal's parameters, and reads the instantiations using the signature
|
lcp@326
|
153 |
associated with the proof state.
|
lcp@104
|
154 |
|
lcp@326
|
155 |
Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated
|
lcp@326
|
156 |
incorrectly.
|
lcp@326
|
157 |
|
lcp@326
|
158 |
\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
|
lcp@326
|
159 |
resembles \hbox{\tt read_instantiate {\it insts} {\it thm}}, but reads
|
lcp@326
|
160 |
the instantiations under signature~{\it sg}. This is necessary to
|
lcp@326
|
161 |
instantiate a rule from a general theory, such as first-order logic,
|
lcp@326
|
162 |
using the notation of some specialized theory. Use the function {\tt
|
lcp@326
|
163 |
sign_of} to get a theory's signature.
|
lcp@104
|
164 |
|
lcp@104
|
165 |
\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}]
|
lcp@104
|
166 |
is similar to {\tt read_instantiate}, but the instantiations are provided
|
lcp@104
|
167 |
as pairs of certified terms, not as strings to be read.
|
lcp@326
|
168 |
\end{ttdescription}
|
lcp@104
|
169 |
|
lcp@104
|
170 |
|
clasohm@866
|
171 |
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
|
lcp@326
|
172 |
\index{theorems!standardizing}
|
lcp@104
|
173 |
\begin{ttbox}
|
lcp@332
|
174 |
standard : thm -> thm
|
lcp@332
|
175 |
zero_var_indexes : thm -> thm
|
lcp@332
|
176 |
make_elim : thm -> thm
|
lcp@104
|
177 |
rule_by_tactic : tactic -> thm -> thm
|
lcp@104
|
178 |
\end{ttbox}
|
lcp@326
|
179 |
\begin{ttdescription}
|
lcp@104
|
180 |
\item[\ttindexbold{standard} $thm$]
|
lcp@104
|
181 |
puts $thm$ into the standard form of object-rules. It discharges all
|
lcp@332
|
182 |
meta-assumptions, replaces free variables by schematic variables, and
|
lcp@104
|
183 |
renames schematic variables to have subscript zero.
|
lcp@104
|
184 |
|
lcp@104
|
185 |
\item[\ttindexbold{zero_var_indexes} $thm$]
|
lcp@104
|
186 |
makes all schematic variables have subscript zero, renaming them to avoid
|
lcp@104
|
187 |
clashes.
|
lcp@104
|
188 |
|
lcp@104
|
189 |
\item[\ttindexbold{make_elim} $thm$]
|
lcp@104
|
190 |
\index{rules!converting destruction to elimination}
|
lcp@104
|
191 |
converts $thm$, a destruction rule of the form $\List{P@1;\ldots;P@m}\Imp
|
lcp@104
|
192 |
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This
|
lcp@104
|
193 |
is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
|
lcp@104
|
194 |
|
lcp@104
|
195 |
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}]
|
lcp@104
|
196 |
applies {\it tac\/} to the {\it thm}, freezing its variables first, then
|
lcp@104
|
197 |
yields the proof state returned by the tactic. In typical usage, the
|
lcp@104
|
198 |
{\it thm\/} represents an instance of a rule with several premises, some
|
lcp@104
|
199 |
with contradictory assumptions (because of the instantiation). The
|
lcp@104
|
200 |
tactic proves those subgoals and does whatever else it can, and returns
|
lcp@104
|
201 |
whatever is left.
|
lcp@326
|
202 |
\end{ttdescription}
|
lcp@104
|
203 |
|
lcp@104
|
204 |
|
lcp@104
|
205 |
\subsection{Taking a theorem apart}
|
lcp@326
|
206 |
\index{theorems!taking apart}
|
lcp@104
|
207 |
\index{flex-flex constraints}
|
lcp@104
|
208 |
\begin{ttbox}
|
lcp@104
|
209 |
concl_of : thm -> term
|
lcp@104
|
210 |
prems_of : thm -> term list
|
lcp@104
|
211 |
nprems_of : thm -> int
|
lcp@104
|
212 |
tpairs_of : thm -> (term*term)list
|
lcp@104
|
213 |
stamps_of_thy : thm -> string ref list
|
clasohm@866
|
214 |
theory_of_thm : thm -> theory
|
lcp@286
|
215 |
dest_state : thm*int -> (term*term)list*term list*term*term
|
paulson@2040
|
216 |
rep_thm : thm -> \{prop: term, hyps: term list, der: deriv,
|
paulson@2040
|
217 |
maxidx: int, sign: Sign.sg, shyps: sort list\}
|
lcp@104
|
218 |
\end{ttbox}
|
lcp@326
|
219 |
\begin{ttdescription}
|
lcp@104
|
220 |
\item[\ttindexbold{concl_of} $thm$]
|
lcp@104
|
221 |
returns the conclusion of $thm$ as a term.
|
lcp@104
|
222 |
|
lcp@104
|
223 |
\item[\ttindexbold{prems_of} $thm$]
|
lcp@104
|
224 |
returns the premises of $thm$ as a list of terms.
|
lcp@104
|
225 |
|
lcp@104
|
226 |
\item[\ttindexbold{nprems_of} $thm$]
|
lcp@286
|
227 |
returns the number of premises in $thm$, and is equivalent to {\tt
|
lcp@286
|
228 |
length(prems_of~$thm$)}.
|
lcp@104
|
229 |
|
lcp@104
|
230 |
\item[\ttindexbold{tpairs_of} $thm$]
|
lcp@104
|
231 |
returns the flex-flex constraints of $thm$.
|
lcp@104
|
232 |
|
lcp@104
|
233 |
\item[\ttindexbold{stamps_of_thm} $thm$]
|
lcp@332
|
234 |
returns the \rmindex{stamps} of the signature associated with~$thm$.
|
lcp@104
|
235 |
|
clasohm@866
|
236 |
\item[\ttindexbold{theory_of_thm} $thm$]
|
clasohm@866
|
237 |
returns the theory associated with $thm$.
|
clasohm@866
|
238 |
|
lcp@104
|
239 |
\item[\ttindexbold{dest_state} $(thm,i)$]
|
lcp@104
|
240 |
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
|
lcp@104
|
241 |
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
|
lcp@104
|
242 |
(this will be an implication if there are more than $i$ subgoals).
|
lcp@104
|
243 |
|
paulson@2040
|
244 |
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record containing the
|
paulson@2040
|
245 |
statement of~$thm$ ({\tt prop}), its list of meta-assumptions ({\tt hyps}),
|
paulson@2040
|
246 |
its derivation ({\tt der}), a bound on the maximum subscript of its
|
paulson@2040
|
247 |
unknowns ({\tt maxidx}), and its signature ({\tt sign}). The {\tt shyps}
|
paulson@2040
|
248 |
field is discussed below.
|
lcp@326
|
249 |
\end{ttdescription}
|
lcp@104
|
250 |
|
lcp@104
|
251 |
|
paulson@2040
|
252 |
\subsection{*Sort hypotheses}
|
paulson@2040
|
253 |
\index{sort hypotheses}
|
paulson@2040
|
254 |
\begin{ttbox}
|
paulson@2040
|
255 |
force_strip_shyps : bool ref \hfill{\bf initially true}
|
paulson@2040
|
256 |
\end{ttbox}
|
paulson@2040
|
257 |
|
paulson@2040
|
258 |
\begin{ttdescription}
|
paulson@2040
|
259 |
\item[\ttindexbold{force_strip_shyps}]
|
paulson@2040
|
260 |
causes sort hypotheses to be deleted, printing a warning.
|
paulson@2040
|
261 |
\end{ttdescription}
|
paulson@2040
|
262 |
|
paulson@2040
|
263 |
A sort is {\em empty\/} if there are no types having that sort. If a theorem
|
paulson@2040
|
264 |
contain a type variable whose sort is empty, then that theorem has no
|
paulson@2040
|
265 |
instances. In effect, it asserts nothing. But what if it is used to prove
|
paulson@2040
|
266 |
another theorem that no longer involves that sort? The latter theorem holds
|
paulson@2040
|
267 |
only if the sort is non-empty.
|
paulson@2040
|
268 |
|
paulson@2040
|
269 |
Theorems are therefore subject to sort hypotheses, which express that certain
|
paulson@2040
|
270 |
sorts are non-empty. The {\tt shyps} field is a list of sorts occurring in
|
paulson@2040
|
271 |
type variables. The list includes all sorts from the current theorem (the
|
paulson@2040
|
272 |
{\tt prop} and {\tt hyps} fields). It also includes sorts used in the
|
paulson@2040
|
273 |
theorem's proof --- so-called {\em dangling\/} sort constraints. These are
|
paulson@2040
|
274 |
the critical ones that must be non-empty in order for the proof to be valid.
|
paulson@2040
|
275 |
|
paulson@2040
|
276 |
Isabelle removes sorts from the {\tt shyps} field whenever
|
paulson@2040
|
277 |
non-emptiness holds. Because its current implementation is highly incomplete,
|
paulson@2040
|
278 |
the flag shown above is available. Setting it to true (the default) allows
|
paulson@2040
|
279 |
existing proofs to run.
|
paulson@2040
|
280 |
|
paulson@2040
|
281 |
|
lcp@104
|
282 |
\subsection{Tracing flags for unification}
|
lcp@326
|
283 |
\index{tracing!of unification}
|
lcp@104
|
284 |
\begin{ttbox}
|
lcp@104
|
285 |
Unify.trace_simp : bool ref \hfill{\bf initially false}
|
lcp@104
|
286 |
Unify.trace_types : bool ref \hfill{\bf initially false}
|
lcp@104
|
287 |
Unify.trace_bound : int ref \hfill{\bf initially 10}
|
lcp@104
|
288 |
Unify.search_bound : int ref \hfill{\bf initially 20}
|
lcp@104
|
289 |
\end{ttbox}
|
lcp@104
|
290 |
Tracing the search may be useful when higher-order unification behaves
|
lcp@104
|
291 |
unexpectedly. Letting {\tt res_inst_tac} circumvent the problem is easier,
|
lcp@104
|
292 |
though.
|
lcp@326
|
293 |
\begin{ttdescription}
|
lcp@326
|
294 |
\item[Unify.trace_simp := true;]
|
lcp@104
|
295 |
causes tracing of the simplification phase.
|
lcp@104
|
296 |
|
lcp@326
|
297 |
\item[Unify.trace_types := true;]
|
lcp@104
|
298 |
generates warnings of incompleteness, when unification is not considering
|
lcp@104
|
299 |
all possible instantiations of type unknowns.
|
lcp@104
|
300 |
|
lcp@326
|
301 |
\item[Unify.trace_bound := $n$;]
|
lcp@104
|
302 |
causes unification to print tracing information once it reaches depth~$n$.
|
lcp@104
|
303 |
Use $n=0$ for full tracing. At the default value of~10, tracing
|
lcp@104
|
304 |
information is almost never printed.
|
lcp@104
|
305 |
|
lcp@326
|
306 |
\item[Unify.search_bound := $n$;]
|
lcp@104
|
307 |
causes unification to limit its search to depth~$n$. Because of this
|
lcp@104
|
308 |
bound, higher-order unification cannot return an infinite sequence, though
|
lcp@104
|
309 |
it can return a very long one. The search rarely approaches the default
|
lcp@104
|
310 |
value of~20. If the search is cut off, unification prints {\tt
|
lcp@104
|
311 |
***Unification bound exceeded}.
|
lcp@326
|
312 |
\end{ttdescription}
|
lcp@104
|
313 |
|
lcp@104
|
314 |
|
lcp@104
|
315 |
\section{Primitive meta-level inference rules}
|
lcp@104
|
316 |
\index{meta-rules|(}
|
lcp@104
|
317 |
These implement the meta-logic in {\sc lcf} style, as functions from theorems
|
lcp@104
|
318 |
to theorems. They are, rarely, useful for deriving results in the pure
|
lcp@104
|
319 |
theory. Mainly, they are included for completeness, and most users should
|
lcp@326
|
320 |
not bother with them. The meta-rules raise exception \xdx{THM} to signal
|
lcp@104
|
321 |
malformed premises, incompatible signatures and similar errors.
|
lcp@104
|
322 |
|
lcp@326
|
323 |
\index{meta-assumptions}
|
lcp@104
|
324 |
The meta-logic uses natural deduction. Each theorem may depend on
|
lcp@332
|
325 |
meta-level assumptions. Certain rules, such as $({\Imp}I)$,
|
lcp@104
|
326 |
discharge assumptions; in most other rules, the conclusion depends on all
|
lcp@104
|
327 |
of the assumptions of the premises. Formally, the system works with
|
lcp@104
|
328 |
assertions of the form
|
lcp@104
|
329 |
\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
|
lcp@332
|
330 |
where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions. Do not confuse
|
lcp@104
|
331 |
meta-level assumptions with the object-level assumptions in a subgoal,
|
lcp@104
|
332 |
which are represented in the meta-logic using~$\Imp$.
|
lcp@104
|
333 |
|
lcp@104
|
334 |
Each theorem has a signature. Certified terms have a signature. When a
|
lcp@104
|
335 |
rule takes several premises and certified terms, it merges the signatures
|
lcp@104
|
336 |
to make a signature for the conclusion. This fails if the signatures are
|
lcp@104
|
337 |
incompatible.
|
lcp@104
|
338 |
|
lcp@326
|
339 |
\index{meta-implication}
|
lcp@332
|
340 |
The {\bf implication} rules are $({\Imp}I)$
|
lcp@104
|
341 |
and $({\Imp}E)$:
|
lcp@104
|
342 |
\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad
|
lcp@104
|
343 |
\infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi} \]
|
lcp@104
|
344 |
|
lcp@326
|
345 |
\index{meta-equality}
|
lcp@104
|
346 |
Equality of truth values means logical equivalence:
|
lcp@104
|
347 |
\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} &
|
lcp@286
|
348 |
\infer*{\phi}{[\psi]}}
|
lcp@104
|
349 |
\qquad
|
lcp@104
|
350 |
\infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \]
|
lcp@104
|
351 |
|
lcp@332
|
352 |
The {\bf equality} rules are reflexivity, symmetry, and transitivity:
|
lcp@104
|
353 |
\[ {a\equiv a}\,(refl) \qquad
|
lcp@104
|
354 |
\infer[(sym)]{b\equiv a}{a\equiv b} \qquad
|
lcp@104
|
355 |
\infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c} \]
|
lcp@104
|
356 |
|
lcp@326
|
357 |
\index{lambda calc@$\lambda$-calculus}
|
lcp@104
|
358 |
The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
|
lcp@104
|
359 |
extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
|
lcp@104
|
360 |
in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
|
lcp@104
|
361 |
\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])} \qquad
|
lcp@104
|
362 |
{((\lambda x.a)(b)) \equiv a[b/x]} \qquad
|
lcp@104
|
363 |
\infer[(ext)]{f\equiv g}{f(x) \equiv g(x)} \]
|
lcp@104
|
364 |
|
lcp@332
|
365 |
The {\bf abstraction} and {\bf combination} rules let conversions be
|
lcp@332
|
366 |
applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
|
lcp@104
|
367 |
assumptions.}
|
lcp@104
|
368 |
\[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad
|
lcp@104
|
369 |
\infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b} \]
|
lcp@104
|
370 |
|
lcp@326
|
371 |
\index{meta-quantifiers}
|
lcp@332
|
372 |
The {\bf universal quantification} rules are $(\Forall I)$ and $(\Forall
|
lcp@104
|
373 |
E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
|
lcp@104
|
374 |
\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad
|
lcp@286
|
375 |
\infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi} \]
|
lcp@104
|
376 |
|
lcp@104
|
377 |
|
lcp@326
|
378 |
\subsection{Assumption rule}
|
lcp@326
|
379 |
\index{meta-assumptions}
|
lcp@104
|
380 |
\begin{ttbox}
|
lcp@104
|
381 |
assume: Sign.cterm -> thm
|
lcp@104
|
382 |
\end{ttbox}
|
lcp@326
|
383 |
\begin{ttdescription}
|
lcp@104
|
384 |
\item[\ttindexbold{assume} $ct$]
|
lcp@332
|
385 |
makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
|
lcp@104
|
386 |
The rule checks that $ct$ has type $prop$ and contains no unknowns, which
|
lcp@332
|
387 |
are not allowed in assumptions.
|
lcp@326
|
388 |
\end{ttdescription}
|
lcp@104
|
389 |
|
lcp@326
|
390 |
\subsection{Implication rules}
|
lcp@326
|
391 |
\index{meta-implication}
|
lcp@104
|
392 |
\begin{ttbox}
|
lcp@104
|
393 |
implies_intr : Sign.cterm -> thm -> thm
|
lcp@104
|
394 |
implies_intr_list : Sign.cterm list -> thm -> thm
|
lcp@104
|
395 |
implies_intr_hyps : thm -> thm
|
lcp@104
|
396 |
implies_elim : thm -> thm -> thm
|
lcp@104
|
397 |
implies_elim_list : thm -> thm list -> thm
|
lcp@104
|
398 |
\end{ttbox}
|
lcp@326
|
399 |
\begin{ttdescription}
|
lcp@104
|
400 |
\item[\ttindexbold{implies_intr} $ct$ $thm$]
|
lcp@104
|
401 |
is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$. It
|
lcp@332
|
402 |
maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
|
lcp@332
|
403 |
occurrences of~$\phi$ from the assumptions. The rule checks that $ct$ has
|
lcp@332
|
404 |
type $prop$.
|
lcp@104
|
405 |
|
lcp@104
|
406 |
\item[\ttindexbold{implies_intr_list} $cts$ $thm$]
|
lcp@104
|
407 |
applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
|
lcp@104
|
408 |
|
lcp@104
|
409 |
\item[\ttindexbold{implies_intr_hyps} $thm$]
|
lcp@332
|
410 |
applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
|
lcp@332
|
411 |
It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
|
lcp@104
|
412 |
$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
|
lcp@104
|
413 |
|
lcp@104
|
414 |
\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$]
|
lcp@104
|
415 |
applies $({\Imp}E)$ to $thm@1$ and~$thm@2$. It maps the premises $\phi\Imp
|
lcp@104
|
416 |
\psi$ and $\phi$ to the conclusion~$\psi$.
|
lcp@104
|
417 |
|
lcp@104
|
418 |
\item[\ttindexbold{implies_elim_list} $thm$ $thms$]
|
lcp@104
|
419 |
applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
|
wenzelm@151
|
420 |
turn. It maps the premises $\List{\phi@1,\ldots,\phi@n}\Imp\psi$ and
|
lcp@104
|
421 |
$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
|
lcp@326
|
422 |
\end{ttdescription}
|
lcp@104
|
423 |
|
lcp@326
|
424 |
\subsection{Logical equivalence rules}
|
lcp@326
|
425 |
\index{meta-equality}
|
lcp@104
|
426 |
\begin{ttbox}
|
lcp@326
|
427 |
equal_intr : thm -> thm -> thm
|
lcp@326
|
428 |
equal_elim : thm -> thm -> thm
|
lcp@104
|
429 |
\end{ttbox}
|
lcp@326
|
430 |
\begin{ttdescription}
|
lcp@104
|
431 |
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
|
lcp@332
|
432 |
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$
|
lcp@332
|
433 |
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
|
lcp@332
|
434 |
the first premise with~$\phi$ removed, plus those of
|
lcp@332
|
435 |
the second premise with~$\psi$ removed.
|
lcp@104
|
436 |
|
lcp@104
|
437 |
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
|
lcp@104
|
438 |
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
|
lcp@104
|
439 |
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
|
lcp@326
|
440 |
\end{ttdescription}
|
lcp@104
|
441 |
|
lcp@104
|
442 |
|
lcp@104
|
443 |
\subsection{Equality rules}
|
lcp@326
|
444 |
\index{meta-equality}
|
lcp@104
|
445 |
\begin{ttbox}
|
lcp@104
|
446 |
reflexive : Sign.cterm -> thm
|
lcp@104
|
447 |
symmetric : thm -> thm
|
lcp@104
|
448 |
transitive : thm -> thm -> thm
|
lcp@104
|
449 |
\end{ttbox}
|
lcp@326
|
450 |
\begin{ttdescription}
|
lcp@104
|
451 |
\item[\ttindexbold{reflexive} $ct$]
|
wenzelm@151
|
452 |
makes the theorem \(ct\equiv ct\).
|
lcp@104
|
453 |
|
lcp@104
|
454 |
\item[\ttindexbold{symmetric} $thm$]
|
lcp@104
|
455 |
maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
|
lcp@104
|
456 |
|
lcp@104
|
457 |
\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
|
lcp@104
|
458 |
maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
|
lcp@326
|
459 |
\end{ttdescription}
|
lcp@104
|
460 |
|
lcp@104
|
461 |
|
lcp@104
|
462 |
\subsection{The $\lambda$-conversion rules}
|
lcp@326
|
463 |
\index{lambda calc@$\lambda$-calculus}
|
lcp@104
|
464 |
\begin{ttbox}
|
lcp@104
|
465 |
beta_conversion : Sign.cterm -> thm
|
lcp@104
|
466 |
extensional : thm -> thm
|
lcp@104
|
467 |
abstract_rule : string -> Sign.cterm -> thm -> thm
|
lcp@104
|
468 |
combination : thm -> thm -> thm
|
lcp@104
|
469 |
\end{ttbox}
|
lcp@326
|
470 |
There is no rule for $\alpha$-conversion because Isabelle regards
|
lcp@326
|
471 |
$\alpha$-convertible theorems as equal.
|
lcp@326
|
472 |
\begin{ttdescription}
|
lcp@104
|
473 |
\item[\ttindexbold{beta_conversion} $ct$]
|
lcp@104
|
474 |
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
|
lcp@104
|
475 |
term $(\lambda x.a)(b)$.
|
lcp@104
|
476 |
|
lcp@104
|
477 |
\item[\ttindexbold{extensional} $thm$]
|
lcp@104
|
478 |
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
|
lcp@104
|
479 |
Parameter~$x$ is taken from the premise. It may be an unknown or a free
|
lcp@332
|
480 |
variable (provided it does not occur in the assumptions); it must not occur
|
lcp@104
|
481 |
in $f$ or~$g$.
|
lcp@104
|
482 |
|
lcp@104
|
483 |
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
|
lcp@104
|
484 |
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
|
lcp@104
|
485 |
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
|
lcp@104
|
486 |
Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
|
lcp@332
|
487 |
variable (provided it does not occur in the assumptions). In the
|
lcp@104
|
488 |
conclusion, the bound variable is named~$v$.
|
lcp@104
|
489 |
|
lcp@104
|
490 |
\item[\ttindexbold{combination} $thm@1$ $thm@2$]
|
lcp@104
|
491 |
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
|
lcp@104
|
492 |
g(b)$.
|
lcp@326
|
493 |
\end{ttdescription}
|
lcp@104
|
494 |
|
lcp@104
|
495 |
|
lcp@326
|
496 |
\subsection{Forall introduction rules}
|
lcp@326
|
497 |
\index{meta-quantifiers}
|
lcp@104
|
498 |
\begin{ttbox}
|
lcp@104
|
499 |
forall_intr : Sign.cterm -> thm -> thm
|
lcp@104
|
500 |
forall_intr_list : Sign.cterm list -> thm -> thm
|
lcp@104
|
501 |
forall_intr_frees : thm -> thm
|
lcp@104
|
502 |
\end{ttbox}
|
lcp@104
|
503 |
|
lcp@326
|
504 |
\begin{ttdescription}
|
lcp@104
|
505 |
\item[\ttindexbold{forall_intr} $x$ $thm$]
|
lcp@104
|
506 |
applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
|
lcp@104
|
507 |
The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
|
lcp@104
|
508 |
Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
|
lcp@332
|
509 |
variable (provided it does not occur in the assumptions).
|
lcp@104
|
510 |
|
lcp@104
|
511 |
\item[\ttindexbold{forall_intr_list} $xs$ $thm$]
|
lcp@104
|
512 |
applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
|
lcp@104
|
513 |
|
lcp@104
|
514 |
\item[\ttindexbold{forall_intr_frees} $thm$]
|
lcp@104
|
515 |
applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
|
lcp@104
|
516 |
of the premise.
|
lcp@326
|
517 |
\end{ttdescription}
|
lcp@104
|
518 |
|
lcp@104
|
519 |
|
lcp@326
|
520 |
\subsection{Forall elimination rules}
|
lcp@104
|
521 |
\begin{ttbox}
|
lcp@104
|
522 |
forall_elim : Sign.cterm -> thm -> thm
|
lcp@104
|
523 |
forall_elim_list : Sign.cterm list -> thm -> thm
|
lcp@104
|
524 |
forall_elim_var : int -> thm -> thm
|
lcp@104
|
525 |
forall_elim_vars : int -> thm -> thm
|
lcp@104
|
526 |
\end{ttbox}
|
lcp@104
|
527 |
|
lcp@326
|
528 |
\begin{ttdescription}
|
lcp@104
|
529 |
\item[\ttindexbold{forall_elim} $ct$ $thm$]
|
lcp@104
|
530 |
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
|
lcp@104
|
531 |
$\phi[ct/x]$. The rule checks that $ct$ and $x$ have the same type.
|
lcp@104
|
532 |
|
lcp@104
|
533 |
\item[\ttindexbold{forall_elim_list} $cts$ $thm$]
|
lcp@104
|
534 |
applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
|
lcp@104
|
535 |
|
lcp@104
|
536 |
\item[\ttindexbold{forall_elim_var} $k$ $thm$]
|
lcp@104
|
537 |
applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
|
lcp@104
|
538 |
$\phi[\Var{x@k}/x]$. Thus, it replaces the outermost $\Forall$-bound
|
lcp@104
|
539 |
variable by an unknown having subscript~$k$.
|
lcp@104
|
540 |
|
lcp@104
|
541 |
\item[\ttindexbold{forall_elim_vars} $ks$ $thm$]
|
lcp@104
|
542 |
applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
|
lcp@326
|
543 |
\end{ttdescription}
|
lcp@104
|
544 |
|
lcp@326
|
545 |
\subsection{Instantiation of unknowns}
|
lcp@326
|
546 |
\index{instantiation}
|
lcp@104
|
547 |
\begin{ttbox}
|
lcp@286
|
548 |
instantiate: (indexname*Sign.ctyp)list *
|
lcp@286
|
549 |
(Sign.cterm*Sign.cterm)list -> thm -> thm
|
lcp@104
|
550 |
\end{ttbox}
|
lcp@326
|
551 |
\begin{ttdescription}
|
lcp@326
|
552 |
\item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$]
|
lcp@326
|
553 |
simultaneously substitutes types for type unknowns (the
|
lcp@104
|
554 |
$tyinsts$) and terms for term unknowns (the $insts$). Instantiations are
|
lcp@104
|
555 |
given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
|
lcp@104
|
556 |
same type as $v$) or a type (of the same sort as~$v$). All the unknowns
|
lcp@104
|
557 |
must be distinct. The rule normalizes its conclusion.
|
lcp@326
|
558 |
\end{ttdescription}
|
lcp@104
|
559 |
|
lcp@104
|
560 |
|
lcp@326
|
561 |
\subsection{Freezing/thawing type unknowns}
|
lcp@326
|
562 |
\index{type unknowns!freezing/thawing of}
|
lcp@104
|
563 |
\begin{ttbox}
|
lcp@104
|
564 |
freezeT: thm -> thm
|
lcp@104
|
565 |
varifyT: thm -> thm
|
lcp@104
|
566 |
\end{ttbox}
|
lcp@326
|
567 |
\begin{ttdescription}
|
lcp@104
|
568 |
\item[\ttindexbold{freezeT} $thm$]
|
lcp@104
|
569 |
converts all the type unknowns in $thm$ to free type variables.
|
lcp@104
|
570 |
|
lcp@104
|
571 |
\item[\ttindexbold{varifyT} $thm$]
|
lcp@104
|
572 |
converts all the free type variables in $thm$ to type unknowns.
|
lcp@326
|
573 |
\end{ttdescription}
|
lcp@104
|
574 |
|
lcp@104
|
575 |
|
lcp@104
|
576 |
\section{Derived rules for goal-directed proof}
|
lcp@104
|
577 |
Most of these rules have the sole purpose of implementing particular
|
lcp@104
|
578 |
tactics. There are few occasions for applying them directly to a theorem.
|
lcp@104
|
579 |
|
lcp@104
|
580 |
\subsection{Proof by assumption}
|
lcp@326
|
581 |
\index{meta-assumptions}
|
lcp@104
|
582 |
\begin{ttbox}
|
lcp@104
|
583 |
assumption : int -> thm -> thm Sequence.seq
|
lcp@104
|
584 |
eq_assumption : int -> thm -> thm
|
lcp@104
|
585 |
\end{ttbox}
|
lcp@326
|
586 |
\begin{ttdescription}
|
lcp@104
|
587 |
\item[\ttindexbold{assumption} {\it i} $thm$]
|
lcp@104
|
588 |
attempts to solve premise~$i$ of~$thm$ by assumption.
|
lcp@104
|
589 |
|
lcp@104
|
590 |
\item[\ttindexbold{eq_assumption}]
|
lcp@104
|
591 |
is like {\tt assumption} but does not use unification.
|
lcp@326
|
592 |
\end{ttdescription}
|
lcp@104
|
593 |
|
lcp@104
|
594 |
|
lcp@104
|
595 |
\subsection{Resolution}
|
lcp@326
|
596 |
\index{resolution}
|
lcp@104
|
597 |
\begin{ttbox}
|
lcp@104
|
598 |
biresolution : bool -> (bool*thm)list -> int -> thm
|
lcp@104
|
599 |
-> thm Sequence.seq
|
lcp@104
|
600 |
\end{ttbox}
|
lcp@326
|
601 |
\begin{ttdescription}
|
lcp@104
|
602 |
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$]
|
lcp@326
|
603 |
performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
|
lcp@104
|
604 |
(flag,rule)$ pairs. For each pair, it applies resolution if the flag
|
lcp@104
|
605 |
is~{\tt false} and elim-resolution if the flag is~{\tt true}. If $match$
|
lcp@104
|
606 |
is~{\tt true}, the $state$ is not instantiated.
|
lcp@326
|
607 |
\end{ttdescription}
|
lcp@104
|
608 |
|
lcp@104
|
609 |
|
lcp@104
|
610 |
\subsection{Composition: resolution without lifting}
|
lcp@326
|
611 |
\index{resolution!without lifting}
|
lcp@104
|
612 |
\begin{ttbox}
|
lcp@104
|
613 |
compose : thm * int * thm -> thm list
|
lcp@104
|
614 |
COMP : thm * thm -> thm
|
lcp@104
|
615 |
bicompose : bool -> bool * thm * int -> int -> thm
|
lcp@104
|
616 |
-> thm Sequence.seq
|
lcp@104
|
617 |
\end{ttbox}
|
lcp@104
|
618 |
In forward proof, a typical use of composition is to regard an assertion of
|
lcp@104
|
619 |
the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so
|
lcp@104
|
620 |
beware of clashes!
|
lcp@326
|
621 |
\begin{ttdescription}
|
lcp@104
|
622 |
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)]
|
lcp@104
|
623 |
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
|
lcp@104
|
624 |
of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
|
lcp@104
|
625 |
\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the
|
lcp@104
|
626 |
result list contains the theorem
|
lcp@104
|
627 |
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
|
lcp@104
|
628 |
\]
|
lcp@104
|
629 |
|
lcp@1119
|
630 |
\item[$thm@1$ \ttindexbold{COMP} $thm@2$]
|
lcp@104
|
631 |
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
|
lcp@326
|
632 |
unique; otherwise, it raises exception~\xdx{THM}\@. It is
|
lcp@104
|
633 |
analogous to {\tt RS}\@.
|
lcp@104
|
634 |
|
lcp@104
|
635 |
For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
|
lcp@332
|
636 |
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
|
lcp@104
|
637 |
principle of contrapositives. Then the result would be the
|
lcp@104
|
638 |
derived rule $\neg(b=a)\Imp\neg(a=b)$.
|
lcp@104
|
639 |
|
lcp@104
|
640 |
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
|
lcp@104
|
641 |
refines subgoal~$i$ of $state$ using $rule$, without lifting. The $rule$
|
lcp@104
|
642 |
is taken to have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where
|
lcp@326
|
643 |
$\psi$ need not be atomic; thus $m$ determines the number of new
|
lcp@104
|
644 |
subgoals. If $flag$ is {\tt true} then it performs elim-resolution --- it
|
lcp@104
|
645 |
solves the first premise of~$rule$ by assumption and deletes that
|
lcp@104
|
646 |
assumption. If $match$ is~{\tt true}, the $state$ is not instantiated.
|
lcp@326
|
647 |
\end{ttdescription}
|
lcp@104
|
648 |
|
lcp@104
|
649 |
|
lcp@104
|
650 |
\subsection{Other meta-rules}
|
lcp@104
|
651 |
\begin{ttbox}
|
lcp@104
|
652 |
trivial : Sign.cterm -> thm
|
lcp@104
|
653 |
lift_rule : (thm * int) -> thm -> thm
|
lcp@104
|
654 |
rename_params_rule : string list * int -> thm -> thm
|
lcp@104
|
655 |
rewrite_cterm : thm list -> Sign.cterm -> thm
|
lcp@104
|
656 |
flexflex_rule : thm -> thm Sequence.seq
|
lcp@104
|
657 |
\end{ttbox}
|
lcp@326
|
658 |
\begin{ttdescription}
|
lcp@104
|
659 |
\item[\ttindexbold{trivial} $ct$]
|
lcp@104
|
660 |
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
|
lcp@104
|
661 |
This is the initial state for a goal-directed proof of~$\phi$. The rule
|
lcp@104
|
662 |
checks that $ct$ has type~$prop$.
|
lcp@104
|
663 |
|
lcp@104
|
664 |
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
|
lcp@104
|
665 |
prepares $rule$ for resolution by lifting it over the parameters and
|
lcp@104
|
666 |
assumptions of subgoal~$i$ of~$state$.
|
lcp@104
|
667 |
|
lcp@104
|
668 |
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$]
|
lcp@104
|
669 |
uses the $names$ to rename the parameters of premise~$i$ of $thm$. The
|
lcp@104
|
670 |
names must be distinct. If there are fewer names than parameters, then the
|
lcp@104
|
671 |
rule renames the innermost parameters and may modify the remaining ones to
|
lcp@104
|
672 |
ensure that all the parameters are distinct.
|
lcp@104
|
673 |
\index{parameters!renaming}
|
lcp@104
|
674 |
|
lcp@104
|
675 |
\item[\ttindexbold{rewrite_cterm} $defs$ $ct$]
|
lcp@104
|
676 |
transforms $ct$ to $ct'$ by repeatedly applying $defs$ as rewrite rules; it
|
lcp@104
|
677 |
returns the conclusion~$ct\equiv ct'$. This underlies the meta-rewriting
|
lcp@104
|
678 |
tactics and rules.
|
lcp@326
|
679 |
\index{meta-rewriting!in terms}
|
lcp@104
|
680 |
|
lcp@104
|
681 |
\item[\ttindexbold{flexflex_rule} $thm$] \index{flex-flex constraints}
|
lcp@104
|
682 |
removes all flex-flex pairs from $thm$ using the trivial unifier.
|
lcp@326
|
683 |
\end{ttdescription}
|
paulson@1590
|
684 |
\index{meta-rules|)}
|
paulson@1590
|
685 |
|
paulson@1590
|
686 |
|
paulson@1846
|
687 |
\section{Proof objects}\label{sec:proofObjects}
|
paulson@1590
|
688 |
\index{proof objects|(} Isabelle can record the full meta-level proof of each
|
paulson@1590
|
689 |
theorem. The proof object contains all logical inferences in detail, while
|
paulson@1590
|
690 |
omitting bookkeeping steps that have no logical meaning to an outside
|
paulson@1590
|
691 |
observer. Rewriting steps are recorded in similar detail as the output of
|
paulson@1590
|
692 |
simplifier tracing. The proof object can be inspected by a separate
|
paulson@1590
|
693 |
proof-checker, or used to generate human-readable proof digests.
|
paulson@1590
|
694 |
|
paulson@1590
|
695 |
Full proof objects are large. They multiply storage requirements by about
|
paulson@1590
|
696 |
seven; attempts to build large logics (such as {\sc zf} and {\sc hol}) may
|
paulson@1590
|
697 |
fail. Isabelle normally builds minimal proof objects, which include only uses
|
paulson@1590
|
698 |
of oracles. You can also request an intermediate level of detail, containing
|
paulson@1590
|
699 |
uses of oracles, axioms and theorems. These smaller proof objects indicate a
|
paulson@1590
|
700 |
theorem's dependencies.
|
paulson@1590
|
701 |
|
paulson@1590
|
702 |
Isabelle provides proof objects for the sake of transparency. Their aim is to
|
paulson@1590
|
703 |
increase your confidence in Isabelle. They let you inspect proofs constructed
|
paulson@1590
|
704 |
by the classical reasoner or simplifier, and inform you of all uses of
|
paulson@1590
|
705 |
oracles. Seldom will proof objects be given whole to an automatic
|
paulson@1590
|
706 |
proof-checker: none has been written. It is up to you to examine and
|
paulson@1590
|
707 |
interpret them sensibly. For example, when scrutinizing a theorem's
|
paulson@1590
|
708 |
derivation for dependence upon some oracle or axiom, remember to scrutinize
|
paulson@1590
|
709 |
all of its lemmas. Their proofs are included in the main derivation, through
|
paulson@1590
|
710 |
the {\tt Theorem} constructor.
|
paulson@1590
|
711 |
|
paulson@1590
|
712 |
Proof objects are expressed using a polymorphic type of variable-branching
|
paulson@1590
|
713 |
trees. Proof objects (formally known as {\em derivations\/}) are trees
|
paulson@1590
|
714 |
labelled by rules, where {\tt rule} is a complicated datatype declared in the
|
paulson@1590
|
715 |
file {\tt Pure/thm.ML}.
|
paulson@1590
|
716 |
\begin{ttbox}
|
paulson@1590
|
717 |
datatype 'a mtree = Join of 'a * 'a mtree list;
|
paulson@1590
|
718 |
datatype rule = \(\ldots\);
|
paulson@1590
|
719 |
type deriv = rule mtree;
|
paulson@1590
|
720 |
\end{ttbox}
|
paulson@1590
|
721 |
%
|
paulson@1590
|
722 |
Each theorem's derivation is stored as the {\tt der} field of its internal
|
paulson@1590
|
723 |
record:
|
paulson@1590
|
724 |
\begin{ttbox}
|
paulson@1590
|
725 |
#der (rep_thm conjI);
|
paulson@1590
|
726 |
{\out Join (Theorem ({ProtoPure, CPure, HOL},"conjI"),}
|
paulson@1590
|
727 |
{\out [Join (MinProof,[])]) : deriv}
|
paulson@1590
|
728 |
\end{ttbox}
|
paulson@1590
|
729 |
This proof object identifies a labelled theorem, {\tt conjI}, whose underlying
|
paulson@1590
|
730 |
proof has not been recorded; all we have is {\tt MinProof}.
|
paulson@1590
|
731 |
|
paulson@1590
|
732 |
Nontrivial proof objects are unreadably large and complex. Isabelle provides
|
paulson@1590
|
733 |
several functions to help you inspect them informally. These functions omit
|
paulson@1590
|
734 |
the more obscure inferences and attempt to restructure the others into natural
|
paulson@1590
|
735 |
formats, linear or tree-structured.
|
paulson@1590
|
736 |
|
paulson@1590
|
737 |
\begin{ttbox}
|
paulson@1590
|
738 |
keep_derivs : deriv_kind ref
|
paulson@1590
|
739 |
Deriv.size : deriv -> int
|
paulson@1590
|
740 |
Deriv.drop : 'a mtree * int -> 'a mtree
|
paulson@1590
|
741 |
Deriv.linear : deriv -> deriv list
|
paulson@1876
|
742 |
Deriv.tree : deriv -> Deriv.orule mtree
|
paulson@1590
|
743 |
\end{ttbox}
|
paulson@1590
|
744 |
|
paulson@1590
|
745 |
\begin{ttdescription}
|
paulson@1590
|
746 |
\item[\ttindexbold{keep_derivs} := MinDeriv $|$ ThmDeriv $|$ FullDeriv;]
|
paulson@1590
|
747 |
specifies one of the three options for keeping derivations. They can be
|
paulson@1590
|
748 |
minimal (oracles only), include theorems and axioms, or be full.
|
paulson@1590
|
749 |
|
paulson@1590
|
750 |
\item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation,
|
paulson@1590
|
751 |
excluding lemmas.
|
paulson@1590
|
752 |
|
paulson@1590
|
753 |
\item[\ttindexbold{Deriv.drop} ($tree$,$n$)] returns the subtree $n$ levels
|
paulson@1590
|
754 |
down, always following the first child. It is good for stripping off
|
paulson@1590
|
755 |
outer level inferences that are used to put a theorem into standard form.
|
paulson@1590
|
756 |
|
paulson@1590
|
757 |
\item[\ttindexbold{Deriv.linear} $der$] converts a derivation into a linear
|
paulson@1590
|
758 |
format, replacing the deep nesting by a list of rules. Intuitively, this
|
paulson@1590
|
759 |
reveals the single-step Isabelle proof that is constructed internally by
|
paulson@1590
|
760 |
tactics.
|
paulson@1590
|
761 |
|
paulson@1590
|
762 |
\item[\ttindexbold{Deriv.tree} $der$] converts a derivation into an
|
paulson@1590
|
763 |
object-level proof tree. A resolution by an object-rule is converted to a
|
paulson@1590
|
764 |
tree node labelled by that rule. Complications arise if the object-rule is
|
paulson@1590
|
765 |
itself derived in some way. Nested resolutions are unravelled, but other
|
paulson@1590
|
766 |
operations on rules (such as rewriting) are left as-is.
|
paulson@1590
|
767 |
\end{ttdescription}
|
paulson@1590
|
768 |
|
paulson@2040
|
769 |
Functions {\tt Deriv.linear} and {\tt Deriv.tree} omit the proof of any named
|
paulson@2040
|
770 |
theorems (constructor {\tt Theorem}) they encounter in a derivation. Applying
|
paulson@2040
|
771 |
them directly to the derivation of a named theorem is therefore pointless.
|
paulson@2040
|
772 |
Use {\tt Deriv.drop} with argument~1 to skip over the initial {\tt Theorem}
|
paulson@2040
|
773 |
constructor.
|
paulson@2040
|
774 |
|
paulson@2040
|
775 |
|
paulson@1590
|
776 |
\index{proof objects|)}
|
lcp@104
|
777 |
\index{theorems|)}
|