Theory Card_Partitions.Set_Partition

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Set Partitions›

theory Set_Partition
imports
  "HOL-Library.Disjoint_Sets"
  "HOL-Library.FuncSet"
begin

subsection ‹Useful Additions to Main Theories›

lemma set_eqI':
  assumes "⋀x. x ∈ A ⟹ x ∈ B"
  assumes "⋀x. x ∈ B ⟹ x ∈ A"
  shows "A = B"
using assms by auto

lemma comp_image:
  "((`) f ∘ (`) g) = (`) (f o g)"
by rule auto

subsection ‹Introduction and Elimination Rules›

text ‹The definition of @{const partition_on} is in @{theory "HOL-Library.Disjoint_Sets"}.›

(* TODO: move the following theorems to Disjoint Sets *)

lemma partition_onI:
  assumes "⋀p. p ∈ P ⟹ p ≠ {}"
  assumes "⋃P = A"
  assumes "⋀p p'. p ∈ P ⟹ p' ∈ P ⟹ p ≠ p' ⟹ p ∩ p' = {}"
  shows "partition_on A P"
using assms unfolding partition_on_def disjoint_def by blast

lemma partition_onE:
  assumes "partition_on A P"
  obtains "⋀p. p ∈ P ⟹ p ≠ {}"
     "⋃P = A"
     "⋀p p'. p ∈ P ⟹ p' ∈ P ⟹ p ≠ p' ⟹ p ∩ p' = {}"
using assms unfolding partition_on_def disjoint_def by blast

subsection ‹Basic Facts on Set Partitions›

lemma partition_onD4: "partition_on A P ⟹ p ∈ P ⟹ q ∈ P ⟹ x ∈ p ⟹ x ∈ q ⟹ p = q"
  by (auto simp: partition_on_def disjoint_def)

lemma partition_subset_imp_notin:
  assumes "partition_on A P" "X ∈ P"
  assumes "X' ⊂ X"
  shows "X' ∉ P"
proof
  assume "X' ∈ P"
  from ‹X' ∈ P› ‹partition_on A P› have "X' ≠ {}"
    using partition_onD3 by blast
  moreover from ‹X' ∈ P› ‹X ∈ P› ‹partition_on A P› ‹X' ⊂ X› have "disjnt X X'"
    by (metis disjnt_def disjointD inf.strict_order_iff partition_onD2)
  moreover note ‹X' ⊂ X›
  ultimately show False
    by (meson all_not_in_conv disjnt_iff psubsetD)
qed

lemma partition_on_Diff:
  assumes P: "partition_on A P" shows "Q ⊆ P ⟹ partition_on (A - ⋃Q) (P - Q)"
  using P P[THEN partition_onD4] by (auto simp: partition_on_def disjoint_def)

lemma partition_on_UN:
  assumes A: "partition_on A B" and B: "⋀b. b ∈ B ⟹ partition_on b (P b)"
  shows "partition_on A (⋃b∈B. P b)"
proof (rule partition_onI)
  show "⋃(⋃b∈B. P b) = A"
    using B[THEN partition_onD1] A[THEN partition_onD1] by blast
next
  show "p ≠ {}" if "p ∈ (⋃b∈B. P b)" for p
    using B[THEN partition_onD3] that by auto
next
  fix p q assume "p ∈ (⋃i∈B. P i)" "q ∈ (⋃i∈B. P i)" and "p ≠ q"
  then obtain i j where i: "p ∈ P i" "i ∈ B" and j: "q ∈ P j" "j ∈ B"
    by auto
  show "p ∩ q = {}"
  proof cases
    assume "i = j" then show ?thesis
      using i j ‹p ≠ q› B[THEN partition_onD2, of i] by (simp add: disjointD)
  next
    assume "i ≠ j"
    then have "disjnt i j"
      using i j A[THEN partition_onD2] by (auto simp: pairwise_def)
    moreover have "p ⊆ i" "q ⊆ j"
      using B[THEN partition_onD1, of i, symmetric] B[THEN partition_onD1, of j, symmetric] i j by auto
    ultimately show ?thesis
      by (auto simp: disjnt_def)
  qed
qed

lemma partition_on_notemptyI:
  assumes "partition_on A P"
  assumes "A ≠ {}"
  shows "P ≠ {}"
using assms by (auto elim: partition_onE)

lemma partition_on_disjoint:
  assumes "partition_on A P"
  assumes "partition_on B Q"
  assumes "A ∩ B = {}"
  shows "P ∩ Q = {}"
using assms by (fastforce elim: partition_onE)

