Package monoid-mult-add-thm: Correctness of monoid multiplication by repeated addition
Information
| name | monoid-mult-add-thm |
| version | 1.6 |
| description | Correctness of monoid multiplication by repeated addition |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-06-12 |
| requires | bool list monoid-mult-add-def 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-thm-1.6.tgz
- Theory source file monoid-mult-add-thm.thy (included in the package tarball)
Theorems
⊦ ∀x n. multAdd 0 x (Bits.fromNatural n) = x * n
⊦ ∀z x l. multAdd z x l = z + x * Bits.toNatural l
External Type Operators
- →
- bool
- Algebra
- Monoid
- monoid
- Monoid
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- Algebra
- Monoid
- *
- +
- 0
- multAdd
- Monoid
- Data
- Bool
- ∀
- ∧
- ⇒
- ∨
- cond
- ⊥
- ⊤
- List
- ::
- []
- Bool
- Number
- Natural
- *
- +
- bit0
- bit1
- fromBool
- zero
- Bits
- Bits.cons
- Bits.fromNatural
- Bits.toNatural
- Natural
Assumptions
⊦ ⊤
⊦ Bits.toNatural [] = 0
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀x. x * 0 = 0
⊦ ∀x. 0 + x = x
⊦ ∀x. x + 0 = x
⊦ ∀n. Bits.toNatural (Bits.fromNatural 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
⊦ ∀z x. multAdd z x [] = z
⊦ ∀b. fromBool b = if b then 1 else 0
⊦ ∀x. x * 2 = x + x
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural 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
⊦ ∀z x h t.
multAdd z x (h :: t) = multAdd (if h then z + x else z) (x + x) t