Filter
Top Products
Chapter 12
Mathematical theories
To prove theorems in HOL Light, one needs a reasonable grasp of the theorem
proving infrastructure. But equally important is knowing what has already been
proved, and what the theorem one is after has been called. The following is not an
exhaustive list, but gives some of the main theorems, grouped according to subject
area. The following gives only a general overview; the reader should browse the
source files to become more familiar with what is available.
12.1 Pairs
There is a type constructor prod that constructs Cartesian product types. In the
concrete syntax of the type parser it is written as #. For example num # num is
the type of pairs of natural numbers. Larger tuples can be built by iterating the
pairing operation; the type constructor and the term function that constructs pairs
(the infix comma) are both right associative. Destructors FST and SND are defined.
Some of the main theorems about pairs are:
PAIR_EQ = |- !x y a b. (x,y = a,b) = (x = a) /\ (y = b)
PAIR_SURJECTIVE = |- !p. ?x y. p = x,y
FST = |- !x y. FST (x,y) = x
SND = |- !x y. SND (x,y) = y
PAIR = |- !x. FST x,SND x = x
pair_INDUCT = |- (!x y. P (x,y)) ==> (!p. P p)
pair_RECURSION = |- !PAIR’. ?fn. !a0 a1. fn (a0,a1) = PAIR’ a0 a1
The last two are chosen as if pairs had been defined as a recursive type, though
in fact they logically precede other recursive types.
12.2 Natural numbers
The type of natural numbers is carved out, using an inductive definition, from the
infinite type ind. The Peano axioms are derived from the definition and the axioms
of infinity. As with pairs, two theorems mimic those resulting from recursive type
definitions, allowing proofs by induction and definitions by primitive recursion:
93