Theory Poly_Typeclass

section ‹Linking the carrier-set polynomial ring to Isabelle's polynomial type›

theory Poly_Typeclass
  imports Poly_Ring Ring_Theory "HOL-Computational_Algebra.Polynomial"
begin

text ‹
  ‹Poly_Ring› represents a polynomial as a finite-support function
  @{typ "nat ⇒ 'a"} with coefficients in a carrier @{term R}, which is exactly the representing
  set of HOL's @{typ "'a poly"} once the carrier is the whole type.  So for a type-class field the
  two developments describe the same objects, and the dictionary between them is little more than
  @{const Abs_poly}: this theory writes it out, so that the ring-theoretic results proved for
  @{term poly_carrier} --- irreducibility, division, unique factorisation --- become available to
  the extension and Galois theory, which is phrased throughout in terms of @{typ "'a poly"}.
›

subsection ‹Finite composites are sums and products›

text ‹The carrier-set @{const commutative_monoid.fincomp} at the whole type is HOL's
  @{const sum} or @{const prod}; the guard @{term commutative_monoid.M_ify} in its definition is
  vacuous there.›

lemma fincomp_TC_sum:
  "commutative_monoid.fincomp (UNIV :: 'a :: comm_monoid_add set) (+) 0 f A = sum f A"
proof -
  interpret M: commutative_monoid "UNIV :: 'a set" "(+)" 0
    by unfold_locales (auto simp: ac_simps)
  show ?thesis
    by (induct A rule: infinite_finite_induct) auto
qed

lemma fincomp_TC_prod:
  "commutative_monoid.fincomp (UNIV :: 'a :: comm_monoid_mult set) (*) 1 f A = prod f A"
proof -
  interpret M: commutative_monoid "UNIV :: 'a set" "(*)" 1
    by unfold_locales (auto simp: ac_simps)
  show ?thesis
    by (induct A rule: infinite_finite_induct) auto
qed


subsection ‹The two representations of a polynomial›

text ‹A finite-support function read as a polynomial.  Off the finite-support functions the value
  is arbitrary; @{term 0} is chosen so that the map is total.›

definition poly_of_fun :: "(nat ⇒ 'a :: zero) ⇒ 'a poly"
  where "poly_of_fun p ≡ (if finite {i. p i ≠ 0} then Abs_poly p else 0)"

lemma coeff_poly_of_fun [simp]:
  "finite {i. p i ≠ 0} ⟹ Polynomial.coeff (poly_of_fun p) = p"
  by (simp add: poly_of_fun_def Abs_poly_inverse MOST_iff_cofinite)

lemma finite_support_coeff [simp, intro]: "finite {i. Polynomial.coeff p i ≠ 0}"
  using MOST_coeff_eq_0 [of p] by (simp add: MOST_iff_cofinite)

lemma poly_of_fun_coeff [simp]: "poly_of_fun (Polynomial.coeff p) = p"
  by (simp add: poly_of_fun_def coeff_inverse)

lemma inj_on_poly_of_fun: "inj_on poly_of_fun {p. finite {i. p i ≠ 0}}"
  by (rule inj_onI) (metis coeff_poly_of_fun mem_Collect_eq)


subsection ‹The dictionary at a type-class field›

text ‹Fixing the carrier to be the whole type turns every constant of ‹Poly_Ring›
  into an operation on finite-support functions over a type-class field; the locale below exists only
  to make those constants available unqualified.›

locale poly_TC = Field "UNIV :: 'a :: field set" "(+)" "(*)" "0" "1"

interpretation poly_TC
  by (simp add: poly_TC_def field_TC.Field_axioms)

context poly_TC
begin

text ‹Membership of the carrier is finite support alone: every coefficient lies in the carrier
  because the carrier is everything.›
lemma poly_carrier_TC: "poly_carrier = {p :: nat ⇒ 'a. finite {i. p i ≠ 0}}"
  by (auto simp: poly_carrier_def)

lemma poly_carrier_iff: "p ∈ poly_carrier ⟷ finite {i. p i ≠ 0}"
  by (simp add: poly_carrier_TC)

lemma coeff_in_poly_carrier [simp, intro]: "Polynomial.coeff q ∈ poly_carrier"
  by (simp add: poly_carrier_iff)

lemma coeff_poly_of_fun_carrier [simp]:
  "p ∈ poly_carrier ⟹ Polynomial.coeff (poly_of_fun p) = p"
  by (simp add: poly_carrier_iff)

text ‹The additive inverse supplied by the group structure is HOL's, though the two are distinct
  constants and print alike; without this the coefficientwise proofs below cannot close.›
