Package pair-thm: Properties of product types

Information

namepair-thm
version1.15
descriptionProperties of product types
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-12-18
requiresbool
pair-def
showData.Bool
Data.Pair

Files

Theorems

x. (fst x, snd x) = x

P. (p. P p) p1 p2. P (p1, p2)

P. (p. P p) p1 p2. P (p1, p2)

P. (x y. P (x, y)) p. P p

PAIR'. fn. a0 a1. fn (a0, a1) = PAIR' a0 a1

t. (λp. t p) = λ(x, y). t (x, y)

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

t. t t

F p. p

t. t ¬t

(¬) = λp. p F

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx. T

t. ¬¬t t

t. (T t) t

t. F t F

t. T t t

t. F t T

t. T t t

t. t T T

t. F t t

t. T t T

t. t F t

t. t T T

t. (F t) ¬t

t. t F ¬t

() = λp q. p q p

t. (t T) (t F)

x y. fst (x, y) = x

x y. snd (x, y) = y

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

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

p. x y. p = (x, y)

x y. x = y y = x

t1 t2. t1 t2 t2 t1

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

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