Package gfp-div-def: Definition of GF(p) field division
Information
| name | gfp-div-def |
| version | 1.13 |
| description | Definition of GF(p) field division |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2011-11-28 |
| requires | bool natural natural-divides natural-gcd natural-prime gfp-witness gfp-def |
| show | Data.Bool Number.GF(p) Number.Natural |
Files
- Package tarball gfp-div-def-1.13.tgz
- Theory 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
Input Type Operators
- →
- bool
- Number
- GF(p)
- gfp
- Natural
- natural
- GF(p)
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- F
- T
- Bool
- Number
- GF(p)
- *
- +
- ~
- fromNatural
- oddprime
- toNatural
- Natural
- *
- +
- bit1
- distance
- divides
- gcd
- mod
- prime
- zero
- GF(p)
Assumptions
⊦ T
⊦ prime oddprime
⊦ ¬(oddprime = 0)
⊦ ¬F ⇔ T
⊦ F ⇔ ∀p. p
⊦ fromNatural oddprime = 0
⊦ 0 mod oddprime = 0
⊦ (¬) = λp. p ⇒ F
⊦ (∃) = λP. P ((select) P)
⊦ (∀) = λp. p = λx. T
⊦ ~0 = 0
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. T ∧ t ⇔ t
⊦ ∀t. T ⇒ t ⇔ t
⊦ ∀x. fromNatural (toNatural x) = x
⊦ ∀t. t ⇒ F ⇔ ¬t
⊦ ∀x. 0 + x = x
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀x. x * 0 = 0
⊦ ∀x. x + ~x = 0
⊦ ∀x. toNatural x mod oddprime = toNatural x
⊦ ∀x. 1 * x = x
⊦ ∀x. toNatural (fromNatural x) = x mod oddprime
⊦ ∀x y. x * y = y * x
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀x y. ~x * y = ~(x * y)
⊦ ∀x y. toNatural x = toNatural y ⇒ x = y
⊦ ∀x y. ~x + ~y = ~(x + y)
⊦ ∀x1 y1. fromNatural (x1 * y1) = fromNatural x1 * fromNatural y1
⊦ ∀x1 y1. fromNatural (x1 + y1) = fromNatural x1 + fromNatural y1
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀P Q. P ⇒ (∃x. Q x) ⇔ ∃x. P ⇒ Q x
⊦ ∀x y z. x * y * z = x * (y * z)
⊦ ∀x y z. y + x = z + x ⇔ y = z
⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃y. ∀x. P x (y x)
⊦ ∀a b. ∃s t. distance (s * a) (t * b) = gcd a b
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)
⊦ ∀p n. prime p ∧ ¬divides p n ⇒ gcd p n = 1
⊦ ∀m n p. distance m n = p ⇔ m + p = n ∨ n + p = m