Package bool-class: Classical boolean theorems

Information

namebool-class
version1.13
descriptionClassical boolean theorems
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-12-18
requiresbool-def
bool-int
axiom-extensionality
bool-ext
axiom-choice
showData.Bool

Files

Theorems

t. t ¬t

() = λp. p ((select) p)

t. ¬¬t t

x. (select y. y = x) = x

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. (b. p b) p T p F

p. (b. p b) p T p F

p. p F p T 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. ¬(x. p x) x. ¬p x

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

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. (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. (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)

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. ∃!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)

b p q r s. (p q) (r s) (if b then p else r) if b then q else s

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

t. t t

F p. p

(¬) = λp. p F

t. (x. t) t

t. (λx. t x) = t

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

t. (T t) t

t. (t T) t

t. F t 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 T T

t. (F t) ¬t

t. (t F) ¬t

() = λp q. p q p

p x. p x p ((select) p)

x y. x = y y = x

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

() = λp. q. (x. p x q) q

f g. (x. f x = g x) f = g

f g. (x. f x = g x) f = g

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

p q. (x. p x q x) (x. p x) x. q x

cond = λt t1 t2. select x. ((t T) x = t1) ((t F) x = t2)

p. (∃!x. p x) (x. p x) x x'. p x p x' x = x'