Theory Polynomial_Interpolation.Ring_Hom_Poly

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Connecting Polynomials with Homomorphism Locales›

theory Ring_Hom_Poly
imports 
  "HOL-Computational_Algebra.Euclidean_Algorithm"
  Ring_Hom
  Missing_Polynomial
begin

text‹@{term poly} as a homomorphism. Note that types differ.›

interpretation poly_hom: comm_semiring_hom "λp. poly p a" by (unfold_locales, auto)

interpretation poly_hom: comm_ring_hom "λp. poly p a"..

interpretation poly_hom: idom_hom "λp. poly p a"..

text ‹@{term "(∘⇩p)"} as a homomorphism.›

interpretation pcompose_hom: comm_semiring_hom "λq. q ∘⇩p p"
  using pcompose_add pcompose_mult pcompose_1 by (unfold_locales, auto)

interpretation pcompose_hom: comm_ring_hom "λq. q ∘⇩p p" ..

interpretation pcompose_hom: idom_hom "λq. q ∘⇩p p" ..



definition eval_poly :: "('a ⇒ 'b :: comm_semiring_1) ⇒ 'a :: zero poly ⇒ 'b ⇒ 'b" where
  [code del]: "eval_poly h p = poly (map_poly h p)"

lemma eval_poly_code[code]: "eval_poly h p x = fold_coeffs (λ a b. h a + x * b) p 0" 
  by (induct p, auto simp: eval_poly_def)

lemma eval_poly_as_sum:
  fixes h :: "'a :: zero ⇒ 'b :: comm_semiring_1"
  assumes "h 0 = 0"
  shows "eval_poly h p x = (∑i≤degree p. x^i * h (coeff p i))"
  unfolding eval_poly_def
proof (induct p)
  case 0 show ?case using assms by simp
  next case (pCons a p) thus ?case
    proof (cases "p = 0")
      case True show ?thesis by (simp add: True map_poly_simps assms)
      next case False show ?thesis
        unfolding degree_pCons_eq[OF False]
        unfolding sum.atMost_Suc_shift
        unfolding map_poly_pCons[OF pCons(1)]
        by (simp add: pCons(2) sum_distrib_left mult.assoc)
  qed
qed

lemma coeff_const: "coeff [: a :] i = (if i = 0 then a else 0)"
  by (metis coeff_monom monom_0)

lemma x_as_monom: "[:0,1:] = monom 1 1"
  by (simp add: monom_0 monom_Suc)

lemma x_pow_n: "monom 1 1 ^ n = monom 1 n"
  by (induct n) (simp_all add: monom_0 monom_Suc)

lemma map_poly_eval_poly: assumes h0: "h 0 = 0"
  shows "map_poly h p = eval_poly (λ a. [: h a :]) p [:0,1:]" (is "?mp = ?ep")
