diff --git a/thys/Groebner_Macaulay/Cone_Decomposition.thy b/thys/Groebner_Macaulay/Cone_Decomposition.thy --- a/thys/Groebner_Macaulay/Cone_Decomposition.thy +++ b/thys/Groebner_Macaulay/Cone_Decomposition.thy @@ -1,4893 +1,4893 @@ (* Author: Alexander Maletzky *) section \Cone Decompositions\ theory Cone_Decomposition imports Groebner_Bases.Groebner_PM Monomial_Module Hilbert_Function begin subsection \More Properties of Reduced Gr\"obner Bases\ context pm_powerprod begin lemmas reduced_GB_subset_monic_Polys = punit.reduced_GB_subset_monic_dgrad_p_set[simplified, OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum] lemmas reduced_GB_is_monomial_set_Polys = punit.reduced_GB_is_monomial_set_dgrad_p_set[simplified, OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum] lemmas is_red_reduced_GB_monomial_lt_GB_Polys = punit.is_red_reduced_GB_monomial_lt_GB_dgrad_p_set[simplified, OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum] lemmas reduced_GB_monomial_lt_reduced_GB_Polys = punit.reduced_GB_monomial_lt_reduced_GB_dgrad_p_set[simplified, OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum] end subsection \Quotient Ideals\ definition quot_set :: "'a set \ 'a \ 'a::semigroup_mult set" (infixl "\
" 55) where "quot_set A x = (*) x -` A" lemma quot_set_iff: "a \ A \
x \ x * a \ A" by (simp add: quot_set_def) lemma quot_setI: "x * a \ A \ a \ A \
x" by (simp only: quot_set_iff) lemma quot_setD: "a \ A \
x \ x * a \ A" by (simp only: quot_set_iff) lemma quot_set_quot_set [simp]: "A \
x \
y = A \
x * y" by (rule set_eqI) (simp add: quot_set_iff mult.assoc) lemma quot_set_one [simp]: "A \
(1::_::monoid_mult) = A" by (rule set_eqI) (simp add: quot_set_iff) lemma ideal_quot_set_ideal [simp]: "ideal (ideal B \
x) = (ideal B) \
(x::_::comm_ring)" proof show "ideal (ideal B \
x) \ ideal B \
x" proof fix b assume "b \ ideal (ideal B \
x)" thus "b \ ideal B \
x" proof (induct b rule: ideal.span_induct') case base show ?case by (simp add: quot_set_iff ideal.span_zero) next case (step b q p) hence "x * b \ ideal B" and "x * p \ ideal B" by (simp_all add: quot_set_iff) hence "x * b + q * (x * p) \ ideal B" by (intro ideal.span_add ideal.span_scale[where c=q]) thus ?case by (simp only: quot_set_iff algebra_simps) qed qed qed (fact ideal.span_superset) lemma quot_set_image_times: "inj ((*) x) \ ((*) x ` A) \
x = A" by (simp add: quot_set_def inj_vimage_image_eq) subsection \Direct Decompositions of Polynomial Rings\ context pm_powerprod begin definition normal_form :: "(('x \\<^sub>0 nat) \\<^sub>0 'a) set \ (('x \\<^sub>0 nat) \\<^sub>0 'a::field) \ (('x \\<^sub>0 nat) \\<^sub>0 'a::field)" where "normal_form F p = (SOME q. (punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p q \ \ punit.is_red (punit.reduced_GB F) q)" text \Of course, @{const normal_form} could be defined in a much more general context.\ context fixes X :: "'x set" assumes fin_X: "finite X" begin context fixes F :: "(('x \\<^sub>0 nat) \\<^sub>0 'a::field) set" assumes F_sub: "F \ P[X]" begin lemma normal_form: shows "(punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p (normal_form F p)" (is ?thesis1) and "\ punit.is_red (punit.reduced_GB F) (normal_form F p)" (is ?thesis2) proof - from fin_X F_sub have "finite (punit.reduced_GB F)" by (rule finite_reduced_GB_Polys) hence "wfP (punit.red (punit.reduced_GB F))\\" by (rule punit.red_wf_finite) then obtain q where "(punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p q" and "\ punit.is_red (punit.reduced_GB F) q" unfolding punit.is_red_def not_not by (rule relation.wf_imp_nf_ex) hence "(punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p q \ \ punit.is_red (punit.reduced_GB F) q" .. hence "?thesis1 \ ?thesis2" unfolding normal_form_def by (rule someI) thus ?thesis1 and ?thesis2 by simp_all qed lemma normal_form_unique: assumes "(punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p q" and "\ punit.is_red (punit.reduced_GB F) q" shows "normal_form F p = q" proof (rule relation.ChurchRosser_unique_final) from fin_X F_sub have "punit.is_Groebner_basis (punit.reduced_GB F)" by (rule reduced_GB_is_GB_Polys) thus "relation.is_ChurchRosser (punit.red (punit.reduced_GB F))" by (simp only: punit.is_Groebner_basis_def) next show "(punit.red (punit.reduced_GB F))\<^sup>*\<^sup>* p (normal_form F p)" by (rule normal_form) next have "\ punit.is_red (punit.reduced_GB F) (normal_form F p)" by (rule normal_form) thus "relation.is_final (punit.red (punit.reduced_GB F)) (normal_form F p)" by (simp add: punit.is_red_def) next from assms(2) show "relation.is_final (punit.red (punit.reduced_GB F)) q" by (simp add: punit.is_red_def) qed fact lemma normal_form_id_iff: "normal_form F p = p \ (\ punit.is_red (punit.reduced_GB F) p)" proof assume "normal_form F p = p" with normal_form(2)[of p] show "\ punit.is_red (punit.reduced_GB F) p" by simp next assume "\ punit.is_red (punit.reduced_GB F) p" with rtranclp.rtrancl_refl show "normal_form F p = p" by (rule normal_form_unique) qed lemma normal_form_normal_form: "normal_form F (normal_form F p) = normal_form F p" by (simp add: normal_form_id_iff normal_form) lemma normal_form_zero: "normal_form F 0 = 0" by (simp add: normal_form_id_iff punit.irred_0) lemma normal_form_map_scale: "normal_form F (c \ p) = c \ (normal_form F p)" by (intro normal_form_unique punit.is_irred_map_scale normal_form) (simp add: punit.map_scale_eq_monom_mult punit.red_rtrancl_mult normal_form) lemma normal_form_uminus: "normal_form F (- p) = - normal_form F p" by (intro normal_form_unique punit.red_rtrancl_uminus normal_form) (simp add: punit.is_red_uminus normal_form) lemma normal_form_plus_normal_form: "normal_form F (normal_form F p + normal_form F q) = normal_form F p + normal_form F q" by (intro normal_form_unique rtranclp.rtrancl_refl punit.is_irred_plus normal_form) lemma normal_form_minus_normal_form: "normal_form F (normal_form F p - normal_form F q) = normal_form F p - normal_form F q" by (intro normal_form_unique rtranclp.rtrancl_refl punit.is_irred_minus normal_form) lemma normal_form_ideal_Polys: "normal_form (ideal F \ P[X]) = normal_form F" proof - let ?F = "ideal F \ P[X]" from fin_X have eq: "punit.reduced_GB ?F = punit.reduced_GB F" proof (rule reduced_GB_unique_Polys) from fin_X F_sub show "punit.is_reduced_GB (punit.reduced_GB F)" by (rule reduced_GB_is_reduced_GB_Polys) next from fin_X F_sub have "ideal (punit.reduced_GB F) = ideal F" by (rule reduced_GB_ideal_Polys) also have "\ = ideal (ideal F \ P[X])" proof (intro subset_antisym ideal.span_subset_spanI) from ideal.span_superset[of F] F_sub have "F \ ideal F \ P[X]" by simp thus "F \ ideal (ideal F \ P[X])" using ideal.span_superset by (rule subset_trans) qed blast finally show "ideal (punit.reduced_GB F) = ideal (ideal F \ P[X])" . qed blast show ?thesis by (rule ext) (simp only: normal_form_def eq) qed lemma normal_form_diff_in_ideal: "p - normal_form F p \ ideal F" proof - from normal_form(1) have "p - normal_form F p \ ideal (punit.reduced_GB F)" by (rule punit.red_rtranclp_diff_in_pmdl[simplified]) also from fin_X F_sub have "\ = ideal F" by (rule reduced_GB_ideal_Polys) finally show ?thesis . qed lemma normal_form_zero_iff: "normal_form F p = 0 \ p \ ideal F" proof assume "normal_form F p = 0" with normal_form_diff_in_ideal[of p] show "p \ ideal F" by simp next assume "p \ ideal F" hence "p - (p - normal_form F p) \ ideal F" using normal_form_diff_in_ideal by (rule ideal.span_diff) also from fin_X F_sub have "\ = ideal (punit.reduced_GB F)" by (rule reduced_GB_ideal_Polys[symmetric]) finally have *: "normal_form F p \ ideal (punit.reduced_GB F)" by simp show "normal_form F p = 0" proof (rule ccontr) from fin_X F_sub have "punit.is_Groebner_basis (punit.reduced_GB F)" by (rule reduced_GB_is_GB_Polys) moreover note * moreover assume "normal_form F p \ 0" ultimately obtain g where "g \ punit.reduced_GB F" and "g \ 0" and a: "lpp g adds lpp (normal_form F p)" by (rule punit.GB_adds_lt[simplified]) note this(1, 2) moreover from \normal_form F p \ 0\ have "lpp (normal_form F p) \ keys (normal_form F p)" by (rule punit.lt_in_keys) ultimately have "punit.is_red (punit.reduced_GB F) (normal_form F p)" using a by (rule punit.is_red_addsI[simplified]) with normal_form(2) show False .. qed qed lemma normal_form_eq_iff: "normal_form F p = normal_form F q \ p - q \ ideal F" proof - have "p - q - (normal_form F p - normal_form F q) = (p - normal_form F p) - (q - normal_form F q)" by simp also from normal_form_diff_in_ideal normal_form_diff_in_ideal have "\ \ ideal F" by (rule ideal.span_diff) finally have *: "p - q - (normal_form F p - normal_form F q) \ ideal F" . show ?thesis proof assume "normal_form F p = normal_form F q" with * show "p - q \ ideal F" by simp next assume "p - q \ ideal F" hence "p - q - (p - q - (normal_form F p - normal_form F q)) \ ideal F" using * by (rule ideal.span_diff) hence "normal_form F (normal_form F p - normal_form F q) = 0" by (simp add: normal_form_zero_iff) thus "normal_form F p = normal_form F q" by (simp add: normal_form_minus_normal_form) qed qed lemma Polys_closed_normal_form: assumes "p \ P[X]" shows "normal_form F p \ P[X]" proof - from fin_X F_sub have "punit.reduced_GB F \ P[X]" by (rule reduced_GB_Polys) with fin_X show ?thesis using assms normal_form(1) by (rule punit.dgrad_p_set_closed_red_rtrancl[OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum]) qed lemma image_normal_form_iff: "p \ normal_form F ` P[X] \ (p \ P[X] \ \ punit.is_red (punit.reduced_GB F) p)" proof assume "p \ normal_form F ` P[X]" then obtain q where "q \ P[X]" and p: "p = normal_form F q" .. from this(1) show "p \ P[X] \ \ punit.is_red (punit.reduced_GB F) p" unfolding p by (intro conjI Polys_closed_normal_form normal_form) next assume "p \ P[X] \ \ punit.is_red (punit.reduced_GB F) p" hence "p \ P[X]" and "\ punit.is_red (punit.reduced_GB F) p" by simp_all from this(2) have "normal_form F p = p" by (simp add: normal_form_id_iff) from this[symmetric] \p \ P[X]\ show "p \ normal_form F ` P[X]" by (rule image_eqI) qed end lemma direct_decomp_ideal_insert: fixes F and f defines "I \ ideal (insert f F)" defines "L \ (ideal F \
f) \ P[X]" assumes "F \ P[X]" and "f \ P[X]" shows "direct_decomp (I \ P[X]) [ideal F \ P[X], (*) f ` normal_form L ` P[X]]" (is "direct_decomp _ ?ss") proof (rule direct_decompI_alt) fix qs assume "qs \ listset ?ss" then obtain x y where x: "x \ ideal F \ P[X]" and y: "y \ (*) f ` normal_form L ` P[X]" and qs: "qs = [x, y]" by (rule listset_doubletonE) have "sum_list qs = x + y" by (simp add: qs) also have "\ \ I \ P[X]" unfolding I_def proof (intro IntI ideal.span_add Polys_closed_plus) have "ideal F \ ideal (insert f F)" by (rule ideal.span_mono) blast with x show "x \ ideal (insert f F)" and "x \ P[X]" by blast+ next from y obtain p where "p \ P[X]" and y: "y = f * normal_form L p" by blast have "f \ ideal (insert f F)" by (rule ideal.span_base) simp hence "normal_form L p * f \ ideal (insert f F)" by (rule ideal.span_scale) thus "y \ ideal (insert f F)" by (simp only: mult.commute y) have "L \ P[X]" by (simp add: L_def) hence "normal_form L p \ P[X]" using \p \ P[X]\ by (rule Polys_closed_normal_form) with assms(4) show "y \ P[X]" unfolding y by (rule Polys_closed_times) qed finally show "sum_list qs \ I \ P[X]" . next fix a assume "a \ I \ P[X]" hence "a \ I" and "a \ P[X]" by simp_all from assms(3, 4) have "insert f F \ P[X]" by simp then obtain F0 q0 where "F0 \ insert f F" and "finite F0" and q0: "\f0. q0 f0 \ P[X]" and a: "a = (\f0\F0. q0 f0 * f0)" using \a \ P[X]\ \a \ I\ unfolding I_def by (rule in_idealE_Polys) blast obtain q a' where a': "a' \ ideal F" and "a' \ P[X]" and "q \ P[X]" and a: "a = q * f + a'" proof (cases "f \ F0") case True with \F0 \ insert f F\ have "F0 - {f} \ F" by blast show ?thesis proof have "(\f0\F0 - {f}. q0 f0 * f0) \ ideal (F0 - {f})" by (rule ideal.sum_in_spanI) also from \F0 - {f} \ F\ have "\ \ ideal F" by (rule ideal.span_mono) finally show "(\f0\F0 - {f}. q0 f0 * f0) \ ideal F" . next show "(\f0\F0 - {f}. q0 f0 * f0) \ P[X]" proof (intro Polys_closed_sum Polys_closed_times q0) fix f0 assume "f0 \ F0 - {f}" also have "\ \ F0" by blast also have "\ \ insert f F" by fact also have "\ \ P[X]" by fact finally show "f0 \ P[X]" . qed next from \finite F0\ True show "a = q0 f * f + (\f0\F0 - {f}. q0 f0 * f0)" by (simp only: a sum.remove) qed fact next case False with \F0 \ insert f F\ have "F0 \ F" by blast show ?thesis proof have "a \ ideal F0" unfolding a by (rule ideal.sum_in_spanI) also from \F0 \ F\ have "\ \ ideal F" by (rule ideal.span_mono) finally show "a \ ideal F" . next show "a = 0 * f + a" by simp qed (fact \a \ P[X]\, fact zero_in_Polys) qed let ?a = "f * (normal_form L q)" have "L \ P[X]" by (simp add: L_def) hence "normal_form L q \ P[X]" using \q \ P[X]\ by (rule Polys_closed_normal_form) with assms(4) have "?a \ P[X]" by (rule Polys_closed_times) from \L \ P[X]\ have "q - normal_form L q \ ideal L" by (rule normal_form_diff_in_ideal) also have "\ \ ideal (ideal F \
f)" unfolding L_def by (rule ideal.span_mono) blast finally have "f * (q - normal_form L q) \ ideal F" by (simp add: quot_set_iff) with \a' \ ideal F\ have "a' + f * (q - normal_form L q) \ ideal F" by (rule ideal.span_add) hence "a - ?a \ ideal F" by (simp add: a algebra_simps) define qs where "qs = [a - ?a, ?a]" show "\!qs\listset ?ss. a = sum_list qs" proof (intro ex1I conjI allI impI) have "a - ?a \ ideal F \ P[X]" proof from assms(4) \a \ P[X]\ \normal_form L q \ P[X]\ show "a - ?a \ P[X]" by (intro Polys_closed_minus Polys_closed_times) qed fact moreover from \q \ P[X]\ have "?a \ (*) f ` normal_form L ` P[X]" by (intro imageI) ultimately show "qs \ listset ?ss" using qs_def by (rule listset_doubletonI) next fix qs0 assume "qs0 \ listset ?ss \ a = sum_list qs0" hence "qs0 \ listset ?ss" and "a = sum_list qs0" by simp_all from this(1) obtain x y where "x \ ideal F \ P[X]" and "y \ (*) f ` normal_form L ` P[X]" and qs0: "qs0 = [x, y]" by (rule listset_doubletonE) from this(2) obtain a0 where "a0 \ P[X]" and y: "y = f * normal_form L a0" by blast from \x \ ideal F \ P[X]\ have "x \ ideal F" by simp have x: "x = a - y" by (simp add: \a = sum_list qs0\ qs0) have "f * (normal_form L q - normal_form L a0) = x - (a - ?a)" by (simp add: x y a algebra_simps) also from \x \ ideal F\ \a - ?a \ ideal F\ have "\ \ ideal F" by (rule ideal.span_diff) finally have "normal_form L q - normal_form L a0 \ ideal F \
f" by (rule quot_setI) moreover from \L \ P[X]\ \q \ P[X]\ \a0 \ P[X]\ have "normal_form L q - normal_form L a0 \ P[X]" by (intro Polys_closed_minus Polys_closed_normal_form) ultimately have "normal_form L q - normal_form L a0 \ L" by (simp add: L_def) also have "\ \ ideal L" by (fact ideal.span_superset) finally have "normal_form L q - normal_form L a0 = 0" using \L \ P[X]\ by (simp only: normal_form_minus_normal_form flip: normal_form_zero_iff) thus "qs0 = qs" by (simp add: qs0 qs_def x y) qed (simp_all add: qs_def) qed corollary direct_decomp_ideal_normal_form: assumes "F \ P[X]" shows "direct_decomp P[X] [ideal F \ P[X], normal_form F ` P[X]]" proof - from assms one_in_Polys have "direct_decomp (ideal (insert 1 F) \ P[X]) [ideal F \ P[X], (*) 1 ` normal_form ((ideal F \
1) \ P[X]) ` P[X]]" by (rule direct_decomp_ideal_insert) moreover have "ideal (insert 1 F) = UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one ideal.span_base) moreover from refl have "((*) 1 \ normal_form F) ` P[X] = normal_form F ` P[X]" by (rule image_cong) simp ultimately show ?thesis using assms by (simp add: image_comp normal_form_ideal_Polys) qed end subsection \Basic Cone Decompositions\ definition cone :: "((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) \ (('x \\<^sub>0 nat) \\<^sub>0 'a::comm_semiring_0) set" where "cone hU = (*) (fst hU) ` P[snd hU]" lemma coneI: "p = a * h \ a \ P[U] \ p \ cone (h, U)" by (auto simp: cone_def mult.commute[of a]) lemma coneE: assumes "p \ cone (h, U)" obtains a where "a \ P[U]" and "p = a * h" using assms by (auto simp: cone_def mult.commute) lemma cone_empty: "cone (h, {}) = range (\c. c \ h)" by (auto simp: Polys_empty map_scale_eq_times intro: coneI elim!: coneE) lemma cone_zero [simp]: "cone (0, U) = {0}" by (auto simp: cone_def intro: zero_in_Polys) lemma cone_one [simp]: "cone (1::_ \\<^sub>0 'a::comm_semiring_1, U) = P[U]" by (auto simp: cone_def) lemma zero_in_cone: "0 \ cone hU" by (auto simp: cone_def intro!: image_eqI zero_in_Polys) corollary empty_not_in_map_cone: "{} \ set (map cone ps)" using zero_in_cone by fastforce lemma tip_in_cone: "h \ cone (h::_ \\<^sub>0 _::comm_semiring_1, U)" using _ one_in_Polys by (rule coneI) simp lemma cone_closed_plus: assumes "a \ cone hU" and "b \ cone hU" shows "a + b \ cone hU" proof - obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with assms have "a \ cone (h, U)" and "b \ cone (h, U)" by simp_all from this(1) obtain a' where "a' \ P[U]" and a: "a = a' * h" by (rule coneE) from \b \ cone (h, U)\ obtain b' where "b' \ P[U]" and b: "b = b' * h" by (rule coneE) have "a + b = (a' + b') * h" by (simp only: a b algebra_simps) moreover from \a' \ P[U]\ \b' \ P[U]\ have "a' + b' \ P[U]" by (rule Polys_closed_plus) ultimately show ?thesis unfolding hU by (rule coneI) qed lemma cone_closed_uminus: assumes "(a::_ \\<^sub>0 _::comm_ring) \ cone hU" shows "- a \ cone hU" proof - obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with assms have "a \ cone (h, U)" by simp from this(1) obtain a' where "a' \ P[U]" and a: "a = a' * h" by (rule coneE) have "- a = (- a') * h" by (simp add: a) moreover from \a' \ P[U]\ have "- a' \ P[U]" by (rule Polys_closed_uminus) ultimately show ?thesis unfolding hU by (rule coneI) qed lemma cone_closed_minus: assumes "(a::_ \\<^sub>0 _::comm_ring) \ cone hU" and "b \ cone hU" shows "a - b \ cone hU" proof - from assms(2) have "- b \ cone hU" by (rule cone_closed_uminus) with assms(1) have "a + (- b) \ cone hU" by (rule cone_closed_plus) thus ?thesis by simp qed lemma cone_closed_times: assumes "a \ cone (h, U)" and "q \ P[U]" shows "q * a \ cone (h, U)" proof - from assms(1) obtain a' where "a' \ P[U]" and a: "a = a' * h" by (rule coneE) have "q * a = (q * a') * h" by (simp only: a ac_simps) moreover from assms(2) \a' \ P[U]\ have "q * a' \ P[U]" by (rule Polys_closed_times) ultimately show ?thesis by (rule coneI) qed corollary cone_closed_monom_mult: assumes "a \ cone (h, U)" and "t \ .[U]" shows "punit.monom_mult c t a \ cone (h, U)" proof - from assms(2) have "monomial c t \ P[U]" by (rule Polys_closed_monomial) with assms(1) have "monomial c t * a \ cone (h, U)" by (rule cone_closed_times) thus ?thesis by (simp only: times_monomial_left) qed lemma coneD: assumes "p \ cone (h, U)" and "p \ 0" shows "lpp h adds lpp (p::_ \\<^sub>0 _::{comm_semiring_0,semiring_no_zero_divisors})" proof - from assms(1) obtain a where p: "p = a * h" by (rule coneE) with assms(2) have "a \ 0" and "h \ 0" by auto hence "lpp p = lpp a + lpp h" unfolding p by (rule lp_times) also have "\ = lpp h + lpp a" by (rule add.commute) finally show ?thesis by (rule addsI) qed lemma cone_mono_1: assumes "h' \ P[U]" shows "cone (h' * h, U) \ cone (h, U)" proof fix p assume "p \ cone (h' * h, U)" then obtain a' where "a' \ P[U]" and "p = a' * (h' * h)" by (rule coneE) from this(2) have "p = a' * h' * h" by (simp only: mult.assoc) moreover from \a' \ P[U]\ assms have "a' * h' \ P[U]" by (rule Polys_closed_times) ultimately show "p \ cone (h, U)" by (rule coneI) qed lemma cone_mono_2: assumes "U1 \ U2" shows "cone (h, U1) \ cone (h, U2)" proof from assms have "P[U1] \ P[U2]" by (rule Polys_mono) fix p assume "p \ cone (h, U1)" then obtain a where "a \ P[U1]" and "p = a * h" by (rule coneE) note this(2) moreover from \a \ P[U1]\ \P[U1] \ P[U2]\ have "a \ P[U2]" .. ultimately show "p \ cone (h, U2)" by (rule coneI) qed lemma cone_subsetD: assumes "cone (h1, U1) \ cone (h2::_ \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}, U2)" shows "h2 dvd h1" and "h1 \ 0 \ U1 \ U2" proof - from tip_in_cone assms have "h1 \ cone (h2, U2)" .. then obtain a1' where "a1' \ P[U2]" and h1: "h1 = a1' * h2" by (rule coneE) from this(2) have "h1 = h2 * a1'" by (simp only: mult.commute) thus "h2 dvd h1" .. assume "h1 \ 0" with h1 have "a1' \ 0" and "h2 \ 0" by auto show "U1 \ U2" proof fix x assume "x \ U1" hence "monomial (1::'a) (Poly_Mapping.single x 1) \ P[U1]" (is "?p \ _") by (intro Polys_closed_monomial PPs_closed_single) with refl have "?p * h1 \ cone (h1, U1)" by (rule coneI) hence "?p * h1 \ cone (h2, U2)" using assms .. then obtain a where "a \ P[U2]" and "?p * h1 = a * h2" by (rule coneE) from this(2) have "(?p * a1') * h2 = a * h2" by (simp only: h1 ac_simps) hence "?p * a1' = a" using \h2 \ 0\ by (rule times_canc_right) with \a \ P[U2]\ have "a1' * ?p \ P[U2]" by (simp add: mult.commute) hence "?p \ P[U2]" using \a1' \ P[U2]\ \a1' \ 0\ by (rule times_in_PolysD) thus "x \ U2" by (simp add: Polys_def PPs_def) qed qed lemma cone_subset_PolysD: assumes "cone (h::_ \\<^sub>0 'a::{comm_semiring_1,semiring_no_zero_divisors}, U) \ P[X]" shows "h \ P[X]" and "h \ 0 \ U \ X" proof - from tip_in_cone assms show "h \ P[X]" .. assume "h \ 0" show "U \ X" proof fix x assume "x \ U" hence "monomial (1::'a) (Poly_Mapping.single x 1) \ P[U]" (is "?p \ _") by (intro Polys_closed_monomial PPs_closed_single) with refl have "?p * h \ cone (h, U)" by (rule coneI) hence "?p * h \ P[X]" using assms .. hence "h * ?p \ P[X]" by (simp only: mult.commute) hence "?p \ P[X]" using \h \ P[X]\ \h \ 0\ by (rule times_in_PolysD) thus "x \ X" by (simp add: Polys_def PPs_def) qed qed lemma cone_subset_PolysI: assumes "h \ P[X]" and "h \ 0 \ U \ X" shows "cone (h, U) \ P[X]" proof (cases "h = 0") case True thus ?thesis by (simp add: zero_in_Polys) next case False hence "U \ X" by (rule assms(2)) hence "P[U] \ P[X]" by (rule Polys_mono) show ?thesis proof fix a assume "a \ cone (h, U)" then obtain q where "q \ P[U]" and a: "a = q * h" by (rule coneE) from this(1) \P[U] \ P[X]\ have "q \ P[X]" .. from this assms(1) show "a \ P[X]" unfolding a by (rule Polys_closed_times) qed qed lemma cone_image_times: "(*) a ` cone (h, U) = cone (a * h, U)" by (auto simp: ac_simps image_image intro!: image_eqI coneI elim!: coneE) lemma cone_image_times': "(*) a ` cone hU = cone (apfst ((*) a) hU)" proof - obtain h U where "hU = (h, U)" using prod.exhaust by blast thus ?thesis by (simp add: cone_image_times) qed lemma homogeneous_set_coneI: assumes "homogeneous h" shows "homogeneous_set (cone (h, U))" proof (rule homogeneous_setI) fix a n assume "a \ cone (h, U)" then obtain q where "q \ P[U]" and a: "a = q * h" by (rule coneE) from this(1) show "hom_component a n \ cone (h, U)" unfolding a proof (induct q rule: poly_mapping_plus_induct) case 1 show ?case by (simp add: zero_in_cone) next case (2 p c t) have "p \ P[U]" proof (intro PolysI subsetI) fix s assume "s \ keys p" moreover from 2(2) this have "s \ keys (monomial c t)" by auto ultimately have "s \ keys (monomial c t + p)" by (rule in_keys_plusI2) also from 2(4) have "\ \ .[U]" by (rule PolysD) finally show "s \ .[U]" . qed hence *: "hom_component (p * h) n \ cone (h, U)" by (rule 2(3)) from 2(1) have "t \ keys (monomial c t)" by simp hence "t \ keys (monomial c t + p)" using 2(2) by (rule in_keys_plusI1) also from 2(4) have "\ \ .[U]" by (rule PolysD) finally have "monomial c t \ P[U]" by (rule Polys_closed_monomial) with refl have "monomial c t * h \ cone (h, U)" (is "?h \ _") by (rule coneI) from assms have "homogeneous ?h" by (simp add: homogeneous_times) hence "hom_component ?h n = (?h when n = poly_deg ?h)" by (rule hom_component_of_homogeneous) with \?h \ cone (h, U)\ have **: "hom_component ?h n \ cone (h, U)" by (simp add: when_def zero_in_cone) have "hom_component ((monomial c t + p) * h) n = hom_component ?h n + hom_component (p * h) n" by (simp only: distrib_right hom_component_plus) also from ** * have "\ \ cone (h, U)" by (rule cone_closed_plus) finally show ?case . qed qed lemma subspace_cone: "phull.subspace (cone hU)" using zero_in_cone cone_closed_plus proof (rule phull.subspaceI) fix c a assume "a \ cone hU" moreover obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast ultimately have "a \ cone (h, U)" by simp thus "c \ a \ cone hU" unfolding hU punit.map_scale_eq_monom_mult using zero_in_PPs by (rule cone_closed_monom_mult) qed lemma direct_decomp_cone_insert: fixes h :: "_ \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}" assumes "x \ U" shows "direct_decomp (cone (h, insert x U)) [cone (h, U), cone (monomial 1 (Poly_Mapping.single x (Suc 0)) * h, insert x U)]" proof - let ?x = "Poly_Mapping.single x (Suc 0)" define xx where "xx = monomial (1::'a) ?x" show "direct_decomp (cone (h, insert x U)) [cone (h, U), cone (xx * h, insert x U)]" (is "direct_decomp _ ?ss") proof (rule direct_decompI_alt) fix qs assume "qs \ listset ?ss" then obtain a b where "a \ cone (h, U)" and b: "b \ cone (xx * h, insert x U)" and qs: "qs = [a, b]" by (rule listset_doubletonE) note this(1) also have "cone (h, U) \ cone (h, insert x U)" by (rule cone_mono_2) blast finally have a: "a \ cone (h, insert x U)" . have "cone (xx * h, insert x U) \ cone (h, insert x U)" by (rule cone_mono_1) (simp add: xx_def Polys_def PPs_closed_single) with b have "b \ cone (h, insert x U)" .. with a have "a + b \ cone (h, insert x U)" by (rule cone_closed_plus) thus "sum_list qs \ cone (h, insert x U)" by (simp add: qs) next fix a assume "a \ cone (h, insert x U)" then obtain q where "q \ P[insert x U]" and a: "a = q * h" by (rule coneE) define qU where "qU = except q (- .[U])" define qx where "qx = except q .[U]" have q: "q = qU + qx" by (simp only: qU_def qx_def add.commute flip: except_decomp) have "qU \ P[U]" by (rule PolysI) (simp add: qU_def keys_except) have x_adds: "?x adds t" if "t \ keys qx" for t unfolding adds_poly_mapping le_fun_def proof fix y show "lookup ?x y \ lookup t y" proof (cases "y = x") case True from that have "t \ keys q" and "t \ .[U]" by (simp_all add: qx_def keys_except) from \q \ P[insert x U]\ have "keys q \ .[insert x U]" by (rule PolysD) with \t \ keys q\ have "t \ .[insert x U]" .. hence "keys t \ insert x U" by (rule PPsD) moreover from \t \ .[U]\ have "\ keys t \ U" by (simp add: PPs_def) ultimately have "x \ keys t" by blast thus ?thesis by (simp add: lookup_single True in_keys_iff) next case False thus ?thesis by (simp add: lookup_single) qed qed define qx' where "qx' = Poly_Mapping.map_key ((+) ?x) qx" have lookup_qx': "lookup qx' = (\t. lookup qx (?x + t))" by (rule ext) (simp add: qx'_def map_key.rep_eq) have "qx' * xx = punit.monom_mult 1 ?x qx'" by (simp only: xx_def mult.commute flip: times_monomial_left) also have "\ = qx" by (auto simp: punit.lookup_monom_mult lookup_qx' add.commute[of ?x] adds_minus simp flip: not_in_keys_iff_lookup_eq_zero dest: x_adds intro!: poly_mapping_eqI) finally have qx: "qx = qx' * xx" by (rule sym) have "qx' \ P[insert x U]" proof (intro PolysI subsetI) fix t assume "t \ keys qx'" hence "t + ?x \ keys qx" by (simp only: lookup_qx' in_keys_iff not_False_eq_True add.commute) also have "\ \ keys q" by (auto simp: qx_def keys_except) also from \q \ P[insert x U]\ have "\ \ .[insert x U]" by (rule PolysD) finally have "(t + ?x) - ?x \ .[insert x U]" by (rule PPs_closed_minus) thus "t \ .[insert x U]" by simp qed define qs where "qs = [qU * h, qx' * (xx * h)]" show "\!qs\listset ?ss. a = sum_list qs" proof (intro ex1I conjI allI impI) from refl \qU \ P[U]\ have "qU * h \ cone (h, U)" by (rule coneI) moreover from refl \qx' \ P[insert x U]\ have "qx' * (xx * h) \ cone (xx * h, insert x U)" by (rule coneI) ultimately show "qs \ listset ?ss" using qs_def by (rule listset_doubletonI) next fix qs0 assume "qs0 \ listset ?ss \ a = sum_list qs0" hence "qs0 \ listset ?ss" and a0: "a = sum_list qs0" by simp_all from this(1) obtain p1 p2 where "p1 \ cone (h, U)" and p2: "p2 \ cone (xx * h, insert x U)" and qs0: "qs0 = [p1, p2]" by (rule listset_doubletonE) from this(1) obtain qU0 where "qU0 \ P[U]" and p1: "p1 = qU0 * h" by (rule coneE) from p2 obtain qx0 where p2: "p2 = qx0 * (xx * h)" by (rule coneE) show "qs0 = qs" proof (cases "h = 0") case True thus ?thesis by (simp add: qs_def qs0 p1 p2) next case False from a0 have "(qU - qU0) * h = (qx0 - qx') * xx * h" by (simp add: a qs0 p1 p2 q qx algebra_simps) hence eq: "qU - qU0 = (qx0 - qx') * xx" using False by (rule times_canc_right) have "qx0 = qx'" proof (rule ccontr) assume "qx0 \ qx'" hence "qx0 - qx' \ 0" by simp moreover have "xx \ 0" by (simp add: xx_def monomial_0_iff) ultimately have "lpp ((qx0 - qx') * xx) = lpp (qx0 - qx') + lpp xx" by (rule lp_times) also have "lpp xx = ?x" by (simp add: xx_def punit.lt_monomial) finally have "?x adds lpp (qU - qU0)" by (simp add: eq) hence "lookup ?x x \ lookup (lpp (qU - qU0)) x" by (simp only: adds_poly_mapping le_fun_def) hence "x \ keys (lpp (qU - qU0))" by (simp add: in_keys_iff lookup_single) moreover have "lpp (qU - qU0) \ keys (qU - qU0)" proof (rule punit.lt_in_keys) from \qx0 - qx' \ 0\ \xx \ 0\ show "qU - qU0 \ 0" unfolding eq by (rule times_not_zero) qed ultimately have "x \ indets (qU - qU0)" by (rule in_indetsI) from \qU \ P[U]\ \qU0 \ P[U]\ have "qU - qU0 \ P[U]" by (rule Polys_closed_minus) hence "indets (qU - qU0) \ U" by (rule PolysD) with \x \ indets (qU - qU0)\ have "x \ U" .. with assms show False .. qed moreover from this eq have "qU0 = qU" by simp ultimately show ?thesis by (simp only: qs_def qs0 p1 p2) qed qed (simp_all add: qs_def a q qx, simp only: algebra_simps) qed qed definition valid_decomp :: "'x set \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ bool" where "valid_decomp X ps \ ((\(h, U)\set ps. h \ P[X] \ h \ 0 \ U \ X))" definition monomial_decomp :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::{one,zero}) \ 'x set) list \ bool" where "monomial_decomp ps \ (\hU\set ps. is_monomial (fst hU) \ punit.lc (fst hU) = 1)" definition hom_decomp :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::{one,zero}) \ 'x set) list \ bool" where "hom_decomp ps \ (\hU\set ps. homogeneous (fst hU))" definition cone_decomp :: "(('x \\<^sub>0 nat) \\<^sub>0 'a) set \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::comm_semiring_0) \ 'x set) list \ bool" where "cone_decomp T ps \ direct_decomp T (map cone ps)" lemma valid_decompI: "(\h U. (h, U) \ set ps \ h \ P[X]) \ (\h U. (h, U) \ set ps \ h \ 0) \ (\h U. (h, U) \ set ps \ U \ X) \ valid_decomp X ps" unfolding valid_decomp_def by blast lemma valid_decompD: assumes "valid_decomp X ps" and "(h, U) \ set ps" shows "h \ P[X]" and "h \ 0" and "U \ X" using assms unfolding valid_decomp_def by blast+ lemma valid_decompD_finite: assumes "finite X" and "valid_decomp X ps" and "(h, U) \ set ps" shows "finite U" proof - from assms(2, 3) have "U \ X" by (rule valid_decompD) thus ?thesis using assms(1) by (rule finite_subset) qed lemma valid_decomp_Nil: "valid_decomp X []" by (simp add: valid_decomp_def) lemma valid_decomp_concat: assumes "\ps. ps \ set pss \ valid_decomp X ps" shows "valid_decomp X (concat pss)" proof (rule valid_decompI) fix h U assume "(h, U) \ set (concat pss)" then obtain ps where "ps \ set pss" and "(h, U) \ set ps" unfolding set_concat .. from this(1) have "valid_decomp X ps" by (rule assms) thus "h \ P[X]" and "h \ 0" and "U \ X" using \(h, U) \ set ps\ by (rule valid_decompD)+ qed corollary valid_decomp_append: assumes "valid_decomp X ps" and "valid_decomp X qs" shows "valid_decomp X (ps @ qs)" proof - have "valid_decomp X (concat [ps, qs])" by (rule valid_decomp_concat) (auto simp: assms) thus ?thesis by simp qed lemma valid_decomp_map_times: assumes "valid_decomp X ps" and "s \ P[X]" and "s \ (0::_ \\<^sub>0 _::semiring_no_zero_divisors)" shows "valid_decomp X (map (apfst ((*) s)) ps)" proof (rule valid_decompI) fix h U assume "(h, U) \ set (map (apfst ((*) s)) ps)" then obtain x where "x \ set ps" and "(h, U) = apfst ((*) s) x" unfolding set_map .. moreover obtain a b where "x = (a, b)" using prod.exhaust by blast ultimately have h: "h = s * a" and "(a, U) \ set ps" by simp_all from assms(1) this(2) have "a \ P[X]" and "a \ 0" and "U \ X" by (rule valid_decompD)+ from assms(2) this(1) show "h \ P[X]" unfolding h by (rule Polys_closed_times) from assms(3) \a \ 0\ show "h \ 0" unfolding h by (rule times_not_zero) from \U \ X\ show "U \ X" . qed lemma monomial_decompI: "(\h U. (h, U) \ set ps \ is_monomial h) \ (\h U. (h, U) \ set ps \ punit.lc h = 1) \ monomial_decomp ps" by (auto simp: monomial_decomp_def) lemma monomial_decompD: assumes "monomial_decomp ps" and "(h, U) \ set ps" shows "is_monomial h" and "punit.lc h = 1" using assms by (auto simp: monomial_decomp_def) lemma monomial_decomp_append_iff: "monomial_decomp (ps @ qs) \ monomial_decomp ps \ monomial_decomp qs" by (auto simp: monomial_decomp_def) lemma monomial_decomp_concat: "(\ps. ps \ set pss \ monomial_decomp ps) \ monomial_decomp (concat pss)" by (induct pss) (auto simp: monomial_decomp_def) lemma monomial_decomp_map_times: assumes "monomial_decomp ps" and "is_monomial f" and "punit.lc f = (1::'a::semiring_1)" shows "monomial_decomp (map (apfst ((*) f)) ps)" proof (rule monomial_decompI) fix h U assume "(h, U) \ set (map (apfst ((*) f)) ps)" then obtain x where "x \ set ps" and "(h, U) = apfst ((*) f) x" unfolding set_map .. moreover obtain a b where "x = (a, b)" using prod.exhaust by blast ultimately have h: "h = f * a" and "(a, U) \ set ps" by simp_all from assms(1) this(2) have "is_monomial a" and "punit.lc a = 1" by (rule monomial_decompD)+ from this(1) have "monomial (punit.lc a) (lpp a) = a" by (rule punit.monomial_eq_itself) moreover define t where "t = lpp a" ultimately have a: "a = monomial 1 t" by (simp only: \punit.lc a = 1\) from assms(2) have "monomial (punit.lc f) (lpp f) = f" by (rule punit.monomial_eq_itself) moreover define s where "s = lpp f" ultimately have f: "f = monomial 1 s" by (simp only: assms(3)) show "is_monomial h" by (simp add: h a f times_monomial_monomial monomial_is_monomial) show "punit.lc h = 1" by (simp add: h a f times_monomial_monomial) qed lemma monomial_decomp_monomial_in_cone: assumes "monomial_decomp ps" and "hU \ set ps" and "a \ cone hU" shows "monomial (lookup a t) t \ cone hU" proof (cases "t \ keys a") case True obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with assms(2) have "(h, U) \ set ps" by simp with assms(1) have "is_monomial h" by (rule monomial_decompD) then obtain c s where h: "h = monomial c s" by (rule is_monomial_monomial) from assms(3) obtain q where "q \ P[U]" and "a = q * h" unfolding hU by (rule coneE) from this(2) have "a = h * q" by (simp only: mult.commute) also have "\ = punit.monom_mult c s q" by (simp only: h times_monomial_left) finally have a: "a = punit.monom_mult c s q" . with True have "t \ keys (punit.monom_mult c s q)" by simp hence "t \ (+) s ` keys q" using punit.keys_monom_mult_subset[simplified] .. then obtain u where "u \ keys q" and t: "t = s + u" .. note this(1) also from \q \ P[U]\ have "keys q \ .[U]" by (rule PolysD) finally have "u \ .[U]" . have "monomial (lookup a t) t = monomial (lookup q u) u * h" by (simp add: a t punit.lookup_monom_mult h times_monomial_monomial mult.commute) moreover from \u \ .[U]\ have "monomial (lookup q u) u \ P[U]" by (rule Polys_closed_monomial) ultimately show ?thesis unfolding hU by (rule coneI) next case False thus ?thesis by (simp add: zero_in_cone in_keys_iff) qed lemma monomial_decomp_sum_list_monomial_in_cone: assumes "monomial_decomp ps" and "a \ sum_list ` listset (map cone ps)" and "t \ keys a" obtains c h U where "(h, U) \ set ps" and "c \ 0" and "monomial c t \ cone (h, U)" proof - from assms(2) obtain qs where qs_in: "qs \ listset (map cone ps)" and a: "a = sum_list qs" .. from assms(3) keys_sum_list_subset have "t \ Keys (set qs)" unfolding a .. then obtain q where "q \ set qs" and "t \ keys q" by (rule in_KeysE) from this(1) obtain i where "i < length qs" and q: "q = qs ! i" by (metis in_set_conv_nth) moreover from qs_in have "length qs = length (map cone ps)" by (rule listsetD) ultimately have "i < length (map cone ps)" by simp moreover from qs_in this have "qs ! i \ (map cone ps) ! i" by (rule listsetD) ultimately have "ps ! i \ set ps" and "q \ cone (ps ! i)" by (simp_all add: q) with assms(1) have *: "monomial (lookup q t) t \ cone (ps ! i)" by (rule monomial_decomp_monomial_in_cone) obtain h U where psi: "ps ! i = (h, U)" using prod.exhaust by blast show ?thesis proof from \ps ! i \ set ps\ show "(h, U) \ set ps" by (simp only: psi) next from \t \ keys q\ show "lookup q t \ 0" by (simp add: in_keys_iff) next from * show "monomial (lookup q t) t \ cone (h, U)" by (simp only: psi) qed qed lemma hom_decompI: "(\h U. (h, U) \ set ps \ homogeneous h) \ hom_decomp ps" by (auto simp: hom_decomp_def) lemma hom_decompD: "hom_decomp ps \ (h, U) \ set ps \ homogeneous h" by (auto simp: hom_decomp_def) lemma hom_decomp_append_iff: "hom_decomp (ps @ qs) \ hom_decomp ps \ hom_decomp qs" by (auto simp: hom_decomp_def) lemma hom_decomp_concat: "(\ps. ps \ set pss \ hom_decomp ps) \ hom_decomp (concat pss)" by (induct pss) (auto simp: hom_decomp_def) lemma hom_decomp_map_times: assumes "hom_decomp ps" and "homogeneous f" shows "hom_decomp (map (apfst ((*) f)) ps)" proof (rule hom_decompI) fix h U assume "(h, U) \ set (map (apfst ((*) f)) ps)" then obtain x where "x \ set ps" and "(h, U) = apfst ((*) f) x" unfolding set_map .. moreover obtain a b where "x = (a, b)" using prod.exhaust by blast ultimately have h: "h = f * a" and "(a, U) \ set ps" by simp_all from assms(1) this(2) have "homogeneous a" by (rule hom_decompD) with assms(2) show "homogeneous h" unfolding h by (rule homogeneous_times) qed lemma monomial_decomp_imp_hom_decomp: assumes "monomial_decomp ps" shows "hom_decomp ps" proof (rule hom_decompI) fix h U assume "(h, U) \ set ps" with assms have "is_monomial h" by (rule monomial_decompD) then obtain c t where h: "h = monomial c t" by (rule is_monomial_monomial) show "homogeneous h" unfolding h by (fact homogeneous_monomial) qed lemma cone_decompI: "direct_decomp T (map cone ps) \ cone_decomp T ps" unfolding cone_decomp_def by blast lemma cone_decompD: "cone_decomp T ps \ direct_decomp T (map cone ps)" unfolding cone_decomp_def by blast lemma cone_decomp_cone_subset: assumes "cone_decomp T ps" and "hU \ set ps" shows "cone hU \ T" proof fix p assume "p \ cone hU" from assms(2) obtain i where "i < length ps" and hU: "hU = ps ! i" by (metis in_set_conv_nth) define qs where "qs = (map 0 ps)[i := p]" have "sum_list qs \ T" proof (intro direct_decompD listsetI) from assms(1) show "direct_decomp T (map cone ps)" by (rule cone_decompD) next fix j assume "j < length (map cone ps)" with \i < length ps\ \p \ cone hU\ show "qs ! j \ map cone ps ! j" by (auto simp: qs_def nth_list_update zero_in_cone hU) qed (simp add: qs_def) also have "sum_list qs = qs ! i" by (rule sum_list_eq_nthI) (simp_all add: qs_def \i < length ps\) also from \i < length ps\ have "\ = p" by (simp add: qs_def) finally show "p \ T" . qed lemma cone_decomp_indets: assumes "cone_decomp T ps" and "T \ P[X]" and "(h, U) \ set ps" shows "h \ P[X]" and "h \ (0::_ \\<^sub>0 _::{comm_semiring_1,semiring_no_zero_divisors}) \ U \ X" proof - from assms(1, 3) have "cone (h, U) \ T" by (rule cone_decomp_cone_subset) hence "cone (h, U) \ P[X]" using assms(2) by (rule subset_trans) thus "h \ P[X]" and "h \ 0 \ U \ X" by (rule cone_subset_PolysD)+ qed lemma cone_decomp_closed_plus: assumes "cone_decomp T ps" and "a \ T" and "b \ T" shows "a + b \ T" proof - from assms(1) have dd: "direct_decomp T (map cone ps)" by (rule cone_decompD) then obtain qsa where qsa: "qsa \ listset (map cone ps)" and a: "a = sum_list qsa" using assms(2) by (rule direct_decompE) from dd assms(3) obtain qsb where qsb: "qsb \ listset (map cone ps)" and b: "b = sum_list qsb" by (rule direct_decompE) from qsa have "length qsa = length (map cone ps)" by (rule listsetD) moreover from qsb have "length qsb = length (map cone ps)" by (rule listsetD) ultimately have "a + b = sum_list (map2 (+) qsa qsb)" by (simp only: sum_list_map2_plus a b) also from dd have "sum_list (map2 (+) qsa qsb) \ T" proof (rule direct_decompD) from qsa qsb show "map2 (+) qsa qsb \ listset (map cone ps)" proof (rule listset_closed_map2) fix c p1 p2 assume "c \ set (map cone ps)" then obtain hU where c: "c = cone hU" by auto assume "p1 \ c" and "p2 \ c" thus "p1 + p2 \ c" unfolding c by (rule cone_closed_plus) qed qed finally show ?thesis . qed lemma cone_decomp_closed_uminus: assumes "cone_decomp T ps" and "(a::_ \\<^sub>0 _::comm_ring) \ T" shows "- a \ T" proof - from assms(1) have dd: "direct_decomp T (map cone ps)" by (rule cone_decompD) then obtain qsa where qsa: "qsa \ listset (map cone ps)" and a: "a = sum_list qsa" using assms(2) by (rule direct_decompE) from qsa have "length qsa = length (map cone ps)" by (rule listsetD) have "- a = sum_list (map uminus qsa)" unfolding a by (induct qsa, simp_all) also from dd have "\ \ T" proof (rule direct_decompD) from qsa show "map uminus qsa \ listset (map cone ps)" proof (rule listset_closed_map) fix c p assume "c \ set (map cone ps)" then obtain hU where c: "c = cone hU" by auto assume "p \ c" thus "- p \ c" unfolding c by (rule cone_closed_uminus) qed qed finally show ?thesis . qed corollary cone_decomp_closed_minus: assumes "cone_decomp T ps" and "(a::_ \\<^sub>0 _::comm_ring) \ T" and "b \ T" shows "a - b \ T" proof - from assms(1, 3) have "- b \ T" by (rule cone_decomp_closed_uminus) with assms(1, 2) have "a + (- b) \ T" by (rule cone_decomp_closed_plus) thus ?thesis by simp qed lemma cone_decomp_Nil: "cone_decomp {0} []" by (auto simp: cone_decomp_def intro: direct_decompI_alt) lemma cone_decomp_singleton: "cone_decomp (cone (t, U)) [(t, U)]" by (simp add: cone_decomp_def direct_decomp_singleton) lemma cone_decomp_append: assumes "direct_decomp T [S1, S2]" and "cone_decomp S1 ps" and "cone_decomp S2 qs" shows "cone_decomp T (ps @ qs)" proof (rule cone_decompI) from assms(2) have "direct_decomp S1 (map cone ps)" by (rule cone_decompD) with assms(1) have "direct_decomp T ([S2] @ map cone ps)" by (rule direct_decomp_direct_decomp) hence "direct_decomp T (S2 # map cone ps)" by simp moreover from assms(3) have "direct_decomp S2 (map cone qs)" by (rule cone_decompD) ultimately have "direct_decomp T (map cone ps @ map cone qs)" by (intro direct_decomp_direct_decomp) thus "direct_decomp T (map cone (ps @ qs))" by simp qed lemma cone_decomp_concat: assumes "direct_decomp T ss" and "length pss = length ss" and "\i. i < length ss \ cone_decomp (ss ! i) (pss ! i)" shows "cone_decomp T (concat pss)" using assms(2, 1, 3) proof (induct pss ss arbitrary: T rule: list_induct2) case Nil from Nil(1) show ?case by (simp add: cone_decomp_def) next case (Cons ps pss s ss) have "0 < length (s # ss)" by simp hence "cone_decomp ((s # ss) ! 0) ((ps # pss) ! 0)" by (rule Cons.prems) hence "cone_decomp s ps" by simp hence *: "direct_decomp s (map cone ps)" by (rule cone_decompD) with Cons.prems(1) have "direct_decomp T (ss @ map cone ps)" by (rule direct_decomp_direct_decomp) hence 1: "direct_decomp T [sum_list ` listset ss, sum_list ` listset (map cone ps)]" and 2: "direct_decomp (sum_list ` listset ss) ss" by (auto dest: direct_decomp_appendD intro!: empty_not_in_map_cone) note 1 moreover from 2 have "cone_decomp (sum_list ` listset ss) (concat pss)" proof (rule Cons.hyps) fix i assume "i < length ss" hence "Suc i < length (s # ss)" by simp hence "cone_decomp ((s # ss) ! Suc i) ((ps # pss) ! Suc i)" by (rule Cons.prems) thus "cone_decomp (ss ! i) (pss ! i)" by simp qed moreover have "cone_decomp (sum_list ` listset (map cone ps)) ps" proof (intro cone_decompI direct_decompI refl) from * show "inj_on sum_list (listset (map cone ps))" by (simp only: direct_decomp_def bij_betw_def) qed ultimately have "cone_decomp T (concat pss @ ps)" by (rule cone_decomp_append) hence "direct_decomp T (map cone (concat pss) @ map cone ps)" by (simp add: cone_decomp_def) hence "direct_decomp T (map cone ps @ map cone (concat pss))" using perm_append_swap by (rule direct_decomp_perm) thus ?case by (simp add: cone_decomp_def) qed lemma cone_decomp_map_times: assumes "cone_decomp T ps" shows "cone_decomp ((*) s ` T) (map (apfst ((*) (s::_ \\<^sub>0 _::{comm_ring_1,ring_no_zero_divisors}))) ps)" proof (rule cone_decompI) from assms have "direct_decomp T (map cone ps)" by (rule cone_decompD) hence "direct_decomp ((*) s ` T) (map ((`) ((*) s)) (map cone ps))" by (rule direct_decomp_image_times) (rule times_canc_left) also have "map ((`) ((*) s)) (map cone ps) = map cone (map (apfst ((*) s)) ps)" by (simp add: cone_image_times') finally show "direct_decomp ((*) s ` T) (map cone (map (apfst ((*) s)) ps))" . qed lemma cone_decomp_perm: assumes "cone_decomp T ps" and "perm ps qs" shows "cone_decomp T qs" using assms(1) unfolding cone_decomp_def proof (rule direct_decomp_perm) - from assms(2) show "perm (map cone ps) (map cone qs)" - by (induct ps qs rule: perm.induct) auto + from \perm ps qs\ show \perm (map cone ps) (map cone qs)\ + by (simp add: perm_iff_eq_mset) qed lemma valid_cone_decomp_subset_Polys: assumes "valid_decomp X ps" and "cone_decomp T ps" shows "T \ P[X]" proof fix p assume "p \ T" from assms(2) have "direct_decomp T (map cone ps)" by (rule cone_decompD) then obtain qs where "qs \ listset (map cone ps)" and p: "p = sum_list qs" using \p \ T\ by (rule direct_decompE) from assms(1) this(1) show "p \ P[X]" unfolding p proof (induct ps arbitrary: qs) case Nil from Nil(2) show ?case by (simp add: zero_in_Polys) next case (Cons a ps) obtain h U where a: "a = (h, U)" using prod.exhaust by blast hence "(h, U) \ set (a # ps)" by simp with Cons.prems(1) have "h \ P[X]" and "U \ X" by (rule valid_decompD)+ hence "cone a \ P[X]" unfolding a by (rule cone_subset_PolysI) from Cons.prems(1) have "valid_decomp X ps" by (simp add: valid_decomp_def) from Cons.prems(2) have "qs \ listset (cone a # map cone ps)" by simp then obtain q qs' where "q \ cone a" and qs': "qs' \ listset (map cone ps)" and qs: "qs = q # qs'" by (rule listset_ConsE) from this(1) \cone a \ P[X]\ have "q \ P[X]" .. moreover from \valid_decomp X ps\ qs' have "sum_list qs' \ P[X]" by (rule Cons.hyps) ultimately have "q + sum_list qs' \ P[X]" by (rule Polys_closed_plus) thus ?case by (simp add: qs) qed qed lemma homogeneous_set_cone_decomp: assumes "cone_decomp T ps" and "hom_decomp ps" shows "homogeneous_set T" proof (rule homogeneous_set_direct_decomp) from assms(1) show "direct_decomp T (map cone ps)" by (rule cone_decompD) next fix cn assume "cn \ set (map cone ps)" then obtain hU where "hU \ set ps" and cn: "cn = cone hU" unfolding set_map .. moreover obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set ps" by simp with assms(2) have "homogeneous h" by (rule hom_decompD) thus "homogeneous_set cn" unfolding cn hU by (rule homogeneous_set_coneI) qed lemma subspace_cone_decomp: assumes "cone_decomp T ps" shows "phull.subspace (T::(_ \\<^sub>0 _::field) set)" proof (rule phull.subspace_direct_decomp) from assms show "direct_decomp T (map cone ps)" by (rule cone_decompD) next fix cn assume "cn \ set (map cone ps)" then obtain hU where "hU \ set ps" and cn: "cn = cone hU" unfolding set_map .. show "phull.subspace cn" unfolding cn by (rule subspace_cone) qed definition pos_decomp :: "((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list" ("(_\<^sub>+)" [1000] 999) where "pos_decomp ps = filter (\p. snd p \ {}) ps" definition standard_decomp :: "nat \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ bool" where "standard_decomp k ps \ (\(h, U)\set (ps\<^sub>+). k \ poly_deg h \ (\d. k \ d \ d \ poly_deg h \ (\(h', U')\set ps. poly_deg h' = d \ card U \ card U')))" lemma pos_decomp_Nil [simp]: "[]\<^sub>+ = []" by (simp add: pos_decomp_def) lemma pos_decomp_subset: "set (ps\<^sub>+) \ set ps" by (simp add: pos_decomp_def) lemma pos_decomp_append: "(ps @ qs)\<^sub>+ = ps\<^sub>+ @ qs\<^sub>+" by (simp add: pos_decomp_def) lemma pos_decomp_concat: "(concat pss)\<^sub>+ = concat (map pos_decomp pss)" by (metis (mono_tags, lifting) filter_concat map_eq_conv pos_decomp_def) lemma pos_decomp_map: "(map (apfst f) ps)\<^sub>+ = map (apfst f) (ps\<^sub>+)" by (metis (mono_tags, lifting) pos_decomp_def filter_cong filter_map o_apply snd_apfst) lemma card_Diff_pos_decomp: "card {(h, U) \ set qs - set (qs\<^sub>+). P h} = card {h. (h, {}) \ set qs \ P h}" proof - have "{h. (h, {}) \ set qs \ P h} = fst ` {(h, U) \ set qs - set (qs\<^sub>+). P h}" by (auto simp: pos_decomp_def image_Collect) also have "card \ = card {(h, U) \ set qs - set (qs\<^sub>+). P h}" by (rule card_image, auto simp: pos_decomp_def intro: inj_onI) finally show ?thesis by (rule sym) qed lemma standard_decompI: assumes "\h U. (h, U) \ set (ps\<^sub>+) \ k \ poly_deg h" and "\h U d. (h, U) \ set (ps\<^sub>+) \ k \ d \ d \ poly_deg h \ (\h' U'. (h', U') \ set ps \ poly_deg h' = d \ card U \ card U')" shows "standard_decomp k ps" unfolding standard_decomp_def using assms by blast lemma standard_decompD: "standard_decomp k ps \ (h, U) \ set (ps\<^sub>+) \ k \ poly_deg h" unfolding standard_decomp_def by blast lemma standard_decompE: assumes "standard_decomp k ps" and "(h, U) \ set (ps\<^sub>+)" and "k \ d" and "d \ poly_deg h" obtains h' U' where "(h', U') \ set ps" and "poly_deg h' = d" and "card U \ card U'" using assms unfolding standard_decomp_def by blast lemma standard_decomp_Nil: "ps\<^sub>+ = [] \ standard_decomp k ps" by (simp add: standard_decomp_def) lemma standard_decomp_singleton: "standard_decomp (poly_deg h) [(h, U)]" by (simp add: standard_decomp_def pos_decomp_def) lemma standard_decomp_concat: assumes "\ps. ps \ set pss \ standard_decomp k ps" shows "standard_decomp k (concat pss)" proof (rule standard_decompI) fix h U assume "(h, U) \ set ((concat pss)\<^sub>+)" then obtain ps where "ps \ set pss" and *: "(h, U) \ set (ps\<^sub>+)" by (auto simp: pos_decomp_concat) from this(1) have "standard_decomp k ps" by (rule assms) thus "k \ poly_deg h" using * by (rule standard_decompD) fix d assume "k \ d" and "d \ poly_deg h" with \standard_decomp k ps\ * obtain h' U' where "(h', U') \ set ps" and "poly_deg h' = d" and "card U \ card U'" by (rule standard_decompE) note this(2, 3) moreover from \(h', U') \ set ps\ \ps \ set pss\ have "(h', U') \ set (concat pss)" by auto ultimately show "\h' U'. (h', U') \ set (concat pss) \ poly_deg h' = d \ card U \ card U'" by blast qed corollary standard_decomp_append: assumes "standard_decomp k ps" and "standard_decomp k qs" shows "standard_decomp k (ps @ qs)" proof - have "standard_decomp k (concat [ps, qs])" by (rule standard_decomp_concat) (auto simp: assms) thus ?thesis by simp qed lemma standard_decomp_map_times: assumes "standard_decomp k ps" and "valid_decomp X ps" and "s \ (0::_ \\<^sub>0 'a::semiring_no_zero_divisors)" shows "standard_decomp (k + poly_deg s) (map (apfst ((*) s)) ps)" proof (rule standard_decompI) fix h U assume "(h, U) \ set ((map (apfst ((*) s)) ps)\<^sub>+)" then obtain h0 where 1: "(h0, U) \ set (ps\<^sub>+)" and h: "h = s * h0" by (fastforce simp: pos_decomp_map) from this(1) pos_decomp_subset have "(h0, U) \ set ps" .. with assms(2) have "h0 \ 0" by (rule valid_decompD) with assms(3) have deg_h: "poly_deg h = poly_deg s + poly_deg h0" unfolding h by (rule poly_deg_times) moreover from assms(1) 1 have "k \ poly_deg h0" by (rule standard_decompD) ultimately show "k + poly_deg s \ poly_deg h" by simp fix d assume "k + poly_deg s \ d" and "d \ poly_deg h" hence "k \ d - poly_deg s" and "d - poly_deg s \ poly_deg h0" by (simp_all add: deg_h) with assms(1) 1 obtain h' U' where 2: "(h', U') \ set ps" and "poly_deg h' = d - poly_deg s" and "card U \ card U'" by (rule standard_decompE) from assms(2) this(1) have "h' \ 0" by (rule valid_decompD) with assms(3) have deg_h': "poly_deg (s * h') = poly_deg s + poly_deg h'" by (rule poly_deg_times) from 2 have "(s * h', U') \ set (map (apfst ((*) s)) ps)" by force moreover from \k + poly_deg s \ d\ \poly_deg h' = d - poly_deg s\ have "poly_deg (s * h') = d" by (simp add: deg_h') ultimately show "\h' U'. (h', U') \ set (map (apfst ((*) s)) ps) \ poly_deg h' = d \ card U \ card U'" using \card U \ card U'\ by fastforce qed lemma standard_decomp_nonempty_unique: assumes "finite X" and "valid_decomp X ps" and "standard_decomp k ps" and "ps\<^sub>+ \ []" shows "k = Min (poly_deg ` fst ` set (ps\<^sub>+))" proof - let ?A = "poly_deg ` fst ` set (ps\<^sub>+)" define m where "m = Min ?A" have "finite ?A" by simp moreover from assms(4) have "?A \ {}" by simp ultimately have "m \ ?A" unfolding m_def by (rule Min_in) then obtain h U where "(h, U) \ set (ps\<^sub>+)" and m: "m = poly_deg h" by fastforce have m_min: "m \ poly_deg h'" if "(h', U') \ set (ps\<^sub>+)" for h' U' proof - from that have "poly_deg (fst (h', U')) \ ?A" by (intro imageI) with \finite ?A\ have "m \ poly_deg (fst (h', U'))" unfolding m_def by (rule Min_le) thus ?thesis by simp qed show ?thesis proof (rule linorder_cases) assume "k < m" hence "k \ poly_deg h" by (simp add: m) with assms(3) \(h, U) \ set (ps\<^sub>+)\ le_refl obtain h' U' where "(h', U') \ set ps" and "poly_deg h' = k" and "card U \ card U'" by (rule standard_decompE) from this(2) \k < m\ have "\ m \ poly_deg h'" by simp with m_min have "(h', U') \ set (ps\<^sub>+)" by blast with \(h', U') \ set ps\ have "U' = {}" by (simp add: pos_decomp_def) with \card U \ card U'\ have "U = {} \ infinite U" by (simp add: card_eq_0_iff) thus ?thesis proof assume "U = {}" with \(h, U) \ set (ps\<^sub>+)\ show ?thesis by (simp add: pos_decomp_def) next assume "infinite U" moreover from assms(1, 2) have "finite U" proof (rule valid_decompD_finite) from \(h, U) \ set (ps\<^sub>+)\ show "(h, U) \ set ps" by (simp add: pos_decomp_def) qed ultimately show ?thesis .. qed next assume "m < k" hence "\ k \ m" by simp moreover from assms(3) \(h, U) \ set (ps\<^sub>+)\ have "k \ m" unfolding m by (rule standard_decompD) ultimately show ?thesis .. qed (simp only: m_def) qed lemma standard_decomp_SucE: assumes "finite X" and "U \ X" and "h \ P[X]" and "h \ (0::_ \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors})" obtains ps where "valid_decomp X ps" and "cone_decomp (cone (h, U)) ps" and "standard_decomp (Suc (poly_deg h)) ps" and "is_monomial h \ punit.lc h = 1 \ monomial_decomp ps" and "homogeneous h \ hom_decomp ps" proof - from assms(2, 1) have "finite U" by (rule finite_subset) thus ?thesis using assms(2) that proof (induct U arbitrary: thesis rule: finite_induct) case empty from assms(3, 4) have "valid_decomp X [(h, {})]" by (simp add: valid_decomp_def) moreover note cone_decomp_singleton moreover have "standard_decomp (Suc (poly_deg h)) [(h, {})]" by (rule standard_decomp_Nil) (simp add: pos_decomp_def) ultimately show ?case by (rule empty) (simp_all add: monomial_decomp_def hom_decomp_def) next case (insert x U) from insert.prems(1) have "x \ X" and "U \ X" by simp_all from this(2) obtain ps where 0: "valid_decomp X ps" and 1: "cone_decomp (cone (h, U)) ps" and 2: "standard_decomp (Suc (poly_deg h)) ps" and 3: "is_monomial h \ punit.lc h = 1 \ monomial_decomp ps" and 4: "homogeneous h \ hom_decomp ps" by (rule insert.hyps) blast let ?x = "monomial (1::'a) (Poly_Mapping.single x (Suc 0))" have "?x \ 0" by (simp add: monomial_0_iff) with assms(4) have deg: "poly_deg (?x * h) = Suc (poly_deg h)" by (simp add: poly_deg_times poly_deg_monomial deg_pm_single) define qs where "qs = [(?x * h, insert x U)]" show ?case proof (rule insert.prems) from \x \ X\ have "?x \ P[X]" by (intro Polys_closed_monomial PPs_closed_single) hence "?x * h \ P[X]" using assms(3) by (rule Polys_closed_times) moreover from \?x \ 0\ assms(4) have "?x * h \ 0" by (rule times_not_zero) ultimately have "valid_decomp X qs" using insert.hyps(1) \x \ X\ \U \ X\ by (simp add: qs_def valid_decomp_def) with 0 show "valid_decomp X (ps @ qs)" by (rule valid_decomp_append) next show "cone_decomp (cone (h, insert x U)) (ps @ qs)" proof (rule cone_decomp_append) show "direct_decomp (cone (h, insert x U)) [cone (h, U), cone (?x * h, insert x U)]" using insert.hyps(2) by (rule direct_decomp_cone_insert) next show "cone_decomp (cone (?x * h, insert x U)) qs" by (simp add: qs_def cone_decomp_singleton) qed (fact 1) next from standard_decomp_singleton[of "?x * h" "insert x U"] have "standard_decomp (Suc (poly_deg h)) qs" by (simp add: deg qs_def) with 2 show "standard_decomp (Suc (poly_deg h)) (ps @ qs)" by (rule standard_decomp_append) next assume "is_monomial h" and "punit.lc h = 1" hence "monomial_decomp ps" by (rule 3) moreover have "monomial_decomp qs" proof - have "is_monomial (?x * h)" by (metis \is_monomial h\ is_monomial_monomial monomial_is_monomial mult.commute mult.right_neutral mult_single) thus ?thesis by (simp add: monomial_decomp_def qs_def lc_times \punit.lc h = 1\) qed ultimately show "monomial_decomp (ps @ qs)" by (simp only: monomial_decomp_append_iff) next assume "homogeneous h" hence "hom_decomp ps" by (rule 4) moreover from \homogeneous h\ have "hom_decomp qs" by (simp add: hom_decomp_def qs_def homogeneous_times) ultimately show "hom_decomp (ps @ qs)" by (simp only: hom_decomp_append_iff) qed qed qed lemma standard_decomp_geE: assumes "finite X" and "valid_decomp X ps" and "cone_decomp (T::(('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) set) ps" and "standard_decomp k ps" and "k \ d" obtains qs where "valid_decomp X qs" and "cone_decomp T qs" and "standard_decomp d qs" and "monomial_decomp ps \ monomial_decomp qs" and "hom_decomp ps \ hom_decomp qs" proof - have "\qs. valid_decomp X qs \ cone_decomp T qs \ standard_decomp (k + i) qs \ (monomial_decomp ps \ monomial_decomp qs) \ (hom_decomp ps \ hom_decomp qs)" for i proof (induct i) case 0 from assms(2, 3, 4) show ?case unfolding add_0_right by blast next case (Suc i) then obtain qs where 0: "valid_decomp X qs" and 1: "cone_decomp T qs" and 2: "standard_decomp (k + i) qs" and 3: "monomial_decomp ps \ monomial_decomp qs" and 4: "hom_decomp ps \ hom_decomp qs" by blast let ?P = "\hU. poly_deg (fst hU) \ k + i" define rs where "rs = filter (- ?P) qs" define ss where "ss = filter ?P qs" have "set rs \ set qs" by (auto simp: rs_def) have "set ss \ set qs" by (auto simp: ss_def) define f where "f = (\hU. SOME ps'. valid_decomp X ps' \ cone_decomp (cone hU) ps' \ standard_decomp (Suc (poly_deg ((fst hU)::('x \\<^sub>0 _) \\<^sub>0 'a))) ps' \ (monomial_decomp ps \ monomial_decomp ps') \ (hom_decomp ps \ hom_decomp ps'))" have "valid_decomp X (f hU) \ cone_decomp (cone hU) (f hU) \ standard_decomp (Suc (k + i)) (f hU) \ (monomial_decomp ps \ monomial_decomp (f hU)) \ (hom_decomp ps \ hom_decomp (f hU))" if "hU \ set rs" for hU proof - obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with that have eq: "poly_deg (fst hU) = k + i" by (simp add: rs_def) from that \set rs \ set qs\ have "(h, U) \ set qs" unfolding hU .. with 0 have "U \ X" and "h \ P[X]" and "h \ 0" by (rule valid_decompD)+ with assms(1) obtain ps' where "valid_decomp X ps'" and "cone_decomp (cone (h, U)) ps'" and "standard_decomp (Suc (poly_deg h)) ps'" and md: "is_monomial h \ punit.lc h = 1 \ monomial_decomp ps'" and hd: "homogeneous h \ hom_decomp ps'" by (rule standard_decomp_SucE) blast note this(1-3) moreover have "monomial_decomp ps'" if "monomial_decomp ps" proof - from that have "monomial_decomp qs" by (rule 3) hence "is_monomial h" and "punit.lc h = 1" using \(h, U) \ set qs\ by (rule monomial_decompD)+ thus ?thesis by (rule md) qed moreover have "hom_decomp ps'" if "hom_decomp ps" proof - from that have "hom_decomp qs" by (rule 4) hence "homogeneous h" using \(h, U) \ set qs\ by (rule hom_decompD) thus ?thesis by (rule hd) qed ultimately have "valid_decomp X ps' \ cone_decomp (cone hU) ps' \ standard_decomp (Suc (poly_deg (fst hU))) ps' \ (monomial_decomp ps \ monomial_decomp ps') \ (hom_decomp ps \ hom_decomp ps')" by (simp add: hU) thus ?thesis unfolding f_def eq by (rule someI) qed hence f1: "\ps. ps \ set (map f rs) \ valid_decomp X ps" and f2: "\hU. hU \ set rs \ cone_decomp (cone hU) (f hU)" and f3: "\ps. ps \ set (map f rs) \ standard_decomp (Suc (k + i)) ps" and f4: "\ps'. monomial_decomp ps \ ps' \ set (map f rs) \ monomial_decomp ps'" and f5: "\ps'. hom_decomp ps \ ps' \ set (map f rs) \ hom_decomp ps'" by auto define rs' where "rs' = concat (map f rs)" show ?case unfolding add_Suc_right proof (intro exI conjI impI) have "valid_decomp X ss" proof (rule valid_decompI) fix h U assume "(h, U) \ set ss" hence "(h, U) \ set qs" using \set ss \ set qs\ .. with 0 show "h \ P[X]" and "h \ 0" and "U \ X" by (rule valid_decompD)+ qed moreover have "valid_decomp X rs'" unfolding rs'_def using f1 by (rule valid_decomp_concat) ultimately show "valid_decomp X (ss @ rs')" by (rule valid_decomp_append) next from 1 have "direct_decomp T (map cone qs)" by (rule cone_decompD) hence "direct_decomp T ((map cone ss) @ (map cone rs))" unfolding ss_def rs_def by (rule direct_decomp_split_map) hence ss: "cone_decomp (sum_list ` listset (map cone ss)) ss" and "cone_decomp (sum_list ` listset (map cone rs)) rs" and T: "direct_decomp T [sum_list ` listset (map cone ss), sum_list ` listset (map cone rs)]" by (auto simp: cone_decomp_def dest: direct_decomp_appendD intro!: empty_not_in_map_cone) from this(2) have "direct_decomp (sum_list ` listset (map cone rs)) (map cone rs)" by (rule cone_decompD) hence "cone_decomp (sum_list ` listset (map cone rs)) rs'" unfolding rs'_def proof (rule cone_decomp_concat) fix i assume *: "i < length (map cone rs)" hence "rs ! i \ set rs" by simp hence "cone_decomp (cone (rs ! i)) (f (rs ! i))" by (rule f2) with * show "cone_decomp (map cone rs ! i) (map f rs ! i)" by simp qed simp with T ss show "cone_decomp T (ss @ rs')" by (rule cone_decomp_append) next have "standard_decomp (Suc (k + i)) ss" proof (rule standard_decompI) fix h U assume "(h, U) \ set (ss\<^sub>+)" hence "(h, U) \ set (qs\<^sub>+)" and "poly_deg h \ k + i" by (simp_all add: pos_decomp_def ss_def) from 2 this(1) have "k + i \ poly_deg h" by (rule standard_decompD) with \poly_deg h \ k + i\ show "Suc (k + i) \ poly_deg h" by simp fix d' assume "Suc (k + i) \ d'" and "d' \ poly_deg h" from this(1) have "k + i \ d'" and "d' \ k + i" by simp_all from 2 \(h, U) \ set (qs\<^sub>+)\ this(1) obtain h' U' where "(h', U') \ set qs" and "poly_deg h' = d'" and "card U \ card U'" using \d' \ poly_deg h\ by (rule standard_decompE) moreover from \d' \ k + i\ this(1, 2) have "(h', U') \ set ss" by (simp add: ss_def) ultimately show "\h' U'. (h', U') \ set ss \ poly_deg h' = d' \ card U \ card U'" by blast qed moreover have "standard_decomp (Suc (k + i)) rs'" unfolding rs'_def using f3 by (rule standard_decomp_concat) ultimately show "standard_decomp (Suc (k + i)) (ss @ rs')" by (rule standard_decomp_append) next assume *: "monomial_decomp ps" hence "monomial_decomp qs" by (rule 3) hence "monomial_decomp ss" by (simp add: monomial_decomp_def ss_def) moreover have "monomial_decomp rs'" unfolding rs'_def using f4[OF *] by (rule monomial_decomp_concat) ultimately show "monomial_decomp (ss @ rs')" by (simp only: monomial_decomp_append_iff) next assume *: "hom_decomp ps" hence "hom_decomp qs" by (rule 4) hence "hom_decomp ss" by (simp add: hom_decomp_def ss_def) moreover have "hom_decomp rs'" unfolding rs'_def using f5[OF *] by (rule hom_decomp_concat) ultimately show "hom_decomp (ss @ rs')" by (simp only: hom_decomp_append_iff) qed qed then obtain qs where 1: "valid_decomp X qs" and 2: "cone_decomp T qs" and "standard_decomp (k + (d - k)) qs" and 4: "monomial_decomp ps \ monomial_decomp qs" and 5: "hom_decomp ps \ hom_decomp qs" by blast from this(3) assms(5) have "standard_decomp d qs" by simp with 1 2 show ?thesis using 4 5 .. qed subsection \Splitting w.r.t. Ideals\ context fixes X :: "'x set" begin definition splits_wrt :: "(((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list) \ (('x \\<^sub>0 nat) \\<^sub>0 'a::comm_ring_1) set \ (('x \\<^sub>0 nat) \\<^sub>0 'a) set \ bool" where "splits_wrt pqs T F \ cone_decomp T (fst pqs @ snd pqs) \ (\hU\set (fst pqs). cone hU \ ideal F \ P[X]) \ (\(h, U)\set (snd pqs). cone (h, U) \ P[X] \ cone (h, U) \ ideal F = {0})" lemma splits_wrtI: assumes "cone_decomp T (ps @ qs)" and "\h U. (h, U) \ set ps \ cone (h, U) \ P[X]" and "\h U. (h, U) \ set ps \ h \ ideal F" and "\h U. (h, U) \ set qs \ cone (h, U) \ P[X]" and "\h U a. (h, U) \ set qs \ a \ cone (h, U) \ a \ ideal F \ a = 0" shows "splits_wrt (ps, qs) T F" unfolding splits_wrt_def fst_conv snd_conv proof (intro conjI ballI) fix hU assume "hU \ set ps" moreover obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set ps" by simp hence "cone (h, U) \ P[X]" and "h \ ideal F" by (rule assms)+ from _ this(1) show "cone hU \ ideal F \ P[X]" unfolding hU proof (rule Int_greatest) show "cone (h, U) \ ideal F" proof fix a assume "a \ cone (h, U)" then obtain a' where "a' \ P[U]" and a: "a = a' * h" by (rule coneE) from \h \ ideal F\ show "a \ ideal F" unfolding a by (rule ideal.span_scale) qed qed next fix hU assume "hU \ set qs" moreover obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set qs" by simp hence "cone (h, U) \ P[X]" and "\a. a \ cone (h, U) \ a \ ideal F \ a = 0" by (rule assms)+ moreover have "0 \ cone (h, U) \ ideal F" by (simp add: zero_in_cone ideal.span_zero) ultimately show "case hU of (h, U) \ cone (h, U) \ P[X] \ cone (h, U) \ ideal F = {0}" by (fastforce simp: hU) qed (fact assms)+ lemma splits_wrtI_valid_decomp: assumes "valid_decomp X ps" and "valid_decomp X qs" and "cone_decomp T (ps @ qs)" and "\h U. (h, U) \ set ps \ h \ ideal F" and "\h U a. (h, U) \ set qs \ a \ cone (h, U) \ a \ ideal F \ a = 0" shows "splits_wrt (ps, qs) T F" using assms(3) _ _ _ assms(5) proof (rule splits_wrtI) fix h U assume "(h, U) \ set ps" thus "h \ ideal F" by (rule assms(4)) from assms(1) \(h, U) \ set ps\ have "h \ P[X]" and "U \ X" by (rule valid_decompD)+ thus "cone (h, U) \ P[X]" by (rule cone_subset_PolysI) next fix h U assume "(h, U) \ set qs" with assms(2) have "h \ P[X]" by (rule valid_decompD) moreover from assms(2) \(h, U) \ set qs\ have "U \ X" by (rule valid_decompD) ultimately show "cone (h, U) \ P[X]" by (rule cone_subset_PolysI) qed lemma splits_wrtD: assumes "splits_wrt (ps, qs) T F" shows "cone_decomp T (ps @ qs)" and "hU \ set ps \ cone hU \ ideal F \ P[X]" and "hU \ set qs \ cone hU \ P[X]" and "hU \ set qs \ cone hU \ ideal F = {0}" using assms by (fastforce simp: splits_wrt_def)+ lemma splits_wrt_image_sum_list_fst_subset: assumes "splits_wrt (ps, qs) T F" shows "sum_list ` listset (map cone ps) \ ideal F \ P[X]" proof fix x assume x_in: "x \ sum_list ` listset (map cone ps)" have "listset (map cone ps) \ listset (map (\_. ideal F \ P[X]) ps)" proof (rule listset_mono) fix i assume i: "i < length (map (\_. ideal F \ P[X]) ps)" hence "ps ! i \ set ps" by simp with assms(1) have "cone (ps ! i) \ ideal F \ P[X]" by (rule splits_wrtD) with i show "map cone ps ! i \ map (\_. ideal F \ P[X]) ps ! i" by simp qed simp hence "sum_list ` listset (map cone ps) \ sum_list ` listset (map (\_. ideal F \ P[X]) ps)" by (rule image_mono) with x_in have "x \ sum_list ` listset (map (\_. ideal F \ P[X]) ps)" .. then obtain xs where xs: "xs \ listset (map (\_. ideal F \ P[X]) ps)" and x: "x = sum_list xs" .. have 1: "y \ ideal F \ P[X]" if "y \ set xs" for y proof - from that obtain i where "i < length xs" and y: "y = xs ! i" by (metis in_set_conv_nth) moreover from xs have "length xs = length (map (\_. ideal F \ P[X]) ps)" by (rule listsetD) ultimately have "i < length (map (\_. ideal F \ P[X]) ps)" by simp moreover from xs this have "xs ! i \ (map (\_. ideal F \ P[X]) ps) ! i" by (rule listsetD) ultimately show "y \ ideal F \ P[X]" by (simp add: y) qed show "x \ ideal F \ P[X]" unfolding x proof show "sum_list xs \ ideal F" proof (rule ideal.span_closed_sum_list[simplified]) fix y assume "y \ set xs" hence "y \ ideal F \ P[X]" by (rule 1) thus "y \ ideal F" by simp qed next show "sum_list xs \ P[X]" proof (rule Polys_closed_sum_list) fix y assume "y \ set xs" hence "y \ ideal F \ P[X]" by (rule 1) thus "y \ P[X]" by simp qed qed qed lemma splits_wrt_image_sum_list_snd_subset: assumes "splits_wrt (ps, qs) T F" shows "sum_list ` listset (map cone qs) \ P[X]" proof fix x assume x_in: "x \ sum_list ` listset (map cone qs)" have "listset (map cone qs) \ listset (map (\_. P[X]) qs)" proof (rule listset_mono) fix i assume i: "i < length (map (\_. P[X]) qs)" hence "qs ! i \ set qs" by simp with assms(1) have "cone (qs ! i) \ P[X]" by (rule splits_wrtD) with i show "map cone qs ! i \ map (\_. P[X]) qs ! i" by simp qed simp hence "sum_list ` listset (map cone qs) \ sum_list ` listset (map (\_. P[X]) qs)" by (rule image_mono) with x_in have "x \ sum_list ` listset (map (\_. P[X]) qs)" .. then obtain xs where xs: "xs \ listset (map (\_. P[X]) qs)" and x: "x = sum_list xs" .. show "x \ P[X]" unfolding x proof (rule Polys_closed_sum_list) fix y assume "y \ set xs" then obtain i where "i < length xs" and y: "y = xs ! i" by (metis in_set_conv_nth) moreover from xs have "length xs = length (map (\_. P[X]::(_ \\<^sub>0 'a) set) qs)" by (rule listsetD) ultimately have "i < length (map (\_. P[X]) qs)" by simp moreover from xs this have "xs ! i \ (map (\_. P[X]) qs) ! i" by (rule listsetD) ultimately show "y \ P[X]" by (simp add: y) qed qed lemma splits_wrt_cone_decomp_1: assumes "splits_wrt (ps, qs) T F" and "monomial_decomp qs" and "is_monomial_set (F::(_ \\<^sub>0 'a::field) set)" \\The last two assumptions are missing in the paper.\ shows "cone_decomp (T \ ideal F) ps" proof - from assms(1) have *: "cone_decomp T (ps @ qs)" by (rule splits_wrtD) hence "direct_decomp T (map cone ps @ map cone qs)" by (simp add: cone_decomp_def) hence 1: "direct_decomp (sum_list ` listset (map cone ps)) (map cone ps)" and 2: "direct_decomp T [sum_list ` listset (map cone ps), sum_list ` listset (map cone qs)]" by (auto dest: direct_decomp_appendD intro!: empty_not_in_map_cone) let ?ss = "[sum_list ` listset (map cone ps), sum_list ` listset (map cone qs)]" show ?thesis proof (intro cone_decompI direct_decompI) from 1 show "inj_on sum_list (listset (map cone ps))" by (simp only: direct_decomp_def bij_betw_def) next from assms(1) have "sum_list ` listset (map cone ps) \ ideal F \ P[X]" by (rule splits_wrt_image_sum_list_fst_subset) hence sub: "sum_list ` listset (map cone ps) \ ideal F" by simp show "sum_list ` listset (map cone ps) = T \ ideal F" proof (rule set_eqI) fix x show "x \ sum_list ` listset (map cone ps) \ x \ T \ ideal F" proof assume x_in: "x \ sum_list ` listset (map cone ps)" show "x \ T \ ideal F" proof (intro IntI) have "map (\_. 0) qs \ listset (map cone qs)" (is "?ys \ _") by (induct qs) (auto intro: listset_ConsI zero_in_cone simp del: listset.simps(2)) hence "sum_list ?ys \ sum_list ` listset (map cone qs)" by (rule imageI) hence "0 \ sum_list ` listset (map cone qs)" by simp with x_in have "[x, 0] \ listset ?ss" using refl by (rule listset_doubletonI) with 2 have "sum_list [x, 0] \ T" by (rule direct_decompD) thus "x \ T" by simp next from x_in sub show "x \ ideal F" .. qed next assume "x \ T \ ideal F" hence "x \ T" and "x \ ideal F" by simp_all from 2 this(1) obtain xs where "xs \ listset ?ss" and x: "x = sum_list xs" by (rule direct_decompE) from this(1) obtain p q where p: "p \ sum_list ` listset (map cone ps)" and q: "q \ sum_list ` listset (map cone qs)" and xs: "xs = [p, q]" by (rule listset_doubletonE) from \x \ ideal F\ have "p + q \ ideal F" by (simp add: x xs) moreover from p sub have "p \ ideal F" .. ultimately have "p + q - p \ ideal F" by (rule ideal.span_diff) hence "q \ ideal F" by simp have "q = 0" proof (rule ccontr) assume "q \ 0" hence "keys q \ {}" by simp then obtain t where "t \ keys q" by blast with assms(2) q obtain c h U where "(h, U) \ set qs" and "c \ 0" and "monomial c t \ cone (h, U)" by (rule monomial_decomp_sum_list_monomial_in_cone) moreover from assms(3) \q \ ideal F\ \t \ keys q\ have "monomial c t \ ideal F" by (rule punit.monomial_pmdl_field[simplified]) ultimately have "monomial c t \ cone (h, U) \ ideal F" by simp also from assms(1) \(h, U) \ set qs\ have "\ = {0}" by (rule splits_wrtD) finally have "c = 0" by (simp add: monomial_0_iff) with \c \ 0\ show False .. qed with p show "x \ sum_list ` listset (map cone ps)" by (simp add: x xs) qed qed qed qed text \Together, Theorems \splits_wrt_image_sum_list_fst_subset\ and \splits_wrt_cone_decomp_1\ imply that @{term ps} is also a cone decomposition of @{term "T \ ideal F \ P[X]"}.\ lemma splits_wrt_cone_decomp_2: assumes "finite X" and "splits_wrt (ps, qs) T F" and "monomial_decomp qs" and "is_monomial_set F" and "F \ P[X]" shows "cone_decomp (T \ normal_form F ` P[X]) qs" proof - from assms(2) have *: "cone_decomp T (ps @ qs)" by (rule splits_wrtD) hence "direct_decomp T (map cone ps @ map cone qs)" by (simp add: cone_decomp_def) hence 1: "direct_decomp (sum_list ` listset (map cone qs)) (map cone qs)" and 2: "direct_decomp T [sum_list ` listset (map cone ps), sum_list ` listset (map cone qs)]" by (auto dest: direct_decomp_appendD intro!: empty_not_in_map_cone) let ?ss = "[sum_list ` listset (map cone ps), sum_list ` listset (map cone qs)]" let ?G = "punit.reduced_GB F" from assms(1, 5) have "?G \ P[X]" and G_is_GB: "punit.is_Groebner_basis ?G" and ideal_G: "ideal ?G = ideal F" by (rule reduced_GB_Polys, rule reduced_GB_is_GB_Polys, rule reduced_GB_ideal_Polys) show ?thesis proof (intro cone_decompI direct_decompI) from 1 show "inj_on sum_list (listset (map cone qs))" by (simp only: direct_decomp_def bij_betw_def) next from assms(2) have "sum_list ` listset (map cone ps) \ ideal F \ P[X]" by (rule splits_wrt_image_sum_list_fst_subset) hence sub: "sum_list ` listset (map cone ps) \ ideal F" by simp show "sum_list ` listset (map cone qs) = T \ normal_form F ` P[X]" proof (rule set_eqI) fix x show "x \ sum_list ` listset (map cone qs) \ x \ T \ normal_form F ` P[X]" proof assume x_in: "x \ sum_list ` listset (map cone qs)" show "x \ T \ normal_form F ` P[X]" proof (intro IntI) have "map (\_. 0) ps \ listset (map cone ps)" (is "?ys \ _") by (induct ps) (auto intro: listset_ConsI zero_in_cone simp del: listset.simps(2)) hence "sum_list ?ys \ sum_list ` listset (map cone ps)" by (rule imageI) hence "0 \ sum_list ` listset (map cone ps)" by simp from this x_in have "[0, x] \ listset ?ss" using refl by (rule listset_doubletonI) with 2 have "sum_list [0, x] \ T" by (rule direct_decompD) thus "x \ T" by simp next from assms(2) have "sum_list ` listset (map cone qs) \ P[X]" by (rule splits_wrt_image_sum_list_snd_subset) with x_in have "x \ P[X]" .. moreover have "\ punit.is_red ?G x" proof assume "punit.is_red ?G x" then obtain g t where "g \ ?G" and "t \ keys x" and "g \ 0" and adds: "lpp g adds t" by (rule punit.is_red_addsE[simplified]) from assms(3) x_in this(2) obtain c h U where "(h, U) \ set qs" and "c \ 0" and "monomial c t \ cone (h, U)" by (rule monomial_decomp_sum_list_monomial_in_cone) note this(3) moreover have "monomial c t \ ideal ?G" proof (rule punit.is_red_monomial_monomial_set_in_pmdl[simplified]) from \c \ 0\ show "is_monomial (monomial c t)" by (rule monomial_is_monomial) next from assms(1, 5, 4) show "is_monomial_set ?G" by (rule reduced_GB_is_monomial_set_Polys) next from \c \ 0\ have "t \ keys (monomial c t)" by simp with \g \ ?G\ \g \ 0\ show "punit.is_red ?G (monomial c t)" using adds by (rule punit.is_red_addsI[simplified]) qed ultimately have "monomial c t \ cone (h, U) \ ideal F" by (simp add: ideal_G) also from assms(2) \(h, U) \ set qs\ have "\ = {0}" by (rule splits_wrtD) finally have "c = 0" by (simp add: monomial_0_iff) with \c \ 0\ show False .. qed ultimately show "x \ normal_form F ` P[X]" using assms(1, 5) by (simp add: image_normal_form_iff) qed next assume "x \ T \ normal_form F ` P[X]" hence "x \ T" and "x \ normal_form F ` P[X]" by simp_all from this(2) assms(1, 5) have "x \ P[X]" and irred: "\ punit.is_red ?G x" by (simp_all add: image_normal_form_iff) from 2 \x \ T\ obtain xs where "xs \ listset ?ss" and x: "x = sum_list xs" by (rule direct_decompE) from this(1) obtain p q where p: "p \ sum_list ` listset (map cone ps)" and q: "q \ sum_list ` listset (map cone qs)" and xs: "xs = [p, q]" by (rule listset_doubletonE) have "x = p + q" by (simp add: x xs) from p sub have "p \ ideal F" .. have "p = 0" proof (rule ccontr) assume "p \ 0" hence "keys p \ {}" by simp then obtain t where "t \ keys p" by blast from assms(4) \p \ ideal F\ \t \ keys p\ have 3: "monomial c t \ ideal F" for c by (rule punit.monomial_pmdl_field[simplified]) have "t \ keys q" proof assume "t \ keys q" with assms(3) q obtain c h U where "(h, U) \ set qs" and "c \ 0" and "monomial c t \ cone (h, U)" by (rule monomial_decomp_sum_list_monomial_in_cone) from this(3) 3 have "monomial c t \ cone (h, U) \ ideal F" by simp also from assms(2) \(h, U) \ set qs\ have "\ = {0}" by (rule splits_wrtD) finally have "c = 0" by (simp add: monomial_0_iff) with \c \ 0\ show False .. qed with \t \ keys p\ have "t \ keys x" unfolding \x = p + q\ by (rule in_keys_plusI1) have "punit.is_red ?G x" proof - note G_is_GB moreover from 3 have "monomial 1 t \ ideal ?G" by (simp only: ideal_G) moreover have "monomial (1::'a) t \ 0" by (simp add: monomial_0_iff) ultimately obtain g where "g \ ?G" and "g \ 0" and "lpp g adds lpp (monomial (1::'a) t)" by (rule punit.GB_adds_lt[simplified]) from this(3) have "lpp g adds t" by (simp add: punit.lt_monomial) with \g \ ?G\ \g \ 0\ \t \ keys x\ show ?thesis by (rule punit.is_red_addsI[simplified]) qed with irred show False .. qed with q show "x \ sum_list ` listset (map cone qs)" by (simp add: x xs) qed qed qed qed lemma quot_monomial_ideal_monomial: "ideal (monomial 1 ` S) \
monomial 1 (Poly_Mapping.single (x::'x) (1::nat)) = ideal (monomial (1::'a::comm_ring_1) ` (\s. s - Poly_Mapping.single x 1) ` S)" proof (rule set_eqI) let ?x = "Poly_Mapping.single x (1::nat)" fix a have "a \ ideal (monomial 1 ` S) \
monomial 1 ?x \ punit.monom_mult 1 ?x a \ ideal (monomial (1::'a) ` S)" by (simp only: quot_set_iff times_monomial_left) also have "\ \ a \ ideal (monomial 1 ` (\s. s - ?x) ` S)" proof (induct a rule: poly_mapping_plus_induct) case 1 show ?case by (simp add: ideal.span_zero) next case (2 a c t) let ?S = "monomial (1::'a) ` (\s. s - ?x) ` S" show ?case proof assume 0: "punit.monom_mult 1 ?x (monomial c t + a) \ ideal (monomial 1 ` S)" have "is_monomial_set (monomial (1::'a) ` S)" by (auto intro!: is_monomial_setI monomial_is_monomial) moreover from 0 have 1: "monomial c (?x + t) + punit.monom_mult 1 ?x a \ ideal (monomial 1 ` S)" by (simp add: punit.monom_mult_monomial punit.monom_mult_dist_right) moreover have "?x + t \ keys (monomial c (?x + t) + punit.monom_mult 1 ?x a)" proof (intro in_keys_plusI1 notI) from 2(1) show "?x + t \ keys (monomial c (?x + t))" by simp next assume "?x + t \ keys (punit.monom_mult 1 ?x a)" also have "\ \ (+) ?x ` keys a" by (rule punit.keys_monom_mult_subset[simplified]) finally obtain s where "s \ keys a" and "?x + t = ?x + s" .. from this(2) have "t = s" by simp with \s \ keys a\ 2(2) show False by simp qed ultimately obtain f where "f \ monomial (1::'a) ` S" and adds: "lpp f adds ?x + t" by (rule punit.keys_monomial_pmdl[simplified]) from this(1) obtain s where "s \ S" and f: "f = monomial 1 s" .. from adds have "s adds ?x + t" by (simp add: f punit.lt_monomial) hence "s - ?x adds t" by (metis (no_types, lifting) add_minus_2 adds_minus adds_triv_right plus_minus_assoc_pm_nat_1) then obtain s' where t: "t = (s - ?x) + s'" by (rule addsE) from \s \ S\ have "monomial 1 (s - ?x) \ ?S" by (intro imageI) also have "\ \ ideal ?S" by (rule ideal.span_superset) finally have "monomial c s' * monomial 1 (s - ?x) \ ideal ?S" by (rule ideal.span_scale) hence "monomial c t \ ideal ?S" by (simp add: times_monomial_monomial t add.commute) moreover have "a \ ideal ?S" proof - from \f \ monomial 1 ` S\ have "f \ ideal (monomial 1 ` S)" by (rule ideal.span_base) hence "punit.monom_mult c (?x + t - s) f \ ideal (monomial 1 ` S)" by (rule punit.pmdl_closed_monom_mult[simplified]) with \s adds ?x + t\ have "monomial c (?x + t) \ ideal (monomial 1 ` S)" by (simp add: f punit.monom_mult_monomial adds_minus) with 1 have "monomial c (?x + t) + punit.monom_mult 1 ?x a - monomial c (?x + t) \ ideal (monomial 1 ` S)" by (rule ideal.span_diff) thus ?thesis by (simp add: 2(3) del: One_nat_def) qed ultimately show "monomial c t + a \ ideal ?S" by (rule ideal.span_add) next have "is_monomial_set ?S" by (auto intro!: is_monomial_setI monomial_is_monomial) moreover assume 1: "monomial c t + a \ ideal ?S" moreover from _ 2(2) have "t \ keys (monomial c t + a)" proof (rule in_keys_plusI1) from 2(1) show "t \ keys (monomial c t)" by simp qed ultimately obtain f where "f \ ?S" and adds: "lpp f adds t" by (rule punit.keys_monomial_pmdl[simplified]) from this(1) obtain s where "s \ S" and f: "f = monomial 1 (s - ?x)" by blast from adds have "s - ?x adds t" by (simp add: f punit.lt_monomial) hence "s adds ?x + t" by (auto simp: adds_poly_mapping le_fun_def lookup_add lookup_minus lookup_single when_def split: if_splits) then obtain s' where t: "?x + t = s + s'" by (rule addsE) from \s \ S\ have "monomial 1 s \ monomial 1 ` S" by (rule imageI) also have "\ \ ideal (monomial 1 ` S)" by (rule ideal.span_superset) finally have "monomial c s' * monomial 1 s \ ideal (monomial 1 ` S)" by (rule ideal.span_scale) hence "monomial c (?x + t) \ ideal (monomial 1 ` S)" by (simp only: t) (simp add: times_monomial_monomial add.commute) moreover have "punit.monom_mult 1 ?x a \ ideal (monomial 1 ` S)" proof - from \f \ ?S\ have "f \ ideal ?S" by (rule ideal.span_base) hence "punit.monom_mult c (t - (s - ?x)) f \ ideal ?S" by (rule punit.pmdl_closed_monom_mult[simplified]) with \s - ?x adds t\ have "monomial c t \ ideal ?S" by (simp add: f punit.monom_mult_monomial adds_minus) with 1 have "monomial c t + a - monomial c t \ ideal ?S" by (rule ideal.span_diff) thus ?thesis by (simp add: 2(3) del: One_nat_def) qed ultimately have "monomial c (?x + t) + punit.monom_mult 1 ?x a \ ideal (monomial 1 ` S)" by (rule ideal.span_add) thus "punit.monom_mult 1 ?x (monomial c t + a) \ ideal (monomial 1 ` S)" by (simp add: punit.monom_mult_monomial punit.monom_mult_dist_right) qed qed finally show "a \ ideal (monomial 1 ` S) \
monomial 1 ?x \ a \ ideal (monomial 1 ` (\s. s - ?x) ` S)" . qed lemma lem_4_2_1: assumes "ideal F \
monomial 1 t = ideal (monomial (1::'a::comm_ring_1) ` S)" shows "cone (monomial 1 t, U) \ ideal F \ 0 \ S" proof have "monomial 1 t \ cone (monomial (1::'a) t, U)" by (rule tip_in_cone) also assume "cone (monomial 1 t, U) \ ideal F" finally have *: "monomial 1 t * 1 \ ideal F" by simp have "is_monomial_set (monomial (1::'a) ` S)" by (auto intro!: is_monomial_setI monomial_is_monomial) moreover from * have "1 \ ideal (monomial (1::'a) ` S)" by (simp only: quot_set_iff flip: assms) moreover have "0 \ keys (1::_ \\<^sub>0 'a)" by simp ultimately obtain g where "g \ monomial (1::'a) ` S" and adds: "lpp g adds 0" by (rule punit.keys_monomial_pmdl[simplified]) from this(1) obtain s where "s \ S" and g: "g = monomial 1 s" .. from adds have "s adds 0" by (simp add: g punit.lt_monomial flip: single_one) with \s \ S\ show "0 \ S" by (simp only: adds_zero) next assume "0 \ S" hence "monomial 1 0 \ monomial (1::'a) ` S" by (rule imageI) hence "1 \ ideal (monomial (1::'a) ` S)" unfolding single_one by (rule ideal.span_base) hence eq: "ideal F \
monomial 1 t = UNIV" (is "_ \
?t = _") by (simp only: assms ideal_eq_UNIV_iff_contains_one) show "cone (monomial 1 t, U) \ ideal F" proof fix a assume "a \ cone (?t, U)" then obtain q where a: "a = q * ?t" by (rule coneE) have "q \ ideal F \
?t" by (simp add: eq) thus "a \ ideal F" by (simp only: a quot_set_iff mult.commute) qed qed lemma lem_4_2_2: assumes "ideal F \
monomial 1 t = ideal (monomial (1::'a::comm_ring_1) ` S)" shows "cone (monomial 1 t, U) \ ideal F = {0} \ S \ .[U] = {}" proof let ?t = "monomial (1::'a) t" assume eq: "cone (?t, U) \ ideal F = {0}" { fix s assume "s \ S" hence "monomial 1 s \ monomial (1::'a) ` S" (is "?s \ _") by (rule imageI) hence "?s \ ideal (monomial 1 ` S)" by (rule ideal.span_base) also have "\ = ideal F \
?t" by (simp only: assms) finally have *: "?s * ?t \ ideal F" by (simp only: quot_set_iff mult.commute) assume "s \ .[U]" hence "?s \ P[U]" by (rule Polys_closed_monomial) with refl have "?s * ?t \ cone (?t, U)" by (rule coneI) with * have "?s * ?t \ cone (?t, U) \ ideal F" by simp hence False by (simp add: eq times_monomial_monomial monomial_0_iff) } thus "S \ .[U] = {}" by blast next let ?t = "monomial (1::'a) t" assume eq: "S \ .[U] = {}" { fix a assume "a \ cone (?t, U)" then obtain q where "q \ P[U]" and a: "a = q * ?t" by (rule coneE) assume "a \ ideal F" have "a = 0" proof (rule ccontr) assume "a \ 0" hence "q \ 0" by (auto simp: a) from \a \ ideal F\ have *: "q \ ideal F \
?t" by (simp only: quot_set_iff a mult.commute) have "is_monomial_set (monomial (1::'a) ` S)" by (auto intro!: is_monomial_setI monomial_is_monomial) moreover from * have q_in: "q \ ideal (monomial 1 ` S)" by (simp only: assms) moreover from \q \ 0\ have "lpp q \ keys q" by (rule punit.lt_in_keys) ultimately obtain g where "g \ monomial (1::'a) ` S" and adds: "lpp g adds lpp q" by (rule punit.keys_monomial_pmdl[simplified]) from this(1) obtain s where "s \ S" and g: "g = monomial 1 s" .. from \q \ 0\ have "lpp q \ keys q" by (rule punit.lt_in_keys) also from \q \ P[U]\ have "\ \ .[U]" by (rule PolysD) finally have "lpp q \ .[U]" . moreover from adds have "s adds lpp q" by (simp add: g punit.lt_monomial) ultimately have "s \ .[U]" by (rule PPs_closed_adds) with eq \s \ S\ show False by blast qed } thus "cone (?t, U) \ ideal F = {0}" using zero_in_cone ideal.span_zero by blast qed subsection \Function \split\\ definition max_subset :: "'a set \ ('a set \ bool) \ 'a set" where "max_subset A P = (ARG_MAX card B. B \ A \ P B)" lemma max_subset: assumes "finite A" and "B \ A" and "P B" shows "max_subset A P \ A" (is ?thesis1) and "P (max_subset A P)" (is ?thesis2) and "card B \ card (max_subset A P)" (is ?thesis3) proof - from assms(2, 3) have "B \ A \ P B" by simp moreover have "\C. C \ A \ P C \ card C < Suc (card A)" proof (intro allI impI, elim conjE) fix C assume "C \ A" with assms(1) have "card C \ card A" by (rule card_mono) thus "card C < Suc (card A)" by simp qed ultimately have "?thesis1 \ ?thesis2" and ?thesis3 unfolding max_subset_def by (rule arg_max_natI, rule arg_max_nat_le) thus ?thesis1 and ?thesis2 and ?thesis3 by simp_all qed function (domintros) split :: "('x \\<^sub>0 nat) \ 'x set \ ('x \\<^sub>0 nat) set \ ((((('x \\<^sub>0 nat) \\<^sub>0 'a) \ ('x set)) list) \ (((('x \\<^sub>0 nat) \\<^sub>0 'a::{zero,one}) \ ('x set)) list))" where "split t U S = (if 0 \ S then ([(monomial 1 t, U)], []) else if S \ .[U] = {} then ([], [(monomial 1 t, U)]) else let x = SOME x'. x' \ U - (max_subset U (\V. S \ .[V] = {})); (ps0, qs0) = split t (U - {x}) S; (ps1, qs1) = split (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` S) in (ps0 @ ps1, qs0 @ qs1))" by auto text \Function @{const split} is not executable, because this is not necessary. With some effort, it could be made executable, though.\ lemma split_domI': assumes "finite X" and "fst (snd args) \ X" and "finite (snd (snd args))" shows "split_dom TYPE('a::{zero,one}) args" proof - let ?m = "\args'. card (fst (snd args')) + sum deg_pm (snd (snd args'))" from wf_measure[of ?m] assms(2, 3) show ?thesis proof (induct args) case (less args) obtain t U F where args: "args = (t, U, F)" using prod.exhaust by metis from less.prems have "U \ X" and "finite F" by (simp_all only: args fst_conv snd_conv) from this(1) assms(1) have "finite U" by (rule finite_subset) have IH: "split_dom TYPE('a) (t', U', F')" if "U' \ X" and "finite F'" and "card U' + sum deg_pm F' < card U + sum deg_pm F" for t' U' F' using less.hyps that by (simp add: args) define S where "S = max_subset U (\V. F \ .[V] = {})" define x where "x = (SOME x'. x' \ U \ x' \ S)" show ?case unfolding args proof (rule split.domintros, simp_all only: x_def[symmetric] S_def[symmetric]) fix f assume "0 \ F" and "f \ F" and "f \ .[U]" from this(1) have "F \ .[{}] = {}" by simp with \finite U\ empty_subsetI have "S \ U" and "F \ .[S] = {}" unfolding S_def by (rule max_subset)+ have "x \ U \ x \ S" unfolding x_def proof (rule someI_ex) from \f \ F\ \f \ .[U]\ \F \ .[S] = {}\ have "S \ U" by blast with \S \ U\ show "\y. y \ U \ y \ S" by blast qed hence "x \ U" and "x \ S" by simp_all { assume "\ split_dom TYPE('a) (t, U - {x}, F)" moreover from _ \finite F\ have "split_dom TYPE('a) (t, U - {x}, F)" proof (rule IH) from \U \ X\ show "U - {x} \ X" by blast next from \finite U\ \x \ U\ have "card (U - {x}) < card U" by (rule card_Diff1_less) thus "card (U - {x}) + sum deg_pm F < card U + sum deg_pm F" by simp qed ultimately show False .. } { let ?args = "(Poly_Mapping.single x (Suc 0) + t, U, (\f. f - Poly_Mapping.single x (Suc 0)) ` F)" assume "\ split_dom TYPE('a) ?args" moreover from \U \ X\ have "split_dom TYPE('a) ?args" proof (rule IH) from \finite F\ show "finite ((\f. f - Poly_Mapping.single x (Suc 0)) ` F)" by (rule finite_imageI) next have "sum deg_pm ((\f. f - Poly_Mapping.single x (Suc 0)) ` F) \ sum (deg_pm \ (\f. f - Poly_Mapping.single x (Suc 0))) F" using \finite F\ by (rule sum_image_le) simp also from \finite F\ have "\ < sum deg_pm F" proof (rule sum_strict_mono_ex1) show "\f\F. (deg_pm \ (\f. f - Poly_Mapping.single x (Suc 0))) f \ deg_pm f" by (simp add: deg_pm_minus_le) next show "\f\F. (deg_pm \ (\f. f - Poly_Mapping.single x (Suc 0))) f < deg_pm f" proof (rule ccontr) assume *: "\ (\f\F. (deg_pm \ (\f. f - Poly_Mapping.single x (Suc 0))) f < deg_pm f)" note \finite U\ moreover from \x \ U\ \S \ U\ have "insert x S \ U" by (rule insert_subsetI) moreover have "F \ .[insert x S] = {}" proof - { fix s assume "s \ F" with * have "\ deg_pm (s - Poly_Mapping.single x (Suc 0)) < deg_pm s" by simp with deg_pm_minus_le[of s "Poly_Mapping.single x (Suc 0)"] have "deg_pm (s - Poly_Mapping.single x (Suc 0)) = deg_pm s" by simp hence "keys s \ keys (Poly_Mapping.single x (Suc 0)) = {}" by (simp only: deg_pm_minus_id_iff) hence "x \ keys s" by simp moreover assume "s \ .[insert x S]" ultimately have "s \ .[S]" by (fastforce simp: PPs_def) with \s \ F\ \F \ .[S] = {}\ have False by blast } thus ?thesis by blast qed ultimately have "card (insert x S) \ card S" unfolding S_def by (rule max_subset) moreover from \S \ U\ \finite U\ have "finite S" by (rule finite_subset) ultimately show False using \x \ S\ by simp qed qed finally show "card U + sum deg_pm ((\f. f - monomial (Suc 0) x) ` F) < card U + sum deg_pm F" by simp qed ultimately show False .. } qed qed qed corollary split_domI: "finite X \ U \ X \ finite S \ split_dom TYPE('a::{zero,one}) (t, U, S)" using split_domI'[of "(t, U, S)"] by simp lemma split_empty: assumes "finite X" and "U \ X" shows "split t U {} = ([], [(monomial (1::'a::{zero,one}) t, U)])" proof - have "finite {}" .. with assms have "split_dom TYPE('a) (t, U, {})" by (rule split_domI) thus ?thesis by (simp add: split.psimps) qed lemma split_induct [consumes 3, case_names base1 base2 step]: fixes P :: "('x \\<^sub>0 nat) \ _" assumes "finite X" and "U \ X" and "finite S" assumes "\t U S. U \ X \ finite S \ 0 \ S \ P t U S ([(monomial (1::'a::{zero,one}) t, U)], [])" assumes "\t U S. U \ X \ finite S \ 0 \ S \ S \ .[U] = {} \ P t U S ([], [(monomial 1 t, U)])" assumes "\t U S V x ps0 ps1 qs0 qs1. U \ X \ finite S \ 0 \ S \ S \ .[U] \ {} \ V \ U \ S \ .[V] = {} \ (\V'. V' \ U \ S \ .[V'] = {} \ card V' \ card V) \ x \ U \ x \ V \ V = max_subset U (\V'. S \ .[V'] = {}) \ x = (SOME x'. x' \ U - V) \ (ps0, qs0) = split t (U - {x}) S \ (ps1, qs1) = split (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` S) \ split t U S = (ps0 @ ps1, qs0 @ qs1) \ P t (U - {x}) S (ps0, qs0) \ P (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` S) (ps1, qs1) \ P t U S (ps0 @ ps1, qs0 @ qs1)" shows "P t U S (split t U S)" proof - from assms(1-3) have "split_dom TYPE('a) (t, U, S)" by (rule split_domI) thus ?thesis using assms(2,3) proof (induct t U S rule: split.pinduct) case step: (1 t U F) from step(4) assms(1) have "finite U" by (rule finite_subset) define S where "S = max_subset U (\V. F \ .[V] = {})" define x where "x = (SOME x'. x' \ U \ x' \ S)" show ?case proof (simp add: split.psimps[OF step(1)] S_def[symmetric] x_def[symmetric] split: prod.split, intro allI conjI impI) assume "0 \ F" with step(4, 5) show "P t U F ([(monomial 1 t, U)], [])" by (rule assms(4)) thus "P t U F ([(monomial 1 t, U)], [])" . next assume "0 \ F" and "F \ .[U] = {}" with step(4, 5) show "P t U F ([], [(monomial 1 t, U)])" by (rule assms(5)) next fix ps0 qs0 ps1 qs1 :: "((_ \\<^sub>0 'a) \ _) list" assume "split (Poly_Mapping.single x (Suc 0) + t) U ((\f. f - Poly_Mapping.single x (Suc 0)) ` F) = (ps1, qs1)" hence PQ1[symmetric]: "split (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` F) = (ps1, qs1)" by simp assume PQ0[symmetric]: "split t (U - {x}) F = (ps0, qs0)" assume "F \ .[U] \ {}" and "0 \ F" from this(2) have "F \ .[{}] = {}" by simp with \finite U\ empty_subsetI have "S \ U" and "F \ .[S] = {}" unfolding S_def by (rule max_subset)+ have S_max: "card S' \ card S" if "S' \ U" and "F \ .[S'] = {}" for S' using \finite U\ that unfolding S_def by (rule max_subset) have "x \ U \ x \ S" unfolding x_def proof (rule someI_ex) from \F \ .[U] \ {}\ \F \ .[S] = {}\ have "S \ U" by blast with \S \ U\ show "\y. y \ U \ y \ S" by blast qed hence "x \ U" and "x \ S" by simp_all from step(4, 5) \0 \ F\ \F \ .[U] \ {}\ \S \ U\ \F \ .[S] = {}\ S_max \x \ U\ \x \ S\ S_def _ PQ0 PQ1 show "P t U F (ps0 @ ps1, qs0 @ qs1)" proof (rule assms(6)) show "P t (U - {x}) F (ps0, qs0)" unfolding PQ0 using \0 \ F\ \F \ .[U] \ {}\ _ _ step(5) proof (rule step(2)) from \U \ X\ show "U - {x} \ X" by fastforce qed (simp add: x_def S_def) next show "P (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` F) (ps1, qs1)" unfolding PQ1 using \0 \ F\ \F \ .[U] \ {}\ _ refl PQ0 \U \ X\ proof (rule step(3)) from \finite F\ show "finite ((\f. f - Poly_Mapping.single x 1) ` F)" by (rule finite_imageI) qed (simp add: x_def S_def) next show "split t U F = (ps0 @ ps1, qs0 @ qs1)" using \0 \ F\ \F \ .[U] \ {}\ by (simp add: split.psimps[OF step(1)] Let_def flip: S_def x_def PQ0 PQ1 del: One_nat_def) qed (assumption+, simp add: x_def S_def) qed qed qed lemma valid_decomp_split: assumes "finite X" and "U \ X" and "finite S" and "t \ .[X]" shows "valid_decomp X (fst ((split t U S)::(_ \ (((_ \\<^sub>0 'a::zero_neq_one) \ _) list))))" and "valid_decomp X (snd ((split t U S)::(_ \ (((_ \\<^sub>0 'a::zero_neq_one) \ _) list))))" (is "valid_decomp _ (snd ?s)") proof - from assms have "valid_decomp X (fst ?s) \ valid_decomp X (snd ?s)" proof (induct t U S rule: split_induct) case (base1 t U S) from base1(1, 4) show ?case by (simp add: valid_decomp_def monomial_0_iff Polys_closed_monomial) next case (base2 t U S) from base2(1, 5) show ?case by (simp add: valid_decomp_def monomial_0_iff Polys_closed_monomial) next case (step t U S V x ps0 ps1 qs0 qs1) from step.hyps(8, 1) have "x \ X" .. hence "Poly_Mapping.single x 1 \ .[X]" by (rule PPs_closed_single) hence "Poly_Mapping.single x 1 + t \ .[X]" using step.prems by (rule PPs_closed_plus) with step.hyps(15, 16) step.prems show ?case by (simp add: valid_decomp_append) qed thus "valid_decomp X (fst ?s)" and "valid_decomp X (snd ?s)" by simp_all qed lemma monomial_decomp_split: assumes "finite X" and "U \ X" and "finite S" shows "monomial_decomp (fst ((split t U S)::(_ \ (((_ \\<^sub>0 'a::zero_neq_one) \ _) list))))" and "monomial_decomp (snd ((split t U S)::(_ \ (((_ \\<^sub>0 'a::zero_neq_one) \ _) list))))" (is "monomial_decomp (snd ?s)") proof - from assms have "monomial_decomp (fst ?s) \ monomial_decomp (snd ?s)" proof (induct t U S rule: split_induct) case (base1 t U S) from base1(1) show ?case by (simp add: monomial_decomp_def monomial_is_monomial) next case (base2 t U S) from base2(1) show ?case by (simp add: monomial_decomp_def monomial_is_monomial) next case (step t U S V x ps0 ps1 qs0 qs1) from step.hyps(15, 16) show ?case by (auto simp: monomial_decomp_def) qed thus "monomial_decomp (fst ?s)" and "monomial_decomp (snd ?s)" by simp_all qed lemma split_splits_wrt: assumes "finite X" and "U \ X" and "finite S" and "t \ .[X]" and "ideal F \
monomial 1 t = ideal (monomial 1 ` S)" shows "splits_wrt (split t U S) (cone (monomial (1::'a::{comm_ring_1,ring_no_zero_divisors}) t, U)) F" using assms proof (induct t U S rule: split_induct) case (base1 t U S) from base1(3) have "cone (monomial 1 t, U) \ ideal F" by (simp only: lem_4_2_1 base1(5)) show ?case proof (rule splits_wrtI) fix h0 U0 assume "(h0, U0) \ set [(monomial (1::'a) t, U)]" hence h0: "h0 = monomial 1 t" and "U0 = U" by simp_all note this(1) also have "monomial 1 t \ cone (monomial (1::'a) t, U)" by (fact tip_in_cone) also have "\ \ ideal F" by fact finally show "h0 \ ideal F" . from base1(4) have "h0 \ P[X]" unfolding h0 by (rule Polys_closed_monomial) moreover from base1(1) have "U0 \ X" by (simp only: \U0 = U\) ultimately show "cone (h0, U0) \ P[X]" by (rule cone_subset_PolysI) qed (simp_all add: cone_decomp_singleton \U \ X\) next case (base2 t U S) from base2(4) have "cone (monomial 1 t, U) \ ideal F = {0}" by (simp only: lem_4_2_2 base2(6)) show ?case proof (rule splits_wrtI) fix h0 U0 assume "(h0, U0) \ set [(monomial (1::'a) t, U)]" hence h0: "h0 = monomial 1 t" and "U0 = U" by simp_all note this(1) also from base2(5) have "monomial 1 t \ P[X]" by (rule Polys_closed_monomial) finally have "h0 \ P[X]" . moreover from base2(1) have "U0 \ X" by (simp only: \U0 = U\) ultimately show "cone (h0, U0) \ P[X]" by (rule cone_subset_PolysI) next fix h0 U0 a assume "(h0, U0) \ set [(monomial (1::'a) t, U)]" and "a \ cone (h0, U0)" hence "a \ cone (monomial 1 t, U)" by simp moreover assume "a \ ideal F" ultimately have "a \ cone (monomial 1 t, U) \ ideal F" by (rule IntI) also have "\ = {0}" by fact finally show "a = 0" by simp qed (simp_all add: cone_decomp_singleton \U \ X\) next case (step t U S V x ps0 ps1 qs0 qs1) let ?x = "Poly_Mapping.single x 1" from step.prems have 0: "splits_wrt (ps0, qs0) (cone (monomial 1 t, U - {x})) F" by (rule step.hyps) have 1: "splits_wrt (ps1, qs1) (cone (monomial 1 (?x + t), U)) F" proof (rule step.hyps) from step.hyps(8, 1) have "x \ X" .. hence "?x \ .[X]" by (rule PPs_closed_single) thus "?x + t \ .[X]" using step.prems(1) by (rule PPs_closed_plus) next have "ideal F \
monomial 1 (?x + t) = ideal F \
monomial 1 t \
monomial 1 ?x" by (simp add: times_monomial_monomial add.commute) also have "\ = ideal (monomial 1 ` S) \
monomial 1 ?x" by (simp only: step.prems) finally show "ideal F \
monomial 1 (?x + t) = ideal (monomial 1 ` (\s. s - ?x) ` S)" by (simp only: quot_monomial_ideal_monomial) qed show ?case proof (rule splits_wrtI) from step.hyps(8) have U: "insert x U = U" by blast have "direct_decomp (cone (monomial (1::'a) t, insert x (U - {x}))) [cone (monomial 1 t, U - {x}), cone (monomial 1 (monomial (Suc 0) x) * monomial 1 t, insert x (U - {x}))]" by (rule direct_decomp_cone_insert) simp hence "direct_decomp (cone (monomial (1::'a) t, U)) [cone (monomial 1 t, U - {x}), cone (monomial 1 (?x + t), U)]" by (simp add: U times_monomial_monomial) moreover from 0 have "cone_decomp (cone (monomial 1 t, U - {x})) (ps0 @ qs0)" by (rule splits_wrtD) moreover from 1 have "cone_decomp (cone (monomial 1 (?x + t), U)) (ps1 @ qs1)" by (rule splits_wrtD) ultimately have "cone_decomp (cone (monomial 1 t, U)) ((ps0 @ qs0) @ (ps1 @ qs1))" by (rule cone_decomp_append) thus "cone_decomp (cone (monomial 1 t, U)) ((ps0 @ ps1) @ qs0 @ qs1)" by (rule cone_decomp_perm) (metis append.assoc perm_append1 perm_append2 perm_append_swap) next fix h0 U0 assume "(h0, U0) \ set (ps0 @ ps1)" hence "(h0, U0) \ set ps0 \ set ps1" by simp hence "cone (h0, U0) \ ideal F \ P[X]" proof assume "(h0, U0) \ set ps0" with 0 show ?thesis by (rule splits_wrtD) next assume "(h0, U0) \ set ps1" with 1 show ?thesis by (rule splits_wrtD) qed hence *: "cone (h0, U0) \ ideal F" and "cone (h0, U0) \ P[X]" by simp_all from this(2) show "cone (h0, U0) \ P[X]" . from tip_in_cone * show "h0 \ ideal F" .. next fix h0 U0 assume "(h0, U0) \ set (qs0 @ qs1)" hence "(h0, U0) \ set qs0 \ set qs1" by simp thus "cone (h0, U0) \ P[X]" proof assume "(h0, U0) \ set qs0" with 0 show ?thesis by (rule splits_wrtD) next assume "(h0, U0) \ set qs1" with 1 show ?thesis by (rule splits_wrtD) qed from \(h0, U0) \ set qs0 \ set qs1\ have "cone (h0, U0) \ ideal F = {0}" proof assume "(h0, U0) \ set qs0" with 0 show ?thesis by (rule splits_wrtD) next assume "(h0, U0) \ set qs1" with 1 show ?thesis by (rule splits_wrtD) qed thus "\a. a \ cone (h0, U0) \ a \ ideal F \ a = 0" by blast qed qed lemma lem_4_5: assumes "finite X" and "U \ X" and "t \ .[X]" and "F \ P[X]" and "ideal F \
monomial 1 t = ideal (monomial (1::'a) ` S)" and "cone (monomial (1::'a::field) t', V) \ cone (monomial 1 t, U) \ normal_form F ` P[X]" shows "V \ U" and "S \ .[V] = {}" proof - let ?t = "monomial (1::'a) t" let ?t' = "monomial (1::'a) t'" from assms(6) have 1: "cone (?t', V) \ cone (?t, U)" and 2: "cone (?t', V) \ normal_form F ` P[X]" by blast+ from this(1) show "V \ U" by (rule cone_subsetD) (simp add: monomial_0_iff) show "S \ .[V] = {}" proof let ?t = "monomial (1::'a) t" let ?t' = "monomial (1::'a) t'" show "S \ .[V] \ {}" proof fix s assume "s \ S \ .[V]" hence "s \ S" and "s \ .[V]" by simp_all from this(2) have "monomial (1::'a) s \ P[V]" (is "?s \ _") by (rule Polys_closed_monomial) with refl have "?s * ?t \ cone (?t, V)" by (rule coneI) from tip_in_cone 1 have "?t' \ cone (?t, U)" .. then obtain s' where "s' \ P[U]" and t': "?t' = s' * ?t" by (rule coneE) note this(1) also from assms(2) have "P[U] \ P[X]" by (rule Polys_mono) finally have "s' \ P[X]" . have "s' * ?s * ?t = ?s * ?t'" by (simp add: t') also from refl \?s \ P[V]\ have "\ \ cone (?t', V)" by (rule coneI) finally have "s' * ?s * ?t \ cone (?t', V)" . hence 1: "s' * ?s * ?t \ normal_form F ` P[X]" using 2 .. from \s \ S\ have "?s \ monomial 1 ` S" by (rule imageI) hence "?s \ ideal (monomial 1 ` S)" by (rule ideal.span_base) hence "s' * ?s \ ideal (monomial 1 ` S)" by (rule ideal.span_scale) hence "s' * ?s \ ideal F \
?t" by (simp only: assms(5)) hence "s' * ?s * ?t \ ideal F" by (simp only: quot_set_iff mult.commute) hence "s' * ?s * ?t \ ideal F \ normal_form F ` P[X]" using 1 by (rule IntI) also from assms(1, 4) have "\ \ {0}" by (auto simp: normal_form_normal_form simp flip: normal_form_zero_iff) finally have "?s * ?t' = 0" by (simp add: t' ac_simps) thus "s \ {}" by (simp add: times_monomial_monomial monomial_0_iff) qed qed (fact empty_subsetI) qed lemma lem_4_6: assumes "finite X" and "U \ X" and "finite S" and "t \ .[X]" and "F \ P[X]" and "ideal F \
monomial 1 t = ideal (monomial 1 ` S)" assumes "cone (monomial 1 t', V) \ cone (monomial 1 t, U) \ normal_form F ` P[X]" obtains V' where "(monomial 1 t, V') \ set (snd (split t U S))" and "card V \ card V'" proof - let ?t = "monomial (1::'a) t" let ?t' = "monomial (1::'a) t'" from assms(7) have "cone (?t', V) \ cone (?t, U)" and "cone (?t', V) \ normal_form F ` P[X]" by blast+ from assms(1, 2, 4, 5, 6, 7) have "V \ U" and "S \ .[V] = {}" by (rule lem_4_5)+ with assms(1, 2, 3) show ?thesis using that proof (induct t U S arbitrary: V thesis rule: split_induct) case (base1 t U S) from base1.hyps(3) have "0 \ S \ .[V]" using zero_in_PPs by (rule IntI) thus ?case by (simp add: base1.prems(2)) next case (base2 t U S) show ?case proof (rule base2.prems) from base2.hyps(1) assms(1) have "finite U" by (rule finite_subset) thus "card V \ card U" using base2.prems(1) by (rule card_mono) qed simp next case (step t U S V0 x ps0 ps1 qs0 qs1) from step.prems(1, 2) have 0: "card V \ card V0" by (rule step.hyps) from step.hyps(5, 9) have "V0 \ U - {x}" by blast then obtain V' where 1: "(monomial 1 t, V') \ set (snd (ps0, qs0))" and 2: "card V0 \ card V'" using step.hyps(6) by (rule step.hyps) show ?case proof (rule step.prems) from 1 show "(monomial 1 t, V') \ set (snd (ps0 @ ps1, qs0 @ qs1))" by simp next from 0 2 show "card V \ card V'" by (rule le_trans) qed qed qed lemma lem_4_7: assumes "finite X" and "S \ .[X]" and "g \ punit.reduced_GB (monomial (1::'a) ` S)" and "cone_decomp (P[X] \ ideal (monomial (1::'a::field) ` S)) ps" and "monomial_decomp ps" obtains U where "(g, U) \ set ps" proof - let ?S = "monomial (1::'a) ` S" let ?G = "punit.reduced_GB ?S" note assms(1) moreover from assms(2) have "?S \ P[X]" by (auto intro: Polys_closed_monomial) moreover have "is_monomial_set ?S" by (auto intro!: is_monomial_setI monomial_is_monomial) ultimately have "is_monomial_set ?G" by (rule reduced_GB_is_monomial_set_Polys) hence "is_monomial g" using assms(3) by (rule is_monomial_setD) hence "g \ 0" by (rule monomial_not_0) moreover from assms(1) \?S \ P[X]\ have "punit.is_monic_set ?G" by (rule reduced_GB_is_monic_set_Polys) ultimately have "punit.lc g = 1" using assms(3) by (simp add: punit.is_monic_set_def) moreover define t where "t = lpp g" moreover from \is_monomial g\ have "monomial (punit.lc g) (lpp g) = g" by (rule punit.monomial_eq_itself) ultimately have g: "g = monomial 1 t" by simp hence "t \ keys g" by simp from assms(3) have "g \ ideal ?G" by (rule ideal.span_base) also from assms(1) \?S \ P[X]\ have ideal_G: "\ = ideal ?S" by (rule reduced_GB_ideal_Polys) finally have "g \ ideal ?S" . moreover from assms(3) have "g \ P[X]" by rule (intro reduced_GB_Polys assms(1) \?S \ P[X]\) ultimately have "g \ P[X] \ ideal ?S" by simp with assms(4) have "g \ sum_list ` listset (map cone ps)" by (simp only: cone_decomp_def direct_decompD) with assms(5) obtain d h U where *: "(h, U) \ set ps" and "d \ 0" and "monomial d t \ cone (h, U)" using \t \ keys g\ by (rule monomial_decomp_sum_list_monomial_in_cone) from this(3) zero_in_PPs have "punit.monom_mult (1 / d) 0 (monomial d t) \ cone (h, U)" by (rule cone_closed_monom_mult) with \d \ 0\ have "g \ cone (h, U)" by (simp add: g punit.monom_mult_monomial) then obtain q where "q \ P[U]" and g': "g = q * h" by (rule coneE) from \g \ 0\ have "q \ 0" and "h \ 0" by (auto simp: g') hence lt_g': "lpp g = lpp q + lpp h" unfolding g' by (rule lp_times) hence adds1: "lpp h adds t" by (simp add: t_def) from assms(5) * have "is_monomial h" and "punit.lc h = 1" by (rule monomial_decompD)+ moreover from this(1) have "monomial (punit.lc h) (lpp h) = h" by (rule punit.monomial_eq_itself) moreover define s where "s = lpp h" ultimately have h: "h = monomial 1 s" by simp have "punit.lc q = punit.lc g" by (simp add: g' lc_times \punit.lc h = 1\) hence "punit.lc q = 1" by (simp only: \punit.lc g = 1\) note tip_in_cone also from assms(4) * have "cone (h, U) \ P[X] \ ideal ?S" by (rule cone_decomp_cone_subset) also have "\ \ ideal ?G" by (simp add: ideal_G) finally have "h \ ideal ?G" . from assms(1) \?S \ P[X]\ have "punit.is_Groebner_basis ?G" by (rule reduced_GB_is_GB_Polys) then obtain g' where "g' \ ?G" and "g' \ 0" and adds2: "lpp g' adds lpp h" using \h \ ideal ?G\ \h \ 0\ by (rule punit.GB_adds_lt[simplified]) from this(3) adds1 have "lpp g' adds t" by (rule adds_trans) with _ \g' \ 0\ \t \ keys g\ have "punit.is_red {g'} g" by (rule punit.is_red_addsI[simplified]) simp have "g' = g" proof (rule ccontr) assume "g' \ g" with \g' \ ?G\ have "{g'} \ ?G - {g}" by simp with \punit.is_red {g'} g\ have red: "punit.is_red (?G - {g}) g" by (rule punit.is_red_subset) from assms(1) \?S \ P[X]\ have "punit.is_auto_reduced ?G" by (rule reduced_GB_is_auto_reduced_Polys) hence "\ punit.is_red (?G - {g}) g" using assms(3) by (rule punit.is_auto_reducedD) thus False using red .. qed with adds2 have "t adds lpp h" by (simp only: t_def) with adds1 have "lpp h = t" by (rule adds_antisym) hence "lpp q = 0" using lt_g' by (simp add: t_def) hence "monomial (punit.lc q) 0 = q" by (rule punit.lt_eq_min_term_monomial[simplified]) hence "g = h" by (simp add: \punit.lc q = 1\ g') with * have "(g, U) \ set ps" by simp thus ?thesis .. qed lemma snd_splitI: assumes "finite X" and "U \ X" and "finite S" and "0 \ S" obtains V where "V \ U" and "(monomial 1 t, V) \ set (snd (split t U S))" using assms proof (induct t U S arbitrary: thesis rule: split_induct) case (base1 t U S) from base1.prems(2) base1.hyps(3) show ?case .. next case (base2 t U S) from subset_refl show ?case by (rule base2.prems) simp next case (step t U S V0 x ps0 ps1 qs0 qs1) from step.hyps(3) obtain V where 1: "V \ U - {x}" and 2: "(monomial 1 t, V) \ set (snd (ps0, qs0))" using step.hyps(15) by blast show ?case proof (rule step.prems) from 1 show "V \ U" by blast next from 2 show "(monomial 1 t, V) \ set (snd (ps0 @ ps1, qs0 @ qs1))" by fastforce qed qed lemma fst_splitE: assumes "finite X" and "U \ X" and "finite S" and "0 \ S" and "(monomial (1::'a) s, V) \ set (fst (split t U S))" obtains t' x where "t' \ .[X]" and "x \ X" and "V \ U" and "0 \ (\s. s - t') ` S" and "s = t' + t + Poly_Mapping.single x 1" and "(monomial (1::'a::zero_neq_one) s, V) \ set (fst (split (t' + t) V ((\s. s - t') ` S)))" and "set (snd (split (t' + t) V ((\s. s - t') ` S))) \ (set (snd (split t U S)) :: ((_ \\<^sub>0 'a) \ _) set)" using assms proof (induct t U S arbitrary: thesis rule: split_induct) case (base1 t U S) from base1.prems(2) base1.hyps(3) show ?case .. next case (base2 t U S) from base2.prems(3) show ?case by simp next case (step t U S V0 x ps0 ps1 qs0 qs1) from step.prems(3) have "(monomial 1 s, V) \ set ps0 \ set ps1" by simp thus ?case proof assume "(monomial 1 s, V) \ set ps0" hence "(monomial (1::'a) s, V) \ set (fst (ps0, qs0))" by (simp only: fst_conv) with step.hyps(3) obtain t' x' where "t' \ .[X]" and "x' \ X" and "V \ U - {x}" and "0 \ (\s. s - t') ` S" and "s = t' + t + Poly_Mapping.single x' 1" and "(monomial (1::'a) s, V) \ set (fst (split (t' + t) V ((\s. s - t') ` S)))" and "set (snd (split (t' + t) V ((\s. s - t') ` S))) \ set (snd (ps0, qs0))" using step.hyps(15) by blast note this(7) also have "set (snd (ps0, qs0)) \ set (snd (ps0 @ ps1, qs0 @ qs1))" by simp finally have "set (snd (split (t' + t) V ((\s. s - t') ` S))) \ set (snd (ps0 @ ps1, qs0 @ qs1))" . from \V \ U - {x}\ have "V \ U" by blast show ?thesis by (rule step.prems) fact+ next assume "(monomial 1 s, V) \ set ps1" show ?thesis proof (cases "0 \ (\f. f - Poly_Mapping.single x 1) ` S") case True from step.hyps(2) have fin: "finite ((\f. f - Poly_Mapping.single x 1) ` S)" by (rule finite_imageI) have "split (Poly_Mapping.single x 1 + t) U ((\f. f - Poly_Mapping.single x 1) ` S) = ([(monomial (1::'a) (Poly_Mapping.single x 1 + t), U)], [])" by (simp only: split.psimps[OF split_domI, OF assms(1) step.hyps(1) fin] True if_True) hence "ps1 = [(monomial 1 (Poly_Mapping.single x 1 + t), U)]" by (simp only: step.hyps(13)[symmetric] prod.inject) with \(monomial 1 s, V) \ set ps1\ have s: "s = Poly_Mapping.single x 1 + t" and "V = U" by (auto dest!: monomial_inj) show ?thesis proof (rule step.prems) show "0 \ .[X]" by (fact zero_in_PPs) next from step.hyps(8, 1) show "x \ X" .. next show "V \ U" by (simp add: \V = U\) next from step.hyps(3) show "0 \ (\s. s - 0) ` S" by simp next show "s = 0 + t + Poly_Mapping.single x 1" by (simp add: s add.commute) next show "(monomial (1::'a) s, V) \ set (fst (split (0 + t) V ((\s. s - 0) ` S)))" using \(monomial 1 s, V) \ set ps1\ by (simp add: step.hyps(14) \V = U\) next show "set (snd (split (0 + t) V ((\s. s - 0) ` S))) \ set (snd (ps0 @ ps1, qs0 @ qs1))" by (simp add: step.hyps(14) \V = U\) qed next case False moreover from \(monomial 1 s, V) \ set ps1\ have "(monomial 1 s, V) \ set (fst (ps1, qs1))" by (simp only: fst_conv) ultimately obtain t' x' where "t' \ .[X]" and "x' \ X" and "V \ U" and 1: "0 \ (\s. s - t') ` (\f. f - Poly_Mapping.single x 1) ` S" and s: "s = t' + (Poly_Mapping.single x 1 + t) + Poly_Mapping.single x' 1" and 2: "(monomial (1::'a) s, V) \ set (fst (split (t' + (Poly_Mapping.single x 1 + t)) V ((\s. s - t') ` (\f. f - Poly_Mapping.single x 1) ` S)))" and 3: "set (snd (split (t' + (Poly_Mapping.single x 1 + t)) V ((\s. s - t') ` (\f. f - monomial 1 x) ` S))) \ set (snd (ps1, qs1))" using step.hyps(16) by blast have eq: "(\s. s - t') ` (\f. f - Poly_Mapping.single x 1) ` S = (\s. s - (t' + Poly_Mapping.single x 1)) ` S" by (simp add: image_image add.commute diff_diff_eq) show ?thesis proof (rule step.prems) from step.hyps(8, 1) have "x \ X" .. hence "Poly_Mapping.single x 1 \ .[X]" by (rule PPs_closed_single) with \t' \ .[X]\ show "t' + Poly_Mapping.single x 1 \ .[X]" by (rule PPs_closed_plus) next from 1 show "0 \ (\s. s - (t' + Poly_Mapping.single x 1)) ` S" by (simp only: eq not_False_eq_True) next show "s = t' + Poly_Mapping.single x 1 + t + Poly_Mapping.single x' 1" by (simp only: s ac_simps) next show "(monomial (1::'a) s, V) \ set (fst (split (t' + Poly_Mapping.single x 1 + t) V ((\s. s - (t' + Poly_Mapping.single x 1)) ` S)))" using 2 by (simp only: eq add.assoc) next have "set (snd (split (t' + Poly_Mapping.single x 1 + t) V ((\s. s - (t' + Poly_Mapping.single x 1)) ` S))) \ set (snd (ps1, qs1))" (is "?x \ _") using 3 by (simp only: eq add.assoc) also have "\ \ set (snd (ps0 @ ps1, qs0 @ qs1))" by simp finally show "?x \ set (snd (ps0 @ ps1, qs0 @ qs1))" . qed fact+ qed qed qed lemma lem_4_8: assumes "finite X" and "finite S" and "S \ .[X]" and "0 \ S" and "g \ punit.reduced_GB (monomial (1::'a) ` S)" obtains t U where "U \ X" and "(monomial (1::'a::field) t, U) \ set (snd (split 0 X S))" and "poly_deg g = Suc (deg_pm t)" proof - let ?S = "monomial (1::'a) ` S" let ?G = "punit.reduced_GB ?S" have md1: "monomial_decomp (fst ((split 0 X S)::(_ \ (((_ \\<^sub>0 'a) \ _) list))))" and md2: "monomial_decomp (snd ((split 0 X S)::(_ \ (((_ \\<^sub>0 'a) \ _) list))))" using assms(1) subset_refl assms(2) by (rule monomial_decomp_split)+ from assms(3) have 0: "?S \ P[X]" by (auto intro: Polys_closed_monomial) with assms(1) have "punit.is_auto_reduced ?G" and "punit.is_monic_set ?G" and ideal_G: "ideal ?G = ideal ?S" and "0 \ ?G" by (rule reduced_GB_is_auto_reduced_Polys, rule reduced_GB_is_monic_set_Polys, rule reduced_GB_ideal_Polys, rule reduced_GB_nonzero_Polys) from this(2, 4) assms(5) have "punit.lc g = 1" by (auto simp: punit.is_monic_set_def) have "is_monomial_set ?S" by (auto intro!: is_monomial_setI monomial_is_monomial) with assms(1) 0 have "is_monomial_set ?G" by (rule reduced_GB_is_monomial_set_Polys) hence "is_monomial g" using assms(5) by (rule is_monomial_setD) moreover define s where "s = lpp g" ultimately have g: "g = monomial 1 s" using \punit.lc g = 1\ by (metis punit.monomial_eq_itself) note assms(1) subset_refl assms(2) zero_in_PPs moreover have "ideal ?G \
monomial 1 0 = ideal ?S" by (simp add: ideal_G) ultimately have "splits_wrt (split 0 X S) (cone (monomial (1::'a) 0, X)) ?G" by (rule split_splits_wrt) hence "splits_wrt (fst (split 0 X S), snd (split 0 X S)) P[X] ?G" by simp hence "cone_decomp (P[X] \ ideal ?G) (fst (split 0 X S))" using md2 \is_monomial_set ?G\ by (rule splits_wrt_cone_decomp_1) hence "cone_decomp (P[X] \ ideal ?S) (fst (split 0 X S))" by (simp only: ideal_G) with assms(1, 3, 5) obtain U where "(g, U) \ set (fst (split 0 X S))" using md1 by (rule lem_4_7) with assms(1) subset_refl assms(2, 4) obtain t' x where "t' \ .[X]" and "x \ X" and "U \ X" and "0 \ (\s. s - t') ` S" and s: "s = t' + 0 + Poly_Mapping.single x 1" and "(g, U) \ set (fst (split (t' + 0) U ((\s. s - t') ` S)))" and "set (snd (split (t' + 0) U ((\s. s - t') ` S))) \ (set (snd (split 0 X S)) :: ((_ \\<^sub>0 'a) \ _) set)" unfolding g by (rule fst_splitE) let ?S = "(\s. s - t') ` S" from assms(2) have "finite ?S" by (rule finite_imageI) with assms(1) \U \ X\ obtain V where "V \ U" and "(monomial (1::'a) (t' + 0), V) \ set (snd (split (t' + 0) U ?S))" using \0 \ ?S\ by (rule snd_splitI) note this(2) also have "\ \ set (snd (split 0 X S))" by fact finally have "(monomial (1::'a) t', V) \ set (snd (split 0 X S))" by simp have "poly_deg g = Suc (deg_pm t')" by (simp add: g s deg_pm_plus deg_pm_single poly_deg_monomial) from \V \ U\ \U \ X\ have "V \ X" by (rule subset_trans) show ?thesis by rule fact+ qed corollary cor_4_9: assumes "finite X" and "finite S" and "S \ .[X]" and "g \ punit.reduced_GB (monomial (1::'a::field) ` S)" shows "poly_deg g \ Suc (Max (poly_deg ` fst ` (set (snd (split 0 X S)) :: ((_ \\<^sub>0 'a) \ _) set)))" (is "_ \ Suc (Max (poly_deg ` fst ` ?S))") proof (cases "0 \ S") case True hence "1 \ monomial (1::'a) ` S" by (rule rev_image_eqI) (simp only: single_one) hence "1 \ ideal (monomial (1::'a) ` S)" by (rule ideal.span_base) hence "ideal (monomial (1::'a) ` S) = UNIV" by (simp only: ideal_eq_UNIV_iff_contains_one) moreover from assms(3) have "monomial (1::'a) ` S \ P[X]" by (auto intro: Polys_closed_monomial) ultimately have "punit.reduced_GB (monomial (1::'a) ` S) = {1}" using assms(1) by (simp only: ideal_eq_UNIV_iff_reduced_GB_eq_one_Polys) with assms(4) show ?thesis by simp next case False from finite_set have fin: "finite (poly_deg ` fst ` ?S)" by (intro finite_imageI) obtain t U where "(monomial 1 t, U) \ ?S" and g: "poly_deg g = Suc (deg_pm t)" using assms(1-3) False assms(4) by (rule lem_4_8) from this(1) have "poly_deg (fst (monomial (1::'a) t, U)) \ poly_deg ` fst ` ?S" by (intro imageI) hence "deg_pm t \ poly_deg ` fst ` ?S" by (simp add: poly_deg_monomial) with fin have "deg_pm t \ Max (poly_deg ` fst ` ?S)" by (rule Max_ge) thus "poly_deg g \ Suc (Max (poly_deg ` fst ` ?S))" by (simp add: g) qed lemma standard_decomp_snd_split: assumes "finite X" and "U \ X" and "finite S" and "S \ .[X]" and "t \ .[X]" shows "standard_decomp (deg_pm t) (snd (split t U S) :: ((_ \\<^sub>0 'a::field) \ _) list)" using assms proof (induct t U S rule: split_induct) case (base1 t U S) show ?case by (simp add: standard_decomp_Nil) next case (base2 t U S) have "deg_pm t = poly_deg (monomial (1::'a) t)" by (simp add: poly_deg_monomial) thus ?case by (simp add: standard_decomp_singleton) next case (step t U S V x ps0 ps1 qs0 qs1) from step.hyps(15) step.prems have qs0: "standard_decomp (deg_pm t) qs0" by (simp only: snd_conv) have "(\s. s - Poly_Mapping.single x 1) ` S \ .[X]" proof fix u assume "u \ (\s. s - Poly_Mapping.single x 1) ` S" then obtain s where "s \ S" and u: "u = s - Poly_Mapping.single x 1" .. from this(1) step.prems(1) have "s \ .[X]" .. thus "u \ .[X]" unfolding u by (rule PPs_closed_minus) qed moreover from _ step.prems(2) have "Poly_Mapping.single x 1 + t \ .[X]" proof (rule PPs_closed_plus) from step.hyps(8, 1) have "x \ X" .. thus "Poly_Mapping.single x 1 \ .[X]" by (rule PPs_closed_single) qed ultimately have qs1: "standard_decomp (Suc (deg_pm t)) qs1" using step.hyps(16) by (simp add: deg_pm_plus deg_pm_single) show ?case unfolding snd_conv proof (rule standard_decompI) fix h U0 assume "(h, U0) \ set ((qs0 @ qs1)\<^sub>+)" hence *: "(h, U0) \ set (qs0\<^sub>+) \ set (qs1\<^sub>+)" by (simp add: pos_decomp_append) thus "deg_pm t \ poly_deg h" proof assume "(h, U0) \ set (qs0\<^sub>+)" with qs0 show ?thesis by (rule standard_decompD) next assume "(h, U0) \ set (qs1\<^sub>+)" with qs1 have "Suc (deg_pm t) \ poly_deg h" by (rule standard_decompD) thus ?thesis by simp qed fix d assume d1: "deg_pm t \ d" and d2: "d \ poly_deg h" from * show "\t' U'. (t', U') \ set (qs0 @ qs1) \ poly_deg t' = d \ card U0 \ card U'" proof assume "(h, U0) \ set (qs0\<^sub>+)" with qs0 obtain h' U' where "(h', U') \ set qs0" and "poly_deg h' = d" and "card U0 \ card U'" using d1 d2 by (rule standard_decompE) moreover from this(1) have "(h', U') \ set (qs0 @ qs1)" by simp ultimately show ?thesis by blast next assume "(h, U0) \ set (qs1\<^sub>+)" hence "(h, U0) \ set qs1" by (simp add: pos_decomp_def) from assms(1) step.hyps(1, 2) have "monomial_decomp (snd (split t U S) :: ((_ \\<^sub>0 'a) \ _) list)" by (rule monomial_decomp_split) hence md: "monomial_decomp (qs0 @ qs1)" by (simp add: step.hyps(14)) moreover from \(h, U0) \ set qs1\ have "(h, U0) \ set (qs0 @ qs1)" by simp ultimately have "is_monomial h" and "punit.lc h = 1" by (rule monomial_decompD)+ moreover from this(1) have "monomial (punit.lc h) (lpp h) = h" by (rule punit.monomial_eq_itself) moreover define s where "s = lpp h" ultimately have h: "h = monomial 1 s" by simp from d1 have "deg_pm t = d \ Suc (deg_pm t) \ d" by auto thus ?thesis proof assume "deg_pm t = d" define F where "F = (*) (monomial 1 t) ` monomial (1::'a) ` S" have "F \ P[X]" proof fix f assume "f \ F" then obtain u where "u \ S" and f: "f = monomial 1 (t + u)" by (auto simp: F_def times_monomial_monomial) from this(1) step.prems(1) have "u \ .[X]" .. with step.prems(2) have "t + u \ .[X]" by (rule PPs_closed_plus) thus "f \ P[X]" unfolding f by (rule Polys_closed_monomial) qed have "ideal F = (*) (monomial 1 t) ` ideal (monomial 1 ` S)" by (simp only: ideal.span_image_scale_eq_image_scale F_def) moreover have "inj ((*) (monomial (1::'a) t))" by (auto intro!: injI simp: times_monomial_left monomial_0_iff dest!: punit.monom_mult_inj_3) ultimately have eq: "ideal F \
monomial 1 t = ideal (monomial 1 ` S)" by (simp only: quot_set_image_times) with assms(1) step.hyps(1, 2) step.prems(2) have "splits_wrt (split t U S) (cone (monomial (1::'a) t, U)) F" by (rule split_splits_wrt) hence "splits_wrt (ps0 @ ps1, qs0 @ qs1) (cone (monomial 1 t, U)) F" by (simp only: step.hyps(14)) with assms(1) have "cone_decomp (cone (monomial (1::'a) t, U) \ normal_form F ` P[X]) (qs0 @ qs1)" using md _ \F \ P[X]\ by (rule splits_wrt_cone_decomp_2) (auto intro!: is_monomial_setI monomial_is_monomial simp: F_def times_monomial_monomial) hence "cone (monomial 1 s, U0) \ cone (monomial (1::'a) t, U) \ normal_form F ` P[X]" using \(h, U0) \ set (qs0 @ qs1)\ unfolding h by (rule cone_decomp_cone_subset) with assms(1) step.hyps(1, 2) step.prems(2) \F \ P[X]\ eq obtain U' where "(monomial (1::'a) t, U') \ set (snd (split t U S))" and "card U0 \ card U'" by (rule lem_4_6) from this(1) have "(monomial 1 t, U') \ set (qs0 @ qs1)" by (simp add: step.hyps(14)) show ?thesis proof (intro exI conjI) show "poly_deg (monomial (1::'a) t) = d" by (simp add: poly_deg_monomial \deg_pm t = d\) qed fact+ next assume "Suc (deg_pm t) \ d" with qs1 \(h, U0) \ set (qs1\<^sub>+)\ obtain h' U' where "(h', U') \ set qs1" and "poly_deg h' = d" and "card U0 \ card U'" using d2 by (rule standard_decompE) moreover from this(1) have "(h', U') \ set (qs0 @ qs1)" by simp ultimately show ?thesis by blast qed qed qed qed theorem standard_cone_decomp_snd_split: fixes F defines "G \ punit.reduced_GB F" defines "ss \ (split 0 X (lpp ` G)) :: ((_ \\<^sub>0 'a::field) \ _) list \ _" defines "d \ Suc (Max (poly_deg ` fst ` set (snd ss)))" assumes "finite X" and "F \ P[X]" shows "standard_decomp 0 (snd ss)" (is ?thesis1) and "cone_decomp (normal_form F ` P[X]) (snd ss)" (is ?thesis2) and "(\f. f \ F \ homogeneous f) \ g \ G \ poly_deg g \ d" proof - have "ideal G = ideal F" and "punit.is_Groebner_basis G" and "finite G" and "0 \ G" and "G \ P[X]" and "punit.is_reduced_GB G" using assms(4, 5) unfolding G_def by (rule reduced_GB_ideal_Polys, rule reduced_GB_is_GB_Polys, rule finite_reduced_GB_Polys, rule reduced_GB_nonzero_Polys, rule reduced_GB_Polys, rule reduced_GB_is_reduced_GB_Polys) define S where "S = lpp ` G" note assms(4) subset_refl moreover from \finite G\ have "finite S" unfolding S_def by (rule finite_imageI) moreover from \G \ P[X]\ have "S \ .[X]" unfolding S_def by (rule PPs_closed_image_lpp) ultimately have "standard_decomp (deg_pm (0::'x \\<^sub>0 nat)) (snd ss)" using zero_in_PPs unfolding ss_def S_def by (rule standard_decomp_snd_split) thus ?thesis1 by simp let ?S = "monomial (1::'a) ` S" from \S \ .[X]\ have "?S \ P[X]" by (auto intro: Polys_closed_monomial) have "splits_wrt ss (cone (monomial 1 0, X)) ?S" using assms(4) subset_refl \finite S\ zero_in_PPs unfolding ss_def S_def by (rule split_splits_wrt) simp hence "splits_wrt (fst ss, snd ss) P[X] ?S" by simp with assms(4) have "cone_decomp (P[X] \ normal_form ?S ` P[X]) (snd ss)" using _ _ \?S \ P[X]\ proof (rule splits_wrt_cone_decomp_2) from assms(4) subset_refl \finite S\ show "monomial_decomp (snd ss)" unfolding ss_def S_def by (rule monomial_decomp_split) qed (auto intro!: is_monomial_setI monomial_is_monomial) moreover have "normal_form ?S ` P[X] = normal_form F ` P[X]" by (rule set_eqI) (simp add: image_normal_form_iff[OF assms(4)] assms(5) \?S \ P[X]\, simp add: S_def is_red_reduced_GB_monomial_lt_GB_Polys[OF assms(4)] \G \ P[X]\ \0 \ G\ flip: G_def) moreover from assms(4, 5) have "normal_form F ` P[X] \ P[X]" by (auto intro: Polys_closed_normal_form) ultimately show ?thesis2 by (simp only: Int_absorb1) assume "\f. f \ F \ homogeneous f" moreover note \punit.is_reduced_GB G\ \ideal G = ideal F\ moreover assume "g \ G" ultimately have "homogeneous g" by (rule is_reduced_GB_homogeneous) moreover have "lpp g \ keys g" proof (rule punit.lt_in_keys) from \g \ G\ \0 \ G\ show "g \ 0" by blast qed ultimately have deg_lt: "deg_pm (lpp g) = poly_deg g" by (rule homogeneousD_poly_deg) from \g \ G\ have "monomial 1 (lpp g) \ ?S" unfolding S_def by (intro imageI) also have "\ = punit.reduced_GB ?S" unfolding S_def G_def using assms(4, 5) by (rule reduced_GB_monomial_lt_reduced_GB_Polys[symmetric]) finally have "monomial 1 (lpp g) \ punit.reduced_GB ?S" . with assms(4) \finite S\ \S \ .[X]\ have "poly_deg (monomial (1::'a) (lpp g)) \ d" unfolding d_def ss_def S_def[symmetric] by (rule cor_4_9) thus "poly_deg g \ d" by (simp add: poly_deg_monomial deg_lt) qed subsection \Splitting Ideals\ qualified definition ideal_decomp_aux :: "(('x \\<^sub>0 nat) \\<^sub>0 'a) set \ (('x \\<^sub>0 nat) \\<^sub>0 'a) \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::field) set \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list)" where "ideal_decomp_aux F f = (let J = ideal F; L = (J \
f) \ P[X]; L' = lpp ` punit.reduced_GB L in ((*) f ` normal_form L ` P[X], map (apfst ((*) f)) (snd (split 0 X L'))))" context assumes fin_X: "finite X" begin lemma ideal_decomp_aux: assumes "finite F" and "F \ P[X]" and "f \ P[X]" shows "fst (ideal_decomp_aux F f) \ ideal {f}" (is ?thesis1) and "ideal F \ fst (ideal_decomp_aux F f) = {0}" (is ?thesis2) and "direct_decomp (ideal (insert f F) \ P[X]) [fst (ideal_decomp_aux F f), ideal F \ P[X]]" (is ?thesis3) and "cone_decomp (fst (ideal_decomp_aux F f)) (snd (ideal_decomp_aux F f))" (is ?thesis4) and "f \ 0 \ valid_decomp X (snd (ideal_decomp_aux F f))" (is "_ \ ?thesis5") and "f \ 0 \ standard_decomp (poly_deg f) (snd (ideal_decomp_aux F f))" (is "_ \ ?thesis6") and "homogeneous f \ hom_decomp (snd (ideal_decomp_aux F f))" (is "_ \ ?thesis7") proof - define J where "J = ideal F" define L where "L = (J \
f) \ P[X]" define S where "S = (*) f ` normal_form L ` P[X]" define L' where "L' = lpp ` punit.reduced_GB L" have eq: "ideal_decomp_aux F f = (S, map (apfst ((*) f)) (snd (split 0 X L')))" by (simp add: J_def ideal_decomp_aux_def Let_def L_def L'_def S_def) have L_sub: "L \ P[X]" by (simp add: L_def) show ?thesis1 unfolding eq fst_conv proof fix s assume "s \ S" then obtain q where "s = normal_form L q * f" unfolding S_def by (elim imageE) auto also have "\ \ ideal {f}" by (intro ideal.span_scale ideal.span_base singletonI) finally show "s \ ideal {f}" . qed show ?thesis2 proof (rule set_eqI) fix h show "h \ ideal F \ fst (ideal_decomp_aux F f) \ h \ {0}" proof assume "h \ ideal F \ fst (ideal_decomp_aux F f)" hence "h \ J" and "h \ S" by (simp_all add: J_def S_def eq) from this(2) obtain q where "q \ P[X]" and h: "h = f * normal_form L q" by (auto simp: S_def) from fin_X L_sub this(1) have "normal_form L q \ P[X]" by (rule Polys_closed_normal_form) moreover from \h \ J\ have "f * normal_form L q \ J" by (simp add: h) ultimately have "normal_form L q \ L" by (simp add: L_def quot_set_iff) hence "normal_form L q \ ideal L" by (rule ideal.span_base) with normal_form_diff_in_ideal[OF fin_X L_sub] have "(q - normal_form L q) + normal_form L q \ ideal L" by (rule ideal.span_add) hence "normal_form L q = 0" using fin_X L_sub by (simp add: normal_form_zero_iff) thus "h \ {0}" by (simp add: h) next assume "h \ {0}" moreover have "0 \ (*) f ` normal_form L ` P[X]" proof (intro image_eqI) from fin_X L_sub show "0 = normal_form L 0" by (simp only: normal_form_zero) qed (simp_all add: zero_in_Polys) ultimately show "h \ ideal F \ fst (ideal_decomp_aux F f)" by (simp add: ideal.span_zero eq S_def) qed qed have "direct_decomp (ideal (insert f F) \ P[X]) [ideal F \ P[X], fst (ideal_decomp_aux F f)]" unfolding eq fst_conv S_def L_def J_def using fin_X assms(2, 3) by (rule direct_decomp_ideal_insert) thus ?thesis3 using perm.swap by (rule direct_decomp_perm) have std: "standard_decomp 0 (snd (split 0 X L') :: ((_ \\<^sub>0 'a) \ _) list)" and "cone_decomp (normal_form L ` P[X]) (snd (split 0 X L'))" unfolding L'_def using fin_X \L \ P[X]\ by (rule standard_cone_decomp_snd_split)+ from this(2) show ?thesis4 unfolding eq fst_conv snd_conv S_def by (rule cone_decomp_map_times) from fin_X \L \ P[X]\ have "finite (punit.reduced_GB L)" by (rule finite_reduced_GB_Polys) hence "finite L'" unfolding L'_def by (rule finite_imageI) { have "monomial_decomp (snd (split 0 X L') :: ((_ \\<^sub>0 'a) \ _) list)" using fin_X subset_refl \finite L'\ by (rule monomial_decomp_split) hence "hom_decomp (snd (split 0 X L') :: ((_ \\<^sub>0 'a) \ _) list)" by (rule monomial_decomp_imp_hom_decomp) moreover assume "homogeneous f" ultimately show ?thesis7 unfolding eq snd_conv by (rule hom_decomp_map_times) } have vd: "valid_decomp X (snd (split 0 X L') :: ((_ \\<^sub>0 'a) \ _) list)" using fin_X subset_refl \finite L'\ zero_in_PPs by (rule valid_decomp_split) moreover note assms(3) moreover assume "f \ 0" ultimately show ?thesis5 unfolding eq snd_conv by (rule valid_decomp_map_times) from std vd \f \ 0\ have "standard_decomp (0 + poly_deg f) (map (apfst ((*) f)) (snd (split 0 X L')))" by (rule standard_decomp_map_times) thus ?thesis6 by (simp add: eq) qed lemma ideal_decompE: fixes f0 :: "_ \\<^sub>0 'a::field" assumes "finite F" and "F \ P[X]" and "f0 \ P[X]" and "\f. f \ F \ poly_deg f \ poly_deg f0" obtains T ps where "valid_decomp X ps" and "standard_decomp (poly_deg f0) ps" and "cone_decomp T ps" and "(\f. f \ F \ homogeneous f) \ hom_decomp ps" and "direct_decomp (ideal (insert f0 F) \ P[X]) [ideal {f0} \ P[X], T]" using assms(1, 2, 4) proof (induct F arbitrary: thesis) case empty show ?case proof (rule empty.prems) show "valid_decomp X []" by (rule valid_decompI) simp_all next show "standard_decomp (poly_deg f0) []" by (rule standard_decompI) simp_all next show "cone_decomp {0} []" by (rule cone_decompI) (simp add: direct_decomp_def bij_betw_def) next have "direct_decomp (ideal {f0} \ P[X]) [ideal {f0} \ P[X]]" by (fact direct_decomp_singleton) hence "direct_decomp (ideal {f0} \ P[X]) [{0}, ideal {f0} \ P[X]]" by (rule direct_decomp_Cons_zeroI) thus "direct_decomp (ideal {f0} \ P[X]) [ideal {f0} \ P[X], {0}]" using perm.swap by (rule direct_decomp_perm) qed (simp add: hom_decomp_def) next case (insert f F) from insert.prems(2) have "F \ P[X]" by simp moreover have "poly_deg f' \ poly_deg f0" if "f' \ F" for f' proof - from that have "f' \ insert f F" by simp thus ?thesis by (rule insert.prems) qed ultimately obtain T ps where valid_ps: "valid_decomp X ps" and std_ps: "standard_decomp (poly_deg f0) ps" and cn_ps: "cone_decomp T ps" and dd: "direct_decomp (ideal (insert f0 F) \ P[X]) [ideal {f0} \ P[X], T]" and hom_ps: "(\f. f \ F \ homogeneous f) \ hom_decomp ps" using insert.hyps(3) by metis show ?case proof (cases "f = 0") case True show ?thesis proof (rule insert.prems) from dd show "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) [ideal {f0} \ P[X], T]" by (simp only: insert_commute[of f0] True ideal.span_insert_zero) next assume "\f'. f' \ insert f F \ homogeneous f'" hence "\f. f \ F \ homogeneous f" by blast thus "hom_decomp ps" by (rule hom_ps) qed fact+ next case False let ?D = "ideal_decomp_aux (insert f0 F) f" from insert.hyps(1) have f0F_fin: "finite (insert f0 F)" by simp moreover from \F \ P[X]\ assms(3) have f0F_sub: "insert f0 F \ P[X]" by simp moreover from insert.prems(2) have "f \ P[X]" by simp ultimately have eq: "ideal (insert f0 F) \ fst ?D = {0}" and "valid_decomp X (snd ?D)" and cn_D: "cone_decomp (fst ?D) (snd ?D)" and "standard_decomp (poly_deg f) (snd ?D)" and dd': "direct_decomp (ideal (insert f (insert f0 F)) \ P[X]) [fst ?D, ideal (insert f0 F) \ P[X]]" and hom_D: "homogeneous f \ hom_decomp (snd ?D)" by (rule ideal_decomp_aux, auto intro: ideal_decomp_aux simp: False) note fin_X this(2-4) moreover have "poly_deg f \ poly_deg f0" by (rule insert.prems) simp ultimately obtain qs where valid_qs: "valid_decomp X qs" and cn_qs: "cone_decomp (fst ?D) qs" and std_qs: "standard_decomp (poly_deg f0) qs" and hom_qs: "hom_decomp (snd ?D) \ hom_decomp qs" by (rule standard_decomp_geE) blast let ?T = "sum_list ` listset [T, fst ?D]" let ?ps = "ps @ qs" show ?thesis proof (rule insert.prems) from valid_ps valid_qs show "valid_decomp X ?ps" by (rule valid_decomp_append) next from std_ps std_qs show "standard_decomp (poly_deg f0) ?ps" by (rule standard_decomp_append) next from dd perm.swap have "direct_decomp (ideal (insert f0 F) \ P[X]) [T, ideal {f0} \ P[X]]" by (rule direct_decomp_perm) hence "T \ ideal (insert f0 F) \ P[X]" by (rule direct_decomp_Cons_subsetI) (simp add: ideal.span_zero zero_in_Polys) hence "T \ fst ?D \ ideal (insert f0 F) \ fst ?D" by blast hence "T \ fst ?D \ {0}" by (simp only: eq) from refl have "direct_decomp ?T [T, fst ?D]" proof (intro direct_decompI inj_onI) fix xs ys assume "xs \ listset [T, fst ?D]" then obtain x1 x2 where "x1 \ T" and "x2 \ fst ?D" and xs: "xs = [x1, x2]" by (rule listset_doubletonE) assume "ys \ listset [T, fst ?D]" then obtain y1 y2 where "y1 \ T" and "y2 \ fst ?D" and ys: "ys = [y1, y2]" by (rule listset_doubletonE) assume "sum_list xs = sum_list ys" hence "x1 - y1 = y2 - x2" by (simp add: xs ys) (metis add_diff_cancel_left add_diff_cancel_right) moreover from cn_ps \x1 \ T\ \y1 \ T\ have "x1 - y1 \ T" by (rule cone_decomp_closed_minus) moreover from cn_D \y2 \ fst ?D\ \x2 \ fst ?D\ have "y2 - x2 \ fst ?D" by (rule cone_decomp_closed_minus) ultimately have "y2 - x2 \ T \ fst ?D" by simp also have "\ \ {0}" by fact finally have "x2 = y2" by simp with \x1 - y1 = y2 - x2\ show "xs = ys" by (simp add: xs ys) qed thus "cone_decomp ?T ?ps" using cn_ps cn_qs by (rule cone_decomp_append) next assume "\f'. f' \ insert f F \ homogeneous f'" hence "homogeneous f" and "\f'. f' \ F \ homogeneous f'" by blast+ from this(2) have "hom_decomp ps" by (rule hom_ps) moreover from \homogeneous f\ have "hom_decomp qs" by (intro hom_qs hom_D) ultimately show "hom_decomp (ps @ qs)" by (simp only: hom_decomp_append_iff) next from dd' have "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) [ideal (insert f0 F) \ P[X], fst ?D]" by (simp add: insert_commute direct_decomp_perm perm.swap) hence "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) ([fst ?D] @ [ideal {f0} \ P[X], T])" using dd by (rule direct_decomp_direct_decomp) hence "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) ([ideal {f0} \ P[X]] @ [T, fst ?D])" by (rule direct_decomp_perm) auto hence "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) [sum_list ` listset [ideal {f0} \ P[X]], ?T]" by (rule direct_decomp_appendD) thus "direct_decomp (ideal (insert f0 (insert f F)) \ P[X]) [ideal {f0} \ P[X], ?T]" by (simp add: image_image) qed qed qed subsection \Exact Cone Decompositions\ definition exact_decomp :: "nat \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ bool" where "exact_decomp m ps \ (\(h, U)\set ps. h \ P[X] \ U \ X) \ (\(h, U)\set ps. \(h', U')\set ps. poly_deg h = poly_deg h' \ m < card U \ m < card U' \ (h, U) = (h', U'))" lemma exact_decompI: "(\h U. (h, U) \ set ps \ h \ P[X]) \ (\h U. (h, U) \ set ps \ U \ X) \ (\h h' U U'. (h, U) \ set ps \ (h', U') \ set ps \ poly_deg h = poly_deg h' \ m < card U \ m < card U' \ (h, U) = (h', U')) \ exact_decomp m ps" unfolding exact_decomp_def by fastforce lemma exact_decompD: assumes "exact_decomp m ps" and "(h, U) \ set ps" shows "h \ P[X]" and "U \ X" and "(h', U') \ set ps \ poly_deg h = poly_deg h' \ m < card U \ m < card U' \ (h, U) = (h', U')" using assms unfolding exact_decomp_def by fastforce+ lemma exact_decompI_zero: assumes "\h U. (h, U) \ set ps \ h \ P[X]" and "\h U. (h, U) \ set ps \ U \ X" and "\h h' U U'. (h, U) \ set (ps\<^sub>+) \ (h', U') \ set (ps\<^sub>+) \ poly_deg h = poly_deg h' \ (h, U) = (h', U')" shows "exact_decomp 0 ps" using assms(1, 2) proof (rule exact_decompI) fix h h' and U U' :: "'x set" assume "0 < card U" hence "U \ {}" by auto moreover assume "(h, U) \ set ps" ultimately have "(h, U) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) assume "0 < card U'" hence "U' \ {}" by auto moreover assume "(h', U') \ set ps" ultimately have "(h', U') \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) assume "poly_deg h = poly_deg h'" with \(h, U) \ set (ps\<^sub>+)\ \(h', U') \ set (ps\<^sub>+)\ show "(h, U) = (h', U')" by (rule assms(3)) qed lemma exact_decompD_zero: assumes "exact_decomp 0 ps" and "(h, U) \ set (ps\<^sub>+)" and "(h', U') \ set (ps\<^sub>+)" and "poly_deg h = poly_deg h'" shows "(h, U) = (h', U')" proof - from assms(2) have "(h, U) \ set ps" and "U \ {}" by (simp_all add: pos_decomp_def) from assms(1) this(1) have "U \ X" by (rule exact_decompD) hence "finite U" using fin_X by (rule finite_subset) with \U \ {}\ have "0 < card U" by (simp add: card_gt_0_iff) from assms(3) have "(h', U') \ set ps" and "U' \ {}" by (simp_all add: pos_decomp_def) from assms(1) this(1) have "U' \ X" by (rule exact_decompD) hence "finite U'" using fin_X by (rule finite_subset) with \U' \ {}\ have "0 < card U'" by (simp add: card_gt_0_iff) show ?thesis by (rule exact_decompD) fact+ qed lemma exact_decomp_imp_valid_decomp: assumes "exact_decomp m ps" and "\h U. (h, U) \ set ps \ h \ 0" shows "valid_decomp X ps" proof (rule valid_decompI) fix h U assume *: "(h, U) \ set ps" with assms(1) show "h \ P[X]" and "U \ X" by (rule exact_decompD)+ from * show "h \ 0" by (rule assms(2)) qed lemma exact_decomp_card_X: assumes "valid_decomp X ps" and "card X \ m" shows "exact_decomp m ps" proof (rule exact_decompI) fix h U assume "(h, U) \ set ps" with assms(1) show "h \ P[X]" and "U \ X" by (rule valid_decompD)+ next fix h1 h2 U1 U2 assume "(h1, U1) \ set ps" with assms(1) have "U1 \ X" by (rule valid_decompD) with fin_X have "card U1 \ card X" by (rule card_mono) also have "\ \ m" by (fact assms(2)) also assume "m < card U1" finally show "(h1, U1) = (h2, U2)" by simp qed definition \ :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ nat" where "\ ps = (LEAST k. standard_decomp k ps)" definition \ :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ nat \ nat" where "\ ps i = (LEAST d. \ ps \ d \ (\(h, U)\set ps. i \ card U \ poly_deg h < d))" lemma \: "standard_decomp k ps \ standard_decomp (\ ps) ps" unfolding \_def by (rule LeastI) lemma \_Nil: assumes "ps\<^sub>+ = []" shows "\ ps = 0" proof - from assms have "standard_decomp 0 ps" by (rule standard_decomp_Nil) thus ?thesis unfolding \_def by (rule Least_eq_0) qed lemma \_nonempty: assumes "valid_decomp X ps" and "standard_decomp k ps" and "ps\<^sub>+ \ []" shows "\ ps = Min (poly_deg ` fst ` set (ps\<^sub>+))" using fin_X assms(1) _ assms(3) proof (rule standard_decomp_nonempty_unique) from assms(2) show "standard_decomp (\ ps) ps" by (rule \) qed lemma \_nonempty_unique: assumes "valid_decomp X ps" and "standard_decomp k ps" and "ps\<^sub>+ \ []" shows "\ ps = k" proof - from assms have "\ ps = Min (poly_deg ` fst ` set (ps\<^sub>+))" by (rule \_nonempty) moreover from fin_X assms have "k = Min (poly_deg ` fst ` set (ps\<^sub>+))" by (rule standard_decomp_nonempty_unique) ultimately show ?thesis by simp qed lemma \: shows "\ ps \ \ ps i" and "(h, U) \ set ps \ i \ card U \ poly_deg h < \ ps i" proof - let ?A = "poly_deg ` fst ` set ps" define A where "A = insert (\ ps) ?A" define m where "m = Suc (Max A)" from finite_set have "finite ?A" by (intro finite_imageI) hence "finite A" by (simp add: A_def) have "\ ps \ \ ps i \ (\(h', U')\set ps. i \ card U' \ poly_deg h' < \ ps i)" unfolding \_def proof (rule LeastI) have "\ ps \ A" by (simp add: A_def) with \finite A\ have "\ ps \ Max A" by (rule Max_ge) hence "\ ps \ m" by (simp add: m_def) moreover { fix h U assume "(h, U) \ set ps" hence "poly_deg (fst (h, U)) \ ?A" by (intro imageI) hence "poly_deg h \ A" by (simp add: A_def) with \finite A\ have "poly_deg h \ Max A" by (rule Max_ge) hence "poly_deg h < m" by (simp add: m_def) } ultimately show "\ ps \ m \ (\(h, U)\set ps. i \ card U \ poly_deg h < m)" by blast qed thus "\ ps \ \ ps i" and "(h, U) \ set ps \ i \ card U \ poly_deg h < \ ps i" by blast+ qed lemma \_le: "\ ps \ d \ (\h' U'. (h', U') \ set ps \ i \ card U' \ poly_deg h' < d) \ \ ps i \ d" unfolding \_def by (intro Least_le) blast lemma \_decreasing: assumes "i \ j" shows "\ ps j \ \ ps i" proof (rule \_le) fix h U assume "(h, U) \ set ps" assume "j \ card U" with assms(1) have "i \ card U" by (rule le_trans) with \(h, U) \ set ps\ show "poly_deg h < \ ps i" by (rule \) qed (fact \) lemma \_Nil: assumes "ps\<^sub>+ = []" and "Suc 0 \ i" shows "\ ps i = 0" unfolding \_def proof (rule Least_eq_0) from assms(1) have "\ ps = 0" by (rule \_Nil) moreover { fix h and U::"'x set" note assms(2) also assume "i \ card U" finally have "U \ {}" by auto moreover assume "(h, U) \ set ps" ultimately have "(h, U) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) hence False by (simp add: assms) } ultimately show "\ ps \ 0 \ (\(h, U)\set ps. i \ card U \ poly_deg h < 0)" by blast qed lemma \_zero: assumes "ps \ []" shows "Suc (Max (poly_deg ` fst ` set ps)) \ \ ps 0" proof - from finite_set have "finite (poly_deg ` fst ` set ps)" by (intro finite_imageI) moreover from assms have "poly_deg ` fst ` set ps \ {}" by simp moreover have "\a\poly_deg ` fst ` set ps. a < \ ps 0" proof fix d assume "d \ poly_deg ` fst ` set ps" then obtain p where "p \ set ps" and "d = poly_deg (fst p)" by blast moreover obtain h U where "p = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set ps" and d: "d = poly_deg h" by simp_all from this(1) le0 show "d < \ ps 0" unfolding d by (rule \) qed ultimately have "Max (poly_deg ` fst ` set ps) < \ ps 0" by simp thus ?thesis by simp qed corollary \_zero_gr: assumes "(h, U) \ set ps" shows "poly_deg h < \ ps 0" proof - have "poly_deg h \ Max (poly_deg ` fst ` set ps)" proof (rule Max_ge) from finite_set show "finite (poly_deg ` fst ` set ps)" by (intro finite_imageI) next from assms have "poly_deg (fst (h, U)) \ poly_deg ` fst ` set ps" by (intro imageI) thus "poly_deg h \ poly_deg ` fst ` set ps" by simp qed also have "\ < Suc \" by simp also have "\ \ \ ps 0" proof (rule \_zero) from assms show "ps \ []" by auto qed finally show ?thesis . qed lemma \_one: assumes "valid_decomp X ps" and "standard_decomp k ps" shows "\ ps (Suc 0) = (if ps\<^sub>+ = [] then 0 else Suc (Max (poly_deg ` fst ` set (ps\<^sub>+))))" proof (cases "ps\<^sub>+ = []") case True hence "\ ps (Suc 0) = 0" using le_refl by (rule \_Nil) with True show ?thesis by simp next case False with assms have aP: "\ ps = Min (poly_deg ` fst ` set (ps\<^sub>+))" (is "_ = Min ?A") by (rule \_nonempty) from pos_decomp_subset finite_set have "finite (set (ps\<^sub>+))" by (rule finite_subset) hence "finite ?A" by (intro finite_imageI) from False have "?A \ {}" by simp have "\ ps (Suc 0) = Suc (Max ?A)" unfolding \_def proof (rule Least_equality) from \finite ?A\ \?A \ {}\ have "\ ps \ ?A" unfolding aP by (rule Min_in) with \finite ?A\ have "\ ps \ Max ?A" by (rule Max_ge) hence "\ ps \ Suc (Max ?A)" by simp moreover { fix h U assume "(h, U) \ set ps" with fin_X assms(1) have "finite U" by (rule valid_decompD_finite) moreover assume "Suc 0 \ card U" ultimately have "U \ {}" by auto with \(h, U) \ set ps\ have "(h, U) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) hence "poly_deg (fst (h, U)) \ ?A" by (intro imageI) hence "poly_deg h \ ?A" by (simp only: fst_conv) with \finite ?A\ have "poly_deg h \ Max ?A" by (rule Max_ge) hence "poly_deg h < Suc (Max ?A)" by simp } ultimately show "\ ps \ Suc (Max ?A) \ (\(h, U)\set ps. Suc 0 \ card U \ poly_deg h < Suc (Max ?A))" by blast next fix d assume "\ ps \ d \ (\(h, U)\set ps. Suc 0 \ card U \ poly_deg h < d)" hence rl: "poly_deg h < d" if "(h, U) \ set ps" and "0 < card U" for h U using that by auto have "Max ?A < d" unfolding Max_less_iff[OF \finite ?A\ \?A \ {}\] proof fix d0 assume "d0 \ poly_deg ` fst ` set (ps\<^sub>+)" then obtain h U where "(h, U) \ set (ps\<^sub>+)" and d0: "d0 = poly_deg h" by auto from this(1) have "(h, U) \ set ps" and "U \ {}" by (simp_all add: pos_decomp_def) from fin_X assms(1) this(1) have "finite U" by (rule valid_decompD_finite) with \U \ {}\ have "0 < card U" by (simp add: card_gt_0_iff) with \(h, U) \ set ps\ show "d0 < d" unfolding d0 by (rule rl) qed thus "Suc (Max ?A) \ d" by simp qed with False show ?thesis by simp qed corollary \_one_gr: assumes "valid_decomp X ps" and "standard_decomp k ps" and "(h, U) \ set (ps\<^sub>+)" shows "poly_deg h < \ ps (Suc 0)" proof - from assms(3) have "ps\<^sub>+ \ []" by auto with assms(1, 2) have eq: "\ ps (Suc 0) = Suc (Max (poly_deg ` fst ` set (ps\<^sub>+)))" by (simp add: \_one) have "poly_deg h \ Max (poly_deg ` fst ` set (ps\<^sub>+))" proof (rule Max_ge) from finite_set show "finite (poly_deg ` fst ` set (ps\<^sub>+))" by (intro finite_imageI) next from assms(3) have "poly_deg (fst (h, U)) \ poly_deg ` fst ` set (ps\<^sub>+)" by (intro imageI) thus "poly_deg h \ poly_deg ` fst ` set (ps\<^sub>+)" by simp qed also have "\ < \ ps (Suc 0)" by (simp add: eq) finally show ?thesis . qed lemma \_card_X: assumes "exact_decomp m ps" and "Suc (card X) \ i" shows "\ ps i = \ ps" unfolding \_def proof (rule Least_equality) { fix h U assume "(h, U) \ set ps" with assms(1) have "U \ X" by (rule exact_decompD) note assms(2) also assume "i \ card U" finally have "card X < card U" by simp with fin_X have "\ U \ X" by (auto dest: card_mono leD) hence False using \U \ X\ .. } thus "\ ps \ \ ps \ (\(h, U)\set ps. i \ card U \ poly_deg h < \ ps)" by blast qed simp lemma lem_6_1_1: assumes "standard_decomp k ps" and "exact_decomp m ps" and "Suc 0 \ i" and "i \ card X" and "\ ps (Suc i) \ d" and "d < \ ps i" obtains h U where "(h, U) \ set (ps\<^sub>+)" and "poly_deg h = d" and "card U = i" proof - have "ps\<^sub>+ \ []" proof assume "ps\<^sub>+ = []" hence "\ ps i = 0" using assms(3) by (rule \_Nil) with assms(6) show False by simp qed have eq1: "\ ps (Suc (card X)) = \ ps" using assms(2) le_refl by (rule \_card_X) from assms(1) have std: "standard_decomp (\ ps (Suc (card X))) ps" unfolding eq1 by (rule \) from assms(4) have "Suc i \ Suc (card X)" .. hence "\ ps (Suc (card X)) \ \ ps (Suc i)" by (rule \_decreasing) hence "\ ps \ \ ps (Suc i)" by (simp only: eq1) have "\h U. (h, U) \ set ps \ i \ card U \ \ ps i \ Suc (poly_deg h)" proof (rule ccontr) assume *: "\h U. (h, U) \ set ps \ i \ card U \ \ ps i \ Suc (poly_deg h)" note \\ ps \ \ ps (Suc i)\ also from assms(5, 6) have "\ ps (Suc i) < \ ps i" by (rule le_less_trans) finally have "\ ps < \ ps i" . hence "\ ps \ \ ps i - 1" by simp hence "\ ps i \ \ ps i - 1" proof (rule \_le) fix h U assume "(h, U) \ set ps" and "i \ card U" show "poly_deg h < \ ps i - 1" proof (rule ccontr) assume "\ poly_deg h < \ ps i - 1" hence "\ ps i \ Suc (poly_deg h)" by simp with * \(h, U) \ set ps\ \i \ card U\ show False by auto qed qed thus False using \\ ps < \ ps i\ by linarith qed then obtain h U where "(h, U) \ set ps" and "i \ card U" and "\ ps i \ Suc (poly_deg h)" by blast from assms(3) this(2) have "U \ {}" by auto with \(h, U) \ set ps\ have "(h, U) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) note std this moreover have "\ ps (Suc (card X)) \ d" unfolding eq1 using \\ ps \ \ ps (Suc i)\ assms(5) by (rule le_trans) moreover have "d \ poly_deg h" proof - from assms(6) \\ ps i \ Suc (poly_deg h)\ have "d < Suc (poly_deg h)" by (rule less_le_trans) thus ?thesis by simp qed ultimately obtain h' U' where "(h', U') \ set ps" and d: "poly_deg h' = d" and "card U \ card U'" by (rule standard_decompE) from \i \ card U\ this(3) have "i \ card U'" by (rule le_trans) with assms(3) have "U' \ {}" by auto with \(h', U') \ set ps\ have "(h', U') \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) moreover note \poly_deg h' = d\ moreover have "card U' = i" proof (rule ccontr) assume "card U' \ i" with \i \ card U'\ have "Suc i \ card U'" by simp with \(h', U') \ set ps\ have "poly_deg h' < \ ps (Suc i)" by (rule \) with assms(5) show False by (simp add: d) qed ultimately show ?thesis .. qed corollary lem_6_1_2: assumes "standard_decomp k ps" and "exact_decomp 0 ps" and "Suc 0 \ i" and "i \ card X" and "\ ps (Suc i) \ d" and "d < \ ps i" obtains h U where "{(h', U') \ set (ps\<^sub>+). poly_deg h' = d} = {(h, U)}" and "card U = i" proof - from assms obtain h U where "(h, U) \ set (ps\<^sub>+)" and "poly_deg h = d" and "card U = i" by (rule lem_6_1_1) hence "{(h, U)} \ {(h', U') \ set (ps\<^sub>+). poly_deg h' = d}" (is "_ \ ?A") by simp moreover have "?A \ {(h, U)}" proof fix x assume "x \ ?A" then obtain h' U' where "(h', U') \ set (ps\<^sub>+)" and "poly_deg h' = d" and x: "x = (h', U')" by blast note assms(2) \(h, U) \ set (ps\<^sub>+)\ this(1) moreover have "poly_deg h = poly_deg h'" by (simp only: \poly_deg h = d\ \poly_deg h' = d\) ultimately have "(h, U) = (h', U')" by (rule exact_decompD_zero) thus "x \ {(h, U)}" by (simp add: x) qed ultimately have "{(h, U)} = ?A" .. hence "?A = {(h, U)}" by (rule sym) thus ?thesis using \card U = i\ .. qed corollary lem_6_1_2': assumes "standard_decomp k ps" and "exact_decomp 0 ps" and "Suc 0 \ i" and "i \ card X" and "\ ps (Suc i) \ d" and "d < \ ps i" shows "card {(h', U') \ set (ps\<^sub>+). poly_deg h' = d} = 1" (is "card ?A = _") and "{(h', U') \ set (ps\<^sub>+). poly_deg h' = d \ card U' = i} = {(h', U') \ set (ps\<^sub>+). poly_deg h' = d}" (is "?B = _") and "card {(h', U') \ set (ps\<^sub>+). poly_deg h' = d \ card U' = i} = 1" proof - from assms obtain h U where "?A = {(h, U)}" and "card U = i" by (rule lem_6_1_2) from this(1) show "card ?A = 1" by simp moreover show "?B = ?A" proof have "(h, U) \ ?A" by (simp add: \?A = {(h, U)}\) have "?A = {(h, U)}" by fact also from \(h, U) \ ?A\ \card U = i\ have "\ \ ?B" by simp finally show "?A \ ?B" . qed blast ultimately show "card ?B = 1" by simp qed corollary lem_6_1_3: assumes "standard_decomp k ps" and "exact_decomp 0 ps" and "Suc 0 \ i" and "i \ card X" and "(h, U) \ set (ps\<^sub>+)" and "card U = i" shows "\ ps (Suc i) \ poly_deg h" proof (rule ccontr) define j where "j = (LEAST j'. \ ps j' \ poly_deg h)" assume "\ \ ps (Suc i) \ poly_deg h" hence "poly_deg h < \ ps (Suc i)" by simp from assms(2) le_refl have "\ ps (Suc (card X)) = \ ps" by (rule \_card_X) also from _ assms(5) have "\ \ poly_deg h" proof (rule standard_decompD) from assms(1) show "standard_decomp (\ ps) ps" by (rule \) qed finally have "\ ps (Suc (card X)) \ poly_deg h" . hence 1: "\ ps j \ poly_deg h" unfolding j_def by (rule LeastI) have "Suc i < j" proof (rule ccontr) assume "\ Suc i < j" hence "j \ Suc i" by simp hence "\ ps (Suc i) \ \ ps j" by (rule \_decreasing) also have "\ \ poly_deg h" by fact finally show False using \poly_deg h < \ ps (Suc i)\ by simp qed hence eq: "Suc (j - 1) = j" by simp note assms(1, 2) moreover from assms(3) have "Suc 0 \ j - 1" proof (rule le_trans) from \Suc i < j\ show "i \ j - 1" by simp qed moreover have "j - 1 \ card X" proof - have "j \ Suc (card X)" unfolding j_def by (rule Least_le) fact thus ?thesis by simp qed moreover from 1 have "\ ps (Suc (j - 1)) \ poly_deg h" by (simp only: eq) moreover have "poly_deg h < \ ps (j - 1)" proof (rule ccontr) assume "\ poly_deg h < \ ps (j - 1)" hence "\ ps (j - 1) \ poly_deg h" by simp hence "j \ j - 1" unfolding j_def by (rule Least_le) also have "\ < Suc (j - 1)" by simp finally show False by (simp only: eq) qed ultimately obtain h0 U0 where eq1: "{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = poly_deg h} = {(h0, U0)}" and "card U0 = j - 1" by (rule lem_6_1_2) from assms(5) have "(h, U) \ {(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = poly_deg h}" by simp hence "(h, U) \ {(h0, U0)}" by (simp only: eq1) hence "U = U0" by simp hence "card U = j - 1" by (simp only: \card U0 = j - 1\) hence "i = j - 1" by (simp only: assms(6)) hence "Suc i = j" by (simp only: eq) with \Suc i < j\ show False by simp qed qualified fun shift_list :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) \ 'x \ _ list \ _ list" where "shift_list (h, U) x ps = ((punit.monom_mult 1 (Poly_Mapping.single x 1) h, U) # (h, U - {x}) # removeAll (h, U) ps)" declare shift_list.simps[simp del] lemma monomial_decomp_shift_list: assumes "monomial_decomp ps" and "hU \ set ps" shows "monomial_decomp (shift_list hU x ps)" proof - let ?x = "Poly_Mapping.single x (1::nat)" obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with assms(2) have "(h, U) \ set ps" by simp with assms(1) have 1: "is_monomial h" and 2: "lcf h = 1" by (rule monomial_decompD)+ from this(1) have "monomial (lcf h) (lpp h) = h" by (rule punit.monomial_eq_itself) moreover define t where "t = lpp h" ultimately have "h = monomial 1 t" by (simp only: 2) hence "is_monomial (punit.monom_mult 1 ?x h)" and "lcf (punit.monom_mult 1 ?x h) = 1" by (simp_all add: punit.monom_mult_monomial monomial_is_monomial) with assms(1) 1 2 show ?thesis by (simp add: shift_list.simps monomial_decomp_def hU) qed lemma hom_decomp_shift_list: assumes "hom_decomp ps" and "hU \ set ps" shows "hom_decomp (shift_list hU x ps)" proof - let ?x = "Poly_Mapping.single x (1::nat)" obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast with assms(2) have "(h, U) \ set ps" by simp with assms(1) have 1: "homogeneous h" by (rule hom_decompD) hence "homogeneous (punit.monom_mult 1 ?x h)" by (simp only: homogeneous_monom_mult) with assms(1) 1 show ?thesis by (simp add: shift_list.simps hom_decomp_def hU) qed lemma valid_decomp_shift_list: assumes "valid_decomp X ps" and "(h, U) \ set ps" and "x \ U" shows "valid_decomp X (shift_list (h, U) x ps)" proof - let ?x = "Poly_Mapping.single x (1::nat)" from assms(1, 2) have "h \ P[X]" and "h \ 0" and "U \ X" by (rule valid_decompD)+ moreover from this(1) have "punit.monom_mult 1 ?x h \ P[X]" proof (intro Polys_closed_monom_mult PPs_closed_single) from \x \ U\ \U \ X\ show "x \ X" .. qed moreover from \U \ X\ have "U - {x} \ X" by blast ultimately show ?thesis using assms(1) \h \ 0\ by (simp add: valid_decomp_def punit.monom_mult_eq_zero_iff shift_list.simps) qed lemma standard_decomp_shift_list: assumes "standard_decomp k ps" and "(h1, U1) \ set ps" and "(h2, U2) \ set ps" and "poly_deg h1 = poly_deg h2" and "card U2 \ card U1" and "(h1, U1) \ (h2, U2)" and "x \ U2" shows "standard_decomp k (shift_list (h2, U2) x ps)" proof (rule standard_decompI) let ?p1 = "(punit.monom_mult 1 (Poly_Mapping.single x 1) h2, U2)" let ?p2 = "(h2, U2 - {x})" let ?qs = "removeAll (h2, U2) ps" fix h U assume "(h, U) \ set ((shift_list (h2, U2) x ps)\<^sub>+)" hence disj: "(h, U) = ?p1 \ ((h, U) = ?p2 \ U2 - {x} \ {}) \ (h, U) \ set (ps\<^sub>+)" by (auto simp: pos_decomp_def shift_list.simps split: if_split_asm) from assms(7) have "U2 \ {}" by blast with assms(3) have "(h2, U2) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) with assms(1) have k_le: "k \ poly_deg h2" by (rule standard_decompD) let ?x = "Poly_Mapping.single x 1" from disj show "k \ poly_deg h" proof (elim disjE) assume "(h, U) = ?p1" hence h: "h = punit.monom_mult (1::'a) ?x h2" by simp note k_le also have "poly_deg h2 \ poly_deg h" by (cases "h2 = 0") (simp_all add: h poly_deg_monom_mult) finally show ?thesis . next assume "(h, U) = ?p2 \ U2 - {x} \ {}" with k_le show ?thesis by simp next assume "(h, U) \ set (ps\<^sub>+)" with assms(1) show ?thesis by (rule standard_decompD) qed fix d assume "k \ d" and "d \ poly_deg h" from disj obtain h' U' where 1: "(h', U') \ set (?p1 # ps)" and "poly_deg h' = d" and "card U \ card U'" proof (elim disjE) assume "(h, U) = ?p1" hence h: "h = punit.monom_mult 1 ?x h2" and "U = U2" by simp_all from \d \ poly_deg h\ have "d \ poly_deg h2 \ poly_deg h = d" by (cases "h2 = 0") (auto simp: h poly_deg_monom_mult deg_pm_single) thus ?thesis proof assume "d \ poly_deg h2" with assms(1) \(h2, U2) \ set (ps\<^sub>+)\ \k \ d\ obtain h' U' where "(h', U') \ set ps" and "poly_deg h' = d" and "card U2 \ card U'" by (rule standard_decompE) from this(1) have "(h', U') \ set (?p1 # ps)" by simp moreover note \poly_deg h' = d\ moreover from \card U2 \ card U'\ have "card U \ card U'" by (simp only: \U = U2\) ultimately show ?thesis .. next have "(h, U) \ set (?p1 # ps)" by (simp add: \(h, U) = ?p1\) moreover assume "poly_deg h = d" ultimately show ?thesis using le_refl .. qed next assume "(h, U) = ?p2 \ U2 - {x} \ {}" hence "h = h2" and U: "U = U2 - {x}" by simp_all from \d \ poly_deg h\ this(1) have "d \ poly_deg h2" by simp with assms(1) \(h2, U2) \ set (ps\<^sub>+)\ \k \ d\ obtain h' U' where "(h', U') \ set ps" and "poly_deg h' = d" and "card U2 \ card U'" by (rule standard_decompE) from this(1) have "(h', U') \ set (?p1 # ps)" by simp moreover note \poly_deg h' = d\ moreover from _ \card U2 \ card U'\ have "card U \ card U'" unfolding U by (rule le_trans) (metis Diff_empty card_Diff1_le card.infinite finite_Diff_insert order_refl) ultimately show ?thesis .. next assume "(h, U) \ set (ps\<^sub>+)" from assms(1) this \k \ d\ \d \ poly_deg h\ obtain h' U' where "(h', U') \ set ps" and "poly_deg h' = d" and "card U \ card U'" by (rule standard_decompE) from this(1) have "(h', U') \ set (?p1 # ps)" by simp thus ?thesis using \poly_deg h' = d\ \card U \ card U'\ .. qed show "\h' U'. (h', U') \ set (shift_list (h2, U2) x ps) \ poly_deg h' = d \ card U \ card U'" proof (cases "(h', U') = (h2, U2)") case True hence "h' = h2" and "U' = U2" by simp_all from assms(2, 6) have "(h1, U1) \ set (shift_list (h2, U2) x ps)" by (simp add: shift_list.simps) moreover from \poly_deg h' = d\ have "poly_deg h1 = d" by (simp only: \h' = h2\ assms(4)) moreover from \card U \ card U'\ assms(5) have "card U \ card U1" by (simp add: \U' = U2\) ultimately show ?thesis by blast next case False with 1 have "(h', U') \ set (shift_list (h2, U2) x ps)" by (auto simp: shift_list.simps) thus ?thesis using \poly_deg h' = d\ \card U \ card U'\ by blast qed qed lemma cone_decomp_shift_list: assumes "valid_decomp X ps" and "cone_decomp T ps" and "(h, U) \ set ps" and "x \ U" shows "cone_decomp T (shift_list (h, U) x ps)" proof - let ?p1 = "(punit.monom_mult 1 (Poly_Mapping.single x 1) h, U)" let ?p2 = "(h, U - {x})" let ?qs = "removeAll (h, U) ps" from assms(3) obtain ps1 ps2 where ps: "ps = ps1 @ (h, U) # ps2" and *: "(h, U) \ set ps1" by (meson split_list_first) have "count_list ps2 (h, U) = 0" proof (rule ccontr) from assms(1, 3) have "h \ 0" by (rule valid_decompD) assume "count_list ps2 (h, U) \ 0" hence "1 < count_list ps (h, U)" by (simp add: ps count_list_append) also have "\ \ count_list (map cone ps) (cone (h, U))" by (fact count_list_map_ge) finally have "1 < count_list (map cone ps) (cone (h, U))" . with cone_decompD have "cone (h, U) = {0}" proof (rule direct_decomp_repeated_eq_zero) fix s assume "s \ set (map cone ps)" thus "0 \ s" by (auto intro: zero_in_cone) qed (fact assms(2)) with tip_in_cone[of h U] have "h = 0" by simp with \h \ 0\ show False .. qed hence **: "(h, U) \ set ps2" by (simp add: count_list_eq_0_iff) have "perm ps ((h, U) # ps1 @ ps2)" (is "perm _ ?ps") by (rule perm_sym) (simp only: perm_append_Cons ps) with assms(2) have "cone_decomp T ?ps" by (rule cone_decomp_perm) hence "direct_decomp T (map cone ?ps)" by (rule cone_decompD) hence "direct_decomp T (cone (h, U) # map cone (ps1 @ ps2))" by simp hence "direct_decomp T ((map cone (ps1 @ ps2)) @ [cone ?p1, cone ?p2])" proof (rule direct_decomp_direct_decomp) let ?x = "Poly_Mapping.single x (Suc 0)" have "direct_decomp (cone (h, insert x (U - {x}))) [cone (h, U - {x}), cone (monomial (1::'a) ?x * h, insert x (U - {x}))]" by (rule direct_decomp_cone_insert) simp with assms(4) show "direct_decomp (cone (h, U)) [cone ?p1, cone ?p2]" by (simp add: insert_absorb times_monomial_left direct_decomp_perm perm.swap) qed hence "direct_decomp T (map cone (ps1 @ ps2 @ [?p1, ?p2]))" by simp hence "cone_decomp T (ps1 @ ps2 @ [?p1, ?p2])" by (rule cone_decompI) moreover have "perm (ps1 @ ps2 @ [?p1, ?p2]) (?p1 # ?p2 # (ps1 @ ps2))" proof - have "ps1 @ ps2 @ [?p1, ?p2] = (ps1 @ ps2) @ [?p1, ?p2]" by simp also have "perm \ ([?p1, ?p2] @ (ps1 @ ps2))" by (rule perm_append_swap) also have "\ = ?p1 # ?p2 # (ps1 @ ps2)" by simp finally show ?thesis . qed ultimately have "cone_decomp T (?p1 # ?p2 # (ps1 @ ps2))" by (rule cone_decomp_perm) also from * ** have "ps1 @ ps2 = removeAll (h, U) ps" by (simp add: remove1_append ps) finally show ?thesis by (simp only: shift_list.simps) qed subsection \Functions \shift\ and \exact\\ context fixes k m :: nat begin context fixes d :: nat begin definition shift2_inv :: "((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) list \ bool" where "shift2_inv qs \ valid_decomp X qs \ standard_decomp k qs \ exact_decomp (Suc m) qs \ (\d0 set qs. poly_deg (fst q) = d0 \ m < card (snd q)} \ 1)" fun shift1_inv :: "(((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::zero) \ 'x set) set) \ bool" where "shift1_inv (qs, B) \ B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)} \ shift2_inv qs" lemma shift2_invI: "valid_decomp X qs \ standard_decomp k qs \ exact_decomp (Suc m) qs \ (\d0. d0 < d \ card {q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)} \ 1) \ shift2_inv qs" by (simp add: shift2_inv_def) lemma shift2_invD: assumes "shift2_inv qs" shows "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" and "d0 < d \ card {q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)} \ 1" using assms by (simp_all add: shift2_inv_def) lemma shift1_invI: "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)} \ shift2_inv qs \ shift1_inv (qs, B)" by simp lemma shift1_invD: assumes "shift1_inv (qs, B)" shows "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" and "shift2_inv qs" using assms by simp_all declare shift1_inv.simps[simp del] lemma shift1_inv_finite_snd: assumes "shift1_inv (qs, B)" shows "finite B" proof (rule finite_subset) from assms have "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" by (rule shift1_invD) also have "\ \ set qs" by blast finally show "B \ set qs" . qed (fact finite_set) lemma shift1_inv_some_snd: assumes "shift1_inv (qs, B)" and "1 < card B" and "(h, U) = (SOME b. b \ B \ card (snd b) = Suc m)" shows "(h, U) \ B" and "(h, U) \ set qs" and "poly_deg h = d" and "card U = Suc m" proof - define A where "A = {q \ B. card (snd q) = Suc m}" define Y where "Y = {q \ set qs. poly_deg (fst q) = d \ Suc m < card (snd q)}" from assms(1) have B: "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" and inv2: "shift2_inv qs" by (rule shift1_invD)+ have B': "B = A \ Y" by (auto simp: B A_def Y_def) have "finite A" proof (rule finite_subset) show "A \ B" unfolding A_def by blast next from assms(1) show "finite B" by (rule shift1_inv_finite_snd) qed moreover have "finite Y" proof (rule finite_subset) show "Y \ set qs" unfolding Y_def by blast qed (fact finite_set) moreover have "A \ Y = {}" by (auto simp: A_def Y_def) ultimately have "card (A \ Y) = card A + card Y" by (rule card_Un_disjoint) with assms(2) have "1 < card A + card Y" by (simp only: B') thm card_le_Suc0_iff_eq[OF \finite Y\] moreover have "card Y \ 1" unfolding One_nat_def card_le_Suc0_iff_eq[OF \finite Y\] proof (intro ballI) fix q1 q2 :: "(('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set" obtain h1 U1 where q1: "q1 = (h1, U1)" using prod.exhaust by blast obtain h2 U2 where q2: "q2 = (h2, U2)" using prod.exhaust by blast assume "q1 \ Y" hence "(h1, U1) \ set qs" and "poly_deg h1 = d" and "Suc m < card U1" by (simp_all add: q1 Y_def) assume "q2 \ Y" hence "(h2, U2) \ set qs" and "poly_deg h2 = d" and "Suc m < card U2" by (simp_all add: q2 Y_def) from this(2) have "poly_deg h1 = poly_deg h2" by (simp only: \poly_deg h1 = d\) from inv2 have "exact_decomp (Suc m) qs" by (rule shift2_invD) thus "q1 = q2" unfolding q1 q2 by (rule exact_decompD) fact+ qed ultimately have "0 < card A" by simp hence "A \ {}" by auto then obtain a where "a \ A" by blast have "(h, U) \ B \ card (snd (h, U)) = Suc m" unfolding assms(3) proof (rule someI) from \a \ A\ show "a \ B \ card (snd a) = Suc m" by (simp add: A_def) qed thus "(h, U) \ B" and "card U = Suc m" by simp_all from this(1) show "(h, U) \ set qs" and "poly_deg h = d" by (simp_all add: B) qed lemma shift1_inv_preserved: assumes "shift1_inv (qs, B)" and "1 < card B" and "(h, U) = (SOME b. b \ B \ card (snd b) = Suc m)" and "x = (SOME y. y \ U)" shows "shift1_inv (shift_list (h, U) x qs, B - {(h, U)})" proof - let ?p1 = "(punit.monom_mult 1 (Poly_Mapping.single x 1) h, U)" let ?p2 = "(h, U - {x})" let ?qs = "removeAll (h, U) qs" let ?B = "B - {(h, U)}" from assms(1, 2, 3) have "(h, U) \ B" and "(h, U) \ set qs" and deg_h: "poly_deg h = d" and card_U: "card U = Suc m" by (rule shift1_inv_some_snd)+ from card_U have "U \ {}" by auto then obtain y where "y \ U" by blast hence "x \ U" unfolding assms(4) by (rule someI) with card_U have card_Ux: "card (U - {x}) = m" by (metis card_Diff_singleton card.infinite diff_Suc_1 nat.simps(3)) from assms(1) have B: "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" and inv2: "shift2_inv qs" by (rule shift1_invD)+ from inv2 have valid_qs: "valid_decomp X qs" by (rule shift2_invD) hence "h \ 0" using \(h, U) \ set qs\ by (rule valid_decompD) show ?thesis proof (intro shift1_invI shift2_invI) show "?B = {q \ set (shift_list (h, U) x qs). poly_deg (fst q) = d \ m < card (snd q)}" (is "_ = ?C") proof (rule Set.set_eqI) fix b show "b \ ?B \ b \ ?C" proof assume "b \ ?C" hence "b \ insert ?p1 (insert ?p2 (set ?qs))" and b1: "poly_deg (fst b) = d" and b2: "m < card (snd b)" by (simp_all add: shift_list.simps) from this(1) show "b \ ?B" proof (elim insertE) assume "b = ?p1" with \h \ 0\ have "poly_deg (fst b) = Suc d" by (simp add: poly_deg_monom_mult deg_pm_single deg_h) thus ?thesis by (simp add: b1) next assume "b = ?p2" hence "card (snd b) = m" by (simp add: card_Ux) with b2 show ?thesis by simp next assume "b \ set ?qs" with b1 b2 show ?thesis by (auto simp: B) qed qed (auto simp: B shift_list.simps) qed next from valid_qs \(h, U) \ set qs\ \x \ U\ show "valid_decomp X (shift_list (h, U) x qs)" by (rule valid_decomp_shift_list) next from inv2 have std: "standard_decomp k qs" by (rule shift2_invD) have "?B \ {}" proof assume "?B = {}" hence "B \ {(h, U)}" by simp with _ have "card B \ card {(h, U)}" by (rule card_mono) simp with assms(2) show False by simp qed then obtain h' U' where "(h', U') \ B" and "(h', U') \ (h, U)" by auto from this(1) have "(h', U') \ set qs" and "poly_deg h' = d" and "Suc m \ card U'" by (simp_all add: B) note std this(1) \(h, U) \ set qs\ moreover from \poly_deg h' = d\ have "poly_deg h' = poly_deg h" by (simp only: deg_h) moreover from \Suc m \ card U'\ have "card U \ card U'" by (simp only: card_U) ultimately show "standard_decomp k (shift_list (h, U) x qs)" by (rule standard_decomp_shift_list) fact+ next from inv2 have exct: "exact_decomp (Suc m) qs" by (rule shift2_invD) show "exact_decomp (Suc m) (shift_list (h, U) x qs)" proof (rule exact_decompI) fix h' U' assume "(h', U') \ set (shift_list (h, U) x qs)" hence *: "(h', U') \ insert ?p1 (insert ?p2 (set ?qs))" by (simp add: shift_list.simps) thus "h' \ P[X]" proof (elim insertE) assume "(h', U') = ?p1" hence h': "h' = punit.monom_mult 1 (Poly_Mapping.single x 1) h" by simp from exct \(h, U) \ set qs\ have "U \ X" by (rule exact_decompD) with \x \ U\ have "x \ X" .. hence "Poly_Mapping.single x 1 \ .[X]" by (rule PPs_closed_single) moreover from exct \(h, U) \ set qs\ have "h \ P[X]" by (rule exact_decompD) ultimately show ?thesis unfolding h' by (rule Polys_closed_monom_mult) next assume "(h', U') = ?p2" hence "h' = h" by simp also from exct \(h, U) \ set qs\ have "\ \ P[X]" by (rule exact_decompD) finally show ?thesis . next assume "(h', U') \ set ?qs" hence "(h', U') \ set qs" by simp with exct show ?thesis by (rule exact_decompD) qed from * show "U' \ X" proof (elim insertE) assume "(h', U') = ?p1" hence "U' = U" by simp also from exct \(h, U) \ set qs\ have "\ \ X" by (rule exact_decompD) finally show ?thesis . next assume "(h', U') = ?p2" hence "U' = U - {x}" by simp also have "\ \ U" by blast also from exct \(h, U) \ set qs\ have "\ \ X" by (rule exact_decompD) finally show ?thesis . next assume "(h', U') \ set ?qs" hence "(h', U') \ set qs" by simp with exct show ?thesis by (rule exact_decompD) qed next fix h1 h2 U1 U2 assume "(h1, U1) \ set (shift_list (h, U) x qs)" and "Suc m < card U1" hence "(h1, U1) \ set qs" using card_U card_Ux by (auto simp: shift_list.simps) assume "(h2, U2) \ set (shift_list (h, U) x qs)" and "Suc m < card U2" hence "(h2, U2) \ set qs" using card_U card_Ux by (auto simp: shift_list.simps) assume "poly_deg h1 = poly_deg h2" from exct show "(h1, U1) = (h2, U2)" by (rule exact_decompD) fact+ qed next fix d0 assume "d0 < d" have "finite {q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)}" (is "finite ?A") by auto moreover have "{q \ set (shift_list (h, U) x qs). poly_deg (fst q) = d0 \ m < card (snd q)} \ ?A" (is "?C \ _") proof fix q assume "q \ ?C" hence "q = ?p1 \ q = ?p2 \ q \ set ?qs" and 1: "poly_deg (fst q) = d0" and 2: "m < card (snd q)" by (simp_all add: shift_list.simps) from this(1) show "q \ ?A" proof (elim disjE) assume "q = ?p1" with \h \ 0\ have "d \ poly_deg (fst q)" by (simp add: poly_deg_monom_mult deg_h) with \d0 < d\ show ?thesis by (simp only: 1) next assume "q = ?p2" hence "d \ poly_deg (fst q)" by (simp add: deg_h) with \d0 < d\ show ?thesis by (simp only: 1) next assume "q \ set ?qs" with 1 2 show ?thesis by simp qed qed ultimately have "card ?C \ card ?A" by (rule card_mono) also from inv2 \d0 < d\ have "\ \ 1" by (rule shift2_invD) finally show "card ?C \ 1" . qed qed function (domintros) shift1 :: "(((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) set) \ (((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) set)" where "shift1 (qs, B) = (if 1 < card B then let (h, U) = SOME b. b \ B \ card (snd b) = Suc m; x = SOME y. y \ U in shift1 (shift_list (h, U) x qs, B - {(h, U)}) else (qs, B))" by auto lemma shift1_domI: assumes "shift1_inv args" shows "shift1_dom args" proof - from wf_measure[of "card \ snd"] show ?thesis using assms proof (induct) case (less args) obtain qs B where args: "args = (qs, B)" using prod.exhaust by blast have IH: "shift1_dom (qs0, B0)" if "card B0 < card B" and "shift1_inv (qs0, B0)" for qs0 and B0::"((_ \\<^sub>0 'a) \ _) set" using _ that(2) proof (rule less) from that(1) show "((qs0, B0), args) \ measure (card \ snd)" by (simp add: args) qed from less(2) have inv: "shift1_inv (qs, B)" by (simp only: args) show ?case unfolding args proof (rule shift1.domintros) fix h U assume hU: "(h, U) = (SOME b. b \ B \ card (snd b) = Suc m)" define x where "x = (SOME y. y \ U)" assume "Suc 0 < card B" hence "1 < card B" by simp have "shift1_dom (shift_list (h, U) x qs, B - {(h, U)})" proof (rule IH) from inv have "finite B" by (rule shift1_inv_finite_snd) moreover from inv \1 < card B\ hU have "(h, U) \ B" by (rule shift1_inv_some_snd) ultimately show "card (B - {(h, U)}) < card B" by (rule card_Diff1_less) next from inv \1 < card B\ hU x_def show "shift1_inv (shift_list (h, U) x qs, (B - {(h, U)}))" by (rule shift1_inv_preserved) qed thus "shift1_dom (shift_list (SOME b. b \ B \ card (snd b) = Suc m) (SOME y. y \ U) qs, B - {SOME b. b \ B \ card (snd b) = Suc m})" by (simp add: hU x_def) qed qed qed lemma shift1_induct [consumes 1, case_names base step]: assumes "shift1_inv args" assumes "\qs B. shift1_inv (qs, B) \ card B \ 1 \ P (qs, B) (qs, B)" assumes "\qs B h U x. shift1_inv (qs, B) \ 1 < card B \ (h, U) = (SOME b. b \ B \ card (snd b) = Suc m) \ x = (SOME y. y \ U) \ finite U \ x \ U \ card (U - {x}) = m \ P (shift_list (h, U) x qs, B - {(h, U)}) (shift1 (shift_list (h, U) x qs, B - {(h, U)})) \ P (qs, B) (shift1 (shift_list (h, U) x qs, B - {(h, U)}))" shows "P args (shift1 args)" proof - from assms(1) have "shift1_dom args" by (rule shift1_domI) thus ?thesis using assms(1) proof (induct args rule: shift1.pinduct) case step: (1 qs B) obtain h U where hU: "(h, U) = (SOME b. b \ B \ card (snd b) = Suc m)" by (smt prod.exhaust) define x where "x = (SOME y. y \ U)" show ?case proof (simp add: shift1.psimps[OF step.hyps(1)] flip: hU x_def del: One_nat_def, intro conjI impI) let ?args = "(shift_list (h, U) x qs, B - {(h, U)})" assume "1 < card B" with step.prems have card_U: "card U = Suc m" using hU by (rule shift1_inv_some_snd) from card_U have "finite U" using card.infinite by fastforce from card_U have "U \ {}" by auto then obtain y where "y \ U" by blast hence "x \ U" unfolding x_def by (rule someI) with step.prems \1 < card B\ hU x_def \finite U\ show "P (qs, B) (shift1 ?args)" proof (rule assms(3)) from \finite U\ \x \ U\ show "card (U - {x}) = m" by (simp add: card_U) next from \1 < card B\ refl hU x_def show "P ?args (shift1 ?args)" proof (rule step.hyps) from step.prems \1 < card B\ hU x_def show "shift1_inv ?args" by (rule shift1_inv_preserved) qed qed next assume "\ 1 < card B" hence "card B \ 1" by simp with step.prems show "P (qs, B) (qs, B)" by (rule assms(2)) qed qed qed lemma shift1_1: assumes "shift1_inv args" and "d0 \ d" shows "card {q \ set (fst (shift1 args)). poly_deg (fst q) = d0 \ m < card (snd q)} \ 1" using assms(1) proof (induct args rule: shift1_induct) case (base qs B) from assms(2) have "d0 < d \ d0 = d" by auto thus ?case proof from base(1) have "shift2_inv qs" by (rule shift1_invD) moreover assume "d0 < d" ultimately show ?thesis unfolding fst_conv by (rule shift2_invD) next assume "d0 = d" from base(1) have "B = {q \ set (fst (qs, B)). poly_deg (fst q) = d0 \ m < card (snd q)}" unfolding fst_conv \d0 = d\ by (rule shift1_invD) with base(2) show ?thesis by simp qed qed lemma shift1_2: "shift1_inv args \ card {q \ set (fst (shift1 args)). m < card (snd q)} \ card {q \ set (fst args). m < card (snd q)}" proof (induct args rule: shift1_induct) case (base qs B) show ?case .. next case (step qs B h U x) let ?x = "Poly_Mapping.single x (1::nat)" let ?p1 = "(punit.monom_mult 1 ?x h, U)" let ?A = "{q \ set qs. m < card (snd q)}" from step(1-3) have card_U: "card U = Suc m" and "(h, U) \ set qs" by (rule shift1_inv_some_snd)+ from step(1) have "shift2_inv qs" by (rule shift1_invD) hence "valid_decomp X qs" by (rule shift2_invD) hence "h \ 0" using \(h, U) \ set qs\ by (rule valid_decompD) have fin1: "finite ?A" by auto hence fin2: "finite (insert ?p1 ?A)" by simp from \(h, U) \ set qs\ have hU_in: "(h, U) \ insert ?p1 ?A" by (simp add: card_U) have "?p1 \ (h, U)" proof assume "?p1 = (h, U)" hence "lpp (punit.monom_mult 1 ?x h) = lpp h" by simp with \h \ 0\ show False by (simp add: punit.lt_monom_mult monomial_0_iff) qed let ?qs = "shift_list (h, U) x qs" have "{q \ set (fst (?qs, B - {(h, U)})). m < card (snd q)} = (insert ?p1 ?A) - {(h, U)}" using step(7) card_U \?p1 \ (h, U)\ by (fastforce simp: shift_list.simps) also from fin2 hU_in have "card \ = card (insert ?p1 ?A) - 1" by (simp add: card_Diff_singleton_if) also from fin1 have "\ \ Suc (card ?A) - 1" by (simp add: card_insert_if) also have "\ = card {q \ set (fst (qs, B)). m < card (snd q)}" by simp finally have "card {q \ set (fst (?qs, B - {(h, U)})). m < card (snd q)} \ card {q \ set (fst (qs, B)). m < card (snd q)}" . with step(8) show ?case by (rule le_trans) qed lemma shift1_3: "shift1_inv args \ cone_decomp T (fst args) \ cone_decomp T (fst (shift1 args))" proof (induct args rule: shift1_induct) case (base qs B) from base(3) show ?case . next case (step qs B h U x) from step.hyps(1) have "shift2_inv qs" by (rule shift1_invD) hence "valid_decomp X qs" by (rule shift2_invD) moreover from step.prems have "cone_decomp T qs" by (simp only: fst_conv) moreover from step.hyps(1-3) have "(h, U) \ set qs" by (rule shift1_inv_some_snd) ultimately have "cone_decomp T (fst (shift_list (h, U) x qs, B - {(h, U)}))" unfolding fst_conv using step.hyps(6) by (rule cone_decomp_shift_list) thus ?case by (rule step.hyps(8)) qed lemma shift1_4: "shift1_inv args \ Max (poly_deg ` fst ` set (fst args)) \ Max (poly_deg ` fst ` set (fst (shift1 args)))" proof (induct args rule: shift1_induct) case (base qs B) show ?case .. next case (step qs B h U x) let ?x = "Poly_Mapping.single x 1" let ?p1 = "(punit.monom_mult 1 ?x h, U)" let ?qs = "shift_list (h, U) x qs" from step(1) have "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" and inv2: "shift2_inv qs" by (rule shift1_invD)+ from this(1) have "B \ set qs" by auto with step(2) have "set qs \ {}" by auto from finite_set have fin: "finite (poly_deg ` fst ` set ?qs)" by (intro finite_imageI) have "Max (poly_deg ` fst ` set (fst (qs, B))) \ Max (poly_deg ` fst ` set (fst (?qs, B - {(h, U)})))" unfolding fst_conv proof (rule Max.boundedI) from finite_set show "finite (poly_deg ` fst ` set qs)" by (intro finite_imageI) next from \set qs \ {}\ show "poly_deg ` fst ` set qs \ {}" by simp next fix a assume "a \ poly_deg ` fst ` set qs" then obtain q where "q \ set qs" and a: "a = poly_deg (fst q)" by blast show "a \ Max (poly_deg ` fst ` set ?qs)" proof (cases "q = (h, U)") case True hence "a \ poly_deg (fst ?p1)" by (cases "h = 0") (simp_all add: a poly_deg_monom_mult) also from fin have "\ \ Max (poly_deg ` fst ` set ?qs)" proof (rule Max_ge) have "?p1 \ set ?qs" by (simp add: shift_list.simps) thus "poly_deg (fst ?p1) \ poly_deg ` fst ` set ?qs" by (intro imageI) qed finally show ?thesis . next case False with \q \ set qs\ have "q \ set ?qs" by (simp add: shift_list.simps) hence "a \ poly_deg ` fst ` set ?qs" unfolding a by (intro imageI) with fin show ?thesis by (rule Max_ge) qed qed thus ?case using step(8) by (rule le_trans) qed lemma shift1_5: "shift1_inv args \ fst (shift1 args) = [] \ fst args = []" proof (induct args rule: shift1_induct) case (base qs B) show ?case .. next case (step qs B h U x) let ?p1 = "(punit.monom_mult 1 (Poly_Mapping.single x 1) h, U)" let ?qs = "shift_list (h, U) x qs" from step(1) have "B = {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}" and inv2: "shift2_inv qs" by (rule shift1_invD)+ from this(1) have "B \ set qs" by auto with step(2) have "qs \ []" by auto moreover have "fst (shift1 (?qs, B - {(h, U)})) \ []" by (simp add: step.hyps(8) del: One_nat_def) (simp add: shift_list.simps) ultimately show ?case by simp qed lemma shift1_6: "shift1_inv args \ monomial_decomp (fst args) \ monomial_decomp (fst (shift1 args))" proof (induct args rule: shift1_induct) case (base qs B) from base(3) show ?case . next case (step qs B h U x) from step(1-3) have "(h, U) \ set qs" by (rule shift1_inv_some_snd) with step.prems have "monomial_decomp (fst (shift_list (h, U) x qs, B - {(h, U)}))" unfolding fst_conv by (rule monomial_decomp_shift_list) thus ?case by (rule step.hyps) qed lemma shift1_7: "shift1_inv args \ hom_decomp (fst args) \ hom_decomp (fst (shift1 args))" proof (induct args rule: shift1_induct) case (base qs B) from base(3) show ?case . next case (step qs B h U x) from step(1-3) have "(h, U) \ set qs" by (rule shift1_inv_some_snd) with step.prems have "hom_decomp (fst (shift_list (h, U) x qs, B - {(h, U)}))" unfolding fst_conv by (rule hom_decomp_shift_list) thus ?case by (rule step.hyps) qed end lemma shift2_inv_preserved: assumes "shift2_inv d qs" shows "shift2_inv (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))" proof - define args where "args = (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" from refl assms have inv1: "shift1_inv d args" unfolding args_def by (rule shift1_invI) hence "shift1_inv d (shift1 args)" by (induct args rule: shift1_induct) hence "shift1_inv d (fst (shift1 args), snd (shift1 args))" by simp hence "shift2_inv d (fst (shift1 args))" by (rule shift1_invD) hence "valid_decomp X (fst (shift1 args))" and "standard_decomp k (fst (shift1 args))" and "exact_decomp (Suc m) (fst (shift1 args))" by (rule shift2_invD)+ thus "shift2_inv (Suc d) (fst (shift1 args))" proof (rule shift2_invI) fix d0 assume "d0 < Suc d" hence "d0 \ d" by simp with inv1 show "card {q \ set (fst (shift1 args)). poly_deg (fst q) = d0 \ m < card (snd q)} \ 1" by (rule shift1_1) qed qed function shift2 :: "nat \ nat \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) list" where "shift2 c d qs = (if c \ d then qs else shift2 c (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}))))" by auto termination proof show "wf (measure (\(c, d, _). c - d))" by (fact wf_measure) qed simp lemma shift2_1: "shift2_inv d qs \ shift2_inv c (shift2 c d qs)" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) show ?case proof (subst shift2.simps, simp del: shift2.simps, intro conjI impI) assume "c \ d" show "shift2_inv c qs" proof (rule shift2_invI) from IH(2) show "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" by (rule shift2_invD)+ next fix d0 assume "d0 < c" hence "d0 < d" using \c \ d\ by (rule less_le_trans) with IH(2) show "card {q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)} \ 1" by (rule shift2_invD) qed next assume "\ c \ d" thus "shift2_inv c (shift2 c (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}))))" proof (rule IH) from IH(2) show "shift2_inv (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))" by (rule shift2_inv_preserved) qed qed qed lemma shift2_2: "shift2_inv d qs \ card {q \ set (shift2 c d qs). m < card (snd q)} \ card {q \ set qs. m < card (snd q)}" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) let ?A = "{q \ set (shift2 c (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))). m < card (snd q)}" show ?case proof (subst shift2.simps, simp del: shift2.simps, intro impI) assume "\ c \ d" hence "card ?A \ card {q \ set (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}))). m < card (snd q)}" proof (rule IH) show "shift2_inv (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))" using IH(2) by (rule shift2_inv_preserved) qed also have "\ \ card {q \ set (fst (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})). m < card (snd q)}" using refl IH(2) by (intro shift1_2 shift1_invI) finally show "card ?A \ card {q \ set qs. m < card (snd q)}" by (simp only: fst_conv) qed qed lemma shift2_3: "shift2_inv d qs \ cone_decomp T qs \ cone_decomp T (shift2 c d qs)" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) have inv2: "shift2_inv (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))" using IH(2) by (rule shift2_inv_preserved) show ?case proof (subst shift2.simps, simp add: IH.prems del: shift2.simps, intro impI) assume "\ c \ d" moreover note inv2 moreover have "cone_decomp T (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})))" proof (rule shift1_3) from refl IH(2) show "shift1_inv d (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" by (rule shift1_invI) qed (simp add: IH.prems) ultimately show "cone_decomp T (shift2 c (Suc d) (fst (shift1 (qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)}))))" by (rule IH) qed qed lemma shift2_4: "shift2_inv d qs \ Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (shift2 c d qs))" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) let ?args = "(qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" show ?case proof (subst shift2.simps, simp del: shift2.simps, intro impI) assume "\ c \ d" have "Max (poly_deg ` fst ` set (fst ?args)) \ Max (poly_deg ` fst ` set (fst (shift1 ?args)))" using refl IH(2) by (intro shift1_4 shift1_invI) also from \\ c \ d\ have "\ \ Max (poly_deg ` fst ` set (shift2 c (Suc d) (fst (shift1 ?args))))" proof (rule IH) from IH(2) show "shift2_inv (Suc d) (fst (shift1 ?args))" by (rule shift2_inv_preserved) qed finally show "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (shift2 c (Suc d) (fst (shift1 ?args))))" by (simp only: fst_conv) qed qed lemma shift2_5: "shift2_inv d qs \ shift2 c d qs = [] \ qs = []" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) let ?args = "(qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" show ?case proof (subst shift2.simps, simp del: shift2.simps, intro impI) assume "\ c \ d" hence "shift2 c (Suc d) (fst (shift1 ?args)) = [] \ fst (shift1 ?args) = []" proof (rule IH) from IH(2) show "shift2_inv (Suc d) (fst (shift1 ?args))" by (rule shift2_inv_preserved) qed also from refl IH(2) have "\ \ fst ?args = []" by (intro shift1_5 shift1_invI) finally show "shift2 c (Suc d) (fst (shift1 ?args)) = [] \ qs = []" by (simp only: fst_conv) qed qed lemma shift2_6: "shift2_inv d qs \ monomial_decomp qs \ monomial_decomp (shift2 c d qs)" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) let ?args = "(qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" show ?case proof (subst shift2.simps, simp del: shift2.simps, intro conjI impI IH) from IH(2) show "shift2_inv (Suc d) (fst (shift1 ?args))" by (rule shift2_inv_preserved) next from refl IH(2) have "shift1_inv d ?args" by (rule shift1_invI) moreover from IH(3) have "monomial_decomp (fst ?args)" by simp ultimately show "monomial_decomp (fst (shift1 ?args))" by (rule shift1_6) qed qed lemma shift2_7: "shift2_inv d qs \ hom_decomp qs \ hom_decomp (shift2 c d qs)" proof (induct c d qs rule: shift2.induct) case IH: (1 c d qs) let ?args = "(qs, {q \ set qs. poly_deg (fst q) = d \ m < card (snd q)})" show ?case proof (subst shift2.simps, simp del: shift2.simps, intro conjI impI IH) from IH(2) show "shift2_inv (Suc d) (fst (shift1 ?args))" by (rule shift2_inv_preserved) next from refl IH(2) have "shift1_inv d ?args" by (rule shift1_invI) moreover from IH(3) have "hom_decomp (fst ?args)" by simp ultimately show "hom_decomp (fst (shift1 ?args))" by (rule shift1_7) qed qed definition shift :: "((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) list" where "shift qs = shift2 (k + card {q \ set qs. m < card (snd q)}) k qs" lemma shift2_inv_init: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" shows "shift2_inv k qs" using assms proof (rule shift2_invI) fix d0 assume "d0 < k" have "{q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)} = {}" proof - { fix q assume "q \ set qs" obtain h U where q: "q = (h, U)" using prod.exhaust by blast assume "poly_deg (fst q) = d0" and "m < card (snd q)" hence "poly_deg h < k" and "m < card U" using \d0 < k\ by (simp_all add: q) from this(2) have "U \ {}" by auto with \q \ set qs\ have "(h, U) \ set (qs\<^sub>+)" by (simp add: q pos_decomp_def) with assms(2) have "k \ poly_deg h" by (rule standard_decompD) with \poly_deg h < k\ have False by simp } thus ?thesis by blast qed thus "card {q \ set qs. poly_deg (fst q) = d0 \ m < card (snd q)} \ 1" by (simp only: card.empty) qed lemma shift: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" shows "valid_decomp X (shift qs)" and "standard_decomp k (shift qs)" and "exact_decomp m (shift qs)" proof - define c where "c = card {q \ set qs. m < card (snd q)}" define A where "A = {q \ set (shift qs). m < card (snd q)}" from assms have "shift2_inv k qs" by (rule shift2_inv_init) hence inv2: "shift2_inv (k + c) (shift qs)" and "card A \ c" unfolding shift_def c_def A_def by (rule shift2_1, rule shift2_2) from inv2 have fin: "valid_decomp X (shift qs)" and std: "standard_decomp k (shift qs)" and exct: "exact_decomp (Suc m) (shift qs)" by (rule shift2_invD)+ show "valid_decomp X (shift qs)" and "standard_decomp k (shift qs)" by fact+ have "finite A" by (auto simp: A_def) show "exact_decomp m (shift qs)" proof (rule exact_decompI) fix h U assume "(h, U) \ set (shift qs)" with exct show "h \ P[X]" and "U \ X" by (rule exact_decompD)+ next fix h1 h2 U1 U2 assume 1: "(h1, U1) \ set (shift qs)" and 2: "(h2, U2) \ set (shift qs)" assume 3: "poly_deg h1 = poly_deg h2" and 4: "m < card U1" and 5: "m < card U2" from 5 have "U2 \ {}" by auto with 2 have "(h2, U2) \ set ((shift qs)\<^sub>+)" by (simp add: pos_decomp_def) let ?C = "{q \ set (shift qs). poly_deg (fst q) = poly_deg h2 \ m < card (snd q)}" define B where "B = {q \ A. k \ poly_deg (fst q) \ poly_deg (fst q) \ poly_deg h2}" have "Suc (poly_deg h2) - k \ card B" proof - have "B = (\d0\{k..poly_deg h2}. {q \ A. poly_deg (fst q) = d0})" by (auto simp: B_def) also have "card \ = (\d0=k..poly_deg h2. card {q \ A. poly_deg (fst q) = d0})" proof (intro card_UN_disjoint ballI impI) fix d0 from _ \finite A\ show "finite {q \ A. poly_deg (fst q) = d0}" by (rule finite_subset) blast next fix d0 d1 :: nat assume "d0 \ d1" thus "{q \ A. poly_deg (fst q) = d0} \ {q \ A. poly_deg (fst q) = d1} = {}" by blast qed (fact finite_atLeastAtMost) also have "\ \ (\d0=k..poly_deg h2. 1)" proof (rule sum_mono) fix d0 assume "d0 \ {k..poly_deg h2}" hence "k \ d0" and "d0 \ poly_deg h2" by simp_all with std \(h2, U2) \ set ((shift qs)\<^sub>+)\ obtain h' U' where "(h', U') \ set (shift qs)" and "poly_deg h' = d0" and "card U2 \ card U'" by (rule standard_decompE) from 5 this(3) have "m < card U'" by (rule less_le_trans) with \(h', U') \ set (shift qs)\ have "(h', U') \ {q \ A. poly_deg (fst q) = d0}" by (simp add: A_def \poly_deg h' = d0\) hence "{q \ A. poly_deg (fst q) = d0} \ {}" by blast moreover from _ \finite A\ have "finite {q \ A. poly_deg (fst q) = d0}" by (rule finite_subset) blast ultimately show "1 \ card {q \ A. poly_deg (fst q) = d0}" by (simp add: card_gt_0_iff Suc_le_eq) qed also have "(\d0=k..poly_deg h2. 1) = Suc (poly_deg h2) - k" by auto finally show ?thesis . qed also from \finite A\ _ have "\ \ card A" by (rule card_mono) (auto simp: B_def) also have "\ \ c" by fact finally have "poly_deg h2 < k + c" by simp with inv2 have "card ?C \ 1" by (rule shift2_invD) have "finite ?C" by auto moreover note \card ?C \ 1\ moreover from 1 3 4 have "(h1, U1) \ ?C" by simp moreover from 2 5 have "(h2, U2) \ ?C" by simp ultimately show "(h1, U1) = (h2, U2)" by (auto simp: card_le_Suc0_iff_eq) qed qed lemma monomial_decomp_shift: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" and "monomial_decomp qs" shows "monomial_decomp (shift qs)" proof - from assms(1, 2, 3) have "shift2_inv k qs" by (rule shift2_inv_init) thus ?thesis unfolding shift_def using assms(4) by (rule shift2_6) qed lemma hom_decomp_shift: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" and "hom_decomp qs" shows "hom_decomp (shift qs)" proof - from assms(1, 2, 3) have "shift2_inv k qs" by (rule shift2_inv_init) thus ?thesis unfolding shift_def using assms(4) by (rule shift2_7) qed lemma cone_decomp_shift: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" and "cone_decomp T qs" shows "cone_decomp T (shift qs)" proof - from assms(1, 2, 3) have "shift2_inv k qs" by (rule shift2_inv_init) thus ?thesis unfolding shift_def using assms(4) by (rule shift2_3) qed lemma Max_shift_ge: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" shows "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (shift qs))" proof - from assms(1-3) have "shift2_inv k qs" by (rule shift2_inv_init) thus ?thesis unfolding shift_def by (rule shift2_4) qed lemma shift_Nil_iff: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp (Suc m) qs" shows "shift qs = [] \ qs = []" proof - from assms(1-3) have "shift2_inv k qs" by (rule shift2_inv_init) thus ?thesis unfolding shift_def by (rule shift2_5) qed end primrec exact_aux :: "nat \ nat \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) list" where "exact_aux k 0 qs = qs" | "exact_aux k (Suc m) qs = exact_aux k m (shift k m qs)" lemma exact_aux: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" shows "valid_decomp X (exact_aux k m qs)" (is ?thesis1) and "standard_decomp k (exact_aux k m qs)" (is ?thesis2) and "exact_decomp 0 (exact_aux k m qs)" (is ?thesis3) proof - from assms have "?thesis1 \ ?thesis2 \ ?thesis3" proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" have "valid_decomp X (exact_aux k m ?qs) \ standard_decomp k (exact_aux k m ?qs) \ exact_decomp 0 (exact_aux k m ?qs)" proof (rule Suc) from Suc.prems show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" by (rule shift)+ qed thus ?case by simp qed thus ?thesis1 and ?thesis2 and ?thesis3 by simp_all qed lemma monomial_decomp_exact_aux: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" and "monomial_decomp qs" shows "monomial_decomp (exact_aux k m qs)" using assms proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" have "monomial_decomp (exact_aux k m ?qs)" proof (rule Suc) show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" using Suc.prems(1, 2, 3) by (rule shift)+ next from Suc.prems show "monomial_decomp ?qs" by (rule monomial_decomp_shift) qed thus ?case by simp qed lemma hom_decomp_exact_aux: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" and "hom_decomp qs" shows "hom_decomp (exact_aux k m qs)" using assms proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" have "hom_decomp (exact_aux k m ?qs)" proof (rule Suc) show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" using Suc.prems(1, 2, 3) by (rule shift)+ next from Suc.prems show "hom_decomp ?qs" by (rule hom_decomp_shift) qed thus ?case by simp qed lemma cone_decomp_exact_aux: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" and "cone_decomp T qs" shows "cone_decomp T (exact_aux k m qs)" using assms proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" have "cone_decomp T (exact_aux k m ?qs)" proof (rule Suc) show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" using Suc.prems(1, 2, 3) by (rule shift)+ next from Suc.prems show "cone_decomp T ?qs" by (rule cone_decomp_shift) qed thus ?case by simp qed lemma Max_exact_aux_ge: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" shows "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (exact_aux k m qs))" using assms proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" from Suc.prems have "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set ?qs)" by (rule Max_shift_ge) also have "\ \ Max (poly_deg ` fst ` set (exact_aux k m ?qs))" proof (rule Suc) from Suc.prems show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" by (rule shift)+ qed finally show ?case by simp qed lemma exact_aux_Nil_iff: assumes "valid_decomp X qs" and "standard_decomp k qs" and "exact_decomp m qs" shows "exact_aux k m qs = [] \ qs = []" using assms proof (induct m arbitrary: qs) case 0 thus ?case by simp next case (Suc m) let ?qs = "shift k m qs" have "exact_aux k m ?qs = [] \ ?qs = []" proof (rule Suc) from Suc.prems show "valid_decomp X ?qs" and "standard_decomp k ?qs" and "exact_decomp m ?qs" by (rule shift)+ qed also from Suc.prems have "\ \ qs = []" by (rule shift_Nil_iff) finally show ?case by simp qed definition exact :: "nat \ ((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) list \ ((('x \\<^sub>0 nat) \\<^sub>0 'a::{comm_ring_1,ring_no_zero_divisors}) \ 'x set) list" where "exact k qs = exact_aux k (card X) qs" lemma exact: assumes "valid_decomp X qs" and "standard_decomp k qs" shows "valid_decomp X (exact k qs)" (is ?thesis1) and "standard_decomp k (exact k qs)" (is ?thesis2) and "exact_decomp 0 (exact k qs)" (is ?thesis3) proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms show ?thesis1 and ?thesis2 and ?thesis3 unfolding exact_def by (rule exact_aux)+ qed lemma monomial_decomp_exact: assumes "valid_decomp X qs" and "standard_decomp k qs" and "monomial_decomp qs" shows "monomial_decomp (exact k qs)" proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms(1, 2) show ?thesis unfolding exact_def using assms(3) by (rule monomial_decomp_exact_aux) qed lemma hom_decomp_exact: assumes "valid_decomp X qs" and "standard_decomp k qs" and "hom_decomp qs" shows "hom_decomp (exact k qs)" proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms(1, 2) show ?thesis unfolding exact_def using assms(3) by (rule hom_decomp_exact_aux) qed lemma cone_decomp_exact: assumes "valid_decomp X qs" and "standard_decomp k qs" and "cone_decomp T qs" shows "cone_decomp T (exact k qs)" proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms(1, 2) show ?thesis unfolding exact_def using assms(3) by (rule cone_decomp_exact_aux) qed lemma Max_exact_ge: assumes "valid_decomp X qs" and "standard_decomp k qs" shows "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (exact k qs))" proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms(1, 2) show ?thesis unfolding exact_def by (rule Max_exact_aux_ge) qed lemma exact_Nil_iff: assumes "valid_decomp X qs" and "standard_decomp k qs" shows "exact k qs = [] \ qs = []" proof - from assms(1) le_refl have "exact_decomp (card X) qs" by (rule exact_decomp_card_X) with assms(1, 2) show ?thesis unfolding exact_def by (rule exact_aux_Nil_iff) qed corollary \_zero_exact: assumes "valid_decomp X qs" and "standard_decomp k qs" and "qs \ []" shows "Suc (Max (poly_deg ` fst ` set qs)) \ \ (exact k qs) 0" proof - from assms(1, 2) have "Max (poly_deg ` fst ` set qs) \ Max (poly_deg ` fst ` set (exact k qs))" by (rule Max_exact_ge) also have "Suc \ \ \ (exact k qs) 0" proof (rule \_zero) from assms show "exact k qs \ []" by (simp add: exact_Nil_iff) qed finally show ?thesis by simp qed lemma normal_form_exact_decompE: assumes "F \ P[X]" obtains qs where "valid_decomp X qs" and "standard_decomp 0 qs" and "monomial_decomp qs" and "cone_decomp (normal_form F ` P[X]) qs" and "exact_decomp 0 qs" and "\g. (\f. f \ F \ homogeneous f) \ g \ punit.reduced_GB F \ poly_deg g \ \ qs 0" proof - let ?G = "punit.reduced_GB F" let ?S = "lpp ` ?G" let ?N = "normal_form F ` P[X]" define qs::"((_ \\<^sub>0 'a) \ _) list" where "qs = snd (split 0 X ?S)" from fin_X assms have std: "standard_decomp 0 qs" and cn: "cone_decomp ?N qs" unfolding qs_def by (rule standard_cone_decomp_snd_split)+ from fin_X assms have "finite ?G" by (rule finite_reduced_GB_Polys) hence "finite ?S" by (rule finite_imageI) with fin_X subset_refl have valid: "valid_decomp X qs" unfolding qs_def using zero_in_PPs by (rule valid_decomp_split) from fin_X subset_refl \finite ?S\ have md: "monomial_decomp qs" unfolding qs_def by (rule monomial_decomp_split) let ?qs = "exact 0 qs" from valid std have "valid_decomp X ?qs" and "standard_decomp 0 ?qs" by (rule exact)+ moreover from valid std md have "monomial_decomp ?qs" by (rule monomial_decomp_exact) moreover from valid std cn have "cone_decomp ?N ?qs" by (rule cone_decomp_exact) moreover from valid std have "exact_decomp 0 ?qs" by (rule exact) moreover have "poly_deg g \ \ ?qs 0" if "\f. f \ F \ homogeneous f" and "g \ ?G" for g proof (cases "qs = []") case True from one_in_Polys have "normal_form F 1 \ ?N" by (rule imageI) also from True cn have "\ = {0}" by (simp add: cone_decomp_def direct_decomp_def bij_betw_def) finally have "?G = {1}" using fin_X assms by (simp add: normal_form_zero_iff ideal_eq_UNIV_iff_reduced_GB_eq_one_Polys flip: ideal_eq_UNIV_iff_contains_one) with that(2) show ?thesis by simp next case False from fin_X assms that have "poly_deg g \ Suc (Max (poly_deg ` fst ` set qs))" unfolding qs_def by (rule standard_cone_decomp_snd_split) also from valid std False have "\ \ \ ?qs 0" by (rule \_zero_exact) finally show ?thesis . qed ultimately show ?thesis .. qed end end end (* pm_powerprod *) end (* theory *)