Theory Polynomials.MPoly_PM

(* Author: Alexander Maletzky *)

section ‹Multivariate Polynomials with Power-Products Represented by Polynomial Mappings›

theory MPoly_PM
  imports Quasi_PM_Power_Products
begin

text ‹Many notions introduced in this theory for type @{typ "('x 0 'a) 0 'b"} closely resemble
  those introduced in @{theory Polynomials.MPoly_Type} for type @{typ "'a mpoly"}.›

lemma monomial_single_power:
  "(monomial c (Poly_Mapping.single x k)) ^ n = monomial (c ^ n) (Poly_Mapping.single x (k * n))"
proof -
  have eq: "(i = 0..<n. Poly_Mapping.single x k) = Poly_Mapping.single x (k * n)"
    by (induct n, simp_all add: add.commute single_add)
  show ?thesis by (simp add: punit.monomial_power eq)
qed

lemma monomial_power_map_scale: "(monomial c t) ^ n = monomial (c ^ n) (n  t)"
proof -
  have "(i = 0..<n. t) = (i = 0..<n. 1)  t"
    by (simp only: map_scale_sum_distrib_right map_scale_one_left)
  thus ?thesis by (simp add: punit.monomial_power)
qed

lemma times_canc_left:
  assumes "h * p = h * q" and "h  (0::('x::linorder 0 nat) 0 'a::ring_no_zero_divisors)"
  shows "p = q"
proof (rule ccontr)
  assume "p  q"
  hence "p - q  0" by simp
  with assms(2) have "h * (p - q)  0" by simp
  hence "h * p  h * q" by (simp add: algebra_simps)
  thus False using assms(1) ..
qed

lemma times_canc_right:
  assumes "p * h = q * h" and "h  (0::('x::linorder 0 nat) 0 'a::ring_no_zero_divisors)"
  shows "p = q"
proof (rule ccontr)
  assume "p  q"
  hence "p - q  0" by simp
  hence "(p - q) * h  0" using assms(2) by simp
  hence "p * h  q * h" by (simp add: algebra_simps)
  thus False using assms(1) ..
qed

subsection ‹Degree›

lemma plus_minus_assoc_pm_nat_1: "s + t - u = (s - (u - t)) + (t - (u::_ 0 nat))"
  by (rule poly_mapping_eqI, simp add: lookup_add lookup_minus)

lemma plus_minus_assoc_pm_nat_2:
  "s + (t - u) = (s + (except (u - t) (- keys s))) + t - (u::_ 0 nat)"
proof (rule poly_mapping_eqI)
  fix x
  show "lookup (s + (t - u)) x = lookup (s + except (u - t) (- keys s) + t - u) x"
  proof (cases "x  keys s")
    case True
    thus ?thesis
      by (simp add: plus_minus_assoc_pm_nat_1 lookup_add lookup_minus lookup_except)
  next
    case False
    hence "lookup s x = 0" by (simp add: in_keys_iff)
    with False show ?thesis
      by (simp add: lookup_add lookup_minus lookup_except)
  qed
qed

lemma deg_pm_sum: "deg_pm (sum t A) = (aA. deg_pm (t a))"
  by (induct A rule: infinite_finite_induct) (auto simp: deg_pm_plus)

lemma deg_pm_mono: "s adds t  deg_pm s  deg_pm (t::_ 0 _::add_linorder_min)"
  by (metis addsE deg_pm_plus le_iff_add)

lemma adds_deg_pm_antisym: "s adds t  deg_pm t  deg_pm (s::_ 0 _::add_linorder_min)  s = t"
  by (metis (no_types, lifting) add.right_neutral add.right_neutral add_left_cancel addsE
      deg_pm_eq_0_iff deg_pm_mono deg_pm_plus dual_order.antisym)

lemma deg_pm_minus:
  assumes "s adds (t::_ 0 _::comm_monoid_add)"
  shows "deg_pm (t - s) = deg_pm t - deg_pm s"
proof -
  from assms have "(t - s) + s = t" by (rule adds_minus)
  hence "deg_pm t = deg_pm ((t - s) + s)" by simp
  also have " = deg_pm (t - s) + deg_pm s" by (simp only: deg_pm_plus)
  finally show ?thesis by simp
qed

lemma adds_group [simp]: "s adds (t::'a 0 'b::ab_group_add)"
proof (rule addsI)
  show "t = s + (t - s)" by simp
qed

lemmas deg_pm_minus_group = deg_pm_minus[OF adds_group]

lemma deg_pm_minus_le: "deg_pm (t - s)  deg_pm (t::_ 0 nat)"
proof -
  have "keys (t - s)  keys t" by (rule, simp add: lookup_minus in_keys_iff)
  hence "deg_pm (t - s) = (xkeys t. lookup (t - s) x)" using finite_keys by (rule deg_pm_superset)
  also have "  (xkeys t. lookup t x)" by (rule sum_mono) (simp add: lookup_minus)
  also have " = deg_pm t" by (rule sym, rule deg_pm_superset, fact subset_refl, fact finite_keys)
  finally show ?thesis .
qed

lemma minus_id_iff: "t - s = t  keys t  keys (s::_ 0 nat) = {}"
proof
  assume "t - s = t"
  {
    fix x
    assume "x  keys t" and "x  keys s"
    hence "0 < lookup t x" and "0 < lookup s x" by (simp_all add: in_keys_iff)
    hence "lookup (t - s) x  lookup t x" by (simp add: lookup_minus)
    with t - s = t have False by simp
  }
  thus "keys t  keys s = {}" by blast
next
  assume *: "keys t  keys s = {}"
  show "t - s = t"
  proof (rule poly_mapping_eqI)
    fix x
    have "lookup t x - lookup s x = lookup t x"
    proof (cases "x  keys t")
      case True
      with * have "x  keys s" by blast
      thus ?thesis by (simp add: in_keys_iff)
    next
      case False
      thus ?thesis by (simp add: in_keys_iff)
    qed
    thus "lookup (t - s) x = lookup t x" by (simp only: lookup_minus)
  qed
qed

lemma deg_pm_minus_id_iff: "deg_pm (t - s) = deg_pm t  keys t  keys (s::_ 0 nat) = {}"
proof
  assume eq: "deg_pm (t - s) = deg_pm t"
  {
    fix x
    assume "x  keys t" and "x  keys s"
    hence "0 < lookup t x" and "0 < lookup s x" by (simp_all add: in_keys_iff)
    hence *: "lookup (t - s) x < lookup t x" by (simp add: lookup_minus)
    have "keys (t - s)  keys t" by (rule, simp add: lookup_minus in_keys_iff)
    hence "deg_pm (t - s) = (xkeys t. lookup (t - s) x)" using finite_keys by (rule deg_pm_superset)
    also from finite_keys have " < (xkeys t. lookup t x)"
    proof (rule sum_strict_mono_ex1)
      show "xkeys t. lookup (t - s) x  lookup t x" by (simp add: lookup_minus)
    next
      from x  keys t * show "xkeys t. lookup (t - s) x < lookup t x" ..
    qed
    also have " = deg_pm t" by (rule sym, rule deg_pm_superset, fact subset_refl, fact finite_keys)
    finally have False by (simp add: eq)
  }
  thus "keys t  keys s = {}" by blast
next
  assume "keys t  keys s = {}"
  hence "t - s = t" by (simp only: minus_id_iff)
  thus "deg_pm (t - s) = deg_pm t" by (simp only:)
qed

definition poly_deg :: "(('x 0 'a::add_linorder) 0 'b::zero)  'a" where
  "poly_deg p = (if keys p = {} then 0 else Max (deg_pm ` keys p))"

definition maxdeg :: "(('x 0 'a::add_linorder) 0 'b::zero) set  'a" where
  "maxdeg A = Max (poly_deg ` A)"
  
definition mindeg :: "(('x 0 'a::add_linorder) 0 'b::zero) set  'a" where
  "mindeg A = Min (poly_deg ` A)"

lemma poly_deg_monomial: "poly_deg (monomial c t) = (if c = 0 then 0 else deg_pm t)"
  by (simp add: poly_deg_def)

lemma poly_deg_monomial_zero [simp]: "poly_deg (monomial c 0) = 0"
  by (simp add: poly_deg_monomial)

lemma poly_deg_zero [simp]: "poly_deg 0 = 0"
  by (simp only: single_zero[of 0, symmetric] poly_deg_monomial_zero)

lemma poly_deg_one [simp]: "poly_deg 1 = 0"
  by (simp only: single_one[symmetric] poly_deg_monomial_zero)

lemma poly_degE:
  assumes "p  0"
  obtains t where "t  keys p" and "poly_deg p = deg_pm t"
proof -
  from assms have "poly_deg p = Max (deg_pm ` keys p)" by (simp add: poly_deg_def)
  also have "  deg_pm ` keys p"
  proof (rule Max_in)
    from assms show "deg_pm ` keys p  {}" by simp
  qed simp
  finally obtain t where "t  keys p" and "poly_deg p = deg_pm t" ..
  thus ?thesis ..
qed

lemma poly_deg_max_keys: "t  keys p  deg_pm t  poly_deg p"
  using finite_keys by (auto simp: poly_deg_def)

lemma poly_deg_leI: "(t. t  keys p  deg_pm t  (d::'a::add_linorder_min))  poly_deg p  d"
  using finite_keys by (auto simp: poly_deg_def)

lemma poly_deg_lessI:
  "p  0  (t. t  keys p  deg_pm t < (d::'a::add_linorder_min))  poly_deg p < d"
  using finite_keys by (auto simp: poly_deg_def)

lemma poly_deg_zero_imp_monomial:
  assumes "poly_deg p = (0::'a::add_linorder_min)"
  shows "monomial (lookup p 0) 0 = p"
proof (rule keys_subset_singleton_imp_monomial, rule)
  fix t
  assume "t  keys p"
  have "t = 0"
  proof (rule ccontr)
    assume "t  0"
    hence "deg_pm t  0" by simp
    hence "0 < deg_pm t" using not_gr_zero by blast
    also from t  keys p have "...  poly_deg p" by (rule poly_deg_max_keys)
    finally have "poly_deg p  0" by simp
    from this assms show False ..
  qed
  thus "t  {0}" by simp
qed

lemma poly_deg_plus_le:
  "poly_deg (p + q)  max (poly_deg p) (poly_deg (q::(_ 0 'a::add_linorder_min) 0 _))"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (p + q)"
  also have "...  keys p  keys q" by (fact Poly_Mapping.keys_add)
  finally show "deg_pm t  max (poly_deg p) (poly_deg q)"
  proof
    assume "t  keys p"
    hence "deg_pm t  poly_deg p" by (rule poly_deg_max_keys)
    thus ?thesis by (simp add: le_max_iff_disj)
  next
    assume "t  keys q"
    hence "deg_pm t  poly_deg q" by (rule poly_deg_max_keys)
    thus ?thesis by (simp add: le_max_iff_disj)
  qed
qed

lemma poly_deg_uminus [simp]: "poly_deg (-p) = poly_deg p"
  by (simp add: poly_deg_def keys_uminus)

lemma poly_deg_minus_le:
  "poly_deg (p - q)  max (poly_deg p) (poly_deg (q::(_ 0 'a::add_linorder_min) 0 _))"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (p - q)"
  also have "...  keys p  keys q" by (fact keys_minus)
  finally show "deg_pm t  max (poly_deg p) (poly_deg q)"
  proof
    assume "t  keys p"
    hence "deg_pm t  poly_deg p" by (rule poly_deg_max_keys)
    thus ?thesis by (simp add: le_max_iff_disj)
  next
    assume "t  keys q"
    hence "deg_pm t  poly_deg q" by (rule poly_deg_max_keys)
    thus ?thesis by (simp add: le_max_iff_disj)
  qed
qed

lemma poly_deg_times_le:
  "poly_deg (p * q)  poly_deg p + poly_deg (q::(_ 0 'a::add_linorder_min) 0 _)"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (p * q)"
  then obtain u v where "u  keys p" and "v  keys q" and "t = u + v" by (rule in_keys_timesE)
  from u  keys p have "deg_pm u  poly_deg p" by (rule poly_deg_max_keys)
  moreover from v  keys q have "deg_pm v  poly_deg q" by (rule poly_deg_max_keys)
  ultimately show "deg_pm t  poly_deg p + poly_deg q" by (simp add: t = u + v deg_pm_plus add_mono)
qed

lemma poly_deg_times:
  assumes "p  0" and "q  (0::('x::linorder 0 'a::add_linorder_min) 0 'b::semiring_no_zero_divisors)"
  shows "poly_deg (p * q) = poly_deg p + poly_deg q"
  using poly_deg_times_le
proof (rule antisym)
  let ?A = "λf. {u. deg_pm u < poly_deg f}"
  define p1 where "p1 = except p (?A p)"
  define p2 where "p2 = except p (- ?A p)"
  define q1 where "q1 = except q (?A q)"
  define q2 where "q2 = except q (- ?A q)"
  have deg_p1: "deg_pm t = poly_deg p" if "t  keys p1" for t
  proof -
    from that have "t  keys p" and "poly_deg p  deg_pm t"
      by (simp_all add: p1_def keys_except not_less)
    from this(1) have "deg_pm t  poly_deg p" by (rule poly_deg_max_keys)
    thus ?thesis using poly_deg p  deg_pm t by (rule antisym)
  qed
  have deg_p2: "t  keys p2  deg_pm t < poly_deg p" for t by (simp add: p2_def keys_except)
  have deg_q1: "deg_pm t = poly_deg q" if "t  keys q1" for t
  proof -
    from that have "t  keys q" and "poly_deg q  deg_pm t"
      by (simp_all add: q1_def keys_except not_less)
    from this(1) have "deg_pm t  poly_deg q" by (rule poly_deg_max_keys)
    thus ?thesis using poly_deg q  deg_pm t by (rule antisym)
  qed
  have deg_q2: "t  keys q2  deg_pm t < poly_deg q" for t by (simp add: q2_def keys_except)
  have p: "p = p1 + p2" unfolding p1_def p2_def by (fact except_decomp)
  have "p1  0"
  proof -
    from assms(1) obtain t where "t  keys p" and "poly_deg p = deg_pm t" by (rule poly_degE)
    hence "t  keys p1" by (simp add: p1_def keys_except)
    thus ?thesis by auto
  qed
  have q: "q = q1 + q2" unfolding q1_def q2_def by (fact except_decomp)
  have "q1  0"
  proof -
    from assms(2) obtain t where "t  keys q" and "poly_deg q = deg_pm t" by (rule poly_degE)
    hence "t  keys q1" by (simp add: q1_def keys_except)
    thus ?thesis by auto
  qed
  with p1  0 have "p1 * q1  0" by simp
  hence "keys (p1 * q1)  {}" by simp
  then obtain u where "u  keys (p1 * q1)" by blast
  then obtain s t where "s  keys p1" and "t  keys q1" and u: "u = s + t" by (rule in_keys_timesE)
  from s  keys p1 have "deg_pm s = poly_deg p" by (rule deg_p1)
  moreover from t  keys q1 have "deg_pm t = poly_deg q" by (rule deg_q1)
  ultimately have eq: "poly_deg p + poly_deg q = deg_pm u" by (simp only: u deg_pm_plus)
  also have "  poly_deg (p * q)"
  proof (rule poly_deg_max_keys)
    have "u  keys (p1 * q2 + p2 * q)"
    proof
      assume "u  keys (p1 * q2 + p2 * q)"
      also have "  keys (p1 * q2)  keys (p2 * q)" by (rule Poly_Mapping.keys_add)
      finally have "deg_pm u < poly_deg p + poly_deg q"
      proof
        assume "u  keys (p1 * q2)"
        then obtain s' t' where "s'  keys p1" and "t'  keys q2" and u: "u = s' + t'"
          by (rule in_keys_timesE)
        from s'  keys p1 have "deg_pm s' = poly_deg p" by (rule deg_p1)
        moreover from t'  keys q2 have "deg_pm t' < poly_deg q" by (rule deg_q2)
        ultimately show ?thesis by (simp add: u deg_pm_plus)
      next
        assume "u  keys (p2 * q)"
        then obtain s' t' where "s'  keys p2" and "t'  keys q" and u: "u = s' + t'"
          by (rule in_keys_timesE)
        from s'  keys p2 have "deg_pm s' < poly_deg p" by (rule deg_p2)
        moreover from t'  keys q have "deg_pm t'  poly_deg q" by (rule poly_deg_max_keys)
        ultimately show ?thesis by (simp add: u deg_pm_plus add_less_le_mono)
      qed
      thus False by (simp only: eq)
    qed
    with u  keys (p1 * q1) have "u  keys (p1 * q1 + (p1 * q2 + p2 * q))" by (rule in_keys_plusI1)
    thus "u  keys (p * q)" by (simp only: p q algebra_simps)
  qed
  finally show "poly_deg p + poly_deg q  poly_deg (p * q)" .
qed

corollary poly_deg_monom_mult_le:
  "poly_deg (punit.monom_mult c (t::_ 0 'a::add_linorder_min) p)  deg_pm t + poly_deg p"
proof -
  have "poly_deg (punit.monom_mult c t p)  poly_deg (monomial c t) + poly_deg p"
    by (simp only: times_monomial_left[symmetric] poly_deg_times_le)
  also have "...  deg_pm t + poly_deg p" by (simp add: poly_deg_monomial)
  finally show ?thesis .
qed

lemma poly_deg_monom_mult:
  assumes "c  0" and "p  (0::(_ 0 'a::add_linorder_min) 0 'b::semiring_no_zero_divisors)"
  shows "poly_deg (punit.monom_mult c t p) = deg_pm t + poly_deg p"
proof (rule order.antisym, fact poly_deg_monom_mult_le)
  from assms(2) obtain s where "s  keys p" and "poly_deg p = deg_pm s" by (rule poly_degE)
  have "deg_pm t + poly_deg p = deg_pm (t + s)" by (simp add: poly_deg p = deg_pm s deg_pm_plus)
  also have "...  poly_deg (punit.monom_mult c t p)"
  proof (rule poly_deg_max_keys)
    from s  keys p show "t + s  keys (punit.monom_mult c t p)"
      unfolding punit.keys_monom_mult[OF assms(1)] by fastforce
  qed
  finally show "deg_pm t + poly_deg p  poly_deg (punit.monom_mult c t p)" .
qed

lemma poly_deg_map_scale:
  "poly_deg (c  p) = (if c = (0::_::semiring_no_zero_divisors) then 0 else poly_deg p)"
  by (simp add: poly_deg_def keys_map_scale)

lemma poly_deg_sum_le: "((poly_deg (sum f A))::'a::add_linorder_min)  Max (poly_deg ` f ` A)"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    show ?case by simp
  next
    case (insert a A)
    show ?case
    proof (cases "A = {}")
      case True
      thus ?thesis by simp
    next
      case False
      have "poly_deg (sum f (insert a A))  max (poly_deg (f a)) (poly_deg (sum f A))"
        by (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)] poly_deg_plus_le)
      also have "...  max (poly_deg (f a)) (Max (poly_deg ` f ` A))"
        using insert(3) max.mono by blast
      also have "... = (Max (poly_deg ` f ` (insert a A)))" using False by (simp add: insert(1))
      finally show ?thesis .
    qed
  qed
next
  case False
  thus ?thesis by simp
qed

lemma poly_deg_prod_le: "((poly_deg (prod f A))::'a::add_linorder_min)  (aA. poly_deg (f a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    show ?case by simp
  next
    case (insert a A)
    have "poly_deg (prod f (insert a A))  (poly_deg (f a)) + (poly_deg (prod f A))"
      by (simp only: comm_monoid_mult_class.prod.insert[OF insert(1) insert(2)] poly_deg_times_le)
    also have "...  (poly_deg (f a)) + (aA. poly_deg (f a))"
      using insert(3) add_le_cancel_left by blast
    also have "... = (ainsert a A. poly_deg (f a))" by (simp add: insert(1) insert(2))
    finally show ?case .
  qed
next
  case False
  thus ?thesis by simp
qed

lemma maxdeg_max:
  assumes "finite A" and "p  A"
  shows "poly_deg p  maxdeg A"
  unfolding maxdeg_def using assms by auto

lemma mindeg_min:
  assumes "finite A" and "p  A"
  shows "mindeg A  poly_deg p"
  unfolding mindeg_def using assms by auto

subsection ‹Indeterminates›

definition indets :: "(('x 0 nat) 0 'b::zero)  'x set"
  where "indets p =  (keys ` keys p)"

definition PPs :: "'x set  ('x 0 nat) set"  (".[(_)]")
  where "PPs X = {t. keys t  X}"

definition Polys :: "'x set  (('x 0 nat) 0 'b::zero) set"  ("P[(_)]")
  where "Polys X = {p. keys p  .[X]}"

subsubsection @{const indets}

lemma in_indetsI:
  assumes "x  keys t" and "t  keys p"
  shows "x  indets p"
  using assms by (auto simp add: indets_def)

lemma in_indetsE:
  assumes "x  indets p"
  obtains t where "t  keys p" and "x  keys t"
  using assms by (auto simp add: indets_def)

lemma keys_subset_indets: "t  keys p  keys t  indets p"
  by (auto dest: in_indetsI)

lemma indets_empty_imp_monomial:
  assumes "indets p = {}"
  shows "monomial (lookup p 0) 0 = p"
proof (rule keys_subset_singleton_imp_monomial, rule)
  fix t
  assume "t  keys p"
  have "t = 0"
  proof (rule ccontr)
    assume "t  0"
    hence "keys t  {}" by simp
    then obtain x where "x  keys t" by blast
    from this t  keys p have "x  indets p" by (rule in_indetsI)
    with assms show False by simp
  qed
  thus "t  {0}" by simp
qed

lemma finite_indets: "finite (indets p)"
  by (simp only: indets_def, rule finite_UN_I, (rule finite_keys)+)

lemma indets_zero [simp]: "indets 0 = {}"
  by (simp add: indets_def)

lemma indets_one [simp]: "indets 1 = {}"
  by (simp add: indets_def)

lemma indets_monomial_single_subset: "indets (monomial c (Poly_Mapping.single v k))  {v}"
proof
  fix x assume "x  indets (monomial c (Poly_Mapping.single v k))"
  then have "x = v" unfolding indets_def
    by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq)
  thus "x  {v}" by simp
qed

lemma indets_monomial_single:
  assumes "c  0" and "k  0"
  shows "indets (monomial c (Poly_Mapping.single v k)) = {v}"
proof (rule, fact indets_monomial_single_subset, simp)
  from assms show "v  indets (monomial c (monomial k v))" by (simp add: indets_def)
qed

lemma indets_monomial:
  assumes "c  0"
  shows "indets (monomial c t) = keys t"
proof (rule antisym; rule subsetI)
  fix x
  assume "x  indets (monomial c t)"
  then have "lookup t x  0" unfolding indets_def
    by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq)
  thus "x  keys t" by (meson lookup_not_eq_zero_eq_in_keys)
next
  fix x
  assume "x  keys t"
  then have "lookup t x  0" by (meson lookup_not_eq_zero_eq_in_keys)
  thus "x  indets (monomial c t)" unfolding indets_def using assms
    by (metis UN_iff lookup_not_eq_zero_eq_in_keys lookup_single_eq)
qed

lemma indets_monomial_subset: "indets (monomial c t)  keys t"
  by (cases "c = 0", simp_all add: indets_def)

lemma indets_monomial_zero [simp]: "indets (monomial c 0) = {}"
  by (simp add: indets_def)

lemma indets_plus_subset: "indets (p + q)  indets p  indets q"
proof
  fix x
  assume "x  indets (p + q)"
  then obtain t where "x  keys t" and "t  keys (p + q)" by (metis UN_E indets_def)
  hence "t  keys p  keys q" by (metis Poly_Mapping.keys_add subsetCE)
  thus "x  indets p  indets q" using indets_def x  keys t by fastforce
qed

lemma indets_uminus [simp]: "indets (-p) = indets p"
  by (simp add: indets_def keys_uminus)

lemma indets_minus_subset: "indets (p - q)  indets p  indets q"
proof
  fix x
  assume "x  indets (p - q)"
  then obtain t where "x  keys t" and "t  keys (p - q)" by (metis UN_E indets_def)
  hence "t  keys p  keys q" by (metis keys_minus subsetCE)
  thus "x  indets p  indets q" using indets_def x  keys t by fastforce
qed

lemma indets_times_subset: "indets (p * q)  indets p  indets (q::(_ 0 _::cancel_comm_monoid_add) 0 _)"
proof
  fix x
  assume "x  indets (p * q)"
  then obtain t where "t  keys (p * q)" and "x  keys t" unfolding indets_def by blast
  from this(1) obtain u v where "u  keys p" "v  keys q" and "t = u + v" by (rule in_keys_timesE)
  hence "x  keys u  keys v" by (metis x  keys t Poly_Mapping.keys_add subsetCE)
  thus "x  indets p  indets q" unfolding indets_def using u  keys p v  keys q by blast
qed

corollary indets_monom_mult_subset: "indets (punit.monom_mult c t p)  keys t  indets p"
proof -
  have "indets (punit.monom_mult c t p)  indets (monomial c t)  indets p"
    by (simp only: times_monomial_left[symmetric] indets_times_subset)
  also have "...  keys t  indets p" using indets_monomial_subset[of t c] by blast
  finally show ?thesis .
qed

lemma indets_monom_mult:
  assumes "c  0" and "p  (0::('x 0 nat) 0 'b::semiring_no_zero_divisors)"
  shows "indets (punit.monom_mult c t p) = keys t  indets p"
proof (rule, fact indets_monom_mult_subset, rule)
  fix x
  assume "x  keys t  indets p"
  thus "x  indets (punit.monom_mult c t p)"
  proof
    assume "x  keys t"
    from assms(2) have "keys p  {}" by simp
    then obtain s where "s  keys p" by blast
    hence "t + s  (+) t ` keys p" by fastforce
    also from assms(1) have "... = keys (punit.monom_mult c t p)" by (simp add: punit.keys_monom_mult)
    finally have "t + s  keys (punit.monom_mult c t p)" .
    show ?thesis
    proof (rule in_indetsI)
      from x  keys t show "x  keys (t + s)" by (simp add: keys_plus_ninv_comm_monoid_add)
    qed fact
  next
    assume "x  indets p"
    then obtain s where "s  keys p" and "x  keys s" by (rule in_indetsE)
    from this(1) have "t + s  (+) t ` keys p" by fastforce
    also from assms(1) have "... = keys (punit.monom_mult c t p)" by (simp add: punit.keys_monom_mult)
    finally have "t + s  keys (punit.monom_mult c t p)" .
    show ?thesis
    proof (rule in_indetsI)
      from x  keys s show "x  keys (t + s)" by (simp add: keys_plus_ninv_comm_monoid_add)
    qed fact
  qed
qed

lemma indets_sum_subset: "indets (sum f A)  (aA. indets (f a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    show ?case by simp
  next
    case (insert a A)
    have "indets (sum f (insert a A))  indets (f a)  indets (sum f A)"
      by (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)] indets_plus_subset)
    also have "...  indets (f a)  (aA. indets (f a))" using insert(3) by blast
    also have "... = (ainsert a A. indets (f a))" by simp
    finally show ?case .
  qed
next
  case False
  thus ?thesis by simp
qed

