Theory "bool"

Signature

Axioms

BOOL_CASES_AX

|- ∀t. (t ⇔ T) ∨ (t ⇔ F)

ETA_AX

|- ∀t. (λx. t x) = t

SELECT_AX

|- ∀P x. P x ⇒ P ($@ P)

INFINITY_AX

|- ∃f. ONE_ONE f ∧ ¬ONTO f

Definitions

T_DEF

|- T ⇔ ((λx. x) = (λx. x))

FORALL_DEF

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

EXISTS_DEF

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

AND_DEF

|- $/\ = (λt1 t2. ∀t. (t1 ⇒ t2 ⇒ t) ⇒ t)

OR_DEF

|- $\/ = (λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t)

F_DEF

|- F ⇔ ∀t. t

NOT_DEF

|- $~ = (λt. t ⇒ F)

EXISTS_UNIQUE_DEF

|- $?! = (λP. $? P ∧ ∀x y. P x ∧ P y ⇒ (x = y))

LET_DEF

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

COND_DEF

|- COND = (λt t1 t2. @x. ((t ⇔ T) ⇒ (x = t1)) ∧ ((t ⇔ F) ⇒ (x = t2)))

ONE_ONE_DEF

|- ONE_ONE = (λf. ∀x1 x2. (f x1 = f x2) ⇒ (x1 = x2))

ONTO_DEF

|- ONTO = (λf. ∀y. ∃x. y = f x)

TYPE_DEFINITION

