Package bool: Boolean operators and quantifiers

Information

name	bool
version	1.23
description	Boolean operators and quantifiers
author	Joe Hurd <joe@gilith.com>
license	MIT
show	Data.Bool

Files

Package tarball bool-1.23.tgz
Theory file bool.thy (included in the package tarball)

Defined Constants

Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - F
  - T

Theorems

⊦ T

⊦ ¬F ⇔ T

⊦ ¬T ⇔ F

⊦ ∀x. x = x

⊦ ∀t. t ⇒ t

⊦ F ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ F

⊦ (∃) = λp. p ((select) p)

⊦ ∀a. ∃x. x = a

⊦ ∀a. ∃!x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

⊦ T ⇔ (λp. p) = λp. p

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

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (T ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ T) ⇔ t

⊦ ∀t. F ∧ t ⇔ F

⊦ ∀t. T ∧ t ⇔ t

⊦ ∀t. t ∧ F ⇔ F

⊦ ∀t. t ∧ T ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀t. F ⇒ t ⇔ T

⊦ ∀t. T ⇒ t ⇔ t

⊦ ∀t. t ⇒ T ⇔ T

⊦ ∀t. F ∨ t ⇔ t

⊦ ∀t. T ∨ t ⇔ T

⊦ ∀t. t ∨ F ⇔ t

⊦ ∀t. t ∨ T ⇔ T

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀t1 t2. (let x ← t2 in t1) = t1

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

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

⊦ ∀t. t ⇒ F ⇔ ¬t

⊦ ∀x. (select y. y = x) = x

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

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀t1 t2. (if F then t1 else t2) = t2

⊦ ∀t1 t2. (if T then t1 else t2) = t1

⊦ ∀b t. (if b then t else t) = t

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

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

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

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

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

⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1

⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b

⊦ ∀p. (∀b. p b) ⇔ p T ∧ p F

⊦ ∀p. (∃b. p b) ⇔ p T ∨ p F

⊦ ∀p. p F ∧ p T ⇒ ∀x. p x

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

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

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

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

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

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

⊦ ∀p q. (q ⇒ p) ⇒ ¬p ⇒ ¬q

⊦ ∀t1 t2. ¬(t1 ⇒ t2) ⇔ t1 ∧ ¬t2

⊦ ∀t1 t2. (¬t1 ⇔ ¬t2) ⇔ t1 ⇔ t2

⊦ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1

⊦ ∀t1 t2. ¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2

⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2

⊦ ∀a b. ∃f. f F = a ∧ f T = b

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ ∀f g. (∀x. f x = g x) ⇒ f = g

⊦ ∀p a. (∀x. a = x ⇒ p x) ⇔ p a

⊦ ∀p a. (∀x. x = a ⇒ p x) ⇔ p a

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ ∀p a. (∃x. x = a ∧ p x) ⇔ p a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r

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

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

⊦ ∀p x. (∀y. p y ⇔ y = x) ⇒ (select) p = x

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

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

⊦ ∀b f g. (λx. if b then f x else g x) = if b then f else g

⊦ ∀b t1 t2. (if b then t1 else t2) ⇔ (¬b ∨ t1) ∧ (b ∨ t2)

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

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

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

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

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

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

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y

⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x

⊦ ∀p. (∃!x. p x) ⇔ ∃x. p x ∧ ∀y. p y ⇒ y = 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 ⇒ q x) ⇒ (∃x. p x) ⇒ ∃x. q x

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

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

⊦ cond = λt t1 t2. select x. ((t ⇔ T) ⇒ x = t1) ∧ ((t ⇔ F) ⇒ x = t2)

⊦ ∀p1 p2 q1 q2. (p1 ⇒ p2) ∧ (q1 ⇒ q2) ⇒ p1 ∧ q1 ⇒ p2 ∧ q2

⊦ ∀p1 p2 q1 q2. (p1 ⇒ p2) ∧ (q1 ⇒ q2) ⇒ p1 ∨ q1 ⇒ p2 ∨ q2

⊦ ∀p1 p2 q1 q2. (p2 ⇒ p1) ∧ (q1 ⇒ q2) ⇒ (p1 ⇒ q1) ⇒ p2 ⇒ q2

⊦ ∀p. (∀x. ∃!y. p x y) ⇔ ∃f. ∀x y. p x y ⇔ f x = y

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀p. (∃!x. p x) ⇔ (∃x. p x) ∧ ∀x x'. p x ∧ p x' ⇒ x = x'

⊦ ∀b p q r s. (p ⇒ q) ∧ (r ⇒ s) ⇒ (if b then p else r) ⇒ if b then q else s

Input Type Operators

→
bool

Input Constants

=
select

Assumptions

⊦ let a d ← (λe. d e) = d in a = λb. (λc. c) = λc. c

⊦ let a d ←
      let e g ←
          (let h ← d g in
           λi.
             (let j ← h in
              λk. (λl. l j k) = λm. m ((λc. c) = λc. c) ((λc. c) = λc. c))
               i ⇔ h) (d ((select) d)) in
      e = (λf. (λc. c) = λc. c) in
  a = λb. (λc. c) = λc. c