Package bool-class: Classical boolean theorems

Information

namebool-class
version1.22
descriptionClassical boolean theorems
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-06-12
requiresaxiom-choice
axiom-extensionality
bool-def
bool-ext
bool-int
showData.Bool

Files

Theorems

t. t ¬t

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

t. ¬¬t t

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

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

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

p. (b. p b) p p

p. (b. p b) p p

p. p p 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 = a f = b

c x y. (if ¬c then x else y) = if c then y else 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. (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

r. (x. y. r x y) f. x. r x (f 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)

p r. (x. p x y. r x y) f. x. p x r x (f x)

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

External Type Operators

External Constants

Assumptions

¬

¬

t. t t

p. p

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t

t. ( t) ¬t

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

() = λ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 ) x = t1) ((t ) x = t2)

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