Package set-finite-def: Definition of finite sets

Information

Files

• Package tarball set-finite-def-1.37.tgz
• Theory source file set-finite-def.thy (included in the package tarball)

Defined Constants

• Set
  • finite
  • infinite

Theorems

⊦ finite ∅

⊦ ∀s. infinite s ⇔ ¬finite s

⊦ ∀x s. finite s ⇒ finite (insert x s)

⊦ ∀a. finite a ⇔ a = ∅ ∨ ∃x s. a = insert x s ∧ finite s

⊦ ∀p. p ∅ ∧ (∀x s. p s ⇒ p (insert x s)) ⇒ ∀a. finite a ⇒ p a

External Type Operators

• →
• bool
• Set
  • set

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • ⊤
• Set
  • ∅
  • insert

Assumptions

⊦ ⊤

⊦ (∀) = λp. p = λx. ⊤

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

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

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

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

⊦ ∀p q. (∀x. p x ⇒ q x) ⇒ (∃x. p x) ⇒ ∃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 document generated by opentheory 1.3 (release 20150429)