author | desharna |
Mon, 13 Jun 2022 20:02:00 +0200 | |
changeset 75560 | aeb797356de0 |
parent 74598 | 5d91897a8e54 |
child 80067 | c40bdfc84640 |
permissions | -rw-r--r-- |
73477 | 1 |
(* Author: Johannes Hölzl, TU München |
60727 | 2 |
*) |
3 |
||
63098 | 4 |
section \<open>Partitions and Disjoint Sets\<close> |
60727 | 5 |
|
6 |
theory Disjoint_Sets |
|
74590
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
7 |
imports FuncSet |
60727 | 8 |
begin |
9 |
||
74590
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
10 |
lemma mono_imp_UN_eq_last: "mono A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n" |
60727 | 11 |
unfolding mono_def by auto |
12 |
||
13 |
subsection \<open>Set of Disjoint Sets\<close> |
|
14 |
||
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
|
15 |
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
|
16 |
|
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset
|
17 |
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
|
18 |
unfolding pairwise_def disjnt_def by auto |
60727 | 19 |
|
20 |
lemma disjointI: |
|
21 |
"(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A" |
|
22 |
unfolding disjoint_def by auto |
|
23 |
||
24 |
lemma disjointD: |
|
25 |
"disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}" |
|
26 |
unfolding disjoint_def by auto |
|
27 |
||
67399 | 28 |
lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint ((`) f ` A)" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
29 |
unfolding inj_on_def disjoint_def by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
30 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
31 |
lemma assumes "disjoint (A \<union> B)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
32 |
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
|
33 |
using assms by (simp_all add: disjoint_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
34 |
|
60727 | 35 |
lemma disjoint_INT: |
36 |
assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" |
|
37 |
shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}" |
|
38 |
proof (safe intro!: disjointI del: equalityI) |
|
63098 | 39 |
fix A B :: "'a \<Rightarrow> 'b set" assume "(\<Inter>i\<in>I. A i) \<noteq> (\<Inter>i\<in>I. B i)" |
60727 | 40 |
then obtain i where "A i \<noteq> B i" "i \<in> I" |
41 |
by auto |
|
42 |
moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i" |
|
43 |
ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}" |
|
44 |
using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"] |
|
68406 | 45 |
by (auto simp flip: INT_Int_distrib) |
60727 | 46 |
qed |
47 |
||
69712 | 48 |
lemma diff_Union_pairwise_disjoint: |
49 |
assumes "pairwise disjnt \<A>" "\<B> \<subseteq> \<A>" |
|
50 |
shows "\<Union>\<A> - \<Union>\<B> = \<Union>(\<A> - \<B>)" |
|
51 |
proof - |
|
52 |
have "False" |
|
53 |
if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B |
|
54 |
proof - |
|
55 |
have "A \<inter> B = {}" |
|
56 |
using assms disjointD AB by blast |
|
57 |
with x show ?thesis |
|
58 |
by blast |
|
59 |
qed |
|
60 |
then show ?thesis by auto |
|
61 |
qed |
|
62 |
||
63 |
lemma Int_Union_pairwise_disjoint: |
|
64 |
assumes "pairwise disjnt (\<A> \<union> \<B>)" |
|
65 |
shows "\<Union>\<A> \<inter> \<Union>\<B> = \<Union>(\<A> \<inter> \<B>)" |
|
66 |
proof - |
|
67 |
have "False" |
|
68 |
if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B |
|
69 |
proof - |
|
70 |
have "A \<inter> B = {}" |
|
71 |
using assms disjointD AB by blast |
|
72 |
with x show ?thesis |
|
73 |
by blast |
|
74 |
qed |
|
75 |
then show ?thesis by auto |
|
76 |
qed |
|
77 |
||
78 |
lemma psubset_Union_pairwise_disjoint: |
|
79 |
assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}" |
|
80 |
shows "\<Union>\<A> \<subset> \<Union>\<B>" |
|
81 |
unfolding psubset_eq |
|
82 |
proof |
|
83 |
show "\<Union>\<A> \<subseteq> \<Union>\<B>" |
|
84 |
using assms by blast |
|
85 |
have "\<A> \<subseteq> \<B>" "\<Union>(\<B> - \<A> \<inter> (\<B> - {{}})) \<noteq> {}" |
|
86 |
using assms by blast+ |
|
87 |
then show "\<Union>\<A> \<noteq> \<Union>\<B>" |
|
88 |
using diff_Union_pairwise_disjoint [OF \<B>] by blast |
|
89 |
qed |
|
90 |
||
60727 | 91 |
subsubsection "Family of Disjoint Sets" |
92 |
||
93 |
definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where |
|
94 |
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" |
|
95 |
||
96 |
abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV" |
|
97 |
||
63928
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
98 |
lemma disjoint_family_elem_disjnt: |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
99 |
assumes "infinite A" "finite C" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
100 |
and df: "disjoint_family_on B A" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
101 |
obtains x where "x \<in> A" "disjnt C (B x)" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
102 |
proof - |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
103 |
have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
104 |
proof - |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
105 |
obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
106 |
using * by metis |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
107 |
with df have "inj_on g A" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
108 |
by (fastforce simp add: inj_on_def disjoint_family_on_def) |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
109 |
then have "infinite (g ` A)" |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
110 |
using \<open>infinite A\<close> finite_image_iff by blast |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
111 |
then show False |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
112 |
by (meson \<open>finite C\<close> finite_subset g image_subset_iff) |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
113 |
qed |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
114 |
then show ?thesis |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
115 |
by (force simp: disjnt_iff intro: that) |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
116 |
qed |
d81fb5b46a5c
new material about topological concepts, etc
paulson <lp15@cam.ac.uk>
parents:
63148
diff
changeset
|
117 |
|
60727 | 118 |
lemma disjoint_family_onD: |
119 |
"disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
|
120 |
by (auto simp: disjoint_family_on_def) |
|
121 |
||
122 |
lemma disjoint_family_subset: "disjoint_family A \<Longrightarrow> (\<And>x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B" |
|
123 |
by (force simp add: disjoint_family_on_def) |
|
124 |
||
74598
5d91897a8e54
moved a theorem to a sensible place
paulson <lp15@cam.ac.uk>
parents:
74590
diff
changeset
|
125 |
lemma disjoint_family_on_insert: |
5d91897a8e54
moved a theorem to a sensible place
paulson <lp15@cam.ac.uk>
parents:
74590
diff
changeset
|
126 |
"i \<notin> I \<Longrightarrow> disjoint_family_on A (insert i I) \<longleftrightarrow> A i \<inter> (\<Union>i\<in>I. A i) = {} \<and> disjoint_family_on A I" |
5d91897a8e54
moved a theorem to a sensible place
paulson <lp15@cam.ac.uk>
parents:
74590
diff
changeset
|
127 |
by (fastforce simp: disjoint_family_on_def) |
5d91897a8e54
moved a theorem to a sensible place
paulson <lp15@cam.ac.uk>
parents:
74590
diff
changeset
|
128 |
|
60727 | 129 |
lemma disjoint_family_on_bisimulation: |
130 |
assumes "disjoint_family_on f S" |
|
131 |
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 = {}" |
|
132 |
shows "disjoint_family_on g S" |
|
133 |
using assms unfolding disjoint_family_on_def by auto |
|
134 |
||
135 |
lemma disjoint_family_on_mono: |
|
136 |
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A" |
|
137 |
unfolding disjoint_family_on_def by auto |
|
138 |
||
139 |
lemma disjoint_family_Suc: |
|
140 |
"(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)" |
|
141 |
using lift_Suc_mono_le[of A] |
|
142 |
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
|
143 |
(metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le) |
60727 | 144 |
|
145 |
lemma disjoint_family_on_disjoint_image: |
|
146 |
"disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)" |
|
147 |
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
|
148 |
|
60727 | 149 |
lemma disjoint_family_on_vimageI: "disjoint_family_on F I \<Longrightarrow> disjoint_family_on (\<lambda>i. f -` F i) I" |
150 |
by (auto simp: disjoint_family_on_def) |
|
151 |
||
152 |
lemma disjoint_image_disjoint_family_on: |
|
153 |
assumes d: "disjoint (A ` I)" and i: "inj_on A I" |
|
154 |
shows "disjoint_family_on A I" |
|
155 |
unfolding disjoint_family_on_def |
|
156 |
proof (intro ballI impI) |
|
157 |
fix n m assume nm: "m \<in> I" "n \<in> I" and "n \<noteq> m" |
|
158 |
with i[THEN inj_onD, of n m] show "A n \<inter> A m = {}" |
|
159 |
by (intro disjointD[OF d]) auto |
|
160 |
qed |
|
161 |
||
74438
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
162 |
lemma disjoint_family_on_iff_disjoint_image: |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
163 |
assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<noteq> {}" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
164 |
shows "disjoint_family_on A I \<longleftrightarrow> disjoint (A ` I) \<and> inj_on A I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
165 |
proof |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
166 |
assume "disjoint_family_on A I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
167 |
then show "disjoint (A ` I) \<and> inj_on A I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
168 |
by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
169 |
qed (use disjoint_image_disjoint_family_on in metis) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
170 |
|
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
171 |
lemma card_UN_disjoint': |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
172 |
assumes "disjoint_family_on A I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "finite I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
173 |
shows "card (\<Union>i\<in>I. A i) = (\<Sum>i\<in>I. card (A i))" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
174 |
using assms by (simp add: card_UN_disjoint disjoint_family_on_def) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
175 |
|
60727 | 176 |
lemma disjoint_UN: |
69745 | 177 |
assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I" |
60727 | 178 |
shows "disjoint (\<Union>i\<in>I. F i)" |
179 |
proof (safe intro!: disjointI del: equalityI) |
|
180 |
fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I" |
|
181 |
show "A \<inter> B = {}" |
|
182 |
proof cases |
|
183 |
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 = {}" |
|
184 |
by (auto dest: disjointD) |
|
185 |
next |
|
186 |
assume "i \<noteq> j" |
|
69745 | 187 |
with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>(F i)) \<inter> (\<Union>(F j)) = {}" |
60727 | 188 |
by (rule disjoint_family_onD) |
189 |
with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close> |
|
190 |
show "A \<inter> B = {}" |
|
191 |
by auto |
|
192 |
qed |
|
193 |
qed |
|
194 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
195 |
lemma distinct_list_bind: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
196 |
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
|
197 |
"disjoint_family_on (set \<circ> f) (set xs)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
198 |
shows "distinct (List.bind xs f)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
199 |
using assms |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
200 |
by (induction xs) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
201 |
(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
|
202 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
203 |
lemma bij_betw_UNION_disjoint: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
204 |
assumes disj: "disjoint_family_on A' I" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
205 |
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
|
206 |
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
|
207 |
unfolding bij_betw_def |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
208 |
proof |
69313 | 209 |
from bij show eq: "f ` \<Union>(A ` I) = \<Union>(A' ` I)" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
210 |
by (auto simp: bij_betw_def image_UN) |
69313 | 211 |
show "inj_on f (\<Union>(A ` I))" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
212 |
proof (rule inj_onI, clarify) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
by (auto simp: bij_betw_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
216 |
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
|
217 |
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
|
218 |
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
|
219 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
220 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
221 |
|
60727 | 222 |
lemma disjoint_union: "disjoint C \<Longrightarrow> disjoint B \<Longrightarrow> \<Union>C \<inter> \<Union>B = {} \<Longrightarrow> disjoint (C \<union> B)" |
223 |
using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def) |
|
224 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
225 |
text \<open> |
74438
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
226 |
Sum/product of the union of a finite disjoint family |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
227 |
\<close> |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
228 |
context comm_monoid_set |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
229 |
begin |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
230 |
|
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
231 |
lemma UNION_disjoint_family: |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
232 |
assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
233 |
and "disjoint_family_on A I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
234 |
shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
235 |
using assms unfolding disjoint_family_on_def by (rule UNION_disjoint) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
236 |
|
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
237 |
lemma Union_disjoint_sets: |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
238 |
assumes "\<forall>A\<in>C. finite A" and "disjoint C" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
239 |
shows "F g (\<Union>C) = (F \<circ> F) g C" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
240 |
using assms unfolding disjoint_def by (rule Union_disjoint) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
241 |
|
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
242 |
end |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
243 |
|
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
244 |
text \<open> |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
245 |
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
|
246 |
\<close> |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
247 |
lemma infinite_disjoint_family_imp_infinite_UNION: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
248 |
assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A" |
69313 | 249 |
shows "\<not>finite (\<Union>(f ` A))" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
250 |
proof - |
63148 | 251 |
define g where "g x = (SOME y. y \<in> f x)" for x |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
252 |
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
|
253 |
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
|
254 |
have inj_on_g: "inj_on g A" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
255 |
proof (rule inj_onI, rule ccontr) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
256 |
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
|
257 |
with g[of x] g[of y] have "g x \<in> f x" "g x \<in> f y" by auto |
63145 | 258 |
with A \<open>x \<noteq> y\<close> assms show False |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
259 |
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
|
260 |
qed |
69313 | 261 |
from g have "g ` A \<subseteq> \<Union>(f ` A)" by blast |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
262 |
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
|
263 |
using finite_imageD by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
264 |
ultimately show ?thesis using finite_subset by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
265 |
qed |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
266 |
|
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62843
diff
changeset
|
267 |
|
60727 | 268 |
subsection \<open>Construct Disjoint Sequences\<close> |
269 |
||
270 |
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set" where |
|
271 |
"disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)" |
|
272 |
||
273 |
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" |
|
274 |
proof (induct n) |
|
275 |
case 0 show ?case by simp |
|
276 |
next |
|
277 |
case (Suc n) |
|
278 |
thus ?case by (simp add: atLeastLessThanSuc disjointed_def) |
|
279 |
qed |
|
280 |
||
281 |
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" |
|
282 |
by (rule UN_finite2_eq [where k=0]) |
|
283 |
(simp add: finite_UN_disjointed_eq) |
|
284 |
||
285 |
lemma less_disjoint_disjointed: "m < n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" |
|
286 |
by (auto simp add: disjointed_def) |
|
287 |
||
288 |
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" |
|
289 |
by (simp add: disjoint_family_on_def) |
|
290 |
(metis neq_iff Int_commute less_disjoint_disjointed) |
|
291 |
||
292 |
lemma disjointed_subset: "disjointed A n \<subseteq> A n" |
|
293 |
by (auto simp add: disjointed_def) |
|
294 |
||
295 |
lemma disjointed_0[simp]: "disjointed A 0 = A 0" |
|
296 |
by (simp add: disjointed_def) |
|
297 |
||
298 |
lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n" |
|
74590
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
299 |
using mono_imp_UN_eq_last[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) |
60727 | 300 |
|
63098 | 301 |
subsection \<open>Partitions\<close> |
302 |
||
303 |
text \<open> |
|
69593 | 304 |
Partitions \<^term>\<open>P\<close> of a set \<^term>\<open>A\<close>. We explicitly disallow empty sets. |
63098 | 305 |
\<close> |
306 |
||
307 |
definition partition_on :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" |
|
308 |
where |
|
309 |
"partition_on A P \<longleftrightarrow> \<Union>P = A \<and> disjoint P \<and> {} \<notin> P" |
|
310 |
||
311 |
lemma partition_onI: |
|
312 |
"\<Union>P = A \<Longrightarrow> (\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> p \<noteq> q \<Longrightarrow> disjnt p q) \<Longrightarrow> {} \<notin> P \<Longrightarrow> partition_on A P" |
|
313 |
by (auto simp: partition_on_def pairwise_def) |
|
314 |
||
315 |
lemma partition_onD1: "partition_on A P \<Longrightarrow> A = \<Union>P" |
|
316 |
by (auto simp: partition_on_def) |
|
317 |
||
318 |
lemma partition_onD2: "partition_on A P \<Longrightarrow> disjoint P" |
|
319 |
by (auto simp: partition_on_def) |
|
320 |
||
321 |
lemma partition_onD3: "partition_on A P \<Longrightarrow> {} \<notin> P" |
|
322 |
by (auto simp: partition_on_def) |
|
323 |
||
324 |
subsection \<open>Constructions of partitions\<close> |
|
325 |
||
326 |
lemma partition_on_empty: "partition_on {} P \<longleftrightarrow> P = {}" |
|
327 |
unfolding partition_on_def by fastforce |
|
328 |
||
329 |
lemma partition_on_space: "A \<noteq> {} \<Longrightarrow> partition_on A {A}" |
|
330 |
by (auto simp: partition_on_def disjoint_def) |
|
331 |
||
332 |
lemma partition_on_singletons: "partition_on A ((\<lambda>x. {x}) ` A)" |
|
333 |
by (auto simp: partition_on_def disjoint_def) |
|
334 |
||
335 |
lemma partition_on_transform: |
|
336 |
assumes P: "partition_on A P" |
|
337 |
assumes F_UN: "\<Union>(F ` P) = F (\<Union>P)" and F_disjnt: "\<And>p q. p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (F p) (F q)" |
|
338 |
shows "partition_on (F A) (F ` P - {{}})" |
|
339 |
proof - |
|
340 |
have "\<Union>(F ` P - {{}}) = F A" |
|
341 |
unfolding P[THEN partition_onD1] F_UN[symmetric] by auto |
|
342 |
with P show ?thesis |
|
343 |
by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt) |
|
344 |
qed |
|
345 |
||
67399 | 346 |
lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) ((\<inter>) B ` P - {{}})" |
63098 | 347 |
by (intro partition_on_transform) (auto simp: disjnt_def) |
348 |
||
67399 | 349 |
lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) ((-`) f ` P - {{}})" |
63098 | 350 |
by (intro partition_on_transform) (auto simp: disjnt_def) |
351 |
||
352 |
lemma partition_on_inj_image: |
|
353 |
assumes P: "partition_on A P" and f: "inj_on f A" |
|
67399 | 354 |
shows "partition_on (f ` A) ((`) f ` P - {{}})" |
63098 | 355 |
proof (rule partition_on_transform[OF P]) |
356 |
show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q |
|
357 |
using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def) |
|
358 |
qed auto |
|
359 |
||
74223
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
360 |
lemma partition_on_insert: |
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
361 |
assumes "disjnt p (\<Union>P)" |
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
362 |
shows "partition_on A (insert p P) \<longleftrightarrow> partition_on (A-p) P \<and> p \<subseteq> A \<and> p \<noteq> {}" |
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
363 |
using assms |
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
364 |
by (auto simp: partition_on_def disjnt_iff pairwise_insert) |
527088d4a89b
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
paulson <lp15@cam.ac.uk>
parents:
73477
diff
changeset
|
365 |
|
63098 | 366 |
subsection \<open>Finiteness of partitions\<close> |
367 |
||
368 |
lemma finitely_many_partition_on: |
|
369 |
assumes "finite A" |
|
370 |
shows "finite {P. partition_on A P}" |
|
371 |
proof (rule finite_subset) |
|
372 |
show "{P. partition_on A P} \<subseteq> Pow (Pow A)" |
|
373 |
unfolding partition_on_def by auto |
|
374 |
show "finite (Pow (Pow A))" |
|
375 |
using assms by simp |
|
376 |
qed |
|
377 |
||
378 |
lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P" |
|
379 |
using partition_onD1[of A P] by (simp add: finite_UnionD) |
|
380 |
||
74438
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
381 |
lemma product_partition: |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
382 |
assumes "partition_on A P" and "\<And>p. p \<in> P \<Longrightarrow> finite p" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
383 |
shows "card A = (\<Sum>p\<in>P. card p)" |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
384 |
using assms unfolding partition_on_def by (meson card_Union_disjoint) |
5827b91ef30e
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
paulson <lp15@cam.ac.uk>
parents:
74223
diff
changeset
|
385 |
|
63098 | 386 |
subsection \<open>Equivalence of partitions and equivalence classes\<close> |
387 |
||
388 |
lemma partition_on_quotient: |
|
389 |
assumes r: "equiv A r" |
|
390 |
shows "partition_on A (A // r)" |
|
391 |
proof (rule partition_onI) |
|
392 |
from r have "refl_on A r" |
|
393 |
by (auto elim: equivE) |
|
394 |
then show "\<Union>(A // r) = A" "{} \<notin> A // r" |
|
395 |
by (auto simp: refl_on_def quotient_def) |
|
396 |
||
397 |
fix p q assume "p \<in> A // r" "q \<in> A // r" "p \<noteq> q" |
|
398 |
then obtain x y where "x \<in> A" "y \<in> A" "p = r `` {x}" "q = r `` {y}" |
|
399 |
by (auto simp: quotient_def) |
|
400 |
with r equiv_class_eq_iff[OF r, of x y] \<open>p \<noteq> q\<close> show "disjnt p q" |
|
401 |
by (auto simp: disjnt_equiv_class) |
|
402 |
qed |
|
403 |
||
404 |
lemma equiv_partition_on: |
|
405 |
assumes P: "partition_on A P" |
|
406 |
shows "equiv A {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p}" |
|
407 |
proof (rule equivI) |
|
408 |
have "A = \<Union>P" "disjoint P" "{} \<notin> P" |
|
409 |
using P by (auto simp: partition_on_def) |
|
410 |
then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}" |
|
411 |
unfolding refl_on_def by auto |
|
412 |
show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}" |
|
413 |
using \<open>disjoint P\<close> by (auto simp: trans_def disjoint_def) |
|
414 |
qed (auto simp: sym_def) |
|
415 |
||
416 |
lemma partition_on_eq_quotient: |
|
417 |
assumes P: "partition_on A P" |
|
418 |
shows "A // {(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} = P" |
|
419 |
unfolding quotient_def |
|
420 |
proof safe |
|
421 |
fix x assume "x \<in> A" |
|
422 |
then obtain p where "p \<in> P" "x \<in> p" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q" |
|
423 |
using P by (auto simp: partition_on_def disjoint_def) |
|
424 |
then have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p" |
|
425 |
by (safe intro!: bexI[of _ p]) simp |
|
426 |
then show "{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x} \<in> P" |
|
427 |
by (simp add: \<open>p \<in> P\<close>) |
|
428 |
next |
|
429 |
fix p assume "p \<in> P" |
|
430 |
then have "p \<noteq> {}" |
|
431 |
using P by (auto simp: partition_on_def) |
|
432 |
then obtain x where "x \<in> p" |
|
433 |
by auto |
|
434 |
then have "x \<in> A" "\<And>q. q \<in> P \<Longrightarrow> x \<in> q \<Longrightarrow> p = q" |
|
435 |
using P \<open>p \<in> P\<close> by (auto simp: partition_on_def disjoint_def) |
|
436 |
with \<open>p\<in>P\<close> \<open>x \<in> p\<close> have "{y. \<exists>p\<in>P. x \<in> p \<and> y \<in> p} = p" |
|
437 |
by (safe intro!: bexI[of _ p]) simp |
|
438 |
then show "p \<in> (\<Union>x\<in>A. {{(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p} `` {x}})" |
|
439 |
by (auto intro: \<open>x \<in> A\<close>) |
|
440 |
qed |
|
441 |
||
442 |
lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)" |
|
443 |
by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on) |
|
444 |
||
74574 | 445 |
subsection \<open>Refinement of partitions\<close> |
446 |
||
447 |
definition refines :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set \<Rightarrow> bool" |
|
448 |
where "refines A P Q \<equiv> |
|
449 |
partition_on A P \<and> partition_on A Q \<and> (\<forall>X\<in>P. \<exists>Y\<in>Q. X \<subseteq> Y)" |
|
450 |
||
451 |
lemma refines_refl: "partition_on A P \<Longrightarrow> refines A P P" |
|
452 |
using refines_def by blast |
|
453 |
||
454 |
lemma refines_asym1: |
|
455 |
assumes "refines A P Q" "refines A Q P" |
|
456 |
shows "P \<subseteq> Q" |
|
457 |
proof |
|
458 |
fix X |
|
459 |
assume "X \<in> P" |
|
460 |
then obtain Y X' where "Y \<in> Q" "X \<subseteq> Y" "X' \<in> P" "Y \<subseteq> X'" |
|
461 |
by (meson assms refines_def) |
|
462 |
then have "X' = X" |
|
463 |
using assms(2) unfolding partition_on_def refines_def |
|
464 |
by (metis \<open>X \<in> P\<close> \<open>X \<subseteq> Y\<close> disjnt_self_iff_empty disjnt_subset1 pairwiseD) |
|
465 |
then show "X \<in> Q" |
|
466 |
using \<open>X \<subseteq> Y\<close> \<open>Y \<in> Q\<close> \<open>Y \<subseteq> X'\<close> by force |
|
467 |
qed |
|
468 |
||
469 |
lemma refines_asym: "\<lbrakk>refines A P Q; refines A Q P\<rbrakk> \<Longrightarrow> P=Q" |
|
470 |
by (meson antisym_conv refines_asym1) |
|
471 |
||
472 |
lemma refines_trans: "\<lbrakk>refines A P Q; refines A Q R\<rbrakk> \<Longrightarrow> refines A P R" |
|
473 |
by (meson order.trans refines_def) |
|
474 |
||
475 |
lemma refines_obtains_subset: |
|
476 |
assumes "refines A P Q" "q \<in> Q" |
|
477 |
shows "partition_on q {p \<in> P. p \<subseteq> q}" |
|
478 |
proof - |
|
479 |
have "p \<subseteq> q \<or> disjnt p q" if "p \<in> P" for p |
|
480 |
using that assms unfolding refines_def partition_on_def disjoint_def |
|
481 |
by (metis disjnt_def disjnt_subset1) |
|
482 |
with assms have "q \<subseteq> Union {p \<in> P. p \<subseteq> q}" |
|
483 |
using assms |
|
484 |
by (clarsimp simp: refines_def disjnt_iff partition_on_def) (metis Union_iff) |
|
485 |
with assms have "q = Union {p \<in> P. p \<subseteq> q}" |
|
486 |
by auto |
|
487 |
then show ?thesis |
|
488 |
using assms by (auto simp: refines_def disjoint_def partition_on_def) |
|
489 |
qed |
|
490 |
||
74590
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
491 |
subsection \<open>The coarsest common refinement of a set of partitions\<close> |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
492 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
493 |
definition common_refinement :: "'a set set set \<Rightarrow> 'a set set" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
494 |
where "common_refinement \<P> \<equiv> (\<Union>f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P). {\<Inter> (f ` \<P>)}) - {{}}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
495 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
496 |
text \<open>With non-extensional function space\<close> |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
497 |
lemma common_refinement: "common_refinement \<P> = (\<Union>f \<in> (\<Pi> P\<in>\<P>. P). {\<Inter> (f ` \<P>)}) - {{}}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
498 |
(is "?lhs = ?rhs") |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
499 |
proof |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
500 |
show "?rhs \<subseteq> ?lhs" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
501 |
apply (clarsimp simp add: common_refinement_def PiE_def Ball_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
502 |
by (metis restrict_Pi_cancel image_restrict_eq restrict_extensional) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
503 |
qed (auto simp add: common_refinement_def PiE_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
504 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
505 |
lemma common_refinement_exists: "\<lbrakk>X \<in> common_refinement \<P>; P \<in> \<P>\<rbrakk> \<Longrightarrow> \<exists>R\<in>P. X \<subseteq> R" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
506 |
by (auto simp add: common_refinement) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
507 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
508 |
lemma Union_common_refinement: "\<Union> (common_refinement \<P>) = (\<Inter> P\<in>\<P>. \<Union>P)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
509 |
proof |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
510 |
show "(\<Inter> P\<in>\<P>. \<Union>P) \<subseteq> \<Union> (common_refinement \<P>)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
511 |
proof (clarsimp simp: common_refinement) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
512 |
fix x |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
513 |
assume "\<forall>P\<in>\<P>. \<exists>X\<in>P. x \<in> X" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
514 |
then obtain F where F: "\<And>P. P\<in>\<P> \<Longrightarrow> F P \<in> P \<and> x \<in> F P" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
515 |
by metis |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
516 |
then have "x \<in> \<Inter> (F ` \<P>)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
517 |
by force |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
518 |
with F show "\<exists>X\<in>(\<Union>x\<in>\<Pi> P\<in>\<P>. P. {\<Inter> (x ` \<P>)}) - {{}}. x \<in> X" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
519 |
by (auto simp add: Pi_iff Bex_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
520 |
qed |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
521 |
qed (auto simp: common_refinement_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
522 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
523 |
lemma partition_on_common_refinement: |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
524 |
assumes A: "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" and "\<P> \<noteq> {}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
525 |
shows "partition_on A (common_refinement \<P>)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
526 |
proof (rule partition_onI) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
527 |
show "\<Union> (common_refinement \<P>) = A" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
528 |
using assms by (simp add: partition_on_def Union_common_refinement) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
529 |
fix P Q |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
530 |
assume "P \<in> common_refinement \<P>" and "Q \<in> common_refinement \<P>" and "P \<noteq> Q" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
531 |
then obtain f g where f: "f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P)" and P: "P = \<Inter> (f ` \<P>)" and "P \<noteq> {}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
532 |
and g: "g \<in> (\<Pi>\<^sub>E P\<in>\<P>. P)" and Q: "Q = \<Inter> (g ` \<P>)" and "Q \<noteq> {}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
533 |
by (auto simp add: common_refinement_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
534 |
have "f=g" if "x \<in> P" "x \<in> Q" for x |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
535 |
proof (rule extensionalityI [of _ \<P>]) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
536 |
fix R |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
537 |
assume "R \<in> \<P>" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
538 |
with that P Q f g A [unfolded partition_on_def, OF \<open>R \<in> \<P>\<close>] |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
539 |
show "f R = g R" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
540 |
by (metis INT_E Int_iff PiE_iff disjointD emptyE) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
541 |
qed (use PiE_iff f g in auto) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
542 |
then show "disjnt P Q" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
543 |
by (metis P Q \<open>P \<noteq> Q\<close> disjnt_iff) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
544 |
qed (simp add: common_refinement_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
545 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
546 |
lemma refines_common_refinement: |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
547 |
assumes "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" "P \<in> \<P>" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
548 |
shows "refines A (common_refinement \<P>) P" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
549 |
unfolding refines_def |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
550 |
proof (intro conjI strip) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
551 |
fix X |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
552 |
assume "X \<in> common_refinement \<P>" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
553 |
with assms show "\<exists>Y\<in>P. X \<subseteq> Y" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
554 |
by (auto simp: common_refinement_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
555 |
qed (use assms partition_on_common_refinement in auto) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
556 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
557 |
text \<open>The common refinement is itself refined by any other\<close> |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
558 |
lemma common_refinement_coarsest: |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
559 |
assumes "\<And>P. P \<in> \<P> \<Longrightarrow> partition_on A P" "partition_on A R" "\<And>P. P \<in> \<P> \<Longrightarrow> refines A R P" "\<P> \<noteq> {}" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
560 |
shows "refines A R (common_refinement \<P>)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
561 |
unfolding refines_def |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
562 |
proof (intro conjI ballI partition_on_common_refinement) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
563 |
fix X |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
564 |
assume "X \<in> R" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
565 |
have "\<exists>p \<in> P. X \<subseteq> p" if "P \<in> \<P>" for P |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
566 |
by (meson \<open>X \<in> R\<close> assms(3) refines_def that) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
567 |
then obtain F where f: "\<And>P. P \<in> \<P> \<Longrightarrow> F P \<in> P \<and> X \<subseteq> F P" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
568 |
by metis |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
569 |
with \<open>partition_on A R\<close> \<open>X \<in> R\<close> \<open>\<P> \<noteq> {}\<close> |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
570 |
have "\<Inter> (F ` \<P>) \<in> common_refinement \<P>" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
571 |
apply (simp add: partition_on_def common_refinement Pi_iff Bex_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
572 |
by (metis (no_types, lifting) cINF_greatest subset_empty) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
573 |
with f show "\<exists>Y\<in>common_refinement \<P>. X \<subseteq> Y" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
574 |
by (metis \<open>\<P> \<noteq> {}\<close> cINF_greatest) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
575 |
qed (use assms in auto) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
576 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
577 |
lemma finite_common_refinement: |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
578 |
assumes "finite \<P>" "\<And>P. P \<in> \<P> \<Longrightarrow> finite P" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
579 |
shows "finite (common_refinement \<P>)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
580 |
proof - |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
581 |
have "finite (\<Pi>\<^sub>E P\<in>\<P>. P)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
582 |
by (simp add: assms finite_PiE) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
583 |
then show ?thesis |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
584 |
by (auto simp: common_refinement_def) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
585 |
qed |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
586 |
|
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
587 |
lemma card_common_refinement: |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
588 |
assumes "finite \<P>" "\<And>P. P \<in> \<P> \<Longrightarrow> finite P" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
589 |
shows "card (common_refinement \<P>) \<le> (\<Prod>P \<in> \<P>. card P)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
590 |
proof - |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
591 |
have "card (common_refinement \<P>) \<le> card (\<Union>f \<in> (\<Pi>\<^sub>E P\<in>\<P>. P). {\<Inter> (f ` \<P>)})" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
592 |
unfolding common_refinement_def by (meson card_Diff1_le) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
593 |
also have "\<dots> \<le> (\<Sum>f\<in>(\<Pi>\<^sub>E P\<in>\<P>. P). card{\<Inter> (f ` \<P>)})" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
594 |
by (metis assms finite_PiE card_UN_le) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
595 |
also have "\<dots> = card(\<Pi>\<^sub>E P\<in>\<P>. P)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
596 |
by simp |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
597 |
also have "\<dots> = (\<Prod>P \<in> \<P>. card P)" |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
598 |
by (simp add: assms(1) card_PiE dual_order.eq_iff) |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
599 |
finally show ?thesis . |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
600 |
qed |
00ffae972fc0
Added / moved some simple set-theoretic lemmas
paulson <lp15@cam.ac.uk>
parents:
74574
diff
changeset
|
601 |
|
62390 | 602 |
end |