Theory Polynomials.More_MPoly_Type

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)

theory More_MPoly_Type
imports MPoly_Type
begin

abbreviation "lookup == Poly_Mapping.lookup"
abbreviation "keys == Poly_Mapping.keys"

section "MPpoly Mapping extenion"

lemma lookup_Abs_poly_mapping_when_finite:
assumes "finite S"
shows "lookup (Abs_poly_mapping (λx. f x when x∈S)) = (λx. f x when x∈S)"
proof -
  have "finite {x. (f x when x∈S) ≠ 0}" using assms by auto
  then show ?thesis using lookup_Abs_poly_mapping by fast
qed

definition remove_key::"'a ⇒ ('a ⇒⇩0 'b::monoid_add) ⇒ ('a ⇒⇩0 'b)" where
  "remove_key k0 f = Abs_poly_mapping (λk. lookup f k when k ≠ k0)"

lemma remove_key_lookup:
  "lookup (remove_key k0 f) k = (lookup f k when k ≠ k0)"
unfolding remove_key_def using finite_subset by (simp add: lookup_Abs_poly_mapping)

lemma remove_key_keys: "keys f - {k} = keys (remove_key k f)" (is "?A = ?B")
proof (rule antisym; rule subsetI)
  fix x assume "x ∈ ?A"
  then show "x ∈ ?B" using remove_key_lookup lookup_not_eq_zero_eq_in_keys DiffD1 DiffD2 insertCI
    by (metis (mono_tags, lifting) when_def)
next
  fix x assume "x ∈ ?B"
  then have "lookup (remove_key k f) x ≠ 0"  by blast
  then show "x ∈ ?A"
    by (simp add: lookup_not_eq_zero_eq_in_keys remove_key_lookup)
qed


lemma remove_key_sum: "remove_key k f + Poly_Mapping.single k (lookup f k) = f"
proof -
  {
  fix k'
  have rem:"(lookup f k' when k' ≠ k) = lookup (remove_key k f) k'"
    using when_def by (simp add: remove_key_lookup)
  have sin:"(lookup f k when k'=k) =  lookup (Poly_Mapping.single k (lookup f k)) k'"
    by (simp add: lookup_single_not_eq when_def)
  have "lookup f k' = (lookup f k' when k' ≠ k) + ((lookup f k) when k'=k)"
    unfolding when_def by fastforce
  with rem sin have "lookup f k' = lookup ((remove_key k f) + Poly_Mapping.single k (lookup f k)) k'"
    using lookup_add by metis
  }
  then show ?thesis by (metis poly_mapping_eqI)
qed

lemma remove_key_single[simp]: "remove_key v (Poly_Mapping.single v n) = 0"
proof -
 have 0:"⋀k. (lookup (Poly_Mapping.single v n) k when k ≠ v) = 0" by (simp add: lookup_single_not_eq when_def)
 show ?thesis unfolding remove_key_def 0
   by auto
qed

lemma remove_key_add: "remove_key v m + remove_key v m' = remove_key v (m + m')"
  by (rule poly_mapping_eqI; simp add: lookup_add remove_key_lookup when_add_distrib)

lemma poly_mapping_induct [case_names single sum]:
fixes P::"('a, 'b::monoid_add) poly_mapping ⇒ bool"
assumes single:"⋀k v. P (Poly_Mapping.single k v)"
and sum:"(⋀f g k v. P f ⟹ P g ⟹ g = (Poly_Mapping.single k v) ⟹ k ∉ keys f ⟹ P (f+g))"
shows "P f" using finite_keys[of f]
proof (induction "keys f" arbitrary: f rule: finite_induct)
  case (empty)
  then show ?case using single[of _ 0] by (metis (full_types) aux empty_iff not_in_keys_iff_lookup_eq_zero single_zero)
next
  case (insert k K f)
  obtain f1 f2 where f12_def: "f1 = remove_key k f" "f2 = Poly_Mapping.single k (lookup f k)" by blast
  have "P f1"
  proof -
    have "Suc (card (keys f1)) = card (keys f)"
      using remove_key_keys finite_keys f12_def(1) by (metis (no_types) Diff_insert_absorb card_insert_disjoint insert.hyps(2) insert.hyps(4))
    then show ?thesis using insert lessI by (metis Diff_insert_absorb f12_def(1) remove_key_keys)
  qed
  have "P f2" by (simp add: single f12_def(2))
  have "f1 + f2 = f" using remove_key_sum f12_def by auto
  have "k ∉ keys f1" using remove_key_keys f12_def by fast
  then show ?case using ‹P f1› ‹P f2› sum[of f1 f2 k "lookup f k"] ‹f1 + f2 = f› f12_def by auto
qed


