Package gfp-def: Definition of GF(p) finite fields

Information

name	gfp-def
version	1.22
description	Definition of GF(p) finite fields
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-11-15
requires	bool gfp-witness natural natural-divides natural-prime
show	Data.Bool Number.GF(p) Number.Natural

Files

Package tarball gfp-def-1.22.tgz
Theory file gfp-def.thy (included in the package tarball)

Defined Type Operator

Number
- GF(p)
  - gfp

Defined Constants

Number
- GF(p)
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - ~
  - fromNatural
  - toNatural

Theorems

⊦ ¬(oddprime = 0)

⊦ fromNatural oddprime = 0

⊦ oddprime mod oddprime = 0

⊦ 0 mod oddprime = 0

⊦ ∀x. toNatural x < oddprime

⊦ ~0 = 0

⊦ ∀x. ~~x = x

⊦ ∀x. fromNatural (toNatural x) = x

⊦ ∀n. n mod oddprime < oddprime

⊦ ∀x. x + 0 = x

⊦ ∀x. x ↑ 1 = x

⊦ ∀x. 0 + x = x

⊦ ∀x. toNatural x div oddprime = 0

⊦ ∀x. x ↑ 0 = 1

⊦ ∀x. x * 0 = 0

⊦ ∀x. x + ~x = 0

⊦ ∀x. 0 * x = 0

⊦ ∀x. ~x + x = 0

⊦ ∀x. toNatural x mod oddprime = toNatural x

⊦ ∀x. x * 1 = x

⊦ ∀x. 1 * x = x

⊦ ∀x. toNatural (fromNatural x) = x mod oddprime

⊦ ∀x. ~x = fromNatural (oddprime - toNatural x)

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

⊦ ∀x y. x + y = y + x

⊦ ∀n. divides oddprime n ⇔ n mod oddprime = 0

⊦ ∀n. n < oddprime ⇒ n mod oddprime = n

⊦ ∀x. fromNatural x = 0 ⇔ divides oddprime x

⊦ ∀n. n mod oddprime mod oddprime = n mod oddprime

⊦ ∀x y. x < y ⇔ ¬(y ≤ x)

⊦ ∀x y. x - y = x + ~y

⊦ ∀x. ~x = 0 ⇔ x = 0

⊦ ∀x y. x < y ⇔ toNatural x < toNatural y

⊦ ∀x y. x ≤ y ⇔ toNatural x ≤ toNatural y

⊦ ∀x y. x * ~y = ~(x * y)

⊦ ∀x y. ~x * y = ~(x * y)

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

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

⊦ ∀m n. fromNatural (m ↑ n) = fromNatural m ↑ n

⊦ ∀x y. x + y = x ⇔ y = 0

⊦ ∀x y. y + x = x ⇔ y = 0

⊦ ∀x y. ~x + ~y = ~(x + y)

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

⊦ ∀x₁ y₁. fromNatural (x₁ * y₁) = fromNatural x₁ * fromNatural y₁

⊦ ∀x₁ y₁. fromNatural (x₁ + y₁) = fromNatural x₁ + fromNatural y₁

⊦ ∀x y. toNatural (x * y) = toNatural x * toNatural y mod oddprime

⊦ ∀x y. toNatural (x + y) = (toNatural x + toNatural y) mod oddprime

⊦ ∀x y z. x * y * z = x * (y * z)

⊦ ∀x y z. x + y + z = x + (y + z)

⊦ ∀x y z. x + y = x + z ⇔ y = z

⊦ ∀x y z. y + x = z + x ⇔ y = z

⊦ ∀n. 0 ↑ n = if n = 0 then 1 else 0

⊦ ∀x y. fromNatural x = fromNatural y ⇔ x mod oddprime = y mod oddprime

⊦ ∀x y z. x * (y + z) = x * y + x * z

⊦ ∀x y z. (y + z) * x = y * x + z * x

⊦ ∀x m n. x ↑ m * x ↑ n = x ↑ (m + n)

⊦ ∀m n.
(m mod oddprime) * (n mod oddprime) mod oddprime = m * n mod oddprime

⊦ ∀m n.
(m mod oddprime + n mod oddprime) mod oddprime = (m + n) mod oddprime

⊦ ∀x y. x < oddprime ∧ y < oddprime ∧ fromNatural x = fromNatural y ⇒ x = y

Input Type Operators

→
bool
Number
- Natural
  - natural

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
Number
- GF(p)
  - oddprime
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - div
  - divides
  - mod
  - prime
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ prime oddprime

⊦ ¬prime 0

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

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

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀n. 0 * n = 0

⊦ ∀n. 0 + n = n

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. 1 * m = m

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀m n. m < n ⇒ m ≤ n

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

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

⊦ ∀n. ¬(n = 0) ⇒ n mod n = 0

⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x

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

⊦ ∀m n. m < n ⇒ m div n = 0

⊦ ∀m n. m < n ⇒ m mod n = m

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀n. 0 ↑ n = if n = 0 then 1 else 0

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

⊦ ∀m n. ¬(n = 0) ⇒ m mod n < n

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀m n. n ≤ m ⇒ m - n + n = m

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

⊦ ∀m n p. m * (n * p) = m * n * p

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)

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

⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ b mod a = 0)

⊦ ∀m n. ¬(n = 0) ⇒ m mod n mod n = m mod n

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀m n p. (m + n) * p = m * p + n * p

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀m n. ¬(n = 0) ⇒ (m div n) * n + m mod n = m

⊦ ∀m n p. ¬(n = 0) ⇒ (m mod n) * (p mod n) mod n = m * p mod n

⊦ ∀a b n. ¬(n = 0) ⇒ (a mod n + b mod n) mod n = (a + b) mod n