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

Information

name	haskell-prime-test
version	1.10
description	QuickCheck tests 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-divides natural-prime
show	Data.Bool 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.10.tgz
Theory file haskell-prime-test.thy (included in the package tarball)

Theorems

⊦ ∀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

Input Type Operators

→
bool
Data
- Pair
  - ×
- Stream
  - stream
Number
- Natural
  - natural
Probability
- Random
  - random

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - ⊥
  - ⊤
- Pair
  - ,
- Stream
  - nth
Haskell
- Data
  - Stream
    - H.nth
- Number
  - Natural
    - Geometric
      - H.Geometric.fromRandom
    - Prime
      - H.Prime.all
Number
- Natural
  - +
  - <
  - ≤
  - bit0
  - bit1
  - divides
  - mod
  - suc
  - zero
  - Prime
    - Prime.all

Assumptions

⊦ ⊤

⊦ H.Prime.all = Prime.all

⊦ H.nth = nth

⊦ ¬⊥ ⇔ ⊤

⊦ bit0 0 = 0

⊦ ⊥ ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀i. ¬(nth Prime.all i = 0)

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀xy. ∃x y. xy = (x, y)

⊦ ∀x y. x = y ⇔ y = x

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j

⊦ ∀n₁ n₂. divides (nth Prime.all n₁) (nth Prime.all n₂) ⇔ n₁ = n₂

⊦ ∀f. ∃fn. ∀x y. fn (x, y) = f x y

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)