diff --git a/thys/Groebner_Macaulay/Degree_Bound_Utils.thy b/thys/Groebner_Macaulay/Degree_Bound_Utils.thy --- a/thys/Groebner_Macaulay/Degree_Bound_Utils.thy +++ b/thys/Groebner_Macaulay/Degree_Bound_Utils.thy @@ -1,314 +1,314 @@ (* Author: Alexander Maletzky *) section \Utility Definitions and Lemmas about Degree Bounds for Gr\"obner Bases\ theory Degree_Bound_Utils imports Groebner_Bases.Groebner_PM begin context pm_powerprod begin definition is_GB_cofactor_bound :: "(('x \\<^sub>0 nat) \\<^sub>0 'b::field) set \ nat \ bool" where "is_GB_cofactor_bound F b \ - (\G. punit.is_Groebner_basis G \ ideal G = ideal F \ UNION G indets \ UNION F indets \ + (\G. punit.is_Groebner_basis G \ ideal G = ideal F \ (UN g:G. indets g) \ (UN f:F. indets f) \ (\g\G. \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f\F'. poly_deg (q f * f) \ b)))" definition is_hom_GB_bound :: "(('x \\<^sub>0 nat) \\<^sub>0 'b::field) set \ nat \ bool" where "is_hom_GB_bound F b \ ((\f\F. homogeneous f) \ (\g\punit.reduced_GB F. poly_deg g \ b))" lemma is_GB_cofactor_boundI: - assumes "punit.is_Groebner_basis G" and "ideal G = ideal F" and "UNION G indets \ UNION F indets" + assumes "punit.is_Groebner_basis G" and "ideal G = ideal F" and "\(indets ` G) \ \(indets ` F)" and "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f\F'. poly_deg (q f * f) \ b)" shows "is_GB_cofactor_bound F b" unfolding is_GB_cofactor_bound_def using assms by blast lemma is_GB_cofactor_boundE: fixes F :: "(('x \\<^sub>0 nat) \\<^sub>0 'b::field) set" assumes "is_GB_cofactor_bound F b" - obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "UNION G indets \ UNION F indets" + obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "\(indets ` G) \ \(indets ` F)" and "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ - (\f. indets (q f) \ UNION F indets \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" + (\f. indets (q f) \ \(indets ` F) \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" proof - - let ?X = "UNION F indets" - from assms obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "UNION G indets \ ?X" + let ?X = "\(indets ` F)" + from assms obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "\(indets ` G) \ ?X" and 1: "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f\F'. poly_deg (q f * f) \ b)" by (auto simp: is_GB_cofactor_bound_def) from this(1, 2, 3) show ?thesis proof fix g assume "g \ G" show "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. indets (q f) \ ?X \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" proof (cases "g = 0") case True define q where "q = (\f::('x \\<^sub>0 nat) \\<^sub>0 'b. 0::('x \\<^sub>0 nat) \\<^sub>0 'b)" show ?thesis proof (intro exI conjI allI) show "g = (\f\{}. q f * f)" by (simp add: True q_def) qed (simp_all add: q_def) next case False - let ?X = "UNION F indets" + let ?X = "\(indets ` F)" from \g \ G\ have "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f\F'. poly_deg (q f * f) \ b)" by (rule 1) then obtain F' q0 where "finite F'" and "F' \ F" and g: "g = (\f\F'. q0 f * f)" and q0: "\f. f \ F' \ poly_deg (q0 f * f) \ b" by blast define sub where "sub = (\x::'x. if x \ ?X then monomial (1::'b) (Poly_Mapping.single x (1::nat)) else 1)" have 1: "sub x = monomial 1 (monomial 1 x)" if "x \ indets g" for x proof (simp add: sub_def, rule) - from that \g \ G\ have "x \ UNION G indets" by blast + from that \g \ G\ have "x \ \(indets ` G)" by blast also have "\ \ ?X" by fact finally obtain f where "f \ F" and "x \ indets f" .. assume "\f\F. x \ indets f" hence "x \ indets f" using \f \ F\ .. thus "monomial 1 (monomial (Suc 0) x) = 1" using \x \ indets f\ .. qed have 2: "sub x = monomial 1 (monomial 1 x)" if "f \ F'" and "x \ indets f" for f x proof (simp add: sub_def, rule) assume "\f\F. x \ indets f" moreover from that(1) \F' \ F\ have "f \ F" .. ultimately have "x \ indets f" .. thus "monomial 1 (monomial (Suc 0) x) = 1" using that(2) .. qed have 3: "poly_subst sub f = f" if "f \ F'" for f by (rule poly_subst_id, rule 2, rule that) define q where "q = (\f. if f \ F' then poly_subst sub (q0 f) else 0)" show ?thesis proof (intro exI allI conjI impI) from 1 have "g = poly_subst sub g" by (rule poly_subst_id[symmetric]) also have "\ = (\f\F'. q f * (poly_subst sub f))" by (simp add: g poly_subst_sum poly_subst_times q_def cong: sum.cong) also from refl have "\ = (\f\F'. q f * f)" proof (rule sum.cong) fix f assume "f \ F'" hence "poly_subst sub f = f" by (rule 3) thus "q f * poly_subst sub f = q f * f" by simp qed finally show "g = (\f\F'. q f * f)" . next fix f have "indets (q f) \ ?X \ poly_deg (q f * f) \ b" proof (cases "f \ F'") case True hence qf: "q f = poly_subst sub (q0 f)" by (simp add: q_def) show ?thesis proof show "indets (q f) \ ?X" proof fix x assume "x \ indets (q f)" then obtain y where "x \ indets (sub y)" unfolding qf by (rule in_indets_poly_substE) hence y: "y \ ?X" and "x \ indets (monomial (1::'b) (monomial (1::nat) y))" by (simp_all add: sub_def split: if_splits) from this(2) have "x = y" by (simp add: indets_monomial) with y show "x \ ?X" by (simp only:) qed next from \f \ F'\ have "poly_subst sub f = f" by (rule 3) hence "poly_deg (q f * f) = poly_deg (q f * poly_subst sub f)" by (simp only:) also have "\ = poly_deg (poly_subst sub (q0 f * f))" by (simp only: qf poly_subst_times) also have "\ \ poly_deg (q0 f * f)" proof (rule poly_deg_poly_subst_le) fix x show "poly_deg (sub x) \ 1" by (simp add: sub_def poly_deg_monomial deg_pm_single) qed also from \f \ F'\ have "\ \ b" by (rule q0) finally show "poly_deg (q f * f) \ b" . qed next case False thus ?thesis by (simp add: q_def) qed thus "indets (q f) \ ?X" and "poly_deg (q f * f) \ b" by simp_all assume "f \ F'" thus "q f = 0" by (simp add: q_def) qed fact+ qed qed qed lemma is_GB_cofactor_boundE_Polys: fixes F :: "(('x \\<^sub>0 nat) \\<^sub>0 'b::field) set" assumes "is_GB_cofactor_bound F b" and "F \ P[X]" obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[X]" and "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" proof - - let ?X = "UNION F indets" + let ?X = "\(indets ` F)" have "?X \ X" proof fix x assume "x \ ?X" then obtain f where "f \ F" and "x \ indets f" .. from this(1) assms(2) have "f \ P[X]" .. hence "indets f \ X" by (rule PolysD) with \x \ indets f\ show "x \ X" .. qed from assms(1) obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" - and 1: "UNION G indets \ ?X" + and 1: "\(indets ` G) \ ?X" and 2: "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. indets (q f) \ ?X \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" by (rule is_GB_cofactor_boundE) blast from this(1, 2) show ?thesis proof show "G \ P[X]" proof fix g assume "g \ G" - hence "indets g \ UNION G indets" by blast + hence "indets g \ \(indets ` G)" by blast also have "\ \ ?X" by fact also have "\ \ X" by fact finally show "g \ P[X]" by (rule PolysI_alt) qed next fix g assume "g \ G" hence "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. indets (q f) \ ?X \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" by (rule 2) then obtain F' q where "finite F'" and "F' \ F" and "g = (\f\F'. q f * f)" and "\f. indets (q f) \ ?X" and "\f. poly_deg (q f * f) \ b" and "\f. f \ F' \ q f = 0" by blast show "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" proof (intro exI allI conjI impI) fix f from \indets (q f) \ ?X\ \?X \ X\ have "indets (q f) \ X" by (rule subset_trans) thus "q f \ P[X]" by (rule PolysI_alt) qed fact+ qed qed lemma is_GB_cofactor_boundE_finite_Polys: fixes F :: "(('x \\<^sub>0 nat) \\<^sub>0 'b::field) set" assumes "is_GB_cofactor_bound F b" and "finite F" and "F \ P[X]" obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[X]" and "\g. g \ G \ \q. g = (\f\F. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b)" proof - from assms(1, 3) obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[X]" and 1: "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" by (rule is_GB_cofactor_boundE_Polys) blast from this(1, 2, 3) show ?thesis proof fix g assume "g \ G" hence "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b \ (f \ F' \ q f = 0))" by (rule 1) then obtain F' q where "F' \ F" and g: "g = (\f\F'. q f * f)" and "\f. q f \ P[X]" and "\f. poly_deg (q f * f) \ b" and 2: "\f. f \ F' \ q f = 0" by blast show "\q. g = (\f\F. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b)" proof (intro exI conjI impI allI) from assms(2) \F' \ F\ have "(\f\F'. q f * f) = (\f\F. q f * f)" proof (intro sum.mono_neutral_left ballI) fix f assume "f \ F - F'" hence "f \ F'" by simp hence "q f = 0" by (rule 2) thus "q f * f = 0" by simp qed thus "g = (\f\F. q f * f)" by (simp only: g) qed fact+ qed qed lemma is_GB_cofactor_boundI_subset_zero: assumes "F \ {0}" shows "is_GB_cofactor_bound F b" using punit.is_Groebner_basis_empty proof (rule is_GB_cofactor_boundI) from assms show "ideal {} = ideal F" by (metis ideal.span_empty ideal_eq_zero_iff) qed simp_all lemma is_hom_GB_boundI: "(\g. (\f. f \ F \ homogeneous f) \ g \ punit.reduced_GB F \ poly_deg g \ b) \ is_hom_GB_bound F b" unfolding is_hom_GB_bound_def by blast lemma is_hom_GB_boundD: "is_hom_GB_bound F b \ (\f. f \ F \ homogeneous f) \ g \ punit.reduced_GB F \ poly_deg g \ b" unfolding is_hom_GB_bound_def by blast text \The following is the main theorem in this theory. It shows that a bound for Gr\"obner bases of homogenized input sets is always also a cofactor bound for the original input sets.\ lemma (in extended_ord_pm_powerprod) hom_GB_bound_is_GB_cofactor_bound: assumes "finite X" and "F \ P[X]" and "extended_ord.is_hom_GB_bound (homogenize None ` extend_indets ` F) b" shows "is_GB_cofactor_bound F b" proof - let ?F = "homogenize None ` extend_indets ` F" define Y where "Y = \ (indets ` F)" define G where "G = restrict_indets ` (extended_ord.punit.reduced_GB ?F)" have "Y \ X" proof fix x assume "x \ Y" then obtain f where "f \ F" and "x \ indets f" unfolding Y_def .. from this(1) assms(2) have "f \ P[X]" .. hence "indets f \ X" by (rule PolysD) with \x \ indets f\ show "x \ X" .. qed hence "finite Y" using assms(1) by (rule finite_subset) moreover have "F \ P[Y]" by (auto simp: Y_def Polys_alt) ultimately have "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[Y]" unfolding G_def by (rule restrict_indets_reduced_GB)+ from this(1, 2) show ?thesis proof (rule is_GB_cofactor_boundI) from \G \ P[Y]\ show "\ (indets ` G) \ \ (indets ` F)" by (auto simp: Y_def Polys_alt) next fix g assume "g \ G" then obtain g' where g': "g' \ extended_ord.punit.reduced_GB ?F" and g: "g = restrict_indets g'" unfolding G_def .. have "f \ ?F \ homogeneous f" for f by (auto simp: homogeneous_homogenize) with assms(3) have "poly_deg g' \ b" using g' by (rule extended_ord.is_hom_GB_boundD) from g' have "g' \ ideal (extended_ord.punit.reduced_GB ?F)" by (rule ideal.span_base) also have "\ = ideal ?F" proof (rule extended_ord.reduced_GB_ideal_Polys) from \finite Y\ show "finite (insert None (Some ` Y))" by simp next show "?F \ P[insert None (Some ` Y)]" proof fix f0 assume "f0 \ ?F" then obtain f where "f \ F" and f0: "f0 = homogenize None (extend_indets f)" by blast from this(1) \F \ P[Y]\ have "f \ P[Y]" .. hence "extend_indets f \ P[Some ` Y]" by (auto simp: indets_extend_indets Polys_alt) thus "f0 \ P[insert None (Some ` Y)]" unfolding f0 by (rule homogenize_in_Polys) qed qed finally have "g' \ ideal ?F" . with \\f. f \ ?F \ homogeneous f\ obtain F0 q where "finite F0" and "F0 \ ?F" and g': "g' = (\f\F0. q f * f)" and deg_le: "\f. poly_deg (q f * f) \ poly_deg g'" by (rule homogeneous_idealE) blast+ from this(2) obtain F' where "F' \ F" and F0: "F0 = homogenize None ` extend_indets ` F'" and inj_on: "inj_on (homogenize None \ extend_indets) F'" unfolding image_comp by (rule subset_imageE_inj) show "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f\F'. poly_deg (q f * f) \ b)" proof (intro exI conjI ballI) from inj_on \finite F0\ show "finite F'" by (simp only: finite_image_iff F0 image_comp) next from inj_on show "g = (\f\F'. (restrict_indets \ q \ homogenize None \ extend_indets) f * f)" by (simp add: g g' F0 restrict_indets_sum restrict_indets_times sum.reindex image_comp o_def) next fix f assume "f \ F'" have "poly_deg ((restrict_indets \ q \ homogenize None \ extend_indets) f * f) = poly_deg (restrict_indets (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f)))" by (simp add: restrict_indets_times) also have "\ \ poly_deg (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f))" by (rule poly_deg_restrict_indets_le) also have "\ \ poly_deg g'" by (rule deg_le) also have "\ \ b" by fact finally show "poly_deg ((restrict_indets \ q \ homogenize None \ extend_indets) f * f) \ b" . qed fact qed qed end (* pm_powerprod *) end (* theory *) diff --git a/thys/Groebner_Macaulay/Dube_Bound.thy b/thys/Groebner_Macaulay/Dube_Bound.thy --- a/thys/Groebner_Macaulay/Dube_Bound.thy +++ b/thys/Groebner_Macaulay/Dube_Bound.thy @@ -1,1583 +1,1583 @@ (* Author: Alexander Maletzky *) section \Dub\'{e}'s Degree-Bound for Homogeneous Gr\"obner Bases\ theory Dube_Bound imports Poly_Fun Cone_Decomposition Degree_Bound_Utils begin context fixes n d :: nat begin function Dube_aux :: "nat \ nat" where "Dube_aux j = (if j + 2 < n then 2 + ((Dube_aux (j + 1)) choose 2) + (\i=j+3..n-1. (Dube_aux i) choose (Suc (i - j))) else if j + 2 = n then d\<^sup>2 + 2 * d else 2 * d)" by pat_completeness auto termination proof show "wf (measure ((-) n))" by (fact wf_measure) qed auto definition Dube :: nat where "Dube = (if n \ 1 \ d = 0 then d else Dube_aux 1)" lemma Dube_aux_ge_d: "d \ Dube_aux j" proof (induct j rule: Dube_aux.induct) case step: (1 j) have "j + 2 < n \ j + 2 = n \ n < j + 2" by auto show ?case proof (rule linorder_cases) assume *: "j + 2 < n" hence 1: "d \ Dube_aux (j + 1)" by (rule step.hyps)+ show ?thesis proof (cases "d \ 2") case True also from * have "2 \ Dube_aux j" by simp finally show ?thesis . next case False hence "2 < d" by simp hence "2 < Dube_aux (j + 1)" using 1 by (rule less_le_trans) with _ have "Dube_aux (j + 1) \ Dube_aux (j + 1) choose 2" by (rule upper_le_binomial) simp also from * have "\ \ Dube_aux j" by simp finally have "Dube_aux (j + 1) \ Dube_aux j" . with 1 show ?thesis by (rule le_trans) qed next assume "j + 2 = n" thus ?thesis by simp next assume "n < j + 2" thus ?thesis by simp qed qed corollary Dube_ge_d: "d \ Dube" by (simp add: Dube_def Dube_aux_ge_d del: Dube_aux.simps) text \Dub\'{e} in @{cite Dube1990} proves the following theorem, to obtain a short closed form for the degree bound. However, the proof he gives is wrong: In the last-but-one proof step of Lemma 8.1 the sum on the right-hand-side of the inequality can be greater than 1/2 (e.g. for @{prop "n = 7"}, @{prop "d = 2"} and @{prop "j = 1"}), rendering the value inside the big brackets negative. This is also true without the additional summand \2\ we had to introduce in function @{const Dube_aux} to correct another mistake found in @{cite Dube1990}. Nonetheless, experiments carried out in Mathematica still suggest that the short closed form is a valid upper bound for @{const Dube}, even with the additional summand \2\. So, with some effort it might be possible to prove the theorem below; but in fact function @{const Dube} gives typically much better (i.e. smaller) values for concrete values of \n\ and \d\, so it is better to stick to @{const Dube} instead of the closed form anyway. Asymptotically, as \n\ tends to infinity, @{const Dube} grows double exponentially, too.\ theorem "rat_of_nat Dube \ 2 * ((rat_of_nat d)\<^sup>2 / 2 + (rat_of_nat d)) ^ (2 ^ (n - 2))" oops end subsection \Hilbert Function and Hilbert Polynomial\ context pm_powerprod begin context fixes X :: "'x set" assumes fin_X: "finite X" begin lemma Hilbert_fun_cone_aux: assumes "h \ P[X]" and "h \ 0" and "U \ X" and "homogeneous (h::_ \\<^sub>0 'a::field)" shows "Hilbert_fun (cone (h, U)) z = card {t \ .[U]. deg_pm t + poly_deg h = z}" proof - from assms(2) have "lpp h \ keys h" by (rule punit.lt_in_keys) with assms(4) have deg_h[symmetric]: "deg_pm (lpp h) = poly_deg h" by (rule homogeneousD_poly_deg) from assms(1, 3) have "cone (h, U) \ P[X]" by (rule cone_subset_PolysI) with fin_X have "Hilbert_fun (cone (h, U)) z = card (lpp ` (hom_deg_set z (cone (h, U)) - {0}))" using subspace_cone[of "(h, U)"] by (simp only: Hilbert_fun_alt) also from assms(4) have "lpp ` (hom_deg_set z (cone (h, U)) - {0}) = {t \ lpp ` (cone (h, U) - {0}). deg_pm t = z}" by (intro image_lt_hom_deg_set homogeneous_set_coneI) also have "{t \ lpp ` (cone (h, U) - {0}). deg_pm t = z} = (\t. t + lpp h) ` {t \ .[U]. deg_pm t + poly_deg h = z}" (is "?A = ?B") proof show "?A \ ?B" proof fix t assume "t \ ?A" hence "t \ lpp ` (cone (h, U) - {0})" and "deg_pm t = z" by simp_all from this(1) obtain a where "a \ cone (h, U) - {0}" and 2: "t = lpp a" .. from this(1) have "a \ cone (h, U)" and "a \ 0" by simp_all from this(1) obtain q where "q \ P[U]" and a: "a = q * h" by (rule coneE) from \a \ 0\ have "q \ 0" by (auto simp: a) hence t: "t = lpp q + lpp h" using assms(2) unfolding 2 a by (rule lp_times) hence "deg_pm (lpp q) + poly_deg h = deg_pm t" by (simp add: deg_pm_plus deg_h) also have "\ = z" by fact finally have "deg_pm (lpp q) + poly_deg h = z" . moreover from \q \ P[U]\ have "lpp q \ .[U]" by (rule PPs_closed_lpp) ultimately have "lpp q \ {t \ .[U]. deg_pm t + poly_deg h = z}" by simp moreover have "t = lpp q + lpp h" by (simp only: t) ultimately show "t \ ?B" by (rule rev_image_eqI) qed next show "?B \ ?A" proof fix t assume "t \ ?B" then obtain s where "s \ {t \ .[U]. deg_pm t + poly_deg h = z}" and t1: "t = s + lpp h" .. from this(1) have "s \ .[U]" and 1: "deg_pm s + poly_deg h = z" by simp_all let ?q = "monomial (1::'a) s" have "?q \ 0" by (simp add: monomial_0_iff) hence "?q * h \ 0" and "lpp (?q * h) = lpp ?q + lpp h" using \h \ 0\ by (rule times_not_zero, rule lp_times) hence t: "t = lpp (?q * h)" by (simp add: t1 punit.lt_monomial) from \s \ .[U]\ have "?q \ P[U]" by (rule Polys_closed_monomial) with refl have "?q * h \ cone (h, U)" by (rule coneI) moreover from _ assms(2) have "?q * h \ 0" by (rule times_not_zero) (simp add: monomial_0_iff) ultimately have "?q * h \ cone (h, U) - {0}" by simp hence "t \ lpp ` (cone (h, U) - {0})" unfolding t by (rule imageI) moreover have "deg_pm t = int z" by (simp add: t1) (simp add: deg_pm_plus deg_h flip: 1) ultimately show "t \ ?A" by simp qed qed also have "card \ = card {t \ .[U]. deg_pm t + poly_deg h = z}" by (simp add: card_image) finally show ?thesis . qed lemma Hilbert_fun_cone_empty: assumes "h \ P[X]" and "h \ 0" and "homogeneous (h::_ \\<^sub>0 'a::field)" shows "Hilbert_fun (cone (h, {})) z = (if poly_deg h = z then 1 else 0)" proof - have "Hilbert_fun (cone (h, {})) z = card {t \ .[{}::'x set]. deg_pm t + poly_deg h = z}" using assms(1, 2) empty_subsetI assms(3) by (rule Hilbert_fun_cone_aux) also have "\ = (if poly_deg h = z then 1 else 0)" by simp finally show ?thesis . qed lemma Hilbert_fun_cone_nonempty: assumes "h \ P[X]" and "h \ 0" and "U \ X" and "homogeneous (h::_ \\<^sub>0 'a::field)" and "U \ {}" shows "Hilbert_fun (cone (h, U)) z = (if poly_deg h \ z then ((z - poly_deg h) + (card U - 1)) choose (card U - 1) else 0)" proof (cases "poly_deg h \ z") case True from assms(3) fin_X have "finite U" by (rule finite_subset) from assms(1-4) have "Hilbert_fun (cone (h, U)) z = card {t \ .[U]. deg_pm t + poly_deg h = z}" by (rule Hilbert_fun_cone_aux) also from True have "{t \ .[U]. deg_pm t + poly_deg h = z} = deg_sect U (z - poly_deg h)" by (auto simp: deg_sect_def) also from \finite U\ assms(5) have "card \ = (z - poly_deg h) + (card U - 1) choose (card U - 1)" by (rule card_deg_sect) finally show ?thesis by (simp add: True) next case False from assms(1-4) have "Hilbert_fun (cone (h, U)) z = card {t \ .[U]. deg_pm t + poly_deg h = z}" by (rule Hilbert_fun_cone_aux) also from False have "{t \ .[U]. deg_pm t + poly_deg h = z} = {}" by auto hence "card {t \ .[U]. deg_pm t + poly_deg h = z} = card ({}::('x \\<^sub>0 nat) set)" by (rule arg_cong) also have "\ = 0" by simp finally show ?thesis by (simp add: False) qed corollary Hilbert_fun_Polys: assumes "X \ {}" shows "Hilbert_fun (P[X]::(_ \\<^sub>0 'a::field) set) z = (z + (card X - 1)) choose (card X - 1)" proof - let ?one = "1::('x \\<^sub>0 nat) \\<^sub>0 'a" have "Hilbert_fun (P[X]::(_ \\<^sub>0 'a) set) z = Hilbert_fun (cone (?one, X)) z" by simp also have "\ = (if poly_deg ?one \ z then ((z - poly_deg ?one) + (card X - 1)) choose (card X - 1) else 0)" using one_in_Polys _ subset_refl _ assms by (rule Hilbert_fun_cone_nonempty) simp_all also have "\ = (z + (card X - 1)) choose (card X - 1)" by simp finally show ?thesis . qed lemma Hilbert_fun_cone_decomp: assumes "cone_decomp T ps" and "valid_decomp X ps" and "hom_decomp ps" shows "Hilbert_fun T z = (\hU\set ps. Hilbert_fun (cone hU) z)" proof - note fin_X moreover from assms(2, 1) have "T \ P[X]" by (rule valid_cone_decomp_subset_Polys) moreover from assms(1) have dd: "direct_decomp T (map cone ps)" by (rule cone_decompD) ultimately have "Hilbert_fun T z = (\s\set (map cone ps). Hilbert_fun s z)" proof (rule Hilbert_fun_direct_decomp) fix cn assume "cn \ set (map cone ps)" then obtain hU where "hU \ set ps" and cn: "cn = cone hU" unfolding set_map .. note this(1) moreover obtain h U where hU: "hU = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set ps" by simp with assms(3) have "homogeneous h" by (rule hom_decompD) thus "homogeneous_set cn" unfolding cn hU by (rule homogeneous_set_coneI) show "phull.subspace cn" unfolding cn by (fact subspace_cone) qed also have "\ = (\hU\set ps. ((\s. Hilbert_fun s z) \ cone) hU)" unfolding set_map using finite_set proof (rule sum.reindex_nontrivial) fix hU1 hU2 assume "hU1 \ set ps" and "hU2 \ set ps" and "hU1 \ hU2" with dd have "cone hU1 \ cone hU2 = {0}" using zero_in_cone by (rule direct_decomp_map_Int_zero) moreover assume "cone hU1 = cone hU2" ultimately show "Hilbert_fun (cone hU1) z = 0" by simp qed finally show ?thesis by simp qed definition Hilbert_poly :: "(nat \ nat) \ int \ int" where "Hilbert_poly b = (\z::int. let n = card X in ((z - b (Suc n) + n) gchoose n) - 1 - (\i=1..n. (z - b i + i - 1) gchoose i))" lemma poly_fun_Hilbert_poly: "poly_fun (Hilbert_poly b)" by (simp add: Hilbert_poly_def Let_def) lemma Hilbert_fun_eq_Hilbert_poly_plus_card: assumes "X \ {}" and "valid_decomp X ps" and "hom_decomp ps" and "cone_decomp T ps" and "standard_decomp k ps" and "exact_decomp X 0 ps" and "\ ps (Suc 0) \ d" shows "int (Hilbert_fun T d) = card {h::_ \\<^sub>0 'a::field. (h, {}) \ set ps \ poly_deg h = d} + Hilbert_poly (\ ps) d" proof - define n where "n = card X" with assms(1) have "0 < n" using fin_X by (simp add: card_gt_0_iff) hence "1 \ n" and "Suc 0 \ n" by simp_all from pos_decomp_subset have eq0: "(set ps - set (ps\<^sub>+)) \ set (ps\<^sub>+) = set ps" by blast have "set ps - set (ps\<^sub>+) \ set ps" by blast hence fin2: "finite (set ps - set (ps\<^sub>+))" using finite_set by (rule finite_subset) have "(\hU\set ps - set (ps\<^sub>+). Hilbert_fun (cone hU) d) = (\(h, U)\set ps - set (ps\<^sub>+). if poly_deg h = d then 1 else 0)" using refl proof (rule sum.cong) fix x assume "x \ set ps - set (ps\<^sub>+)" moreover obtain h U where x: "x = (h, U)" using prod.exhaust by blast ultimately have "U = {}" and "(h, U) \ set ps" by (simp_all add: pos_decomp_def) from assms(2) this(2) have "h \ P[X]" and "h \ 0" by (rule valid_decompD)+ moreover from assms(3) \(h, U) \ set ps\ have "homogeneous h" by (rule hom_decompD) ultimately show "Hilbert_fun (cone x) d = (case x of (h, U) \ if poly_deg h = d then 1 else 0)" by (simp add: x \U = {}\ Hilbert_fun_cone_empty split del: if_split) qed also from fin2 have "\ = (\(h, U)\{(h', U') \ set ps - set (ps\<^sub>+). poly_deg h' = d}. 1)" by (rule sum.mono_neutral_cong_right) (auto split: if_splits) also have "\ = card {(h, U) \ set ps - set (ps\<^sub>+). poly_deg h = d}" by auto also have "\ = card {h. (h, {}) \ set ps \ poly_deg h = d}" by (fact card_Diff_pos_decomp) finally have eq1: "(\hU\set ps - set (ps\<^sub>+). Hilbert_fun (cone hU) d) = card {h. (h, {}) \ set ps \ poly_deg h = d}" . let ?f = "\a b. (int d) - a + b gchoose b" have "int (\hU\set (ps\<^sub>+). Hilbert_fun (cone hU) d) = (\hU\set (ps\<^sub>+). int (Hilbert_fun (cone hU) d))" by (simp add: int_sum prod.case_distrib) also have "\ = (\(h, U)\(\i\{1..n}. {(h, U) \ set (ps\<^sub>+). card U = i}). ?f (poly_deg h) (card U - 1))" proof (rule sum.cong) show "set (ps\<^sub>+) = (\i\{1..n}. {(h, U). (h, U) \ set (ps\<^sub>+) \ card U = i})" proof (rule Set.set_eqI, rule) fix x assume "x \ set (ps\<^sub>+)" moreover obtain h U where x: "x = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set (ps\<^sub>+)" by simp hence "(h, U) \ set ps" and "U \ {}" by (simp_all add: pos_decomp_def) from fin_X assms(6) 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) moreover from fin_X \U \ X\ have "card U \ n" unfolding n_def by (rule card_mono) ultimately have "card U \ {1..n}" by simp moreover from \(h, U) \ set (ps\<^sub>+)\ have "(h, U) \ {(h', U'). (h', U') \ set (ps\<^sub>+) \ card U' = card U}" by simp ultimately show "x \ (\i\{1..n}. {(h, U). (h, U) \ set (ps\<^sub>+) \ card U = i})" by (simp add: x) qed blast next fix x assume "x \ (\i\{1..n}. {(h, U). (h, U) \ set (ps\<^sub>+) \ card U = i})" then obtain j where "j \ {1..n}" and "x \ {(h, U). (h, U) \ set (ps\<^sub>+) \ card U = j}" .. from this(2) obtain h U where "(h, U) \ set (ps\<^sub>+)" and "card U = j" and x: "x = (h, U)" by blast from fin_X assms(2, 5) this(1) have "poly_deg h < \ ps (Suc 0)" by (rule \_one_gr) also have "\ \ d" by fact finally have "poly_deg h < d" . hence int1: "int (d - poly_deg h) = int d - int (poly_deg h)" by simp from \card U = j\ \j \ {1..n}\ have "0 < card U" by simp hence int2: "int (card U - Suc 0) = int (card U) - 1" by simp from \(h, U) \ set (ps\<^sub>+)\ have "(h, U) \ set ps" using pos_decomp_subset .. with assms(2) have "h \ P[X]" and "h \ 0" and "U \ X" by (rule valid_decompD)+ moreover from assms(3) \(h, U) \ set ps\ have "homogeneous h" by (rule hom_decompD) moreover from \0 < card U\ have "U \ {}" by auto ultimately have "Hilbert_fun (cone (h, U)) d = (if poly_deg h \ d then (d - poly_deg h + (card U - 1)) choose (card U - 1) else 0)" by (rule Hilbert_fun_cone_nonempty) also from \poly_deg h < d\ have "\ = (d - poly_deg h + (card U - 1)) choose (card U - 1)" by simp finally have "int (Hilbert_fun (cone (h, U)) d) = (int d - int (poly_deg h) + (int (card U - 1))) gchoose (card U - 1)" by (simp add: int_binomial int1 int2) thus "int (Hilbert_fun (cone x) d) = (case x of (h, U) \ int d - int (poly_deg h) + (int (card U - 1)) gchoose (card U - 1))" by (simp add: x) qed also have "\ = (\j=1..n. \(h, U)\{(h', U') \ set (ps\<^sub>+). card U' = j}. ?f (poly_deg h) (card U - 1))" proof (intro sum.UNION_disjoint ballI) fix j have "{(h, U). (h, U) \ set (ps\<^sub>+) \ card U = j} \ set (ps\<^sub>+)" by blast thus "finite {(h, U). (h, U) \ set (ps\<^sub>+) \ card U = j}" using finite_set by (rule finite_subset) qed blast+ also from refl have "\ = (\j=1..n. ?f (\ ps (Suc j)) j - ?f (\ ps j) j)" proof (rule sum.cong) fix j assume "j \ {1..n}" hence "Suc 0 \ j" and "0 < j" and "j \ n" by simp_all from fin_X this(1) have "\ ps j \ \ ps (Suc 0)" by (rule \_decreasing) also have "\ \ d" by fact finally have "\ ps j \ d" . from fin_X have "\ ps (Suc j) \ \ ps j" by (rule \_decreasing) simp hence "\ ps (Suc j) \ d" using \\ ps j \ d\ by (rule le_trans) from \0 < j\ have int_j: "int (j - Suc 0) = int j - 1" by simp have "(\(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ card U' = j}. ?f (poly_deg h) (card U - 1)) = (\(h, U)\(\d0\{\ ps (Suc j)..int (\ ps j) - 1}. {(h', U'). (h', U') \ set (ps\<^sub>+) \ int (poly_deg h') = d0 \ card U' = j}). ?f (poly_deg h) (card U - 1))" using _ refl proof (rule sum.cong) show "{(h', U'). (h', U') \ set (ps\<^sub>+) \ card U' = j} = (\d0\{\ ps (Suc j)..int (\ ps j) - 1}. {(h', U'). (h', U') \ set (ps\<^sub>+) \ int (poly_deg h') = d0 \ card U' = j})" proof (rule Set.set_eqI, rule) fix x assume "x \ {(h', U'). (h', U') \ set (ps\<^sub>+) \ card U' = j}" moreover obtain h U where x: "x = (h, U)" using prod.exhaust by blast ultimately have "(h, U) \ set (ps\<^sub>+)" and "card U = j" by simp_all with fin_X assms(5, 6) \Suc 0 \ j\ \j \ n\ have "\ ps (Suc j) \ poly_deg h" unfolding n_def by (rule lem_6_1_3) moreover from fin_X have "poly_deg h < \ ps j" proof (rule \) from \(h, U) \ set (ps\<^sub>+)\ show "(h, U) \ set ps" using pos_decomp_subset .. next show "j \ card U" by (simp add: \card U = j\) qed ultimately have "poly_deg h \ {\ ps (Suc j)..int (\ ps j) - 1}" by simp moreover have "(h, U) \ {(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = poly_deg h \ card U' = card U}" using \(h, U) \ set (ps\<^sub>+)\ by simp ultimately show "x \ (\d0\{\ ps (Suc j)..int (\ ps j) - 1}. {(h', U'). (h', U') \ set (ps\<^sub>+) \ int (poly_deg h') = d0 \ card U' = j})" by (simp add: x \card U = j\) qed blast qed also have "\ = (\d0=\ ps (Suc j)..int (\ ps j) - 1. \(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j}. ?f (poly_deg h) (card U - 1))" proof (intro sum.UNION_disjoint ballI) fix d0::int have "{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j} \ set (ps\<^sub>+)" by blast thus "finite {(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j}" using finite_set by (rule finite_subset) qed blast+ also from refl have "\ = (\d0=\ ps (Suc j)..int (\ ps j) - 1. ?f d0 (j - 1))" proof (rule sum.cong) fix d0 assume "d0 \ {\ ps (Suc j)..int (\ ps j) - 1}" hence "\ ps (Suc j) \ d0" and "d0 < int (\ ps j)" by simp_all hence "\ ps (Suc j) \ nat d0" and "nat d0 < \ ps j" by simp_all have "(\(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j}. ?f (poly_deg h) (card U - 1)) = (\(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j}. ?f d0 (j - 1))" using refl by (rule sum.cong) auto also have "\ = card {(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = nat d0 \ card U' = j} * ?f d0 (j - 1)" using \\ ps (Suc j) \ d0\ by (simp add: int_eq_iff) also have "\ = ?f d0 (j - 1)" using fin_X assms(5, 6) \Suc 0 \ j\ \j \ n\ \\ ps (Suc j) \ nat d0\ \nat d0 < \ ps j\ by (simp only: n_def lem_6_1_2'(3)) finally show "(\(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ poly_deg h' = d0 \ card U' = j}. ?f (poly_deg h) (card U - 1)) = ?f d0 (j - 1)" . qed also have "\ = (\d0\(-) (int d) ` {\ ps (Suc j)..int (\ ps j) - 1}. d0 + int (j - 1) gchoose (j - 1))" proof - have "inj_on ((-) (int d)) {\ ps (Suc j)..int (\ ps j) - 1}" by (auto simp: inj_on_def) thus ?thesis by (simp only: sum.reindex o_def) qed also have "\ = (\d0\{0..int d - (\ ps (Suc j))}-{0..int d - \ ps j}. d0 + int (j - 1) gchoose (j - 1))" using _ refl proof (rule sum.cong) have "(-) (int d) ` {\ ps (Suc j)..int (\ ps j) - 1} = {int d - (int (\ ps j) - 1)..int d - int (\ ps (Suc j))}" by (simp only: image_diff_atLeastAtMost) also have "\ = {0..int d - int (\ ps (Suc j))} - {0..int d - int (\ ps j)}" proof - from \\ ps j \ d\ have "int (\ ps j) - 1 \ int d" by simp thus ?thesis by auto qed finally show "(-) (int d) ` {\ ps (Suc j)..int (\ ps j) - 1} = {0..int d - int (\ ps (Suc j))} - {0..int d - int (\ ps j)}" . qed also have "\ = (\d0=0..int d - (\ ps (Suc j)). d0 + int (j - 1) gchoose (j - 1)) - (\d0=0..int d - \ ps j. d0 + int (j - 1) gchoose (j - 1))" by (rule sum_diff) (auto simp: \\ ps (Suc j) \ \ ps j\) also from \\ ps (Suc j) \ d\ \\ ps j \ d\ have "\ = ?f (\ ps (Suc j)) j - ?f (\ ps j) j" by (simp add: gchoose_rising_sum, simp add: int_j ac_simps \0 < j\) finally show "(\(h, U)\{(h', U'). (h', U') \ set (ps\<^sub>+) \ card U' = j}. ?f (poly_deg h) (card U - 1)) = ?f (\ ps (Suc j)) j - ?f (\ ps j) j" . qed also have "\ = (\j=1..n. ?f (\ ps (Suc j)) j) - (\j=1..n. ?f (\ ps j) j)" by (fact sum_subtractf) also have "\ = ?f (\ ps (Suc n)) n + (\j=1..n-1. ?f (\ ps (Suc j)) j) - (\j=1..n. ?f (\ ps j) j)" by (simp only: sum_tail_nat[OF \0 < n\ \1 \ n\]) also have "\ = ?f (\ ps (Suc n)) n - ?f (\ ps 1) 1 + ((\j=1..n-1. ?f (\ ps (Suc j)) j) - (\j=1..n-1. ?f (\ ps (Suc j)) (Suc j)))" by (simp only: sum.atLeast_Suc_atMost[OF \1 \ n\] sum_atLeast_Suc_shift[OF \0 < n\ \1 \ n\]) also have "\ = ?f (\ ps (Suc n)) n - ?f (\ ps 1) 1 - (\j=1..n-1. ?f (\ ps (Suc j)) (Suc j) - ?f (\ ps (Suc j)) j)" by (simp only: sum_subtractf) also have "\ = ?f (\ ps (Suc n)) n - 1 - ((int d - \ ps (Suc 0)) gchoose (Suc 0)) - (\j=1..n-1. (int d - \ ps (Suc j) + j) gchoose (Suc j))" proof - have "?f (\ ps 1) 1 = 1 + ((int d - \ ps (Suc 0)) gchoose (Suc 0))" by (simp add: plus_Suc_gbinomial) moreover from refl have "(\j=1..n-1. ?f (\ ps (Suc j)) (Suc j) - ?f (\ ps (Suc j)) j) = (\j=1..n-1. (int d - \ ps (Suc j) + j) gchoose (Suc j))" by (rule sum.cong) (simp add: plus_Suc_gbinomial) ultimately show ?thesis by (simp only:) qed also have "\ = ?f (\ ps (Suc n)) n - 1 - (\j=0..n-1. (int d - \ ps (Suc j) + j) gchoose (Suc j))" by (simp only: sum.atLeast_Suc_atMost[OF le0], simp) also have "\ = ?f (\ ps (Suc n)) n - 1 - (\j=Suc 0..Suc (n-1). (int d - \ ps j + j - 1) gchoose j)" by (simp only: sum.shift_bounds_cl_Suc_ivl, simp add: ac_simps) also have "\ = Hilbert_poly (\ ps) d" using \0 < n\ by (simp add: Hilbert_poly_def Let_def n_def) finally have eq2: "int (\hU\set (ps\<^sub>+). Hilbert_fun (cone hU) d) = Hilbert_poly (\ ps) (int d)" . from assms(4, 2, 3) have "Hilbert_fun T d = (\hU\set ps. Hilbert_fun (cone hU) d)" by (rule Hilbert_fun_cone_decomp) also have "\ = (\hU\(set ps - set (ps\<^sub>+)) \ set (ps\<^sub>+). Hilbert_fun (cone hU) d)" by (simp only: eq0) also have "\ = (\hU\set ps - set (ps\<^sub>+). Hilbert_fun (cone hU) d) + (\hU\set (ps\<^sub>+). Hilbert_fun (cone hU) d)" using fin2 finite_set by (rule sum.union_disjoint) blast also have "\ = card {h. (h, {}) \ set ps \ poly_deg h = d} + (\hU\set (ps\<^sub>+). Hilbert_fun (cone hU) d)" by (simp only: eq1) also have "int \ = card {h. (h, {}) \ set ps \ poly_deg h = d} + Hilbert_poly (\ ps) d" by (simp only: eq2 int_plus) finally show ?thesis . qed corollary Hilbert_fun_eq_Hilbert_poly: assumes "X \ {}" and "valid_decomp X ps" and "hom_decomp ps" and "cone_decomp T ps" and "standard_decomp k ps" and "exact_decomp X 0 ps" and "\ ps 0 \ d" shows "int (Hilbert_fun (T::(_ \\<^sub>0 'a::field) set) d) = Hilbert_poly (\ ps) d" proof - from fin_X have "\ ps (Suc 0) \ \ ps 0" using le0 by (rule \_decreasing) also have "\ \ d" by fact finally have "\ ps (Suc 0) \ d" . with assms(1-6) have "int (Hilbert_fun T d) = int (card {h. (h, {}) \ set ps \ poly_deg h = d}) + Hilbert_poly (\ ps) (int d)" by (rule Hilbert_fun_eq_Hilbert_poly_plus_card) also have "\ = Hilbert_poly (\ ps) (int d)" proof - have eq: "{h. (h, {}) \ set ps \ poly_deg h = d} = {}" proof - { fix h assume "(h, {}) \ set ps" and "poly_deg h = d" from fin_X this(1) le0 have "poly_deg h < \ ps 0" by (rule \) with assms(7) have False by (simp add: \poly_deg h = d\) } thus ?thesis by blast qed show ?thesis by (simp add: eq) qed finally show ?thesis . qed subsection \Dub\'{e}'s Bound\ context fixes f :: "('x \\<^sub>0 nat) \\<^sub>0 'a::field" fixes F assumes n_gr_1: "1 < card X" and fin_F: "finite F" and F_sub: "F \ P[X]" and f_in: "f \ F" and hom_F: "\f'. f' \ F \ homogeneous f'" and f_max: "\f'. f' \ F \ poly_deg f' \ poly_deg f" and d_gr_0: "0 < poly_deg f" and ideal_f_neq: "ideal {f} \ ideal F" begin private abbreviation (input) "n \ card X" private abbreviation (input) "d \ poly_deg f" lemma f_in_Polys: "f \ P[X]" using f_in F_sub .. lemma hom_f: "homogeneous f" using f_in by (rule hom_F) lemma f_not_0: "f \ 0" using d_gr_0 by auto lemma X_not_empty: "X \ {}" using n_gr_1 by auto lemma n_gr_0: "0 < n" using \1 < n\ by simp corollary int_n_minus_1 [simp]: "int (n - Suc 0) = int n - 1" using n_gr_0 by simp lemma int_n_minus_2 [simp]: "int (n - Suc (Suc 0)) = int n - 2" using n_gr_1 by simp lemma cone_f_X_sub: "cone (f, X) \ P[X]" proof - have "cone (f, X) = cone (f * 1, X)" by simp also from f_in_Polys have "\ \ cone (1, X)" by (rule cone_mono_1) finally show ?thesis by simp qed lemma ideal_Int_Polys_eq_cone: "ideal {f} \ P[X] = cone (f, X)" proof (intro subset_antisym subsetI) fix p assume "p \ ideal {f} \ P[X]" hence "p \ ideal {f}" and "p \ P[X]" by simp_all have "finite {f}" by simp then obtain q where "p = (\f'\{f}. q f' * f')" using \p \ ideal {f}\ by (rule ideal.span_finiteE) hence p: "p = q f * f" by simp with \p \ P[X]\ have "f * q f \ P[X]" by (simp only: mult.commute) hence "q f \ P[X]" using f_in_Polys f_not_0 by (rule times_in_PolysD) with p show "p \ cone (f, X)" by (rule coneI) next fix p assume "p \ cone (f, X)" then obtain q where "q \ P[X]" and p: "p = q * f" by (rule coneE) have "f \ ideal {f}" by (rule ideal.span_base) simp with \q \ P[X]\ f_in_Polys show "p \ ideal {f} \ P[X]" unfolding p by (intro IntI ideal.span_scale Polys_closed_times) qed private definition P_ps where "P_ps = (SOME x. valid_decomp X (snd x) \ standard_decomp d (snd x) \ exact_decomp X 0 (snd x) \ cone_decomp (fst x) (snd x) \ hom_decomp (snd x) \ direct_decomp (ideal F \ P[X]) [ideal {f} \ P[X], fst x])" private definition P where "P = fst P_ps" private definition ps where "ps = snd P_ps" lemma shows valid_ps: "valid_decomp X ps" (is ?thesis1) and std_ps: "standard_decomp d ps" (is ?thesis2) and ext_ps: "exact_decomp X 0 ps" (is ?thesis3) and cn_ps: "cone_decomp P ps" (is ?thesis4) and hom_ps: "hom_decomp ps" (is ?thesis5) and decomp_F: "direct_decomp (ideal F \ P[X]) [ideal {f} \ P[X], P]" (is ?thesis6) proof - note fin_X moreover from fin_F have "finite (F - {f})" by simp moreover from F_sub have "F - {f} \ P[X]" by blast ultimately obtain P' ps' where 1: "valid_decomp X ps'" and 2: "standard_decomp d ps'" and 3: "cone_decomp P' ps'" and 40: "(\f'. f' \ F - {f} \ homogeneous f') \ hom_decomp ps'" and 50: "direct_decomp (ideal (insert f (F - {f})) \ P[X]) [ideal {f} \ P[X], P']" using f_in_Polys f_max by (rule ideal_decompE) blast+ have 4: "hom_decomp ps'" by (intro 40 hom_F) simp from 50 f_in have 5: "direct_decomp (ideal F \ P[X]) [ideal {f} \ P[X], P']" by (simp add: insert_absorb) let ?ps = "exact X (poly_deg f) ps'" from fin_X 1 2 have "valid_decomp X ?ps" and "standard_decomp d ?ps" and "exact_decomp X 0 ?ps" by (rule exact)+ moreover from fin_X 1 2 3 have "cone_decomp P' ?ps" by (rule cone_decomp_exact) moreover from fin_X 1 2 4 have "hom_decomp ?ps" by (rule hom_decomp_exact) ultimately have "valid_decomp X (snd (P', ?ps)) \ standard_decomp d (snd (P', ?ps)) \ exact_decomp X 0 (snd (P', ?ps)) \ cone_decomp (fst (P', ?ps)) (snd (P', ?ps)) \ hom_decomp (snd (P', ?ps)) \ direct_decomp (ideal F \ P[X]) [ideal {f} \ P[X], fst (P', ?ps)]" using 5 by simp hence "?thesis1 \ ?thesis2 \ ?thesis3 \ ?thesis4 \ ?thesis5 \ ?thesis6" unfolding P_def ps_def P_ps_def by (rule someI) thus ?thesis1 and ?thesis2 and ?thesis3 and ?thesis4 and ?thesis5 and ?thesis6 by simp_all qed lemma P_sub: "P \ P[X]" using valid_ps cn_ps by (rule valid_cone_decomp_subset_Polys) lemma ps_not_Nil: "ps\<^sub>+ \ []" proof assume "ps\<^sub>+ = []" have "Keys P \ (\hU\set ps. keys (fst hU))" (is "_ \ ?A") proof fix t assume "t \ Keys P" then obtain p where "p \ P" and "t \ keys p" by (rule in_KeysE) from cn_ps have "direct_decomp P (map cone ps)" by (rule cone_decompD) then obtain qs where qs: "qs \ listset (map cone ps)" and p: "p = sum_list qs" using \p \ P\ by (rule direct_decompE) from \t \ keys p\ keys_sum_list_subset have "t \ Keys (set qs)" unfolding p .. 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 = qs ! i" by (metis in_set_conv_nth) with qs have "i < length ps" and "q \ (map cone ps) ! i" by (simp_all add: listsetD del: nth_map) hence "q \ cone (ps ! i)" by simp obtain h U where eq: "ps ! i = (h, U)" using prod.exhaust by blast from \i < length ps\ this[symmetric] have "(h, U) \ set ps" by simp have "U = {}" proof (rule ccontr) assume "U \ {}" with \(h, U) \ set ps\ have "(h, U) \ set (ps\<^sub>+)" by (simp add: pos_decomp_def) with \ps\<^sub>+ = []\ show False by simp qed with \q \ cone (ps ! i)\ have "q \ range (\c. c \ h)" by (simp only: eq cone_empty) then obtain c where "q = c \ h" .. also have "keys \ \ keys h" by (fact keys_map_scale_subset) finally have "t \ keys h" using \t \ keys q\ .. hence "t \ keys (fst (h, U))" by simp with \(h, U) \ set ps\ show "t \ ?A" .. qed moreover from finite_set finite_keys have "finite ?A" by (rule finite_UN_I) ultimately have "finite (Keys P)" by (rule finite_subset) have "\q\ideal F. q \ P[X] \ q \ 0 \ \ lpp f adds lpp q" proof (rule ccontr) assume "\ (\q\ideal F. q \ P[X] \ q \ 0 \ \ lpp f adds lpp q)" hence adds: "lpp f adds lpp q" if "q \ ideal F" and "q \ P[X]" and "q \ 0" for q using that by blast from fin_X _ F_sub have "ideal {f} = ideal F" proof (rule punit.pmdl_eqI_adds_lt_dgrad_p_set[simplified, OF dickson_grading_varnum, where m=0, simplified dgrad_p_set_varnum]) from f_in_Polys show "{f} \ P[X]" by simp next from f_in have "{f} \ F" by simp thus "ideal {f} \ ideal F" by (rule ideal.span_mono) next fix q assume "q \ ideal F" and "q \ P[X]" and "q \ 0" hence "lpp f adds lpp q" by (rule adds) with f_not_0 show "\g\{f}. g \ 0 \ lpp g adds lpp q" by blast qed with ideal_f_neq show False .. qed then obtain q0 where "q0 \ ideal F" and "q0 \ P[X]" and "q0 \ 0" and nadds_q0: "\ lpp f adds lpp q0" by blast define q where "q = hom_component q0 (deg_pm (lpp q0))" from hom_F \q0 \ ideal F\ have "q \ ideal F" unfolding q_def by (rule homogeneous_ideal) from homogeneous_set_Polys \q0 \ P[X]\ have "q \ P[X]" unfolding q_def by (rule homogeneous_setD) from \q0 \ 0\ have "q \ 0" and "lpp q = lpp q0" unfolding q_def by (rule hom_component_lpp)+ from nadds_q0 this(2) have nadds_q: "\ lpp f adds lpp q" by simp have hom_q: "homogeneous q" by (simp only: q_def homogeneous_hom_component) from nadds_q obtain x where x: "\ lookup (lpp f) x \ lookup (lpp q) x" by (auto simp add: adds_poly_mapping le_fun_def) obtain y where "y \ X" and "y \ x" proof - from n_gr_1 have "2 \ n" by simp then obtain Y where "Y \ X" and "card Y = 2" by (rule card_geq_ex_subset) from this(2) obtain u v where "u \ v" and "Y = {u, v}" by (rule card_2_E) from this obtain y where "y \ Y" and "y \ x" by blast from this(1) \Y \ X\ have "y \ X" .. thus ?thesis using \y \ x\ .. qed define q' where "q' = (\k. punit.monom_mult 1 (Poly_Mapping.single y k) q)" have inj1: "inj q'" by (auto intro!: injI simp: q'_def \q \ 0\ dest: punit.monom_mult_inj_2 monomial_inj) have q'_in: "q' k \ ideal F \ P[X]" for k unfolding q'_def using \q \ ideal F\ \q \ P[X]\ \y \ X\ by (intro IntI punit.pmdl_closed_monom_mult[simplified] Polys_closed_monom_mult PPs_closed_single) have lpp_q': "lpp (q' k) = Poly_Mapping.single y k + lpp q" for k using \q \ 0\ by (simp add: q'_def punit.lt_monom_mult) have inj2: "inj_on (deg_pm \ lpp) (range q')" by (auto intro!: inj_onI simp: lpp_q' deg_pm_plus deg_pm_single dest: monomial_inj) have "(deg_pm \ lpp) ` range q' \ deg_pm ` Keys P" proof fix d assume "d \ (deg_pm \ lpp) ` range q'" then obtain k where d: "d = deg_pm (lpp (q' k))" (is "_ = deg_pm ?t") by auto from hom_q have hom_q': "homogeneous (q' k)" by (simp add: q'_def homogeneous_monom_mult) from \q \ 0\ have "q' k \ 0" by (simp add: q'_def punit.monom_mult_eq_zero_iff) hence "?t \ keys (q' k)" by (rule punit.lt_in_keys) with hom_q' have deg_q': "d = poly_deg (q' k)" unfolding d by (rule homogeneousD_poly_deg) from decomp_F q'_in obtain qs where "qs \ listset [ideal {f} \ P[X], P]" and "q' k = sum_list qs" by (rule direct_decompE) moreover from this(1) obtain f0 p0 where f0: "f0 \ ideal {f} \ P[X]" and p0: "p0 \ P" and "qs = [f0, p0]" by (rule listset_doubletonE) ultimately have q': "q' k = f0 + p0" by simp define f1 where "f1 = hom_component f0 d" define p1 where "p1 = hom_component p0 d" from hom_q have "homogeneous (q' k)" by (simp add: q'_def homogeneous_monom_mult) hence "q' k = hom_component (q' k) d" by (simp add: hom_component_of_homogeneous deg_q') also have "\ = f1 + p1" by (simp only: q' hom_component_plus f1_def p1_def) finally have "q' k = f1 + p1" . have "keys p1 \ {}" proof assume "keys p1 = {}" with \q' k = f1 + p1\ \q' k \ 0\ have t: "?t = lpp f1" and "f1 \ 0" by simp_all from f0 have "f0 \ ideal {f}" by simp with _ have "f1 \ ideal {f}" unfolding f1_def by (rule homogeneous_ideal) (simp add: hom_f) with punit.is_Groebner_basis_singleton obtain g where "g \ {f}" and "lpp g adds lpp f1" using \f1 \ 0\ by (rule punit.GB_adds_lt[simplified]) hence "lpp f adds ?t" by (simp add: t) hence "lookup (lpp f) x \ lookup ?t x" by (simp add: adds_poly_mapping le_fun_def) also have "\ = lookup (lpp q) x" by (simp add: lpp_q' lookup_add lookup_single \y \ x\) finally have "lookup (lpp f) x \ lookup (lpp q) x" . with x show False .. qed then obtain t where "t \ keys p1" by blast hence "d = deg_pm t" by (simp add: p1_def keys_hom_component) from cn_ps hom_ps have "homogeneous_set P" by (intro homogeneous_set_cone_decomp) hence "p1 \ P" using \p0 \ P\ unfolding p1_def by (rule homogeneous_setD) with \t \ keys p1\ have "t \ Keys P" by (rule in_KeysI) with \d = deg_pm t\ show "d \ deg_pm ` Keys P" by (rule image_eqI) qed moreover from inj1 inj2 have "infinite ((deg_pm \ lpp) ` range q')" by (simp add: finite_image_iff o_def) ultimately have "infinite (deg_pm ` Keys P)" by (rule infinite_super) hence "infinite (Keys P)" by blast thus False using \finite (Keys P)\ .. qed private definition N where "N = normal_form F ` P[X]" private definition qs where "qs = (SOME qs'. valid_decomp X qs' \ standard_decomp 0 qs' \ monomial_decomp qs' \ cone_decomp N qs' \ exact_decomp X 0 qs' \ (\g\punit.reduced_GB F. poly_deg g \ \ qs' 0))" private definition "aa \ \ ps" private definition "bb \ \ qs" private abbreviation (input) "cc \ (\i. aa i + bb i)" lemma shows valid_qs: "valid_decomp X qs" (is ?thesis1) and std_qs: "standard_decomp 0 qs" (is ?thesis2) and mon_qs: "monomial_decomp qs" (is ?thesis3) and hom_qs: "hom_decomp qs" (is ?thesis6) and cn_qs: "cone_decomp N qs" (is ?thesis4) and ext_qs: "exact_decomp X 0 qs" (is ?thesis5) and deg_RGB: "g \ punit.reduced_GB F \ poly_deg g \ bb 0" proof - from fin_X F_sub obtain qs' where 1: "valid_decomp X qs'" and 2: "standard_decomp 0 qs'" and 3: "monomial_decomp qs'" and 4: "cone_decomp (normal_form F ` P[X]) qs'" and 5: "exact_decomp X 0 qs'" and 60: "\g. (\f. f \ F \ homogeneous f) \ g \ punit.reduced_GB F \ poly_deg g \ \ qs' 0" by (rule normal_form_exact_decompE) blast from hom_F have "\g. g \ punit.reduced_GB F \ poly_deg g \ \ qs' 0" by (rule 60) with 1 2 3 4 5 have "valid_decomp X qs' \ standard_decomp 0 qs' \ monomial_decomp qs' \ cone_decomp N qs' \ exact_decomp X 0 qs' \ (\g\punit.reduced_GB F. poly_deg g \ \ qs' 0)" by (simp add: N_def) hence "?thesis1 \ ?thesis2 \ ?thesis3 \ ?thesis4 \ ?thesis5 \ (\g\punit.reduced_GB F. poly_deg g \ bb 0)" unfolding qs_def bb_def by (rule someI) thus ?thesis1 and ?thesis2 and ?thesis3 and ?thesis4 and ?thesis5 and "g \ punit.reduced_GB F \ poly_deg g \ bb 0" by simp_all from \?thesis3\ show ?thesis6 by (rule monomial_decomp_imp_hom_decomp) qed lemma N_sub: "N \ P[X]" using valid_qs cn_qs by (rule valid_cone_decomp_subset_Polys) lemma decomp_Polys: "direct_decomp P[X] [ideal {f} \ P[X], P, N]" proof - from fin_X F_sub have "direct_decomp P[X] [ideal F \ P[X], N]" unfolding N_def by (rule direct_decomp_ideal_normal_form) hence "direct_decomp P[X] ([N] @ [ideal {f} \ P[X], P])" using decomp_F by (rule direct_decomp_direct_decomp) hence "direct_decomp P[X] ([ideal {f} \ P[X], P] @ [N])" using perm_append_swap by (rule direct_decomp_perm) thus ?thesis by simp qed lemma aa_Suc_n [simp]: "aa (Suc n) = d" proof - from fin_X ext_ps le_refl have "aa (Suc n) = \ ps" unfolding aa_def by (rule \_card_X) also from fin_X valid_ps std_ps ps_not_Nil have "\ = d" by (rule \_nonempty_unique) finally show ?thesis . qed lemma bb_Suc_n [simp]: "bb (Suc n) = 0" proof - from fin_X ext_qs le_refl have "bb (Suc n) = \ qs" unfolding bb_def by (rule \_card_X) also from std_qs have "\ = 0" unfolding \_def[OF fin_X] by (rule Least_eq_0) finally show ?thesis . qed lemma Hilbert_fun_X: assumes "d \ z" shows "Hilbert_fun (P[X]::(_ \\<^sub>0 'a) set) z = ((z - d) + (n - 1)) choose (n - 1) + Hilbert_fun P z + Hilbert_fun N z" proof - define ss where "ss = [ideal {f} \ P[X], P, N]" have "homogeneous_set A \ phull.subspace A" if "A \ set ss" for A proof - from that have "A = ideal {f} \ P[X] \ A = P \ A = N" by (simp add: ss_def) thus ?thesis proof (elim disjE) assume A: "A = ideal {f} \ P[X]" show ?thesis unfolding A by (intro conjI homogeneous_set_IntI phull.subspace_inter homogeneous_set_homogeneous_ideal homogeneous_set_Polys subspace_ideal subspace_Polys) (simp add: hom_f) next assume A: "A = P" from cn_ps hom_ps show ?thesis unfolding A by (intro conjI homogeneous_set_cone_decomp subspace_cone_decomp) next assume A: "A = N" from cn_qs hom_qs show ?thesis unfolding A by (intro conjI homogeneous_set_cone_decomp subspace_cone_decomp) qed qed hence 1: "\A. A \ set ss \ homogeneous_set A" and 2: "\A. A \ set ss \ phull.subspace A" by simp_all have "Hilbert_fun (P[X]::(_ \\<^sub>0 'a) set) z = (\p\set ss. Hilbert_fun p z)" using fin_X subset_refl decomp_Polys unfolding ss_def proof (rule Hilbert_fun_direct_decomp) fix A assume "A \ set [ideal {f} \ P[X], P, N]" hence "A \ set ss" by (simp only: ss_def) thus "homogeneous_set A" and "phull.subspace A" by (rule 1, rule 2) qed also have "\ = (\p\set ss. count_list ss p * Hilbert_fun p z)" using refl proof (rule sum.cong) fix p assume "p \ set ss" hence "count_list ss p \ 0" by (simp only: count_list_eq_0_iff not_not) hence "count_list ss p = 1 \ 1 < count_list ss p" by auto thus "Hilbert_fun p z = count_list ss p * Hilbert_fun p z" proof assume "1 < count_list ss p" with decomp_Polys have "p = {0}" unfolding ss_def[symmetric] using phull.subspace_0 by (rule direct_decomp_repeated_eq_zero) (rule 2) thus ?thesis by simp qed simp qed also have "\ = sum_list (map (\p. Hilbert_fun p z) ss)" by (rule sym) (rule sum_list_map_eq_sum_count) also have "\ = Hilbert_fun (cone (f, X)) z + Hilbert_fun P z + Hilbert_fun N z" by (simp add: ss_def ideal_Int_Polys_eq_cone) also have "Hilbert_fun (cone (f, X)) z = (z - d + (n - 1)) choose (n - 1)" using f_not_0 f_in_Polys fin_X hom_f X_not_empty by (simp add: Hilbert_fun_cone_nonempty assms) finally show ?thesis . qed lemma dube_eq_0: "(\z::int. (z + int n - 1) gchoose (n - 1)) = (\z::int. ((z - d + n - 1) gchoose (n - 1)) + Hilbert_poly aa z + Hilbert_poly bb z)" (is "?f = ?g") proof (rule poly_fun_eqI_ge) fix z::int let ?z = "nat z" assume "max (aa 0) (bb 0) \ z" hence "aa 0 \ nat z" and "bb 0 \ nat z" and "0 \ z" by simp_all from this(3) have int_z: "int ?z = z" by simp have "d \ aa 0" unfolding aa_Suc_n[symmetric] using fin_X le0 unfolding aa_def by (rule \_decreasing) hence "d \ ?z" using \aa 0 \ nat z\ by (rule le_trans) hence int_zd: "int (?z - d) = z - int d" using int_z by linarith from \d \ ?z\ have "Hilbert_fun (P[X]::(_ \\<^sub>0 'a) set) ?z = ((?z - d) + (n - 1)) choose (n - 1) + Hilbert_fun P ?z + Hilbert_fun N ?z" by (rule Hilbert_fun_X) also have "int \ = (z - d + (n - 1)) gchoose (n - 1) + Hilbert_poly aa z + Hilbert_poly bb z" using X_not_empty valid_ps hom_ps cn_ps std_ps ext_ps \aa 0 \ nat z\ valid_qs hom_qs cn_qs std_qs ext_qs \bb 0 \ nat z\ \0 \ z\ by (simp add: Hilbert_fun_eq_Hilbert_poly int_z aa_def bb_def int_binomial int_zd) finally show "?f z = ?g z" using fin_X X_not_empty \0 \ z\ by (simp add: Hilbert_fun_Polys int_binomial) smt qed (simp_all add: poly_fun_Hilbert_poly) corollary dube_eq_1: "(\z::int. (z + int n - 1) gchoose (n - 1)) = (\z::int. ((z - d + n - 1) gchoose (n - 1)) + ((z - d + n) gchoose n) + ((z + n) gchoose n) - 2 - (\i=1..n. ((z - aa i + i - 1) gchoose i) + ((z - bb i + i - 1) gchoose i)))" by (simp only: dube_eq_0) (auto simp: Hilbert_poly_def Let_def sum.distrib) lemma dube_eq_2: assumes "j < n" shows "(\z::int. (z + int n - int j - 1) gchoose (n - j - 1)) = (\z::int. ((z - d + n - int j - 1) gchoose (n - j - 1)) + ((z - d + n - j) gchoose (n - j)) + ((z + n - j) gchoose (n - j)) - 2 - (\i=Suc j..n. ((z - aa i + i - j - 1) gchoose (i - j)) + ((z - bb i + i - j - 1) gchoose (i - j))))" (is "?f = ?g") proof - let ?h = "\z i. ((z + (int i - aa i - 1)) gchoose i) + ((z + (int i - bb i - 1)) gchoose i)" let ?hj = "\z i. ((z + (int i - aa i - 1) - j) gchoose (i - j)) + ((z + (int i - bb i - 1) - j) gchoose (i - j))" from assms have 1: "j \ n - Suc 0" and 2: "j \ n" by simp_all have eq1: "(bw_diff ^^ j) (\z. \i=1..j. ?h z i) = (\_. if j = 0 then 0 else 2)" proof (cases j) case 0 thus ?thesis by simp next case (Suc j0) hence "j \ 0" by simp have "(\z::int. \i = 1..j. ?h z i) = (\z::int. (\i = 1..j0. ?h z i) + ?h z j)" by (simp add: \j = Suc j0\) moreover have "(bw_diff ^^ j) \ = (\z::int. (\i = 1..j0. (bw_diff ^^ j) (\z. ?h z i) z) + 2)" by (simp add: bw_diff_gbinomial_pow) moreover have "(\i = 1..j0. (bw_diff ^^ j) (\z. ?h z i) z) = (\i = 1..j0. 0)" for z::int using refl proof (rule sum.cong) fix i assume "i \ {1..j0}" hence "\ j \ i" by (simp add: \j = Suc j0\) thus "(bw_diff ^^ j) (\z. ?h z i) z = 0" by (simp add: bw_diff_gbinomial_pow) qed ultimately show ?thesis by (simp add: \j \ 0\) qed have eq2: "(bw_diff ^^ j) (\z. \i=Suc j..n. ?h z i) = (\z. (\i=Suc j..n. ?hj z i))" proof - have "(bw_diff ^^ j) (\z. \i=Suc j..n. ?h z i) = (\z. \i=Suc j..n. (bw_diff ^^ j) (\z. ?h z i) z)" by simp also have "\ = (\z. (\i=Suc j..n. ?hj z i))" proof (intro ext sum.cong) fix z i assume "i \ {Suc j..n}" hence "j \ i" by simp thus "(bw_diff ^^ j) (\z. ?h z i) z = ?hj z i" by (simp add: bw_diff_gbinomial_pow) qed (fact refl) finally show ?thesis . qed from 1 have "?f = (bw_diff ^^ j) (\z::int. (z + (int n - 1)) gchoose (n - 1))" by (simp add: bw_diff_gbinomial_pow) (simp only: algebra_simps) also have "\ = (bw_diff ^^ j) (\z::int. (z + int n - 1) gchoose (n - 1))" by (simp only: algebra_simps) also have "\ = (bw_diff ^^ j) (\z::int. ((z - d + n - 1) gchoose (n - 1)) + ((z - d + n) gchoose n) + ((z + n) gchoose n) - 2 - (\i=1..n. ((z - aa i + i - 1) gchoose i) + ((z - bb i + i - 1) gchoose i)))" by (simp only: dube_eq_1) also have "\ = (bw_diff ^^ j) (\z::int. ((z + (int n - d - 1)) gchoose (n - 1)) + ((z + (int n - d)) gchoose n) + ((z + n) gchoose n) - 2 - (\i=1..n. ?h z i))" by (simp only: algebra_simps) also have "\ = (\z::int. ((z + (int n - d - 1) - j) gchoose (n - 1 - j)) + ((z + (int n - d) - j) gchoose (n - j)) + ((z + n - j) gchoose (n - j)) - (if j = 0 then 2 else 0) - (bw_diff ^^ j) (\z. \i=1..n. ?h z i) z)" using 1 2 by (simp add: bw_diff_const_pow bw_diff_gbinomial_pow del: bw_diff_sum_pow) also from \j \ n\ have "(\z. \i=1..n. ?h z i) = (\z. (\i=1..j. ?h z i) + (\i=Suc j..n. ?h z i))" by (simp add: sum_split_nat_ivl) also have "(bw_diff ^^ j) \ = (\z. (bw_diff ^^ j) (\z. \i=1..j. ?h z i) z + (bw_diff ^^ j) (\z. \i=Suc j..n. ?h z i) z)" by (simp only: bw_diff_plus_pow) also have "\ = (\z. (if j = 0 then 0 else 2) + (\i=Suc j..n. ?hj z i))" by (simp only: eq1 eq2) finally show ?thesis by (simp add: algebra_simps) qed lemma dube_eq_3: assumes "j < n" shows "(1::int) = (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - j) * ((int d - 1) gchoose (n - j)) - 1 - (\i=Suc j..n. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" proof - from assms have 1: "int (n - Suc j) = int n - j - 1" and 2: "int (n - j) = int n - j" by simp_all from assms have "int n - int j - 1 = int (n - j - 1)" by simp hence eq1: "int n - int j - 1 gchoose (n - Suc j) = 1" by simp from assms have "int n - int j = int (n - j)" by simp hence eq2: "int n - int j gchoose (n - j) = 1" by simp have eq3: "int n - d - j - 1 gchoose (n - Suc j) = (- 1)^(n - Suc j) * (int d - 1 gchoose (n - Suc j))" by (simp add: gbinomial_int_negated_upper[of "int n - d - j - 1"] 1) have eq4: "int n - d - j gchoose (n - j) = (- 1)^(n - j) * (int d - 1 gchoose (n - j))" by (simp add: gbinomial_int_negated_upper[of "int n - d - j"] 2) have eq5: "(\i = Suc j..n. int i - aa i - j - 1 gchoose (i - j) + (int i - bb i - j - 1 gchoose (i - j))) = (\i=Suc j..n. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" using refl proof (rule sum.cong) fix i assume "i \ {Suc j..n}" hence "j \ i" by simp hence 3: "int (i - j) = int i - j" by simp show "int i - aa i - j - 1 gchoose (i - j) + (int i - bb i - j - 1 gchoose (i - j)) = (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j)))" by (simp add: gbinomial_int_negated_upper[of "int i - aa i - j - 1"] gbinomial_int_negated_upper[of "int i - bb i - j - 1"] 3 distrib_left) qed from fun_cong[OF dube_eq_2, OF assms, of 0] show ?thesis by (simp add: eq1 eq2 eq3 eq4 eq5) qed lemma dube_aux_1: assumes "(h, {}) \ set ps \ set qs" shows "poly_deg h < max (aa 1) (bb 1)" proof (rule ccontr) define z where "z = poly_deg h" assume "\ z < max (aa 1) (bb 1)" let ?S = "\A. {h. (h, {}) \ A \ poly_deg h = z}" have fin: "finite (?S A)" if "finite A" for A::"((('x \\<^sub>0 nat) \\<^sub>0 'a) \ 'x set) set" proof - have "(\t. (t, {})) ` ?S A \ A" by blast hence "finite ((\t. (t, {}::'x set)) ` ?S A)" using that by (rule finite_subset) moreover have "inj_on (\t. (t, {}::'x set)) (?S A)" by (rule inj_onI) simp ultimately show ?thesis by (rule finite_imageD) qed from finite_set have 1: "finite (?S (set ps))" by (rule fin) from finite_set have 2: "finite (?S (set qs))" by (rule fin) from \\ z < max (aa 1) (bb 1)\ have "aa 1 \ z" and "bb 1 \ z" by simp_all have "d \ aa 1" unfolding aa_Suc_n[symmetric] aa_def using fin_X by (rule \_decreasing) simp hence "d \ z" using \aa 1 \ z\ by (rule le_trans) hence eq: "int (z - d) = int z - int d" by simp from \d \ z\ have "Hilbert_fun (P[X]::(_ \\<^sub>0 'a) set) z = ((z - d) + (n - 1)) choose (n - 1) + Hilbert_fun P z + Hilbert_fun N z" by (rule Hilbert_fun_X) also have "int \ = ((int z - d + (n - 1)) gchoose (n - 1) + Hilbert_poly aa z + Hilbert_poly bb z) + (int (card (?S (set ps))) + int (card (?S (set qs))))" using X_not_empty valid_ps hom_ps cn_ps std_ps ext_ps \aa 1 \ z\ valid_qs hom_qs cn_qs std_qs ext_qs \bb 1 \ z\ by (simp add: Hilbert_fun_eq_Hilbert_poly_plus_card aa_def bb_def int_binomial eq) finally have "((int z - d + n - 1) gchoose (n - 1) + Hilbert_poly aa z + Hilbert_poly bb z) + (int (card (?S (set ps))) + int (card (?S (set qs)))) = int z + n - 1 gchoose (n - 1)" using fin_X X_not_empty by (simp add: Hilbert_fun_Polys int_binomial algebra_simps) also have "\ = (int z - d + n - 1) gchoose (n - 1) + Hilbert_poly aa z + Hilbert_poly bb z" by (fact dube_eq_0[THEN fun_cong]) finally have "int (card (?S (set ps))) + int (card (?S (set qs))) = 0" by simp hence "card (?S (set ps)) = 0" and "card (?S (set qs)) = 0" by simp_all with 1 2 have "?S (set ps \ set qs) = {}" by auto moreover from assms have "h \ ?S (set ps \ set qs)" by (simp add: z_def) ultimately have "h \ {}" by (rule subst) thus False by simp qed lemma shows aa_n: "aa n = d" and bb_n: "bb n = 0" and bb_0: "bb 0 \ max (aa 1) (bb 1)" proof - let ?j = "n - Suc 0" from n_gr_0 have "?j < n" and eq1: "Suc ?j = n" and eq2: "n - ?j = 1" by simp_all from this(1) have "(1::int) = (- 1)^(n - Suc ?j) * ((int d - 1) gchoose (n - Suc ?j)) + (- 1)^(n - ?j) * ((int d - 1) gchoose (n - ?j)) - 1 - (\i=Suc ?j..n. (- 1)^(i - ?j) * ((int (aa i) gchoose (i - ?j)) + (int (bb i) gchoose (i - ?j))))" by (rule dube_eq_3) hence eq: "aa n + bb n = d" by (simp add: eq1 eq2) hence "aa n \ d" by simp moreover have "d \ aa n" unfolding aa_Suc_n[symmetric] aa_def using fin_X by (rule \_decreasing) simp ultimately show "aa n = d" by (rule antisym) with eq show "bb n = 0" by simp have "bb 0 = \ qs 0" by (simp only: bb_def) also from fin_X have "\ \ max (aa 1) (bb 1)" (is "_ \ ?m") proof (rule \_le) from fin_X ext_qs have "\ qs = bb (Suc n)" by (simp add: \_card_X bb_def) also have "\ \ bb 1" unfolding bb_def using fin_X by (rule \_decreasing) simp also have "\ \ ?m" by (rule max.cobounded2) finally show "\ qs \ ?m" . next fix h U assume "(h, U) \ set qs" show "poly_deg h < ?m" proof (cases "card U = 0") case True from fin_X valid_qs \(h, U) \ set qs\ have "finite U" by (rule valid_decompD_finite) with True have "U = {}" by simp with \(h, U) \ set qs\ have "(h, {}) \ set ps \ set qs" by simp thus ?thesis by (rule dube_aux_1) next case False hence "1 \ card U" by simp with fin_X \(h, U) \ set qs\ have "poly_deg h < bb 1" unfolding bb_def by (rule \) also have "\ \ ?m" by (rule max.cobounded2) finally show ?thesis . qed qed finally show "bb 0 \ ?m" . qed lemma dube_eq_4: assumes "j < n" shows "(1::int) = 2 * (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) - 1 - (\i=Suc j..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" proof - from assms have "Suc j \ n" and "0 < n" and 1: "Suc (n - Suc j) = n - j" by simp_all have 2: "(- 1) ^ (n - Suc j) = - ((- (1::int)) ^ (n - j))" by (simp flip: 1) from assms have "(1::int) = (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - j) * ((int d - 1) gchoose (n - j)) - 1 - (\i=Suc j..n. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" by (rule dube_eq_3) also have "\ = (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - j) * ((int d - 1) gchoose (n - j)) - 1 - (- 1)^(n - j) * ((int (aa n) gchoose (n - j)) + (int (bb n) gchoose (n - j))) - (\i=Suc j..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" using \0 < n\ \Suc j \ n\ by (simp only: sum_tail_nat) also have "\ = (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - j) * (((int d - 1) gchoose (n - j)) - (int d gchoose (n - j))) - 1 - (\i=Suc j..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" using assms by (simp add: aa_n bb_n gbinomial_0_left right_diff_distrib) also have "(- 1)^(n - j) * (((int d - 1) gchoose (n - j)) - (int d gchoose (n - j))) = (- 1)^(n - Suc j) * (((int d - 1 + 1) gchoose (Suc (n - Suc j))) - ((int d - 1) gchoose (Suc (n - Suc j))))" by (simp add: 1 2 flip: mult_minus_right) also have "\ = (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j))" by (simp only: gbinomial_int_Suc_Suc, simp) finally show ?thesis by simp qed lemma cc_Suc: assumes "j < n - 1" shows "int (cc (Suc j)) = 2 + 2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) + (\i=j+2..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" proof - from assms have "j < n" and "Suc j \ n - 1" by simp_all hence "n - j = Suc (n - Suc j)" by simp hence eq: "(- 1) ^ (n - Suc j) = - ((- (1::int)) ^ (n - j))" by simp from \j < n\ have "(1::int) = 2 * (- 1)^(n - Suc j) * ((int d - 1) gchoose (n - Suc j)) - 1 - (\i=Suc j..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" by (rule dube_eq_4) also have "\ = cc (Suc j) - 2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) - 1 - (\i=j+2..n-1. (- 1)^(i - j) * ((int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))))" using \Suc j \ n - 1\ by (simp add: sum.atLeast_Suc_atMost eq) finally show ?thesis by simp qed lemma cc_n_minus_1: "cc (n - 1) = 2 * d" proof - let ?j = "n - 2" from n_gr_1 have 1: "Suc ?j = n - 1" and "?j < n - 1" and 2: "Suc (n - 1) = n" and 3: "n - (n - Suc 0) = Suc 0" and 4: "n - ?j = 2" by simp_all have "int (cc (n - 1)) = int (cc (Suc ?j))" by (simp only: 1) also from \?j < n - 1\ have "\ = 2 + 2 * (- 1) ^ (n - ?j) * (int d - 1 gchoose (n - Suc ?j)) + (\i = ?j+2..n-1. (- 1) ^ (i - ?j) * (int (aa i) gchoose (i - ?j) + (int (bb i) gchoose (i - ?j))))" by (rule cc_Suc) also have "\ = int (2 * d)" by (simp add: 1 2 3 4) finally show ?thesis by (simp only: int_int_eq) qed text \Since the case @{prop "n = 2"} is settled, we can concentrate on @{prop "2 < n"} now.\ context assumes n_gr_2: "2 < n" begin lemma cc_n_minus_2: "cc (n - 2) \ d\<^sup>2 + 2 * d" proof - let ?j = "n - 3" from n_gr_2 have 1: "Suc ?j = n - 2" and "?j < n - 1" and 2: "Suc (n - 2) = n - Suc 0" and 3: "n - (n - 2) = 2" and 4: "n - ?j = 3" by simp_all have "int (cc (n - 2)) = int (cc (Suc ?j))" by (simp only: 1) also from \?j < n - 1\ have "\ = 2 + 2 * (- 1) ^ (n - ?j) * (int d - 1 gchoose (n - Suc ?j)) + (\i = ?j+2..n-1. (- 1) ^ (i - ?j) * (int (aa i) gchoose (i - ?j) + (int (bb i) gchoose (i - ?j))))" by (rule cc_Suc) also have "\ = (2 - 2 * (int d - 1 gchoose 2)) + ((int (aa (n - 1)) gchoose 2) + (int (bb (n - 1)) gchoose 2))" by (simp add: 1 2 3 4) also have "\ \ (2 - 2 * (int d - 1 gchoose 2)) + (2 * int d gchoose 2)" proof (rule add_left_mono) have "int (aa (n - 1)) gchoose 2 + (int (bb (n - 1)) gchoose 2) \ int (aa (n - 1)) + int (bb (n - 1)) gchoose 2" by (rule gbinomial_int_plus_le) simp_all also have "\ = int (2 * d) gchoose 2" by (simp flip: cc_n_minus_1) also have "\ = 2 * int d gchoose 2" by (simp add: int_ops(7)) finally show "int (aa (n - 1)) gchoose 2 + (int (bb (n - 1)) gchoose 2) \ 2 * int d gchoose 2" . qed also have "\ = 2 - fact 2 * (int d - 1 gchoose 2) + (2 * int d gchoose 2)" by (simp only: fact_2) also have "\ = 2 - (int d - 1) * (int d - 2) + (2 * int d gchoose 2)" by (simp only: gbinomial_int_mult_fact) (simp add: numeral_2_eq_2 prod.atLeast0_lessThan_Suc) also have "\ = 2 - (int d - 1) * (int d - 2) + int d * (2 * int d - 1)" by (simp add: gbinomial_prod_rev numeral_2_eq_2 prod.atLeast0_lessThan_Suc) also have "\ = int (d\<^sup>2 + 2 * d)" by (simp add: power2_eq_square) (simp only: algebra_simps) finally show ?thesis by (simp only: int_int_eq) qed lemma cc_Suc_le: assumes "j < n - 3" shows "int (cc (Suc j)) \ 2 + (int (cc (j + 2)) gchoose 2) + (\i=j+4..n-1. int (cc i) gchoose (i - j))" \\Could be proved without coercing to @{typ int}, because everything is non-negative.\ proof - let ?f = "\i j. (int (aa i) gchoose (i - j)) + (int (bb i) gchoose (i - j))" let ?S = "\x y. (\i=j+x..n-y. (- 1)^(i - j) * ?f i j)" let ?S3 = "\x y. (\i=j+x..n-y. (int (cc i) gchoose (i - j)))" have ie1: "int (aa i) gchoose k + (int (bb i) gchoose k) \ int (cc i) gchoose k" if "0 < k" for i k proof - from that have "int (aa i) gchoose k + (int (bb i) gchoose k) \ int (aa i) + int (bb i) gchoose k" by (rule gbinomial_int_plus_le) simp_all also have "\ = int (cc i) gchoose k" by simp finally show ?thesis . qed from d_gr_0 have "0 \ int d - 1" by simp from assms have "0 < n - Suc j" by simp have f_nonneg: "0 \ ?f i j" for i by (simp add: gbinomial_int_nonneg) show ?thesis proof (cases "n = j + 4") case True hence j: "j = n - 4" by simp have 1: "n - Suc j = 3" and "j < n - 1" and 2: "Suc (n - 3) = Suc (Suc j)" and 3: "n - (n - 3) = 3" and 4: "n - j = 4" and 5: "n - Suc 0 = Suc (Suc (Suc j))" and 6: "n - 2 = Suc (Suc j)" by (simp_all add: True) from \j < n - 1\ have "int (cc (Suc j)) = 2 + 2 * (- 1) ^ (n - j) * (int d - 1 gchoose (n - Suc j)) + (\i = j+2..n-1. (- 1) ^ (i - j) * (int (aa i) gchoose (i - j) + (int (bb i) gchoose (i - j))))" by (rule cc_Suc) also have "\ = (2 + ((int (aa (n - 2)) gchoose 2) + (int (bb (n - 2)) gchoose 2))) + (2 * (int d - 1 gchoose 3) - ((int (aa (n - 1)) gchoose 3) + (int (bb (n - 1)) gchoose 3)))" by (simp add: 1 2 3 4 5 6) also have "\ \ (2 + ((int (aa (n - 2)) gchoose 2) + (int (bb (n - 2)) gchoose 2))) + 0" proof (rule add_left_mono) from cc_n_minus_1 have eq1: "int (aa (n - 1)) + int (bb (n - 1)) = 2 * int d" by simp hence ie2: "int (aa (n - 1)) \ 2 * int d" by simp from \0 \ int d - 1\ have "int d - 1 gchoose 3 \ int d gchoose 3" by (rule gbinomial_int_mono) simp hence "2 * (int d - 1 gchoose 3) \ 2 * (int d gchoose 3)" by simp also from _ ie2 have "\ \ int (aa (n - 1)) gchoose 3 + (2 * int d - int (aa (n - 1)) gchoose 3)" by (rule binomial_int_ineq_3) simp also have "\ = int (aa (n - 1)) gchoose 3 + (int (bb (n - 1)) gchoose 3)" by (simp flip: eq1) finally show "2 * (int d - 1 gchoose 3) - (int (aa (n - 1)) gchoose 3 + (int (bb (n - 1)) gchoose 3)) \ 0" by simp qed also have "\ = 2 + ((int (aa (n - 2)) gchoose 2) + (int (bb (n - 2)) gchoose 2))" by simp also from ie1 have "\ \ 2 + (int (cc (n - 2)) gchoose 2)" by (rule add_left_mono) simp also have "\ = 2 + (int (cc (j + 2)) gchoose 2) + ?S3 4 1" by (simp add: True) finally show ?thesis . next case False with assms have "j + 4 \ n - 1" by simp from n_gr_1 have "0 < n - 1" by simp from assms have "j + 2 \ n - 1" and "j + 2 \ n - 2" by simp_all hence "n - j = Suc (n - Suc j)" by simp hence 1: "(- 1) ^ (n - Suc j) = - ((- (1::int)) ^ (n - j))" by simp from assms have "j < n - 1" by simp hence "int (cc (Suc j)) = 2 + 2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) + ?S 2 1" by (rule cc_Suc) also have "\ = 2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - Suc j) * ((int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j))) + (2 + ?S 2 2)" using \0 < n - 1\ \j + 2 \ n - 1\ by (simp only: sum_tail_nat) (simp flip: numeral_2_eq_2) also have "\ \ (int (cc (n - 1)) gchoose (n - Suc j)) + (2 + ?S 2 2)" proof (rule add_right_mono) have rl: "x - y \ x" if "0 \ y" for x y :: int using that by simp have "2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - Suc j) * ((int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j))) = (-1)^(n - j) * (2 * ((int d - 1) gchoose (n - Suc j)) - (int (aa (n - 1)) gchoose (n - Suc j)) - (int (bb (n - 1)) gchoose (n - Suc j)))" by (simp only: 1 algebra_simps) also have "\ \ (int (cc (n - 1))) gchoose (n - Suc j)" proof (cases "even (n - j)") case True hence "(- 1) ^ (n - j) * (2 * (int d - 1 gchoose (n - Suc j)) - (int (aa (n - 1)) gchoose (n - Suc j)) - (int (bb (n - 1)) gchoose (n - Suc j))) = 2 * (int d - 1 gchoose (n - Suc j)) - ((int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j)))" by simp also have "\ \ 2 * (int d - 1 gchoose (n - Suc j))" by (rule rl) (simp add: gbinomial_int_nonneg) also have "\ = (int d - 1 gchoose (n - Suc j)) + (int d - 1 gchoose (n - Suc j))" by simp also have "\ \ (int d - 1) + (int d - 1) gchoose (n - Suc j)" using \0 < n - Suc j\ \0 \ int d - 1\ \0 \ int d - 1\ by (rule gbinomial_int_plus_le) also have "\ \ 2 * int d gchoose (n - Suc j)" proof (rule gbinomial_int_mono) from \0 \ int d - 1\ show "0 \ int d - 1 + (int d - 1)" by simp qed simp also have "\ = int (cc (n - 1)) gchoose (n - Suc j)" by (simp only: cc_n_minus_1) simp finally show ?thesis . next case False hence "(- 1) ^ (n - j) * (2 * (int d - 1 gchoose (n - Suc j)) - (int (aa (n - 1)) gchoose (n - Suc j)) - (int (bb (n - 1)) gchoose (n - Suc j))) = ((int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j))) - 2 * (int d - 1 gchoose (n - Suc j))" by simp also have "\ \ (int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j))" by (rule rl) (simp add: gbinomial_int_nonneg d_gr_0) also from \0 < n - Suc j\ have "\ \ int (cc (n - 1)) gchoose (n - Suc j)" by (rule ie1) finally show ?thesis . qed finally show "2 * (- 1)^(n - j) * ((int d - 1) gchoose (n - Suc j)) + (- 1)^(n - Suc j) * ((int (aa (n - 1)) gchoose (n - Suc j)) + (int (bb (n - 1)) gchoose (n - Suc j))) \ (int (cc (n - 1))) gchoose (n - Suc j)" . qed also have "\ = 2 + (int (cc (n - 1)) gchoose ((n - 1) - j)) + ((int (aa (j + 2)) gchoose 2) + (int (bb (j + 2)) gchoose 2)) + ?S 3 2" using \j + 2 \ n - 2\ by (simp add: sum.atLeast_Suc_atMost numeral_3_eq_3) also have "\ \ 2 + (int (cc (n - 1)) gchoose ((n - 1) - j)) + ((int (aa (j + 2)) gchoose 2) + (int (bb (j + 2)) gchoose 2)) + ?S3 4 2" proof (rule add_left_mono) from \j + 4 \ n - 1\ have "j + 3 \ n - 2" by simp hence "?S 3 2 = ?S 4 2 - ?f (j + 3) j" by (simp add: sum.atLeast_Suc_atMost add.commute) hence "?S 3 2 \ ?S 4 2" using f_nonneg[of "j + 3"] by simp also have "\ \ ?S3 4 2" proof (rule sum_mono) fix i assume "i \ {j + 4..n - 2}" hence "0 < i - j" by simp from f_nonneg[of i] have "(- 1)^(i - j) * ?f i j \ ?f i j" by (smt minus_one_mult_self mult_cancel_right1 pos_zmult_eq_1_iff_lemma zero_less_mult_iff) also from \0 < i - j\ have "\ \ int (cc i) gchoose (i - j)" by (rule ie1) finally show "(- 1)^(i - j) * ?f i j \ int (cc i) gchoose (i - j)" . qed finally show "?S 3 2 \ ?S3 4 2" . qed also have "\ = ((int (aa (j + 2)) gchoose 2) + (int (bb (j + 2)) gchoose 2)) + (2 + ?S3 4 1)" using \0 < n - 1\ \j + 4 \ n - 1\ by (simp only: sum_tail_nat) (simp flip: numeral_2_eq_2) also from ie1 have "\ \ int (cc (j + 2)) gchoose 2 + (2 + ?S3 4 1)" by (rule add_right_mono) simp also have "\ = 2 + (int (cc (j + 2)) gchoose 2) + ?S3 4 1" by (simp only: ac_simps) finally show ?thesis . qed qed corollary cc_le: assumes "0 < j" and "j < n - 2" shows "cc j \ 2 + (cc (j + 1) choose 2) + (\i=j+3..n-1. cc i choose (Suc (i - j)))" proof - define j0 where "j0 = j - 1" with assms have j: "j = Suc j0" and "j0 < n - 3" by simp_all have "int (cc j) = int (cc (Suc j0))" by (simp only: j) also have "\ \ 2 + (int (cc (j0 + 2)) gchoose 2) + (\i=j0+4..n-1. int (cc i) gchoose (i - j0))" using \j0 < n - 3\ by (rule cc_Suc_le) also have "\ = 2 + (int (cc (j + 1)) gchoose 2) + (\i=j0+4..n-1. int (cc i) gchoose (i - j0))" by (simp add: j) also have "(\i=j0+4..n-1. int (cc i) gchoose (i - j0)) = int (\i=j+3..n-1. cc i choose (Suc (i - j)))" unfolding int_sum proof (rule sum.cong) fix i assume "i \ {j + 3..n - 1}" hence "Suc j0 < i" by (simp add: j) hence "i - j0 = Suc (i - j)" by (simp add: j) thus "int (cc i) gchoose (i - j0) = int (cc i choose (Suc (i - j)))" by (simp add: int_binomial) qed (simp add: j) finally have "int (cc j) \ int (2 + (cc (j + 1) choose 2) + (\i = j + 3..n - 1. cc i choose (Suc (i - j))))" by (simp only: int_plus int_binomial) thus ?thesis by (simp only: zle_int) qed corollary cc_le_Dube_aux: "0 < j \ j + 1 \ n \ cc j \ Dube_aux n d j" proof (induct j rule: Dube_aux.induct[where n=n]) case step: (1 j) from step.prems(2) have "j + 2 < n \ j + 2 = n \ j + 1 = n" by auto thus ?case proof (elim disjE) assume *: "j + 2 < n" moreover have "0 < j + 1" by simp moreover from * have "j + 1 + 1 \ n" by simp ultimately have "cc (j + 1) \ Dube_aux n d (j + 1)" by (rule step.hyps) hence 1: "cc (j + 1) choose 2 \ Dube_aux n d (j + 1) choose 2" by (rule Binomial_Int.binomial_mono) have 2: "(\i = j + 3..n - 1. cc i choose Suc (i - j)) \ (\i = j + 3..n - 1. Dube_aux n d i choose Suc (i - j))" proof (rule sum_mono) fix i::nat note * moreover assume "i \ {j + 3..n - 1}" moreover from this \2 < n\ have "0 < i" and "i + 1 \ n" by auto ultimately have "cc i \ Dube_aux n d i" by (rule step.hyps) thus "cc i choose Suc (i - j) \ Dube_aux n d i choose Suc (i - j)" by (rule Binomial_Int.binomial_mono) qed from * have "j < n - 2" by simp with step.prems(1) have "cc j \ 2 + (cc (j + 1) choose 2) + (\i = j + 3..n - 1. cc i choose Suc (i - j))" by (rule cc_le) also from * 1 2 have "\ \ Dube_aux n d j" by simp finally show ?thesis . next assume "j + 2 = n" hence "j = n - 2" and "Dube_aux n d j = d\<^sup>2 + 2 * d" by simp_all thus ?thesis by (simp only: cc_n_minus_2) next assume "j + 1 = n" hence "j = n - 1" and "Dube_aux n d j = 2 * d" by simp_all thus ?thesis by (simp only: cc_n_minus_1) qed qed end lemma Dube_aux: assumes "g \ punit.reduced_GB F" shows "poly_deg g \ Dube_aux n d 1" proof (cases "n = 2") case True from assms have "poly_deg g \ bb 0" by (rule deg_RGB) also have "\ \ max (aa 1) (bb 1)" by (fact bb_0) also have "\ \ cc (n - 1)" by (simp add: True) also have "\ = 2 * d" by (fact cc_n_minus_1) also have "\ = Dube_aux n d 1" by (simp add: True) finally show ?thesis . next case False with \1 < n\ have "2 < n" and "1 + 1 \ n" by simp_all from assms have "poly_deg g \ bb 0" by (rule deg_RGB) also have "\ \ max (aa 1) (bb 1)" by (fact bb_0) also have "\ \ cc 1" by simp also from \2 < n\ _ \1 + 1 \ n\ have "\ \ Dube_aux n d 1" by (rule cc_le_Dube_aux) simp finally show ?thesis . qed end theorem Dube: assumes "finite F" and "F \ P[X]" and "\f. f \ F \ homogeneous f" and "g \ punit.reduced_GB F" shows "poly_deg g \ Dube (card X) (maxdeg F)" proof (cases "F \ {0}") case True hence "F = {} \ F = {0}" by blast with assms(4) show ?thesis by (auto simp: punit.reduced_GB_empty punit.reduced_GB_singleton) next case False hence "F - {0} \ {}" by simp hence "F \ {}" by blast hence "poly_deg ` F \ {}" by simp from assms(1) have fin1: "finite (poly_deg ` F)" by (rule finite_imageI) from assms(1) have "finite (F - {0})" by simp hence fin: "finite (poly_deg ` (F - {0}))" by (rule finite_imageI) moreover from \F - {0} \ {}\ have *: "poly_deg ` (F - {0}) \ {}" by simp ultimately have "maxdeg (F - {0}) \ poly_deg ` (F - {0})" unfolding maxdeg_def by (rule Max_in) then obtain f where "f \ F - {0}" and md1: "maxdeg (F - {0}) = poly_deg f" .. note this(2) moreover have "maxdeg (F - {0}) \ maxdeg F" unfolding maxdeg_def using image_mono * fin1 by (rule Max_mono) blast ultimately have "poly_deg f \ maxdeg F" by simp from \f \ F - {0}\ have "f \ F" and "f \ 0" by simp_all from this(1) assms(2) have "f \ P[X]" .. have f_max: "poly_deg f' \ poly_deg f" if "f' \ F" for f' proof (cases "f' = 0") case True thus ?thesis by simp next case False with that have "f' \ F - {0}" by simp hence "poly_deg f' \ poly_deg ` (F - {0})" by (rule imageI) with fin show "poly_deg f' \ poly_deg f" unfolding md1[symmetric] maxdeg_def by (rule Max_ge) qed have "maxdeg F \ poly_deg f" unfolding maxdeg_def using fin1 \poly_deg ` F \ {}\ proof (rule Max.boundedI) fix d assume "d \ poly_deg ` F" then obtain f' where "f' \ F" and "d = poly_deg f'" .. note this(2) also from \f' \ F\ have "poly_deg f' \ poly_deg f" by (rule f_max) finally show "d \ poly_deg f" . qed with \poly_deg f \ maxdeg F\ have md: "poly_deg f = maxdeg F" by (rule antisym) show ?thesis proof (cases "ideal {f} = ideal F") case True note assms(4) also have "punit.reduced_GB F = punit.reduced_GB {f}" using punit.finite_reduced_GB_finite punit.reduced_GB_is_reduced_GB_finite by (rule punit.reduced_GB_unique) (simp_all add: punit.reduced_GB_pmdl_finite[simplified] True) also have "\ \ {punit.monic f}" by (simp add: punit.reduced_GB_singleton) finally have "g \ {punit.monic f}" . hence "poly_deg g = poly_deg (punit.monic f)" by simp also from poly_deg_monom_mult_le[where c="1 / lcf f" and t=0 and p=f] have "\ \ poly_deg f" by (simp add: punit.monic_def) also have "\ = maxdeg F" by (fact md) also have "\ \ Dube (card X) (maxdeg F)" by (fact Dube_ge_d) finally show ?thesis . next case False show ?thesis proof (cases "poly_deg f = 0") case True hence "monomial (lookup f 0) 0 = f" by (rule poly_deg_zero_imp_monomial) moreover define c where "c = lookup f 0" ultimately have f: "f = monomial c 0" by simp with \f \ 0\ have "c \ 0" by (simp add: monomial_0_iff) from \f \ F\ have "f \ ideal F" by (rule ideal.span_base) hence "punit.monom_mult (1 / c) 0 f \ ideal F" by (rule punit.pmdl_closed_monom_mult[simplified]) with \c \ 0\ have "ideal F = UNIV" by (simp add: f punit.monom_mult_monomial ideal_eq_UNIV_iff_contains_one) with assms(1) have "punit.reduced_GB F = {1}" by (simp only: ideal_eq_UNIV_iff_reduced_GB_eq_one_finite) with assms(4) show ?thesis by simp next case False hence "0 < poly_deg f" by simp have "card X \ 1 \ 1 < card X" by auto thus ?thesis proof note fin_X moreover assume "card X \ 1" moreover note assms(2) moreover from \f \ F\ have "f \ ideal F" by (rule ideal.span_base) ultimately have "poly_deg g \ poly_deg f" using \f \ 0\ assms(4) by (rule deg_reduced_GB_univariate_le) also have "\ \ Dube (card X) (maxdeg F)" unfolding md by (fact Dube_ge_d) finally show ?thesis . next assume "1 < card X" hence "poly_deg g \ Dube_aux (card X) (poly_deg f) 1" using assms(1, 2) \f \ F\ assms(3) f_max \0 < poly_deg f\ \ideal {f} \ ideal F\ assms(4) by (rule Dube_aux) also from \1 < card X\ \0 < poly_deg f\ have "\ = Dube (card X) (maxdeg F)" by (simp add: Dube_def md) finally show ?thesis . qed qed qed qed corollary Dube_is_hom_GB_bound: "finite F \ F \ P[X] \ is_hom_GB_bound F (Dube (card X) (maxdeg F))" by (intro is_hom_GB_boundI Dube) end corollary Dube_indets: assumes "finite F" and "\f. f \ F \ homogeneous f" and "g \ punit.reduced_GB F" - shows "poly_deg g \ Dube (card (UNION F indets)) (maxdeg F)" + shows "poly_deg g \ Dube (card (\(indets ` F))) (maxdeg F)" using _ assms(1) _ assms(2, 3) proof (rule Dube) - from assms show "finite (UNION F indets)" by (simp add: finite_indets) + from assms show "finite (\(indets ` F))" by (simp add: finite_indets) next - show "F \ P[UNION F indets]" by (auto simp: Polys_alt) + show "F \ P[\(indets ` F)]" by (auto simp: Polys_alt) qed corollary Dube_is_hom_GB_bound_indets: - "finite F \ is_hom_GB_bound F (Dube (card (UNION F indets)) (maxdeg F))" + "finite F \ is_hom_GB_bound F (Dube (card (\(indets ` F))) (maxdeg F))" by (intro is_hom_GB_boundI Dube_indets) end (* pm_powerprod *) hide_const (open) pm_powerprod.\ pm_powerprod.\ context extended_ord_pm_powerprod begin lemma Dube_is_GB_cofactor_bound: assumes "finite X" and "finite F" and "F \ P[X]" shows "is_GB_cofactor_bound F (Dube (Suc (card X)) (maxdeg F))" using assms(1, 3) proof (rule hom_GB_bound_is_GB_cofactor_bound) let ?F = "homogenize None ` extend_indets ` F" let ?X = "insert None (Some ` X)" from assms(1) have "finite ?X" by simp moreover from assms(2) have "finite ?F" by (intro finite_imageI) moreover have "?F \ P[?X]" proof fix f' assume "f' \ ?F" then obtain f where "f \ F" and f': "f' = homogenize None (extend_indets f)" by blast from this(1) assms(3) have "f \ P[X]" .. hence "extend_indets f \ P[Some ` X]" by (auto simp: Polys_alt indets_extend_indets) thus "f' \ P[?X]" unfolding f' by (rule homogenize_in_Polys) qed ultimately have "extended_ord.is_hom_GB_bound ?F (Dube (card ?X) (maxdeg ?F))" by (rule extended_ord.Dube_is_hom_GB_bound) moreover have "maxdeg ?F = maxdeg F" proof - have "maxdeg ?F = maxdeg (extend_indets ` F)" by (auto simp: indets_extend_indets intro: maxdeg_homogenize) also have "\ = maxdeg F" by (simp add: maxdeg_def image_image) finally show "maxdeg ?F = maxdeg F" . qed moreover from assms(1) have "card ?X = card X + 1" by (simp add: card_image) ultimately show "extended_ord.is_hom_GB_bound ?F (Dube (Suc (card X)) (maxdeg F))" by simp qed lemma Dube_is_GB_cofactor_bound_explicit: assumes "finite X" and "finite F" and "F \ P[X]" obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[X]" and "\g. g \ G \ \q. g = (\f\F. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ Dube (Suc (card X)) (maxdeg F) \ (f \ F \ q f = 0))" proof - from assms have "is_GB_cofactor_bound F (Dube (Suc (card X)) (maxdeg F))" (is "is_GB_cofactor_bound _ ?b") by (rule Dube_is_GB_cofactor_bound) moreover note assms(3) ultimately obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G \ P[X]" and 1: "\g. g \ G \ \F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ ?b \ (f \ F' \ q f = 0))" by (rule is_GB_cofactor_boundE_Polys) blast from this(1-3) show ?thesis proof fix g assume "g \ G" hence "\F' q. finite F' \ F' \ F \ g = (\f\F'. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ ?b \ (f \ F' \ q f = 0))" by (rule 1) then obtain F' q where "F' \ F" and g: "g = (\f\F'. q f * f)" and "\f. q f \ P[X]" and "\f. poly_deg (q f * f) \ ?b" and 2: "\f. f \ F' \ q f = 0" by blast show "\q. g = (\f\F. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ ?b \ (f \ F \ q f = 0))" proof (intro exI allI conjI impI) from assms(2) \F' \ F\ have "(\f\F'. q f * f) = (\f\F. q f * f)" proof (intro sum.mono_neutral_left ballI) fix f assume "f \ F - F'" hence "f \ F'" by simp hence "q f = 0" by (rule 2) thus "q f * f = 0" by simp qed thus "g = (\f\F. q f * f)" by (simp only: g) next fix f assume "f \ F" with \F' \ F\ have "f \ F'" by blast thus "q f = 0" by (rule 2) qed fact+ qed qed corollary Dube_is_GB_cofactor_bound_indets: assumes "finite F" - shows "is_GB_cofactor_bound F (Dube (Suc (card (UNION F indets))) (maxdeg F))" + shows "is_GB_cofactor_bound F (Dube (Suc (card (\(indets ` F)))) (maxdeg F))" using _ assms _ proof (rule Dube_is_GB_cofactor_bound) - from assms show "finite (UNION F indets)" by (simp add: finite_indets) + from assms show "finite (\(indets ` F))" by (simp add: finite_indets) next - show "F \ P[UNION F indets]" by (auto simp: Polys_alt) + show "F \ P[\(indets ` F)]" by (auto simp: Polys_alt) qed end (* extended_ord_pm_powerprod *) end (* theory *) diff --git a/thys/Groebner_Macaulay/Groebner_Macaulay.thy b/thys/Groebner_Macaulay/Groebner_Macaulay.thy --- a/thys/Groebner_Macaulay/Groebner_Macaulay.thy +++ b/thys/Groebner_Macaulay/Groebner_Macaulay.thy @@ -1,212 +1,212 @@ (* Author: Alexander Maletzky *) section \Computing Gr\"obner Bases by Triangularizing Macaulay Matrices\ theory Groebner_Macaulay imports Groebner_Bases.Macaulay_Matrix Groebner_Bases.Groebner_PM Degree_Section Degree_Bound_Utils begin text \Relationship between Gr\"obner bases and Macaulay matrices, following @{cite "Wiesinger-Widi2015"}.\ subsection \Gr\"obner Bases\ lemma (in gd_term) Macaulay_list_is_GB: assumes "is_Groebner_basis G" and "pmdl (set ps) = pmdl G" and "G \ phull (set ps)" shows "is_Groebner_basis (set (Macaulay_list ps))" proof (simp only: GB_alt_3_finite[OF finite_set] pmdl_Macaulay_list, intro ballI impI) fix f assume "f \ pmdl (set ps)" also from assms(2) have "\ = pmdl G" . finally have "f \ pmdl G" . assume "f \ 0" with assms(1) \f \ pmdl G\ obtain g where "g \ G" and "g \ 0" and "lt g adds\<^sub>t lt f" by (rule GB_adds_lt) from assms(3) \g \ G\ have "g \ phull (set ps)" .. from this \g \ 0\ obtain g' where "g' \ set (Macaulay_list ps)" and "g' \ 0" and "lt g = lt g'" by (rule Macaulay_list_lt) show "\g\set (Macaulay_list ps). g \ 0 \ lt g adds\<^sub>t lt f" proof (rule, rule) from \lt g adds\<^sub>t lt f\ show "lt g' adds\<^sub>t lt f" by (simp only: \lt g = lt g'\) qed fact+ qed subsection \Bounds\ context pm_powerprod begin context fixes X :: "'x set" assumes fin_X: "finite X" begin definition deg_shifts :: "nat \ (('x \\<^sub>0 nat) \\<^sub>0 'b) list \ (('x \\<^sub>0 nat) \\<^sub>0 'b::semiring_1) list" where "deg_shifts d fs = concat (map (\f. (map (\t. punit.monom_mult 1 t f) (punit.pps_to_list (deg_le_sect X (d - poly_deg f))))) fs)" lemma set_deg_shifts: "set (deg_shifts d fs) = (\f\set fs. (\t. punit.monom_mult 1 t f) ` (deg_le_sect X (d - poly_deg f)))" proof - from fin_X have "finite (deg_le_sect X d0)" for d0 by (rule finite_deg_le_sect) thus ?thesis by (simp add: deg_shifts_def punit.set_pps_to_list) qed corollary set_deg_shifts_singleton: "set (deg_shifts d [f]) = (\t. punit.monom_mult 1 t f) ` (deg_le_sect X (d - poly_deg f))" by (simp add: set_deg_shifts) lemma deg_shifts_superset: "set fs \ set (deg_shifts d fs)" proof - have "set fs = (\f\set fs. {punit.monom_mult 1 0 f})" by simp also have "\ \ set (deg_shifts d fs)" unfolding set_deg_shifts using subset_refl proof (rule UN_mono) fix f assume "f \ set fs" have "punit.monom_mult 1 0 f \ (\t. punit.monom_mult 1 t f) ` deg_le_sect X (d - poly_deg f)" using zero_in_deg_le_sect by (rule imageI) thus "{punit.monom_mult 1 0 f} \ (\t. punit.monom_mult 1 t f) ` deg_le_sect X (d - poly_deg f)" by simp qed finally show ?thesis . qed lemma deg_shifts_mono: assumes "set fs \ set gs" shows "set (deg_shifts d fs) \ set (deg_shifts d gs)" using assms by (auto simp add: set_deg_shifts) lemma ideal_deg_shifts [simp]: "ideal (set (deg_shifts d fs)) = ideal (set fs)" proof show "ideal (set (deg_shifts d fs)) \ ideal (set fs)" by (rule ideal.span_subset_spanI, simp add: set_deg_shifts UN_subset_iff, intro ballI image_subsetI) (metis ideal.span_scale times_monomial_left ideal.span_base) next from deg_shifts_superset show "ideal (set fs) \ ideal (set (deg_shifts d fs))" by (rule ideal.span_mono) qed lemma thm_2_3_6: assumes "set fs \ P[X]" and "is_GB_cofactor_bound (set fs) b" shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts b fs)))" proof - from assms(2) finite_set assms(1) obtain G where "punit.is_Groebner_basis G" and ideal_G: "ideal G = ideal (set fs)" and G_sub: "G \ P[X]" and 1: "\g. g \ G \ \q. g = (\f\set fs. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b)" by (rule is_GB_cofactor_boundE_finite_Polys) blast from this(1) show ?thesis proof (rule punit.Macaulay_list_is_GB) show "G \ phull (set (deg_shifts b fs))" (is "_ \ ?H") proof fix g assume "g \ G" hence "\q. g = (\f\set fs. q f * f) \ (\f. q f \ P[X] \ poly_deg (q f * f) \ b)" by (rule 1) then obtain q where g: "g = (\f\set fs. q f * f)" and "\f. q f \ P[X]" and "\f. poly_deg (q f * f) \ b" by blast show "g \ ?H" unfolding g proof (rule phull.span_sum) fix f assume "f \ set fs" have "1 \ (0::'a)" by simp show "q f * f \ ?H" proof (cases "f = 0 \ q f = 0") case True thus ?thesis by (auto simp add: phull.span_zero) next case False hence "q f \ 0" and "f \ 0" by simp_all with \poly_deg (q f * f) \ b\ have "poly_deg (q f) \ b - poly_deg f" by (simp add: poly_deg_times) with \q f \ P[X]\ have "keys (q f) \ deg_le_sect X (b - poly_deg f)" by (rule keys_subset_deg_le_sectI) with finite_deg_le_sect[OF fin_X] have "q f * f = (\t\deg_le_sect X (b - poly_deg f). punit.monom_mult (lookup (q f) t) t f)" unfolding punit.mult_scalar_sum_monomials[simplified] by (rule sum.mono_neutral_left) (simp add: in_keys_iff) also have "\ = (\t\deg_le_sect X (b - poly_deg f). (lookup (q f) t) \ (punit.monom_mult 1 t f))" by (simp add: punit.monom_mult_assoc punit.map_scale_eq_monom_mult) also have "\ = (\t\deg_le_sect X (b - poly_deg f). ((\f0. (lookup (q f) (punit.lp f0 - punit.lp f)) \ f0) \ (\t. punit.monom_mult 1 t f)) t)" using refl by (rule sum.cong) (simp add: punit.lt_monom_mult[OF \1 \ 0\ \f \ 0\]) also have "\ = (\f0\set (deg_shifts b [f]). (lookup (q f) (punit.lp f0 - punit.lp f)) \ f0)" unfolding set_deg_shifts_singleton proof (intro sum.reindex[symmetric] inj_onI) fix s t assume "punit.monom_mult 1 s f = punit.monom_mult 1 t f" thus "s = t" using \1 \ 0\ \f \ 0\ by (rule punit.monom_mult_inj_2) qed finally have "q f * f \ phull (set (deg_shifts b [f]))" by (simp add: phull.sum_in_spanI) also have "\ \ ?H" by (rule phull.span_mono, rule deg_shifts_mono, simp add: \f \ set fs\) finally show ?thesis . qed qed qed qed (simp add: ideal_G) qed lemma thm_2_3_7: assumes "set fs \ P[X]" and "is_GB_cofactor_bound (set fs) b" shows "1 \ ideal (set fs) \ 1 \ set (punit.Macaulay_list (deg_shifts b fs))" (is "?L \ ?R") proof assume ?L let ?G = "set (punit.Macaulay_list (deg_shifts b fs))" from assms have "punit.is_Groebner_basis ?G" by (rule thm_2_3_6) moreover from \?L\ have "1 \ ideal ?G" by (simp add: punit.pmdl_Macaulay_list[simplified]) moreover have "1 \ (0::_ \\<^sub>0 'a)" by simp ultimately obtain g where "g \ ?G" and "g \ 0" and "punit.lt g adds punit.lt (1::_ \\<^sub>0 'a)" by (rule punit.GB_adds_lt[simplified]) from this(3) have lp_g: "punit.lt g = 0" by (simp add: punit.lt_monomial adds_zero flip: single_one) from punit.Macaulay_list_is_monic_set \g \ ?G\ \g \ 0\ have lc_g: "punit.lc g = 1" by (rule punit.is_monic_setD) have "g = 1" proof (rule poly_mapping_eqI) fix t show "lookup g t = lookup 1 t" proof (cases "t = 0") case True thus ?thesis using lc_g by (simp add: lookup_one punit.lc_def lp_g) next case False with zero_min[of t] have "\ t \ punit.lt g" by (simp add: lp_g) with punit.lt_max_keys have "t \ keys g" by blast with False show ?thesis by (simp add: lookup_one in_keys_iff) qed qed with \g \ ?G\ show "1 \ ?G" by simp next assume ?R also have "\ \ phull (set (punit.Macaulay_list (deg_shifts b fs)))" by (rule phull.span_superset) also have "\ = phull (set (deg_shifts b fs))" by (fact punit.phull_Macaulay_list) also have "\ \ ideal (set (deg_shifts b fs))" using punit.phull_subset_module by force finally show ?L by simp qed end lemma thm_2_3_6_indets: assumes "is_GB_cofactor_bound (set fs) b" - shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts (UNION (set fs) indets) b fs)))" + shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts (\(indets ` (set fs))) b fs)))" using _ _ assms proof (rule thm_2_3_6) - from finite_set show "finite (UNION (set fs) indets)" by (simp add: finite_indets) + from finite_set show "finite (\(indets ` (set fs)))" by (simp add: finite_indets) next - show "set fs \ P[UNION (set fs) indets]" by (auto simp: Polys_alt) + show "set fs \ P[\(indets ` (set fs))]" by (auto simp: Polys_alt) qed lemma thm_2_3_7_indets: assumes "is_GB_cofactor_bound (set fs) b" - shows "1 \ ideal (set fs) \ 1 \ set (punit.Macaulay_list (deg_shifts (UNION (set fs) indets) b fs))" + shows "1 \ ideal (set fs) \ 1 \ set (punit.Macaulay_list (deg_shifts (\(indets ` (set fs))) b fs))" using _ _ assms proof (rule thm_2_3_7) - from finite_set show "finite (UNION (set fs) indets)" by (simp add: finite_indets) + from finite_set show "finite (\(indets ` (set fs)))" by (simp add: finite_indets) next - show "set fs \ P[UNION (set fs) indets]" by (auto simp: Polys_alt) + show "set fs \ P[\(indets ` (set fs))]" by (auto simp: Polys_alt) qed end (* pm_powerprod *) end (* theory *) diff --git a/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy b/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy --- a/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy +++ b/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy @@ -1,652 +1,652 @@ (* Author: Alexander Maletzky *) section \Sample Computations of Gr\"obner Bases via Macaulay Matrices\ theory Groebner_Macaulay_Examples imports Groebner_Macaulay Dube_Bound Groebner_Bases.Benchmarks Jordan_Normal_Form.Gauss_Jordan_IArray_Impl Groebner_Bases.Code_Target_Rat begin subsection \Combining @{theory Groebner_Macaulay.Groebner_Macaulay} and @{theory Groebner_Macaulay.Dube_Bound}\ context extended_ord_pm_powerprod begin theorem thm_2_3_6_Dube: assumes "finite X" and "set fs \ P[X]" shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts X (Dube (Suc (card X)) (maxdeg (set fs))) fs)))" using assms Dube_is_GB_cofactor_bound by (rule thm_2_3_6) (simp_all add: assms) theorem thm_2_3_7_Dube: assumes "finite X" and "set fs \ P[X]" shows "1 \ ideal (set fs) \ 1 \ set (punit.Macaulay_list (deg_shifts X (Dube (Suc (card X)) (maxdeg (set fs))) fs))" using assms Dube_is_GB_cofactor_bound by (rule thm_2_3_7) (simp_all add: assms) theorem thm_2_3_6_indets_Dube: fixes fs - defines "X \ UNION (set fs) indets" + defines "X \ \(indets ` set fs)" shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts X (Dube (Suc (card X)) (maxdeg (set fs))) fs)))" unfolding X_def using Dube_is_GB_cofactor_bound_indets by (rule thm_2_3_6_indets) (fact finite_set) theorem thm_2_3_7_indets_Dube: fixes fs - defines "X \ UNION (set fs) indets" + defines "X \ \(indets ` set fs)" shows "1 \ ideal (set fs) \ 1 \ set (punit.Macaulay_list (deg_shifts X (Dube (Suc (card X)) (maxdeg (set fs))) fs))" unfolding X_def using Dube_is_GB_cofactor_bound_indets by (rule thm_2_3_7_indets) (fact finite_set) end (* extended_ord_pm_powerprod *) subsection \Preparations\ (* This is exactly the same as in "Groebner_Bases.F4_Examples". Pull out into common ancestor? *) primrec remdups_wrt_rev :: "('a \ 'b) \ 'a list \ 'b list \ 'a list" where "remdups_wrt_rev f [] vs = []" | "remdups_wrt_rev f (x # xs) vs = (let fx = f x in if List.member vs fx then remdups_wrt_rev f xs vs else x # (remdups_wrt_rev f xs (fx # vs)))" lemma remdups_wrt_rev_notin: "v \ set vs \ v \ f ` set (remdups_wrt_rev f xs vs)" proof (induct xs arbitrary: vs) case Nil show ?case by simp next case (Cons x xs) from Cons(2) have 1: "v \ f ` set (remdups_wrt_rev f xs vs)" by (rule Cons(1)) from Cons(2) have "v \ set (f x # vs)" by simp hence 2: "v \ f ` set (remdups_wrt_rev f xs (f x # vs))" by (rule Cons(1)) from Cons(2) show ?case by (auto simp: Let_def 1 2 List.member_def) qed lemma distinct_remdups_wrt_rev: "distinct (map f (remdups_wrt_rev f xs vs))" proof (induct xs arbitrary: vs) case Nil show ?case by simp next case (Cons x xs) show ?case by (simp add: Let_def Cons(1) remdups_wrt_rev_notin) qed lemma map_of_remdups_wrt_rev': "map_of (remdups_wrt_rev fst xs vs) k = map_of (filter (\x. fst x \ set vs) xs) k" proof (induct xs arbitrary: vs) case Nil show ?case by simp next case (Cons x xs) show ?case proof (simp add: Let_def List.member_def Cons, intro impI) assume "k \ fst x" have "map_of (filter (\y. fst y \ fst x \ fst y \ set vs) xs) = map_of (filter (\y. fst y \ fst x) (filter (\y. fst y \ set vs) xs))" by (simp only: filter_filter conj_commute) also have "... = map_of (filter (\y. fst y \ set vs) xs) |` {y. y \ fst x}" by (rule map_of_filter) finally show "map_of (filter (\y. fst y \ fst x \ fst y \ set vs) xs) k = map_of (filter (\y. fst y \ set vs) xs) k" by (simp add: restrict_map_def \k \ fst x\) qed qed corollary map_of_remdups_wrt_rev: "map_of (remdups_wrt_rev fst xs []) = map_of xs" by (rule ext, simp add: map_of_remdups_wrt_rev') lemma (in term_powerprod) compute_list_to_poly [code]: "list_to_poly ts cs = distr\<^sub>0 DRLEX (remdups_wrt_rev fst (zip ts cs) [])" by (rule poly_mapping_eqI, simp add: lookup_list_to_poly list_to_fun_def distr\<^sub>0_def oalist_of_list_ntm_def oa_ntm.lookup_oalist_of_list distinct_remdups_wrt_rev lookup_dflt_def map_of_remdups_wrt_rev) lemma (in ordered_term) compute_Macaulay_list [code]: "Macaulay_list ps = (let ts = Keys_to_list ps in filter (\p. p \ 0) (mat_to_polys ts (row_echelon (polys_to_mat ts ps))) )" by (simp add: Macaulay_list_def Macaulay_mat_def Let_def) declare conversep_iff [code] derive (eq) ceq poly_mapping derive (no) ccompare poly_mapping derive (dlist) set_impl poly_mapping derive (no) cenum poly_mapping derive (eq) ceq rat derive (no) ccompare rat derive (dlist) set_impl rat derive (no) cenum rat subsubsection \Connection between @{typ "('x \\<^sub>0 'a) \\<^sub>0 'b"} and @{typ "('x, 'a) pp \\<^sub>0 'b"}\ (* Move into "Polynomials.PP_Type"? *) definition keys_pp_to_list :: "('x::linorder, 'a::zero) pp \ 'x list" where "keys_pp_to_list t = sorted_list_of_set (keys_pp t)" lemma inj_PP: "inj PP" by (simp add: PP_inject inj_def) lemma inj_mapping_of: "inj mapping_of" by (simp add: mapping_of_inject inj_def) lemma mapping_of_comp_PP [simp]: "mapping_of \ PP = (\x. x)" "PP \ mapping_of = (\x. x)" by (simp_all add: comp_def PP_inverse mapping_of_inverse) lemma map_key_PP_mapping_of [simp]: "Poly_Mapping.map_key PP (Poly_Mapping.map_key mapping_of p) = p" by (simp add: map_key_compose[OF inj_PP inj_mapping_of] comp_def PP_inverse map_key_id) lemma map_key_mapping_of_PP [simp]: "Poly_Mapping.map_key mapping_of (Poly_Mapping.map_key PP p) = p" by (simp add: map_key_compose[OF inj_mapping_of inj_PP] comp_def mapping_of_inverse map_key_id) lemmas map_key_PP_plus = map_key_plus[OF inj_PP] lemmas map_key_PP_zero [simp] = map_key_zero[OF inj_PP] lemma lookup_map_key_PP: "lookup (Poly_Mapping.map_key PP p) t = lookup p (PP t)" by (simp add: map_key.rep_eq inj_PP) lemma keys_map_key_PP: "keys (Poly_Mapping.map_key PP p) = mapping_of ` keys p" by (simp add: keys_map_key inj_PP) (smt Collect_cong PP_inverse UNIV_I image_def pp.mapping_of_inverse vimage_def) lemma map_key_PP_zero_iff [iff]: "Poly_Mapping.map_key PP p = 0 \ p = 0" by (metis map_key_PP_zero map_key_mapping_of_PP) lemma map_key_PP_uminus [simp]: "Poly_Mapping.map_key PP (- p) = - Poly_Mapping.map_key PP p" by (rule poly_mapping_eqI) (simp add: lookup_map_key_PP) lemma map_key_PP_minus: "Poly_Mapping.map_key PP (p - q) = Poly_Mapping.map_key PP p - Poly_Mapping.map_key PP q" by (rule poly_mapping_eqI) (simp add: lookup_map_key_PP lookup_minus) lemma map_key_PP_monomial [simp]: "Poly_Mapping.map_key PP (monomial c t) = monomial c (mapping_of t)" proof - have "Poly_Mapping.map_key PP (monomial c t) = Poly_Mapping.map_key PP (monomial c (PP (mapping_of t)))" by (simp only: mapping_of_inverse) also from inj_PP have "\ = monomial c (mapping_of t)" by (fact map_key_single) finally show ?thesis . qed lemma map_key_PP_one [simp]: "Poly_Mapping.map_key PP 1 = 1" by (simp add: zero_pp.rep_eq flip: single_one) lemma map_key_PP_monom_mult_punit: "Poly_Mapping.map_key PP (monom_mult_punit c t p) = monom_mult_punit c (mapping_of t) (Poly_Mapping.map_key PP p)" by (rule poly_mapping_eqI) (simp add: punit.lookup_monom_mult monom_mult_punit_def adds_pp_iff PP_inverse lookup_map_key_PP mapping_of_inverse flip: minus_pp.abs_eq) lemma map_key_PP_times: "Poly_Mapping.map_key PP (p * q) = Poly_Mapping.map_key PP p * Poly_Mapping.map_key PP (q::(_, _::add_linorder) pp \\<^sub>0 _)" by (induct p rule: poly_mapping_plus_induct) (simp_all add: distrib_right map_key_PP_plus times_monomial_left map_key_PP_monom_mult_punit flip: monom_mult_punit_def) lemma map_key_PP_sum: "Poly_Mapping.map_key PP (sum f A) = (\a\A. Poly_Mapping.map_key PP (f a))" by (induct A rule: infinite_finite_induct) (simp_all add: map_key_PP_plus) lemma map_key_PP_ideal: "Poly_Mapping.map_key PP ` ideal F = ideal (Poly_Mapping.map_key PP ` (F::((_, _::add_linorder) pp \\<^sub>0 _) set))" proof - from map_key_PP_mapping_of have "surj (Poly_Mapping.map_key PP)" by (rule surjI) with map_key_PP_plus map_key_PP_times show ?thesis by (rule image_ideal_eq_surj) qed subsubsection \Locale \pp_powerprod\\ text \We have to introduce a new locale analogous to @{locale pm_powerprod}, but this time for power-products represented by @{type pp} rather than @{type poly_mapping}. This apparently leads to some (more-or-less) duplicate definitions and lemmas, but seems to be the only feasible way to get both \<^item> the convenient representation by @{type poly_mapping} for theory development, and \<^item> the executable representation by @{type pp} for code generation.\ locale pp_powerprod = ordered_powerprod ord ord_strict for ord::"('x::{countable,linorder}, nat) pp \ ('x, nat) pp \ bool" and ord_strict begin sublocale gd_powerprod .. sublocale pp_pm: extended_ord_pm_powerprod "\s t. ord (PP s) (PP t)" "\s t. ord_strict (PP s) (PP t)" by standard (auto simp: zero_min plus_monotone simp flip: zero_pp_def plus_pp.abs_eq PP_inject) definition poly_deg_pp :: "(('x, nat) pp \\<^sub>0 'a::zero) \ nat" where "poly_deg_pp p = (if p = 0 then 0 else max_list (map deg_pp (punit.keys_to_list p)))" primrec deg_le_sect_pp_aux :: "'x list \ nat \ ('x, nat) pp \\<^sub>0 nat" where "deg_le_sect_pp_aux xs 0 = 1" | "deg_le_sect_pp_aux xs (Suc n) = (let p = deg_le_sect_pp_aux xs n in p + foldr (\x. (+) (monom_mult_punit 1 (single_pp x 1) p)) xs 0)" definition deg_le_sect_pp :: "'x list \ nat \ ('x, nat) pp list" where "deg_le_sect_pp xs d = punit.keys_to_list (deg_le_sect_pp_aux xs d)" definition deg_shifts_pp :: "'x list \ nat \ (('x, nat) pp \\<^sub>0 'b) list \ (('x, nat) pp \\<^sub>0 'b::semiring_1) list" where "deg_shifts_pp xs d fs = concat (map (\f. (map (\t. monom_mult_punit 1 t f) (deg_le_sect_pp xs (d - poly_deg_pp f)))) fs)" definition indets_pp :: "(('x, nat) pp \\<^sub>0 'b::zero) \ 'x list" where "indets_pp p = remdups (concat (map keys_pp_to_list (punit.keys_to_list p)))" definition Indets_pp :: "(('x, nat) pp \\<^sub>0 'b::zero) list \ 'x list" where "Indets_pp ps = remdups (concat (map indets_pp ps))" lemma map_PP_insort: "map PP (pp_pm.ordered_powerprod_lin.insort x xs) = ordered_powerprod_lin.insort (PP x) (map PP xs)" by (induct xs) simp_all lemma map_PP_sorted_list_of_set: "map PP (pp_pm.ordered_powerprod_lin.sorted_list_of_set T) = ordered_powerprod_lin.sorted_list_of_set (PP ` T)" proof (induct T rule: infinite_finite_induct) case (infinite T) moreover from inj_PP subset_UNIV have "inj_on PP T" by (rule inj_on_subset) ultimately show ?case by (simp add: inj_PP finite_image_iff) next case empty show ?case by simp next case (insert t T) moreover from insert(2) have "PP t \ PP ` T" by (simp add: PP_inject image_iff) ultimately show ?case by (simp add: map_PP_insort) qed lemma map_PP_pps_to_list: "map PP (pp_pm.punit.pps_to_list T) = punit.pps_to_list (PP ` T)" by (simp add: pp_pm.punit.pps_to_list_def punit.pps_to_list_def map_PP_sorted_list_of_set flip: rev_map) lemma map_mapping_of_pps_to_list: "map mapping_of (punit.pps_to_list T) = pp_pm.punit.pps_to_list (mapping_of ` T)" proof - have "map mapping_of (punit.pps_to_list T) = map mapping_of (punit.pps_to_list (PP ` mapping_of ` T))" by (simp add: image_comp) also have "\ = map mapping_of (map PP (pp_pm.punit.pps_to_list (mapping_of ` T)))" by (simp only: map_PP_pps_to_list) also have "\ = pp_pm.punit.pps_to_list (mapping_of ` T)" by simp finally show ?thesis . qed lemma keys_to_list_map_key_PP: "pp_pm.punit.keys_to_list (Poly_Mapping.map_key PP p) = map mapping_of (punit.keys_to_list p)" by (simp add: pp_pm.punit.keys_to_list_def punit.keys_to_list_def keys_map_key_PP map_mapping_of_pps_to_list) lemma Keys_to_list_map_key_PP: "pp_pm.punit.Keys_to_list (map (Poly_Mapping.map_key PP) fs) = map mapping_of (punit.Keys_to_list fs)" by (simp add: punit.Keys_to_list_eq_pps_to_list pp_pm.punit.Keys_to_list_eq_pps_to_list map_mapping_of_pps_to_list Keys_def image_UN keys_map_key_PP) lemma poly_deg_map_key_PP: "poly_deg (Poly_Mapping.map_key PP p) = poly_deg_pp p" proof - { assume "p \ 0" hence "map deg_pp (punit.keys_to_list p) \ []" by (simp add: punit.keys_to_list_def punit.pps_to_list_def) hence "Max (deg_pp ` keys p) = max_list (map deg_pp (punit.keys_to_list p))" by (simp add: max_list_Max punit.set_keys_to_list) } thus ?thesis by (simp add: poly_deg_def poly_deg_pp_def keys_map_key_PP image_image flip: deg_pp.rep_eq) qed lemma deg_le_sect_pp_aux_1: assumes "t \ keys (deg_le_sect_pp_aux xs n)" shows "deg_pp t \ n" and "keys_pp t \ set xs" proof - from assms have "deg_pp t \ n \ keys_pp t \ set xs" proof (induct n arbitrary: t) case 0 thus ?case by (simp_all add: keys_pp.rep_eq zero_pp.rep_eq) next case (Suc n) define X where "X = set xs" define q where "q = deg_le_sect_pp_aux xs n" have 1: "s \ keys q \ deg_pp s \ n \ keys_pp s \ X" for s unfolding q_def X_def by (fact Suc.hyps) note Suc.prems also have "keys (deg_le_sect_pp_aux xs (Suc n)) \ keys q \ keys (foldr (\x. (+) (monom_mult_punit 1 (single_pp x 1) q)) xs 0)" (is "_ \ _ \ keys (foldr ?r xs 0)") by (simp add: Let_def Poly_Mapping.keys_add flip: q_def) finally show ?case proof assume "t \ keys q" hence "deg_pp t \ n \ keys_pp t \ set xs" unfolding q_def by (rule Suc.hyps) thus ?thesis by simp next assume "t \ keys (foldr ?r xs 0)" moreover have "set xs \ X" by (simp add: X_def) ultimately have "deg_pp t \ Suc n \ keys_pp t \ X" proof (induct xs arbitrary: t) case Nil thus ?case by simp next case (Cons x xs) from Cons.prems(2) have "x \ X" and "set xs \ X" by simp_all note Cons.prems(1) also have "keys (foldr ?r (x # xs) 0) \ keys (?r x 0) \ keys (foldr ?r xs 0)" by (simp add: Poly_Mapping.keys_add) finally show ?case proof assume "t \ keys (?r x 0)" also have "\ = (+) (single_pp x 1) ` keys q" by (simp add: monom_mult_punit_def punit.keys_monom_mult) finally obtain s where "s \ keys q" and t: "t = single_pp x 1 + s" .. from this(1) have "deg_pp s \ n \ keys_pp s \ X" by (rule 1) with \x \ X\ show ?thesis by (simp add: t deg_pp_plus deg_pp_single keys_pp.rep_eq plus_pp.rep_eq keys_plus_ninv_comm_monoid_add single_pp.rep_eq) next assume "t \ keys (foldr ?r xs 0)" thus "deg_pp t \ Suc n \ keys_pp t \ X" using \set xs \ X\ by (rule Cons.hyps) qed qed thus ?thesis by (simp only: X_def) qed qed thus "deg_pp t \ n" and "keys_pp t \ set xs" by simp_all qed lemma deg_le_sect_pp_aux_2: assumes "deg_pp t \ n" and "keys_pp t \ set xs" shows "t \ keys (deg_le_sect_pp_aux xs n)" using assms proof (induct n arbitrary: t) case 0 thus ?case by simp next case (Suc n) have foldr: "foldr (\x. (+) (f x)) ys 0 + y = foldr (\x. (+) (f x)) ys y" for f ys and y::"'z::monoid_add" by (induct ys) (simp_all add: ac_simps) define q where "q = deg_le_sect_pp_aux xs n" from Suc.prems(1) have "deg_pp t \ n \ deg_pp t = Suc n" by auto thus ?case proof assume "deg_pp t \ n" hence "t \ keys q" unfolding q_def using Suc.prems(2) by (rule Suc.hyps) hence "0 < lookup q t" by (simp add: in_keys_iff) also have "\ \ lookup (deg_le_sect_pp_aux xs (Suc n)) t" by (simp add: Let_def lookup_add flip: q_def) finally show ?thesis by (simp add: in_keys_iff) next assume eq: "deg_pp t = Suc n" hence "keys_pp t \ {}" by (auto simp: keys_pp.rep_eq deg_pp.rep_eq) then obtain x where "x \ keys_pp t" by blast with Suc.prems(2) have "x \ set xs" .. then obtain xs1 xs2 where xs: "xs = xs1 @ x # xs2" by (meson split_list) define s where "s = t - single_pp x 1" from \x \ keys_pp t\ have "single_pp x 1 adds t" by (simp add: adds_pp_iff single_pp.rep_eq keys_pp.rep_eq adds_poly_mapping le_fun_def lookup_single when_def in_keys_iff) hence "s + single_pp x 1 = (t + single_pp x 1) - single_pp x 1" unfolding s_def by (rule minus_plus) hence t: "t = single_pp x 1 + s" by (simp add: add.commute) with eq have "deg_pp s \ n" by (simp add: deg_pp_plus deg_pp_single) moreover have "keys_pp s \ set xs" proof (rule subset_trans) from Suc.prems(2) \x \ set xs\ show "keys_pp t \ keys_pp (single_pp x (Suc 0)) \ set xs" by (simp add: keys_pp.rep_eq single_pp.rep_eq) qed (simp add: s_def keys_pp.rep_eq minus_pp.rep_eq keys_diff) ultimately have "s \ keys q" unfolding q_def by (rule Suc.hyps) hence "t \ keys (monom_mult_punit 1 (single_pp x 1) q)" by (simp add: monom_mult_punit_def punit.keys_monom_mult t) hence "0 < lookup (monom_mult_punit 1 (single_pp x 1) q) t" by (simp add: in_keys_iff) also have "\ \ lookup (q + (foldr (\x. (+) (monom_mult_punit 1 (single_pp x 1) q)) xs1 0 + (monom_mult_punit 1 (single_pp x 1) q + foldr (\x. (+) (monom_mult_punit 1 (single_pp x 1) q)) xs2 0))) t" by (simp add: lookup_add) also have "\ = lookup (deg_le_sect_pp_aux xs (Suc n)) t" by (simp add: Let_def foldr flip: q_def, simp add: xs) finally show ?thesis by (simp add: in_keys_iff) qed qed lemma keys_deg_le_sect_pp_aux: "keys (deg_le_sect_pp_aux xs n) = {t. deg_pp t \ n \ keys_pp t \ set xs}" by (auto dest: deg_le_sect_pp_aux_1 deg_le_sect_pp_aux_2) lemma deg_le_sect_deg_le_sect_pp: "map PP (pp_pm.punit.pps_to_list (deg_le_sect (set xs) d)) = deg_le_sect_pp xs d" proof - have "PP ` {t. deg_pm t \ d \ keys t \ set xs} = PP ` {t. deg_pp (PP t) \ d \ keys_pp (PP t) \ set xs}" by (simp only: keys_pp.abs_eq deg_pp.abs_eq) also have "\ = {t. deg_pp t \ d \ keys_pp t \ set xs}" proof (intro subset_antisym subsetI) fix t assume "t \ {t. deg_pp t \ d \ keys_pp t \ set xs}" moreover have "t = PP (mapping_of t)" by (simp only: mapping_of_inverse) ultimately show "t \ PP ` {t. deg_pp (PP t) \ d \ keys_pp (PP t) \ set xs}" by auto qed auto finally show ?thesis by (simp add: deg_le_sect_pp_def punit.keys_to_list_def keys_deg_le_sect_pp_aux deg_le_sect_alt PPs_def conj_commute map_PP_pps_to_list flip: Collect_conj_eq) qed lemma deg_shifts_deg_shifts_pp: "pp_pm.deg_shifts (set xs) d (map (Poly_Mapping.map_key PP) fs) = map (Poly_Mapping.map_key PP) (deg_shifts_pp xs d fs)" by (simp add: pp_pm.deg_shifts_def deg_shifts_pp_def map_concat comp_def poly_deg_map_key_PP map_key_PP_monom_mult_punit PP_inverse flip: deg_le_sect_deg_le_sect_pp monom_mult_punit_def) lemma ideal_deg_shifts_pp: "ideal (set (deg_shifts_pp xs d fs)) = ideal (set fs)" proof - have "ideal (set (deg_shifts_pp xs d fs)) = Poly_Mapping.map_key mapping_of ` Poly_Mapping.map_key PP ` ideal (set (deg_shifts_pp xs d fs))" by (simp add: image_comp) also have "\ = Poly_Mapping.map_key mapping_of ` ideal (set (map (Poly_Mapping.map_key PP) (deg_shifts_pp xs d fs)))" by (simp add: map_key_PP_ideal) also have "\ = Poly_Mapping.map_key mapping_of ` ideal (Poly_Mapping.map_key PP ` set fs)" by (simp flip: deg_shifts_deg_shifts_pp) also have "\ = Poly_Mapping.map_key mapping_of ` Poly_Mapping.map_key PP ` ideal (set fs)" by (simp only: map_key_PP_ideal) also have "\ = ideal (set fs)" by (simp add: image_comp) finally show ?thesis . qed lemma set_indets_pp: "set (indets_pp p) = indets (Poly_Mapping.map_key PP p)" by (simp add: indets_pp_def indets_def keys_pp_to_list_def keys_pp.rep_eq punit.set_keys_to_list keys_map_key_PP) lemma poly_to_row_map_key_PP: "poly_to_row (map pp.mapping_of xs) (Poly_Mapping.map_key PP p) = poly_to_row xs p" by (simp add: poly_to_row_def comp_def lookup_map_key_PP mapping_of_inverse) lemma Macaulay_mat_map_key_PP: "pp_pm.punit.Macaulay_mat (map (Poly_Mapping.map_key PP) fs) = punit.Macaulay_mat fs" by (simp add: punit.Macaulay_mat_def pp_pm.punit.Macaulay_mat_def Keys_to_list_map_key_PP polys_to_mat_def comp_def poly_to_row_map_key_PP) lemma row_to_poly_mapping_of: assumes "distinct ts" and "dim_vec r = length ts" shows "row_to_poly (map pp.mapping_of ts) r = Poly_Mapping.map_key PP (row_to_poly ts r)" proof (rule poly_mapping_eqI, simp only: lookup_map_key_PP) fix t let ?ts = "map mapping_of ts" from inj_mapping_of subset_UNIV have "inj_on mapping_of (set ts)" by (rule inj_on_subset) with assms(1) have 1: "distinct ?ts" by (simp add: distinct_map) from assms(2) have 2: "dim_vec r = length ?ts" by simp show "lookup (row_to_poly ?ts r) t = lookup (row_to_poly ts r) (PP t)" proof (cases "t \ set ?ts") case True then obtain i where i1: "i < length ?ts" and t1: "t = ?ts ! i" by (metis in_set_conv_nth) hence i2: "i < length ts" and t2: "PP t = ts ! i" by (simp_all add: mapping_of_inverse) have "lookup (row_to_poly ?ts r) t = r $ i" unfolding t1 using 1 2 i1 by (rule punit.lookup_row_to_poly) moreover have "lookup (row_to_poly ts r) (PP t) = r $ i" unfolding t2 using assms i2 by (rule punit.lookup_row_to_poly) ultimately show ?thesis by simp next case False have "PP t \ set ts" proof assume "PP t \ set ts" hence "mapping_of (PP t) \ mapping_of ` set ts" by (rule imageI) with False show False by (simp add: PP_inverse) qed with punit.keys_row_to_poly have "lookup (row_to_poly ts r) (PP t) = 0" by (metis in_keys_iff in_mono) moreover from False punit.keys_row_to_poly have "lookup (row_to_poly ?ts r) t = 0" by (metis in_keys_iff in_mono) ultimately show ?thesis by simp qed qed lemma mat_to_polys_mapping_of: assumes "distinct ts" and "dim_col m = length ts" shows "mat_to_polys (map pp.mapping_of ts) m = map (Poly_Mapping.map_key PP) (mat_to_polys ts m)" proof - { fix r assume "r \ set (rows m)" then obtain i where "r = row m i" by (auto simp: rows_def) hence "dim_vec r = length ts" by (simp add: assms(2)) with assms(1) have "row_to_poly (map pp.mapping_of ts) r = Poly_Mapping.map_key PP (row_to_poly ts r)" by (rule row_to_poly_mapping_of) } thus ?thesis using assms by (simp add: mat_to_polys_def) qed lemma map_key_PP_Macaulay_list: "map (Poly_Mapping.map_key PP) (punit.Macaulay_list fs) = pp_pm.punit.Macaulay_list (map (Poly_Mapping.map_key PP) fs)" by (simp add: punit.Macaulay_list_def pp_pm.punit.Macaulay_list_def Macaulay_mat_map_key_PP Keys_to_list_map_key_PP mat_to_polys_mapping_of filter_map comp_def punit.distinct_Keys_to_list punit.length_Keys_to_list) lemma lpp_map_key_PP: "pp_pm.lpp (Poly_Mapping.map_key PP p) = mapping_of (lpp p)" proof (cases "p = 0") case True thus ?thesis by (simp add: zero_pp.rep_eq) next case False show ?thesis proof (rule pp_pm.punit.lt_eqI_keys) show "pp.mapping_of (lpp p) \ keys (Poly_Mapping.map_key PP p)" unfolding keys_map_key_PP by (intro imageI punit.lt_in_keys False) next fix s assume "s \ keys (Poly_Mapping.map_key PP p)" then obtain t where "t \ keys p" and s: "s = mapping_of t" unfolding keys_map_key_PP .. thus "ord (PP s) (PP (pp.mapping_of (lpp p)))" by (simp add: mapping_of_inverse punit.lt_max_keys) qed qed lemma is_GB_map_key_PP: "finite G \ pp_pm.punit.is_Groebner_basis (Poly_Mapping.map_key PP ` G) \ punit.is_Groebner_basis G" by (simp add: punit.GB_alt_3_finite pp_pm.punit.GB_alt_3_finite lpp_map_key_PP adds_pp_iff flip: map_key_PP_ideal) lemma thm_2_3_6_pp: assumes "pp_pm.is_GB_cofactor_bound (Poly_Mapping.map_key PP ` set fs) b" shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts_pp (Indets_pp fs) b fs)))" proof - let ?fs = "map (Poly_Mapping.map_key PP) fs" from assms have "pp_pm.is_GB_cofactor_bound (set ?fs) b" by simp hence "pp_pm.punit.is_Groebner_basis (set (pp_pm.punit.Macaulay_list (pp_pm.deg_shifts (\ (indets ` set ?fs)) b ?fs)))" by (rule pp_pm.thm_2_3_6_indets) also have "(\ (indets ` set ?fs)) = set (Indets_pp fs)" by (simp add: Indets_pp_def set_indets_pp) finally show ?thesis by (simp add: deg_shifts_deg_shifts_pp map_key_PP_Macaulay_list flip: set_map is_GB_map_key_PP) qed lemma Dube_is_GB_cofactor_bound_pp: "pp_pm.is_GB_cofactor_bound (Poly_Mapping.map_key PP ` set fs) (Dube (Suc (length (Indets_pp fs))) (max_list (map poly_deg_pp fs)))" proof (cases "fs = []") case True show ?thesis by (rule pp_pm.is_GB_cofactor_boundI_subset_zero) (simp add: True) next case False let ?F = "Poly_Mapping.map_key PP ` set fs" have "pp_pm.is_GB_cofactor_bound ?F (Dube (Suc (card (\ (indets ` ?F)))) (maxdeg ?F))" by (intro pp_pm.Dube_is_GB_cofactor_bound_indets finite_imageI finite_set) moreover have "card (\ (indets ` ?F)) = length (Indets_pp fs)" by (simp add: Indets_pp_def length_remdups_card_conv set_indets_pp) moreover from False have "maxdeg ?F = max_list (map poly_deg_pp fs)" by (simp add: max_list_Max maxdeg_def image_image poly_deg_map_key_PP) ultimately show ?thesis by simp qed definition GB_Macaulay_Dube :: "(('x, nat) pp \\<^sub>0 'a) list \ (('x, nat) pp \\<^sub>0 'a::field) list" where "GB_Macaulay_Dube fs = punit.Macaulay_list (deg_shifts_pp (Indets_pp fs) (Dube (Suc (length (Indets_pp fs))) (max_list (map poly_deg_pp fs))) fs)" lemma GB_Macaulay_Dube_is_GB: "punit.is_Groebner_basis (set (GB_Macaulay_Dube fs))" unfolding GB_Macaulay_Dube_def using Dube_is_GB_cofactor_bound_pp by (rule thm_2_3_6_pp) lemma ideal_GB_Macaulay_Dube: "ideal (set (GB_Macaulay_Dube fs)) = ideal (set fs)" by (simp add: GB_Macaulay_Dube_def punit.pmdl_Macaulay_list[simplified] ideal_deg_shifts_pp) end global_interpretation punit': pp_powerprod "ord_pp_punit cmp_term" "ord_pp_strict_punit cmp_term" rewrites "punit.adds_term = (adds)" and "punit.pp_of_term = (\x. x)" and "punit.component_of_term = (\_. ())" and "punit.monom_mult = monom_mult_punit" and "punit.mult_scalar = mult_scalar_punit" and "punit'.punit.min_term = min_term_punit" and "punit'.punit.lt = lt_punit cmp_term" and "punit'.punit.lc = lc_punit cmp_term" and "punit'.punit.tail = tail_punit cmp_term" and "punit'.punit.ord_p = ord_p_punit cmp_term" and "punit'.punit.keys_to_list = keys_to_list_punit cmp_term" for cmp_term :: "('a::nat, nat) pp nat_term_order" defines max_punit = punit'.ordered_powerprod_lin.max and max_list_punit = punit'.ordered_powerprod_lin.max_list and Keys_to_list_punit = punit'.punit.Keys_to_list and Macaulay_mat_punit = punit'.punit.Macaulay_mat and Macaulay_list_punit = punit'.punit.Macaulay_list and poly_deg_pp_punit = punit'.poly_deg_pp and deg_le_sect_pp_aux_punit = punit'.deg_le_sect_pp_aux and deg_le_sect_pp_punit = punit'.deg_le_sect_pp and deg_shifts_pp_punit = punit'.deg_shifts_pp and indets_pp_punit = punit'.indets_pp and Indets_pp_punit = punit'.Indets_pp and GB_Macaulay_Dube_punit = punit'.GB_Macaulay_Dube (* Only needed for auto-reduction: *) and find_adds_punit = punit'.punit.find_adds and trd_aux_punit = punit'.punit.trd_aux and trd_punit = punit'.punit.trd and comp_min_basis_punit = punit'.punit.comp_min_basis and comp_red_basis_aux_punit = punit'.punit.comp_red_basis_aux and comp_red_basis_punit = punit'.punit.comp_red_basis subgoal unfolding punit0.ord_pp_def punit0.ord_pp_strict_def .. subgoal by (fact punit_adds_term) subgoal by (simp add: id_def) subgoal by (fact punit_component_of_term) subgoal by (simp only: monom_mult_punit_def) subgoal by (simp only: mult_scalar_punit_def) subgoal using min_term_punit_def by fastforce subgoal by (simp only: lt_punit_def ord_pp_punit_alt) subgoal by (simp only: lc_punit_def ord_pp_punit_alt) subgoal by (simp only: tail_punit_def ord_pp_punit_alt) subgoal by (simp only: ord_p_punit_def ord_pp_strict_punit_alt) subgoal by (simp only: keys_to_list_punit_def ord_pp_punit_alt) done subsection \Computations\ experiment begin interpretation trivariate\<^sub>0_rat . lemma "comp_red_basis_punit DRLEX (GB_Macaulay_Dube_punit DRLEX [X * Y\<^sup>2 + 3 * X\<^sup>2 * Y, Y ^ 3 - X ^ 3]) = [X ^ 5, X ^ 3 * Y - C\<^sub>0 (1 / 9) * X ^ 4, Y ^ 3 - X ^ 3, X * Y\<^sup>2 + 3 * X\<^sup>2 * Y]" by eval end end (* theory *)