Theory MPoly_Type_Class_Ordered
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 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"
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 "∀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 ∈ keys p" and "v ≺⇩t lt p"
shows "v ≼⇩t lt (tail p)"
proof (rule lt_max_keys, simp add: keys_tail assms(2))
from assms(3) show "v ≠ lt p" by auto
qed
lemma keys_tail_less_lt:
assumes "v ∈ keys (tail p)"
shows "v ≺⇩t lt p"
using assms by (meson in_keys_iff lookup_tail)
lemma tt_tail:
assumes "tail p ≠ 0"
shows "tt (tail p) = tt p"
proof (rule tt_eqI, simp_all add: keys_tail)
from assms have "p ≠ 0" using tail_zero by auto
show "tt p ∈ keys p ∧ tt p ≠ lt p"
proof (rule conjI, rule tt_in_keys, fact)
have "tt p ≺⇩t lt p"
by (metis assms lower_eq_zero_iff' tail_def ord_term_lin.le_less_linear)
thus "tt p ≠ lt p" by simp
qed
next
fix u
assume "u ∈ keys p ∧ u ≠ lt p"
hence "u ∈ keys p" ..
thus "tt p ≼⇩t u" by (rule tt_min_keys)
qed
lemma tc_tail:
assumes "tail p ≠ 0"
shows "tc (tail p) = tc p"
proof (simp add: tc_def tt_tail[OF assms] lookup_tail_2, rule)
assume "tt p = lt p"
moreover have "tt p ≺⇩t lt p"
by (metis assms lower_eq_zero_iff' tail_def ord_term_lin.le_less_linear)
ultimately show "lookup p (lt p) = 0" by simp
qed
lemma tt_tail_min:
assumes "s ∈ keys p"
shows "tt (tail p) ≼⇩t s"
proof (cases "tail p = 0")
case True
hence "tt (tail p) = min_term" by (simp add: tt_def)
thus ?thesis by (simp add: min_term_min)
next
case False
from assms show ?thesis by (simp add: tt_tail[OF False], rule tt_min_keys)
qed
lemma tail_monom_mult:
"tail (monom_mult c t p) = monom_mult (c::'b::semiring_no_zero_divisors) t (tail p)"
proof (cases "p = 0")
case True
hence "tail p = 0" and "monom_mult c t p = 0" by simp_all
thus ?thesis by simp
next
case False
show ?thesis
proof (cases "c = 0")
case True
hence "monom_mult c t p = 0" and "monom_mult c t (tail p) = 0" by simp_all
thus ?thesis by simp
next
case False
let ?a = "monom_mult c t p"
let ?b = "monom_mult c t (tail p)"
from ‹p ≠ 0› False have "?a ≠ 0" by (simp add: monom_mult_eq_zero_iff)
from False ‹p ≠ 0› have lt_a: "lt ?a = t ⊕ lt p" by (rule lt_monom_mult)
show ?thesis
proof (rule poly_mapping_eqI, simp add: lookup_tail lt_a, intro conjI impI)
fix u
assume "u ≺⇩t t ⊕ lt p"
show "lookup (monom_mult c t p) u = lookup (monom_mult c t (tail p)) u"
proof (cases "t adds⇩p u")
case True
then obtain v where "u = t ⊕ v" by (rule adds_ppE)
from ‹u ≺⇩t t ⊕ lt p› have "v ≺⇩t lt p" unfolding ‹u = t ⊕ v› by (rule ord_term_strict_canc)
hence "lookup p v = lookup (tail p) v" by (simp add: lookup_tail)
thus ?thesis by (simp add: ‹u = t ⊕ v› lookup_monom_mult_plus)
next
case False
hence "lookup ?a u = 0" by (simp add: lookup_monom_mult)
moreover have "lookup ?b u = 0"
proof (rule ccontr, simp only: in_keys_iff[symmetric] keys_monom_mult[OF ‹c ≠ 0›])
assume "u ∈ (⊕) t ` keys (tail p)"
then obtain v where "u = t ⊕ v" by auto
hence "t adds⇩p u" by (simp add: term_simps)
with False show False ..
qed
ultimately show ?thesis by simp
qed
next
fix u
assume "¬ u ≺⇩t t ⊕ lt p"
hence "t ⊕ lt p ≼⇩t u" by simp
show "lookup (monom_mult c t (tail p)) u = 0"
proof (rule ccontr, simp only: in_keys_iff[symmetric] keys_monom_mult[OF False])
assume "u ∈ (⊕) t ` keys (tail p)"
then obtain v where "v ∈ keys (tail p)" and "u = t ⊕ v" by auto
from ‹t ⊕ lt p ≼⇩t u› have "lt p ≼⇩t v" unfolding ‹u = t ⊕ v› by (rule ord_term_canc)
from ‹v ∈ keys (tail p)› have "v ∈ keys p" and "v ≠ lt p" by (simp_all add: keys_tail)
from ‹v ∈ keys p› have "v ≼⇩t lt p" by (rule lt_max_keys)
with ‹lt p ≼⇩t v› have "v = lt p " by simp
with ‹v ≠ lt p› show False ..
qed
qed
qed
qed
lemma keys_plus_eq_lt_tt_D:
assumes "keys (p + q) = {lt p, tt q}" and "lt q ≺⇩t lt p" and "tt q ≺⇩t tt (p::_ ⇒⇩0 'b::comm_monoid_add)"
shows "tail p + higher q (tt q) = 0"
proof -
note assms(3)
also have "... ≼⇩t lt p" by (rule lt_ge_tt)
finally have "tt q ≺⇩t lt p" .
hence "lt p ≠ tt q" by simp
have "q ≠ 0"
proof
assume "q = 0"
hence "tt q = min_term" by (simp add: tt_def)
with ‹q = 0› assms(1) have "keys p = {lt p, min_term}" by simp
hence "min_term ∈ keys p" by simp
hence "tt p ≼⇩t tt q" unfolding ‹tt q = min_term› by (rule tt_min_keys)
with assms(3) show False by simp
qed
hence "tc q ≠ 0" by (rule tc_not_0)
have "p = monomial (lc p) (lt p) + tail p" by (rule leading_monomial_tail)
moreover from ‹q ≠ 0› have "q = higher q (tt q) + monomial (tc q) (tt q)" by (rule trailing_monomial_higher)
ultimately have pq: "p + q = (monomial (lc p) (lt p) + monomial (tc q) (tt q)) + (tail p + higher q (tt q))"
(is "_ = (?m1 + ?m2) + ?b") by (simp add: algebra_simps)
have keys_m1: "keys ?m1 = {lt p}"
proof (rule keys_of_monomial, rule lc_not_0, rule)
assume "p = 0"
with assms(2) have "lt q ≺⇩t min_term" by (simp add: lt_def)
with min_term_min[of "lt q"] show False by simp
qed
moreover from ‹tc q ≠ 0› have keys_m2: "keys ?m2 = {tt q}" by (rule keys_of_monomial)
ultimately have keys_m1_m2: "keys (?m1 + ?m2) = {lt p, tt q}"
using ‹lt p ≠ tt q› keys_plus_eqI[of ?m1 ?m2] by auto
show ?thesis
proof (rule ccontr)
assume "?b ≠ 0"
hence "keys ?b ≠ {}" by simp
then obtain t where "t ∈ keys ?b" by blast
hence t_in: "t ∈ keys (tail p) ∪ keys (higher q (tt q))"
using Poly_Mapping.keys_add[of "tail p" "higher q (tt q)"] by blast
hence "t ≠ lt p"
proof (rule, simp add: keys_tail, simp add: keys_higher, elim conjE)
assume "t ∈ keys q"
hence "t ≼⇩t lt q" by (rule lt_max_keys)
from this assms(2) show ?thesis by simp
qed
moreover from t_in have "t ≠ tt q"
proof (rule, simp add: keys_tail, elim conjE)
assume "t ∈ keys p"
hence "tt p ≼⇩t t" by (rule tt_min_keys)
with assms(3) show ?thesis by simp
next
assume "t ∈ keys (higher q (tt q))"
thus ?thesis by (auto simp only: keys_higher)
qed
ultimately have "t ∉ keys (?m1 + ?m2)" by (simp add: keys_m1_m2)
moreover from in_keys_plusI2[OF ‹t ∈ keys ?b› this] have "t ∈ keys (?m1 + ?m2)"
by (simp only: keys_m1_m2 pq[symmetric] assms(1))
ultimately show False ..
qed
qed
subsection ‹Order Relation on Polynomials›
definition ord_strict_p :: "('t ⇒⇩0 'b::zero) ⇒ ('t ⇒⇩0 'b) ⇒ bool" (infixl "≺⇩p" 50) where
"p ≺⇩p q ⟷ (∃v. lookup p v = 0 ∧ lookup q v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup p u = lookup q u))"
definition ord_p :: "('t ⇒⇩0 'b::zero) ⇒ ('t ⇒⇩0 'b) ⇒ bool" (infixl "≼⇩p" 50) where
"ord_p p q ≡ (p ≺⇩p q ∨ p = q)"
lemma ord_strict_pI:
assumes "lookup p v = 0" and "lookup q v ≠ 0" and "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u"
shows "p ≺⇩p q"
unfolding ord_strict_p_def using assms by blast
lemma ord_strict_pE:
assumes "p ≺⇩p q"
obtains v where "lookup p v = 0" and "lookup q v ≠ 0" and "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u"
using assms unfolding ord_strict_p_def by blast
lemma not_ord_pI:
assumes "lookup p v ≠ lookup q v" and "lookup p v ≠ 0" and "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u"
shows "¬ p ≼⇩p q"
proof
assume "p ≼⇩p q"
hence "p ≺⇩p q ∨ p = q" by (simp only: ord_p_def)
thus False
proof
assume "p ≺⇩p q"
then obtain v' where 1: "lookup p v' = 0" and 2: "lookup q v' ≠ 0"
and 3: "⋀u. v' ≺⇩t u ⟹ lookup p u = lookup q u" by (rule ord_strict_pE, blast)
from 1 2 have "lookup p v' ≠ lookup q v'" by simp
hence "¬ v ≺⇩t v'" using assms(3) by blast
hence "v' ≺⇩t v ∨ v' = v" by auto
thus ?thesis
proof
assume "v' ≺⇩t v"
hence "lookup p v = lookup q v" by (rule 3)
with assms(1) show ?thesis ..
next
assume "v' = v"
with assms(2) 1 show ?thesis by auto
qed
next
assume "p = q"
hence "lookup p v = lookup q v" by simp
with assms(1) show ?thesis ..
qed
qed
corollary not_ord_strict_pI:
assumes "lookup p v ≠ lookup q v" and "lookup p v ≠ 0" and "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u"
shows "¬ p ≺⇩p q"
proof -
from assms have "¬ p ≼⇩p q" by (rule not_ord_pI)
thus ?thesis by (simp add: ord_p_def)
qed
lemma ord_strict_higher: "p ≺⇩p q ⟷ (∃v. lookup p v = 0 ∧ lookup q v ≠ 0 ∧ higher p v = higher q v)"
unfolding ord_strict_p_def higher_eq_iff ..
lemma ord_strict_p_asymmetric:
assumes "p ≺⇩p q"
shows "¬ q ≺⇩p p"
using assms unfolding ord_strict_p_def
proof
fix v1::'t
assume "lookup p v1 = 0 ∧ lookup q v1 ≠ 0 ∧ (∀u. v1 ≺⇩t u ⟶ lookup p u = lookup q u)"
hence "lookup p v1 = 0" and "lookup q v1 ≠ 0" and v1: "∀u. v1 ≺⇩t u ⟶ lookup p u = lookup q u"
by auto
show "¬ (∃v. lookup q v = 0 ∧ lookup p v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup q u = lookup p u))"
proof (intro notI, erule exE)
fix v2::'t
assume "lookup q v2 = 0 ∧ lookup p v2 ≠ 0 ∧ (∀u. v2 ≺⇩t u ⟶ lookup q u = lookup p u)"
hence "lookup q v2 = 0" and "lookup p v2 ≠ 0" and v2: "∀u. v2 ≺⇩t u ⟶ lookup q u = lookup p u"
by auto
show False
proof (rule ord_term_lin.linorder_cases)
assume "v1 ≺⇩t v2"
from v1[rule_format, OF this] ‹lookup q v2 = 0› ‹lookup p v2 ≠ 0› show ?thesis by simp
next
assume "v1 = v2"
thus ?thesis using ‹lookup p v1 = 0› ‹lookup p v2 ≠ 0› by simp
next
assume "v2 ≺⇩t v1"
from v2[rule_format, OF this] ‹lookup p v1 = 0› ‹lookup q v1 ≠ 0› show ?thesis by simp
qed
qed
qed
lemma ord_strict_p_irreflexive: "¬ p ≺⇩p p"
unfolding ord_strict_p_def
proof (intro notI, erule exE)
fix v::'t
assume "lookup p v = 0 ∧ lookup p v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup p u = lookup p u)"
hence "lookup p v = 0" and "lookup p v ≠ 0" by auto
thus False by simp
qed
lemma ord_strict_p_transitive:
assumes "a ≺⇩p b" and "b ≺⇩p c"
shows "a ≺⇩p c"
proof -
from ‹a ≺⇩p b› obtain v1 where "lookup a v1 = 0"
and "lookup b v1 ≠ 0"
and v1[rule_format]: "(∀u. v1 ≺⇩t u ⟶ lookup a u = lookup b u)"
unfolding ord_strict_p_def by auto
from ‹b ≺⇩p c› obtain v2 where "lookup b v2 = 0"
and "lookup c v2 ≠ 0"
and v2[rule_format]: "(∀u. v2 ≺⇩t u ⟶ lookup b u = lookup c u)"
unfolding ord_strict_p_def by auto
show "a ≺⇩p c"
proof (rule ord_term_lin.linorder_cases)
assume "v1 ≺⇩t v2"
show ?thesis unfolding ord_strict_p_def
proof
show "lookup a v2 = 0 ∧ lookup c v2 ≠ 0 ∧ (∀u. v2 ≺⇩t u ⟶ lookup a u = lookup c u)"
proof (intro conjI allI impI)
from ‹lookup b v2 = 0› v1[OF ‹v1 ≺⇩t v2›] show "lookup a v2 = 0" by simp
next
from ‹lookup c v2 ≠ 0› show "lookup c v2 ≠ 0" .
next
fix u
assume "v2 ≺⇩t u"
from ord_term_lin.less_trans[OF ‹v1 ≺⇩t v2› this] have "v1 ≺⇩t u" .
from v2[OF ‹v2 ≺⇩t u›] v1[OF this] show "lookup a u = lookup c u" by simp
qed
qed
next
assume "v2 ≺⇩t v1"
show ?thesis unfolding ord_strict_p_def
proof
show "lookup a v1 = 0 ∧ lookup c v1 ≠ 0 ∧ (∀u. v1 ≺⇩t u ⟶ lookup a u = lookup c u)"
proof (intro conjI allI impI)
from ‹lookup a v1 = 0› show "lookup a v1 = 0" .
next
from ‹lookup b v1 ≠ 0› v2[OF ‹v2 ≺⇩t v1›] show "lookup c v1 ≠ 0" by simp
next
fix u
assume "v1 ≺⇩t u"
from ord_term_lin.less_trans[OF ‹v2 ≺⇩t v1› this] have "v2 ≺⇩t u" .
from v1[OF ‹v1 ≺⇩t u›] v2[OF this] show "lookup a u = lookup c u" by simp
qed
qed
next
assume "v1 = v2"
thus ?thesis using ‹lookup b v1 ≠ 0› ‹lookup b v2 = 0› by simp
qed
qed
sublocale order ord_p ord_strict_p
proof (intro order_strictI)
fix p q :: "'t ⇒⇩0 'b"
show "(p ≼⇩p q) = (p ≺⇩p q ∨ p = q)" unfolding ord_p_def ..
next
fix p q :: "'t ⇒⇩0 'b"
assume "p ≺⇩p q"
thus "¬ q ≺⇩p p" by (rule ord_strict_p_asymmetric)
next
fix p::"'t ⇒⇩0 'b"
show "¬ p ≺⇩p p" by (fact ord_strict_p_irreflexive)
next
fix a b c :: "'t ⇒⇩0 'b"
assume "a ≺⇩p b" and "b ≺⇩p c"
thus "a ≺⇩p c" by (rule ord_strict_p_transitive)
qed
lemma ord_p_zero_min: "0 ≼⇩p p"
unfolding ord_p_def ord_strict_p_def
proof (cases "p = 0")
case True
thus "(∃v. lookup 0 v = 0 ∧ lookup p v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup 0 u = lookup p u)) ∨ 0 = p"
by auto
next
case False
show "(∃v. lookup 0 v = 0 ∧ lookup p v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup 0 u = lookup p u)) ∨ 0 = p"
proof
show "(∃v. lookup 0 v = 0 ∧ lookup p v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup 0 u = lookup p u))"
proof
show "lookup 0 (lt p) = 0 ∧ lookup p (lt p) ≠ 0 ∧ (∀u. (lt p) ≺⇩t u ⟶ lookup 0 u = lookup p u)"
proof (intro conjI allI impI)
show "lookup 0 (lt p) = 0" by (transfer, simp)
next
from lc_not_0[OF False] show "lookup p (lt p) ≠ 0" unfolding lc_def .
next
fix u
assume "lt p ≺⇩t u"
hence "¬ u ≼⇩t lt p" by simp
hence "lookup p u = 0" using lt_max[of p u] by metis
thus "lookup 0 u = lookup p u" by simp
qed
qed
qed
qed
lemma lt_ord_p:
assumes "lt p ≺⇩t lt q"
shows "p ≺⇩p q"
proof -
have "q ≠ 0"
proof
assume "q = 0"
with assms have "lt p ≺⇩t min_term" by (simp add: lt_def)
with min_term_min[of "lt p"] show False by simp
qed
show ?thesis unfolding ord_strict_p_def
proof (intro exI conjI allI impI)
show "lookup p (lt q) = 0"
proof (rule ccontr)
assume "lookup p (lt q) ≠ 0"
from lt_max[OF this] ‹lt p ≺⇩t lt q› show False by simp
qed
next
from lc_not_0[OF ‹q ≠ 0›] show "lookup q (lt q) ≠ 0" unfolding lc_def .
next
fix u
assume "lt q ≺⇩t u"
hence "lt p ≺⇩t u" using ‹lt p ≺⇩t lt q› by simp
have c1: "lookup q u = 0"
proof (rule ccontr)
assume "lookup q u ≠ 0"
from lt_max[OF this] ‹lt q ≺⇩t u› show False by simp
qed
have c2: "lookup p u = 0"
proof (rule ccontr)
assume "lookup p u ≠ 0"
from lt_max[OF this] ‹lt p ≺⇩t u› show False by simp
qed
from c1 c2 show "lookup p u = lookup q u" by simp
qed
qed
lemma ord_p_lt:
assumes "p ≼⇩p q"
shows "lt p ≼⇩t lt q"
proof (rule ccontr)
assume "¬ lt p ≼⇩t lt q"
hence "lt q ≺⇩t lt p" by simp
from lt_ord_p[OF this] ‹p ≼⇩p q› show False by simp
qed
lemma ord_p_tail:
assumes "p ≠ 0" and "lt p = lt q" and "p ≺⇩p q"
shows "tail p ≺⇩p tail q"
using assms unfolding ord_strict_p_def
proof -
assume "p ≠ 0" and "lt p = lt q"
and "∃v. lookup p v = 0 ∧ lookup q v ≠ 0 ∧ (∀u. v ≺⇩t u ⟶ lookup p u = lookup q u)"
then obtain v where "lookup p v = 0"
and "lookup q v ≠ 0"
and a: "∀u. v ≺⇩t u ⟶ lookup p u = lookup q u" by auto
from lt_max[OF ‹lookup q v ≠ 0›] ‹lt p = lt q› have "v ≺⇩t lt p ∨ v = lt p" by auto
hence "v ≺⇩t lt p"
proof
assume "v ≺⇩t lt p"
thus ?thesis .
next
assume "v = lt p"
thus ?thesis using lc_not_0[OF ‹p ≠ 0›] ‹lookup p v = 0› unfolding lc_def by auto
qed
have pt: "lookup (tail p) v = lookup p v" using lookup_tail[of p v] ‹v ≺⇩t lt p› by simp
have "q ≠ 0"
proof
assume "q = 0"
hence "p ≺⇩p 0" using ‹p ≺⇩p q› by simp
hence "¬ 0 ≼⇩p p" by auto
thus False using ord_p_zero_min[of p] by simp
qed
have qt: "lookup (tail q) v = lookup q v"
using lookup_tail[of q v] ‹v ≺⇩t lt p› ‹lt p = lt q› by simp
show "∃w. lookup (tail p) w = 0 ∧ lookup (tail q) w ≠ 0 ∧
(∀u. w ≺⇩t u ⟶ lookup (tail p) u = lookup (tail q) u)"
proof (intro exI conjI allI impI)
from pt ‹lookup p v = 0› show "lookup (tail p) v = 0" by simp
next
from qt ‹lookup q v ≠ 0› show "lookup (tail q) v ≠ 0" by simp
next
fix u
assume "v ≺⇩t u"
from a[rule_format, OF ‹v ≺⇩t u›] lookup_tail[of p u] lookup_tail[of q u]
‹lt p = lt q› show "lookup (tail p) u = lookup (tail q) u" by simp
qed
qed
lemma tail_ord_p:
assumes "p ≠ 0"
shows "tail p ≺⇩p p"
proof (cases "tail p = 0")
case True
with ord_p_zero_min[of p] ‹p ≠ 0› show ?thesis by simp
next
case False
from lt_tail[OF False] show ?thesis by (rule lt_ord_p)
qed
lemma higher_lookup_eq_zero:
assumes pt: "lookup p v = 0" and hp: "higher p v = 0" and le: "q ≼⇩p p"
shows "(lookup q v = 0) ∧ (higher q v) = 0"
using le unfolding ord_p_def
proof
assume "q ≺⇩p p"
thus ?thesis unfolding ord_strict_p_def
proof
fix w
assume "lookup q w = 0 ∧ lookup p w ≠ 0 ∧ (∀u. w ≺⇩t u ⟶ lookup q u = lookup p u)"
hence qs: "lookup q w = 0" and ps: "lookup p w ≠ 0" and u: "∀u. w ≺⇩t u ⟶ lookup q u = lookup p u"
by auto
from hp have pu: "∀u. v ≺⇩t u ⟶ lookup p u = 0" by (simp only: higher_eq_zero_iff)
from pu[rule_format, of w] ps have "¬ v ≺⇩t w" by auto
hence "w ≼⇩t v" by simp
hence "w ≺⇩t v ∨ w = v" by auto
hence st: "w ≺⇩t v"
proof (rule disjE, simp_all)
assume "w = v"
from this pt ps show False by simp
qed
show ?thesis
proof
from u[rule_format, OF st] pt show "lookup q v = 0" by simp
next
have "∀u. v ≺⇩t u ⟶ lookup q u = 0"
proof (intro allI, intro impI)
fix u
assume "v ≺⇩t u"
from this st have "w ≺⇩t u" by simp
from u[rule_format, OF this] pu[rule_format, OF ‹v ≺⇩t u›] show "lookup q u = 0" by simp
qed
thus "higher q v = 0" by (simp only: higher_eq_zero_iff)
qed
qed
next
assume "q = p"
thus ?thesis using assms by simp
qed
lemma ord_strict_p_recI:
assumes "lt p = lt q" and "lc p = lc q" and tail: "tail p ≺⇩p tail q"
shows "p ≺⇩p q"
proof -
from tail obtain v where pt: "lookup (tail p) v = 0"
and qt: "lookup (tail q) v ≠ 0"
and a: "∀u. v ≺⇩t u ⟶ lookup (tail p) u = lookup (tail q) u"
unfolding ord_strict_p_def by auto
from qt lookup_zero[of v] have "tail q ≠ 0" by auto
from lt_max[OF qt] lt_tail[OF this] have "v ≺⇩t lt q" by simp
hence "v ≺⇩t lt p" using ‹lt p = lt q› by simp
show ?thesis unfolding ord_strict_p_def
proof (rule exI[of _ v], intro conjI allI impI)
from lookup_tail[of p v] ‹v ≺⇩t lt p› pt show "lookup p v = 0" by simp
next
from lookup_tail[of q v] ‹v ≺⇩t lt q› qt show "lookup q v ≠ 0" by simp
next
fix u
assume "v ≺⇩t u"
from this a have s: "lookup (tail p) u = lookup (tail q) u" by simp
show "lookup p u = lookup q u"
proof (cases "u = lt p")
case True
from True ‹lc p = lc q› ‹lt p = lt q› show ?thesis unfolding lc_def by simp
next
case False
from False s lookup_tail_2[of p u] lookup_tail_2[of q u] ‹lt p = lt q› show ?thesis by simp
qed
qed
qed
lemma ord_strict_p_recE1:
assumes "p ≺⇩p q"
shows "q ≠ 0"
proof
assume "q = 0"
from this assms ord_p_zero_min[of p] show False by simp
qed
lemma ord_strict_p_recE2:
assumes "p ≠ 0" and "p ≺⇩p q" and "lt p = lt q"
shows "lc p = lc q"
proof -
from ‹p ≺⇩p q› obtain v where pt: "lookup p v = 0"
and qt: "lookup q v ≠ 0"
and a: "∀u. v ≺⇩t u ⟶ lookup p u = lookup q u"
unfolding ord_strict_p_def by auto
show ?thesis
proof (cases "v ≺⇩t lt p")
case True
from this a have "lookup p (lt p) = lookup q (lt p)" by simp
thus ?thesis using ‹lt p = lt q› unfolding lc_def by simp
next
case False
from this lt_max[OF qt] ‹lt p = lt q› have "v = lt p" by simp
from this lc_not_0[OF ‹p ≠ 0›] pt show ?thesis unfolding lc_def by auto
qed
qed
lemma ord_strict_p_rec [code]:
"p ≺⇩p q =
(q ≠ 0 ∧
(p = 0 ∨
(let v1 = lt p; v2 = lt q in
(v1 ≺⇩t v2 ∨ (v1 = v2 ∧ lookup p v1 = lookup q v2 ∧ lower p v1 ≺⇩p lower q v2))
)
)
)"
(is "?L = ?R")
proof
assume ?L
show ?R
proof (intro conjI, rule ord_strict_p_recE1, fact)
have "((lt p = lt q ∧ lc p = lc q ∧ tail p ≺⇩p tail q) ∨ lt p ≺⇩t lt q) ∨ p = 0"
proof (intro disjCI)
assume "p ≠ 0" and nl: "¬ lt p ≺⇩t lt q"
from ‹?L› have "p ≼⇩p q" by simp
from ord_p_lt[OF this] nl have "lt p = lt q" by simp
show "lt p = lt q ∧ lc p = lc q ∧ tail p ≺⇩p tail q"
by (intro conjI, fact, rule ord_strict_p_recE2, fact+, rule ord_p_tail, fact+)
qed
thus "p = 0 ∨
(let v1 = lt p; v2 = lt q in
(v1 ≺⇩t v2 ∨ v1 = v2 ∧ lookup p v1 = lookup q v2 ∧ lower p v1 ≺⇩p lower q v2)
)"
unfolding lc_def tail_def by auto
qed
next
assume ?R
hence "q ≠ 0"
and dis: "p = 0 ∨
(let v1 = lt p; v2 = lt q in
(v1 ≺⇩t v2 ∨ v1 = v2 ∧ lookup p v1 = lookup q v2 ∧ lower p v1 ≺⇩p lower q v2)
)"
by simp_all
show ?L
proof (cases "p = 0")
assume "p = 0"
hence "p ≼⇩p q" using ord_p_zero_min[of q] by simp
thus ?thesis using ‹p = 0› ‹q ≠ 0› by simp
next
assume "p ≠ 0"
hence "let v1 = lt p; v2 = lt q in
(v1 ≺⇩t v2 ∨ v1 = v2 ∧ lookup p v1 = lookup q v2 ∧ lower p v1 ≺⇩p lower q v2)"
using dis by simp
hence "lt p ≺⇩t lt q ∨ (lt p = lt q ∧ lc p = lc q ∧ tail p ≺⇩p tail q)"
unfolding lc_def tail_def by (simp add: Let_def)
thus ?thesis
proof
assume "lt p ≺⇩t lt q"
from lt_ord_p[OF this] show ?thesis .
next
assume "lt p = lt q ∧ lc p = lc q ∧ tail p ≺⇩p tail q"
hence "lt p = lt q" and "lc p = lc q" and "tail p ≺⇩p tail q" by simp_all
thus ?thesis by (rule ord_strict_p_recI)
qed
qed
qed
lemma ord_strict_p_monomial_iff: "p ≺⇩p monomial c v ⟷ (c ≠ 0 ∧ (p = 0 ∨ lt p ≺⇩t v))"
proof -
from ord_p_zero_min[of "tail p"] have *: "¬ tail p ≺⇩p 0" by auto
show ?thesis
by (simp add: ord_strict_p_rec[of p] Let_def tail_def[symmetric] lc_def[symmetric]
monomial_0_iff tail_monomial *, simp add: lt_monomial cong: conj_cong)
qed
corollary ord_strict_p_monomial_plus:
assumes "p ≺⇩p monomial c v" and "q ≺⇩p monomial c v"
shows "p + q ≺⇩p monomial c v"
proof -
from assms(1) have "c ≠ 0" and "p = 0 ∨ lt p ≺⇩t v" by (simp_all add: ord_strict_p_monomial_iff)
from this(2) show ?thesis
proof
assume "p = 0"
with assms(2) show ?thesis by simp
next
assume "lt p ≺⇩t v"
from assms(2) have "q = 0 ∨ lt q ≺⇩t v" by (simp add: ord_strict_p_monomial_iff)
thus ?thesis
proof
assume "q = 0"
with assms(1) show ?thesis by simp
next
assume "lt q ≺⇩t v"
with ‹lt p ≺⇩t v› have "lt (p + q) ≺⇩t v"
using lt_plus_le_max ord_term_lin.dual_order.strict_trans2 ord_term_lin.max_less_iff_conj
by blast
with ‹c ≠ 0› show ?thesis by (simp add: ord_strict_p_monomial_iff)
qed
qed
qed
lemma ord_strict_p_monom_mult:
assumes "p ≺⇩p q" and "c ≠ (0::'b::semiring_no_zero_divisors)"
shows "monom_mult c t p ≺⇩p monom_mult c t q"
proof -
from assms(1) obtain v where 1: "lookup p v = 0" and 2: "lookup q v ≠ 0"
and 3: "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u" unfolding ord_strict_p_def by auto
show ?thesis unfolding ord_strict_p_def
proof (intro exI conjI allI impI)
from 1 show "lookup (monom_mult c t p) (t ⊕ v) = 0" by (simp add: lookup_monom_mult_plus)
next
from 2 assms(2) show "lookup (monom_mult c t q) (t ⊕ v) ≠ 0" by (simp add: lookup_monom_mult_plus)
next
fix u
assume "t ⊕ v ≺⇩t u"
show "lookup (monom_mult c t p) u = lookup (monom_mult c t q) u"
proof (cases "t adds⇩p u")
case True
then obtain w where u: "u = t ⊕ w" ..
from ‹t ⊕ v ≺⇩t u› have "v ≺⇩t w" unfolding u by (rule ord_term_strict_canc)
hence "lookup p w = lookup q w" by (rule 3)
thus ?thesis by (simp add: u lookup_monom_mult_plus)
next
case False
thus ?thesis by (simp add: lookup_monom_mult)
qed
qed
qed
lemma ord_strict_p_plus:
assumes "p ≺⇩p q" and "keys r ∩ keys q = {}"
shows "p + r ≺⇩p q + r"
proof -
from assms(1) obtain v where 1: "lookup p v = 0" and 2: "lookup q v ≠ 0"
and 3: "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u" unfolding ord_strict_p_def by auto
have eq: "lookup r v = 0"
by (meson "2" assms(2) disjoint_iff_not_equal in_keys_iff)
show ?thesis unfolding ord_strict_p_def
proof (intro exI conjI allI impI, simp_all add: lookup_add)
from 1 show "lookup p v + lookup r v = 0" by (simp add: eq)
next
from 2 show "lookup q v + lookup r v ≠ 0" by (simp add: eq)
next
fix u
assume "v ≺⇩t u"
hence "lookup p u = lookup q u" by (rule 3)
thus "lookup p u + lookup r u = lookup q u + lookup r u" by simp
qed
qed
lemma poly_mapping_tail_induct [case_names 0 tail]:
assumes "P 0" and "⋀p. p ≠ 0 ⟹ P (tail p) ⟹ P p"
shows "P p"
proof (induct "card (keys p)" arbitrary: p)
case 0
with finite_keys[of p] have "keys p = {}" by simp
hence "p = 0" by simp
from ‹P 0› show ?case unfolding ‹p = 0› .
next
case ind: (Suc n)
from ind(2) have "keys p ≠ {}" by auto
hence "p ≠ 0" by simp
thus ?case
proof (rule assms(2))
show "P (tail p)"
proof (rule ind(1))
from ‹p ≠ 0› have "lt p ∈ keys p" by (rule lt_in_keys)
hence "card (keys (tail p)) = card (keys p) - 1" by (simp add: keys_tail)
also have "... = n" unfolding ind(2)[symmetric] by simp
finally show "n = card (keys (tail p))" by simp
qed
qed
qed
lemma poly_mapping_neqE:
assumes "p ≠ q"
obtains v where "v ∈ keys p ∪ keys q" and "lookup p v ≠ lookup q v"
and "⋀u. v ≺⇩t u ⟹ lookup p u = lookup q u"
proof -
let ?A = "{v. lookup p v ≠ lookup q v}"
define v where "v = ord_term_lin.Max ?A"
have "?A ⊆ keys p ∪ keys q"
using UnI2 in_keys_iff by fastforce
also have "finite ..." by (rule finite_UnI) (fact finite_keys)+
finally(finite_subset) have fin: "finite ?A" .
moreover have "?A ≠ {}"
proof
assume "?A = {}"
hence "p = q"
using poly_mapping_eqI by fastforce
with assms show False ..
qed
ultimately have "v ∈ ?A" unfolding v_def by (rule ord_term_lin.Max_in)
show ?thesis
proof
from ‹?A ⊆ keys p ∪ keys q› ‹v ∈ ?A› show "v ∈ keys p ∪ keys q" ..
next
from ‹v ∈ ?A› show "lookup p v ≠ lookup q v" by simp
next
fix u
assume "v ≺⇩t u"
show "lookup p u = lookup q u"
proof (rule ccontr)
assume "lookup p u ≠ lookup q u"
hence "u ∈ ?A" by simp
with fin have "u ≼⇩t v" unfolding v_def by (rule ord_term_lin.Max_ge)
with ‹v ≺⇩t u› show False by simp
qed
qed
qed
subsection ‹Monomials›
lemma keys_monomial:
assumes "is_monomial p"
shows "keys p = {lt p}"
using assms by (metis is_monomial_monomial lt_monomial keys_of_monomial)
lemma monomial_eq_itself:
assumes "is_monomial p"
shows "monomial (lc p) (lt p) = p"
proof -
from assms have "p ≠ 0" by (rule monomial_not_0)
hence "lc p ≠ 0" by (rule lc_not_0)
hence keys1: "keys (monomial (lc p) (lt p)) = {lt p}" by (rule keys_of_monomial)
show ?thesis
by (rule poly_mapping_keys_eqI, simp only: keys_monomial[OF assms] keys1,
simp only: keys1 lookup_single Poly_Mapping.when_def, auto simp add: lc_def)
qed
lemma lt_eq_min_term_monomial:
assumes "lt p = min_term"
shows "monomial (lc p) min_term = p"
proof (rule poly_mapping_eqI)
fix v
from min_term_min[of v] have "v = min_term ∨ min_term ≺⇩t v" by auto
thus "lookup (monomial (lc p) min_term) v = lookup p v"
proof
assume "v = min_term"
thus ?thesis by (simp add: lookup_single lc_def assms)
next
assume "min_term ≺⇩t v"
moreover have "v ∉ keys p"
proof
assume "v ∈ keys p"
hence "v ≼⇩t lt p" by (rule lt_max_keys)
with ‹min_term ≺⇩t v› show False by (simp add: assms)
qed
ultimately show ?thesis by (simp add: lookup_single in_keys_iff)
qed
qed
lemma is_monomial_monomial_ordered:
assumes "is_monomial p"
obtains c v where "c ≠ 0" and "lc p = c" and "lt p = v" and "p = monomial c v"
proof -
from assms obtain c v where "c ≠ 0" and p_eq: "p = monomial c v" by (rule is_monomial_monomial)
note this(1)
moreover have "lc p = c" unfolding p_eq by (rule lc_monomial)
moreover from ‹c ≠ 0› have "lt p = v" unfolding p_eq by (rule lt_monomial)
ultimately show ?thesis using p_eq ..
qed
lemma monomial_plus_not_0:
assumes "c ≠ 0" and "lt p ≺⇩t v"
shows "monomial c v + p ≠ 0"
proof
assume "monomial c v + p = 0"
hence "0 = lookup (monomial c v + p) v" by simp
also have "... = c + lookup p v" by (simp add: lookup_add)
also have "... = c"
proof -
from assms(2) have "¬ v ≼⇩t lt p" by simp
with lt_max[of p v] have "lookup p v = 0" by blast
thus ?thesis by simp
qed
finally show False using ‹c ≠ 0› by simp
qed
lemma lt_monomial_plus:
assumes "c ≠ (0::'b::comm_monoid_add)" and "lt p ≺⇩t v"
shows "lt (monomial c v + p) = v"
proof -
have eq: "lt (monomial c v) = v" by (simp only: lt_monomial[OF ‹c ≠ 0›])
moreover have "lt (p + monomial c v) = lt (monomial c v)" by (rule lt_plus_eqI, simp only: eq, fact)
ultimately show ?thesis by (simp add: add.commute)
qed
lemma lc_monomial_plus:
assumes "c ≠ (0::'b::comm_monoid_add)" and "lt p ≺⇩t v"
shows "lc (monomial c v + p) = c"
proof -
from assms(2) have "¬ v ≼⇩t lt p" by simp
with lt_max[of p v] have "lookup p v = 0" by blast
thus ?thesis by (simp add: lc_def lt_monomial_plus[OF assms] lookup_add)
qed
lemma tt_monomial_plus:
assumes "p ≠ (0::_ ⇒⇩0 'b::comm_monoid_add)" and "lt p ≺⇩t v"
shows "tt (monomial c v + p) = tt p"
proof (cases "c = 0")
case True
thus ?thesis by (simp add: monomial_0I)
next
case False
have eq: "tt (monomial c v) = v" by (simp only: tt_monomial[OF ‹c ≠ 0›])
moreover have "tt (p + monomial c v) = tt p"
proof (rule tt_plus_eqI, fact, simp only: eq)
from lt_ge_tt[of p] assms(2) show "tt p ≺⇩t v" by simp
qed
ultimately show ?thesis by (simp add: ac_simps)
qed
lemma tc_monomial_plus:
assumes "p ≠ (0::_ ⇒⇩0 'b::comm_monoid_add)" and "lt p ≺⇩t v"
shows "tc (monomial c v + p) = tc p"
proof (simp add: tc_def tt_monomial_plus[OF assms] lookup_add lookup_single Poly_Mapping.when_def,
rule impI)
assume "v = tt p"
with assms(2) have "lt p ≺⇩t tt p" by simp
with lt_ge_tt[of p] show "c + lookup p (tt p) = lookup p (tt p)" by simp
qed
lemma tail_monomial_plus:
assumes "c ≠ (0::'b::comm_monoid_add)" and "lt p ≺⇩t v"
shows "tail (monomial c v + p) = p" (is "tail ?q = _")
proof -
from assms have "lt ?q = v" by (rule lt_monomial_plus)
moreover have "lower (monomial c v) v = 0"
by (simp add: lower_eq_zero_iff', rule disjI2, simp add: tt_monomial[OF ‹c ≠ 0›])
ultimately show ?thesis by (simp add: tail_def lower_plus lower_id_iff, intro disjI2 assms(2))
qed
subsection ‹Lists of Keys›
text ‹In algorithms one very often needs to compute the sorted list of all terms appearing
in a list of polynomials.›
definition pps_to_list :: "'t set ⇒ 't list" where
"pps_to_list S = rev (ord_term_lin.sorted_list_of_set S)"
definition keys_to_list :: "('t ⇒⇩0 'b::zero) ⇒ 't list"
where "keys_to_list p = pps_to_list (keys p)"
definition Keys_to_list :: "('t ⇒⇩0 'b::zero) list ⇒ 't list"
where "Keys_to_list ps = fold (λp ts. merge_wrt (≻⇩t) (keys_to_list p) ts) ps []"
text ‹Function @{const pps_to_list} turns finite sets of terms into sorted lists, where the
lists are sorted descending (i.\,e. greater elements come before smaller ones).›
lemma distinct_pps_to_list: "distinct (pps_to_list S)"
unfolding pps_to_list_def distinct_rev by (rule ord_term_lin.distinct_sorted_list_of_set)
lemma set_pps_to_list:
assumes "finite S"
shows "set (pps_to_list S) = S"
unfolding pps_to_list_def set_rev using assms by simp
lemma length_pps_to_list: "length (pps_to_list S) = card S"
proof (cases "finite S")
case True
from distinct_card[OF distinct_pps_to_list] have "length (pps_to_list S) = card (set (pps_to_list S))"
by simp
also from True have "... = card S" by (simp only: set_pps_to_list)
finally show ?thesis .
next
case False
thus ?thesis by (simp add: pps_to_list_def)
qed
lemma pps_to_list_sorted_wrt: "sorted_wrt (≻⇩t) (pps_to_list S)"
proof -
have "sorted_wrt (≽⇩t) (pps_to_list S)"
proof -
have tr: "transp (≼⇩t)" using transp_def by fastforce
have *: "(λx y. y ≽⇩t x) = (≼⇩t)" by simp
show ?thesis
by (simp only: * pps_to_list_def sorted_wrt_rev,
rule ord_term_lin.sorted_sorted_list_of_set)
qed
with distinct_pps_to_list have "sorted_wrt (λx y. x ≽⇩t y ∧ x ≠ y) (pps_to_list S)"
by (rule distinct_sorted_wrt_imp_sorted_wrt_strict)
moreover have "(≻⇩t) = (λx y. x ≽⇩t y ∧ x ≠ y)"
using ord_term_lin.dual_order.order_iff_strict by auto
ultimately show ?thesis by simp
qed
lemma pps_to_list_nth_leI:
assumes "j ≤ i" and "i < card S"
shows "(pps_to_list S) ! i ≼⇩t (pps_to_list S) ! j"
proof (cases "j = i")
case True
show ?thesis by (simp add: True)
next
case False
with assms(1) have "j < i" by simp
let ?ts = "pps_to_list S"
from pps_to_list_sorted_wrt ‹j < i› have "(≺⇩t)¯¯ (?ts ! j) (?ts ! i)"
proof (rule sorted_wrt_nth_less)
from assms(2) show "i < length ?ts" by (simp only: length_pps_to_list)
qed
thus ?thesis by simp
qed
lemma pps_to_list_nth_lessI:
assumes "j < i" and "i < card S"
shows "(pps_to_list S) ! i ≺⇩t (pps_to_list S) ! j"
proof -
let ?ts = "pps_to_list S"
from assms(1) have "j ≤ i" and "i ≠ j" by simp_all
with assms(2) have "i < length ?ts" and "j < length ?ts" by (simp_all only: length_pps_to_list)
show ?thesis
proof (rule ord_term_lin.neq_le_trans)
from ‹i ≠ j› show "?ts ! i ≠ ?ts ! j"
by (simp add: nth_eq_iff_index_eq[OF distinct_pps_to_list ‹i < length ?ts› ‹j < length ?ts›])
next
from ‹j ≤ i› assms(2) show "?ts ! i ≼⇩t ?ts ! j" by (rule pps_to_list_nth_leI)
qed
qed
lemma pps_to_list_nth_leD:
assumes "(pps_to_list S) ! i ≼⇩t (pps_to_list S) ! j" and "j < card S"
shows "j ≤ i"
proof (rule ccontr)
assume "¬ j ≤ i"
hence "i < j" by simp
from this ‹j < card S› have "(pps_to_list S) ! j ≺⇩t (pps_to_list S) ! i" by (rule pps_to_list_nth_lessI)
with assms(1) show False by simp
qed
lemma pps_to_list_nth_lessD:
assumes "(pps_to_list S) ! i ≺⇩t (pps_to_list S) ! j" and "j < card S"
shows "j < i"
proof (rule ccontr)
assume "¬ j < i"
hence "i ≤ j" by simp
from this ‹j < card S› have "(pps_to_list S) ! j ≼⇩t (pps_to_list S) ! i" by (rule pps_to_list_nth_leI)
with assms(1) show False by simp
qed
lemma set_keys_to_list: "set (keys_to_list p) = keys p"
by (simp add: keys_to_list_def set_pps_to_list)
lemma length_keys_to_list: "length (keys_to_list p) = card (keys p)"
by (simp only: keys_to_list_def length_pps_to_list)
lemma keys_to_list_zero [simp]: "keys_to_list 0 = []"
by (simp add: keys_to_list_def pps_to_list_def)
lemma Keys_to_list_Nil [simp]: "Keys_to_list [] = []"
by (simp add: Keys_to_list_def)
lemma set_Keys_to_list: "set (Keys_to_list ps) = Keys (set ps)"
proof -
have "set (Keys_to_list ps) = (⋃p∈set ps. set (keys_to_list p)) ∪ set []"
unfolding Keys_to_list_def by (rule set_fold, simp only: set_merge_wrt)
also have "... = Keys (set ps)" by (simp add: Keys_def set_keys_to_list)
finally show ?thesis .
qed
lemma Keys_to_list_sorted_wrt_aux:
assumes "sorted_wrt (≻⇩t) ts"
shows "sorted_wrt (≻⇩t) (fold (λp ts. merge_wrt (≻⇩t) (keys_to_list p) ts) ps ts)"
using assms
proof (induct ps arbitrary: ts)
case Nil
thus ?case by simp
next
case (Cons p ps)
show ?case
proof (simp only: fold.simps o_def, rule Cons(1), rule sorted_merge_wrt)
show "transp (≻⇩t)" unfolding transp_def by fastforce
next
fix x y :: 't
assume "x ≠ y"
thus "x ≻⇩t y ∨ y ≻⇩t x" by auto
next
show "sorted_wrt (≻⇩t) (keys_to_list p)" unfolding keys_to_list_def
by (fact pps_to_list_sorted_wrt)
qed fact
qed
corollary Keys_to_list_sorted_wrt: "sorted_wrt (≻⇩t) (Keys_to_list ps)"
unfolding Keys_to_list_def
proof (rule Keys_to_list_sorted_wrt_aux)
show "sorted_wrt (≻⇩t) []" by simp
qed
corollary distinct_Keys_to_list: "distinct (Keys_to_list ps)"
proof (rule distinct_sorted_wrt_irrefl)
show "irreflp (≻⇩t)" by (simp add: irreflp_def)
next
show "transp (≻⇩t)" unfolding transp_def by fastforce
next
show "sorted_wrt (≻⇩t) (Keys_to_list ps)" by (fact Keys_to_list_sorted_wrt)
qed
lemma length_Keys_to_list: "length (Keys_to_list ps) = card (Keys (set ps))"
proof -
from distinct_Keys_to_list have "card (set (Keys_to_list ps)) = length (Keys_to_list ps)"
by (rule distinct_card)
thus ?thesis by (simp only: set_Keys_to_list)
qed
lemma Keys_to_list_eq_pps_to_list: "Keys_to_list ps = pps_to_list (Keys (set ps))"
using _ Keys_to_list_sorted_wrt distinct_Keys_to_list pps_to_list_sorted_wrt distinct_pps_to_list
proof (rule sorted_wrt_distinct_set_unique)
show "antisymp (≻⇩t)" unfolding antisymp_def by fastforce
next
from finite_set have fin: "finite (Keys (set ps))" by (rule finite_Keys)
show "set (Keys_to_list ps) = set (pps_to_list (Keys (set ps)))"
by (simp add: set_Keys_to_list set_pps_to_list[OF fin])
qed
subsection ‹Multiplication›
lemma in_keys_mult_scalar_le:
assumes "v ∈ keys (p ⊙ q)"
shows "v ≼⇩t punit.lt p ⊕ lt q"
proof -
from assms obtain t u where "t ∈ keys p" and "u ∈ keys q" and "v = t ⊕ u"
by (rule in_keys_mult_scalarE)
from ‹t ∈ keys p› have "t ≼ punit.lt p" by (rule punit.lt_max_keys)
from ‹u ∈ keys q› have "u ≼⇩t lt q" by (rule lt_max_keys)
hence "v ≼⇩t t ⊕ lt q" unfolding ‹v = t ⊕ u› by (rule splus_mono)
also from ‹t ≼ punit.lt p› have "... ≼⇩t punit.lt p ⊕ lt q" by (rule splus_mono_left)
finally show ?thesis .
qed
lemma in_keys_mult_scalar_ge:
assumes "v ∈ keys (p ⊙ q)"
shows "punit.tt p ⊕ tt q ≼⇩t v"
proof -
from assms obtain t u where "t ∈ keys p" and "u ∈ keys q" and "v = t ⊕ u"
by (rule in_keys_mult_scalarE)
from ‹t ∈ keys p› have "punit.tt p ≼ t" by (rule punit.tt_min_keys)
from ‹u ∈ keys q› have "tt q ≼⇩t u" by (rule tt_min_keys)
hence "punit.tt p ⊕ tt q ≼⇩t punit.tt p ⊕ u" by (rule splus_mono)
also from ‹punit.tt p ≼ t› have "... ≼⇩t v" unfolding ‹v = t ⊕ u› by (rule splus_mono_left)
finally show ?thesis .
qed
lemma (in ordered_term) lookup_mult_scalar_lt_lt:
"lookup (p ⊙ q) (punit.lt p ⊕ lt q) = punit.lc p * lc q"
proof (induct p rule: punit.poly_mapping_tail_induct)
case 0
show ?case by simp
next
case step: (tail p)
from step(1) have "punit.lc p ≠ 0" by (rule punit.lc_not_0)
let ?t = "punit.lt p ⊕ lt q"
show ?case
proof (cases "is_monomial p")
case True
then obtain c t where "c ≠ 0" and "punit.lt p = t" and "punit.lc p = c" and p_eq: "p = monomial c t"
by (rule punit.is_monomial_monomial_ordered)
hence "p ⊙ q = monom_mult (punit.lc p) (punit.lt p) q" by (simp add: mult_scalar_monomial)
thus ?thesis by (simp add: lookup_monom_mult_plus lc_def)
next
case False
have "punit.lt (punit.tail p) ≠ punit.lt p"
proof (simp add: punit.tail_def punit.lt_lower_eq_iff, rule)
assume "punit.lt p = 0"
have "keys p ⊆ {punit.lt p}"
proof (rule, simp)
fix s
assume "s ∈ keys p"
hence "s ≼ punit.lt p" by (rule punit.lt_max_keys)
moreover have "punit.lt p ≼ s" unfolding ‹punit.lt p = 0› by (rule zero_min)
ultimately show "s = punit.lt p" by simp
qed
hence "card (keys p) = 0 ∨ card (keys p) = 1" using subset_singletonD by fastforce
thus False
proof
assume "card (keys p) = 0"
hence "p = 0" by (meson card_0_eq keys_eq_empty finite_keys)
with step(1) show False ..
next
assume "card (keys p) = 1"
with False show False unfolding is_monomial_def ..
qed
qed
with punit.lt_lower[of p "punit.lt p"] have "punit.lt (punit.tail p) ≺ punit.lt p"
by (simp add: punit.tail_def)
have eq: "lookup ((punit.tail p) ⊙ q) ?t = 0"
proof (rule ccontr)
assume "lookup ((punit.tail p) ⊙ q) ?t ≠ 0"
hence "?t ≼⇩t punit.lt (punit.tail p) ⊕ lt q"
by (meson in_keys_mult_scalar_le lookup_not_eq_zero_eq_in_keys)
hence "punit.lt p ≼ punit.lt (punit.tail p)" by (rule ord_term_canc_left)
also have "... ≺ punit.lt p" by fact
finally show False ..
qed
from step(2) have "lookup (monom_mult (punit.lc p) (punit.lt p) q) ?t = punit.lc p * lc q"
by (simp only: lookup_monom_mult_plus lc_def)
thus ?thesis by (simp add: mult_scalar_tail_rec_left[of p q] lookup_add eq)
qed
qed
lemma lookup_mult_scalar_tt_tt: "lookup (p ⊙ q) (punit.tt p ⊕ tt q) = punit.tc p * tc q"
proof (induct p rule: punit.poly_mapping_tail_induct)
case 0
show ?case by simp
next
case step: (tail p)
from step(1) have "punit.lc p ≠ 0" by (rule punit.lc_not_0)
let ?t = "punit.tt p ⊕ tt q"
show ?case
proof (cases "is_monomial p")
case True
then obtain c t where "c ≠ 0" and "punit.lt p = t" and "punit.lc p = c" and p_eq: "p = monomial c t"
by (rule punit.is_monomial_monomial_ordered)
from ‹c ≠ 0› have "punit.tt p = t" and "punit.tc p = c" by (simp_all add: p_eq punit.tt_monomial)
with p_eq have "p ⊙ q = monom_mult (punit.tc p) (punit.tt p) q" by (simp add: mult_scalar_monomial)
thus ?thesis by (simp add: lookup_monom_mult_plus tc_def)
next
case False
from step(1) have "keys p ≠ {}" by simp
with finite_keys have "card (keys p) ≠ 0" by auto
with False have "2 ≤ card (keys p)" unfolding is_monomial_def by linarith
then obtain s t where "s ∈ keys p" and "t ∈ keys p" and "s ≺ t"
by (metis (mono_tags, lifting) card.empty card.infinite card_insert_disjoint card_mono empty_iff
finite.emptyI insertCI lessI not_less numeral_2_eq_2 ordered_powerprod_lin.infinite_growing
ordered_powerprod_lin.neqE preorder_class.less_le_trans subsetI)
from this(1) this(3) have "punit.tt p ≺ t" by (rule punit.tt_less)
also from ‹t ∈ keys p› have "t ≼ punit.lt p" by (rule punit.lt_max_keys)
finally have "punit.tt p ≺ punit.lt p" .
hence tt_tail: "punit.tt (punit.tail p) = punit.tt p" and tc_tail: "punit.tc (punit.tail p) = punit.tc p"
unfolding punit.tail_def by (rule punit.tt_lower, rule punit.tc_lower)
have eq: "lookup (monom_mult (punit.lc p) (punit.lt p) q) ?t = 0"
proof (rule ccontr)
assume "lookup (monom_mult (punit.lc p) (punit.lt p) q) ?t ≠ 0"
hence "punit.lt p ⊕ tt q ≼⇩t ?t"
by (meson in_keys_iff in_keys_monom_mult_ge)
hence "punit.lt p ≼ punit.tt p" by (rule ord_term_canc_left)
also have "... ≺ punit.lt p" by fact
finally show False ..
qed
from step(2) have "lookup (punit.tail p ⊙ q) ?t = punit.tc p * tc q" by (simp only: tt_tail tc_tail)
thus ?thesis by (simp add: mult_scalar_tail_rec_left[of p q] lookup_add eq)
qed
qed
lemma lt_mult_scalar:
assumes "p ≠ 0" and "q ≠ (0::'t ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "lt (p ⊙ q) = punit.lt p ⊕ lt q"
proof (rule lt_eqI_keys, simp only: in_keys_iff lookup_mult_scalar_lt_lt)
from assms(1) have "punit.lc p ≠ 0" by (rule punit.lc_not_0)
moreover from assms(2) have "lc q ≠ 0" by (rule lc_not_0)
ultimately show "punit.lc p * lc q ≠ 0" by simp
qed (rule in_keys_mult_scalar_le)
lemma tt_mult_scalar:
assumes "p ≠ 0" and "q ≠ (0::'t ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "tt (p ⊙ q) = punit.tt p ⊕ tt q"
proof (rule tt_eqI, simp only: in_keys_iff lookup_mult_scalar_tt_tt)
from assms(1) have "punit.tc p ≠ 0" by (rule punit.tc_not_0)
moreover from assms(2) have "tc q ≠ 0" by (rule tc_not_0)
ultimately show "punit.tc p * tc q ≠ 0" by simp
qed (rule in_keys_mult_scalar_ge)
lemma lc_mult_scalar: "lc (p ⊙ q) = punit.lc p * lc (q::'t ⇒⇩0 'b::semiring_no_zero_divisors)"
proof (cases "p = 0")
case True
thus ?thesis by (simp add: lc_def)
next
case False
show ?thesis
proof (cases "q = 0")
case True
thus ?thesis by (simp add: lc_def)
next
case False
with ‹p ≠ 0› show ?thesis by (simp add: lc_def lt_mult_scalar lookup_mult_scalar_lt_lt)
qed
qed
lemma tc_mult_scalar: "tc (p ⊙ q) = punit.tc p * tc (q::'t ⇒⇩0 'b::semiring_no_zero_divisors)"
proof (cases "p = 0")
case True
thus ?thesis by (simp add: tc_def)
next
case False
show ?thesis
proof (cases "q = 0")
case True
thus ?thesis by (simp add: tc_def)
next
case False
with ‹p ≠ 0› show ?thesis by (simp add: tc_def tt_mult_scalar lookup_mult_scalar_tt_tt)
qed
qed
lemma mult_scalar_not_zero:
assumes "p ≠ 0" and "q ≠ (0::'t ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "p ⊙ q ≠ 0"
proof
assume "p ⊙ q = 0"
hence "0 = lc (p ⊙ q)" by (simp add: lc_def)
also have "... = punit.lc p * lc q" by (rule lc_mult_scalar)
finally have "punit.lc p * lc q = 0" by simp
moreover from assms(1) have "punit.lc p ≠ 0" by (rule punit.lc_not_0)
moreover from assms(2) have "lc q ≠ 0" by (rule lc_not_0)
ultimately show False by simp
qed
end
context ordered_powerprod
begin
lemmas in_keys_times_le = punit.in_keys_mult_scalar_le[simplified]
lemmas in_keys_times_ge = punit.in_keys_mult_scalar_ge[simplified]
lemmas lookup_times_lp_lp = punit.lookup_mult_scalar_lt_lt[simplified]
lemmas lookup_times_tp_tp = punit.lookup_mult_scalar_tt_tt[simplified]
lemmas lookup_times_monomial_right_plus = punit.lookup_mult_scalar_monomial_right_plus[simplified]
lemmas lookup_times_monomial_right = punit.lookup_mult_scalar_monomial_right[simplified]
lemmas lp_times = punit.lt_mult_scalar[simplified]
lemmas tp_times = punit.tt_mult_scalar[simplified]
lemmas lc_times = punit.lc_mult_scalar[simplified]
lemmas tc_times = punit.tc_mult_scalar[simplified]
lemmas times_not_zero = punit.mult_scalar_not_zero[simplified]
lemmas times_tail_rec_left = punit.mult_scalar_tail_rec_left[simplified]
lemmas times_tail_rec_right = punit.mult_scalar_tail_rec_right[simplified]
lemmas punit_in_keys_monom_mult_le = punit.in_keys_monom_mult_le[simplified]
lemmas punit_in_keys_monom_mult_ge = punit.in_keys_monom_mult_ge[simplified]
lemmas lp_monom_mult = punit.lt_monom_mult[simplified]
lemmas tp_monom_mult = punit.tt_monom_mult[simplified]
end
subsection ‹@{term dgrad_p_set} and @{term dgrad_p_set_le}›
locale gd_term =
ordered_term pair_of_term term_of_pair ord ord_strict ord_term ord_term_strict
for pair_of_term::"'t ⇒ ('a::graded_dickson_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)
begin
sublocale gd_powerprod ..
lemma adds_term_antisym:
assumes "u adds⇩t v" and "v adds⇩t u"
shows "u = v"
using assms unfolding adds_term_def using adds_antisym by (metis term_of_pair_pair)
definition dgrad_p_set :: "('a ⇒ nat) ⇒ nat ⇒ ('t ⇒⇩0 'b::zero) set"
where "dgrad_p_set d m = {p. pp_of_term ` keys p ⊆ dgrad_set d m}"
definition dgrad_p_set_le :: "('a ⇒ nat) ⇒ (('t ⇒⇩0 'b) set) ⇒ (('t ⇒⇩0 'b::zero) set) ⇒ bool"
where "dgrad_p_set_le d F G ⟷ (dgrad_set_le d (pp_of_term ` Keys F) (pp_of_term ` Keys G))"
lemma in_dgrad_p_set_iff: "p ∈ dgrad_p_set d m ⟷ (∀v∈keys p. d (pp_of_term v) ≤ m)"
by (auto simp add: dgrad_p_set_def dgrad_set_def)
lemma dgrad_p_setI [intro]:
assumes "⋀v. v ∈ keys p ⟹ d (pp_of_term v) ≤ m"
shows "p ∈ dgrad_p_set d m"
using assms by (auto simp: in_dgrad_p_set_iff)
lemma dgrad_p_setD:
assumes "p ∈ dgrad_p_set d m" and "v ∈ keys p"
shows "d (pp_of_term v) ≤ m"
using assms by (simp only: in_dgrad_p_set_iff)
lemma zero_in_dgrad_p_set: "0 ∈ dgrad_p_set d m"
by (rule, simp)
lemma dgrad_p_set_zero [simp]: "dgrad_p_set (λ_. 0) m = UNIV"
by auto
lemma subset_dgrad_p_set_zero: "F ⊆ dgrad_p_set (λ_. 0) m"
by simp
lemma dgrad_p_set_subset:
assumes "m ≤ n"
shows "dgrad_p_set d m ⊆ dgrad_p_set d n"
using assms by (auto simp: dgrad_p_set_def dgrad_set_def)
lemma dgrad_p_setD_lp:
assumes "p ∈ dgrad_p_set d m" and "p ≠ 0"
shows "d (lp p) ≤ m"
by (rule dgrad_p_setD, fact, rule lt_in_keys, fact)
lemma dgrad_p_set_exhaust_expl:
assumes "finite F"
shows "F ⊆ dgrad_p_set d (Max (d ` pp_of_term ` Keys F))"
proof
fix f
assume "f ∈ F"
from assms have "finite (Keys F)" by (rule finite_Keys)
have fin: "finite (d ` pp_of_term ` Keys F)" by (intro finite_imageI, fact)
show "f ∈ dgrad_p_set d (Max (d ` pp_of_term ` Keys F))"
proof (rule dgrad_p_setI)
fix v
assume "v ∈ keys f"
from this ‹f ∈ F› have "v ∈ Keys F" by (rule in_KeysI)
hence "d (pp_of_term v) ∈ d ` pp_of_term ` Keys F" by simp
with fin show "d (pp_of_term v) ≤ Max (d ` pp_of_term ` Keys F)" by (rule Max_ge)
qed
qed
lemma dgrad_p_set_exhaust:
assumes "finite F"
obtains m where "F ⊆ dgrad_p_set d m"
proof
from assms show "F ⊆ dgrad_p_set d (Max (d ` pp_of_term ` Keys F))" by (rule dgrad_p_set_exhaust_expl)
qed
lemma dgrad_p_set_insert:
assumes "F ⊆ dgrad_p_set d m"
obtains n where "m ≤ n" and "f ∈ dgrad_p_set d n" and "F ⊆ dgrad_p_set d n"
proof -
have "finite {f}" by simp
then obtain m1 where "{f} ⊆ dgrad_p_set d m1" by (rule dgrad_p_set_exhaust)
hence "f ∈ dgrad_p_set d m1" by simp
define n where "n = ord_class.max m m1"
have "m ≤ n" and "m1 ≤ n" by (simp_all add: n_def)
from this(1) show ?thesis
proof
from ‹m1 ≤ n› have "dgrad_p_set d m1 ⊆ dgrad_p_set d n" by (rule dgrad_p_set_subset)
with ‹f ∈ dgrad_p_set d m1› show "f ∈ dgrad_p_set d n" ..
next
from ‹m ≤ n› have "dgrad_p_set d m ⊆ dgrad_p_set d n" by (rule dgrad_p_set_subset)
with assms show "F ⊆ dgrad_p_set d n" by (rule subset_trans)
qed
qed
lemma dgrad_p_set_leI:
assumes "⋀f. f ∈ F ⟹ dgrad_p_set_le d {f} G"
shows "dgrad_p_set_le d F G"
unfolding dgrad_p_set_le_def dgrad_set_le_def
proof
fix s
assume "s ∈ pp_of_term ` Keys F"
then obtain v where "v ∈ Keys F" and "s = pp_of_term v" ..
from this(1) obtain f where "f ∈ F" and "v ∈ keys f" by (rule in_KeysE)
from this(2) have "s ∈ pp_of_term ` Keys {f}" by (simp add: ‹s = pp_of_term v› Keys_insert)
from ‹f ∈ F› have "dgrad_p_set_le d {f} G" by (rule assms)
from this ‹s ∈ pp_of_term ` Keys {f}› show "∃t∈pp_of_term ` Keys G. d s ≤ d t"
unfolding dgrad_p_set_le_def dgrad_set_le_def ..
qed
lemma dgrad_p_set_le_trans [trans]:
assumes "dgrad_p_set_le d F G" and "dgrad_p_set_le d G H"
shows "dgrad_p_set_le d F H"
using assms unfolding dgrad_p_set_le_def by (rule dgrad_set_le_trans)
lemma dgrad_p_set_le_subset:
assumes "F ⊆ G"
shows "dgrad_p_set_le d F G"
unfolding dgrad_p_set_le_def by (rule dgrad_set_le_subset, rule image_mono, rule Keys_mono, fact)
lemma dgrad_p_set_leI_insert_keys:
assumes "dgrad_p_set_le d F G" and "dgrad_set_le d (pp_of_term ` keys f) (pp_of_term ` Keys G)"
shows "dgrad_p_set_le d (insert f F) G"
using assms by (simp add: dgrad_p_set_le_def Keys_insert dgrad_set_le_Un image_Un)
lemma dgrad_p_set_leI_insert:
assumes "dgrad_p_set_le d F G" and "dgrad_p_set_le d {f} G"
shows "dgrad_p_set_le d (insert f F) G"
using assms by (simp add: dgrad_p_set_le_def Keys_insert dgrad_set_le_Un image_Un)
lemma dgrad_p_set_leI_Un:
assumes "dgrad_p_set_le d F1 G" and "dgrad_p_set_le d F2 G"
shows "dgrad_p_set_le d (F1 ∪ F2) G"
using assms by (auto simp: dgrad_p_set_le_def dgrad_set_le_def Keys_Un)
lemma dgrad_p_set_le_dgrad_p_set:
assumes "dgrad_p_set_le d F G" and "G ⊆ dgrad_p_set d m"
shows "F ⊆ dgrad_p_set d m"
proof
fix f
assume "f ∈ F"
show "f ∈ dgrad_p_set d m"
proof (rule dgrad_p_setI)
fix v
assume "v ∈ keys f"
from this ‹f ∈ F› have "v ∈ Keys F" by (rule in_KeysI)
hence "pp_of_term v ∈ pp_of_term ` Keys F" by simp
with assms(1) obtain s where "s ∈ pp_of_term ` Keys G" and "d (pp_of_term v) ≤ d s"
unfolding dgrad_p_set_le_def by (rule dgrad_set_leE)
from this(1) obtain u where "u ∈ Keys G" and s: "s = pp_of_term u" ..
from this(1) obtain g where "g ∈ G" and "u ∈ keys g" by (rule in_KeysE)
from this(1) assms(2) have "g ∈ dgrad_p_set d m" ..
from this ‹u ∈ keys g› have "d s ≤ m" unfolding s by (rule dgrad_p_setD)
with ‹d (pp_of_term v) ≤ d s› show "d (pp_of_term v) ≤ m" by (rule le_trans)
qed
qed
lemma dgrad_p_set_le_except: "dgrad_p_set_le d {except p S} {p}"
by (auto simp add: dgrad_p_set_le_def Keys_insert keys_except intro: dgrad_set_le_subset)
lemma dgrad_p_set_le_tail: "dgrad_p_set_le d {tail p} {p}"
by (simp only: tail_def lower_def, fact dgrad_p_set_le_except)
lemma dgrad_p_set_le_plus: "dgrad_p_set_le d {p + q} {p, q}"
by (simp add: dgrad_p_set_le_def Keys_insert, rule dgrad_set_le_subset, rule image_mono, fact Poly_Mapping.keys_add)
lemma dgrad_p_set_le_uminus: "dgrad_p_set_le d {-p} {p}"
by (simp add: dgrad_p_set_le_def Keys_insert keys_uminus, fact dgrad_set_le_refl)
lemma dgrad_p_set_le_minus: "dgrad_p_set_le d {p - q} {p, q}"
by (simp add: dgrad_p_set_le_def Keys_insert, rule dgrad_set_le_subset, rule image_mono, fact keys_minus)
lemma dgrad_set_le_monom_mult:
assumes "dickson_grading d"
shows "dgrad_set_le d (pp_of_term ` keys (monom_mult c t p)) (insert t (pp_of_term ` keys p))"
proof (rule dgrad_set_leI)
fix s
assume "s ∈ pp_of_term ` keys (monom_mult c t p)"
with keys_monom_mult_subset have "s ∈ pp_of_term ` ((⊕) t ` keys p)" by fastforce
then obtain v where "v ∈ keys p" and s: "s = pp_of_term (t ⊕ v)" by fastforce
have "d s = ord_class.max (d t) (d (pp_of_term v))"
by (simp only: s pp_of_term_splus dickson_gradingD1[OF assms(1)])
hence "d s = d t ∨ d s = d (pp_of_term v)" by auto
thus "∃t∈insert t (pp_of_term ` keys p). d s ≤ d t"
proof
assume "d s = d t"
thus ?thesis by simp
next
assume "d s = d (pp_of_term v)"
show ?thesis
proof
from ‹d s = d (pp_of_term v)› show "d s ≤ d (pp_of_term v)" by simp
next
from ‹v ∈ keys p› show "pp_of_term v ∈ insert t (pp_of_term ` keys p)" by simp
qed
qed
qed
lemma dgrad_p_set_closed_plus:
assumes "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m"
shows "p + q ∈ dgrad_p_set d m"
proof -
from dgrad_p_set_le_plus have "{p + q} ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
from assms show "{p, q} ⊆ dgrad_p_set d m" by simp
qed
thus ?thesis by simp
qed
lemma dgrad_p_set_closed_uminus:
assumes "p ∈ dgrad_p_set d m"
shows "-p ∈ dgrad_p_set d m"
proof -
from dgrad_p_set_le_uminus have "{-p} ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
from assms show "{p} ⊆ dgrad_p_set d m" by simp
qed
thus ?thesis by simp
qed
lemma dgrad_p_set_closed_minus:
assumes "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m"
shows "p - q ∈ dgrad_p_set d m"
proof -
from dgrad_p_set_le_minus have "{p - q} ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
from assms show "{p, q} ⊆ dgrad_p_set d m" by simp
qed
thus ?thesis by simp
qed
lemma dgrad_p_set_closed_monom_mult:
assumes "dickson_grading d" and "d t ≤ m" and "p ∈ dgrad_p_set d m"
shows "monom_mult c t p ∈ dgrad_p_set d m"
proof (rule dgrad_p_setI)
fix v
assume "v ∈ keys (monom_mult c t p)"
hence "pp_of_term v ∈ pp_of_term ` keys (monom_mult c t p)" by simp
with dgrad_set_le_monom_mult[OF assms(1)] obtain s where "s ∈ insert t (pp_of_term ` keys p)"
and "d (pp_of_term v) ≤ d s" by (rule dgrad_set_leE)
from this(1) have "s = t ∨ s ∈ pp_of_term ` keys p" by simp
thus "d (pp_of_term v) ≤ m"
proof
assume "s = t"
with ‹d (pp_of_term v) ≤ d s› assms(2) show ?thesis by simp
next
assume "s ∈ pp_of_term ` keys p"
then obtain u where "u ∈ keys p" and "s = pp_of_term u" ..
from assms(3) this(1) have "d s ≤ m" unfolding ‹s = pp_of_term u› by (rule dgrad_p_setD)
with ‹d (pp_of_term v) ≤ d s› show ?thesis by (rule le_trans)
qed
qed
lemma dgrad_p_set_closed_monom_mult_zero:
assumes "p ∈ dgrad_p_set d m"
shows "monom_mult c 0 p ∈ dgrad_p_set d m"
proof (rule dgrad_p_setI)
fix v
assume "v ∈ keys (monom_mult c 0 p)"
hence "pp_of_term v ∈ pp_of_term ` keys (monom_mult c 0 p)" by simp
then obtain u where "u ∈ keys (monom_mult c 0 p)" and eq: "pp_of_term v = pp_of_term u" ..
from this(1) have "u ∈ keys p" by (metis keys_monom_multE splus_zero)
with assms have "d (pp_of_term u) ≤ m" by (rule dgrad_p_setD)
thus "d (pp_of_term v) ≤ m" by (simp only: eq)
qed
lemma dgrad_p_set_closed_except:
assumes "p ∈ dgrad_p_set d m"
shows "except p S ∈ dgrad_p_set d m"
by (rule dgrad_p_setI, rule dgrad_p_setD, rule assms, simp add: keys_except)
lemma dgrad_p_set_closed_tail:
assumes "p ∈ dgrad_p_set d m"
shows "tail p ∈ dgrad_p_set d m"
unfolding tail_def lower_def using assms by (rule dgrad_p_set_closed_except)
subsection ‹Dickson's Lemma for Sequences of Terms›
lemma Dickson_term:
assumes "dickson_grading d" and "finite K"
shows "almost_full_on (adds⇩t) {t. pp_of_term t ∈ dgrad_set d m ∧ component_of_term t ∈ K}"
(is "almost_full_on _ ?A")
proof (rule almost_full_onI)
fix seq :: "nat ⇒ 't"
assume *: "∀i. seq i ∈ ?A"
define seq' where "seq' = (λi. (pp_of_term (seq i), component_of_term (seq i)))"
have "pp_of_term ` ?A ⊆ {x. d x ≤ m}" by (auto dest: dgrad_setD)
moreover from assms(1) have "almost_full_on (adds) {x. d x ≤ m}" by (rule dickson_gradingD2)
ultimately have "almost_full_on (adds) (pp_of_term ` ?A)" by (rule almost_full_on_subset)
moreover have "almost_full_on (=) (component_of_term ` ?A)"
proof (rule eq_almost_full_on_finite_set)
have "component_of_term ` ?A ⊆ K" by blast
thus "finite (component_of_term ` ?A)" using assms(2) by (rule finite_subset)
qed
ultimately have "almost_full_on (prod_le (adds) (=)) (pp_of_term ` ?A × component_of_term ` ?A)"
by (rule almost_full_on_Sigma)
moreover from * have "⋀i. seq' i ∈ pp_of_term ` ?A × component_of_term ` ?A" by (simp add: seq'_def)
ultimately obtain i j where "i < j" and "prod_le (adds) (=) (seq' i) (seq' j)"
by (rule almost_full_onD)
from this(2) have "seq i adds⇩t seq j" by (simp add: seq'_def prod_le_def adds_term_def)
with ‹i < j› show "good (adds⇩t) seq" by (rule goodI)
qed
corollary Dickson_termE:
assumes "dickson_grading d" and "finite (component_of_term ` range (f::nat ⇒ 't))"
and "pp_of_term ` range f ⊆ dgrad_set d m"
obtains i j where "i < j" and "f i adds⇩t f j"
proof -
let ?A = "{t. pp_of_term t ∈ dgrad_set d m ∧ component_of_term t ∈ component_of_term ` range f}"
from assms(1, 2) have "almost_full_on (adds⇩t) ?A" by (rule Dickson_term)
moreover from assms(3) have "⋀i. f i ∈ ?A" by blast
ultimately obtain i j where "i < j" and "f i adds⇩t f j" by (rule almost_full_onD)
thus ?thesis ..
qed
lemma ex_finite_adds_term:
assumes "dickson_grading d" and "finite (component_of_term ` S)" and "pp_of_term ` S ⊆ dgrad_set d m"
obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. t adds⇩t s)"
proof -
let ?A = "{t. pp_of_term t ∈ dgrad_set d m ∧ component_of_term t ∈ component_of_term ` S}"
have "reflp ((adds⇩t)::'t ⇒ _)" by (simp add: reflp_def adds_term_refl)
moreover have "almost_full_on (adds⇩t) S"
proof (rule almost_full_on_subset)
from assms(3) show "S ⊆ ?A" by blast
next
from assms(1, 2) show "almost_full_on (adds⇩t) ?A" by (rule Dickson_term)
qed
ultimately obtain T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. t adds⇩t s)"
by (rule almost_full_on_finite_subsetE, blast)
thus ?thesis ..
qed
subsection ‹Well-foundedness›
definition dickson_less_v :: "('a ⇒ nat) ⇒ nat ⇒ 't ⇒ 't ⇒ bool"
where "dickson_less_v d m v u ⟷ (d (pp_of_term v) ≤ m ∧ d (pp_of_term u) ≤ m ∧ v ≺⇩t u)"
definition dickson_less_p :: "('a ⇒ nat) ⇒ nat ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b::zero) ⇒ bool"
where "dickson_less_p d m p q ⟷ ({p, q} ⊆ dgrad_p_set d m ∧ p ≺⇩p q)"
lemma dickson_less_vI:
assumes "d (pp_of_term v) ≤ m" and "d (pp_of_term u) ≤ m" and "v ≺⇩t u"
shows "dickson_less_v d m v u"
using assms by (simp add: dickson_less_v_def)
lemma dickson_less_vD1:
assumes "dickson_less_v d m v u"
shows "d (pp_of_term v) ≤ m"
using assms by (simp add: dickson_less_v_def)
lemma dickson_less_vD2:
assumes "dickson_less_v d m v u"
shows "d (pp_of_term u) ≤ m"
using assms by (simp add: dickson_less_v_def)
lemma dickson_less_vD3:
assumes "dickson_less_v d m v u"
shows "v ≺⇩t u"
using assms by (simp add: dickson_less_v_def)
lemma dickson_less_v_irrefl: "¬ dickson_less_v d m v v"
by (simp add: dickson_less_v_def)
lemma dickson_less_v_trans:
assumes "dickson_less_v d m v u" and "dickson_less_v d m u w"
shows "dickson_less_v d m v w"
using assms by (auto simp add: dickson_less_v_def)
lemma wf_dickson_less_v_aux1:
assumes "dickson_grading d" and "⋀i::nat. dickson_less_v d m (seq (Suc i)) (seq i)"
obtains i where "⋀j. j > i ⟹ component_of_term (seq j) < component_of_term (seq i)"
proof -
let ?Q = "pp_of_term ` range seq"
have "pp_of_term (seq 0) ∈ ?Q" by simp
with wf_dickson_less[OF assms(1)] obtain t where "t ∈ ?Q" and *: "⋀s. dickson_less d m s t ⟹ s ∉ ?Q"
by (rule wfE_min[to_pred], blast)
from this(1) obtain i where t: "t = pp_of_term (seq i)" by fastforce
show ?thesis
proof
fix j
assume "i < j"
with _ assms(2) have dlv: "dickson_less_v d m (seq j) (seq i)"
proof (rule transp_sequence)
from dickson_less_v_trans show "transp (dickson_less_v d m)" by (rule transpI)
qed
hence "seq j ≺⇩t seq i" by (rule dickson_less_vD3)
define s where "s = pp_of_term (seq j)"
have "pp_of_term (seq j) ∈ ?Q" by simp
hence "¬ dickson_less d m s t" unfolding s_def using * by blast
moreover from dlv have "d s ≤ m" and "d t ≤ m" unfolding s_def t
by (rule dickson_less_vD1, rule dickson_less_vD2)
ultimately have "t ≼ s" by (simp add: dickson_less_def)
show "component_of_term (seq j) < component_of_term (seq i)"
proof (rule ccontr, simp only: not_less)
assume "component_of_term (seq i) ≤ component_of_term (seq j)"
with ‹t ≼ s› have "seq i ≼⇩t seq j" unfolding s_def t by (rule ord_termI)
moreover from dlv have "seq j ≺⇩t seq i" by (rule dickson_less_vD3)
ultimately show False by simp
qed
qed
qed
lemma wf_dickson_less_v_aux2:
assumes "dickson_grading d" and "⋀i::nat. dickson_less_v d m (seq (Suc i)) (seq i)"
and "⋀i::nat. component_of_term (seq i) < k"
shows thesis
using assms(2, 3)
proof (induct k arbitrary: seq thesis rule: less_induct)
case (less k)
from assms(1) less(2) obtain i where *: "⋀j. j > i ⟹ component_of_term (seq j) < component_of_term (seq i)"
by (rule wf_dickson_less_v_aux1, blast)
define seq1 where "seq1 = (λj. seq (Suc (i + j)))"
from less(3) show ?case
proof (rule less(1))
fix j
show "dickson_less_v d m (seq1 (Suc j)) (seq1 j)" by (simp add: seq1_def, fact less(2))
next
fix j
show "component_of_term (seq1 j) < component_of_term (seq i)" by (simp add: seq1_def *)
qed
qed
lemma wf_dickson_less_v:
assumes "dickson_grading d"
shows "wfP (dickson_less_v d m)"
proof (rule wfP_chain, rule, elim exE)
fix seq::"nat ⇒ 't"
assume "∀i. dickson_less_v d m (seq (Suc i)) (seq i)"
hence *: "⋀i. dickson_less_v d m (seq (Suc i)) (seq i)" ..
with assms obtain i where **: "⋀j. j > i ⟹ component_of_term (seq j) < component_of_term (seq i)"
by (rule wf_dickson_less_v_aux1, blast)
define seq1 where "seq1 = (λj. seq (Suc (i + j)))"
from assms show False
proof (rule wf_dickson_less_v_aux2)
fix j
show "dickson_less_v d m (seq1 (Suc j)) (seq1 j)" by (simp add: seq1_def, fact *)
next
fix j
show "component_of_term (seq1 j) < component_of_term (seq i)" by (simp add: seq1_def **)
qed
qed
lemma dickson_less_v_zero: "dickson_less_v (λ_. 0) m = (≺⇩t)"
by (rule, rule, simp add: dickson_less_v_def)
lemma dickson_less_pI:
assumes "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m" and "p ≺⇩p q"
shows "dickson_less_p d m p q"
using assms by (simp add: dickson_less_p_def)
lemma dickson_less_pD1:
assumes "dickson_less_p d m p q"
shows "p ∈ dgrad_p_set d m"
using assms by (simp add: dickson_less_p_def)
lemma dickson_less_pD2:
assumes "dickson_less_p d m p q"
shows "q ∈ dgrad_p_set d m"
using assms by (simp add: dickson_less_p_def)
lemma dickson_less_pD3:
assumes "dickson_less_p d m p q"
shows "p ≺⇩p q"
using assms by (simp add: dickson_less_p_def)
lemma dickson_less_p_irrefl: "¬ dickson_less_p d m p p"
by (simp add: dickson_less_p_def)
lemma dickson_less_p_trans:
assumes "dickson_less_p d m p q" and "dickson_less_p d m q r"
shows "dickson_less_p d m p r"
using assms by (auto simp add: dickson_less_p_def)
lemma dickson_less_p_mono:
assumes "dickson_less_p d m p q" and "m ≤ n"
shows "dickson_less_p d n p q"
proof -
from assms(2) have "dgrad_p_set d m ⊆ dgrad_p_set d n" by (rule dgrad_p_set_subset)
moreover from assms(1) have "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m" and "p ≺⇩p q"
by (rule dickson_less_pD1, rule dickson_less_pD2, rule dickson_less_pD3)
ultimately have "p ∈ dgrad_p_set d n" and "q ∈ dgrad_p_set d n" by auto
from this ‹p ≺⇩p q› show ?thesis by (rule dickson_less_pI)
qed
lemma dickson_less_p_zero: "dickson_less_p (λ_. 0) m = (≺⇩p)"
by (rule, rule, simp add: dickson_less_p_def)
lemma wf_dickson_less_p_aux:
assumes "dickson_grading d"
assumes "x ∈ Q" and "∀y∈Q. y ≠ 0 ⟶ (y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) u)"
shows "∃p∈Q. (∀q∈Q. ¬ dickson_less_p d m q p)"
using assms(2) assms(3)
proof (induct u arbitrary: x Q rule: wfP_induct[OF wf_dickson_less_v, OF assms(1)])
fix u::'t and x::"'t ⇒⇩0 'b" and Q::"('t ⇒⇩0 'b) set"
assume hyp: "∀u0. dickson_less_v d m u0 u ⟶ (∀x0 Q0::('t ⇒⇩0 'b) set. x0 ∈ Q0 ⟶
(∀y∈Q0. y ≠ 0 ⟶ (y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) u0)) ⟶
(∃p∈Q0. ∀q∈Q0. ¬ dickson_less_p d m q p))"
assume "x ∈ Q"
assume "∀y∈Q. y ≠ 0 ⟶ (y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) u)"
hence bounded: "⋀y. y ∈ Q ⟹ y ≠ 0 ⟹ (y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) u)" by auto
show "∃p∈Q. ∀q∈Q. ¬ dickson_less_p d m q p"
proof (cases "0 ∈ Q")
case True
show ?thesis
proof (rule, rule, rule)
fix q::"'t ⇒⇩0 'b"
assume "dickson_less_p d m q 0"
hence "q ≺⇩p 0" by (rule dickson_less_pD3)
thus False using ord_p_zero_min[of q] by simp
next
from True show "0 ∈ Q" .
qed
next
case False
define Q1 where "Q1 = {lt p | p. p ∈ Q}"
from ‹x ∈ Q› have "lt x ∈ Q1" unfolding Q1_def by auto
with wf_dickson_less_v[OF assms(1)] obtain v
where "v ∈ Q1" and v_min_1: "⋀q. dickson_less_v d m q v ⟹ q ∉ Q1"
by (rule wfE_min[to_pred], auto)
have v_min: "⋀q. q ∈ Q ⟹ ¬ dickson_less_v d m (lt q) v"
proof -
fix q
assume "q ∈ Q"
hence "lt q ∈ Q1" unfolding Q1_def by auto
thus "¬ dickson_less_v d m (lt q) v" using v_min_1 by auto
qed
from ‹v ∈ Q1› obtain p where "lt p = v" and "p ∈ Q" unfolding Q1_def by auto
hence "p ≠ 0" using False by auto
with ‹p ∈ Q› have "p ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt p) u" by (rule bounded)
hence "p ∈ dgrad_p_set d m" and "dickson_less_v d m (lt p) u" by simp_all
moreover from this(1) ‹p ≠ 0› have "d (pp_of_term (lt p)) ≤ m" by (rule dgrad_p_setD_lp)
ultimately have "d (pp_of_term v) ≤ m" by (simp only: ‹lt p = v›)
define Q2 where "Q2 = {tail p | p. p ∈ Q ∧ lt p = v}"
from ‹p ∈ Q› ‹lt p = v› have "tail p ∈ Q2" unfolding Q2_def by auto
have "∀q∈Q2. q ≠ 0 ⟶ (q ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt q) (lt p))"
proof (intro ballI impI)
fix q
assume "q ∈ Q2"
then obtain q0 where q: "q = tail q0" and "lt q0 = lt p" and "q0 ∈ Q"
using ‹lt p = v› by (auto simp add: Q2_def)
assume "q ≠ 0"
hence "tail q0 ≠ 0" using ‹q = tail q0› by simp
hence "q0 ≠ 0" by auto
with ‹q0 ∈ Q› have "q0 ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt q0) u" by (rule bounded)
hence "q0 ∈ dgrad_p_set d m" and "dickson_less_v d m (lt q0) u" by simp_all
from this(1) have "q ∈ dgrad_p_set d m" unfolding q by (rule dgrad_p_set_closed_tail)
show "q ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt q) (lt p)"
proof
show "dickson_less_v d m (lt q) (lt p)"
proof (rule dickson_less_vI)
from ‹q ∈ dgrad_p_set d m› ‹q ≠ 0› show "d (pp_of_term (lt q)) ≤ m" by (rule dgrad_p_setD_lp)
next
from ‹dickson_less_v d m (lt p) u› show "d (pp_of_term (lt p)) ≤ m" by (rule dickson_less_vD1)
next
from lt_tail[OF ‹tail q0 ≠ 0›] ‹q = tail q0› ‹lt q0 = lt p› show "lt q ≺⇩t lt p" by simp
qed
qed fact
qed
with hyp ‹dickson_less_v d m (lt p) u› ‹tail p ∈ Q2› have "∃p∈Q2. ∀q∈Q2. ¬ dickson_less_p d m q p"
by blast
then obtain q where "q ∈ Q2" and q_min: "∀r∈Q2. ¬ dickson_less_p d m r q" ..
from ‹q ∈ Q2› obtain q0 where "q = tail q0" and "q0 ∈ Q" and "lt q0 = v" unfolding Q2_def by auto
from q_min ‹q = tail q0› have q0_tail_min: "⋀r. r ∈ Q2 ⟹ ¬ dickson_less_p d m r (tail q0)" by simp
from ‹q0 ∈ Q› show ?thesis
proof
show "∀r∈Q. ¬ dickson_less_p d m r q0"
proof (intro ballI notI)
fix r
assume "dickson_less_p d m r q0"
hence "r ∈ dgrad_p_set d m" and "q0 ∈ dgrad_p_set d m" and "r ≺⇩p q0"
by (rule dickson_less_pD1, rule dickson_less_pD2, rule dickson_less_pD3)
from this(3) have "lt r ≼⇩t lt q0" by (simp add: ord_p_lt)
with ‹lt q0 = v› have "lt r ≼⇩t v" by simp
assume "r ∈ Q"
hence "¬ dickson_less_v d m (lt r) v" by (rule v_min)
from False ‹r ∈ Q› have "r ≠ 0" using False by blast
with ‹r ∈ dgrad_p_set d m› have "d (pp_of_term (lt r)) ≤ m" by (rule dgrad_p_setD_lp)
have "¬ lt r ≺⇩t v"
proof
assume "lt r ≺⇩t v"
with ‹d (pp_of_term (lt r)) ≤ m› ‹d (pp_of_term v) ≤ m› have "dickson_less_v d m (lt r) v"
by (rule dickson_less_vI)
with ‹¬ dickson_less_v d m (lt r) v› show False ..
qed
with ‹lt r ≼⇩t v› have "lt r = v" by simp
with ‹r ∈ Q› have "tail r ∈ Q2" by (auto simp add: Q2_def)
have "dickson_less_p d m (tail r) (tail q0)"
proof (rule dickson_less_pI)
show "tail r ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_tail, fact)
next
show "tail q0 ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_tail, fact)
next
have "lt r = lt q0" by (simp only: ‹lt r = v› ‹lt q0 = v›)
from ‹r ≠ 0› this ‹r ≺⇩p q0› show "tail r ≺⇩p tail q0" by (rule ord_p_tail)
qed
with q0_tail_min[OF ‹tail r ∈ Q2›] show False ..
qed
qed
qed
qed
theorem wf_dickson_less_p:
assumes "dickson_grading d"
shows "wfP (dickson_less_p d m)"
proof (rule wfI_min[to_pred])
fix Q::"('t ⇒⇩0 'b) set" and x
assume "x ∈ Q"
show "∃z∈Q. ∀y. dickson_less_p d m y z ⟶ y ∉ Q"
proof (cases "0 ∈ Q")
case True
show ?thesis
proof (rule, rule, rule)
from True show "0 ∈ Q" .
next
fix q::"'t ⇒⇩0 'b"
assume "dickson_less_p d m q 0"
hence "q ≺⇩p 0" by (rule dickson_less_pD3)
thus "q ∉ Q" using ord_p_zero_min[of q] by simp
qed
next
case False
show ?thesis
proof (cases "Q ⊆ dgrad_p_set d m")
case True
let ?L = "lt ` Q"
from ‹x ∈ Q› have "lt x ∈ ?L" by simp
with wf_dickson_less_v[OF assms] obtain v where "v ∈ ?L"
and v_min: "⋀u. dickson_less_v d m u v ⟹ u ∉ ?L" by (rule wfE_min[to_pred], blast)
from this(1) obtain x1 where "x1 ∈ Q" and "v = lt x1" ..
from this(1) True False have "x1 ∈ dgrad_p_set d m" and "x1 ≠ 0" by auto
hence "d (pp_of_term v) ≤ m" unfolding ‹v = lt x1› by (rule dgrad_p_setD_lp)
define Q1 where "Q1 = {tail p | p. p ∈ Q ∧ lt p = v}"
from ‹x1 ∈ Q› have "tail x1 ∈ Q1" by (auto simp add: Q1_def ‹v = lt x1›)
with assms have "∃p∈Q1. ∀q∈Q1. ¬ dickson_less_p d m q p"
proof (rule wf_dickson_less_p_aux)
show "∀y∈Q1. y ≠ 0 ⟶ y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) v"
proof (intro ballI impI)
fix y
assume "y ∈ Q1" and "y ≠ 0"
from this(1) obtain y1 where "y1 ∈ Q" and "v = lt y1" and "y = tail y1" unfolding Q1_def
by blast
from this(1) True have "y1 ∈ dgrad_p_set d m" ..
hence "y ∈ dgrad_p_set d m" unfolding ‹y = tail y1› by (rule dgrad_p_set_closed_tail)
thus "y ∈ dgrad_p_set d m ∧ dickson_less_v d m (lt y) v"
proof
show "dickson_less_v d m (lt y) v"
proof (rule dickson_less_vI)
from ‹y ∈ dgrad_p_set d m› ‹y ≠ 0› show "d (pp_of_term (lt y)) ≤ m"
by (rule dgrad_p_setD_lp)
next
from ‹y ≠ 0› show "lt y ≺⇩t v" unfolding ‹v = lt y1› ‹y = tail y1› by (rule lt_tail)
qed fact
qed
qed
qed
then obtain p0 where "p0 ∈ Q1" and p0_min: "⋀q. q ∈ Q1 ⟹ ¬ dickson_less_p d m q p0" by blast
from this(1) obtain p where "p ∈ Q" and "v = lt p" and "p0 = tail p" unfolding Q1_def
by blast
from this(1) False have "p ≠ 0" by blast
show ?thesis
proof (intro bexI allI impI notI)
fix y
assume "y ∈ Q"
hence "y ≠ 0" using False by blast
assume "dickson_less_p d m y p"
hence "y ∈ dgrad_p_set d m" and "p ∈ dgrad_p_set d m" and "y ≺⇩p p"
by (rule dickson_less_pD1, rule dickson_less_pD2, rule dickson_less_pD3)
from this(3) have "y ≼⇩p p" by simp
hence "lt y ≼⇩t lt p" by (rule ord_p_lt)
moreover have "¬ lt y ≺⇩t lt p"
proof
assume "lt y ≺⇩t lt p"
have "dickson_less_v d m (lt y) v" unfolding ‹v = lt p›
by (rule dickson_less_vI, rule dgrad_p_setD_lp, fact+, rule dgrad_p_setD_lp, fact+)
hence "lt y ∉ ?L" by (rule v_min)
hence "y ∉ Q" by fastforce
from this ‹y ∈ Q› show False ..
qed
ultimately have "lt y = lt p" by simp
from ‹y ≠ 0› this ‹y ≺⇩p p› have "tail y ≺⇩p tail p" by (rule ord_p_tail)
from ‹y ∈ Q› have "tail y ∈ Q1" by (auto simp add: Q1_def ‹v = lt p› ‹lt y = lt p›[symmetric])
hence "¬ dickson_less_p d m (tail y) p0" by (rule p0_min)
moreover have "dickson_less_p d m (tail y) p0" unfolding ‹p0 = tail p›
by (rule dickson_less_pI, rule dgrad_p_set_closed_tail, fact, rule dgrad_p_set_closed_tail, fact+)
ultimately show False ..
qed fact
next
case False
then obtain q where "q ∈ Q" and "q ∉ dgrad_p_set d m" by blast
from this(1) show ?thesis
proof
show "∀y. dickson_less_p d m y q ⟶ y ∉ Q"
proof (intro allI impI)
fix y
assume "dickson_less_p d m y q"
hence "q ∈ dgrad_p_set d m" by (rule dickson_less_pD2)
with ‹q ∉ dgrad_p_set d m› show "y ∉ Q" ..
qed
qed
qed
qed
qed
corollary ord_p_minimum_dgrad_p_set:
assumes "dickson_grading d" and "x ∈ Q" and "Q ⊆ dgrad_p_set d m"
obtains q where "q ∈ Q" and "⋀y. y ≺⇩p q ⟹ y ∉ Q"
proof -
from assms(1) have "wfP (dickson_less_p d m)" by (rule wf_dickson_less_p)
from this assms(2) obtain q where "q ∈ Q" and *: "⋀y. dickson_less_p d m y q ⟹ y ∉ Q"
by (rule wfE_min[to_pred], auto)
from assms(3) ‹q ∈ Q› have "q ∈ dgrad_p_set d m" ..
from ‹q ∈ Q› show ?thesis
proof
fix y
assume "y ≺⇩p q"
show "y ∉ Q"
proof
assume "y ∈ Q"
with assms(3) have "y ∈ dgrad_p_set d m" ..
from this ‹q ∈ dgrad_p_set d m› ‹y ≺⇩p q› have "dickson_less_p d m y q"
by (rule dickson_less_pI)
hence "y ∉ Q" by (rule *)
from this ‹y ∈ Q› show False ..
qed
qed
qed
lemma ord_term_minimum_dgrad_set:
assumes "dickson_grading d" and "v ∈ V" and "pp_of_term ` V ⊆ dgrad_set d m"
obtains u where "u ∈ V" and "⋀w. w ≺⇩t u ⟹ w ∉ V"
proof -
from assms(1) have "wfP (dickson_less_v d m)" by (rule wf_dickson_less_v)
then obtain u where "u ∈ V" and *: "⋀w. dickson_less_v d m w u ⟹ w ∉ V" using assms(2)
by (rule wfE_min[to_pred]) blast
from this(1) have "pp_of_term u ∈ pp_of_term ` V" by (rule imageI)
with assms(3) have "pp_of_term u ∈ dgrad_set d m" ..
hence "d (pp_of_term u) ≤ m" by (rule dgrad_setD)
from ‹u ∈ V› show ?thesis
proof
fix w
assume "w ≺⇩t u"
show "w ∉ V"
proof
assume "w ∈ V"
hence "pp_of_term w ∈ pp_of_term ` V" by (rule imageI)
with assms(3) have "pp_of_term w ∈ dgrad_set d m" ..
hence "d (pp_of_term w) ≤ m" by (rule dgrad_setD)
from this ‹d (pp_of_term u) ≤ m› ‹w ≺⇩t u› have "dickson_less_v d m w u"
by (rule dickson_less_vI)
hence "w ∉ V" by (rule *)
from this ‹w ∈ V› show False ..
qed
qed
qed
end
subsection ‹More Interpretations›
context gd_powerprod
begin
sublocale punit: gd_term to_pair_unit fst "(≼)" "(≺)" "(≼)" "(≺)" ..
end
locale od_term =
ordered_term pair_of_term term_of_pair ord ord_strict ord_term ord_term_strict
for pair_of_term::"'t ⇒ ('a::dickson_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)
begin
sublocale gd_term ..
lemma ord_p_wf: "wfP (≺⇩p)"
proof -
from dickson_grading_zero have "wfP (dickson_less_p (λ_. 0) 0)" by (rule wf_dickson_less_p)
thus ?thesis by (simp only: dickson_less_p_zero)
qed
end
end