Theory "pair"

Signature

Definitions

prod_TY_DEF

|- ∃rep. TYPE_DEFINITION (λp. ∃x y. p = (λa b. (a = x) ∧ (b = y))) rep

ABS_REP_prod

|- (∀a. ABS_prod (REP_prod a) = a) ∧
   ∀r.
     (λp. ∃x y. p = (λa b. (a = x) ∧ (b = y))) r ⇔ (REP_prod (ABS_prod r) = r)

COMMA_DEF

|- ∀x y. (x,y) = ABS_prod (λa b. (a = x) ∧ (b = y))

PAIR

|- ∀x. (FST x,SND x) = x

SWAP_def

|- ∀a. SWAP a = (SND a,FST a)

CURRY_DEF

|- ∀f x y. CURRY f x y = f (x,y)

UNCURRY

|- ∀f v. UNCURRY f v = f (FST v) (SND v)

PAIR_MAP

|- ∀f g p. (f ## g) p = (f (FST p),g (SND p))

pair_CASE_def

|- ∀p f. pair_CASE p f = f (FST p) (SND p)

LEX_DEF

|- ∀R1 R2. R1 LEX R2 = (λ(s,t) (u,v). R1 s u ∨ (s = u) ∧ R2 t v)

RPROD_DEF

|- ∀R1 R2. RPROD R1 R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)

Theorems

PAIR_EQ

|- ((x,y) = (a,b)) ⇔ (x = a) ∧ (y = b)

CLOSED_PAIR_EQ

|- ∀x y a b. ((x,y) = (a,b)) ⇔ (x = a) ∧ (y = b)

ABS_PAIR_THM

|- ∀x. ∃q r. x = (q,r)

pair_CASES

|- ∀x. ∃q r. x = (q,r)

FST

|- ∀x y. FST (x,y) = x

SND

|- ∀x y. SND (x,y) = y

PAIR_FST_SND_EQ

|- ∀p q. (p = q) ⇔ (FST p = FST q) ∧ (SND p = SND q)

UNCURRY_VAR

|- ∀f v. UNCURRY f v = f (FST v) (SND v)

ELIM_UNCURRY

|- ∀f. UNCURRY f = (λx. f (FST x) (SND x))

UNCURRY_DEF

|- ∀f x y. UNCURRY f (x,y) = f x y

CURRY_UNCURRY_THM

|- ∀f. CURRY (UNCURRY f) = f

UNCURRY_CURRY_THM

|- ∀f. UNCURRY (CURRY f) = f

CURRY_ONE_ONE_THM

|- (CURRY f = CURRY g) ⇔ (f = g)

UNCURRY_ONE_ONE_THM

|- (UNCURRY f = UNCURRY g) ⇔ (f = g)

pair_Axiom

|- ∀f. ∃fn. ∀x y. fn (x,y) = f x y

UNCURRY_CONG

|- ∀f' f M' M.
     (M = M') ∧ (∀x y. (M' = (x,y)) ⇒ (f x y = f' x y)) ⇒
     (UNCURRY f M = UNCURRY f' M')

LAMBDA_PROD

|- ∀P. (λp. P p) = (λ(p1,p2). P (p1,p2))

EXISTS_PROD

|- (∃p. P p) ⇔ ∃p_1 p_2. P (p_1,p_2)

FORALL_PROD

|- (∀p. P p) ⇔ ∀p_1 p_2. P (p_1,p_2)

pair_induction

|- (∀p_1 p_2. P (p_1,p_2)) ⇒ ∀p. P p

ELIM_PEXISTS

|- (∃p. P (FST p) (SND p)) ⇔ ∃p1 p2. P p1 p2

ELIM_PFORALL

|- (∀p. P (FST p) (SND p)) ⇔ ∀p1 p2. P p1 p2

PFORALL_THM

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

PEXISTS_THM

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

ELIM_PEXISTS_EVAL

|- $? (UNCURRY (λx. P x)) ⇔ ∃x. $? (P x)

ELIM_PFORALL_EVAL

|- $! (UNCURRY (λx. P x)) ⇔ ∀x. $! (P x)

PAIR_MAP_THM

|- ∀f g x y. (f ## g) (x,y) = (f x,g y)

FST_PAIR_MAP

|- ∀p f g. FST ((f ## g) p) = f (FST p)

SND_PAIR_MAP

|- ∀p f g. SND ((f ## g) p) = g (SND p)

LET2_RAND

|- ∀P M N. P (let (x,y) = M in N x y) = (let (x,y) = M in P (N x y))

LET2_RATOR

|- ∀M N b. (let (x,y) = M in N x y) b = (let (x,y) = M in N x y b)

o_UNCURRY_R

|- f o UNCURRY g = UNCURRY ($o f o g)

C_UNCURRY_L

|- combin$C (UNCURRY f) x = UNCURRY (combin$C (combin$C o f) x)

S_UNCURRY_R

|- S f (UNCURRY g) = UNCURRY (S (S o $o f o $,) g)

FORALL_UNCURRY

|- $! (UNCURRY f) ⇔ $! ($! o f)

PAIR_FUN_THM

|- ∀P. (∃!f. P f) ⇔ ∃!p. P (λa. (FST p a,SND p a))

pair_case_thm

|- pair_CASE (x,y) f = f x y

pair_case_def

|- pair_CASE (x,y) f = f x y

pair_case_cong

|- ∀M M' f.
     (M = M') ∧ (∀x y. (M' = (x,y)) ⇒ (f x y = f' x y)) ⇒
     (pair_CASE M f = pair_CASE M' f')

datatype_pair

|- DATATYPE (pair $,)

LEX_DEF_THM

|- (R1 LEX R2) (a,b) (c,d) ⇔ R1 a c ∨ (a = c) ∧ R2 b d

WF_LEX

|- ∀R Q. WF R ∧ WF Q ⇒ WF (R LEX Q)

WF_RPROD

|- ∀R Q. WF R ∧ WF Q ⇒ WF (RPROD R Q)

total_LEX

|- total R1 ∧ total R2 ⇒ total (R1 LEX R2)

transitive_LEX

|- transitive R1 ∧ transitive R2 ⇒ transitive (R1 LEX R2)

reflexive_LEX

|- reflexive (R1 LEX R2) ⇔ reflexive R1 ∨ reflexive R2

symmetric_LEX

|- symmetric R1 ∧ symmetric R2 ⇒ symmetric (R1 LEX R2)