Package real-def: Definition of the real numbers

Information

namereal-def
version1.63
descriptionDefinition of the real numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-11-10
requiresbool
function
natural
pair
set
showData.Bool
Data.Pair
Function
Number.Natural as Natural
Number.Real
Set

Files

Defined Type Operator

Defined Constants

Theorems

x. x x

x. 0 + x = x

x. x 0 = 1

x. ~x + x = 0

x. 1 * x = x

x y. x > y y < x

x y. x y y x

x y. x * y = y * x

x y. x + y = y + x

x y. x y y x

x y. x < y ¬(y x)

x y. x - y = x + ~y

m n. fromNatural m = fromNatural n m = n

m n. fromNatural m fromNatural n Natural.≤ m n

x. abs x = if 0 x then x else ~x

m n. fromNatural m * fromNatural n = fromNatural (Natural.* m n)

m n. fromNatural m + fromNatural n = fromNatural (Natural.+ m n)

x n. x Natural.suc n = x * x n

m n. max m n = if m n then n else m

m n. min m n = if m n then m else n

x y. x y y x x = y

x y z. y z x + y x + z

x y z. x * (y * z) = x * y * z

x y z. x + (y + z) = x + y + z

x y z. x y y z x z

x. ¬(x = 0) inv x * x = 1

x y. ¬(y = 0) x / y = x * inv y

x y z. x * (y + z) = x * y + x * z

x y. 0 x 0 y 0 x * y

s x. ¬(s = ) (m. x. x s x m) x s x sup s

s m.
    ¬(s = ) (m. x. x s x m) (x. x s x m) sup s m

Input Type Operators

Input Constants

Assumptions

¬

¬

Natural.bit0 0 = 0

t. t t

n. Natural.≤ 0 n

n. Natural.≤ n n

p. p

x. id x = x

t. t ¬t

m. ¬Natural.< m 0

n. ¬Natural.< n n

(¬) = λp. p

() = λp. p ((select) p)

a. x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(Natural.suc n = 0)

n. Natural.* 0 n = 0

m. Natural.* m 0 = 0

n. Natural.+ 0 n = n

m. Natural.+ m 0 = m

n. Natural.distance 0 n = n

n. Natural.distance n 0 = n

n. Natural.distance n n = 0

t. ( t) ¬t

t. t ¬t

n. Natural.bit1 n = Natural.suc (Natural.bit0 n)

m. Natural.* m 1 = m

m. Natural.* 1 m = m

x. (select y. y = x) = x

m n. Natural.≤ m (Natural.+ m n)

m n. Natural.≤ n (Natural.+ m n)

() = λp q. p q p

t. (t ) (t )

m. Natural.suc m = Natural.+ m 1

m. Natural.≤ m 0 m = 0

xy. (fst xy, snd xy) = xy

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

x y. fst (x, y) = x

x y. snd (x, y) = y

p x. p x p ((select) p)

n.
    Natural.bit0 (Natural.suc n) =
    Natural.suc (Natural.suc (Natural.bit0 n))

f y. (let x y in f x) = f y

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

a b. (a b) a b

m n. Natural.* m n = Natural.* n m

m n. Natural.+ m n = Natural.+ n m

m n. Natural.distance m n = Natural.distance n m

m n. m = n Natural.≤ m n

m n. Natural.< m n Natural.≤ m n

m n. Natural.≤ m n Natural.≤ n m

m n. Natural.≤ (Natural.distance m n) (Natural.+ m n)

m n. Natural.distance m (Natural.+ m n) = n

m n. Natural.distance (Natural.+ m n) m = n

n. Natural.* 2 n = Natural.+ n n

m n. ¬Natural.< m n Natural.≤ n m

m n. ¬Natural.≤ m n Natural.< n m

m n. Natural.≤ (Natural.suc m) n Natural.< m n

s. (x. x s) ¬(s = )

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

m n. Natural.+ m (Natural.suc n) = Natural.suc (Natural.+ m n)

m n. Natural.+ (Natural.suc m) n = Natural.suc (Natural.+ m n)

m n. Natural.suc m = Natural.suc n m = n

m n. Natural.distance m n = 0 m = n

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. Natural.* m (Natural.suc n) = Natural.+ m (Natural.* m n)

m n. Natural.* (Natural.suc m) n = Natural.+ (Natural.* m n) n

m n. ¬(n = 0) Natural.< (Natural.mod m n) n

p. (xy. p xy) x y. p (x, y)

m n. Natural.≤ m n d. n = Natural.+ m d

a b. (n. Natural.≤ (Natural.* a n) b) a = 0

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

