Session Groebner_Macaulay

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"
  by (simp add: deg_sect_def)

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"
  by (simp add: deg_le_sect_alt)

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"
  by (simp add: deg_le_sect_alt zero_in_PPs)

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)"
  by (simp add: deg_le_sect_def finite_deg_sect)

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"
  by (metis add_diff_cancel_left' binomial_symmetric le_add1)

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)"
      by (simp add: finite_deg_sect)
    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"
      by (simp add: eq1 add.commute)
    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)
      qed (simp_all add: 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
      proof (simp add: sub_def, rule)
        from that β€Ήg ∈ Gβ€Ί have "x ∈ ⋃(indets ` G)" by blast
        also have "… βŠ† ?X" by fact
        finally obtain f where "f ∈ F" and "x ∈ indets f" ..
        assume "βˆ€f∈F. x βˆ‰ indets f"
        hence "x βˆ‰ indets f" using β€Ήf ∈ Fβ€Ί ..
        thus "monomial 1 (monomial (Suc 0) x) = 1" using β€Ήx ∈ indets fβ€Ί ..
      qed
      have 2: "sub x = monomial 1 (monomial 1 x)" if "f ∈ F'" and "x ∈ indets f" for f x
      proof (simp add: sub_def, rule)
        assume "βˆ€f∈F. x βˆ‰ indets f"
        moreover from that(1) β€ΉF' βŠ† Fβ€Ί have "f ∈ F" ..
        ultimately have "x βˆ‰ indets f" ..
        thus "monomial 1 (monomial (Suc 0) x) = 1" using that(2) ..
      qed
      have 3: "poly_subst sub f = f" if "f ∈ F'" for f by (rule poly_subst_id, rule 2, rule that)
      define q where "q = (λf. if f ∈ F' then poly_subst sub (q0 f) else 0)"
      show ?thesis
      proof (intro exI allI conjI impI)
        from 1 have "g = poly_subst sub g" by (rule poly_subst_id[symmetric])
        also have "… = (βˆ‘f∈F'. q f * (poly_subst sub f))"
          by (simp add: g poly_subst_sum poly_subst_times q_def cong: sum.cong)
        also from refl have "… = (βˆ‘f∈F'. q f * f)"
        proof (rule sum.cong)
          fix f
          assume "f ∈ F'"
          hence "poly_subst sub f = f" by (rule 3)
          thus "q f * poly_subst sub f = q f * f" by simp
        qed
        finally show "g = (βˆ‘f∈F'. q f * f)" .
      next
        fix f
        have "indets (q f) βŠ† ?X ∧ poly_deg (q f * f) ≀ b"
        proof (cases "f ∈ F'")
          case True
          hence qf: "q f = poly_subst sub (q0 f)" by (simp add: q_def)
          show ?thesis
          proof
            show "indets (q f) βŠ† ?X"
            proof
              fix x
              assume "x ∈ indets (q f)"
              then obtain y where "x ∈ indets (sub y)" unfolding qf by (rule in_indets_poly_substE)
              hence y: "y ∈ ?X" and "x ∈ indets (monomial (1::'b) (monomial (1::nat) y))"
                by (simp_all add: sub_def split: if_splits)
              from this(2) have "x = y" by (simp add: indets_monomial)
              with y show "x ∈ ?X" by (simp only:)
            qed
          next
            from β€Ήf ∈ F'β€Ί have "poly_subst sub f = f" by (rule 3)
            hence "poly_deg (q f * f) = poly_deg (q f * poly_subst sub f)" by (simp only:)
            also have "… = poly_deg (poly_subst sub (q0 f * f))" by (simp only: qf poly_subst_times)
            also have "… ≀ poly_deg (q0 f * f)"
            proof (rule poly_deg_poly_subst_le)
              fix x
              show "poly_deg (sub x) ≀ 1" by (simp add: sub_def poly_deg_monomial deg_pm_single)
            qed
            also from β€Ήf ∈ F'β€Ί have "… ≀ b" by (rule q0)
            finally show "poly_deg (q f * f) ≀ b" .
          qed
        next
          case False
          thus ?thesis by (simp add: q_def)
        qed
        thus "indets (q f) βŠ† ?X" and "poly_deg (q f * f) ≀ b" by simp_all

        assume "f βˆ‰ F'"
        thus "q f = 0" by (simp add: q_def)
      qed fact+
    qed
  qed
qed

lemma is_GB_cofactor_boundE_Polys:
  fixes F :: "(('x β‡’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)))"
        by (simp add: restrict_indets_times)
      also have "… ≀ poly_deg (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f))"
        by (rule poly_deg_restrict_indets_le)
      also have "… ≀ poly_deg g'" by (rule deg_le)
      also have "… ≀ b" by fact
      finally show "poly_deg ((restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f) ≀ b" .
    qed fact
  qed
qed

end (* pm_powerprod *)

end (* theory *)

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 addst lt f"
    by (rule GB_adds_lt)
  from assms(3) β€Ήg ∈ Gβ€Ί have "g ∈ phull (set ps)" ..
  from this β€Ήg β‰  0β€Ί obtain g' where "g' ∈ set (Macaulay_list ps)" and "g' β‰  0" and "lt g = lt g'"
    by (rule Macaulay_list_lt)
  show "βˆƒg∈set (Macaulay_list ps). g β‰  0 ∧ lt g addst lt f"
  proof (rule, rule)
    from β€Ήlt g addst lt fβ€Ί show "lt g' addst 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))"
  by (simp add: set_deg_shifts)

lemma deg_shifts_superset: "set fs βŠ† set (deg_shifts d fs)"
proof -
  have "set fs = (⋃f∈set fs. {punit.monom_mult 1 0 f})" by simp
  also have "… βŠ† set (deg_shifts d fs)" unfolding set_deg_shifts using subset_refl
  proof (rule UN_mono)
    fix f
    assume "f ∈ set fs"
    have "punit.monom_mult 1 0 f ∈ (λt. punit.monom_mult 1 t f) ` deg_le_sect X (d - poly_deg f)"
      using zero_in_deg_le_sect by (rule imageI)
    thus "{punit.monom_mult 1 0 f} βŠ† (Ξ»t. punit.monom_mult 1 t f) ` deg_le_sect X (d - poly_deg f)"
      by simp
  qed
  finally show ?thesis .
qed

lemma deg_shifts_mono:
  assumes "set fs βŠ† set gs"
  shows "set (deg_shifts d fs) βŠ† set (deg_shifts d gs)"
  using assms by (auto simp add: set_deg_shifts)

lemma ideal_deg_shifts [simp]: "ideal (set (deg_shifts d fs)) = ideal (set fs)"
proof
  show "ideal (set (deg_shifts d fs)) βŠ† ideal (set fs)"
    by (rule ideal.span_subset_spanI, simp add: set_deg_shifts UN_subset_iff,
        intro ballI image_subsetI) (metis ideal.span_scale times_monomial_left ideal.span_base)
next
  from deg_shifts_superset show "ideal (set fs) βŠ† ideal (set (deg_shifts d fs))"
    by (rule ideal.span_mono)
qed

lemma thm_2_3_6:
  assumes "set fs βŠ† P[X]" and "is_GB_cofactor_bound (set fs) b"
  shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts b fs)))"
