(* Title: HOL/Library/Disjoint_Sets.thy
Author: Johannes Hölzl, TU München
*)
section \Partitions and Disjoint Sets\
theory Disjoint_Sets
imports Main
begin
lemma range_subsetD: "range f \ B \ f i \ B"
by blast
lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}"
by blast
lemma Int_Diff_Un: "A \ B \ (A - B) = A"
by blast
lemma mono_Un: "mono A \ (\i\n. A i) = A n"
unfolding mono_def by auto
lemma disjnt_equiv_class: "equiv A r \ disjnt (r``{a}) (r``{b}) \ (a, b) \ r"
by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
subsection \Set of Disjoint Sets\
abbreviation disjoint :: "'a set set \ bool" where "disjoint \ pairwise disjnt"
lemma disjoint_def: "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})"
unfolding pairwise_def disjnt_def by auto
lemma disjointI:
"(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A"
unfolding disjoint_def by auto
lemma disjointD:
"disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}"
unfolding disjoint_def by auto
lemma disjoint_image: "inj_on f (\A) \ disjoint A \ disjoint ((`) f ` A)"
unfolding inj_on_def disjoint_def by blast
lemma assumes "disjoint (A \ B)"
shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B"
using assms by (simp_all add: disjoint_def)
lemma disjoint_INT:
assumes *: "\i. i \ I \ disjoint (F i)"
shows "disjoint {\i\I. X i | X. \i\I. X i \ F i}"
proof (safe intro!: disjointI del: equalityI)
fix A B :: "'a \ 'b set" assume "(\i\I. A i) \ (\i\I. B i)"
then obtain i where "A i \ B i" "i \ I"
by auto
moreover assume "\i\I. A i \ F i" "\i\I. B i \ F i"
ultimately show "(\i\I. A i) \ (\i\I. B i) = {}"
using *[OF \i\I\, THEN disjointD, of "A i" "B i"]
by (auto simp: INT_Int_distrib[symmetric])
qed
subsubsection "Family of Disjoint Sets"
definition disjoint_family_on :: "('i \ 'a set) \ 'i set \ bool" where
"disjoint_family_on A S \ (\m\S. \n\S. m \ n \ A m \ A n = {})"
abbreviation "disjoint_family A \ disjoint_family_on A UNIV"
lemma disjoint_family_elem_disjnt:
assumes "infinite A" "finite C"
and df: "disjoint_family_on B A"
obtains x where "x \ A" "disjnt C (B x)"
proof -
have "False" if *: "\x \ A. \y. y \ C \ y \ B x"
proof -
obtain g where g: "\x \ A. g x \ C \ g x \ B x"
using * by metis
with df have "inj_on g A"
by (fastforce simp add: inj_on_def disjoint_family_on_def)
then have "infinite (g ` A)"
using \infinite A\ finite_image_iff by blast
then show False
by (meson \finite C\ finite_subset g image_subset_iff)
qed
then show ?thesis
by (force simp: disjnt_iff intro: that)
qed
lemma disjoint_family_onD:
"disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}"
by (auto simp: disjoint_family_on_def)
lemma disjoint_family_subset: "disjoint_family A \ (\x. B x \ A x) \ disjoint_family B"
by (force simp add: disjoint_family_on_def)
lemma disjoint_family_on_bisimulation:
assumes "disjoint_family_on f S"
and "\n m. n \ S \ m \ S \ n \ m \ f n \ f m = {} \ g n \ g m = {}"
shows "disjoint_family_on g S"
using assms unfolding disjoint_family_on_def by auto
lemma disjoint_family_on_mono:
"A \ B \ disjoint_family_on f B \ disjoint_family_on f A"
unfolding disjoint_family_on_def by auto
lemma disjoint_family_Suc:
"(\n. A n \ A (Suc n)) \ disjoint_family (\i. A (Suc i) - A i)"
using lift_Suc_mono_le[of A]
by (auto simp add: disjoint_family_on_def)
(metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
lemma disjoint_family_on_disjoint_image:
"disjoint_family_on A I \ disjoint (A ` I)"
unfolding disjoint_family_on_def disjoint_def by force
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \ disjoint_family_on (\i. f -` F i) I"
by (auto simp: disjoint_family_on_def)
lemma disjoint_image_disjoint_family_on:
assumes d: "disjoint (A ` I)" and i: "inj_on A I"
shows "disjoint_family_on A I"
unfolding disjoint_family_on_def
proof (intro ballI impI)
fix n m assume nm: "m \ I" "n \ I" and "n \ m"
with i[THEN inj_onD, of n m] show "A n \ A m = {}"
by (intro disjointD[OF d]) auto
qed
lemma disjoint_UN:
assumes F: "\i. i \ I \ disjoint (F i)" and *: "disjoint_family_on (\i. \F i) I"
shows "disjoint (\i\I. F i)"
proof (safe intro!: disjointI del: equalityI)
fix A B i j assume "A \ B" "A \ F i" "i \ I" "B \ F j" "j \ I"
show "A \ B = {}"
proof cases
assume "i = j" with F[of i] \i \ I\ \A \ F i\ \B \ F j\ \A \ B\ show "A \ B = {}"
by (auto dest: disjointD)
next
assume "i \ j"
with * \i\I\ \j\I\ have "(\F i) \ (\F j) = {}"
by (rule disjoint_family_onD)
with \A\F i\ \i\I\ \B\F j\ \j\I\
show "A \ B = {}"
by auto
qed
qed
lemma distinct_list_bind:
assumes "distinct xs" "\x. x \ set xs \ distinct (f x)"
"disjoint_family_on (set \ f) (set xs)"
shows "distinct (List.bind xs f)"
using assms
by (induction xs)
(auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind)
lemma bij_betw_UNION_disjoint:
assumes disj: "disjoint_family_on A' I"
assumes bij: "\i. i \ I \ bij_betw f (A i) (A' i)"
shows "bij_betw f (\i\I. A i) (\i\I. A' i)"
unfolding bij_betw_def
proof
from bij show eq: "f ` UNION I A = UNION I A'"
by (auto simp: bij_betw_def image_UN)
show "inj_on f (UNION I A)"
proof (rule inj_onI, clarify)
fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y"
from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j"
by (auto simp: bij_betw_def)
with B have "A' i \ A' j \ {}" by auto
with disj A have "i = j" unfolding disjoint_family_on_def by blast
with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD)
qed
qed
lemma disjoint_union: "disjoint C \ disjoint B \ \C \ \B = {} \ disjoint (C \ B)"
using disjoint_UN[of "{C, B}" "\x. x"] by (auto simp add: disjoint_family_on_def)
text \
The union of an infinite disjoint family of non-empty sets is infinite.
\
lemma infinite_disjoint_family_imp_infinite_UNION:
assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A"
shows "\finite (UNION A f)"
proof -
define g where "g x = (SOME y. y \ f x)" for x
have g: "g x \ f x" if "x \ A" for x
unfolding g_def by (rule someI_ex, insert assms(2) that) blast
have inj_on_g: "inj_on g A"
proof (rule inj_onI, rule ccontr)
fix x y assume A: "x \ A" "y \ A" "g x = g y" "x \ y"
with g[of x] g[of y] have "g x \ f x" "g x \ f y" by auto
with A \x \ y\ assms show False
by (auto simp: disjoint_family_on_def inj_on_def)
qed
from g have "g ` A \ UNION A f" by blast
moreover from inj_on_g \\finite A\ have "\finite (g ` A)"
using finite_imageD by blast
ultimately show ?thesis using finite_subset by blast
qed
subsection \Construct Disjoint Sequences\
definition disjointed :: "(nat \ 'a set) \ nat \ 'a set" where
"disjointed A n = A n - (\i\{0..i\{0..i\{0..i. disjointed A i) = (\i. A i)"
by (rule UN_finite2_eq [where k=0])
(simp add: finite_UN_disjointed_eq)
lemma less_disjoint_disjointed: "m < n \