Theory Polynomials.MPoly_Type_Class_Ordered

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Type-Class-Multivariate Polynomials in Ordered Terms›

theory MPoly_Type_Class_Ordered
  imports MPoly_Type_Class
begin

class the_min = linorder +
  fixes the_min::'a
  assumes the_min_min: "the_min  x"

text ‹Type class @{class the_min} guarantees that a least element exists. Instances of @{class the_min}
  should provide @{emph ‹computable›} definitions of that element.›

instantiation nat :: the_min
begin
  definition "the_min_nat = (0::nat)"
  instance by (standard, simp add: the_min_nat_def)
end

instantiation unit :: the_min
begin
  definition "the_min_unit = ()"
  instance by (standard, simp add: the_min_unit_def)
end

locale ordered_term =
    term_powerprod pair_of_term term_of_pair +
    ordered_powerprod ord ord_strict +
    ord_term_lin: linorder ord_term ord_term_strict
      for pair_of_term::"'t  ('a::comm_powerprod × 'k::{the_min,wellorder})"
      and term_of_pair::"('a × 'k)  't"
      and ord::"'a  'a  bool" (infixl "" 50)
      and ord_strict (infixl "" 50)
      and ord_term::"'t  't  bool" (infixl "t" 50)
      and ord_term_strict::"'t  't  bool" (infixl "t" 50) +
		assumes splus_mono: "v t w  t  v t t  w"
    assumes ord_termI: "pp_of_term v  pp_of_term w  component_of_term v  component_of_term w  v t w"
begin

abbreviation ord_term_conv (infixl "t" 50) where "ord_term_conv  (≼t)¯¯"
abbreviation ord_term_strict_conv (infixl "t" 50) where "ord_term_strict_conv  (≺t)¯¯"

text ‹The definition of @{locale ordered_term} only covers TOP and POT orderings. 
  These two types of orderings are the only interesting ones.›

definition "min_term  term_of_pair (0, the_min)"

lemma min_term_min: "min_term t v"
proof (rule ord_termI)
  show "pp_of_term min_term  pp_of_term v" by (simp add: min_term_def zero_min term_simps)
next
  show "component_of_term min_term  component_of_term v" by (simp add: min_term_def the_min_min term_simps)
qed

lemma splus_mono_strict:
  assumes "v t w"
  shows "t  v t t  w"
proof -
  from assms have "v t w" and "v  w" by simp_all
  from this(1) have "t  v t t  w" by (rule splus_mono)
  moreover from v  w have "t  v  t  w" by (simp add: term_simps)
  ultimately show ?thesis using ord_term_lin.antisym_conv1 by blast
qed

lemma splus_mono_left:
  assumes "s  t"
  shows "s  v t t  v"
proof (rule ord_termI, simp_all add: term_simps)
  from assms show "s + pp_of_term v  t + pp_of_term v" by (rule plus_monotone)
qed

lemma splus_mono_strict_left:
  assumes "s  t"
  shows "s  v t t  v"
proof -
  from assms have "s  t" and "s  t" by simp_all
  from this(1) have "s  v t t  v" by (rule splus_mono_left)
  moreover from s  t have "s  v  t  v" by (simp add: term_simps)
  ultimately show ?thesis using ord_term_lin.antisym_conv1 by blast
qed

lemma ord_term_canc:
  assumes "t  v t t  w"
  shows "v t w"
proof (rule ccontr)
  assume "¬ v t w"
  hence "w t v" by simp
  hence "t  w t t  v" by (rule splus_mono_strict)
  with assms show False by simp
qed

lemma ord_term_strict_canc:
  assumes "t  v t t  w"
  shows "v t w"
proof (rule ccontr)
  assume "¬ v t w"
  hence "w t v" by simp
  hence "t  w t t  v" by (rule splus_mono)
  with assms show False by simp
qed

lemma ord_term_canc_left:
  assumes "t  v t s  v"
  shows "t  s"
proof (rule ccontr)
  assume "¬ t  s"
  hence "s  t" by simp
  hence "s  v t t  v" by (rule splus_mono_strict_left)
  with assms show False by simp
qed

lemma ord_term_strict_canc_left:
  assumes "t  v t s  v"
  shows "t  s"
proof (rule ccontr)
  assume "¬ t  s"
  hence "s  t" by simp
  hence "s  v t t  v" by (rule splus_mono_left)
  with assms show False by simp
qed

lemma ord_adds_term:
  assumes "u addst v"
  shows "u t v"
proof -
  from assms have *: "component_of_term u  component_of_term v" and "pp_of_term u adds pp_of_term v"
    by (simp_all add: adds_term_def)
  from this(2) have "pp_of_term u  pp_of_term v" by (rule ord_adds)
  from this * show ?thesis by (rule ord_termI)
qed

end

subsection ‹Interpretations›

context ordered_powerprod
begin

subsubsection ‹Unit›

sublocale punit: ordered_term to_pair_unit fst "(≼)" "(≺)" "(≼)" "(≺)"
  apply standard
  subgoal by (simp, fact plus_monotone_left)
  subgoal by (simp only: punit_pp_of_term punit_component_of_term)
  done

lemma punit_min_term [simp]: "punit.min_term = 0"
  by (simp add: punit.min_term_def)

end

subsection ‹Definitions›

context ordered_term
begin

definition higher :: "('t 0 'b)  't  ('t 0 'b::zero)"
  where "higher p t = except p {s. s t t}"

definition lower :: "('t 0 'b)  't  ('t 0 'b::zero)"
  where "lower p t = except p {s. t t s}"

definition lt :: "('t 0 'b::zero)  't"
  where "lt p = (if p = 0 then min_term else ord_term_lin.Max (keys p))"

abbreviation "lp p  pp_of_term (lt p)"

definition lc :: "('t 0 'b::zero)  'b"
  where "lc p = lookup p (lt p)"

definition tt :: "('t 0 'b::zero)  't"
  where "tt p = (if p = 0 then min_term else ord_term_lin.Min (keys p))"

abbreviation "tp p  pp_of_term (tt p)"

definition tc :: "('t 0 'b::zero)  'b"
  where "tc p  lookup p (tt p)"

definition tail :: "('t 0 'b)  ('t 0 'b::zero)"
  where "tail p  lower p (lt p)"

subsection ‹Leading Term and Leading Coefficient: @{const lt} and @{const lc}

lemma lt_zero [simp]: "lt 0 = min_term"
  by (simp add: lt_def)

lemma lc_zero [simp]: "lc 0 = 0"
  by (simp add: lc_def)

lemma lt_uminus [simp]: "lt (- p) = lt p"
  by (simp add: lt_def keys_uminus)

lemma lc_uminus [simp]: "lc (- p) = - lc p"
  by (simp add: lc_def)

lemma lt_alt:
  assumes "p  0"
  shows "lt p = ord_term_lin.Max (keys p)"
  using assms unfolding lt_def by simp

lemma lt_max:
  assumes "lookup p v  0"
  shows "v t lt p"
proof -
  from assms have t_in: "v  keys p" by (simp add: in_keys_iff)
  hence "keys p  {}" by auto
  hence "p  0" using keys_zero by blast
  from lt_alt[OF this] ord_term_lin.Max_ge[OF finite_keys t_in] show ?thesis by simp
qed

lemma lt_eqI:
  assumes "lookup p v  0" and "u. lookup p u  0  u t v"
  shows "lt p = v"