proof -
  from assms(2) finite_set assms(1) obtain G where "punit.is_Groebner_basis G"
    and ideal_G: "ideal G = ideal (set fs)" and G_sub: "G βŠ† P[X]"
    and 1: "β‹€g. g ∈ G ⟹ βˆƒq. g = (βˆ‘f∈set fs. q f * f) ∧ (βˆ€f. q f ∈ P[X] ∧ poly_deg (q f * f) ≀ b)"
    by (rule is_GB_cofactor_boundE_finite_Polys) blast
  from this(1) show ?thesis
  proof (rule punit.Macaulay_list_is_GB)
    show "G βŠ† phull (set (deg_shifts b fs))" (is "_ βŠ† ?H")
    proof
      fix g
      assume "g ∈ G"
      hence "βˆƒq. g = (βˆ‘f∈set fs. q f * f) ∧ (βˆ€f. q f ∈ P[X] ∧ poly_deg (q f * f) ≀ b)" by (rule 1)
      then obtain q where g: "g = (βˆ‘f∈set fs. q f * f)" and "β‹€f. q f ∈ P[X]"
        and "β‹€f. poly_deg (q f * f) ≀ b" by blast
      show "g ∈ ?H" unfolding g
      proof (rule phull.span_sum)
        fix f
        assume "f ∈ set fs"
        have "1 β‰  (0::'a)" by simp
        show "q f * f ∈ ?H"
        proof (cases "f = 0 ∨ q f = 0")
          case True
          thus ?thesis by (auto simp add: phull.span_zero)
        next
          case False
          hence "q f β‰  0" and "f β‰  0" by simp_all
          with β€Ήpoly_deg (q f * f) ≀ bβ€Ί have "poly_deg (q f) ≀ b - poly_deg f"
            by (simp add: poly_deg_times)
          with β€Ήq f ∈ P[X]β€Ί have "keys (q f) βŠ† deg_le_sect X (b - poly_deg f)"
            by (rule keys_subset_deg_le_sectI)
          with finite_deg_le_sect[OF fin_X]
          have "q f * f = (βˆ‘t∈deg_le_sect X (b - poly_deg f). punit.monom_mult (lookup (q f) t) t f)"
            unfolding punit.mult_scalar_sum_monomials[simplified]
            by (rule sum.mono_neutral_left) (simp add: in_keys_iff)
          also have "… = (βˆ‘t∈deg_le_sect X (b - poly_deg f).
                              (lookup (q f) t) β‹… (punit.monom_mult 1 t f))"
            by (simp add: punit.monom_mult_assoc punit.map_scale_eq_monom_mult)
          also have "… = (βˆ‘t∈deg_le_sect X (b - poly_deg f).
                          ((Ξ»f0. (lookup (q f) (punit.lp f0 - punit.lp f)) β‹… f0) ∘
                          (Ξ»t. punit.monom_mult 1 t f)) t)"
            using refl by (rule sum.cong) (simp add: punit.lt_monom_mult[OF β€Ή1 β‰  0β€Ί β€Ήf β‰  0β€Ί])
          also have "… = (βˆ‘f0∈set (deg_shifts b [f]). (lookup (q f) (punit.lp f0 - punit.lp f)) β‹… f0)"
            unfolding set_deg_shifts_singleton
          proof (intro sum.reindex[symmetric] inj_onI)
            fix s t
            assume "punit.monom_mult 1 s f = punit.monom_mult 1 t f"
            thus "s = t" using β€Ή1 β‰  0β€Ί β€Ήf β‰  0β€Ί by (rule punit.monom_mult_inj_2)
          qed
          finally have "q f * f ∈ phull (set (deg_shifts b [f]))"
            by (simp add: phull.sum_in_spanI)
          also have "… βŠ† ?H" by (rule phull.span_mono, rule deg_shifts_mono, simp add: β€Ήf ∈ set fsβ€Ί)
          finally show ?thesis .
        qed
      qed
    qed
  qed (simp add: ideal_G)
