Package natural-prime: Prime natural numbers
Information
name | natural-prime |
version | 1.58 |
description | Prime natural numbers |
author | Joe Leslie-Hurd <joe@gilith.com> |
license | MIT |
requires | bool function list natural natural-divides natural-gcd pair relation stream |
show | Data.Bool Data.List Data.Pair Data.Stream Function Number.Natural Number.Natural.Prime.Sieve as Sieve |
Files
- Package tarball natural-prime-1.58.tgz
- Theory source file natural-prime.thy (included in the package tarball)
Defined Type Operator
- Number
- Natural
- Prime
- Sieve
- Sieve.sieve
- Sieve
- Prime
- Natural
Defined Constants
- Number
- Natural
- prime
- Prime
- Prime.all
- Prime.below
- Sieve
- Sieve.dest
- Sieve.increment
- Sieve.increment.inc
- Sieve.initial
- Sieve.invariant
- Sieve.invariant.inv
- Sieve.max
- Sieve.mk
- Sieve.next
- Sieve.primes
- Natural
Theorems
⊦ ¬prime 0
⊦ ¬prime 1
⊦ prime 2
⊦ prime 3
⊦ Prime.below 0 = []
⊦ Sieve.max Sieve.initial = 1
⊦ Prime.below 1 = []
⊦ unfold Sieve.next Sieve.initial = Prime.all
⊦ ∀i. prime (nth Prime.all i)
⊦ Prime.below 2 = []
⊦ ∀a. Sieve.mk (Sieve.dest a) = a
⊦ ∀n i. Sieve.invariant.inv n i []
⊦ Sieve.initial = Sieve.mk (1, [])
⊦ nth Prime.all 0 = 2
⊦ ∀i. ¬(nth Prime.all i = 0)
⊦ ∀s. Sieve.max s = fst (Sieve.dest s)
⊦ ∀n. ∃p. n ≤ p ∧ prime p
⊦ ∀i. Prime.below (nth Prime.all i) = take Prime.all i
⊦ ∀s. Sieve.primes s = map fst (snd (Sieve.dest s))
⊦ ∀r. Sieve.invariant r ⇔ Sieve.dest (Sieve.mk r) = r
⊦ Prime.below 3 = 2 :: []
⊦ ∀s. Sieve.primes s = Prime.below (Sieve.max s + 1)
⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p
⊦ ∀p. prime p ∧ even p ⇒ p = 2
⊦ ∀n. Prime.below n = take Prime.all (minimal i. n ≤ nth Prime.all i)
⊦ ∀n p. member p (Prime.below n) ⇔ prime p ∧ p < n
⊦ ∀n1 n2. nth Prime.all n1 = nth Prime.all n2 ⇔ n1 = n2
⊦ ∀i j. nth Prime.all i < nth Prime.all j ⇔ i < j
⊦ ∀i j. nth Prime.all i ≤ nth Prime.all j ⇔ i ≤ j
⊦ ∀n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) ⇔ n1 = n2
⊦ ∀n1 n2. nth Prime.all n1 = nth Prime.all n2 ⇒ n1 = n2
⊦ ∀n1 n2. divides (nth Prime.all n1) (nth Prime.all n2) ⇒ n1 = n2
⊦ ∀n. ¬(n = 1) ⇒ ∃p. prime p ∧ divides p n
⊦ ∀n. Prime.below (suc n) = Prime.below n @ if prime n then n :: [] else []
⊦ ∀p1 p2. prime p1 ∧ prime p2 ∧ divides p1 p2 ⇒ p1 = p2
⊦ ∀p n. prime p ⇒ (gcd p n = 1 ⇔ ¬divides p n)
⊦ ∀n i. Sieve.increment.inc n i [] = (⊤, (n, 0, 0) :: [])
⊦ ∀p n. prime p ∧ ¬divides p n ⇒ gcd p n = 1
⊦ ∀p m n. prime p ⇒ (divides p (m * n) ⇔ divides p m ∨ divides p n)
⊦ ∀n.
prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ all (λp. ¬divides p n) (Prime.below n)
⊦ ∀p m n. prime p ∧ ¬divides p m ∧ ¬divides p n ⇒ ¬divides p (m * n)
⊦ ∀p. prime p ⇔ ¬(p = 1) ∧ ∀n. divides n p ⇒ n = 1 ∨ n = p
⊦ ∀s.
Sieve.next s =
let (b, s') ← Sieve.increment s in
if b then (Sieve.max s', s') else Sieve.next s'
⊦ ∀s b s'.
Sieve.increment s = (b, s') ⇒
Sieve.max s' = Sieve.max s + 1 ∧ (b ⇔ prime (Sieve.max s'))
⊦ ∀n ps.
Sieve.invariant (n, ps) ⇔
¬(n = 0) ∧ map fst ps = Prime.below (n + 1) ∧
Sieve.invariant.inv n 0 ps
⊦ ∀n. prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ ∀p. prime p ∧ p < n ⇒ ¬divides p n
⊦ ∀ps.
ps = Prime.all ⇔
(∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧ ∀p. prime p ⇔ ∃i. nth ps i = p
⊦ ∀n i p k j ps.
Sieve.invariant.inv n i ((p, k, j) :: ps) ⇔
¬(p = 0) ∧ (k + i) mod p = n mod p ∧ Sieve.invariant.inv n (i + j) ps
⊦ ∀s.
Sieve.increment s =
let (n, ps) ← Sieve.dest s in
let n' ← n + 1 in
let (b, ps') ← Sieve.increment.inc n' 1 ps in
(b, Sieve.mk (n', ps'))
⊦ ∀n i p k j ps.
Sieve.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') ← Sieve.increment.inc n j' ps in (b, (p, k', 0) :: ps')
⊦ ∀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
External Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- any
- map
- member
- Pair
- ,
- fst
- snd
- Stream
- ::
- nth
- take
- unfold
- Bool
- Function
- ∘
- Number
- Natural
- *
- +
- -
- <
- ≤
- bit0
- bit1
- distance
- div
- divides
- even
- factorial
- gcd
- minimal
- mod
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ∀n. n ≤ n
⊦ ∀a. divides a 0
⊦ ∀a. divides a a
⊦ ∀p. all p []
⊦ ⊥ ⇔ ∀p. p
⊦ (minimal n. ⊤) = 0
⊦ ∀x. ¬member x []
⊦ ∀t. t ∨ ¬t
⊦ ∀m. ¬(m < 0)
⊦ ∀n. 0 < suc n
⊦ ∀n. n < suc n
⊦ ∀a. divides 1 a
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀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
⊦ ∀t. t ∨ ⊤ ⇔ ⊤
⊦ ∀t. t ∨ t ⇔ t
⊦ ∀n. ¬(factorial n = 0)
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. 0 * n = 0
⊦ ∀n. 0 + n = n
⊦ ∀m. m + 0 = m
⊦ ∀l. [] @ l = l
⊦ ∀l. l @ [] = l
⊦ ∀s. take s 0 = []
⊦ ∀f. map f [] = []
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀m. m * 1 = m
⊦ ∀m. 1 * m = m
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀m. suc m = m + 1
⊦ ∀n. even (suc n) ⇔ ¬even n
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀a. divides 0 a ⇔ a = 0
⊦ ∀x. (fst x, snd x) = x
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀a b. fst (a, b) = a
⊦ ∀a b. snd (a, b) = b
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀a. divides 2 a ⇔ even a
⊦ ∀x. ∃a b. x = (a, b)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀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
⊦ ∀m n. m < n ⇒ m ≤ n
⊦ ∀m n. m ≤ n ∨ n ≤ m
⊦ ∀m n. distance m (m + n) = n
⊦ ∀a. divides a 1 ⇔ a = 1
⊦ ∀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
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀p. (∀b. p b) ⇔ p ⊤ ∧ 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. ¬(∃x. p x) ⇔ ∀x. ¬p x
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀t1 t2. ¬(t1 ⇒ t2) ⇔ t1 ∧ ¬t2
⊦ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1
⊦ ∀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
⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n
⊦ ∀m n. m + n = m ⇔ n = 0
⊦ ∀m n. m + n = n ⇔ m = 0
⊦ ∀a b. gcd a b = a ⇔ divides a b
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀t1 t2. ¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2
⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2
⊦ ∀m n. even (m * n) ⇔ even m ∨ even n
⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n
⊦ ∀a b c. divides a b ⇒ divides a (b * c)
⊦ ∀a b c. divides a c ⇒ divides a (b * c)
⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d
⊦ ∀a b. divides a b ⇔ ∃c. c * a = b
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ ∀p l. ¬any p l ⇔ all (λx. ¬p x) l
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. n ≤ m ⇒ m - n + n = m
⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n
⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b
⊦ ∀h t n. nth (h :: t) (suc n) = nth t n
⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d
⊦ ∀p l. (∀x. member x l ⇒ p x) ⇔ all p l
⊦ ∀p l. (∃x. member x l ∧ p x) ⇔ any p l
⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y
⊦ ∀p q. p ∧ (∃x. q x) ⇔ ∃x. p ∧ q x
⊦ ∀p q. p ∨ (∀x. q x) ⇔ ∀x. p ∨ q x
⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x
⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)
⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n
⊦ ∀a b. ¬(b = 0) ∧ divides a b ⇒ a ≤ b
⊦ ∀p q. (∃x. p x) ∧ q ⇔ ∃x. p x ∧ q
⊦ ∀p q. (∃x. p x) ∨ q ⇔ ∃x. p x ∨ q
⊦ ∀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
⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀a b c. divides a b ∧ divides b c ⇒ divides a c
⊦ ∀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
⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)
⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n
⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀a b. ¬(b = 0) ∧ b ≤ a ⇒ divides b (factorial a)
⊦ ∀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
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)
⊦ ∀n m. ¬(n = 0) ⇒ m mod n mod n = m mod n
⊦ ∀s n. take s (suc n) = take s n @ nth s n :: []
⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t
⊦ ∀p q r. p ∧ (q ∨ r) ⇔ p ∧ q ∨ p ∧ r
⊦ ∀a b c. divides (gcd a (b * c)) (gcd a b * gcd a c)
⊦ ∀a. divides a 2 ⇔ a = 1 ∨ a = 2
⊦ ∀a. divides a 3 ⇔ a = 1 ∨ a = 3
⊦ ∀l1 l2 x. member x (l1 @ l2) ⇔ member x l1 ∨ member x l2
⊦ ∀p. (∀n. (∀m. m < n ⇒ p m) ⇒ p n) ⇒ ∀n. p n
⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x
⊦ ∀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
⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n
⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m
⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p
⊦ ∀h1 h2 t1 t2. h1 :: t1 = h2 :: t2 ⇔ h1 = h2 ∧ t1 = t2
⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'
⊦ ∀s n x. member x (take s n) ⇔ ∃i. i < n ∧ x = nth s i
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)
⊦ ∀b f. ∃fn. fn [] = b ∧ ∀h t. fn (h :: t) = f h t (fn t)
⊦ ∀a b s t. distance (s * a) (t * b) = 1 ⇒ gcd a b = 1
⊦ ∀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
⊦ ∀a b. (∀c. divides c a ∧ divides c b ⇒ c = 1) ⇒ gcd a b = 1
⊦ ∀f b. unfold f b = let (a, b') ← f b in a :: unfold f b'
⊦ ∀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)
⊦ ∀p.
(∀m. ∃n. m ≤ n ∧ p n) ⇒
∃s. (∀i j. nth s i ≤ nth s j ⇔ i ≤ j) ∧ ∀n. p n ⇔ ∃i. nth s i = n