lemma indets_prod_subset:
  "indets (prod (f::_  ((_ 0 _::cancel_comm_monoid_add) 0 _)) A)  (aA. indets (f a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    show ?case by simp
  next
    case (insert a A)
    have "indets (prod f (insert a A))  indets (f a)  indets (prod f A)"
      by (simp only: comm_monoid_mult_class.prod.insert[OF insert(1) insert(2)] indets_times_subset)
    also have "...  indets (f a)  (aA. indets (f a))" using insert(3) by blast
    also have "... = (ainsert a A. indets (f a))" by simp
    finally show ?case .
  qed
next
  case False
  thus ?thesis by simp
qed

lemma indets_power_subset: "indets (p ^ n)  indets (p::('x 0 nat) 0 'b::comm_semiring_1)"
proof -
  have "p ^ n = (i=0..<n. p)" by simp
  also have "indets ...  (i{0..<n}. indets p)" by (fact indets_prod_subset)
  also have "...  indets p" by simp
  finally show ?thesis .
qed

lemma indets_empty_iff_poly_deg_zero: "indets p = {}  poly_deg p = 0"
proof
  assume "indets p = {}"
  hence "monomial (lookup p 0) 0 = p" by (rule indets_empty_imp_monomial)
  moreover have "poly_deg (monomial (lookup p 0) 0) = 0" by simp
  ultimately show "poly_deg p = 0" by metis
next
  assume "poly_deg p = 0"
  hence "monomial (lookup p 0) 0 = p" by (rule poly_deg_zero_imp_monomial)
  moreover have "indets (monomial (lookup p 0) 0) = {}" by simp
  ultimately show "indets p = {}" by metis
qed

subsubsection @{const PPs}

lemma PPsI: "keys t  X  t  .[X]"
  by (simp add: PPs_def)

lemma PPsD: "t  .[X]  keys t  X"
  by (simp add: PPs_def)

lemma PPs_empty [simp]: ".[{}] = {0}"
  by (simp add: PPs_def)

lemma PPs_UNIV [simp]: ".[UNIV] = UNIV"
  by (simp add: PPs_def)

lemma PPs_singleton: ".[{x}] = range (Poly_Mapping.single x)"
proof (rule set_eqI)
  fix t
  show "t  .[{x}]  t  range (Poly_Mapping.single x)"
  proof
    assume "t  .[{x}]"
    hence "keys t  {x}" by (rule PPsD)
    hence "Poly_Mapping.single x (lookup t x) = t" by (rule keys_subset_singleton_imp_monomial)
    from this[symmetric] UNIV_I show "t  range (Poly_Mapping.single x)" ..
  next
    assume "t  range (Poly_Mapping.single x)"
    then obtain e where "t = Poly_Mapping.single x e" ..
    thus "t  .[{x}]" by (simp add: PPs_def)
  qed
qed

lemma zero_in_PPs: "0  .[X]"
  by (simp add: PPs_def)

lemma PPs_mono: "X  Y  .[X]  .[Y]"
  by (auto simp: PPs_def)

lemma PPs_closed_single:
  assumes "x  X"
  shows "Poly_Mapping.single x e  .[X]"
proof (rule PPsI)
  have "keys (Poly_Mapping.single x e)  {x}" by simp
  also from assms have "...  X" by simp
  finally show "keys (Poly_Mapping.single x e)  X" .
qed

lemma PPs_closed_plus:
  assumes "s  .[X]" and "t  .[X]"
  shows "s + t  .[X]"
proof -
  have "keys (s + t)  keys s  keys t" by (fact Poly_Mapping.keys_add)
  also from assms have "...  X" by (simp add: PPs_def)
  finally show ?thesis by (rule PPsI)
qed

lemma PPs_closed_minus:
  assumes "s  .[X]"
  shows "s - t  .[X]"
proof -
  have "keys (s - t)  keys s" by (metis lookup_minus lookup_not_eq_zero_eq_in_keys subsetI zero_diff)
  also from assms have "...  X" by (rule PPsD)
  finally show ?thesis by (rule PPsI)
qed

lemma PPs_closed_adds:
  assumes "s  .[X]" and "t adds s"
  shows "t  .[X]"
proof -
  from assms(2) have "s - (s - t) = t" by (metis add_minus_2 adds_minus)
  moreover from assms(1) have "s - (s - t)  .[X]" by (rule PPs_closed_minus)
  ultimately show ?thesis by simp
qed

lemma PPs_closed_gcs:
  assumes "s  .[X]"
  shows "gcs s t  .[X]"
  using assms gcs_adds by (rule PPs_closed_adds)

lemma PPs_closed_lcs:
  assumes "s  .[X]" and "t  .[X]"
  shows "lcs s t  .[X]"
proof -
  from assms have "s + t  .[X]" by (rule PPs_closed_plus)
  hence "(s + t) - gcs s t  .[X]" by (rule PPs_closed_minus)
  thus ?thesis by (simp add: gcs_plus_lcs[of s t, symmetric])
qed

lemma PPs_closed_except': "t  .[X]  except t Y  .[X - Y]"
  by (auto simp: keys_except PPs_def)

lemma PPs_closed_except: "t  .[X]  except t Y  .[X]"
  by (auto simp: keys_except PPs_def)

lemma PPs_UnI:
  assumes "tx  .[X]" and "ty  .[Y]" and "t = tx + ty"
  shows "t  .[X  Y]"
proof -
  from assms(1) have "tx  .[X  Y]" by rule (simp add: PPs_mono)
  moreover from assms(2) have "ty  .[X  Y]" by rule (simp add: PPs_mono)
  ultimately show ?thesis unfolding assms(3) by (rule PPs_closed_plus)
qed

lemma PPs_UnE:
  assumes "t  .[X  Y]"
  obtains tx ty where "tx  .[X]" and "ty  .[Y]" and "t = tx + ty"
proof -
  from assms have "keys t  X  Y" by (rule PPsD)
  define tx where "tx = except t (- X)"
  have "keys tx  X" by (simp add: tx_def keys_except)
  hence "tx  .[X]" by (simp add: PPs_def)
  have "tx adds t" by (simp add: tx_def adds_poly_mappingI le_fun_def lookup_except)
  from adds_minus[OF this] have "t = tx + (t - tx)" by (simp only: ac_simps)
  have "t - tx  .[Y]"
  proof (rule PPsI, rule)
    fix x
    assume "x  keys (t - tx)"
    also have "...  keys t  keys tx" by (rule keys_minus)
    also from keys t  X  Y keys tx  X have "...  X  Y" by blast
    finally show "x  Y"
    proof
      assume "x  X"
      hence "x  keys (t - tx)" by (simp add: tx_def lookup_except lookup_minus in_keys_iff)
      thus ?thesis using x  keys (t - tx) ..
    qed
  qed
  with tx  .[X] show ?thesis using t = tx + (t - tx) ..
qed

lemma PPs_Un: ".[X  Y] = (t.[X]. (+) t ` .[Y])"  (is "?A = ?B")
proof (rule set_eqI)
  fix t
  show "t  ?A  t  ?B"
  proof
    assume "t  ?A"
    then obtain tx ty where "tx  .[X]" and "ty  .[Y]" and "t = tx + ty" by (rule PPs_UnE)
    from this(2) have "t  (+) tx ` .[Y]" unfolding t = tx + ty by (rule imageI)
    with tx  .[X] show "t  ?B" ..
  next
    assume "t  ?B"
    then obtain tx where "tx  .[X]" and "t  (+) tx ` .[Y]" ..
    from this(2) obtain ty where "ty  .[Y]" and "t = tx + ty" ..
    with tx  .[X] show "t  ?A" by (rule PPs_UnI)
  qed
qed

corollary PPs_insert: ".[insert x X] = (e. (+) (Poly_Mapping.single x e) ` .[X])"
proof -
  have ".[insert x X] = .[{x}  X]" by simp
  also have "... = (t.[{x}]. (+) t ` .[X])" by (fact PPs_Un)
  also have "... = (e. (+) (Poly_Mapping.single x e) ` .[X])" by (simp add: PPs_singleton)
  finally show ?thesis .
qed

corollary PPs_insertI:
  assumes "tx  .[X]" and "t = Poly_Mapping.single x e + tx"
  shows "t  .[insert x X]"
proof -
  from assms(1) have "t  (+) (Poly_Mapping.single x e) ` .[X]" unfolding assms(2) by (rule imageI)
  with UNIV_I show ?thesis unfolding PPs_insert by (rule UN_I)
qed

corollary PPs_insertE:
  assumes "t  .[insert x X]"
  obtains e tx where "tx  .[X]" and "t = Poly_Mapping.single x e + tx"
proof -
  from assms obtain e where "t  (+) (Poly_Mapping.single x e) ` .[X]" unfolding PPs_insert ..
  then obtain tx where "tx  .[X]" and "t = Poly_Mapping.single x e + tx" ..
  thus ?thesis ..
qed

lemma PPs_Int: ".[X  Y] = .[X]  .[Y]"
  by (auto simp: PPs_def)

lemma PPs_INT: ".[ X] =  (PPs ` X)"
  by (auto simp: PPs_def)

subsubsection @{const Polys}

lemma Polys_alt: "P[X] = {p. indets p  X}"
  by (auto simp: Polys_def PPs_def indets_def)

lemma PolysI: "keys p  .[X]  p  P[X]"
  by (simp add: Polys_def)

lemma PolysI_alt: "indets p  X  p  P[X]"
  by (simp add: Polys_alt)

lemma PolysD:
  assumes "p  P[X]"
  shows "keys p  .[X]" and "indets p  X"
  using assms by (simp add: Polys_def, simp add: Polys_alt)

lemma Polys_empty: "P[{}] = ((range (Poly_Mapping.single 0))::(('x 0 nat) 0 'b::zero) set)"
proof (rule set_eqI)
  fix p :: "('x 0 nat) 0 'b::zero"
  show "p  P[{}]  p  range (Poly_Mapping.single 0)"
  proof
    assume "p  P[{}]"
    hence "keys p  .[{}]" by (rule PolysD)
    also have "... = {0}" by simp
    finally have "keys p  {0}" .
    hence "Poly_Mapping.single 0 (lookup p 0) = p" by (rule keys_subset_singleton_imp_monomial)
    from this[symmetric] UNIV_I show "p  range (Poly_Mapping.single 0)" ..
  next
    assume "p  range (Poly_Mapping.single 0)"
    then obtain c where "p = monomial c 0" ..
    thus "p  P[{}]" by (simp add: Polys_def)
  qed
qed

lemma Polys_UNIV [simp]: "P[UNIV] = UNIV"
  by (simp add: Polys_def)

lemma zero_in_Polys: "0  P[X]"
  by (simp add: Polys_def)

lemma one_in_Polys: "1  P[X]"
  by (simp add: Polys_def zero_in_PPs)

lemma Polys_mono: "X  Y  P[X]  P[Y]"
  by (auto simp: Polys_alt)

lemma Polys_closed_monomial: "t  .[X]  monomial c t  P[X]"
  using indets_monomial_subset[where c=c and t=t] by (auto simp: Polys_alt PPs_def)

lemma Polys_closed_plus: "p  P[X]  q  P[X]  p + q  P[X]"
  using indets_plus_subset[of p q] by (auto simp: Polys_alt PPs_def)

lemma Polys_closed_uminus: "p  P[X]  -p  P[X]"
  by (simp add: Polys_def keys_uminus)

lemma Polys_closed_minus: "p  P[X]  q  P[X]  p - q  P[X]"
  using indets_minus_subset[of p q] by (auto simp: Polys_alt PPs_def)

lemma Polys_closed_monom_mult: "t  .[X]  p  P[X]  punit.monom_mult c t p  P[X]"
  using indets_monom_mult_subset[of c t p] by (auto simp: Polys_alt PPs_def)

corollary Polys_closed_map_scale: "p  P[X]  (c::_::semiring_0)  p  P[X]"
  unfolding punit.map_scale_eq_monom_mult using zero_in_PPs by (rule Polys_closed_monom_mult)

lemma Polys_closed_times: "p  P[X]  q  P[X]  p * q  P[X]"
  using indets_times_subset[of p q] by (auto simp: Polys_alt PPs_def)

lemma Polys_closed_power: "p  P[X]  p ^ m  P[X]"
  by (induct m) (auto intro: one_in_Polys Polys_closed_times)

lemma Polys_closed_sum: "(a. a  A  f a  P[X])  sum f A  P[X]"
  by (induct A rule: infinite_finite_induct) (auto intro: zero_in_Polys Polys_closed_plus)

lemma Polys_closed_prod: "(a. a  A  f a  P[X])  prod f A  P[X]"
  by (induct A rule: infinite_finite_induct) (auto intro: one_in_Polys Polys_closed_times)

lemma Polys_closed_sum_list: "(x. x  set xs  x  P[X])  sum_list xs  P[X]"
  by (induct xs) (auto intro: zero_in_Polys Polys_closed_plus)

lemma Polys_closed_except: "p  P[X]  except p T  P[X]"
  by (auto intro!: PolysI simp: keys_except dest!: PolysD(1))

lemma times_in_PolysD:
  assumes "p * q  P[X]" and "p  P[X]" and "p  (0::('x::linorder 0 nat) 0 'a::semiring_no_zero_divisors)"
  shows "q  P[X]"
proof -
  define qX where "qX = except q (- .[X])"
  define qY where "qY = except q .[X]"
  have q: "q = qX + qY" by (simp only: qX_def qY_def add.commute flip: except_decomp)
  have "qX  P[X]" by (rule PolysI) (simp add: qX_def keys_except)
  with assms(2) have "p * qX  P[X]" by (rule Polys_closed_times)
  show ?thesis
  proof (cases "qY = 0")
    case True
    with qX  P[X] show ?thesis by (simp add: q)
  next
    case False
    with assms(3) have "p * qY  0" by simp
    hence "keys (p * qY)  {}" by simp
    then obtain t where "t  keys (p * qY)" by blast
    then obtain t1 t2 where "t2  keys qY" and t: "t = t1 + t2" by (rule in_keys_timesE)
    have "t  .[X]" unfolding t
    proof
      assume "t1 + t2  .[X]"
      hence "t1 + t2 - t1  .[X]" by (rule PPs_closed_minus)
      hence "t2  .[X]" by simp
      with t2  keys qY show False by (simp add: qY_def keys_except)
    qed
    have "t  keys (p * qX)"
    proof
      assume "t  keys (p * qX)"
      also from p * qX  P[X] have "  .[X]" by (rule PolysD)
      finally have "t  .[X]" .
      with t  .[X] show False ..
    qed
    with t  keys (p * qY) have "t  keys (p * qX + p * qY)" by (rule in_keys_plusI2)
    also have " = keys (p * q)" by (simp only: q algebra_simps)
    finally have "p * q  P[X]" using t  .[X] by (auto simp: Polys_def)
    thus ?thesis using assms(1) ..
  qed
qed

lemma poly_mapping_plus_induct_Polys [consumes 1, case_names 0 plus]:
  assumes "p  P[X]" and "P 0"
    and "p c t. t  .[X]  p  P[X]  c  0  t  keys p  P p  P (monomial c t + p)"
  shows "P p"
  using assms(1)
proof (induct p rule: poly_mapping_plus_induct)
  case 1
  show ?case by (fact assms(2))
next
  case step: (2 p c t)
  from step.hyps(1) have 1: "keys (monomial c t) = {t}" by simp
  also from step.hyps(2) have "  keys p = {}" by simp
  finally have "keys (monomial c t + p) = keys (monomial c t)  keys p" by (rule keys_add[symmetric])
  hence "keys (monomial c t + p) = insert t (keys p)" by (simp only: 1 flip: insert_is_Un)
  moreover from step.prems(1) have "keys (monomial c t + p)  .[X]" by (rule PolysD)
  ultimately have "t  .[X]" and "keys p  .[X]" by blast+
  from this(2) have "p  P[X]" by (rule PolysI)
  hence "P p" by (rule step.hyps)
  with t  .[X] p  P[X] step.hyps(1, 2) show ?case by (rule assms(3))
qed

lemma Polys_Int: "P[X  Y] = P[X]  P[Y]"
  by (auto simp: Polys_def PPs_Int)

lemma Polys_INT: "P[ X] =  (Polys ` X)"
  by (auto simp: Polys_def PPs_INT)

subsection ‹Substitution Homomorphism›

text ‹The substitution homomorphism defined here is more general than @{const insertion}, since
  it replaces indeterminates by @{emph ‹polynomials›} rather than coefficients, and therefore
  constructs new polynomials.›

definition subst_pp :: "('x  (('y 0 nat) 0 'a))  ('x 0 nat)  (('y 0 nat) 0 'a::comm_semiring_1)"
  where "subst_pp f t = (xkeys t. (f x) ^ (lookup t x))"

definition poly_subst :: "('x  (('y 0 nat) 0 'a))  (('x 0 nat) 0 'a)  (('y 0 nat) 0 'a::comm_semiring_1)"
  where "poly_subst f p = (tkeys p. punit.monom_mult (lookup p t) 0 (subst_pp f t))"

lemma subst_pp_alt: "subst_pp f t = (x. (f x) ^ (lookup t x))"
proof -
  from finite_keys have "subst_pp f t = (x. if x  keys t then (f x) ^ (lookup t x) else 1)"
    unfolding subst_pp_def by (rule Prod_any.conditionalize)
  also have "... = (x. (f x) ^ (lookup t x))" by (rule Prod_any.cong) (simp add: in_keys_iff)
  finally show ?thesis .
qed

lemma subst_pp_zero [simp]: "subst_pp f 0 = 1"
  by (simp add: subst_pp_def)

lemma subst_pp_trivial_not_zero:
  assumes "t  0"
  shows "subst_pp (λ_. 0) t = (0::(_ 0 'b::comm_semiring_1))"
  unfolding subst_pp_def using finite_keys
proof (rule prod_zero)
  from assms have "keys t  {}" by simp
  then obtain x where "x  keys t" by blast
  thus "xkeys t. 0 ^ lookup t x = (0::(_ 0 'b))"
  proof
    from x  keys t have "0 < lookup t x" by (simp add: in_keys_iff)
    thus "0 ^ lookup t x = (0::(_ 0 'b))" by (rule Power.semiring_1_class.zero_power)
  qed
qed

lemma subst_pp_single: "subst_pp f (Poly_Mapping.single x e) = (f x) ^ e"
  by (simp add: subst_pp_def)

corollary subst_pp_trivial: "subst_pp (λ_. 0) t = (if t = 0 then 1 else 0)"
  by (simp split: if_split add: subst_pp_trivial_not_zero)

lemma power_lookup_not_one_subset_keys: "{x. f x ^ (lookup t x)  1}  keys t"
proof (rule, simp)
  fix x
  assume "f x ^ (lookup t x)  1"
  thus "x  keys t" unfolding in_keys_iff by (metis power_0)
qed

corollary finite_power_lookup_not_one: "finite {x. f x ^ (lookup t x)  1}"
  by (rule finite_subset, fact power_lookup_not_one_subset_keys, fact finite_keys)

lemma subst_pp_plus: "subst_pp f (s + t) = subst_pp f s * subst_pp f t"
  by (simp add: subst_pp_alt lookup_add power_add, rule Prod_any.distrib, (fact finite_power_lookup_not_one)+)

lemma subst_pp_id:
  assumes "x. x  keys t  f x = monomial 1 (Poly_Mapping.single x 1)"
  shows "subst_pp f t = monomial 1 t"
proof -
  have "subst_pp f t = (xkeys t. monomial 1 (Poly_Mapping.single x (lookup t x)))"
  proof (simp only: subst_pp_def, rule prod.cong, fact refl)
    fix x
    assume "x  keys t"
    thus "f x ^ lookup t x = monomial 1 (Poly_Mapping.single x (lookup t x))"
      by (simp add: assms monomial_single_power)
  qed
  also have "... = monomial 1 t"
    by (simp add: punit.monomial_prod_sum[symmetric] poly_mapping_sum_monomials)
  finally show ?thesis .
qed

lemma in_indets_subst_ppE:
  assumes "x  indets (subst_pp f t)"
  obtains y where "y  keys t" and "x  indets (f y)"
proof -
  note assms
  also have "indets (subst_pp f t)  (ykeys t. indets ((f y) ^ (lookup t y)))" unfolding subst_pp_def
    by (rule indets_prod_subset)
  finally obtain y where "y  keys t" and "x  indets ((f y) ^ (lookup t y))" ..
  note this(2)
  also have "indets ((f y) ^ (lookup t y))  indets (f y)" by (rule indets_power_subset)
  finally have "x  indets (f y)" .
  with y  keys t show ?thesis ..
qed

lemma subst_pp_by_monomials:
  assumes "y. y  keys t  f y = monomial (c y) (s y)"
  shows "subst_pp f t = monomial (ykeys t. (c y) ^ lookup t y) (ykeys t. lookup t y  s y)"
  by (simp add: subst_pp_def assms monomial_power_map_scale punit.monomial_prod_sum)

lemma poly_deg_subst_pp_eq_zeroI:
  assumes "x. x  keys t  poly_deg (f x) = 0"
  shows "poly_deg (subst_pp f t) = 0"
proof -
  have "poly_deg (subst_pp f t)  (xkeys t. poly_deg ((f x) ^ (lookup t x)))"
    unfolding subst_pp_def by (fact poly_deg_prod_le)
  also have "... = 0"
  proof (rule sum.neutral, rule)
    fix x
    assume "x  keys t"
    hence "poly_deg (f x) = 0" by (rule assms)
    have "f x ^ lookup t x = (i=0..<lookup t x. f x)" by simp
    also have "poly_deg ...  (i=0..<lookup t x. poly_deg (f x))" by (rule poly_deg_prod_le)
    also have "... = 0" by (simp add: poly_deg (f x) = 0)
    finally show "poly_deg (f x ^ lookup t x) = 0" by simp
  qed
  finally show ?thesis by simp
qed

lemma poly_deg_subst_pp_le:
  assumes "x. x  keys t  poly_deg (f x)  1"
  shows "poly_deg (subst_pp f t)  deg_pm t"
proof -
  have "poly_deg (subst_pp f t)  (xkeys t. poly_deg ((f x) ^ (lookup t x)))"
    unfolding subst_pp_def by (fact poly_deg_prod_le)
  also have "...  (xkeys t. lookup t x)"
  proof (rule sum_mono)
    fix x
    assume "x  keys t"
    hence "poly_deg (f x)  1" by (rule assms)
    have "f x ^ lookup t x = (i=0..<lookup t x. f x)" by simp
    also have "poly_deg ...  (i=0..<lookup t x. poly_deg (f x))" by (rule poly_deg_prod_le)
    also from poly_deg (f x)  1 have "...  (i=0..<lookup t x. 1)" by (rule sum_mono)
    finally show "poly_deg (f x ^ lookup t x)  lookup t x" by simp
  qed
  also have "... = deg_pm t" by (rule deg_pm_superset[symmetric], fact subset_refl, fact finite_keys)
  finally show ?thesis by simp
qed

lemma poly_subst_alt: "poly_subst f p = (t. punit.monom_mult (lookup p t) 0 (subst_pp f t))"
proof -
  from finite_keys have "poly_subst f p = (t. if t  keys p then punit.monom_mult (lookup p t) 0 (subst_pp f t) else 0)"
    unfolding poly_subst_def by (rule Sum_any.conditionalize)
  also have " = (t. punit.monom_mult (lookup p t) 0 (subst_pp f t))"
    by (rule Sum_any.cong) (simp add: in_keys_iff)
  finally show ?thesis .
qed

lemma poly_subst_trivial [simp]: "poly_subst (λ_. 0) p = monomial (lookup p 0) 0"
  by (simp add: poly_subst_def subst_pp_trivial if_distrib in_keys_iff cong: if_cong)
      (metis mult.right_neutral times_monomial_left)

lemma poly_subst_zero [simp]: "poly_subst f 0 = 0"
  by (simp add: poly_subst_def)

lemma monom_mult_lookup_not_zero_subset_keys:
  "{t. punit.monom_mult (lookup p t) 0 (subst_pp f t)  0}  keys p"
proof (rule, simp)
  fix t
  assume "punit.monom_mult (lookup p t) 0 (subst_pp f t)  0"
  thus "t  keys p" unfolding in_keys_iff by (metis punit.monom_mult_zero_left)
qed

corollary finite_monom_mult_lookup_not_zero:
  "finite {t. punit.monom_mult (lookup p t) 0 (subst_pp f t)  0}"
  by (rule finite_subset, fact monom_mult_lookup_not_zero_subset_keys, fact finite_keys)

lemma poly_subst_plus: "poly_subst f (p + q) = poly_subst f p + poly_subst f q"
  by (simp add: poly_subst_alt lookup_add punit.monom_mult_dist_left, rule Sum_any.distrib,
      (fact finite_monom_mult_lookup_not_zero)+)

lemma poly_subst_uminus: "poly_subst f (-p) = - poly_subst f (p::('x 0 nat) 0 'b::comm_ring_1)"
  by (simp add: poly_subst_def keys_uminus punit.monom_mult_uminus_left sum_negf)

lemma poly_subst_minus:
  "poly_subst f (p - q) = poly_subst f p - poly_subst f (q::('x 0 nat) 0 'b::comm_ring_1)"
proof -
  have "poly_subst f (p + (-q)) = poly_subst f p + poly_subst f (-q)" by (fact poly_subst_plus)
  thus ?thesis by (simp add: poly_subst_uminus)
qed

lemma poly_subst_monomial: "poly_subst f (monomial c t) = punit.monom_mult c 0 (subst_pp f t)"
  by (simp add: poly_subst_def lookup_single)

corollary poly_subst_one [simp]: "poly_subst f 1 = 1"
  by (simp add: single_one[symmetric] poly_subst_monomial punit.monom_mult_monomial del: single_one)

