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 (bB. P b)"
proof (rule partition_onI)
  show "(bB. P b) = A"
    using B[THEN partition_onD1] A[THEN partition_onD1] by blast
next
  show "p  {}" if "p  (bB. P b)" for p
    using B[THEN partition_onD3] that by auto
next
  fix p q assume "p  (iB. P i)" "q  (iB. 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. XP. x  X  y  X}"
proof
  show "(THE X. x  X  X  P)  {y. XP. 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. XP. x  X  y  X}" by auto
  qed
next
  show "{y. XP. x  X  y  X}  (THE X. x  X  X  P)"
  proof
    fix y
    assume "y  {y. XP. 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. XP. 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. XP. 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. XP. 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: "pP. p  {}" "P = insert a A"
      "pP. 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 "pP. 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'. painsert (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 "pP. 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: "xX. 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 "xY. 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