Package natural-prime-stream-def: Definition of the ordered stream of all prime numbers
Information
| name | natural-prime-stream-def |
| version | 1.22 |
| description | Definition of the ordered stream of all prime numbers |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-04 |
| checksum | c0bfa33424ba1e4ed8e054b75972429903f73294 |
| requires | bool natural natural-prime-thm stream |
| show | Data.Bool Data.List Data.Stream Number.Natural |
Files
- Package tarball natural-prime-stream-def-1.22.tgz
- Theory source file natural-prime-stream-def.thy (included in the package tarball)
Defined Constants
- Number
- Natural
- Prime
- Prime.all
- Prime.below
- Prime
- Natural
Theorems
⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p
⊦ ∀n. Prime.below n = take Prime.all (minimal i. n ≤ nth Prime.all i)
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
External Type Operators
- →
- bool
- Data
- List
- list
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊤
- Stream
- nth
- take
- Bool
- Number
- Natural
- ≤
- minimal
- prime
- Natural
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ (∀) = λp. p = λx. ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀n. ∃p. n ≤ p ∧ prime p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀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