lemma poly_subst_times: "poly_subst f (p * q) = poly_subst f p * poly_subst f q"
proof -
  have bij: "bij (λ(l, n, m). (m, l, n))"
    by (auto intro!: bijI injI simp add: image_def)
  let ?P = "keys p"
  let ?Q = "keys q"
  let ?PQ = "{s + t | s t. lookup p s  0  lookup q t  0}"
  have fin_PQ: "finite ?PQ"
    by (rule finite_not_eq_zero_sumI, simp_all)
  have fin_1: "finite {l. lookup p l * (qa. lookup q qa when t = l + qa)  0}" for t
  proof (rule finite_subset)
    show "{l. lookup p l * (qa. lookup q qa when t = l + qa)  0}  keys p"
      by (rule, auto simp: in_keys_iff)
  qed (fact finite_keys)
  have fin_2: "finite {v. (lookup q v when t = u + v)  0}" for t u
  proof (rule finite_subset)
    show "{v. (lookup q v when t = u + v)  0}  keys q"
      by (rule, auto simp: in_keys_iff)
  qed (fact finite_keys)
  have fin_3: "finite {v. (lookup p u * lookup q v when t = u + v)  0}" for t u
  proof (rule finite_subset)
    show "{v. (lookup p u * lookup q v when t = u + v)  0}  keys q"
      by (rule, auto simp add: in_keys_iff simp del: lookup_not_eq_zero_eq_in_keys)
  qed (fact finite_keys)
  have "(t. punit.monom_mult (lookup (p * q) t) 0 (subst_pp f t)) =
        (t. u. punit.monom_mult (lookup p u * (v. lookup q v when t = u + v)) 0 (subst_pp f t))"
    by (simp add: times_poly_mapping.rep_eq prod_fun_def punit.monom_mult_Sum_any_left[OF fin_1])
  also have " = (t. u. v. (punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t)) when t = u + v)"
    by (simp add: Sum_any_right_distrib[OF fin_2] punit.monom_mult_Sum_any_left[OF fin_3] mult_when punit.when_monom_mult)
  also have " = (t. ((u, v). (punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t)) when t = u + v))"
    by (subst (2) Sum_any.cartesian_product [of "?P × ?Q"]) (auto simp: in_keys_iff)
  also have " = ((t, u, v). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
    apply (subst Sum_any.cartesian_product [of "?PQ × (?P × ?Q)"])
    apply (auto simp: fin_PQ in_keys_iff)
    apply (metis monomial_0I mult_not_zero times_monomial_left)
    done
  also have " = ((u, v, t). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
    using bij by (rule Sum_any.reindex_cong [of "λ(u, v, t). (t, u, v)"]) (simp add: fun_eq_iff)
  also have " = ((u, v). t. punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
    apply (subst Sum_any.cartesian_product2 [of "(?P × ?Q) × ?PQ"])
    apply (auto simp: fin_PQ in_keys_iff)
    apply (metis monomial_0I mult_not_zero times_monomial_left)
    done
  also have " = ((u, v). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f u * subst_pp f v))"
    by (simp add: subst_pp_plus)
  also have " = (u. v. punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f u * subst_pp f v))"
    by (subst Sum_any.cartesian_product [of "?P × ?Q"]) (auto simp: in_keys_iff)
  also have " = (u. v. (punit.monom_mult (lookup p u) 0 (subst_pp f u)) * (punit.monom_mult (lookup q v) 0 (subst_pp f v)))"
    by (simp add: times_monomial_left[symmetric] ac_simps mult_single)
  also have " = (t. punit.monom_mult (lookup p t) 0 (subst_pp f t)) *
                  (t. punit.monom_mult (lookup q t) 0 (subst_pp f t))"
    by (rule Sum_any_product [symmetric], (fact finite_monom_mult_lookup_not_zero)+)
  finally show ?thesis by (simp add: poly_subst_alt)
qed

corollary poly_subst_monom_mult:
  "poly_subst f (punit.monom_mult c t p) = punit.monom_mult c 0 (subst_pp f t * poly_subst f p)"
  by (simp only: times_monomial_left[symmetric] poly_subst_times poly_subst_monomial mult.assoc)

corollary poly_subst_monom_mult':
  "poly_subst f (punit.monom_mult c t p) = (punit.monom_mult c 0 (subst_pp f t)) * poly_subst f p"
  by (simp only: times_monomial_left[symmetric] poly_subst_times poly_subst_monomial)

lemma poly_subst_sum: "poly_subst f (sum p A) = (aA. poly_subst f (p a))"
  by (rule fun_sum_commute, simp_all add: poly_subst_plus)

lemma poly_subst_prod: "poly_subst f (prod p A) = (aA. poly_subst f (p a))"
  by (rule fun_prod_commute, simp_all add: poly_subst_times)

lemma poly_subst_power: "poly_subst f (p ^ n) = (poly_subst f p) ^ n"
  by (induct n, simp_all add: poly_subst_times)

lemma poly_subst_subst_pp: "poly_subst f (subst_pp g t) = subst_pp (λx. poly_subst f (g x)) t"
  by (simp only: subst_pp_def poly_subst_prod poly_subst_power)

lemma poly_subst_poly_subst: "poly_subst f (poly_subst g p) = poly_subst (λx. poly_subst f (g x)) p"
proof -
  have "poly_subst f (poly_subst g p) =
          poly_subst f (tkeys p. punit.monom_mult (lookup p t) 0 (subst_pp g t))"
    by (simp only: poly_subst_def)
  also have " = (tkeys p. punit.monom_mult (lookup p t) 0 (subst_pp (λx. poly_subst f (g x)) t))"
    by (simp add: poly_subst_sum poly_subst_monom_mult poly_subst_subst_pp)
  also have " = poly_subst (λx. poly_subst f (g x)) p" by (simp only: poly_subst_def)
  finally show ?thesis .
qed

lemma poly_subst_id:
  assumes "x. x  indets p  f x = monomial 1 (Poly_Mapping.single x 1)"
  shows "poly_subst f p = p"
proof -
  have "poly_subst f p = (tkeys p. monomial (lookup p t) t)"
  proof (simp only: poly_subst_def, rule sum.cong, fact refl)
    fix t
    assume "t  keys p"
    have eq: "subst_pp f t = monomial 1 t"
      by (rule subst_pp_id, rule assms, erule in_indetsI, fact t  keys p)
    show "punit.monom_mult (lookup p t) 0 (subst_pp f t) = monomial (lookup p t) t"
      by (simp add: eq punit.monom_mult_monomial)
  qed
  also have "... = p" by (simp only: poly_mapping_sum_monomials)
  finally show ?thesis .
qed

lemma in_keys_poly_substE:
  assumes "t  keys (poly_subst f p)"
  obtains s where "s  keys p" and "t  keys (subst_pp f s)"
proof -
  note assms
  also have "keys (poly_subst f p)  (tkeys p. keys (punit.monom_mult (lookup p t) 0 (subst_pp f t)))"
    unfolding poly_subst_def by (rule keys_sum_subset)
  finally obtain s where "s  keys p" and "t  keys (punit.monom_mult (lookup p s) 0 (subst_pp f s))" ..
  note this(2)
  also have "  (+) 0 ` keys (subst_pp f s)" by (rule punit.keys_monom_mult_subset[simplified])
  also have " = keys (subst_pp f s)" by simp
  finally have "t  keys (subst_pp f s)" .
  with s  keys p show ?thesis ..
qed

lemma in_indets_poly_substE:
  assumes "x  indets (poly_subst f p)"
  obtains y where "y  indets p" and "x  indets (f y)"
proof -
  note assms
  also have "indets (poly_subst f p)  (tkeys p. indets (punit.monom_mult (lookup p t) 0 (subst_pp f t)))"
    unfolding poly_subst_def by (rule indets_sum_subset)
  finally obtain t where "t  keys p" and "x  indets (punit.monom_mult (lookup p t) 0 (subst_pp f t))" ..
  note this(2)
  also have "indets (punit.monom_mult (lookup p t) 0 (subst_pp f t))  keys (0::('a 0 nat))  indets (subst_pp f t)"
    by (rule indets_monom_mult_subset)
  also have "... = indets (subst_pp f t)" by simp
  finally obtain y where "y  keys t" and "x  indets (f y)" by (rule in_indets_subst_ppE)
  from this(1) t  keys p have "y  indets p" by (rule in_indetsI)
  from this x  indets (f y) show ?thesis ..
qed

lemma poly_deg_poly_subst_eq_zeroI:
  assumes "x. x  indets p  poly_deg (f x) = 0"
  shows "poly_deg (poly_subst (f::_  (('y 0 _) 0 _)) (p::('x 0 _) 0 'b::comm_semiring_1)) = 0"
proof (cases "p = 0")
  case True
  thus ?thesis by simp
next
  case False
  have "poly_deg (poly_subst f p)  Max (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
    unfolding poly_subst_def by (fact poly_deg_sum_le)
  also have "...  0"
  proof (rule Max.boundedI)
    show "finite (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
      by (simp add: finite_image_iff)
  next
    from False show "poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p  {}" by simp
  next
    fix d
    assume "d  poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p"
    then obtain t where "t  keys p" and d: "d = poly_deg (punit.monom_mult (lookup p t) 0 (subst_pp f t))"
      by fastforce
    have "d  deg_pm (0::'y 0 nat) + poly_deg (subst_pp f t)"
      unfolding d by (fact poly_deg_monom_mult_le)
    also have "... = poly_deg (subst_pp f t)" by simp
    also have "... = 0" by (rule poly_deg_subst_pp_eq_zeroI, rule assms, erule in_indetsI, fact)
    finally show "d  0" .
  qed
  finally show ?thesis by simp
qed

lemma poly_deg_poly_subst_le:
  assumes "x. x  indets p  poly_deg (f x)  1"
  shows "poly_deg (poly_subst (f::_  (('y 0 _) 0 _)) (p::('x 0 nat) 0 'b::comm_semiring_1))  poly_deg p"
proof (cases "p = 0")
  case True
  thus ?thesis by simp
next
  case False
  have "poly_deg (poly_subst f p)  Max (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
    unfolding poly_subst_def by (fact poly_deg_sum_le)
  also have "...  poly_deg p"
  proof (rule Max.boundedI)
    show "finite (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
      by (simp add: finite_image_iff)
  next
    from False show "poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p  {}" by simp
  next
    fix d
    assume "d  poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p"
    then obtain t where "t  keys p" and d: "d = poly_deg (punit.monom_mult (lookup p t) 0 (subst_pp f t))"
      by fastforce
    have "d  deg_pm (0::'y 0 nat) + poly_deg (subst_pp f t)"
      unfolding d by (fact poly_deg_monom_mult_le)
    also have "... = poly_deg (subst_pp f t)" by simp
    also have "...  deg_pm t" by (rule poly_deg_subst_pp_le, rule assms, erule in_indetsI, fact)
    also from t  keys p have "...  poly_deg p" by (rule poly_deg_max_keys)
    finally show "d  poly_deg p" .
  qed
  finally show ?thesis by simp
qed

lemma subst_pp_cong: "s = t  (x. x  keys t  f x = g x)  subst_pp f s = subst_pp g t"
  by (simp add: subst_pp_def)

lemma poly_subst_cong:
  assumes "p = q" and "x. x  indets q  f x = g x"
  shows "poly_subst f p = poly_subst g q"
proof (simp add: poly_subst_def assms(1), rule sum.cong)
  fix t
  assume "t  keys q"
  {
    fix x
    assume "x  keys t"
    with t  keys q have "x  indets q" by (auto simp: indets_def)
    hence "f x = g x" by (rule assms(2))
  }
  thus "punit.monom_mult (lookup q t) 0 (subst_pp f t) = punit.monom_mult (lookup q t) 0 (subst_pp g t)"
    by (simp cong: subst_pp_cong)
qed (fact refl)

lemma Polys_homomorphismE:
  obtains h where "p q. h (p + q) = h p + h q" and "p q. h (p * q) = h p * h q"
    and "p::('x 0 nat) 0 'a::comm_ring_1. h (h p) = h p" and "range h = P[X]"
proof -
  let ?f = "λx. if x  X then monomial (1::'a) (Poly_Mapping.single x 1) else 1"

  have 1: "poly_subst ?f p = p" if "p  P[X]" for p
  proof (rule poly_subst_id)
    fix x
    assume "x  indets p"
    also from that have "  X" by (rule PolysD)
    finally show "?f x = monomial 1 (Poly_Mapping.single x 1)" by simp
  qed

  have 2: "poly_subst ?f p  P[X]" for p
  proof (intro PolysI_alt subsetI)
    fix x
    assume "x  indets (poly_subst ?f p)"
    then obtain y where "x  indets (?f y)" by (rule in_indets_poly_substE)
    thus "x  X" by (simp add: indets_monomial split: if_split_asm)
  qed

  from poly_subst_plus poly_subst_times show ?thesis
  proof
    fix p
    from 2 show "poly_subst ?f (poly_subst ?f p) = poly_subst ?f p" by (rule 1)
  next
    show "range (poly_subst ?f) = P[X]"
    proof (intro set_eqI iffI)
      fix p :: "_ 0 'a"
      assume "p  P[X]"
      hence "p = poly_subst ?f p" by (simp only: 1)
      thus "p  range (poly_subst ?f)" by (rule image_eqI) simp
    qed (auto intro: 2)
  qed
qed

lemma in_idealE_Polys_finite:
  assumes "finite B" and "B  P[X]" and "p  P[X]" and "(p::('x 0 nat) 0 'a::comm_ring_1)  ideal B"
  obtains q where "b. q b  P[X]" and "p = (bB. q b * b)"
proof -
  obtain h where "p q. h (p + q) = h p + h q" and "p q. h (p * q) = h p * h q"
    and "p::('x 0 nat) 0 'a. h (h p) = h p" and rng[symmetric]: "range h = P[X]"
    by (rule Polys_homomorphismE) blast
  from this(1-3) assms obtain q where "b. q b  P[X]" and "p = (bB. q b * b)"
    unfolding rng by (rule in_idealE_homomorphism_finite) blast
  thus ?thesis ..
qed

corollary in_idealE_Polys:
  assumes "B  P[X]" and "p  P[X]" and "p  ideal B"
  obtains A q where "finite A" and "A  B" and "b. q b  P[X]" and "p = (bA. q b * b)"
proof -
  from assms(3) obtain A where "finite A" and "A  B" and "p  ideal A"
    by (rule ideal.span_finite_subset)
  from this(2) assms(1) have "A  P[X]" by (rule subset_trans)
  with finite A obtain q where "b. q b  P[X]" and "p = (bA. q b * b)"
    using assms(2) p  ideal A by (rule in_idealE_Polys_finite) blast
  with finite A A  B show ?thesis ..
qed

lemma ideal_induct_Polys [consumes 3, case_names 0 plus]:
  assumes "F  P[X]" and "p  P[X]" and "p  ideal F"
  assumes "P 0" and "c q h. c  P[X]  q  F  P h  h  P[X]  P (c * q + h)"
  shows "P (p::('x 0 nat) 0 'a::comm_ring_1)"
proof -
  obtain h where "p q. h (p + q) = h p + h q" and "p q. h (p * q) = h p * h q"
    and "p::('x 0 nat) 0 'a. h (h p) = h p" and rng[symmetric]: "range h = P[X]"
    by (rule Polys_homomorphismE) blast
  from this(1-3) assms show ?thesis
    unfolding rng by (rule ideal_induct_homomorphism) blast
qed

lemma image_poly_subst_ideal_subset: "poly_subst g ` ideal F  ideal (poly_subst g ` F)"
proof (intro subsetI, elim imageE)
  fix h f
  assume h: "h = poly_subst g f"
  assume "f  ideal F"
  thus "h  ideal (poly_subst g ` F)" unfolding h
  proof (induct f rule: ideal.span_induct_alt)
    case base
    show ?case by (simp add: ideal.span_zero)
  next
    case (step c f h)
    from step.hyps(1) have "poly_subst g f  ideal (poly_subst g ` F)"
      by (intro ideal.span_base imageI)
    hence "poly_subst g c * poly_subst g f  ideal (poly_subst g ` F)" by (rule ideal.span_scale)
    hence "poly_subst g c * poly_subst g f + poly_subst g h  ideal (poly_subst g ` F)"
      using step.hyps(2) by (rule ideal.span_add)
    thus ?case by (simp only: poly_subst_plus poly_subst_times)
  qed
qed

subsection ‹Evaluating Polynomials›

lemma lookup_times_zero:
  "lookup (p * q) 0 = lookup p 0 * lookup q (0::'a::{comm_powerprod,ninv_comm_monoid_add})"
proof -
  have eq: "(vkeys q. lookup q v when t + v = 0) = (lookup q 0 when t = 0)" for t
  proof -
    have "(vkeys q. lookup q v when t + v = 0) = (vkeys q  {0}. lookup q v when t + v = 0)"
    proof (intro sum.mono_neutral_right ballI)
      fix v
      assume "v  keys q - keys q  {0}"
      hence "v  0" by blast
      hence "t + v  0" using plus_eq_zero_2 by blast
      thus "(lookup q v when t + v = 0) = 0" by simp
    qed simp_all
    also have " = (lookup q 0 when t = 0)" by (cases "0  keys q") (simp_all add: in_keys_iff)
    finally show ?thesis .
  qed
  have "(tkeys p. lookup p t * lookup q 0 when t = 0) =
          (tkeys p  {0}. lookup p t * lookup q 0 when t = 0)"
  proof (intro sum.mono_neutral_right ballI)
    fix t
    assume "t  keys p - keys p  {0}"
    hence "t  0" by blast
    thus "(lookup p t * lookup q 0 when t = 0) = 0" by simp
  qed simp_all
  also have " = lookup p 0 * lookup q 0" by (cases "0  keys p") (simp_all add: in_keys_iff)
  finally show ?thesis by (simp add: lookup_times eq when_distrib)
qed

corollary lookup_prod_zero:
  "lookup (prod f I) 0 = (iI. lookup (f i) (0::_::{comm_powerprod,ninv_comm_monoid_add}))"
  by (induct I rule: infinite_finite_induct) (simp_all add: lookup_times_zero)

corollary lookup_power_zero:
  "lookup (p ^ k) 0 = lookup p (0::_::{comm_powerprod,ninv_comm_monoid_add}) ^ k"
  by (induct k) (simp_all add: lookup_times_zero)

definition poly_eval :: "('x  'a)  (('x 0 nat) 0 'a)  'a::comm_semiring_1"
  where "poly_eval a p = lookup (poly_subst (λy. monomial (a y) (0::'x 0 nat)) p) 0"

lemma poly_eval_alt: "poly_eval a p = (tkeys p. lookup p t * (xkeys t. a x ^ lookup t x))"
  by (simp add: poly_eval_def poly_subst_def lookup_sum lookup_times_zero subst_pp_def
          lookup_prod_zero lookup_power_zero flip: times_monomial_left)

lemma poly_eval_monomial: "poly_eval a (monomial c t) = c * (xkeys t. a x ^ lookup t x)"
  by (simp add: poly_eval_def poly_subst_monomial subst_pp_def punit.lookup_monom_mult
      lookup_prod_zero lookup_power_zero)

lemma poly_eval_zero [simp]: "poly_eval a 0 = 0"
  by (simp only: poly_eval_def poly_subst_zero lookup_zero)

lemma poly_eval_zero_left [simp]: "poly_eval 0 p = lookup p 0"
  by (simp add: poly_eval_def)

lemma poly_eval_plus: "poly_eval a (p + q) = poly_eval a p + poly_eval a q"
  by (simp only: poly_eval_def poly_subst_plus lookup_add)

lemma poly_eval_uminus [simp]: "poly_eval a (- p) = - poly_eval (a::_::comm_ring_1) p"
  by (simp only: poly_eval_def poly_subst_uminus lookup_uminus)

lemma poly_eval_minus: "poly_eval a (p - q) = poly_eval a p - poly_eval (a::_::comm_ring_1) q"
  by (simp only: poly_eval_def poly_subst_minus lookup_minus)

lemma poly_eval_one [simp]: "poly_eval a 1 = 1"
  by (simp add: poly_eval_def lookup_one)

lemma poly_eval_times: "poly_eval a (p * q) = poly_eval a p * poly_eval a q"
  by (simp only: poly_eval_def poly_subst_times lookup_times_zero)

lemma poly_eval_power: "poly_eval a (p ^ m) = poly_eval a p ^ m"
  by (induct m) (simp_all add: poly_eval_times)

lemma poly_eval_sum: "poly_eval a (sum f I) = (iI. poly_eval a (f i))"
  by (induct I rule: infinite_finite_induct) (simp_all add: poly_eval_plus)

lemma poly_eval_prod: "poly_eval a (prod f I) = (iI. poly_eval a (f i))"
  by (induct I rule: infinite_finite_induct) (simp_all add: poly_eval_times)

lemma poly_eval_cong: "p = q  (x. x  indets q  a x = b x)  poly_eval a p = poly_eval b q"
  by (simp add: poly_eval_def cong: poly_subst_cong)

lemma indets_poly_eval_subset:
  "indets (poly_eval a p)   (indets ` a ` indets p)   (indets ` lookup p ` keys p)"
proof (induct p rule: poly_mapping_plus_induct)
  case 1
  show ?case by simp
next
  case (2 p c t)
  have "keys (monomial c t + p) = keys (monomial c t)  keys p"
    by (rule keys_plus_eqI) (simp add: 2(2))
  with 2(1) have eq1: "keys (monomial c t + p) = insert t (keys p)" by simp
  hence eq2: "indets (monomial c t + p) = keys t  indets p" by (simp add: indets_def)
  from 2(2) have eq3: "lookup (monomial c t + p) t = c" by (simp add: lookup_add in_keys_iff)
  have eq4: "lookup (monomial c t + p) s = lookup p s" if "s  keys p" for s
    using that 2(2) by (auto simp: lookup_add lookup_single when_def)
  have "indets (poly_eval a (monomial c t + p)) =
          indets (c * (xkeys t. a x ^ lookup t x) + poly_eval a p)"
    by (simp only: poly_eval_plus poly_eval_monomial)
  also have "  indets (c * (xkeys t. a x ^ lookup t x))  indets (poly_eval a p)"
    by (fact indets_plus_subset)
  also have "  indets c  ( (indets ` a ` keys t)) 
                    ( (indets ` a ` indets p)   (indets ` lookup p ` keys p))"
  proof (intro Un_mono 2(3))
    have "indets (c * (xkeys t. a x ^ lookup t x))  indets c  indets (xkeys t. a x ^ lookup t x)"
      by (fact indets_times_subset)
    also have "indets (xkeys t. a x ^ lookup t x)  (xkeys t. indets (a x ^ lookup t x))"
      by (fact indets_prod_subset)
    also have "  (xkeys t. indets (a x))" by (intro UN_mono subset_refl indets_power_subset)
    also have " =  (indets ` a ` keys t)" by simp
    finally show "indets (c * (xkeys t. a x ^ lookup t x))  indets c   (indets ` a ` keys t)"
      by blast
  qed
  also have " =  (indets ` a ` indets (monomial c t + p)) 
                     (indets ` lookup (monomial c t + p) ` keys (monomial c t + p))"
    by (simp add: eq1 eq2 eq3 eq4 Un_commute Un_assoc Un_left_commute)
  finally show ?case .
qed

lemma image_poly_eval_ideal: "poly_eval a ` ideal F = ideal (poly_eval a ` F)"
proof (intro image_ideal_eq_surj poly_eval_plus poly_eval_times surjI)
  fix x
  show "poly_eval a (monomial x 0) = x" by (simp add: poly_eval_monomial)
qed

subsection ‹Replacing Indeterminates›

definition map_indets where "map_indets f = poly_subst (λx. monomial 1 (Poly_Mapping.single (f x) 1))"

lemma
  shows map_indets_zero [simp]: "map_indets f 0 = 0"
    and map_indets_one [simp]: "map_indets f 1 = 1"
    and map_indets_uminus [simp]: "map_indets f (- r) = - map_indets f (r::_ 0 _::comm_ring_1)"
    and map_indets_plus: "map_indets f (p + q) = map_indets f p + map_indets f q"
    and map_indets_minus: "map_indets f (r - s) = map_indets f r - map_indets f s"
    and map_indets_times: "map_indets f (p * q) = map_indets f p * map_indets f q"
    and map_indets_power [simp]: "map_indets f (p ^ m) = map_indets f p ^ m"
    and map_indets_sum: "map_indets f (sum g A) = (aA. map_indets f (g a))"
    and map_indets_prod: "map_indets f (prod g A) = (aA. map_indets f (g a))"
  by (simp_all add: map_indets_def poly_subst_uminus poly_subst_plus poly_subst_minus poly_subst_times
      poly_subst_power poly_subst_sum poly_subst_prod)

lemma map_indets_monomial:
  "map_indets f (monomial c t) = monomial c (xkeys t. Poly_Mapping.single (f x) (lookup t x))"
  by (simp add: map_indets_def poly_subst_monomial subst_pp_def monomial_power_map_scale
      punit.monom_mult_monomial flip: punit.monomial_prod_sum)

lemma map_indets_id: "(x. x  indets p  f x = x)  map_indets f p = p"
  by (simp add: map_indets_def poly_subst_id)

lemma map_indets_map_indets: "map_indets f (map_indets g p) = map_indets (f  g) p"
  by (simp add: map_indets_def poly_subst_poly_subst poly_subst_monomial subst_pp_single)

lemma map_indets_cong: "p = q  (x. x  indets q  f x = g x)  map_indets f p = map_indets g q"
  unfolding map_indets_def by (simp cong: poly_subst_cong)

lemma poly_subst_map_indets: "poly_subst f (map_indets g p) = poly_subst (f  g) p"
  by (simp add: map_indets_def poly_subst_poly_subst poly_subst_monomial subst_pp_single comp_def)

lemma poly_eval_map_indets: "poly_eval a (map_indets g p) = poly_eval (a  g) p"
  by (simp add: poly_eval_def poly_subst_map_indets comp_def)
      (simp add: poly_subst_def lookup_sum lookup_times_zero subst_pp_def lookup_prod_zero
          lookup_power_zero flip: times_monomial_left)

lemma map_indets_inverseE_Polys:
  assumes "inj_on f X" and "p  P[X]"
  shows "map_indets (the_inv_into X f) (map_indets f p) = p"
  unfolding map_indets_map_indets
proof (rule map_indets_id)
  fix x
  assume "x  indets p"
  also from assms(2) have "  X" by (rule PolysD)
  finally show "(the_inv_into X f  f) x = x" using assms(1) by (auto intro: the_inv_into_f_f)
qed

lemma map_indets_inverseE:
  assumes "inj f"
  obtains g where "g = the_inv f" and "g  f = id" and "map_indets g  map_indets f = id"
proof -
  define g where "g = the_inv f"
  moreover from assms have eq: "g  f = id" by (auto intro!: ext the_inv_f_f simp: g_def)
  moreover have "map_indets g  map_indets f = id"
    by (rule ext) (simp add: map_indets_map_indets eq map_indets_id)
  ultimately show ?thesis ..
qed

lemma indets_map_indets_subset: "indets (map_indets f (p::_ 0 'a::comm_semiring_1))  f ` indets p"
proof
  fix x
  assume "x  indets (map_indets f p)"
  then obtain y where "y  indets p" and "x  indets (monomial (1::'a) (Poly_Mapping.single (f y) 1))"
    unfolding map_indets_def by (rule in_indets_poly_substE)
  from this(2) have x: "x = f y" by (simp add: indets_monomial)
  from y  indets p show "x  f ` indets p" unfolding x by (rule imageI)
qed

corollary map_indets_in_Polys: "map_indets f p  P[f ` indets p]"
  using indets_map_indets_subset by (rule PolysI_alt)

lemma indets_map_indets:
  assumes "inj_on f (indets p)"
  shows "indets (map_indets f p) = f ` indets p"
  using indets_map_indets_subset
proof (rule subset_antisym)
  let ?g = "the_inv_into (indets p) f"
  have "p = map_indets ?g (map_indets f p)" unfolding map_indets_map_indets
    by (rule sym, rule map_indets_id) (simp add: assms the_inv_into_f_f)
  also have "indets   ?g ` indets (map_indets f p)" by (fact indets_map_indets_subset)
  finally have "f ` indets p  f ` ?g ` indets (map_indets f p)" by (rule image_mono)
  also have " = (λx. x) ` indets (map_indets f p)" unfolding image_image using refl
  proof (rule image_cong)
    fix x
    assume "x  indets (map_indets f p)"
    with indets_map_indets_subset have "x  f ` indets p" ..
    with assms show "f (?g x) = x" by (rule f_the_inv_into_f)
  qed
  finally show "f ` indets p  indets (map_indets f p)" by simp
qed

