Theory Poly_Mod_Finite_Field_Record_Based

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
*)
subsubsection ‹Over a Finite Field›
theory Poly_Mod_Finite_Field_Record_Based
imports
Poly_Mod_Finite_Field
Finite_Field_Record_Based
Polynomial_Record_Based
begin

locale arith_ops_record = arith_ops ops + poly_mod m for ops :: "'i arith_ops_record" and m :: int
begin
definition M_rel_i :: "'i ⇒ int ⇒ bool" where
"M_rel_i f F = (arith_ops_record.to_int ops f = M F)"

definition Mp_rel_i :: "'i list ⇒ int poly ⇒ bool" where
"Mp_rel_i f F = (map (arith_ops_record.to_int ops) f = coeffs (Mp F))"

lemma Mp_rel_i_Mp[simp]: "Mp_rel_i f (Mp F) = Mp_rel_i f F" unfolding Mp_rel_i_def by auto

lemma Mp_rel_i_Mp_to_int_poly_i: "Mp_rel_i f F ⟹ Mp (to_int_poly_i ops f) = to_int_poly_i ops f"
unfolding Mp_rel_i_def to_int_poly_i_def by simp
end

locale mod_ring_gen = ring_ops ff_ops R for ff_ops :: "'i arith_ops_record" and
R :: "'i ⇒ 'a :: nontriv mod_ring ⇒ bool" +
fixes p :: int
assumes p: "p = int CARD('a)"
and of_int: "0 ≤ x ⟹ x < p ⟹ R (arith_ops_record.of_int ff_ops x) (of_int x)"
and to_int: "R y z ⟹ arith_ops_record.to_int ff_ops y = to_int_mod_ring z"
and to_int': "0 ≤ arith_ops_record.to_int ff_ops y ⟹ arith_ops_record.to_int ff_ops y < p ⟹
R y (of_int (arith_ops_record.to_int ff_ops y))"
begin

lemma nat_p: "nat p = CARD('a)" unfolding p by simp

sublocale poly_mod_type p "TYPE('a)"
by (unfold_locales, rule p)

lemma coeffs_to_int_poly: "coeffs (to_int_poly (x :: 'a mod_ring poly)) = map to_int_mod_ring (coeffs x)"
by (rule coeffs_map_poly, auto)

lemma coeffs_of_int_poly: "coeffs (of_int_poly (Mp x) :: 'a mod_ring poly) = map of_int (coeffs (Mp x))"
apply (rule coeffs_map_poly)
by (metis M_0 M_M Mp_coeff leading_coeff_0_iff of_int_hom.hom_zero to_int_mod_ring_of_int_M)

lemma to_int_poly_i: assumes "poly_rel f g" shows "to_int_poly_i ff_ops f = to_int_poly g"
proof -
have *: "map (arith_ops_record.to_int ff_ops) f = coeffs (to_int_poly g)"
unfolding coeffs_to_int_poly
by (rule nth_equalityI, insert assms, auto simp: list_all2_conv_all_nth poly_rel_def to_int)
show ?thesis unfolding coeffs_eq_iff to_int_poly_i_def poly_of_list_def coeffs_Poly *
strip_while_coeffs..
qed

lemma poly_rel_of_int_poly: assumes id: "f' = of_int_poly_i ff_ops (Mp f)" "f'' = of_int_poly (Mp f)"
shows "poly_rel f' f''" unfolding id poly_rel_def
unfolding list_all2_conv_all_nth coeffs_of_int_poly of_int_poly_i_def length_map
by (rule conjI[OF refl], intro allI impI, simp add: nth_coeffs_coeff Mp_coeff M_def, rule of_int,
insert p, auto)

sublocale arith_ops_record ff_ops p .

lemma Mp_rel_iI: "poly_rel f1 f2 ⟹ MP_Rel f3 f2 ⟹ Mp_rel_i f1 f3"
unfolding Mp_rel_i_def MP_Rel_def poly_rel_def
by (auto simp add: list_all2_conv_all_nth to_int intro: nth_equalityI)

lemma M_rel_iI: "R f1 f2 ⟹ M_Rel f3 f2 ⟹ M_rel_i f1 f3"
unfolding M_rel_i_def M_Rel_def by (simp add: to_int)

lemma M_rel_iI': assumes "R f1 f2"
shows "M_rel_i f1 (arith_ops_record.to_int ff_ops f1)"
by (rule M_rel_iI[OF assms], simp add: to_int[OF assms] M_Rel_def M_to_int_mod_ring)

