Theory 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 xS)) = (λx. f x when xS)"
proof -
  have "finite {x. (f x when xS)  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 "xkeys 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 "xkeys (f+g)" using xkeys f by (metis not_in_keys_iff_lookup_eq_zero)
  qed
  moreover have "keys g  keys (f+g)"
  proof
    fix x assume "xkeys 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 "xkeys (f+g)" using xkeys 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 "a0"
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 "k0"
  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 "a0"
    then have "v  vars (monom (Poly_Mapping.single v k) a)" by (simp add: k  0 vars_def)
    then show ?thesis using a0 k  0 vars_monom_single by fastforce
  qed
qed

lemma vars_monom:
assumes "a0"
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 "xvars (p*q)"
  then obtain m where "mkeys (mapping_of (p*q))" "xkeys m"
    using vars_def  by blast
  then have "mkeys (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 (mS. f m)  (mS. 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 "...  (minsert 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. v0v  lookup (Poly_Mapping.single v n) v0 = 0" by (simp add: lookup_single_not_eq)
  then have "va. vav  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::"nat0nat"
    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. vvars 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 = (mS. 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: "NN'  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. iI  polyfun N (f i)"
shows "polyfun N (λx. iI. 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. iI  polyfun N (f i)"
shows "polyfun N (λx. iI. 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 "iN"
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