# 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:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "⋃(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
define q where "q = (λf::('x ⇒⇩0 nat) ⇒⇩0 'b. 0::('x ⇒⇩0 nat) ⇒⇩0 'b)"
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:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b" and "F ⊆ P[X]"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
proof -
let ?X = "⋃(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:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b" and "finite F" and "F ⊆ P[X]"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and "⋀g. g ∈ G ⟹ ∃q. g = (∑f∈F. q f * f) ∧ (∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b)"
proof -
from assms(1, 3) obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and 1: "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule is_GB_cofactor_boundE_Polys) blast
from this(1, 2, 3) show ?thesis
proof
fix g
assume "g ∈ G"
hence "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule 1)
then obtain F' q where "F' ⊆ F" and g: "g = (∑f∈F'. q f * f)"
and "⋀f. q f ∈ P[X]" and "⋀f. poly_deg (q f * f) ≤ b" and 2: "⋀f. f ∉ F' ⟹ q f = 0" by blast
show "∃q. g = (∑f∈F. q f * f) ∧ (∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b)"
proof (intro exI conjI impI allI)
from assms(2) ‹F' ⊆ F› have "(∑f∈F'. q f * f) = (∑f∈F. q f * f)"
proof (intro sum.mono_neutral_left ballI)
fix f
assume "f ∈ F - F'"
hence "f ∉ F'" by simp
hence "q f = 0" by (rule 2)
thus "q f * f = 0" by simp
qed
thus "g = (∑f∈F. q f * f)" by (simp only: g)
qed fact+
qed
qed

lemma is_GB_cofactor_boundI_subset_zero:
assumes "F ⊆ {0}"
shows "is_GB_cofactor_bound F b"
using punit.is_Groebner_basis_empty
proof (rule is_GB_cofactor_boundI)
from assms show "ideal {} = ideal F" by (metis ideal.span_empty ideal_eq_zero_iff)
qed simp_all

lemma is_hom_GB_boundI:
"(⋀g. (⋀f. f ∈ F ⟹ homogeneous f) ⟹ g ∈ punit.reduced_GB F ⟹ poly_deg g ≤ b) ⟹ is_hom_GB_bound F b"
unfolding is_hom_GB_bound_def by blast

lemma is_hom_GB_boundD:
"is_hom_GB_bound F b ⟹ (⋀f. f ∈ F ⟹ homogeneous f) ⟹ g ∈ punit.reduced_GB F ⟹ poly_deg g ≤ b"
unfolding is_hom_GB_bound_def by blast

text ‹The following is the main theorem in this theory. It shows that a bound for Gr\"obner bases of
homogenized input sets is always also a cofactor bound for the original input sets.›