lemma Mp_rel_iI': assumes "poly_rel f1 f2"
shows "Mp_rel_i f1 (to_int_poly_i ff_ops f1)"
proof (rule Mp_rel_iI[OF assms], unfold to_int_poly_i[OF assms])
show "MP_Rel (to_int_poly f2) f2" unfolding MP_Rel_def by (simp add: Mp_to_int_poly)
qed

lemma M_rel_iD: assumes "M_rel_i f1 f3"
shows
"R f1 (of_int (M f3))"
"M_Rel f3 (of_int (M f3))"
proof -
show "M_Rel f3 (of_int (M f3))"
using M_Rel_def to_int_mod_ring_of_int_M by auto
from assms show "R f1 (of_int (M f3))"
unfolding M_rel_i_def
by (metis int_one_le_iff_zero_less leD linear m1 poly_mod.M_def pos_mod_sign pos_mod_bound to_int')
qed

lemma Mp_rel_iD: assumes "Mp_rel_i f1 f3"
shows
"poly_rel f1 (of_int_poly (Mp f3))"
"MP_Rel f3 (of_int_poly (Mp f3))"
proof -
show Rel: "MP_Rel f3 (of_int_poly (Mp f3))"
using MP_Rel_def Mp_Mp Mp_f_representative by auto
let ?ti = "arith_ops_record.to_int ff_ops"
from assms[unfolded Mp_rel_i_def] have
*: "coeffs (Mp f3) = map ?ti f1" by auto
{
fix x
assume "x ∈ set f1"
hence "?ti x ∈ set (map ?ti f1)" by auto
from this[folded *] have "?ti x ∈ range M"
by (metis (no_types, lifting) MP_Rel_def M_to_int_mod_ring Rel coeffs_to_int_poly ex_map_conv range_eqI)
hence "?ti x ≥ 0" "?ti x < p" unfolding M_def using m1 by auto
hence "R x (of_int (?ti x))"
by (rule to_int')
}
thus "poly_rel f1 (of_int_poly (Mp f3))" using *
unfolding poly_rel_def coeffs_of_int_poly
by (auto simp: list_all2_map2 list_all2_same)
qed
end

locale prime_field_gen = field_ops ff_ops R + mod_ring_gen ff_ops R p for ff_ops :: "'i arith_ops_record" and
R :: "'i ⇒ 'a :: prime_card mod_ring ⇒ bool" and p :: int
begin

sublocale poly_mod_prime_type p "TYPE('a)"
by (unfold_locales, rule p)

end

lemma (in mod_ring_locale) mod_ring_rel_of_int:
"0 ≤ x ⟹ x < p ⟹ mod_ring_rel x (of_int x)"
unfolding mod_ring_rel_def
by (transfer, auto simp: p)

context prime_field
begin

lemma prime_field_finite_field_ops_int: "prime_field_gen (finite_field_ops_int p) mod_ring_rel p"
proof -
interpret field_ops "finite_field_ops_int p" mod_ring_rel by (rule finite_field_ops_int)
show ?thesis
by (unfold_locales, rule p,
auto simp: finite_field_ops_int_def p mod_ring_rel_def of_int_of_int_mod_ring)
qed

lemma prime_field_finite_field_ops_integer: "prime_field_gen (finite_field_ops_integer (integer_of_int p)) mod_ring_rel_integer p"
proof -
interpret field_ops "finite_field_ops_integer (integer_of_int p)" mod_ring_rel_integer by (rule finite_field_ops_integer, simp)
have pp: "p = int_of_integer (integer_of_int p)" by auto
interpret int: prime_field_gen "finite_field_ops_int p" mod_ring_rel
by (rule prime_field_finite_field_ops_int)
show ?thesis
by (unfold_locales, rule p, auto simp: finite_field_ops_integer_def
mod_ring_rel_integer_def[OF pp] urel_integer_def[OF pp] mod_ring_rel_of_int
int.to_int[symmetric] finite_field_ops_int_def)
qed

lemma prime_field_finite_field_ops32: assumes small: "p ≤ 65535"
shows "prime_field_gen (finite_field_ops32 (uint32_of_int p)) mod_ring_rel32 p"
proof -
let ?pp = "uint32_of_int p"
have ppp: "p = int_of_uint32 ?pp"
by (subst int_of_uint32_inv, insert small p2, auto)
note * = ppp small
interpret field_ops "finite_field_ops32 ?pp" mod_ring_rel32
by (rule finite_field_ops32, insert *)
interpret int: prime_field_gen "finite_field_ops_int p" mod_ring_rel
by (rule prime_field_finite_field_ops_int)
show ?thesis
proof (unfold_locales, rule p, auto simp: finite_field_ops32_def)
fix x
assume x: "0 ≤ x" "x < p"
from int.of_int[OF this] have "mod_ring_rel x (of_int x)" by (simp add: finite_field_ops_int_def)
thus "mod_ring_rel32 (uint32_of_int x) (of_int x)" unfolding mod_ring_rel32_def[OF *]
by (intro exI[of _ x], auto simp: urel32_def[OF *], subst int_of_uint32_inv, insert * x, auto)
next
fix y z
assume "mod_ring_rel32 y z"
from this[unfolded mod_ring_rel32_def[OF *]] obtain x where yx: "urel32 y x" and xz: "mod_ring_rel x z" by auto
from int.to_int[OF xz] have zx: "to_int_mod_ring z = x" by (simp add: finite_field_ops_int_def)
show "int_of_uint32 y = to_int_mod_ring z" unfolding zx using yx unfolding urel32_def[OF *] by simp
next
fix y
show "0 ≤ int_of_uint32 y ⟹ int_of_uint32 y < p ⟹ mod_ring_rel32 y (of_int (int_of_uint32 y))"
unfolding mod_ring_rel32_def[OF *] urel32_def[OF *]
by (intro exI[of _ "int_of_uint32 y"], auto simp: mod_ring_rel_of_int)
qed
qed

lemma prime_field_finite_field_ops64: assumes small: "p ≤ 4294967295"
shows "prime_field_gen (finite_field_ops64 (uint64_of_int p)) mod_ring_rel64 p"
proof -
let ?pp = "uint64_of_int p"
have ppp: "p = int_of_uint64 ?pp"
by (subst int_of_uint64_inv, insert small p2, auto)
note * = ppp small
interpret field_ops "finite_field_ops64 ?pp" mod_ring_rel64
by (rule finite_field_ops64, insert *)
interpret int: prime_field_gen "finite_field_ops_int p" mod_ring_rel
by (rule prime_field_finite_field_ops_int)
show ?thesis
proof (unfold_locales, rule p, auto simp: finite_field_ops64_def)
fix x
assume x: "0 ≤ x" "x < p"
from int.of_int[OF this] have "mod_ring_rel x (of_int x)" by (simp add: finite_field_ops_int_def)
thus "mod_ring_rel64 (uint64_of_int x) (of_int x)" unfolding mod_ring_rel64_def[OF *]
by (intro exI[of _ x], auto simp: urel64_def[OF *], subst int_of_uint64_inv, insert * x, auto)
next
fix y z
assume "mod_ring_rel64 y z"
from this[unfolded mod_ring_rel64_def[OF *]] obtain x where yx: "urel64 y x" and xz: "mod_ring_rel x z" by auto
from int.to_int[OF xz] have zx: "to_int_mod_ring z = x" by (simp add: finite_field_ops_int_def)
show "int_of_uint64 y = to_int_mod_ring z" unfolding zx using yx unfolding urel64_def[OF *] by simp
next
fix y
show "0 ≤ int_of_uint64 y ⟹ int_of_uint64 y < p ⟹ mod_ring_rel64 y (of_int (int_of_uint64 y))"
unfolding mod_ring_rel64_def[OF *] urel64_def[OF *]
by (intro exI[of _ "int_of_uint64 y"], auto simp: mod_ring_rel_of_int)
qed
qed
end

context mod_ring_locale
begin
lemma mod_ring_finite_field_ops_int: "mod_ring_gen (finite_field_ops_int p) mod_ring_rel p"
proof -
interpret ring_ops "finite_field_ops_int p" mod_ring_rel by (rule ring_finite_field_ops_int)
show ?thesis
by (unfold_locales, rule p,
auto simp: finite_field_ops_int_def p mod_ring_rel_def of_int_of_int_mod_ring)
qed

lemma mod_ring_finite_field_ops_integer: "mod_ring_gen (finite_field_ops_integer (integer_of_int p)) mod_ring_rel_integer p"
proof -
interpret ring_ops "finite_field_ops_integer (integer_of_int p)" mod_ring_rel_integer by (rule ring_finite_field_ops_integer, simp)
have pp: "p = int_of_integer (integer_of_int p)" by auto
interpret int: mod_ring_gen "finite_field_ops_int p" mod_ring_rel
by (rule mod_ring_finite_field_ops_int)
show ?thesis
by (unfold_locales, rule p, auto simp: finite_field_ops_integer_def
mod_ring_rel_integer_def[OF pp] urel_integer_def[OF pp] mod_ring_rel_of_int
int.to_int[symmetric] finite_field_ops_int_def)
qed

lemma mod_ring_finite_field_ops32: assumes small: "p ≤ 65535"
shows "mod_ring_gen (finite_field_ops32 (uint32_of_int p)) mod_ring_rel32 p"
proof -
let ?pp = "uint32_of_int p"
have ppp: "p = int_of_uint32 ?pp"
by (subst int_of_uint32_inv, insert small p2, auto)
note * = ppp small
interpret ring_ops "finite_field_ops32 ?pp" mod_ring_rel32
by (rule ring_finite_field_ops32, insert *)
interpret int: mod_ring_gen "finite_field_ops_int p" mod_ring_rel
by (rule mod_ring_finite_field_ops_int)
show ?thesis
proof (unfold_locales, rule p, auto simp: finite_field_ops32_def)
fix x
assume x: "0 ≤ x" "x < p"
from int.of_int[OF this] have "mod_ring_rel x (of_int x)" by (simp add: finite_field_ops_int_def)
thus "mod_ring_rel32 (uint32_of_int x) (of_int x)" unfolding mod_ring_rel32_def[OF *]
by (intro exI[of _ x], auto simp: urel32_def[OF *], subst int_of_uint32_inv, insert * x, auto)
next
fix y z
assume "mod_ring_rel32 y z"
from this[unfolded mod_ring_rel32_def[OF *]] obtain x where yx: "urel32 y x" and xz: "mod_ring_rel x z" by auto
from int.to_int[OF xz] have zx: "to_int_mod_ring z = x" by (simp add: finite_field_ops_int_def)
show "int_of_uint32 y = to_int_mod_ring z" unfolding zx using yx unfolding urel32_def[OF *] by simp
next
fix y
show "0 ≤ int_of_uint32 y ⟹ int_of_uint32 y < p ⟹ mod_ring_rel32 y (of_int (int_of_uint32 y))"
unfolding mod_ring_rel32_def[OF *] urel32_def[OF *]
by (intro exI[of _ "int_of_uint32 y"], auto simp: mod_ring_rel_of_int)
qed
qed

lemma mod_ring_finite_field_ops64: assumes small: "p ≤ 4294967295"
shows "mod_ring_gen (finite_field_ops64 (uint64_of_int p)) mod_ring_rel64 p"
proof -
let ?pp = "uint64_of_int p"
have ppp: "p = int_of_uint64 ?pp"
by (subst int_of_uint64_inv, insert small p2, auto)
note * = ppp small
interpret ring_ops "finite_field_ops64 ?pp" mod_ring_rel64
by (rule ring_finite_field_ops64, insert *)
interpret int: mod_ring_gen "finite_field_ops_int p" mod_ring_rel
by (rule mod_ring_finite_field_ops_int)
show ?thesis
proof (unfold_locales, rule p, auto simp: finite_field_ops64_def)
fix x
assume x: "0 ≤ x" "x < p"
from int.of_int[OF this] have "mod_ring_rel x (of_int x)" by (simp add: finite_field_ops_int_def)
thus "mod_ring_rel64 (uint64_of_int x) (of_int x)" unfolding mod_ring_rel64_def[OF *]
by (intro exI[of _ x], auto simp: urel64_def[OF *], subst int_of_uint64_inv, insert * x, auto)
next
fix y z
assume "mod_ring_rel64 y z"
from this[unfolded mod_ring_rel64_def[OF *]] obtain x where yx: "urel64 y x" and xz: "mod_ring_rel x z" by auto
from int.to_int[OF xz] have zx: "to_int_mod_ring z = x" by (simp add: finite_field_ops_int_def)
show "int_of_uint64 y = to_int_mod_ring z" unfolding zx using yx unfolding urel64_def[OF *] by simp
next
fix y
show "0 ≤ int_of_uint64 y ⟹ int_of_uint64 y < p ⟹ mod_ring_rel64 y (of_int (int_of_uint64 y))"
unfolding mod_ring_rel64_def[OF *] urel64_def[OF *]
by (intro exI[of _ "int_of_uint64 y"], auto simp: mod_ring_rel_of_int)
qed
qed
end

end
```