GEN_REWRITE_RULE : ((conv -> conv) -> rewrites -> thm list -> thm -> thm)
Equations used in rewriting are obtained from the theorem lists given as arguments to the function. These are at first transformed into a form suitable for rewriting. Conjunctions are separated into individual rewrites. Theorems with conclusions of the form "~t" are transformed into the corresponding equations "t = F". Theorems "t" which are not equations are cast as equations of form "t = T".
If a theorem is used to rewrite the object theorem, its assumptions are added to the assumptions of the returned theorem, unless they are alpha-convertible to existing assumptions. The matching involved uses variable instantiation. Thus, all free variables are generalized, and terms are instantiated before substitution. Theorems may have universally quantified variables.
The theorems with which rewriting is done are divided into two groups, to facilitate implementing other rewriting tools. However, they are considered in an order-independent fashion. (That is, the ordering is an implementation detail which is not specified.)
The search strategy for finding matching subterms is the first argument to the rule. Matching and substitution may occur at any level of the term, according to the specified search strategy: the whole term, or starting from any subterm. The search strategy also specifies the depth of the search: recursively up to an arbitrary depth until no matches occur, once over the selected subterm, or any more complex scheme.
thm = |- (1 + 2) + 3 = (3 + 1) + 2
GEN_REWRITE_RULE (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [ADD_SYM] mythm
As another example, REWRITE_RULE could be implemented as
GEN_REWRITE_RULE TOP_DEPTH_CONV (implicit_rewrites())