Theory Polynomial_Crit_Geometry_Library

(*
  File:      Polynomial_Crit_Geometry/Polynomial_Crit_Geometry_Library.thy
  Authors:   Manuel Eberl, University of Innsbruck
*)
section ‹Missing Library Material›
theory Polynomial_Crit_Geometry_Library
imports
  "HOL-Computational_Algebra.Computational_Algebra"
  "HOL-Library.FuncSet"
  "Polynomial_Interpolation.Ring_Hom_Poly"
begin

(* TODO: all of this probably belongs in the library *)

subsection ‹Multisets›

lemma size_repeat_mset [simp]: "size (repeat_mset n A) = n * size A"
  by (induction n) auto

lemma count_image_mset_inj:
  "inj f  count (image_mset f A) (f x) = count A x"
  by (induction A) (auto dest!: injD)

lemma count_le_size: "count A x  size A"
  by (induction A) auto

lemma image_mset_cong_simp:
  "M = M'  (x. x ∈# M =simp=> f x = g x)  {#f x. x ∈# M#} = {#g x. x ∈# M'#}"
  unfolding simp_implies_def by (auto intro: image_mset_cong)

lemma sum_mset_nonneg:
  fixes A :: "'a :: ordered_comm_monoid_add multiset"
  assumes "x. x ∈# A  x  0"
  shows   "sum_mset A  0"
  using assms by (induction A) auto

lemma sum_mset_pos:
  fixes A :: "'a :: ordered_comm_monoid_add multiset"
  assumes "A  {#}"
  assumes "x. x ∈# A  x > 0"
  shows   "sum_mset A > 0"
proof -
  from assms obtain x where "x ∈# A"
    by auto
  hence "A = {#x#} + (A - {#x#})"
    by auto
  also have "sum_mset  = x + sum_mset (A - {#x#})"
    by simp
  also have " > 0"
  proof (rule add_pos_nonneg)
    show "x > 0"
      using x ∈# A assms by auto
    show "sum_mset (A - {#x#})  0"
      using assms sum_mset_nonneg by (metis in_diffD order_less_imp_le)
  qed
  finally show ?thesis .
qed


subsection ‹Polynomials›

lemma order_pos_iff: "p  0  order x p > 0  poly p x = 0"
  by (cases "order x p = 0") (auto simp: order_root order_0I)

lemma order_prod_mset:
  "0 ∉# P  order x (prod_mset P) = sum_mset (image_mset (λp. order x p) P)"
  by (induction P) (auto simp: order_mult)

lemma order_prod:
  "(x. x  I  f x  0)  order x (prod f I) = (iI. order x (f i))"
  by (induction I rule: infinite_finite_induct) (auto simp: order_mult)

lemma order_linear_factor:
  assumes "a  0  b  0"
  shows "order x [:a, b:] = (if b * x + a = 0 then 1 else 0)"
proof (cases "b * x + a = 0")
  case True
  have "order x [:a, b:]  degree [:a, b:]"
    using assms by (intro order_degree) auto
  also have "  1"
    by simp
  finally have "order x [:a, b:]  1" .
  moreover have "order x [:a, b:] > 0"
    using assms True by (subst order_pos_iff) (auto simp: algebra_simps)
  ultimately have "order x [:a, b:] = 1"
    by linarith
  with True show ?thesis
    by simp
qed (auto intro!: order_0I simp: algebra_simps)

lemma order_linear_factor' [simp]:
  assumes "a  0  b  0" "b * x + a = 0"
  shows "order x [:a, b:] = 1"
  using assms by (subst order_linear_factor) auto

lemma degree_prod_mset_eq: "0 ∉# P  degree (prod_mset P) = (p∈#P. degree p)"
  for P :: "'a::idom poly multiset"
  by (induction P) (auto simp: degree_mult_eq)

lemma degree_prod_list_eq: "0  set ps  degree (prod_list ps) = (pps. degree p)"
  for ps :: "'a::idom poly list"
  by (induction ps) (auto simp: degree_mult_eq prod_list_zero_iff)

lemma order_conv_multiplicity:
  assumes "p  0"
  shows   "order x p = multiplicity [:-x, 1:] p"
  using assms order[of p x] multiplicity_eqI by metis


subsection ‹Polynomials over algebraically closed fields›

lemma irreducible_alg_closed_imp_degree_1:
  assumes "irreducible (p :: 'a :: alg_closed_field poly)"
  shows   "degree p = 1"
proof -
  have "¬(degree p > 1)"
    using assms alg_closed_imp_reducible by blast
  moreover from assms have "degree p  0"
    by (auto simp: irreducible_def is_unit_iff_degree)
  ultimately show ?thesis
    by linarith
