Package natural-prime-stream: The ordered stream of all prime numbers

Information

Files

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

Defined Constants

• Number
  • Natural
    • Prime
      • Prime.all
      • Prime.below

Theorems

⊦ Prime.below 0 = []

⊦ Prime.below 1 = []

⊦ ∀i. prime (nth Prime.all i)

⊦ ¬(nth Prime.all 0 = 0)

⊦ Prime.below 2 = []

⊦ nth Prime.all 0 = 2

⊦ ∀i. ¬(nth Prime.all i = 0)

⊦ ∀i. Prime.below (nth Prime.all i) = take Prime.all i

⊦ Prime.below 3 = 2 :: []

⊦ ∀p. prime p ⇔ ∃i. nth Prime.all i = p

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

⊦ ∀n.
    prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ all (λp. ¬divides p n) (Prime.below n)

⊦ ∀n i.
    any (λp. divides p (n + 2)) (take Prime.all i) ∨
    nth Prime.all i ≤ n + 2

⊦ ∀ps.
    ps = Prime.all ⇔
    (∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧ ∀p. prime p ⇔ ∃i. nth ps i = p

⊦ ∀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
  • Stream
    • stream
• Number
  • Natural
    • natural

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • @
    • []
    • all
    • any
    • member
  • Stream
    • nth
    • take
• Number
  • Natural
    • +
    • -
    • <
    • ≤
    • bit0
    • bit1
    • divides
    • minimal
    • prime
    • suc
    • zero

Assumptions

⊦ ⊤

⊦ ¬prime 0

⊦ ¬prime 1

⊦ prime 2

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ∀a. divides a a

⊦ ⊥ ⇔ ∀p. p

⊦ (minimal n. ⊤) = 0

⊦ ∀x. ¬member x []

⊦ ∀t. t ∨ ¬t

⊦ ∀m. ¬(m < 0)

⊦ ∀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 ∨ ⊤ ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 + n = n

⊦ ∀l. [] @ l = l

⊦ ∀l. l @ [] = l

⊦ ∀s. take s 0 = []

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

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

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

⊦ ∀m. suc m = m + 1

⊦ ∀m. m ≤ 0 ⇔ m = 0

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

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

⊦ ∀n. ∃p. n ≤ p ∧ prime p

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

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

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

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

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

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

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

⊦ ∀m n. m + n = m ⇔ n = 0

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

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

⊦ ∀n. ¬(n = 1) ⇒ ∃p. prime p ∧ divides p n

⊦ ∀p q. (∃x. p x) ∧ q ⇔ ∃x. p x ∧ q

⊦ ∀p q. (∃x. p x) ∨ q ⇔ ∃x. p x ∨ q

⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

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

⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

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

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p 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

⊦ ∀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 q. (∃x. p x) ∨ (∃x. q x) ⇔ ∃x. p x ∨ q x

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

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

⊦ ∀n. prime n ⇔ ¬(n = 0) ∧ ¬(n = 1) ∧ ∀p. prime p ∧ p < n ⇒ ¬divides p 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 20150429)