lemma map_lookup:
assumes "g 0 = 0"
shows "lookup (Poly_Mapping.map g f) x = g ((lookup f) x)"
proof -
  have "(g (lookup f x) when lookup f x ≠ 0) = g (lookup f x)"
    by (metis (mono_tags, lifting) assms when_def)
  then have "(g (lookup f x) when x ∈ keys f) = g (lookup f x)"
    using lookup_not_eq_zero_eq_in_keys [of f] by simp
  then show ?thesis 
    by (simp add: Poly_Mapping.map_def map_fun_def in_keys_iff)
qed

lemma keys_add:
assumes "keys f ∩ keys g = {}"
shows "keys f ∪ keys g = keys (f+g)"
proof
  have "keys f ⊆ keys (f+g)"
  proof
    fix x assume "x∈keys f"
    then have "lookup (f+g) x = lookup f x " by (metis add.right_neutral assms disjoint_iff_not_equal not_in_keys_iff_lookup_eq_zero plus_poly_mapping.rep_eq)
    then show "x∈keys (f+g)" using ‹x∈keys f› by (metis not_in_keys_iff_lookup_eq_zero)
  qed
  moreover have "keys g ⊆ keys (f+g)"
  proof
    fix x assume "x∈keys g"
    then have "lookup (f+g) x = lookup g x "  by (metis IntI add.left_neutral assms empty_iff not_in_keys_iff_lookup_eq_zero plus_poly_mapping.rep_eq)
    then show "x∈keys (f+g)" using ‹x∈keys g› by (metis not_in_keys_iff_lookup_eq_zero)
  qed
  ultimately show "keys f ∪ keys g ⊆ keys (f+g)" by simp
next
  show "keys (f + g) ⊆ keys f ∪ keys g" by (simp add: keys_add)
qed

lemma fun_when:
"f 0 = 0 ⟹ f (a when P) = (f a when P)" by (simp add: when_def)

section "MPoly extension"

lemma coeff_all_0:"(⋀m. coeff p m = 0) ⟹ p=0"
  by (metis aux coeff_def mapping_of_inject zero_mpoly.rep_eq)

definition vars::"'a::zero mpoly ⇒ nat set" where
  "vars p = ⋃ (keys ` keys (mapping_of p))"

lemma vars_finite: "finite (vars p)" unfolding vars_def by auto

lemma vars_monom_single: "vars (monom (Poly_Mapping.single v k) a) ⊆ {v}"
proof
  fix w assume "w ∈ vars (monom (Poly_Mapping.single v k) a)"
  then have "w = v" using vars_def by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq monom.rep_eq)
  then show "w ∈ {v}" by auto
qed

lemma vars_monom_keys:
assumes "a≠0"
shows "vars (monom m a) = keys m"
proof (rule antisym; rule subsetI)
  fix w assume "w ∈ vars (monom m a)"
  then have "lookup m w ≠ 0" using vars_def by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq monom.rep_eq)
  then show "w ∈ keys m" by (meson lookup_not_eq_zero_eq_in_keys)
next
  fix w assume "w ∈ keys m"
  then have "lookup m w ≠ 0" by (meson lookup_not_eq_zero_eq_in_keys)
  then show "w ∈ vars (monom m a)" unfolding vars_def using assms by (metis UN_iff lookup_not_eq_zero_eq_in_keys lookup_single_eq monom.rep_eq)
qed

lemma vars_monom_subset:
shows "vars (monom m a) ⊆ keys m"
  by (cases "a=0"; simp add: vars_def vars_monom_keys)

lemma vars_monom_single_cases: "vars (monom (Poly_Mapping.single v k) a) = (if k=0 ∨ a=0 then {} else {v})"
proof(cases "k=0")
  assume "k=0"
  then have "(Poly_Mapping.single v k) = 0" by simp
  then have "vars (monom (Poly_Mapping.single v k) a) = {}"
    by (metis (mono_tags, lifting) single_zero singleton_inject subset_singletonD vars_monom_single zero_neq_one)
  then show ?thesis using ‹k=0› by auto
next
  assume "k≠0"
  then show ?thesis
  proof (cases "a=0")
    assume "a=0"
    then have "monom (Poly_Mapping.single v k) a = 0" by (metis monom.abs_eq monom_zero single_zero)
    then show ?thesis by (metis (mono_tags, opaque_lifting) ‹k ≠ 0› ‹a=0› monom.abs_eq single_zero singleton_inject subset_singletonD vars_monom_single)
  next
    assume "a≠0"
    then have "v ∈ vars (monom (Poly_Mapping.single v k) a)" by (simp add: ‹k ≠ 0› vars_def)
    then show ?thesis using ‹a≠0› ‹k ≠ 0› vars_monom_single by fastforce
  qed
qed

lemma vars_monom:
assumes "a≠0"
shows "vars (monom m (1::'a::zero_neq_one)) = vars (monom m (a::'a))"
  unfolding vars_monom_keys[OF assms] using vars_monom_keys[of 1] one_neq_zero by blast

