Theory "bool"

Signature

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)

BOUNDED_DEF

⊢ BOUNDED = (λv. T)

COND_DEF

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

DATATYPE_TAG_DEF

⊢ DATATYPE = (λx. T)

EXISTS_DEF

⊢ $? = (λP. P ($@ P))

EXISTS_UNIQUE_DEF

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

FORALL_DEF

⊢ $! = (λP. P = (λx. T))

F_DEF

⊢ F ⇔ ∀t. t

IN_DEF

⊢ $IN = (λx f. f x)

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)

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)

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_FORALL_DEF

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

RES_SELECT_DEF

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

TYPE_DEFINITION

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

T_DEF

⊢ T ⇔ ((λx. x) = (λx. x))

itself_TY_DEF

⊢ ∃rep. TYPE_DEFINITION ($= ARB) rep

itself_case_thm

⊢ ∀b. (case (:α) of (:α) => b) = b

literal_case_DEF

⊢ literal_case = (λf x. f 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_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

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

BOUNDED_THM

⊢ ∀v. BOUNDED v ⇔ T

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_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

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

DATATYPE_BOOL

⊢ DATATYPE (bool T F) ⇔ T

DATATYPE_TAG_THM

⊢ ∀x. DATATYPE x ⇔ T

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_EQ_IMP

⊢ ∀A B. A ∨ B ⇔ ¬A ⇒ B

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_THM

⊢ $? f ⇔ ∃x. f x

EXISTS_UNIQUE_ALT'

⊢ (∃!x. P x) ⇔ ∃x. ∀y. P y ⇔ (y = x)

EXISTS_UNIQUE_REFL

⊢ ∀a. ∃!x. x = a

EXISTS_UNIQUE_THM

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

EXISTS_itself

⊢ (∃x. P x) ⇔ P (:α)

FALSITY

⊢ ∀t. F ⇒ t

FORALL_AND_THM

⊢ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

FORALL_BOOL

⊢ (∀b. P b) ⇔ P T ∧ P F

FORALL_SIMP

⊢ ∀t. (∀x. t) ⇔ t

FORALL_THM

⊢ $! f ⇔ ∀x. f x

FORALL_itself

⊢ (∀x. P x) ⇔ P (:α)

FUN_EQ_THM

⊢ ∀f g. (f = g) ⇔ ∀x. f x = g x

F_IMP

⊢ ∀t. ¬t ⇒ t ⇒ F

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_CONJ_THM

⊢ ∀P Q R. P ⇒ Q ∧ R ⇔ (P ⇒ Q) ∧ (P ⇒ R)

IMP_DISJ_THM

⊢ ∀A B. A ⇒ B ⇔ ¬A ∨ B

IMP_F

⊢ ∀t. (t ⇒ F) ⇒ ¬t

IMP_F_EQ_F

⊢ ∀t. t ⇒ F ⇔ (t ⇔ F)

ITSELF_UNIQUE

⊢ ∀i. i = (:α)

JRH_INDUCT_UTIL

⊢ ∀P t. (∀x. (x = t) ⇒ P x) ⇒ $? P

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)

LEFT_AND_CONG

⊢ ∀P P' Q Q'. (P ⇔ P') ∧ (P' ⇒ (Q ⇔ Q')) ⇒ (P ∧ Q ⇔ P' ∧ Q')

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_CONG

⊢ ∀P P' Q Q'. (P ⇔ P') ∧ (¬P' ⇒ (Q ⇔ Q')) ⇒ (P ∨ Q ⇔ P' ∨ 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_NOT_EQ

⊢ 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

PEIRCE

⊢ ((P ⇒ Q) ⇒ P) ⇒ P

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)

REFL_CLAUSE

⊢ ∀x. (x = x) ⇔ T

RES_EXISTS_CONG

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

RES_EXISTS_FALSE

⊢ (∃x::P. F) ⇔ F

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_FORALL_CONG

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

RES_FORALL_THM

⊢ ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

RES_FORALL_TRUE

⊢ (∀x::P. T) ⇔ T

RES_SELECT_THM

⊢ ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

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_ELIM_THM

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

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

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

bool_case_ID

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

bool_case_thm

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

itself_Axiom

⊢ ∀e. ∃f. f (:α) = e

itself_induction

⊢ ∀P. P (:α) ⇒ ∀i. P i

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_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_THM

⊢ ∀f x. literal_case f x = f x

literal_case_id

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