# Theory Degree_Section

(* Author: Alexander Maletzky *)

section βΉDegree Sections of Power-ProductsβΊ

theory Degree_Section
imports Polynomials.MPoly_PM
begin

definition deg_sect :: "'x set β nat β ('x::countable ββ©0 nat) set"
where "deg_sect X d = .[X] β© {t. deg_pm t = d}"

definition deg_le_sect :: "'x set β nat β ('x::countable ββ©0 nat) set"
where "deg_le_sect X d = (βd0β€d. deg_sect X d0)"

lemma deg_sectI: "t β .[X] βΉ deg_pm t = d βΉ t β deg_sect X d"

lemma deg_sectD:
assumes "t β deg_sect X d"
shows "t β .[X]" and "deg_pm t = d"
using assms by (simp_all add: deg_sect_def)

lemma deg_le_sect_alt: "deg_le_sect X d = .[X] β© {t. deg_pm t β€ d}"
by (auto simp: deg_le_sect_def deg_sect_def)

lemma deg_le_sectI: "t β .[X] βΉ deg_pm t β€ d βΉ t β deg_le_sect X d"

lemma deg_le_sectD:
assumes "t β deg_le_sect X d"
shows "t β .[X]" and "deg_pm t β€ d"
using assms by (simp_all add: deg_le_sect_alt)

lemma deg_sect_zero [simp]: "deg_sect X 0 = {0}"
by (auto simp: deg_sect_def zero_in_PPs)

lemma deg_sect_empty: "deg_sect {} d = (if d = 0 then {0} else {})"
by (auto simp: deg_sect_def)

lemma deg_sect_singleton [simp]: "deg_sect {x} d = {Poly_Mapping.single x d}"
by (auto simp: deg_sect_def deg_pm_single PPs_singleton)

lemma deg_le_sect_zero [simp]: "deg_le_sect X 0 = {0}"
by (auto simp: deg_le_sect_def)

lemma deg_le_sect_empty [simp]: "deg_le_sect {} d = {0}"
by (auto simp: deg_le_sect_alt varnum_eq_zero_iff)

lemma deg_le_sect_singleton: "deg_le_sect {x} d = Poly_Mapping.single x  {..d}"
by (auto simp: deg_le_sect_alt deg_pm_single PPs_singleton)

lemma deg_sect_mono: "X β Y βΉ deg_sect X d β deg_sect Y d"
by (auto simp: deg_sect_def dest: PPs_mono)

lemma deg_le_sect_mono_1: "X β Y βΉ deg_le_sect X d β deg_le_sect Y d"
by (auto simp: deg_le_sect_alt dest: PPs_mono)

lemma deg_le_sect_mono_2: "d1 β€ d2 βΉ deg_le_sect X d1 β deg_le_sect X d2"
by (auto simp: deg_le_sect_alt)

lemma zero_in_deg_le_sect: "0 β deg_le_sect n d"

lemma deg_sect_disjoint: "d1 β  d2 βΉ deg_sect X d1 β© deg_sect Y d2 = {}"
by (auto simp: deg_sect_def)

lemma deg_le_sect_deg_sect_disjoint: "d1 < d2 βΉ deg_le_sect Y d1 β© deg_sect X d2 = {}"
by (auto simp: deg_sect_def deg_le_sect_alt)

lemma deg_sect_Suc:
"deg_sect X (Suc d) = (βxβX. (+) (Poly_Mapping.single x 1)  deg_sect X d)" (is "?A = ?B")
proof (rule set_eqI)
fix t
show "t β ?A β· t β ?B"
proof
assume "t β ?A"
hence "t β .[X]" and "deg_pm t = Suc d" by (rule deg_sectD)+
from this(2) have "keys t β  {}" by auto
then obtain x where "x β keys t" by blast
hence "1 β€ lookup t x" by (simp add: in_keys_iff)
from βΉt β .[X]βΊ have "keys t β X" by (rule PPsD)
with βΉx β keys tβΊ have "x β X" ..
let ?s = "Poly_Mapping.single x (1::nat)"
from βΉ1 β€ lookup t xβΊ have "?s adds t"
by (auto simp: lookup_single when_def intro!: adds_poly_mappingI le_funI)
hence t: "?s + (t - ?s) = t" by (metis add.commute adds_minus)
have "t - ?s β deg_sect X d"
proof (rule deg_sectI)
from βΉt β .[X]βΊ show "t - ?s β .[X]" by (rule PPs_closed_minus)
next
from deg_pm_plus[of ?s "t - ?s"] have "deg_pm t = Suc (deg_pm (t - ?s))"
by (simp only: t deg_pm_single)
thus "deg_pm (t - ?s) = d" by (simp add: βΉdeg_pm t = Suc dβΊ)
qed
hence "?s + (t - ?s) β (+) ?s  deg_sect X d" by (rule imageI)
hence "t β (+) ?s  deg_sect X d" by (simp only: t)
with βΉx β XβΊ show "t β ?B" ..
next
assume "t β ?B"
then obtain x where "x β X" and "t β (+) (Poly_Mapping.single x 1)  deg_sect X d" ..
from this(2) obtain s where s: "s β deg_sect X d"
and t: "t = Poly_Mapping.single x 1 + s" (is "t = ?s + s") ..
show "t β ?A"
proof (rule deg_sectI)
from βΉx β XβΊ have "?s β .[X]" by (rule PPs_closed_single)
moreover from s have "s β .[X]" by (rule deg_sectD)
ultimately show "t β .[X]" unfolding t by (rule PPs_closed_plus)
next
from s have "deg_pm s = d" by (rule deg_sectD)
thus "deg_pm t = Suc d" by (simp add: t deg_pm_single deg_pm_plus)
qed
qed
qed

lemma deg_sect_insert:
"deg_sect (insert x X) d = (βd0β€d. (+) (Poly_Mapping.single x (d - d0))  deg_sect X d0)"
(is "?A = ?B")
proof (rule set_eqI)
fix t
show "t β ?A β· t β ?B"
proof
assume "t β ?A"
hence "t β .[insert x X]" and "deg_pm t = d" by (rule deg_sectD)+
from this(1) obtain e tx where "tx β .[X]" and t: "t = Poly_Mapping.single x e + tx"
by (rule PPs_insertE)
have "e + deg_pm tx = deg_pm t" by (simp add: t deg_pm_plus deg_pm_single)
hence "e + deg_pm tx = d" by (simp only: βΉdeg_pm t = dβΊ)
hence "deg_pm tx β {..d}" and e: "e = d - deg_pm tx" by simp_all
from βΉtx β .[X]βΊ refl have "tx β deg_sect X (deg_pm tx)" by (rule deg_sectI)
hence "t β (+) (Poly_Mapping.single x (d - deg_pm tx))  deg_sect X (deg_pm tx)"
unfolding t e by (rule imageI)
with βΉdeg_pm tx β {..d}βΊ show "t β ?B" ..
next
assume "t β ?B"
then obtain d0 where "d0 β {..d}" and "t β (+) (Poly_Mapping.single x (d - d0))  deg_sect X d0" ..
from this(2) obtain s where s: "s β deg_sect X d0"
and t: "t = Poly_Mapping.single x (d - d0) + s" (is "t = ?s + s") ..
show "t β ?A"
proof (rule deg_sectI)
have "?s β .[insert x X]" by (rule PPs_closed_single, simp)
from s have "s β .[X]" by (rule deg_sectD)
also have "... β .[insert x X]" by (rule PPs_mono, blast)
finally have "s β .[insert x X]" .
with βΉ?s β .[insert x X]βΊ show "t β .[insert x X]" unfolding t by (rule PPs_closed_plus)
next
from s have "deg_pm s = d0" by (rule deg_sectD)
moreover from βΉd0 β {..d}βΊ have "d0 β€ d" by simp
ultimately show "deg_pm t = d" by (simp add: t deg_pm_single deg_pm_plus)
qed
qed
qed

lemma deg_le_sect_Suc: "deg_le_sect X (Suc d) = deg_le_sect X d βͺ deg_sect X (Suc d)"
by (simp add: deg_le_sect_def atMost_Suc Un_commute)

lemma deg_le_sect_Suc_2:
"deg_le_sect X (Suc d) = insert 0 (βxβX. (+) (Poly_Mapping.single x 1)  deg_le_sect X d)"
(is "?A = ?B")
proof -
have eq1: "{Suc 0..Suc d} = Suc  {..d}" by (simp add: image_Suc_atMost)
have "insert 0 {1..Suc d} = {..Suc d}" by fastforce
hence "?A = (βd0βinsert 0 {1..Suc d}. deg_sect X d0)" by (simp add: deg_le_sect_def)
also have "... = insert 0 (βd0β€d. deg_sect X (Suc d0))" by (simp add: eq1)
also have "... = insert 0 (βd0β€d. (βxβX. (+) (Poly_Mapping.single x 1)  deg_sect X d0))"
by (simp only: deg_sect_Suc)
also have "... = insert 0 (βxβX. (+) (Poly_Mapping.single x 1)  (βd0β€d. deg_sect X d0))"
by fastforce
also have "... = ?B" by (simp only: deg_le_sect_def)
finally show ?thesis .
qed

lemma finite_deg_sect:
assumes "finite X"
shows "finite ((deg_sect X d)::('x::countable ββ©0 nat) set)"
proof (induct d)
case 0
show ?case by simp
next
case (Suc d)
with assms show ?case by (simp add: deg_sect_Suc)
qed

corollary finite_deg_le_sect: "finite X βΉ finite ((deg_le_sect X d)::('x::countable ββ©0 nat) set)"

lemma keys_subset_deg_le_sectI:
assumes "p β P[X]" and "poly_deg p β€ d"
shows "keys p β deg_le_sect X d"
proof
fix t
assume "t β keys p"
also from assms(1) have "... β .[X]" by (rule PolysD)
finally have "t β .[X]" .
from βΉt β keys pβΊ have "deg_pm t β€ poly_deg p" by (rule poly_deg_max_keys)
from this assms(2) have "deg_pm t β€ d" by (rule le_trans)
with βΉt β .[X]βΊ show "t β deg_le_sect X d" by (rule deg_le_sectI)
qed

lemma binomial_symmetric_plus: "(n + k) choose n = (n + k) choose k"

lemma card_deg_sect:
assumes "finite X" and "X β  {}"
shows "card (deg_sect X d) = (d + (card X - 1)) choose (card X - 1)"
using assms
proof (induct X arbitrary: d)
case empty
thus ?case by simp
next
case (insert x X)
from insert(1, 2) have eq1: "card (insert x X) = Suc (card X)" by simp
show ?case
proof (cases "X = {}")
case True
thus ?thesis by simp
next
case False
with insert.hyps(1) have "0 < card X" by (simp add: card_gt_0_iff)
let ?f = "Ξ»d0. Poly_Mapping.single x (d - d0)"
from False have eq2: "card (deg_sect X d0) = d0 + (card X - 1) choose (card X - 1)" for d0
by (rule insert.hyps)
have "finite {..d}" by simp
moreover from insert.hyps(1) have "βd0β{..d}. finite ((+) (?f d0)  deg_sect X d0)"
moreover have "βd0β{..d}. βd1β{..d}. d0 β  d1 βΆ
((+) (?f d0)  deg_sect X d0) β© ((+) (?f d1)  deg_sect X d1) = {}"
proof (intro ballI impI, rule ccontr)
fix d1 d2 :: nat
assume "d1 β  d2"
assume "((+) (?f d1)  deg_sect X d1) β© ((+) (?f d2)  deg_sect X d2) β  {}"
then obtain t where "t β ((+) (?f d1)  deg_sect X d1) β© ((+) (?f d2)  deg_sect X d2)"
by blast
hence t1: "t β (+) (?f d1)  deg_sect X d1" and t2: "t β (+) (?f d2)  deg_sect X d2" by simp_all
from t1 obtain s1 where "s1 β deg_sect X d1" and s1: "t = ?f d1 + s1" ..
from this(1) have "s1 β .[X]" by (rule deg_sectD)
hence "keys s1 β X" by (rule PPsD)
with insert.hyps(2) have eq3: "lookup s1 x = 0" by (auto simp: in_keys_iff)
from t2 obtain s2 where "s2 β deg_sect X d2" and s2: "t = ?f d2 + s2" ..
from this(1) have "s2 β .[X]" by (rule deg_sectD)
hence "keys s2 β X" by (rule PPsD)
with insert.hyps(2) have eq4: "lookup s2 x = 0" by (auto simp: in_keys_iff)
from s2 have "lookup (?f d1 + s1) x = lookup (?f d2 + s2) x" by (simp only: s1)
hence "d - d1 = d - d2" by (simp add: lookup_add eq3 eq4)
moreover assume "d1 β {..d}" and "d2 β {..d}"
ultimately have "d1 = d2" by simp
with βΉd1 β  d2βΊ show False ..
qed
ultimately have "card (deg_sect (insert x X) d) =
(βd0β€d. card ((+) (monomial (d - d0) x)  deg_sect X d0))"
unfolding deg_sect_insert by (rule card_UN_disjoint)
also from refl have "... = (βd0β€d. card (deg_sect X d0))"
proof (rule sum.cong)
fix d0
have "inj_on ((+) (monomial (d - d0) x)) (deg_sect X d0)" by (rule, rule add_left_imp_eq)
thus "card ((+) (monomial (d - d0) x)  deg_sect X d0) = card (deg_sect X d0)"
by (rule card_image)
qed
also have "... = (βd0β€d. (card X - 1) + d0 choose (card X - 1))" by (simp only: eq2 add.commute)
also have "... = (βd0β€d. (card X - 1) + d0 choose d0)" by (simp only: binomial_symmetric_plus)
also have "... = Suc ((card X - 1) + d) choose d" by (rule sum_choose_lower)
also from βΉ0 < card XβΊ have "... = d + (card (insert x X) - 1) choose d"
also have "... = d + (card (insert x X) - 1) choose (card (insert x X) - 1)"
by (fact binomial_symmetric_plus)
finally show ?thesis .
qed
qed

corollary card_deg_sect_Suc:
assumes "finite X"
shows "card (deg_sect X (Suc d)) = (d + card X) choose (Suc d)"
proof (cases "X = {}")
case True
thus ?thesis by (simp add: deg_sect_empty)
next
case False
with assms have "0 < card X" by (simp add: card_gt_0_iff)
from assms False have "card (deg_sect X (Suc d)) = (Suc d + (card X - 1)) choose (card X - 1)"
by (rule card_deg_sect)
also have "... = (Suc d + (card X - 1)) choose (Suc d)" by (rule sym, rule binomial_symmetric_plus)
also from βΉ0 < card XβΊ have "... = (d + card X) choose (Suc d)" by simp
finally show ?thesis .
qed