lemma vars_add: "vars (p1 + p2) ⊆ vars p1 ∪ vars p2"
proof
  fix w assume "w ∈ vars (p1 + p2)"
  then obtain m where "w ∈ keys m" "m ∈ keys (mapping_of (p1 + p2))" by (metis UN_E vars_def)
  then have "m ∈ keys (mapping_of (p1)) ∪ keys (mapping_of (p2))"
    by (metis Poly_Mapping.keys_add plus_mpoly.rep_eq subset_iff)
  then show "w ∈ vars p1 ∪ vars p2" using vars_def ‹w ∈ keys m› by fastforce
qed

lemma vars_mult: "vars (p*q) ⊆ vars p ∪ vars q"
proof
  fix x assume "x∈vars (p*q)"
  then obtain m where "m∈keys (mapping_of (p*q))" "x∈keys m"
    using vars_def  by blast
  then have "m∈keys (mapping_of p * mapping_of q)"
    by (simp add: times_mpoly.rep_eq)
  then obtain a b where "m=a + b" "a ∈ keys (mapping_of p)" "b ∈ keys (mapping_of q)"
    using keys_mult by blast
  then have "x ∈ keys a ∪ keys b"
    using Poly_Mapping.keys_add ‹x ∈ keys m› by force
  then show "x ∈ vars p ∪ vars q" unfolding vars_def
    using ‹a ∈ keys (mapping_of p)› ‹b ∈ keys (mapping_of q)› by blast
qed

lemma vars_add_monom:
assumes "p2 = monom m a" "m ∉ keys (mapping_of p1)"
shows "vars (p1 + p2) = vars p1 ∪ vars p2"
proof -
  have "keys (mapping_of p2) ⊆ {m}" using monom_def keys_single assms by auto
  have "keys (mapping_of (p1+p2)) = keys (mapping_of p1) ∪ keys (mapping_of p2)"
    using keys_add by (metis Int_insert_right_if0 ‹keys (mapping_of p2) ⊆ {m}› assms(2) inf_bot_right plus_mpoly.rep_eq subset_singletonD)
  then show ?thesis unfolding vars_def by simp
qed

lemma vars_setsum: "finite S ⟹ vars (∑m∈S. f m) ⊆ (⋃m∈S. vars (f m))"
proof (induction S rule:finite_induct)
  case empty
  then show ?case by (metis UN_empty eq_iff monom_zero sum.empty single_zero vars_monom_single_cases)
next
  case (insert s S)
  then have "vars (sum f (insert s S)) = vars (f s + sum f S)" by (metis sum.insert)
  also have "... ⊆ vars (f s) ∪ vars (sum f S)" by (simp add: vars_add)
  also have "... ⊆ (⋃m∈insert s S. vars (f m))" using insert.IH by auto
  finally show ?case by metis
qed

lemma coeff_monom: "coeff (monom m a) m' = (a when m'=m)"
  by (simp add: coeff_def lookup_single_not_eq when_def)

lemma coeff_add: "coeff p m + coeff q m = coeff (p+q) m"
  by (simp add: coeff_def lookup_add plus_mpoly.rep_eq)

lemma coeff_eq: "coeff p = coeff q ⟷ p=q" by (simp add: coeff_def lookup_inject mapping_of_inject)

lemma coeff_monom_mult: "coeff ((monom m' a)  * q) (m' + m)  = a * coeff q m"
  unfolding coeff_def times_mpoly.rep_eq lookup_mult mapping_of_monom lookup_single when_mult
  Sum_any_when_equal' Groups.cancel_semigroup_add_class.add_left_cancel by metis

lemma one_term_is_monomial:
assumes "card (keys (mapping_of p)) ≤ 1"
obtains m where "p = monom m (coeff p m)"
proof (cases "keys (mapping_of p) = {}")
  case True
  then show ?thesis using aux coeff_def empty_iff mapping_of_inject mapping_of_monom not_in_keys_iff_lookup_eq_zero single_zero by (metis (no_types) that)
next
  case False
  then obtain m where "keys (mapping_of p) = {m}" using assms by (metis One_nat_def Suc_leI antisym card_0_eq card_eq_SucD finite_keys neq0_conv)
  have "p = monom m (coeff p m)"
    unfolding mapping_of_inject[symmetric]
    by (rule poly_mapping_eqI, metis (no_types, lifting) ‹keys (mapping_of p) = {m}›
    coeff_def keys_single lookup_single_eq  mapping_of_monom not_in_keys_iff_lookup_eq_zero
    singletonD)
  then show ?thesis ..
qed

(* remove_term is eventually unnessecary *)
definition remove_term::"(nat ⇒⇩0 nat) ⇒ 'a::zero mpoly ⇒ 'a mpoly" where
  "remove_term m0 p = MPoly (Abs_poly_mapping (λm. coeff p m when m ≠ m0))"

