Package pair-thm: Properties of product types

Information

namepair-thm
version1.31
descriptionProperties of product types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory exported on 2018-08-28
checksum3a1a48fb8c9b98348986a95a38415f0e0b2c2985
requiresbool
function
pair-def
showData.Bool
Data.Pair

Files

Theorems

x. (fst x, snd x) = x

p. (x. p x) a b. p (a, b)

p. (x. p x) a b. p (a, b)

p. (a b. p (a, b)) x. p x

p. (f. p f) f. p (λa b. f (a, b))

p. (f. p f) f. p (λa b. f (a, b))

f. fn. a b. fn (a, b) = f a b

p. (x y. p x y) z. p (fst z) (snd z)

p. (x y. p x y) z. p (fst z) (snd z)

p. (f. p f) g h. p (λa. (g a, h a))

p. (f. p f) g h. p (λa. (g a, h a))

p. (f g. p f g) h. p (Function.∘ fst h) (Function.∘ snd h)

p. (f g. p f g) h. p (Function.∘ fst h) (Function.∘ snd h)

f. (λx. f x) = λ(a, b). f (a, b)

f. (λ(x, y). f x y) = λp. f (fst p) (snd p)

p. (f. p f) f. p (λ(a, b). f a b)

p. (f. p f) f. p (λ(a, b). f a b)

p. ((a, b). p a b) a b. p a b

p. ((a, b). p a b) a b. p a b

p. (select (a, b). p a b) = select x. p (fst x) (snd x)

f. (λt. f t) = λ(x, y, z). f (x, y, z)

f. (λ(x, y, z). f x y z) = λt. f (fst t) (fst (snd t)) (snd (snd t))

p. ((a, b, c). p a b c) a b c. p a b c

p. ((a, b, c). p a b c) a b c. p a b c

p q. (a b. p a b) (a b. p a b q (a, b)) q (select (a, b). p a b)

(f. (λ(a, b). f (a, b)) = f) (f. (λ(a, b, c). f (a, b, c)) = f)
  f. (λ(a, b, c, d). f (a, b, c, d)) = f

External Type Operators

External Constants

Assumptions

¬

¬

t. t t

p. p

t. t ¬t

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

Function.∘ = λf g x. f (g x)

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

a b. fst (a, b) = a

a b. snd (a, b) = b

p x. p x p ((select) p)

f y. (let x y in f x) = f y

x. a b. x = (a, b)

x y. x = y y = x

t1 t2. t1 t2 t2 t1

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

t1 t2 t3. (t1 t2) t3 t1 t2 t3

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x