Package group-mult-add: Group multiplication by repeated addition
Information
| name | group-mult-add |
| version | 1.8 |
| description | Group multiplication by repeated addition |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| requires | bool 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-1.8.tgz
- Theory source file group-mult-add.thy (included in the package tarball)
Defined Constant
- Algebra
- Group
- multAdd
- Group
Theorems
⊦ ∀z x. multAdd z x [] = z
⊦ ∀x n. x * n = multAdd 0 x (Bits.fromNatural n)
⊦ ∀z x l. multAdd z x l = z + x * Bits.toNatural 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
- Group
- group
- Group
- Data
- List
- list
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Algebra
- Group
- *
- +
- ~
- 0
- Group
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- cond
- ⊥
- ⊤
- List
- ::
- []
- Bool
- Number
- Natural
- *
- +
- bit0
- bit1
- zero
- Bits
- Bits.fromNatural
- Bits.toNatural
- Natural
Assumptions
⊦ ⊤
⊦ Bits.toNatural [] = 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.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
⊦ ∀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
⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)
⊦ ∀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
⊦ ∀b f. ∃fn. fn [] = b ∧ ∀h t. fn (h :: t) = f h t (fn t)