lemma remove_term_coeff: "coeff (remove_term m0 p) m = (coeff p m when m ≠ m0)"
proof -
  have "{m. (coeff p m when m ≠ m0) ≠ 0} ⊆ {m. coeff p m ≠ 0}" by auto
  then have "finite {m. (coeff p m when m ≠ m0) ≠ 0}" unfolding coeff_def using finite_subset by auto
  then have "lookup (Abs_poly_mapping (λm. coeff p m when m ≠ m0)) m = (coeff p m when m ≠ m0)" using lookup_Abs_poly_mapping by fastforce
  then show ?thesis unfolding remove_term_def using coeff_def by (metis (mono_tags, lifting) Quotient_mpoly Quotient_rep_abs_fold_unmap)
qed

lemma coeff_keys: "m ∈ keys (mapping_of p) ⟷ coeff p m ≠ 0"
  by (simp add: coeff_def in_keys_iff)

lemma remove_term_keys:
shows "keys (mapping_of p) - {m} = keys (mapping_of (remove_term m p))" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix m' assume "m'∈?A"
    then show "m' ∈ ?B" by (simp add: coeff_keys remove_term_coeff)
  qed
  show "?B ⊆ ?A"
  proof
    fix m' assume "m'∈ ?B"
    then show "m' ∈ ?A" by (simp add: coeff_keys remove_term_coeff)
  qed
qed


lemma remove_term_sum: "remove_term m p + monom m (coeff p m) = p"
proof -
  have "coeff p = (λm'. (coeff p m' when m' ≠ m) + ((coeff p m) when m'=m))" unfolding when_def by fastforce
  moreover have "coeff (remove_term m p + monom m (coeff p m)) = ..."
    using remove_term_coeff coeff_monom coeff_add by (metis (no_types))
  ultimately show ?thesis using coeff_eq by auto
qed

lemma mpoly_induct [case_names monom sum]:
assumes monom:"⋀m a. P (monom m a)"
and sum:"(⋀p1 p2 m a. P p1 ⟹ P p2 ⟹ p2 = (monom m a) ⟹ m ∉ keys (mapping_of p1) ⟹ P (p1+p2))"
shows "P p" using assms
  using poly_mapping_induct[of "λp :: (nat ⇒⇩0 nat) ⇒⇩0 'a. P (MPoly p)"] MPoly_induct monom.abs_eq plus_mpoly.abs_eq
  by (metis (no_types) MPoly_inverse UNIV_I)

lemma monom_pow:"monom (Poly_Mapping.single v n0) a ^ n = monom (Poly_Mapping.single v (n0*n)) (a ^ n)"
apply (induction n)
apply auto
by (metis (no_types, lifting) mult_monom single_add)

lemma insertion_fun_single: "insertion_fun f (λm. (a when (Poly_Mapping.single (v::nat) (n::nat)) = m)) = a * f v ^ n" (is "?i = _")
proof -
  have setsum_single:"⋀ a f. (∑m∈{a}. f m) = f a"
   by (metis add.right_neutral empty_Diff finite.emptyI sum.empty sum.insert_remove)

  have 1:"?i = (∑m. (a when Poly_Mapping.single v n = m) * (∏v. f v ^ lookup m v))"
    unfolding insertion_fun_def by metis
  have "∀m. m ≠ Poly_Mapping.single v n ⟶ (a when Poly_Mapping.single v n = m) = 0" by simp

  have "(∑m∈{Poly_Mapping.single v n}. (a when Poly_Mapping.single v n = m) * (∏v. f v ^ lookup m v)) = ?i"
    unfolding 1 when_mult unfolding when_def by auto
  then have 2:"?i = a * (∏va. f va ^ lookup (Poly_Mapping.single v n) va)"
    unfolding setsum_single[of "λm. (a when Poly_Mapping.single v n = m) * (∏v. f v ^ lookup m v)" "Poly_Mapping.single k v"]
    by auto
  have "∀v0. v0≠v ⟶ lookup (Poly_Mapping.single v n) v0 = 0" by (simp add: lookup_single_not_eq)
  then have "∀va. va≠v ⟶ f va ^ lookup (Poly_Mapping.single v n) va = 1"  by simp
  then have "a * (∏va∈{v}. f va ^ lookup (Poly_Mapping.single v n) va) = ?i" unfolding 2
    using Prod_any.expand_superset[of "{v}" "λva. f va ^ lookup (Poly_Mapping.single v n) va", simplified]
    by fastforce
  then show ?thesis by simp
qed

lemma insertion_single[simp]: "insertion f (monom (Poly_Mapping.single (v::nat) (n::nat)) a) = a * f v ^ n"
  using insertion_fun_single  Sum_any.cong insertion.rep_eq insertion_aux.rep_eq insertion_fun_def
  mapping_of_monom single.rep_eq by (metis (no_types, lifting))