proof -
  from assms(1) have "v  keys p" by (simp add: in_keys_iff)
  hence "keys p  {}" by auto
  hence "p  0"
    using keys_zero by blast
  have "u t v" if "u  keys p" for u
  proof -
    from that have "lookup p u  0" by (simp add: in_keys_iff)
    thus "u t v" by (rule assms(2))
  qed
  from lt_alt[OF p  0] ord_term_lin.Max_eqI[OF finite_keys this v  keys p] show ?thesis by simp
qed

lemma lt_less:
  assumes "p  0" and "u. v t u  lookup p u = 0"
  shows "lt p t v"
proof -
  from p  0 have "keys p  {}"
    by simp
  have "ukeys p. u t v"
  proof
    fix u::'t
    assume "u  keys p"
    hence "lookup p u  0" by (simp add: in_keys_iff)
    hence "¬ v t u" using assms(2)[of u] by auto
    thus "u t v" by simp
  qed
  with lt_alt[OF assms(1)] ord_term_lin.Max_less_iff[OF finite_keys keys p  {}] show ?thesis by simp
qed

lemma lt_le:
  assumes "u. v t u  lookup p u = 0"
  shows "lt p t v"
proof (cases "p = 0")
  case True
  show ?thesis by (simp add: True min_term_min)
next
  case False
  hence "keys p  {}" by simp
  have "ukeys p. u t v"
  proof
    fix u::'t
    assume "u  keys p"
    hence "lookup p u  0" unfolding keys_def by simp
    hence "¬ v t u" using assms[of u] by auto
    thus "u t v" by simp
  qed
  with lt_alt[OF False] ord_term_lin.Max_le_iff[OF finite_keys[of p] keys p  {}]
    show ?thesis by simp
qed

lemma lt_gr:
  assumes "lookup p s  0" and "t t s"
  shows "t t lt p"
  using assms lt_max ord_term_lin.order.strict_trans2 by blast

lemma lc_not_0:
  assumes "p  0"
  shows "lc p  0"
proof -
  from keys_zero assms have "keys p  {}" by auto
  from lt_alt[OF assms] ord_term_lin.Max_in[OF finite_keys this] show ?thesis by (simp add: in_keys_iff lc_def)
qed

lemma lc_eq_zero_iff: "lc p = 0  p = 0"
  using lc_not_0 lc_zero by blast

lemma lt_in_keys:
  assumes "p  0"
  shows "lt p  (keys p)"
  by (metis assms in_keys_iff lc_def lc_not_0)

lemma lt_monomial:
  "lt (monomial c t) = t" if "c  0"
  using that by (auto simp add: lt_def dest: monomial_0D)

lemma lc_monomial [simp]: "lc (monomial c t) = c"
proof (cases "c = 0")
  case True
  thus ?thesis by simp
next
  case False
  thus ?thesis by (simp add: lc_def lt_monomial)
qed
   
lemma lt_le_iff: "lt p t v  (u. v t u  lookup p u = 0)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (intro allI impI)
    fix u
    note lt p t v
    also assume "v t u"
    finally have "lt p t u" .
    hence "¬ u t lt p" by simp
    with lt_max[of p u] show "lookup p u = 0" by blast
  qed
next
  assume ?R
  thus ?L using lt_le by auto
qed

lemma lt_plus_eqI:
  assumes "lt p t lt q"
  shows "lt (p + q) = lt q"
proof (cases "q = 0")
  case True
  with assms have "lt p t min_term" by (simp add: lt_def)
  with min_term_min[of "lt p"] show ?thesis by simp
next
  case False
  show ?thesis
  proof (intro lt_eqI)
    from lt_gr[of p "lt q" "lt p"] assms have "lookup p (lt q) = 0" by blast
    with lookup_add[of p q "lt q"] lc_not_0[OF False] show "lookup (p + q) (lt q)  0"
      unfolding lc_def by simp
  next
    fix u
    assume "lookup (p + q) u  0"
    show "u t lt q"
    proof (rule ccontr)
      assume "¬ u t lt q"
      hence qs: "lt q t u" by simp
      with assms have "lt p t u" by simp
      with lt_gr[of p u "lt p"] have "lookup p u = 0" by blast
      moreover from qs lt_gr[of q u "lt q"] have "lookup q u = 0" by blast
      ultimately show False using lookup (p + q) u  0 lookup_add[of p q u] by auto
    qed
  qed
qed

lemma lt_plus_eqI_2:
  assumes "lt q t lt p"
  shows "lt (p + q) = lt p"
proof (cases "p = 0")
  case True
  with assms have "lt q t min_term" by (simp add: lt_def)
  with min_term_min[of "lt q"] show ?thesis by simp
next
  case False
  show ?thesis
  proof (intro lt_eqI)
    from lt_gr[of q "lt p" "lt q"] assms have "lookup q (lt p) = 0" by blast
    with lookup_add[of p q "lt p"] lc_not_0[OF False] show "lookup (p + q) (lt p)  0"
      unfolding lc_def by simp
  next
    fix u
    assume "lookup (p + q) u  0"
    show "u t lt p"
    proof (rule ccontr)
      assume "¬ u t lt p"
      hence ps: "lt p t u" by simp
      with assms have "lt q t u" by simp
      with lt_gr[of q u "lt q"] have "lookup q u = 0" by blast
      also from ps lt_gr[of p u "lt p"] have "lookup p u = 0" by blast
      ultimately show False using lookup (p + q) u  0 lookup_add[of p q u] by auto
    qed
  qed
qed

lemma lt_plus_eqI_3:
  assumes "lt q = lt p" and "lc p + lc q  0"
  shows "lt (p + q) = lt (p::'t 0 'b::monoid_add)"
proof (rule lt_eqI)
  from assms(2) show "lookup (p + q) (lt p)  0" by (simp add: lookup_add lc_def assms(1))
next
  fix u
  assume "lookup (p + q) u  0"
  hence "lookup p u + lookup q u  0" by (simp add: lookup_add)
  hence "lookup p u  0  lookup q u  0" by auto
  thus "u t lt p"
  proof
    assume "lookup p u  0"
    thus ?thesis by (rule lt_max)
  next
    assume "lookup q u  0"
    hence "u t lt q" by (rule lt_max)
    thus ?thesis by (simp only: assms(1))
  qed
qed

lemma lt_plus_lessE:
  assumes "lt p t lt (p + q)"
  shows "lt p t lt q"
proof (rule ccontr)
  assume "¬ lt p t lt q"
  hence "lt p = lt q  lt q t lt p" by auto
  thus False
  proof
    assume lt_eq: "lt p = lt q"
    have "lt (p + q) t lt p"
    proof (rule lt_le)
      fix u
      assume "lt p t u"
      with lt_gr[of p u "lt p"] have "lookup p u = 0" by blast
      from lt p t u have "lt q t u" using lt_eq by simp
      with lt_gr[of q u "lt q"] have "lookup q u = 0" by blast
      with lookup p u = 0 show "lookup (p + q) u = 0" by (simp add: lookup_add)
    qed
    with assms show False by simp
  next
    assume "lt q t lt p"
    from lt_plus_eqI_2[OF this] assms show False by simp
  qed
qed

lemma lt_plus_lessE_2:
  assumes "lt q t lt (p + q)"
  shows "lt q t lt p"
