Package gfp-div-thm: Properties of GF(p) field division
Information
| name | gfp-div-thm |
| version | 1.18 |
| description | Properties of GF(p) field division |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-02-10 |
| requires | bool gfp-def gfp-thm gfp-div-def |
| show | Data.Bool Number.GF(p) Number.Natural |
Files
- Package tarball gfp-div-thm-1.18.tgz
- Theory file gfp-div-thm.thy (included in the package tarball)
Theorems
⊦ inv 1 = 1
⊦ ∀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 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 = 0) ∧ ¬(y = 0) ∧ inv x = inv y ⇒ x = y
⊦ ∀x y. ¬(x = 0) ∧ ¬(y = 0) ⇒ inv x * inv y = inv (x * y)
Input Type Operators
- →
- bool
- Number
- GF(p)
- gfp
- Natural
- natural
- GF(p)
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- ⊥
- ⊤
- Bool
- Number
- GF(p)
- *
- /
- fromNatural
- inv
- Natural
- bit1
- zero
- GF(p)
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ⊥ ⇔ ∀p. p
⊦ ∀t. t ∨ ¬t
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ¬(1 = 0)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀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
⊦ (∨) = λ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
⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0