Theory Preliminaries_on_Polynomials_1

section ‹Preliminaries: Extending the Library on Multivariate Polynomials›

subsection ‹Part 1 -- Extensions Without Importing Univariate Polynomials›

theory Preliminaries_on_Polynomials_1
  imports 
    Polynomials.More_MPoly_Type
    Polynomials.MPoly_Type_Class_Finite_Map
begin

type_synonym var = nat
type_synonym monom = "var ⇒⇩0 nat" 

definition substitute :: "(var ⇒ 'a mpoly) ⇒ 'a :: comm_semiring_1 mpoly ⇒ 'a mpoly" where
  "substitute σ p = insertion σ (replace_coeff Const p)" 

lemma Const_0: "Const 0 = 0"
  by (transfer, simp add: Const⇩0_zero)

lemma Const_1: "Const 1 = 1"
  by (transfer, simp add: Const⇩0_one)

lemma insertion_Var: "insertion α (Var x) = α x" 
  apply transfer
  by (metis One_nat_def Var⇩0_def insertion.abs_eq insertion_single mapping_of_inverse monom.rep_eq mult.right_neutral mult_1 power.simps(2) power_0)

lemma insertion_Const: "insertion α (Const a) = a"
  by (metis Const.abs_eq Const⇩0_def insertion_single monom.abs_eq mult.right_neutral power_0 single_zero)

lemma insertion_power: "insertion α (p^n) = (insertion α p)^n" 
  by (induct n, auto simp: insertion_mult)

lemma insertion_monom_add: "insertion α (monom (f + g) a) = insertion α (monom f 1) * insertion α (monom g a)" 
  by (metis insertion_mult mult_1 mult_monom)

lemma insertion_uminus: "insertion α (- p) = - insertion α p"
  by (metis add_eq_0_iff insertion_add insertion_zero)

lemma insertion_sum_list: "insertion α (sum_list ps) = sum_list (map (insertion α) ps)" 
  by (induct ps, auto simp: insertion_add)

lemma coeff_uminus: "coeff (- p) m = - coeff p m"
  by (simp add: coeff_def uminus_mpoly.rep_eq)

lemma insertion_substitute: "insertion α (substitute σ p) = insertion (λ x. insertion α (σ x)) p" 
  unfolding substitute_def
proof (induct p rule: mpoly_induct)
  case (monom m a)
  show ?case 
    apply (subst replace_coeff_monom)
    subgoal by (simp add: Const_0)
    subgoal proof (induct m arbitrary: a rule: poly_mapping_induct)
      case (single k v)
      show ?case by (simp add: insertion_mult insertion_Const insertion_power)  
    next
      case (sum f g k v a)
      from sum(1)[of 1] sum(2)[of a] show ?case 
        by (simp add: insertion_monom_add insertion_mult Const_1)
    qed
    done
