Package pair: Product types

Information

Files

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

Defined Type Operator

• Data
  • Pair
    • ×

Defined Constants

• Data
  • Pair
    • ,
    • fst
    • snd

Theorems

⊦ ∀x. (fst x, snd x) = x

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

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

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

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

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

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

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • ⊥
    • ⊤
• Function
  • Function.∘

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) 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 ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

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

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

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

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀f y. (let x ← y in f x) = f y

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

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

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

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

OpenTheory package document generated by opentheory 1.4 (release 20180810)