corollary card_deg_le_sect:
assumes "finite X"
shows "card (deg_le_sect X d) = (d + card X) choose card X"
proof (induct d)
case 0
show ?case by simp
next
case (Suc d)
from assms have "finite (deg_le_sect X d)" by (rule finite_deg_le_sect)
moreover from assms have "finite (deg_sect X (Suc d))" by (rule finite_deg_sect)
moreover from lessI have "deg_le_sect X d β© deg_sect X (Suc d) = {}"
by (rule deg_le_sect_deg_sect_disjoint)
ultimately have "card (deg_le_sect X (Suc d)) = card (deg_le_sect X d) + card (deg_sect X (Suc d))"
unfolding deg_le_sect_Suc by (rule card_Un_disjoint)
also from assms have "... = (Suc d + card X) choose Suc d"
by (simp add: Suc.hyps card_deg_sect_Suc binomial_symmetric_plus[of d])
also have "... = (Suc d + card X) choose card X" by (rule binomial_symmetric_plus)
finally show ?case .
qed

end (* theory *)


# Theory Degree_Bound_Utils

(* 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 ββ©0 nat) ββ©0 'b::field) set β nat β bool"
where "is_GB_cofactor_bound F b β·
(β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 ββ©0 nat) ββ©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 "β(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:
assumes "is_GB_cofactor_bound F b"
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) β β(indets  F) β§ poly_deg (q f * f) β€ b β§ (f β F' βΆ q f = 0))"
proof -
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
show ?thesis
proof (intro exI conjI allI)
show "g = (βfβ{}. q f * f)" by (simp add: True q_def)
next
case False
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
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
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:
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 = "β(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: "β(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 β β(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:
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)))"
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 *)


# Theory Groebner_Macaulay

(* 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β©t lt f"
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β©t lt f"
proof (rule, rule)
qed fact+
qed

subsection βΉBoundsβΊ

context pm_powerprod
begin

context
fixes X :: "'x set"
assumes fin_X: "finite X"
begin

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))"

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"
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))"
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]))"
also have "β¦ β ?H" by (rule phull.span_mono, rule deg_shifts_mono, simp add: βΉf β set fsβΊ)
finally show ?thesis .
qed
qed
qed
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::_ ββ©0 'a)" by simp
ultimately obtain g where "g β ?G" and "g β  0" and "punit.lt g adds punit.lt (1::_ ββ©0 'a)"
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 (β(indets  (set fs))) b fs)))"
using _ _ assms
proof (rule thm_2_3_6)
from finite_set show "finite (β(indets  (set fs)))" by (simp add: finite_indets)
next
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 (β(indets  (set fs))) b fs))"
using _ _ assms
proof (rule thm_2_3_7)
from finite_set show "finite (β(indets  (set fs)))" by (simp add: finite_indets)
next
show "set fs β P[β(indets  (set fs))]" by (auto simp: Polys_alt)
qed

end (* pm_powerprod *)

end (* theory *)


# Theory Binomial_Int

(* Author: Alexander Maletzky *)

section βΉInteger Binomial CoefficientsβΊ

theory Binomial_Int
imports Complex_Main
begin

