Package gfp-thm: Properties of GF(p) finite fields
Information
| name | gfp-thm |
| version | 1.18 |
| description | Properties of GF(p) finite fields |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-03-08 |
| requires | bool natural natural-divides natural-prime gfp-witness gfp-def |
| show | Data.Bool Number.GF(p) Number.Natural |
Files
- Package tarball gfp-thm-1.18.tgz
- Theory file gfp-thm.thy (included in the package tarball)
Theorems
⊦ 1 < oddprime
⊦ ¬(oddprime = 1)
⊦ ¬divides oddprime 1
⊦ 2 < oddprime
⊦ ¬(oddprime = 2)
⊦ ¬divides oddprime 2
⊦ ¬divides 2 oddprime
⊦ ¬(1 = 0)
⊦ 1 mod oddprime = 1
⊦ ¬(2 = 0)
⊦ 2 mod oddprime = 2
⊦ ∀m n. divides oddprime (m * n) ⇔ divides oddprime m ∨ divides oddprime n
⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
⊦ ∀x n. x ^ n = 0 ⇔ x = 0 ∧ ¬(n = 0)
Input Type Operators
- →
- bool
- Number
- GF(p)
- gfp
- Natural
- natural
- GF(p)
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- ⊥
- ⊤
- Bool
- Number
- GF(p)
- *
- ^
- fromNatural
- oddprime
- toNatural
- Natural
- *
- <
- ≤
- bit0
- bit1
- divides
- even
- mod
- odd
- prime
- suc
- zero
- GF(p)
Assumptions
⊦ ⊤
⊦ odd oddprime
⊦ prime oddprime
⊦ ¬prime 1
⊦ ¬(oddprime = 0)
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ odd 0 ⇔ ⊥
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ⊥ ⇔ ∀p. p
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. t ∧ ⊥ ⇔ ⊥
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. t ∨ t ⇔ t
⊦ ∀x. fromNatural (toNatural x) = x
⊦ ∀n. ¬(suc n = 0)
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀n. ¬even n ⇔ odd n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀x. x ^ 0 = 1
⊦ ∀x. x * 0 = 0
⊦ ∀x. 0 * x = 0
⊦ ∀x. x * 1 = x
⊦ ∀n. odd (suc n) ⇔ ¬odd n
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀a. divides 2 a ⇔ even a
⊦ ∀n. n < oddprime ⇒ n mod oddprime = n
⊦ ∀a. divides a 1 ⇔ a = 1
⊦ ∀x. fromNatural x = 0 ⇔ divides oddprime x
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀x n. x ^ suc n = x * x ^ n
⊦ ∀x1 y1. fromNatural (x1 * y1) = fromNatural x1 * fromNatural y1
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)
⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n
⊦ ∀a. divides a 2 ⇔ a = 1 ∨ a = 2
⊦ ∀p m n. prime p ⇒ (divides p (m * n) ⇔ divides p m ∨ divides p n)