lemma insertion_fun_irrelevant_vars:
fixes p::"((nat ⇒⇩0 nat) ⇒ 'a::comm_ring_1)"
assumes "⋀m v. p m ≠ 0 ⟹ lookup m v ≠ 0 ⟹ f v = g v"
shows "insertion_fun f p = insertion_fun g p"
proof -
  {
    fix m::"nat⇒⇩0nat"
    assume "p m ≠ 0"
    then have "(∏v. f v ^ lookup m v) = (∏v. g v ^ lookup m v)"
      using assms by (metis power_0)
  }
  then show ?thesis unfolding insertion_fun_def by (metis (no_types, lifting) mult_not_zero)
qed

lemma insertion_aux_irrelevant_vars:
fixes p::"((nat ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1)"
assumes "⋀m v. lookup p m ≠ 0 ⟹ lookup m v ≠ 0 ⟹ f v = g v"
shows "insertion_aux f p = insertion_aux g p"
  using insertion_fun_irrelevant_vars[of "lookup p" f g] assms
  by (metis insertion_aux.rep_eq)

lemma insertion_irrelevant_vars:
fixes p::"'a::comm_ring_1 mpoly"
assumes "⋀v. v∈vars p ⟹ f v = g v"
shows "insertion f p = insertion g p"
proof -
  {
    fix m v assume "lookup (mapping_of p) m ≠ 0" "lookup m v ≠ 0"
    then have "v ∈ vars p" unfolding vars_def by (meson UN_I lookup_not_eq_zero_eq_in_keys)
    then have "f v = g v" using assms by auto
  }
  then show ?thesis
    unfolding insertion_def using insertion_aux_irrelevant_vars[of "mapping_of p"]
    by (metis insertion.rep_eq insertion_def)
qed

section "Nested MPoly"

definition reduce_nested_mpoly::"'a::comm_ring_1 mpoly mpoly ⇒ 'a mpoly" where
  "reduce_nested_mpoly pp = insertion (λv. monom (Poly_Mapping.single v 1) 1) pp"

lemma reduce_nested_mpoly_sum:
fixes p1::"'a::comm_ring_1 mpoly mpoly"
shows "reduce_nested_mpoly (p1 + p2) = reduce_nested_mpoly p1 + reduce_nested_mpoly p2"
  by (simp add: insertion_add reduce_nested_mpoly_def)

lemma reduce_nested_mpoly_prod:
fixes p1::"'a::comm_ring_1 mpoly mpoly"
shows "reduce_nested_mpoly (p1 * p2) = reduce_nested_mpoly p1 * reduce_nested_mpoly p2"
  by (simp add: insertion_mult reduce_nested_mpoly_def)

lemma reduce_nested_mpoly_0:
shows "reduce_nested_mpoly 0 = 0" by (simp add: reduce_nested_mpoly_def)

lemma insertion_nested_poly:
fixes pp::"'a::comm_ring_1 mpoly mpoly"
shows "insertion f (insertion (λv. monom 0 (f v)) pp) = insertion f (reduce_nested_mpoly pp)"
proof (induction pp rule:mpoly_induct)
  case (monom m a)
  then show ?case
  proof (induction m arbitrary:a rule:poly_mapping_induct)
    case (single v n)
    show ?case unfolding reduce_nested_mpoly_def
      apply (simp add: insertion_mult monom_pow)
      using monom_pow[of 0 0 "f v" n] apply simp
      using insertion_single[of f 0 0] by auto
  next
    case (sum m1 m2 k v)
    then have "insertion f (insertion (λv. monom 0 (f v)) (monom m1 a * monom m2 1))
             = insertion f (reduce_nested_mpoly (monom m1 a * monom m2 1))" unfolding reduce_nested_mpoly_prod insertion_mult by metis
    then show ?case using mult_monom[of m1 a m2 1] by auto
  qed
next
  case (sum p1 p2 m a)
  then show ?case by (simp add: reduce_nested_mpoly_sum insertion_add)
qed

definition extract_var::"'a::comm_ring_1 mpoly ⇒ nat ⇒ 'a::comm_ring_1 mpoly mpoly" where
"extract_var p v = (∑m. monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"

lemma extract_var_finite_set:
assumes "{m'. coeff p m' ≠ 0} ⊆ S"
assumes "finite S"
shows "extract_var p v = (∑m∈S. monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"
proof-
  {
    fix m' assume "coeff p m' = 0"
    then have "monom (remove_key v m') (monom (Poly_Mapping.single v (lookup m' v)) (coeff p m')) = 0"
      using monom.abs_eq monom_zero single_zero by metis
  }
  then have 0:"{a. monom (remove_key v a) (monom (Poly_Mapping.single v (lookup a v)) (coeff p a)) ≠ 0} ⊆ S"
    using ‹{m'. coeff p m' ≠ 0} ⊆ S› by fastforce
  then show ?thesis
    unfolding extract_var_def using Sum_any.expand_superset [OF ‹finite S› 0] by metis
