Package haskell-prime-def: Definition of prime numbers
Information
| name | haskell-prime-def |
| version | 1.7 |
| description | Definition of prime numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-08-13 |
| requires | base |
| show | Data.Bool Data.List Data.Pair Data.Stream Function Haskell.Number.Natural as H Haskell.Number.Natural.Prime.Sieve as H Number.Natural Number.Natural.Prime.Sieve |
Files
- Package tarball haskell-prime-def-1.7.tgz
- Theory file haskell-prime-def.thy (included in the package tarball)
Defined Type Operator
- Haskell
- Number
- Natural
- Prime
- Sieve
- H.Sieve
- Sieve
- Prime
- Natural
- Number
Defined Constants
- Haskell
- Number
- Natural
- Prime
- H.Prime.all
- Sieve
- H.fromHol
- H.increment
- H.increment.inc
- H.initial
- H.next
- H.perimeter
- H.toHol
- H.unSieve
- H.Sieve
- Prime
- Natural
- Number
Theorems
⊦ H.Prime.all = Prime.all
⊦ H.increment.inc = increment.inc
⊦ H.initial = H.fromHol initial
⊦ H.perimeter = mapDomain H.toHol max
⊦ H.unSieve = mapDomain H.toHol dest
⊦ H.Sieve = mapRange H.fromHol mk
⊦ H.increment = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) increment
⊦ H.next = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) next
⊦ (∀h. H.fromHol (H.toHol h) = h) ∧ ∀x. H.toHol (H.fromHol x) = x
Input Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Prime
- Sieve
- sieve
- Sieve
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊤
- Pair
- mapSnd
- Bool
- Function
- mapDomain
- mapRange
- ∘
- Number
- Natural
- Prime
- Prime.all
- Sieve
- dest
- increment
- increment.inc
- initial
- max
- mk
- next
- Prime
- Natural
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∃x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