Package natural-prime-stream: The ordered stream of all prime numbers
Information
| name | natural-prime-stream |
| version | 1.3 |
| description | The ordered stream of all prime numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| requires | bool list natural natural-prime-thm stream |
| show | Data.Bool Data.List Data.Stream Number.Natural |
Files
- Package tarball natural-prime-stream-1.3.tgz
- Theory file natural-prime-stream.thy (included in the package tarball)
Defined Constants
- Number
- Natural
- Prime
- Prime.all
- Prime.below
- Prime
- Natural
Theorems
⊦ Prime.below 0 = []
⊦ Prime.below 1 = []
⊦ ∀i. prime (nth Prime.all i)
⊦ Prime.below 2 = []
⊦ nth Prime.all 0 = 2
⊦ Prime.below 3 = 2 :: []
⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p
⊦ ∀n. Prime.below n = take Prime.all (minimal i. n ≤ nth Prime.all i)
⊦ ∀n p. member p (Prime.below n) ⇔ prime p ∧ p < n
⊦ ∀i j. nth Prime.all i < nth Prime.all j ⇔ i < j
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
⊦ ∀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)
Input Type Operators
- →
- bool
- Data
- List
- list
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- member
- Stream
- nth
- take
- Bool
- Number
- Natural
- +
- <
- ≤
- bit0
- bit1
- divides
- minimal
- prime
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬prime 0
⊦ ¬prime 1
⊦ prime 2
⊦ ¬⊥ ⇔ ⊤
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ (minimal n. ⊤) = 0
⊦ ∀x. ¬member x []
⊦ ∀t. t ∨ ¬t
⊦ ∀m. ¬(m < 0)
⊦ ∀n. n < suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∀x. t) ⇔ 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
⊦ ∀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 ⇔ ⊥)
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀n. ∃p. n ≤ p ∧ prime p
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀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 q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀m n. suc m + n = suc (m + n)
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n
⊦ ∀p l. (∀x. member x l ⇒ p x) ⇔ all p l
⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)
⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n
⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)
⊦ ∀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. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n
⊦ ∀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
⊦ ∀p.
(∀m. ∃n. m ≤ n ∧ p n) ⇒
∃s. (∀i j. nth s i ≤ nth s j ⇔ i ≤ j) ∧ ∀n. p n ⇔ ∃i. nth s i = n