Package real: The real numbers

Information

namereal
version1.24
descriptionThe real numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
pair
natural
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. exp 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

x y. x / y = x * inv 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. exp x (Natural.suc n) = x * exp 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 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

p.
    (x. p x) (m. x. p x x m)
    s. (x. p x x s) m. (x. p x x m) s m

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

Natural.bit0 0 = 0

t. t t

n. Natural.≤ 0 n

n. Natural.≤ n n

F p. p

x. id x = x

t. t ¬t

n. ¬Natural.< n n

(¬) = λp. p F

() = λ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. F t F

t. T t t

t. t T t

t. t t t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

n. ¬(Natural.suc n = 0)

m. Natural.< m 0 F

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. (F t) ¬t

t. t F ¬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) (t F)

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

m. Natural.≤ m 0 m = 0

x. (fst x, snd x) = x

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

t1 t2. (if T 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 T T

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. (p. P p) p1 p2. P (p1, p2)

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 x. x { y. y | p y } p x

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.
    (x. P x) (M. x. P x Natural.≤ x M)
    m. P m x. P x Natural.≤ x 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))
    B. m n. Natural.≤ (P m n) (Natural.* B (Natural.+ m n))