Package sum: Sum types

Information

name	sum
version	1.47
description	Sum types
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool natural pair
show	Data.Bool Data.Pair Data.Sum Number.Natural

Files

Package tarball sum-1.47.tgz
Theory file sum.thy (included in the package tarball)

Defined Type Operator

Data
- Sum
  - +

Defined Constants

Data
- Sum
  - destLeft
  - destRight
  - left
  - right

Theorems

⊦ ∀a. destLeft (left a) = a

⊦ ∀b. destRight (right b) = b

⊦ ∀p. (∀a. p (left a)) ∧ (∀b. p (right b)) ⇒ ∀x. p x

⊦ ∀f g. ∃fn. (∀a. fn (left a) = f a) ∧ ∀b. fn (right b) = g b

Input Type Operators

→
bool
Data
- Pair
  - ×
Number
- Natural
  - natural

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- Pair
  - ,
  - fst
  - snd
Number
- Natural
  - *
  - +
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - even
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ ∀n. 0 ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ ∀a. ∃!x. x = a

⊦ ∀t. (∀x. t) ⇔ t

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

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 + n = n

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀n. even (2 * n)

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀m. m ↑ 0 = 1

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

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

⊦ ∀n. even (suc n) ⇔ ¬even n

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

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

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

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

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

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

⊦ ∀n. 2 * n = n + n

⊦ ∀m n. ¬(m < n ∧ n ≤ m)

⊦ ∀m n. ¬(m ≤ n ∧ n < m)

⊦ ∀m n. suc m ≤ n ⇔ m < n

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. even (m * n) ⇔ even m ∨ even n

⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n

⊦ ∀m n. m ↑ suc n = m * m ↑ n

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

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

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

⊦ ∀m n p. m * (n * p) = m * n * p

⊦ ∀m n p. m + p = n + p ⇔ m = n

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

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

⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n

⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀m n. m ↑ n = 0 ⇔ m = 0 ∧ ¬(n = 0)

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀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 ⇒ q x) ⇒ (∃x. p x) ⇒ ∃x. q x

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

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

⊦ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p

⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p

⊦ ∀p₁ p₂ q₁ q₂. (p₁ ⇒ p₂) ∧ (q₁ ⇒ q₂) ⇒ p₁ ∧ q₁ ⇒ p₂ ∧ q₂

⊦ ∀p₁ p₂ q₁ q₂. (p₁ ⇒ p₂) ∧ (q₁ ⇒ q₂) ⇒ p₁ ∨ q₁ ⇒ p₂ ∨ q₂

⊦ ∀p. (∀x. ∃!y. p x y) ⇔ ∃f. ∀x y. p x y ⇔ f x = y

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀p. (∃!x. p x) ⇔ (∃x. p x) ∧ ∀x x'. p x ∧ p x' ⇒ x = x'