qed

lemma thm_2_3_7:
  assumes "set fs βŠ† P[X]" and "is_GB_cofactor_bound (set fs) b"
  shows "1 ∈ ideal (set fs) ⟷ 1 ∈ set (punit.Macaulay_list (deg_shifts b fs))" (is "?L ⟷ ?R")
proof
  assume ?L
  let ?G = "set (punit.Macaulay_list (deg_shifts b fs))"
  from assms have "punit.is_Groebner_basis ?G" by (rule thm_2_3_6)
  moreover from β€Ή?Lβ€Ί have "1 ∈ ideal ?G" by (simp add: punit.pmdl_Macaulay_list[simplified])
  moreover have "1 β‰  (0::_ β‡’0 'a)" by simp
  ultimately obtain g where "g ∈ ?G" and "g β‰  0" and "punit.lt g adds punit.lt (1::_ β‡’0 'a)"
    by (rule punit.GB_adds_lt[simplified])
  from this(3) have lp_g: "punit.lt g = 0" by (simp add: punit.lt_monomial adds_zero flip: single_one)
  from punit.Macaulay_list_is_monic_set β€Ήg ∈ ?Gβ€Ί β€Ήg β‰  0β€Ί have lc_g: "punit.lc g = 1"
    by (rule punit.is_monic_setD)
  have "g = 1"
  proof (rule poly_mapping_eqI)
    fix t
    show "lookup g t = lookup 1 t"
    proof (cases "t = 0")
      case True
      thus ?thesis using lc_g by (simp add: lookup_one punit.lc_def lp_g)
    next
      case False
      with zero_min[of t] have "Β¬ t β‰Ό punit.lt g" by (simp add: lp_g)
      with punit.lt_max_keys have "t βˆ‰ keys g" by blast
      with False show ?thesis by (simp add: lookup_one in_keys_iff)
    qed
  qed
  with β€Ήg ∈ ?Gβ€Ί show "1 ∈ ?G" by simp
