Package haskell-prime-src: Haskell source for prime numbers
Information
name | haskell-prime-src |
version | 1.8 |
description | Haskell source for prime numbers |
author | Joe Hurd <joe@gilith.com> |
license | MIT |
provenance | HOL Light theory extracted on 2012-08-13 |
requires | base haskell haskell-prime-def natural-prime stream |
show | Data.Bool 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 |
Files
- Package tarball haskell-prime-src-1.8.tgz
- Theory file haskell-prime-src.thy (included in the package tarball)
Theorems
⊦ H.Prime.all = H.unfold H.next H.initial
⊦ ∀s. H.Sieve (H.unSieve s) = s
⊦ H.initial = H.Sieve (1, Data.List.[])
⊦ ∀s. H.perimeter s = fst (H.unSieve s)
⊦ ∀s.
H.next s =
let (b, s') ← H.increment s in
if b then (H.perimeter s', s') else H.next s'
⊦ 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 Data.List.[] =
(⊤, Data.List.:: (n, 0, 0) Data.List.[])) ∧
∀n i p k j ps.
H.increment.inc n i (Data.List.:: (p, k, j) ps) =
let k' ← (k + i) mod p in
let j' ← j + i in
if k' = 0 then (⊥, Data.List.:: (p, 0, j') ps)
else
let (b, ps') ← H.increment.inc n j' ps in
(b, Data.List.:: (p, k', 0) ps')
Input Type Operators
- →
- bool
- Data
- List
- Data.List.list
- Pair
- ×
- Stream
- stream
- List
- Haskell
- Number
- Natural
- Prime
- Sieve
- H.Sieve
- Sieve
- Prime
- Natural
- Number
- Number
- Natural
- natural
- Prime
- Sieve
- sieve
- Sieve
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- cond
- ⊥
- ⊤
- List
- Data.List.::
- Data.List.[]
- Pair
- ,
- fst
- mapSnd
- Stream
- ::
- nth
- unfold
- Bool
- Function
- id
- mapDomain
- mapRange
- ∘
- Haskell
- Data
- Stream
- H.unfold
- Stream
- 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
- Data
- Number
- Natural
- +
- bit1
- mod
- suc
- zero
- Prime
- Prime.all
- Sieve
- dest
- increment
- increment.inc
- initial
- max
- mk
- next
- Natural
Assumptions
⊦ ⊤
⊦ H.Prime.all = Prime.all
⊦ H.unfold = unfold
⊦ 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
⊦ unfold next initial = Prime.all
⊦ ∀x. id x = x
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀a. mk (dest a) = a
⊦ initial = mk (1, Data.List.[])
⊦ ∀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)
⊦ H.increment = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) increment
⊦ H.next = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) next
⊦ ∀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
⊦ ∀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
⊦ ∀f. ∃fn. ∀x y. fn (x, y) = f x y
⊦ (∀h. H.fromHol (H.toHol h) = h) ∧ ∀x. H.toHol (H.fromHol x) = x
⊦ ∀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
⊦ ∀s1 s2. (∀n. nth s1 n = nth s2 n) ⇒ s1 = s2
⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀n i.
increment.inc n i Data.List.[] =
(⊤, Data.List.:: (n, 0, 0) Data.List.[])
⊦ ∀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 (Data.List.:: (p, k, j) ps) =
let k' ← (k + i) mod p in
let j' ← j + i in
if k' = 0 then (⊥, Data.List.:: (p, 0, j') ps)
else
let (b, ps') ← increment.inc n j' ps in
(b, Data.List.:: (p, k', 0) ps')