Package haskell-prime-test: QuickCheck tests for prime numbers
Information
name | haskell-prime-test |
version | 1.33 |
description | QuickCheck tests for prime numbers |
author | Joe Leslie-Hurd <joe@gilith.com> |
license | MIT |
provenance | HOL Light theory extracted on 2014-11-01 |
checksum | 29e7b21a5244d1082c6089ff6f283151f1e4c417 |
requires | base haskell haskell-prime-def natural-divides natural-prime |
show | Data.Bool Data.List Data.Pair Data.Stream Haskell.Data.Stream as H Haskell.Number.Natural as H Number.Natural Probability.Random |
Files
- Package tarball haskell-prime-test-1.33.tgz
- Theory source file haskell-prime-test.thy (included in the package tarball)
Theorems
⊦ ¬(H.nth H.Prime.all 0 = 0)
⊦ ∀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
¬H.divides (H.nth H.Prime.all i) (H.nth H.Prime.all (i + j + 1))
⊦ ∀r.
let (n, r') ← H.fromRandom r in
let (i, r'') ← H.Geometric.fromRandom r' in
any (λp. H.divides p (n + 2)) (H.take' H.Prime.all i) ∨
H.nth H.Prime.all i ≤ n + 2
External Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
- Probability
- Random
- random
- Random
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- ⊤
- List
- any
- Pair
- ,
- Stream
- nth
- take
- Bool
- Haskell
- Data
- Stream
- H.nth
- H.take'
- Stream
- Number
- Natural
- H.divides
- H.fromRandom
- Geometric
- H.Geometric.fromRandom
- Prime
- H.Prime.all
- Natural
- Data
- Number
- Natural
- +
- ≤
- bit0
- bit1
- divides
- zero
- Prime
- Prime.all
- Natural
Assumptions
⊦ ⊤
⊦ H.Prime.all = Prime.all
⊦ H.divides = divides
⊦ H.nth = nth
⊦ H.take' = take
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀x. ∃a b. x = (a, b)
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀ps.
ps = Prime.all ⇔
¬(nth ps 0 = 0) ∧ (∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧
(∀i j. ¬divides (nth ps i) (nth ps (i + (j + 1)))) ∧
∀n i. any (λp. divides p (n + 2)) (take ps i) ∨ nth ps i ≤ n + 2