proof (rule ccontr)
  assume "¬ lt q t lt p"
  hence "lt q = lt p  lt p t lt q" by auto
  thus False
  proof
    assume lt_eq: "lt q = lt p"
    have "lt (p + q) t lt q"
    proof (rule lt_le)
      fix u
      assume "lt q t u"
      with lt_gr[of q u "lt q"] have "lookup q u = 0" by blast
      from lt q t u have "lt p t u" using lt_eq by simp
      with lt_gr[of p u "lt p"] have "lookup p u = 0" by blast
      with lookup q u = 0 show "lookup (p + q) u = 0" by (simp add: lookup_add)
    qed
    with assms show False by simp
  next
    assume "lt p t lt q"
    from lt_plus_eqI[OF this] assms show False by simp
  qed
qed

lemma lt_plus_lessI':
  fixes p q :: "'t 0 'b::monoid_add"
  assumes "p + q  0" and lt_eq: "lt q = lt p" and lc_eq: "lc p + lc q = 0"
  shows "lt (p + q) t lt p"
proof (rule ccontr)
  assume "¬ lt (p + q) t lt p"
  hence "lt (p + q) = lt p  lt p t lt (p + q)" by auto
  thus False
  proof
    assume "lt (p + q) = lt p"
    have "lookup (p + q) (lt p) = (lookup p (lt p)) + (lookup q (lt q))" unfolding lt_eq lookup_add ..
    also have "... = lc p + lc q" unfolding lc_def ..
    also have "... = 0" unfolding lc_eq by simp
    finally have "lookup (p + q) (lt p) = 0" .
    hence "lt (p + q)  lt p" using lc_not_0[OF p + q  0] unfolding lc_def by auto
    with lt (p + q) = lt p show False by simp
  next
    assume "lt p t lt (p + q)"
    have "lt p t lt q" by (rule lt_plus_lessE, fact+)
    hence "lt p  lt q" by simp
    with lt_eq show False by simp
  qed
qed

corollary lt_plus_lessI:
  fixes p q :: "'t 0 'b::group_add"
  assumes "p + q  0" and "lt q = lt p" and "lc q = - lc p"
  shows "lt (p + q) t lt p"
  using assms(1, 2)
