Package real: The real numbers

Information

namereal
version1.54
descriptionThe real numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
natural
pair
set
showData.Bool
Data.Pair
Function
Number.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 m n

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

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

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

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

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

External Type Operators

External Constants

Assumptions

¬

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

x. id x = x

t. t ¬t

m. ¬(m < 0)

n. ¬(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. ¬(suc n = 0)

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. distance 0 n = n

n. distance n 0 = n

n. distance n n = 0

t. ( t) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m * 1 = m

m. 1 * m = m

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

m n. m m + n

m n. n m + n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

m. m 0 m = 0

x. (fst x, snd x) = x

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

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

a b. fst (a, b) = a

a b. snd (a, b) = b

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

n. bit0 (suc n) = suc (suc (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. m * n = n * m

m n. m + n = n + m

m n. distance m n = distance n m

m n. m = n m n

m n. m < n m n

m n. m n n m

m n. distance m n m + n

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

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

n. 2 * n = n + n

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. suc m n 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. m + suc n = suc (m + n)

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

m n. suc m = suc n m = n

m n. distance m n = 0 m = n

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

m n. m * suc n = m + m * n

m n. suc m * n = m * n + n

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

p. (x. p x) a b. p (a, b)

m n. m n d. n = m + d

a b. (n. 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. m < suc n m = n 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. distance m p distance m n + distance n p

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

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

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

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

m n p. m + n m + p n p

m n p. n + m p + m n p

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

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

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

p. p 0 (n. p n p (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. m * (n + p) = m * n + m * p

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

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

p m n. distance m n * p = distance (m * p) (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 (suc n) = f (fn n) n

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

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

m n p. m * n m * p m = 0 n p

m n p. m * p n * p m n p = 0

a b a' b'. (a, b) = (a', b') a = a' b = b'

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

m n p q. m < p n < q m + n < p + q

m n p q. m n p q m * p n * q

m n p q. m p n q m + n p + q

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

m n p. distance m n p m n + p n m + p

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

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

p. (n. p n) (m. n. p n n m) m. p m n. p n n m

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

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

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