Filter
Top Products
96 CHAPTER 12. MATHEMATICAL THEORIES
REVERSE =
|- (REVERSE [] = []) /\ (REVERSE (CONS x l) = APPEND (REVERSE l) [x])
LENGTH =
|- (LENGTH [] = 0) /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))
MAP = |- (!f. MAP f [] = []) /\
(!f h t. MAP f (CONS h t) = CONS (f h) (MAP f t))
LAST = |- LAST (CONS h t) = (if t = [] then h else LAST t)
REPLICATE = |- (REPLICATE 0 x = []) /\
(REPLICATE (SUC n) x = CONS x (REPLICATE n x))
NULL = |- (NULL [] = T) /\ (NULL (CONS h t) = F)
FORALL = |- (FORALL P [] = T) /\
(FORALL P (CONS h t) = P h /\ FORALL P t)
EX = |- (EX P [] = F) /\ (EX P (CONS h t) = P h \/ EX P t)
ITLIST =
|- (ITLIST f [] b = b) /\ (ITLIST f (CONS h t) b = f h (ITLIST f t b))
MEM = |- (MEM x [] = F) /\ (MEM x (CONS h t) = (x = h) \/ MEM x t)
A somewhat ad hoc collection of facts about these functions is collected, for
example:
APPEND_ASSOC = |- !l m n. APPEND l (APPEND m n) = APPEND (APPEND l m) n
LENGTH_APPEND = |- !l m. LENGTH (APPEND l m) = LENGTH l + LENGTH m
LENGTH_MAP = |- !l f. LENGTH (MAP f l) = LENGTH l
REVERSE_REVERSE = |- !l. REVERSE (REVERSE l) = l
MAP_o = |- !f g l. MAP (g o f) l = MAP g (MAP f l)
NOT_EX = |- !P l. ~EX P l = FORALL (\x. ~P x) l
12.4 Well-founded relations
Wellfoundedness of a binary relation can be expressed in many equivalent ways.
HOL Light includes a definition of wellfoundedness and a proof that it equivalent
to several other important properties, like the admissibility of complete induction
and wellfounded recursion. For example, the last theorem below, which also has a
converse, says that one can define recursive functions provided the value of f(x) is
defined in terms of f(y) for y below x in the wellfounded ordering.
WF =
|- WF (<<) = (!P. (?x. P x) ==> (?x. P x /\ (!y. y << x ==> ~P y)))