Theory: pair

Parents

• relation

Types

• prod(Arity = 2)

Constants

• ,  :'a -> 'b -> 'a # 'b
• ##  :('a -> 'c) -> ('b -> 'd) -> 'a # 'b -> 'c # 'd
• CURRY  :('a # 'b -> 'c) -> 'a -> 'b -> 'c
• UNCURRY  :('a -> 'b -> 'c) -> 'a # 'b -> 'c
• REP_prod  :'a # 'b -> 'a -> 'b -> bool
• ABS_prod  :('a -> 'b -> bool) -> 'a # 'b
• IS_PAIR  :('a -> 'b -> bool) -> bool
• MK_PAIR  :'a -> 'b -> 'a -> 'b -> bool
• FST  :'a # 'b -> 'a
• LEX  :('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a # 'b -> 'a # 'b -> bool
• pair_case  :('a -> 'b -> 'c) -> 'a # 'b -> 'c
• SND  :'a # 'b -> 'b
• RPROD  :('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a # 'b -> 'a # 'b -> bool

Definitions

ABS_REP_prod

|- (!a. ABS_prod (REP_prod a) = a) /\
   !r. IS_PAIR r = (REP_prod (ABS_prod r) = r)

COMMA_DEF

|- !x y. (x,y) = ABS_prod (MK_PAIR x y)

CURRY_DEF

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

IS_PAIR_DEF

|- !P. IS_PAIR P = ?x y. P = MK_PAIR x y

LEX_DEF

|- !R1 R2. R1 LEX R2 = (\(s,t) (u,v). R1 s u \/ (s = u) /\ R2 t v)

MK_PAIR_DEF

|- !x y. MK_PAIR x y = (\a b. (a = x) /\ (b = y))

PAIR

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

pair_case_def

|- pair_case = UNCURRY

PAIRMAP

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

prod_TY_DEF

|- ?rep. TYPE_DEFINITION IS_PAIR rep

RPROD_DEF

|- !R1 R2. RPROD R1 R2 = (\(s,t) (u,v). R1 s u /\ R2 t v)

UNCURRY

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

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 (UNCURRY f) = f

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)

FST

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

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)

pair_Axiom

|- !f. ?fn. !x y. fn (x,y) = f x y

pair_case_cong

|- !f' f M' M.
     (M = M') /\ (!x y. (M' = (x,y)) ==> (f x y = f' x y)) ==>
     (pair_case f M = pair_case f' M')

pair_case_thm

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

PAIR_EQ

|- ((x,y) = (a,b)) = (x = a) /\ (y = b)

pair_induction

|- (!p_1 p_2. P (p_1,p_2)) ==> !p. P p

PAIRMAP_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

SND

|- !x y. SND (x,y) = 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')

UNCURRY_CURRY_THM

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

UNCURRY_DEF

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

UNCURRY_ONE_ONE_THM

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

UNCURRY_VAR

|- !f v. UNCURRY 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)