# Theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials

section ‹Bounded Degree Polynomials›

text ‹This section contains a definition for the set of polynomials with a degree bound and
establishes its cardinality.›

theory Bounded_Degree_Polynomials
imports "HOL-Algebra.Polynomial_Divisibility"
begin

lemma (in ring) coeff_in_carrier: "p ∈ carrier (poly_ring R) ⟹ coeff p i ∈ carrier R"
using poly_coeff_in_carrier carrier_is_subring by (simp add: univ_poly_carrier)

definition bounded_degree_polynomials
where "bounded_degree_polynomials F n = {x. x ∈ carrier (poly_ring F) ∧ (degree x < n ∨ x = [])}"

text ‹Note: The definition for @{term "bounded_degree_polynomials"} includes the zero polynomial
in @{term "bounded_degree_polynomials F 0"}. The reason for this adjustment is that, contrary to
definition in HOL Algebra, most authors set the degree of the zero polynomial to
$-\infty$~\<^cite>‹‹\textsection 7.2.2› in "shoup2009computational"›. That
definition make some identities, such as $\mathrm{deg}(f g) = \mathrm{deg}\, f + \mathrm{deg}\, g$
for polynomials $f$ and $g$ unconditionally true.
In particular, it prevents an unnecessary corner case in the statement of the results established
in this entry.›

lemma bounded_degree_polynomials_length:
"bounded_degree_polynomials F n = {x. x ∈ carrier (poly_ring F) ∧ length x ≤ n}"
unfolding bounded_degree_polynomials_def using leI order_less_le_trans by fastforce

lemma (in ring) fin_degree_bounded:
assumes "finite (carrier R)"
shows "finite (bounded_degree_polynomials R n)"
proof -
have "bounded_degree_polynomials R n ⊆ {p. set p ⊆ carrier R ∧ length p ≤ n}"
unfolding bounded_degree_polynomials_length
using assms polynomial_incl univ_poly_carrier by blast
thus ?thesis
using assms finite_lists_length_le finite_subset by fast
qed

lemma (in ring) non_empty_bounded_degree_polynomials:
"bounded_degree_polynomials R k ≠ {}"
proof -
have "𝟬⇘poly_ring R⇙ ∈ bounded_degree_polynomials R k"
by (simp add: bounded_degree_polynomials_def univ_poly_zero univ_poly_zero_closed)
thus ?thesis by auto
qed

lemma in_image_by_witness:
assumes "⋀x. x ∈ A ⟹ g x ∈ B ∧ f (g x) = x"
shows "A ⊆ f  B"
by (metis assms image_eqI subsetI)

lemma card_mostly_constant_maps:
assumes "y ∈ B"
shows "card {f. range f ⊆ B ∧ (∀x. x ≥ n ⟶ f x = y)} = card B ^ n" (is "card ?A = ?B")
proof -
define f where "f = (λf k. if k < n then f k else y)"

have a:"?A ⊆ (f  ({0..<n}  →⇩E B))"
unfolding f_def
by (rule in_image_by_witness[where g="λf. restrict f {0..<n}"], auto)

have b:"(f  ({0..<n}  →⇩E B)) ⊆ ?A"
using f_def assms by auto

have c: "inj_on f ({0..<n} →⇩E B)"
by (rule inj_onI, metis PiE_E atLeastLessThan_iff ext f_def)

have "card ?A = card (f  ({0..<n}  →⇩E B))"
using a b by auto
also have "... = card ({0..<n} →⇩E B)"
by (metis c card_image)
also have "... = card B ^ n"
finally show ?thesis by simp
qed

definition (in ring) build_poly where
"build_poly f n = normalize (rev (map f [0..<n]))"

lemma (in ring) poly_degree_bound_from_coeff:
assumes "x ∈ carrier (poly_ring R)"
assumes "⋀k. k ≥ n ⟹ coeff x k = 𝟬"
shows "degree x < n ∨ x = 𝟬⇘poly_ring R⇙"
proof (rule ccontr)
assume a:"¬(degree x < n ∨ x = 𝟬⇘poly_ring R⇙)"
by (metis assms(1) polynomial_def univ_poly_carrier univ_poly_zero)
hence "coeff x (degree x) ≠ 𝟬"
moreover have "degree x ≥ n" by (meson a not_le)
ultimately show "False" using assms(2) by blast
qed

lemma (in ring) poly_degree_bound_from_coeff_1:
assumes "x ∈ carrier (poly_ring R)"
assumes "⋀k. k ≥ n ⟹ coeff x k = 𝟬"
shows "x ∈ bounded_degree_polynomials R n"
using poly_degree_bound_from_coeff[OF assms]

lemma (in ring) length_build_poly:
"length (build_poly f n) ≤ n"
by (metis length_map build_poly_def normalize_length_le length_rev length_upt
less_imp_diff_less linorder_not_less)

lemma (in ring) build_poly_degree:
"degree (build_poly f n) ≤ n-1"
using length_build_poly diff_le_mono by presburger

lemma (in ring) build_poly_poly:
assumes "⋀i. i < n ⟹ f i ∈ carrier R"
shows "build_poly f n ∈ carrier (poly_ring R)"
unfolding build_poly_def univ_poly_carrier[symmetric]
by (rule normalize_gives_polynomial, simp add:image_subset_iff Ball_def assms)

lemma (in ring) build_poly_coeff:
"coeff (build_poly f n) i = (if i < n then f i else 𝟬)"
proof -
show "coeff (build_poly f n) i = (if i < n then f i else 𝟬)"
unfolding build_poly_def normalize_coeff[symmetric]
by (cases "i < n", (simp add:coeff_nth rev_nth coeff_length)+)
qed

lemma (in ring) build_poly_bounded:
assumes "⋀k. k < n ⟹ f k ∈ carrier R"
shows "build_poly f n ∈ bounded_degree_polynomials R n"
unfolding bounded_degree_polynomials_length
using build_poly_poly[OF assms] length_build_poly by auto

text ‹The following establishes the total number of polynomials with a degree less than $n$.
Unlike the results in the following sections, it is already possible to establish this property for
polynomials with coefficients in a ring.›

lemma (in ring) bounded_degree_polynomials_card:
"card (bounded_degree_polynomials R n) = card (carrier R) ^ n"
proof -
have a:"coeff  bounded_degree_polynomials R n ⊆ {f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)}"
by (rule image_subsetI, auto simp add:bounded_degree_polynomials_def coeff_length coeff_in_carrier)

have b:"{f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)} ⊆ coeff  bounded_degree_polynomials R n"
apply (rule in_image_by_witness[where g="λx. build_poly x n"])

have "inj_on coeff (carrier (poly_ring R))"
by (rule inj_onI, simp add: coeff_iff_polynomial_cond univ_poly_carrier)

hence coeff_inj: "inj_on coeff (bounded_degree_polynomials R n)"
using inj_on_subset bounded_degree_polynomials_def by blast

have "card ( bounded_degree_polynomials R n) = card (coeff   bounded_degree_polynomials R n)"
using coeff_inj card_image[symmetric] by blast
also have "... = card {f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)}"
by (rule arg_cong[where f="card"], rule order_antisym[OF a b])
also have "... = card (carrier R)^n"
by (rule card_mostly_constant_maps, simp)
finally show ?thesis by simp
qed

end`