lemma image_map_indets_Polys: "map_indets f ` P[X] = (P[f ` X]::(_ 0 'a::comm_semiring_1) set)"
proof (intro set_eqI iffI)
  fix p :: "_ 0 'a"
  assume "p  map_indets f ` P[X]"
  then obtain q where "q  P[X]" and "p = map_indets f q" ..
  note this(2)
  also have "map_indets f q  P[f ` indets q]" by (fact map_indets_in_Polys)
  also from q  _ have "  P[f ` X]" by (auto intro!: Polys_mono imageI dest: PolysD)
  finally show "p  P[f ` X]" .
next
  fix p :: "_ 0 'a"
  assume "p  P[f ` X]"
  define g where "g = (λy. SOME x. x  X  f x = y)"
  have "g y  X  f (g y) = y" if "y  indets p" for y
  proof -
    note that
    also from p  _ have "indets p  f ` X" by (rule PolysD)
    finally obtain x where "x  X" and "y = f x" ..
    hence "x  X  f x = y" by simp
    thus ?thesis unfolding g_def by (rule someI)
  qed
  hence 1: "g y  X" and 2: "f (g y) = y" if "y  indets p" for y using that by simp_all
  show "p  map_indets f ` P[X]"
  proof
    show "p = map_indets f (map_indets g p)"
      by (rule sym) (simp add: map_indets_map_indets map_indets_id 2)
  next
    have "map_indets g p  P[g ` indets p]" by (fact map_indets_in_Polys)
    also have "  P[X]" by (auto intro!: Polys_mono 1)
    finally show "map_indets g p  P[X]" .
  qed
qed

corollary range_map_indets: "range (map_indets f) = P[range f]"
proof -
  have "range (map_indets f) = map_indets f ` P[UNIV]" by simp
  also have " = P[range f]" by (simp only: image_map_indets_Polys)
  finally show ?thesis .
qed

lemma in_keys_map_indetsE:
  assumes "t  keys (map_indets f (p::_ 0 'a::comm_semiring_1))"
  obtains s where "s  keys p" and "t = (xkeys s. Poly_Mapping.single (f x) (lookup s x))"
proof -
  let ?f = "(λx. monomial (1::'a) (Poly_Mapping.single (f x) 1))"
  from assms obtain s where "s  keys p" and "t  keys (subst_pp ?f s)" unfolding map_indets_def
    by (rule in_keys_poly_substE)
  note this(2)
  also have "  {xkeys s. Poly_Mapping.single (f x) (lookup s x)}"
    by (simp add: subst_pp_def monomial_power_map_scale flip: punit.monomial_prod_sum)
  finally have "t = (xkeys s. Poly_Mapping.single (f x) (lookup s x))" by simp
  with s  keys p show ?thesis ..
qed

lemma keys_map_indets_subset:
  "keys (map_indets f p)  (λt. xkeys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p"
  by (auto elim: in_keys_map_indetsE)

lemma keys_map_indets:
  assumes "inj_on f (indets p)"
  shows "keys (map_indets f p) = (λt. xkeys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p"
  using keys_map_indets_subset
proof (rule subset_antisym)
  let ?g = "the_inv_into (indets p) f"
  have "p = map_indets ?g (map_indets f p)" unfolding map_indets_map_indets
    by (rule sym, rule map_indets_id) (simp add: assms the_inv_into_f_f)
  also have "keys   (λt. xkeys t. monomial (lookup t x) (?g x)) ` keys (map_indets f p)"
    by (rule keys_map_indets_subset)
  finally have "(λt. xkeys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p 
                (λt. xkeys t. Poly_Mapping.single (f x) (lookup t x)) `
                (λt. xkeys t. Poly_Mapping.single (?g x) (lookup t x)) ` keys (map_indets f p)"
    by (rule image_mono)
  also from refl have " = (λt. x. Poly_Mapping.single (f x) (lookup t x)) `
                       (λt. xkeys t. Poly_Mapping.single (?g x) (lookup t x)) ` keys (map_indets f p)"
    by (rule image_cong)
        (smt Sum_any.conditionalize Sum_any.cong finite_keys not_in_keys_iff_lookup_eq_zero single_zero)
  also have " = (λt. t) ` keys (map_indets f p)" unfolding image_image using refl
  proof (rule image_cong)
    fix t
    assume "t  keys (map_indets f p)"
    have "(x. monomial (lookup (ykeys t. Poly_Mapping.single (?g y) (lookup t y)) x) (f x)) =
          (x. ykeys t. monomial (lookup t y when ?g y = x) (f x))"
      by (simp add: lookup_sum lookup_single monomial_sum)
    also have " = (xindets p. ykeys t. Poly_Mapping.single (f x) (lookup t y when ?g y = x))"
    proof (intro Sum_any.expand_superset finite_indets subsetI)
      fix x
      assume "x  {a. (ykeys t. Poly_Mapping.single (f a) (lookup t y when ?g y = a))  0}"
      hence "(ykeys t. Poly_Mapping.single (f x) (lookup t y when ?g y = x))  0" by simp
      then obtain y where "y  keys t" and *: "Poly_Mapping.single (f x) (lookup t y when ?g y = x)  0"
        by (rule sum.not_neutral_contains_not_neutral)
      from this(1) have "y  indets (map_indets f p)" using t  _ by (rule in_indetsI)
      with indets_map_indets_subset have "y  f ` indets p" ..
      from * have "x = ?g y" by (simp add: when_def split: if_split_asm)
      also from assms y  f ` indets p subset_refl have "  indets p" by (rule the_inv_into_into)
      finally show "x  indets p" .
    qed
    also have " = (ykeys t. xindets p. Poly_Mapping.single (f x) (lookup t y when ?g y = x))"
      by (fact sum.swap)
    also from refl have " = (ykeys t. Poly_Mapping.single y (lookup t y))"
    proof (rule sum.cong)
      fix x
      assume "x  keys t"
      hence "x  indets (map_indets f p)" using t  _ by (rule in_indetsI)
      with indets_map_indets_subset have "x  f ` indets p" ..
      with assms have "?g x  indets p" using subset_refl by (rule the_inv_into_into)
      hence "{?g x}  indets p" by simp
      with finite_indets have "(yindets p. Poly_Mapping.single (f y) (lookup t x when ?g x = y)) =
                                (y{?g x}. Poly_Mapping.single (f y) (lookup t x when ?g x = y))"
        by (rule sum.mono_neutral_right) (simp add: monomial_0_iff when_def)
      also from assms x  f ` indets p have " = Poly_Mapping.single x (lookup t x)"
        by (simp add: f_the_inv_into_f)
      finally show "(yindets p. Poly_Mapping.single (f y) (lookup t x when ?g x = y)) =
                      Poly_Mapping.single x (lookup t x)" .
    qed
    also have " = t" by (fact poly_mapping_sum_monomials)
    finally show "(x. monomial (lookup (ykeys t. Poly_Mapping.single (?g y) (lookup t y)) x) (f x)) = t" .
  qed
  also have " = keys (map_indets f p)" by simp
  finally show "(λt. xkeys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p  keys (map_indets f p)" .
qed

lemma poly_deg_map_indets_le: "poly_deg (map_indets f p)  poly_deg p"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (map_indets f p)"
  then obtain s where "s  keys p" and t: "t = (xkeys s. Poly_Mapping.single (f x) (lookup s x))"
    by (rule in_keys_map_indetsE)
  from this(1) have "deg_pm s  poly_deg p" by (rule poly_deg_max_keys)
  thus "deg_pm t  poly_deg p"
    by (simp add: t deg_pm_sum deg_pm_single deg_pm_superset[OF subset_refl])
qed

lemma poly_deg_map_indets:
  assumes "inj_on f (indets p)"
  shows "poly_deg (map_indets f p) = poly_deg p"
proof -
  from assms have "deg_pm ` keys (map_indets f p) = deg_pm ` keys p"
    by (simp add: keys_map_indets image_image deg_pm_sum deg_pm_single
          flip: deg_pm_superset[OF subset_refl])
  thus ?thesis by (auto simp: poly_deg_def)
qed

lemma map_indets_inj_on_PolysI:
  assumes "inj_on (f::'x  'y) X"
  shows "inj_on ((map_indets f)::_  _ 0 'a::comm_semiring_1) P[X]"
proof (rule inj_onI)
  fix p q :: "_ 0 'a"
  assume "p  P[X]"
  with assms have 1: "map_indets (the_inv_into X f) (map_indets f p) = p" (is "map_indets ?g _ = _")
    by (rule map_indets_inverseE_Polys)
  assume "q  P[X]"
  with assms have "map_indets ?g (map_indets f q) = q" by (rule map_indets_inverseE_Polys)
  moreover assume "map_indets f p = map_indets f q"
  ultimately show "p = q" using 1 by (simp add: map_indets_map_indets)
qed

lemma map_indets_injI:
  assumes "inj f"
  shows "inj (map_indets f)"
proof -
  from assms have "inj_on (map_indets f) P[UNIV]" by (rule map_indets_inj_on_PolysI)
  thus ?thesis by simp
qed

lemma image_map_indets_ideal:
  assumes "inj f"
  shows "map_indets f ` ideal F = ideal (map_indets f ` (F::(_ 0 'a::comm_ring_1) set))  P[range f]"
proof
  from map_indets_plus map_indets_times have "map_indets f ` ideal F  ideal (map_indets f ` F)"
    by (rule image_ideal_subset)
  moreover from subset_UNIV have "map_indets f ` ideal F  range (map_indets f)" by (rule image_mono)
  ultimately show "map_indets f ` ideal F  ideal (map_indets f ` F)  P[range f]"
    unfolding range_map_indets by blast
next
  show "ideal (map_indets f ` F)  P[range f]  map_indets f ` ideal F"
  proof
    fix p
    assume "p  ideal (map_indets f ` F)  P[range f]"
    hence "p  ideal (map_indets f ` F)" and "p  range (map_indets f)"
      by (simp_all add: range_map_indets)
    from this(1) obtain F0 q where "F0  map_indets f ` F" and p: "p = (f'F0. q f' * f')"
      by (rule ideal.spanE)
    from this(1) obtain F' where "F'  F" and F0: "F0 = map_indets f ` F'" by (rule subset_imageE)
    from assms obtain g where "map_indets g  map_indets f = (id::_  _ 0 'a)"
      by (rule map_indets_inverseE)
    hence eq: "map_indets g (map_indets f p') = p'" for p'::"_ 0 'a"
      by (simp add: pointfree_idE)
    from assms have "inj (map_indets f)" by (rule map_indets_injI)
    from this subset_UNIV have "inj_on (map_indets f) F'" by (rule inj_on_subset)
    from p  range _ obtain p' where "p = map_indets f p'" ..
    hence "p = map_indets f (map_indets g p)" by (simp add: eq)
    also from inj_on _ F' have " = map_indets f (f'F'. map_indets g (q (map_indets f f')) * f')"
      by (simp add: p F0 sum.reindex map_indets_sum map_indets_times eq)
    finally have "p = map_indets f (f'F'. map_indets g (q (map_indets f f')) * f')" .
    moreover have "(f'F'. map_indets g (q (map_indets f f')) * f')  ideal F"
    proof
      show "(f'F'. map_indets g (q (map_indets f f')) * f')  ideal F'" by (rule ideal.sum_in_spanI)
    next
      from F'  F show "ideal F'  ideal F" by (rule ideal.span_mono)
    qed
    ultimately show "p  map_indets f ` ideal F" by (rule image_eqI)
  qed
qed

subsection ‹Homogeneity›

definition homogeneous :: "(('x 0 nat) 0 'a::zero)  bool"
  where "homogeneous p  (skeys p. tkeys p. deg_pm s = deg_pm t)"

definition hom_component :: "(('x 0 nat) 0 'a)  nat  (('x 0 nat) 0 'a::zero)"
  where "hom_component p n = except p {t. deg_pm t  n}"

definition hom_components :: "(('x 0 nat) 0 'a)  (('x 0 nat) 0 'a::zero) set"
  where "hom_components p = hom_component p ` deg_pm ` keys p"

definition homogeneous_set :: "(('x 0 nat) 0 'a::zero) set  bool"
  where "homogeneous_set A  (aA. n. hom_component a n  A)"

lemma homogeneousI: "(s t. s  keys p  t  keys p  deg_pm s = deg_pm t)  homogeneous p"
  unfolding homogeneous_def by blast

lemma homogeneousD: "homogeneous p  s  keys p  t  keys p  deg_pm s = deg_pm t"
  unfolding homogeneous_def by blast

lemma homogeneousD_poly_deg:
  assumes "homogeneous p" and "t  keys p"
  shows "deg_pm t = poly_deg p"
proof (rule antisym)
  from assms(2) show "deg_pm t  poly_deg p" by (rule poly_deg_max_keys)
next
  show "poly_deg p  deg_pm t"
  proof (rule poly_deg_leI)
    fix s
    assume "s  keys p"
    with assms(1) have "deg_pm s = deg_pm t" using assms(2) by (rule homogeneousD)
    thus "deg_pm s  deg_pm t" by simp
  qed
qed

lemma homogeneous_monomial [simp]: "homogeneous (monomial c t)"
  by (auto split: if_split_asm intro: homogeneousI)

corollary homogeneous_zero [simp]: "homogeneous 0" and homogeneous_one [simp]: "homogeneous 1"
  by (simp_all only: homogeneous_monomial flip: single_zero[of 0] single_one)

lemma homogeneous_uminus_iff [simp]: "homogeneous (- p)  homogeneous p"
  by (auto intro!: homogeneousI dest: homogeneousD simp: keys_uminus)

lemma homogeneous_monom_mult: "homogeneous p  homogeneous (punit.monom_mult c t p)"
  by (auto intro!: homogeneousI elim!: punit.keys_monom_multE simp: deg_pm_plus dest: homogeneousD)

lemma homogeneous_monom_mult_rev:
  assumes "c  (0::'a::semiring_no_zero_divisors)" and "homogeneous (punit.monom_mult c t p)"
  shows "homogeneous p"
proof (rule homogeneousI)
  fix s s'
  assume "s  keys p"
  hence 1: "t + s  keys (punit.monom_mult c t p)"
    using assms(1) by (rule punit.keys_monom_multI[simplified])
  assume "s'  keys p"
  hence "t + s'  keys (punit.monom_mult c t p)"
    using assms(1) by (rule punit.keys_monom_multI[simplified])
  with assms(2) 1 have "deg_pm (t + s) = deg_pm (t + s')" by (rule homogeneousD)
  thus "deg_pm s = deg_pm s'" by (simp add: deg_pm_plus)
qed

lemma homogeneous_times:
  assumes "homogeneous p" and "homogeneous q"
  shows "homogeneous (p * q)"
proof (rule homogeneousI)
  fix s t
  assume "s  keys (p * q)"
  then obtain sp sq where sp: "sp  keys p" and sq: "sq  keys q" and s: "s = sp + sq"
    by (rule in_keys_timesE)
  assume "t  keys (p * q)"
  then obtain tp tq where tp: "tp  keys p" and tq: "tq  keys q" and t: "t = tp + tq"
    by (rule in_keys_timesE)
  from assms(1) sp tp have "deg_pm sp = deg_pm tp" by (rule homogeneousD)
  moreover from assms(2) sq tq have "deg_pm sq = deg_pm tq" by (rule homogeneousD)
  ultimately show "deg_pm s = deg_pm t" by (simp only: s t deg_pm_plus)
qed

lemma lookup_hom_component: "lookup (hom_component p n) = (λt. lookup p t when deg_pm t = n)"
  by (rule ext) (simp add: hom_component_def lookup_except)

lemma keys_hom_component: "keys (hom_component p n) = {t. t  keys p  deg_pm t = n}"
  by (auto simp: hom_component_def keys_except)

lemma keys_hom_componentD:
  assumes "t  keys (hom_component p n)"
  shows "t  keys p" and "deg_pm t = n"
  using assms by (simp_all add: keys_hom_component)

lemma homogeneous_hom_component: "homogeneous (hom_component p n)"
  by (auto dest: keys_hom_componentD intro: homogeneousI)

lemma hom_component_zero [simp]: "hom_component 0 = 0"
  by (rule ext) (simp add: hom_component_def)

lemma hom_component_zero_iff: "hom_component p n = 0  (tkeys p. deg_pm t  n)"
  by (metis (mono_tags, lifting) empty_iff keys_eq_empty_iff keys_hom_component mem_Collect_eq subsetI subset_antisym)

lemma hom_component_uminus [simp]: "hom_component (- p) = - hom_component p"
  by (intro ext poly_mapping_eqI) (simp add: hom_component_def lookup_except)

lemma hom_component_plus: "hom_component (p + q) n = hom_component p n + hom_component q n"
  by (rule poly_mapping_eqI) (simp add: hom_component_def lookup_except lookup_add)

lemma hom_component_minus: "hom_component (p - q) n = hom_component p n - hom_component q n"
  by (rule poly_mapping_eqI) (simp add: hom_component_def lookup_except lookup_minus)

lemma hom_component_monom_mult:
  "punit.monom_mult c t (hom_component p n) = hom_component (punit.monom_mult c t p) (deg_pm t + n)"
  by (auto simp: hom_component_def lookup_except punit.lookup_monom_mult deg_pm_minus deg_pm_mono intro!: poly_mapping_eqI)

lemma hom_component_inject:
  assumes "t  keys p" and "hom_component p (deg_pm t) = hom_component p n"
  shows "deg_pm t = n"
proof -
  from assms(1) have "t  keys (hom_component p (deg_pm t))" by (simp add: keys_hom_component)
  hence "0  lookup (hom_component p (deg_pm t)) t" by (simp add: in_keys_iff)
  also have "lookup (hom_component p (deg_pm t)) t = lookup (hom_component p n) t"
    by (simp only: assms(2))
  also have " = (lookup p t when deg_pm t = n)" by (simp only: lookup_hom_component)
  finally show ?thesis by simp
qed

lemma hom_component_of_homogeneous:
  assumes "homogeneous p"
  shows "hom_component p n = (p when n = poly_deg p)"
proof (cases "n = poly_deg p")
  case True
  have "hom_component p n = p"
  proof (rule poly_mapping_eqI)
    fix t
    show "lookup (hom_component p n) t = lookup p t"
    proof (cases "t  keys p")
      case True
      with assms have "deg_pm t = n" unfolding n = poly_deg p by (rule homogeneousD_poly_deg)
      thus ?thesis by (simp add: lookup_hom_component)
    next
      case False
      moreover from this have "t  keys (hom_component p n)" by (simp add: keys_hom_component)
      ultimately show ?thesis by (simp add: in_keys_iff)
    qed
  qed
  with True show ?thesis by simp
next
  case False
  have "hom_component p n = 0" unfolding hom_component_zero_iff
  proof (intro ballI notI)
    fix t
    assume "t  keys p"
    with assms have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
    moreover assume "deg_pm t = n"
    ultimately show False using False by simp
  qed
  with False show ?thesis by simp
qed

lemma hom_components_zero [simp]: "hom_components 0 = {}"
  by (simp add: hom_components_def)

lemma hom_components_zero_iff [simp]: "hom_components p = {}  p = 0"
  by (simp add: hom_components_def)

lemma hom_components_uminus: "hom_components (- p) = uminus ` hom_components p"
  by (simp add: hom_components_def keys_uminus image_image)

lemma hom_components_monom_mult:
  "hom_components (punit.monom_mult c t p) = (if c = 0 then {} else punit.monom_mult c t ` hom_components p)"
  for c::"'a::semiring_no_zero_divisors"
  by (simp add: hom_components_def punit.keys_monom_mult image_image deg_pm_plus hom_component_monom_mult)

lemma hom_componentsI: "q = hom_component p (deg_pm t)  t  keys p  q  hom_components p"
  unfolding hom_components_def by blast

lemma hom_componentsE:
  assumes "q  hom_components p"
  obtains t where "t  keys p" and "q = hom_component p (deg_pm t)"
  using assms unfolding hom_components_def by blast

lemma hom_components_of_homogeneous:
  assumes "homogeneous p"
  shows "hom_components p = (if p = 0 then {} else {p})"
proof (split if_split, intro conjI impI)
  assume "p  0"
  have "deg_pm ` keys p = {poly_deg p}"
  proof (rule set_eqI)
    fix n
    have "n  deg_pm ` keys p  n = poly_deg p"
    proof
      assume "n  deg_pm ` keys p"
      then obtain t where "t  keys p" and "n = deg_pm t" ..
      from assms this(1) have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
      thus "n = poly_deg p" by (simp only: n = deg_pm t)
    next
      assume "n = poly_deg p"
      from p  0 have "keys p  {}" by simp
      then obtain t where "t  keys p" by blast
      with assms have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
      hence "n = deg_pm t" by (simp only: n = poly_deg p)
      with t  keys p show "n  deg_pm ` keys p" by (rule rev_image_eqI)
    qed
    thus "n  deg_pm ` keys p  n  {poly_deg p}" by simp
  qed
  with assms show "hom_components p = {p}"
    by (simp add: hom_components_def hom_component_of_homogeneous)
qed simp

lemma finite_hom_components: "finite (hom_components p)"
  unfolding hom_components_def using finite_keys by (intro finite_imageI)

lemma hom_components_homogeneous: "q  hom_components p  homogeneous q"
  by (elim hom_componentsE) (simp only: homogeneous_hom_component)

lemma hom_components_nonzero: "q  hom_components p  q  0"
  by (auto elim!: hom_componentsE simp: hom_component_zero_iff)

lemma deg_pm_hom_components:
  assumes "q1  hom_components p" and "q2  hom_components p" and "t1  keys q1" and "t2  keys q2"
  shows "deg_pm t1 = deg_pm t2  q1 = q2"
proof -
  from assms(1) obtain s1 where "s1  keys p" and q1: "q1 = hom_component p (deg_pm s1)"
    by (rule hom_componentsE)
  from assms(3) have t1: "deg_pm t1 = deg_pm s1" unfolding q1 by (rule keys_hom_componentD)
  from assms(2) obtain s2 where "s2  keys p" and q2: "q2 = hom_component p (deg_pm s2)"
    by (rule hom_componentsE)
  from assms(4) have t2: "deg_pm t2 = deg_pm s2" unfolding q2 by (rule keys_hom_componentD)
  from s1  keys p show ?thesis by (auto simp: q1 q2 t1 t2 dest: hom_component_inject)
qed

lemma poly_deg_hom_components:
  assumes "q1  hom_components p" and "q2  hom_components p"
  shows "poly_deg q1 = poly_deg q2  q1 = q2"
proof -
  from assms(1) have "homogeneous q1" and "q1  0"
    by (rule hom_components_homogeneous, rule hom_components_nonzero)
  from this(2) have "keys q1  {}" by simp
  then obtain t1 where "t1  keys q1" by blast
  with homogeneous q1 have t1: "deg_pm t1 = poly_deg q1" by (rule homogeneousD_poly_deg)
  from assms(2) have "homogeneous q2" and "q2  0"
    by (rule hom_components_homogeneous, rule hom_components_nonzero)
  from this(2) have "keys q2  {}" by simp
  then obtain t2 where "t2  keys q2" by blast
  with homogeneous q2 have t2: "deg_pm t2 = poly_deg q2" by (rule homogeneousD_poly_deg)
  from assms t1  keys q1 t2  keys q2 have "deg_pm t1 = deg_pm t2  q1 = q2"
    by (rule deg_pm_hom_components)
  thus ?thesis by (simp only: t1 t2)
qed

lemma hom_components_keys_disjoint:
  assumes "q1  hom_components p" and "q2  hom_components p" and "q1  q2"
  shows "keys q1  keys q2 = {}"
proof (rule ccontr)
  assume "keys q1  keys q2  {}"
  then obtain t where "t  keys q1" and "t  keys q2" by blast
  with assms(1, 2) have "deg_pm t = deg_pm t  q1 = q2" by (rule deg_pm_hom_components)
  with assms(3) show False by simp
qed

lemma Keys_hom_components: "Keys (hom_components p) = keys p"
  by (auto simp: Keys_def hom_components_def keys_hom_component)

lemma lookup_hom_components: "q  hom_components p  t  keys q  lookup q t = lookup p t"
  by (auto elim!: hom_componentsE simp: keys_hom_component lookup_hom_component)

lemma poly_deg_hom_components_le:
  assumes "q  hom_components p"
  shows "poly_deg q  poly_deg p"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys q"
  also from assms have "  Keys (hom_components p)" by (rule keys_subset_Keys)
  also have " = keys p" by (fact Keys_hom_components)
  finally show "deg_pm t  poly_deg p" by (rule poly_deg_max_keys)
qed

lemma sum_hom_components: "(hom_components p) = p"
proof (rule poly_mapping_eqI)
  fix t
  show "lookup ((hom_components p)) t = lookup p t" unfolding lookup_sum
  proof (cases "t  keys p")
    case True
    also have "keys p = Keys (hom_components p)" by (simp only: Keys_hom_components)
    finally obtain q where q: "q  hom_components p" and t: "t  keys q" by (rule in_KeysE)
    from this(1) have "(q0hom_components p. lookup q0 t) =
                        (q0insert q (hom_components p). lookup q0 t)"
      by (simp only: insert_absorb)
    also from finite_hom_components have " = lookup q t + (q0hom_components p - {q}. lookup q0 t)"
      by (rule sum.insert_remove)
    also from q t have " = lookup p t + (q0hom_components p - {q}. lookup q0 t)"
      by (simp only: lookup_hom_components)
    also have "(q0hom_components p - {q}. lookup q0 t) = 0"
    proof (intro sum.neutral ballI)
      fix q0
      assume "q0  hom_components p - {q}"
      hence "q0  hom_components p" and "q  q0" by blast+
      with q have "keys q  keys q0 = {}" by (rule hom_components_keys_disjoint)
      with t have "t  keys q0" by blast
      thus "lookup q0 t = 0" by (simp add: in_keys_iff)
    qed
    finally show "(qhom_components p. lookup q t) = lookup p t" by simp
  next
    case False
    hence "t  Keys (hom_components p)" by (simp add: Keys_hom_components)
    hence "qhom_components p. lookup q t = 0" by (simp add: Keys_def in_keys_iff)
    hence "(qhom_components p. lookup q t) = 0" by (rule sum.neutral)
    also from False have " = lookup p t" by (simp add: in_keys_iff)
    finally show "(qhom_components p. lookup q t) = lookup p t" .
  qed
qed

lemma homogeneous_setI: "(a n. a  A  hom_component a n  A)  homogeneous_set A"
  by (simp add: homogeneous_set_def)

lemma homogeneous_setD: "homogeneous_set A  a  A  hom_component a n  A"
  by (simp add: homogeneous_set_def)

lemma homogeneous_set_Polys: "homogeneous_set (P[X]::(_ 0 'a::zero) set)"
proof (intro homogeneous_setI PolysI subsetI)
  fix p::"_ 0 'a" and n t
  assume "p  P[X]"
  assume "t  keys (hom_component p n)"
  hence "t  keys p" by (rule keys_hom_componentD)
  also from p  P[X] have "  .[X]" by (rule PolysD)
  finally show "t  .[X]" .
qed

lemma homogeneous_set_IntI: "homogeneous_set A  homogeneous_set B  homogeneous_set (A  B)"
  by (simp add: homogeneous_set_def)

lemma homogeneous_setD_hom_components:
  assumes "homogeneous_set A" and "a  A" and "b  hom_components a"
  shows "b  A"
proof -
  from assms(3) obtain t::"'a 0 nat" where "b = hom_component a (deg_pm t)"
    by (rule hom_componentsE)
  also from assms(1, 2) have "  A" by (rule homogeneous_setD)
  finally show ?thesis .
qed

lemma zero_in_homogeneous_set:
  assumes "homogeneous_set A" and "A  {}"
  shows "0  A"
proof -
  from assms(2) obtain a where "a  A" by blast
  have "lookup a t = 0" if "deg_pm t = Suc (poly_deg a)" for t
  proof (rule ccontr)
    assume "lookup a t  0"
    hence "t  keys a" by (simp add: in_keys_iff)
    hence "deg_pm t  poly_deg a" by (rule poly_deg_max_keys)
    thus False by (simp add: that)
  qed
  hence "0 = hom_component a (Suc (poly_deg a))"
    by (intro poly_mapping_eqI) (simp add: lookup_hom_component when_def)
  also from assms(1) a  A have "  A" by (rule homogeneous_setD)
  finally show ?thesis .
qed

lemma homogeneous_ideal:
  assumes "f. f  F  homogeneous f" and "p  ideal F"
  shows "hom_component p n  ideal F"
proof -
  from assms(2) have "p  punit.pmdl F" by simp
  thus ?thesis
  proof (induct p rule: punit.pmdl_induct)
    case module_0
    show ?case by (simp add: ideal.span_zero)
  next
    case (module_plus a f c t)
    let ?f = "punit.monom_mult c t f"
    from module_plus.hyps(3) have "f  punit.pmdl F" by (simp add: ideal.span_base)
    hence *: "?f  punit.pmdl F" by (rule punit.pmdl_closed_monom_mult)
    from module_plus.hyps(3) have "homogeneous f" by (rule assms(1))
    hence "homogeneous ?f" by (rule homogeneous_monom_mult)
    hence "hom_component ?f n = (?f when n = poly_deg ?f)" by (rule hom_component_of_homogeneous)
    also from * have "  ideal F" by (simp add: when_def ideal.span_zero)
    finally have "hom_component ?f n  ideal F" .
    with module_plus.hyps(2) show ?case unfolding hom_component_plus by (rule ideal.span_add)
  qed
qed

corollary homogeneous_set_homogeneous_ideal:
  "(f. f  F  homogeneous f)  homogeneous_set (ideal F)"
  by (auto intro: homogeneous_setI homogeneous_ideal)

corollary homogeneous_ideal':
  assumes "f. f  F  homogeneous f" and "p  ideal F" and "q  hom_components p"
  shows "q  ideal F"
  using _ assms(2, 3)
proof (rule homogeneous_setD_hom_components)
  from assms(1) show "homogeneous_set (ideal F)" by (rule homogeneous_set_homogeneous_ideal)
qed

lemma homogeneous_idealE_homogeneous:
  assumes "f. f  F  homogeneous f" and "p  ideal F" and "homogeneous p"
  obtains F' q where "finite F'" and "F'  F" and "p = (fF'. q f * f)" and "f. homogeneous (q f)"
    and "f. f  F'  poly_deg (q f * f) = poly_deg p" and "f. f  F'  q f = 0"
proof -
  from assms(2) obtain F'' q' where "finite F''" and "F''  F" and p: "p = (fF''. q' f * f)"
    by (rule ideal.spanE)
  let ?A = "λf. {h  hom_components (q' f). poly_deg h + poly_deg f = poly_deg p}"
  let ?B = "λf. {h  hom_components (q' f). poly_deg h + poly_deg f  poly_deg p}"
  define F' where "F' = {f  F''. ((?A f)) * f  0}"
  define q where "q = (λf. ((?A f)) when f  F')"
  have "F'  F''" by (simp add: F'_def)
  hence "F'  F" using F''  F by (rule subset_trans)
  have 1: "deg_pm t + poly_deg f = poly_deg p" if "f  F'" and "t  keys (q f)" for f t
  proof -
    from that have "t  keys ((?A f))" by (simp add: q_def)
    also have "  (h?A f. keys h)" by (fact keys_sum_subset)
    finally obtain h where "h  ?A f" and "t  keys h" ..
    from this(1) have "h  hom_components (q' f)" and eq: "poly_deg h + poly_deg f = poly_deg p"
      by simp_all
    from this(1) have "homogeneous h" by (rule hom_components_homogeneous)
    hence "deg_pm t = poly_deg h" using t  keys h by (rule homogeneousD_poly_deg)
    thus ?thesis by (simp only: eq)
  qed
  have 2: "deg_pm t = poly_deg p" if "f  F'" and "t  keys (q f * f)" for f t
  proof -
    from that(1) F'  F have "f  F" ..
    hence "homogeneous f" by (rule assms(1))
    from that(2) obtain s1 s2 where "s1  keys (q f)" and "s2  keys f" and t: "t = s1 + s2"
      by (rule in_keys_timesE)
    from that(1) this(1) have "deg_pm s1 + poly_deg f = poly_deg p" by (rule 1)
    moreover from homogeneous f s2  keys f have "deg_pm s2 = poly_deg f"
      by (rule homogeneousD_poly_deg)
    ultimately show ?thesis by (simp add: t deg_pm_plus)
  qed
  from F'  F'' finite F'' have "finite F'" by (rule finite_subset)
  thus ?thesis using F'  F
  proof
    note p
    also from refl have "(fF''. q' f * f) = (fF''. ((?A f) * f) + ((?B f) * f))"
    proof (rule sum.cong)
      fix f
      assume "f  F''"
      from sum_hom_components have "q' f = ((hom_components (q' f)))" by (rule sym)
      also have " = ((?A f  ?B f))" by (rule arg_cong[where f="sum (λx. x)"]) blast
      also have " = (?A f) + (?B f)"
      proof (rule sum.union_disjoint)
        have "?A f  hom_components (q' f)" by blast
        thus "finite (?A f)" using finite_hom_components by (rule finite_subset)
      next
        have "?B f  hom_components (q' f)" by blast
        thus "finite (?B f)" using finite_hom_components by (rule finite_subset)
      qed blast
      finally show "q' f * f = ((?A f) * f) + ((?B f) * f)"
        by (metis (no_types, lifting) distrib_right)
    qed
    also have " = (fF''. (?A f) * f) + (fF''. (?B f) * f)" by (rule sum.distrib)
    also from finite F'' F'  F'' have "(fF''. (?A f) * f) = (fF'. q f * f)"
    proof (intro sum.mono_neutral_cong_right ballI)
      fix f
      assume "f  F'' - F'"
      thus "(?A f) * f = 0" by (simp add: F'_def)
    next
      fix f
      assume "f  F'"
      thus "(?A f) * f = q f * f" by (simp add: q_def)
    qed
    finally have p[symmetric]: "p = (fF'. q f * f) + (fF''. (?B f) * f)" .
    moreover have "keys (fF''. (?B f) * f) = {}"
    proof (rule, rule)
      fix t
      assume t_in: "t  keys (fF''. (?B f) * f)"
      also have "  (fF''. keys ((?B f) * f))" by (fact keys_sum_subset)
      finally obtain f where "f  F''" and "t  keys ((?B f) * f)" ..
      from this(2) obtain s1 s2 where "s1  keys ((?B f))" and "s2  keys f" and t: "t = s1 + s2"
        by (rule in_keys_timesE)
      from f  F'' F''  F have "f  F" ..
      hence "homogeneous f" by (rule assms(1))
      note s1  keys ((?B f))
      also have "keys ((?B f))  (h?B f. keys h)" by (fact keys_sum_subset)
      finally obtain h where "h  ?B f" and "s1  keys h" ..
      from this(1) have "h  hom_components (q' f)" and neq: "poly_deg h + poly_deg f  poly_deg p"
        by simp_all
      from this(1) have "homogeneous h" by (rule hom_components_homogeneous)
      hence "deg_pm s1 = poly_deg h" using s1  keys h by (rule homogeneousD_poly_deg)
      moreover from homogeneous f s2  keys f have "deg_pm s2 = poly_deg f"
        by (rule homogeneousD_poly_deg)
      ultimately have "deg_pm t  poly_deg p" using neq by (simp add: t deg_pm_plus)
      have "t  keys (fF'. q f * f)"
      proof
        assume "t  keys (fF'. q f * f)"
        also have "  (fF'. keys (q f * f))" by (fact keys_sum_subset)
        finally obtain f where "f  F'" and "t  keys (q f * f)" ..
        hence "deg_pm t = poly_deg p" by (rule 2)
        with deg_pm t  poly_deg p show False ..
      qed
      with t_in have "t  keys ((fF'. q f * f) + (fF''. (?B f) * f))"
        by (rule in_keys_plusI2)
      hence "t  keys p" by (simp only: p)
      with assms(3) have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
      with deg_pm t  poly_deg p show "t  {}" ..
    qed (fact empty_subsetI)
    ultimately show "p = (fF'. q f * f)" by simp
  next
    fix f
    show "homogeneous (q f)"
    proof (cases "f  F'")
      case True
      show ?thesis
      proof (rule homogeneousI)
        fix s t
        assume "s  keys (q f)"
        with True have *: "deg_pm s + poly_deg f = poly_deg p" by (rule 1)
        assume "t  keys (q f)"
        with True have "deg_pm t + poly_deg f = poly_deg p" by (rule 1)
        with * show "deg_pm s = deg_pm t" by simp
      qed
    next
      case False
      thus ?thesis by (simp add: q_def)
    qed

    assume "f  F'"
    show "poly_deg (q f * f) = poly_deg p"
    proof (intro antisym)
      show "poly_deg (q f * f)  poly_deg p"
      proof (rule poly_deg_leI)
        fix t
        assume "t  keys (q f * f)"
        with f  F' have "deg_pm t = poly_deg p" by (rule 2)
        thus "deg_pm t  poly_deg p" by simp
      qed
    next
      from f  F' have "q f * f  0" by (simp add: q_def F'_def)
      hence "keys (q f * f)  {}" by simp
      then obtain t where "t  keys (q f * f)" by blast
      with f  F' have "deg_pm t = poly_deg p" by (rule 2)
      moreover from t  keys (q f * f) have "deg_pm t  poly_deg (q f * f)" by (rule poly_deg_max_keys)
      ultimately show "poly_deg p  poly_deg (q f * f)" by simp
    qed
  qed (simp add: q_def)