lemma partition_on_eq_implies_eq_carrier:
  assumes "partition_on A Q"
  assumes "partition_on B Q"
  shows "A = B"
using assms by (fastforce elim: partition_onE)

lemma partition_on_insert:
  assumes "partition_on A P"
  assumes "disjnt A X" "X ≠ {}"
  assumes "A ∪ X = A'"
  shows "partition_on A' (insert X P)"
using assms by (auto simp: partition_on_def disjoint_def disjnt_def)

text ‹An alternative formulation of @{thm partition_on_insert}›
lemma partition_on_insert':
  assumes "partition_on (A - X) P"
  assumes "X ⊆ A" "X ≠ {}"
  shows "partition_on A (insert X P)"
proof -
  have "disjnt (A - X) X" by (simp add: disjnt_iff)
  from assms(1) this assms(3) have "partition_on ((A - X) ∪ X) (insert X P)"
    by (auto intro: partition_on_insert)
  from this ‹X ⊆ A› show ?thesis
    by (metis Diff_partition sup_commute)
qed

lemma partition_on_insert_singleton:
  assumes "partition_on A P" "a ∉ A" "insert a A = A'"
  shows "partition_on A' (insert {a} P)"
using assms by (auto simp: partition_on_def disjoint_def disjnt_def)

lemma partition_on_remove_singleton:
  assumes "partition_on A P" "X ∈ P" "A - X = A'"
  shows "partition_on A' (P - {X})"
using assms partition_on_Diff by (metis Diff_cancel Diff_subset cSup_singleton insert_subset)

subsection ‹The Unique Part Containing an Element in a Set Partition›

lemma partition_on_partition_on_unique:
  assumes "partition_on A P"
  assumes "x ∈ A"
  shows "∃!X. x ∈ X ∧ X ∈ P"
proof -
  from ‹partition_on A P› have "⋃P = A"
    by (auto elim: partition_onE)
  from this ‹x ∈ A› obtain X where X: "x ∈ X ∧ X ∈ P" by blast
  {
    fix Y
    assume "x ∈ Y ∧ Y ∈ P"
    from this have "X = Y"
      using X ‹partition_on A P› by (meson partition_onE disjoint_iff_not_equal)
  }
  from this X show ?thesis by auto
qed

lemma partition_on_the_part_mem:
  assumes "partition_on A P"
  assumes "x ∈ A"
  shows "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
proof -
  from ‹x ∈ A› have "∃!X. x ∈ X ∧ X ∈ P"
    using ‹partition_on A P› by (simp add: partition_on_partition_on_unique)
  from this show "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
    by (metis (no_types, lifting) theI)
qed

lemma partition_on_in_the_unique_part:
  assumes "partition_on A P"
  assumes "x ∈ A"
  shows "x ∈ (THE X. x ∈ X ∧ X ∈ P)"
