Package pair-thm: Properties of product types
Information
| name | pair-thm |
| version | 1.31 |
| description | Properties of product types |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory exported on 2018-08-28 |
| checksum | 3a1a48fb8c9b98348986a95a38415f0e0b2c2985 |
| requires | bool function pair-def |
| show | Data.Bool Data.Pair |
Files
- Package tarball pair-thm-1.31.tgz
- Theory source file pair-thm.thy (included in the package tarball)
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
- →
- bool
- Data
- Pair
- ×
- Pair
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- ⊥
- ⊤
- Pair
- ,
- fst
- snd
- Bool
- Function
- Function.∘
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