wenzelm@30184
|
1 |
|
lcp@104
|
2 |
\chapter{Theorems and Forward Proof}
|
lcp@104
|
3 |
\index{theorems|(}
|
lcp@326
|
4 |
|
wenzelm@3108
|
5 |
Theorems, which represent the axioms, theorems and rules of
|
wenzelm@44136
|
6 |
object-logics, have type \mltydx{thm}. This chapter describes
|
wenzelm@44136
|
7 |
operations that join theorems in forward proof. Most theorem
|
wenzelm@44136
|
8 |
operations are intended for advanced applications, such as programming
|
wenzelm@44136
|
9 |
new proof procedures.
|
lcp@104
|
10 |
|
lcp@104
|
11 |
|
lcp@104
|
12 |
\section{Basic operations on theorems}
|
lcp@104
|
13 |
|
lcp@326
|
14 |
\subsection{Forward proof: joining rules by resolution}
|
lcp@326
|
15 |
\index{theorems!joining by resolution}
|
lcp@326
|
16 |
\index{resolution}\index{forward proof}
|
lcp@104
|
17 |
\begin{ttbox}
|
paulson@8136
|
18 |
RSN : thm * (int * thm) -> thm \hfill\textbf{infix}
|
paulson@8136
|
19 |
RS : thm * thm -> thm \hfill\textbf{infix}
|
paulson@8136
|
20 |
MRS : thm list * thm -> thm \hfill\textbf{infix}
|
wenzelm@9288
|
21 |
OF : thm * thm list -> thm \hfill\textbf{infix}
|
paulson@8136
|
22 |
RLN : thm list * (int * thm list) -> thm list \hfill\textbf{infix}
|
paulson@8136
|
23 |
RL : thm list * thm list -> thm list \hfill\textbf{infix}
|
paulson@8136
|
24 |
MRL : thm list list * thm list -> thm list \hfill\textbf{infix}
|
lcp@104
|
25 |
\end{ttbox}
|
lcp@326
|
26 |
Joining rules together is a simple way of deriving new rules. These
|
lcp@876
|
27 |
functions are especially useful with destruction rules. To store
|
lcp@876
|
28 |
the result in the theorem database, use \ttindex{bind_thm}
|
lcp@876
|
29 |
(\S\ref{ExtractingAndStoringTheProvedTheorem}).
|
lcp@326
|
30 |
\begin{ttdescription}
|
lcp@104
|
31 |
\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN}
|
lcp@326
|
32 |
resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.
|
lcp@326
|
33 |
Unless there is precisely one resolvent it raises exception
|
lcp@326
|
34 |
\xdx{THM}; in that case, use {\tt RLN}.
|
lcp@104
|
35 |
|
lcp@104
|
36 |
\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS}
|
lcp@104
|
37 |
abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}. Thus, it resolves the
|
lcp@104
|
38 |
conclusion of $thm@1$ with the first premise of~$thm@2$.
|
lcp@104
|
39 |
|
lcp@104
|
40 |
\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS}
|
lcp@332
|
41 |
uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
|
lcp@104
|
42 |
$i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$
|
lcp@104
|
43 |
premises of $thm$. Because the theorems are used from right to left, it
|
lcp@104
|
44 |
does not matter if the $thm@i$ create new premises. {\tt MRS} is useful
|
lcp@104
|
45 |
for expressing proof trees.
|
wenzelm@9288
|
46 |
|
wenzelm@9288
|
47 |
\item[\tt {$thm$ OF $[thm@1,\ldots,thm@n]$}] \indexbold{*OF} is the same as
|
wenzelm@9288
|
48 |
\texttt{$[thm@1,\ldots,thm@n]$ MRS $thm$}, with slightly more readable
|
wenzelm@9288
|
49 |
argument order, though.
|
lcp@104
|
50 |
|
wenzelm@151
|
51 |
\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN}
|
lcp@326
|
52 |
joins lists of theorems. For every $thm@1$ in $thms@1$ and $thm@2$ in
|
lcp@326
|
53 |
$thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise
|
lcp@326
|
54 |
of~$thm@2$, accumulating the results.
|
lcp@104
|
55 |
|
wenzelm@151
|
56 |
\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL}
|
wenzelm@151
|
57 |
abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}.
|
lcp@104
|
58 |
|
lcp@104
|
59 |
\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL}
|
lcp@104
|
60 |
is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
|
lcp@104
|
61 |
It too is useful for expressing proof trees.
|
lcp@326
|
62 |
\end{ttdescription}
|
lcp@104
|
63 |
|
lcp@104
|
64 |
|
lcp@104
|
65 |
\subsection{Expanding definitions in theorems}
|
lcp@326
|
66 |
\index{meta-rewriting!in theorems}
|
lcp@104
|
67 |
\begin{ttbox}
|
lcp@104
|
68 |
rewrite_rule : thm list -> thm -> thm
|
lcp@104
|
69 |
rewrite_goals_rule : thm list -> thm -> thm
|
lcp@104
|
70 |
\end{ttbox}
|
lcp@326
|
71 |
\begin{ttdescription}
|
lcp@104
|
72 |
\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]
|
lcp@104
|
73 |
unfolds the {\it defs} throughout the theorem~{\it thm}.
|
lcp@104
|
74 |
|
lcp@104
|
75 |
\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]
|
paulson@8136
|
76 |
unfolds the {\it defs} in the premises of~{\it thm}, but it leaves the
|
paulson@8136
|
77 |
conclusion unchanged. This rule is the basis for \ttindex{rewrite_goals_tac},
|
paulson@8136
|
78 |
but it serves little purpose in forward proof.
|
lcp@326
|
79 |
\end{ttdescription}
|
lcp@104
|
80 |
|
lcp@104
|
81 |
|
paulson@4383
|
82 |
\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
|
lcp@326
|
83 |
\index{instantiation}
|
paulson@8136
|
84 |
\begin{alltt}\footnotesize
|
paulson@4383
|
85 |
read_instantiate : (string*string) list -> thm -> thm
|
paulson@4383
|
86 |
read_instantiate_sg : Sign.sg -> (string*string) list -> thm -> thm
|
paulson@4383
|
87 |
cterm_instantiate : (cterm*cterm) list -> thm -> thm
|
paulson@4383
|
88 |
instantiate' : ctyp option list -> cterm option list -> thm -> thm
|
paulson@8136
|
89 |
\end{alltt}
|
lcp@104
|
90 |
These meta-rules instantiate type and term unknowns in a theorem. They are
|
lcp@104
|
91 |
occasionally useful. They can prevent difficulties with higher-order
|
lcp@104
|
92 |
unification, and define specialized versions of rules.
|
lcp@326
|
93 |
\begin{ttdescription}
|
lcp@104
|
94 |
\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}]
|
lcp@104
|
95 |
processes the instantiations {\it insts} and instantiates the rule~{\it
|
lcp@104
|
96 |
thm}. The processing of instantiations is described
|
lcp@326
|
97 |
in \S\ref{res_inst_tac}, under {\tt res_inst_tac}.
|
lcp@104
|
98 |
|
lcp@104
|
99 |
Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
|
lcp@104
|
100 |
and refine a particular subgoal. The tactic allows instantiation by the
|
lcp@104
|
101 |
subgoal's parameters, and reads the instantiations using the signature
|
lcp@326
|
102 |
associated with the proof state.
|
lcp@104
|
103 |
|
lcp@326
|
104 |
Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated
|
lcp@326
|
105 |
incorrectly.
|
lcp@326
|
106 |
|
lcp@326
|
107 |
\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
|
paulson@4597
|
108 |
is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads
|
lcp@326
|
109 |
the instantiations under signature~{\it sg}. This is necessary to
|
lcp@326
|
110 |
instantiate a rule from a general theory, such as first-order logic,
|
lcp@326
|
111 |
using the notation of some specialized theory. Use the function {\tt
|
lcp@326
|
112 |
sign_of} to get a theory's signature.
|
lcp@104
|
113 |
|
lcp@104
|
114 |
\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}]
|
lcp@104
|
115 |
is similar to {\tt read_instantiate}, but the instantiations are provided
|
lcp@104
|
116 |
as pairs of certified terms, not as strings to be read.
|
wenzelm@4317
|
117 |
|
wenzelm@4317
|
118 |
\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}]
|
wenzelm@4317
|
119 |
instantiates {\it thm} according to the positional arguments {\it
|
wenzelm@4317
|
120 |
ctyps} and {\it cterms}. Counting from left to right, schematic
|
wenzelm@4317
|
121 |
variables $?x$ are either replaced by $t$ for any argument
|
wenzelm@4317
|
122 |
\texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or
|
wenzelm@4317
|
123 |
if the end of the argument list is encountered. Types are
|
wenzelm@4317
|
124 |
instantiated before terms.
|
wenzelm@4317
|
125 |
|
lcp@326
|
126 |
\end{ttdescription}
|
lcp@104
|
127 |
|
lcp@104
|
128 |
|
clasohm@866
|
129 |
\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
|
lcp@326
|
130 |
\index{theorems!standardizing}
|
lcp@104
|
131 |
\begin{ttbox}
|
paulson@8969
|
132 |
standard : thm -> thm
|
paulson@8969
|
133 |
zero_var_indexes : thm -> thm
|
paulson@8969
|
134 |
make_elim : thm -> thm
|
paulson@8969
|
135 |
rule_by_tactic : tactic -> thm -> thm
|
paulson@8969
|
136 |
rotate_prems : int -> thm -> thm
|
paulson@8969
|
137 |
permute_prems : int -> int -> thm -> thm
|
oheimb@11163
|
138 |
rearrange_prems : int list -> thm -> thm
|
lcp@104
|
139 |
\end{ttbox}
|
lcp@326
|
140 |
\begin{ttdescription}
|
wenzelm@3108
|
141 |
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
|
wenzelm@3108
|
142 |
of object-rules. It discharges all meta-assumptions, replaces free
|
wenzelm@3108
|
143 |
variables by schematic variables, renames schematic variables to
|
wenzelm@3108
|
144 |
have subscript zero, also strips outer (meta) quantifiers and
|
wenzelm@3108
|
145 |
removes dangling sort hypotheses.
|
lcp@104
|
146 |
|
lcp@104
|
147 |
\item[\ttindexbold{zero_var_indexes} $thm$]
|
lcp@104
|
148 |
makes all schematic variables have subscript zero, renaming them to avoid
|
lcp@104
|
149 |
clashes.
|
lcp@104
|
150 |
|
lcp@104
|
151 |
\item[\ttindexbold{make_elim} $thm$]
|
lcp@104
|
152 |
\index{rules!converting destruction to elimination}
|
paulson@8136
|
153 |
converts $thm$, which should be a destruction rule of the form
|
paulson@8136
|
154 |
$\List{P@1;\ldots;P@m}\Imp
|
lcp@104
|
155 |
Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This
|
lcp@104
|
156 |
is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
|
lcp@104
|
157 |
|
lcp@104
|
158 |
\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}]
|
lcp@104
|
159 |
applies {\it tac\/} to the {\it thm}, freezing its variables first, then
|
lcp@104
|
160 |
yields the proof state returned by the tactic. In typical usage, the
|
lcp@104
|
161 |
{\it thm\/} represents an instance of a rule with several premises, some
|
lcp@104
|
162 |
with contradictory assumptions (because of the instantiation). The
|
lcp@104
|
163 |
tactic proves those subgoals and does whatever else it can, and returns
|
lcp@104
|
164 |
whatever is left.
|
paulson@4607
|
165 |
|
paulson@4607
|
166 |
\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
|
paulson@8969
|
167 |
the left by~$k$ positions (to the right if $k<0$). It simply calls
|
paulson@8969
|
168 |
\texttt{permute_prems}, below, with $j=0$. Used with
|
paulson@8969
|
169 |
\texttt{eresolve_tac}\index{*eresolve_tac!on other than first premise}, it
|
paulson@8969
|
170 |
gives the effect of applying the tactic to some other premise of $thm$ than
|
paulson@8969
|
171 |
the first.
|
paulson@8969
|
172 |
|
paulson@8969
|
173 |
\item[\ttindexbold{permute_prems} $j$ $k$ $thm$] rotates the premises of $thm$
|
paulson@8969
|
174 |
leaving the first $j$ premises unchanged. It
|
paulson@8969
|
175 |
requires $0\leq j\leq n$, where $n$ is the number of premises. If $k$ is
|
paulson@8969
|
176 |
positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
|
paulson@8969
|
177 |
negative then it rotates the premises to the right.
|
oheimb@11163
|
178 |
|
oheimb@11163
|
179 |
\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$
|
oheimb@11163
|
180 |
where the value at the $i$-th position (counting from $0$) in the list $ps$
|
oheimb@11163
|
181 |
gives the position within the original thm to be transferred to position $i$.
|
oheimb@11163
|
182 |
Any remaining trailing positions are left unchanged.
|
lcp@326
|
183 |
\end{ttdescription}
|
lcp@104
|
184 |
|
lcp@104
|
185 |
|
lcp@104
|
186 |
\subsection{Taking a theorem apart}
|
lcp@326
|
187 |
\index{theorems!taking apart}
|
lcp@104
|
188 |
\index{flex-flex constraints}
|
lcp@104
|
189 |
\begin{ttbox}
|
wenzelm@4317
|
190 |
cprop_of : thm -> cterm
|
lcp@104
|
191 |
concl_of : thm -> term
|
lcp@104
|
192 |
prems_of : thm -> term list
|
wenzelm@4317
|
193 |
cprems_of : thm -> cterm list
|
lcp@104
|
194 |
nprems_of : thm -> int
|
paulson@4383
|
195 |
tpairs_of : thm -> (term*term) list
|
wenzelm@4317
|
196 |
sign_of_thm : thm -> Sign.sg
|
clasohm@866
|
197 |
theory_of_thm : thm -> theory
|
paulson@8136
|
198 |
dest_state : thm * int -> (term*term) list * term list * term * term
|
wenzelm@9499
|
199 |
rep_thm : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
|
paulson@8136
|
200 |
shyps: sort list, hyps: term list, prop: term\}
|
wenzelm@9499
|
201 |
crep_thm : thm -> \{sign_ref: Sign.sg_ref, der: bool * deriv, maxidx: int,
|
paulson@8136
|
202 |
shyps: sort list, hyps: cterm list, prop:{\ts}cterm\}
|
lcp@104
|
203 |
\end{ttbox}
|
lcp@326
|
204 |
\begin{ttdescription}
|
wenzelm@4317
|
205 |
\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
|
wenzelm@4317
|
206 |
a certified term.
|
wenzelm@4317
|
207 |
|
wenzelm@4317
|
208 |
\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
|
wenzelm@4317
|
209 |
a term.
|
wenzelm@4317
|
210 |
|
wenzelm@4317
|
211 |
\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
|
wenzelm@4317
|
212 |
list of terms.
|
wenzelm@4317
|
213 |
|
wenzelm@4317
|
214 |
\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
|
wenzelm@4317
|
215 |
a list of certified terms.
|
lcp@104
|
216 |
|
lcp@104
|
217 |
\item[\ttindexbold{nprems_of} $thm$]
|
lcp@286
|
218 |
returns the number of premises in $thm$, and is equivalent to {\tt
|
wenzelm@4317
|
219 |
length~(prems_of~$thm$)}.
|
lcp@104
|
220 |
|
wenzelm@4317
|
221 |
\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
|
wenzelm@4317
|
222 |
of $thm$.
|
wenzelm@4317
|
223 |
|
wenzelm@4317
|
224 |
\item[\ttindexbold{sign_of_thm} $thm$] returns the signature
|
wenzelm@4317
|
225 |
associated with $thm$.
|
wenzelm@4317
|
226 |
|
wenzelm@4317
|
227 |
\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
|
wenzelm@4317
|
228 |
with $thm$. Note that this does a lookup in Isabelle's global
|
wenzelm@4317
|
229 |
database of loaded theories.
|
clasohm@866
|
230 |
|
lcp@104
|
231 |
\item[\ttindexbold{dest_state} $(thm,i)$]
|
lcp@104
|
232 |
decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
|
lcp@104
|
233 |
list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
|
lcp@104
|
234 |
(this will be an implication if there are more than $i$ subgoals).
|
lcp@104
|
235 |
|
wenzelm@4317
|
236 |
\item[\ttindexbold{rep_thm} $thm$] decomposes $thm$ as a record
|
wenzelm@4317
|
237 |
containing the statement of~$thm$ ({\tt prop}), its list of
|
wenzelm@4317
|
238 |
meta-assumptions ({\tt hyps}), its derivation ({\tt der}), a bound
|
wenzelm@4317
|
239 |
on the maximum subscript of its unknowns ({\tt maxidx}), and a
|
wenzelm@4317
|
240 |
reference to its signature ({\tt sign_ref}). The {\tt shyps} field
|
wenzelm@4317
|
241 |
is discussed below.
|
wenzelm@4317
|
242 |
|
wenzelm@4317
|
243 |
\item[\ttindexbold{crep_thm} $thm$] like \texttt{rep_thm}, but returns
|
wenzelm@4317
|
244 |
the hypotheses and statement as certified terms.
|
wenzelm@4317
|
245 |
|
lcp@326
|
246 |
\end{ttdescription}
|
lcp@104
|
247 |
|
lcp@104
|
248 |
|
wenzelm@5777
|
249 |
\subsection{*Sort hypotheses} \label{sec:sort-hyps}
|
paulson@2040
|
250 |
\index{sort hypotheses}
|
paulson@2040
|
251 |
\begin{ttbox}
|
wenzelm@7644
|
252 |
strip_shyps : thm -> thm
|
wenzelm@7644
|
253 |
strip_shyps_warning : thm -> thm
|
paulson@2040
|
254 |
\end{ttbox}
|
paulson@2040
|
255 |
|
paulson@2044
|
256 |
Isabelle's type variables are decorated with sorts, constraining them to
|
paulson@2044
|
257 |
certain ranges of types. This has little impact when sorts only serve for
|
paulson@2044
|
258 |
syntactic classification of types --- for example, FOL distinguishes between
|
paulson@2044
|
259 |
terms and other types. But when type classes are introduced through axioms,
|
paulson@2044
|
260 |
this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
|
wenzelm@4317
|
261 |
a type belonging to it because certain sets of axioms are unsatisfiable.
|
paulson@2040
|
262 |
|
wenzelm@3108
|
263 |
If a theorem contains a type variable that is constrained by an empty
|
paulson@3485
|
264 |
sort, then that theorem has no instances. It is basically an instance
|
wenzelm@3108
|
265 |
of {\em ex falso quodlibet}. But what if it is used to prove another
|
wenzelm@3108
|
266 |
theorem that no longer involves that sort? The latter theorem holds
|
wenzelm@3108
|
267 |
only if under an additional non-emptiness assumption.
|
paulson@2040
|
268 |
|
paulson@3485
|
269 |
Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt
|
paulson@2044
|
270 |
shyps} field is a list of sorts occurring in type variables in the current
|
paulson@2044
|
271 |
{\tt prop} and {\tt hyps} fields. It may also includes sorts used in the
|
paulson@2044
|
272 |
theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
|
paulson@3485
|
273 |
fields --- so-called {\em dangling\/} sort constraints. These are the
|
paulson@2044
|
274 |
critical ones, asserting non-emptiness of the corresponding sorts.
|
paulson@2044
|
275 |
|
wenzelm@7644
|
276 |
Isabelle automatically removes extraneous sorts from the {\tt shyps} field at
|
wenzelm@7644
|
277 |
the end of a proof, provided that non-emptiness can be established by looking
|
wenzelm@7644
|
278 |
at the theorem's signature: from the {\tt classes} and {\tt arities}
|
wenzelm@7644
|
279 |
information. This operation is performed by \texttt{strip_shyps} and
|
wenzelm@7644
|
280 |
\texttt{strip_shyps_warning}.
|
wenzelm@7644
|
281 |
|
wenzelm@7644
|
282 |
\begin{ttdescription}
|
wenzelm@7644
|
283 |
|
wenzelm@7644
|
284 |
\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
|
wenzelm@7644
|
285 |
that can be witnessed from the type signature.
|
wenzelm@7644
|
286 |
|
wenzelm@7644
|
287 |
\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
|
wenzelm@7644
|
288 |
issues a warning message of any pending sort hypotheses that do not have a
|
wenzelm@7644
|
289 |
(syntactic) witness.
|
wenzelm@7644
|
290 |
|
wenzelm@7644
|
291 |
\end{ttdescription}
|
paulson@2040
|
292 |
|
paulson@2040
|
293 |
|
lcp@104
|
294 |
\subsection{Tracing flags for unification}
|
lcp@326
|
295 |
\index{tracing!of unification}
|
lcp@104
|
296 |
\begin{ttbox}
|
paulson@8136
|
297 |
Unify.trace_simp : bool ref \hfill\textbf{initially false}
|
paulson@8136
|
298 |
Unify.trace_types : bool ref \hfill\textbf{initially false}
|
paulson@8136
|
299 |
Unify.trace_bound : int ref \hfill\textbf{initially 10}
|
paulson@8136
|
300 |
Unify.search_bound : int ref \hfill\textbf{initially 20}
|
lcp@104
|
301 |
\end{ttbox}
|
lcp@104
|
302 |
Tracing the search may be useful when higher-order unification behaves
|
lcp@104
|
303 |
unexpectedly. Letting {\tt res_inst_tac} circumvent the problem is easier,
|
lcp@104
|
304 |
though.
|
lcp@326
|
305 |
\begin{ttdescription}
|
wenzelm@4317
|
306 |
\item[set Unify.trace_simp;]
|
lcp@104
|
307 |
causes tracing of the simplification phase.
|
lcp@104
|
308 |
|
wenzelm@4317
|
309 |
\item[set Unify.trace_types;]
|
lcp@104
|
310 |
generates warnings of incompleteness, when unification is not considering
|
lcp@104
|
311 |
all possible instantiations of type unknowns.
|
lcp@104
|
312 |
|
lcp@326
|
313 |
\item[Unify.trace_bound := $n$;]
|
lcp@104
|
314 |
causes unification to print tracing information once it reaches depth~$n$.
|
lcp@104
|
315 |
Use $n=0$ for full tracing. At the default value of~10, tracing
|
lcp@104
|
316 |
information is almost never printed.
|
lcp@104
|
317 |
|
paulson@8136
|
318 |
\item[Unify.search_bound := $n$;] prevents unification from
|
paulson@8136
|
319 |
searching past the depth~$n$. Because of this bound, higher-order
|
wenzelm@4317
|
320 |
unification cannot return an infinite sequence, though it can return
|
paulson@8136
|
321 |
an exponentially long one. The search rarely approaches the default value
|
wenzelm@4317
|
322 |
of~20. If the search is cut off, unification prints a warning
|
wenzelm@4317
|
323 |
\texttt{Unification bound exceeded}.
|
lcp@326
|
324 |
\end{ttdescription}
|
lcp@104
|
325 |
|
lcp@104
|
326 |
|
wenzelm@4317
|
327 |
\section{*Primitive meta-level inference rules}
|
lcp@104
|
328 |
\index{meta-rules|(}
|
lcp@104
|
329 |
|
lcp@326
|
330 |
\subsection{Logical equivalence rules}
|
lcp@326
|
331 |
\index{meta-equality}
|
lcp@104
|
332 |
\begin{ttbox}
|
lcp@326
|
333 |
equal_intr : thm -> thm -> thm
|
lcp@326
|
334 |
equal_elim : thm -> thm -> thm
|
lcp@104
|
335 |
\end{ttbox}
|
lcp@326
|
336 |
\begin{ttdescription}
|
lcp@104
|
337 |
\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
|
lcp@332
|
338 |
applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$
|
lcp@332
|
339 |
and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
|
lcp@332
|
340 |
the first premise with~$\phi$ removed, plus those of
|
lcp@332
|
341 |
the second premise with~$\psi$ removed.
|
lcp@104
|
342 |
|
lcp@104
|
343 |
\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
|
lcp@104
|
344 |
applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
|
lcp@104
|
345 |
$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
|
lcp@326
|
346 |
\end{ttdescription}
|
lcp@104
|
347 |
|
lcp@104
|
348 |
|
lcp@104
|
349 |
\subsection{Equality rules}
|
lcp@326
|
350 |
\index{meta-equality}
|
lcp@104
|
351 |
\begin{ttbox}
|
wenzelm@3108
|
352 |
reflexive : cterm -> thm
|
lcp@104
|
353 |
symmetric : thm -> thm
|
lcp@104
|
354 |
transitive : thm -> thm -> thm
|
lcp@104
|
355 |
\end{ttbox}
|
lcp@326
|
356 |
\begin{ttdescription}
|
lcp@104
|
357 |
\item[\ttindexbold{reflexive} $ct$]
|
wenzelm@151
|
358 |
makes the theorem \(ct\equiv ct\).
|
lcp@104
|
359 |
|
lcp@104
|
360 |
\item[\ttindexbold{symmetric} $thm$]
|
lcp@104
|
361 |
maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
|
lcp@104
|
362 |
|
lcp@104
|
363 |
\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
|
lcp@104
|
364 |
maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
|
lcp@326
|
365 |
\end{ttdescription}
|
lcp@104
|
366 |
|
lcp@104
|
367 |
|
lcp@104
|
368 |
\subsection{The $\lambda$-conversion rules}
|
lcp@326
|
369 |
\index{lambda calc@$\lambda$-calculus}
|
lcp@104
|
370 |
\begin{ttbox}
|
wenzelm@3108
|
371 |
beta_conversion : cterm -> thm
|
lcp@104
|
372 |
extensional : thm -> thm
|
wenzelm@3108
|
373 |
abstract_rule : string -> cterm -> thm -> thm
|
lcp@104
|
374 |
combination : thm -> thm -> thm
|
lcp@104
|
375 |
\end{ttbox}
|
lcp@326
|
376 |
There is no rule for $\alpha$-conversion because Isabelle regards
|
lcp@326
|
377 |
$\alpha$-convertible theorems as equal.
|
lcp@326
|
378 |
\begin{ttdescription}
|
lcp@104
|
379 |
\item[\ttindexbold{beta_conversion} $ct$]
|
lcp@104
|
380 |
makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
|
lcp@104
|
381 |
term $(\lambda x.a)(b)$.
|
lcp@104
|
382 |
|
lcp@104
|
383 |
\item[\ttindexbold{extensional} $thm$]
|
lcp@104
|
384 |
maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
|
lcp@104
|
385 |
Parameter~$x$ is taken from the premise. It may be an unknown or a free
|
lcp@332
|
386 |
variable (provided it does not occur in the assumptions); it must not occur
|
lcp@104
|
387 |
in $f$ or~$g$.
|
lcp@104
|
388 |
|
lcp@104
|
389 |
\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
|
lcp@104
|
390 |
maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
|
lcp@104
|
391 |
(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
|
lcp@104
|
392 |
Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
|
lcp@332
|
393 |
variable (provided it does not occur in the assumptions). In the
|
lcp@104
|
394 |
conclusion, the bound variable is named~$v$.
|
lcp@104
|
395 |
|
lcp@104
|
396 |
\item[\ttindexbold{combination} $thm@1$ $thm@2$]
|
lcp@104
|
397 |
maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
|
lcp@104
|
398 |
g(b)$.
|
lcp@326
|
399 |
\end{ttdescription}
|
lcp@104
|
400 |
|
lcp@104
|
401 |
|
lcp@104
|
402 |
\section{Derived rules for goal-directed proof}
|
lcp@104
|
403 |
Most of these rules have the sole purpose of implementing particular
|
lcp@104
|
404 |
tactics. There are few occasions for applying them directly to a theorem.
|
lcp@104
|
405 |
|
lcp@104
|
406 |
\subsection{Proof by assumption}
|
lcp@326
|
407 |
\index{meta-assumptions}
|
lcp@104
|
408 |
\begin{ttbox}
|
wenzelm@4276
|
409 |
assumption : int -> thm -> thm Seq.seq
|
lcp@104
|
410 |
eq_assumption : int -> thm -> thm
|
lcp@104
|
411 |
\end{ttbox}
|
lcp@326
|
412 |
\begin{ttdescription}
|
lcp@104
|
413 |
\item[\ttindexbold{assumption} {\it i} $thm$]
|
lcp@104
|
414 |
attempts to solve premise~$i$ of~$thm$ by assumption.
|
lcp@104
|
415 |
|
lcp@104
|
416 |
\item[\ttindexbold{eq_assumption}]
|
lcp@104
|
417 |
is like {\tt assumption} but does not use unification.
|
lcp@326
|
418 |
\end{ttdescription}
|
lcp@104
|
419 |
|
lcp@104
|
420 |
|
lcp@104
|
421 |
\subsection{Resolution}
|
lcp@326
|
422 |
\index{resolution}
|
lcp@104
|
423 |
\begin{ttbox}
|
lcp@104
|
424 |
biresolution : bool -> (bool*thm)list -> int -> thm
|
wenzelm@4276
|
425 |
-> thm Seq.seq
|
lcp@104
|
426 |
\end{ttbox}
|
lcp@326
|
427 |
\begin{ttdescription}
|
lcp@104
|
428 |
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$]
|
lcp@326
|
429 |
performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
|
lcp@104
|
430 |
(flag,rule)$ pairs. For each pair, it applies resolution if the flag
|
lcp@104
|
431 |
is~{\tt false} and elim-resolution if the flag is~{\tt true}. If $match$
|
lcp@104
|
432 |
is~{\tt true}, the $state$ is not instantiated.
|
lcp@326
|
433 |
\end{ttdescription}
|
lcp@104
|
434 |
|
lcp@104
|
435 |
|
lcp@104
|
436 |
\subsection{Composition: resolution without lifting}
|
lcp@326
|
437 |
\index{resolution!without lifting}
|
lcp@104
|
438 |
\begin{ttbox}
|
lcp@104
|
439 |
compose : thm * int * thm -> thm list
|
lcp@104
|
440 |
COMP : thm * thm -> thm
|
lcp@104
|
441 |
bicompose : bool -> bool * thm * int -> int -> thm
|
wenzelm@4276
|
442 |
-> thm Seq.seq
|
lcp@104
|
443 |
\end{ttbox}
|
lcp@104
|
444 |
In forward proof, a typical use of composition is to regard an assertion of
|
lcp@104
|
445 |
the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so
|
lcp@104
|
446 |
beware of clashes!
|
lcp@326
|
447 |
\begin{ttdescription}
|
lcp@104
|
448 |
\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)]
|
lcp@104
|
449 |
uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
|
lcp@104
|
450 |
of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
|
lcp@104
|
451 |
\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the
|
lcp@104
|
452 |
result list contains the theorem
|
lcp@104
|
453 |
\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
|
lcp@104
|
454 |
\]
|
lcp@104
|
455 |
|
lcp@1119
|
456 |
\item[$thm@1$ \ttindexbold{COMP} $thm@2$]
|
lcp@104
|
457 |
calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
|
lcp@326
|
458 |
unique; otherwise, it raises exception~\xdx{THM}\@. It is
|
lcp@104
|
459 |
analogous to {\tt RS}\@.
|
lcp@104
|
460 |
|
lcp@104
|
461 |
For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
|
lcp@332
|
462 |
that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
|
lcp@104
|
463 |
principle of contrapositives. Then the result would be the
|
lcp@104
|
464 |
derived rule $\neg(b=a)\Imp\neg(a=b)$.
|
lcp@104
|
465 |
|
lcp@104
|
466 |
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
|
lcp@104
|
467 |
refines subgoal~$i$ of $state$ using $rule$, without lifting. The $rule$
|
lcp@104
|
468 |
is taken to have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where
|
lcp@326
|
469 |
$\psi$ need not be atomic; thus $m$ determines the number of new
|
lcp@104
|
470 |
subgoals. If $flag$ is {\tt true} then it performs elim-resolution --- it
|
lcp@104
|
471 |
solves the first premise of~$rule$ by assumption and deletes that
|
lcp@104
|
472 |
assumption. If $match$ is~{\tt true}, the $state$ is not instantiated.
|
lcp@326
|
473 |
\end{ttdescription}
|
lcp@104
|
474 |
|
lcp@104
|
475 |
|
lcp@104
|
476 |
\subsection{Other meta-rules}
|
lcp@104
|
477 |
\begin{ttbox}
|
wenzelm@3108
|
478 |
trivial : cterm -> thm
|
lcp@104
|
479 |
lift_rule : (thm * int) -> thm -> thm
|
lcp@104
|
480 |
rename_params_rule : string list * int -> thm -> thm
|
wenzelm@4276
|
481 |
flexflex_rule : thm -> thm Seq.seq
|
lcp@104
|
482 |
\end{ttbox}
|
lcp@326
|
483 |
\begin{ttdescription}
|
lcp@104
|
484 |
\item[\ttindexbold{trivial} $ct$]
|
lcp@104
|
485 |
makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
|
lcp@104
|
486 |
This is the initial state for a goal-directed proof of~$\phi$. The rule
|
lcp@104
|
487 |
checks that $ct$ has type~$prop$.
|
lcp@104
|
488 |
|
lcp@104
|
489 |
\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
|
lcp@104
|
490 |
prepares $rule$ for resolution by lifting it over the parameters and
|
lcp@104
|
491 |
assumptions of subgoal~$i$ of~$state$.
|
lcp@104
|
492 |
|
lcp@104
|
493 |
\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$]
|
lcp@104
|
494 |
uses the $names$ to rename the parameters of premise~$i$ of $thm$. The
|
lcp@104
|
495 |
names must be distinct. If there are fewer names than parameters, then the
|
lcp@104
|
496 |
rule renames the innermost parameters and may modify the remaining ones to
|
lcp@104
|
497 |
ensure that all the parameters are distinct.
|
lcp@104
|
498 |
\index{parameters!renaming}
|
lcp@104
|
499 |
|
lcp@104
|
500 |
\item[\ttindexbold{flexflex_rule} $thm$] \index{flex-flex constraints}
|
lcp@104
|
501 |
removes all flex-flex pairs from $thm$ using the trivial unifier.
|
lcp@326
|
502 |
\end{ttdescription}
|
paulson@1590
|
503 |
\index{meta-rules|)}
|
paulson@1590
|
504 |
|
paulson@1590
|
505 |
|
berghofe@11622
|
506 |
\section{Proof terms}\label{sec:proofObjects}
|
berghofe@11622
|
507 |
\index{proof terms|(} Isabelle can record the full meta-level proof of each
|
berghofe@11622
|
508 |
theorem. The proof term contains all logical inferences in detail.
|
berghofe@11622
|
509 |
%while
|
berghofe@11622
|
510 |
%omitting bookkeeping steps that have no logical meaning to an outside
|
berghofe@11622
|
511 |
%observer. Rewriting steps are recorded in similar detail as the output of
|
berghofe@11622
|
512 |
%simplifier tracing.
|
berghofe@11622
|
513 |
Resolution and rewriting steps are broken down to primitive rules of the
|
berghofe@11622
|
514 |
meta-logic. The proof term can be inspected by a separate proof-checker,
|
berghofe@11622
|
515 |
for example.
|
paulson@1590
|
516 |
|
berghofe@11622
|
517 |
According to the well-known {\em Curry-Howard isomorphism}, a proof can
|
berghofe@11622
|
518 |
be viewed as a $\lambda$-term. Following this idea, proofs
|
berghofe@11622
|
519 |
in Isabelle are internally represented by a datatype similar to the one for
|
berghofe@11622
|
520 |
terms described in \S\ref{sec:terms}.
|
berghofe@11622
|
521 |
\begin{ttbox}
|
berghofe@11622
|
522 |
infix 8 % %%;
|
paulson@1590
|
523 |
|
berghofe@11622
|
524 |
datatype proof =
|
berghofe@11622
|
525 |
PBound of int
|
berghofe@11622
|
526 |
| Abst of string * typ option * proof
|
berghofe@11622
|
527 |
| AbsP of string * term option * proof
|
berghofe@11622
|
528 |
| op % of proof * term option
|
berghofe@11622
|
529 |
| op %% of proof * proof
|
berghofe@11622
|
530 |
| Hyp of term
|
berghofe@11622
|
531 |
| PThm of (string * (string * string list) list) *
|
berghofe@11622
|
532 |
proof * term * typ list option
|
berghofe@11622
|
533 |
| PAxm of string * term * typ list option
|
berghofe@11622
|
534 |
| Oracle of string * term * typ list option
|
berghofe@11622
|
535 |
| MinProof of proof list;
|
berghofe@11622
|
536 |
\end{ttbox}
|
paulson@1590
|
537 |
|
berghofe@11622
|
538 |
\begin{ttdescription}
|
berghofe@11622
|
539 |
\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over
|
berghofe@11622
|
540 |
a {\it term variable} of type $\tau$ in the body $prf$. Logically, this
|
berghofe@11622
|
541 |
corresponds to $\bigwedge$ introduction. The name $a$ is used only for
|
berghofe@11622
|
542 |
parsing and printing.
|
berghofe@11622
|
543 |
\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction
|
berghofe@11622
|
544 |
over a {\it proof variable} standing for a proof of proposition $\varphi$
|
berghofe@11622
|
545 |
in the body $prf$. This corresponds to $\Longrightarrow$ introduction.
|
berghofe@11622
|
546 |
\item[$prf$ \% $t$] \index{\%@{\tt\%}|bold}
|
berghofe@11622
|
547 |
is the application of proof $prf$ to term $t$
|
berghofe@11622
|
548 |
which corresponds to $\bigwedge$ elimination.
|
berghofe@11622
|
549 |
\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}|bold}
|
berghofe@11622
|
550 |
is the application of proof $prf@1$ to
|
berghofe@11622
|
551 |
proof $prf@2$ which corresponds to $\Longrightarrow$ elimination.
|
berghofe@11622
|
552 |
\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn
|
berghofe@11622
|
553 |
\cite{debruijn72} index $i$.
|
berghofe@11622
|
554 |
\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level
|
berghofe@11622
|
555 |
hypothesis $\varphi$.
|
berghofe@11622
|
556 |
\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)]
|
berghofe@11622
|
557 |
stands for a pre-proved theorem, where $name$ is the name of the theorem,
|
berghofe@11622
|
558 |
$prf$ is its actual proof, $\varphi$ is the proven proposition,
|
berghofe@11622
|
559 |
and $\overline{\tau}$ is
|
berghofe@11622
|
560 |
a type assignment for the type variables occurring in the proposition.
|
berghofe@11622
|
561 |
\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)]
|
berghofe@11622
|
562 |
corresponds to the use of an axiom with name $name$ and proposition
|
berghofe@11622
|
563 |
$\varphi$, where $\overline{\tau}$ is a type assignment for the type
|
berghofe@11622
|
564 |
variables occurring in the proposition.
|
berghofe@11622
|
565 |
\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)]
|
berghofe@11622
|
566 |
denotes the invocation of an oracle with name $name$ which produced
|
berghofe@11622
|
567 |
a proposition $\varphi$, where $\overline{\tau}$ is a type assignment
|
berghofe@11622
|
568 |
for the type variables occurring in the proposition.
|
berghofe@11622
|
569 |
\item[\ttindexbold{MinProof} $prfs$]
|
berghofe@11622
|
570 |
represents a {\em minimal proof} where $prfs$ is a list of theorems,
|
berghofe@11622
|
571 |
axioms or oracles.
|
berghofe@11622
|
572 |
\end{ttdescription}
|
berghofe@11622
|
573 |
Note that there are no separate constructors
|
berghofe@11622
|
574 |
for abstraction and application on the level of {\em types}, since
|
berghofe@11622
|
575 |
instantiation of type variables is accomplished via the type assignments
|
berghofe@11622
|
576 |
attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}.
|
berghofe@11622
|
577 |
|
paulson@1590
|
578 |
Each theorem's derivation is stored as the {\tt der} field of its internal
|
paulson@1590
|
579 |
record:
|
paulson@1590
|
580 |
\begin{ttbox}
|
berghofe@11622
|
581 |
#2 (#der (rep_thm conjI));
|
berghofe@11622
|
582 |
{\out PThm (("HOL.conjI", []),}
|
berghofe@11622
|
583 |
{\out AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %}
|
berghofe@11622
|
584 |
{\out None % None : Proofterm.proof}
|
paulson@1590
|
585 |
\end{ttbox}
|
berghofe@11622
|
586 |
This proof term identifies a labelled theorem, {\tt conjI} of theory
|
berghofe@11622
|
587 |
\texttt{HOL}, whose underlying proof is
|
berghofe@11622
|
588 |
{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}.
|
berghofe@11622
|
589 |
The theorem is applied to two (implicit) term arguments, which correspond
|
berghofe@11622
|
590 |
to the two variables occurring in its proposition.
|
paulson@1590
|
591 |
|
berghofe@11622
|
592 |
Isabelle's inference kernel can produce proof objects with different
|
berghofe@11622
|
593 |
levels of detail. This is controlled via the global reference variable
|
berghofe@11622
|
594 |
\ttindexbold{proofs}:
|
paulson@1590
|
595 |
\begin{ttdescription}
|
berghofe@11622
|
596 |
\item[proofs := 0;] only record uses of oracles
|
berghofe@11622
|
597 |
\item[proofs := 1;] record uses of oracles as well as dependencies
|
berghofe@11622
|
598 |
on other theorems and axioms
|
berghofe@11622
|
599 |
\item[proofs := 2;] record inferences in full detail
|
paulson@1590
|
600 |
\end{ttdescription}
|
berghofe@11622
|
601 |
Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
|
berghofe@11622
|
602 |
will not work for proofs constructed with {\tt proofs} set to
|
berghofe@11622
|
603 |
{\tt 0} or {\tt 1}.
|
berghofe@11622
|
604 |
Theorems involving oracles will be printed with a
|
berghofe@11622
|
605 |
suffixed \verb|[!]| to point out the different quality of confidence achieved.
|
wenzelm@5371
|
606 |
|
berghofe@7871
|
607 |
\medskip
|
berghofe@7871
|
608 |
|
berghofe@11622
|
609 |
The dependencies of theorems can be viewed using the function
|
berghofe@11622
|
610 |
\ttindexbold{thm_deps}\index{theorems!dependencies}:
|
berghofe@7871
|
611 |
\begin{ttbox}
|
berghofe@7871
|
612 |
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
|
berghofe@7871
|
613 |
\end{ttbox}
|
berghofe@7871
|
614 |
generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
|
berghofe@11622
|
615 |
displays it using Isabelle's graph browser. For this to work properly,
|
berghofe@11622
|
616 |
the theorems in question have to be proved with {\tt proofs} set to a value
|
berghofe@11622
|
617 |
greater than {\tt 0}. You can use
|
berghofe@7871
|
618 |
\begin{ttbox}
|
berghofe@11622
|
619 |
ThmDeps.enable : unit -> unit
|
berghofe@11622
|
620 |
ThmDeps.disable : unit -> unit
|
berghofe@7871
|
621 |
\end{ttbox}
|
berghofe@11622
|
622 |
to set \texttt{proofs} appropriately.
|
berghofe@11622
|
623 |
|
berghofe@11622
|
624 |
\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
|
berghofe@11622
|
625 |
\index{proof terms!reconstructing}
|
berghofe@11622
|
626 |
\index{proof terms!checking}
|
berghofe@11622
|
627 |
|
berghofe@11622
|
628 |
When looking at the above datatype of proofs more closely, one notices that
|
berghofe@11622
|
629 |
some arguments of constructors are {\it optional}. The reason for this is that
|
berghofe@11622
|
630 |
keeping a full proof term for each theorem would result in enormous memory
|
berghofe@11622
|
631 |
requirements. Fortunately, typical proof terms usually contain quite a lot of
|
berghofe@11622
|
632 |
redundant information that can be reconstructed from the context. Therefore,
|
berghofe@11622
|
633 |
Isabelle's inference kernel creates only {\em partial} (or {\em implicit})
|
berghofe@11622
|
634 |
\index{proof terms!partial} proof terms, in which
|
berghofe@11622
|
635 |
all typing information in terms, all term and type labels of abstractions
|
berghofe@11622
|
636 |
{\tt AbsP} and {\tt Abst}, and (if possible) some argument terms of
|
berghofe@11622
|
637 |
\verb!%! are omitted. The following functions are available for
|
berghofe@11622
|
638 |
reconstructing and checking proof terms:
|
berghofe@11622
|
639 |
\begin{ttbox}
|
berghofe@11622
|
640 |
Reconstruct.reconstruct_proof :
|
berghofe@11622
|
641 |
Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
|
berghofe@11622
|
642 |
Reconstruct.expand_proof :
|
berghofe@11622
|
643 |
Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
|
berghofe@11622
|
644 |
ProofChecker.thm_of_proof : theory -> Proofterm.proof -> thm
|
berghofe@11622
|
645 |
\end{ttbox}
|
berghofe@11622
|
646 |
|
berghofe@11622
|
647 |
\begin{ttdescription}
|
berghofe@11622
|
648 |
\item[Reconstruct.reconstruct_proof $sg$ $t$ $prf$]
|
berghofe@11622
|
649 |
turns the partial proof $prf$ into a full proof of the
|
berghofe@11622
|
650 |
proposition denoted by $t$, with respect to signature $sg$.
|
berghofe@11622
|
651 |
Reconstruction will fail with an error message if $prf$
|
berghofe@11622
|
652 |
is not a proof of $t$, is ill-formed, or does not contain
|
berghofe@11622
|
653 |
sufficient information for reconstruction by
|
berghofe@11622
|
654 |
{\em higher order pattern unification}
|
berghofe@11622
|
655 |
\cite{nipkow-patterns, Berghofer-Nipkow:2000:TPHOL}.
|
berghofe@11622
|
656 |
The latter may only happen for proofs
|
berghofe@11622
|
657 |
built up ``by hand'' but not for those produced automatically
|
berghofe@11622
|
658 |
by Isabelle's inference kernel.
|
berghofe@11622
|
659 |
\item[Reconstruct.expand_proof $sg$
|
berghofe@11622
|
660 |
\ttlbrack$name@1$, $\ldots$, $name@n${\ttrbrack} $prf$]
|
berghofe@11622
|
661 |
expands and reconstructs the proofs of all theorems with names
|
berghofe@11622
|
662 |
$name@1$, $\ldots$, $name@n$ in the (full) proof $prf$.
|
berghofe@11622
|
663 |
\item[ProofChecker.thm_of_proof $thy$ $prf$] turns the (full) proof
|
berghofe@11622
|
664 |
$prf$ into a theorem with respect to theory $thy$ by replaying
|
berghofe@11622
|
665 |
it using only primitive rules from Isabelle's inference kernel.
|
berghofe@11622
|
666 |
\end{ttdescription}
|
berghofe@11622
|
667 |
|
berghofe@11622
|
668 |
\subsection{Parsing and printing proof terms}
|
berghofe@11622
|
669 |
\index{proof terms!parsing}
|
berghofe@11622
|
670 |
\index{proof terms!printing}
|
berghofe@11622
|
671 |
|
berghofe@11622
|
672 |
Isabelle offers several functions for parsing and printing
|
berghofe@11622
|
673 |
proof terms. The concrete syntax for proof terms is described
|
berghofe@11622
|
674 |
in Fig.\ts\ref{fig:proof_gram}.
|
berghofe@11622
|
675 |
Implicit term arguments in partial proofs are indicated
|
berghofe@11622
|
676 |
by ``{\tt _}''.
|
berghofe@11622
|
677 |
Type arguments for theorems and axioms may be specified using
|
berghofe@11622
|
678 |
\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
|
berghofe@11622
|
679 |
(see \S\ref{sec:basic_syntax}).
|
berghofe@11622
|
680 |
They must appear before any other term argument of a theorem
|
berghofe@11622
|
681 |
or axiom. In contrast to term arguments, type arguments may
|
berghofe@11622
|
682 |
be completely omitted.
|
berghofe@11622
|
683 |
\begin{ttbox}
|
berghofe@11625
|
684 |
ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
|
berghofe@11625
|
685 |
ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
|
berghofe@11625
|
686 |
ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
|
berghofe@11625
|
687 |
ProofSyntax.print_proof_of : bool -> thm -> unit
|
berghofe@11622
|
688 |
\end{ttbox}
|
berghofe@11622
|
689 |
\begin{figure}
|
berghofe@11622
|
690 |
\begin{center}
|
berghofe@11622
|
691 |
\begin{tabular}{rcl}
|
berghofe@11622
|
692 |
$proof$ & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
|
berghofe@11622
|
693 |
$\Lambda params${\tt .} $proof$ \\
|
berghofe@11622
|
694 |
& $|$ & $proof$ \verb!%! $any$ ~~$|$~~
|
berghofe@11622
|
695 |
$proof$ $\cdot$ $any$ \\
|
berghofe@11622
|
696 |
& $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
|
berghofe@11622
|
697 |
$proof$ {\boldmath$\cdot$} $proof$ \\
|
berghofe@11622
|
698 |
& $|$ & $id$ ~~$|$~~ $longid$ \\\\
|
berghofe@11622
|
699 |
$param$ & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
|
berghofe@11622
|
700 |
{\tt (} $param$ {\tt )} \\\\
|
berghofe@11622
|
701 |
$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
|
berghofe@11622
|
702 |
\end{tabular}
|
berghofe@11622
|
703 |
\end{center}
|
berghofe@11622
|
704 |
\caption{Proof term syntax}\label{fig:proof_gram}
|
berghofe@11622
|
705 |
\end{figure}
|
berghofe@11622
|
706 |
The function {\tt read_proof} reads in a proof term with
|
berghofe@11622
|
707 |
respect to a given theory. The boolean flag indicates whether
|
berghofe@11622
|
708 |
the proof term to be parsed contains explicit typing information
|
berghofe@11622
|
709 |
to be taken into account.
|
berghofe@11622
|
710 |
Usually, typing information is left implicit and
|
berghofe@11622
|
711 |
is inferred during proof reconstruction. The pretty printing
|
berghofe@11622
|
712 |
functions operating on theorems take a boolean flag as an
|
berghofe@11622
|
713 |
argument which indicates whether the proof term should
|
berghofe@11622
|
714 |
be reconstructed before printing.
|
berghofe@11622
|
715 |
|
berghofe@11622
|
716 |
The following example (based on Isabelle/HOL) illustrates how
|
berghofe@11622
|
717 |
to parse and check proof terms. We start by parsing a partial
|
berghofe@11622
|
718 |
proof term
|
berghofe@11622
|
719 |
\begin{ttbox}
|
berghofe@11622
|
720 |
val prf = ProofSyntax.read_proof Main.thy false
|
berghofe@11622
|
721 |
"impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %%
|
berghofe@11622
|
722 |
(Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))";
|
berghofe@11622
|
723 |
{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%}
|
berghofe@11622
|
724 |
{\out AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %}
|
berghofe@11622
|
725 |
{\out None % None % None %% PBound 0 %%}
|
berghofe@11622
|
726 |
{\out AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof}
|
berghofe@11622
|
727 |
\end{ttbox}
|
berghofe@11622
|
728 |
The statement to be established by this proof is
|
berghofe@11622
|
729 |
\begin{ttbox}
|
berghofe@11622
|
730 |
val t = term_of
|
berghofe@11622
|
731 |
(read_cterm (sign_of Main.thy) ("A & B --> B & A", propT));
|
berghofe@11622
|
732 |
{\out val t = Const ("Trueprop", "bool => prop") $}
|
berghofe@11622
|
733 |
{\out (Const ("op -->", "[bool, bool] => bool") $}
|
berghofe@11622
|
734 |
{\out \dots $ \dots : Term.term}
|
berghofe@11622
|
735 |
\end{ttbox}
|
berghofe@11622
|
736 |
Using {\tt t} we can reconstruct the full proof
|
berghofe@11622
|
737 |
\begin{ttbox}
|
berghofe@11622
|
738 |
val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf;
|
berghofe@11622
|
739 |
{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %}
|
berghofe@11622
|
740 |
{\out Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %}
|
berghofe@11622
|
741 |
{\out Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%}
|
berghofe@11622
|
742 |
{\out AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)}
|
berghofe@11622
|
743 |
{\out : Proofterm.proof}
|
berghofe@11622
|
744 |
\end{ttbox}
|
berghofe@11622
|
745 |
This proof can finally be turned into a theorem
|
berghofe@11622
|
746 |
\begin{ttbox}
|
berghofe@11622
|
747 |
val thm = ProofChecker.thm_of_proof Main.thy prf';
|
berghofe@11622
|
748 |
{\out val thm = "A & B --> B & A" : Thm.thm}
|
berghofe@11622
|
749 |
\end{ttbox}
|
berghofe@11622
|
750 |
|
berghofe@11622
|
751 |
\index{proof terms|)}
|
berghofe@11622
|
752 |
\index{theorems|)}
|
berghofe@7871
|
753 |
|
wenzelm@5371
|
754 |
|
wenzelm@5371
|
755 |
%%% Local Variables:
|
wenzelm@5371
|
756 |
%%% mode: latex
|
wenzelm@5371
|
757 |
%%% TeX-master: "ref"
|
wenzelm@5371
|
758 |
%%% End:
|