Package gfp-div-gcd-def: Definition of a GF(p) division algorithm based on gcd

Information

name	gfp-div-gcd-def
version	1.12
description	Definition of a GF(p) division algorithm based on gcd
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-02-10
requires	bool pair relation
show	Data.Bool Data.Pair Number.GF(p) Number.Natural

Files

Package tarball gfp-div-gcd-def-1.12.tgz
Theory file gfp-div-gcd-def.thy (included in the package tarball)

Defined Constant

Number
- GF(p)
  - gcdDiv

Theorem

⊦ ∀u v x1 x2.
    gcdDiv u v x1 x2 =
    if u = 1 then x1
    else if v = 1 then x2
    else if even u then gcdDiv (u div 2) v (x1 / 2) x2
    else if even v then gcdDiv u (v div 2) x1 (x2 / 2)
    else if v ≤ u then gcdDiv (u - v) v (x1 - x2) x2
    else gcdDiv u (v - u) x1 (x2 - x1)

Input Type Operators

→
bool
Data
- Pair
  - ×
Number
- GF(p)
  - gfp
- Natural
  - natural

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- Pair
  - ,
Number
- GF(p)
  - -
  - /
  - fromNatural
- Natural
  - -
  - ≤
  - bit0
  - bit1
  - div
  - even
  - zero

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2

⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀P. (∀p. P p) ⇔ ∀p1 p2. P (p1, p2)

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀PAIR'. ∃fn. ∀a0 a1. fn (a0, a1) = PAIR' a0 a1

⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)

⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x