next
  assume ?R
  also have "… βŠ† phull (set (punit.Macaulay_list (deg_shifts b fs)))"
    by (rule phull.span_superset)
  also have "… = phull (set (deg_shifts b fs))" by (fact punit.phull_Macaulay_list)
  also have "… βŠ† ideal (set (deg_shifts b fs))" using punit.phull_subset_module by force
  finally show ?L by simp
qed

end

lemma thm_2_3_6_indets:
  assumes "is_GB_cofactor_bound (set fs) b"
  shows "punit.is_Groebner_basis (set (punit.Macaulay_list (deg_shifts (⋃(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"
  by (simp add: falling_fact_pochhammer pochhammer_minus')

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)"
  by (simp add: gbinomial_int_binomial)

corollary gbinomial_neg: "a < 0 ⟹ a gchoose k = (-1::int)^k * int ((k + (nat (- a)) - 1) choose k)"
  by (simp add: gbinomial_int_binomial)

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"
  by (simp add: gbinomial_int_binomial)

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"
        by (simp add: gbinomial_int_negated_upper[of a])
      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)"
    by (simp add: int_binomial add.commute)
  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)"
    proof (rule add_mono)
      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))"
    proof (rule add_mono)
      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))"
      by (simp add: eq algebra_simps)
    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)"
  by (simp add: pochhammer_prod)

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"
  by (simp add: is_monomial_set_def)

