Package haskell-prime-test: QuickCheck tests for prime numbers

Information

name	haskell-prime-test
version	1.29
description	QuickCheck tests for prime numbers
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-12-10
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.29.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
Number
- Natural
  - natural
Probability
- Random
  - random

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - ⊤
- List
  - any
- Pair
  - ,
- Stream
  - nth
  - take
Haskell
- Data
  - Stream
    - H.nth
    - H.take'
- Number
  - Natural
    - H.divides
    - H.fromRandom
    - Geometric
      - H.Geometric.fromRandom
    - Prime
      - H.Prime.all
Number
- Natural
  - +
  - ≤
  - bit0
  - bit1
  - divides
  - zero
  - Prime
    - Prime.all

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