The Theory pair
Parents
misc
Children

Constants
IsPairRep
('a → 'b → BOOL) → BOOL
$,
'a → 'b → 'a × 'b
Fst
'a × 'b → 'a
Snd
'a × 'b → 'b
Uncurry
('a → 'b → 'c) → 'a × 'b → 'c
Curry
('a × 'b → 'c) → 'a → 'b → 'c
Pair
('a → 'b) × ('a → 'c) → 'a → 'b × 'c
Types
'1 × '2
Fixity
Right Infix 150:
, ×
Terminators
×
Definitions
IsPairRep
is_pair_rep_def
⊢ ∃ comma fst snd
fill• (∀ x y
fill• IsPairRep (comma x y)
fill∧ fst (comma x y) = x
fill∧ snd (comma x y) = y)
fill∧ (∀ x y a b
fill• comma a b = comma x y ⇔ a = x ∧ b = y)
fill∧ (∀ p• IsPairRep p ⇒ comma (fst p) (snd p) = p)
×
×_def
⊢ ∃ f• TypeDefn IsPairRep f
comma_def
⊢ ∃ fst snd
fill• (∀ x y• fst (x, y) = x ∧ snd (x, y) = y)
fill∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y)
fill∧ (∀ p• (fst p, snd p) = p)
fst_def
⊢ ∃ snd
fill• (∀ x y• Fst (x, y) = x ∧ snd (x, y) = y)
fill∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y)
fill∧ (∀ p• (Fst p, snd p) = p)
,
Fst
Snd
pair_ops_def
snd_def
⊢ (∀ x y• Fst (x, y) = x ∧ Snd (x, y) = y)
fill∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y)
fill∧ (∀ p• (Fst p, Snd p) = p)
Uncurry
uncurry_def
⊢ ∀ f x y• Uncurry f (x, y) = f x y
Curry
curry_def
⊢ ∀ f x y• Curry f x y = f (x, y)
Pair
pair_def
⊢ ∀ f g• Pair (f, g) = (λ x• (f x, g x))
Theorems
pair_clauses
⊢ ∀ x y a b p fu fc fg
fill• Fst (x, y) = x
fill∧ Snd (x, y) = y
fill∧ ((a, b) = (x, y) ⇔ a = x ∧ b = y)
fill∧ (Fst p, Snd p) = p
fill∧ Curry fc x y = fc (x, y)
fill∧ Uncurry fu (x, y) = fu x y
fill∧ Uncurry fu p = fu (Fst p) (Snd p)
fill∧ ((a, b) = p ⇔ a = Fst p ∧ b = Snd p)
fill∧ (p = (a, b) ⇔ Fst p = a ∧ Snd p = b)
fill∧ Pair fg x = (Fst fg x, Snd fg x)

up quick index

privacy policy

Created:

V