lemma is_monomial_setD: "is_monomial_set A ⟹ p ∈ A ⟹ is_monomial p"
  by (simp add: is_monomial_set_def)

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"
    by (simp only: single_add lookup_add)
  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 addst 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 addst 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}β€Ί)
    hence "lt f0 addst t" by (simp add: term_simps)
    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 addst 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 addst 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 addst 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 addst 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 addst t"
      by (rule keys_monomial_pmdl)
    from this(1) have "red G ?f f"
    proof (rule red_setI)
      from β€Ήlt g addst tβ€Ί have "component_of_term (lt g) = component_of_term t" and "lp g adds pp_of_term t"
        by (simp_all add: adds_term_def)
      from this have eq: "(pp_of_term t - lp g) βŠ• lt g = t"
        by (simp add: adds_minus splus_def term_of_pair_pair)
      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))"
          by (simp add: monom_mult_monomial eq)
        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
  assumes dgrad: "dickson_grading (d::'a β‡’ nat)"
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' addst 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 addst 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' addst lt f}"
    from dgrad fin_comps have "almost_full_on (addst) ?A" by (rule Dickson_term)
    moreover have "transp_on (addst) ?A" by (auto intro: transp_onI dest: adds_term_trans)
    ultimately have "wfp_on (strict (addst)) ?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)
      also from β€Ήq ∈ dgrad_p_set d mβ€Ί have "… βŠ† dgrad_set d m" by (simp add: dgrad_p_set_def)
      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 (addst) 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 addst lt f" by simp_all
    show ?thesis
    proof (rule that)
      {
        fix f'
        assume "f' ∈ F'"
        assume "lt f' addst lt g"
        hence "lt f' addst lt f" using adds by (rule adds_term_trans)
        with β€Ήf' ∈ F'β€Ί have "f' ∈ ?Q" by simp
        hence "lt f' ∈ lt ` ?Q" by (rule imageI)
        with t_min have "Β¬ strict (addst) (lt f') (lt g)" unfolding t by blast
        with β€Ήlt f' addst lt gβ€Ί have "lt g addst lt f'" by blast
        with β€Ήlt f' addst 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 addst t"
      by (rule keys_monomial_pmdl)
    from this(1, 2) obtain g where "g ∈ G" and "lt g addst lt f" by (rule 1)
    from this(2) have **: "lt g addst 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)
  note dgrad fin_comps F_sub
  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)
    from dgrad show "is_Groebner_basis G"
    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' addst 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)
      note dgrad
      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

corollary reduced_GB_is_monomial_set_dgrad_p_set: "is_monomial_set (reduced_GB F)"
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

lemma is_red_reduced_GB_monomial_dgrad_set:
  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 addst v"
      by (rule is_red_addsE)
    from this(1) have "f ∈ pmdl ?F" by (rule pmdl.span_base)
    from dgrad 1 2 have "is_Groebner_basis (reduced_GB ?F)" by (rule reduced_GB_is_GB_dgrad_p_set)
    moreover from β€Ήf ∈ pmdl ?Fβ€Ί dgrad 1 2 have "f ∈ pmdl (reduced_GB ?F)"
      by (simp only: reduced_GB_pmdl_dgrad_p_set)
    ultimately obtain g where "g ∈ reduced_GB ?F" and "g β‰  0" and "lt g addst lt f"
      using β€Ήf β‰  0β€Ί by (rule GB_adds_lt)
    from this(3) adds1 have "lt g addst v" by (rule adds_term_trans)
    with β€Ήg ∈ reduced_GB ?Fβ€Ί β€Ήg β‰  0β€Ί β€Ήv ∈ keys pβ€Ί show "is_red (reduced_GB ?F) p"
      by (rule is_red_addsI)
  qed
qed

corollary is_red_reduced_GB_monomial_lt_GB_dgrad_p_set:
  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

lemma reduced_GB_monomial_lt_reduced_GB_dgrad_p_set:
  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"
    by (rule reduced_GB_nonzero_dgrad_p_set, rule reduced_GB_is_auto_reduced_dgrad_p_set,
        rule finite_reduced_GB_dgrad_p_set)
  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' addst v"
        by (rule is_red_addsE)
      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"
      proof (rule is_red_addsI)
        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
        from adds1 show adds2: "lt g' addst lt g" by (simp add: v f' lt_monomial)
      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}"
  by (metis Suc_eq_plus1 le_Suc_ex sum.ub_add_nat)

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)"
  by (simp add: set_Cons_def)

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 (simp add: ys 1)
  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]"
  by (simp add: set_Cons_def)

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 (simp add: ys)
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 (simp add: ys1 ys2)
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"
  by (simp add: direct_decomp_def bij_betw_def)

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}"
    by (simp_all add: bij_betw_def lessThan_atLeast0)
  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})"
    by (simp add: image_mset_mset_set 2)
  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"
          by (simp_all add: len_qs2 len_qs)
        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 (simp add: qs_def a)
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]"
            by (simp add: k)
          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