Structure Opening

Source File Identifier index Theory binding index

signature Opening = sig

(* ----------------------------------------------------------------------
* CONGPROC
*
* INPUTS
*    The first argument should be a function implementing reflexivity
* for the congruence relation (e.g. REFL for equality).  For any
* reflexivity theorem you can make this easily by:
*    fun refl x = SPEC x thm;
*
*    The second should be the congruence theorem for the relation
*    Providing these two returns a function which implements a
* congruence rule suitable for use with the TRAVERSE engine.
* Create a congruence procedure for a given congruence rule.
*
* "CONGRUENCE" PROCEDURES
*   - Use the given continuation to derive simplified subterms
*   - Use the provided solver to solve side conditions (solver
* is normally just ASSUME)
*   - Rename abstractions to avoid certain variables. (only implemented
* for EQ_CONGPROC at present).
*
* NOTES FROM THE SIMPLIFIER DOCUMENTATION
*
* Arbitrary extra contextual information can be introduced by
* using "congurence rules".  These are theorems of a particular
* shape.
*
* The general form must be:
* \begin{verbatim}
* |- !x1 x1' ... xn xn'.
*      side-condition1 ==>
*      side-condition2 ==>
*      (!v11...v1m. x1 v11 ... v1m REL x1' v11 ... v1m) ==>
*      (!v21...v2m. [P[x1',v21,...v2m] ==>] x2 v21 ... v2m REL
*                                           x2' v21 ... v2m) ==>
*      ...
*      F[x1,x2,..,xn] REL F[x1',x2',..,xn']
* \end{verbatim}
* That probably doesn't make much sense.  Think of F as the construct
* over which you are expressing the congruence.  Think of x1,x2,...xn
* as the sub-constructs which are being rewritten, some of them under
* additional assumptions.  The implications (one on each line in the
* sample above) state the necessary results which need to be derived
* about the subcomponents before the congruence can be deduced.  Some
* of these subcomponenets may be simplified with extra assumpions - this
* is indicated by P[x1] above.
*
* Some subterms may be functions which we want
* to rewrite under application. See the rule for restricted
* quantifiers for examples.
* The simplifier does a degree of higher order matching when
* these variables are specified.
*
* Some examples (where REL is HOL equality)
* \begin{verbatim}
*  |- !g g' t t' e e'.
*        (g = g') ==>
*        (g ==> (t = t')) ==>
*        (~g ==> (e = e')) ==>
*        ((g => t | e) = (g' => t' | e')) : thm
*
*   |- !P P' Q Q'.
*        (!x. P x = P' x) ==>
*        (!x. P x ==> (Q x = Q' x)) ==>
*        (RES_EXISTS P Q = RES_EXISTS P' Q') : thm
* \end{verbatim}
*
* ---------------------------------------------------------------------*)

include Abbrev
type congproc = {relation: term,
solver : term -> thm,
freevars: term list,
depther : (thm list * term) -> conv} -> conv
val samerel            : term -> term -> bool
val CONGPROC           : ({Rinst:term,arg:term} -> thm) -> thm -> congproc
val rel_of_congrule    : thm -> term
val nconds_of_congrule : thm -> int

(* ---------------------------------------------------------------------
* EQ_CONGPROC
*
* Optimized implementations of the HOL equality congruence rules using the
* built in operations AP_TERM, AP_THM, MK_ABS and MK_COMB.  These could
* conceivably be implemented by:
*     (x = x') ==> (f = f') ==> (f x = f' x')
*     (b = b') ==> (\x. b) = (\x. b')
* ---------------------------------------------------------------------*)

val EQ_CONGPROC : congproc

end (* sig *)



Source File Identifier index Theory binding index