section ‹Handling 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
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_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_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 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)
subsection ‹Construct Disjoint Sequences›
definition disjointed :: "(nat ⇒ 'a set) ⇒ nat ⇒ 'a set" where
"disjointed A n = A n - (⋃i∈{0..<n}. A i)"
lemma finite_UN_disjointed_eq: "(⋃i∈{0..<n}. disjointed A i) = (⋃i∈{0..<n}. A i)"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
qed
lemma UN_disjointed_eq: "(⋃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 ⟹ disjointed A m ∩ disjointed A n = {}"
by (auto simp add: disjointed_def)
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
by (simp add: disjoint_family_on_def)
(metis neq_iff Int_commute less_disjoint_disjointed)
lemma disjointed_subset: "disjointed A n ⊆ A n"
by (auto simp add: disjointed_def)
lemma disjointed_0[simp]: "disjointed A 0 = A 0"
by (simp add: disjointed_def)
lemma disjointed_mono: "mono A ⟹ disjointed A (Suc n) = A (Suc n) - A n"
using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
end