proof -
  from assms have "∃!X. x ∈ X ∧ X ∈ P"
    by (simp add: partition_on_partition_on_unique)
  from this show ?thesis
    by (metis (mono_tags, lifting) theI')
qed

lemma partition_on_the_part_eq:
  assumes "partition_on A P"
  assumes "x ∈ X" "X ∈ P"
  shows "(THE X. x ∈ X ∧ X ∈ P) = X"
proof -
  from ‹x ∈ X› ‹X ∈ P› have "x ∈ A"
    using ‹partition_on A P› by (auto elim: partition_onE)
  from this have "∃!X. x ∈ X ∧ X ∈ P"
    using ‹partition_on A P› by (simp add: partition_on_partition_on_unique)
  from ‹x ∈ X› ‹X ∈ P› this show "(THE X. x ∈ X ∧ X ∈ P) = X"
    by (auto intro!: the1_equality)
qed


lemma the_unique_part_alternative_def:
  assumes "partition_on A P"
  assumes "x ∈ A"
  shows "(THE X. x ∈ X ∧ X ∈ P) = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
proof
  show "(THE X. x ∈ X ∧ X ∈ P) ⊆ {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
  proof
    fix y
    assume "y ∈ (THE X. x ∈ X ∧ X ∈ P)"
    moreover from ‹x ∈ A› have "x ∈ (THE X. x ∈ X ∧ X ∈ P)"
      using ‹partition_on A P› partition_on_in_the_unique_part by force
    moreover from ‹x ∈ A› have "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
      using ‹partition_on A P› partition_on_the_part_mem by force
    ultimately show "y ∈ {y. ∃X∈P. x ∈ X ∧ y ∈ X}" by auto
  qed
next
  show "{y. ∃X∈P. x ∈ X ∧ y ∈ X} ⊆ (THE X. x ∈ X ∧ X ∈ P)"
  proof
    fix y
    assume "y ∈ {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
    from this obtain X where "x ∈ X" and "y ∈ X" and "X ∈ P" by auto
    from ‹x ∈ X› ‹X ∈ P› have "(THE X. x ∈ X ∧ X ∈ P) = X"
      using ‹partition_on A P› partition_on_the_part_eq by force
    from this ‹y ∈ X› show "y ∈ (THE X. x ∈ X ∧ X ∈ P)" by simp
  qed
qed

lemma partition_on_all_in_part_eq_part:
  assumes "partition_on A P"
  assumes "X' ∈ P"
  shows "{x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'} = X'"
proof
  show "{x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'} ⊆ X'"
    using assms(1) partition_on_in_the_unique_part by force
next
  show "X' ⊆ {x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'}"
  proof
    fix x
    assume "x ∈ X'"
    from ‹x ∈ X'› ‹X' ∈ P› have "x ∈ A"
      using ‹partition_on A P› by (auto elim: partition_onE)
    moreover from ‹x ∈ X'› ‹X' ∈ P› have "(THE X. x ∈ X ∧ X ∈ P) = X'"
      using ‹partition_on A P› partition_on_the_part_eq by fastforce
    ultimately show "x ∈ {x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'}" by auto
  qed
qed

lemma partition_on_part_characteristic:
  assumes "partition_on A P"
  assumes "X ∈ P" "x ∈ X"
  shows "X = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
proof -
  from ‹x ∈ X› ‹X ∈ P› have "x ∈ A"
    using ‹partition_on A P› partition_onE by blast
  from  ‹x ∈ X› ‹X ∈ P› have "X = (THE X. x ∈ X ∧ X ∈ P)"
    using ‹partition_on A P› by (simp add: partition_on_the_part_eq)
  also from ‹x ∈ A› have "(THE X. x ∈ X ∧ X ∈ P) = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
    using ‹partition_on A P› the_unique_part_alternative_def by force
  finally show ?thesis .
qed

lemma partition_on_no_partition_outside_carrier:
  assumes "partition_on A P"
  assumes "x ∉ A"
  shows "{y. ∃X∈P. x ∈ X ∧ y ∈ X} = {}"
using assms unfolding partition_on_def by auto

subsection ‹Cardinality of Parts in a Set Partition›

lemma partition_on_le_set_elements:
  assumes "finite A"
  assumes "partition_on A P"
  shows "card P ≤ card A"
using assms
proof (induct A arbitrary: P)
  case empty
  from this show "card P ≤ card {}" by (simp add: partition_on_empty)
next
  case (insert a A)
  show ?case
  proof (cases "{a} ∈ P")
    case True
    have prop_partition_on: "∀p∈P. p ≠ {}" "⋃P = insert a A"
      "∀p∈P. ∀p'∈P. p ≠ p' ⟶ p ∩ p' = {}"
      using ‹partition_on (insert a A) P› by (fastforce elim: partition_onE)+
    from this(2, 3) ‹a ∉ A› ‹{a} ∈ P› have A_eq: "A = ⋃(P - {{a}})"
      by auto (metis Int_iff UnionI empty_iff insert_iff)
    from prop_partition_on A_eq have partition_on: "partition_on A (P - {{a}})"
      by (intro partition_onI) auto
    from insert.hyps(3) this have "card (P - {{a}}) ≤ card A" by simp
    from this insert(1, 2, 4) ‹{a} ∈ P› show ?thesis
      using finite_elements[OF ‹finite A› partition_on] by simp
  next
    case False
    from ‹partition_on (insert a A) P› obtain p where p_def: "p ∈ P" "a ∈ p"
      by (blast elim: partition_onE)
    from ‹partition_on (insert a A) P› p_def have a_notmem: "∀p'∈ P - {p}. a ∉ p'"
      by (blast elim: partition_onE)
    from ‹partition_on (insert a A) P› p_def have "p - {a} ∉ P"
      unfolding partition_on_def disjoint_def
      by (metis Diff_insert_absorb Diff_subset inf.orderE mk_disjoint_insert)
    let ?P' = "insert (p - {a}) (P - {p})"
    have "partition_on A ?P'"
    proof (rule partition_onI)
      from ‹partition_on (insert a A) P› have "∀p∈P. p ≠ {}" by (auto elim: partition_onE)
      from this p_def ‹{a} ∉ P› show "⋀p'. p'∈insert (p - {a}) (P - {p}) ⟹ p' ≠ {}"
        by (simp; metis (no_types) Diff_eq_empty_iff subset_singletonD)
    next
      from ‹partition_on (insert a A) P› have "⋃P = insert a A" by (auto elim: partition_onE)
      from p_def this ‹a ∉ A› a_notmem show "⋃(insert (p - {a}) (P - {p})) = A" by auto
    next
      show "⋀pa pa'. pa∈insert (p - {a}) (P - {p}) ⟹ pa'∈insert (p - {a}) (P - {p}) ⟹ pa ≠ pa' ⟹ pa ∩ pa' = {}"
        using ‹partition_on (insert a A) P› p_def a_notmem
        unfolding partition_on_def disjoint_def
        by (metis disjoint_iff_not_equal insert_Diff insert_iff)
    qed
    have "finite P" using ‹finite A› ‹partition_on A ?P'› finite_elements by fastforce
    have "card P = Suc (card (P - {p}))"
      using p_def ‹finite P› card.remove by fastforce
    also have "… = card ?P'" using ‹p - {a} ∉ P› ‹finite P› by simp
    also have "… ≤ card A" using ‹partition_on A ?P'› insert.hyps(3) by simp
    also have "… ≤ card (insert a A)" by (simp add: card_insert_le ‹finite A› )
    finally show ?thesis .
  qed
qed

subsection ‹Operations on Set Partitions›

lemma partition_on_union:
  assumes "A ∩ B = {}"
  assumes "partition_on A P"
  assumes "partition_on B Q"
  shows "partition_on (A ∪ B) (P ∪ Q)"
proof (rule partition_onI)
  fix X
  assume "X ∈ P ∪ Q"
  from this ‹partition_on A P› ‹partition_on B Q› show "X ≠ {}"
    by (auto elim: partition_onE)
next
  show "⋃(P ∪ Q) = A ∪ B"
    using ‹partition_on A P› ‹partition_on B Q› by (auto elim: partition_onE)
next
  fix X Y
  assume "X ∈ P ∪ Q" "Y ∈ P ∪ Q" "X ≠ Y"
  from this assms show "X ∩ Y = {}"
    by (elim UnE partition_onE) auto
qed

lemma partition_on_split1:
  assumes "partition_on A (P ∪ Q)"
  shows "partition_on (⋃P) P"
proof (rule partition_onI)
  fix p
  assume "p ∈ P"
  from this assms show "p ≠ {}"
    using Un_iff partition_onE by auto
next
  show "⋃P = ⋃P" ..
next
  fix p p'
  assume a: "p ∈ P" "p' ∈ P" "p ≠ p'"
  from this assms show "p ∩ p' = {}"
    using partition_onE subsetCE sup_ge1 by blast
qed

lemma partition_on_split2:
  assumes "partition_on A (P ∪ Q)"
  shows "partition_on (⋃Q) Q"
using assms partition_on_split1 sup_commute by metis

lemma partition_on_intersect_on_elements:
  assumes "partition_on (A ∪ C) P"
  assumes "∀X ∈ P. ∃x. x ∈ X ∩ C"
  shows "partition_on C ((λX. X ∩ C) ` P)"
proof (rule partition_onI)
  fix p
  assume "p ∈ (λX. X ∩ C) ` P"
  from this assms show "p ≠ {}" by auto
next
  have "⋃P = A ∪ C"
    using assms by (auto elim: partition_onE)
  from this show "⋃((λX. X ∩ C) ` P) = C" by auto
next
  fix p p'
  assume "p ∈ (λX. X ∩ C) ` P" "p' ∈ (λX. X ∩ C) ` P" "p ≠ p'"
  from this assms(1) show "p ∩ p' = {}"
    by (blast elim: partition_onE)
qed

lemma partition_on_insert_elements:
  assumes "A ∩ B = {}"
  assumes "partition_on B P"
  assumes "f ∈ A →⇩E P"
  shows "partition_on (A ∪ B) ((λX. X ∪ {x ∈ A. f x = X}) ` P)" (is "partition_on _ ?P")
proof (rule partition_onI)
  fix X
  assume "X ∈ ?P"
  from this ‹partition_on B P› show "X ≠ {}"
    by (auto elim: partition_onE)
next
  show "⋃?P = A ∪ B"
    using ‹partition_on B P› ‹f ∈ A →⇩E P› by (auto elim: partition_onE)
next
  fix X Y
  assume "X ∈ ?P" "Y ∈ ?P" "X ≠ Y"
  from ‹X ∈ ?P› obtain X' where X': "X = X' ∪ {x ∈ A. f x = X'}" "X' ∈ P" by auto
  from ‹Y ∈ ?P› obtain Y' where Y': "Y = Y' ∪ {x ∈ A. f x = Y'}" "Y' ∈ P" by auto
  from ‹X ≠ Y› X' Y' have "X' ≠ Y'" by auto
  from this X' Y' have "X' ∩ Y' = {}"
    using ‹partition_on B P› by (auto elim!: partition_onE)
  from X' Y' have "X' ⊆ B" "Y' ⊆ B"
    using ‹partition_on B P› by (auto elim!: partition_onE)
  from this ‹X' ∩ Y' = {}› X' Y' ‹X' ≠ Y'› show "X ∩ Y = {}"
    using ‹A ∩ B = {}› by auto
qed

lemma partition_on_map:
  assumes "inj_on f A"
  assumes "partition_on A P"
  shows "partition_on (f ` A) ((`) f ` P)"
proof -
  {
    fix X Y
    assume "X ∈ P" "Y ∈ P" "f ` X ≠ f ` Y"
    moreover from assms have "∀p∈P. ∀p'∈P. p ≠ p' ⟶ p ∩ p' = {}" and "inj_on f (⋃P)"
      by (auto elim!: partition_onE)
    ultimately have "f ` X ∩ f ` Y = {}"
      unfolding inj_on_def by auto (metis IntI empty_iff rev_image_eqI)+
  }
  from assms this show "partition_on (f ` A) ((`) f ` P)"
    by (auto intro!: partition_onI elim!: partition_onE)
qed

lemma set_of_partition_on_map:
  assumes "inj_on f A"
  shows "(`) ((`) f) ` {P. partition_on A P} = {P. partition_on (f ` A) P}"
proof (rule set_eqI')
  fix x
  assume "x ∈ (`) ((`) f) ` {P. partition_on A P}"
  from this ‹inj_on f A› show "x ∈ {P. partition_on (f ` A) P}"
    by (auto intro: partition_on_map)
next
  fix P
  assume "P ∈ {P. partition_on (f ` A) P}"
  from this have "partition_on (f ` A) P" by auto
  from this have mem: "⋀X x. X ∈ P ⟹ x ∈ X ⟹ x ∈ f ` A"
    by (auto elim!: partition_onE)
  have "(`) (f ∘ the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P"
    by (simp add: image_image cong: image_cong_simp)
  moreover have "P = (`) (f ∘ the_inv_into A f) ` P"
  proof (rule set_eqI')
    fix X
    assume X: "X ∈ P"
    moreover from X mem have in_range: "∀x∈X. x ∈ f ` A" by auto
    moreover have "X = (f ∘ the_inv_into A f) ` X"
    proof (rule set_eqI')
      fix x
      assume "x ∈ X"
      show "x ∈ (f ∘ the_inv_into A f) ` X"
      proof (rule image_eqI)
        from in_range ‹x ∈ X› assms show "x = (f ∘ the_inv_into A f) x"
          by (auto simp add: f_the_inv_into_f[of f])
        from ‹x ∈ X› show "x ∈ X" by assumption
      qed
    next
      fix x
      assume "x ∈ (f ∘ the_inv_into A f) ` X"
      from this obtain x' where x': "x' ∈ X ∧ x = f (the_inv_into A f x')" by auto
      from in_range x' have f: "f (the_inv_into A f x') ∈ X"
        by (subst f_the_inv_into_f[of f]) (auto intro: ‹inj_on f A›)
      from x' ‹X ∈ P› f show "x ∈ X" by auto
    qed
    ultimately show "X ∈ (`) (f ∘ the_inv_into A f) ` P" by auto
  next
    fix X
    assume "X ∈ (`) (f ∘ the_inv_into A f) ` P"
    moreover
    {
      fix Y
      assume "Y ∈ P"
      from this ‹inj_on f A› mem have "∀x∈Y. f (the_inv_into A f x) = x"
        by (auto simp add: f_the_inv_into_f)
      from this have "(f ∘ the_inv_into A f) ` Y = Y" by force
    }
    ultimately show "X ∈ P" by auto
  qed
  ultimately have P: "P = (`) f ` (`) (the_inv_into A f) ` P" by simp
  have A_eq: "A = the_inv_into A f ` f ` A" by (simp add: assms)
  from ‹inj_on f A› have "inj_on (the_inv_into A f) (f ` A)"
    using ‹partition_on (f ` A) P› by (simp add: inj_on_the_inv_into)
  from this have  "(`) (the_inv_into A f) ` P ∈ {P. partition_on A P}"
    using ‹partition_on (f ` A) P› by (subst A_eq, auto intro!: partition_on_map)
  from P this show "P ∈ (`) ((`) f) ` {P. partition_on A P}" by (rule image_eqI)
qed

end