Package real-def: Definition of the real numbers
Information
| name | real-def |
| version | 1.60 |
| description | Definition of the real numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2012-08-06 |
| requires | bool function natural pair set |
| show | Data.Bool Data.Pair Function Number.Natural as Natural Number.Real Set |
Files
- Package tarball real-def-1.60.tgz
- Theory file real-def.thy (included in the package tarball)
Defined Type Operator
- Number
- Real
- real
- Real
Defined Constants
- Number
- Real
- *
- +
- -
- /
- <
- ≤
- >
- ≥
- ↑
- ~
- abs
- fromNatural
- inv
- max
- min
- sup
- Real
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
- →
- bool
- Data
- Pair
- ×
- Pair
- Number
- Natural
- Natural.natural
- Natural
- Set
- set
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∃!
- ∨
- ¬
- cond
- ⊥
- ⊤
- Pair
- ,
- fst
- snd
- Bool
- Function
- id
- Number
- Natural
- Natural.*
- Natural.+
- Natural.<
- Natural.≤
- Natural.bit0
- Natural.bit1
- Natural.distance
- Natural.div
- Natural.mod
- Natural.suc
- Natural.zero
- Natural
- Set
- ∅
- ∈
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))