proof (rule poly_eqI)
  fix i :: nat
  have 2: "(∑x≤i. ∑xa≤degree p. (if xa = x then 1 else 0) * coeff [:h (coeff p xa):] (i - x)) 
    = h (coeff p i)" (is "sum ?f ?s = ?r")
  proof -
    have "sum ?f ?s = ?f i + sum ?f ({..i} - {i})"
      by (rule sum.remove[of _ i], auto)
    also have "sum ?f ({..i} - {i}) = 0"
      by (rule sum.neutral, intro ballI, rule sum.neutral, auto simp: coeff_const)
    also have "?f i = (∑xa≤degree p. (if xa = i then 1 else 0) * h (coeff p xa))" (is "_ = ?m")
      unfolding coeff_const by simp
    also have "… = ?r"
    proof (cases "i ≤ degree p")
      case True
      show ?thesis
        by (subst sum.remove[of _ i], insert True, auto)
    next
      case False
      hence [simp]: "coeff p i = 0" using le_degree by blast
      show ?thesis
        by (subst sum.neutral, auto simp: h0)
    qed
    finally show ?thesis by simp
  qed
  have h'0: "[: h 0 :] = 0" using h0 by auto
  show "coeff ?mp i = coeff ?ep i"
    unfolding coeff_map_poly[of h, OF h0]
    unfolding eval_poly_as_sum[of "λa. [: h a :]", OF h'0]
    unfolding coeff_sum
    unfolding x_as_monom x_pow_n coeff_mult
    unfolding sum.swap[of _ _ "{..degree p}"]
    unfolding coeff_monom using 2 by auto
qed

lemma smult_as_map_poly: "smult a = map_poly ((*) a)"
  by (rule ext, rule poly_eqI, subst coeff_map_poly, auto)


subsection ‹@{const map_poly} of Homomorphisms›

context zero_hom begin
  text ‹We will consider @{term hom} is always simpler than @{term "map_poly hom"}.›
  lemma map_poly_hom_monom[simp]: "map_poly hom (monom a i) = monom (hom a) i"
    by(rule map_poly_monom, auto)
  lemma coeff_map_poly_hom[simp]: "coeff (map_poly hom p) i = hom (coeff p i)"
    by (rule coeff_map_poly, rule hom_zero)
end

locale map_poly_zero_hom = base: zero_hom
begin
  sublocale zero_hom "map_poly hom" by (unfold_locales, auto)
end

text ‹@{const map_poly} preserves homomorphisms over addition.›

context comm_monoid_add_hom
begin
  lemma map_poly_hom_add[hom_distribs]:
    "map_poly hom (p + q) = map_poly hom p + map_poly hom q"
    by (rule map_poly_add; simp add: hom_distribs)
end

locale map_poly_comm_monoid_add_hom = base: comm_monoid_add_hom
begin
  sublocale comm_monoid_add_hom "map_poly hom" by (unfold_locales, auto simp:hom_distribs)
end

text ‹To preserve homomorphisms over multiplication, it demands commutative ring homomorphisms.›
context comm_semiring_hom begin
  lemma map_poly_pCons_hom[hom_distribs]: "map_poly hom (pCons a p) = pCons (hom a) (map_poly hom p)"
    unfolding map_poly_simps by auto
  lemma map_poly_hom_smult[hom_distribs]:
    "map_poly hom (smult c p) = smult (hom c) (map_poly hom p)"
    by (induct p, auto simp: hom_distribs)
  lemma poly_map_poly[simp]: "poly (map_poly hom p) (hom x) = hom (poly p x)"
    by (induct p; simp add: hom_distribs)
end

locale map_poly_comm_semiring_hom = base: comm_semiring_hom
begin
  sublocale map_poly_comm_monoid_add_hom..
  sublocale comm_semiring_hom "map_poly hom"
  proof
    show "map_poly hom 1 = 1" by simp
    fix p q show "map_poly hom (p * q) = map_poly hom p * map_poly hom q"
      by (induct p, auto simp: hom_distribs)
  qed
end

locale map_poly_comm_ring_hom = base: comm_ring_hom
begin
  sublocale map_poly_comm_semiring_hom..
  sublocale comm_ring_hom "map_poly hom"..
end

locale map_poly_idom_hom = base: idom_hom
begin
  sublocale map_poly_comm_ring_hom..
  sublocale idom_hom "map_poly hom"..
end

subsubsection ‹Injectivity›

locale map_poly_inj_zero_hom = base: inj_zero_hom
begin
  sublocale inj_zero_hom "map_poly hom"
  proof (unfold_locales)
    fix p q :: "'a poly" assume "map_poly hom p = map_poly hom q"
    from cong[of "λp. coeff p _", OF refl this] show "p = q" by (auto intro: poly_eqI)
  qed simp
end

locale map_poly_inj_comm_monoid_add_hom = base: inj_comm_monoid_add_hom
begin
  sublocale map_poly_comm_monoid_add_hom..
  sublocale map_poly_inj_zero_hom..
  sublocale inj_comm_monoid_add_hom "map_poly hom"..
end

locale map_poly_inj_comm_semiring_hom = base: inj_comm_semiring_hom
begin
  sublocale map_poly_comm_semiring_hom..
  sublocale map_poly_inj_zero_hom..
  sublocale inj_comm_semiring_hom "map_poly hom"..
end

locale map_poly_inj_comm_ring_hom = base: inj_comm_ring_hom
begin
  sublocale map_poly_inj_comm_semiring_hom..
  sublocale inj_comm_ring_hom "map_poly hom"..
end

locale map_poly_inj_idom_hom = base: inj_idom_hom
begin
  sublocale map_poly_inj_comm_ring_hom..
  sublocale inj_idom_hom "map_poly hom"..
end




lemma degree_map_poly_le: "degree (map_poly f p) ≤ degree p"
  by(induct p;auto)

lemma coeffs_map_poly: (* An exact variant *)
  assumes "f (lead_coeff p) = 0 ⟷ p = 0"
  shows "coeffs (map_poly f p) = map f (coeffs p)"
  unfolding coeffs_map_poly using assms by (simp add:coeffs_def)

lemma degree_map_poly: (* An exact variant *)
  assumes "f (lead_coeff p) = 0 ⟷ p = 0"
  shows   "degree (map_poly f p) = degree p"
  unfolding degree_eq_length_coeffs unfolding coeffs_map_poly[of f, OF assms] by simp

context zero_hom_0 begin
  lemma degree_map_poly_hom[simp]: "degree (map_poly hom p) = degree p"
    by (rule degree_map_poly, auto)
  lemma coeffs_map_poly_hom[simp]: "coeffs (map_poly hom p) = map hom (coeffs p)"
    by (rule coeffs_map_poly, auto)
  lemma hom_lead_coeff[simp]: "lead_coeff (map_poly hom p) = hom (lead_coeff p)"
    by simp
end

context comm_semiring_hom begin

  interpretation map_poly_hom: map_poly_comm_semiring_hom..

  lemma poly_map_poly_0[simp]:
    "poly (map_poly hom p) 0 = hom (poly p 0)" (is "?l = ?r")
  proof-
    have "?l = poly (map_poly hom p) (hom 0)" by auto
    then show ?thesis unfolding poly_map_poly.
  qed

  lemma poly_map_poly_1[simp]:
    "poly (map_poly hom p) 1 = hom (poly p 1)" (is "?l = ?r")
  proof-
    have "?l = poly (map_poly hom p) (hom 1)" by auto
    then show ?thesis unfolding poly_map_poly.
  qed

  lemma map_poly_hom_as_monom_sum:
    "(∑j≤degree p. monom (hom (coeff p j)) j) = map_poly hom p"
  proof -
    show ?thesis
      by (subst(6) poly_as_sum_of_monoms'[OF le_refl, symmetric], simp add: hom_distribs)
  qed

  lemma map_poly_pcompose[hom_distribs]:
    "map_poly hom (f ∘⇩p g) = map_poly hom f ∘⇩p map_poly hom g"
    by (induct f arbitrary: g; auto simp: hom_distribs)

end

context comm_semiring_hom begin

lemma eval_poly_0[simp]: "eval_poly hom 0 x = 0" unfolding eval_poly_def by simp
lemma eval_poly_monom: "eval_poly hom (monom a n) x = hom a * x ^ n"
  unfolding eval_poly_def
  unfolding map_poly_monom[of hom, OF hom_zero] using poly_monom.

lemma poly_map_poly_eval_poly: "poly (map_poly hom p) = eval_poly hom p"
  unfolding eval_poly_def..

lemma map_poly_eval_poly: 
  "map_poly hom p = eval_poly (λ a. [: hom a :]) p [:0,1:]" 
  by (rule map_poly_eval_poly, simp)

lemma degree_extension: assumes "degree p ≤ n"
  shows "(∑i≤degree p. x ^ i * hom (coeff p i))
      = (∑i≤n. x ^ i * hom (coeff p i))" (is "?l = ?r")
proof -
  let ?f = "λ i. x ^ i * hom (coeff p i)"
  define m where "m = n - degree p"
  have n: "n = degree p + m" unfolding m_def using assms by auto
  have "?r = (∑ i ≤ degree p + m. ?f i)" unfolding n ..
  also have "… = ?l + sum ?f {Suc (degree p) .. degree p + m}"
    by (subst sum.union_disjoint[symmetric], auto intro: sum.cong)
  also have "sum ?f {Suc (degree p) .. degree p + m} = 0"
    by (rule sum.neutral, auto simp: coeff_eq_0)
  finally show ?thesis by simp
qed

lemma eval_poly_add[simp]: "eval_poly hom (p + q) x = eval_poly hom p x + eval_poly hom q x"
  unfolding eval_poly_def hom_distribs..

lemma eval_poly_sum: "eval_poly hom (∑k∈A. p k) x = (∑k∈A. eval_poly hom (p k) x)"
proof (induct A rule: infinite_finite_induct)
  case (insert a A)
  show ?case
    unfolding sum.insert[OF insert(1-2)] insert(3)[symmetric] by simp
qed (auto simp: eval_poly_def)

lemma eval_poly_poly: "eval_poly hom p (hom x) = hom (poly p x)"
  unfolding eval_poly_def by auto

end

context comm_ring_hom begin
  interpretation map_poly_hom: map_poly_comm_ring_hom..

  lemma pseudo_divmod_main_hom:
    "pseudo_divmod_main (hom lc) (map_poly hom q) (map_poly hom r) (map_poly hom d) dr i =
     map_prod (map_poly hom) (map_poly hom) (pseudo_divmod_main lc q r d dr i)"
  proof-
    show ?thesis by (induct lc q r d dr i rule:pseudo_divmod_main.induct, auto simp: Let_def hom_distribs)
  qed
end

lemma(in inj_comm_ring_hom) pseudo_divmod_hom:
  "pseudo_divmod (map_poly hom p) (map_poly hom q) =
   map_prod (map_poly hom) (map_poly hom) (pseudo_divmod p q)"
  unfolding pseudo_divmod_def using pseudo_divmod_main_hom[of _ 0] by (cases "q = 0",auto)

lemma(in inj_idom_hom) pseudo_mod_hom:
  "pseudo_mod (map_poly hom p) (map_poly hom q) = map_poly hom (pseudo_mod p q)"
  using pseudo_divmod_hom unfolding pseudo_mod_def by auto

lemma(in idom_hom) map_poly_pderiv[hom_distribs]:
  "map_poly hom (pderiv p) = pderiv (map_poly hom p)"
proof (induct p rule: pderiv.induct)
  case (1 a p)
  then show ?case unfolding pderiv.simps map_poly_pCons_hom by (cases "p = 0", auto simp: hom_distribs)
qed

lemma(in idom_hom) map_poly_higher_pderiv[hom_distribs]:
  "map_poly hom ((pderiv ^^ n) p) = (pderiv ^^ n) (map_poly hom p)"
  by (induction n) (auto simp: hom_distribs)

context field_hom
begin

lemma dvd_map_poly_hom_imp_dvd: ‹map_poly hom x dvd map_poly hom y ⟹ x dvd y›
  by (smt (verit, del_insts) degree_map_poly_hom hom_0 hom_div hom_lead_coeff hom_one hom_power map_poly_hom_smult map_poly_zero mod_eq_0_iff_dvd mod_poly_def pseudo_mod_hom)

lemma map_poly_pdivmod [hom_distribs]:
  ‹map_prod (map_poly hom) (map_poly hom) (p div q, p mod q) =
    (map_poly hom p div map_poly hom q, map_poly hom p mod map_poly hom q)›
proof -
  let ?mp = ‹map_poly hom›
  interpret map_poly_hom: map_poly_idom_hom ..
  have ‹(?mp p div ?mp q, ?mp p mod ?mp q) = (?mp (p div q), ?mp (p mod q))›
  proof (induction rule: euclidean_relation_polyI)
    case by0
    then show ?case
      by simp
  next
    case divides
    then have ‹q ≠ 0› ‹q dvd p›
      by (auto dest: dvd_map_poly_hom_imp_dvd)
    from ‹q dvd p› obtain r where ‹p = q * r› ..
    with ‹q ≠ 0› show ?case
      by (simp add: map_poly_hom.hom_mult)
  next
    case euclidean_relation
    with degree_mod_less_degree [of q p] show ?case
      by (auto simp flip: map_poly_hom.hom_mult map_poly_hom_add)
  qed
  then show ?thesis
    by simp
qed

lemma map_poly_div[hom_distribs]: "map_poly hom (p div q) = map_poly hom p div map_poly hom q"
  using map_poly_pdivmod[of p q] by simp

lemma map_poly_mod[hom_distribs]: "map_poly hom (p mod q) = map_poly hom p mod map_poly hom q"
  using map_poly_pdivmod[of p q] by simp

end

locale field_hom' = field_hom hom
  for hom :: "'a :: {field_gcd} ⇒ 'b :: {field_gcd}"
begin

lemma map_poly_normalize[hom_distribs]: "map_poly hom (normalize p) = normalize (map_poly hom p)"
  by (simp add: normalize_poly_def hom_distribs)

lemma map_poly_gcd[hom_distribs]: "map_poly hom (gcd p q) = gcd (map_poly hom p) (map_poly hom q)"
  by (induct p q rule: eucl_induct)
    (simp_all add: map_poly_normalize ac_simps hom_distribs)

end

definition div_poly :: "'a :: euclidean_semiring ⇒ 'a poly ⇒ 'a poly" where
  "div_poly a p = map_poly (λ c. c div a) p"

lemma smult_div_poly: assumes "⋀ c. c ∈ set (coeffs p) ⟹ a dvd c"
  shows "smult a (div_poly a p) = p" 
  unfolding smult_as_map_poly div_poly_def 
  by (subst map_poly_map_poly, force, subst map_poly_idI, insert assms, auto)

lemma coeff_div_poly: "coeff (div_poly a f) n = coeff f n div a" 
  unfolding div_poly_def
  by (rule coeff_map_poly, auto)

locale map_poly_inj_idom_divide_hom = base: inj_idom_divide_hom
begin
sublocale map_poly_idom_hom ..
sublocale map_poly_inj_zero_hom .. 
sublocale inj_idom_hom "map_poly hom" ..
lemma divide_poly_main_hom: defines "hh ≡ map_poly hom" 
  shows "hh (divide_poly_main lc f g h i j) = divide_poly_main (hom lc) (hh f) (hh g) (hh h) i j"  
  unfolding hh_def
proof (induct j arbitrary: lc f g h i)
  case (Suc j lc f g h i)
  let ?h = "map_poly hom" 
  show ?case unfolding divide_poly_main.simps Let_def
    unfolding base.coeff_map_poly_hom base.hom_div[symmetric] base.hom_mult[symmetric] base.eq_iff
      if_distrib[of ?h] hom_zero
    by (rule if_cong[OF refl _ refl], subst Suc, simp add: hom_minus hom_add hom_mult)
qed simp

sublocale inj_idom_divide_hom "map_poly hom" 
proof
  fix f g :: "'a poly" 
  let ?h = "map_poly hom" 
  show "?h (f div g) = (?h f) div (?h g)" unfolding divide_poly_def if_distrib[of ?h]
    divide_poly_main_hom by simp
qed

lemma order_hom: "order (hom x) (map_poly hom f) = order x f"
  unfolding Polynomial.order_def unfolding hom_dvd_iff[symmetric]
  unfolding hom_power by (simp add: base.hom_uminus)
end


subsection ‹Example Interpretations›

abbreviation "of_int_poly ≡ map_poly of_int"

interpretation of_int_poly_hom: map_poly_comm_semiring_hom of_int..
interpretation of_int_poly_hom: map_poly_comm_ring_hom of_int..
interpretation of_int_poly_hom: map_poly_idom_hom of_int..
interpretation of_int_poly_hom:
  map_poly_inj_comm_ring_hom "of_int :: int  ⇒ 'a :: {comm_ring_1,ring_char_0}" ..
interpretation of_int_poly_hom:
  map_poly_inj_idom_hom "of_int :: int  ⇒ 'a :: {idom,ring_char_0}" ..


text ‹The following operations are homomorphic w.r.t. only @{class monoid_add}.›

interpretation pCons_0_hom: injective "pCons 0" by (unfold_locales, auto)
interpretation pCons_0_hom: zero_hom_0 "pCons 0" by (unfold_locales, auto)
interpretation pCons_0_hom: inj_comm_monoid_add_hom "pCons 0" by (unfold_locales, auto)
interpretation pCons_0_hom: inj_ab_group_add_hom "pCons 0" by (unfold_locales, auto)

interpretation monom_hom: injective "λx. monom x d" by (unfold_locales, auto)
interpretation monom_hom: inj_monoid_add_hom "λx. monom x d" by (unfold_locales, auto simp: add_monom)
interpretation monom_hom: inj_comm_monoid_add_hom "λx. monom x d"..

end