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])" by (rule direct_decomp_perm) simp 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 \ 0" by (simp only: count_list_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 (\(indets ` F))) (maxdeg F)" using _ assms(1) _ assms(2, 3) proof (rule Dube) from assms show "finite (\(indets ` F))" by (simp add: finite_indets) next 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 (\(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 (\(indets ` F)))) (maxdeg F))" using _ assms _ proof (rule Dube_is_GB_cofactor_bound) from assms show "finite (\(indets ` F))" by (simp add: finite_indets) next show "F \ P[\(indets ` F)]" by (auto simp: Polys_alt) qed end (* extended_ord_pm_powerprod *) end (* theory *)