qed

corollary homogeneous_idealE:
  assumes "f. f  F  homogeneous f" and "p  ideal F"
  obtains F' q where "finite F'" and "F'  F" and "p = (fF'. q f * f)"
    and "f. poly_deg (q f * f)  poly_deg p" and "f. f  F'  q f = 0"
proof (cases "p = 0")
  case True
  show ?thesis
  proof
    show "p = (f{}. (λ_. 0) f * f)" by (simp add: True)
  qed simp_all
next
  case False
  define P where "P = (λh qf. finite (fst qf)  fst qf  F  h = (ffst qf. snd qf f * f) 
                  (ffst qf. poly_deg (snd qf f * f) = poly_deg h)  (f. f  fst qf  snd qf f = 0))"
  define q0 where "q0 = (λh. SOME qf. P h qf)"
  have 1: "P h (q0 h)" if "h  hom_components p" for h
  proof -
    note assms(1)
    moreover from assms that have "h  ideal F" by (rule homogeneous_ideal')
    moreover from that have "homogeneous h" by (rule hom_components_homogeneous)
    ultimately obtain F' q where "finite F'" and "F'  F" and "h = (fF'. q f * f)"
      and "f. f  F'  poly_deg (q f * f) = poly_deg h" and "f. f  F'  q f = 0"
      by (rule homogeneous_idealE_homogeneous) blast+
    hence "P h (F', q)" by (simp add: P_def)
    thus ?thesis unfolding q0_def by (rule someI)
  qed
  define F' where "F' = (hhom_components p. fst (q0 h))"
  define q where "q = (λf. hhom_components p. snd (q0 h) f)"
  show ?thesis
  proof
    have "finite F'  F'  F" unfolding F'_def UN_subset_iff finite_UN[OF finite_hom_components]
    proof (intro conjI ballI)
      fix h
      assume "h  hom_components p"
      hence "P h (q0 h)" by (rule 1)
      thus "finite (fst (q0 h))" and "fst (q0 h)  F" by (simp_all only: P_def)
    qed
    thus "finite F'" and "F'  F" by simp_all

    from sum_hom_components have "p = ((hom_components p))" by (rule sym)
    also from refl have " = (hhom_components p. fF'. snd (q0 h) f * f)"
    proof (rule sum.cong)
      fix h
      assume "h  hom_components p"
      hence "P h (q0 h)" by (rule 1)
      hence "h = (ffst (q0 h). snd (q0 h) f * f)" and 2: "f. f  fst (q0 h)  snd (q0 h) f = 0"
        by (simp_all add: P_def)
      note this(1)
      also from finite F' have "(ffst (q0 h). (snd (q0 h)) f * f) = (fF'. snd (q0 h) f * f)"
      proof (intro sum.mono_neutral_left ballI)
        show "fst (q0 h)  F'" unfolding F'_def using h  hom_components p by blast
      next
        fix f
        assume "f  F' - fst (q0 h)"
        hence "f  fst (q0 h)" by simp
        hence "snd (q0 h) f = 0" by (rule 2)
        thus "snd (q0 h) f * f = 0" by simp
      qed
      finally show "h = (fF'. snd (q0 h) f * f)" .
    qed
    also have " = (fF'. hhom_components p. snd (q0 h) f * f)" by (rule sum.swap)
    also have " = (fF'. q f * f)" by (simp only: q_def sum_distrib_right)
    finally show "p = (fF'. q f * f)" .

    fix f
    have "poly_deg (q f * f) = poly_deg (hhom_components p. snd (q0 h) f * f)"
      by (simp only: q_def sum_distrib_right)
    also have "  Max (poly_deg ` (λh. snd (q0 h) f * f) ` hom_components p)"
      by (rule poly_deg_sum_le)
    also have " = Max ((λh. poly_deg (snd (q0 h) f * f)) ` hom_components p)"
      (is "_ = Max (?f ` _)") by (simp only: image_image)
    also have "  poly_deg p"
    proof (rule Max.boundedI)
      from finite_hom_components show "finite (?f ` hom_components p)" by (rule finite_imageI)
    next
      from False show "?f ` hom_components p  {}" by simp
    next
      fix d
      assume "d  ?f ` hom_components p"
      then obtain h where "h  hom_components p" and d: "d = ?f h" ..
      from this(1) have "P h (q0 h)" by (rule 1)
      hence 2: "f. f  fst (q0 h)  poly_deg (snd (q0 h) f * f) = poly_deg h"
        and 3: "f. f  fst (q0 h)  snd (q0 h) f = 0" by (simp_all add: P_def)
      show "d  poly_deg p"
      proof (cases "f  fst (q0 h)")
        case True
        hence "poly_deg (snd (q0 h) f * f) = poly_deg h" by (rule 2)
        hence "d = poly_deg h" by (simp only: d)
        also from h  hom_components p have "  poly_deg p" by (rule poly_deg_hom_components_le)
        finally show ?thesis .
      next
        case False
        hence "snd (q0 h) f = 0" by (rule 3)
        thus ?thesis by (simp add: d)
      qed
    qed
    finally show "poly_deg (q f * f)  poly_deg p" .

    assume "f  F'"
    show "q f = 0" unfolding q_def
    proof (intro sum.neutral ballI)
      fix h
      assume "h  hom_components p"
      hence "P h (q0 h)" by (rule 1)
      hence 2: "f. f  fst (q0 h)  snd (q0 h) f = 0" by (simp add: P_def)
      show "snd (q0 h) f = 0"
      proof (intro 2 notI)
        assume "f  fst (q0 h)"
        hence "f  F'" unfolding F'_def using h  hom_components p by blast
        with f  F' show False ..
      qed
    qed
  qed
qed

corollary homogeneous_idealE_finite:
  assumes "finite F" and "f. f  F  homogeneous f" and "p  ideal F"
  obtains q where "p = (fF. q f * f)" and "f. poly_deg (q f * f)  poly_deg p"
    and "f. f  F  q f = 0"
proof -
  from assms(2, 3) obtain F' q where "F'  F" and p: "p = (fF'. q f * f)"
    and "f. poly_deg (q f * f)  poly_deg p" and 1: "f. f  F'  q f = 0"
    by (rule homogeneous_idealE) blast+
  show ?thesis
  proof
    from assms(1) F'  F have "(fF'. q f * f) = (fF. q f * f)"
    proof (intro sum.mono_neutral_left ballI)
      fix f
      assume "f  F - F'"
      hence "f  F'" by simp
      hence "q f = 0" by (rule 1)
      thus "q f * f = 0" by simp
    qed
    thus "p = (fF. q f * f)" by (simp only: p)
  next
    fix f
    show "poly_deg (q f * f)  poly_deg p" by fact

    assume "f  F"
    with F'  F have "f  F'" by blast
    thus "q f = 0" by (rule 1)
  qed
qed

subsubsection ‹Homogenization and Dehomogenization›

definition homogenize :: "'x  (('x 0 nat) 0 'a)  (('x 0 nat) 0 'a::semiring_1)"
  where "homogenize x p = (tkeys p. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"

definition dehomo_subst :: "'x  'x  (('x 0 nat) 0 'a::zero_neq_one)"
  where "dehomo_subst x = (λy. if y = x then 1 else monomial 1 (Poly_Mapping.single y 1))"

definition dehomogenize :: "'x  (('x 0 nat) 0 'a)  (('x 0 nat) 0 'a::comm_semiring_1)"
  where "dehomogenize x = poly_subst (dehomo_subst x)"

lemma homogenize_zero [simp]: "homogenize x 0 = 0"
  by (simp add: homogenize_def)

lemma homogenize_uminus [simp]: "homogenize x (- p) = - homogenize x (p::_ 0 'a::ring_1)"
  by (simp add: homogenize_def keys_uminus sum.reindex inj_on_def single_uminus sum_negf)

lemma homogenize_monom_mult [simp]:
  "homogenize x (punit.monom_mult c t p) = punit.monom_mult c t (homogenize x p)"
  for c::"'a::{semiring_1,semiring_no_zero_divisors_cancel}"
proof (cases "p = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof (cases "c = 0")
    case True
    thus ?thesis by simp
  next
    case False
    show ?thesis
      by (simp add: homogenize_def punit.keys_monom_mult p  0 False sum.reindex
          punit.lookup_monom_mult punit.monom_mult_sum_right poly_deg_monom_mult
          punit.monom_mult_monomial ac_simps deg_pm_plus)
  qed
qed

lemma homogenize_alt:
  "homogenize x p = (qhom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
proof -
  have "homogenize x p = (tKeys (hom_components p). monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
    by (simp only: homogenize_def Keys_hom_components)
  also have " = (t( (keys ` hom_components p)). monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
    by (simp only: Keys_def)
  also have " = (qhom_components p. (tkeys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)))"
    by (auto intro!: sum.UNION_disjoint finite_hom_components finite_keys dest: hom_components_keys_disjoint)
  also have " = (qhom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
    using refl
  proof (rule sum.cong)
    fix q
    assume q: "q  hom_components p"
    hence "homogeneous q" by (rule hom_components_homogeneous)
    have "(tkeys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)) =
          (tkeys q. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) (monomial (lookup q t) t))"
      using refl
    proof (rule sum.cong)
      fix t
      assume "t  keys q"
      with homogeneous q have "deg_pm t = poly_deg q" by (rule homogeneousD_poly_deg)
      moreover from q t  keys q have "lookup q t = lookup p t" by (rule lookup_hom_components)
      ultimately show "monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t) =
            punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) (monomial (lookup q t) t)"
        by (simp add: punit.monom_mult_monomial)
    qed
    also have " = punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q"
      by (simp only: poly_mapping_sum_monomials flip: punit.monom_mult_sum_right)
    finally show "(tkeys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)) =
                  punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q" .
  qed
  finally show ?thesis .
qed

lemma keys_homogenizeE:
  assumes "t  keys (homogenize x p)"
  obtains t' where "t'  keys p" and "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'"
proof -
  note assms
  also have "keys (homogenize x p) 
            (tkeys p. keys (monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)))"
    unfolding homogenize_def by (rule keys_sum_subset)
  finally obtain t' where "t'  keys p"
    and "t  keys (monomial (lookup p t') (Poly_Mapping.single x (poly_deg p - deg_pm t') + t'))" ..
  from this(2) have "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'"
    by (simp split: if_split_asm)
  with t'  keys p show ?thesis ..
qed

lemma keys_homogenizeE_alt:
  assumes "t  keys (homogenize x p)"
  obtains q t' where "q  hom_components p" and "t'  keys q"
    and "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'"
proof -
  note assms
  also have "keys (homogenize x p) 
            (qhom_components p. keys (punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q))"
    unfolding homogenize_alt by (rule keys_sum_subset)
  finally obtain q where q: "q  hom_components p"
    and "t  keys (punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)" ..
  note this(2)
  also have "  (+) (Poly_Mapping.single x (poly_deg p - poly_deg q)) ` keys q"
    by (rule punit.keys_monom_mult_subset[simplified])
  finally obtain t' where "t'  keys q" and "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'" ..
  with q show ?thesis ..
qed

lemma deg_pm_homogenize:
  assumes "t  keys (homogenize x p)"
  shows "deg_pm t = poly_deg p"
proof -
  from assms obtain q t' where q: "q  hom_components p" and "t'  keys q"
    and t: "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'" by (rule keys_homogenizeE_alt)
  from q have "homogeneous q" by (rule hom_components_homogeneous)
  hence "deg_pm t' = poly_deg q" using t'  keys q by (rule homogeneousD_poly_deg)
  moreover from q have "poly_deg q  poly_deg p" by (rule poly_deg_hom_components_le)
  ultimately show ?thesis by (simp add: t deg_pm_plus deg_pm_single)
qed

corollary homogeneous_homogenize: "homogeneous (homogenize x p)"
proof (rule homogeneousI)
  fix s t
  assume "s  keys (homogenize x p)"
  hence *: "deg_pm s = poly_deg p" by (rule deg_pm_homogenize)
  assume "t  keys (homogenize x p)"
  hence "deg_pm t = poly_deg p" by (rule deg_pm_homogenize)
  with * show "deg_pm s = deg_pm t" by simp
qed

corollary poly_deg_homogenize_le: "poly_deg (homogenize x p)  poly_deg p"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (homogenize x p)"
  hence "deg_pm t = poly_deg p" by (rule deg_pm_homogenize)
  thus "deg_pm t  poly_deg p" by simp
qed

lemma homogenize_id_iff [simp]: "homogenize x p = p  homogeneous p"
proof
  assume "homogenize x p = p"
  moreover have "homogeneous (homogenize x p)" by (fact homogeneous_homogenize)
  ultimately show "homogeneous p" by simp
next
  assume "homogeneous p"
  hence "hom_components p = (if p = 0 then {} else {p})" by (rule hom_components_of_homogeneous)
  thus "homogenize x p = p" by (simp add: homogenize_alt split: if_split_asm)
qed

lemma homogenize_homogenize [simp]: "homogenize x (homogenize x p) = homogenize x p"
  by (simp add: homogeneous_homogenize)

lemma homogenize_monomial: "homogenize x (monomial c t) = monomial c t"
  by (simp only: homogenize_id_iff homogeneous_monomial)

lemma indets_homogenize_subset: "indets (homogenize x p)  insert x (indets p)"
proof
  fix y
  assume "y  indets (homogenize x p)"
  then obtain t where "t  keys (homogenize x p)" and "y  keys t" by (rule in_indetsE)
  from this(1) obtain t' where "t'  keys p"
    and t: "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'" by (rule keys_homogenizeE)
  note y  keys t
  also have "keys t  keys (Poly_Mapping.single x (poly_deg p - deg_pm t'))  keys t'"
    unfolding t by (rule Poly_Mapping.keys_add)
  finally show "y  insert x (indets p)"
  proof
    assume "y  keys (Poly_Mapping.single x (poly_deg p - deg_pm t'))"
    thus ?thesis by (simp split: if_split_asm)
  next
    assume "y  keys t'"
    hence "y  indets p" using t'  keys p by (rule in_indetsI)
    thus ?thesis by simp
  qed
qed

lemma homogenize_in_Polys: "p  P[X]  homogenize x p  P[insert x X]"
  using indets_homogenize_subset[of x p] by (auto simp: Polys_alt)

lemma lookup_homogenize:
  assumes "x  indets p" and "x  keys t"
  shows "lookup (homogenize x p) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t) = lookup p t"
