Package bool-class: Classical boolean theorems

Information

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

Files

Theorems

t. t ¬t

() = λP. P ((select) P)

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

t. (t T) (t F)

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 t2 t1

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)

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

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

(t. ¬¬t t) (¬T F) (¬F T)

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)

t1 t2. (¬(t1 t2) ¬t1 ¬t2) (¬(t1 t2) ¬t1 ¬t2)

b A B C D. (A B) (C D) (if b then A else C) if b then B else D

Input Type Operators

Input Constants

Assumptions

T

F p. p

(¬) = λp. p F

t. (x. t) t

t. (λx. t x) = t

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

x. x = x T

() = λp q. p q p

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

(¬T F) (¬F T)

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

() = λP. q. (x. P x q) q

f g. f = g x. f x = g x

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'

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)