Package natural-prime: Prime natural numbers

Information

namenatural-prime
version1.85
descriptionPrime natural numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
homepagehttp://opentheory.gilith.com/?pkg=natural-prime
hol-light-int-filehol-light.int
hol-light-thm-filehol-light.art
haskell-nameopentheory-prime
haskell-categoryNumber Theory
haskell-int-filehaskell.int
haskell-src-filehaskell.art
haskell-test-filehaskell-test.art
checksum4ee03b18ee8209d1bf91831616d3a569bc2829a6
requiresbase
natural-divides
stream
showData.Bool
Data.List
Data.Pair
Data.Stream
Function
Number.Natural
Number.Natural.Prime.Sieve as Sieve

Files

Defined Type Operator

Defined Constants

Theorems

¬prime 0

¬prime 1

prime 2

prime 3

Prime.below 0 = []

Prime.all = unfold Sieve.next Sieve.initial

Sieve.max Sieve.initial = 1

Prime.below 1 = []

unfold Sieve.next Sieve.initial = Prime.all

i. prime (nth Prime.all i)

¬(nth Prime.all 0 = 0)

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)

i j. i < j nth Prime.all i < nth Prime.all j

i j. i j nth Prime.all i nth Prime.all j

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 []

i j. ¬divides (nth Prime.all i) (nth Prime.all (i + (j + 1)))

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'

n i.
    any (λp. divides p (n + 2)) (take Prime.all i)
    nth Prime.all i n + 2

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

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.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

(n i. Sieve.increment.inc n i [] = (, (n, 0, 0) :: []))
  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')

External Type Operators

External Constants

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

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

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

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

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

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

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