Package natural-prime-sieve-def: Definition of the sieve of Eratosthenes

Information

name	natural-prime-sieve-def
version	1.25
description	Definition of the sieve of Eratosthenes
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-12-10
requires	bool list natural natural-prime-stream pair relation
show	Data.Bool Data.List Data.Pair Number.Natural Number.Natural.Prime.Sieve

Files

Package tarball natural-prime-sieve-def-1.25.tgz
Theory source file natural-prime-sieve-def.thy (included in the package tarball)

Defined Type Operator

Number
- Natural
  - Prime
    - Sieve
      - sieve

Defined Constants

Number
- Natural
  - Prime
    - Sieve
      - dest
      - increment
        increment.inc
      - initial
      - invariant
        invariant.inv
      - max
      - mk
      - next
      - primes

Theorems

⊦ ∀a. mk (dest a) = a

⊦ ∀n i. invariant.inv n i []

⊦ initial = mk (1, [])

⊦ ∀s. max s = fst (dest s)

⊦ ∀s. primes s = map fst (snd (dest s))

⊦ ∀r. invariant r ⇔ dest (mk r) = r

⊦ ∀n i. increment.inc n i [] = (⊤, (n, 0, 0) :: [])

⊦ ∀s.
next s =
let (b, s') ← increment s in if b then (max s', s') else next s'

⊦ ∀n ps.
invariant (n, ps) ⇔
¬(n = 0) ∧ map fst ps = Prime.below (n + 1) ∧ invariant.inv n 0 ps

⊦ ∀n i p k j ps.
invariant.inv n i ((p, k, j) :: ps) ⇔
¬(p = 0) ∧ (k + i) mod p = n mod p ∧ invariant.inv n (i + j) ps

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

External Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - map
- Pair
  - ,
  - fst
  - snd
Number
- Natural
  - +
  - bit0
  - bit1
  - mod
  - suc
  - zero
  - Prime
    - Prime.below

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ ⊥ ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

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

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

⊦ Prime.below 2 = []

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 + n = n

⊦ ∀f. map f [] = []

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

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

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

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

⊦ ∀x. ∃a b. x = (a, b)

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

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

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

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b

⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)

⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x

⊦ ∀b f. ∃fn. fn [] = b ∧ ∀h t. fn (h :: t) = f h t (fn t)