60727
|
1 |
(* Title: HOL/Library/Disjoint_Sets.thy
|
|
2 |
Author: Johannes Hölzl, TU München
|
|
3 |
*)
|
|
4 |
|
|
5 |
section \<open>Handling Disjoint Sets\<close>
|
|
6 |
|
|
7 |
theory Disjoint_Sets
|
|
8 |
imports Main
|
|
9 |
begin
|
|
10 |
|
|
11 |
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
|
|
12 |
by blast
|
|
13 |
|
|
14 |
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
|
|
15 |
by blast
|
|
16 |
|
|
17 |
lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
|
|
18 |
by blast
|
|
19 |
|
|
20 |
lemma mono_Un: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
|
|
21 |
unfolding mono_def by auto
|
|
22 |
|
|
23 |
subsection \<open>Set of Disjoint Sets\<close>
|
|
24 |
|
|
25 |
definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
|
|
26 |
|
|
27 |
lemma disjointI:
|
|
28 |
"(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
|
|
29 |
unfolding disjoint_def by auto
|
|
30 |
|
|
31 |
lemma disjointD:
|
|
32 |
"disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
|
|
33 |
unfolding disjoint_def by auto
|
|
34 |
|
|
35 |
lemma disjoint_empty[iff]: "disjoint {}"
|
|
36 |
by (auto simp: disjoint_def)
|
|
37 |
|
|
38 |
lemma disjoint_INT:
|
|
39 |
assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
|
|
40 |
shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
|
|
41 |
proof (safe intro!: disjointI del: equalityI)
|
|
42 |
fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)"
|
|
43 |
then obtain i where "A i \<noteq> B i" "i \<in> I"
|
|
44 |
by auto
|
|
45 |
moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
|
|
46 |
ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
|
|
47 |
using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
|
|
48 |
by (auto simp: INT_Int_distrib[symmetric])
|
|
49 |
qed
|
|
50 |
|
|
51 |
lemma disjoint_singleton[simp]: "disjoint {A}"
|
|
52 |
by(simp add: disjoint_def)
|
|
53 |
|
|
54 |
subsubsection "Family of Disjoint Sets"
|
|
55 |
|
|
56 |
definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
|
|
57 |
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
|
|
58 |
|
|
59 |
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
|
|
60 |
|
|
61 |
lemma disjoint_family_onD:
|
|
62 |
"disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
|
|
63 |
by (auto simp: disjoint_family_on_def)
|
|
64 |
|
|
65 |
lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
|
|
66 |
by (force simp add: disjoint_family_on_def)
|
|
67 |
|
|
68 |
lemma disjoint_family_on_bisimulation:
|
|
69 |
assumes "disjoint_family_on f S"
|
|
70 |
and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}"
|
|
71 |
shows "disjoint_family_on g S"
|
|
72 |
using assms unfolding disjoint_family_on_def by auto
|
|
73 |
|
|
74 |
lemma disjoint_family_on_mono:
|
|
75 |
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A"
|
|
76 |
unfolding disjoint_family_on_def by auto
|
|
77 |
|
|
78 |
lemma disjoint_family_Suc:
|
|
79 |
"(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
|
|
80 |
using lift_Suc_mono_le[of A]
|
|
81 |
by (auto simp add: disjoint_family_on_def)
|
|
82 |
(metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
|
|
83 |
|
|
84 |
lemma disjoint_family_on_disjoint_image:
|
|
85 |
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
|
|
86 |
unfolding disjoint_family_on_def disjoint_def by force
|
|
87 |
|
|
88 |
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I"
|
|
89 |
by (auto simp: disjoint_family_on_def)
|
|
90 |
|
|
91 |
lemma disjoint_image_disjoint_family_on:
|
|
92 |
assumes d: "disjoint (A ` I)" and i: "inj_on A I"
|
|
93 |
shows "disjoint_family_on A I"
|
|
94 |
unfolding disjoint_family_on_def
|
|
95 |
proof (intro ballI impI)
|
|
96 |
fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m"
|
|
97 |
with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}"
|
|
98 |
by (intro disjointD[OF d]) auto
|
|
99 |
qed
|
|
100 |
|
|
101 |
lemma disjoint_UN:
|
|
102 |
assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
|
|
103 |
shows "disjoint (\<Union>i\<in>I. F i)"
|
|
104 |
proof (safe intro!: disjointI del: equalityI)
|
|
105 |
fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
|
|
106 |
show "A \<inter> B = {}"
|
|
107 |
proof cases
|
|
108 |
assume "i = j" with F[of i] \<open>i \<in> I\<close> \<open>A \<in> F i\<close> \<open>B \<in> F j\<close> \<open>A \<noteq> B\<close> show "A \<inter> B = {}"
|
|
109 |
by (auto dest: disjointD)
|
|
110 |
next
|
|
111 |
assume "i \<noteq> j"
|
|
112 |
with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
|
|
113 |
by (rule disjoint_family_onD)
|
|
114 |
with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
|
|
115 |
show "A \<inter> B = {}"
|
|
116 |
by auto
|
|
117 |
qed
|
|
118 |
qed
|
|
119 |
|
|
120 |
lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)"
|
|
121 |
using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
|
|
122 |
|
|
123 |
subsection \<open>Construct Disjoint Sequences\<close>
|
|
124 |
|
|
125 |
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where
|
|
126 |
"disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
|
|
127 |
|
|
128 |
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
|
|
129 |
proof (induct n)
|
|
130 |
case 0 show ?case by simp
|
|
131 |
next
|
|
132 |
case (Suc n)
|
|
133 |
thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
|
|
134 |
qed
|
|
135 |
|
|
136 |
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
|
|
137 |
by (rule UN_finite2_eq [where k=0])
|
|
138 |
(simp add: finite_UN_disjointed_eq)
|
|
139 |
|
|
140 |
lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
|
|
141 |
by (auto simp add: disjointed_def)
|
|
142 |
|
|
143 |
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
|
|
144 |
by (simp add: disjoint_family_on_def)
|
|
145 |
(metis neq_iff Int_commute less_disjoint_disjointed)
|
|
146 |
|
|
147 |
lemma disjointed_subset: "disjointed A n \<subseteq> A n"
|
|
148 |
by (auto simp add: disjointed_def)
|
|
149 |
|
|
150 |
lemma disjointed_0[simp]: "disjointed A 0 = A 0"
|
|
151 |
by (simp add: disjointed_def)
|
|
152 |
|
|
153 |
lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
|
|
154 |
using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
|
|
155 |
|
|
156 |
end |