# 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

assumes "u adds⇩t 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"
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 "∀u∈keys 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 "∀u∈keys 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 "∀u∈keys 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) = {u∈keys 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) = {u∈keys 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 "tail p ≠ 0" and "v ```