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_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_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)
  with assms have "count_list zs x ≠ 0" by simp
  hence "x ∈ set zs" by (simp only: count_list_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 *)