Package pair-def: Definition of product types

Information

name	pair-def
version	1.19
description	Definition of product types
author	Joe Leslie-Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2012-12-10
requires	bool
show	Data.Bool Data.Pair

Files

Package tarball pair-def-1.19.tgz
Theory source file pair-def.thy (included in the package tarball)

Defined Type Operator

Data
- Pair
  - ×

Defined Constants

Data
- Pair
  - ,
  - fst
  - snd

Theorems

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

External Type Operators

→
bool

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - ⊥
  - ⊤

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀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

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ (∧) = λ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. (∃x. p x) ∧ q ⇔ ∃x. p x ∧ q

⊦ ∀p q. (∀x. p x) ∨ q ⇔ ∀x. p x ∨ q

⊦ ∀p q. (∃x. p x) ∨ q ⇔ ∃x. p x ∨ q

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

⊦ ∀p x. (∀y. p y ⇔ y = x) ⇒ (select) p = x

⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)

⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x