|- TYPE_DEFINITION =
   (λP rep.
      (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧ ∀x. P x ⇔ ∃x'. x = rep x')

literal_case_DEF

|- literal_case = (λf x. f x)

IN_DEF

|- $IN = (λx f. f x)

RES_FORALL_DEF

|- RES_FORALL = (λp m. ∀x. x ∈ p ⇒ m x)

RES_EXISTS_DEF

|- RES_EXISTS = (λp m. ∃x. x ∈ p ∧ m x)

RES_EXISTS_UNIQUE_DEF

|- RES_EXISTS_UNIQUE = (λp m. (∃x::p. m x) ∧ ∀x y::p. m x ∧ m y ⇒ (x = y))

RES_SELECT_DEF

|- RES_SELECT = (λp m. @x. x ∈ p ∧ m x)

BOUNDED_DEF

|- BOUNDED = (λv. T)

DATATYPE_TAG_DEF

|- DATATYPE = (λx. T)

RES_ABSTRACT_DEF

|- (∀p m x. x ∈ p ⇒ (RES_ABSTRACT p m x = m x)) ∧
   ∀p m1 m2.
     (∀x. x ∈ p ⇒ (m1 x = m2 x)) ⇒ (RES_ABSTRACT p m1 = RES_ABSTRACT p m2)

itself_TY_DEF

|- ∃rep. TYPE_DEFINITION ($= ARB) rep

itself_case_thm

|- ∀b. (case (:α) of (:α) => b) = b

Theorems

TRUTH

|- T

IMP_ANTISYM_AX

|- ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

FALSITY

|- ∀t. F ⇒ t

ETA_THM

|- ∀M. (λx. M x) = M

EXCLUDED_MIDDLE

|- ∀t. t ∨ ¬t

BETA_THM

|- ∀f y. (λx. f x) y = f y

LET_THM

|- ∀f x. LET f x = f x

FORALL_THM

|- $! f ⇔ ∀x. f x

EXISTS_THM

|- $? f ⇔ ∃x. f x

ABS_SIMP

|- ∀t1 t2. (λx. t1) t2 = t1

FORALL_SIMP

|- ∀t. (∀x. t) ⇔ t

EXISTS_SIMP

|- ∀t. (∃x. t) ⇔ t

AND_INTRO_THM

|- ∀t1 t2. t1 ⇒ t2 ⇒ t1 ∧ t2

AND1_THM

|- ∀t1 t2. t1 ∧ t2 ⇒ t1

AND2_THM

|- ∀t1 t2. t1 ∧ t2 ⇒ t2

CONJ_SYM

|- ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

CONJ_COMM

|- ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

CONJ_ASSOC

|- ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3

OR_INTRO_THM1

|- ∀t1 t2. t1 ⇒ t1 ∨ t2

OR_INTRO_THM2

|- ∀t1 t2. t2 ⇒ t1 ∨ t2

OR_ELIM_THM

|- ∀t t1 t2. t1 ∨ t2 ⇒ (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t

IMP_F

|- ∀t. (t ⇒ F) ⇒ ¬t

F_IMP

|- ∀t. ¬t ⇒ t ⇒ F

NOT_F

|- ∀t. ¬t ⇒ (t ⇔ F)

NOT_AND

|- ¬(t ∧ ¬t)

AND_CLAUSES

|- ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

OR_CLAUSES

|- ∀t. (T ∨ t ⇔ T) ∧ (t ∨ T ⇔ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)

IMP_CLAUSES

|- ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

NOT_CLAUSES

|- (∀t. ¬ ¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

EQ_REFL

|- ∀x. x = x

REFL_CLAUSE

|- ∀x. (x = x) ⇔ T

EQ_SYM

|- ∀x y. (x = y) ⇒ (y = x)

EQ_SYM_EQ

|- ∀x y. (x = y) ⇔ (y = x)

EQ_EXT

|- ∀f g. (∀x. f x = g x) ⇒ (f = g)

FUN_EQ_THM

|- ∀f g. (f = g) ⇔ ∀x. f x = g x

EQ_TRANS

|- ∀x y z. (x = y) ∧ (y = z) ⇒ (x = z)

BOOL_EQ_DISTINCT

|- (T ⇎ F) ∧ (F ⇎ T)

EQ_CLAUSES

|- ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

COND_CLAUSES

|- ∀t1 t2. ((if T then t1 else t2) = t1) ∧ ((if F then t1 else t2) = t2)

COND_ID

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

SELECT_THM

|- ∀P. P (@x. P x) ⇔ ∃x. P x

SELECT_REFL

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

SELECT_REFL_2

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

SELECT_UNIQUE

|- ∀P x. (∀y. P y ⇔ (y = x)) ⇒ ($@ P = x)

SELECT_ELIM_THM

|- ∀P Q. (∃x. P x) ∧ (∀x. P x ⇒ Q x) ⇒ Q ($@ P)

NOT_FORALL_THM

|- ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x

NOT_EXISTS_THM

|- ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x

FORALL_AND_THM

|- ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

LEFT_AND_FORALL_THM

|- ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q

RIGHT_AND_FORALL_THM

|- ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x

EXISTS_OR_THM

|- ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x

LEFT_OR_EXISTS_THM

|- ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q

RIGHT_OR_EXISTS_THM

|- ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x

BOTH_EXISTS_AND_THM

|- ∀P Q. (∃x. P ∧ Q) ⇔ (∃x. P) ∧ ∃x. Q

LEFT_EXISTS_AND_THM

|- ∀P Q. (∃x. P x ∧ Q) ⇔ (∃x. P x) ∧ Q

RIGHT_EXISTS_AND_THM

|- ∀P Q. (∃x. P ∧ Q x) ⇔ P ∧ ∃x. Q x

BOTH_FORALL_OR_THM

|- ∀P Q. (∀x. P ∨ Q) ⇔ (∀x. P) ∨ ∀x. Q

LEFT_FORALL_OR_THM

|- ∀Q P. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q

RIGHT_FORALL_OR_THM

|- ∀P Q. (∀x. P ∨ Q x) ⇔ P ∨ ∀x. Q x

BOTH_FORALL_IMP_THM

|- ∀P Q. (∀x. P ⇒ Q) ⇔ (∃x. P) ⇒ ∀x. Q

LEFT_FORALL_IMP_THM

|- ∀P Q. (∀x. P x ⇒ Q) ⇔ (∃x. P x) ⇒ Q

RIGHT_FORALL_IMP_THM

|- ∀P Q. (∀x. P ⇒ Q x) ⇔ P ⇒ ∀x. Q x

BOTH_EXISTS_IMP_THM

|- ∀P Q. (∃x. P ⇒ Q) ⇔ (∀x. P) ⇒ ∃x. Q

LEFT_EXISTS_IMP_THM

|- ∀P Q. (∃x. P x ⇒ Q) ⇔ (∀x. P x) ⇒ Q

RIGHT_EXISTS_IMP_THM

|- ∀P Q. (∃x. P ⇒ Q x) ⇔ P ⇒ ∃x. Q x

OR_IMP_THM

|- ∀A B. (A ⇔ B ∨ A) ⇔ B ⇒ A

NOT_IMP

|- ∀A B. ¬(A ⇒ B) ⇔ A ∧ ¬B

DISJ_ASSOC

|- ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

DISJ_SYM

|- ∀A B. A ∨ B ⇔ B ∨ A

DISJ_COMM

|- ∀A B. A ∨ B ⇔ B ∨ A

DE_MORGAN_THM

|- ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)

LEFT_AND_OVER_OR

|- ∀A B C. A ∧ (B ∨ C) ⇔ A ∧ B ∨ A ∧ C

RIGHT_AND_OVER_OR

|- ∀A B C. (B ∨ C) ∧ A ⇔ B ∧ A ∨ C ∧ A

LEFT_OR_OVER_AND

|- ∀A B C. A ∨ B ∧ C ⇔ (A ∨ B) ∧ (A ∨ C)

RIGHT_OR_OVER_AND

|- ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)

IMP_DISJ_THM

|- ∀A B. A ⇒ B ⇔ ¬A ∨ B

DISJ_IMP_THM

|- ∀P Q R. P ∨ Q ⇒ R ⇔ (P ⇒ R) ∧ (Q ⇒ R)

IMP_CONJ_THM

|- ∀P Q R. P ⇒ Q ∧ R ⇔ (P ⇒ Q) ∧ (P ⇒ R)

IMP_F_EQ_F

|- ∀t. t ⇒ F ⇔ (t ⇔ F)

AND_IMP_INTRO

|- ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3

EQ_IMP_THM

|- ∀t1 t2. (t1 ⇔ t2) ⇔ (t1 ⇒ t2) ∧ (t2 ⇒ t1)

EQ_EXPAND

|- ∀t1 t2. (t1 ⇔ t2) ⇔ t1 ∧ t2 ∨ ¬t1 ∧ ¬t2

COND_RATOR

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

COND_RAND

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

COND_ABS

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

COND_EXPAND

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

COND_EXPAND_IMP

|- ∀b t1 t2. (if b then t1 else t2) ⇔ (b ⇒ t1) ∧ (¬b ⇒ t2)

COND_EXPAND_OR

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

TYPE_DEFINITION_THM

|- ∀P rep.
     TYPE_DEFINITION P rep ⇔
     (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧ ∀x. P x ⇔ ∃x'. x = rep x'

ONTO_THM

|- ∀f. ONTO f ⇔ ∀y. ∃x. y = f x

ONE_ONE_THM

|- ∀f. ONE_ONE f ⇔ ∀x1 x2. (f x1 = f x2) ⇒ (x1 = x2)

ABS_REP_THM

|- ∀P.
     (∃rep. TYPE_DEFINITION P rep) ⇒
     ∃rep abs. (∀a. abs (rep a) = a) ∧ ∀r. P r ⇔ (rep (abs r) = r)

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)

SWAP_FORALL_THM

|- ∀P. (∀x y. P x y) ⇔ ∀y x. P x y

SWAP_EXISTS_THM

|- ∀P. (∃x y. P x y) ⇔ ∃y x. P x y

EXISTS_UNIQUE_THM

|- (∃!x. P x) ⇔ (∃x. P x) ∧ ∀x y. P x ∧ P y ⇒ (x = y)

LET_CONG

|- ∀f g M N. (M = N) ∧ (∀x. (x = N) ⇒ (f x = g x)) ⇒ (LET f M = LET g N)

IMP_CONG

|- ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')

AND_CONG

|- ∀P P' Q Q'. (Q ⇒ (P ⇔ P')) ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

LEFT_AND_CONG

|- ∀P P' Q Q'. (P ⇔ P') ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

OR_CONG

|- ∀P P' Q Q'. (¬Q ⇒ (P ⇔ P')) ∧ (¬P' ⇒ (Q ⇔ Q')) ⇒ (P ∨ Q ⇔ P' ∨ Q')

LEFT_OR_CONG

|- ∀P P' Q Q'. (P ⇔ P') ∧ (¬P' ⇒ (Q ⇔ Q')) ⇒ (P ∨ Q ⇔ P' ∨ Q')

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')

RES_FORALL_CONG

|- (P = Q) ⇒ (∀x. x ∈ Q ⇒ (f x ⇔ g x)) ⇒ (RES_FORALL P f ⇔ RES_FORALL Q g)

RES_EXISTS_CONG

|- (P = Q) ⇒ (∀x. x ∈ Q ⇒ (f x ⇔ g x)) ⇒ (RES_EXISTS P f ⇔ RES_EXISTS Q g)

MONO_AND

|- (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w

MONO_OR

|- (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∨ z ⇒ y ∨ w

MONO_IMP

|- (y ⇒ x) ∧ (z ⇒ w) ⇒ (x ⇒ z) ⇒ y ⇒ w

MONO_NOT

|- (y ⇒ x) ⇒ ¬x ⇒ ¬y

MONO_NOT_EQ

|- y ⇒ x ⇔ ¬x ⇒ ¬y

MONO_ALL

|- (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x

MONO_EXISTS

|- (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x

MONO_COND

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

EXISTS_REFL

|- ∀a. ∃x. x = a

EXISTS_UNIQUE_REFL

|- ∀a. ∃!x. x = a

UNWIND_THM1

|- ∀P a. (∃x. (a = x) ∧ P x) ⇔ P a

UNWIND_THM2

|- ∀P a. (∃x. (x = a) ∧ P x) ⇔ P a

UNWIND_FORALL_THM1

|- ∀f v. (∀x. (v = x) ⇒ f x) ⇔ f v

UNWIND_FORALL_THM2

|- ∀f v. (∀x. (x = v) ⇒ f x) ⇔ f v

SKOLEM_THM

|- ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)

bool_case_thm

|- (∀t1 t2. (if T then t1 else t2) = t1) ∧ ∀t1 t2. (if F then t1 else t2) = t2

bool_case_ID

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

boolAxiom

|- ∀t1 t2. ∃fn. (fn T = t1) ∧ (fn F = t2)

bool_INDUCT

|- ∀P. P T ∧ P F ⇒ ∀b. P b

bool_case_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')

FORALL_BOOL

|- (∀b. P b) ⇔ P T ∧ P F

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

RES_FORALL_THM

|- ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

RES_EXISTS_THM

|- ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x

RES_EXISTS_UNIQUE_THM

|- ∀P f. RES_EXISTS_UNIQUE P f ⇔ (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ (x = y)

RES_SELECT_THM

|- ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

RES_FORALL_TRUE

|- (∀x::P. T) ⇔ T

RES_EXISTS_FALSE

|- (∃x::P. F) ⇔ F

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

literal_case_THM

|- ∀f x. literal_case f x = f x

literal_case_RAND

|- P (case M of x => N x) ⇔ case M of x => P (N x)

literal_case_RATOR

|- (case M of x => N x) b = case M of x => N x b

literal_case_CONG

|- ∀f g M N.
     (M = N) ∧ (∀x. (x = N) ⇒ (f x = g x)) ⇒
     (literal_case f M = literal_case g N)

literal_case_id

|- (case a of a => t | x => u) = t

BOUNDED_THM

|- ∀v. BOUNDED v ⇔ T

LCOMM_THM

|- ∀f.
     (∀x y z. f x (f y z) = f (f x y) z) ⇒
     (∀x y. f x y = f y x) ⇒
     ∀x y z. f x (f y z) = f y (f x z)

DATATYPE_TAG_THM

|- ∀x. DATATYPE x ⇔ T

DATATYPE_BOOL

|- DATATYPE (bool T F) ⇔ T

ITSELF_UNIQUE

|- ∀i. i = (:α)

itself_Axiom

|- ∀e. ∃f. f (:β) = e

itself_induction

|- ∀P. P (:α) ⇒ ∀i. P i

PULL_EXISTS

|- ∀P Q.
     ((∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q) ∧ ((∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q) ∧
     (Q ∧ (∃x. P x) ⇔ ∃x. Q ∧ P x)

PULL_FORALL

|- ∀P Q.
     (Q ⇒ (∀x. P x) ⇔ ∀x. Q ⇒ P x) ∧ ((∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q) ∧
     (Q ∧ (∀x. P x) ⇔ ∀x. Q ∧ P x)

PEIRCE

|- ((P ⇒ Q) ⇒ P) ⇒ P

JRH_INDUCT_UTIL

|- ∀P t. (∀x. (x = t) ⇒ P x) ⇒ $? P