res_quan/Manual/description.tex

3 \chapter{The \resquan\ Library}
5 The \resquan\ library provides some basic facilities for working with
12 The description in this chapter begins with a brief introduction to
16 manual for all ML functions appears in Chapter~2. The last chapter
29 The qualifier {\small\verb|::|} can be used with {\small\verb|\|} and any
30 binder, including user defined ones. The appropriate meanings are
42 The constants \con{RES\_ABSTRACT}, \con{RES\_FORALL}, \con{RES\_EXISTS} and
89 The flag \ml{print\_restrict} has default \ml{true}, but if set to
117 The syntax for restricted quantification provides a method of
125 \section{The theory {\tt res\_quan.{}th}}
129 The following four theorems state the distributivity property of these
149 The theorems \ml{RESQ\_FORALL\_REORDER} and \ml{RESQ\_EXISTS\_REORDER}
160 The theorem \ml{RESQ\_FORALL\_FORALL} states the reordering property of
171 The ML functions available when this library is loaded can be divided
178 The conditional rewriting tools are not specific for restricted
186 The conditional rewriting tools consists of a simple tactic which is
203 conjunctions. The idea of  conditional rewriting is that the
208 The ML function \ml{COND\_REWR\_CANON} transforms a theorem
209 into the canonical form in~\ref{eq-cond-thm}. The antecedents of the
226 The basic conditional rewriting tactic is
243 The theorem $th$ supplied to \ml{COND\_REWRITE1\_TAC} is processed by
244 \ml{COND\_REWR\_CANON} first. The resulting theorem is passed to the low
249 implemented. The details of the tactics and search functions can be
256 The basic conditional rewriting conversion is
263 rewriting tactics. The difference is that the instances of the
264 antecedents are added to the list of assumptions of the resulting theorem. The
299 The introduction and elimination rules for the restricted universal
301 to the rules for the universal quantifier. The specification of these
341 The rule for eliminating restricted existential quantification is
350 The function \ml{RESQ\_MATCH\_MP} eliminates a restricted universal
360 universal quantification. The conversion \ml{RESQ\_FORALL\_CONV}
368 The ML function
369 \ml{IMP\_RESQ\_FORALL\_CONV} performs the reverse conversion. The ML
374 The conversions \ml{RESQ\_FORALL\_AND\_CONV} and
377 The conversion \linebreak\ml{RESQ\_FORALL\_SWAP\_CONV} changes the order of two
390 The conversion \ml{RESQ\_EXISTS\_CONV} transforms a restricted
416 The simple tactics \ml{RESQ\_GEN\_TAC} and \ml{RESQ\_EXISTS\_TAC} are
422 The resolution tactics and tactical listed below are in analogy to
433 The theorem-tactic \ml{RESQ\_IMP\_RES\_TAC} uses a restricted universally
439 The theorem-tactic \ml{RESQ\_REWRITE1\_TAC} uses a restricted universally
447 gln}. The main subgoal {\tt gl0} is obtained by replacing instances of
448 $u$ in {\tt gl} with corresponding instances of $v$. The new subgoals
462 The constant \con{C} may be an ordinary constant, or it may have
463 either `infix' or `binder' status. The ML functions for defining
477 the name \verb|C_DEF| in the current theory. The definition is