Package natural-prime-stream-thm: Properties of the ordered stream of all prime numbers
Information
| name | natural-prime-stream-thm |
| version | 1.21 |
| description | Properties of the ordered stream of all prime numbers |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-12-02 |
| requires | bool list natural natural-divides natural-prime-stream-def natural-prime-thm stream |
| show | Data.Bool Data.List Data.Stream Number.Natural |
Files
- Package tarball natural-prime-stream-thm-1.21.tgz
- Theory source file natural-prime-stream-thm.thy (included in the package tarball)
Theorems
⊦ Prime.below 0 = []
⊦ Prime.below 1 = []
⊦ ∀i. prime (nth Prime.all i)
⊦ Prime.below 2 = []
⊦ nth Prime.all 0 = 2
⊦ ∀i. ¬(nth Prime.all i = 0)
⊦ ∀i. Prime.below (nth Prime.all i) = take Prime.all i
⊦ Prime.below 3 = 2 :: []
⊦ ∀n p. member p (Prime.below n) ⇔ prime p ∧ p < n
⊦ ∀n1 n2. nth Prime.all n1 = nth Prime.all n2 ⇔ n1 = n2
⊦ ∀i j. nth Prime.all i < nth Prime.all j ⇔ i < j
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
⊦ ∀n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) ⇔ n1 = n2
⊦ ∀n1 n2. nth Prime.all n1 = nth Prime.all n2 ⇒ n1 = n2
⊦ ∀n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) ⇒ n1 = n2
⊦ ∀n. Prime.below (suc n) = Prime.below n @ if prime n then n :: [] else []
⊦ ∀n.
prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ all (λp. ¬divides p n) (Prime.below n)
⊦ ∀ps.
ps = Prime.all ⇔
(∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧ ∀p. prime p ⇔ ∃i. nth ps i = p
⊦ ∀ps.
ps = Prime.all ⇔
¬(nth ps 0 = 0) ∧ (∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧
(∀i j. ¬divides (nth ps i) (nth ps (i + (j + 1)))) ∧
∀n i. any (λp. divides p (n + 2)) (take ps i) ∨ nth ps i ≤ n + 2
External Type Operators
- →
- bool
- Data
- List
- list
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- any
- member
- Stream
- nth
- take
- Bool
- Number
- Natural
- +
- -
- <
- ≤
- bit0
- bit1
- divides
- minimal
- prime
- suc
- zero
- Prime
- Prime.all
- Prime.below
- Natural
Assumptions
⊦ ⊤
⊦ ¬prime 0
⊦ ¬prime 1
⊦ prime 2
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ∀a. divides a a
⊦ ⊥ ⇔ ∀p. p
⊦ (minimal n. ⊤) = 0
⊦ ∀x. ¬member x []
⊦ ∀t. t ∨ ¬t
⊦ ∀m. ¬(m < 0)
⊦ ∀n. n < suc n
⊦ ∀a. divides 1 a
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀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 ∨ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. 0 + n = n
⊦ ∀l. [] @ l = l
⊦ ∀l. l @ [] = l
⊦ ∀s. take s 0 = []
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀m. suc m = m + 1
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. ¬(m ≤ n) ⇔ n < m
⊦ ∀m n. m < suc n ⇔ m ≤ n
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀p. (∀b. p b) ⇔ p ⊤ ∧ p ⊥
⊦ (∧) = λ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. suc m ≤ suc n ⇔ m ≤ n
⊦ ∀m n. m + n = m ⇔ n = 0
⊦ ∀n. Prime.below n = take Prime.all (minimal i. n ≤ nth Prime.all i)
⊦ ∀p l. ¬any p l ⇔ all (λx. ¬p x) l
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. n ≤ m ⇒ m - n + n = m
⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d
⊦ ∀p l. (∀x. member x l ⇒ p x) ⇔ all p l
⊦ ∀p l. (∃x. member x l ∧ p x) ⇔ any p l
⊦ ∀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 < n ⇔ m ≤ n ∧ ¬(m = n)
⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n
⊦ ∀a b. ¬(b = 0) ∧ divides a b ⇒ a ≤ b
⊦ ∀n. ¬(n = 1) ⇒ ∃p. prime p ∧ divides p n
⊦ ∀p q. (∃x. p x) ∧ q ⇔ ∃x. p x ∧ q
⊦ ∀p q. (∃x. p x) ∨ q ⇔ ∃x. p x ∨ q
⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀s1 s2. (∀n. nth s1 n = nth s2 n) ⇒ s1 = s2
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀p1 p2. prime p1 ∧ prime p2 ∧ divides p1 p2 ⇒ p1 = p2
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀s n. take s (suc n) = take s n @ nth s n :: []
⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t
⊦ ∀p q r. p ∧ (q ∨ r) ⇔ p ∧ q ∨ p ∧ r
⊦ ∀l1 l2 x. member x (l1 @ l2) ⇔ member x l1 ∨ member x l2
⊦ ∀p. (∀n. (∀m. m < n ⇒ p m) ⇒ p n) ⇒ ∀n. p n
⊦ ∀p q. (∃x. p x) ∨ (∃x. q x) ⇔ ∃x. p x ∨ q x
⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n
⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m
⊦ ∀s n x. member x (take s n) ⇔ ∃i. i < n ∧ x = nth s i
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)
⊦ ∀n. prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ ∀p. prime p ∧ p < n ⇒ ¬divides p n