lemma upper_le_binomial:
assumes "0 < k" and "k < n"
shows "n β€ n choose k"
proof -
from assms have "1 β€ n" by simp
define k' where "k' = (if n div 2 β€ k then k else n - k)"
from assms have 1: "k' β€ n - 1" and 2: "n div 2 β€ k'" by (auto simp: k'_def)
from assms(2) have "k β€ n" by simp
have "n choose k = n choose k'" by (simp add: k'_def binomial_symmetric[OF βΉk β€ nβΊ])
have "n = n choose 1" by (simp only: choose_one)
also from βΉ1 β€ nβΊ have "β¦ = n choose (n - 1)" by (rule binomial_symmetric)
also from 1 2 have "β¦ β€ n choose k'" by (rule binomial_antimono) simp
also have "β¦ = n choose k" by (simp add: k'_def binomial_symmetric[OF βΉk β€ nβΊ])
finally show ?thesis .
qed

text βΉRestore original sort constraints:βΊ
setup βΉSign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::{semidom_divide,semiring_char_0} β nat β 'a"})βΊ

lemma gbinomial_0_left: "0 gchoose k = (if k = 0 then 1 else 0)"
by (cases k) simp_all

lemma gbinomial_eq_0_int:
assumes "n < k"
shows "(int n) gchoose k = 0"
proof -
have "βaβ{0..<k}. int n - int a = 0"
proof
show "int n - int n = 0" by simp
next
from assms show "n β {0..<k}" by simp
qed
with finite_atLeastLessThan have eq: "prod (Ξ»i. int n - int i) {0..<k} = 0" by (rule prod_zero)
show ?thesis by (simp add: gbinomial_prod_rev eq)
qed

corollary gbinomial_eq_0: "0 β€ a βΉ a < int k βΉ a gchoose k = 0"
by (metis nat_eq_iff2 nat_less_iff gbinomial_eq_0_int)

lemma int_binomial: "int (n choose k) = (int n) gchoose k"
proof (cases "k β€ n")
case True
from refl have eq: "(βi = 0..<k. int (n - i)) = (βi = 0..<k. int n - int i)"
proof (rule prod.cong)
fix i
assume "i β {0..<k}"
with True show "int (n - i) = int n - int i" by simp
qed
show ?thesis
by (simp add: gbinomial_binomial[symmetric] gbinomial_prod_rev zdiv_int eq)
next
case False
thus ?thesis by (simp add: gbinomial_eq_0_int)
qed

lemma falling_fact_pochhammer: "prod (Ξ»i. a - int i) {0..<k} = (- 1) ^ k * pochhammer (- a) k"
proof -
have eq: "z ^ Suc n * prod f {0..n} = prod (Ξ»x. z * f x) {0..n}" for z::int and n f
by (induct n) (simp_all add: ac_simps)
show ?thesis
proof (cases k)
case 0
thus ?thesis by (simp add: pochhammer_minus)
next
case (Suc n)
thus ?thesis
by (simp only: pochhammer_prod atLeastLessThanSuc_atLeastAtMost
prod.atLeast_Suc_atMost_Suc_shift eq flip: power_mult_distrib) (simp add: of_nat_diff)
qed
qed

lemma falling_fact_pochhammer': "prod (Ξ»i. a - int i) {0..<k} = pochhammer (a - int k + 1) k"

lemma gbinomial_int_pochhammer: "(a::int) gchoose k = (- 1) ^ k * pochhammer (- a) k div fact k"
by (simp only: gbinomial_prod_rev falling_fact_pochhammer)

lemma gbinomial_int_pochhammer': "a gchoose k = pochhammer (a - int k + 1) k div fact k"
by (simp only: gbinomial_prod_rev falling_fact_pochhammer')

lemma fact_dvd_pochhammer: "fact k dvd pochhammer (a::int) k"
proof -
have dvd: "y β  0 βΉ ((of_int (x div y))::'a::field_char_0) = of_int x / of_int y βΉ y dvd x"
for x y :: int
by (smt dvd_triv_left mult.commute nonzero_eq_divide_eq of_int_eq_0_iff of_int_eq_iff of_int_mult)
show ?thesis
proof (cases "0 < a")
case True
moreover define n where "n = nat (a - 1) + k"
ultimately have a: "a = int n - int k + 1" by simp
from fact_nonzero show ?thesis unfolding a
proof (rule dvd)
have "of_int (pochhammer (int n - int k + 1) k div fact k) = (of_int (int n gchoose k)::rat)"
by (simp only: gbinomial_int_pochhammer')
also have "β¦ = of_int (int (n choose k))" by (simp only: int_binomial)
also have "β¦ = of_nat (n choose k)" by simp
also have "β¦ = (of_nat n) gchoose k" by (fact binomial_gbinomial)
also have "β¦ = pochhammer (of_nat n - of_nat k + 1) k / fact k"
by (fact gbinomial_pochhammer')
also have "β¦ = pochhammer (of_int (int n - int k + 1)) k / fact k" by simp
also have "β¦ = (of_int (pochhammer (int n - int k + 1) k)) / (of_int (fact k))"
by (simp only: of_int_fact pochhammer_of_int)
finally show "of_int (pochhammer (int n - int k + 1) k div fact k) =
of_int (pochhammer (int n - int k + 1) k) / rat_of_int (fact k)" .
qed
next
case False
moreover define n where "n = nat (- a)"
ultimately have a: "a = - int n" by simp
from fact_nonzero have "fact k dvd (-1)^k * pochhammer (- int n) k"
proof (rule dvd)
have "of_int ((-1)^k * pochhammer (- int n) k div fact k) = (of_int (int n gchoose k)::rat)"
by (simp only: gbinomial_int_pochhammer)
also have "β¦ = of_int (int (n choose k))" by (simp only: int_binomial)
also have "β¦ = of_nat (n choose k)" by simp
also have "β¦ = (of_nat n) gchoose k" by (fact binomial_gbinomial)
also have "β¦ = (-1)^k * pochhammer (- of_nat n) k / fact k"
by (fact gbinomial_pochhammer)
also have "β¦ = (-1)^k * pochhammer (of_int (- int n)) k / fact k" by simp
also have "β¦ = (-1)^k * (of_int (pochhammer (- int n) k)) / (of_int (fact k))"
by (simp only: of_int_fact pochhammer_of_int)
also have "β¦ = (of_int ((-1)^k * pochhammer (- int n) k)) / (of_int (fact k))" by simp
finally show "of_int ((- 1) ^ k * pochhammer (- int n) k div fact k) =
of_int ((- 1) ^ k * pochhammer (- int n) k) / rat_of_int (fact k)" .
qed
thus ?thesis unfolding a by (metis dvdI dvd_mult_unit_iff' minus_one_mult_self)
qed
qed

lemma gbinomial_int_negated_upper: "(a gchoose k) = (-1) ^ k * ((int k - a - 1) gchoose k)"
by (simp add: gbinomial_int_pochhammer pochhammer_minus algebra_simps fact_dvd_pochhammer div_mult_swap)

lemma gbinomial_int_mult_fact: "fact k * (a gchoose k) = (βi = 0..<k. a - int i)"
by (simp only: gbinomial_int_pochhammer' fact_dvd_pochhammer dvd_mult_div_cancel falling_fact_pochhammer')

corollary gbinomial_int_mult_fact': "(a gchoose k) * fact k = (βi = 0..<k. a - int i)"
using gbinomial_int_mult_fact[of k a] by (simp add: ac_simps)

lemma gbinomial_int_binomial:
"a gchoose k = (if 0 β€ a then int ((nat a) choose k) else (-1::int)^k * int ((k + (nat (- a)) - 1) choose k))"
by (auto simp: int_binomial gbinomial_int_negated_upper[of a] int_ops(6))

corollary gbinomial_nneg: "0 β€ a βΉ a gchoose k = int ((nat a) choose k)"

corollary gbinomial_neg: "a < 0 βΉ a gchoose k = (-1::int)^k * int ((k + (nat (- a)) - 1) choose k)"

lemma of_int_gbinomial: "of_int (a gchoose k) = (of_int a :: 'a::field_char_0) gchoose k"
proof -
have of_int_div: "y dvd x βΉ of_int (x div y) = of_int x / (of_int y :: 'a)" for x y :: int by auto
show ?thesis
by (simp add: gbinomial_int_pochhammer' gbinomial_pochhammer' of_int_div fact_dvd_pochhammer
pochhammer_of_int[symmetric])
qed

lemma uminus_one_gbinomial [simp]: "(- 1::int) gchoose k = (- 1) ^ k"

lemma gbinomial_int_Suc_Suc: "(x + 1::int) gchoose (Suc k) = (x gchoose k) + (x gchoose (Suc k))"
proof (rule linorder_cases)
assume 1: "x + 1 < 0"
hence 2: "x < 0" by simp
then obtain n where 3: "nat (- x) = Suc n" using not0_implies_Suc by fastforce
hence 4: "nat (- x - 1) = n" by simp
show ?thesis
proof (cases k)
case 0
show ?thesis by (simp add: βΉk = 0βΊ)
next
case (Suc k')
from 1 2 3 4 show ?thesis by (simp add: βΉk = Suc k'βΊ gbinomial_int_binomial int_distrib(2))
qed
next
assume "x + 1 = 0"
hence "x = - 1" by simp
thus ?thesis by simp
next
assume "0 < x + 1"
hence "0 β€ x + 1" and "0 β€ x" and "nat (x + 1) = Suc (nat x)" by simp_all
thus ?thesis by (simp add: gbinomial_int_binomial)
qed

corollary plus_Suc_gbinomial:
"(x + (1 + int k)) gchoose (Suc k) = ((x + int k) gchoose k) + ((x + int k) gchoose (Suc k))"
(is "?l = ?r")
proof -
have "?l = (x + int k + 1) gchoose (Suc k)" by (simp only: ac_simps)
also have "β¦ = ?r" by (fact gbinomial_int_Suc_Suc)
finally show ?thesis .
qed

lemma gbinomial_int_n_n [simp]: "(int n) gchoose n = 1"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "int (Suc n) gchoose Suc n = (int n + 1) gchoose Suc n" by (simp add: add.commute)
also have "β¦ = (int n gchoose n) + (int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
finally show ?case by (simp add: Suc gbinomial_eq_0)
qed

lemma gbinomial_int_Suc_n [simp]: "(1 + int n) gchoose n = 1 + int n"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "1 + int (Suc n) gchoose Suc n = (1 + int n) + 1 gchoose Suc n" by simp
also have "β¦ = (1 + int n gchoose n) + (1 + int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
also have "β¦ = 1 + int n + (int (Suc n) gchoose (Suc n))" by (simp add: Suc)
also have "β¦ = 1 + int (Suc n)" by (simp only: gbinomial_int_n_n)
finally show ?case .
qed

lemma zbinomial_eq_0_iff [simp]: "a gchoose k = 0 β· (0 β€ a β§ a < int k)"
proof
assume a: "a gchoose k = 0"
have 1: "b < int k" if "b gchoose k = 0" for b
proof (rule ccontr)
assume "Β¬ b < int k"
hence "0 β€ b" and "k β€ nat b" by simp_all
from this(1) have "int ((nat b) choose k) = b gchoose k" by (simp add: gbinomial_int_binomial)
also have "β¦ = 0" by (fact that)
finally show False using βΉk β€ nat bβΊ by simp
qed
show "0 β€ a β§ a < int k"
proof
show "0 β€ a"
proof (rule ccontr)
assume "Β¬ 0 β€ a"
hence "(-1) ^ k * ((int k - a - 1) gchoose k) = a gchoose k"
also have "β¦ = 0" by (fact a)
finally have "(int k - a - 1) gchoose k = 0" by simp
hence "int k - a - 1 < int k" by (rule 1)
with βΉΒ¬ 0 β€ aβΊ show False by simp
qed
next
from a show "a < int k" by (rule 1)
qed
qed (auto intro: gbinomial_eq_0)

subsection βΉSumsβΊ

lemma gchoose_rising_sum_nat: "(βjβ€n. int j + int k gchoose k) = (int n + int k + 1) gchoose (Suc k)"
proof -
have "(βjβ€n. int j + int k gchoose k) = int (βjβ€n. k + j choose k)"
also have "(βjβ€n. k + j choose k) = (k + n + 1) choose (k + 1)" by (fact choose_rising_sum(1))
also have "int β¦ = (int n + int k + 1) gchoose (Suc k)"
by (simp add: int_binomial ac_simps del: binomial_Suc_Suc)
finally show ?thesis .
qed

lemma gchoose_rising_sum:
assumes "0 β€ n"   ββΉNecessary condition.βΊ
shows "(βj=0..n. j + int k gchoose k) = (n + int k + 1) gchoose (Suc k)"
proof -
from _ refl have "(βj=0..n. j + int k gchoose k) = (βjβint  {0..nat n}. j + int k gchoose k)"
proof (rule sum.cong)
from assms show "{0..n} = int  {0..nat n}" by (simp add: image_int_atLeastAtMost)
qed
also have "β¦ = (βjβ€nat n. int j + int k gchoose k)" by (simp add: sum.reindex atMost_atLeast0)
also have "β¦ = (int (nat n) + int k + 1) gchoose (Suc k)" by (fact gchoose_rising_sum_nat)
also from assms have "β¦ = (n + int k + 1) gchoose (Suc k)" by (simp add: add.assoc add.commute)
finally show ?thesis .
qed

subsection βΉInequalitiesβΊ

lemma binomial_mono:
assumes "m β€ n"
shows "m choose k β€ n choose k"
proof -
define l where "l = n - m"
with assms have n: "n = m + l" by simp
have "m choose k β€ (m + l) choose k"
proof (induct l)
case 0
show ?case by simp
next
case *: (Suc l)
show ?case
proof (cases k)
case 0
thus ?thesis by simp
next
case k: (Suc k0)
note *
also have "m + l choose k β€ m + l choose k + (m + l choose k0)" by simp
also have "β¦ = m + Suc l choose k" by (simp add: k)
finally show ?thesis .
qed
qed
thus ?thesis by (simp only: n)
qed

lemma binomial_plus_le:
assumes "0 < k"
shows "(m choose k) + (n choose k) β€ (m + n) choose k"
proof -
define k0 where "k0 = k - 1"
with assms have k: "k = Suc k0" by simp
show ?thesis unfolding k
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "m choose Suc k0 + (Suc n choose Suc k0) = m choose Suc k0 + (n choose Suc k0) + (n choose k0)"
by (simp only: binomial_Suc_Suc)
also from Suc have "β¦ β€ (m + n) choose Suc k0 + ((m + n) choose k0)"
have "n β€ m + n" by simp
thus "n choose k0 β€ m + n choose k0" by (rule binomial_mono)
qed
also have "β¦ = m + Suc n choose Suc k0" by simp
finally show ?case .
qed
qed

lemma binomial_ineq_1: "2 * ((n + i) choose k) β€ n choose k + ((n + 2 * i) choose k)"
proof (cases k)
case 0
thus ?thesis by simp
next
case k: (Suc k0)
show ?thesis unfolding k
proof (induct i)
case 0
thus ?case by simp
next
case (Suc i)
have "2 * (n + Suc i choose Suc k0) = 2 * (n + i choose k0) + 2 * (n + i choose Suc k0)"
by simp
also have "β¦ β€ (n + 2 * i choose k0 + (Suc (n + 2 * i) choose k0)) + (n choose Suc k0 + (n + 2 * i choose Suc k0))"
have "n + i choose k0 β€ n + 2 * i choose k0" by (rule binomial_mono) simp
moreover have "n + 2 * i choose k0 β€ Suc (n + 2 * i) choose k0" by (rule binomial_mono) simp
ultimately show "2 * (n + i choose k0) β€ n + 2 * i choose k0 + (Suc (n + 2 * i) choose k0)"
by simp
qed (fact Suc)
also have "β¦ = n choose Suc k0 + (n + 2 * Suc i choose Suc k0)" by simp
finally show ?case .
qed
qed

lemma gbinomial_int_nonneg:
assumes "0 β€ (x::int)"
shows "0 β€ x gchoose k"
proof -
have "0 β€ int (nat x choose k)" by simp
also from assms have "β¦ = x gchoose k" by (simp add: int_binomial)
finally show ?thesis .
qed

lemma gbinomial_int_mono:
assumes "0 β€ x" and "x β€ (y::int)"
shows "x gchoose k β€ y gchoose k"
proof -
from assms have "nat x β€ nat y" by simp
hence "nat x choose k β€ nat y choose k" by (rule binomial_mono)
hence "int (nat x choose k) β€ int (nat y choose k)" by (simp only: zle_int)
hence "int (nat x) gchoose k β€ int (nat y) gchoose k" by (simp only: int_binomial)
with assms show ?thesis by simp
qed

lemma gbinomial_int_plus_le:
assumes "0 < k" and "0 β€ x" and "0 β€ (y::int)"
shows "(x gchoose k) + (y gchoose k) β€ (x + y) gchoose k"
proof -
from assms(1) have "nat x choose k + (nat y choose k) β€ nat x + nat y choose k"
by (rule binomial_plus_le)
hence "int (nat x choose k + (nat y choose k)) β€ int (nat x + nat y choose k)"
by (simp only: zle_int)
hence "int (nat x) gchoose k + (int (nat y) gchoose k) β€ int (nat x) + int (nat y) gchoose k"
by (simp only: int_plus int_binomial)
with assms(2, 3) show ?thesis by simp
qed

lemma binomial_int_ineq_1:
assumes "0 β€ x" and "0 β€ (y::int)"
shows "2 * (x + y gchoose k) β€ x gchoose k + ((x + 2 * y) gchoose k)"
proof -
from binomial_ineq_1[of "nat x" "nat y" k]
have "int (2 * (nat x + nat y choose k)) β€ int (nat x choose k + (nat x + 2 * nat y choose k))"
by (simp only: zle_int)
hence "2 * (int (nat x) + int (nat y) gchoose k) β€ int (nat x) gchoose k + (int (nat x) + 2 * int (nat y) gchoose k)"
by (simp only: int_binomial int_plus int_ops(7)) simp
with assms show ?thesis by simp
qed

corollary binomial_int_ineq_2:
assumes "0 β€ y" and "y β€ (x::int)"
shows "2 * (x gchoose k) β€ x - y gchoose k + (x + y gchoose k)"
proof -
from assms(2) have "0 β€ x - y" by simp
hence "2 * ((x - y) + y gchoose k) β€ x - y gchoose k + ((x - y + 2 * y) gchoose k)"
using assms(1) by (rule binomial_int_ineq_1)
thus ?thesis by smt
qed

corollary binomial_int_ineq_3:
assumes "0 β€ y" and "y β€ 2 * (x::int)"
shows "2 * (x gchoose k) β€ y gchoose k + (2 * x - y gchoose k)"
proof (cases "y β€ x")
case True
hence "0 β€ x - y" by simp
moreover from assms(1) have "x - y β€ x" by simp
ultimately have "2 * (x gchoose k) β€ x - (x - y) gchoose k + (x + (x - y) gchoose k)"
by (rule binomial_int_ineq_2)
thus ?thesis by simp
next
case False
hence "0 β€ y - x" by simp
moreover from assms(2) have "y - x β€ x" by simp
ultimately have "2 * (x gchoose k) β€ x - (y - x) gchoose k + (x + (y - x) gchoose k)"
by (rule binomial_int_ineq_2)
thus ?thesis by simp
qed

subsection βΉBackward Difference OperatorβΊ

definition bw_diff :: "('a β 'a) β 'a β 'a::{ab_group_add,one}"
where "bw_diff f x = f x - f (x - 1)"

lemma bw_diff_const [simp]: "bw_diff (Ξ»_. c) = (Ξ»_. 0)"
by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_id [simp]: "bw_diff (Ξ»x. x) = (Ξ»_. 1)"
by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_plus [simp]: "bw_diff (Ξ»x. f x + g x) = (Ξ»x. bw_diff f x + bw_diff g x)"
by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_uminus [simp]: "bw_diff (Ξ»x. - f x) = (Ξ»x. - bw_diff f x)"
by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_minus [simp]: "bw_diff (Ξ»x. f x - g x) = (Ξ»x. bw_diff f x - bw_diff g x)"
by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_const_pow: "(bw_diff ^^ k) (Ξ»_. c) = (if k = 0 then Ξ»_. c else (Ξ»_. 0))"
by (induct k, simp_all)

lemma bw_diff_id_pow:
"(bw_diff ^^ k) (Ξ»x. x) = (if k = 0 then (Ξ»x. x) else if k = 1 then (Ξ»_. 1) else (Ξ»_. 0))"
by (induct k, simp_all)

lemma bw_diff_plus_pow [simp]:
"(bw_diff ^^ k) (Ξ»x. f x + g x) = (Ξ»x. (bw_diff ^^ k) f x + (bw_diff ^^ k) g x)"
by (induct k, simp_all)

lemma bw_diff_uminus_pow [simp]: "(bw_diff ^^ k) (Ξ»x. - f x) = (Ξ»x. - (bw_diff ^^ k) f x)"
by (induct k, simp_all)

lemma bw_diff_minus_pow [simp]:
"(bw_diff ^^ k) (Ξ»x. f x - g x) = (Ξ»x. (bw_diff ^^ k) f x - (bw_diff ^^ k) g x)"
by (induct k, simp_all)

lemma bw_diff_sum_pow [simp]:
"(bw_diff ^^ k) (Ξ»x. (βiβI. f i x)) = (Ξ»x. (βiβI. (bw_diff ^^ k) (f i) x))"
by (induct I rule: infinite_finite_induct, simp_all add: bw_diff_const_pow)

lemma bw_diff_gbinomial:
assumes "0 < k"
shows "bw_diff (Ξ»x::int. (x + n) gchoose k) = (Ξ»x. (x + n - 1) gchoose (k - 1))"
proof (rule ext)
fix x::int
from assms have eq: "Suc (k - Suc 0) = k" by simp
have "x + n gchoose k = (x + n - 1) + 1 gchoose (Suc (k - 1))" by (simp add: eq)
also have "β¦ = (x + n - 1) gchoose (k - 1) + ((x + n - 1) gchoose (Suc (k - 1)))"
by (fact gbinomial_int_Suc_Suc)
finally show "bw_diff (Ξ»x. x + n gchoose k) x = x + n - 1 gchoose (k - 1)"
by (simp add: eq bw_diff_def algebra_simps)
qed

lemma bw_diff_gbinomial_pow:
"(bw_diff ^^ l) (Ξ»x::int. (x + n) gchoose k) =
(if l β€ k then (Ξ»x. (x + n - int l) gchoose (k - l)) else (Ξ»_. 0))"
proof -
have *: "l0 β€ k βΉ (bw_diff ^^ l0) (Ξ»x::int. (x + n) gchoose k) = (Ξ»x. (x + n - int l0) gchoose (k - l0))"
for l0
proof (induct l0)
case 0
show ?case by simp
next
case (Suc l0)
from Suc.prems have "0 < k - l0" and "l0 β€ k" by simp_all
from this(2) have eq: "(bw_diff ^^ l0) (Ξ»x. x + n gchoose k) = (Ξ»x. x + n - int l0 gchoose (k - l0))"
by (rule Suc.hyps)
have "(bw_diff ^^ Suc l0) (Ξ»x. x + n gchoose k) = bw_diff (Ξ»x. x + (n - int l0) gchoose (k - l0))"
also from βΉ0 < k - l0βΊ have "β¦ = (Ξ»x. (x + (n - int l0) - 1) gchoose (k - l0 - 1))"
by (rule bw_diff_gbinomial)
also have "β¦ = (Ξ»x. x + n - int (Suc l0) gchoose (k - Suc l0))" by (simp add: algebra_simps)
finally show ?case .
qed
show ?thesis
proof (simp add: * split: if_split, intro impI)
assume "Β¬ l β€ k"
hence "(l - k) + k = l" and "l - k β  0" by simp_all
hence "(bw_diff ^^ l) (Ξ»x. x + n gchoose k) = (bw_diff ^^ ((l - k) + k)) (Ξ»x. x + n gchoose k)"
by (simp only:)
also have "β¦ = (bw_diff ^^ (l - k)) (Ξ»_. 1)" by (simp add: * funpow_add)
also from βΉl - k β  0βΊ have "β¦ = (Ξ»_. 0)" by (simp add: bw_diff_const_pow)
finally show "(bw_diff ^^ l) (Ξ»x. x + n gchoose k) = (Ξ»_. 0)" .
qed
qed

end (* theory *)


# Theory Poly_Fun

section βΉInteger Polynomial FunctionsβΊ

theory Poly_Fun
imports Binomial_Int "HOL-Computational_Algebra.Polynomial"
begin

subsection βΉDefinition and Basic PropertiesβΊ

definition poly_fun :: "(int β int) β bool"
where "poly_fun f β· (βp::rat poly. βa. rat_of_int (f a) = poly p (rat_of_int a))"

lemma poly_funI: "(βa. rat_of_int (f a) = poly p (rat_of_int a)) βΉ poly_fun f"
by (auto simp: poly_fun_def)

lemma poly_funE:
assumes "poly_fun f"
obtains p where "βa. rat_of_int (f a) = poly p (rat_of_int a)"
using assms by (auto simp: poly_fun_def)

lemma poly_fun_eqI:
assumes "poly_fun f" and "poly_fun g" and "infinite {a. f a = g a}"
shows "f = g"
proof (rule ext)
fix a
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
from assms(2) obtain q where q: "βa. rat_of_int (g a) = poly q (rat_of_int a)"
by (rule poly_funE, blast)
have "p = q"
proof (rule ccontr)
let ?A = "{a. poly p (rat_of_int a) = poly q (rat_of_int a)}"
assume "p β  q"
hence "p - q β  0" by simp
hence fin: "finite {x. poly (p - q) x = 0}" by (rule poly_roots_finite)
have "rat_of_int  ?A β {x. poly (p - q) x = 0}" by (simp add: image_Collect_subsetI)
hence "finite (rat_of_int  ?A)" using fin by (rule finite_subset)
moreover have "inj_on rat_of_int ?A" by (simp add: inj_on_def)
ultimately have "finite ?A" by (simp only: finite_image_iff)
also have "?A = {a. f a = g a}" by (simp flip: p q)
finally show False using assms(3) by simp
qed
hence "rat_of_int (f a) = rat_of_int (g a)" by (simp add: p q)
thus "f a = g a" by simp
qed

corollary poly_fun_eqI_ge:
assumes "poly_fun f" and "poly_fun g" and "βa. b β€ a βΉ f a = g a"
shows "f = g"
using assms(1, 2)
proof (rule poly_fun_eqI)
have "{b..} β {a. f a = g a}" by (auto intro: assms(3))
thus "infinite {a. f a = g a}" using infinite_Ici by (rule infinite_super)
qed

corollary poly_fun_eqI_gr:
assumes "poly_fun f" and "poly_fun g" and "βa. b < a βΉ f a = g a"
shows "f = g"
using assms(1, 2)
proof (rule poly_fun_eqI)
have "{b<..} β {a. f a = g a}" by (auto intro: assms(3))
thus "infinite {a. f a = g a}" using infinite_Ioi by (rule infinite_super)
qed

subsection βΉClosure PropertiesβΊ

lemma poly_fun_const [simp]: "poly_fun (Ξ»_. c)"
by (rule poly_funI[where p="[:rat_of_int c:]"]) simp

lemma poly_fun_id [simp]: "poly_fun (Ξ»x. x)" "poly_fun id"
proof -
show "poly_fun (Ξ»x. x)" by (rule poly_funI[where p="[:0, 1:]"]) simp
thus "poly_fun id" by (simp only: id_def)
qed

lemma poly_fun_uminus:
assumes "poly_fun f"
shows "poly_fun (Ξ»x. - f x)" and "poly_fun (- f)"
proof -
from assms obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
show "poly_fun (Ξ»x. - f x)" by (rule poly_funI[where p="- p"]) (simp add: p)
thus "poly_fun (- f)" by (simp only: fun_Compl_def)
qed

lemma poly_fun_uminus_iff [simp]:
"poly_fun (Ξ»x. - f x) β· poly_fun f" "poly_fun (- f) β· poly_fun f"
proof -
show "poly_fun (Ξ»x. - f x) β· poly_fun f"
proof
assume "poly_fun (Ξ»x. - f x)"
hence "poly_fun (Ξ»x. - (- f x))" by (rule poly_fun_uminus)
thus "poly_fun f" by simp
qed (rule poly_fun_uminus)
thus "poly_fun (- f) β· poly_fun f" by (simp only: fun_Compl_def)
qed

lemma poly_fun_plus [simp]:
assumes "poly_fun f" and "poly_fun g"
shows "poly_fun (Ξ»x. f x + g x)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
from assms(2) obtain q where q: "βa. rat_of_int (g a) = poly q (rat_of_int a)"
by (rule poly_funE, blast)
show ?thesis by (rule poly_funI[where p="p + q"]) (simp add: p q)
qed

lemma poly_fun_minus [simp]:
assumes "poly_fun f" and "poly_fun g"
shows "poly_fun (Ξ»x. f x - g x)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
from assms(2) obtain q where q: "βa. rat_of_int (g a) = poly q (rat_of_int a)"
by (rule poly_funE, blast)
show ?thesis by (rule poly_funI[where p="p - q"]) (simp add: p q)
qed

lemma poly_fun_times [simp]:
assumes "poly_fun f" and "poly_fun g"
shows "poly_fun (Ξ»x. f x * g x)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
from assms(2) obtain q where q: "βa. rat_of_int (g a) = poly q (rat_of_int a)"
by (rule poly_funE, blast)
show ?thesis by (rule poly_funI[where p="p * q"]) (simp add: p q)
qed

lemma poly_fun_divide:
assumes "poly_fun f" and "βa. c dvd f a"
shows "poly_fun (Ξ»x. f x div c)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
let ?p = "p * [:1 / rat_of_int c:]"
show ?thesis
proof (rule poly_funI)
fix a
have "c dvd f a" by fact
hence "rat_of_int (f a div c) = rat_of_int (f a) / rat_of_int c" by auto
also have "β¦ = poly ?p (rat_of_int a)" by (simp add: p)
finally show "rat_of_int (f a div c) = poly ?p (rat_of_int a)" .
qed
qed

lemma poly_fun_pow [simp]:
assumes "poly_fun f"
shows "poly_fun (Ξ»x. f x ^ k)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
show ?thesis by (rule poly_funI[where p="p ^ k"]) (simp add: p)
qed

lemma poly_fun_comp:
assumes "poly_fun f" and "poly_fun g"
shows "poly_fun (Ξ»x. f (g x))" and "poly_fun (f β g)"
proof -
from assms(1) obtain p where p: "βa. rat_of_int (f a) = poly p (rat_of_int a)"
by (rule poly_funE, blast)
from assms(2) obtain q where q: "βa. rat_of_int (g a) = poly q (rat_of_int a)"
by (rule poly_funE, blast)
show "poly_fun (Ξ»x. f (g x))" by (rule poly_funI[where p="p ββ©p q"]) (simp add: p q poly_pcompose)
thus "poly_fun (f β g)" by (simp only: comp_def)
qed

lemma poly_fun_sum [simp]: "(βi. i β I βΉ poly_fun (f i)) βΉ poly_fun (Ξ»x. (βiβI. f i x))"
proof (induct I rule: infinite_finite_induct)
case (infinite I)
from infinite(1) show ?case by simp
next
case empty
show ?case by simp
next
case (insert i I)
have "i β insert i I" by simp
hence "poly_fun (f i)" by (rule insert.prems)
moreover have "poly_fun (Ξ»x. βiβI. f i x)"
proof (rule insert.hyps)
fix j
assume "j β I"
hence "j β insert i I" by simp
thus "poly_fun (f j)" by (rule insert.prems)
qed
ultimately have "poly_fun (Ξ»x. f i x + (βiβI. f i x))" by (rule poly_fun_plus)
with insert.hyps(1, 2) show ?case by simp
qed

lemma poly_fun_prod [simp]: "(βi. i β I βΉ poly_fun (f i)) βΉ poly_fun (Ξ»x. (βiβI. f i x))"
proof (induct I rule: infinite_finite_induct)
case (infinite I)
from infinite(1) show ?case by simp
next
case empty
show ?case by simp
next
case (insert i I)
have "i β insert i I" by simp
hence "poly_fun (f i)" by (rule insert.prems)
moreover have "poly_fun (Ξ»x. βiβI. f i x)"
proof (rule insert.hyps)
fix j
assume "j β I"
hence "j β insert i I" by simp
thus "poly_fun (f j)" by (rule insert.prems)
qed
ultimately have "poly_fun (Ξ»x. f i x * (βiβI. f i x))" by (rule poly_fun_times)
with insert.hyps(1, 2) show ?case by simp
qed

lemma poly_fun_pochhammer [simp]: "poly_fun f βΉ poly_fun (Ξ»x. pochhammer (f x) k)"

lemma poly_fun_gbinomial [simp]: "poly_fun f βΉ poly_fun (Ξ»x. f x gchoose k)"
by (simp add: gbinomial_int_pochhammer' poly_fun_divide fact_dvd_pochhammer)

end (* theory *)


# Theory Monomial_Module

section βΉMonomial ModulesβΊ

theory Monomial_Module
imports Groebner_Bases.Reduced_GB
begin

text βΉProperties of modules generated by sets of monomials, and (reduced) Gr\"obner bases thereof.βΊ

subsection βΉSets of MonomialsβΊ

definition is_monomial_set :: "('a ββ©0 'b::zero) set β bool"
where "is_monomial_set A β· (βpβA. is_monomial p)"

lemma is_monomial_setI: "(βp. p β A βΉ is_monomial p) βΉ is_monomial_set A"

lemma is_monomial_setD: "is_monomial_set A βΉ p β A βΉ is_monomial p"

lemma is_monomial_set_subset: "is_monomial_set B βΉ A β B βΉ is_monomial_set A"
by (auto simp: is_monomial_set_def)

lemma is_monomial_set_Un: "is_monomial_set (A βͺ B) β· (is_monomial_set A β§ is_monomial_set B)"
by (auto simp: is_monomial_set_def)

subsection βΉModulesβΊ

context term_powerprod
begin

lemma monomial_pmdl:
assumes "is_monomial_set B" and "p β pmdl B"
shows "monomial (lookup p v) v β pmdl B"
using assms(2)
proof (induct p rule: pmdl_induct)
case base: module_0
show ?case by (simp add: pmdl.span_zero)
next
case step: (module_plus p b c t)
have eq: "monomial (lookup (p + monom_mult c t b) v) v =
monomial (lookup p v) v + monomial (lookup (monom_mult c t b) v) v"
from assms(1) step.hyps(3) have "is_monomial b" by (rule is_monomial_setD)
then obtain d u where b: "b = monomial d u" by (rule is_monomial_monomial)
have "monomial (lookup (monom_mult c t b) v) v β pmdl B"
proof (simp add: b monom_mult_monomial lookup_single when_def pmdl.span_zero, intro impI)
assume "t β u = v"
hence "monomial (c * d) v = monom_mult c t b" by (simp add: b monom_mult_monomial)
also from step.hyps(3) have "β¦ β pmdl B" by (rule monom_mult_in_pmdl)
finally show "monomial (c * d) v β pmdl B" .
qed
with step.hyps(2) show ?case unfolding eq by (rule pmdl.span_add)
qed

lemma monomial_pmdl_field:
assumes "is_monomial_set B" and "p β pmdl B" and "v β keys (p::_ ββ©0 'b::field)"
shows "monomial c v β pmdl B"
proof -
from assms(1, 2) have "monomial (lookup p v) v β pmdl B" by (rule monomial_pmdl)
hence "monom_mult (c / lookup p v) 0 (monomial (lookup p v) v) β pmdl B"
by (rule pmdl_closed_monom_mult)
with assms(3) show ?thesis by (simp add: monom_mult_monomial splus_zero in_keys_iff)
qed

end (* term_powerprod *)

context ordered_term
begin

lemma keys_monomial_pmdl:
assumes "is_monomial_set F" and "p β pmdl F" and "t β keys p"
obtains f where "f β F" and "f β  0" and "lt f addsβ©t t"
using assms(2) assms(3)
proof (induct arbitrary: thesis rule: pmdl_induct)
case module_0
from this(2) show ?case by simp
next
case step: (module_plus p f0 c s)
from assms(1) step(3) have "is_monomial f0" unfolding is_monomial_set_def ..
hence "keys f0 = {lt f0}" and "f0 β  0" by (rule keys_monomial, rule monomial_not_0)
from Poly_Mapping.keys_add step(6) have "t β keys p βͺ keys (monom_mult c s f0)" ..
thus ?case
proof
assume "t β keys p"
from step(2)[OF _ this] obtain f where "f β F" and "f β  0" and "lt f addsβ©t t" by blast
thus ?thesis by (rule step(5))
next
assume "t β keys (monom_mult c s f0)"
with keys_monom_mult_subset have "t β (β) s  keys f0" ..
hence "t = s β lt f0" by (simp add: βΉkeys f0 = {lt f0}βΊ)
with βΉf0 β FβΊ βΉf0 β  0βΊ show ?thesis by (rule step(5))
qed
qed

lemma image_lt_monomial_lt: "lt  monomial (1::'b::zero_neq_one)  lt  F = lt  F"
by (auto simp: lt_monomial intro!: image_eqI)

subsection βΉReductionβΊ

lemma red_setE2:
assumes "red B p q"
obtains b where "b β B" and "b β  0" and "red {b} p q"
proof -
from assms obtain b t where "b β B" and "red_single p q b t" by (rule red_setE)
from this(2) have "b β  0" by (simp add: red_single_def)
have "red {b} p q" by (rule red_setI, simp, fact)
show ?thesis by (rule, fact+)
qed

lemma red_monomial_keys:
assumes "is_monomial r" and "red {r} p q"
shows "card (keys p) = Suc (card (keys q))"
proof -
from assms(2) obtain s where rs: "red_single p q r s" unfolding red_singleton ..
hence cp0: "lookup p (s β lt r) β  0" and q_def0: "q = p - monom_mult (lookup p (s β lt r) / lc r) s r"
unfolding red_single_def by simp_all
from assms(1) obtain c t where "c β  0" and r_def: "r = monomial c t" by (rule is_monomial_monomial)
have ltr: "lt r = t" unfolding r_def by (rule lt_monomial, fact)
have lcr: "lc r = c" unfolding r_def by (rule lc_monomial)
define u where "u = s β t"
from q_def0 have "q = p - monom_mult (lookup p u / c) s r" unfolding u_def ltr lcr .
also have "... = p - monomial ((lookup p u / c) * c) u" unfolding u_def r_def monom_mult_monomial ..
finally have q_def: "q = p - monomial (lookup p u) u" using βΉc β  0βΊ by simp
from cp0 have "lookup p u β  0" unfolding u_def ltr .
hence "u β keys p" by (simp add: in_keys_iff)

have "keys q = keys p - {u}" unfolding q_def
proof (rule, rule)
fix x
assume "x β keys (p - monomial (lookup p u) u)"
hence "lookup (p - monomial (lookup p u) u) x β  0" by (simp add: in_keys_iff)
hence a: "lookup p x - lookup (monomial (lookup p u) u) x β  0" unfolding lookup_minus .
hence "x β  u" unfolding lookup_single by auto
with a have "lookup p x β  0" unfolding lookup_single by auto
show "x β keys p - {u}"
proof
from βΉlookup p x β  0βΊ show "x β keys p" by (simp add: in_keys_iff)
next
from βΉx β  uβΊ show "x β {u}" by simp
qed
next
show "keys p - {u} β keys (p - monomial (lookup p u) u)"
proof
fix x
assume "x β keys p - {u}"
hence "x β keys p" and "x β  u" by auto
from βΉx β keys pβΊ have "lookup p x β  0" by (simp add: in_keys_iff)
with βΉx β  uβΊ have "lookup (p - monomial (lookup p u) u) x β  0" by (simp add: lookup_minus lookup_single)
thus "x β keys (p - monomial (lookup p u) u)" by (simp add: in_keys_iff)
qed
qed

have "Suc (card (keys q)) = card (keys p)" unfolding βΉkeys q = keys p - {u}βΊ
by (rule card_Suc_Diff1, rule finite_keys, fact)
thus ?thesis by simp
qed

lemma red_monomial_monomial_setD:
assumes "is_monomial p" and "is_monomial_set B" and "red B p q"
shows "q = 0"
proof -
from assms(3) obtain b where "b β B" and "b β  0" and *: "red {b} p q" by (rule red_setE2)
from assms(2) this(1) have "is_monomial b" by (rule is_monomial_setD)
hence "card (keys p) = Suc (card (keys q))" using * by (rule red_monomial_keys)
with assms(1) show ?thesis by (simp add: is_monomial_def)
qed

corollary is_red_monomial_monomial_setD:
assumes "is_monomial p" and "is_monomial_set B" and "is_red B p"
shows "red B p 0"
proof -
from assms(3) obtain q where "red B p q" by (rule is_redE)
moreover from assms(1, 2) this have "q = 0" by (rule red_monomial_monomial_setD)
ultimately show ?thesis by simp
qed

corollary is_red_monomial_monomial_set_in_pmdl:
"is_monomial p βΉ is_monomial_set B βΉ is_red B p βΉ p β pmdl B"
by (intro red_rtranclp_0_in_pmdl r_into_rtranclp is_red_monomial_monomial_setD)

corollary red_rtrancl_monomial_monomial_set_cases:
assumes "is_monomial p" and "is_monomial_set B" and "(red B)β§*β§* p q"
obtains "q = p" | "q = 0"
using assms(3)
proof (induct q arbitrary: thesis rule: rtranclp_induct)
case base
from refl show ?case by (rule base)
next
case (step y z)
show ?case
proof (rule step.hyps)
assume "y = p"
with step.hyps(2) have "red B p z" by simp
with assms(1, 2) have "z = 0" by (rule red_monomial_monomial_setD)
thus ?thesis by (rule step.prems)
next
assume "y = 0"
from step.hyps(2) have "is_red B 0" unfolding βΉy = 0βΊ by (rule is_redI)
with irred_0 show ?thesis ..
qed
qed

lemma is_red_monomial_lt:
assumes "0 β B"
shows "is_red (monomial (1::'b::field)  lt  B) = is_red B"
proof
fix p
let ?B = "monomial (1::'b)  lt  B"
show "is_red ?B p β· is_red B p"
proof
assume "is_red ?B p"
from this(1) have "lt f β lt  ?B" by (rule imageI)
also have "β¦ = lt  B" by (fact image_lt_monomial_lt)
finally obtain b where "b β B" and eq: "lt f = lt b" ..
note this(1)
moreover from this assms have "b β  0" by blast
moreover note βΉv β keys pβΊ
ultimately show "is_red B p" by (rule is_red_addsI)
next
assume "is_red B p"
from this(1) have "lt b β lt  B" by (rule imageI)
also from image_lt_monomial_lt have "β¦ = lt  ?B" by (rule sym)
finally obtain f where "f β ?B" and eq: "lt b = lt f" ..
note this(1)
moreover from this have "f β  0" by (auto simp: monomial_0_iff)
moreover note βΉv β keys pβΊ
ultimately show "is_red ?B p" by (rule is_red_addsI)
qed
qed

end (* ordered_term *)

subsection βΉGr\"obner BasesβΊ

context gd_term
begin

lemma monomial_set_is_GB:
assumes "is_monomial_set G"
shows "is_Groebner_basis G"
unfolding GB_alt_1
proof
fix f
assume "f β pmdl G"
thus "(red G)β§*β§* f 0"
proof (induct f rule: poly_mapping_plus_induct)
case 1
show ?case ..
next
case (2 f c t)
let ?f = "monomial c t + f"
from 2(1) have "t β keys (monomial c t)" by simp
from this 2(2) have "t β keys ?f" by (rule in_keys_plusI1)
with assms βΉ?f β pmdl GβΊ obtain g where "g β G" and "g β  0" and "lt g addsβ©t t"
by (rule keys_monomial_pmdl)
from this(1) have "red G ?f f"
proof (rule red_setI)
from βΉlt g addsβ©t tβΊ have "component_of_term (lt g) = component_of_term t" and "lp g adds pp_of_term t"
from this have eq: "(pp_of_term t - lp g) β lt g = t"
moreover from 2(2) have "lookup ?f t = c" by (simp add: lookup_add in_keys_iff)
ultimately show "red_single (monomial c t + f) f g (pp_of_term t - lp g)"
proof (simp add: red_single_def βΉg β  0βΊ βΉt β keys ?fβΊ 2(1))
from βΉg β  0βΊ have "lc g β  0" by (rule lc_not_0)
hence "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) (monomial (lc g) (lt g))"
moreover from assms βΉg β GβΊ have "is_monomial g" unfolding is_monomial_set_def ..
ultimately show "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) g"
by (simp only: monomial_eq_itself)
qed
qed
have "f β pmdl G" by (rule pmdl_closed_red, fact subset_refl, fact+)
hence "(red G)β§*β§* f 0" by (rule 2(3))
with βΉred G ?f fβΊ show ?case by simp
qed
qed

context
fixes d
begin

context
fixes F m
assumes fin_comps: "finite (component_of_term  Keys F)"
and F_sub: "F β dgrad_p_set d m"
and F_monom: "is_monomial_set (F::(_ ββ©0 'b::field) set)"
begin

text βΉThe proof of the following lemma could be simplified, analogous to homogeneous ideals.βΊ

lemma reduced_GB_subset_monic_dgrad_p_set: "reduced_GB F β monic  F"
proof -
from subset_refl obtain F' where "F' β F - {0}" and "lt  (F - {0}) = lt  F'" and "inj_on lt F'"
by (rule subset_imageE_inj)
define G where "G = {f β F'. βf'βF'. lt f' addsβ©t lt f βΆ f' = f}"
have "G β F'" by (simp add: G_def)
hence "G β F - {0}" using βΉF' β F - {0}βΊ by (rule subset_trans)
also have "β¦ β F" by blast
finally have "G β F" .
have 1: thesis if "f β F" and "f β  0" and "βg. g β G βΉ lt g addsβ©t lt f βΉ thesis" for thesis f
proof -
let ?K = "component_of_term  Keys F"
let ?A = "{t. pp_of_term t β dgrad_set d m β§ component_of_term t β ?K}"
moreover have "lt f β lt  ?Q"
proof -
from that(1, 2) have "f β F - {0}" by simp
hence "lt f β lt  (F - {0})" by (rule imageI)
also have "β¦ = lt  F'" by fact
finally have "lt f β lt  F'" .
with adds_term_refl show ?thesis by fastforce
qed
moreover have "lt  ?Q β ?A"
proof
fix s
assume "s β lt  ?Q"
then obtain q where "q β ?Q" and s: "s = lt q" ..
from this(1) have "q β F'" by simp
hence "q β F - {0}" using βΉF' β F - {0}βΊ ..
hence "q β F" and "q β  0" by simp_all
from this(1) F_sub have "q β dgrad_p_set d m" ..
from βΉq β  0βΊ have "lt q β keys q" by (rule lt_in_keys)
hence "pp_of_term (lt q) β pp_of_term  keys q" by (rule imageI)
finally have 1: "pp_of_term s β dgrad_set d m" by (simp only: s)
from βΉlt q β keys qβΊ βΉq β FβΊ have "lt q β Keys F" by (rule in_KeysI)
hence "component_of_term s β ?K" unfolding s by (rule imageI)
with 1 show "s β ?A" by simp
qed
ultimately obtain t where "t β lt  ?Q" and t_min: "βs. strict (addsβ©t) s t βΉ s β lt  ?Q"
by (rule wfp_onE_min) blast
from this(1) obtain g where "g β ?Q" and t: "t = lt g" ..
show ?thesis
proof (rule that)
{
fix f'
assume "f' β F'"
with βΉf' β F'βΊ have "f' β ?Q" by simp
hence "lt f' β lt  ?Q" by (rule imageI)
with t_min have "Β¬ strict (addsβ©t) (lt f') (lt g)" unfolding t by blast
with βΉinj_on lt F'βΊ have "f' = g" using βΉf' β F'βΊ βΉg β F'βΊ by (rule inj_onD)
}
with βΉg β F'βΊ show "g β G" by (simp add: G_def)
qed fact
qed
have 2: "is_red G q" if "q β pmdl F" and "q β  0" for q
proof -
from that(2) have "keys q β  {}" by simp
then obtain t where "t β keys q" by blast
with F_monom that(1) obtain f where "f β F" and "f β  0" and *: "lt f addsβ©t t"
by (rule keys_monomial_pmdl)
from this(1, 2) obtain g where "g β G" and "lt g addsβ©t lt f" by (rule 1)
from βΉg β GβΊ βΉG β F - {0}βΊ have "g β F - {0}" ..
hence "g β  0" by simp
with βΉg β GβΊ show ?thesis using βΉt β keys qβΊ ** by (rule is_red_addsI)
qed
from βΉG β F - {0}βΊ have "G β F" by blast
hence "pmdl G β pmdl F" by (rule pmdl.span_mono)
moreover have "is_reduced_GB (monic  G)" unfolding is_reduced_GB_def GB_image_monic
proof (intro conjI image_monic_is_auto_reduced image_monic_is_monic_set)
proof (rule isGB_I_is_red)
from βΉG β FβΊ F_sub show "G β dgrad_p_set d m" by (rule subset_trans)
next
fix f
assume "f β pmdl G"
hence "f β pmdl F" using βΉpmdl G β pmdl FβΊ ..
moreover assume "f β  0"
ultimately show "is_red G f" by (rule 2)
qed
next
show "is_auto_reduced G" unfolding is_auto_reduced_def
proof (intro ballI notI)
fix g
assume "g β G"
hence "g β F" using βΉG β FβΊ ..
with F_monom have "is_monomial g" by (rule is_monomial_setD)
hence keys_g: "keys g = {lt g}" by (rule keys_monomial)
assume "is_red (G - {g}) g"
then obtain g' t where "g' β G - {g}" and "t β keys g" and adds: "lt g' addsβ©t t" by (rule is_red_addsE)
from this(1) have "g' β F'" and "g' β  g" by (simp_all add: G_def)
from βΉt β keys gβΊ have "t = lt g" by (simp add: keys_g)
with βΉg β GβΊ βΉg' β F'βΊ adds have "g' = g" by (simp add: G_def)
with βΉg' β  gβΊ show False ..
qed
next
show "0 β monic  G"
proof
assume "0 β monic  G"
then obtain g where "0 = monic g" and "g β G" ..
moreover from this(2) βΉG β F - {0}βΊ have "g β  0" by blast
ultimately show False by (simp add: monic_0_iff)
qed
qed
moreover have "pmdl (monic  G) = pmdl F" unfolding pmdl_image_monic
proof
show "pmdl F β pmdl G"
proof (rule pmdl.span_subset_spanI, rule)
fix f
assume "f β F"
hence "f β pmdl F" by (rule pmdl.span_base)
moreover from βΉG β FβΊ F_sub have "G β dgrad_p_set d m" by (rule subset_trans)
moreover note βΉpmdl G β pmdl FβΊ 2 βΉf β pmdl FβΊ
moreover from βΉf β FβΊ F_sub have "f β dgrad_p_set d m" ..
ultimately have "(red G)β§*β§* f 0" by (rule is_red_implies_0_red_dgrad_p_set)
thus "f β pmdl G" by (rule red_rtranclp_0_in_pmdl)
qed
qed fact
ultimately have "reduced_GB F = monic  G" by (rule reduced_GB_unique_dgrad_p_set)
also from βΉG β FβΊ have "β¦ β monic  F" by (rule image_mono)
finally show ?thesis .
qed

proof (rule is_monomial_setI)
fix g
assume "g β reduced_GB F"
also have "β¦ β monic  F" by (fact reduced_GB_subset_monic_dgrad_p_set)
finally obtain f where "f β F" and g: "g = monic f" ..
from F_monom this(1) have "is_monomial f" by (rule is_monomial_setD)
hence "card (keys f) = 1" by (simp only: is_monomial_def)
hence "f β  0" by auto
hence "lc f β  0" by (rule lc_not_0)
hence "1 / lc f β  0" by simp
hence "keys g = (β) 0  keys f" by (simp add: keys_monom_mult monic_def g)
also from refl have "β¦ = (Ξ»x. x)  keys f" by (rule image_cong) (simp only: splus_zero)
finally show "is_monomial g" using βΉcard (keys f) = 1βΊ by (simp only: is_monomial_def image_ident)
qed

end

assumes "finite (component_of_term  S)" and "pp_of_term  S β dgrad_set d m"
shows "is_red (reduced_GB (monomial 1  S)) = is_red (monomial (1::'b::field)  S)"
proof
fix p
let ?F = "monomial (1::'b)  S"
from assms(1) have 1: "finite (component_of_term  Keys ?F)" by (simp add: Keys_def)
moreover from assms(2) have 2: "?F β dgrad_p_set d m" by (auto simp: dgrad_p_set_def)
moreover have "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial)
ultimately have "reduced_GB ?F β monic  ?F" by (rule reduced_GB_subset_monic_dgrad_p_set)
also have "β¦ = ?F" by (auto simp: monic_def intro!: image_eqI)
finally have 3: "reduced_GB ?F β ?F" .
show "is_red (reduced_GB ?F) p β· is_red ?F p"
proof
assume "is_red (reduced_GB ?F) p"
thus "is_red ?F p" using 3 by (rule is_red_subset)
next
assume "is_red ?F p"
then obtain f v where "f β ?F" and "v β keys p" and "f β  0" and adds1: "lt f addsβ©t v"
from this(1) have "f β pmdl ?F" by (rule pmdl.span_base)
moreover from βΉf β pmdl ?FβΊ dgrad 1 2 have "f β pmdl (reduced_GB ?F)"
ultimately obtain g where "g β reduced_GB ?F" and "g β  0" and "lt g addsβ©t lt f"
using βΉf β  0βΊ by (rule GB_adds_lt)
with βΉg β reduced_GB ?FβΊ βΉg β  0βΊ βΉv β keys pβΊ show "is_red (reduced_GB ?F) p"
qed
qed

assumes "finite (component_of_term  Keys G)" and "G β dgrad_p_set d m" and "0 β G"
shows "is_red (reduced_GB (monomial (1::'b::field)  lt  G)) = is_red G"
proof -
let ?S = "lt  G"
let ?G = "monomial (1::'b)  ?S"
from assms(3) have "?S β Keys G" by (auto intro: lt_in_keys in_KeysI)
hence "component_of_term  ?S β component_of_term  Keys G"
and *: "pp_of_term  ?S β pp_of_term  Keys G" by (rule image_mono)+
from this(1) have "finite (component_of_term  ?S)" using assms(1) by (rule finite_subset)
moreover from * have "pp_of_term  ?S β dgrad_set d m"
proof (rule subset_trans)
from assms(2) show "pp_of_term  Keys G β dgrad_set d m" by (auto simp: dgrad_p_set_def Keys_def)
qed
ultimately have "is_red (reduced_GB ?G) = is_red ?G" by (rule is_red_reduced_GB_monomial_dgrad_set)
also from assms(3) have "β¦ = is_red G" by (rule is_red_monomial_lt)
finally show ?thesis .
qed

assumes "finite (component_of_term  Keys F)" and "F β dgrad_p_set d m"
shows "reduced_GB (monomial 1  lt  reduced_GB F) = monomial (1::'b::field)  lt  reduced_GB F"
proof (rule reduced_GB_unique)
let ?G = "reduced_GB F"
let ?F = "monomial (1::'b)  lt  ?G"

from dgrad assms have "0 β ?G" and ar: "is_auto_reduced ?G" and "finite ?G"
from this(3) show "finite ?F" by (intro finite_imageI)

show "is_reduced_GB ?F" unfolding is_reduced_GB_def
proof (intro conjI monomial_set_is_GB)
show "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial)
next
show "is_monic_set ?F" by (simp add: is_monic_set_def)
next
show "0 β ?F" by (auto simp: monomial_0_iff)
next
show "is_auto_reduced ?F" unfolding is_auto_reduced_def
proof (intro ballI notI)
fix f
assume "f β ?F"
then obtain g where "g β ?G" and f: "f = monomial 1 (lt g)" by blast
assume "is_red (?F - {f}) f"
then obtain f' v where "f' β ?F - {f}" and "v β keys f" and "f' β  0" and adds1: "lt f' addsβ©t v"
from this(1) have "f' β ?F" and "f' β  f" by simp_all
from this(1) obtain g' where "g' β ?G" and f': "f' = monomial 1 (lt g')" by blast
from βΉv β keys fβΊ have v: "v = lt g" by (simp add: f)
from ar βΉg β ?GβΊ have "Β¬ is_red (?G - {g}) g" by (rule is_auto_reducedD)
moreover have "is_red (?G - {g}) g"
from βΉg' β ?GβΊ βΉf' β  fβΊ show "g' β ?G - {g}" by (auto simp: f f')
next
from βΉg' β ?GβΊ βΉ0 β ?GβΊ show "g' β  0" by blast
next
from βΉg β ?GβΊ βΉ0 β ?GβΊ have "g β  0" by blast
thus "lt g β keys g" by (rule lt_in_keys)
next
qed
ultimately show False ..
qed
qed
qed (fact refl)

end

end (* gd_term *)

end (* theory *)


# Theory Dube_Prelims

(* Author: Alexander Maletzky *)

section βΉPreliminariesβΊ

theory Dube_Prelims
imports Groebner_Bases.General
begin

subsection βΉSetsβΊ

lemma card_geq_ex_subset:
assumes "card A β₯ n"
obtains B where "card B = n" and "B β A"
using assms
proof (induct n arbitrary: thesis)
case base: 0
show ?case
proof (rule base(1))
show "card {} = 0" by simp
next
show "{} β A" ..
qed
next
case ind: (Suc n)
from ind(3) have "n < card A" by simp
obtain B where card: "card B = n" and "B β A"
proof (rule ind(1))
from βΉn < card AβΊ show "n β€ card A" by simp
qed
from βΉn < card AβΊ have "card A β  0" by simp
with card.infinite[of A] have "finite A" by blast
let ?C = "A - B"
have "?C β  {}"
proof
assume "A - B = {}"
hence "A β B" by simp
from this βΉB β AβΊ have "A = B" ..
from βΉn < card AβΊ show False unfolding βΉA = BβΊ card by simp
qed
then obtain c where "c β ?C" by auto
hence "c β B" by simp
hence "B - {c} = B" by simp
show ?case
proof (rule ind(2))
thm card.insert_remove
have "card (B βͺ {c}) = card (insert c B)" by simp
also have "... = Suc (card (B - {c}))"
by (rule card.insert_remove, rule finite_subset, fact βΉB β AβΊ, fact)
finally show "card (B βͺ {c}) = Suc n" unfolding βΉB - {c} = BβΊ card .
next
show "B βͺ {c} β A" unfolding Un_subset_iff
proof (intro conjI, fact)
from βΉc β ?CβΊ show "{c} β A" by auto
qed
qed
qed

lemma card_2_E_1:
assumes "card A = 2" and "x β A"
obtains y where "x β  y" and "A = {x, y}"
proof -
have "A - {x} β  {}"
proof
assume "A - {x} = {}"
with assms(2) have "A = {x}" by auto
hence "card A = 1" by simp
with assms show False by simp
qed
then obtain y where "y β A - {x}" by auto
hence "y β A" and "x β  y" by auto
show ?thesis
proof
show "A = {x, y}"
proof (rule sym, rule card_seteq)
from assms(1) show "finite A" using card.infinite by fastforce
next
from βΉx β AβΊ βΉy β AβΊ show "{x, y} β A" by simp
next
from βΉx β  yβΊ show "card A β€ card {x, y}" by (simp add: assms(1))
qed
qed fact
qed

lemma card_2_E:
assumes "card A = 2"
obtains x y where "x β  y" and "A = {x, y}"
proof -
from assms have "A β  {}" by auto
then obtain x where "x β A" by blast
with assms obtain y where "x β  y" and "A = {x, y}" by (rule card_2_E_1)
thus ?thesis ..
qed

subsection βΉSumsβΊ

lemma sum_tail_nat: "0 < b βΉ a β€ (b::nat) βΉ sum f {a..b} = f b + sum f {a..b - 1}"
by (metis One_nat_def Suc_pred add.commute not_le sum.cl_ivl_Suc)

lemma sum_atLeast_Suc_shift: "0 < b βΉ a β€ b βΉ sum f {Suc a..b} = (βi=a..b - 1. f (Suc i))"
by (metis Suc_pred' sum.shift_bounds_cl_Suc_ivl)

lemma sum_split_nat_ivl:
"a β€ Suc j βΉ j β€ b βΉ sum f {a..j} + sum f {Suc j..b} = sum f {a..b}"

subsection βΉ@{const count_list}βΊ

lemma count_list_eq_0_iff: "count_list xs x = 0 β· x β set xs"
by (induct xs) simp_all

lemma count_list_append: "count_list (xs @ ys) x = count_list xs x + count_list ys x"
by (induct xs) simp_all

lemma count_list_map_ge: "count_list xs x β€ count_list (map f xs) (f x)"
by (induct xs) simp_all

lemma count_list_gr_1_E:
assumes "1 < count_list xs x"
obtains i j where "i < j" and "j < length xs" and "xs ! i = x" and "xs ! j = x"
proof -
from assms have "count_list xs x β  0" by simp
hence "x β set xs" by (simp only: count_list_eq_0_iff not_not)
then obtain ys zs where xs: "xs = ys @ x # zs" and "x β set ys" by (meson split_list_first)
hence "count_list xs x = Suc (count_list zs x)" by (simp add: count_list_append)
with assms have "count_list zs x β  0" by simp
hence "x β set zs" by (simp only: count_list_eq_0_iff not_not)
then obtain j where "j < length zs" and "x = zs ! j" by (metis in_set_conv_nth)
show ?thesis
proof
show "length ys < length ys + Suc j" by simp
next
from βΉj < length zsβΊ show "length ys + Suc j < length xs" by (simp add: xs)
next
show "xs ! length ys = x" by (simp add: xs)
next
show "xs ! (length ys + Suc j) = x"
by (simp only: xs βΉx = zs ! jβΊ nth_append_length_plus nth_Cons_Suc)
qed
qed

subsection βΉ@{const listset}βΊ

lemma listset_Cons: "listset (x # xs) = (βyβx. (#) y  listset xs)"
by (auto simp: set_Cons_def)

lemma listset_ConsI: "y β x βΉ ys' β listset xs βΉ ys = y # ys' βΉ ys β listset (x # xs)"

lemma listset_ConsE:
assumes "ys β listset (x# xs)"
obtains y ys' where "y β x" and "ys' β listset xs" and "ys = y # ys'"
using assms by (auto simp: set_Cons_def)

lemma listsetI:
"length ys = length xs βΉ (βi. i < length xs βΉ ys ! i β xs ! i) βΉ ys β listset xs"
by (induct ys xs rule: list_induct2)
(simp_all, smt Suc_mono list.sel(3) mem_Collect_eq nth_Cons_0 nth_tl set_Cons_def zero_less_Suc)

lemma listsetD:
assumes "ys β listset xs"
shows "length ys = length xs" and "βi. i < length xs βΉ ys ! i β xs ! i"
proof -
from assms have "length ys = length xs β§ (βi<length xs. ys ! i β xs ! i)"
proof (induct xs arbitrary: ys)
case Nil
thus ?case by simp
next
case (Cons x xs)
from Cons.prems obtain y ys' where "y β x" and "ys' β listset xs" and ys: "ys = y # ys'"
by (rule listset_ConsE)
from this(2) have "length ys' = length xs β§ (βi<length xs. ys' ! i β xs ! i)" by (rule Cons.hyps)
hence 1: "length ys' = length xs" and 2: "βi. i < length xs βΉ ys' ! i β xs ! i" by simp_all
show ?case
proof (intro conjI allI impI)
fix i
assume "i < length (x # xs)"
show "ys ! i β (x # xs) ! i"
proof (cases i)
case 0
with βΉy β xβΊ show ?thesis by (simp add: ys)
next
case (Suc j)
with βΉi < length (x # xs)βΊ have "j < length xs" by simp
hence "ys' ! j β xs ! j" by (rule 2)
thus ?thesis by (simp add: ys βΉi = Suc jβΊ)
qed
qed
thus "length ys = length xs" and "βi. i < length xs βΉ ys ! i β xs ! i" by simp_all
qed

lemma listset_singletonI: "a β A βΉ ys = [a] βΉ ys β listset [A]"
by simp

lemma listset_singletonE:
assumes "ys β listset [A]"
obtains a where "a β A" and "ys = [a]"
using assms by auto

lemma listset_doubletonI: "a β A βΉ b β B βΉ ys = [a, b] βΉ ys β listset [A, B]"

lemma listset_doubletonE:
assumes "ys β listset [A, B]"
obtains a b where "a β A" and "b β B" and "ys = [a, b]"
using assms by (auto simp: set_Cons_def)

lemma listset_appendI:
"ys1 β listset xs1 βΉ ys2 β listset xs2 βΉ ys = ys1 @ ys2 βΉ ys β listset (xs1 @ xs2)"
by (induct xs1 arbitrary: ys ys1 ys2)
(simp, auto simp del: listset.simps elim!: listset_ConsE intro!: listset_ConsI)

lemma listset_appendE:
assumes "ys β listset (xs1 @ xs2)"
obtains ys1 ys2 where "ys1 β listset xs1" and "ys2 β listset xs2" and "ys = ys1 @ ys2"
using assms
proof (induct xs1 arbitrary: thesis ys)
case Nil
have "[] β listset []" by simp
moreover from Nil(2) have "ys β listset xs2" by simp
ultimately show ?case by (rule Nil) simp
next
case (Cons x xs1)
from Cons.prems(2) have "ys β listset (x # (xs1 @ xs2))" by simp
then obtain y ys' where "y β x" and "ys' β listset (xs1 @ xs2)" and ys: "ys = y # ys'"
by (rule listset_ConsE)
from _ this(2) obtain ys1 ys2 where ys1: "ys1 β listset xs1" and "ys2 β listset xs2"
and ys': "ys' = ys1 @ ys2" by (rule Cons.hyps)
show ?case
proof (rule Cons.prems)
from βΉy β xβΊ ys1 refl show "y # ys1 β listset (x # xs1)" by (rule listset_ConsI)
next
show "ys = (y # ys1) @ ys2" by (simp add: ys ys')
qed fact
qed

lemma listset_map_imageI: "ys' β listset xs βΉ ys = map f ys' βΉ ys β listset (map (() f) xs)"
by (induct xs arbitrary: ys ys')
(simp, auto simp del: listset.simps elim!: listset_ConsE intro!: listset_ConsI)

lemma listset_map_imageE:
assumes "ys β listset (map (() f) xs)"
obtains ys' where "ys' β listset xs" and "ys = map f ys'"
using assms
proof (induct xs arbitrary: thesis ys)
case Nil
from Nil(2) have "ys = map f []" by simp
with _ show ?case by (rule Nil) simp
next
case (Cons x xs)
from Cons.prems(2) have "ys β listset (f  x # map (() f) xs)" by simp
then obtain y ys' where "y β f  x" and "ys' β listset (map (() f) xs)" and ys: "ys = y # ys'"
by (rule listset_ConsE)
from _ this(2) obtain ys1 where ys1: "ys1 β listset xs" and ys': "ys' = map f ys1" by (rule Cons.hyps)
from βΉy β f  xβΊ obtain y1 where "y1 β x" and y: "y = f y1" ..
show ?case
proof (rule Cons.prems)
from βΉy1 β xβΊ ys1 refl show "y1 # ys1 β listset (x # xs)" by (rule listset_ConsI)
qed (simp add: ys ys' y)
qed

lemma listset_permE:
assumes "ys β listset xs" and "bij_betw f {..<length xs} {..<length xs'}"
and "βi. i < length xs βΉ xs' ! i = xs ! f i"
obtains ys' where "ys' β listset xs'" and "length ys' = length ys"
and "βi. i < length ys βΉ ys' ! i = ys ! f i"
proof -
from assms(1) have len_ys: "length ys = length xs" by (rule listsetD)
from assms(2) have "card {..<length xs} = card {..<length xs'}" by (rule bij_betw_same_card)
hence len_xs: "length xs = length xs'" by simp
define ys' where "ys' = map (Ξ»i. ys ! (f i)) [0..<length ys]"
have 1: "ys' ! i = ys ! f i" if "i < length ys" for i using that by (simp add: ys'_def)
show ?thesis
proof
show "ys' β listset xs'"
proof (rule listsetI)
show "length ys' = length xs'" by (simp add: ys'_def len_ys len_xs)

fix i
assume "i < length xs'"
hence "i < length xs" by (simp only: len_xs)
hence "i < length ys" by (simp only: len_ys)
hence "ys' ! i = ys ! (f i)" by (rule 1)
also from assms(1) have "β¦ β xs ! (f i)"
proof (rule listsetD)
from βΉi < length xsβΊ have "i β {..<length xs}" by simp
hence "f i β f  {..<length xs}" by (rule imageI)
also from assms(2) have "β¦ = {..<length xs'}" by (simp add: bij_betw_def)
finally show "f i < length xs" by (simp add: len_xs)
qed
also have "β¦ = xs' ! i" by (rule sym) (rule assms(3), fact)
finally show "ys' ! i β xs' ! i" .
qed
next
show "length ys' = length ys" by (simp add: ys'_def)
qed (rule 1)
qed

lemma listset_closed_map:
assumes "ys β listset xs" and "βx y. x β set xs βΉ y β x βΉ f y β x"
shows "map f ys β listset xs"
using assms
proof (induct xs arbitrary: ys)
case Nil
from Nil(1) show ?case by simp
next
case (Cons x xs)
from Cons.prems(1) obtain y ys' where "y β x" and "ys' β listset xs" and ys: "ys = y # ys'"
by (rule listset_ConsE)
show ?case
proof (rule listset_ConsI)
from _ βΉy β xβΊ show "f y β x" by (rule Cons.prems) simp
next
show "map f ys' β listset xs"
proof (rule Cons.hyps)
fix x0 y0
assume "x0 β set xs"
hence "x0 β set (x # xs)" by simp
moreover assume "y0 β x0"
ultimately show "f y0 β x0" by (rule Cons.prems)
qed fact
qed

lemma listset_closed_map2:
assumes "ys1 β listset xs" and "ys2 β listset xs"
and "βx y1 y2. x β set xs βΉ y1 β x βΉ y2 β x βΉ f y1 y2 β x"
shows "map2 f ys1 ys2 β listset xs"
using assms
proof (induct xs arbitrary: ys1 ys2)
case Nil
from Nil(1) show ?case by simp
next
case (Cons x xs)
from Cons.prems(1) obtain y1 ys1' where "y1 β x" and "ys1' β listset xs" and ys1: "ys1 = y1 # ys1'"
by (rule listset_ConsE)
from Cons.prems(2) obtain y2 ys2' where "y2 β x" and "ys2' β listset xs" and ys2: "ys2 = y2 # ys2'"
by (rule listset_ConsE)
show ?case
proof (rule listset_ConsI)
from _ βΉy1 β xβΊ βΉy2 β xβΊ show "f y1 y2 β x" by (rule Cons.prems) simp
next
show "map2 f ys1' ys2' β listset xs"
proof (rule Cons.hyps)
fix x' y1' y2'
assume "x' β set xs"
hence "x' β set (x # xs)" by simp
moreover assume "y1' β x'" and "y2' β x'"
ultimately show "f y1' y2' β x'" by (rule Cons.prems)
qed fact+
qed

lemma listset_empty_iff: "listset xs = {} β· {} β set xs"
by (induct xs) (auto simp: listset_Cons simp del: listset.simps(2))

lemma listset_mono:
assumes "length xs = length ys" and "βi. i < length ys βΉ xs ! i β ys ! i"
shows "listset xs β listset ys"
using assms
proof (induct xs ys rule: list_induct2)
case Nil
show ?case by simp
next
case (Cons x xs y ys)
show ?case
proof
fix zs'
assume "zs' β listset (x # xs)"
then obtain z zs where "z β x" and zs: "zs β listset xs" and zs': "zs' = z # zs"
by (rule listset_ConsE)
have "0 < length (y # ys)" by simp
hence "(x # xs) ! 0 β (y # ys) ! 0" by (rule Cons.prems)
hence "x β y" by simp
with βΉz β xβΊ have "z β y" ..
moreover from zs have "zs β listset ys"
proof
show "listset xs β listset ys"
proof (rule Cons.hyps)
fix i
assume "i < length ys"
hence "Suc i < length (y # ys)" by simp
hence "(x # xs) ! Suc i β (y # ys) ! Suc i" by (rule Cons.prems)
thus "xs ! i β ys ! i" by simp
qed
qed
ultimately show "zs' β listset (y # ys)" using zs' by (rule listset_ConsI)
qed
qed

end (* theory *)


# Theory Hilbert_Function

(* Author: Alexander Maletzky *)

section βΉDirect Decompositions and Hilbert FunctionsβΊ

theory Hilbert_Function
imports
"HOL-Combinatorics.Permutations"
Dube_Prelims
Degree_Section
begin

subsection βΉDirect DecompositionsβΊ

text βΉThe main reason for defining βΉdirect_decompβΊ in terms of lists rather than sets is that
lemma βΉdirect_decomp_direct_decompβΊ can be proved easier. At some point one could invest the time
to re-define βΉdirect_decompβΊ in terms of sets (possibly adding a couple of further assumptions to
βΉdirect_decomp_direct_decompβΊ).βΊ

definition direct_decomp :: "'a set β 'a::comm_monoid_add set list β bool"
where "direct_decomp A ss β· bij_betw sum_list (listset ss) A"

lemma direct_decompI:
"inj_on sum_list (listset ss) βΉ sum_list  listset ss = A βΉ direct_decomp A ss"

lemma direct_decompI_alt:
"(βqs. qs β listset ss βΉ sum_list qs β A) βΉ (βa. a β A βΉ β!qsβlistset ss. a = sum_list qs) βΉ
direct_decomp A ss"
by (auto simp: direct_decomp_def intro!: bij_betwI') blast

lemma direct_decompD:
assumes "direct_decomp A ss"
shows "qs β listset ss βΉ sum_list qs β A" and "inj_on sum_list (listset ss)"
and "sum_list  listset ss = A"
using assms by (auto simp: direct_decomp_def bij_betw_def)

lemma direct_decompE:
assumes "direct_decomp A ss" and "a β A"
obtains qs where "qs β listset ss" and "a = sum_list qs"
using assms by (auto simp: direct_decomp_def bij_betw_def)

lemma direct_decomp_unique:
"direct_decomp A ss βΉ qs β listset ss βΉ qs' β listset ss βΉ sum_list qs = sum_list qs' βΉ
qs = qs'"
by (auto dest: direct_decompD simp: inj_on_def)

lemma direct_decomp_singleton: "direct_decomp A [A]"
proof (rule direct_decompI_alt)
fix qs
assume "qs β listset [A]"
then obtain q where "q β A" and "qs = [q]" by (rule listset_singletonE)
thus "sum_list qs β A" by simp
next
fix a
assume "a β A"
show "β!qsβlistset [A]. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from βΉa β AβΊ refl show "[a] β listset [A]" by (rule listset_singletonI)
next
fix qs
assume "qs β listset [A] β§ a = sum_list qs"
hence a: "a = sum_list qs" and "qs β listset [A]" by simp_all
from this(2) obtain b where qs: "qs = [b]" by (rule listset_singletonE)
with a show "qs = [a]" by simp
qed simp_all
qed

(* TODO: Move. *)
lemma mset_bij:
assumes "bij_betw f {..<length xs} {..<length ys}" and "βi. i < length xs βΉ xs ! i = ys ! f i"
shows "mset xs = mset ys"
proof -
from assms(1) have 1: "inj_on f {0..<length xs}" and 2: "f  {0..<length xs} = {0..<length ys}"
let ?f = "(!) ys β f"
have "xs = map ?f [0..<length xs]" unfolding list_eq_iff_nth_eq
proof (intro conjI allI impI)
fix i
assume "i < length xs"
hence "xs ! i = ys ! f i" by (rule assms(2))
also from βΉi < length xsβΊ have "β¦ = map ((!) ys β f) [0..<length xs] ! i" by simp
finally show "xs ! i = map ((!) ys β f) [0..<length xs] ! i" .
qed simp
hence "mset xs = mset (map ?f [0..<length xs])" by (rule arg_cong)
also have "β¦ = image_mset ((!) ys) (image_mset f (mset_set {0..<length xs}))"
by (simp flip: image_mset.comp)
also from 1 have "β¦ = image_mset ((!) ys) (mset_set {0..<length ys})"
also have "β¦ = mset (map ((!) ys) [0..<length ys])" by simp
finally show "mset xs = mset ys" by (simp only: map_nth)
qed

lemma direct_decomp_perm:
assumes "direct_decomp A ss1" and "mset ss1 = mset ss2"
shows "direct_decomp A ss2"
proof -
from assms(2) have len_ss1: "length ss1 = length ss2"
using mset_eq_length by blast
from assms(2) obtain f where βΉf permutes {..<length ss2}βΊ
βΉpermute_list f ss2 = ss1βΊ
by (rule mset_eq_permutation)
then have f_bij: "bij_betw f {..<length ss2} {..<length ss1}"
and f: "βi. i < length ss2 βΉ ss1 ! i = ss2 ! f i"
by (auto simp add: permutes_imp_bij permute_list_nth)
define g where "g = inv_into {..<length ss2} f"
from f_bij have g_bij: "bij_betw g {..<length ss1} {..<length ss2}"
unfolding g_def len_ss1 by (rule bij_betw_inv_into)
have f_g: "f (g i) = i" if "i < length ss1" for i
proof -
from that f_bij have "i β f  {..<length ss2}" by (simp add: bij_betw_def len_ss1)
thus ?thesis by (simp only: f_inv_into_f g_def)
qed
have g_f: "g (f i) = i" if "i < length ss2" for i
proof -
from f_bij have "inj_on f {..<length ss2}" by (simp only: bij_betw_def)
moreover from that have "i β {..<length ss2}" by simp
ultimately show ?thesis by (simp add: g_def)
qed
have g: "ss2 ! i = ss1 ! g i" if "i < length ss1" for i
proof -
from that have "i β {..<length ss2}" by (simp add: len_ss1)
hence "g i β g  {..<length ss2}" by (rule imageI)
also from g_bij have "β¦ = {..<length ss2}" by (simp only: len_ss1 bij_betw_def)
finally have "g i < length ss2" by simp
hence "ss1 ! g i = ss2 ! f (g i)" by (rule f)
with that show ?thesis by (simp only: f_g)
qed
show ?thesis
proof (rule direct_decompI_alt)
fix qs2
assume "qs2 β listset ss2"
then obtain qs1 where qs1_in: "qs1 β listset ss1" and len_qs1: "length qs1 = length qs2"
and *: "βi. i < length qs2 βΉ qs1 ! i = qs2 ! f i" using f_bij f by (rule listset_permE) blast+
from βΉqs2 β listset ss2βΊ have "length qs2 = length ss2" by (rule listsetD)
with f_bij have "bij_betw f {..<length qs1} {..<length qs2}" by (simp only: len_qs1 len_ss1)
hence "mset qs1 = mset qs2" using * by (rule mset_bij) (simp only: len_qs1)
hence "sum_list qs2 = sum_list qs1" by (simp flip: sum_mset_sum_list)
also from assms(1) qs1_in have "β¦ β A" by (rule direct_decompD)
finally show "sum_list qs2 β A" .
next
fix a
assume "a β A"
with assms(1) obtain qs where a: "a = sum_list qs" and qs_in: "qs β listset ss1"
by (rule direct_decompE)
from qs_in obtain qs2 where qs2_in: "qs2 β listset ss2" and len_qs2: "length qs2 = length qs"
and 1: "βi. i < length qs βΉ qs2 ! i = qs ! g i" using g_bij g by (rule listset_permE) blast+
show "β!qsβlistset ss2. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs_in have len_qs: "length qs = length ss1" by (rule listsetD)
with g_bij have g_bij2: "bij_betw g {..<length qs2} {..<length qs}" by (simp only: len_qs2 len_ss1)
hence "mset qs2 = mset qs" using 1 by (rule mset_bij) (simp only: len_qs2)
thus a2: "a = sum_list qs2" by (simp only: a flip: sum_mset_sum_list)

fix qs'
assume "qs' β listset ss2 β§ a = sum_list qs'"
hence qs'_in: "qs' β listset ss2" and a': "a = sum_list qs'" by simp_all
from this(1) obtain qs1 where qs1_in: "qs1 β listset ss1" and len_qs1: "length qs1 = length qs'"
and 2: "βi. i < length qs' βΉ qs1 ! i = qs' ! f i" using f_bij f by (rule listset_permE) blast+
from βΉqs' β listset ss2βΊ have "length qs' = length ss2" by (rule listsetD)
with f_bij have "bij_betw f {..<length qs1} {..<length qs'}" by (simp only: len_qs1 len_ss1)
hence "mset qs1 = mset qs'" using 2 by (rule mset_bij) (simp only: len_qs1)
hence "sum_list qs1 = sum_list qs'" by (simp flip: sum_mset_sum_list)
hence "sum_list qs1 = sum_list qs" by (simp only: a flip: a')
with assms(1) qs1_in qs_in have "qs1 = qs" by (rule direct_decomp_unique)
show "qs' = qs2" unfolding list_eq_iff_nth_eq
proof (intro conjI allI impI)
from qs'_in have "length qs' = length ss2" by (rule listsetD)
thus eq: "length qs' = length qs2" by (simp only: len_qs2 len_qs len_ss1)

fix i
assume "i < length qs'"
hence "i < length qs2" by (simp only: eq)
hence "i β {..<length qs2}" and "i < length qs" and "i < length ss1"
from this(1) have "g i β g  {..<length qs2}" by (rule imageI)
also from g_bij2 have "β¦ = {..<length qs}" by (simp only: bij_betw_def)
finally have "g i < length qs'" by (simp add: eq len_qs2)
from βΉi < length qsβΊ have "qs2 ! i = qs ! g i" by (rule 1)
also have "β¦ = qs1 ! g i" by (simp only: βΉqs1 = qsβΊ)
also from βΉg i < length qs'βΊ have "β¦ = qs' ! f (g i)" by (rule 2)
also from βΉi < length ss1βΊ have "β¦ = qs' ! i" by (simp only: f_g)
finally show "qs' ! i = qs2 ! i" by (rule sym)
qed
qed fact
qed
qed

lemma direct_decomp_split_map:
"direct_decomp A (map f ss) βΉ direct_decomp A (map f (filter P ss) @ map f (filter (- P) ss))"
proof (rule direct_decomp_perm)
show "mset (map f ss) = mset (map f (filter P ss) @ map f (filter (- P) ss))"
by simp (metis image_mset_union multiset_partition)
qed

lemmas direct_decomp_split = direct_decomp_split_map[where f=id, simplified]

lemma direct_decomp_direct_decomp:
assumes "direct_decomp A (s # ss)" and "direct_decomp s rs"
shows "direct_decomp A (ss @ rs)" (is "direct_decomp A ?ss")
proof (rule direct_decompI_alt)
fix qs
assume "qs β listset ?ss"
then obtain qs1 qs2 where qs1: "qs1 β listset ss" and qs2: "qs2 β listset rs" and qs: "qs = qs1 @ qs2"
by (rule listset_appendE)
have "sum_list qs = sum_list ((sum_list qs2) # qs1)" by (simp add: qs add.commute)
also from assms(1) have "β¦ β A"
proof (rule direct_decompD)
from assms(2) qs2 have "sum_list qs2 β s" by (rule direct_decompD)
thus "sum_list qs2 # qs1 β listset (s # ss)" using qs1 refl by (rule listset_ConsI)
qed
finally show "sum_list qs β A" .
next
fix a
assume "a β A"
with assms(1) obtain qs1 where qs1_in: "qs1 β listset (s # ss)" and a: "a = sum_list qs1"
by (rule direct_decompE)
from qs1_in obtain qs11 qs12 where "qs11 β s" and qs12_in: "qs12 β listset ss"
and qs1: "qs1 = qs11 # qs12" by (rule listset_ConsE)
from assms(2) this(1) obtain qs2 where qs2_in: "qs2 β listset rs" and qs11: "qs11 = sum_list qs2"
by (rule direct_decompE)
let ?qs = "qs12 @ qs2"
show "β!qsβlistset ?ss. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs12_in qs2_in refl show "?qs β listset ?ss" by (rule listset_appendI)

show "a = sum_list ?qs" by (simp add: a qs1 qs11 add.commute)

fix qs0
assume "qs0 β listset ?ss β§ a = sum_list qs0"
hence qs0_in: "qs0 β listset ?ss" and a2: "a = sum_list qs0" by simp_all
from this(1) obtain qs01 qs02 where qs01_in: "qs01 β listset ss" and qs02_in: "qs02 β listset rs"
and qs0: "qs0 = qs01 @ qs02" by (rule listset_appendE)
note assms(1)
moreover from _ qs01_in refl have "(sum_list qs02) # qs01 β listset (s # ss)" (is "?qs' β _")
proof (rule listset_ConsI)
from assms(2) qs02_in show "sum_list qs02 β s" by (rule direct_decompD)
qed
moreover note qs1_in
moreover from a2 have "sum_list ?qs' = sum_list qs1" by (simp add: qs0 a add.commute)
ultimately have "?qs' = qs11 # qs12" unfolding qs1 by (rule direct_decomp_unique)
hence "qs11 = sum_list qs02" and 1: "qs01 = qs12" by simp_all
from this(1) have "sum_list qs02 = sum_list qs2" by (simp only: qs11)
with assms(2) qs02_in qs2_in have "qs02 = qs2" by (rule direct_decomp_unique)
thus "qs0 = qs12 @ qs2" by (simp only: 1 qs0)
qed
qed

lemma sum_list_map_times: "sum_list (map ((*) x) xs) = (x::'a::semiring_0) * sum_list xs"
by (induct xs) (simp_all add: algebra_simps)

lemma direct_decomp_image_times:
assumes "direct_decomp (A::'a::semiring_0 set) ss" and "βa b. x * a = x * b βΉ x β  0 βΉ a = b"
shows "direct_decomp ((*) x  A) (map (() ((*) x)) ss)" (is "direct_decomp ?A ?ss")
proof (rule direct_decompI_alt)
fix qs
assume "qs β listset ?ss"
then obtain qs0 where qs0_in: "qs0 β listset ss" and qs: "qs = map ((*) x) qs0"
by (rule listset_map_imageE)
have "sum_list qs = x * sum_list qs0" by (simp only: qs sum_list_map_times)
moreover from assms(1) qs0_in have "sum_list qs0 β A" by (rule direct_decompD)
ultimately show "sum_list qs β (*) x  A" by (rule image_eqI)
next
fix a
assume "a β ?A"
then obtain a' where "a' β A" and a: "a = x * a'" ..
from assms(1) this(1) obtain qs' where qs'_in: "qs' β listset ss" and a': "a' = sum_list qs'"
by (rule direct_decompE)
define qs where "qs = map ((*) x) qs'"
show "β!qsβlistset ?ss. a = sum_list qs"
proof (intro ex1I conjI allI impI)
from qs'_in qs_def show "qs β listset ?ss" by (rule listset_map_imageI)

fix qs0
assume "qs0 β listset ?ss β§ a = sum_list qs0"
hence "qs0 β listset ?ss" and a0: "a = sum_list qs0" by simp_all
from this(1) obtain qs1 where qs1_in: "qs1 β listset ss" and qs0: "qs0 = map ((*) x) qs1"
by (rule listset_map_imageE)
show "qs0 = qs"
proof (cases "x = 0")
case True
from qs1_in have "length qs1 = length ss" by (rule listsetD)
moreover from qs'_in have "length qs' = length ss" by (rule listsetD)
ultimately show ?thesis by (simp add: qs_def qs0 list_eq_iff_nth_eq True)
next
case False
have "x * sum_list qs1 = a" by (simp only: a0 qs0 sum_list_map_times)
also have "β¦ = x * sum_list qs'" by (simp only: a' a)
finally have "sum_list qs1 = sum_list qs'" using False by (rule assms(2))
with assms(1) qs1_in qs'_in have "qs1 = qs'" by (rule direct_decomp_unique)
thus ?thesis by (simp only: qs0 qs_def)
qed
qed (simp only: a a' qs_def sum_list_map_times)
qed

lemma direct_decomp_appendD:
assumes "direct_decomp A (ss1 @ ss2)"
shows "{} β set ss2 βΉ direct_decomp (sum_list  listset ss1) ss1" (is "_ βΉ ?thesis1")
and "{} β set ss1 βΉ direct_decomp (sum_list  listset ss2) ss2" (is "_ βΉ ?thesis2")
and "direct_decomp A [sum_list  listset ss1, sum_list  listset ss2]" (is "direct_decomp _ ?ss")
proof -
have rl: "direct_decomp (sum_list  listset ts1) ts1"
if "direct_decomp A (ts1 @ ts2)" and "{} β set ts2" for ts1 ts2
proof (intro direct_decompI inj_onI refl)
fix qs1 qs2
assume qs1: "qs1 β listset ts1" and qs2: "qs2 β listset ts1"
assume eq: "sum_list qs1 = sum_list qs2"
from that(2) have "listset ts2 β  {}" by (simp add: listset_empty_iff)
then obtain qs3 where qs3: "qs3 β listset ts2" by blast
note that(1)
moreover from qs1 qs3 refl have "qs1 @ qs3 β listset (ts1 @ ts2)" by (rule listset_appendI)
moreover from qs2 qs3 refl have "qs2 @ qs3 β listset (ts1 @ ts2)" by (rule listset_appendI)
moreover have "sum_list (qs1 @ qs3) = sum_list (qs2 @ qs3)" by (simp add: eq)
ultimately have "qs1 @ qs3 = qs2 @ qs3" by (rule direct_decomp_unique)
thus "qs1 = qs2" by simp
qed

{
assume "{} β set ss2"
with assms show ?thesis1 by (rule rl)
}

{
from assms have "direct_decomp A (ss2 @ ss1)"
by (rule direct_decomp_perm) simp
moreover assume "{} β set ss1"
ultimately show ?thesis2 by (rule rl)
}

show "direct_decomp A ?ss"
proof (rule direct_decompI_alt)
fix qs
assume "qs β listset ?ss"
then obtain q1 q2 where q1: "q1 β sum_list  listset ss1" and q2: "q2 β sum_list  listset ss2"
and qs: "qs = [q1, q2]" by (rule listset_doubletonE)
from q1 obtain qs1 where qs1: "qs1 β listset ss1" and q1: "q1 = sum_list qs1" ..
from q2 obtain qs2 where qs2: "qs2 β listset ss2" and q2: "q2 = sum_list qs2" ..
from qs1 qs2 refl have "qs1 @ qs2 β listset (ss1 @ ss2)" by (rule listset_appendI)
with assms have "sum_list (qs1 @ qs2) β A" by (rule direct_decompD)
thus "sum_list qs β A" by (simp add: qs q1 q2)
next
fix a
assume "a β A"
with assms obtain qs0 where qs0_in: "qs0 β listset (ss1 @ ss2)" and a: "a = sum_list qs0"
by (rule direct_decompE)
from this(1) obtain qs1 qs2 where qs1: "qs1 β listset ss1" and qs2: "qs2 β listset ss2"
and qs0: "qs0 = qs1 @ qs2" by (rule listset_appendE)
from qs1 have len_qs1: "length qs1 = length ss1" by (rule listsetD)
define qs where "qs = [sum_list qs1, sum_list qs2]"
show "β!qsβlistset ?ss. a = sum_list qs"
proof (intro ex1I conjI)
from qs1 have "sum_list qs1 β sum_list  listset ss1" by (rule imageI)
moreover from qs2 have "sum_list qs2 β sum_list  listset ss2" by (rule imageI)
ultimately show "qs β listset ?ss" using qs_def by (rule listset_doubletonI)

fix qs'
assume "qs' β listset ?ss β§ a = sum_list qs'"
hence "qs' β listset ?ss" and a': "a = sum_list qs'" by simp_all
from this(1) obtain q1 q2 where q1: "q1 β sum_list  listset ss1"
and q2: "q2 β sum_list  listset ss2" and qs': "qs' = [q1, q2]" by (rule listset_doubletonE)
from q1 obtain qs1' where qs1': "qs1' β listset ss1" and q1: "q1 = sum_list qs1'" ..
from q2 obtain qs2' where qs2': "qs2' β listset ss2" and q2: "q2 = sum_list qs2'" ..
from qs1' have len_qs1': "length qs1' = length ss1" by (rule listsetD)
note assms
moreover from qs1' qs2' refl have "qs1' @ qs2' β listset (ss1 @ ss2)" by (rule listset_appendI)
moreover note qs0_in
moreover have "sum_list (qs1' @ qs2') = sum_list qs0" by (simp add: a' qs' flip: a q1 q2)
ultimately have "qs1' @ qs2' = qs0" by (rule direct_decomp_unique)
also have "β¦ = qs1 @ qs2" by fact
finally show "qs' = qs" by (simp add: qs_def qs' q1 q2 len_qs1 len_qs1')
qed (simp add: qs_def a qs0)
qed
qed

lemma direct_decomp_Cons_zeroI:
assumes "direct_decomp A ss"
shows "direct_decomp A ({0} # ss)"
proof (rule direct_decompI_alt)
fix qs
assume "qs β listset ({0} # ss)"
then obtain q qs' where "q β {0}" and "qs' β listset ss" and "qs = q # qs'"
by (rule listset_ConsE)
from this(1, 3) have "sum_list qs = sum_list qs'" by simp
also from assms βΉqs' β listset ssβΊ have "β¦ β A" by (rule direct_decompD)
finally show "sum_list qs β A" .
next
fix a
assume "a β A"
with assms obtain qs' where qs': "qs' β listset ss" and a: "a = sum_list qs'"
by (rule direct_decompE)
define qs where "qs = 0 # qs'"
show "β!qs. qs β listset ({0} # ss) β§ a = sum_list qs"
proof (intro ex1I conjI)
from _ qs' qs_def show "qs β listset ({0} # ss)" by (rule listset_ConsI) simp
next
fix qs0
assume "qs0 β listset ({0} # ss) β§ a = sum_list qs0"
hence "qs0 β listset ({0} # ss)" and a0: "a = sum_list qs0" by simp_all
from this(1) obtain q0 qs0' where "q0 β {0}" and qs0': "qs0' β listset ss"
and qs0: "qs0 = q0 # qs0'" by (rule listset_ConsE)
from this(1, 3) have "sum_list qs0' = sum_list qs'" by (simp add: a0 flip: a)
with assms qs0' qs' have "qs0' = qs'" by (rule direct_decomp_unique)
with βΉq0 β {0}βΊ show "qs0 = qs" by (simp add: qs_def qs0)
qed

lemma direct_decomp_Cons_zeroD:
assumes "direct_decomp A ({0} # ss)"
shows "direct_decomp A ss"
proof -
have "direct_decomp {0} []" by (simp add: direct_decomp_def bij_betw_def)
with assms have "direct_decomp A (ss @ [])" by (rule direct_decomp_direct_decomp)
thus ?thesis by simp
qed

lemma direct_decomp_Cons_subsetI:
assumes "direct_decomp A (s # ss)" and "βs0. s0 β set ss βΉ 0 β s0"
shows "s β A"
proof
fix x
assume "x β s"
moreover from assms(2) have "map (Ξ»_. 0) ss β listset ss"
by (induct ss, auto simp del: listset.simps(2) intro: listset_ConsI)
ultimately have "x # (map (Ξ»_. 0) ss) β listset (s # ss)" using refl by (rule listset_ConsI)
with assms(1) have "sum_list (x # (map (Ξ»_. 0) ss)) β A" by (rule direct_decompD)
thus "x β A" by simp
qed

lemma direct_decomp_Int_zero:
assumes "direct_decomp A ss" and "i < j" and "j < length ss" and "βs. s β set ss βΉ 0 β s"
shows "ss ! i β© ss ! j = {0}"
proof -
from assms(2, 3) have "i < length ss" by (rule less_trans)
hence i_in: "ss ! i β set ss" by simp
from assms(3) have j_in: "ss ! j β set ss" by simp
show ?thesis
proof
show "ss ! i β© ss ! j β {0}"
proof
fix x
assume "x β ss ! i β© ss ! j"
hence x_i: "x β ss ! i" and x_j: "x β ss ! j" by simp_all
have 1: "(map (Ξ»_. 0) ss)[k := y] β listset ss" if "k < length ss" and "y β ss ! k" for k y
using assms(4) that
proof (induct ss arbitrary: k)
case Nil
from Nil(2) show ?case by simp
next
case (Cons s ss)
have *: "βs'. s' β set ss βΉ 0 β s'" by (rule Cons.prems) simp
show ?case
proof (cases k)
case k: 0
with Cons.prems(3) have "y β s" by simp
moreover from * have "map (Ξ»_. 0) ss β listset ss"
by (induct ss) (auto simp del: listset.simps(2) intro: listset_ConsI)
moreover have "(map (Ξ»_. 0) (s # ss))[k := y] = y # map (Ξ»_. 0) ss" by (simp add: k)
ultimately show ?thesis by (rule listset_ConsI)
next
case k: (Suc k')
have "0 β s" by (rule Cons.prems) simp
moreover from * have "(map (Ξ»_. 0) ss)[k' := y] β listset ss"
proof (rule Cons.hyps)
from Cons.prems(2) show "k' < length ss" by (simp add: k)
next
from Cons.prems(3) show "y β ss ! k'" by (simp add: k)
qed
moreover have "(map (Ξ»_. 0) (s # ss))[k := y] = 0 # (map (Ξ»_. 0) ss)[k' := y]"
ultimately show ?thesis by (rule listset_ConsI)
qed
qed
have 2: "sum_list ((map (Ξ»_. 0) ss)[k := y]) = y" if "k < length ss" for k and y::'a
using that by (induct ss arbitrary: k) (auto simp: add_ac split: nat.split)
define qs1 where "qs1 = (map (Ξ»_. 0) ss)[i := x]"
define qs2 where "qs2 = (map (Ξ»_. 0) ss)[j := x]"
note assms(1)
moreover from βΉi < length ssβΊ x_i have "qs1 β listset ss" unfolding qs1_def by (rule 1)
moreover from assms(3) x_j have "qs2 β listset ss" unfolding qs2_def by (rule 1)
thm sum_list_update
moreover from βΉi < length ssβΊ assms(3) have "sum_list qs1 = sum_list qs2"
by (simp add: qs1_def qs2_def 2)
ultimately have "qs1 = qs2" by (rule direct_decomp_unique)
hence "qs1 ! i = qs2 ! i" by simp
with βΉi < length ssβΊ assms(2, 3) show "x β {0}" by (simp add: qs1_def qs2_def)
qed
next
from i_in have "0 β ss ! i" by (rule assms(4))
moreover from j_in have "0 β ss ! j" by (rule assms(4))
ultimately show "{0} β ss ! i β© ss ! j" by simp
qed
qed

corollary direct_decomp_pairwise_zero:
assumes "direct_decomp A ss" and "βs. s β set ss βΉ 0 β s"
shows "pairwise (Ξ»s1 s2. s1 β© s2 = {0}) (set ss)"
proof (rule pairwiseI)
fix s1 s2
assume "s1 β set ss"
then obtain i where "i < length ss" and s1: "s1 = ss ! i" by (metis in_set_conv_nth)
assume "s2 β set ss"
then obtain j where "j < length ss" and s2: "s2 = ss ! j" by (metis in_set_conv_nth)
assume "s1 β  s2"
hence "i < j β¨ j < i" by (auto simp: s1 s2)
thus "s1 β© s2 = {0}"
proof
assume "i < j"
with assms(1) show ?thesis unfolding s1 s2 using βΉj < length ssβΊ assms(2)
by (rule direct_decomp_Int_zero)
next
assume "j < i"
with assms(1) have "s2 β© s1 = {0}" unfolding s1 s2 using βΉi < length ssβΊ assms(2)
by (rule direct_decomp_Int_zero)
thus ?thesis by (simp only: Int_commute)
qed
qed

corollary direct_decomp_repeated_eq_zero:
assumes "direct_decomp A ss" and "1 < count_list ss X" and "βs. s β set ss βΉ 0 β s"
shows "X = {0}"
proof -
from assms(2) obtain i j where "i < j" and "j < length ss" and 1: "ss ! i = X" and 2: "ss ! j = X"
by (rule count_list_gr_1_E)
from assms(1) this(1, 2) assms(3) have "ss ! i β© ss ! j = {0}" by (rule direct_decomp_Int_zero)
thus ?thesis by (simp add: 1 2)
qed

corollary direct_decomp_map_Int_zero:
assumes "direct_decomp A (map f ss)" and "s1 β set ss" and "s2 β set ss" and "s1 β  s2"
and "βs. s β set ss βΉ 0 β f s"
shows "f s1 β© f s2 = {0}"
proof -
from assms(2) obtain i where "i < length ss" and s1: "s1 = ss ! i`