Package real: The real numbers

Information

namereal
version1.10
descriptionThe real numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Number.Natural as Natural
Number.Real
Set

Files

Defined Type Operator

Defined Constants

Theorems

x. x x

x. 0 + x = x

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)

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

(x. exp x 0 = 1) x n. exp x (Natural.suc n) = x * exp x n

P.
    (x. P x) (M. x. P x x M)
    M. (x. P x x M) M'. (x. P x x M') M M'

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

Input Type Operators

Input Constants

Assumptions

T

n. Natural.≤ 0 n

n. Natural.≤ n n

F p. p

x. ¬(x )

x. Function.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

x. x = x T

n. ¬(Natural.suc n = 0)

n. Natural.distance 0 n = n

n. Natural.distance n 0 = n

n. Natural.distance n n = 0

n. Natural.bit0 n = Natural.+ n n

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)

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

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

x. Data.Pair., (Data.Pair.fst x) (Data.Pair.snd x) = x

x y. Data.Pair.fst (Data.Pair., x y) = x

x y. Data.Pair.snd (Data.Pair., x y) = y

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

(¬T F) (¬F T)

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

x y. x = y y = x

a b. (a b) a b

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.suc m = Natural.suc n m = n

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

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

P. (p. P p) p1 p2. P (Data.Pair., p1 p2)

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

A B. (n. Natural.≤ (Natural.* A n) B) A = 0

f g. f = g x. f x = g x

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

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

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. (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

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

p q r. p q r p q r

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.* (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

s t. s = t x. x s x t

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

P. (x. y. P x y) y. x. P x (y x)

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

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

P. P 0 (n. P n P (Natural.suc n)) n. P n

(t. ¬¬t t) (¬T F) (¬F T)

p x. x { y. y | p y } p x

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 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. Data.Pair., x y = Data.Pair., 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)

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

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

P.
    (B. n. Natural.≤ (P n) B)
    A B. n. Natural.≤ (Natural.* n (P n)) (Natural.+ (Natural.* A n) B)

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

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

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)

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)

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))

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

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

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))

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

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

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