p. (x y. p x y) y x. p x y

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

m n. Natural.< m (Natural.suc n) m = n Natural.< m n

p q. (x. p x q) (x. p x) q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p.
    Natural.≤ (Natural.distance m p)
      (Natural.+ (Natural.distance m n) (Natural.distance n p))

m n p. Natural.* m (Natural.* n p) = Natural.* n (Natural.* m p)

m n p. Natural.* m (Natural.* n p) = Natural.* (Natural.* m n) p

m n p. Natural.+ m (Natural.+ n p) = Natural.+ (Natural.+ m n) p

m n p. Natural.+ m n = Natural.+ m p n = p

m n p. Natural.≤ (Natural.+ m n) (Natural.+ m p) Natural.≤ n p

m n p. Natural.≤ (Natural.+ m p) (Natural.+ n p) Natural.≤ m n

m n p.
    Natural.distance (Natural.+ m n) (Natural.+ m p) = Natural.distance n p

m n p. Natural.≤ m n Natural.≤ n p Natural.≤ m p

p x. (y. p y y = x) (select) p = x

p. (x. y. p x y) y. x. p x (y x)

m n. Natural.≤ m (Natural.suc n) m = Natural.suc n Natural.≤ m n

m n. Natural.+ m n = 0 m = 0 n = 0

p. p 0 (n. p n p (Natural.suc n)) n. p n

p q r. p q r (p q) (p r)

m n p.
    Natural.* m (Natural.+ n p) = Natural.+ (Natural.* m n) (Natural.* m p)

m n p.
    Natural.* m (Natural.distance n p) =
    Natural.distance (Natural.* m n) (Natural.* m p)

m n p.
    Natural.* (Natural.+ m n) p = Natural.+ (Natural.* m p) (Natural.* n p)

p m n.
    Natural.* (Natural.distance m n) p =
    Natural.distance (Natural.* m p) (Natural.* n p)

(∃!) = λp. () p x y. p x p y x = y

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

p q. (x. p x) (x. q x) x. p x q x

e f. ∃!fn. fn 0 = e n. fn (Natural.suc n) = f (fn n) n

a b c.
    (n. Natural.≤ (Natural.* a n) (Natural.+ (Natural.* b n) c))
    Natural.≤ a b

m n.
    ¬(n = 0)
    Natural.+ (Natural.* (Natural.div m n) n) (Natural.mod m n) = m

m n p. Natural.≤ (Natural.* m n) (Natural.* m p) m = 0 Natural.≤ n p

m n p. Natural.≤ (Natural.* m p) (Natural.* n p) Natural.≤ m n p = 0

x y a b. (x, y) = (a, b) x = a y = b

m n p q.
    Natural.≤ (Natural.distance m p)
      (Natural.+ (Natural.distance (Natural.+ m n) (Natural.+ p q))
         (Natural.distance n q))

m n p q.
    Natural.< m p Natural.< n q
    Natural.< (Natural.+ m n) (Natural.+ p q)

m n p q.
    Natural.≤ m n Natural.≤ p q
    Natural.≤ (Natural.* m p) (Natural.* n q)

m n p q.
    Natural.≤ m p Natural.≤ n q
    Natural.≤ (Natural.+ m n) (Natural.+ p q)

m n p q.
    Natural.≤ (Natural.distance (Natural.+ m n) (Natural.+ p q))
      (Natural.+ (Natural.distance m p) (Natural.distance n q))

m n p.
    Natural.≤ (Natural.distance m n) p
    Natural.≤ m (Natural.+ n p) Natural.≤ n (Natural.+ m p)

p c x y. p (if c then x else y) (c p x) (¬c p y)

p.
    (b. n. Natural.≤ (p n) b)
    a b. n. Natural.≤ (Natural.* n (p n)) (Natural.+ (Natural.* a n) b)

p.
    (n. p n) (m. n. p n Natural.≤ n m)
    m. p m n. p n Natural.≤ n m

p q.
    (b. i. Natural.≤ (p i) (Natural.+ (q i) b))
    b n. i. Natural.≤ n i Natural.≤ (p i) (Natural.+ (q i) b)

m n p q r s.
    Natural.≤ (Natural.distance m n) r
    Natural.≤ (Natural.distance p q) s
    Natural.≤ (Natural.distance m p)
      (Natural.+ (Natural.distance n q) (Natural.+ r s))

p a b.
    p 0 0 = 0
    (m n. Natural.≤ (p m n) (Natural.+ (Natural.* a (Natural.+ m n)) b))
    c. m n. Natural.≤ (p m n) (Natural.* c (Natural.+ m n))