Theory Finite_Fields_Poly_Ring_Code
section ‹Executable Polynomial Rings›
theory Finite_Fields_Poly_Ring_Code
imports
Finite_Fields_Indexed_Algebra_Code
"HOL-Algebra.Polynomials"
Finite_Fields.Card_Irreducible_Polynomials_Aux
begin
fun o_normalize :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list"
where
"o_normalize E [] = []"
| "o_normalize E p = (if lead_coeff p ≠ 0⇩C⇘E⇙ then p else o_normalize E (tl p))"
fun o_poly_add :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"o_poly_add E p1 p2 = (
if length p1 ≥ length p2
then o_normalize E (map2 (idx_plus E) p1 ((replicate (length p1 - length p2) 0⇩C⇘E⇙ ) @ p2))
else o_poly_add E p2 p1)"
fun o_poly_mult :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ 'a list"
where
"o_poly_mult E [] p2 = []"
| "o_poly_mult E p1 p2 =
o_poly_add E ((map (idx_mult E (hd p1)) p2) @
(replicate (degree p1) 0⇩C⇘E⇙ )) (o_poly_mult E (tl p1) p2)"
definition poly :: "('a,'b) idx_ring_scheme ⇒ 'a list idx_ring"
where "poly E = ⦇
idx_pred = (λx. (x = [] ∨ hd x ≠ 0⇩C⇘E⇙) ∧ list_all (idx_pred E) x),
idx_uminus = (λx. map (idx_uminus E) x),
idx_plus = o_poly_add E,
idx_udivide = (λx. [idx_udivide E (hd x)]),
idx_mult = o_poly_mult E,
idx_zero = [],
idx_one = [idx_one E] ⦈"
definition poly_var :: "('a,'b) idx_ring_scheme ⇒ 'a list" ("X⇩Cı")
where "poly_var E = [idx_one E, idx_zero E]"
lemma poly_var: "poly_var R = X⇘ring_of R⇙"
unfolding var_def poly_var_def by (simp add:ring_of_def)
fun poly_eval :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a ⇒ 'a"
where "poly_eval R fs x = fold (λa b. b *⇩C⇘R⇙ x +⇩C⇘R⇙ a) fs 0⇩C⇘R⇙"
lemma ring_of_poly:
assumes "ring⇩C A"
shows "ring_of (poly A) = poly_ring (ring_of A)"
proof (intro ring.equality)
interpret ring "ring_of A" using assms unfolding ring⇩C_def by auto
have b: "𝟬⇘ring_of A⇙ = 0⇩C⇘A⇙" unfolding ring_of_def by simp
have c: "(⊗⇘ring_of A⇙) = (*⇩C⇘A⇙)" unfolding ring_of_def by simp
have d: "(⊕⇘ring_of A⇙) = (+⇩C⇘A⇙)" unfolding ring_of_def by simp
have " o_normalize A x = normalize x" for x
using b by (induction x) simp_all
hence "o_poly_add A x y = poly_add x y" if "length y ≤ length x" for x y
using that by (subst o_poly_add.simps, subst poly_add.simps) (simp add: b d)
hence a:"o_poly_add A x y = poly_add x y" for x y
by (subst o_poly_add.simps, subst poly_add.simps) simp
hence "x ⊕⇘ring_of (poly A)⇙ y = x ⊕⇘poly_ring (ring_of A)⇙ y" for x y
by (simp add:univ_poly_def poly_def ring_of_def)
thus "(⊕⇘ring_of (poly A)⇙) = (⊕⇘poly_ring (ring_of A)⇙)" by (intro ext)
show "carrier (ring_of (poly A)) = carrier (poly_ring (ring_of A))"
by (auto simp add: ring_of_def poly_def univ_poly_def polynomial_def list_all_iff)
have "o_poly_mult A x y = poly_mult x y" for x y
proof (induction x)
case Nil then show ?case by simp
next
case (Cons a x) then show ?case
by (subst o_poly_mult.simps,subst poly_mult.simps)
(simp add:a b c del:poly_add.simps o_poly_add.simps)
qed
hence "x ⊗⇘ring_of (poly A)⇙ y = x ⊗⇘poly_ring (ring_of A)⇙ y" for x y
by (simp add: univ_poly_def poly_def ring_of_def)
thus "(⊗⇘ring_of (poly A)⇙) = (⊗⇘poly_ring (ring_of A)⇙)" by (intro ext)
qed (simp_all add:ring_of_def poly_def univ_poly_def)
lemma poly_eval:
assumes "ring⇩C R"
assumes fsc:"fs ∈ carrier (ring_of (poly R))" and xc:"x ∈ carrier (ring_of R)"
shows "poly_eval R fs x = ring.eval (ring_of R) fs x"
proof -
interpret ring "ring_of R" using assms unfolding ring⇩C_def by auto
have fs_carr:"fs ∈ carrier (poly_ring (ring_of R))" using ring_of_poly[OF assms(1)] fsc by auto
hence "set fs ⊆ carrier (ring_of R)" by (simp add: polynomial_incl univ_poly_carrier)
thus ?thesis
proof (induction rule:rev_induct)
case Nil thus ?case by simp (simp add:ring_of_def)
next
case (snoc ft fh)
have "poly_eval R (fh @ [ft]) x = poly_eval R fh x *⇩C⇘R⇙ x +⇩C⇘R⇙ ft" by simp
also have "... = eval fh x *⇩C⇘R⇙ x +⇩C⇘R⇙ ft" using snoc by (subst snoc) auto
also have "... = eval fh x ⊗⇘ring_of R⇙ x ⊕⇘ring_of R⇙ ft " by (simp add:ring_of_def)
also have " ... = eval (fh@[ft]) x" using snoc by (intro eval_append_aux[symmetric] xc) auto
finally show ?case by auto
qed
qed
lemma poly_domain:
assumes "domain⇩C A"
shows "domain⇩C (poly A)"
proof -
interpret domain "ring_of A" using assms unfolding domain⇩C_def by auto
have a:"⊖⇘ring_of A⇙ x = -⇩C⇘A⇙ x" if "x ∈ carrier (ring_of A)" for x
using that by (intro domain_cD[symmetric] assms)
have "ring⇩C A"
using assms unfolding domain⇩C_def cring⇩C_def by auto
hence b:"ring_of (poly A) = poly_ring (ring_of A)"
by (subst ring_of_poly) auto
have c:"domain (ring_of (poly A))"
unfolding b by (rule univ_poly_is_domain[OF carrier_is_subring])
interpret d: domain "poly_ring (ring_of A)"
using c unfolding b by simp
have "-⇩C⇘poly A⇙ x = ⊖⇘ring_of (poly A)⇙ x" if "x ∈ carrier (ring_of (poly A))" for x
proof -
have "⊖⇘ring_of (poly A)⇙ x = map (a_inv (ring_of A)) x"
using that unfolding b by (subst univ_poly_a_inv_def'[OF carrier_is_subring]) auto
also have "... = map (λr. -⇩C⇘A⇙ r) x"
using that unfolding b univ_poly_carrier[symmetric] polynomial_def
by (intro map_cong refl a) auto
also have "... = -⇩C⇘poly A⇙ x"
unfolding poly_def by simp
finally show ?thesis by simp
qed
moreover have "x ¯⇩C⇘poly A⇙ = inv⇘ring_of (poly A)⇙ x" if "x ∈ Units (ring_of (poly A))" for x
proof -
have "x ∈ {[k] |k. k ∈ carrier (ring_of A) - {𝟬⇘ring_of A⇙}}"
using that univ_poly_carrier_units_incl unfolding b by auto
then obtain k where x_eq: "k ∈ carrier (ring_of A) - {𝟬⇘ring_of A⇙}" "x = [k]" by auto
have "inv⇘ring_of (poly A)⇙ x ∈ Units (poly_ring (ring_of A))"
using that unfolding b by simp
hence "inv⇘ring_of (poly A)⇙ x ∈ {[k] |k. k ∈ carrier (ring_of A) - {𝟬⇘ring_of A⇙}}"
using that univ_poly_carrier_units_incl unfolding b by auto
then obtain v where x_inv_eq: "v∈ carrier (ring_of A) - {𝟬⇘ring_of A⇙}"
"inv⇘ring_of (poly A)⇙ x = [v]" by auto
have "poly_mult [k] [v] = [k] ⊗⇘ring_of (poly A)⇙ [v]" unfolding b univ_poly_mult by simp
also have "... = x ⊗⇘ring_of (poly A)⇙ inv⇘ring_of (poly A)⇙ x" using x_inv_eq x_eq by auto
also have "... = 𝟭⇘ring_of (poly A)⇙" using that unfolding b by simp
also have "... = [𝟭⇘ring_of A⇙]" unfolding b univ_poly_one by (simp add:ring_of_def)
finally have "poly_mult [k] [v] = [𝟭⇘ring_of A⇙]" by simp
hence "k ⊗⇘ring_of A⇙ v ⊕⇘ring_of A⇙ 𝟬⇘ring_of A⇙ = 𝟭⇘ring_of A⇙"
by (simp add:if_distribR if_distrib) (simp cong:if_cong, metis)
hence e: "k ⊗⇘ring_of A⇙ v = 𝟭⇘ring_of A⇙" using x_eq(1) x_inv_eq(1) by simp
hence f: "v ⊗⇘ring_of A⇙ k = 𝟭⇘ring_of A⇙" using x_eq(1) x_inv_eq(1) m_comm by simp
have g: "v = inv⇘ring_of A⇙ k"
using e x_eq(1) x_inv_eq(1) by (intro comm_inv_char[symmetric]) auto
hence h: "k ∈ Units (ring_of A)" unfolding Units_def using e f x_eq(1) x_inv_eq(1) by blast
have "x ¯⇩C⇘poly A⇙ = [k] ¯⇩C⇘poly A⇙" unfolding x_eq by simp
also have "... = [k ¯⇩C⇘A⇙]" unfolding poly_def by simp
also have "... = [v]"
unfolding g by (intro domain_cD[OF assms(1)] arg_cong2[where f="(#)"] h refl)
also have "... = inv⇘ring_of (poly A)⇙ x" unfolding x_inv_eq by simp
finally show ?thesis by simp
qed
ultimately show ?thesis using c by (intro domain_cI)
qed
function long_division⇩C :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ 'a list × 'a list"
where "long_division⇩C F f g = (
if (length g = 0 ∨ length f < length g)
then ([], f)
else (
let k = length f - length g;
α = -⇩C⇘F⇙ (hd f *⇩C⇘F⇙ (hd g) ¯⇩C⇘F⇙);
h = [α] *⇩C⇘poly F⇙ X⇩C⇘F⇙ ^⇩C⇘poly F⇙ k;
f' = f +⇩C⇘poly F⇙ (h *⇩C⇘poly F⇙ g);
f'' = take (length f - 1) f'
in apfst (λx. x +⇩C⇘poly F⇙ -⇩C⇘poly F⇙ h) (long_division⇩C F f'' g)))"
by pat_completeness auto
lemma pmod_termination_helper:
"g ≠ [] ⟹ ¬length f < length g ⟹ min x (length f - 1) < length f"
by (metis diff_less length_greater_0_conv list.size(3) min.strict_coboundedI2 zero_less_one)
termination by (relation "measure (λ(_, f, _). length f)") (use pmod_termination_helper in auto)
declare long_division⇩C.simps[simp del]
lemma long_division_c_length:
assumes "length g > 0"
shows "length (snd (long_division⇩C R f g)) < length g"
proof (induction "length f" arbitrary:f rule:nat_less_induct)
case 1
have 0:"length (snd (long_division⇩C R x g)) < length g"
if "length x < length f" for x using 1 that by blast
show "length (snd (long_division⇩C R f g)) < length g"
proof (cases "length f < length g")
case True then show ?thesis by (subst long_division⇩C.simps) simp
next
case False
hence "length f > 0" using assms by auto
thus ?thesis using assms by (subst long_division⇩C.simps)
(auto intro!:0 simp: min.commute min.strict_coboundedI1 Let_def)
qed
qed
context field
begin
interpretation r:polynomial_ring R "(carrier R)"
unfolding polynomial_ring_def polynomial_ring_axioms_def
using carrier_is_subfield field_axioms by force
lemma poly_length_from_coeff:
assumes "p ∈ carrier (poly_ring R)"
assumes "⋀i. i ≥ k ⟹ coeff p i = 𝟬"
shows "length p ≤ k"
proof (rule ccontr)
assume a:"¬length p ≤ k"
hence p_nz: "p ≠ []" by auto
have "k < length p" using a by simp
hence "k ≤ length p - 1" by simp
hence "𝟬 = coeff p (degree p)" by (intro assms(2)[symmetric])
also have "... = lead_coeff p" by (intro lead_coeff_simp[OF p_nz])
finally have "𝟬 = lead_coeff p" by simp
thus "False"
using p_nz assms(1) unfolding univ_poly_def polynomial_def by simp
qed
lemma poly_add_cancel_len:
assumes "f ∈ carrier (poly_ring R) - {𝟬⇘poly_ring R⇙}"
assumes "g ∈ carrier (poly_ring R) - {𝟬⇘poly_ring R⇙}"
assumes "hd f = ⊖ hd g" "degree f = degree g"
shows "length (f ⊕⇘poly_ring R⇙ g) < length f"
proof -
have f_ne: "f ≠ []" using assms(1) unfolding univ_poly_zero by simp
have g_ne: "g ≠ []" using assms(2) unfolding univ_poly_zero by simp
have "coeff f i = ⊖coeff g i" if "i ≥ degree f" for i
proof (cases "i = degree f")
case True
have "coeff f i = hd f" unfolding True by (subst lead_coeff_simp[OF f_ne]) simp
also have "... = ⊖hd g" using assms(3) by simp
also have "... = ⊖coeff g i" unfolding True assms(4) by (subst lead_coeff_simp[OF g_ne]) simp
finally show ?thesis by simp
next
case False
hence "i > degree f" "i > degree g" using assms(4) that by auto
thus "coeff f i = ⊖ coeff g i" using coeff_degree by simp
qed
hence "coeff (f ⊕⇘poly_ring R⇙ g) i = 𝟬" if "i ≥ degree f" for i
using assms(1,2) that by (subst r.coeff_add) (auto intro:l_neg simp: r.coeff_range)
hence "length (f ⊕⇘poly_ring R⇙ g) ≤ length f - 1"
using assms(1,2) by (intro poly_length_from_coeff) auto
also have "... < length f" using f_ne by simp
finally show ?thesis by simp
qed
lemma pmod_mult_left:
assumes "f ∈ carrier (poly_ring R)"
assumes "g ∈ carrier (poly_ring R)"
assumes "h ∈ carrier (poly_ring R)"
shows "(f ⊗⇘poly_ring R⇙ g) pmod h = ((f pmod h) ⊗⇘poly_ring R⇙ g) pmod h" (is "?L = ?R")
proof -
have "h pdivides (h ⊗⇘poly_ring R⇙ (f pdiv h)) ⊗⇘poly_ring R⇙ g"
using assms long_division_closed[OF carrier_is_subfield]
by (simp add: dividesI' pdivides_def r.p.m_assoc)
hence 0:"(h ⊗⇘poly_ring R⇙ (f pdiv h)) ⊗⇘poly_ring R⇙ g pmod h = 𝟬⇘poly_ring R⇙"
using pmod_zero_iff_pdivides[OF carrier_is_subfield] assms
long_division_closed[OF carrier_is_subfield] univ_poly_zero
by (metis (no_types, opaque_lifting) r.p.m_closed)
have "?L = (h ⊗⇘poly_ring R⇙ (f pdiv h) ⊕⇘poly_ring R⇙ (f pmod h)) ⊗⇘poly_ring R⇙ g pmod h"
using assms by (intro arg_cong2[where f="(⊗⇘poly_ring R⇙)"] arg_cong2[where f="(pmod)"]
pdiv_pmod[OF carrier_is_subfield]) auto
also have "... = ((h ⊗⇘poly_ring R⇙ (f pdiv h)) ⊗⇘poly_ring R⇙ g ⊕⇘poly_ring R⇙
(f pmod h) ⊗⇘poly_ring R⇙ g) pmod h"
using assms long_division_closed[OF carrier_is_subfield]
by (intro r.p.l_distr arg_cong2[where f="(pmod)"]) auto
also have "... = ((h ⊗⇘poly_ring R⇙ (f pdiv h)) ⊗⇘poly_ring R⇙ g) pmod h ⊕⇘poly_ring R⇙
((f pmod h) ⊗⇘poly_ring R⇙ g pmod h)"
using assms long_division_closed[OF carrier_is_subfield]
by (intro long_division_add[OF carrier_is_subfield]) auto
also have "... = ?R"
using assms long_division_closed[OF carrier_is_subfield] unfolding 0 by auto
finally show ?thesis
by simp
qed
lemma pmod_mult_right:
assumes "f ∈ carrier (poly_ring R)"
assumes "g ∈ carrier (poly_ring R)"
assumes "h ∈ carrier (poly_ring R)"
shows "(f ⊗⇘poly_ring R⇙ g) pmod h = (f ⊗⇘poly_ring R⇙ (g pmod h)) pmod h" (is "?L = ?R")
proof -
have "?L = (g ⊗⇘poly_ring R⇙ f) pmod h" using assms by algebra
also have "... = ((g pmod h) ⊗⇘poly_ring R⇙ f) pmod h" by (intro pmod_mult_left assms)
also have "... = ?R" using assms long_division_closed[OF carrier_is_subfield] by algebra
finally show ?thesis by simp
qed
lemma pmod_mult_both:
assumes "f ∈ carrier (poly_ring R)"
assumes "g ∈ carrier (poly_ring R)"
assumes "h ∈ carrier (poly_ring R)"
shows "(f ⊗⇘poly_ring R⇙ g) pmod h = ((f pmod h) ⊗⇘poly_ring R⇙ (g pmod h)) pmod h"
(is "?L = ?R")
proof -
have "(f ⊗⇘poly_ring R⇙ g) pmod h = ((f pmod h) ⊗⇘poly_ring R⇙ g) pmod h"
by (intro pmod_mult_left assms)
also have "... = ?R"
using assms long_division_closed[OF carrier_is_subfield] by (intro pmod_mult_right) auto
finally show ?thesis by simp
qed
lemma field_Unit_minus_closed:
assumes "x ∈ Units R"
shows "⊖ x ∈ Units R"
using assms mult_of.Units_eq by auto
end
lemma long_division_c:
assumes "field⇩C R"
assumes "f ∈ carrier (poly_ring (ring_of R))"
assumes "g ∈ carrier (poly_ring (ring_of R))"
shows "long_division⇩C R f g = (ring.pdiv (ring_of R) f g, ring.pmod (ring_of R) f g)"
proof -
let ?P = "poly_ring (ring_of R)"
let ?result = "(λf r. f = snd r ⊕⇘poly_ring (ring_of R)⇙ (fst r ⊗⇘poly_ring (ring_of R)⇙ g))"
define r where "r = long_division⇩C R f g"
interpret field "ring_of R" using assms(1) unfolding field⇩C_def by auto
interpret d_poly_ring: domain "poly_ring (ring_of R)"
by (rule univ_poly_is_domain[OF carrier_is_subring])
have ring_c: "ring⇩C R" using assms(1) unfolding field⇩C_def domain⇩C_def cring⇩C_def by auto
have d_poly: "domain⇩C (poly R)" using assms (1) unfolding field⇩C_def by (intro poly_domain) auto
have "r = long_division⇩C R f g ⟹ ?result f r ∧ {fst r, snd r} ⊆ carrier (poly_ring (ring_of R))"
using assms(2)
proof (induction "length f" arbitrary: f r rule:nat_less_induct)
case 1
have ind: "x = snd q ⊕⇘?P⇙ fst q ⊗⇘?P⇙ g" "{fst q, snd q} ⊆ carrier (poly_ring (ring_of R))"
if "length x < length f " "q = long_division⇩C R x g" "x ∈ carrier (poly_ring (ring_of R)) "
for x q using 1(1) that by auto
show ?case
proof (cases "length g = 0 ∨ length f < length g")
case True
hence "r = (𝟬⇘poly_ring (ring_of R)⇙, f)"
unfolding 1(2) univ_poly_zero by (subst long_division⇩C.simps) simp
then show ?thesis using assms(3) 1(3) by simp
next
case False
hence "length g > 0" "length f ≥ length g" by auto
hence "f ≠ []" "g ≠ []" by auto
hence f_carr: "f ∈ carrier ?P - {𝟬⇘?P⇙}" and g_carr: "g ∈ carrier ?P - {𝟬⇘?P⇙}"
using 1(3) assms(3) univ_poly_zero by auto
define k where "k = length f - length g"
define α where "α = -⇩C⇘R⇙ (hd f *⇩C⇘R⇙ (hd g) ¯⇩C⇘R⇙)"
define h where "h = [α] *⇩C⇘poly R⇙ X⇩C⇘R⇙ ^⇩C⇘poly R⇙ k"
define f' where "f' = f +⇩C⇘poly R⇙ (h *⇩C⇘poly R⇙ g)"
define f'' where "f'' = take (length f - 1) f'"
obtain s t where st_def: "(s,t) = long_division⇩C R f'' g" by (metis surj_pair)
have "r = apfst (λx. x +⇩C⇘poly R⇙ -⇩C⇘poly R⇙ h) (long_division⇩C R f'' g)"
using False unfolding 1(2)
by (subst long_division⇩C.simps) (simp add:Let_def f''_def f'_def h_def α_def k_def)
hence r_def: "r = (s +⇩C⇘poly R⇙ -⇩C⇘poly R⇙ h, t)"
unfolding st_def[symmetric] by simp
have "monic_poly (ring_of R) (X⇘ring_of R⇙ [^]⇘poly_ring (ring_of R)⇙ k)"
by (intro monic_poly_pow monic_poly_var)
hence [simp]: "lead_coeff (X⇘ring_of R⇙ [^]⇘poly_ring (ring_of R)⇙ k) = 𝟭⇘ring_of R⇙"
unfolding monic_poly_def by simp
have hd_f_unit: "hd f ∈ Units (ring_of R)" and hd_g_unit: "hd g ∈ Units (ring_of R)"
using f_carr g_carr lead_coeff_carr field_Units by auto
hence hd_f_carr: "hd f ∈ carrier (ring_of R)" and hd_g_carr: "hd g ∈ carrier (ring_of R)"
by auto
have k_def': "k = degree f - degree g" using False unfolding k_def by auto
have α_def': "α = ⊖⇘ring_of R⇙ (hd f ⊗⇘ring_of R⇙ inv⇘ring_of R⇙ hd g)"
unfolding α_def using hd_g_unit hd_f_carr field_cD[OF assms(1)] by simp
have α_unit: "α ∈ Units (ring_of R)" unfolding α_def' using hd_f_unit hd_g_unit
by (intro field_Unit_minus_closed) simp
hence α_carr: "α ∈ carrier (ring_of R) - {𝟬⇘ring_of R⇙}" unfolding field_Units by simp
hence α_poly_carr: "[α] ∈ carrier (poly_ring (ring_of R)) - {𝟬⇘poly_ring (ring_of R)⇙}"
by (simp add: univ_poly_carrier[symmetric] univ_poly_zero polynomial_def)
have h_def': "h = [α] ⊗⇘?P⇙ X⇘ring_of R⇙ [^]⇘?P⇙ k"
unfolding h_def poly_var domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])
have f'_def': "f' = f ⊕⇘?P⇙ (h ⊗⇘?P⇙ g)"
unfolding f'_def domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])
have h_carr: "h ∈ carrier (poly_ring (ring_of R)) - {𝟬⇘poly_ring (ring_of R)⇙}"
using d_poly_ring.mult_of.m_closed α_poly_carr var_pow_carr[OF carrier_is_subring]
unfolding h_def' by auto
have "degree f = k + degree g" using False unfolding k_def by linarith
also have "... = degree [α] + degree (X⇘ring_of R⇙ [^]⇘?P⇙ k) + degree g"
unfolding var_pow_degree[OF carrier_is_subring] by simp
also have "... = degree h + degree g" unfolding h_def'
by (intro arg_cong2[where f="(+)"] degree_mult[symmetric]
carrier_is_subring α_poly_carr var_pow_carr refl)
also have "... = degree (h ⊗⇘poly_ring (ring_of R)⇙ g)"
by (intro degree_mult[symmetric] carrier_is_subring h_carr g_carr)
finally have deg_f: "degree f = degree (h ⊗⇘poly_ring (ring_of R)⇙ g)" by simp
have f'_carr: "f' ∈ carrier (poly_ring (ring_of R))"
using f_carr h_carr g_carr unfolding f'_def' by auto
have "hd f = ⊖⇘ring_of R⇙ (α ⊗⇘ring_of R⇙ lead_coeff g)"
using hd_g_unit hd_f_carr hd_g_carr α_unit α_carr unfolding α_def'
by (simp add: m_assoc l_minus)
also have "... = ⊖⇘ring_of R⇙ (hd h ⊗⇘ring_of R⇙ hd g)"
using hd_f_carr α_carr α_poly_carr var_pow_carr[OF carrier_is_subring] unfolding h_def'
by (subst lead_coeff_mult) (simp_all add:algebra_simps)
also have "... = ⊖⇘ring_of R⇙ hd (h ⊗⇘poly_ring (ring_of R)⇙ g)"
using h_carr g_carr by (subst lead_coeff_mult) auto
finally have "hd f = ⊖⇘ring_of R⇙ hd (h ⊗⇘poly_ring (ring_of R)⇙ g)"
by simp
hence len_f': "length f' < length f" using deg_f h_carr g_carr d_poly_ring.integral
unfolding f'_def' by (intro poly_add_cancel_len f_carr) auto
hence f''_def': "f'' = f'" unfolding f''_def by simp
have "{fst (s,t),snd (s,t)} ⊆ carrier (poly_ring (ring_of R))"
using len_f' f''_def' f'_carr by (intro ind(2)[where x="f''"] st_def) auto
hence s_carr: "s ∈ carrier ?P" and t_carr: "t ∈ carrier ?P" by auto
have r_def': "r = (s ⊖⇘poly_ring (ring_of R)⇙ h, t)"
using h_carr domain_cD[OF d_poly] unfolding r_def a_minus_def
using ring_of_poly[OF ring_c,symmetric] by simp
have r_carr: "{fst r, snd r} ⊆ carrier (poly_ring (ring_of R))"
using s_carr t_carr h_carr unfolding r_def' by auto
have "f = f'' ⊖⇘?P⇙ h ⊗⇘?P⇙ g"
using h_carr g_carr f_carr unfolding f''_def' f'_def' by simp algebra
also have "... = (snd (s,t) ⊕⇘?P⇙ fst (s,t) ⊗⇘?P⇙ g) ⊖⇘?P⇙ h ⊗⇘?P⇙ g"
using f'_carr f''_def' len_f'
by (intro arg_cong2[where f="λx y. x ⊖⇘?P⇙ y"] ind(1) st_def) auto
also have "... = t ⊕⇘?P⇙ (s ⊖⇘?P⇙ h) ⊗⇘?P⇙ g"
using s_carr t_carr h_carr g_carr by simp algebra
also have "... = snd r ⊕⇘poly_ring (ring_of R)⇙ fst r ⊗⇘poly_ring (ring_of R)⇙ g"
unfolding r_def' by simp
finally have "f = snd r ⊕⇘poly_ring (ring_of R)⇙ fst r ⊗⇘poly_ring (ring_of R)⇙ g" by simp
thus ?thesis using r_carr by auto
qed
qed
hence result: "?result f r" "{fst r, snd r} ⊆ carrier (poly_ring (ring_of R))"
using r_def by auto
show ?thesis
proof (cases "g = []")
case True then show ?thesis by (simp add:long_division⇩C.simps pmod_def pdiv_def)
next
case False
hence "snd r = [] ∨ degree (snd r) < degree g"
using long_division_c_length unfolding r_def
by (metis One_nat_def Suc_pred length_greater_0_conv not_less_eq)
moreover have "f = g ⊗⇘?P⇙ (fst r) ⊕⇘poly_ring (ring_of R)⇙ (snd r)"
using result(1,2) assms(2,3) by simp algebra
ultimately have "long_divides f g (fst r, snd r)"
using result(2) unfolding long_divides_def by (auto simp:mem_Times_iff)
hence "(fst r, snd r) = (pdiv f g, pmod f g)"
by (intro long_divisionI[OF carrier_is_subfield] False assms)
then show ?thesis unfolding r_def by simp
qed
qed
definition pdiv⇩C :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"pdiv⇩C R f g = fst (long_division⇩C R f g)"
lemma pdiv_c:
assumes "field⇩C R"
assumes "f ∈ carrier (poly_ring (ring_of R))"
assumes "g ∈ carrier (poly_ring (ring_of R))"
shows "pdiv⇩C R f g = ring.pdiv (ring_of R) f g"
unfolding pdiv⇩C_def long_division_c[OF assms] by simp
definition pmod⇩C :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"pmod⇩C R f g = snd (long_division⇩C R f g)"
lemma pmod_c:
assumes "field⇩C R"
assumes "f ∈ carrier (poly_ring (ring_of R))"
assumes "g ∈ carrier (poly_ring (ring_of R))"
shows "pmod⇩C R f g = ring.pmod (ring_of R) f g"
unfolding pmod⇩C_def long_division_c[OF assms] by simp
function ext_euclidean ::
"('a,'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ ('a list × 'a list) × 'a list"
where "ext_euclidean F f g = (
if f = [] ∨ g = [] then
((1⇩C⇘poly F⇙, 1⇩C⇘poly F⇙),f +⇩C⇘poly F⇙ g)
else (
let (p,q) = long_division⇩C F f g;
((u,v),r) = ext_euclidean F g q
in ((v,u +⇩C⇘poly F⇙ (-⇩C⇘poly F⇙ (p *⇩C⇘poly F⇙ v))),r)))"
by pat_completeness auto
termination
apply (relation "measure (λ(_, _, f). length f)")
subgoal by simp
by (metis case_prod_conv in_measure length_greater_0_conv long_division_c_length prod.sel(2))
lemma (in domain) pdivides_self:
assumes "x ∈ carrier (poly_ring R)"
shows "x pdivides x"
proof -
interpret d:domain "poly_ring R" by (rule univ_poly_is_domain[OF carrier_is_subring])
show ?thesis
using assms unfolding pdivides_def
by (intro dividesI[where c="𝟭⇘poly_ring R⇙"]) simp_all
qed
declare ext_euclidean.simps[simp del]
lemma ext_euclidean:
assumes "field⇩C R"
defines "P ≡ poly_ring (ring_of R)"
assumes "f ∈ carrier (poly_ring (ring_of R))"
assumes "g ∈ carrier (poly_ring (ring_of R))"
defines "r ≡ ext_euclidean R f g"
shows "snd r = f ⊗⇘P⇙ (fst (fst r)) ⊕⇘P⇙ g ⊗⇘P⇙ (snd (fst r))" (is "?T1")
and "snd r pdivides⇘ring_of R⇙ f" (is "?T2") "snd r pdivides⇘ring_of R⇙ g" (is "?T3")
and "{snd r, fst (fst r), snd (fst r)} ⊆ carrier P" (is "?T4")
and "snd r = [] ⟶ f = [] ∧ g = []" (is "?T5")
proof -
let ?P= "poly_ring (ring_of R)"
interpret field "ring_of R" using assms(1) unfolding field⇩C_def by auto
interpret d_poly_ring: domain "poly_ring (ring_of R)"
by (rule univ_poly_is_domain[OF carrier_is_subring])
have ring_c: "ring⇩C R" using assms(1) unfolding field⇩C_def domain⇩C_def cring⇩C_def by auto
have d_poly: "domain⇩C (poly R)" using assms (1) unfolding field⇩C_def by (intro poly_domain) auto
have pdiv_zero: "x pdivides⇘ring_of R⇙ 𝟬⇘?P⇙" if "x ∈ carrier ?P" for x
using that unfolding univ_poly_zero by (intro pdivides_zero[OF carrier_is_subring])
have "snd r = f ⊗⇘?P⇙ (fst (fst r)) ⊕⇘?P⇙ g ⊗⇘?P⇙ (snd (fst r)) ∧
snd r pdivides⇘ring_of R⇙ f ∧ snd r pdivides⇘ring_of R⇙ g ∧
{snd r, fst (fst r), snd (fst r)} ⊆ carrier ?P ∧
(snd r = [] ⟶ f = [] ∧ g = [])"
if "r = ext_euclidean R f g" "{f,g} ⊆ carrier ?P"
using that
proof (induction "length g" arbitrary: f g r rule:nat_less_induct)
case 1
have ind:
"snd s = x ⊗⇘?P⇙ fst (fst s) ⊕⇘?P⇙ y ⊗⇘?P⇙ snd (fst s)"
"snd s pdivides⇘ring_of R⇙ x" "snd s pdivides⇘ring_of R⇙ y"
"{snd s, fst (fst s), snd (fst s)} ⊆ carrier ?P"
"(snd s = [] ⟶ x = [] ∧ y = [])"
if "length y < length g" "s = ext_euclidean R x y" "{x, y} ⊆ carrier ?P"
for x y s using that 1(1) by metis+
show ?case
proof (cases "f = [] ∨ g = []")
case True
hence r_def: "r = ((𝟭⇘?P⇙, 𝟭⇘?P⇙), f ⊕⇘?P⇙ g)" unfolding 1(2)
by (simp add:ext_euclidean.simps domain_cD[OF d_poly] ring_of_poly[OF ring_c])
consider "f = 𝟬⇘?P⇙" | "g = 𝟬⇘?P⇙"
using True unfolding univ_poly_zero by auto
hence "snd r pdivides⇘ring_of R⇙ f ∧ snd r pdivides⇘ring_of R⇙ g"
using 1(3) pdiv_zero pdivides_self unfolding r_def by cases auto
moreover have "snd r = f ⊗⇘?P⇙ fst (fst r) ⊕⇘?P⇙ g ⊗⇘?P⇙ snd (fst r)"
using 1(3) unfolding r_def by simp
moreover have "{snd r, fst (fst r), snd (fst r)} ⊆ carrier ?P"
using 1(3) unfolding r_def by auto
moreover have "snd r = [] ⟶ f = [] ∧ g = []"
using 1(3) True unfolding r_def by (auto simp:univ_poly_zero)
ultimately show ?thesis by (intro conjI) metis+
next
case False
obtain p q where pq_def: "(p,q) = long_division⇩C R f g"
by (metis surj_pair)
obtain u v s where uvs_def: "((u,v),s) = ext_euclidean R g q"
by (metis surj_pair)
have "(p,q) = (pdiv f g, pmod f g)"
using 1(3) unfolding pq_def by (intro long_division_c[OF assms(1)]) auto
hence p_def: "p = pdiv f g" and q_def: "q = pmod f g" by auto
have p_carr: "p ∈ carrier ?P" and q_carr: "q ∈ carrier ?P"
using 1(3) long_division_closed[OF carrier_is_subfield] unfolding p_def q_def by auto
have "length g > 0" using False by auto
hence len_q: "length q < length g" using long_division_c_length pq_def by (metis snd_conv)
have s_eq: "s = g ⊗⇘?P⇙ u ⊕⇘?P⇙ q ⊗⇘?P⇙ v"
and s_div_g: "s pdivides⇘ring_of R⇙ g"
and s_div_q: "s pdivides⇘ring_of R⇙ q"
and suv_carr: "{s,u,v} ⊆ carrier ?P"
and s_zero_iff: "s = [] ⟶ g = [] ∧ q = []"
using ind[OF len_q uvs_def _] q_carr 1(3) by auto
have "r = ((v,u +⇩C⇘poly R⇙ (-⇩C⇘poly R⇙ (p *⇩C⇘poly R⇙ v))),s)" unfolding 1(2) using False
by (subst ext_euclidean.simps) (simp add: pq_def[symmetric] uvs_def[symmetric])
also have "... = ((v, u ⊖⇘?P⇙ (p ⊗⇘?P⇙ v)), s)" using p_carr suv_carr domain_cD[OF d_poly]
unfolding a_minus_def ring_of_poly[OF ring_c] by (intro arg_cong2[where f="Pair"] refl) simp
finally have r_def: "r = ((v, u ⊖⇘?P⇙ (p ⊗⇘?P⇙ v)), s)" by simp
have "snd r = g ⊗⇘?P⇙ u ⊕⇘?P⇙ q ⊗⇘?P⇙ v" unfolding r_def s_eq by simp
also have "... = g ⊗⇘?P⇙ u ⊕⇘?P⇙ (f ⊖⇘?P⇙ g ⊗⇘?P⇙ p) ⊗⇘?P⇙ v"
using 1(3) p_carr q_carr suv_carr
by (subst pdiv_pmod[OF carrier_is_subfield, of "f" "g"])
(simp_all add:p_def[symmetric] q_def[symmetric], algebra)
also have "... = f ⊗⇘?P⇙ v ⊕⇘?P⇙ g ⊗⇘?P⇙ (u ⊖⇘?P⇙ ((p ⊗⇘?P⇙ v)))"
using 1(3) p_carr q_carr suv_carr by simp algebra
finally have r1: "snd r = f ⊗⇘?P⇙ fst (fst r) ⊕⇘?P⇙ g ⊗⇘?P⇙ snd (fst r)"
unfolding r_def by simp
have "pmod f s = pmod (g ⊗⇘?P⇙ p ⊕⇘?P⇙ q) s" using 1(3)
by (subst pdiv_pmod[OF carrier_is_subfield, of "f" "g"])
(simp_all add:p_def[symmetric] q_def[symmetric])
also have "... = pmod (g ⊗⇘?P⇙ p) s ⊕⇘?P⇙ pmod q s"
using 1(3) p_carr q_carr suv_carr
by (subst long_division_add[OF carrier_is_subfield]) simp_all
also have "... = pmod (pmod g s ⊗⇘?P⇙ p) s ⊕⇘?P⇙ []"
using 1(3) p_carr q_carr suv_carr s_div_q
by (intro arg_cong2[where f="(⊕⇘?P⇙)"] pmod_mult_left)
(simp_all add: pmod_zero_iff_pdivides[OF carrier_is_subfield])
also have "... = pmod (𝟬⇘?P⇙ ⊗⇘?P⇙ p) s ⊕⇘?P⇙ 𝟬⇘?P⇙" unfolding univ_poly_zero
using 1(3) p_carr q_carr suv_carr s_div_g by (intro arg_cong2[where f="(⊕⇘?P⇙)"]
arg_cong2[where f="(⊗⇘?P⇙)"] arg_cong2[where f="pmod"])
(simp_all add: pmod_zero_iff_pdivides[OF carrier_is_subfield])
also have "... = pmod 𝟬⇘?P⇙ s"
using p_carr suv_carr long_division_closed[OF carrier_is_subfield] by simp
also have "... = []" unfolding univ_poly_zero
using suv_carr long_division_zero(2)[OF carrier_is_subfield] by simp
finally have "pmod f s = []" by simp
hence r2: "snd r pdivides⇘ring_of R⇙ f" using suv_carr 1(3) unfolding r_def
by (subst pmod_zero_iff_pdivides[OF carrier_is_subfield,symmetric]) simp_all
have r3: "snd r pdivides⇘ring_of R⇙ g" unfolding r_def using s_div_g by auto
have r4: "{snd r, fst (fst r), snd (fst r)} ⊆ carrier ?P"
using suv_carr p_carr unfolding r_def by simp_all
have r5: "f = [] ∧ g = []" if "snd r = []"
proof -
have r5_a: "g = [] ∧ q = []" using that s_zero_iff unfolding r_def by simp
hence "pmod f [] = []" unfolding q_def by auto
hence "f = []" using pmod_def by simp
thus ?thesis using r5_a by auto
qed
show ?thesis using r1 r2 r3 r4 r5 by (intro conjI) metis+
qed
qed
thus ?T1 ?T2 ?T3 ?T4 ?T5 using assms by auto
qed
end