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