(* Author: Fabian Immler, Alexander Maletzky *) section ‹Type-Class-Multivariate Polynomials in Ordered Terms› theory MPoly_Type_Class_Ordered imports MPoly_Type_Class begin class the_min = linorder + fixes the_min::'a assumes the_min_min: "the_min ≤ x" text ‹Type class @{class the_min} guarantees that a least element exists. Instances of @{class the_min} should provide @{emph ‹computable›} definitions of that element.› instantiation nat :: the_min begin definition "the_min_nat = (0::nat)" instance by (standard, simp add: the_min_nat_def) end instantiation unit :: the_min begin definition "the_min_unit = ()" instance by (standard, simp add: the_min_unit_def) end locale ordered_term = term_powerprod pair_of_term term_of_pair + ordered_powerprod ord ord_strict + ord_term_lin: linorder ord_term ord_term_strict for pair_of_term::"'t ⇒ ('a::comm_powerprod × 'k::{the_min,wellorder})" and term_of_pair::"('a × 'k) ⇒ 't" and ord::"'a ⇒ 'a ⇒ bool" (infixl "≼" 50) and ord_strict (infixl "≺" 50) and ord_term::"'t ⇒ 't ⇒ bool" (infixl "≼⇩_{t}" 50) and ord_term_strict::"'t ⇒ 't ⇒ bool" (infixl "≺⇩_{t}" 50) + assumes splus_mono: "v ≼⇩_{t}w ⟹ t ⊕ v ≼⇩_{t}t ⊕ w" assumes ord_termI: "pp_of_term v ≼ pp_of_term w ⟹ component_of_term v ≤ component_of_term w ⟹ v ≼⇩_{t}w" begin abbreviation ord_term_conv (infixl "≽⇩_{t}" 50) where "ord_term_conv ≡ (≼⇩_{t})¯¯" abbreviation ord_term_strict_conv (infixl "≻⇩_{t}" 50) where "ord_term_strict_conv ≡ (≺⇩_{t})¯¯" text ‹The definition of @{locale ordered_term} only covers TOP and POT orderings. These two types of orderings are the only interesting ones.› definition "min_term ≡ term_of_pair (0, the_min)" lemma min_term_min: "min_term ≼⇩_{t}v" proof (rule ord_termI) show "pp_of_term min_term ≼ pp_of_term v" by (simp add: min_term_def zero_min term_simps) next show "component_of_term min_term ≤ component_of_term v" by (simp add: min_term_def the_min_min term_simps) qed lemma splus_mono_strict: assumes "v ≺⇩_{t}w" shows "t ⊕ v ≺⇩_{t}t ⊕ w" proof - from assms have "v ≼⇩_{t}w" and "v ≠ w" by simp_all from this(1) have "t ⊕ v ≼⇩_{t}t ⊕ w" by (rule splus_mono) moreover from ‹v ≠ w› have "t ⊕ v ≠ t ⊕ w" by (simp add: term_simps) ultimately show ?thesis using ord_term_lin.antisym_conv1 by blast qed lemma splus_mono_left: assumes "s ≼ t" shows "s ⊕ v ≼⇩_{t}t ⊕ v" proof (rule ord_termI, simp_all add: term_simps) from assms show "s + pp_of_term v ≼ t + pp_of_term v" by (rule plus_monotone) qed lemma splus_mono_strict_left: assumes "s ≺ t" shows "s ⊕ v ≺⇩_{t}t ⊕ v" proof - from assms have "s ≼ t" and "s ≠ t" by simp_all from this(1) have "s ⊕ v ≼⇩_{t}t ⊕ v" by (rule splus_mono_left) moreover from ‹s ≠ t› have "s ⊕ v ≠ t ⊕ v" by (simp add: term_simps) ultimately show ?thesis using ord_term_lin.antisym_conv1 by blast qed lemma ord_term_canc: assumes "t ⊕ v ≼⇩_{t}t ⊕ w" shows "v ≼⇩_{t}w" proof (rule ccontr) assume "¬ v ≼⇩_{t}w" hence "w ≺⇩_{t}v" by simp hence "t ⊕ w ≺⇩_{t}t ⊕ v" by (rule splus_mono_strict) with assms show False by simp qed lemma ord_term_strict_canc: assumes "t ⊕ v ≺⇩_{t}t ⊕ w" shows "v ≺⇩_{t}w" proof (rule ccontr) assume "¬ v ≺⇩_{t}w" hence "w ≼⇩_{t}v" by simp hence "t ⊕ w ≼⇩_{t}t ⊕ v" by (rule splus_mono) with assms show False by simp qed lemma ord_term_canc_left: assumes "t ⊕ v ≼⇩_{t}s ⊕ v" shows "t ≼ s" proof (rule ccontr) assume "¬ t ≼ s" hence "s ≺ t" by simp hence "s ⊕ v ≺⇩_{t}t ⊕ v" by (rule splus_mono_strict_left) with assms show False by simp qed lemma ord_term_strict_canc_left: assumes "t ⊕ v ≺⇩_{t}s ⊕ v" shows "t ≺ s" proof (rule ccontr) assume "¬ t ≺ s" hence "s ≼ t" by simp hence "s ⊕ v ≼⇩_{t}t ⊕ v" by (rule splus_mono_left) with assms show False by simp qed lemma ord_adds_term: assumes "u 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