Theory Set_Util

theory Set_Util
  imports Main
begin

section ‹Sets›

lemma pigeonhole_principle_advanced:
  assumes "finite A"
  and     "finite B"
  and     "A ∩ B = {}"
  and     "card A > card B"
  and     "bij_betw f (A ∪ B) (A ∪ B)"
shows " ∃a∈A. f a ∈ A"
proof (rule ccontr)
  assume "¬(∃a∈A. f a ∈ A)"
  hence "∀a ∈ A. f a ∉ A"
    by blast
  hence "∀a∈A. f a ∈ B"
    using assms(5) bij_betw_apply by fastforce
  hence "f ` A ⊆ B"
    by blast

  have "inj_on f A"
    by (meson assms(5) bij_betw_def inj_on_Un)
  hence "card (f ` A) = card A"
    using card_image by blast
  hence "f ` A = B"
    by (metis ‹f ` A ⊆ B› assms(2,4) card_mono leD)
  hence "card B = card A"
    using ‹card (f ` A) = card A› by blast
  then show False
    using assms(4) by linarith
qed

lemma Suc_mod_n_bij_betw:
  "bij_betw (λx. Suc x mod n) {0..<n} {0..<n}"
proof (intro bij_betwI')
  fix x y
  assume "x ∈ {0..<n}" "y ∈ {0..<n}"
  then show "(Suc x mod n = Suc y mod n) = (x = y)"
    by (simp add: mod_Suc)
next
  fix x
  assume "x ∈ {0..<n}"
  then show "Suc x mod n ∈ {0..<n}"
    by clarsimp
next
  fix y
  assume "y ∈ {0..<n}"
  then show "∃x∈{0..<n}. y = Suc x mod n"
    by (metis atLeastLessThan_iff bot_nat_0.extremum less_nat_zero_code mod_Suc_eq mod_less
              mod_less_divisor mod_self not_gr_zero old.nat.exhaust)
qed



lemma subset_upt_no_Suc:
  assumes "A ⊆ {1..<n}"
  and     "∀x∈A. Suc x ∉ A"
  shows "card A ≤ n div 2"
proof (rule ccontr)
  assume "¬ card A ≤ n div 2"
  hence "n div 2 < card A"
    by auto

  have "∃a∈A. Suc a mod n ∈ A"
  proof (rule pigeonhole_principle_advanced[of A "{0..<n} - A" "(λx. Suc x mod n)", simplified])
    show "finite A"
      using assms(1) finite_subset by blast
  next
    from card_Diff_subset
    have "card ({0..<n} - A) = card {0..<n} - card A"
      by (metis Diff_subset assms(1) dual_order.trans ivl_diff less_eq_nat.simps(1)
                subset_eq_atLeast0_lessThan_finite)
    moreover
    have "card {0..<n} - card A < card A"
      using ‹¬ card A ≤ n div 2› assms by simp
    ultimately show "card ({0..<n} - A) < card A"
      by simp
  next
    have "A ∪ {0..<n} = {0..<n}"
      using assms(1) dual_order.trans by auto
    with Suc_mod_n_bij_betw[of n]
    show "bij_betw (λx. Suc x mod n) (A ∪ {0..<n}) (A ∪ {0..<n})"
      by simp
  qed
  then obtain x where
    "x ∈ A"
    "Suc x mod n ∈ A"
    by blast

  show False
  proof (cases n)
    case 0
    then show ?thesis
      using ‹Suc x mod n ∈ A› ‹x ∈ A› assms(2) by force
  next
    case (Suc m)
    assume "n = Suc m"

    have "x = m ∨ x < m"
      using Suc ‹x ∈ A› assms(1) by auto
    then show ?thesis
    proof
      assume "x = m"
      then show False
        using Suc ‹Suc x mod n ∈ A› assms(1) by auto
    next
      assume "x < m"
      with mod_less[of "Suc x" "Suc m"]
      show False
        using Suc ‹Suc x mod n ∈ A› ‹x ∈ A› assms(2) by force
    qed
  qed
qed

lemma in_set_mapD:
  "x ∈ set (map f xs) ⟹ ∃y ∈ set xs. x = f y"
  by (simp add: image_iff)

(*****************************)

subsection ‹From AutoCorres ›

lemma disjointI':
  assumes "⋀x y. ⟦ x ∈ A; y ∈ B ⟧ ⟹ x ≠ y"
  shows " A ∩ B = {}"
  using assms by fast

lemma disjoint_subset2:
  assumes "B' ⊆ B" and "A ∩ B = {}"
  shows   "A ∩ B' = {}"
  using assms by fast

(*****************************)

end