next
  case (sum p1 p2 m a)
  then show ?case 
    apply (subst replace_coeff_add)
    subgoal by (simp add: Const_0)
    subgoal by (transfer', simp add: Const⇩0_def single_add)
    by (simp add: insertion_add)
qed

lemma Const_add: "Const (x + y) = Const x + Const y" 
  by (transfer, auto simp: Const⇩0_def single_add)

lemma substitute_add[simp]: "substitute σ (p + q) = substitute σ p + substitute σ q" 
  unfolding substitute_def insertion_add[symmetric] 
  by (subst replace_coeff_add, auto simp: Const_0 Const_add)

lemma Const_sum: "Const (sum f A) = sum (Const o f) A"
  by (metis Const_0 Const_add sum_comp_morphism)

lemma Const_sum_list: "Const (sum_list (map f xs)) = sum_list (map (Const o f) xs)"
  by (induct xs, auto simp: Const_0 Const_add)

lemma Const_0_eq[simp]: "Const x = 0 ⟷ x = 0" 
  by (smt (verit) Const.abs_eq Const⇩0_def coeff_monom monom.abs_eq single_zero when_def zero_mpoly_def)

lemma Const_sum_any: "Const (Sum_any f) = Sum_any (Const o f)"
  unfolding Sum_any.expand_set Const_sum o_def
  by (intro sum.cong[OF _ refl], auto simp: Const_0)

lemma Const_mult: "Const (x * y) = Const x * Const y"
  by (metis Const.abs_eq Const⇩0_def monom.abs_eq smult_conv_mult smult_monom)

lemma Const_power: "Const (x ^ e) = Const x ^ e" 
  by (induct e, auto simp: Const_1 Const_mult)

lemma lookup_replace_Const: "lookup (mapping_of (replace_coeff Const p)) l = Const (lookup (mapping_of p) l)" 
  by (metis Const_0 coeff_def coeff_replace_coeff)

lemma replace_coeff_mult: "replace_coeff Const (p * q) = replace_coeff Const p * replace_coeff Const q" 
  apply (subst coeff_eq[symmetric], intro ext, subst coeff_replace_coeff, rule Const_0)
  apply (unfold coeff_def)
  apply (unfold times_mpoly.rep_eq)
  apply (unfold Poly_Mapping.lookup_mult)
  apply (unfold Const_sum_any o_def Const_mult lookup_replace_Const)
  apply (unfold when_def if_distrib Const_0)
  by auto


lemma substitute_mult[simp]: "substitute σ (p * q) = substitute σ p * substitute σ q" 
  unfolding substitute_def insertion_mult[symmetric] replace_coeff_mult ..

lemma replace_coeff_Var[simp]: "replace_coeff Const (Var x) = Var x"
  by (metis Const_0 Const_1 Var.abs_eq Var⇩0_def monom.abs_eq replace_coeff_monom)

lemma replace_coeff_Const[simp]: "replace_coeff Const (Const c) = Const (Const c)" 
  by (metis Const.abs_eq Const⇩0_def Const_0 monom.abs_eq replace_coeff_monom)

lemma substitute_Var[simp]: "substitute σ (Var x) = σ x" 
  unfolding substitute_def by (simp add: insertion_Var)

lemma substitute_Const[simp]: "substitute σ (Const c) = Const c" 
  unfolding substitute_def by (simp add: insertion_Const)

lemma substitute_0[simp]: "substitute σ 0 = 0" 
  using substitute_Const[of σ 0, unfolded Const_0] .

lemma substitute_1[simp]: "substitute σ 1 = 1" 
  using substitute_Const[of σ 1, unfolded Const_1] .

lemma substitute_power[simp]: "substitute σ (p^e) = (substitute σ p)^e" 
  by (induct e, auto)

lemma substitute_monom[simp]: "substitute σ (monom (monomial e x) c) = Const c * (σ x)^e" 
  by (simp add: replace_coeff_monom substitute_def)

lemma substitute_sum_list: "substitute σ (sum_list (map f xs)) = sum_list (map (substitute σ o f) xs)"
  by (induct xs, auto)

lemma substitute_sum: "substitute σ (sum f xs) = sum (substitute σ o f) xs"
  by (induct xs rule: infinite_finite_induct, auto)

lemma substitute_prod: "substitute σ (prod f xs) = prod (substitute σ o f) xs"
  by (induct xs rule: infinite_finite_induct, auto)

definition vars_list where "vars_list = sorted_list_of_set o vars" 

lemma set_vars_list[simp]: "set (vars_list p) = vars p" 
  unfolding vars_list_def o_def using vars_finite[of p] by auto

lift_definition mpoly_coeff_filter :: "('a :: zero ⇒ bool) ⇒ 'a mpoly ⇒ 'a mpoly" is
  "λ f p. Poly_Mapping.mapp (λ m c. c when f c) p" .

lemma mpoly_coeff_filter: "coeff (mpoly_coeff_filter f p) m = (coeff p m when f (coeff p m))" 
  unfolding coeff_def by transfer (simp add: in_keys_iff mapp.rep_eq)

lemma total_degree_add: assumes "total_degree p ≤ d" "total_degree q ≤ d" 
  shows "total_degree (p + q) ≤ d" 
  using assms
proof transfer
  fix d and p q :: "(nat ⇒⇩0 nat) ⇒⇩0 'a" 
  let ?exp = "λ p. Max (insert (0 :: nat) ((λm. sum (lookup m) (keys m)) ` keys p))" 
  assume d: "?exp p ≤ d" "?exp q ≤ d" 
  have "?exp (p + q) ≤ Max (insert (0 :: nat) ((λm. sum (lookup m) (keys m)) ` (keys p ∪ keys q)))" 
    using Poly_Mapping.keys_add[of p q]
    by (intro Max_mono, auto)
  also have "… = max (?exp p) (?exp q)" 
    by (subst Max_Un[symmetric], auto simp: image_Un)
  also have "… ≤ d" using d by auto
  finally show "?exp (p + q) ≤ d" .
qed

lemma total_degree_Var[simp]: "total_degree (Var x :: 'a :: comm_semiring_1 mpoly) = Suc 0" 
  by (transfer, auto simp: Var⇩0_def)

lemma total_degree_Const[simp]: "total_degree (Const x) = 0" 
  by (transfer, auto simp: Const⇩0_def)

lemma total_degree_Const_mult: assumes "total_degree p ≤ d"
  shows "total_degree (Const x * p) ≤ d" 
  using assms
proof (transfer, goal_cases)
  case (1 p d x)
  have sub: "keys (Const⇩0 x * p) ⊆ keys p" 
    by (rule order.trans[OF keys_mult], auto simp: Const⇩0_def)
  show ?case
    by (rule order.trans[OF _ 1], rule Max_mono, insert sub, auto)
qed

lemma vars_0[simp]: "vars 0 = {}" 
  unfolding vars_def by (simp add: zero_mpoly.rep_eq)

lemma vars_1[simp]: "vars 1 = {}"
  unfolding vars_def by (simp add: one_mpoly.rep_eq)

lemma vars_Var[simp]: "vars (Var x :: 'a :: comm_semiring_1 mpoly) = {x}" 
  unfolding vars_def by (transfer, auto simp: Var⇩0_def)

lemma vars_Const[simp]: "vars (Const c) = {}" 
  unfolding vars_def by (transfer, auto simp: Const⇩0_def)

lemma coeff_sum_list: "coeff (sum_list ps) m = (∑p←ps. coeff p m)"  
  by (induct ps, auto simp: coeff_add[symmetric]) 
    (metis coeff_monom monom_zero zero_when)

lemma coeff_Const_mult: "coeff (Const c * p) m = c * coeff p m" 
  by (metis Const.abs_eq Const⇩0_def add_0 coeff_monom_mult monom.abs_eq)

lemma coeff_Const: "coeff (Const c) m = (if m = 0 then (c :: 'a :: comm_semiring_1) else 0)"
  by (simp add: Const.rep_eq Const⇩0_def coeff_def lookup_single_not_eq)

lemma coeff_Var: "coeff (Var x) m = (if m = monomial 1 x then 1 :: 'a :: comm_semiring_1 else 0)"
  by (simp add: Var.rep_eq Var⇩0_def coeff_def lookup_single_not_eq)



text ‹list-based representations, so that polynomials can be converted to first-order terms›

lift_definition monom_list :: "'a :: comm_semiring_1 mpoly ⇒ (monom × 'a) list"
  is "λ p. map (λ m. (m, lookup p m)) (sorted_list_of_set (keys p))" .

lift_definition var_list :: "monom ⇒ (var × nat) list"
  is "λ m. map (λ x. (x, lookup m x)) (sorted_list_of_set (keys m))" .

lemma monom_list: "p = (∑ (m, c) ← monom_list p. monom m c)" 
  apply transfer
  subgoal for p
    apply (subst poly_mapping_sum_monomials[symmetric])
    apply (subst distinct_sum_list_conv_Sum)
     apply (unfold distinct_map, simp add: inj_on_def)
     apply (meson in_keys_iff monomial_inj)
    apply (unfold set_map image_comp o_def split)
    apply (subst set_sorted_list_of_set, force)
    by (smt (verit, best) finite_keys lookup_eq_zero_in_keys_contradict monomial_inj o_def sum.cong sum.reindex_nontrivial)
  done

lemma monom_list_coeff: "(m,c) ∈ set (monom_list p) ⟹ coeff p m = c" 
  unfolding coeff_def by (transfer, auto)

lemma monom_list_keys: "(m,c) ∈ set (monom_list p) ⟹ keys m ⊆ vars p" 
  unfolding vars_def by (transfer, auto)


lemma var_list: "monom m c = Const (c :: 'a :: comm_semiring_1) * (∏ (x, e) ← var_list m. (Var x)^e)" 
proof transfer
  fix m :: monom and c :: 'a
  have set: "set (sorted_list_of_set (keys m)) = keys m" 
    by (subst set_sorted_list_of_set, force+)
  have id: "(∏(x, y)←map (λx. (x, lookup m x)) (sorted_list_of_set (keys m)). Var⇩0 x ^ y)
    = (∏ x ∈ keys m. Var⇩0 x ^ lookup m x)" (is "?r1 = ?r2")
    apply (unfold map_map o_def split)
    apply (subst prod.distinct_set_conv_list[symmetric])
    by auto
  have "monomial c m = Const⇩0 c * monomial 1 m"
    by (simp add: Const⇩0_one monomial_mp)
  also have "monomial (1 :: 'a) m = ?r1" unfolding id 
  proof (induction m rule: poly_mapping_induct)
    case (single k v)
    then show ?case by (auto simp: Var⇩0_power mult_single)    
  next
    case (sum f g k v)
    have id: "monomial (1 :: 'a) (f + g) = monomial 1 f * monomial 1 g" 
      by (simp add: mult_single)
    have keys: "keys (f + g) = keys f ∪ keys g" "keys f ∩ keys g = {}" 
       apply (intro keys_plus_ninv_comm_monoid_add) 
      using sum(3-4) by simp
    show ?case unfolding id sum(1-2) unfolding keys(1)
      apply (subst prod.union_disjoint, force, force, rule keys)
      apply (intro arg_cong2[of _ _ _ _ "(*)"] prod.cong refl)
       apply (insert keys(2), simp add: disjoint_iff in_keys_iff lookup_add)
      by (metis add_cancel_left_left disjoint_iff_not_equal in_keys_iff plus_poly_mapping.rep_eq)
  qed
  finally show "monomial c m = Const⇩0 c * ?r1" .
qed

lemma var_list_keys: "(x,e) ∈ set (var_list m) ⟹ x ∈ keys m" 
  by (transfer, auto)

lemma vars_substitute: assumes "⋀ x. vars (σ x) ⊆ V" 
  shows "vars (substitute σ p) ⊆ V" 
proof -
  define mcs where "mcs = monom_list p" 
  show ?thesis unfolding monom_list[of p, folded mcs_def]
  proof (induct mcs)
    case (Cons mc mcs)
    obtain m c where mc: "mc = (m,c)" by force
    define xes where "xes = var_list m" 
    have monom: "vars (substitute σ (monom m c)) ⊆ V" unfolding var_list[of m, folded xes_def]
    proof (induct xes)
      case (Cons xe xes)
      obtain x e where xe: "xe = (x,e)" by force
      from assms have "vars (σ x) ⊆ V" .
      hence x: "vars ((σ x)^e) ⊆ V" 
      proof (induct e)
        case (Suc e)
        then show ?case 
          by (simp, intro order.trans[OF vars_mult], auto)
      qed force
      have id: "substitute σ (Const c * (∏a←xe # xes. case a of (x, a) ⇒ Var x ^ a))
        = σ x ^ e * (Const c * substitute σ (∏(x, y)←xes. Var x ^ y))" unfolding xe
        by (simp add: ac_simps)
      show ?case unfolding id 
        apply (rule order.trans[OF vars_mult])
        using Cons x by auto
    qed force
    show ?case unfolding mc 
      apply simp
      apply (rule order.trans[OF vars_add])
      using monom Cons by auto
  qed force
qed

lemma insertion_monom_nonneg: assumes "⋀ x. α x ≥ 0" and c: "(c :: 'a :: {linordered_nonzero_semiring,ordered_semiring_0}) ≥ 0" 
  shows "insertion α (monom m c) ≥ 0" 
proof -
  define xes where "xes = var_list m" 
  show ?thesis unfolding var_list[of m c, folded xes_def]
  proof (induct xes)
    case Nil
    thus ?case using c by (auto simp: insertion_Const)
  next
    case (Cons xe xes)
    obtain x e where xe: "xe = (x,e)" by force
    have id: "insertion α (Const c * (∏a←xe # xes. case a of (x, a) ⇒ Var x ^ a))
      = α x ^ e * insertion α (Const c * (∏a←xes. case a of (x, a) ⇒ Var x ^ a))" 
      unfolding xe
      by (simp add: insertion_mult insertion_power insertion_Var algebra_simps)
    show ?case unfolding id
    proof (intro mult_nonneg_nonneg Cons)
      show "0 ≤ α x ^ e" using assms(1)[of x]
        by (induct e, auto)
    qed
  qed
qed 

lemma insertion_nonneg: assumes "⋀ x. α x ≥ (0 :: 'a :: linordered_idom)" 
  and "⋀ m. coeff p m ≥ 0"  
shows "insertion α p ≥ 0" 
proof -
  define mcs where "mcs = monom_list p" 
  from monom_list[of p] have p: "p = (∑(m, c)← mcs. monom m c)" unfolding mcs_def by auto
  have mcs: "(m,c) ∈ set mcs ⟹ c ≥ 0" for m c 
    using monom_list_coeff assms(2) unfolding mcs_def by auto
  show ?thesis using mcs unfolding p
  proof (induct mcs)
    case Nil
    thus ?case by (auto simp: insertion_Const)
  next
    case (Cons mc mcs)
    obtain m c where mc: "mc = (m,c)" by force
    with Cons have "c ≥ 0" by auto
    from insertion_monom_nonneg[OF assms(1) this]
    have m: "0 ≤ insertion α (monom m c)" by auto
    from Cons(1)[OF Cons(2)] 
    have IH: "0 ≤ insertion α (∑a←mcs. case a of (a, b) ⇒ monom a b)" by force
    show ?case unfolding mc using IH m
      by (auto simp: insertion_add)
  qed
qed 

lemma vars_sumlist: "vars (sum_list ps) ⊆ ⋃ (vars ` set ps)" 
  by (induct ps, insert vars_add, auto)

lemma coefficients_of_linear_poly: assumes linear: "total_degree (p :: 'a :: comm_semiring_1 mpoly) ≤ 1"  
  shows "∃ c a vs. p = Const c + (∑i←vs. Const (a i) * Var i)
     ∧ distinct vs ∧ set vs = vars p ∧ sorted_list_of_set (vars p) = vs ∧ (∀ v ∈ set vs. a v ≠ 0)
     ∧ (∀ i. a i = coeff p (monomial 1 i)) ∧ (c = coeff p 0)" 
proof -
  have sum_zero: "(⋀ x. x ∈ set xs ⟹ x = 0) ⟹ sum_list (xs :: 'a list) = 0" for xs by (induct xs, auto)
  define a :: "var ⇒ 'a" where "a i = coeff p (monomial 1 i)" for i
  define vs where "vs = sorted_list_of_set (vars p)" 
  define c where "c = coeff p 0" 
  define q where "q = Const c + (∑i← vs. Const (a i) * Var i)" 
  show ?thesis
  proof (intro exI[of _ vs] exI[of _ a] exI[of _ c] conjI ballI vs_def[symmetric] c_def allI a_def, 
      unfold q_def[symmetric])
    show "set vs = vars p" and dist: "distinct vs" 
      using sorted_list_of_set[of "vars p", folded vs_def] vars_finite[of p] by auto    
    show "p = q" 
      unfolding coeff_eq[symmetric]
    proof (intro ext)
      fix m
      have "coeff q m = coeff (Const c) m + (∑x←vs. a x * coeff (Var x) m)" 
        unfolding q_def coeff_add[symmetric] coeff_sum_list map_map o_def coeff_Const_mult ..
      also have "… = coeff p m" 
      proof (cases "m = 0")
        case True
        thus ?thesis by (simp add: coeff_Const coeff_Var monomial_0_iff c_def)
      next
        case False
        from False have "coeff (Const (coeff p 0)) m + (∑x←vs. a x * coeff (Var x) m) 
        = (∑x←vs. a x * coeff (Var x) m)" unfolding coeff_Const by simp
        also have "… = coeff p m" 
        proof (cases "∃ i ∈ set vs. m = monomial 1 i")
          case True
          then obtain i where i: "i ∈ set vs" and m: "m = monomial 1 i" by auto
          from split_list[OF i] obtain bef aft where id: "vs = bef @ i # aft" by auto
          from id dist have i: "i ∉ set bef" "i ∉ set aft" by auto
          have [simp]: "(monomial (Suc 0) i = monomial (Suc 0) j) = (i = j)" for i j :: var
            using monomial_inj by fastforce
          show ?thesis 
            apply (subst id, unfold coeff_Var m, simp)
            apply (subst sum_zero, use i in force)
            apply (subst sum_zero, use i in force)
            by (simp add: a_def)
        next
          case mon: False
          hence one: "(∑x←vs. a x * coeff (Var x) m) = 0" 
            by (intro sum_zero, auto simp: coeff_Var)
          have two: "coeff p m = 0" 
          proof (rule ccontr)
            assume n0: "coeff p m ≠ 0" 
            show False
            proof (cases "∃ i. m = monomial 1 i")
              case True
              with mon obtain i where i: "i ∉ set vs" and m: "m = monomial 1 i" by auto
              from n0 m have "i ∈ vars p" unfolding vars_def coeff_def 
                by (metis UN_I in_keys_iff lookup_single_eq one_neq_zero)
              with i ‹set vs = vars p› show False by auto
            next
              case False
              have "sum (lookup m) (keys m) ≤ total_degree p" using n0 unfolding coeff_def
                apply transfer
                by transfer (metis (no_types, lifting) Max_ge finite.insertI finite_imageI finite_keys image_eqI in_keys_iff insertCI)
              also have "… ≤ 1" using linear .
              finally have linear: "sum (lookup m) (keys m) ≤ 1" by auto
              consider (single) x where "keys m = {x}" | (null) "keys m = {}" | 
                (two) x y k where "keys m = {x,y} ∪ k" and "x ≠ y" by blast
              thus False
              proof cases
                case null
                hence "m = 0" by simp
                with ‹m ≠ 0› show False by simp
              next
                case (single x)
                with linear have "lookup m x ≤ 1" by auto
                moreover from single have nz: "lookup m x ≠ 0"
                  by (metis in_keys_iff insertI1)
                ultimately have "lookup m x = 1" by auto
                with single have "m = monomial 1 x"
                  by (metis Diff_cancel Diff_eq_empty_iff keys_subset_singleton_imp_monomial)
                with False show False by auto
              next
                case (two x y k)
                define k' where "k' = k - {x,y}" 
                have "keys m = insert x (insert y k')" "x ≠ y" "x ∉ k'" "y ∉ k'" "finite k'" 
                  unfolding k'_def using two finite_keys[of m] by auto
                hence "lookup m x + lookup m y ≤ sum (lookup m) (keys m)" by simp
                also have "… ≤ 1" by fact
                finally have "lookup m x = 0 ∨ lookup m y = 0" by auto
                with two show False by blast
              qed
            qed
          qed
          from one two show ?thesis by simp
        qed
        finally show ?thesis by (simp add: c_def)
      qed
      finally show "coeff p m = coeff q m" ..
    qed
  
    fix v
    assume v: "v ∈ set vs" 
    hence "v ∈ vars p" using ‹set vs = vars p› by auto
    hence vq: "v ∈ vars q" unfolding ‹p = q› .
    from split_list[OF v] obtain bef aft where vs: "vs = bef @ v # aft" by auto
    with dist have vba: "v ∉ set bef" "v ∉ set aft" by auto
    show "a v ≠ 0" 
    proof
      assume a0: "a v = 0" 
      have "v ∈ vars p" by fact
      also have "p = q" by fact
      also have "vars q ⊆ vars (sum_list (map (λ x. Const (a x) * Var x) bef)) ∪ 
         vars (Const (a v) * Var v)
         ∪ vars (sum_list (map (λ x. Const (a x) * Var x) aft))" 
        unfolding q_def vs apply simp
        apply (rule order.trans[OF vars_add], simp)
        apply (rule order.trans[OF vars_add])
        by (insert vars_add, blast)
      also have "vars (Const (a v) * Var v) = {}" unfolding a0 Const_0 by simp
      finally obtain list where v: "v ∈ vars (sum_list (map (λ x. Const (a x) * Var x) list))"   
        and not_v: "v ∉ set list" using vba by auto
      from set_mp[OF vars_sumlist v] obtain x where "x ∈ set list" and "v ∈ vars (Const (a x) * Var x)" 
        by auto
      with vars_mult[of "Const (a x)" "Var x"] not_v show False by auto
    qed
  qed
qed

text ‹Introduce notion for degree of monom›
definition degree_monom :: "(var ⇒⇩0 nat) ⇒ nat" where
  "degree_monom m = sum (lookup m) (keys m)" 

lemma total_degree_alt_def: "total_degree p = Max (insert 0 (degree_monom ` keys (mapping_of p)))"
  unfolding degree_monom_def
  by transfer' simp

lemma degree_monon_le_total_degree: assumes "coeff p m ≠ 0" 
  shows "degree_monom m ≤ total_degree p"
  using assms unfolding total_degree_alt_def by (simp add: coeff_keys)

lemma degree_monom_eq_total_degree: assumes "p ≠ 0" 
  shows "∃ m. coeff p m ≠ 0 ∧ degree_monom m = total_degree p" 
proof (cases "total_degree p = 0")
  case False
  thus ?thesis unfolding total_degree_alt_def
    by (metis (full_types) Max_in coeff_keys empty_not_insert finite_imageI finite_insert finite_keys image_iff insertE)
next  
  case True
  from assms obtain m where "coeff p m ≠ 0"
    using coeff_all_0 by auto
  with degree_monon_le_total_degree[OF this] True show ?thesis by auto
qed

lemma degree_add_leI: "degree p x ≤ d ⟹ degree q x ≤ d ⟹ degree (p + q) x ≤ d"  
  apply transfer
  subgoal for p x d q using Poly_Mapping.keys_add[of p q]
    by (intro Max.boundedI, auto)
  done

lemma degree_sum_leI: assumes "⋀ i. i ∈ A ⟹ degree (p i) x ≤ d" 
  shows "degree (sum p A) x ≤ d" 
  using assms 
  by (induct A rule: infinite_finite_induct, auto intro: degree_add_leI)

lemma total_degree_sum_leI: assumes "⋀ i. i ∈ A ⟹ total_degree (p i) ≤ d" 
  shows "total_degree (sum p A) ≤ d" 
  using assms 
  by (induct A rule: infinite_finite_induct, auto intro: total_degree_add)

lemma total_degree_monom: assumes "c ≠ 0"  
  shows "total_degree (monom m c) = degree_monom m"
  unfolding total_degree_alt_def using assms by auto

lemma degree_Var[simp]: "degree (Var x :: 'a :: comm_semiring_1 mpoly) x = 1" 
  by (transfer, unfold Var⇩0_def, simp)

lemma Var_neq_0[simp]: "Var x ≠ (0 :: 'a :: comm_semiring_1 mpoly)" 
proof
  assume "Var x = (0 :: 'a mpoly)" 
  from arg_cong[OF this, of "λ p. degree p x"]
  show False by simp
qed

lemma degree_Const[simp]: "degree (Const c) x = 0" 
  by transfer (auto simp: Const⇩0_def)

lemma vars_add_subI: "vars p ⊆ A ⟹ vars q ⊆ A ⟹ vars (p + q) ⊆ A" 
  by (metis le_supI subset_trans vars_add)

lemma vars_mult_subI: "vars p ⊆ A ⟹ vars q ⊆ A ⟹ vars (p * q) ⊆ A" 
  by (metis le_supI subset_trans vars_mult)

lemma vars_eqI: assumes "vars (p :: 'a :: comm_ring_1 mpoly) ⊆ V"
  "⋀ v. v ∈ V ⟹ ∃ a b. insertion a p ≠ insertion (a(v := b)) p" 
shows "vars p = V" 
proof (rule ccontr)
  assume "¬ ?thesis" 
  with assms obtain v where "v ∈ V" and not: "v ∉ vars p" by auto
  from assms(2)[OF this(1)] obtain a b where "insertion a p ≠ insertion (a(v := b)) p" by auto
  moreover have "insertion a p = insertion (a(v := b)) p" 
    by (rule insertion_irrelevant_vars, insert not, auto) 
  ultimately show False by auto
qed


end