qed

lemma prime_poly_alg_closedE:
  assumes "prime (q :: 'a :: {alg_closed_field, field_gcd} poly)"
  obtains c where "q = [:-c, 1:]" "poly q c = 0"
proof -
  from assms have "degree q = 1"
    by (intro irreducible_alg_closed_imp_degree_1 prime_elem_imp_irreducible) auto
  then obtain a b where q: "q = [:a, b:]"
    by (metis One_nat_def degree_pCons_eq_if nat.distinct(1) nat.inject pCons_cases)
  have "unit_factor q = 1"
    using assms by auto
  thus ?thesis
    using that[of "-a"] q degree q = 1
    by (auto simp: unit_factor_poly_def one_pCons dvd_field_iff is_unit_unit_factor split: if_splits)
qed

lemma prime_factors_alg_closed_poly_bij_betw:
  assumes "p  (0 :: 'a :: {alg_closed_field, field_gcd} poly)"
  shows "bij_betw (λx. [:-x, 1:]) {x. poly p x = 0} (prime_factors p)"
proof (rule bij_betwI[of _ _ _ "λq. -poly q 0"], goal_cases)
  case 1
  have [simp]: "p div [:1:] = p" for p :: "'a poly"
    by (simp add: pCons_one)
  show ?case using assms
    by (auto simp: in_prime_factors_iff dvd_iff_poly_eq_0 prime_def 
          prime_elem_linear_field_poly normalize_poly_def one_pCons)
qed (auto simp: in_prime_factors_iff elim!: prime_poly_alg_closedE dvdE)

lemma alg_closed_imp_factorization':
  assumes "p  (0 :: 'a :: alg_closed_field poly)"
  shows "p = smult (lead_coeff p) (x | poly p x = 0. [:-x, 1:] ^ order x p)"
