Package bool-int-and: bool-int-and

Information

Files

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

Theorems

⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3

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

Input Type Operators

• →
• bool

Input Constants

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

Assumptions

⊦ T

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

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