Package gfp-div-exp-thm: Correctness of a GF(p) exponentiation algorithm based on division

Information

name	gfp-div-exp-thm
version	1.38
description	Correctness of a GF(p) exponentiation algorithm based on division
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-12-02
requires	bool gfp-def gfp-div-def gfp-div-exp-def gfp-div-thm gfp-thm list natural natural-fibonacci
show	Data.Bool Data.List Number.GF(p) Number.Natural Number.Natural.Fibonacci

Files

Package tarball gfp-div-exp-thm-1.38.tgz
Theory source 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

External Type Operators

→
bool
Data
- List
  - list
Number
- GF(p)
  - gfp
- Natural
  - natural

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
Number
- GF(p)
  - *
  - /
  - ↑
  - expDiv
  - fromNatural
  - inv
- Natural
  - +
  - bit1
  - zero
  - Fibonacci
    - decode
      - decode.dest
    - encode

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

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀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 [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l

⊦ ∀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