lemma additive_inverse_TC [simp]: "additive.inverse a = uminus a"
  by (intro additive.inverse_equality) simp_all

text ‹On the carrier the dictionary is injective, so an identity between carrier-set polynomials
  may be checked in @{typ "'a poly"} and conversely.›
lemma poly_of_fun_eq_iff [simp]:
  "⟦ p ∈ poly_carrier; q ∈ poly_carrier ⟧ ⟹ poly_of_fun p = poly_of_fun q ⟷ p = q"
  by (metis coeff_poly_of_fun_carrier)


subsection ‹The ring operations correspond›

lemma poly_of_fun_zero [simp]: "poly_of_fun poly_zero = 0"
  by (simp add: poly_zero_def poly_of_fun_def zero_poly_def)

lemma poly_of_fun_one [simp]: "poly_of_fun poly_one = 1"
  by (intro poly_eqI) (simp add: poly_one_def)

lemma poly_of_fun_add [simp]:
  assumes "p ∈ poly_carrier" and "q ∈ poly_carrier"
  shows "poly_of_fun (poly_add p q) = poly_of_fun p + poly_of_fun q"
  using assms poly_add_closed
  by (intro poly_eqI) (simp add: poly_add_def)

lemma poly_of_fun_neg [simp]:
  assumes "p ∈ poly_carrier"
  shows "poly_of_fun (poly_neg p) = - poly_of_fun p"
  using assms poly_neg_closed
  by (intro poly_eqI) (simp add: poly_neg_def)

text ‹The convolution defining @{const poly_mult} is literally HOL's @{thm [source] coeff_mult},
  once the finite composite is read as a sum.›
lemma poly_of_fun_mult [simp]:
  assumes "p ∈ poly_carrier" and "q ∈ poly_carrier"
  shows "poly_of_fun (poly_mult p q) = poly_of_fun p * poly_of_fun q"
  using assms poly_mult_closed
  by (intro poly_eqI) (simp add: poly_mult_def coeff_mult fincomp_TC_sum)


subsection ‹Constants, the indeterminate, degree and evaluation›

lemma poly_of_fun_const [simp]: "poly_of_fun (poly_const c) = [:c:]"
  unfolding poly_const_def
  by (intro poly_eqI) (auto simp: poly_carrier_iff coeff_pCons split: nat.split)

lemma poly_of_fun_monom [simp]: "poly_of_fun (monom c k) = Polynomial.monom c k"
  using local.monom_def by (intro poly_eqI) simp

lemma poly_of_fun_var [simp]: "poly_of_fun var = [:0, 1:]"
  by (simp add: var_def monom_altdef)

text ‹Both notions of degree are pinned by the same two inequalities: no coefficient above the
  degree, and a nonzero coefficient at it.›
lemma degree_poly_of_fun [simp]:
  assumes p: "p ∈ poly_carrier"
  shows "Polynomial.degree (poly_of_fun p) = degree p"
proof -
  have c: "Polynomial.coeff (poly_of_fun p) = p" using p by simp
  show ?thesis
  proof (intro antisym)
    show "Polynomial.degree (poly_of_fun p) ≤ degree p"
      using p c by (intro degree_le) (auto dest: coeff_gt_degree)
    show "degree p ≤ Polynomial.degree (poly_of_fun p)"
      using c coeff_degree_nonzero degree_le_iff p poly_zero_def by (metis le_degree)
  qed
qed

text ‹Powers in the multiplicative monoid of the type are ordinary powers.›
lemma rpow_TC [simp]: "rpow a n = a ^ n"
  by (induct n) simp_all

text ‹Evaluation matches @{thm [source] poly_altdef}, the coefficientwise form of @{const poly}.›
lemma poly_poly_of_fun [simp]:
  assumes "p ∈ poly_carrier"
  shows "Polynomial.poly (poly_of_fun p) x = eval x p"
  using assms by (simp add: poly_altdef eval_def fincomp_TC_sum)


subsection ‹Splitting into linear factors›

lemma poly_of_fun_root_factor [simp]: "poly_of_fun (root_factor a) = [:uminus a, 1:]"
  unfolding root_factor_def
  by (simp add: var_closed poly_const_closed poly_neg_closed)

lemma poly_of_fun_poly_prod:
  assumes "⋀f. f ∈ set fs ⟹ f ∈ poly_carrier"
  shows "poly_of_fun (poly_prod fs) = (∏f←fs. poly_of_fun f)"
  using assms by (induct fs) (auto simp: poly_prod_closed)

