Theory: pair

Parents

• bool

Type constants

• prod(Arity = 2)

Term constants

• MK_PAIR:'a -> 'b -> 'a -> 'b -> bool {fixity = Prefix}
• IS_PAIR:('a -> 'b -> bool) -> bool {fixity = Prefix}
• REP_prod:'a # 'b -> 'a -> 'b -> bool {fixity = Prefix}
• ,:'a -> 'b -> 'a # 'b {fixity = Infix 50}
• FST:'a # 'b -> 'a {fixity = Prefix}
• SND:'a # 'b -> 'b {fixity = Prefix}
• UNCURRY:('a -> 'b -> 'c) -> 'a # 'b -> 'c {fixity = Prefix}
• CURRY:('a # 'b -> 'c) -> 'a -> 'b -> 'c {fixity = Prefix}

Axioms

Definitions

MK_PAIR_DEF

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

IS_PAIR_DEF

|- !p. IS_PAIR p = (?x y. p = MK_PAIR x y)

prod_TY_DEF

|- ?rep. TYPE_DEFINITION IS_PAIR rep

REP_prod

|- REP_prod =
   (@rep.
     (!p' p''. (rep p' = rep p'') ==> (p' = p'')) /\
     (!p. IS_PAIR p = (?p'. p = rep p')))

COMMA_DEF

|- !x y. (x,y) = (@p. REP_prod p = MK_PAIR x y)

FST_DEF

|- !p. FST p = (@x. ?y. MK_PAIR x y = REP_prod p)

SND_DEF

|- !p. SND p = (@y. ?x. MK_PAIR x y = REP_prod p)

UNCURRY_DEF

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

CURRY_DEF

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

Theorems

PAIR

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

FST

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

SND

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

PAIR_EQ

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