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