Package natural-prime-sieve-thm: Properties of the sieve of Eratosthenes
Information
| name | natural-prime-sieve-thm |
| version | 1.22 |
| description | Properties of the sieve of Eratosthenes |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-11-10 |
| requires | bool function list natural natural-divides natural-prime-sieve-def natural-prime-stream pair stream |
| show | Data.Bool Data.List Data.Pair Data.Stream Function Number.Natural Number.Natural.Prime.Sieve |
Files
- Package tarball natural-prime-sieve-thm-1.22.tgz
- Theory file natural-prime-sieve-thm.thy (included in the package tarball)
Theorems
⊦ max initial = 1
⊦ unfold next initial = Prime.all
⊦ ∀s. primes s = Prime.below (max s + 1)
⊦ ∀s b s'.
increment s = (b, s') ⇒ max s' = max s + 1 ∧ (b ⇔ prime (max s'))
Input Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Prime
- Sieve
- sieve
- Sieve
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- map
- Pair
- ,
- fst
- snd
- Stream
- ::
- nth
- unfold
- Bool
- Function
- ∘
- Number
- Natural
- *
- +
- <
- ≤
- bit0
- bit1
- div
- divides
- even
- mod
- prime
- suc
- zero
- Prime
- Prime.all
- Prime.below
- Sieve
- dest
- increment
- increment.inc
- initial
- invariant
- invariant.inv
- max
- mk
- next
- primes
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ∀p. all p []
⊦ ⊥ ⇔ ∀p. p
⊦ ∀t. t ∨ ¬t
⊦ ∀n. 0 < suc n
⊦ ∀n. n < suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ Prime.below 2 = []
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. (t ⇔ ⊤) ⇔ t
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. t ∧ t ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ∀t. t ∨ ⊥ ⇔ t
⊦ ∀t. t ∨ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. 0 * n = 0
⊦ ∀n. 0 + n = n
⊦ ∀m. m + 0 = m
⊦ ∀a. mk (dest a) = a
⊦ ∀l. [] @ l = l
⊦ ∀l. l @ [] = l
⊦ ∀f. map f [] = []
⊦ ∀n i. invariant.inv n i []
⊦ initial = mk (1, [])
⊦ nth Prime.all 0 = 2
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀m. 1 * m = m
⊦ ∀s. max s = fst (dest s)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀m. suc m = m + 1
⊦ ∀n. even (suc n) ⇔ ¬even n
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀xy. (fst xy, snd xy) = xy
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀s. primes s = map fst (snd (dest s))
⊦ ∀xy. ∃x y. xy = (x, y)
⊦ ∀r. invariant r ⇔ dest (mk r) = r
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀h t. nth (h :: t) 0 = h
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀m n. m + n = n + m
⊦ ∀m n. m < n ⇒ m ≤ n
⊦ Prime.below 3 = 2 :: []
⊦ ∀n. 2 * n = n + n
⊦ ∀m n. ¬(m < n ∧ n ≤ m)
⊦ ∀m n. ¬(m ≤ n ∧ n < m)
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. ¬(m ≤ n) ⇔ n < m
⊦ ∀m n. m < suc n ⇔ m ≤ n
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀n. ¬(n = 0) ⇒ 0 mod n = 0
⊦ ∀n. ¬(n = 0) ⇒ n mod n = 0
⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀m n. suc m + n = suc (m + n)
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2
⊦ ∀m n. even (m * n) ⇔ even m ∨ even n
⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n
⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n
⊦ ∀i j. nth Prime.all i < nth Prime.all j ⇔ i < j
⊦ ∀f. ∃fn. ∀x y. fn (x, y) = f x y
⊦ ∀h t n. nth (h :: t) (suc n) = nth t n
⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d
⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y
⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r
⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3
⊦ ∀t1 t2 t3. (t1 ∨ t2) ∨ t3 ⇔ t1 ∨ t2 ∨ t3
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + n < m + p ⇔ n < p
⊦ ∀n. Prime.below (suc n) = Prime.below n @ if prime n then n :: [] else []
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀s1 s2. (∀n. nth s1 n = nth s2 n) ⇒ s1 = s2
⊦ ∀p f l. all p (map f l) ⇔ all (p ∘ f) l
⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n
⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0
⊦ ∀f h t. map f (h :: t) = f h :: map f t
⊦ ∀p h t. all p (h :: t) ⇔ p h ∧ all p t
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀n i. increment.inc n i [] = (⊤, (n, 0, 0) :: [])
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)
⊦ ∀n m. ¬(n = 0) ⇒ m mod n mod n = m mod n
⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x
⊦ ∀p q. (∃x. p x) ∨ (∃x. q x) ⇔ ∃x. p x ∨ q x
⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l
⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p
⊦ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p
⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p
⊦ ∀h1 h2 t1 t2. h1 :: t1 = h2 :: t2 ⇔ h1 = h2 ∧ t1 = t2
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)
⊦ ∀m n q r. m = q * n + r ∧ r < n ⇒ m div n = q
⊦ ∀m n q r. m = q * n + r ∧ r < n ⇒ m mod n = r
⊦ ∀n.
prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ all (λp. ¬divides p n) (Prime.below n)
⊦ ∀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'
⊦ ∀n a b. ¬(n = 0) ⇒ (a mod n + b mod n) mod n = (a + b) mod n
⊦ ∀n a b. ¬(n = 0) ⇒ (suc a mod n = suc b mod n ⇔ a mod n = b mod n)
⊦ ∀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')