Package monoid-mult-add: Monoid multiplication by repeated addition
Information
| name | monoid-mult-add |
| version | 1.13 |
| description | Monoid multiplication by repeated addition |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| checksum | 1cd582d5736dfd40b50d044e147de2b71df9a5fa |
| requires | bool list monoid-mult-def monoid-mult-thm monoid-witness natural natural-bits |
| show | Algebra.Monoid Data.Bool Data.List Number.Natural |
Files
- Package tarball monoid-mult-add-1.13.tgz
- Theory source file monoid-mult-add.thy (included in the package tarball)
Defined Constant
- Algebra
- Monoid
- multAdd
- Monoid
Theorems
⊦ ∀z x. multAdd z x [] = z
⊦ ∀x n. multAdd 0 x (Bits.toList n) = x * n
⊦ ∀z x l. multAdd z x l = z + x * Bits.fromList l
⊦ ∀z x h t.
multAdd z x (h :: t) = multAdd (if h then z + x else z) (x + x) t
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
- zero
- Bits
- Bits.cons
- Bits.fromList
- Bits.toList
- Natural
Assumptions
⊦ ⊤
⊦ Bits.fromList [] = 0
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀x. x * 0 = 0
⊦ ∀x. 0 + x = x
⊦ ∀x. x + 0 = x
⊦ ∀n. Bits.fromList (Bits.toList n) = n
⊦ ∀x. x * 1 = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀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
⊦ ∀x. x * 2 = x + x
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀h t. Bits.fromList (h :: t) = Bits.cons h (Bits.fromList t)
⊦ (∨) = λ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)
⊦ ∀x m n. x * (m * n) = x * m * n
⊦ ∀x m n. x * (m + n) = x * m + x * 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)