Package monoid: Parametric theory of monoids
Information
| name | monoid |
| version | 1.6 |
| description | Parametric theory of monoids |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| requires | bool list monoid-witness natural natural-bits |
| show | Algebra.Monoid Data.Bool Data.List Number.Natural |
Files
- Package tarball monoid-1.6.tgz
- Theory source file monoid.thy (included in the package tarball)
Defined Constants
- Algebra
- Monoid
- *
- multAdd
- Monoid
Theorems
⊦ ∀x. x * 0 = 0
⊦ ∀n. 0 * n = 0
⊦ ∀x. x * 1 = x
⊦ ∀x. 0 + x = x + 0
⊦ ∀x. x + 0 = 0 + x
⊦ ∀z x. multAdd z x [] = z
⊦ ∀x. x * 2 = x + x
⊦ ∀x n. multAdd 0 x (Bits.fromNatural n) = x * n
⊦ ∀x n. x * suc n = x + x * n
⊦ ∀x n. x * suc n = x * n + x
⊦ ∀z x l. multAdd z x l = z + x * Bits.toNatural l
⊦ ∀x m n. x * (m * n) = x * m * n
⊦ ∀x m n. x * (m + n) = x * m + x * n
⊦ ∀x n y. x + y = y + x ⇒ x * n + y = y + x * n
⊦ ∀x n y. y + x = x + y ⇒ y + x * n = x * n + y
⊦ ∀z x h t.
multAdd z x (h :: t) = multAdd (if h then z + x else z) (x + x) t
⊦ ∀x y z. x + z = z + x ∧ y + z = z + y ⇒ x + y + z = z + (x + y)
⊦ ∀x y z. z + x = x + z ∧ z + y = y + z ⇒ z + (x + y) = x + y + z
External Type Operators
- →
- bool
- Algebra
- Monoid
- monoid
- Monoid
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Algebra
- Monoid
- +
- 0
- Monoid
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∃!
- ∨
- cond
- ⊥
- ⊤
- List
- ::
- []
- Bool
- Number
- Natural
- *
- +
- bit0
- bit1
- fromBool
- suc
- zero
- Bits
- Bits.cons
- Bits.fromNatural
- Bits.toNatural
- Natural
Assumptions
⊦ ⊤
⊦ bit0 0 = 0
⊦ Bits.toNatural [] = 0
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀x. 0 + x = x
⊦ ∀x. x + 0 = x
⊦ ∀n. Bits.toNatural (Bits.fromNatural n) = n
⊦ ∀m. m * 0 = 0
⊦ ∀n. 0 + n = n
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀m. suc m = m + 1
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀b. fromBool b = if b then 1 else 0
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x y. x = y ⇒ y = x
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural t)
⊦ ∀m n. suc m + n = suc (m + n)
⊦ ∀m n. m * suc n = m + m * n
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t
⊦ ∀x y z. x + y + z = x + (y + z)
⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y
⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n
⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l
⊦ ∀b f. ∃fn. fn [] = b ∧ ∀h t. fn (h :: t) = f h t (fn t)