1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
\DOC term_order
\TYPE {term_order : term -> term -> bool}
\SYNOPSIS
Term order for use in AC-rewriting.
\DESCRIBE
This binary predicate implements a crude but fairly efficient ordering on terms
that is appropriate for ensuring that ordered rewriting will perform
normalization.
\FAILURE
Never fails.
\EXAMPLE
This example shows how using ordered rewriting with this term ordering can give
normalization under associative and commutative laws given the appropriate
rewrites:
{
# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
}
\noindent
{
# TOP_DEPTH_CONV
(FIRST_CONV(map (ORDERED_REWR_CONV term_order) (CONJUNCTS ADD_AC)))
`d + (f + a) + b + (c + e):num`;;
val it : thm = |- d + (f + a) + b + c + e = a + b + c + d + e + f
}
\USES
It is used automatically when applying permutative rewrite rules inside
rewriting and simplification. Users will not normally want to use it
explicitly, though the example above shows roughly what goes on there.
\SEEALSO
ORDERED_IMP_REWR_CONV, ORDERED_REWR_CONV.
\ENDDOC
|
