Theory Finite_Field

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
section ‹Finite Rings and Fields›

text ‹We start by establishing some preliminary results about finite rings and finite fields›

subsection ‹Finite Rings›

theory Finite_Field
imports 
  "HOL-Computational_Algebra.Primes"
  "HOL-Number_Theory.Residues"
  "HOL-Library.Cardinality"
  Subresultants.Binary_Exponentiation
  Polynomial_Interpolation.Ring_Hom_Poly
begin

typedef ('a::finite) mod_ring = "{0..<int CARD('a)}" by auto

setup_lifting type_definition_mod_ring

lemma CARD_mod_ring[simp]: "CARD('a mod_ring) = CARD('a::finite)" 
proof -
  have "card {y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = card {0..<int CARD('a)}"
  proof (rule bij_betw_same_card)
    have "inj_on Rep_mod_ring {y. ∃x∈{0..<int CARD('a)}. y = Abs_mod_ring x}"
      by (meson Rep_mod_ring_inject inj_onI)      
    moreover have "Rep_mod_ring ` {y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = {0..<int CARD('a)}"
    proof (auto simp add: image_def Rep_mod_ring_inject)
      fix xb show "0 ≤ Rep_mod_ring (Abs_mod_ring xb)" 
        using Rep_mod_ring atLeastLessThan_iff by blast 
      assume xb1: "0 ≤ xb" and xb2: "xb < int CARD('a)"
      thus " Rep_mod_ring (Abs_mod_ring xb) < int CARD('a)"
        by (metis Abs_mod_ring_inverse Rep_mod_ring atLeastLessThan_iff le_less_trans linear)
      have xb: "xb ∈ {0..<int CARD('a)}" using xb1 xb2 by simp
      show "∃xa::'a mod_ring. (∃x∈{0..<int CARD('a)}. xa = Abs_mod_ring x) ∧ xb = Rep_mod_ring xa"
      by (rule exI[of _ "Abs_mod_ring xb"], auto simp add: xb1 xb2, rule Abs_mod_ring_inverse[OF xb, symmetric])
    qed    
    ultimately show "bij_betw Rep_mod_ring
      {y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} 
      {0..<int CARD('a)}"
      by (simp add: bij_betw_def)
  qed
  thus ?thesis
    unfolding type_definition.univ[OF type_definition_mod_ring]
    unfolding image_def by auto
qed

instance mod_ring :: (finite) finite 
proof (intro_classes)
  show "finite (UNIV::'a mod_ring set)" 
    unfolding type_definition.univ[OF type_definition_mod_ring]
    using finite by simp
qed


instantiation mod_ring :: (finite) equal
begin
lift_definition equal_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ bool" is "(=)" .
instance by (intro_classes, transfer, auto)
end

instantiation mod_ring :: (finite) comm_ring
begin

lift_definition plus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
  "λ x y. (x + y) mod int (CARD('a))" by simp

lift_definition uminus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" is
  "λ x. if x = 0 then 0 else int (CARD('a)) - x" by simp

lift_definition minus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
  "λ x y. (x - y) mod int (CARD('a))" by simp

lift_definition times_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
  "λ x y. (x * y) mod int (CARD('a))" by simp

lift_definition zero_mod_ring :: "'a mod_ring" is 0 by simp

instance
  by standard
    (transfer; auto simp add: mod_simps algebra_simps intro: mod_diff_cong)+

end

lift_definition to_int_mod_ring :: "'a::finite mod_ring ⇒ int" is "λ x. x" .

lift_definition of_int_mod_ring :: "int ⇒ 'a::finite mod_ring" is
  "λ x. x mod int (CARD('a))" by simp

interpretation to_int_mod_ring_hom: inj_zero_hom to_int_mod_ring
  by (unfold_locales; transfer, auto)

lemma int_nat_card[simp]: "int (nat CARD('a::finite)) = CARD('a)" by auto

interpretation of_int_mod_ring_hom: zero_hom of_int_mod_ring
  by (unfold_locales, transfer, auto)

lemma of_int_mod_ring_to_int_mod_ring[simp]:
  "of_int_mod_ring (to_int_mod_ring x) = x" by (transfer, auto)

lemma to_int_mod_ring_of_int_mod_ring[simp]: "0 ≤ x ⟹ x < int CARD('a :: finite) ⟹
  to_int_mod_ring (of_int_mod_ring x :: 'a mod_ring) = x"
  by (transfer, auto)

lemma range_to_int_mod_ring:
  "range (to_int_mod_ring :: ('a :: finite mod_ring ⇒ int)) = {0 ..< CARD('a)}"
  apply (intro equalityI subsetI)
  apply (elim rangeE, transfer, force)
  by (auto intro!: range_eqI to_int_mod_ring_of_int_mod_ring[symmetric])

subsection ‹Nontrivial Finite Rings›

class nontriv = assumes nontriv: "CARD('a) > 1"

subclass(in nontriv) finite by(intro_classes,insert nontriv,auto intro:card_ge_0_finite)

instantiation mod_ring :: (nontriv) comm_ring_1
begin

lift_definition one_mod_ring :: "'a mod_ring" is 1 using nontriv[where ?'a='a] by auto

instance by (intro_classes; transfer, simp)

end

interpretation to_int_mod_ring_hom: inj_one_hom to_int_mod_ring
  by (unfold_locales, transfer, simp)

lemma of_nat_of_int_mod_ring [code_unfold]:
  "of_nat = of_int_mod_ring o int"
proof (rule ext, unfold o_def)
  show "of_nat n = of_int_mod_ring (int n)" for n
  proof (induct n)
    case (Suc n)
    show ?case
      by (simp only: of_nat_Suc Suc, transfer) (simp add: mod_simps)
  qed simp
qed

lemma of_nat_card_eq_0[simp]: "(of_nat (CARD('a::nontriv)) :: 'a mod_ring) = 0"
  by (unfold of_nat_of_int_mod_ring, transfer, auto)

lemma of_int_of_int_mod_ring[code_unfold]: "of_int = of_int_mod_ring"
proof (rule ext)
  fix x :: int
  obtain n1 n2 where x: "x = int n1 - int n2" by (rule int_diff_cases)
  show "of_int x = of_int_mod_ring x"
    unfolding x of_int_diff of_int_of_nat_eq of_nat_of_int_mod_ring o_def
    by (transfer, simp add: mod_diff_right_eq mod_diff_left_eq)
qed

unbundle lifting_syntax

lemma pcr_mod_ring_to_int_mod_ring: "pcr_mod_ring = (λx y. x = to_int_mod_ring y)"
 unfolding mod_ring.pcr_cr_eq unfolding cr_mod_ring_def to_int_mod_ring.rep_eq ..

lemma [transfer_rule]:
  "((=) ===> pcr_mod_ring) (λ x. int x mod int (CARD('a :: nontriv))) (of_nat :: nat ⇒ 'a mod_ring)"
  by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_nat_of_int_mod_ring, transfer, auto)

lemma [transfer_rule]:
  "((=) ===> pcr_mod_ring) (λ x. x mod int (CARD('a :: nontriv))) (of_int :: int ⇒ 'a mod_ring)"
  by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_int_of_int_mod_ring, transfer, auto)

lemma one_mod_card [simp]: "1 mod CARD('a::nontriv) = 1"
  using mod_less nontriv by blast 

lemma Suc_0_mod_card [simp]: "Suc 0 mod CARD('a::nontriv) = 1"
  using one_mod_card by simp

lemma one_mod_card_int [simp]: "1 mod int CARD('a::nontriv) = 1"
proof -
  from nontriv [where ?'a = 'a] have "int (1 mod CARD('a::nontriv)) = 1"
    by simp
  then show ?thesis
    using of_nat_mod [of 1 "CARD('a)", where ?'a = int] by simp
qed

lemma pow_mod_ring_transfer[transfer_rule]:
  "(pcr_mod_ring ===> (=) ===> pcr_mod_ring) 
   (λa::int. λn. a^n mod CARD('a::nontriv)) ((^)::'a mod_ring ⇒ nat ⇒ 'a mod_ring)"
unfolding pcr_mod_ring_to_int_mod_ring
proof (intro rel_funI,simp)
  fix x::"'a mod_ring" and n
  show "to_int_mod_ring x ^ n mod int CARD('a) = to_int_mod_ring (x ^ n)"
  proof (induct n)
    case 0
    thus ?case by auto
  next
    case (Suc n)
    have "to_int_mod_ring (x ^ Suc n) = to_int_mod_ring (x * x ^ n)" by auto
    also have "... = to_int_mod_ring x * to_int_mod_ring (x ^ n) mod CARD('a)"
      unfolding to_int_mod_ring_def using times_mod_ring.rep_eq by auto
    also have "... = to_int_mod_ring x * (to_int_mod_ring x ^ n mod CARD('a)) mod CARD('a)"
      using Suc.hyps by auto
    also have "... = to_int_mod_ring x ^ Suc n mod int CARD('a)"
      by (simp add: mod_simps)
    finally show ?case ..
  qed
qed

lemma dvd_mod_ring_transfer[transfer_rule]:
"((pcr_mod_ring :: int ⇒ 'a :: nontriv mod_ring ⇒ bool) ===>
  (pcr_mod_ring :: int ⇒ 'a mod_ring ⇒ bool) ===> (=))
  (λ i j. ∃k ∈ {0..<int CARD('a)}. j = i * k mod int CARD('a)) (dvd)"
proof (unfold pcr_mod_ring_to_int_mod_ring, intro rel_funI iffI)
  fix x y :: "'a mod_ring" and i j
  assume i: "i = to_int_mod_ring x" and j: "j = to_int_mod_ring y"
  { assume "x dvd y"
    then obtain z where "y = x * z" by (elim dvdE, auto)
    then have "j = i * to_int_mod_ring z mod CARD('a)" by (unfold i j, transfer)
    with range_to_int_mod_ring
    show "∃k ∈ {0..<int CARD('a)}. j = i * k mod CARD('a)" by auto
  }
  assume "∃k ∈ {0..<int CARD('a)}. j = i * k mod CARD('a)"
  then obtain k where k: "k ∈ {0..<int CARD('a)}" and dvd: "j = i * k mod CARD('a)" by auto
  from k have "to_int_mod_ring (of_int k :: 'a mod_ring) = k" by (transfer, auto)
  also from dvd have "j = i * ... mod CARD('a)" by auto
  finally have "y = x * (of_int k :: 'a mod_ring)" unfolding i j using k by (transfer, auto)
  then show "x dvd y" by auto
qed

lemma Rep_mod_ring_mod[simp]: "Rep_mod_ring (a :: 'a :: nontriv mod_ring) mod CARD('a) = Rep_mod_ring a"
  using Rep_mod_ring[where 'a = 'a] by auto

subsection ‹Finite Fields›

text ‹When the domain is prime, the ring becomes a field›

class prime_card = assumes prime_card: "prime (CARD('a))"
begin
lemma prime_card_int: "prime (int (CARD('a)))" using prime_card by auto

subclass nontriv using prime_card prime_gt_1_nat by (intro_classes,auto)
end

instance bool :: prime_card
  by standard auto

instantiation mod_ring :: (prime_card) field
begin
 
definition inverse_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where
  "inverse_mod_ring x = (if x = 0 then 0 else x ^ (nat (CARD('a) - 2)))"

definition divide_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring"  where
  "divide_mod_ring x y = x * ((λc. if c = 0 then 0 else c ^ (nat (CARD('a) - 2))) y)" 

instance
proof
  fix a b c::"'a mod_ring"
  show "inverse 0 = (0::'a mod_ring)" by (simp add: inverse_mod_ring_def)
  show "a div b = a * inverse b" 
    unfolding inverse_mod_ring_def by (transfer', simp add: divide_mod_ring_def)
  show "a ≠ 0 ⟹ inverse a * a = 1"
  proof (unfold inverse_mod_ring_def, transfer)
    let ?p="CARD('a)"
    fix x
    assume x: "x ∈ {0..<int CARD('a)}" and x0: "x ≠ 0"
    have p0': "0≤?p" by auto
    have "¬ ?p dvd x"
      using x x0 zdvd_imp_le by fastforce
    then have "¬ CARD('a) dvd nat ¦x¦"
      by simp
    with x have "¬ CARD('a) dvd nat x"
      by simp
    have rw: "x ^ nat (int (?p - 2)) * x = x ^ nat (?p - 1)"
    proof -
      have p2: "0 ≤ int (?p-2)" using x by simp
      have card_rw: "(CARD('a) - Suc 0) = nat (1 + int (CARD('a) - 2))" 
        using nat_eq_iff x x0 by auto
      have "x ^ nat (?p - 2)*x = x ^ (Suc (nat (?p - 2)))" by simp
      also have "... = x ^ (nat (?p - 1))"
        using Suc_nat_eq_nat_zadd1[OF p2] card_rw by auto
      finally show ?thesis .
    qed
    have "[int (nat x ^ (CARD('a) - 1)) = int 1] (mod CARD('a))"
      using fermat_theorem [OF prime_card ‹¬ CARD('a) dvd nat x›]
      by (simp only: cong_def cong_def of_nat_mod [symmetric])
    then have *: "[x ^ (CARD('a) - 1) = 1] (mod CARD('a))"
      using x by auto
    have "x ^ (CARD('a) - 2) mod CARD('a) * x mod CARD('a) 
      = (x ^ nat (CARD('a) - 2) * x) mod CARD('a)" by (simp add: mod_simps)
    also have "... =  (x ^ nat (?p - 1) mod ?p)" unfolding rw by simp
    also have "... = (x ^ (nat ?p - 1) mod ?p)" using p0' by (simp add: nat_diff_distrib')
    also have "... = 1"
      using * by (simp add: cong_def)
    finally show "(if x = 0 then 0 else x ^ nat (int (CARD('a) - 2)) mod CARD('a)) * x mod CARD('a) = 1"
      using x0 by auto
  qed
qed
end

instantiation mod_ring :: (prime_card) "{normalization_euclidean_semiring, euclidean_ring}"
begin

definition modulo_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "modulo_mod_ring x y = (if y = 0 then x else 0)"
definition normalize_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where "normalize_mod_ring x = (if x = 0 then 0 else 1)" 
definition unit_factor_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where "unit_factor_mod_ring x = x" 
definition euclidean_size_mod_ring :: "'a mod_ring ⇒ nat" where "euclidean_size_mod_ring x = (if x = 0 then 0 else 1)" 

instance
proof (intro_classes)
  fix a :: "'a mod_ring" show "a ≠ 0 ⟹ unit_factor a dvd 1"
    unfolding dvd_def unit_factor_mod_ring_def by (intro exI[of _ "inverse a"], auto)
qed (auto simp: normalize_mod_ring_def unit_factor_mod_ring_def modulo_mod_ring_def
     euclidean_size_mod_ring_def field_simps)
end

instantiation mod_ring :: (prime_card) euclidean_ring_gcd
begin

definition gcd_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "gcd_mod_ring = Euclidean_Algorithm.gcd"
definition lcm_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "lcm_mod_ring = Euclidean_Algorithm.lcm"
definition Gcd_mod_ring :: "'a mod_ring set ⇒ 'a mod_ring" where "Gcd_mod_ring = Euclidean_Algorithm.Gcd"
definition Lcm_mod_ring :: "'a mod_ring set ⇒ 'a mod_ring" where "Lcm_mod_ring = Euclidean_Algorithm.Lcm"

instance by (intro_classes, auto simp: gcd_mod_ring_def lcm_mod_ring_def Gcd_mod_ring_def Lcm_mod_ring_def)
end

instantiation mod_ring :: (prime_card) unique_euclidean_ring
begin

definition [simp]: "division_segment_mod_ring (x :: 'a mod_ring) = (1 :: 'a mod_ring)"

instance by intro_classes (auto simp: euclidean_size_mod_ring_def split: if_splits)

end

instance mod_ring :: (prime_card) field_gcd
  by intro_classes auto


lemma surj_of_nat_mod_ring: "∃ i. i < CARD('a :: prime_card) ∧ (x :: 'a mod_ring) = of_nat i" 
  by (rule exI[of _ "nat (to_int_mod_ring x)"], unfold of_nat_of_int_mod_ring o_def,
  subst nat_0_le, transfer, simp, simp, transfer, auto) 

lemma of_nat_0_mod_ring_dvd: assumes x: "of_nat x = (0 :: 'a ::prime_card mod_ring)"
  shows "CARD('a) dvd x" 
proof -
  let ?x = "of_nat x :: int" 
  from x have "of_int_mod_ring ?x = (0 :: 'a mod_ring)" by (fold of_int_of_int_mod_ring, simp)
  hence "?x mod CARD('a) = 0" by (transfer, auto)
  hence "x mod CARD('a) = 0" by presburger
  thus ?thesis unfolding mod_eq_0_iff_dvd .
qed

lemma semiring_char_mod_ring [simp]:
  "CHAR('n :: nontriv mod_ring) = CARD('n)"
proof (rule CHAR_eq_posI)
  fix x assume "x > 0" "x < CARD('n)"
  thus "of_nat x ≠ (0 :: 'n mod_ring)"
    by transfer auto
qed auto


text ‹
  The following Material was contributed by Manuel Eberl
›
instance mod_ring :: (prime_card) finite_field
  by standard simp_all

instantiation mod_ring :: (prime_card) enum_finite_field
begin

definition enum_finite_field_mod_ring :: "nat ⇒ 'a mod_ring" where
  "enum_finite_field_mod_ring n = of_int_mod_ring (int n)"

instance proof
  interpret type_definition "Rep_mod_ring :: 'a mod_ring ⇒ int" Abs_mod_ring "{0..<CARD('a)}"
    by (rule type_definition_mod_ring)
  have "enum_finite_field ` {..<CARD('a mod_ring)} = of_int_mod_ring ` int ` {..<CARD('a mod_ring)}"
    unfolding enum_finite_field_mod_ring_def by (simp add: image_image o_def)
  also have "int ` {..<CARD('a mod_ring)} = {0..<int CARD('a mod_ring)}"
    by (simp add: image_atLeastZeroLessThan_int)
  also have "of_int_mod_ring ` … = (Abs_mod_ring ` … :: 'a mod_ring set)"
    by (intro image_cong refl) (auto simp: of_int_mod_ring_def)
  also have "… = (UNIV :: 'a mod_ring set)"
    using Abs_image by simp
  finally show "enum_finite_field ` {..<CARD('a mod_ring)} = (UNIV :: 'a mod_ring set)" .
qed

end

typedef (overloaded) 'a :: semiring_1 ring_char = "if CHAR('a) = 0 then UNIV else {0..<CHAR('a)}"
  by auto

lemma CARD_ring_char [simp]: "CARD ('a :: semiring_1 ring_char) = CHAR('a)"
proof -
  let ?A = "if CHAR('a) = 0 then UNIV else {0..<CHAR('a)}"
  interpret type_definition "Rep_ring_char :: 'a ring_char ⇒ nat" Abs_ring_char ?A
    by (rule type_definition_ring_char)
  from card show ?thesis
    by auto
qed

instance ring_char :: (semiring_prime_char) nontriv
proof
  show "CARD('a ring_char) > 1"
    using prime_nat_iff by auto
qed

instance ring_char :: (semiring_prime_char) prime_card
proof
  from CARD_ring_char show "prime CARD('a ring_char)"
    by auto
qed

lemma to_int_mod_ring_add:
  "to_int_mod_ring (x + y :: 'a :: finite mod_ring) = (to_int_mod_ring x + to_int_mod_ring y) mod CARD('a)"
  by transfer auto

lemma to_int_mod_ring_mult:
  "to_int_mod_ring (x * y :: 'a :: finite mod_ring) = (to_int_mod_ring x * to_int_mod_ring y) mod CARD('a)"
  by transfer auto

lemma of_nat_mod_CHAR [simp]: "of_nat (x mod CHAR('a :: semiring_1)) = (of_nat x :: 'a)"
  by (metis (no_types, opaque_lifting) comm_monoid_add_class.add_0 div_mod_decomp
         mult_zero_right of_nat_CHAR of_nat_add of_nat_mult)

lemma of_int_mod_CHAR [simp]: "of_int (x mod int CHAR('a :: ring_1)) = (of_int x :: 'a)"
  by (simp add: of_int_eq_iff_cong_CHAR)

end