ORDERED_REWR_CONV : (term -> term -> bool) -> thm -> term -> thm
Basic rewriting conversion restricted by term order.
Given an ordering relation ord, an equational theorem A |- !x1...xn. s = t
that expresses a rewrite rule, the conversion ORDERED_REWR_CONV gives a
conversion that applied to any term s' will attempt to match the left-hand
side of the equation s = t to s', and return the corresponding theorem A
|- s' = t', but only if ord `s'` `t'`, i.e. if the left-hand side is
``greater'' in the ordering than the right-hand side, after instantiation. If
the ordering condition is violated, it will fail, even if the match is fine.
- FAILURE CONDITIONS
Fails if the theorem is not of the right form or the two terms cannot be
matched, for example because the variables that need to be instantiated are
free in the hypotheses A, or if the ordering requirement fails.
We apply the permutative rewrite:
with the default term ordering term_order designed for this kind of
application. Note that it applies in one direction:
val it : thm = |- !m n. m + n = n + m
but not the other:
# ORDERED_REWR_CONV term_order ADD_SYM `1 + 2`;;
val it : thm = |- 1 + 2 = 2 + 1
# ORDERED_REWR_CONV term_order ADD_SYM `2 + 1`;;
Exception: Failure "ORDERED_REWR_CONV: wrong orientation".
Applying conditional rewrite rules that are permutative and would loop without
some restriction. Thanks to the fact that higher-level rewriting operations
like REWRITE_CONV and REWRITE_TAC have ordering built in for permutative
rewrite rules, rewriting with theorem like ADD_AC will effectively normalize
- SEE ALSO
IMP_REWR_CONV, ORDERED_IMP_REWR_CONV, REWR_CONV, SIMP_CONV, term_order.