Package gfp-div-def: Definition of GF(p) field division
Information
| name | gfp-div-def |
| version | 1.67 |
| description | Definition of GF(p) field division |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-04 |
| checksum | 7be958bee2cbe977060d7807c82233df11e014f8 |
| requires | base gfp-def gfp-witness natural-divides natural-prime |
| show | Data.Bool Number.GF(p) Number.Natural |
Files
- Package tarball gfp-div-def-1.67.tgz
- Theory source file gfp-div-def.thy (included in the package tarball)
Defined Constants
- Number
- GF(p)
- /
- inv
- GF(p)
Theorems
⊦ ∀x. ¬(x = 0) ⇒ inv x * x = 1
⊦ ∀x y. ¬(x = 0) ⇒ x * y / x = y
External Type Operators
- →
- bool
- Number
- GF(p)
- gfp
- Natural
- natural
- GF(p)
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- ⊥
- ⊤
- Bool
- Number
- GF(p)
- *
- +
- fromNatural
- oddprime
- toNatural
- Natural
- *
- +
- bit1
- divides
- gcd
- mod
- prime
- zero
- GF(p)
Assumptions
⊦ ⊤
⊦ prime oddprime
⊦ ¬(oddprime = 0)
⊦ ¬⊥ ⇔ ⊤
⊦ ⊥ ⇔ ∀p. p
⊦ fromNatural oddprime = 0
⊦ 0 mod oddprime = 0
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∃) = λp. p ((select) p)
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀x. fromNatural (toNatural x) = x
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀x. 0 + x = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀x. x * 0 = 0
⊦ ∀x. toNatural x mod oddprime = toNatural x
⊦ ∀x. 1 * x = x
⊦ ∀n. toNatural (fromNatural n) = n mod oddprime
⊦ ∀x y. x * y = y * x
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀x y. toNatural x = toNatural y ⇒ x = y
⊦ ∀x1 y1. fromNatural (x1 * y1) = fromNatural x1 * fromNatural y1
⊦ ∀x1 y1. fromNatural (x1 + y1) = fromNatural x1 + fromNatural y1
⊦ ∀p q. p ⇒ (∃x. q x) ⇔ ∃x. p ⇒ q x
⊦ ∀x y z. x * y * z = x * (y * z)
⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)
⊦ ∀p n. prime p ∧ ¬divides p n ⇒ gcd p n = 1
⊦ ∀a b. ¬(a = 0) ⇒ ∃s t. t * b + gcd b a = s * a