Theory Mod_Ring_Numeral

theory Mod_Ring_Numeral
imports
  "Berlekamp_Zassenhaus.Poly_Mod" 
  "Berlekamp_Zassenhaus.Poly_Mod_Finite_Field"
  "HOL-Library.Numeral_Type"

begin
section ‹Lemmas for Simplification of Modulo Equivalences›
lemma to_int_mod_ring_of_int [simp]:
  "to_int_mod_ring (of_int n :: 'a :: nontriv mod_ring) = n mod int CARD('a)"
  by transfer auto

lemma to_int_mod_ring_of_nat [simp]:
  "to_int_mod_ring (of_nat n :: 'a :: nontriv mod_ring) = n mod CARD('a)"
  by transfer (auto simp: of_nat_mod)

lemma to_int_mod_ring_numeral [simp]:
  "to_int_mod_ring (numeral n :: 'a :: nontriv mod_ring) = numeral n mod CARD('a)"
  by (metis of_nat_numeral to_int_mod_ring_of_nat)

lemma of_int_mod_ring_eq_iff [simp]:
  "((of_int a :: 'a :: nontriv mod_ring) = of_int b) ⟷
   ((a mod CARD('a)) = (b mod CARD('a)))"
  by (metis to_int_mod_ring_hom.eq_iff to_int_mod_ring_of_int)

lemma of_nat_mod_ring_eq_iff [simp]:
  "((of_nat a :: 'a :: nontriv mod_ring) = of_nat b) ⟷
   ((a mod CARD('a)) = (b mod CARD('a)))"
  by (metis of_nat_eq_iff to_int_mod_ring_hom.eq_iff to_int_mod_ring_of_nat)

lemma one_eq_numeral_mod_ring_iff [simp]:
  "(1 :: 'a :: nontriv mod_ring) = numeral a ⟷ (1 mod CARD('a)) = (numeral a mod CARD('a))"
  using of_nat_mod_ring_eq_iff[of 1 "numeral a", where ?'a = 'a]
  by (simp del: of_nat_mod_ring_eq_iff)

lemma numeral_eq_one_mod_ring_iff [simp]:
  "numeral a = (1 :: 'a :: nontriv mod_ring) ⟷ (numeral a mod CARD('a)) = (1 mod CARD('a))"
  using of_nat_mod_ring_eq_iff[of "numeral a" 1, where ?'a = 'a]
  by (simp del: of_nat_mod_ring_eq_iff)

lemma zero_eq_numeral_mod_ring_iff [simp]:
  "(0 :: 'a :: nontriv mod_ring) = numeral a ⟷ 0 = (numeral a mod CARD('a))"
  using of_nat_mod_ring_eq_iff[of 0 "numeral a", where ?'a = 'a]
  by (simp del: of_nat_mod_ring_eq_iff)

lemma numeral_eq_zero_mod_ring_iff [simp]:
  "numeral a = (0 :: 'a :: nontriv mod_ring) ⟷ (numeral a mod CARD('a)) = 0"
  using of_nat_mod_ring_eq_iff[of "numeral a" 0, where ?'a = 'a]
  by (simp del: of_nat_mod_ring_eq_iff)

lemma numeral_mod_ring_eq_iff [simp]:
  "((numeral a :: 'a :: nontriv mod_ring) = numeral b) ⟷
   ((numeral a mod CARD('a)) = (numeral b mod CARD('a)))"
  using of_nat_mod_ring_eq_iff[of "numeral a" "numeral b", where ?'a = 'a]
  by (simp del: of_nat_mod_ring_eq_iff)


instantiation bit1 :: (finite) nontriv
begin
instance proof
  show "1 < CARD('a bit1)" by simp
qed
end



end