Package bool-int-eq: bool-int-eq

Information

Files

• Package tarball bool-int-eq-1.0.tgz
• Theory file bool-int-eq.thy (included in the package tarball)

Theorems

⊦ ∀x. x = x

⊦ ∀x. x = x ⇔ T

⊦ ∀t1 t2. (λx. t1) t2 = t1

⊦ ∀f y. (λx. f x) y = f y

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

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

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

Input Type Operators

• →
• bool

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • T

Assumptions

⊦ T

⊦ (∀) = λP. P = λx. T

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

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