Theory 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