Package haskell-prime: Prime numbers
Information
name | haskell-prime |
version | 1.9 |
description | Prime numbers |
author | Joe Hurd <joe@gilith.com> |
license | MIT |
haskell-category | Number Theory |
requires | base haskell natural-divides natural-prime stream |
show | Data.Bool Data.List Data.Pair Data.Stream Function Haskell.Data.Stream as H Haskell.Number.Natural as H Haskell.Number.Natural.Prime.Sieve as H Number.Natural Number.Natural.Prime.Sieve Probability.Random |
Files
- Package tarball haskell-prime-1.9.tgz
- Theory file haskell-prime.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.Prime.all = H.unfold H.next H.initial
⊦ H.perimeter = mapDomain H.toHol max
⊦ H.unSieve = mapDomain H.toHol dest
⊦ H.Sieve = mapRange H.fromHol mk
⊦ ∀s. H.Sieve (H.unSieve s) = s
⊦ H.initial = H.Sieve (1, [])
⊦ ∀s. H.perimeter s = fst (H.unSieve s)
⊦ 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
⊦ ∀s.
H.next s =
let (b, s') ← H.increment s in
if b then (H.perimeter s', s') else H.next s'
⊦ ∀r.
let (i, r') ← H.Geometric.fromRandom r in
let (j, r'') ← H.Geometric.fromRandom r' in
H.nth H.Prime.all i ≤ H.nth H.Prime.all j ⇔ i ≤ j
⊦ ∀r.
let (i, r') ← H.Geometric.fromRandom r in
let (j, r'') ← H.Geometric.fromRandom r' in
0 < H.nth H.Prime.all (i + j + 1) mod H.nth H.Prime.all i
⊦ H.increment =
λs.
let (n, ps) ← H.unSieve s in
let n' ← n + 1 in
let (b, ps') ← H.increment.inc n' 1 ps in
(b, H.Sieve (n', ps'))
⊦ (∀n i. H.increment.inc n i [] = (⊤, (n, 0, 0) :: [])) ∧
∀n i p k j ps.
H.increment.inc n i ((p, k, j) :: ps) =
let k' ← (k + i) mod p in
let j' ← j + i in
if k' = 0 then (⊥, (p, 0, j') :: ps)
else let (b, ps') ← H.increment.inc n j' ps in (b, (p, k', 0) :: ps')
Input Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Prime
- Sieve
- sieve
- Sieve
- Natural
- Probability
- Random
- random
- Random
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- []
- Pair
- ,
- fst
- mapSnd
- Stream
- ::
- nth
- unfold
- Bool
- Function
- id
- mapDomain
- mapRange
- ∘
- Haskell
- Data
- Stream
- H.nth
- H.unfold
- Stream
- Number
- Natural
- Geometric
- H.Geometric.fromRandom
- Geometric
- Natural
- Data
- Number
- Natural
- +
- <
- ≤
- bit0
- bit1
- divides
- mod
- suc
- zero
- Prime
- Prime.all
- Sieve
- dest
- increment
- increment.inc
- initial
- max
- mk
- next
- Natural
Assumptions
⊦ ⊤
⊦ H.nth = nth
⊦ H.unfold = unfold
⊦ ¬⊥ ⇔ ⊤
⊦ bit0 0 = 0
⊦ ⊥ ⇔ ∀p. p
⊦ unfold next initial = Prime.all
⊦ ∀x. id x = x
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∃) = λp. p ((select) p)
⊦ ∀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 ⇒ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀a. mk (dest a) = a
⊦ initial = mk (1, [])
⊦ ∀i. ¬(nth Prime.all i = 0)
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀s. max s = fst (dest s)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀xy. ∃x y. xy = (x, y)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀h t. nth (h :: t) 0 = h
⊦ ∀f g. mapDomain f g = g ∘ f
⊦ ∀f g. mapRange f g = f ∘ g
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. m + n = m ⇔ n = 0
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀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
⊦ ∀f. ∃fn. ∀x y. fn (x, y) = f x y
⊦ ∀h t n. nth (h :: t) (suc n) = nth t n
⊦ ∀f x y. mapSnd f (x, y) = (x, f y)
⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀s1 s2. (∀n. nth s1 n = nth s2 n) ⇒ s1 = s2
⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀n i. increment.inc n i [] = (⊤, (n, 0, 0) :: [])
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)
⊦ ∀f b. unfold f b = let (a, b') ← f b in a :: unfold f b'
⊦ ∀s.
next s =
let (b, s') ← increment s in if b then (max s', s') else next s'
⊦ ∀s.
increment s =
let (n, ps) ← dest s in
let n' ← n + 1 in
let (b, ps') ← increment.inc n' 1 ps in
(b, mk (n', ps'))
⊦ ∀n i p k j ps.
increment.inc n i ((p, k, j) :: ps) =
let k' ← (k + i) mod p in
let j' ← j + i in
if k' = 0 then (⊥, (p, 0, j') :: ps)
else let (b, ps') ← increment.inc n j' ps in (b, (p, k', 0) :: ps')