Package gfp-div-thm: Properties of GF(p) field division

Information

name	gfp-div-thm
version	1.28
description	Properties of GF(p) field division
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-03-26
requires	bool gfp-def gfp-div-def gfp-thm natural
show	Data.Bool Number.GF(p) Number.Natural

Files

Package tarball gfp-div-thm-1.28.tgz
Theory file gfp-div-thm.thy (included in the package tarball)

Theorems

⊦ inv 1 = 1

⊦ ∀x. x / 1 = x

⊦ ∀x. ¬(x = 0) ⇒ inv (inv x) = x

⊦ ∀x. ¬(x = 0) ⇒ ¬(inv x = 0)

⊦ ∀x. ¬(x = 0) ⇒ x * inv 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 n. ¬(x = 0) ⇒ inv x ↑ n = inv (x ↑ n)

⊦ ∀x y. x * y = x ⇔ x = 0 ∨ y = 1

⊦ ∀x y. y * x = x ⇔ x = 0 ∨ y = 1

⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0

⊦ ∀x. ¬(x = 0) ∧ inv x = 1 ⇒ x = 1

⊦ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z

⊦ ∀x y z. y * x = z * x ⇔ x = 0 ∨ y = z

⊦ ∀x y. x * y = if y = 0 then 0 else x / (1 / y)

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

⊦ ∀x y. ¬(x = 0) ∧ ¬(y = 0) ⇒ inv (y / x) = x / y

⊦ ∀x y. ¬(x = 0) ∧ ¬(y = 0) ∧ inv x = inv y ⇒ x = y

⊦ ∀x y. ¬(x = 0) ∧ ¬(y = 0) ⇒ inv x * inv y = inv (x * y)

⊦ ∀x y z. ¬(y = 0) ∧ ¬(z = 0) ⇒ x / (y / z) = x * z / y

Input Type Operators

→
bool
Number
- GF(p)
  - gfp
- Natural
  - natural

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
Number
- GF(p)
  - *
  - /
  - ↑
  - fromNatural
  - inv
- Natural
  - bit1
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ¬(1 = 0)

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

⊦ ∀x. x ↑ 0 = 1

⊦ ∀x. x * 0 = 0

⊦ ∀x. 0 * x = 0

⊦ ∀x. x * 1 = x

⊦ ∀x. 1 * x = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀x y. x * y = y * x

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

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

⊦ ∀x n. x ↑ suc n = x * x ↑ n

⊦ (∨) = λ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. ¬(x = 0) ⇒ inv x * x = 1

⊦ ∀x y. ¬(x = 0) ⇒ x * y / x = y

⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n

⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0

⊦ ∀x n. x ↑ n = 0 ⇔ x = 0 ∧ ¬(n = 0)

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)