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"
  "Formal_Puiseux_Series.Formal_Puiseux_Series" (* for alg_closed_field *)
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) = (∑i∈I. 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) = (∑p←ps. degree p)"
  for ps :: "'a::idom poly list"
  by (induction ps) (auto simp: degree_mult_eq)

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 (intro notI) auto
  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 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. ∏x∈A. f x u) has_field_derivative (∑x∈A. f' x * (∏y∈A-{x}. f y z))) (at z)"
  using assms
proof (cases "finite A")
  case [simp, intro]: True
  have "((λu. ∏x∈A. f x u) has_field_derivative
          (∑x∈A. 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 "(∑x∈A. f' x * (∏y∈#mset_set A-{#x#}. f y z)) =
             (∑x∈A. 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. ∏x∈A. f x u)"
  shows   "(P A has_field_derivative (P A z * (∑x∈A. 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