The Theory pair

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 • (∀ x y • IsPairRep (comma x y) ∧ fst (comma x y) = x ∧ snd (comma x y) = y) ∧ (∀ x y a b • comma a b = comma x y ⇔ a = x ∧ b = y) ∧ (∀ p• IsPairRep p ⇒ comma (fst p) (snd p) = p)
× ×_def	⊢ ∃ f• TypeDefn IsPairRep f
comma_def	⊢ ∃ fst snd • (∀ x y• fst (x, y) = x ∧ snd (x, y) = y) ∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y) ∧ (∀ p• (fst p, snd p) = p)
fst_def	⊢ ∃ snd • (∀ x y• Fst (x, y) = x ∧ snd (x, y) = y) ∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y) ∧ (∀ p• (Fst p, snd p) = p)
, Fst Snd pair_ops_def snd_def	⊢ (∀ x y• Fst (x, y) = x ∧ Snd (x, y) = y) ∧ (∀ x y a b• (a, b) = (x, y) ⇔ a = x ∧ b = y) ∧ (∀ 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

• Fst (x, y) = x

∧ Snd (x, y) = y

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

∧ (Fst p, Snd p) = p

∧ Curry fc x y = fc (x, y)

∧ Uncurry fu (x, y) = fu x y

∧ Uncurry fu p = fu (Fst p) (Snd p)

∧ ((a, b) = p ⇔ a = Fst p ∧ b = Snd p)

∧ (p = (a, b) ⇔ Fst p = a ∧ Snd p = b)

∧ Pair fg x = (Fst fg x, Snd fg x)

privacy policy

Created:

V