proof -
  obtain A where A: "size A = degree p" "p = smult (lead_coeff p) (x∈#A. [:- x, 1:])"
    using alg_closed_imp_factorization[OF assms] by blast
  have "set_mset A = {x. poly p x = 0}" using assms 
    by (subst A(2)) (auto simp flip: poly_hom.prod_mset_image simp: image_image)

  note A(2)
  also have "(x∈#A. [:- x, 1:]) =
               (x(λx. [:- x, 1:]) ` set_mset A. x ^ count {#[:- x, 1:]. x ∈# A#} x)"
    by (subst prod_mset_multiplicity) simp_all
  also have "set_mset A = {x. poly p x = 0}" using assms 
    by (subst A(2)) (auto simp flip: poly_hom.prod_mset_image simp: image_image)
  also have "(x(λx. [:- x, 1:]) ` {x. poly p x = 0}. x ^ count {#[:- x, 1:]. x ∈# A#} x) =
             (x | poly p x = 0. [:- x, 1:] ^ count {#[:- x, 1:]. x ∈# A#} [:- x, 1:])"
    by (subst prod.reindex) (auto intro: inj_onI)
  also have "(λx. count {#[:- x, 1:]. x ∈# A#} [:- x, 1:]) = count A"
    by (subst count_image_mset_inj) (auto intro!: inj_onI)
  also have "count A = (λx. order x p)"
  proof
    fix x :: 'a
    have "order x p = order x (x∈#A. [:- x, 1:])"
      using assms by (subst A(2)) (auto simp: order_smult order_prod_mset)
    also have " = (y∈#A. order x [:-y, 1:])"
      by (subst order_prod_mset) (auto simp: multiset.map_comp o_def)
    also have "image_mset (λy. order x [:-y, 1:]) A = image_mset (λy. if y = x then 1 else 0) A"
      using order_power_n_n[of y 1 for y :: 'a]
      by (intro image_mset_cong) (auto simp: order_0I)
    also have " = replicate_mset (count A x) 1 + replicate_mset (size A - count A x) 0"
      by (induction A) (auto simp: add_ac Suc_diff_le count_le_size)
    also have "sum_mset  = count A x"
      by simp
    finally show "count A x = order x p" ..
  qed
  finally show ?thesis .
qed


subsection ‹Complex polynomials and conjugation›

lemma complex_poly_real_coeffsE:
  assumes "set (coeffs p)  "
  obtains p' where "p = map_poly complex_of_real p'"
proof (rule that)
  have "coeff p n  " for n
    using assms by (metis Reals_0 coeff_in_coeffs in_mono le_degree zero_poly.rep_eq)
  thus "p = map_poly complex_of_real (map_poly Re p)"
    by (subst map_poly_map_poly) (auto simp: poly_eq_iff o_def coeff_map_poly)
qed

lemma order_map_poly_cnj:
  assumes "p  0"
  shows   "order x (map_poly cnj p) = order (cnj x) p"
proof -
  have "order x (map_poly cnj p)  order (cnj x) p" if p: "p  0" for p :: "complex poly" and x
  proof (rule order_max)
    interpret map_poly_idom_hom cnj
      by standard auto
    interpret field_hom cnj
      by standard auto
    have "[:-x, 1:] ^ order x (map_poly cnj p) dvd map_poly cnj p"
      using order[of "map_poly cnj p" x] p by simp
    also have "[:-x, 1:] ^ order x (map_poly cnj p) =
               map_poly cnj ([:-cnj x, 1:] ^ order x (map_poly cnj p))"
      by (simp add: hom_power)
    finally show "[:-cnj x, 1:] ^ order x (map_poly cnj p) dvd p"
      by (rule dvd_map_poly_hom_imp_dvd)
  qed fact+
  from this[of p x] and this[of "map_poly cnj p" "cnj x"] and assms show ?thesis
    by (simp add: map_poly_map_poly o_def)
qed


subsection n›-ary product rule for the derivative›

lemma has_field_derivative_prod_mset [derivative_intros]:
  assumes "x. x ∈# A  (f x has_field_derivative f' x) (at z)"
  shows   "((λu. x∈#A. f x u) has_field_derivative (x∈#A. f' x * (y∈#A-{#x#}. f y z))) (at z)"
  using assms
proof (induction A)
  case (add x A)
  note [derivative_intros] = add
  note [cong] = image_mset_cong_simp
  show ?case
    by (auto simp: field_simps multiset.map_comp o_def  intro!: derivative_eq_intros)
qed auto

lemma has_field_derivative_prod [derivative_intros]:
  assumes "x. x  A  (f x has_field_derivative f' x) (at z)"
  shows   "((λu. xA. f x u) has_field_derivative (xA. f' x * (yA-{x}. f y z))) (at z)"
  using assms
proof (cases "finite A")
  case [simp, intro]: True
  have "((λu. xA. f x u) has_field_derivative
          (xA. f' x * (y∈#mset_set A-{#x#}. f y z))) (at z)"
    using has_field_derivative_prod_mset[of "mset_set A" f f' z] assms
    by (simp add: prod_unfold_prod_mset sum_unfold_sum_mset)
  also have "(xA. f' x * (y∈#mset_set A-{#x#}. f y z)) =
             (xA. f' x * (y∈#mset_set (A-{x}). f y z))"
    by (intro sum.cong) (auto simp: mset_set_Diff)
  finally show ?thesis
    by (simp add: prod_unfold_prod_mset)
qed auto

lemma has_field_derivative_prod_mset':
  assumes "x. x ∈# A  f x z  0"
  assumes "x. x ∈# A  (f x has_field_derivative f' x) (at z)"
  defines "P  (λA u. x∈#A. f x u)"
  shows   "(P A has_field_derivative (P A z * (x∈#A. f' x / f x z))) (at z)"
  using assms
  by (auto intro!: derivative_eq_intros cong: image_mset_cong_simp
           simp:   sum_distrib_right mult_ac prod_mset_diff image_mset_Diff multiset.map_comp o_def)

lemma has_field_derivative_prod':
  assumes "x. x  A  f x z  0"
  assumes "x. x  A  (f x has_field_derivative f' x) (at z)"
  defines "P  (λA u. xA. f x u)"
  shows   "(P A has_field_derivative (P A z * (xA. f' x / f x z))) (at z)"
proof (cases "finite A")
  case True
  show ?thesis using assms True
    by (auto intro!: derivative_eq_intros
             simp: prod_diff1 sum_distrib_left sum_distrib_right mult_ac)
qed (auto simp: P_def)


subsection ‹Facts about complex numbers›

lemma Re_sum_mset: "Re (sum_mset X) = (x∈#X. Re x)"
  by (induction X) auto

lemma Im_sum_mset: "Im (sum_mset X) = (x∈#X. Im x)"
  by (induction X) auto

lemma Re_sum_mset': "Re (x∈#X. f x) = (x∈#X. Re (f x))"
  by (induction X) auto

lemma Im_sum_mset': "Im (x∈#X. f x) = (x∈#X. Im (f x))"
  by (induction X) auto

lemma inverse_complex_altdef: "inverse z = cnj z / norm z ^ 2"
  by (metis complex_div_cnj inverse_eq_divide mult_1)

end