author | eberlm |
Tue, 17 May 2016 17:05:35 +0200 | |
changeset 63099 | af0e964aad7b |
parent 62843 | 313d3b697c9a |
child 63100 | aa5cffd8a606 |
permissions | -rw-r--r-- |
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 |
||
62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset
|
25 |
abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt" |
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset
|
26 |
|
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset
|
27 |
lemma disjoint_def: "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})" |
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset
|
28 |
unfolding pairwise_def disjnt_def by auto |
60727 | 29 |
|
30 |
lemma disjointI: |
|
31 |
"(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A" |
|
32 |
unfolding disjoint_def by auto |
|
33 |
||
34 |
lemma disjointD: |
|
35 |
"disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}" |
|
36 |
unfolding disjoint_def by auto |
|
37 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
38 |
lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
39 |
unfolding inj_on_def disjoint_def by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
40 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
41 |
lemma assumes "disjoint (A \<union> B)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
42 |
shows disjoint_unionD1: "disjoint A" and disjoint_unionD2: "disjoint B" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
43 |
using assms by (simp_all add: disjoint_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
44 |
|
60727 | 45 |
lemma disjoint_INT: |
46 |
assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" |
|
47 |
shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}" |
|
48 |
proof (safe intro!: disjointI del: equalityI) |
|
49 |
fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)" |
|
50 |
then obtain i where "A i \<noteq> B i" "i \<in> I" |
|
51 |
by auto |
|
52 |
moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i" |
|
53 |
ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}" |
|
54 |
using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"] |
|
55 |
by (auto simp: INT_Int_distrib[symmetric]) |
|
56 |
qed |
|
57 |
||
58 |
subsubsection "Family of Disjoint Sets" |
|
59 |
||
60 |
definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |
|
61 |
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" |
|
62 |
||
63 |
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV" |
|
64 |
||
65 |
lemma disjoint_family_onD: |
|
66 |
"disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
|
67 |
by (auto simp: disjoint_family_on_def) |
|
68 |
||
69 |
lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B" |
|
70 |
by (force simp add: disjoint_family_on_def) |
|
71 |
||
72 |
lemma disjoint_family_on_bisimulation: |
|
73 |
assumes "disjoint_family_on f S" |
|
74 |
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 = {}" |
|
75 |
shows "disjoint_family_on g S" |
|
76 |
using assms unfolding disjoint_family_on_def by auto |
|
77 |
||
78 |
lemma disjoint_family_on_mono: |
|
79 |
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A" |
|
80 |
unfolding disjoint_family_on_def by auto |
|
81 |
||
82 |
lemma disjoint_family_Suc: |
|
83 |
"(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)" |
|
84 |
using lift_Suc_mono_le[of A] |
|
85 |
by (auto simp add: disjoint_family_on_def) |
|
61824
dcbe9f756ae0
not_leE -> not_le_imp_less and other tidying
paulson <lp15@cam.ac.uk>
parents:
60727
diff
changeset
|
86 |
(metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le) |
60727 | 87 |
|
88 |
lemma disjoint_family_on_disjoint_image: |
|
89 |
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)" |
|
90 |
unfolding disjoint_family_on_def disjoint_def by force |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
91 |
|
60727 | 92 |
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I" |
93 |
by (auto simp: disjoint_family_on_def) |
|
94 |
||
95 |
lemma disjoint_image_disjoint_family_on: |
|
96 |
assumes d: "disjoint (A ` I)" and i: "inj_on A I" |
|
97 |
shows "disjoint_family_on A I" |
|
98 |
unfolding disjoint_family_on_def |
|
99 |
proof (intro ballI impI) |
|
100 |
fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m" |
|
101 |
with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}" |
|
102 |
by (intro disjointD[OF d]) auto |
|
103 |
qed |
|
104 |
||
105 |
lemma disjoint_UN: |
|
106 |
assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I" |
|
107 |
shows "disjoint (\<Union>i\<in>I. F i)" |
|
108 |
proof (safe intro!: disjointI del: equalityI) |
|
109 |
fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I" |
|
110 |
show "A \<inter> B = {}" |
|
111 |
proof cases |
|
112 |
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 = {}" |
|
113 |
by (auto dest: disjointD) |
|
114 |
next |
|
115 |
assume "i \<noteq> j" |
|
116 |
with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}" |
|
117 |
by (rule disjoint_family_onD) |
|
118 |
with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close> |
|
119 |
show "A \<inter> B = {}" |
|
120 |
by auto |
|
121 |
qed |
|
122 |
qed |
|
123 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
124 |
lemma distinct_list_bind: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
125 |
assumes "distinct xs" "\<And>x. x \<in> set xs \<Longrightarrow> distinct (f x)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
126 |
"disjoint_family_on (set \<circ> f) (set xs)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
127 |
shows "distinct (List.bind xs f)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
128 |
using assms |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
129 |
by (induction xs) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
130 |
(auto simp: disjoint_family_on_def distinct_map inj_on_def set_list_bind) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
131 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
132 |
lemma bij_betw_UNION_disjoint: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
133 |
assumes disj: "disjoint_family_on A' I" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
134 |
assumes bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
135 |
shows "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
136 |
unfolding bij_betw_def |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
137 |
proof |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
138 |
from bij show eq: "f ` UNION I A = UNION I A'" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
139 |
by (auto simp: bij_betw_def image_UN) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
140 |
show "inj_on f (UNION I A)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
141 |
proof (rule inj_onI, clarify) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
142 |
fix i j x y assume A: "i \<in> I" "j \<in> I" "x \<in> A i" "y \<in> A j" and B: "f x = f y" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
143 |
from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
144 |
by (auto simp: bij_betw_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
145 |
with B have "A' i \<inter> A' j \<noteq> {}" by auto |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
146 |
with disj A have "i = j" unfolding disjoint_family_on_def by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
147 |
with A B bij[of i] show "x = y" by (auto simp: bij_betw_def dest: inj_onD) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
148 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
149 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
150 |
|
60727 | 151 |
lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)" |
152 |
using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def) |
|
153 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
154 |
text \<open> |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
155 |
The union of an infinite disjoint family of non-empty sets is infinite. |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
156 |
\<close> |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
157 |
lemma infinite_disjoint_family_imp_infinite_UNION: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
158 |
assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
159 |
shows "\<not>finite (UNION A f)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
160 |
proof - |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
161 |
def g \<equiv> "\<lambda>x. SOME y. y \<in> f x" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
162 |
have g: "g x \<in> f x" if "x \<in> A" for x |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
163 |
unfolding g_def by (rule someI_ex, insert assms(2) that) blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
164 |
have inj_on_g: "inj_on g A" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
165 |
proof (rule inj_onI, rule ccontr) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
166 |
fix x y assume A: "x \<in> A" "y \<in> A" "g x = g y" "x \<noteq> y" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
167 |
with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
168 |
with A `x \<noteq> y` assms show False |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
169 |
by (auto simp: disjoint_family_on_def inj_on_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
170 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
171 |
from g have "g ` A \<subseteq> UNION A f" by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
172 |
moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
173 |
using finite_imageD by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
174 |
ultimately show ?thesis using finite_subset by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
175 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
176 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
177 |
|
60727 | 178 |
subsection \<open>Construct Disjoint Sequences\<close> |
179 |
||
180 |
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where |
|
181 |
"disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)" |
|
182 |
||
183 |
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" |
|
184 |
proof (induct n) |
|
185 |
case 0 show ?case by simp |
|
186 |
next |
|
187 |
case (Suc n) |
|
188 |
thus ?case by (simp add: atLeastLessThanSuc disjointed_def) |
|
189 |
qed |
|
190 |
||
191 |
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" |
|
192 |
by (rule UN_finite2_eq [where k=0]) |
|
193 |
(simp add: finite_UN_disjointed_eq) |
|
194 |
||
195 |
lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" |
|
196 |
by (auto simp add: disjointed_def) |
|
197 |
||
198 |
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" |
|
199 |
by (simp add: disjoint_family_on_def) |
|
200 |
(metis neq_iff Int_commute less_disjoint_disjointed) |
|
201 |
||
202 |
lemma disjointed_subset: "disjointed A n \<subseteq> A n" |
|
203 |
by (auto simp add: disjointed_def) |
|
204 |
||
205 |
lemma disjointed_0[simp]: "disjointed A 0 = A 0" |
|
206 |
by (simp add: disjointed_def) |
|
207 |
||
208 |
lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n" |
|
209 |
using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
210 |
|
62390 | 211 |
end |