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"
    by (simp add: card_PiE[OF finite_atLeastLessThan])
  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)"
  hence b:"lead_coeff x  𝟬R⇙"
    by (metis assms(1) polynomial_def univ_poly_carrier univ_poly_zero)
  hence "coeff x (degree x)  𝟬"
    by (metis a lead_coeff_simp univ_poly_zero)
  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]
  by (simp add:bounded_degree_polynomials_def univ_poly_zero 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"])
    by (auto simp add:build_poly_coeff intro:build_poly_bounded)

  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