Theory: bool

Parents

• min

Types

Constants

• !  :('a -> bool) -> bool
• ?  :('a -> bool) -> bool
• F  :bool
• T  :bool
• ~  :bool -> bool
• /\  :bool -> bool -> bool
• ?!  :('a -> bool) -> bool
• \/  :bool -> bool -> bool
• ONTO  :('a -> 'b) -> bool
• ONE_ONE  :('a -> 'b) -> bool
• TYPE_DEFINITION  :('a -> bool) -> ('b -> 'a) -> bool
• ARB  :'a
• LET  :('a -> 'b) -> 'a -> 'b
• bool_case  :'a -> 'a -> bool -> 'a
• COND  :bool -> 'a -> 'a -> 'a

Axioms

BOOL_CASES_AX

|- !t. (t = T) \/ (t = F)

ETA_AX

|- !t. (\x. t x) = t

INFINITY_AX

|- ?f. ONE_ONE f /\ ~ONTO f

SELECT_AX

|- !P x. P x ==> P ($@ P)

Definitions

AND_DEF

|- $/\ = (\t1 t2. !t. (t1 ==> t2 ==> t) ==> t)

ARB_DEF

|- ARB = @x. T

bool_case_DEF

|- bool_case = (\x y b. (if b then x else y))

COND_DEF

|- COND = (\t t1 t2. @x. ((t = T) ==> (x = t1)) /\ ((t = F) ==> (x = t2)))

EXISTS_DEF

|- $? = (\P. P ($@ P))

EXISTS_UNIQUE_DEF

|- $?! = (\P. $? P /\ !x y. P x /\ P y ==> (x = y))

F_DEF

|- F = !t. t

FORALL_DEF

|- $! = (\P. P = (\x. T))

LET_DEF

|- LET = (\f x. f x)

NOT_DEF

|- $~ = (\t. t ==> F)

ONE_ONE_DEF

|- ONE_ONE = (\f. !x1 x2. (f x1 = f x2) ==> (x1 = x2))

ONTO_DEF

|- ONTO = (\f. !y. ?x. y = f x)

OR_DEF

|- $\/ = (\t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t)

T_DEF

|- T = ((\x. x) = (\x. x))

TYPE_DEFINITION

|- TYPE_DEFINITION =
   (\P rep.
      (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
      !x. P x = ?x'. x = rep x')

Theorems

ABS_REP_THM

|- !P.
     (?rep. TYPE_DEFINITION P rep) ==>
     ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r)

ABS_SIMP

|- !t1 t2. (\x. t1) t2 = t1

AND1_THM

|- !t1 t2. t1 /\ t2 ==> t1

AND2_THM

|- !t1 t2. t1 /\ t2 ==> t2

AND_CLAUSES

|- !t.
     (T /\ t = t) /\ (t /\ T = t) /\ (F /\ t = F) /\ (t /\ F = F) /\
     (t /\ t = t)

AND_CONG

|- !P P' Q Q'. (Q ==> (P = P')) /\ (P' ==> (Q = Q')) ==> (P /\ Q = P' /\ Q')

AND_IMP_INTRO

|- !t1 t2 t3. t1 ==> t2 ==> t3 = t1 /\ t2 ==> t3

AND_INTRO_THM

|- !t1 t2. t1 ==> t2 ==> t1 /\ t2

BETA_THM

|- !f y. (\x. f x) y = f y

bool_case_ID

|- !x b. bool_case x x b = x

bool_case_thm

|- (!e0 e1. bool_case e0 e1 T = e0) /\ !e0 e1. bool_case e0 e1 F = e1

BOOL_EQ_DISTINCT

|- ~(T = F) /\ ~(F = T)

BOOL_FUN_CASES_THM

|- !f. (f = (\b. T)) \/ (f = (\b. F)) \/ (f = (\b. b)) \/ (f = (\b. ~b))

BOOL_FUN_INDUCT

|- !P. P (\b. T) /\ P (\b. F) /\ P (\b. b) /\ P (\b. ~b) ==> !f. P f

bool_INDUCT

|- !P. P T /\ P F ==> !b. P b

boolAxiom

|- !e0 e1. ?fn. (fn T = e0) /\ (fn F = e1)

BOTH_EXISTS_AND_THM

|- !P Q. (?x. P /\ Q) = (?x. P) /\ ?x. Q

BOTH_EXISTS_IMP_THM

|- !P Q. (?x. P ==> Q) = (!x. P) ==> ?x. Q

BOTH_FORALL_IMP_THM

|- !P Q. (!x. P ==> Q) = (?x. P) ==> !x. Q

BOTH_FORALL_OR_THM

|- !P Q. (!x. P \/ Q) = (!x. P) \/ !x. Q

COND_ABS

|- !b f g. (\x. (if b then f x else g x)) = (if b then f else g)

COND_CLAUSES

|- !t1 t2. ((if T then t1 else t2) = t1) /\ ((if F then t1 else t2) = t2)

COND_CONG

|- !P Q x x' y y'.
     (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==>
     ((if P then x else y) = (if Q then x' else y'))

COND_EXPAND

|- !b t1 t2. (if b then t1 else t2) = (~b \/ t1) /\ (b \/ t2)

COND_ID

|- !b t. (if b then t else t) = t

COND_RAND

|- !f b x y. f (if b then x else y) = (if b then f x else f y)

COND_RATOR

|- !b f g x. (if b then f else g) x = (if b then f x else g x)

CONJ_ASSOC

|- !t1 t2 t3. t1 /\ t2 /\ t3 = (t1 /\ t2) /\ t3

CONJ_COMM

|- !t1 t2. t1 /\ t2 = t2 /\ t1

CONJ_SYM

|- !t1 t2. t1 /\ t2 = t2 /\ t1

DE_MORGAN_THM

|- !A B. (~(A /\ B) = ~A \/ ~B) /\ (~(A \/ B) = ~A /\ ~B)

DISJ_ASSOC

|- !A B C. A \/ B \/ C = (A \/ B) \/ C

DISJ_COMM

|- !A B. A \/ B = B \/ A

DISJ_IMP_THM

|- !P Q R. P \/ Q ==> R = (P ==> R) /\ (Q ==> R)

DISJ_SYM

|- !A B. A \/ B = B \/ A

EQ_CLAUSES

|- !t. ((T = t) = t) /\ ((t = T) = t) /\ ((F = t) = ~t) /\ ((t = F) = ~t)

EQ_EXPAND

|- !t1 t2. (t1 = t2) = t1 /\ t2 \/ ~t1 /\ ~t2

EQ_EXT

|- !f g. (!x. f x = g x) ==> (f = g)

EQ_IMP_THM

|- !t1 t2. (t1 = t2) = (t1 ==> t2) /\ (t2 ==> t1)

EQ_REFL

|- !x. x = x

EQ_SYM

|- !x y. (x = y) ==> (y = x)

EQ_SYM_EQ

|- !x y. (x = y) = (y = x)

EQ_TRANS

|- !x y z. (x = y) /\ (y = z) ==> (x = z)

ETA_THM

|- !M. (\x. M x) = M

EXCLUDED_MIDDLE

|- !t. t \/ ~t

EXISTS_OR_THM

|- !P Q. (?x. P x \/ Q x) = (?x. P x) \/ ?x. Q x

EXISTS_REFL

|- !a. ?x. x = a

EXISTS_SIMP

|- !t. (?x. t) = t

EXISTS_UNIQUE_REFL

|- !a. ?!x. x = a

EXISTS_UNIQUE_THM

|- (?!x. P x) = (?x. P x) /\ !x y. P x /\ P y ==> (x = y)

F_IMP

|- !t. ~t ==> t ==> F

FALSITY

|- !t. F ==> t

FORALL_AND_THM

|- !P Q. (!x. P x /\ Q x) = (!x. P x) /\ !x. Q x

FORALL_SIMP

|- !t. (!x. t) = t

FUN_EQ_THM

|- !f g. (f = g) = !x. f x = g x

IMP_ANTISYM_AX

|- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 = t2)

IMP_CLAUSES

|- !t.
     (T ==> t = t) /\ (t ==> T = T) /\ (F ==> t = T) /\ (t ==> t = T) /\
     (t ==> F = ~t)

IMP_CONG

|- !x x' y y'. (x = x') /\ (x' ==> (y = y')) ==> (x ==> y = x' ==> y')

IMP_DISJ_THM

|- !A B. A ==> B = ~A \/ B

IMP_F

|- !t. (t ==> F) ==> ~t

IMP_F_EQ_F

|- !t. t ==> F = (t = F)

LEFT_AND_FORALL_THM

|- !P Q. (!x. P x) /\ Q = !x. P x /\ Q

LEFT_AND_OVER_OR

|- !A B C. A /\ (B \/ C) = A /\ B \/ A /\ C

LEFT_EXISTS_AND_THM

|- !P Q. (?x. P x /\ Q) = (?x. P x) /\ Q

LEFT_EXISTS_IMP_THM

|- !P Q. (?x. P x ==> Q) = (!x. P x) ==> Q

LEFT_FORALL_IMP_THM

|- !P Q. (!x. P x ==> Q) = (?x. P x) ==> Q

LEFT_FORALL_OR_THM

|- !Q P. (!x. P x \/ Q) = (!x. P x) \/ Q

LEFT_OR_EXISTS_THM

|- !P Q. (?x. P x) \/ Q = ?x. P x \/ Q

LEFT_OR_OVER_AND

|- !A B C. A \/ B /\ C = (A \/ B) /\ (A \/ C)

LET_CONG

|- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x)) ==> (LET f M = LET g N)

LET_RAND

|- P (let x = M in N x) = (let x = M in P (N x))

LET_RATOR

|- (let x = M in N x) b = (let x = M in N x b)

LET_THM

|- !f x. LET f x = f x

MONO_ALL

|- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x

MONO_AND

|- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w

MONO_COND

|- (x ==> y) ==> (z ==> w) ==> (if b then x else z) ==> (if b then y else w)

MONO_EXISTS

|- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x

MONO_IMP

|- (y ==> x) /\ (z ==> w) ==> (x ==> z) ==> y ==> w

MONO_NOT

|- (y ==> x) ==> ~x ==> ~y

MONO_OR

|- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w

NOT_AND

|- ~(t /\ ~t)

NOT_CLAUSES

|- (!t. ~~t = t) /\ (~T = F) /\ (~F = T)

NOT_EXISTS_THM

|- !P. ~(?x. P x) = !x. ~P x

NOT_F

|- !t. ~t ==> (t = F)

NOT_FORALL_THM

|- !P. ~(!x. P x) = ?x. ~P x

NOT_IMP

|- !A B. ~(A ==> B) = A /\ ~B

ONE_ONE_THM

|- !f. ONE_ONE f = !x1 x2. (f x1 = f x2) ==> (x1 = x2)

ONTO_THM

|- !f. ONTO f = !y. ?x. y = f x

OR_CLAUSES

|- !t.
     (T \/ t = T) /\ (t \/ T = T) /\ (F \/ t = t) /\ (t \/ F = t) /\
     (t \/ t = t)

OR_CONG

|- !P P' Q Q'. (~Q ==> (P = P')) /\ (~P' ==> (Q = Q')) ==> (P \/ Q = P' \/ Q')

OR_ELIM_THM

|- !t t1 t2. t1 \/ t2 ==> (t1 ==> t) ==> (t2 ==> t) ==> t

OR_IMP_THM

|- !A B. (A = B \/ A) = B ==> A

OR_INTRO_THM1

|- !t1 t2. t1 ==> t1 \/ t2

OR_INTRO_THM2

|- !t1 t2. t2 ==> t1 \/ t2

REFL_CLAUSE

|- !x. (x = x) = T

RIGHT_AND_FORALL_THM

|- !P Q. P /\ (!x. Q x) = !x. P /\ Q x

RIGHT_AND_OVER_OR

|- !A B C. (B \/ C) /\ A = B /\ A \/ C /\ A

RIGHT_EXISTS_AND_THM

|- !P Q. (?x. P /\ Q x) = P /\ ?x. Q x

RIGHT_EXISTS_IMP_THM

|- !P Q. (?x. P ==> Q x) = P ==> ?x. Q x

RIGHT_FORALL_IMP_THM

|- !P Q. (!x. P ==> Q x) = P ==> !x. Q x

RIGHT_FORALL_OR_THM

|- !P Q. (!x. P \/ Q x) = P \/ !x. Q x

RIGHT_OR_EXISTS_THM

|- !P Q. P \/ (?x. Q x) = ?x. P \/ Q x

RIGHT_OR_OVER_AND

|- !A B C. B /\ C \/ A = (B \/ A) /\ (C \/ A)

SELECT_REFL

|- !x. (@y. y = x) = x

SELECT_REFL_2

|- !x. (@y. x = y) = x

SELECT_THM

|- !P. P (@x. P x) = ?x. P x

SELECT_UNIQUE

|- !P x. (!y. P y = (y = x)) ==> ($@ P = x)

SKOLEM_THM

|- !P. (!x. ?y. P x y) = ?f. !x. P x (f x)

SWAP_EXISTS_THM

|- !P. (?x y. P x y) = ?y x. P x y

SWAP_FORALL_THM

|- !P. (!x y. P x y) = !y x. P x y

TRUTH

|- T

TYPE_DEFINITION_THM

|- !P rep.
     TYPE_DEFINITION P rep =
     (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\ !x. P x = ?x'. x = rep x'

UEXISTS_OR_THM

|- !P Q. (?!x. P x \/ Q x) ==> (?!x. P x) \/ ?!x. Q x

UEXISTS_SIMP

|- (?!x. t) = t /\ !x y. x = y

UNWIND_FORALL_THM1

|- !f v. (!x. (v = x) ==> f x) = f v

UNWIND_FORALL_THM2

|- !f v. (!x. (x = v) ==> f x) = f v

UNWIND_THM1

|- !P a. (?x. (a = x) /\ P x) = P a

UNWIND_THM2

|- !P a. (?x. (x = a) /\ P x) = P a