proof -
  let ?p = "homogenize x p"
  let ?t = "Poly_Mapping.single x (poly_deg p - deg_pm t) + t"
  have eq: "(skeys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t) = 0"
  proof (intro sum.neutral ballI)
    fix s
    assume "s  keys p - {t}"
    hence "s  keys p" and "s  t" by simp_all
    from this(1) have "keys s  indets p" by (simp add: in_indetsI subsetI)
    with assms(1) have "x  keys s" by blast
    have "?t  Poly_Mapping.single x (poly_deg p - deg_pm s) + s"
    proof
      assume a: "?t = Poly_Mapping.single x (poly_deg p - deg_pm s) + s"
      hence "lookup ?t x = lookup (Poly_Mapping.single x (poly_deg p - deg_pm s) + s) x"
        by simp
      moreover from assms(2) have "lookup t x = 0" by (simp add: in_keys_iff)
      moreover from x  keys s have "lookup s x = 0" by (simp add: in_keys_iff)
      ultimately have "poly_deg p - deg_pm t = poly_deg p - deg_pm s" by (simp add: lookup_add)
      with a have "s = t" by simp
      with s  t show False ..
    qed
    thus "lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t = 0"
      by (simp add: lookup_single)
  qed
  show ?thesis
  proof (cases "t  keys p")
    case True
    have "lookup ?p ?t = (skeys p. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
      by (simp add: homogenize_def lookup_sum)
    also have " = lookup (monomial (lookup p t) ?t) ?t +
                    (skeys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
      using finite_keys True by (rule sum.remove)
    also have " = lookup p t" by (simp add: eq)
    finally show ?thesis .
  next
    case False
    hence 1: "keys p - {t} = keys p" by simp
    have "lookup ?p ?t = (skeys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
      by (simp add: homogenize_def lookup_sum 1)
    also have " = 0" by (simp only: eq)
    also from False have " = lookup p t" by (simp add: in_keys_iff)
    finally show ?thesis .
  qed
qed

lemma keys_homogenizeI:
  assumes "x  indets p" and "t  keys p"
  shows "Poly_Mapping.single x (poly_deg p - deg_pm t) + t  keys (homogenize x p)" (is "?t  keys ?p")
proof -
  from assms(2) have "keys t  indets p" by (simp add: in_indetsI subsetI)
  with assms(1) have "x  keys t" by blast
  with assms(1) have "lookup ?p ?t = lookup p t" by (rule lookup_homogenize)
  also from assms(2) have "  0" by (simp add: in_keys_iff)
  finally show ?thesis by (simp add: in_keys_iff)
qed

lemma keys_homogenize:
  "x  indets p  keys (homogenize x p) = (λt. Poly_Mapping.single x (poly_deg p - deg_pm t) + t) ` keys p"
  by (auto intro: keys_homogenizeI elim: keys_homogenizeE)

lemma card_keys_homogenize:
  assumes "x  indets p"
  shows "card (keys (homogenize x p)) = card (keys p)"
  unfolding keys_homogenize[OF assms]
proof (intro card_image inj_onI)
  fix s t
  assume "s  keys p" and "t  keys p"
  with assms have "x  keys s" and "x  keys t" by (auto dest: in_indetsI simp only:)
  let ?s = "Poly_Mapping.single x (poly_deg p - deg_pm s)"
  let ?t = "Poly_Mapping.single x (poly_deg p - deg_pm t)"
  assume "?s + s = ?t + t"
  hence "lookup (?s + s) x = lookup (?t + t) x" by simp
  with x  keys s x  keys t have "?s = ?t" by (simp add: lookup_add in_keys_iff)
  with ?s + s = ?t + t show "s = t" by simp
qed

lemma poly_deg_homogenize:
  assumes "x  indets p"
  shows "poly_deg (homogenize x p) = poly_deg p"
proof (cases "p = 0")
  case True
  thus ?thesis by simp
next
  case False
  then obtain t where "t  keys p" and 1: "poly_deg p = deg_pm t" by (rule poly_degE)
  from assms this(1) have "Poly_Mapping.single x (poly_deg p - deg_pm t) + t  keys (homogenize x p)"
    by (rule keys_homogenizeI)
  hence "t  keys (homogenize x p)" by (simp add: 1)
  hence "poly_deg p  poly_deg (homogenize x p)" unfolding 1 by (rule poly_deg_max_keys)
  with poly_deg_homogenize_le show ?thesis by (rule antisym)
qed

lemma maxdeg_homogenize:
  assumes "x   (indets ` F)"
  shows "maxdeg (homogenize x ` F) = maxdeg F"
  unfolding maxdeg_def image_image
proof (rule arg_cong[where f=Max], rule set_eqI)
  fix d
  show "d  (λf. poly_deg (homogenize x f)) ` F  d  poly_deg ` F"
  proof
    assume "d  (λf. poly_deg (homogenize x f)) ` F"
    then obtain f where "f  F" and d: "d = poly_deg (homogenize x f)" ..
    from assms this(1) have "x  indets f" by blast
    hence "d = poly_deg f" by (simp add: d poly_deg_homogenize)
    with f  F show "d  poly_deg ` F" by (rule rev_image_eqI)
  next
    assume "d  poly_deg ` F"
    then obtain f where "f  F" and d: "d = poly_deg f" ..
    from assms this(1) have "x  indets f" by blast
    hence "d = poly_deg (homogenize x f)" by (simp add: d poly_deg_homogenize)
    with f  F show "d  (λf. poly_deg (homogenize x f)) ` F" by (rule rev_image_eqI)
  qed
qed

lemma homogeneous_ideal_homogenize:
  assumes "f. f  F  homogeneous f" and "p  ideal F"
  shows "homogenize x p  ideal F"
proof -
  have "homogenize x p = (qhom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
    by (fact homogenize_alt)
  also have "  ideal F"
  proof (rule ideal.span_sum)
    fix q
    assume "q  hom_components p"
    with assms have "q  ideal F" by (rule homogeneous_ideal')
    thus "punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q  ideal F"
      by (rule punit.pmdl_closed_monom_mult[simplified])
  qed
  finally show ?thesis .
qed

lemma subst_pp_dehomo_subst [simp]:
  "subst_pp (dehomo_subst x) t = monomial (1::'b::comm_semiring_1) (except t {x})"
proof -
  have "subst_pp (dehomo_subst x) t = ((ykeys t. dehomo_subst x y ^ lookup t y)::_ 0 'b)"
    by (fact subst_pp_def)
  also have " = (ykeys t - {y0. dehomo_subst x y0 ^ lookup t y0 = (1::_ 0 'b)}. dehomo_subst x y ^ lookup t y)"
    by (rule sym, rule prod.setdiff_irrelevant, fact finite_keys)
  also have " = (ykeys t - {x}. monomial 1 (Poly_Mapping.single y 1) ^ lookup t y)"
  proof (rule prod.cong)
    have "dehomo_subst x x ^ lookup t x = 1" by (simp add: dehomo_subst_def)
    moreover {
      fix y
      assume "y  x"
      hence "dehomo_subst x y ^ lookup t y = monomial 1 (Poly_Mapping.single y (lookup t y))"
        by (simp add: dehomo_subst_def monomial_single_power)
      moreover assume "dehomo_subst x y ^ lookup t y = 1"
      ultimately have "Poly_Mapping.single y (lookup t y) = 0"
        by (smt single_one monomial_inj zero_neq_one)
      hence "lookup t y = 0" by (rule monomial_0D)
      moreover assume "y  keys t"
      ultimately have False by (simp add: in_keys_iff)
    }
    ultimately show "keys t - {y0. dehomo_subst x y0 ^ lookup t y0 = 1} = keys t - {x}" by auto
  qed (simp add: dehomo_subst_def)
  also have " = (ykeys t - {x}. monomial 1 (Poly_Mapping.single y (lookup t y)))"
    by (simp add: monomial_single_power)
  also have " = monomial 1 (ykeys t - {x}. Poly_Mapping.single y (lookup t y))"
    by (simp flip: punit.monomial_prod_sum)
  also have "(ykeys t - {x}. Poly_Mapping.single y (lookup t y)) = except t {x}"
  proof (rule poly_mapping_eqI, simp add: lookup_sum lookup_except lookup_single, rule)
    fix y
    assume "y  x"
    show "(zkeys t - {x}. lookup t z when z = y) = lookup t y"
    proof (cases "y  keys t")
      case True
      have "finite (keys t - {x})" by simp
      moreover from True y  x have "y  keys t - {x}" by simp
      ultimately have "(zkeys t - {x}. lookup t z when z = y) =
                        (lookup t y when y = y) + (zkeys t - {x} - {y}. lookup t z when z = y)"
        by (rule sum.remove)
      also have "(zkeys t - {x} - {y}. lookup t z when z = y) = 0" by auto
      finally show ?thesis by simp
    next
      case False
      hence "(zkeys t - {x}. lookup t z when z = y) = 0" by (auto simp: when_def)
      also from False have " = lookup t y" by (simp add: in_keys_iff)
      finally show ?thesis .
    qed
  qed
  finally show ?thesis .
qed

lemma
  shows dehomogenize_zero [simp]: "dehomogenize x 0 = 0"
    and dehomogenize_one [simp]: "dehomogenize x 1 = 1"
    and dehomogenize_monomial: "dehomogenize x (monomial c t) = monomial c (except t {x})"
    and dehomogenize_plus: "dehomogenize x (p + q) = dehomogenize x p + dehomogenize x q"
    and dehomogenize_uminus: "dehomogenize x (- r) = - dehomogenize x (r::_ 0 _::comm_ring_1)"
    and dehomogenize_minus: "dehomogenize x (r - r') = dehomogenize x r - dehomogenize x r'"
    and dehomogenize_times: "dehomogenize x (p * q) = dehomogenize x p * dehomogenize x q"
    and dehomogenize_power: "dehomogenize x (p ^ n) = dehomogenize x p ^ n"
    and dehomogenize_sum: "dehomogenize x (sum f A) = (aA. dehomogenize x (f a))"
    and dehomogenize_prod: "dehomogenize x (prod f A) = (aA. dehomogenize x (f a))"
  by (simp_all add: dehomogenize_def poly_subst_monomial poly_subst_plus poly_subst_uminus
      poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod punit.monom_mult_monomial)

corollary dehomogenize_monom_mult:
  "dehomogenize x (punit.monom_mult c t p) = punit.monom_mult c (except t {x}) (dehomogenize x p)"
  by (simp only: times_monomial_left[symmetric] dehomogenize_times dehomogenize_monomial)

lemma poly_deg_dehomogenize_le: "poly_deg (dehomogenize x p)  poly_deg p"
  unfolding dehomogenize_def dehomo_subst_def
  by (rule poly_deg_poly_subst_le) (simp add: poly_deg_monomial deg_pm_single)

lemma indets_dehomogenize: "indets (dehomogenize x p)  indets p - {x}"
  for p::"('x 0 nat) 0 'a::comm_semiring_1"
proof
  fix y::'x
  assume "y  indets (dehomogenize x p)"
  then obtain y' where "y'  indets p" and "y  indets ((dehomo_subst x y')::_ 0 'a)"
    unfolding dehomogenize_def by (rule in_indets_poly_substE)
  from this(2) have "y = y'" and "y'  x"
    by (simp_all add: dehomo_subst_def indets_monomial split: if_split_asm)
  with y'  indets p show "y  indets p - {x}" by simp
qed

lemma dehomogenize_id_iff [simp]: "dehomogenize x p = p  x  indets p"
proof
  assume eq: "dehomogenize x p = p"
  from indets_dehomogenize[of x p] show "x  indets p" by (auto simp: eq)
next
  assume a: "x  indets p"
  show "dehomogenize x p = p" unfolding dehomogenize_def
  proof (rule poly_subst_id)
    fix y
    assume "y  indets p"
    with a have "y  x" by blast
    thus "dehomo_subst x y = monomial 1 (Poly_Mapping.single y 1)" by (simp add: dehomo_subst_def)
  qed
qed

lemma dehomogenize_dehomogenize [simp]: "dehomogenize x (dehomogenize x p) = dehomogenize x p"
proof -
  from indets_dehomogenize[of x p] have "x  indets (dehomogenize x p)" by blast
  thus ?thesis by simp
qed

lemma dehomogenize_homogenize [simp]: "dehomogenize x (homogenize x p) = dehomogenize x p"
proof -
  have "dehomogenize x (homogenize x p) = sum (dehomogenize x) (hom_components p)"
    by (simp add: homogenize_alt dehomogenize_sum dehomogenize_monom_mult except_single)
  also have " = dehomogenize x p" by (simp only: sum_hom_components flip: dehomogenize_sum)
  finally show ?thesis .
qed

corollary dehomogenize_homogenize_id: "x  indets p  dehomogenize x (homogenize x p) = p"
  by simp

lemma range_dehomogenize: "range (dehomogenize x) = (P[- {x}] :: (_ 0 'a::comm_semiring_1) set)"
proof (intro subset_antisym subsetI PolysI_alt range_eqI)
  fix p::"_ 0 'a" and y
  assume "p  range (dehomogenize x)"
  then obtain q where p: "p = dehomogenize x q" ..
  assume "y  indets p"
  hence "y  indets (dehomogenize x q)" by (simp only: p)
  with indets_dehomogenize have "y  indets q - {x}" ..
  thus "y  - {x}" by simp
next
  fix p::"_ 0 'a"
  assume "p  P[- {x}]"
  hence "x  indets p" by (auto dest: PolysD)
  thus "p = dehomogenize x (homogenize x p)" by (rule dehomogenize_homogenize_id[symmetric])
qed

lemma dehomogenize_alt: "dehomogenize x p = (tkeys p. monomial (lookup p t) (except t {x}))"
proof -
  have "dehomogenize x p = dehomogenize x (tkeys p. monomial (lookup p t) t)"
    by (simp only: poly_mapping_sum_monomials)
  also have " = (tkeys p. monomial (lookup p t) (except t {x}))"
    by (simp only: dehomogenize_sum dehomogenize_monomial)
  finally show ?thesis .
qed

lemma keys_dehomogenizeE:
  assumes "t  keys (dehomogenize x p)"
  obtains s where "s  keys p" and "t = except s {x}"
proof -
  note assms
  also have "keys (dehomogenize x p)  (skeys p. keys (monomial (lookup p s) (except s {x})))"
    unfolding dehomogenize_alt by (rule keys_sum_subset)
  finally obtain s where "s  keys p" and "t  keys (monomial (lookup p s) (except s {x}))" ..
  from this(2) have "t = except s {x}" by (simp split: if_split_asm)
  with s  keys p show ?thesis ..
qed

lemma except_inj_on_keys_homogeneous:
  assumes "homogeneous p"
  shows "inj_on (λt. except t {x}) (keys p)"
proof
  fix s t
  assume "s  keys p" and "t  keys p"
  from assms this(1) have "deg_pm s = poly_deg p" by (rule homogeneousD_poly_deg)
  moreover from assms t  keys p have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
  ultimately have "deg_pm (Poly_Mapping.single x (lookup s x) + except s {x}) =
                   deg_pm (Poly_Mapping.single x (lookup t x) + except t {x})"
    by (simp only: flip: plus_except)
  moreover assume 1: "except s {x} = except t {x}"
  ultimately have 2: "lookup s x = lookup t x"
    by (simp only: deg_pm_plus deg_pm_single)
  show "s = t"
  proof (rule poly_mapping_eqI)
    fix y
    show "lookup s y = lookup t y"
    proof (cases "y = x")
      case True
      with 2 show ?thesis by simp
    next
      case False
      hence "lookup s y = lookup (except s {x}) y" and "lookup t y = lookup (except t {x}) y"
        by (simp_all add: lookup_except)
      with 1 show ?thesis by simp
    qed
  qed
qed

lemma lookup_dehomogenize:
  assumes "homogeneous p" and "t  keys p"
  shows "lookup (dehomogenize x p) (except t {x}) = lookup p t"
proof -
  let ?t = "except t {x}"
  have eq: "(skeys p - {t}. lookup (monomial (lookup p s) (except s {x})) ?t) = 0"
  proof (intro sum.neutral ballI)
    fix s
    assume "s  keys p - {t}"
    hence "s  keys p" and "s  t" by simp_all
    have "?t  except s {x}"
    proof
      from assms(1) have "inj_on (λt. except t {x}) (keys p)" by (rule except_inj_on_keys_homogeneous)
      moreover assume "?t = except s {x}"
      ultimately have "t = s" using assms(2) s  keys p by (rule inj_onD)
      with s  t show False by simp
    qed
    thus "lookup (monomial (lookup p s) (except s {x})) ?t = 0" by (simp add: lookup_single)
  qed
  have "lookup (dehomogenize x p) ?t = (skeys p. lookup (monomial (lookup p s) (except s {x})) ?t)"
    by (simp only: dehomogenize_alt lookup_sum)
  also have " = lookup (monomial (lookup p t) ?t) ?t +
                  (skeys p - {t}. lookup (monomial (lookup p s) (except s {x})) ?t)"
    using finite_keys assms(2) by (rule sum.remove)
  also have " = lookup p t" by (simp add: eq)
  finally show ?thesis .
qed

lemma keys_dehomogenizeI:
  assumes "homogeneous p" and "t  keys p"
  shows "except t {x}  keys (dehomogenize x p)"
proof -
  from assms have "lookup (dehomogenize x p) (except t {x}) = lookup p t" by (rule lookup_dehomogenize)
  also from assms(2) have "  0" by (simp add: in_keys_iff)
  finally show ?thesis by (simp add: in_keys_iff)
qed

lemma homogeneous_homogenize_dehomogenize:
  assumes "homogeneous p"
  obtains d where "d = poly_deg p - poly_deg (homogenize x (dehomogenize x p))"
    and "punit.monom_mult 1 (Poly_Mapping.single x d) (homogenize x (dehomogenize x p)) = p"
proof (cases "p = 0")
  case True
  hence "0 = poly_deg p - poly_deg (homogenize x (dehomogenize x p))"
    and "punit.monom_mult 1 (Poly_Mapping.single x 0) (homogenize x (dehomogenize x p)) = p"
    by simp_all
  thus ?thesis ..
next
  case False
  let ?q = "dehomogenize x p"
  let ?p = "homogenize x ?q"
  define d where "d = poly_deg p - poly_deg ?p"
  show ?thesis
  proof
    have "punit.monom_mult 1 (Poly_Mapping.single x d) ?p =
          (tkeys ?q. monomial (lookup ?q t) (Poly_Mapping.single x (d + (poly_deg ?q - deg_pm t)) + t))"
      by (simp add: homogenize_def punit.monom_mult_sum_right punit.monom_mult_monomial flip: add.assoc single_add)
    also have " = (tkeys ?q. monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
      using refl
    proof (rule sum.cong)
      fix t
      assume "t  keys ?q"
      have "poly_deg ?p = poly_deg ?q"
      proof (rule poly_deg_homogenize)
        from indets_dehomogenize show "x  indets ?q" by fastforce
      qed
      hence d: "d = poly_deg p - poly_deg ?q" by (simp only: d_def)
      thm poly_deg_dehomogenize_le
      from t  keys ?q have "d + (poly_deg ?q - deg_pm t) = (d + poly_deg ?q) - deg_pm t"
        by (intro add_diff_assoc poly_deg_max_keys)
      also have "d + poly_deg ?q = poly_deg p" by (simp add: d poly_deg_dehomogenize_le)
      finally show "monomial (lookup ?q t) (Poly_Mapping.single x (d + (poly_deg ?q - deg_pm t)) + t) =
                    monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)"
        by (simp only:)
    qed
    also have " = (t(λs. except s {x}) ` keys p.
                    monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
    proof (rule sum.mono_neutral_left)
      show "keys (dehomogenize x p)  (λs. except s {x}) ` keys p"
      proof
        fix t
        assume "t  keys (dehomogenize x p)"
        then obtain s where "s  keys p" and "t = except s {x}" by (rule keys_dehomogenizeE)
        thus "t  (λs. except s {x}) ` keys p" by (rule rev_image_eqI)
      qed
    qed (simp_all add: in_keys_iff)
    also from assms have " = (tkeys p. monomial (lookup ?q (except t {x}))
                (Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x}))"
      by (intro sum.reindex[unfolded comp_def] except_inj_on_keys_homogeneous)
    also from refl have " = (tkeys p. monomial (lookup p t) t)"
    proof (rule sum.cong)
      fix t
      assume "t  keys p"
      with assms have "lookup ?q (except t {x}) = lookup p t" by (rule lookup_dehomogenize)
      moreover have "Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x} = t"
        (is "?l = _")
      proof (rule poly_mapping_eqI)
        fix y
        show "lookup ?l y = lookup t y"
        proof (cases "y = x")
          case True
          from assms t  keys p have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
          also have "deg_pm t = deg_pm (Poly_Mapping.single x (lookup t x) + except t {x})"
            by (simp flip: plus_except)
          also have " = lookup t x + deg_pm (except t {x})" by (simp only: deg_pm_plus deg_pm_single)
          finally have "poly_deg p - deg_pm (except t {x}) = lookup t x" by simp
          thus ?thesis by (simp add: True lookup_add lookup_except lookup_single)
        next
          case False
          thus ?thesis by (simp add: lookup_add lookup_except lookup_single)
        qed
      qed
      ultimately show "monomial (lookup ?q (except t {x}))
              (Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x}) =
            monomial (lookup p t) t" by (simp only:)
    qed
    also have " = p" by (fact poly_mapping_sum_monomials)
    finally show "punit.monom_mult 1 (Poly_Mapping.single x d) ?p = p" .
  qed (simp only: d_def)
qed

lemma dehomogenize_zeroD:
  assumes "dehomogenize x p = 0" and "homogeneous p"
  shows "p = 0"
proof -
  from assms(2) obtain d
    where "punit.monom_mult 1 (Poly_Mapping.single x d) (homogenize x (dehomogenize x p)) = p"
    by (rule homogeneous_homogenize_dehomogenize)
  thus ?thesis by (simp add: assms(1))
qed

lemma dehomogenize_ideal: "dehomogenize x ` ideal F = ideal (dehomogenize x ` F)  P[- {x}]"
  unfolding range_dehomogenize[symmetric]
  using dehomogenize_plus dehomogenize_times dehomogenize_dehomogenize by (rule image_ideal_eq_Int)

corollary dehomogenize_ideal_subset: "dehomogenize x ` ideal F  ideal (dehomogenize x ` F)"
  by (simp add: dehomogenize_ideal)

lemma ideal_dehomogenize:
  assumes "ideal G = ideal (homogenize x ` F)" and "F  P[UNIV - {x}]"
  shows "ideal (dehomogenize x ` G) = ideal F"
proof -
  have eq: "dehomogenize x (homogenize x f) = f" if "f  F" for f
  proof (rule dehomogenize_homogenize_id)
    from that assms(2) have "f  P[UNIV - {x}]" ..
    thus "x  indets f" by (auto simp: Polys_alt)
  qed
  show ?thesis
  proof (intro Set.equalityI ideal.span_subset_spanI)
    show "dehomogenize x ` G  ideal F"
    proof
      fix q
      assume "q  dehomogenize x ` G"
      then obtain g where "g  G" and q: "q = dehomogenize x g" ..
      from this(1) have "g  ideal G" by (rule ideal.span_base)
      also have " = ideal (homogenize x ` F)" by fact
      finally have "q  dehomogenize x ` ideal (homogenize x ` F)" using q by (rule rev_image_eqI)
      also have "  ideal (dehomogenize x ` homogenize x ` F)" by (rule dehomogenize_ideal_subset)
      also have "dehomogenize x ` homogenize x ` F = F"
        by (auto simp: eq image_image simp del: dehomogenize_homogenize intro!: image_eqI)
      finally show "q  ideal F" .
    qed
  next
    show "F  ideal (dehomogenize x ` G)"
    proof
      fix f
      assume "f  F"
      hence "homogenize x f  homogenize x ` F" by (rule imageI)
      also have "  ideal (homogenize x ` F)" by (rule ideal.span_superset)
      also from assms(1) have " = ideal G" by (rule sym)
      finally have "dehomogenize x (homogenize x f)  dehomogenize x ` ideal G" by (rule imageI)
      with f  F have "f  dehomogenize x ` ideal G" by (simp only: eq)
      also have "  ideal (dehomogenize x ` G)" by (rule dehomogenize_ideal_subset)
      finally show "f  ideal (dehomogenize x ` G)" .
    qed
  qed
qed

subsection ‹Embedding Polynomial Rings in Larger Polynomial Rings (With One Additional Indeterminate)›

text ‹We define a homomorphism for embedding a polynomial ring in a larger polynomial ring, and its
  inverse. This is mainly needed for homogenizing wrt. a fresh indeterminate.›

definition extend_indets_subst :: "'x  ('x option 0 nat) 0 'a::comm_semiring_1"
  where "extend_indets_subst x = monomial 1 (Poly_Mapping.single (Some x) 1)"

definition extend_indets :: "(('x 0 nat) 0 'a)  ('x option 0 nat) 0 'a::comm_semiring_1"
  where "extend_indets = poly_subst extend_indets_subst"

definition restrict_indets_subst :: "'x option  'x 0 nat"
  where "restrict_indets_subst x = (case x of Some y  Poly_Mapping.single y 1 | _  0)"

definition restrict_indets :: "(('x option 0 nat) 0 'a)  ('x 0 nat) 0 'a::comm_semiring_1"
  where "restrict_indets = poly_subst (λx. monomial 1 (restrict_indets_subst x))"

definition restrict_indets_pp :: "('x option 0 nat)  ('x 0 nat)"
  where "restrict_indets_pp t = (xkeys t. lookup t x  restrict_indets_subst x)"

lemma lookup_extend_indets_subst_aux:
  "lookup (ykeys t. Poly_Mapping.single (Some y) (lookup t y)) = (λx. case x of Some y  lookup t y | _  0)"
proof -
  have "(xkeys t. lookup t x when x = y) = lookup t y" for y
  proof (cases "y  keys t")
    case True
    hence "(xkeys t. lookup t x when x = y) = (xinsert y (keys t). lookup t x when x = y)"
      by (simp only: insert_absorb)
    also have " = lookup t y + (xkeys t - {y}. lookup t x when x = y)"
      by (simp add: sum.insert_remove)
    also have "(xkeys t - {y}. lookup t x when x = y) = 0"
      by (auto simp: when_def intro: sum.neutral)
    finally show ?thesis by simp
  next
    case False
    hence "(xkeys t. lookup t x when x = y) = 0" by (auto simp: when_def intro: sum.neutral)
    with False show ?thesis by (simp add: in_keys_iff)
  qed
  thus ?thesis by (auto simp: lookup_sum lookup_single split: option.split)
qed

lemma keys_extend_indets_subst_aux:
  "keys (ykeys t. Poly_Mapping.single (Some y) (lookup t y)) = Some ` keys t"
  by (auto simp: lookup_extend_indets_subst_aux simp flip: lookup_not_eq_zero_eq_in_keys split: option.splits)

lemma subst_pp_extend_indets_subst:
  "subst_pp extend_indets_subst t = monomial 1 (ykeys t. Poly_Mapping.single (Some y) (lookup t y))"
proof -
  have "subst_pp extend_indets_subst t =
      monomial (ykeys t. 1 ^ lookup t y) (ykeys t. lookup t y  Poly_Mapping.single (Some y) 1)"
    by (rule subst_pp_by_monomials) (simp only: extend_indets_subst_def)
  also have " = monomial 1 (ykeys t. Poly_Mapping.single (Some y) (lookup t y))"
    by simp
  finally show ?thesis .
qed

lemma keys_extend_indets:
  "keys (extend_indets p) = (λt. ykeys t. Poly_Mapping.single (Some y) (lookup t y)) ` keys p"
proof -
  have "keys (extend_indets p) = (tkeys p. keys (punit.monom_mult (lookup p t) 0 (subst_pp extend_indets_subst t)))"
    unfolding extend_indets_def poly_subst_def using finite_keys
  proof (rule keys_sum)
    fix s t :: "'a 0 nat"
    assume "s  t"
    then obtain x where "lookup s x  lookup t x" by (meson poly_mapping_eqI)
    have "(ykeys t. monomial (lookup t y) (Some y))  (ykeys s. monomial (lookup s y) (Some y))"
      (is "?l  ?r")
    proof
      assume "?l = ?r"
      hence "lookup ?l (Some x) = lookup ?r (Some x)" by (simp only:)
      hence "lookup s x = lookup t x" by (simp add: lookup_extend_indets_subst_aux)
      with lookup s x  lookup t x show False ..
    qed
    thus "keys (punit.monom_mult (lookup p s) 0 (subst_pp extend_indets_subst s)) 
          keys (punit.monom_mult (lookup p t) 0 (subst_pp extend_indets_subst t)) =
          {}"
      by (simp add: subst_pp_extend_indets_subst punit.monom_mult_monomial)
  qed
  also have " = (λt. ykeys t. monomial (lookup t y) (Some y)) ` keys p"
    by (auto simp: subst_pp_extend_indets_subst punit.monom_mult_monomial split: if_split_asm)
  finally show ?thesis .
qed

lemma indets_extend_indets: "indets (extend_indets p) = Some ` indets (p::_ 0 'a::comm_semiring_1)"
proof (rule set_eqI)
  fix x
  show "x  indets (extend_indets p)  x  Some ` indets p"
  proof
    assume "x  indets (extend_indets p)"
    then obtain y where "y  indets p" and "x  indets (monomial (1::'a) (Poly_Mapping.single (Some y) 1))"
      unfolding extend_indets_def extend_indets_subst_def by (rule in_indets_poly_substE)
    from this(2) indets_monomial_single_subset have "x  {Some y}" ..
    hence "x = Some y" by simp
    with y  indets p show "x  Some ` indets p" by (rule rev_image_eqI)
  next
    assume "x  Some ` indets p"
    then obtain y where "y  indets p" and x: "x = Some y" ..
    from this(1) obtain t where "t  keys p" and "y  keys t" by (rule in_indetsE)
    from this(2) have "Some y  keys (ykeys t. Poly_Mapping.single (Some y) (lookup t y))"
      unfolding keys_extend_indets_subst_aux by (rule imageI)
    moreover have "(ykeys t. Poly_Mapping.single (Some y) (lookup t y))  keys (extend_indets p)"
      unfolding keys_extend_indets using t  keys p by (rule imageI)
    ultimately show "x  indets (extend_indets p)" unfolding x by (rule in_indetsI)
  qed
