Filter
Top Products
9.4. HIGHER ORDER MATCHING 77
#CONJ_ACI;;
it : thm =
|- (p /\ q = q /\ p) /\
((p /\ q) /\ r = p /\ q /\ r) /\
(p /\ q /\ r = q /\ p /\ r) /\
(p /\ p = p) /\
(p /\ p /\ q = p /\ q)
#REWRITE_CONV[CONJ_ACI] ‘p /\ q /\ p /\ r /\ q = r /\ q /\ p‘;;
it : thm = |- (p /\ q /\ p /\ r /\ q = r /\ q /\ p) = T
9.4 Higher order matching
HOL Light supports a limited form of higher order matching. This is immensely
useful in order to express more general term transformations as rewrite rules. If
only simple ‘first order’ matching is used, the scope of rewriting, matching modus
ponens etc. is rather restricted. Even quite simple schematic theorems need to be
instantiated manually — a very tedious task. For example, if we want to use the
theorem:
#SKOLEM_THM;;
it : thm = |- !P. (!x. ?y. P x y) = (?y. !x. P x (y x))
to rewrite the term !n. ?m. m EXP 2 <= n /\ n < (SUC m) EXP 2, then simple
rewriting won’t work; one first needs to instantiate the theorem with
P = (\n m. m EXP 2 <= n /\ n < (SUC m) EXP 2)
then beta-reduce it, and only then rewrite with it. HOL Light will do this automat-
ically in some situations. For example, it will perform the following rewrite, even
though the term isn’t literally an instance of the theorem’s left hand side:
#NOT_FORALL_THM;;
it : thm = |- !P. ~(!x. P x) = (?x. ~P x)
#REWR_CONV NOT_FORALL_THM ‘~(!n. n < n - 1)‘;;
it : thm = |- ~(!n. n < n - 1) = (?n. ~(n < n - 1))
The implementation of higher order matching aims to make matching as gen-
eral as possible while keeping it deterministic. It allows higher order matches of
P x
1
· ·· x
n
where P is an instantiable variable, but only if it can decide with cer-
tainty how to instantiate the x
i
. Generally speaking, there are lots of possible
higher order matches; for example the pattern P(x + y) can be matched against
(a + b) + (c + d) in several different ways, e.g. x = a + b, y = c + d or x = a, y = b.
In order to make the matches determinate, information is taken from corresponding
variable bindings. For example there is no doubt about the matching of ∀x. Px
to ∀n. n < n + 1, whereas with the bound variables removed one could have var-
ious alternatives, e.g. P = λx. n < x + 1 and x = n. Our allowable patterns
correspond quite closely to higher order patterns, for which Miller (1991) proved
even the unification (two-way matching) problem to be decidable and deterministic
(‘unitary’). We generalize higher order patterns in two ways. First, one need not
simply have variables in the patterns, but can have arbitrary terms involving only
these ‘resolvable’ variables. Thus one can match:
|- (!x. P(SUC x)) = !x. 0 < x ==> P x
with a term: