Theory "pair"

Parents relation

Signature

Type	Arity
prod	2
Constant	Type
##	:(α -> γ) -> (β -> δ) -> α # β -> γ # δ
,	:α -> β -> α # β
ABS_prod	:(α -> β -> bool) -> α # β
CURRY	:(α # β -> γ) -> α -> β -> γ
FST	:α # β -> α
LEX	:(α -> α -> bool) -> (β -> β -> bool) -> α # β -> α # β -> bool
PROD_ALL	:(α -> bool) -> (β -> bool) -> α # β -> bool
REP_prod	:α # β -> α -> β -> bool
RPROD	:(α -> α -> bool) -> (β -> β -> bool) -> α # β -> α # β -> bool
SND	:α # β -> β
SWAP	:β # α -> α # β
UNCURRY	:(α -> β -> γ) -> α # β -> γ
pair_CASE	:β # γ -> (β -> γ -> α) -> α

Definitions

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

CURRY_DEF

⊢ ∀f x y. CURRY f x y = f (x,y)

LEX_DEF

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

PAIR

⊢ ∀x. (FST x,SND x) = x

PAIR_MAP

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

PROD_ALL_def

⊢ ∀P Q p. PROD_ALL P Q p ⇔ P (FST p) ∧ Q (SND p)

RPROD_DEF

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

SWAP_def

⊢ ∀a. SWAP a = (SND a,FST a)

UNCURRY

⊢ ∀f v. fᴾ v = f (FST v) (SND v)

pair_CASE_def

⊢ ∀p f. pair_CASE p f = f (FST p) (SND p)

prod_TY_DEF

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

Theorems

ABS_PAIR_THM

⊢ ∀x. ∃q r. x = (q,r)

CLOSED_PAIR_EQ

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

CURRY_ONE_ONE_THM

⊢ (CURRY f = CURRY g) ⇔ (f = g)

CURRY_UNCURRY_THM

⊢ ∀f. CURRY fᴾ = f

C_UNCURRY_L

⊢ flip fᴾ x = (flip (flip ∘ f) x)ᴾ

ELIM_PEXISTS

⊢ (∃p. P (FST p) (SND p)) ⇔ ∃p1 p2. P p1 p2

ELIM_PEXISTS_EVAL

⊢ $? (λx. P x)ᴾ ⇔ ∃x. $? (P x)

ELIM_PFORALL

⊢ (∀p. P (FST p) (SND p)) ⇔ ∀p1 p2. P p1 p2

ELIM_PFORALL_EVAL

⊢ $! (λx. P x)ᴾ ⇔ ∀x. $! (P x)

ELIM_UNCURRY

⊢ ∀f. fᴾ = (λx. f (FST x) (SND x))

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)

FORALL_UNCURRY

⊢ $! fᴾ ⇔ $! ($! ∘ f)

FST

⊢ ∀x y. FST (x,y) = x

FST_EQ_EQUIV

⊢ (FST p = x) ⇔ ∃y. p = (x,y)

FST_PAIR_MAP

⊢ ∀p f g. FST ((f ## g) p) = f (FST p)

LAMBDA_PROD

⊢ ∀P. (λp. P p) = (λ(p1,p2). P (p1,p2))

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)

LEX_CONG

⊢ ∀R1 R2 v1 v2 R1' R2' v1' v2'.
    (v1 = v1') ∧ (v2 = v2') ∧
    (∀a b c d. (v1' = (a,b)) ∧ (v2' = (c,d)) ⇒ (R1 a c ⇔ R1' a c)) ∧
    (∀a b c d. (v1' = (a,b)) ∧ (v2' = (c,d)) ∧ (a = c) ⇒ (R2 b d ⇔ R2' b d)) ⇒
    ((R1 LEX R2) v1 v2 ⇔ (R1' LEX R2') v1' v2')

LEX_DEF_THM

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

LEX_MONO

⊢ (∀x y. R1 x y ⇒ R2 x y) ∧ (∀x y. R3 x y ⇒ R4 x y) ⇒
  (R1 LEX R3) x y ⇒
  (R2 LEX R4) x y

PAIR_EQ

⊢ ((x,y) = (a,b)) ⇔ (x = a) ∧ (y = b)

PAIR_FST_SND_EQ

⊢ ∀p q. (p = q) ⇔ (FST p = FST q) ∧ (SND p = SND q)

PAIR_FUN_THM

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

PAIR_MAP_THM

⊢ ∀f g x y. (f ## g) (x,y) = (f x,g y)

PEXISTS_THM

⊢ ∀P. (∃x y. P x y) ⇔ ∃(x,y). P x y

PFORALL_THM

⊢ ∀P. (∀x y. P x y) ⇔ ∀(x,y). P x y

PROD_ALL_CONG

⊢ ∀p p' P P' Q Q'.
    (p = p') ∧ (∀x y. (p' = (x,y)) ⇒ (P x ⇔ P' x)) ∧
    (∀x y. (p' = (x,y)) ⇒ (Q y ⇔ Q' y)) ⇒
    (PROD_ALL P Q p ⇔ PROD_ALL P' Q' p')

PROD_ALL_MONO

⊢ (∀x. P x ⇒ P' x) ∧ (∀y. Q y ⇒ Q' y) ⇒ PROD_ALL P Q p ⇒ PROD_ALL P' Q' p

PROD_ALL_THM

⊢ PROD_ALL P Q (x,y) ⇔ P x ∧ Q y

SND

⊢ ∀x y. SND (x,y) = y

SND_EQ_EQUIV

⊢ (SND p = y) ⇔ ∃x. p = (x,y)

SND_PAIR_MAP

⊢ ∀p f g. SND ((f ## g) p) = g (SND p)

S_UNCURRY_R

⊢ S f gᴾ = (S (S ∘ $o f ∘ $,) g)ᴾ

UNCURRY_CONG

⊢ ∀f' f M' M.
    (M = M') ∧ (∀x y. (M' = (x,y)) ⇒ (f x y = f' x y)) ⇒ (fᴾ M = f'ᴾ M')

UNCURRY_CURRY_THM

⊢ ∀f. (CURRY f)ᴾ = f

UNCURRY_DEF

⊢ ∀f x y. fᴾ (x,y) = f x y

UNCURRY_ONE_ONE_THM

⊢ (fᴾ = gᴾ) ⇔ (f = g)

UNCURRY_VAR

⊢ ∀f v. fᴾ v = f (FST v) (SND v)

WF_LEX

⊢ ∀R Q. WF R ∧ WF Q ⇒ WF (R LEX Q)

WF_RPROD

⊢ ∀R Q. WF R ∧ WF Q ⇒ WF (RPROD R Q)

datatype_pair

⊢ DATATYPE (pair $,)

o_UNCURRY_R

⊢ f ∘ gᴾ = ($o f ∘ g)ᴾ

pair_Axiom

⊢ ∀f. ∃fn. ∀x y. fn (x,y) = f x y

pair_CASES

⊢ ∀x. ∃q r. x = (q,r)

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

pair_case_def

⊢ pair_CASE (x,y) f = f x y

pair_case_eq

⊢ (pair_CASE p f = v) ⇔ ∃x y. (p = (x,y)) ∧ (f x y = v)

pair_case_thm

⊢ pair_CASE (x,y) f = f x y

pair_induction

⊢ ∀P. (∀p_1 p_2. P (p_1,p_2)) ⇒ ∀p. P p

reflexive_LEX

⊢ reflexive (R1 LEX R2) ⇔ reflexive R1 ∨ reflexive R2

symmetric_LEX

⊢ symmetric R1 ∧ symmetric R2 ⇒ symmetric (R1 LEX R2)

total_LEX

⊢ total R1 ∧ total R2 ⇒ total (R1 LEX R2)

transitive_LEX

⊢ transitive R1 ∧ transitive R2 ⇒ transitive (R1 LEX R2)