qed

lemma poly_deg_extend_indets [simp]: "poly_deg (extend_indets p) = poly_deg p"
proof -
  have eq: "deg_pm ((ykeys t. Poly_Mapping.single (Some y) (lookup t y))) = deg_pm t"
    for t::"'a 0 nat"
  proof -
    have "deg_pm ((ykeys t. Poly_Mapping.single (Some y) (lookup t y))) = (ykeys t. lookup t y)"
      by (simp add: deg_pm_sum deg_pm_single)
    also from subset_refl finite_keys have " = deg_pm t" by (rule deg_pm_superset[symmetric])
    finally show ?thesis .
  qed
  show ?thesis
  proof (rule antisym)
    show "poly_deg (extend_indets p)  poly_deg p"
    proof (rule poly_deg_leI)
      fix t
      assume "t  keys (extend_indets p)"
      then obtain s where "s  keys p" and "t = (ykeys s. Poly_Mapping.single (Some y) (lookup s y))"
        unfolding keys_extend_indets ..
      from this(2) have "deg_pm t = deg_pm s" by (simp only: eq)
      also from s  keys p have "  poly_deg p" by (rule poly_deg_max_keys)
      finally show "deg_pm t  poly_deg p" .
    qed
  next
    show "poly_deg p  poly_deg (extend_indets p)"
    proof (rule poly_deg_leI)
      fix t
      assume "t  keys p"
      hence *: "(ykeys t. Poly_Mapping.single (Some y) (lookup t y))  keys (extend_indets p)"
        unfolding keys_extend_indets by (rule imageI)
      have "deg_pm t = deg_pm (ykeys t. Poly_Mapping.single (Some y) (lookup t y))"
        by (simp only: eq)
      also from * have "  poly_deg (extend_indets p)" by (rule poly_deg_max_keys)
      finally show "deg_pm t  poly_deg (extend_indets p)" .
    qed
  qed
qed

lemma
  shows extend_indets_zero [simp]: "extend_indets 0 = 0"
    and extend_indets_one [simp]: "extend_indets 1 = 1"
    and extend_indets_monomial: "extend_indets (monomial c t) = punit.monom_mult c 0 (subst_pp extend_indets_subst t)"
    and extend_indets_plus: "extend_indets (p + q) = extend_indets p + extend_indets q"
    and extend_indets_uminus: "extend_indets (- r) = - extend_indets (r::_ 0 _::comm_ring_1)"
    and extend_indets_minus: "extend_indets (r - r') = extend_indets r - extend_indets r'"
    and extend_indets_times: "extend_indets (p * q) = extend_indets p * extend_indets q"
    and extend_indets_power: "extend_indets (p ^ n) = extend_indets p ^ n"
    and extend_indets_sum: "extend_indets (sum f A) = (aA. extend_indets (f a))"
    and extend_indets_prod: "extend_indets (prod f A) = (aA. extend_indets (f a))"
  by (simp_all add: extend_indets_def poly_subst_monomial poly_subst_plus poly_subst_uminus
      poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod)

lemma extend_indets_zero_iff [simp]: "extend_indets p = 0  p = 0"
  by (metis (no_types, lifting) imageE imageI keys_extend_indets lookup_zero
      not_in_keys_iff_lookup_eq_zero poly_deg_extend_indets poly_deg_zero poly_deg_zero_imp_monomial)

lemma extend_indets_inject:
  assumes "extend_indets p = extend_indets (q::_ 0 _::comm_ring_1)"
  shows "p = q"
proof -
  from assms have "extend_indets (p - q) = 0" by (simp add: extend_indets_minus)
  thus ?thesis by simp
qed

corollary inj_extend_indets: "inj (extend_indets::_  _ 0 _::comm_ring_1)"
  using extend_indets_inject by (intro injI)

lemma poly_subst_extend_indets: "poly_subst f (extend_indets p) = poly_subst (f  Some) p"
  by (simp add: extend_indets_def poly_subst_poly_subst extend_indets_subst_def poly_subst_monomial
          subst_pp_single o_def)

lemma poly_eval_extend_indets: "poly_eval a (extend_indets p) = poly_eval (a  Some) p"
proof -
  have eq: "poly_eval a (extend_indets (monomial c t)) = poly_eval (λx. a (Some x)) (monomial c t)"
    for c t
    by (simp add: extend_indets_monomial poly_eval_times poly_eval_monomial poly_eval_prod poly_eval_power
                subst_pp_def extend_indets_subst_def flip: times_monomial_left)
  show ?thesis
    by (induct p rule: poly_mapping_plus_induct) (simp_all add: extend_indets_plus poly_eval_plus eq)
qed

lemma lookup_restrict_indets_pp: "lookup (restrict_indets_pp t) = (λx. lookup t (Some x))"
proof -
  let ?f = "λz x. lookup t x * lookup (case x of None  0 | Some y  Poly_Mapping.single y 1) z"
  have "sum (?f z) (keys t) = lookup t (Some z)" for z
  proof (cases "Some z  keys t")
    case True
    hence "sum (?f z) (keys t) = sum (?f z) (insert (Some z) (keys t))"
      by (simp only: insert_absorb)
    also have " = lookup t (Some z) + sum (?f z) (keys t - {Some z})"
      by (simp add: sum.insert_remove)
    also have "sum (?f z) (keys t - {Some z}) = 0"
      by (auto simp: when_def lookup_single intro: sum.neutral split: option.splits)
    finally show ?thesis by simp
  next
    case False
    hence "sum (?f z) (keys t) = 0"
      by (auto simp: when_def lookup_single intro: sum.neutral split: option.splits)
    with False show ?thesis by (simp add: in_keys_iff)
  qed
  thus ?thesis by (auto simp: restrict_indets_pp_def restrict_indets_subst_def lookup_sum)
qed

lemma keys_restrict_indets_pp: "keys (restrict_indets_pp t) = the ` (keys t - {None})"
proof (rule set_eqI)
  fix x
  show "x  keys (restrict_indets_pp t)  x  the ` (keys t - {None})"
  proof
    assume "x  keys (restrict_indets_pp t)"
    hence "Some x  keys t" by (simp add: lookup_restrict_indets_pp flip: lookup_not_eq_zero_eq_in_keys)
    hence "Some x  keys t - {None}" by blast
    moreover have "x = the (Some x)" by simp
    ultimately show "x  the ` (keys t - {None})" by (rule rev_image_eqI)
  next
    assume "x  the ` (keys t - {None})"
    then obtain y where "y  keys t - {None}" and "x = the y" ..
    hence "Some x  keys t" by auto
    thus "x  keys (restrict_indets_pp t)"
      by (simp add: lookup_restrict_indets_pp flip: lookup_not_eq_zero_eq_in_keys)
  qed
qed

lemma subst_pp_restrict_indets_subst:
  "subst_pp (λx. monomial 1 (restrict_indets_subst x)) t = monomial 1 (restrict_indets_pp t)"
  by (simp add: subst_pp_def monomial_power_map_scale restrict_indets_pp_def flip: punit.monomial_prod_sum)

lemma restrict_indets_pp_zero [simp]: "restrict_indets_pp 0 = 0"
  by (simp add: restrict_indets_pp_def)

lemma restrict_indets_pp_plus: "restrict_indets_pp (s + t) = restrict_indets_pp s + restrict_indets_pp t"
  by (rule poly_mapping_eqI) (simp add: lookup_add lookup_restrict_indets_pp)

lemma restrict_indets_pp_except_None [simp]:
  "restrict_indets_pp (except t {None}) = restrict_indets_pp t"
  by (rule poly_mapping_eqI) (simp add: lookup_add lookup_restrict_indets_pp lookup_except)

lemma deg_pm_restrict_indets_pp: "deg_pm (restrict_indets_pp t) + lookup t None = deg_pm t"
proof -
  have "deg_pm t = sum (lookup t) (insert None (keys t))" by (rule deg_pm_superset) auto
  also from finite_keys have " = lookup t None + sum (lookup t) (keys t - {None})"
    by (rule sum.insert_remove)
  also have "sum (lookup t) (keys t - {None}) = (xkeys t. lookup t x * deg_pm (restrict_indets_subst x))"
    by (intro sum.mono_neutral_cong_left) (auto simp: restrict_indets_subst_def deg_pm_single)
  also have " = deg_pm (restrict_indets_pp t)"
    by (simp only: restrict_indets_pp_def deg_pm_sum deg_pm_map_scale)
  finally show ?thesis by simp
qed

lemma keys_restrict_indets_subset: "keys (restrict_indets p)  restrict_indets_pp ` keys p"
proof
  fix t
  assume "t  keys (restrict_indets p)"
  also have " = keys (tkeys p. monomial (lookup p t) (restrict_indets_pp t))"
    by (simp add: restrict_indets_def poly_subst_def subst_pp_restrict_indets_subst punit.monom_mult_monomial)
  also have "  (tkeys p. keys (monomial (lookup p t) (restrict_indets_pp t)))"
    by (rule keys_sum_subset)
  also have " = restrict_indets_pp ` keys p" by (auto split: if_split_asm)
  finally show "t  restrict_indets_pp ` keys p" .
qed

lemma keys_restrict_indets:
  assumes "None  indets p"
  shows "keys (restrict_indets p) = restrict_indets_pp ` keys p"
proof -
  have "keys (restrict_indets p) = keys (tkeys p. monomial (lookup p t) (restrict_indets_pp t))"
    by (simp add: restrict_indets_def poly_subst_def subst_pp_restrict_indets_subst punit.monom_mult_monomial)
  also from finite_keys have " = (tkeys p. keys (monomial (lookup p t) (restrict_indets_pp t)))"
  proof (rule keys_sum)
    fix s t
    assume "s  keys p"
    hence "keys s  indets p" by (rule keys_subset_indets)
    with assms have "None  keys s" by blast
    assume "t  keys p"
    hence "keys t  indets p" by (rule keys_subset_indets)
    with assms have "None  keys t" by blast
    assume "s  t"
    then obtain x where neq: "lookup s x  lookup t x" by (meson poly_mapping_eqI)
    have "x  None"
    proof
      assume "x = None"
      with None  keys s and None  keys t have "x  keys s" and "x  keys t" by blast+
      with neq show False by (simp add: in_keys_iff)
    qed
    then obtain y where x: "x = Some y" by blast
    have "restrict_indets_pp t  restrict_indets_pp s"
    proof
      assume "restrict_indets_pp t = restrict_indets_pp s"
      hence "lookup (restrict_indets_pp t) y = lookup (restrict_indets_pp s) y" by (simp only:)
      hence "lookup s x = lookup t x" by (simp add: x lookup_restrict_indets_pp)
      with neq show False ..
    qed
    thus "keys (monomial (lookup p s) (restrict_indets_pp s)) 
          keys (monomial (lookup p t) (restrict_indets_pp t)) = {}"
      by (simp add: subst_pp_extend_indets_subst)
  qed
  also have " = restrict_indets_pp ` keys p" by (auto split: if_split_asm)
  finally show ?thesis .
qed

lemma indets_restrict_indets_subset: "indets (restrict_indets p)  the ` (indets p - {None})"
proof
  fix x
  assume "x  indets (restrict_indets p)"
  then obtain t where "t  keys (restrict_indets p)" and "x  keys t" by (rule in_indetsE)
  from this(1) keys_restrict_indets_subset have "t  restrict_indets_pp ` keys p" ..
  then obtain s where "s  keys p" and "t = restrict_indets_pp s" ..
  from x  keys t this(2) have "x  the ` (keys s - {None})" by (simp only: keys_restrict_indets_pp)
  also from s  keys p have "  the ` (indets p - {None})"
    by (intro image_mono Diff_mono keys_subset_indets subset_refl)
  finally show "x  the ` (indets p - {None})" .
qed

lemma poly_deg_restrict_indets_le: "poly_deg (restrict_indets p)  poly_deg p"
proof (rule poly_deg_leI)
  fix t
  assume "t  keys (restrict_indets p)"
  hence "t  restrict_indets_pp ` keys p" using keys_restrict_indets_subset ..
  then obtain s where "s  keys p" and "t = restrict_indets_pp s" ..
  from this(2) have "deg_pm t + lookup s None = deg_pm s"
    by (simp only: deg_pm_restrict_indets_pp)
  also from s  keys p have "  poly_deg p" by (rule poly_deg_max_keys)
  finally show "deg_pm t  poly_deg p" by simp
qed

lemma
  shows restrict_indets_zero [simp]: "restrict_indets 0 = 0"
    and restrict_indets_one [simp]: "restrict_indets 1 = 1"
    and restrict_indets_monomial: "restrict_indets (monomial c t) = monomial c (restrict_indets_pp t)"
    and restrict_indets_plus: "restrict_indets (p + q) = restrict_indets p + restrict_indets q"
    and restrict_indets_uminus: "restrict_indets (- r) = - restrict_indets (r::_ 0 _::comm_ring_1)"
    and restrict_indets_minus: "restrict_indets (r - r') = restrict_indets r - restrict_indets r'"
    and restrict_indets_times: "restrict_indets (p * q) = restrict_indets p * restrict_indets q"
    and restrict_indets_power: "restrict_indets (p ^ n) = restrict_indets p ^ n"
    and restrict_indets_sum: "restrict_indets (sum f A) = (aA. restrict_indets (f a))"
    and restrict_indets_prod: "restrict_indets (prod f A) = (aA. restrict_indets (f a))"
  by (simp_all add: restrict_indets_def poly_subst_monomial poly_subst_plus poly_subst_uminus
      poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod
      subst_pp_restrict_indets_subst punit.monom_mult_monomial)

lemma restrict_extend_indets [simp]: "restrict_indets (extend_indets p) = p"
  unfolding extend_indets_def restrict_indets_def poly_subst_poly_subst
  by (rule poly_subst_id)
    (simp add: extend_indets_subst_def restrict_indets_subst_def poly_subst_monomial subst_pp_single)

lemma extend_restrict_indets:
  assumes "None  indets p"
  shows "extend_indets (restrict_indets p) = p"
  unfolding extend_indets_def restrict_indets_def poly_subst_poly_subst
proof (rule poly_subst_id)
  fix x
  assume "x  indets p"
  with assms have "x  None" by meson
  then obtain y where x: "x = Some y" by blast
  thus "poly_subst extend_indets_subst (monomial 1 (restrict_indets_subst x)) =
         monomial 1 (Poly_Mapping.single x 1)"
    by (simp add: extend_indets_subst_def restrict_indets_subst_def poly_subst_monomial subst_pp_single)
qed

lemma restrict_indets_dehomogenize [simp]: "restrict_indets (dehomogenize None p) = restrict_indets p"
proof -
  have eq: "poly_subst (λx. (monomial 1 (restrict_indets_subst x))) (dehomo_subst None y) =
            monomial 1 (restrict_indets_subst y)" for y::"'x option"
    by (auto simp: restrict_indets_subst_def dehomo_subst_def poly_subst_monomial subst_pp_single)
  show ?thesis by (simp only: dehomogenize_def restrict_indets_def poly_subst_poly_subst eq) 
qed

corollary restrict_indets_comp_dehomogenize: "restrict_indets  dehomogenize None = restrict_indets"
  by (rule ext) (simp only: o_def restrict_indets_dehomogenize)

corollary extend_restrict_indets_eq_dehomogenize:
  "extend_indets (restrict_indets p) = dehomogenize None p"
proof -
  have "extend_indets (restrict_indets p) = extend_indets (restrict_indets (dehomogenize None p))"
    by simp
  also have " = dehomogenize None p"
  proof (intro extend_restrict_indets notI)
    assume "None  indets (dehomogenize None p)"
    hence "None  indets p - {None}" using indets_dehomogenize ..
    thus False by simp
  qed
  finally show ?thesis .
qed

corollary extend_indets_comp_restrict_indets: "extend_indets  restrict_indets = dehomogenize None"
  by (rule ext) (simp only: o_def extend_restrict_indets_eq_dehomogenize)

lemma restrict_homogenize_extend_indets [simp]:
  "restrict_indets (homogenize None (extend_indets p)) = p"
proof -
  have "restrict_indets (homogenize None (extend_indets p)) =
          restrict_indets (dehomogenize None (homogenize None (extend_indets p)))"
    by (simp only: restrict_indets_dehomogenize)
  also have " = restrict_indets (dehomogenize None (extend_indets p))"
    by (simp only: dehomogenize_homogenize)
  also have " = p" by simp
  finally show ?thesis .
qed

lemma dehomogenize_extend_indets [simp]: "dehomogenize None (extend_indets p) = extend_indets p"
  by (simp add: indets_extend_indets)

lemma restrict_indets_ideal: "restrict_indets ` ideal F = ideal (restrict_indets ` F)"
  using restrict_indets_plus restrict_indets_times
proof (rule image_ideal_eq_surj)
  from restrict_extend_indets show "surj restrict_indets" by (rule surjI)
qed

lemma ideal_restrict_indets:
  "ideal G = ideal (homogenize None ` extend_indets ` F)  ideal (restrict_indets ` G) = ideal F"
  by (simp flip: restrict_indets_ideal) (simp add: restrict_indets_ideal image_image)

lemma extend_indets_ideal: "extend_indets ` ideal F = ideal (extend_indets ` F)  P[- {None}]"
proof -
  have "extend_indets ` ideal F = extend_indets ` restrict_indets ` ideal (extend_indets ` F)"
    by (simp add: restrict_indets_ideal image_image)
  also have " = ideal (extend_indets ` F)  P[- {None}]"
    by (simp add: extend_restrict_indets_eq_dehomogenize dehomogenize_ideal image_image)
  finally show ?thesis .
qed

corollary extend_indets_ideal_subset: "extend_indets ` ideal F  ideal (extend_indets ` F)"
  by (simp add: extend_indets_ideal)

subsection ‹Canonical Isomorphisms between P[X,Y]› and P[X][Y]›: focus› and flatten›

definition focus :: "'x set  (('x 0 nat) 0 'a)  (('x 0 nat) 0 ('x 0 nat) 0 'a::comm_monoid_add)"
  where "focus X p = (tkeys p. monomial (monomial (lookup p t) (except t X)) (except t (- X)))"

definition flatten :: "('a 0 'a 0 'b)  ('a::comm_powerprod 0 'b::semiring_1)"
  where "flatten p = (tkeys p. punit.monom_mult 1 t (lookup p t))"

lemma focus_superset:
  assumes "finite A" and "keys p  A"
  shows "focus X p = (tA. monomial (monomial (lookup p t) (except t X)) (except t (- X)))"
  unfolding focus_def using assms by (rule sum.mono_neutral_left) (simp add: in_keys_iff)

lemma keys_focus: "keys (focus X p) = (λt. except t (- X)) ` keys p"
proof
  have "keys (focus X p)  (tkeys p. keys (monomial (monomial (lookup p t) (except t X)) (except t (- X))))"
    unfolding focus_def by (rule keys_sum_subset)
  also have "  (tkeys p. {except t (- X)})" by (intro UN_mono subset_refl) simp
  also have " = (λt. except t (- X)) ` keys p" by (rule UNION_singleton_eq_range)
  finally show "keys (focus X p)  (λt. except t (- X)) ` keys p" .
next
  {
    fix s
    assume "s  keys p"
    have "lookup (focus X p) (except s (- X)) =
              (tkeys p. monomial (lookup p t) (except t X) when except t (- X) = except s (- X))"
      (is "_ = ?p")
      by (simp only: focus_def lookup_sum lookup_single)
    also have "  0"
    proof
      have "lookup ?p (except s X) =
              (tkeys p. lookup p t when except t X = except s X  except t (- X) = except s (- X))"
        by (simp add: lookup_sum lookup_single when_def if_distrib if_distribR)
            (metis (no_types, opaque_lifting) lookup_single_eq lookup_single_not_eq lookup_zero)
      also have " = (t{s}. lookup p t)"
      proof (intro sum.mono_neutral_cong_right ballI)
        fix t
        assume "t  keys p - {s}"
        hence "t  s" by simp
        hence "except t X + except t (- X)  except s X + except s (- X)"
          by (simp flip: except_decomp)
        thus "(lookup p t when except t X = except s X  except t (- X) = except s (- X)) = 0"
          by (auto simp: when_def)
      next
        from s  keys p show "{s}  keys p" by simp
      qed simp_all
      also from s  keys p have "  0" by (simp add: in_keys_iff)
      finally have "except s X  keys ?p" by (simp add: in_keys_iff)
      moreover assume "?p = 0"
      ultimately show False by simp
    qed
    finally have "except s (- X)  keys (focus X p)" by (simp add: in_keys_iff)
  }
  thus "(λt. except t (- X)) ` keys p  keys (focus X p)" by blast
qed

lemma keys_coeffs_focus_subset:
  assumes "c  range (lookup (focus X p))"
  shows "keys c  (λt. except t X) ` keys p"
proof -
  from assms obtain s where "c = lookup (focus X p) s" ..
  hence "keys c = keys (lookup (focus X p) s)" by (simp only:)
  also have "  (tkeys p. keys (lookup (monomial (monomial (lookup p t) (except t X)) (except t (- X))) s))"
    unfolding focus_def lookup_sum by (rule keys_sum_subset)
  also from subset_refl have "  (tkeys p. {except t X})"
    by (rule UN_mono) (simp add: lookup_single when_def)
  also have " = (λt. except t X) ` keys p" by (rule UNION_singleton_eq_range)
  finally show ?thesis .
qed

lemma focus_in_Polys':
  assumes "p  P[Y]"
  shows "focus X p  P[Y  X]"
proof (intro PolysI subsetI)
  fix t
  assume "t  keys (focus X p)"
  then obtain s where "s  keys p" and t: "t = except s (- X)" unfolding keys_focus ..
  note this(1)
  also from assms have "keys p  .[Y]" by (rule PolysD)
  finally have "keys s  Y" by (rule PPsD)
  hence "keys t  Y  X" by (simp add: t keys_except le_infI1)
  thus "t  .[Y  X]" by (rule PPsI)
qed

corollary focus_in_Polys: "focus X p  P[X]"
proof -
  have "p  P[UNIV]" by simp
  hence "focus X p  P[UNIV  X]" by (rule focus_in_Polys')
  thus ?thesis by simp
qed

lemma focus_coeffs_subset_Polys':
  assumes "p  P[Y]"
  shows "range (lookup (focus X p))  P[Y - X]"
proof (intro subsetI PolysI)
  fix c t
  assume "c  range (lookup (focus X p))"
  hence "keys c  (λt. except t X) ` keys p" by (rule keys_coeffs_focus_subset)
  moreover assume "t  keys c"
  ultimately have "t  (λt. except t X) ` keys p" ..
  then obtain s where "s  keys p" and t: "t = except s X" ..
  note this(1)
  also from assms have "keys p  .[Y]" by (rule PolysD)
  finally have "keys s  Y" by (rule PPsD)
  hence "keys t  Y - X" by (simp add: t keys_except Diff_mono)
  thus "t  .[Y - X]" by (rule PPsI)
qed

corollary focus_coeffs_subset_Polys: "range (lookup (focus X p))  P[- X]"
proof -
  have "p  P[UNIV]" by simp
  hence "range (lookup (focus X p))  P[UNIV - X]" by (rule focus_coeffs_subset_Polys')
  thus ?thesis by (simp only: Compl_eq_Diff_UNIV)
qed

corollary lookup_focus_in_Polys: "lookup (focus X p) t  P[- X]"
  using focus_coeffs_subset_Polys by blast

lemma focus_zero [simp]: "focus X 0 = 0"
  by (simp add: focus_def)

lemma focus_eq_zero_iff [iff]: "focus X p = 0  p = 0"
  by (simp only: keys_focus flip: keys_eq_empty_iff) simp

lemma focus_one [simp]: "focus X 1 = 1"
  by (simp add: focus_def)

lemma focus_monomial: "focus X (monomial c t) = monomial (monomial c (except t X)) (except t (- X))"
  by (simp add: focus_def)

lemma focus_uminus [simp]: "focus X (- p) = - focus X p"
  by (simp add: focus_def keys_uminus single_uminus sum_negf)

lemma focus_plus: "focus X (p + q) = focus X p + focus X q"
proof -
  have "finite (keys p  keys q)" by simp
  moreover have "keys (p + q)  keys p  keys q" by (rule Poly_Mapping.keys_add)
  ultimately show ?thesis
    by (simp add: focus_superset[where A="keys p  keys q"] lookup_add single_add sum.distrib)
qed

lemma focus_minus: "focus X (p - q) = focus X p - focus X (q::_ 0 _::ab_group_add)"
  by (simp only: diff_conv_add_uminus focus_plus focus_uminus)

lemma focus_times: "focus X (p * q) = focus X p * focus X q"
proof -
  have eq: "focus X (monomial c s * q) = focus X (monomial c s) * focus X q" for c s
  proof -
    have "focus X (monomial c s * q) = focus X (punit.monom_mult c s q)"
      by (simp only: times_monomial_left)
    also have " = (t(+) s ` keys q. monomial (monomial (lookup (punit.monom_mult c s q) t)
                                            (except t X)) (except t (- X)))"
      by (rule focus_superset) (simp_all add: punit.keys_monom_mult_subset[simplified])
    also have " = (tkeys q. ((λt. monomial (monomial (lookup (punit.monom_mult c s q) t)
                                  (except t X)) (except t (- X)))  ((+) s)) t)"
      by (rule sum.reindex) simp
    also have " = monomial (monomial c (except s X)) (except s (- X)) *
                      (tkeys q. monomial (monomial (lookup q t) (except t X)) (except t (- X)))"
      by (simp add: o_def punit.lookup_monom_mult except_plus times_monomial_monomial sum_distrib_left)
    also have " = focus X (monomial c s) * focus X q"
      by (simp only: focus_monomial focus_def[where p=q])
    finally show ?thesis .
  qed
  show ?thesis by (induct p rule: poly_mapping_plus_induct) (simp_all add: ring_distribs focus_plus eq)
qed

lemma focus_sum: "focus X (sum f I) = (iI. focus X (f i))"
  by (induct I rule: infinite_finite_induct) (simp_all add: focus_plus)

lemma focus_prod: "focus X (prod f I) = (iI. focus X (f i))"
  by (induct I rule: infinite_finite_induct) (simp_all add: focus_times)

lemma focus_power [simp]: "focus X (f ^ m) = focus X f ^ m"
  by (induct m) (simp_all add: focus_times)

lemma focus_Polys:
  assumes "p  P[X]"
  shows "focus X p = (tkeys p. monomial (monomial (lookup p t) 0) t)"
  unfolding focus_def
proof (rule sum.cong)
  fix t
  assume "t  keys p"
  also from assms have "  .[X]" by (rule PolysD)
  finally have "keys t  X" by (rule PPsD)
  hence "except t X = 0" and "except t (- X) = t" by (rule except_eq_zeroI, auto simp: except_id_iff)
  thus "monomial (monomial (lookup p t) (except t X)) (except t (- X)) =
        monomial (monomial (lookup p t) 0) t" by simp
