Filter
Top Products
9.3. ORDERED REWRITING 75
Some conversions are made into rules and given names, because they are used
so often. For example:
#let BETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV);;
BETA_RULE : thm -> thm = <fun>
#let REWRITE_RULE thl = CONV_RULE(REWRITE_CONV thl);;
REWRITE_RULE : thm list -> thm -> thm = <fun>
Still more powerful than rewriting is simplification. This allows the use of equa-
tions that are conditional, i.e. of the form p ⇒ l = r. After matching up l
with the term if possible, setting the theorem to p
⇒ l
= r
the conversion is
recursively applied to the hypothesis p
, trying to reduce it to and so eliminate
it. This can often avoid tedious chains of straightforward logical reasoning. For
example, in
#DIV_LT;;
it : thm = |- !m n. m < n ==> (m DIV n = 0)
#SIMP_CONV[DIV_LT; ARITH] ‘3 DIV 7 = 0‘;;
it : thm = |- (3 DIV 7 = 0) = T
the built-in theorem DIV LT is used as a rewrite, giving a hypothesis 3 < 7 which
is then attacked by more simplification, this time using a set of rewrites to do
basic arithmetic (described later). Simplification also accumulates context, so when
traversing a term p ⇒ q and descending to q, additional rewrites are derived from
p, e.g.
#SIMP_CONV [] ‘p /\ q ==> p‘;;
it : thm = |- p /\ q ==> p = T
The rewrite p = T is extracted from the context p and this is used to rewrite
the consequent to T. The final result follows from an additional rewrite with the
built-in simplification p ==> T = T.
9.3 Ordered rewriting
It is possible for rewriting and simplification to go into an infinite loop, e.g. applying
two successive rewrites s = t and t = s alternately. However, HOL tries to avoid
looping in some cases, ignoring rewrites that would loop:
#REWRITE_CONV[ASSUME ‘x = x + 1‘] ‘x:num‘;;
Warning: discarding looping rewrite
it : thm = |- x = x
Some rewrites are said to be permutative, meaning that the left hand side can
be matched to the right hand side and vice versa. For example, there is a built-in
theorem ADD SYM asserting that addition of natural numbers is commutative, and
several others:
#ADD_SYM;;
it : thm = |- !m n. m + n = n + m
#CONJ_SYM;;
it : thm = |- !t1 t2. t1 /\ t2 = t2 /\ t1
#INSERT_COMM;;
it : thm = |- !x y s. x INSERT y INSERT s = y INSERT x INSERT s