Package gfp-div-exp-thm: Properties of a GF(p) exponentiation algorithm based on division
Information
| name | gfp-div-exp-thm |
| version | 1.2 |
| description | Properties of a GF(p) exponentiation algorithm based on division |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-03-08 |
| requires | bool list natural natural-fibonacci gfp-def gfp-thm gfp-div-def gfp-div-thm gfp-div-exp-def |
| show | Data.Bool Data.List Number.GF(p) Number.Natural Number.Natural.Fibonacci |
Files
- Package tarball gfp-div-exp-thm-1.2.tgz
- Theory file gfp-div-exp-thm.thy (included in the package tarball)
Theorems
⊦ ∀x n.
x ^ n =
if n = 0 then 1 else if x = 0 then 0 else expDiv ⊤ 1 1 x 1 (encode n)
⊦ ∀x n d f p l.
¬(x = 0) ∧ ¬(n = 0) ∧ ¬(d = 0) ⇒
expDiv ⊤ n d (x ^ f) (inv (x ^ p)) l =
(n / d) * x ^ decode.dest f p l ∧
expDiv ⊥ n d (inv (x ^ f)) (x ^ p) l = (d / n) * x ^ decode.dest f p l
Input Type Operators
- →
- bool
- Data
- List
- list
- List
- Number
- GF(p)
- gfp
- Natural
- natural
- GF(p)
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- []
- Bool
- Number
- GF(p)
- *
- /
- ^
- expDiv
- fromNatural
- inv
- Natural
- +
- bit1
- zero
- Fibonacci
- decode
- decode.dest
- encode
- decode
- GF(p)
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ ⊥ ⇔ ∀p. p
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ t ⇔ t
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀n. decode (encode n) = n
⊦ ¬(1 = 0)
⊦ ∀x. x ^ 1 = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ inv 1 = 1
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀x. x ^ 0 = 1
⊦ ∀x. x * 1 = x
⊦ ∀x. x / 1 = x
⊦ ∀x. 1 * x = x
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀f p. decode.dest f p [] = 0
⊦ ∀l. decode l = decode.dest 1 0 l
⊦ ∀x y. x = y ⇒ y = x
⊦ ∀x y. x * y = y * x
⊦ ∀m n. m + n = n + m
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀x. ¬(x = 0) ⇒ inv (inv x) = x
⊦ ∀x. ¬(x = 0) ⇒ ¬(inv x = 0)
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r
⊦ ∀x y z. x * y * z = x * (y * z)
⊦ ∀x. ¬(x = 0) ⇒ inv x * x = 1
⊦ ∀x y. ¬(x = 0) ⇒ x * (y / x) = y
⊦ ∀x y. ¬(x = 0) ⇒ (y / x) * x = y
⊦ ∀x y. ¬(x = 0) ⇒ y * x / x = y
⊦ ∀x y. ¬(x = 0) ⇒ y / x = y * inv x
⊦ ∀x m n. x ^ m * x ^ n = x ^ (m + n)
⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
⊦ ∀x n. x ^ n = 0 ⇔ x = 0 ∧ ¬(n = 0)
⊦ ∀P. P [] ∧ (∀a0 a1. P a1 ⇒ P (a0 :: a1)) ⇒ ∀x. P x
⊦ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z
⊦ ∀x y z. y * x = z * x ⇔ x = 0 ∨ y = z
⊦ ∀x y z. ¬(x = 0) ∧ x * y = x * z ⇒ y = z
⊦ ∀x y z. ¬(x = 0) ∧ y * x = z * x ⇒ y = z
⊦ ∀x y. ¬(x = 0) ∧ ¬(y = 0) ⇒ ¬(y / x = 0)
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)
⊦ ∀b n d f p. expDiv b n d f p [] = if b then n / d else d / n
⊦ ∀f p h t.
decode.dest f p (h :: t) =
let s ← f + p in let n ← decode.dest s f t in if h then s + n else n
⊦ ∀b n d f p h t.
expDiv b n d f p (h :: t) =
let s ← p / f in expDiv (¬b) d (if h then n / s else n) s f t