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

Information

name	gfp-div-gcd-def
version	1.21
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-03-26
requires	bool pair relation
show	Data.Bool Data.Pair Number.GF(p) Number.Natural

Files

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

Defined Constant

Number
- GF(p)
  - divGcd

Theorem

⊦ ∀u v x₁ x₂.
    divGcd u v x₁ x₂ =
    if u = 1 then x₁
    else if v = 1 then x₂
    else if even u then divGcd (u div 2) v (x₁ / 2) x₂
    else if even v then divGcd u (v div 2) x₁ (x₂ / 2)
    else if v ≤ u then divGcd (u - v) v (x₁ - x₂) x₂
    else divGcd u (v - u) x₁ (x₂ - x₁)

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

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

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

⊦ ∀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) ⇔ ∀p₁ p₂. P (p₁, p₂)

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

⊦ ∀PAIR'. ∃fn. ∀a₀ a₁. fn (a₀, a₁) = PAIR' a₀ a₁

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