qed

lemma extract_var_non_zero_coeff: "extract_var p v = (∑m∈{m'. coeff p m' ≠ 0}. monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"
  using extract_var_finite_set  coeff_def finite_lookup order_refl by (metis (no_types, lifting) Collect_cong sum.cong)

lemma extract_var_sum: "extract_var (p+p') v = extract_var p v + extract_var p' v"
proof -
  define S where "S = {m. coeff p m ≠ 0} ∪ {m. coeff p' m ≠ 0} ∪ {m. coeff (p+p') m ≠ 0}"
  have subsets:"{m. coeff p m ≠ 0} ⊆ S" "{m. coeff p' m ≠ 0} ⊆ S" "{m. coeff (p+p') m ≠ 0} ⊆ S"
    unfolding S_def by auto
  have "finite S" unfolding S_def using coeff_def finite_lookup
    by (metis (mono_tags) Collect_disj_eq finite_Collect_disjI)
  then show ?thesis  unfolding
    extract_var_finite_set[OF subsets(1) ‹finite S›]
    extract_var_finite_set[OF subsets(2) ‹finite S›]
    extract_var_finite_set[OF subsets(3) ‹finite S›]
    coeff_add[symmetric] monom_add sum.distrib
    by metis
qed



lemma extract_var_monom:
shows "extract_var (monom m a) v = monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) a)"
proof (cases "a = 0")
  assume "a ≠ 0"
  have 0:"{m'. coeff (monom m a) m' ≠ 0} = {m}"
    unfolding coeff_monom using ‹a ≠ 0› by auto
  show ?thesis
    unfolding extract_var_non_zero_coeff unfolding 0 unfolding coeff_monom
    using sum.insert[OF finite.emptyI, unfolded sum.empty add.right_neutral] when_def
    by auto
next
  assume "a = 0"
  have 0:"{m'. coeff (monom m a) m' ≠ 0} = {}"
    unfolding coeff_monom using ‹a = 0› by auto
  show ?thesis unfolding extract_var_non_zero_coeff 0
    using ‹a = 0› monom.abs_eq monom_zero sum.empty single_zero by (metis (no_types, lifting))
qed


lemma extract_var_monom_mult:
shows "extract_var (monom (m+m') (a*b)) v = extract_var (monom m a) v * extract_var (monom m' b) v"
unfolding extract_var_monom remove_key_add lookup_add single_add mult_monom by auto

lemma extract_var_single: "extract_var (monom (Poly_Mapping.single v n) a) v = monom 0 (monom (Poly_Mapping.single v n) a)"
unfolding extract_var_monom by simp

lemma extract_var_single':
assumes "v ≠ v'"
shows "extract_var (monom (Poly_Mapping.single v n) a) v' = monom (Poly_Mapping.single v n) (monom 0 a)"
unfolding extract_var_monom using assms by (metis add.right_neutral lookup_single_not_eq remove_key_sum single_zero)

