Filter
Top Products
12.5. REAL NUMBERS 97
WF_IND =
|- WF (<<) = (!P. (!x. (!y. y << x ==> P y) ==> P x) ==> (!x. P x))
WF_DCHAIN = |- WF (<<) = ~(?s. !n. s (SUC n) << s n)
WF_REC =
|- WF (<<)
==> (!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
==> (?f. !x. f x = H f x))
12.5 Real numbers
HOL Light constructs the real numbers and then proves various properties of them.
Algebraic trivialities include:
REAL_OF_NUM_SUB : thm = |- !m n. m <= n ==> (&n - &m = &(n - m))
REAL_ADD_RID : thm = |- !x. x + &0 = x
REAL_LT_IMP_LE : thm = |- !x y. x < y ==> x <= y
REAL_LT_LADD_IMP : thm = |- !x y z. y < z ==> x + y < x + z
REAL_LT_LNEG : thm = |- !x y. -- x < y = &0 < x + y
REAL_ABS_TRIANGLE : thm = |- !x y. abs (x + y) <= abs x + abs y
REAL_ABS_MUL : thm = |- !x y. abs (x * y) = abs x * abs y
REAL_INV_MUL : thm = |- !x y. inv (x * y) = inv x * inv y
Note that the inverse is defined with 0
−1
= 0. Most theorems not involving
multiplication can be proved automatically using REAL ARITH or the tactic form
REAL ARITH TAC:
#REAL_ARITH ‘abs(x) < y ==> x < y‘;;
it : thm = |- abs x < y ==> x < y
The key higher-order property of the reals asserts that any nonempty bounded
set of reals has a least upper bound:
#REAL_COMPLETE;;
it : thm =
|- !P. (?x. P x) /\ (?M. !x. P x ==> x <= M)
==> (?M. (!x. P x ==> x <= M) /\
(!M’. (!x. P x ==> x <= M’) ==> M <= M’))
There is not much real analysis in the basic system, but there is a reasonable
development included with the examples.
12.6 Integers
A theory of integers is also available, with theorems named by analogy with the
reals, e.g. INT LT IMP LE rather than REAL LT IMP LE. Similarly, there is a decision
procedure for linear integer arithmetic called INT ARITH.