Package natural-def: Constructing the natural numbers

Information

Files

• Package tarball natural-def-1.20.tgz
• Theory file natural-def.thy (included in the package tarball)

Defined Type Operator

• Number
  • Natural
    • natural

Defined Constants

• Number
  • Natural
    • suc
    • zero

Theorems

⊦ ∀n. ¬(suc n = 0)

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n

Input Type Operators

• →
• bool
• ind

Input Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • ⊥
    • ⊤
• Function
  • injective
  • surjective

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. 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

⊦ ∃f. injective f ∧ ¬surjective f

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

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

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀f y. (let x ← y in f x) = f y

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

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x

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

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

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

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

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

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

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

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

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

⊦ ∀f. injective f ⇔ ∀x₁ x₂. f x₁ = f x₂ ⇒ x₁ = x₂

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

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

⊦ ∀p₁ p₂ q₁ q₂. (p₁ ⇒ p₂) ∧ (q₁ ⇒ q₂) ⇒ p₁ ∨ q₁ ⇒ p₂ ∨ q₂

OpenTheory package summary generated by opentheory 1.1 (release 20120326)