text ‹The witnessing product, translated once for both directions of the theorem below.›
lemma poly_of_fun_split_form:
  "poly_of_fun (poly_mult (poly_const c) (poly_prod (List.map root_factor as)))
     = [:c:] * (∏a←as. [:uminus a, 1:])"
proof -
  have rf: "⋀f. f ∈ set (List.map root_factor as) ⟹ f ∈ poly_carrier"
    by (auto intro: root_factor_closed)
  have "poly_of_fun (poly_mult (poly_const c) (poly_prod (List.map root_factor as)))
        = [:c:] * poly_of_fun (poly_prod (List.map root_factor as))"
    using rf poly_of_fun_mult [OF poly_const_closed poly_prod_closed] by fastforce
  also have "poly_of_fun (poly_prod (List.map root_factor as)) = (∏f←List.map root_factor as. poly_of_fun f)"
    using rf by (rule poly_of_fun_poly_prod)
  also have "… = (∏a←as. [:uminus a, 1:])"
    by (induct as) simp_all
  finally show ?thesis .
qed

lemma poly_mult_const_prod_carrier: "poly_mult (poly_const c) (poly_prod (List.map root_factor as)) ∈ poly_carrier"
  by (metis splitsI splits_closed UNIV_I top_greatest)

text ‹@{const splits} says exactly that the corresponding polynomial of @{typ "'a poly"} is a
  constant times a product of linear factors.  Both directions are the dictionary applied to the
  defining equation, the reverse using injectivity on the carrier.›
theorem splits_iff_linear_factors:
  assumes p: "p ∈ poly_carrier"
  shows "splits p ⟷ (∃c as. poly_of_fun p = [:c:] * (∏a←as. [:uminus a, 1:]))"
proof
  assume "splits p"
  then show "∃c as. poly_of_fun p = [:c:] * (∏a←as. [:uminus a, 1:])"
    by (force simp: splits_def poly_of_fun_split_form)
next
  assume "∃c as. poly_of_fun p = [:c:] * (∏a←as. [:uminus a, 1:])"
  then obtain c as where q: "poly_of_fun p = [:c:] * (∏a←as. [:uminus a, 1:])" by blast
  have "poly_of_fun p = poly_of_fun (poly_mult (poly_const c) (poly_prod (List.map root_factor as)))"
    by (simp add: q poly_of_fun_split_form)
  with p poly_mult_const_prod_carrier show "splits p"
    by (force simp: splits_def)
qed

text ‹A splitting polynomial of positive degree has a root: the factor list cannot be empty.›
theorem splits_imp_root:
  assumes p: "p ∈ poly_carrier" and sp: "splits p" and d: "0 < degree p"
  obtains a where "eval a p = 0"
proof -
  from sp obtain c as where q: "poly_of_fun p = [:c:] * (∏a←as. [:uminus a, 1:])"
    using splits_iff_linear_factors [OF p] by blast
  with assms degree_poly_of_fun[of p] have "as ≠ []"
    by (auto split: if_splits)
  then obtain a bs where as: "as = a # bs"
    by (metis list.exhaust)
  have "Polynomial.poly (poly_of_fun p) a = 0"
    unfolding q as by simp
  with p that show thesis by simp
qed


subsection ‹The dictionary read backwards›

text ‹Every polynomial of @{typ "'a poly"} is the reading of its own coefficient function, so each
  correspondence above serves in the other direction too.›

lemma eval_coeff [simp]: "eval x (Polynomial.coeff q) = Polynomial.poly q x"
  by (metis coeff_in_poly_carrier poly_of_fun_coeff poly_poly_of_fun)

lemma splits_coeff_iff:
  "splits (Polynomial.coeff q) ⟷ (∃c as. q = [:c:] * (∏a←as. [:uminus a, 1:]))"
  using splits_iff_linear_factors [OF coeff_in_poly_carrier] by simp

corollary splits_coeff_imp_root:
  assumes "splits (Polynomial.coeff q)" and "0 < Polynomial.degree q"
  obtains a where "Polynomial.poly q a = 0"
  by (metis assms coeff_in_poly_carrier degree_poly_of_fun eval_coeff poly_of_fun_coeff
      splits_imp_root)

end

text ‹Outside the locale the carrier-set degree must be named in full, its only parameter being the
  zero of the ring; that also makes it usable as a simplification rule on ordinary polynomials.›
lemma degree_coeff [simp]:
  fixes q :: "'a :: field poly"
  shows "Ring.degree 0 (Polynomial.coeff q) = Polynomial.degree q"
  by (metis coeff_in_poly_carrier degree_poly_of_fun poly_of_fun_coeff)

end