Filter
Top Products
1.3. DERIVED RULES 5
While the user can enter any (typeable) term in quotations and have it elevated
to a HOL term, it is not possible to do this with theorems. While there’s a com-
putable procedure for deciding if a term is well-typed, HOL has no way in general of
deciding whether it is possible to construct a theorem from the primitive functions.
However, there are some high-level functions that accept a term of a certain form
and prove it automatically, turning it into a theorem. For example ARITH RULE can
prove many basic facts of natural number arithmetic:
#ARITH_RULE ‘2 * x < 2 * (x + 1)‘;;
it : thm = |- 2 * x < 2 * (x + 1)
Note, however, that the theorem is still created under the surface by a (some-
times quite lengthy) series of applications of the primitive rules, maintaining the
guarantee of reliability.
1.3 Derived rules
In general, an inference rule in HOL is simply any ML function that return a theorem
or theorems (objects with ML type thm). Ones like ARITH RULE that turn claims
into theorems are particularly simple to use, but in general HOL inference rules
may require other theorems as input. For example MK COMB accepts two theorems
as input, one saying that two functions (say f and g) are equal, the other saying
two arguments (say x and y) are equal, and if the types match up correctly so it
makes sense to apply f to x and g to y, MK COMB returns a theorem saying that f(x)
and g(y) are equal.
#let th1 = ASSUME ‘f:num->num = g‘;;
th1 : thm = f = g |- f = g
#let th2 = ASSUME ‘m:num = n‘;;
th2 : thm = m = n |- m = n
#MK_COMB(th1,th2);;
it : thm = f = g, m = n |- f m = g n
HOL rules can be separated into the primitive rules like REFL, ASSUME and
MK COMB, of which there are ten, and all the others, which are called derived rules,
since they are built up from the primitives. A lot of HOL Light’s source code is a
systematic building up of a useful set of higher-level derived rules, and the use of
the rules, primitive and derived, to prove useful mathematical theorems. Here is a
very simple but genuine example, one of HOL Light’s simplest inbuilt derived rules
called AP TERM. It accepts a term representing a function f and a theorem asserting
that x and y are equal, and if the types match up, returns a theorem asserting that
f(x) = f(y):
#let AP_TERM tm th =
MK_COMB(REFL tm,th);;
AP_TERM : term -> thm -> thm = <fun>
#AP_TERM ‘h:num->num‘ (ASSUME ‘m = 1‘);;
it : thm = m = 1 |- h m = h 1
The definition of AP TERM is a simple 2-line ML program, which first derives
the trivial theorem that the function is equal to itself, using REFL, and then calls
MK COMB to get the final result. Note that this just expresses generically the way
one would prove such a theorem given only the primitive rules to work with. A
derived rule doesn’t yield a single theorem, but rather a whole family of theorems