qed (fact refl)

corollary lookup_focus_Polys: "p  P[X]  lookup (focus X p) t = monomial (lookup p t) 0"
  by (simp add: focus_Polys lookup_sum lookup_single when_def in_keys_iff)

lemma focus_Polys_Compl:
  assumes "p  P[- X]"
  shows "focus X p = monomial p 0"
proof -
  have "focus X p = (tkeys p. monomial (monomial (lookup p t) t) 0)" unfolding focus_def
  proof (rule sum.cong)
    fix t
    assume "t  keys p"
    also from assms have "  .[- X]" by (rule PolysD)
    finally have "keys t  - X" by (rule PPsD)
    hence "except t (- X) = 0" and "except t X = t" by (rule except_eq_zeroI, auto simp: except_id_iff)
    thus "monomial (monomial (lookup p t) (except t X)) (except t (- X)) =
          monomial (monomial (lookup p t) t) 0" by simp
  qed (fact refl)
  also have " = monomial (tkeys p. monomial (lookup p t) t) 0" by (simp only: monomial_sum)
  also have " = monomial p 0" by (simp only: poly_mapping_sum_monomials)
  finally show ?thesis .
qed

corollary focus_empty [simp]: "focus {} p = monomial p 0"
  by (rule focus_Polys_Compl) simp

lemma focus_Int:
  assumes "p  P[Y]"
  shows "focus (X  Y) p = focus X p"
  unfolding focus_def using refl
proof (rule sum.cong)
  fix t
  assume "t  keys p"
  also from assms have "  .[Y]" by (rule PolysD)
  finally have "keys t  Y" by (rule PPsD)
  hence "keys t  X  Y" by blast
  hence "except t (X  Y) = except t X + except t Y" by (rule except_Int)
  also from keys t  Y have "except t Y = 0" by (rule except_eq_zeroI)
  finally have eq: "except t (X  Y) = except t X" by simp
  have "except t (- (X  Y)) = except (except t (- Y)) (- X)" by (simp add: except_except Un_commute)
  also from keys t  Y have "except t (- Y) = t" by (auto simp: except_id_iff)
  finally show "monomial (monomial (lookup p t) (except t (X  Y))) (except t (- (X  Y))) =
                monomial (monomial (lookup p t) (except t X)) (except t (- X))" by (simp only: eq)
qed

lemma range_focusD:
  assumes "p  range (focus X)"
  shows "p  P[X]" and "range (lookup p)  P[- X]" and "lookup p t  P[- X]"
  using assms by (auto intro: focus_in_Polys lookup_focus_in_Polys)

lemma range_focusI:
  assumes "p  P[X]" and "lookup p ` keys (p::_ 0 _ 0 _::semiring_1)  P[- X]"
  shows "p  range (focus X)"
  using assms
proof (induct p rule: poly_mapping_plus_induct_Polys)
  case 0
  show ?case by simp
next
  case (plus p c t)
  from plus.hyps(3) have 1: "keys (monomial c t) = {t}" by simp
  also from plus.hyps(4) have "  keys p = {}" by simp
  finally have "keys (monomial c t + p) = keys (monomial c t)  keys p" by (rule keys_add[symmetric])
  hence 2: "keys (monomial c t + p) = insert t (keys p)" by (simp only: 1 flip: insert_is_Un)
  from t  .[X] have "keys t  X" by (rule PPsD)
  hence eq1: "except t X = 0" and eq2: "except t (- X) = t"
    by (rule except_eq_zeroI, auto simp: except_id_iff)
  from plus.hyps(3, 4) plus.prems have "c  P[- X]" and "lookup p ` keys p  P[- X]"
    by (simp_all add: 2 lookup_add lookup_single in_keys_iff)
        (smt add.commute add.right_neutral image_cong plus.hyps(4) when_simps(2))
  from this(2) have "p  range (focus X)" by (rule plus.hyps)
  then obtain q where p: "p = focus X q" ..
  moreover from c  P[- X] have "monomial c t = focus X (monomial 1 t * c)"
    by (simp add: focus_times focus_monomial eq1 eq2 focus_Polys_Compl times_monomial_monomial)
  ultimately have "monomial c t + p = focus X (monomial 1 t * c + q)" by (simp only: focus_plus)
  thus ?case by (rule range_eqI)
qed

lemma inj_focus: "inj ((focus X) :: (('x 0 nat) 0 'a::ab_group_add)  _)"
proof (rule injI)
  fix p q :: "('x 0 nat) 0 'a"
  assume "focus X p = focus X q"
  hence "focus X (p - q) = 0" by (simp add: focus_minus)
  thus "p = q" by simp
qed

lemma flatten_superset:
  assumes "finite A" and "keys p  A"
  shows "flatten p = (tA. punit.monom_mult 1 t (lookup p t))"
  unfolding flatten_def using assms by (rule sum.mono_neutral_left) (simp add: in_keys_iff)

lemma keys_flatten_subset: "keys (flatten p)  (tkeys p. (+) t ` keys (lookup p t))"
proof -
  have "keys (flatten p)  (tkeys p. keys (punit.monom_mult 1 t (lookup p t)))"
    unfolding flatten_def by (rule keys_sum_subset)
  also from subset_refl have "  (tkeys p. (+) t ` keys (lookup p t))"
    by (rule UN_mono) (rule punit.keys_monom_mult_subset[simplified])
  finally show ?thesis .
qed

lemma flatten_in_Polys:
  assumes "p  P[X]" and "lookup p ` keys p  P[Y]"
  shows "flatten p  P[X  Y]"
proof (intro PolysI subsetI)
  fix t
  assume "t  keys (flatten p)"
  also have "  (tkeys p. (+) t ` keys (lookup p t))" by (rule keys_flatten_subset)
  finally obtain s where "s  keys p" and "t  (+) s ` keys (lookup p s)" ..
  from this(2) obtain s' where "s'  keys (lookup p s)" and t: "t = s + s'" ..
  from assms(1) have "keys p  .[X]" by (rule PolysD)
  with s  keys p have "s  .[X]" ..
  also have "  .[X  Y]" by (rule PPs_mono) simp
  finally have 1: "s  .[X  Y]" .
  from s  keys p have "lookup p s  lookup p ` keys p" by (rule imageI)
  also have "  P[Y]" by fact
  finally have "keys (lookup p s)  .[Y]" by (rule PolysD)
  with s'  _ have "s'  .[Y]" ..
  also have "  .[X  Y]" by (rule PPs_mono) simp
  finally have "s'  .[X  Y]" .
  with 1 show "t  .[X  Y]" unfolding t by (rule PPs_closed_plus)
qed

lemma flatten_zero [simp]: "flatten 0 = 0"
  by (simp add: flatten_def)

lemma flatten_one [simp]: "flatten 1 = 1"
  by (simp add: flatten_def)

lemma flatten_monomial: "flatten (monomial c t) = punit.monom_mult 1 t c"
  by (simp add: flatten_def)

lemma flatten_uminus [simp]: "flatten (- p) = - flatten (p::_ 0 _ 0 _::ring)"
  by (simp add: flatten_def keys_uminus punit.monom_mult_uminus_right sum_negf)

lemma flatten_plus: "flatten (p + q) = flatten p + flatten q"
proof -
  have "finite (keys p  keys q)" by simp
  moreover have "keys (p + q)  keys p  keys q" by (rule Poly_Mapping.keys_add)
  ultimately show ?thesis
    by (simp add: flatten_superset[where A="keys p  keys q"] punit.monom_mult_dist_right lookup_add
                  sum.distrib)
qed

lemma flatten_minus: "flatten (p - q) = flatten p - flatten (q::_ 0 _ 0 _::ring)"
  by (simp only: diff_conv_add_uminus flatten_plus flatten_uminus)

lemma flatten_times: "flatten (p * q) = flatten p * flatten (q::_ 0 _ 0 'b::comm_semiring_1)"
proof -
  have eq: "flatten (monomial c s * q) = flatten (monomial c s) * flatten q" for c s
  proof -
    have eq: "monomial 1 (t + s) = monomial 1 s * monomial (1::'b) t" for t
      by (simp add: times_monomial_monomial add.commute)
    have "flatten (monomial c s * q) = flatten (punit.monom_mult c s q)"
      by (simp only: times_monomial_left)
    also have " = (t(+) s ` keys q. punit.monom_mult 1 t (lookup (punit.monom_mult c s q) t))"
      by (rule flatten_superset) (simp_all add: punit.keys_monom_mult_subset[simplified])
    also have " = (tkeys q. ((λt. punit.monom_mult 1 t (lookup (punit.monom_mult c s q) t))  (+) s) t)"
      by (rule sum.reindex) simp
    thm times_monomial_left
    also have " = punit.monom_mult 1 s c *
                      (tkeys q. punit.monom_mult 1 t (lookup q t))"
      by (simp add: o_def punit.lookup_monom_mult sum_distrib_left)
          (simp add: algebra_simps eq flip: times_monomial_left)
    also have " = flatten (monomial c s) * flatten q"
      by (simp only: flatten_monomial flatten_def[where p=q])
    finally show ?thesis .
  qed
  show ?thesis by (induct p rule: poly_mapping_plus_induct) (simp_all add: ring_distribs flatten_plus eq)
qed

lemma flatten_monom_mult:
  "flatten (punit.monom_mult c t p) = punit.monom_mult 1 t (c * flatten (p::_ 0 _ 0 'b::comm_semiring_1))"
  by (simp only: flatten_times flatten_monomial mult.assoc flip: times_monomial_left)

lemma flatten_sum: "flatten (sum f I) = (iI. flatten (f i))"
  by (induct I rule: infinite_finite_induct) (simp_all add: flatten_plus)

lemma flatten_prod: "flatten (prod f I) = (iI. flatten (f i :: _ 0 _::comm_semiring_1))"
  by (induct I rule: infinite_finite_induct) (simp_all add: flatten_times)

lemma flatten_power [simp]: "flatten (f ^ m) = flatten (f:: _ 0 _::comm_semiring_1) ^ m"
  by (induct m) (simp_all add: flatten_times)

lemma surj_flatten: "surj flatten"
proof (rule surjI)
  fix p
  show "flatten (monomial p 0) = p" by (simp add: flatten_monomial)
qed

lemma flatten_focus [simp]: "flatten (focus X p) = p"
  by (induct p rule: poly_mapping_plus_induct)
      (simp_all add: focus_plus flatten_plus focus_monomial flatten_monomial
                      punit.monom_mult_monomial add.commute flip: except_decomp)

lemma focus_flatten:
  assumes "p  P[X]" and "lookup p ` keys p  P[- X]"
  shows "focus X (flatten p) = p"
proof -
  from assms have "p  range (focus X)" by (rule range_focusI)
  then obtain q where "p = focus X q" ..
  thus ?thesis by simp
qed

lemma image_focus_ideal: "focus X ` ideal F = ideal (focus X ` F)  range (focus X)"
proof
  from focus_plus focus_times have "focus X ` ideal F  ideal (focus X ` F)"
    by (rule image_ideal_subset)
  moreover from subset_UNIV have "focus X ` ideal F  range (focus X)" by (rule image_mono)
  ultimately show "focus X ` ideal F  ideal (focus X ` F)  range (focus X)" by blast
next
  show "ideal (focus X ` F)  range (focus X)  focus X ` ideal F"
  proof
    fix p
    assume "p  ideal (focus X ` F)  range (focus X)"
    hence "p  ideal (focus X ` F)" and "p  range (focus X)" by simp_all
    from this(1) obtain F0 q where "F0  focus X ` F" and p: "p = (f'F0. q f' * f')"
      by (rule ideal.spanE)
    from this(1) obtain F' where "F'  F" and F0: "F0 = focus X ` F'" by (rule subset_imageE)
    from inj_focus subset_UNIV have "inj_on (focus X) F'" by (rule inj_on_subset)
    from p  range _ obtain p' where "p = focus X p'" ..
    hence "p = focus X (flatten p)" by simp
    also from inj_on _ F' have " = focus X (f'F'. flatten (q (focus X f')) * f')"
      by (simp add: p F0 sum.reindex flatten_sum flatten_times)
    finally have "p = focus X (f'F'. flatten (q (focus X f')) * f')" .
    moreover have "(f'F'. flatten (q (focus X f')) * f')  ideal F"
    proof
      show "(f'F'. flatten (q (focus X f')) * f')  ideal F'" by (rule ideal.sum_in_spanI)
    next
      from F'  F show "ideal F'  ideal F" by (rule ideal.span_mono)
    qed
    ultimately show "p  focus X ` ideal F" by (rule image_eqI)
  qed
qed

lemma image_flatten_ideal: "flatten ` ideal F = ideal (flatten ` F)"
  using flatten_plus flatten_times surj_flatten by (rule image_ideal_eq_surj)

lemma poly_eval_focus:
  "poly_eval a (focus X p) = poly_subst (λx. if x  X then a x else monomial 1 (Poly_Mapping.single x 1)) p"
proof -
  let ?b = "λx. if x  X then a x else monomial 1 (Poly_Mapping.single x 1)"
  have *: "lookup (punit.monom_mult (monomial (lookup p t) (except t X)) 0
              (subst_pp (λx. monomial (a x) 0) (except t (- X)))) 0 =
            punit.monom_mult (lookup p t) 0 (subst_pp ?b t)" for t
  proof -
    have 1: "subst_pp ?b (except t X) = monomial 1 (except t X)"
      by (rule subst_pp_id) (simp add: keys_except)
    from refl have 2: "subst_pp ?b (except t (- X)) = subst_pp a (except t (-X))"
      by (rule subst_pp_cong) (simp add: keys_except)
    have "lookup (punit.monom_mult (monomial (lookup p t) (except t X)) 0
                      (subst_pp (λx. monomial (a x) 0) (except t (- X)))) 0 =
          punit.monom_mult (lookup p t) (except t X) (subst_pp a (except t (- X)))"
      by (simp add: lookup_times_zero subst_pp_def lookup_prod_zero lookup_power_zero
                flip: times_monomial_left)
    also have " = punit.monom_mult (lookup p t) 0 (monomial 1 (except t X) * subst_pp a (except t (- X)))"
      by (simp add: times_monomial_monomial flip: times_monomial_left mult.assoc)
    also have " = punit.monom_mult (lookup p t) 0 (subst_pp ?b (except t X + except t (- X)))"
      by (simp only: subst_pp_plus 1 2)
    also have " = punit.monom_mult (lookup p t) 0 (subst_pp ?b t)" by (simp flip: except_decomp)
    finally show ?thesis .
  qed
  show ?thesis by (simp add: poly_eval_def focus_def poly_subst_sum lookup_sum poly_subst_monomial *
                        flip: poly_subst_def)
qed

corollary poly_eval_poly_eval_focus:
  "poly_eval a (poly_eval b (focus X p)) = poly_eval (λx::'x. if x  X then poly_eval a (b x) else a x) p"
proof -
  have eq: "monomial (lookup (poly_subst (λy. monomial (a y) (0::'x 0 nat)) q) 0) 0 =
              poly_subst (λy. monomial (a y) (0::'x 0 nat)) q" for q
    by (intro poly_deg_zero_imp_monomial poly_deg_poly_subst_eq_zeroI) simp
  show ?thesis unfolding poly_eval_focus
    by (simp add: poly_eval_def poly_subst_poly_subst if_distrib poly_subst_monomial subst_pp_single eq
            cong: if_cong)
qed

lemma indets_poly_eval_focus_subset:
  "indets (poly_eval a (focus X p))   (indets ` a ` X)  (indets p - X)"
proof
  fix x
  assume "x  indets (poly_eval a (focus X p))"
  also have " = indets (poly_subst (λx. if x  X then a x else monomial 1 (Poly_Mapping.single x 1)) p)"
    (is "_ = indets (poly_subst ?f _)") by (simp only: poly_eval_focus)
  finally obtain y where "y  indets p" and "x  indets (?f y)" by (rule in_indets_poly_substE)
  from this(2) have "(x  X  x = y)  (y  X  x  indets (a y))"
    by (simp add: indets_monomial split: if_split_asm)
  thus "x   (indets ` a ` X)  (indets p - X)"
  proof (elim disjE conjE)
    assume "x  X" and "x = y"
    with y  indets p have "x  indets p - X" by simp
    thus ?thesis ..
  next
    assume "y  X" and "x  indets (a y)"
    hence "x   (indets ` a ` X)" by blast
    thus ?thesis ..
  qed
qed

lemma lookup_poly_eval_focus:
  "lookup (poly_eval (λx. monomial (a x) 0) (focus X p)) t = poly_eval a (lookup (focus (- X) p) t)"
proof -
  let ?f = "λx. if x  X then monomial (a x) 0 else monomial 1 (Poly_Mapping.single x 1)"
  have eq: "subst_pp ?f s = monomial (xkeys s  X. a x ^ lookup s x) (except s X)" for s
  proof -
    have "subst_pp ?f s = (x(keys s  X)  (keys s - X). ?f x ^ lookup s x)"
      unfolding subst_pp_def by (rule prod.cong) blast+
    also have " = (xkeys s  X. ?f x ^ lookup s x) * (xkeys s - X. ?f x ^ lookup s x)"
      by (rule prod.union_disjoint) auto
    also have " = monomial (xkeys s  X. a x ^ lookup s x)
                              (xkeys s - X. Poly_Mapping.single x (lookup s x))"
      by (simp add: monomial_power_map_scale times_monomial_monomial flip: punit.monomial_prod_sum)
    also have "(xkeys s - X. Poly_Mapping.single x (lookup s x)) = except s X"
      by (metis (mono_tags, lifting) DiffD2 keys_except lookup_except_eq_idI
              poly_mapping_sum_monomials sum.cong)
    finally show ?thesis .
  qed
  show ?thesis
    by (simp add: poly_eval_focus poly_subst_def lookup_sum eq flip: punit.map_scale_eq_monom_mult)
       (simp add: focus_def lookup_sum poly_eval_sum lookup_single when_distrib poly_eval_monomial
                  keys_except lookup_except_when)
qed

lemma keys_poly_eval_focus_subset:
  "keys (poly_eval (λx. monomial (a x) 0) (focus X p))  (λt. except t X) ` keys p"
proof
  fix t
  assume "t  keys (poly_eval (λx. monomial (a x) 0) (focus X p))"
  hence "lookup (poly_eval (λx. monomial (a x) 0) (focus X p)) t  0" by (simp add: in_keys_iff)
  hence "poly_eval a (lookup (focus (- X) p) t)  0" by (simp add: lookup_poly_eval_focus)
  hence "t  keys (focus (- X) p)" by (auto simp flip: lookup_not_eq_zero_eq_in_keys)
  thus "t  (λt. except t X) ` keys p" by (simp add: keys_focus)
qed

lemma poly_eval_focus_in_Polys:
  assumes "p  P[X]"
  shows "poly_eval (λx. monomial (a x) 0) (focus Y p)  P[X - Y]"
proof (rule PolysI_alt)
  have "indets (poly_eval (λx. monomial (a x) 0) (focus Y p)) 
           (indets ` (λx. monomial (a x) 0) ` Y)  (indets p - Y)"
    by (fact indets_poly_eval_focus_subset)
  also have " = indets p - Y" by simp
  also from assms have "  X - Y" by (auto dest: PolysD)
  finally show "indets (poly_eval (λx. monomial (a x) 0) (focus Y p))  X - Y" .
qed

lemma image_poly_eval_focus_ideal:
  "poly_eval (λx. monomial (a x) 0) ` focus X ` ideal F =
    ideal (poly_eval (λx. monomial (a x) 0) ` focus X ` F) 
      (P[- X]::(('x 0 nat) 0 'a::comm_ring_1) set)"
proof -
  let ?h = "λf. poly_eval (λx. monomial (a x) 0) (focus X f)"
  have h_id: "?h p = p" if "p  P[- X]" for p
  proof -
    from that have "focus X p  P[- X  X]" by (rule focus_in_Polys')
    also have " = P[{}]" by simp
    finally obtain c where eq: "focus X p = monomial c 0" unfolding Polys_empty ..
    hence "flatten (focus X p) = flatten (monomial c 0)" by (rule arg_cong)
    hence "c = p" by (simp add: flatten_monomial)
    thus "?h p = p" by (simp add: eq poly_eval_monomial)
  qed
  have rng: "range ?h = P[- X]"
  proof (intro subset_antisym subsetI, elim rangeE)
    fix b f
    assume b: "b = ?h f"
    have "?h f  P[UNIV - X]" by (rule poly_eval_focus_in_Polys) simp
    thus "b  P[- X]" by (simp add: b Compl_eq_Diff_UNIV)
  next
    fix p :: "('x 0 nat) 0 'a"
    assume "p  P[- X]"
    hence "?h p = p" by (rule h_id)
    hence "p = ?h p" by (rule sym)
    thus "p  range ?h" by (rule range_eqI)
  qed
  have "poly_eval (λx. monomial (a x) 0) ` focus X ` ideal F = ?h ` ideal F" by (fact image_image)
  also have " = ideal (?h ` F)  range ?h"
  proof (rule image_ideal_eq_Int)
    fix p
    have "?h p  range ?h" by (fact rangeI)
    also have " = P[- X]" by fact
    finally show "?h (?h p) = ?h p" by (rule h_id)
  qed (simp_all only: focus_plus poly_eval_plus focus_times poly_eval_times)
  also have " = ideal (poly_eval (λx. monomial (a x) 0) ` focus X ` F)  P[- X]"
    by (simp only: image_image rng)
  finally show ?thesis .
qed

subsection ‹Locale @{term pm_powerprod}

lemma varnum_eq_zero_iff: "varnum X t = 0  t  .[X]"
  by (auto simp: varnum_def PPs_def)

lemma dgrad_set_varnum: "dgrad_set (varnum X) 0 = .[X]"
  by (simp add: dgrad_set_def PPs_def varnum_eq_zero_iff)

context ordered_powerprod
begin

abbreviation "lcf  punit.lc"
abbreviation "tcf  punit.tc"
abbreviation "lpp  punit.lt"
abbreviation "tpp  punit.tt"

end (* ordered_powerprod *)

locale pm_powerprod =
  ordered_powerprod ord ord_strict
  for ord::"('x::{countable,linorder} 0 nat)  ('x 0 nat)  bool" (infixl "" 50)
  and ord_strict (infixl "" 50)
begin

sublocale gd_powerprod ..

lemma PPs_closed_lpp:
  assumes "p  P[X]"
  shows "lpp p  .[X]"
proof (cases "p = 0")
  case True
  thus ?thesis by (simp add: zero_in_PPs)
next
  case False
  hence "lpp p  keys p" by (rule punit.lt_in_keys)
  also from assms have "  .[X]" by (rule PolysD)
  finally show ?thesis .
qed

lemma PPs_closed_tpp:
  assumes "p  P[X]"
  shows "tpp p  .[X]"
proof (cases "p = 0")
  case True
  thus ?thesis by (simp add: zero_in_PPs)
next
  case False
  hence "tpp p  keys p" by (rule punit.tt_in_keys)
  also from assms have "  .[X]" by (rule PolysD)
  finally show ?thesis .
qed

corollary PPs_closed_image_lpp: "F  P[X]  lpp ` F  .[X]"
  by (auto intro: PPs_closed_lpp)

corollary PPs_closed_image_tpp: "F  P[X]  tpp ` F  .[X]"
  by (auto intro: PPs_closed_tpp)

lemma hom_component_lpp:
  assumes "p  0"
  shows "hom_component p (deg_pm (lpp p))  0" (is "?p  0")
    and "lpp (hom_component p (deg_pm (lpp p))) = lpp p"
proof -
  from assms have "lpp p  keys p" by (rule punit.lt_in_keys)
  hence *: "lpp p  keys ?p" by (simp add: keys_hom_component)
  thus "?p  0" by auto

  from * show "lpp ?p = lpp p"
  proof (rule punit.lt_eqI_keys)
    fix t
    assume "t  keys ?p"
    hence "t  keys p" by (simp add: keys_hom_component)
    thus "t  lpp p" by (rule punit.lt_max_keys)
  qed
qed

definition is_hom_ord :: "'x  bool"
  where "is_hom_ord x  (s t. deg_pm s = deg_pm t  (s  t  except s {x}  except t {x}))"

lemma is_hom_ordD: "is_hom_ord x  deg_pm s = deg_pm t  s  t  except s {x}  except t {x}"
  by (simp add: is_hom_ord_def)

lemma dgrad_p_set_varnum: "punit.dgrad_p_set (varnum X) 0 = P[X]"
  by (simp add: punit.dgrad_p_set_def dgrad_set_varnum Polys_def)

end

text ‹We must create a copy of @{locale pm_powerprod} to avoid infinite chains of interpretations.›

instantiation option :: (linorder) linorder
begin

fun less_eq_option :: "'a option  'a option  bool" where
  "less_eq_option None _ = True" |
  "less_eq_option (Some x) None = False" |
  "less_eq_option (Some x) (Some y) = (x  y)"

definition less_option :: "'a option  'a option  bool"
  where "less_option x y  x  y  ¬ y  x"

instance proof
  fix x :: "'a option"
  show "x  x" using less_eq_option.elims(3) by fastforce
qed (auto simp: less_option_def elim!: less_eq_option.elims)

end

locale extended_ord_pm_powerprod = pm_powerprod
begin

definition extended_ord :: "('a option 0 nat)  ('a option 0 nat)  bool"
  where "extended_ord s t  (restrict_indets_pp s  restrict_indets_pp t 
                          (restrict_indets_pp s = restrict_indets_pp t  lookup s None  lookup t None))"

definition extended_ord_strict :: "('a option 0 nat)  ('a option 0 nat)  bool"
  where "extended_ord_strict s t  (restrict_indets_pp s  restrict_indets_pp t 
                          (restrict_indets_pp s = restrict_indets_pp t  lookup s None < lookup t None))"

sublocale extended_ord: pm_powerprod extended_ord extended_ord_strict
proof -
  have 1: "s = t" if "lookup s None = lookup t None" and "restrict_indets_pp s = restrict_indets_pp t"
    for s t :: "'a option 0 nat"
  proof (rule poly_mapping_eqI)
    fix y
    show "lookup s y = lookup t y"
    proof (cases y)
      case None
      with that(1) show ?thesis by simp
    next
      case y: (Some z)
      have "lookup s y = lookup (restrict_indets_pp s) z" by (simp only: lookup_restrict_indets_pp y)
      also have " = lookup (restrict_indets_pp t) z" by (simp only: that(2))
      also have " = lookup t y" by (simp only: lookup_restrict_indets_pp y)
      finally show ?thesis .
    qed
  qed
  have 2: "0  t" if "t  0" for t::"'a 0 nat"
    using that zero_min by (rule ordered_powerprod_lin.dual_order.not_eq_order_implies_strict)
  show "pm_powerprod extended_ord extended_ord_strict"
    by standard (auto simp: extended_ord_def extended_ord_strict_def restrict_indets_pp_plus lookup_add 1
                  dest: plus_monotone_strict 2)
qed

lemma extended_ord_is_hom_ord: "extended_ord.is_hom_ord None"
  by (auto simp add: extended_ord_def lookup_restrict_indets_pp lookup_except extended_ord.is_hom_ord_def
            simp flip: deg_pm_restrict_indets_pp)

end

end (* theory *)