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