Package natural-prime: Prime natural numbers

Information

Files

• Package tarball natural-prime-1.87.tgz
• Theory source file natural-prime.thy (included in the package tarball)

Defined Type Operator

• Number
  • Natural
    • Prime
      • Sieve
        • Sieve.sieve

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

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

⊦ ∀n₁ n₂. nth Prime.all n₁ = nth Prime.all n₂ ⇔ n₁ = n₂

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

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

⊦ ∀n₁ n₂. nth Prime.all n₁ = nth Prime.all n₂ ⇒ n₁ = n₂

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

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

⊦ ∀p₁ p₂. prime p₁ ∧ prime p₂ ∧ divides p₁ p₂ ⇒ p₁ = p₂

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

• →
• bool
• Data
  • List
    • list
  • Pair
    • ×
  • Stream
    • stream
• Number
  • Natural
    • natural

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • @
    • []
    • all
    • any
    • map
    • member
  • Pair
    • ,
    • fst
    • snd
  • Stream
    • ::
    • nth
    • take
    • unfold
• Function
  • ∘
• Number
  • Natural
    • *
    • +
    • -
    • <
    • ≤
    • bit0
    • bit1
    • distance
    • div
    • divides
    • even
    • factorial
    • gcd
    • minimal
    • mod
    • suc
    • zero

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

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

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

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

⊦ ∀t₁ t₂. ¬(t₁ ⇒ t₂) ⇔ t₁ ∧ ¬t₂

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

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

⊦ ∀t₁ t₂. ¬(t₁ ∧ t₂) ⇔ ¬t₁ ∨ ¬t₂

⊦ ∀t₁ t₂. ¬(t₁ ∨ t₂) ⇔ ¬t₁ ∧ ¬t₂

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

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

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

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇒ s₁ = s₂

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

⊦ ∀l₁ l₂ x. member x (l₁ @ l₂) ⇔ member x l₁ ∨ member x l₂

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

⊦ ∀h₁ h₂ t₁ t₂. h₁ :: t₁ = h₂ :: t₂ ⇔ h₁ = h₂ ∧ t₁ = t₂

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

OpenTheory package document generated by opentheory 1.3 (release 20160501)