lemma (in extended_ord_pm_powerprod) hom_GB_bound_is_GB_cofactor_bound:
assumes "finite X" and "F ⊆ P[X]" and "extended_ord.is_hom_GB_bound (homogenize None  extend_indets  F) b"
shows "is_GB_cofactor_bound F b"
proof -
let ?F = "homogenize None  extend_indets  F"
define Y where "Y = ⋃ (indets  F)"
define G where "G = restrict_indets  (extended_ord.punit.reduced_GB ?F)"
have "Y ⊆ X"
proof
fix x
assume "x ∈ Y"
then obtain f where "f ∈ F" and "x ∈ indets f" unfolding Y_def ..
from this(1) assms(2) have "f ∈ P[X]" ..
hence "indets f ⊆ X" by (rule PolysD)
with ‹x ∈ indets f› show "x ∈ X" ..
qed
hence "finite Y" using assms(1) by (rule finite_subset)
moreover have "F ⊆ P[Y]" by (auto simp: Y_def Polys_alt)
ultimately have "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[Y]"
unfolding G_def by (rule restrict_indets_reduced_GB)+
from this(1, 2) show ?thesis
proof (rule is_GB_cofactor_boundI)
from ‹G ⊆ P[Y]› show "⋃ (indets  G) ⊆ ⋃ (indets  F)" by (auto simp: Y_def Polys_alt)
next
fix g
assume "g ∈ G"
then obtain g' where g': "g' ∈ extended_ord.punit.reduced_GB ?F"
and g: "g = restrict_indets g'" unfolding G_def ..
have "f ∈ ?F ⟹ homogeneous f" for f by (auto simp: homogeneous_homogenize)
with assms(3) have "poly_deg g' ≤ b" using g' by (rule extended_ord.is_hom_GB_boundD)
from g' have "g' ∈ ideal (extended_ord.punit.reduced_GB ?F)" by (rule ideal.span_base)
also have "… = ideal ?F"
proof (rule extended_ord.reduced_GB_ideal_Polys)
from ‹finite Y› show "finite (insert None (Some  Y))" by simp
next
show "?F ⊆ P[insert None (Some  Y)]"
proof
fix f0
assume "f0 ∈ ?F"
then obtain f where "f ∈ F" and f0: "f0 = homogenize None (extend_indets f)" by blast
from this(1) ‹F ⊆ P[Y]› have "f ∈ P[Y]" ..
hence "extend_indets f ∈ P[Some  Y]" by (auto simp: indets_extend_indets Polys_alt)
thus "f0 ∈ P[insert None (Some  Y)]" unfolding f0 by (rule homogenize_in_Polys)
qed
qed
finally have "g' ∈ ideal ?F" .
with ‹⋀f. f ∈ ?F ⟹ homogeneous f› obtain F0 q where "finite F0" and "F0 ⊆ ?F"
and g': "g' = (∑f∈F0. q f * f)" and deg_le: "⋀f. poly_deg (q f * f) ≤ poly_deg g'"
by (rule homogeneous_idealE) blast+
from this(2) obtain F' where "F' ⊆ F" and F0: "F0 = homogenize None  extend_indets  F'"
and inj_on: "inj_on (homogenize None ∘ extend_indets) F'"
unfolding image_comp by (rule subset_imageE_inj)
show "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)"
proof (intro exI conjI ballI)
from inj_on ‹finite F0› show "finite F'" by (simp only: finite_image_iff F0 image_comp)
next
from inj_on show "g = (∑f∈F'. (restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f)"
by (simp add: g g' F0 restrict_indets_sum restrict_indets_times sum.reindex image_comp o_def)
next
fix f
assume "f ∈ F'"
have "poly_deg ((restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f) =
poly_deg (restrict_indets (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f)))"
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)
from ‹lt g adds⇩t lt f› show "lt g' adds⇩t lt f" by (simp only: ‹lt g = lt g'›)
qed fact+
qed

subsection ‹Bounds›

context pm_powerprod
begin

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

definition deg_shifts :: "nat ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'b) list ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'b::semiring_1) list"
where "deg_shifts d fs = concat (map (λf. (map (λt. punit.monom_mult 1 t f)
(punit.pps_to_list (deg_le_sect X (d - poly_deg f))))) fs)"

lemma set_deg_shifts:
"set (deg_shifts d fs) = (⋃f∈set fs. (λt. punit.monom_mult 1 t f)  (deg_le_sect X (d - poly_deg f)))"
proof -
from fin_X have "finite (deg_le_sect X d0)" for d0 by (rule finite_deg_le_sect)
thus ?thesis by (simp add: deg_shifts_def punit.set_pps_to_list)
qed

corollary set_deg_shifts_singleton:
"set (deg_shifts d [f]) = (λt. punit.monom_mult 1 t f)  (deg_le_sect X (d - poly_deg f))"

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"
then obtain f v where "f ∈ ?B" and "v ∈ keys p" and adds: "lt f adds⇩t v" by (rule is_red_addsE)
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›
moreover from adds have "lt b adds⇩t v" by (simp only: eq)
ultimately show "is_red B p" by (rule is_red_addsI)
next
assume "is_red B p"
then obtain b v where "b ∈ B" and "v ∈ keys p" and adds: "lt b adds⇩t v" by (rule is_red_addsE)
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›
moreover from adds have "lt f adds⇩t v" by (simp only: eq)
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}"
let ?Q = "{f' ∈ F'. lt f' adds⇩t lt f}"
ultimately have "wfp_on (strict (adds⇩t)) ?A" by (rule af_trans_imp_wf)
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" ..
from this(1) have "g ∈ F'" and adds: "lt g adds⇩t lt f" by simp_all
show ?thesis
proof (rule that)
{
fix f'
assume "f' ∈ F'"
assume "lt f' adds⇩t lt g"
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 ‹lt f' adds⇩t lt g› have "lt g adds⇩t lt f'" by blast
with ‹lt f' adds⇩t lt g› have "lt f' = lt g" by (rule adds_term_antisym)
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 this(2) have **: "lt g adds⇩t t" using * by (rule adds_term_trans)
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`