proof (rule lt_plus_lessI')
  from assms(3) show "lc p + lc q = 0" by simp
qed

lemma lt_plus_distinct_eq_max:
  assumes "lt p  lt q"
  shows "lt (p + q) = ord_term_lin.max (lt p) (lt q)"
proof (rule ord_term_lin.linorder_cases)
  assume a: "lt p t lt q"
  hence "lt (p + q) = lt q" by (rule lt_plus_eqI)
  also from a have "... = ord_term_lin.max (lt p) (lt q)"
    by (simp add: ord_term_lin.max.absorb2)
  finally show ?thesis .
next
  assume a: "lt q t lt p"
  hence "lt (p + q) = lt p" by (rule lt_plus_eqI_2)
  also from a have "... = ord_term_lin.max (lt p) (lt q)"
    by (simp add: ord_term_lin.max.absorb1)
  finally show ?thesis .
next
  assume "lt p = lt q"
  with assms show ?thesis ..
qed

lemma lt_plus_le_max: "lt (p + q) t ord_term_lin.max (lt p) (lt q)"
proof (cases "lt p = lt q")
  case True
  show ?thesis
  proof (rule lt_le)
    fix u
    assume "ord_term_lin.max (lt p) (lt q) t u"
    hence "lt p t u" and "lt q t u" by simp_all
    hence "lookup p u = 0" and "lookup q u = 0" using lt_max ord_term_lin.leD by blast+
    thus "lookup (p + q) u = 0" by (simp add: lookup_add)
  qed
next
  case False
  hence "lt (p + q) = ord_term_lin.max (lt p) (lt q)" by (rule lt_plus_distinct_eq_max)
  thus ?thesis by simp
qed

lemma lt_minus_eqI: "lt p t lt q  lt (p - q) = lt q" for p q :: "'t 0 'b::ab_group_add"
  by (metis lt_plus_eqI_2 lt_uminus uminus_add_conv_diff)

lemma lt_minus_eqI_2: "lt q t lt p  lt (p - q) = lt p" for p q :: "'t 0 'b::ab_group_add"
  by (metis lt_minus_eqI lt_uminus minus_diff_eq)

lemma lt_minus_eqI_3:
  assumes "lt q = lt p" and "lc q  lc p"
  shows "lt (p - q) = lt (p::'t 0 'b::ab_group_add)"
proof (rule lt_eqI)
  from assms(2) show "lookup (p - q) (lt p)  0" by (simp add: lookup_minus lc_def assms(1))
next
  fix u
  assume "lookup (p - q) u  0"
  hence "lookup p u  lookup q u" by (simp add: lookup_minus)
  hence "lookup p u  0  lookup q u  0" by auto
  thus "u t lt p"
  proof
    assume "lookup p u  0"
    thus ?thesis by (rule lt_max)
  next
    assume "lookup q u  0"
    hence "u t lt q" by (rule lt_max)
    thus ?thesis by (simp only: assms(1))
  qed
qed

lemma lt_minus_distinct_eq_max:
  assumes "lt p  lt (q::'t 0 'b::ab_group_add)"
  shows "lt (p - q) = ord_term_lin.max (lt p) (lt q)"
proof (rule ord_term_lin.linorder_cases)
  assume a: "lt p t lt q"
  hence "lt (p - q) = lt q" by (rule lt_minus_eqI)
  also from a have "... = ord_term_lin.max (lt p) (lt q)"
    by (simp add: ord_term_lin.max.absorb2)
  finally show ?thesis .
next
  assume a: "lt q t lt p"
  hence "lt (p - q) = lt p" by (rule lt_minus_eqI_2)
  also from a have "... = ord_term_lin.max (lt p) (lt q)"
    by (simp add: ord_term_lin.max.absorb1)
  finally show ?thesis .
next
  assume "lt p = lt q"
  with assms show ?thesis ..
qed

lemma lt_minus_lessE: "lt p t lt (p - q)  lt p t lt q" for p q :: "'t 0 'b::ab_group_add"
  using lt_minus_eqI_2 by fastforce

lemma lt_minus_lessE_2: "lt q t lt (p - q)  lt q t lt p" for p q :: "'t 0 'b::ab_group_add"
  using lt_plus_eqI_2 by fastforce

lemma lt_minus_lessI: "p - q  0  lt q = lt p  lc q = lc p  lt (p - q) t lt p"
  for p q :: "'t 0 'b::ab_group_add"
  by (metis (no_types, opaque_lifting) diff_diff_eq2 diff_self group_eq_aux lc_def lc_not_0 lookup_minus
      lt_minus_eqI ord_term_lin.antisym_conv3)
    
lemma lt_max_keys:
  assumes "v  keys p"
  shows "v t lt p"
proof (rule lt_max)
  from assms show "lookup p v  0" by (simp add: in_keys_iff)
qed

lemma lt_eqI_keys:
  assumes "v  keys p" and a2: "u. u  keys p  u t v"
  shows "lt p = v"
  by (rule lt_eqI, simp_all only: in_keys_iff[symmetric], fact+)
    
lemma lt_gr_keys:
  assumes "u  keys p" and "v t u"
  shows "v t lt p"
proof (rule lt_gr)
  from assms(1) show "lookup p u  0" by (simp add: in_keys_iff)
qed fact

lemma lt_plus_eq_maxI:
  assumes "lt p = lt q  lc p + lc q  0"
  shows "lt (p + q) = ord_term_lin.max (lt p) (lt q)"
proof (cases "lt p = lt q")
  case True
  show ?thesis
  proof (rule lt_eqI_keys)
    from True have "lc p + lc q  0" by (rule assms)
    thus "ord_term_lin.max (lt p) (lt q)  keys (p + q)"
      by (simp add: in_keys_iff lc_def lookup_add True)
  next
    fix u
    assume "u  keys (p + q)"
    hence "u t lt (p + q)" by (rule lt_max_keys)
    also have "... t ord_term_lin.max (lt p) (lt q)" by (fact lt_plus_le_max)
    finally show "u t ord_term_lin.max (lt p) (lt q)" .
  qed
next
  case False
  thus ?thesis by (rule lt_plus_distinct_eq_max)
qed

lemma lt_monom_mult:
  assumes "c  (0::'b::semiring_no_zero_divisors)" and "p  0"
  shows "lt (monom_mult c t p) = t  lt p"
proof (intro lt_eqI)
  from assms(1) show "lookup (monom_mult c t p) (t  lt p)  0"
  proof (simp add: lookup_monom_mult_plus)
    show "lookup p (lt p)  0"
      using assms(2) lt_in_keys by auto
  qed
next
  fix u::'t
  assume "lookup (monom_mult c t p) u  0"
  hence "u  keys (monom_mult c t p)" by (simp add: in_keys_iff)
  also have "...  (⊕) t ` keys p" by (fact keys_monom_mult_subset)
  finally obtain v where "v  keys p" and "u = t  v" ..
  show "u t t  lt p" unfolding u = t  v
  proof (rule splus_mono)
    from v  keys p show "v t lt p" by (rule lt_max_keys)
  qed
qed

lemma lt_monom_mult_zero:
  assumes "c  (0::'b::semiring_no_zero_divisors)"
  shows "lt (monom_mult c 0 p) = lt p"
proof (cases "p = 0")
  case True
  show ?thesis by (simp add: True)
next
  case False
  with assms show ?thesis by (simp add: lt_monom_mult term_simps)
qed

corollary lt_map_scale: "c  (0::'b::semiring_no_zero_divisors)  lt (c  p) = lt p"
  by (simp add: map_scale_eq_monom_mult lt_monom_mult_zero)

lemma lc_monom_mult [simp]: "lc (monom_mult c t p) = (c::'b::semiring_no_zero_divisors) * lc p"
proof (cases "c = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof (cases "p = 0")
    case True
    thus ?thesis by simp
  next
    case False
    with c  0 show ?thesis by (simp add: lc_def lt_monom_mult lookup_monom_mult_plus)
  qed
qed

corollary lc_map_scale [simp]: "lc (c  p) = (c::'b::semiring_no_zero_divisors) * lc p"
  by (simp add: map_scale_eq_monom_mult)

lemma (in ordered_term) lt_mult_scalar_monomial_right:
  assumes "c  (0::'b::semiring_no_zero_divisors)" and "p  0"
  shows "lt (p  monomial c v) = punit.lt p  v"
proof (intro lt_eqI)
  from assms(1) show "lookup (p  monomial c v) (punit.lt p  v)  0"
  proof (simp add: lookup_mult_scalar_monomial_right_plus)
    from assms(2) show "lookup p (punit.lt p)  0"
      using in_keys_iff punit.lt_in_keys by fastforce
  qed
next
  fix u::'t
  assume "lookup (p  monomial c v) u  0"
  hence "u  keys (p  monomial c v)" by (simp add: in_keys_iff)
  also have "...  (λt. t  v) ` keys p" by (fact keys_mult_scalar_monomial_right_subset)
  finally obtain t where "t  keys p" and "u = t  v" ..
  show "u t punit.lt p  v" unfolding u = t  v
  proof (rule splus_mono_left)
    from t  keys p show "t  punit.lt p" by (rule punit.lt_max_keys)
  qed
qed

lemma lc_mult_scalar_monomial_right:
  "lc (p  monomial c v) = punit.lc p * (c::'b::semiring_no_zero_divisors)"
proof (cases "c = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof (cases "p = 0")
    case True
    thus ?thesis by simp
  next
    case False
    with c  0 show ?thesis
      by (simp add: punit.lc_def lc_def lt_mult_scalar_monomial_right lookup_mult_scalar_monomial_right_plus)
  qed
qed

lemma lookup_monom_mult_eq_zero:
  assumes "s  lt p t v"
  shows "lookup (monom_mult (c::'b::semiring_no_zero_divisors) s p) v = 0"
  by (metis assms aux lt_gr lt_monom_mult monom_mult_zero_left monom_mult_zero_right
      ord_term_lin.order.strict_implies_not_eq)

lemma in_keys_monom_mult_le:
  assumes "v  keys (monom_mult c t p)"
  shows "v t t  lt p"
proof -
  from keys_monom_mult_subset assms have "v  (⊕) t ` (keys p)" ..
  then obtain u where "u  keys p" and "v = t  u" ..
  from u  keys p have "u t lt p" by (rule lt_max_keys)
  thus "v t t  lt p" unfolding v = t  u by (rule splus_mono)
qed

lemma lt_monom_mult_le: "lt (monom_mult c t p) t t  lt p"
  by (metis aux in_keys_monom_mult_le lt_in_keys lt_le_iff)

lemma monom_mult_inj_2:
  assumes "monom_mult c t1 p = monom_mult c t2 p"
    and "c  0" and "(p::'t 0 'b::semiring_no_zero_divisors)  0"
  shows "t1 = t2"
proof -
  from assms(1) have "lt (monom_mult c t1 p) = lt (monom_mult c t2 p)" by simp
  with c  0 p  0 have "t1  lt p = t2  lt p" by (simp add: lt_monom_mult)
  thus ?thesis by (simp add: term_simps)
qed

subsection ‹Trailing Term and Trailing Coefficient: @{const tt} and @{const tc}

lemma tt_zero [simp]: "tt 0 = min_term"
  by (simp add: tt_def)

lemma tc_zero [simp]: "tc 0 = 0"
  by (simp add: tc_def)

lemma tt_alt:
  assumes "p  0"
  shows "tt p = ord_term_lin.Min (keys p)"
  using assms unfolding tt_def by simp

lemma tt_min_keys:
  assumes "v  keys p"
  shows "tt p t v"
proof -
  from assms have "keys p  {}" by auto
  hence "p  0" by simp
  from tt_alt[OF this] ord_term_lin.Min_le[OF finite_keys assms] show ?thesis by simp
qed

lemma tt_min:
  assumes "lookup p v  0"
  shows "tt p t v"
proof -
  from assms have "v  keys p" unfolding keys_def by simp
  thus ?thesis by (rule tt_min_keys)
qed
  
lemma tt_in_keys:
  assumes "p  0"
  shows "tt p  keys p"
  unfolding tt_alt[OF assms]
  by (rule ord_term_lin.Min_in, fact finite_keys, simp add: assms)

lemma tt_eqI:
  assumes "v  keys p" and "u. u  keys p  v t u"
  shows "tt p = v"
proof -
  from assms(1) have "keys p  {}" by auto
  hence "p  0" by simp
  from assms(1) have "tt p t v" by (rule tt_min_keys)
  moreover have "v t tt p" by (rule assms(2), rule tt_in_keys, fact p  0)
  ultimately show ?thesis by simp
qed

lemma tt_gr:
  assumes "u. u  keys p  v t u" and "p  0"
  shows "v t tt p"
proof -
  from p  0 have "keys p  {}" by simp
  show ?thesis by (rule assms(1), rule tt_in_keys, fact p  0)
qed

lemma tt_less:
  assumes "u  keys p" and "u t v"
  shows "tt p t v"
proof -
  from u  keys p have "tt p t u" by (rule tt_min_keys)
  also have "... t v" by fact
  finally show "tt p t v" .
qed

lemma tt_ge:
  assumes "u. u t v  lookup p u = 0" and "p  0"
  shows "v t tt p"
proof -
  from p  0 have "keys p  {}" by simp
  have "ukeys p. v t u"
  proof
    fix u::'t
    assume "u  keys p"
    hence "lookup p u  0" unfolding keys_def by simp
    hence "¬ u t v" using assms(1)[of u] by auto
    thus "v t u" by simp
  qed
  with tt_alt[OF p  0] ord_term_lin.Min_ge_iff[OF finite_keys[of p] keys p  {}]
    show ?thesis by simp
qed
  
lemma tt_ge_keys:
  assumes "u. u  keys p  v t u" and "p  0"
  shows "v t tt p"
  by (rule assms(1), rule tt_in_keys, fact)

lemma tt_ge_iff: "v t tt p  ((p  0  v = min_term)  (u. u t v  lookup p u = 0))"
  (is "?L  (?A  ?B)")
proof
  assume ?L
  show "?A  ?B"
  proof (intro conjI allI impI)
    show "p  0  v = min_term"
    proof (cases "p = 0")
      case True
      show ?thesis
      proof (rule disjI2)
        from ?L True have "v t min_term" by (simp add: tt_def)
        with min_term_min[of v] show "v = min_term" by simp
      qed
    next
      case False
      thus ?thesis ..
    qed
  next
    fix u
    assume "u t v"
    also note v t tt p
    finally have "u t tt p" .
    hence "¬ tt p t u" by simp
    with tt_min[of p u] show "lookup p u = 0" by blast
  qed
next
  assume "?A  ?B"
  hence ?A and ?B by simp_all
  show ?L
  proof (cases "p = 0")
    case True
    with ?A have "v = min_term" by simp
    with True show ?thesis by (simp add: tt_def)
  next
    case False
    from ?B show ?thesis using tt_ge[OF _ False] by auto
  qed
qed

lemma tc_not_0:
  assumes "p  0"
  shows "tc p  0"
  unfolding tc_def in_keys_iff[symmetric] using assms by (rule tt_in_keys)

lemma tt_monomial:
  assumes "c  0"
  shows "tt (monomial c v) = v"
proof (rule tt_eqI)
  from keys_of_monomial[OF assms, of v] show "v  keys (monomial c v)" by simp
next
  fix u
  assume "u  keys (monomial c v)"
  with keys_of_monomial[OF assms, of v] have "u = v" by simp
  thus "v t u" by simp
qed

lemma tc_monomial [simp]: "tc (monomial c t) = c"
proof (cases "c = 0")
  case True
  thus ?thesis by simp
next
  case False
  thus ?thesis by (simp add: tc_def tt_monomial)
qed
  
lemma tt_plus_eqI:
  assumes "p  0" and "tt p t tt q"
  shows "tt (p + q) = tt p"
proof (intro tt_eqI)
  from tt_less[of "tt p" q "tt q"] tt p t tt q have "tt p  keys q" by blast
  with lookup_add[of p q "tt p"] tc_not_0[OF p  0] show "tt p  keys (p + q)"
    unfolding in_keys_iff tc_def by simp
next
  fix u
  assume "u  keys (p + q)"
  show "tt p t u"
  proof (rule ccontr)
    assume "¬ tt p t u"
    hence sp: "u t tt p" by simp
    hence "u t tt q" using tt p t tt q by simp
    with tt_less[of u q "tt q"] have "u  keys q" by blast
    moreover from sp tt_less[of u p "tt p"] have "u  keys p" by blast
    ultimately show False using u  keys (p + q) Poly_Mapping.keys_add[of p q] by auto
  qed
qed
    
lemma tt_plus_lessE:
  fixes p q
  assumes "p + q  0" and tt: "tt (p + q) t tt p"
  shows "tt q t tt p"
proof (cases "p = 0")
  case True
  with tt show ?thesis by simp
next
  case False
  show ?thesis
  proof (rule ccontr)
    assume "¬ tt q t tt p"
    hence "tt p = tt q  tt p t tt q" by auto
    thus False
    proof
      assume tt_eq: "tt p = tt q"
      have "tt p t tt (p + q)"
      proof (rule tt_ge_keys)
        fix u
        assume "u  keys (p + q)"
        hence "u  keys p  keys q"
        proof
          show "keys (p + q)  keys p  keys q" by (fact Poly_Mapping.keys_add)
        qed
        thus "tt p t u"
        proof
          assume "u  keys p"
          thus ?thesis by (rule tt_min_keys)
        next
          assume "u  keys q"
          thus ?thesis unfolding tt_eq by (rule tt_min_keys)
        qed
      qed (fact p + q  0)
      with tt show False by simp
    next
      assume "tt p t tt q"
      from tt_plus_eqI[OF False this] tt show False by (simp add: ac_simps)
    qed
  qed
qed
  
lemma tt_plus_lessI:
  fixes p q :: "_ 0 'b::ring"
  assumes "p + q  0" and tt_eq: "tt q = tt p" and tc_eq: "tc q = - tc p"
  shows "tt p t tt (p + q)"
proof (rule ccontr)
  assume "¬ tt p t tt (p + q)"
  hence "tt p = tt (p + q)  tt (p + q) t tt p" by auto
  thus False
  proof
    assume "tt p = tt (p + q)"
    have "lookup (p + q) (tt p) = (lookup p (tt p)) + (lookup q (tt q))" unfolding tt_eq lookup_add ..
    also have "... = tc p + tc q" unfolding tc_def ..
    also have "... = 0" unfolding tc_eq by simp
    finally have "lookup (p + q) (tt p) = 0" .
    hence "tt (p + q)  tt p" using tc_not_0[OF p + q  0] unfolding tc_def by auto
    with tt p = tt (p + q) show False by simp
  next
    assume "tt (p + q) t tt p"
    have "tt q t tt p" by (rule tt_plus_lessE, fact+)
    hence "tt q  tt p" by simp
    with tt_eq show False by simp
  qed
qed

lemma tt_uminus [simp]: "tt (- p) = tt p"
  by (simp add: tt_def keys_uminus)

lemma tc_uminus [simp]: "tc (- p) = - tc p"
  by (simp add: tc_def)

lemma tt_monom_mult:
  assumes "c  (0::'b::semiring_no_zero_divisors)" and "p  0"
  shows "tt (monom_mult c t p) = t  tt p"
proof (intro tt_eqI, rule keys_monom_multI, rule tt_in_keys, fact, fact)
  fix u
  assume "u  keys (monom_mult c t p)"
  then obtain v where "v  keys p" and u: "u = t  v" by (rule keys_monom_multE)
  show "t  tt p t u" unfolding u add.commute[of t] by (rule splus_mono, rule tt_min_keys, fact)
qed

lemma tt_map_scale: "c  (0::'b::semiring_no_zero_divisors)  tt (c  p) = tt p"
  by (cases "p = 0") (simp_all add: map_scale_eq_monom_mult tt_monom_mult term_simps)

lemma tc_monom_mult [simp]: "tc (monom_mult c t p) = (c::'b::semiring_no_zero_divisors) * tc p"
proof (cases "c = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof (cases "p = 0")
    case True
    thus ?thesis by simp
  next
    case False
    with c  0 show ?thesis by (simp add: tc_def tt_monom_mult lookup_monom_mult_plus)
  qed
qed

corollary tc_map_scale [simp]: "tc (c  p) = (c::'b::semiring_no_zero_divisors) * tc p"
  by (simp add: map_scale_eq_monom_mult)

lemma in_keys_monom_mult_ge:
  assumes "v  keys (monom_mult c t p)"
  shows "t  tt p t v"
proof -
  from keys_monom_mult_subset assms have "v  (⊕) t ` (keys p)" ..
  then obtain u where "u  keys p" and "v = t  u" ..
  from u  keys p have "tt p t u" by (rule tt_min_keys)
  thus "t  tt p t v" unfolding v = t  u by (rule splus_mono)
qed

lemma lt_ge_tt: "tt p t lt p"
proof (cases "p = 0")
  case True
  show ?thesis unfolding True lt_def tt_def by simp
next
  case False
  show ?thesis by (rule lt_max_keys, rule tt_in_keys, fact False)
qed

lemma lt_eq_tt_monomial:
  assumes "is_monomial p"
  shows "lt p = tt p"
proof -
  from assms obtain c v where "c  0" and p: "p = monomial c v" by (rule is_monomial_monomial)
  from c  0 have "lt p = v" and "tt p = v" unfolding p by (rule lt_monomial, rule tt_monomial)
  thus ?thesis by simp
qed

subsection @{const higher} and @{const lower}

lemma lookup_higher: "lookup (higher p u) v = (if u t v then lookup p v else 0)"
  by (auto simp add: higher_def lookup_except)

lemma lookup_higher_when: "lookup (higher p u) v = (lookup p v when u t v)"
  by (auto simp add: lookup_higher when_def)

lemma higher_plus: "higher (p + q) v = higher p v + higher q v"
  by (rule poly_mapping_eqI, simp add: lookup_add lookup_higher)

lemma higher_uminus [simp]: "higher (- p) v = -(higher p v)"
  by (rule poly_mapping_eqI, simp add: lookup_higher)

lemma higher_minus: "higher (p - q) v = higher p v - higher q v"
  by (auto intro!: poly_mapping_eqI simp: lookup_minus lookup_higher)

lemma higher_zero [simp]: "higher 0 t = 0"
  by (rule poly_mapping_eqI, simp add: lookup_higher)

lemma higher_eq_iff: "higher p v = higher q v  (u. v t u  lookup p u = lookup q u)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (intro allI impI)
    fix u
    assume "v t u"
    moreover from ?L have "lookup (higher p v) u = lookup (higher q v) u" by simp
    ultimately show "lookup p u = lookup q u" by (simp add: lookup_higher)
  qed
next
  assume ?R
  show ?L
  proof (rule poly_mapping_eqI, simp add: lookup_higher, rule)
    fix u
    assume "v t u"
    with ?R show "lookup p u = lookup q u" by simp
  qed
qed

lemma higher_eq_zero_iff: "higher p v = 0  (u. v t u  lookup p u = 0)"
proof -
  have "higher p v = higher 0 v  (u. v t u  lookup p u = lookup 0 u)" by (rule higher_eq_iff)
  thus ?thesis by simp
qed

lemma keys_higher: "keys (higher p v) = {ukeys p. v t u}"
  by (rule set_eqI, simp only: in_keys_iff, simp add: lookup_higher)

lemma higher_higher: "higher (higher p u) v = higher p (ord_term_lin.max u v)"
  by (rule poly_mapping_eqI, simp add: lookup_higher)

lemma lookup_lower: "lookup (lower p u) v = (if v t u then lookup p v else 0)"
  by (auto simp add: lower_def lookup_except)

lemma lookup_lower_when: "lookup (lower p u) v = (lookup p v when v t u)"
  by (auto simp add: lookup_lower when_def)

lemma lower_plus: "lower (p + q) v = lower p v + lower q v"
  by (rule poly_mapping_eqI, simp add: lookup_add lookup_lower)

lemma lower_uminus [simp]: "lower (- p) v = - lower p v"
  by (rule poly_mapping_eqI, simp add: lookup_lower)

lemma lower_minus:  "lower (p - (q::_ 0 'b::ab_group_add)) v = lower p v - lower q v"
   by (auto intro!: poly_mapping_eqI simp: lookup_minus lookup_lower)

lemma lower_zero [simp]: "lower 0 v = 0"
  by (rule poly_mapping_eqI, simp add: lookup_lower)

lemma lower_eq_iff: "lower p v = lower q v  (u. u t v  lookup p u = lookup q u)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (intro allI impI)
    fix u
    assume "u t v"
    moreover from ?L have "lookup (lower p v) u = lookup (lower q v) u" by simp
    ultimately show "lookup p u = lookup q u" by (simp add: lookup_lower)
  qed
next
  assume ?R
  show ?L
  proof (rule poly_mapping_eqI, simp add: lookup_lower, rule)
    fix u
    assume "u t v"
    with ?R show "lookup p u = lookup q u" by simp
  qed
qed

lemma lower_eq_zero_iff: "lower p v = 0  (u. u t v  lookup p u = 0)"
proof -
  have "lower p v = lower 0 v  (u. u t v  lookup p u = lookup 0 u)" by (rule lower_eq_iff)
  thus ?thesis by simp
qed

lemma keys_lower: "keys (lower p v) = {ukeys p. u t v}"
  by (rule set_eqI, simp only: in_keys_iff, simp add: lookup_lower)

lemma lower_lower: "lower (lower p u) v = lower p (ord_term_lin.min u v)"
  by (rule poly_mapping_eqI, simp add: lookup_lower)

lemma lt_higher:
  assumes "v t lt p"
  shows "lt (higher p v) = lt p"
proof (rule lt_eqI_keys, simp_all add: keys_higher, rule conjI, rule lt_in_keys, rule)
  assume "p = 0"
  hence "lt p = min_term" by (simp add: lt_def)
  with min_term_min[of v] assms show False by simp
next
  fix u
  assume "u  keys p  v t u"
  hence "u  keys p" ..
  thus "u t lt p" by (rule lt_max_keys)
qed fact

lemma lc_higher:
  assumes "v t lt p"
  shows "lc (higher p v) = lc p"
  by (simp add: lc_def lt_higher assms lookup_higher)

lemma higher_eq_zero_iff': "higher p v = 0  lt p t v"
  by (simp add: higher_eq_zero_iff lt_le_iff)

lemma higher_id_iff: "higher p v = p  (p = 0  v t tt p)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (cases "p = 0")
    case True
    thus ?thesis ..
  next
    case False
    show ?thesis
    proof (rule disjI2, rule tt_gr)
      fix u
      assume "u  keys p"
      hence "lookup p u  0" by (simp add: in_keys_iff)
      from ?L have "lookup (higher p v) u = lookup p u" by simp
      hence "lookup p u = (if v t u then lookup p u else 0)" by (simp only: lookup_higher)
      hence "¬ v t u  lookup p u = 0" by simp
      with lookup p u  0 show "v t u" by auto
    qed fact
  qed
next
  assume ?R
  show ?L
  proof (cases "p = 0")
    case True
    thus ?thesis by simp
  next
    case False
    with ?R have "v t tt p" by simp
    show ?thesis
    proof (rule poly_mapping_eqI, simp add: lookup_higher, intro impI)
      fix u
      assume "¬ v t u"
      hence "u t v" by simp
      from this v t tt p have "u t tt p" by simp
      hence "¬ tt p t u" by simp
      with tt_min[of p u] show "lookup p u = 0" by blast
    qed
  qed
qed

lemma tt_lower:
  assumes "tt p t v"
  shows "tt (lower p v) = tt p"
proof (cases "p = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof (rule tt_eqI, simp_all add: keys_lower, rule, rule tt_in_keys)
    fix u
    assume "u  keys p  u t v"
    hence "u  keys p" ..
    thus "tt p t u" by (rule tt_min_keys)
  qed fact+
qed

lemma tc_lower:
  assumes "tt p t v"
  shows "tc (lower p v) = tc p"
  by (simp add: tc_def tt_lower assms lookup_lower)

lemma lt_lower: "lt (lower p v) t lt p"
proof (cases "lower p v = 0")
  case True
  thus ?thesis by (simp add: lt_def min_term_min)
next
  case False
  show ?thesis
  proof (rule lt_le, simp add: lookup_lower, rule impI, rule ccontr)
    fix u
    assume "lookup p u  0"
    hence "u t lt p" by (rule lt_max)
    moreover assume "lt p t u"
    ultimately show False by simp
  qed
qed

lemma lt_lower_less:
  assumes "lower p v  0"
  shows "lt (lower p v) t v"
  using assms
proof (rule lt_less)
  fix u
  assume "v t u"
  thus "lookup (lower p v) u = 0" by (simp add: lookup_lower_when)
qed

lemma lt_lower_eq_iff: "lt (lower p v) = lt p  (lt p = min_term  lt p t v)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (rule ccontr, simp, elim conjE)
    assume "lt p  min_term"
    hence "min_term t lt p" using min_term_min ord_term_lin.dual_order.not_eq_order_implies_strict
      by blast
    assume "¬ lt p t v"
    hence "v t lt p" by simp
    have "lt (lower p v) t lt p"
    proof (cases "lower p v = 0")
      case True
      thus ?thesis using min_term t lt p by (simp add: lt_def)
    next
      case False
      show ?thesis
      proof (rule lt_less)
        fix u
        assume "lt p t u"
        with v t lt p have "¬ u t v" by simp
        thus "lookup (lower p v) u = 0" by (simp add: lookup_lower)
      qed fact
    qed
    with ?L show False by simp
  qed
next
  assume ?R
  show ?L
  proof (cases "lt p = min_term")
    case True
    hence "lt p t lt (lower p v)" by (simp add: min_term_min)
    with lt_lower[of p v] show ?thesis by simp
  next
    case False
    with ?R have "lt p t v" by simp
    show ?thesis
    proof (rule lt_eqI_keys, simp_all add: keys_lower, rule conjI, rule lt_in_keys, rule)
      assume "p = 0"
      hence "lt p = min_term" by (simp add: lt_def)
      with False show False ..
    next
      fix u
      assume "u  keys p  u t v"
      hence "u  keys p" ..
      thus "u t lt p" by (rule lt_max_keys)
    qed fact
  qed
qed

lemma tt_higher:
  assumes "v t lt p"
  shows "tt p t tt (higher p v)"
proof (rule tt_ge_keys, simp add: keys_higher)
  fix u
  assume "u  keys p  v t u"
  hence "u  keys p" ..
  thus "tt p t u" by (rule tt_min_keys)
next
  show "higher p v  0"
  proof (simp add: higher_eq_zero_iff, intro exI conjI)
    have "p  0"
    proof
      assume "p = 0"
      hence "lt p t v" by (simp add: lt_def min_term_min)
      with assms show False by simp
    qed
    thus "lookup p (lt p)  0"
      using lt_in_keys by auto 
  qed fact
qed

lemma tt_higher_eq_iff:
  "tt (higher p v) = tt p  ((lt p t v  tt p = min_term)  v t tt p)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (rule ccontr, simp, elim conjE)
    assume a: "lt p t v  tt p  min_term"
    assume "¬ v t tt p"
    hence "tt p t v" by simp
    have "tt p t tt (higher p v)"
    proof (cases "higher p v = 0")
      case True
      with ?L have "tt p = min_term" by (simp add: tt_def)
      with a have "v t lt p" by auto
      have "lt p  min_term"
      proof
        assume "lt p = min_term"
        with v t lt p show False using min_term_min[of v] by auto
      qed
      hence "p  0" by (auto simp add: lt_def)
      from v t lt p have "higher p v  0" by (simp add: higher_eq_zero_iff')
      from this True show ?thesis ..
    next
      case False
      show ?thesis
      proof (rule tt_gr)
        fix u
        assume "u  keys (higher p v)"
        hence "v t u" by (simp add: keys_higher)
        with tt p t v show "tt p t u" by simp
      qed fact
    qed
    with ?L show False by simp
  qed
next
  assume ?R
  show ?L
  proof (cases "lt p t v  tt p = min_term")
    case True
    hence "lt p t v" and "tt p = min_term" by simp_all
    from lt p t v have "higher p v = 0" by (simp add: higher_eq_zero_iff')
    with tt p = min_term show ?thesis by (simp add: tt_def)
  next
    case False
    with ?R have "v t tt p" by simp
    show ?thesis
    proof (rule tt_eqI, simp_all add: keys_higher, rule conjI, rule tt_in_keys, rule)
      assume "p = 0"
      hence "tt p = min_term" by (simp add: tt_def)
      with v t tt p min_term_min[of v] show False by simp
    next
      fix u
      assume "u  keys p  v t u"
      hence "u  keys p" ..
      thus "tt p t u" by (rule tt_min_keys)
    qed fact
  qed
qed

lemma lower_eq_zero_iff': "lower p v = 0  (p = 0  v t tt p)"
  by (auto simp add: lower_eq_zero_iff tt_ge_iff)

lemma lower_id_iff: "lower p v = p  (p = 0  lt p t v)" (is "?L  ?R")
proof
  assume ?L
  show ?R
  proof (cases "p = 0")
    case True
    thus ?thesis ..
  next
    case False
    show ?thesis
    proof (rule disjI2, rule lt_less)
      fix u
      assume "v t u"
      from ?L have "lookup (lower p v) u = lookup p u" by simp
      hence "lookup p u = (if u t v then lookup p u else 0)" by (simp only: lookup_lower)
      hence "v t u  lookup p u = 0" by (meson ord_term_lin.leD)
      with v t u show "lookup p u = 0" by simp
    qed fact
  qed
next
  assume ?R
  show ?L
  proof (cases "p = 0", simp)
    case False
    with ?R have "lt p t v" by simp
    show ?thesis
    proof (rule poly_mapping_eqI, simp add: lookup_lower, intro impI)
      fix u
      assume "¬ u t v"
      hence "v t u" by simp
      with lt p t v have "lt p t u" by simp
      hence "¬ u t lt p" by simp
      with lt_max[of p u] show "lookup p u = 0" by blast
    qed
  qed
qed
    
lemma lower_higher_commute: "higher (lower p s) t = lower (higher p t) s"
  by (rule poly_mapping_eqI, simp add: lookup_higher lookup_lower)

lemma lt_lower_higher:
  assumes "v t lt (lower p u)"
  shows "lt (lower (higher p v) u) = lt (lower p u)"
  by (simp add: lower_higher_commute[symmetric] lt_higher[OF assms])

lemma lc_lower_higher:
  assumes "v t lt (lower p u)"
  shows "lc (lower (higher p v) u) = lc (lower p u)"
  using assms by (simp add: lc_def lt_lower_higher lookup_lower lookup_higher)

lemma trailing_monomial_higher:
  assumes "p  0"
  shows "p = (higher p (tt p)) + monomial (tc p) (tt p)"
proof (rule poly_mapping_eqI, simp only: lookup_add)
  fix v
  show "lookup p v = lookup (higher p (tt p)) v + lookup (monomial (tc p) (tt p)) v"
  proof (cases "tt p t v")
    case True
    show ?thesis
    proof (cases "v = tt p")
      assume "v = tt p"
      hence "¬ tt p t v" by simp
      hence "lookup (higher p (tt p)) v = 0" by (simp add: lookup_higher)
      moreover from v = tt p have "lookup (monomial (tc p) (tt p)) v = tc p" by (simp add: lookup_single)
      moreover from v = tt p have "lookup p v = tc p" by (simp add: tc_def)
      ultimately show ?thesis by simp
    next
      assume "v  tt p"
      from this True have "tt p t v" by simp
      hence "lookup (higher p (tt p)) v = lookup p v" by (simp add: lookup_higher)
      moreover from v  tt p have "lookup (monomial (tc p) (tt p)) v = 0" by (simp add: lookup_single)
      ultimately show ?thesis by simp
    qed
  next
    case False
    hence "v t tt p" by simp
    hence "tt p  v" by simp
    from False have "¬ tt p t v" by simp
    have "lookup p v = 0"
    proof (rule ccontr)
      assume "lookup p v  0"
      from tt_min[OF this] False show False by simp
    qed
    moreover from tt p  v have "lookup (monomial (tc p) (tt p)) v = 0" by (simp add: lookup_single)
    moreover from ¬ tt p t v have "lookup (higher p (tt p)) v = 0" by (simp add: lookup_higher)
    ultimately show ?thesis by simp
  qed
qed

lemma higher_lower_decomp: "higher p v + monomial (lookup p v) v + lower p v = p"
proof (rule poly_mapping_eqI)
  fix u
  show "lookup (higher p v + monomial (lookup p v) v + lower p v) u = lookup p u"
  proof (rule ord_term_lin.linorder_cases)
    assume "u t v"
    thus ?thesis by (simp add: lookup_add lookup_higher_when lookup_single lookup_lower_when)
  next
    assume "u = v"
    thus ?thesis by (simp add: lookup_add lookup_higher_when lookup_single lookup_lower_when)
  next
    assume "v t u"
    thus ?thesis by (simp add: lookup_add lookup_higher_when lookup_single lookup_lower_when)
  qed
qed

subsection @{const tail}

lemma lookup_tail: "lookup (tail p) v = (if v t lt p then lookup p v else 0)"
  by (simp add: lookup_lower tail_def)

lemma lookup_tail_when: "lookup (tail p) v = (lookup p v when v t lt p)"
  by (simp add: lookup_lower_when tail_def)

lemma lookup_tail_2: "lookup (tail p) v = (if v = lt p then 0 else lookup p v)"
proof (rule ord_term_lin.linorder_cases[of v "lt p"])
  assume "v t lt p"
  hence "v  lt p" by simp
  from this v t lt p lookup_tail[of p v] show ?thesis by simp
next
  assume "v = lt p"
  hence "¬ v t lt p" by simp
  from v = lt p this lookup_tail[of p v] show ?thesis by simp
next
  assume "lt p t v"
  hence "¬ v t lt p" by simp
  hence cp: "lookup p v = 0"
    using lt_max by blast
  from ¬ v t lt p have "¬ v = lt p" and "¬ v t lt p" by simp_all
  thus ?thesis using cp lookup_tail[of p v] by simp
qed

lemma leading_monomial_tail: "p = monomial (lc p) (lt p) + tail p" for p::"_ 0 'b::comm_monoid_add"
proof (rule poly_mapping_eqI)
  fix v
  have "lookup p v = lookup (monomial (lc p) (lt p)) v + lookup (tail p) v"
  proof (cases "v t lt p")
    case True
    show ?thesis
    proof (cases "v = lt p")
      assume "v = lt p"
      hence "¬ v t lt p" by simp
      hence c3: "lookup (tail p) v = 0" unfolding lookup_tail[of p v] by simp
      from v = lt p have c2: "lookup (monomial (lc p) (lt p)) v = lc p" by simp
      from v = lt p have c1: "lookup p v = lc p" by (simp add: lc_def)
      from c1 c2 c3 show ?thesis by simp
    next
      assume "v  lt p"
      from this True have "v t lt p" by simp
      hence c2: "lookup (tail p) v = lookup p v" unfolding lookup_tail[of p v] by simp
      from v  lt p have c1: "lookup (monomial (lc p) (lt p)) v = 0" by (simp add: lookup_single)
      from c1 c2 show ?thesis by simp
    qed
  next
    case False
    hence "lt p t v" by simp
    hence "lt p  v" by simp
    from False have "¬ v t lt p" by simp
    have c1: "lookup p v = 0"
    proof (rule ccontr)
      assume "lookup p v  0"
      from lt_max[OF this] False show False by simp
    qed
    from lt p  v have c2: "lookup (monomial (lc p) (lt p)) v = 0" by (simp add: lookup_single)
    from ¬ v t lt p lookup_tail[of p v] have c3: "lookup (tail p) v = 0" by simp
    from c1 c2 c3 show ?thesis by simp
  qed
  thus "lookup p v = lookup (monomial (lc p) (lt p) + tail p) v" by (simp add: lookup_add)
qed

lemma tail_alt: "tail p = except p {lt p}"
  by (rule poly_mapping_eqI, simp add: lookup_tail_2 lookup_except)

corollary tail_alt_2: "tail p = p - monomial (lc p) (lt p)"
proof -
  have "p = monomial (lc p) (lt p) + tail p" by (fact leading_monomial_tail)
  also have "... = tail p + monomial (lc p) (lt p)" by (simp only: add.commute)
  finally have "p - monomial (lc p) (lt p) = (tail p + monomial (lc p) (lt p)) - monomial (lc p) (lt p)" by simp
  thus ?thesis by simp
qed

lemma tail_zero [simp]: "tail 0 = 0"
  by (simp only: tail_alt except_zero)

lemma lt_tail:
  assumes "tail p  0"
  shows "lt (tail p) t lt p"
proof (intro lt_less)
  fix u
  assume "lt p t u"
  hence "¬ u t lt p" by simp
  thus "lookup (tail p) u = 0" unfolding lookup_tail[of p u] by simp
qed fact

lemma keys_tail: "keys (tail p) = keys p - {lt p}"
  by (simp add: tail_alt keys_except)

lemma tail_monomial: "tail (monomial c v) = 0"
  by (metis (no_types, lifting) lookup_tail_2 lookup_single_not_eq lt_less lt_monomial
      ord_term_lin.dual_order.strict_implies_not_eq single_zero tail_zero)

lemma (in ordered_term) mult_scalar_tail_rec_left:
  "p  q = monom_mult (punit.lc p) (punit.lt p) q + (punit.tail p)  q"
  unfolding punit.lc_def punit.tail_alt by (fact mult_scalar_rec_left)

lemma mult_scalar_tail_rec_right: "p  q = p  monomial (lc q) (lt q) + p  tail q"
  unfolding tail_alt lc_def by (rule mult_scalar_rec_right)

lemma lt_tail_max:
  assumes