Filter
Top Products
74 CHAPTER 9. DERIVED RULES
9.2 Rewriting and simplification
HOL has various rules and conversions at a somewhat higher level. Some of the
most useful of these automatically work out how to instantiate variables to apply to
the case in hand. For example, the above ‘Modus Ponens’ rule requires the theorems
to match up exactly:
2
#MP (ASSUME ‘x < 1 ==> x <= 1‘) (ASSUME ‘x < 1‘);;
it : thm = x > 1 ==> x >= 1, x >= 1 |- x > 1
#MP (ASSUME ‘y < 1 ==> y <= 1‘) (ASSUME ‘x < 1‘);;
Uncaught exception: Failure "MP: theorems do not agree"
A more powerful rule, MATCH MP, tries to work out settings for free or universally
quantified variables in the first theorem in order to make things match up. we can
illustrate this using a built-in theorem LT IMP LE:
#let th1 = LT_IMP_LE;;
th1 : thm = |- !m n. m < n ==> m <= n
#MATCH_MP th1 (ASSUME ‘x < 1‘);;
it : thm = x < 1 |- x <= 1
A similar rule, actually a conversion, is REWR CONV. It takes an equation, perhaps
universally quantified, and sets the variables if possible so that the left-hand side
matches the proffered term, ‘rewriting’ it. Again, we will illustrate it using a built-in
theorem:
#let th1 = NOT_LE;;
th1 : thm = |- !m n. ~(m <= n) = n < m
#REWR_CONV th1 ‘~(x + 1 <= x)‘;;
it : thm = |- ~(x + 1 <= x) = x < x + 1
Since it is a conversion, REWR CONV can be combined with various depth con-
versions to rewrite repeatedly at various levels of a term. Built-in functions like
REWRITE CONV take a whole list of theorems, extract rewrites from them and re-
peatedly apply them to a term.
3
Moreover, they throw in a set of handy rewrites to
get rid of trivial propositional clutter, e.g. reducing p /\ p to p. They are one of
the workhorses in typical HOL proofs. If the additional propositional simplifications
are not required, prefix the name with PURE:
#PURE_REWRITE_CONV[NOT_LE; LT_REFL] ‘~(x < x) \/ q‘;;
it : thm = |- ~(x < x) \/ q = ~F \/ q
#REWRITE_CONV[NOT_LE; LT_REFL] ‘~(x < x) \/ q‘;;
it : thm = |- ~(x < x) \/ q = T
As in this example, one often rewrites Boolean terms. In cases where conversions
are applied to Boolean terms, it’s often handy to convert conversions to forward
inference rules. This is done using CONV RULE, whose definition is simply:
#let CONV_RULE conv th =
EQ_MP (conv(concl th)) th;;
CONV_RULE : (term -> thm) -> thm -> thm = <fun>
#CONV_RULE(REWRITE_CONV[NOT_LE; LT_REFL]) (ASSUME ‘~(x < x) \/ q‘);;
it : thm = ~(x < x) \/ q |- T
2
Actually, only up to alpha-equivalence, i.e. renaming of bound variables.
3
They do work by applying REWR CONV at depth, but are optimized using term nets to avoid too
many wasteful attempts to match theorems against subterms.