lemma reduce_nested_mpoly_extract_var:
fixes p::"'a::comm_ring_1 mpoly"
shows "reduce_nested_mpoly (extract_var p v) = p"
proof (induction p rule:mpoly_induct)
  case (monom m a)
  then show ?case
  proof (induction m arbitrary:a rule:poly_mapping_induct)
    case (single v' n)
    show ?case
    proof (cases "v' = v")
      case True
      then show ?thesis
        by (metis (no_types, lifting) insertion_single mult.right_neutral power_0
        reduce_nested_mpoly_def single_zero extract_var_single)
    next
      case False
      then show ?thesis unfolding extract_var_single'[OF False] reduce_nested_mpoly_def insertion_single
        by (simp add: monom_pow mult_monom)
    qed
  next
    case (sum m m' v n a)
    then show ?case
      using extract_var_monom_mult[of m m' a 1] reduce_nested_mpoly_prod by (metis mult.right_neutral mult_monom)
  qed
next
  case (sum p1 p2 m a)
  then show ?case unfolding extract_var_sum reduce_nested_mpoly_sum by auto
qed


lemma vars_extract_var_subset: "vars (extract_var p v) ⊆ vars p"
proof
  have "finite {m'. coeff p m' ≠ 0}" by (simp add: coeff_def)
  fix x assume "x ∈ vars (extract_var p v)"
  then have "x ∈ vars (∑m∈{m'. coeff p m' ≠ 0}. monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"
    unfolding extract_var_non_zero_coeff by metis
  then have "x ∈ (⋃m∈{m'. coeff p m' ≠ 0}. vars (monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m))))"
    using vars_setsum[OF ‹finite {m'. coeff p m' ≠ 0}›] by auto
  then obtain m where "m∈{m'. coeff p m' ≠ 0}" "x ∈ vars (monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"
    by blast
  show "x ∈ vars p" by (metis (mono_tags, lifting) DiffD1 UN_I ‹m ∈ {m'. coeff p m' ≠ 0}›
    ‹x ∈ vars (monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))›
    coeff_keys mem_Collect_eq remove_key_keys subsetCE vars_def vars_monom_subset)
qed

lemma v_not_in_vars_extract_var: "v ∉ vars (extract_var p v)"
proof -
  have "finite {m'. coeff p m' ≠ 0}" by (simp add: coeff_def)
  have "⋀m. m∈{m'. coeff p m' ≠ 0} ⟹ v ∉ vars (monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m)))"
    by (metis Diff_iff remove_key_keys singletonI subsetCE vars_monom_subset)
  then have "v ∉ (⋃m∈{m'. coeff p m' ≠ 0}. vars (monom (remove_key v m) (monom (Poly_Mapping.single v (lookup m v)) (coeff p m))))"
    by simp
  then show ?thesis
   unfolding extract_var_non_zero_coeff using vars_setsum[OF ‹finite {m'. coeff p m' ≠ 0}›] by blast
qed

lemma vars_coeff_extract_var: "vars (coeff (extract_var p v) j) ⊆ {v}"
proof (induction p rule:mpoly_induct)
  case (monom m a)
  then show ?case unfolding extract_var_monom coeff_monom vars_monom_single_cases
    by (metis monom_zero single_zero vars_monom_single when_def)
next
  case (sum p1 p2 m a)
  then show ?case unfolding extract_var_sum coeff_add[symmetric]
    by (metis (no_types, lifting) Un_insert_right insert_absorb2 subset_insertI2 subset_singletonD sup_bot.right_neutral vars_add)
qed

definition replace_coeff
where "replace_coeff f p = MPoly (Abs_poly_mapping (λm. f (lookup (mapping_of p) m)))"

lemma coeff_replace_coeff:
assumes "f 0 = 0"
shows "coeff (replace_coeff f p) m = f (coeff p m)"
proof -
  have 0:"finite {m. f (lookup (mapping_of p) m) ≠ 0}"
    unfolding coeff_def[symmetric] by (metis (mono_tags, lifting) Collect_mono assms(1) coeff_def finite_lookup finite_subset)+
  then show ?thesis unfolding replace_coeff_def coeff_def using lookup_Abs_poly_mapping[OF 0]
    by (metis (mono_tags, lifting) Quotient_mpoly Quotient_rep_abs_fold_unmap)
qed

lemma replace_coeff_monom:
assumes "f 0 = 0"
shows "replace_coeff f (monom m a) = monom m (f a)"
  unfolding replace_coeff_def
  unfolding  mapping_of_inject[symmetric] lookup_inject[symmetric] apply (rule HOL.ext)
  unfolding lookup_single  mapping_of_monom fun_when[of f, OF ‹f 0 = 0›]
  by (metis coeff_def coeff_monom lookup_single lookup_single_not_eq monom.abs_eq single.abs_eq)

lemma replace_coeff_add:
assumes "f 0 = 0"
assumes "⋀a b. f (a+b) = f a + f b"
shows "replace_coeff f (p1 + p2) = replace_coeff f p1 + replace_coeff f p2"
proof -
  have "finite {m. f (lookup (mapping_of p1) m) ≠ 0}"
       "finite {m. f (lookup (mapping_of p2) m) ≠ 0}"
    unfolding coeff_def[symmetric] by (metis (mono_tags, lifting) Collect_mono assms(1) coeff_def finite_lookup finite_subset)+
  then show ?thesis
    unfolding replace_coeff_def plus_mpoly.rep_eq unfolding Poly_Mapping.plus_poly_mapping.rep_eq
    unfolding assms(2) plus_mpoly.abs_eq using Poly_Mapping.plus_poly_mapping.abs_eq[unfolded eq_onp_def] by fastforce
qed

lemma insertion_replace_coeff:
fixes pp::"'a::comm_ring_1 mpoly mpoly"
shows "insertion f (replace_coeff (insertion f) pp) = insertion f (reduce_nested_mpoly pp)"
proof (induction pp rule:mpoly_induct)
  case (monom m a)
  then show ?case
  proof (induction m arbitrary:a rule:poly_mapping_induct)
    case (single v n)
    show ?case unfolding reduce_nested_mpoly_def  unfolding replace_coeff_monom[of "insertion f", OF insertion_zero]
      insertion_single insertion_mult using insertion_single by (simp add: monom_pow)
  next
    case (sum m1 m2 k v)
    have "replace_coeff (insertion f) (monom m1 a * monom m2 1) = replace_coeff (insertion f) (monom m1 a) * replace_coeff (insertion f) (monom m2 1)"
      by (simp add: mult_monom replace_coeff_monom)
    then have "insertion f (replace_coeff (insertion f) (monom m1 a * monom m2 1)) = insertion f (reduce_nested_mpoly (monom m1 a * monom m2 1))"
      unfolding reduce_nested_mpoly_prod insertion_mult
      by (simp add: insertion_mult sum.IH(1) sum.IH(2))
    then show ?case using mult_monom[of m1 a m2 1] by auto
  qed
next
  case (sum p1 p2 m a)
  then show ?case using reduce_nested_mpoly_sum insertion_add
    replace_coeff_add[of "insertion f", OF insertion_zero insertion_add] by metis
qed

lemma replace_coeff_extract_var_cong:
assumes "f v = g v"
shows "replace_coeff (insertion f) (extract_var p v) = replace_coeff (insertion g) (extract_var p v)"
  by (induction p rule:mpoly_induct;simp add: assms extract_var_monom replace_coeff_monom
  extract_var_sum insertion_add replace_coeff_add)

lemma vars_replace_coeff:
assumes "f 0 = 0"
shows "vars (replace_coeff f p) ⊆ vars p"
  unfolding vars_def apply (rule subsetI) unfolding mem_simps(8) coeff_keys
  using assms coeff_replace_coeff by (metis coeff_keys)

(* Polynomial functions *)

definition polyfun :: "nat set ⇒ ((nat ⇒ 'a::comm_semiring_1) ⇒ 'a) ⇒ bool"
  where "polyfun N f = (∃p. vars p ⊆ N ∧ (∀x. insertion x p = f x))"

lemma polyfunI: "(⋀P. (⋀p. vars p ⊆ N ⟹ (⋀x. insertion x p = f x) ⟹ P) ⟹ P) ⟹ polyfun N f"
  unfolding polyfun_def by metis

lemma polyfun_subset: "N⊆N' ⟹ polyfun N f ⟹ polyfun N' f"
  unfolding polyfun_def by blast

lemma polyfun_const: "polyfun N (λ_. c)"
proof -
  have "⋀x. insertion x (monom 0 c) = c" using insertion_single by (metis insertion_one monom_one mult.commute mult.right_neutral single_zero)
  then show ?thesis unfolding polyfun_def by (metis (full_types) empty_iff keys_single single_zero subsetI subset_antisym vars_monom_subset)
qed

lemma polyfun_add:
assumes "polyfun N f" "polyfun N g"
shows "polyfun N (λx. f x + g x)"
proof -
  obtain p1 p2 where "vars p1 ⊆ N" "∀x. insertion x p1 = f x"
                     "vars p2 ⊆ N" "∀x. insertion x p2 = g x"
    using polyfun_def assms by metis
  then have "vars (p1 + p2) ⊆ N" "∀x. insertion x (p1 + p2) = f x + g x"
    using vars_add using Un_iff subsetCE subsetI apply blast
    by (simp add: ‹∀x. insertion x p1 = f x› ‹∀x. insertion x p2 = g x› insertion_add)
  then show ?thesis using polyfun_def by blast
qed

lemma polyfun_mult:
assumes "polyfun N f" "polyfun N g"
shows "polyfun N (λx. f x * g x)"
proof -
  obtain p1 p2 where "vars p1 ⊆ N" "∀x. insertion x p1 = f x"
                     "vars p2 ⊆ N" "∀x. insertion x p2 = g x"
    using polyfun_def assms by metis
  then have "vars (p1 * p2) ⊆ N" "∀x. insertion x (p1 * p2) = f x * g x"
    using vars_mult using Un_iff subsetCE subsetI apply blast
    by (simp add: ‹∀x. insertion x p1 = f x› ‹∀x. insertion x p2 = g x› insertion_mult)
  then show ?thesis using polyfun_def by blast
qed

lemma polyfun_Sum:
assumes "finite I"
assumes "⋀i. i∈I ⟹ polyfun N (f i)"
shows "polyfun N (λx. ∑i∈I. f i x)"
  using assms
  apply (induction I rule:finite_induct)
  apply (simp add: polyfun_const)
  using comm_monoid_add_class.sum.insert polyfun_add by fastforce

lemma polyfun_Prod:
assumes "finite I"
assumes "⋀i. i∈I ⟹ polyfun N (f i)"
shows "polyfun N (λx. ∏i∈I. f i x)"
  using assms
  apply (induction I rule:finite_induct)
  apply (simp add: polyfun_const)
  using comm_monoid_add_class.sum.insert polyfun_mult by fastforce

lemma polyfun_single:
assumes "i∈N"
shows "polyfun N (λx. x i)"
proof -
  have "∀f. insertion f (monom (Poly_Mapping.single i 1) 1) = f i" using insertion_single by simp
  then show ?thesis unfolding polyfun_def
    using vars_monom_single[of i 1 1] One_nat_def assms singletonD subset_eq
    by blast
qed

end