src/HOL/Finite_Set.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 63099 af0e964aad7b child 63365 5340fb6633d0 permissions -rw-r--r--
Lots of new material for multivariate analysis
1 (*  Title:      HOL/Finite_Set.thy
2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
3                 with contributions by Jeremy Avigad and Andrei Popescu
4 *)
6 section \<open>Finite sets\<close>
8 theory Finite_Set
9 imports Product_Type Sum_Type Fields
10 begin
12 subsection \<open>Predicate for finite sets\<close>
14 context
15   notes [[inductive_internals]]
16 begin
18 inductive finite :: "'a set \<Rightarrow> bool"
19   where
20     emptyI [simp, intro!]: "finite {}"
21   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
23 end
25 simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
27 declare [[simproc del: finite_Collect]]
29 lemma finite_induct [case_names empty insert, induct set: finite]:
30   \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
31   assumes "finite F"
32   assumes "P {}"
33     and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
34   shows "P F"
35 using \<open>finite F\<close>
36 proof induct
37   show "P {}" by fact
38   fix x F assume F: "finite F" and P: "P F"
39   show "P (insert x F)"
40   proof cases
41     assume "x \<in> F"
42     hence "insert x F = F" by (rule insert_absorb)
43     with P show ?thesis by (simp only:)
44   next
45     assume "x \<notin> F"
46     from F this P show ?thesis by (rule insert)
47   qed
48 qed
50 lemma infinite_finite_induct [case_names infinite empty insert]:
51   assumes infinite: "\<And>A. \<not> finite A \<Longrightarrow> P A"
52   assumes empty: "P {}"
53   assumes insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
54   shows "P A"
55 proof (cases "finite A")
56   case False with infinite show ?thesis .
57 next
58   case True then show ?thesis by (induct A) (fact empty insert)+
59 qed
62 subsubsection \<open>Choice principles\<close>
64 lemma ex_new_if_finite: \<comment> "does not depend on def of finite at all"
65   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
66   shows "\<exists>a::'a. a \<notin> A"
67 proof -
68   from assms have "A \<noteq> UNIV" by blast
69   then show ?thesis by blast
70 qed
72 text \<open>A finite choice principle. Does not need the SOME choice operator.\<close>
74 lemma finite_set_choice:
75   "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
76 proof (induct rule: finite_induct)
77   case empty then show ?case by simp
78 next
79   case (insert a A)
80   then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
81   show ?case (is "EX f. ?P f")
82   proof
83     show "?P(%x. if x = a then b else f x)" using f ab by auto
84   qed
85 qed
88 subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close>
90 lemma finite_imp_nat_seg_image_inj_on:
91   assumes "finite A"
92   shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
93 using assms
94 proof induct
95   case empty
96   show ?case
97   proof
98     show "\<exists>f. {} = f ` {i::nat. i < 0} \<and> inj_on f {i. i < 0}" by simp
99   qed
100 next
101   case (insert a A)
102   have notinA: "a \<notin> A" by fact
103   from insert.hyps obtain n f
104     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
105   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
106         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
107     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
108   thus ?case by blast
109 qed
111 lemma nat_seg_image_imp_finite:
112   "A = f ` {i::nat. i < n} \<Longrightarrow> finite A"
113 proof (induct n arbitrary: A)
114   case 0 thus ?case by simp
115 next
116   case (Suc n)
117   let ?B = "f ` {i. i < n}"
118   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
119   show ?case
120   proof cases
121     assume "\<exists>k<n. f n = f k"
122     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
123     thus ?thesis using finB by simp
124   next
125     assume "\<not>(\<exists> k<n. f n = f k)"
126     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
127     thus ?thesis using finB by simp
128   qed
129 qed
131 lemma finite_conv_nat_seg_image:
132   "finite A \<longleftrightarrow> (\<exists>(n::nat) f. A = f ` {i::nat. i < n})"
133   by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
135 lemma finite_imp_inj_to_nat_seg:
136   assumes "finite A"
137   shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A"
138 proof -
139   from finite_imp_nat_seg_image_inj_on[OF \<open>finite A\<close>]
140   obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
141     by (auto simp:bij_betw_def)
142   let ?f = "the_inv_into {i. i<n} f"
143   have "inj_on ?f A & ?f ` A = {i. i<n}"
144     by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
145   thus ?thesis by blast
146 qed
148 lemma finite_Collect_less_nat [iff]:
149   "finite {n::nat. n < k}"
150   by (fastforce simp: finite_conv_nat_seg_image)
152 lemma finite_Collect_le_nat [iff]:
153   "finite {n::nat. n \<le> k}"
154   by (simp add: le_eq_less_or_eq Collect_disj_eq)
157 subsubsection \<open>Finiteness and common set operations\<close>
159 lemma rev_finite_subset:
160   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A"
161 proof (induct arbitrary: A rule: finite_induct)
162   case empty
163   then show ?case by simp
164 next
165   case (insert x F A)
166   have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F \<Longrightarrow> finite (A - {x})" by fact+
167   show "finite A"
168   proof cases
169     assume x: "x \<in> A"
170     with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
171     with r have "finite (A - {x})" .
172     hence "finite (insert x (A - {x}))" ..
173     also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
174     finally show ?thesis .
175   next
176     show ?thesis when "A \<subseteq> F"
177       using that by fact
178     assume "x \<notin> A"
179     with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
180   qed
181 qed
183 lemma finite_subset:
184   "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
185   by (rule rev_finite_subset)
187 lemma finite_UnI:
188   assumes "finite F" and "finite G"
189   shows "finite (F \<union> G)"
190   using assms by induct simp_all
192 lemma finite_Un [iff]:
193   "finite (F \<union> G) \<longleftrightarrow> finite F \<and> finite G"
194   by (blast intro: finite_UnI finite_subset [of _ "F \<union> G"])
196 lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A"
197 proof -
198   have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp
199   then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un)
200   then show ?thesis by simp
201 qed
203 lemma finite_Int [simp, intro]:
204   "finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)"
205   by (blast intro: finite_subset)
207 lemma finite_Collect_conjI [simp, intro]:
208   "finite {x. P x} \<or> finite {x. Q x} \<Longrightarrow> finite {x. P x \<and> Q x}"
211 lemma finite_Collect_disjI [simp]:
212   "finite {x. P x \<or> Q x} \<longleftrightarrow> finite {x. P x} \<and> finite {x. Q x}"
215 lemma finite_Diff [simp, intro]:
216   "finite A \<Longrightarrow> finite (A - B)"
217   by (rule finite_subset, rule Diff_subset)
219 lemma finite_Diff2 [simp]:
220   assumes "finite B"
221   shows "finite (A - B) \<longleftrightarrow> finite A"
222 proof -
223   have "finite A \<longleftrightarrow> finite((A - B) \<union> (A \<inter> B))" by (simp add: Un_Diff_Int)
224   also have "\<dots> \<longleftrightarrow> finite (A - B)" using \<open>finite B\<close> by simp
225   finally show ?thesis ..
226 qed
228 lemma finite_Diff_insert [iff]:
229   "finite (A - insert a B) \<longleftrightarrow> finite (A - B)"
230 proof -
231   have "finite (A - B) \<longleftrightarrow> finite (A - B - {a})" by simp
232   moreover have "A - insert a B = A - B - {a}" by auto
233   ultimately show ?thesis by simp
234 qed
236 lemma finite_compl[simp]:
237   "finite (A :: 'a set) \<Longrightarrow> finite (- A) \<longleftrightarrow> finite (UNIV :: 'a set)"
240 lemma finite_Collect_not[simp]:
241   "finite {x :: 'a. P x} \<Longrightarrow> finite {x. \<not> P x} \<longleftrightarrow> finite (UNIV :: 'a set)"
244 lemma finite_Union [simp, intro]:
245   "finite A \<Longrightarrow> (\<And>M. M \<in> A \<Longrightarrow> finite M) \<Longrightarrow> finite(\<Union>A)"
246   by (induct rule: finite_induct) simp_all
248 lemma finite_UN_I [intro]:
249   "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
250   by (induct rule: finite_induct) simp_all
252 lemma finite_UN [simp]:
253   "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
254   by (blast intro: finite_subset)
256 lemma finite_Inter [intro]:
257   "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
258   by (blast intro: Inter_lower finite_subset)
260 lemma finite_INT [intro]:
261   "\<exists>x\<in>I. finite (A x) \<Longrightarrow> finite (\<Inter>x\<in>I. A x)"
262   by (blast intro: INT_lower finite_subset)
264 lemma finite_imageI [simp, intro]:
265   "finite F \<Longrightarrow> finite (h ` F)"
266   by (induct rule: finite_induct) simp_all
268 lemma finite_image_set [simp]:
269   "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
270   by (simp add: image_Collect [symmetric])
272 lemma finite_image_set2:
273   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y | x y. P x \<and> Q y}"
274   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
276 lemma finite_imageD:
277   assumes "finite (f ` A)" and "inj_on f A"
278   shows "finite A"
279 using assms
280 proof (induct "f ` A" arbitrary: A)
281   case empty then show ?case by simp
282 next
283   case (insert x B)
284   then have B_A: "insert x B = f ` A" by simp
285   then obtain y where "x = f y" and "y \<in> A" by blast
286   from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}" by blast
287   with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
288     by (simp add: inj_on_image_set_diff Set.Diff_subset)
289   moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})" by (rule inj_on_diff)
290   ultimately have "finite (A - {y})" by (rule insert.hyps)
291   then show "finite A" by simp
292 qed
294 lemma finite_image_iff:
295   assumes "inj_on f A"
296   shows "finite (f ` A) \<longleftrightarrow> finite A"
297 using assms finite_imageD by blast
299 lemma finite_surj:
300   "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
301   by (erule finite_subset) (rule finite_imageI)
303 lemma finite_range_imageI:
304   "finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))"
305   by (drule finite_imageI) (simp add: range_composition)
307 lemma finite_subset_image:
308   assumes "finite B"
309   shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
310 using assms
311 proof induct
312   case empty then show ?case by simp
313 next
314   case insert then show ?case
315     by (clarsimp simp del: image_insert simp add: image_insert [symmetric])
316        blast
317 qed
319 lemma finite_vimage_IntI:
320   "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
321   apply (induct rule: finite_induct)
322    apply simp_all
323   apply (subst vimage_insert)
324   apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
325   done
327 lemma finite_finite_vimage_IntI:
328   assumes "finite F" and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
329   shows "finite (h -` F \<inter> A)"
330 proof -
331   have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
332     by blast
333   show ?thesis
334     by (simp only: * assms finite_UN_I)
335 qed
337 lemma finite_vimageI:
338   "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
339   using finite_vimage_IntI[of F h UNIV] by auto
341 lemma finite_vimageD': "\<lbrakk> finite (f -` A); A \<subseteq> range f \<rbrakk> \<Longrightarrow> finite A"
342 by(auto simp add: subset_image_iff intro: finite_subset[rotated])
344 lemma finite_vimageD: "\<lbrakk> finite (h -` F); surj h \<rbrakk> \<Longrightarrow> finite F"
345 by(auto dest: finite_vimageD')
347 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
348   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
350 lemma finite_Collect_bex [simp]:
351   assumes "finite A"
352   shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
353 proof -
354   have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto
355   with assms show ?thesis by simp
356 qed
358 lemma finite_Collect_bounded_ex [simp]:
359   assumes "finite {y. P y}"
360   shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})"
361 proof -
362   have "{x. EX y. P y & Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})" by auto
363   with assms show ?thesis by simp
364 qed
366 lemma finite_Plus:
367   "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)"
370 lemma finite_PlusD:
371   fixes A :: "'a set" and B :: "'b set"
372   assumes fin: "finite (A <+> B)"
373   shows "finite A" "finite B"
374 proof -
375   have "Inl ` A \<subseteq> A <+> B" by auto
376   then have "finite (Inl ` A :: ('a + 'b) set)" using fin by (rule finite_subset)
377   then show "finite A" by (rule finite_imageD) (auto intro: inj_onI)
378 next
379   have "Inr ` B \<subseteq> A <+> B" by auto
380   then have "finite (Inr ` B :: ('a + 'b) set)" using fin by (rule finite_subset)
381   then show "finite B" by (rule finite_imageD) (auto intro: inj_onI)
382 qed
384 lemma finite_Plus_iff [simp]:
385   "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
386   by (auto intro: finite_PlusD finite_Plus)
388 lemma finite_Plus_UNIV_iff [simp]:
389   "finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
390   by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)
392 lemma finite_SigmaI [simp, intro]:
393   "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)"
394   by (unfold Sigma_def) blast
396 lemma finite_SigmaI2:
397   assumes "finite {x\<in>A. B x \<noteq> {}}"
398   and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
399   shows "finite (Sigma A B)"
400 proof -
401   from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)" by auto
402   also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto
403   finally show ?thesis .
404 qed
406 lemma finite_cartesian_product:
407   "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
408   by (rule finite_SigmaI)
410 lemma finite_Prod_UNIV:
411   "finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)"
412   by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
414 lemma finite_cartesian_productD1:
415   assumes "finite (A \<times> B)" and "B \<noteq> {}"
416   shows "finite A"
417 proof -
418   from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
419     by (auto simp add: finite_conv_nat_seg_image)
420   then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp
421   with \<open>B \<noteq> {}\<close> have "A = (fst \<circ> f) ` {i::nat. i < n}"
423   then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast
424   then show ?thesis
425     by (auto simp add: finite_conv_nat_seg_image)
426 qed
428 lemma finite_cartesian_productD2:
429   assumes "finite (A \<times> B)" and "A \<noteq> {}"
430   shows "finite B"
431 proof -
432   from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
433     by (auto simp add: finite_conv_nat_seg_image)
434   then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp
435   with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}"
437   then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast
438   then show ?thesis
439     by (auto simp add: finite_conv_nat_seg_image)
440 qed
442 lemma finite_cartesian_product_iff:
443   "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
444   by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
446 lemma finite_prod:
447   "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
448   using finite_cartesian_product_iff[of UNIV UNIV] by simp
450 lemma finite_Pow_iff [iff]:
451   "finite (Pow A) \<longleftrightarrow> finite A"
452 proof
453   assume "finite (Pow A)"
454   then have "finite ((%x. {x}) ` A)" by (blast intro: finite_subset)
455   then show "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
456 next
457   assume "finite A"
458   then show "finite (Pow A)"
459     by induct (simp_all add: Pow_insert)
460 qed
462 corollary finite_Collect_subsets [simp, intro]:
463   "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
464   by (simp add: Pow_def [symmetric])
466 lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)"
467 by(simp only: finite_Pow_iff Pow_UNIV[symmetric])
469 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
470   by (blast intro: finite_subset [OF subset_Pow_Union])
472 lemma finite_set_of_finite_funs: assumes "finite A" "finite B"
473 shows "finite{f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
474 proof-
475   let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}"
476   have "?F ` ?S \<subseteq> Pow(A \<times> B)" by auto
477   from finite_subset[OF this] assms have 1: "finite (?F ` ?S)" by simp
478   have 2: "inj_on ?F ?S"
479     by(fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)
480   show ?thesis by(rule finite_imageD[OF 1 2])
481 qed
483 lemma not_finite_existsD:
484   assumes "\<not> finite {a. P a}"
485   shows "\<exists>a. P a"
486 proof (rule classical)
487   assume "\<not> (\<exists>a. P a)"
488   with assms show ?thesis by auto
489 qed
492 subsubsection \<open>Further induction rules on finite sets\<close>
494 lemma finite_ne_induct [case_names singleton insert, consumes 2]:
495   assumes "finite F" and "F \<noteq> {}"
496   assumes "\<And>x. P {x}"
497     and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F  \<Longrightarrow> P (insert x F)"
498   shows "P F"
499 using assms
500 proof induct
501   case empty then show ?case by simp
502 next
503   case (insert x F) then show ?case by cases auto
504 qed
506 lemma finite_subset_induct [consumes 2, case_names empty insert]:
507   assumes "finite F" and "F \<subseteq> A"
508   assumes empty: "P {}"
509     and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
510   shows "P F"
511 using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
512 proof induct
513   show "P {}" by fact
514 next
515   fix x F
516   assume "finite F" and "x \<notin> F" and
517     P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
518   show "P (insert x F)"
519   proof (rule insert)
520     from i show "x \<in> A" by blast
521     from i have "F \<subseteq> A" by blast
522     with P show "P F" .
523     show "finite F" by fact
524     show "x \<notin> F" by fact
525   qed
526 qed
528 lemma finite_empty_induct:
529   assumes "finite A"
530   assumes "P A"
531     and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
532   shows "P {}"
533 proof -
534   have "\<And>B. B \<subseteq> A \<Longrightarrow> P (A - B)"
535   proof -
536     fix B :: "'a set"
537     assume "B \<subseteq> A"
538     with \<open>finite A\<close> have "finite B" by (rule rev_finite_subset)
539     from this \<open>B \<subseteq> A\<close> show "P (A - B)"
540     proof induct
541       case empty
542       from \<open>P A\<close> show ?case by simp
543     next
544       case (insert b B)
545       have "P (A - B - {b})"
546       proof (rule remove)
547         from \<open>finite A\<close> show "finite (A - B)" by induct auto
548         from insert show "b \<in> A - B" by simp
549         from insert show "P (A - B)" by simp
550       qed
551       also have "A - B - {b} = A - insert b B" by (rule Diff_insert [symmetric])
552       finally show ?case .
553     qed
554   qed
555   then have "P (A - A)" by blast
556   then show ?thesis by simp
557 qed
559 lemma finite_update_induct [consumes 1, case_names const update]:
560   assumes finite: "finite {a. f a \<noteq> c}"
561   assumes const: "P (\<lambda>a. c)"
562   assumes update: "\<And>a b f. finite {a. f a \<noteq> c} \<Longrightarrow> f a = c \<Longrightarrow> b \<noteq> c \<Longrightarrow> P f \<Longrightarrow> P (f(a := b))"
563   shows "P f"
564 using finite proof (induct "{a. f a \<noteq> c}" arbitrary: f)
565   case empty with const show ?case by simp
566 next
567   case (insert a A)
568   then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c"
569     by auto
570   with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}"
571     by simp
572   have "(f(a := c)) a = c"
573     by simp
574   from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))"
575     by simp
576   with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close> have "P ((f(a := c))(a := f a))"
577     by (rule update)
578   then show ?case by simp
579 qed
582 subsection \<open>Class \<open>finite\<close>\<close>
584 class finite =
585   assumes finite_UNIV: "finite (UNIV :: 'a set)"
586 begin
588 lemma finite [simp]: "finite (A :: 'a set)"
589   by (rule subset_UNIV finite_UNIV finite_subset)+
591 lemma finite_code [code]: "finite (A :: 'a set) \<longleftrightarrow> True"
592   by simp
594 end
596 instance prod :: (finite, finite) finite
597   by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
599 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
600   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
602 instance "fun" :: (finite, finite) finite
603 proof
604   show "finite (UNIV :: ('a => 'b) set)"
605   proof (rule finite_imageD)
606     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
607     have "range ?graph \<subseteq> Pow UNIV" by simp
608     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
609       by (simp only: finite_Pow_iff finite)
610     ultimately show "finite (range ?graph)"
611       by (rule finite_subset)
612     show "inj ?graph" by (rule inj_graph)
613   qed
614 qed
616 instance bool :: finite
617   by standard (simp add: UNIV_bool)
619 instance set :: (finite) finite
620   by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
622 instance unit :: finite
623   by standard (simp add: UNIV_unit)
625 instance sum :: (finite, finite) finite
626   by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
629 subsection \<open>A basic fold functional for finite sets\<close>
631 text \<open>The intended behaviour is
632 \<open>fold f z {x\<^sub>1, ..., x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
633 if \<open>f\<close> is ``left-commutative'':
634 \<close>
636 locale comp_fun_commute =
637   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
638   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
639 begin
641 lemma fun_left_comm: "f y (f x z) = f x (f y z)"
642   using comp_fun_commute by (simp add: fun_eq_iff)
644 lemma commute_left_comp:
645   "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
646   by (simp add: o_assoc comp_fun_commute)
648 end
650 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
651 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
652   emptyI [intro]: "fold_graph f z {} z" |
653   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
654       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
656 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
658 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
659   "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"
661 text\<open>A tempting alternative for the definiens is
662 @{term "if finite A then THE y. fold_graph f z A y else e"}.
663 It allows the removal of finiteness assumptions from the theorems
664 \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
665 The proofs become ugly. It is not worth the effort. (???)\<close>
667 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
668 by (induct rule: finite_induct) auto
671 subsubsection\<open>From @{const fold_graph} to @{term fold}\<close>
673 context comp_fun_commute
674 begin
676 lemma fold_graph_finite:
677   assumes "fold_graph f z A y"
678   shows "finite A"
679   using assms by induct simp_all
681 lemma fold_graph_insertE_aux:
682   "fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
683 proof (induct set: fold_graph)
684   case (insertI x A y) show ?case
685   proof (cases "x = a")
686     assume "x = a" with insertI show ?case by auto
687   next
688     assume "x \<noteq> a"
689     then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
690       using insertI by auto
691     have "f x y = f a (f x y')"
692       unfolding y by (rule fun_left_comm)
693     moreover have "fold_graph f z (insert x A - {a}) (f x y')"
694       using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close>
695       by (simp add: insert_Diff_if fold_graph.insertI)
696     ultimately show ?case by fast
697   qed
698 qed simp
700 lemma fold_graph_insertE:
701   assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
702   obtains y where "v = f x y" and "fold_graph f z A y"
703 using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
705 lemma fold_graph_determ:
706   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
707 proof (induct arbitrary: y set: fold_graph)
708   case (insertI x A y v)
709   from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
710   obtain y' where "v = f x y'" and "fold_graph f z A y'"
711     by (rule fold_graph_insertE)
712   from \<open>fold_graph f z A y'\<close> have "y' = y" by (rule insertI)
713   with \<open>v = f x y'\<close> show "v = f x y" by simp
714 qed fast
716 lemma fold_equality:
717   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
718   by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)
720 lemma fold_graph_fold:
721   assumes "finite A"
722   shows "fold_graph f z A (fold f z A)"
723 proof -
724   from assms have "\<exists>x. fold_graph f z A x" by (rule finite_imp_fold_graph)
725   moreover note fold_graph_determ
726   ultimately have "\<exists>!x. fold_graph f z A x" by (rule ex_ex1I)
727   then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI')
728   with assms show ?thesis by (simp add: fold_def)
729 qed
731 text \<open>The base case for \<open>fold\<close>:\<close>
733 lemma (in -) fold_infinite [simp]:
734   assumes "\<not> finite A"
735   shows "fold f z A = z"
736   using assms by (auto simp add: fold_def)
738 lemma (in -) fold_empty [simp]:
739   "fold f z {} = z"
740   by (auto simp add: fold_def)
742 text\<open>The various recursion equations for @{const fold}:\<close>
744 lemma fold_insert [simp]:
745   assumes "finite A" and "x \<notin> A"
746   shows "fold f z (insert x A) = f x (fold f z A)"
747 proof (rule fold_equality)
748   fix z
749   from \<open>finite A\<close> have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold)
750   with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI)
751   then show "fold_graph f z (insert x A) (f x (fold f z A))" by simp
752 qed
754 declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
755   \<comment> \<open>No more proofs involve these.\<close>
757 lemma fold_fun_left_comm:
758   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
759 proof (induct rule: finite_induct)
760   case empty then show ?case by simp
761 next
762   case (insert y A) then show ?case
763     by (simp add: fun_left_comm [of x])
764 qed
766 lemma fold_insert2:
767   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A)  = fold f (f x z) A"
770 lemma fold_rec:
771   assumes "finite A" and "x \<in> A"
772   shows "fold f z A = f x (fold f z (A - {x}))"
773 proof -
774   have A: "A = insert x (A - {x})" using \<open>x \<in> A\<close> by blast
775   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
776   also have "\<dots> = f x (fold f z (A - {x}))"
777     by (rule fold_insert) (simp add: \<open>finite A\<close>)+
778   finally show ?thesis .
779 qed
781 lemma fold_insert_remove:
782   assumes "finite A"
783   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
784 proof -
785   from \<open>finite A\<close> have "finite (insert x A)" by auto
786   moreover have "x \<in> insert x A" by auto
787   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
788     by (rule fold_rec)
789   then show ?thesis by simp
790 qed
792 lemma fold_set_union_disj:
793   assumes "finite A" "finite B" "A \<inter> B = {}"
794   shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
795 using assms(2,1,3) by induction simp_all
797 end
799 text\<open>Other properties of @{const fold}:\<close>
801 lemma fold_image:
802   assumes "inj_on g A"
803   shows "fold f z (g ` A) = fold (f \<circ> g) z A"
804 proof (cases "finite A")
805   case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def)
806 next
807   case True
808   have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
809   proof
810     fix w
811     show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
812     proof
813       assume ?P then show ?Q using assms
814       proof (induct "g ` A" w arbitrary: A)
815         case emptyI then show ?case by (auto intro: fold_graph.emptyI)
816       next
817         case (insertI x A r B)
818         from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A' where
819           "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
820           by (rule inj_img_insertE)
821         from insertI.prems have "fold_graph (f o g) z A' r"
822           by (auto intro: insertI.hyps)
823         with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
824           by (rule fold_graph.insertI)
825         then show ?case by simp
826       qed
827     next
828       assume ?Q then show ?P using assms
829       proof induct
830         case emptyI thus ?case by (auto intro: fold_graph.emptyI)
831       next
832         case (insertI x A r)
833         from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A" by auto
834         moreover from insertI have "fold_graph f z (g ` A) r" by simp
835         ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
836           by (rule fold_graph.insertI)
837         then show ?case by simp
838       qed
839     qed
840   qed
841   with True assms show ?thesis by (auto simp add: fold_def)
842 qed
844 lemma fold_cong:
845   assumes "comp_fun_commute f" "comp_fun_commute g"
846   assumes "finite A" and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
847     and "s = t" and "A = B"
848   shows "fold f s A = fold g t B"
849 proof -
850   have "fold f s A = fold g s A"
851   using \<open>finite A\<close> cong proof (induct A)
852     case empty then show ?case by simp
853   next
854     case (insert x A)
855     interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
856     interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
857     from insert show ?case by simp
858   qed
859   with assms show ?thesis by simp
860 qed
863 text \<open>A simplified version for idempotent functions:\<close>
865 locale comp_fun_idem = comp_fun_commute +
866   assumes comp_fun_idem: "f x \<circ> f x = f x"
867 begin
869 lemma fun_left_idem: "f x (f x z) = f x z"
870   using comp_fun_idem by (simp add: fun_eq_iff)
872 lemma fold_insert_idem:
873   assumes fin: "finite A"
874   shows "fold f z (insert x A)  = f x (fold f z A)"
875 proof cases
876   assume "x \<in> A"
877   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
878   then show ?thesis using assms by (simp add: comp_fun_idem fun_left_idem)
879 next
880   assume "x \<notin> A" then show ?thesis using assms by simp
881 qed
883 declare fold_insert [simp del] fold_insert_idem [simp]
885 lemma fold_insert_idem2:
886   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
889 end
892 subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
894 lemma (in comp_fun_commute) comp_comp_fun_commute:
895   "comp_fun_commute (f \<circ> g)"
896 proof
899 lemma (in comp_fun_idem) comp_comp_fun_idem:
900   "comp_fun_idem (f \<circ> g)"
901   by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
904 lemma (in comp_fun_commute) comp_fun_commute_funpow:
905   "comp_fun_commute (\<lambda>x. f x ^^ g x)"
906 proof
907   fix y x
908   show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y"
909   proof (cases "x = y")
910     case True then show ?thesis by simp
911   next
912     case False show ?thesis
913     proof (induct "g x" arbitrary: g)
914       case 0 then show ?case by simp
915     next
916       case (Suc n g)
917       have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y"
918       proof (induct "g y" arbitrary: g)
919         case 0 then show ?case by simp
920       next
921         case (Suc n g)
922         define h where "h z = g z - 1" for z
923         with Suc have "n = h y" by simp
924         with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
925           by auto
926         from Suc h_def have "g y = Suc (h y)" by simp
927         then show ?case by (simp add: comp_assoc hyp)
929       qed
930       define h where "h z = (if z = x then g x - 1 else g z)" for z
931       with Suc have "n = h x" by simp
932       with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
933         by auto
934       with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
935       from Suc h_def have "g x = Suc (h x)" by simp
936       then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
938     qed
939   qed
940 qed
943 subsubsection \<open>Expressing set operations via @{const fold}\<close>
945 lemma comp_fun_commute_const:
946   "comp_fun_commute (\<lambda>_. f)"
947 proof
948 qed rule
950 lemma comp_fun_idem_insert:
951   "comp_fun_idem insert"
952 proof
953 qed auto
955 lemma comp_fun_idem_remove:
956   "comp_fun_idem Set.remove"
957 proof
958 qed auto
960 lemma (in semilattice_inf) comp_fun_idem_inf:
961   "comp_fun_idem inf"
962 proof
963 qed (auto simp add: inf_left_commute)
965 lemma (in semilattice_sup) comp_fun_idem_sup:
966   "comp_fun_idem sup"
967 proof
968 qed (auto simp add: sup_left_commute)
970 lemma union_fold_insert:
971   assumes "finite A"
972   shows "A \<union> B = fold insert B A"
973 proof -
974   interpret comp_fun_idem insert by (fact comp_fun_idem_insert)
975   from \<open>finite A\<close> show ?thesis by (induct A arbitrary: B) simp_all
976 qed
978 lemma minus_fold_remove:
979   assumes "finite A"
980   shows "B - A = fold Set.remove B A"
981 proof -
982   interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove)
983   from \<open>finite A\<close> have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto
984   then show ?thesis ..
985 qed
987 lemma comp_fun_commute_filter_fold:
988   "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
989 proof -
990   interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
991   show ?thesis by standard (auto simp: fun_eq_iff)
992 qed
994 lemma Set_filter_fold:
995   assumes "finite A"
996   shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
997 using assms
998 by (induct A)
999   (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
1001 lemma inter_Set_filter:
1002   assumes "finite B"
1003   shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B"
1004 using assms
1005 by (induct B) (auto simp: Set.filter_def)
1007 lemma image_fold_insert:
1008   assumes "finite A"
1009   shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
1010 using assms
1011 proof -
1012   interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by standard auto
1013   show ?thesis using assms by (induct A) auto
1014 qed
1016 lemma Ball_fold:
1017   assumes "finite A"
1018   shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
1019 using assms
1020 proof -
1021   interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by standard auto
1022   show ?thesis using assms by (induct A) auto
1023 qed
1025 lemma Bex_fold:
1026   assumes "finite A"
1027   shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
1028 using assms
1029 proof -
1030   interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by standard auto
1031   show ?thesis using assms by (induct A) auto
1032 qed
1034 lemma comp_fun_commute_Pow_fold:
1035   "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
1036   by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
1038 lemma Pow_fold:
1039   assumes "finite A"
1040   shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A"
1041 using assms
1042 proof -
1043   interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A" by (rule comp_fun_commute_Pow_fold)
1044   show ?thesis using assms by (induct A) (auto simp: Pow_insert)
1045 qed
1047 lemma fold_union_pair:
1048   assumes "finite B"
1049   shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
1050 proof -
1051   interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by standard auto
1052   show ?thesis using assms  by (induct B arbitrary: A) simp_all
1053 qed
1055 lemma comp_fun_commute_product_fold:
1056   assumes "finite B"
1057   shows "comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
1058   by standard (auto simp: fold_union_pair[symmetric] assms)
1060 lemma product_fold:
1061   assumes "finite A"
1062   assumes "finite B"
1063   shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A"
1064 using assms unfolding Sigma_def
1065 by (induct A)
1066   (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
1069 context complete_lattice
1070 begin
1072 lemma inf_Inf_fold_inf:
1073   assumes "finite A"
1074   shows "inf (Inf A) B = fold inf B A"
1075 proof -
1076   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
1077   from \<open>finite A\<close> fold_fun_left_comm show ?thesis by (induct A arbitrary: B)
1079 qed
1081 lemma sup_Sup_fold_sup:
1082   assumes "finite A"
1083   shows "sup (Sup A) B = fold sup B A"
1084 proof -
1085   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
1086   from \<open>finite A\<close> fold_fun_left_comm show ?thesis by (induct A arbitrary: B)
1088 qed
1090 lemma Inf_fold_inf:
1091   assumes "finite A"
1092   shows "Inf A = fold inf top A"
1093   using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
1095 lemma Sup_fold_sup:
1096   assumes "finite A"
1097   shows "Sup A = fold sup bot A"
1098   using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
1100 lemma inf_INF_fold_inf:
1101   assumes "finite A"
1102   shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
1103 proof (rule sym)
1104   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
1105   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
1106   from \<open>finite A\<close> show "?fold = ?inf"
1107     by (induct A arbitrary: B)
1109 qed
1111 lemma sup_SUP_fold_sup:
1112   assumes "finite A"
1113   shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
1114 proof (rule sym)
1115   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
1116   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
1117   from \<open>finite A\<close> show "?fold = ?sup"
1118     by (induct A arbitrary: B)
1120 qed
1122 lemma INF_fold_inf:
1123   assumes "finite A"
1124   shows "INFIMUM A f = fold (inf \<circ> f) top A"
1125   using assms inf_INF_fold_inf [of A top] by simp
1127 lemma SUP_fold_sup:
1128   assumes "finite A"
1129   shows "SUPREMUM A f = fold (sup \<circ> f) bot A"
1130   using assms sup_SUP_fold_sup [of A bot] by simp
1132 end
1135 subsection \<open>Locales as mini-packages for fold operations\<close>
1137 subsubsection \<open>The natural case\<close>
1139 locale folding =
1140   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
1141   fixes z :: "'b"
1142   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
1143 begin
1145 interpretation fold?: comp_fun_commute f
1146   by standard (insert comp_fun_commute, simp add: fun_eq_iff)
1148 definition F :: "'a set \<Rightarrow> 'b"
1149 where
1150   eq_fold: "F A = fold f z A"
1152 lemma empty [simp]:"F {} = z"
1155 lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
1158 lemma insert [simp]:
1159   assumes "finite A" and "x \<notin> A"
1160   shows "F (insert x A) = f x (F A)"
1161 proof -
1162   from fold_insert assms
1163   have "fold f z (insert x A) = f x (fold f z A)" by simp
1164   with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
1165 qed
1167 lemma remove:
1168   assumes "finite A" and "x \<in> A"
1169   shows "F A = f x (F (A - {x}))"
1170 proof -
1171   from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
1172     by (auto dest: mk_disjoint_insert)
1173   moreover from \<open>finite A\<close> A have "finite B" by simp
1174   ultimately show ?thesis by simp
1175 qed
1177 lemma insert_remove:
1178   assumes "finite A"
1179   shows "F (insert x A) = f x (F (A - {x}))"
1180   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
1182 end
1185 subsubsection \<open>With idempotency\<close>
1187 locale folding_idem = folding +
1188   assumes comp_fun_idem: "f x \<circ> f x = f x"
1189 begin
1191 declare insert [simp del]
1193 interpretation fold?: comp_fun_idem f
1194   by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
1196 lemma insert_idem [simp]:
1197   assumes "finite A"
1198   shows "F (insert x A) = f x (F A)"
1199 proof -
1200   from fold_insert_idem assms
1201   have "fold f z (insert x A) = f x (fold f z A)" by simp
1202   with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
1203 qed
1205 end
1208 subsection \<open>Finite cardinality\<close>
1210 text \<open>
1212   @{prop "card A \<equiv> LEAST n. EX f. A = {f i | i. i < n}"}
1213   is ugly to work with.
1214   But now that we have @{const fold} things are easy:
1215 \<close>
1217 global_interpretation card: folding "\<lambda>_. Suc" 0
1218   defines card = "folding.F (\<lambda>_. Suc) 0"
1219   by standard rule
1221 lemma card_infinite:
1222   "\<not> finite A \<Longrightarrow> card A = 0"
1223   by (fact card.infinite)
1225 lemma card_empty:
1226   "card {} = 0"
1227   by (fact card.empty)
1229 lemma card_insert_disjoint:
1230   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
1231   by (fact card.insert)
1233 lemma card_insert_if:
1234   "finite A \<Longrightarrow> card (insert x A) = (if x \<in> A then card A else Suc (card A))"
1235   by auto (simp add: card.insert_remove card.remove)
1237 lemma card_ge_0_finite:
1238   "card A > 0 \<Longrightarrow> finite A"
1239   by (rule ccontr) simp
1241 lemma card_0_eq [simp]:
1242   "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
1243   by (auto dest: mk_disjoint_insert)
1245 lemma finite_UNIV_card_ge_0:
1246   "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
1247   by (rule ccontr) simp
1249 lemma card_eq_0_iff:
1250   "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
1251   by auto
1253 lemma card_gt_0_iff:
1254   "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
1255   by (simp add: neq0_conv [symmetric] card_eq_0_iff)
1257 lemma card_Suc_Diff1:
1258   "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
1259 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1260 apply(simp del:insert_Diff_single)
1261 done
1263 lemma card_insert_le_m1: "n>0 \<Longrightarrow> card y \<le> n-1 \<Longrightarrow> card (insert x y) \<le> n"
1264   apply (cases "finite y")
1265   apply (cases "x \<in> y")
1266   apply (auto simp: insert_absorb)
1267   done
1269 lemma card_Diff_singleton:
1270   "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
1271   by (simp add: card_Suc_Diff1 [symmetric])
1273 lemma card_Diff_singleton_if:
1274   "finite A \<Longrightarrow> card (A - {x}) = (if x \<in> A then card A - 1 else card A)"
1277 lemma card_Diff_insert[simp]:
1278   assumes "finite A" and "a \<in> A" and "a \<notin> B"
1279   shows "card (A - insert a B) = card (A - B) - 1"
1280 proof -
1281   have "A - insert a B = (A - B) - {a}" using assms by blast
1282   then show ?thesis using assms by(simp add: card_Diff_singleton)
1283 qed
1285 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
1286   by (fact card.insert_remove)
1288 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
1291 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"
1292 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
1294 lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = Suc n"
1295 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)
1297 lemma card_mono:
1298   assumes "finite B" and "A \<subseteq> B"
1299   shows "card A \<le> card B"
1300 proof -
1301   from assms have "finite A" by (auto intro: finite_subset)
1302   then show ?thesis using assms proof (induct A arbitrary: B)
1303     case empty then show ?case by simp
1304   next
1305     case (insert x A)
1306     then have "x \<in> B" by simp
1307     from insert have "A \<subseteq> B - {x}" and "finite (B - {x})" by auto
1308     with insert.hyps have "card A \<le> card (B - {x})" by auto
1309     with \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case by simp (simp only: card.remove)
1310   qed
1311 qed
1313 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1314 apply (induct rule: finite_induct)
1315 apply simp
1316 apply clarify
1317 apply (subgoal_tac "finite A & A - {x} <= F")
1318  prefer 2 apply (blast intro: finite_subset, atomize)
1319 apply (drule_tac x = "A - {x}" in spec)
1321 apply (case_tac "card A", auto)
1322 done
1324 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
1325 apply (simp add: psubset_eq linorder_not_le [symmetric])
1326 apply (blast dest: card_seteq)
1327 done
1329 lemma card_Un_Int:
1330   assumes "finite A" and "finite B"
1331   shows "card A + card B = card (A \<union> B) + card (A \<inter> B)"
1332 using assms proof (induct A)
1333   case empty then show ?case by simp
1334 next
1335  case (insert x A) then show ?case
1336     by (auto simp add: insert_absorb Int_insert_left)
1337 qed
1339 lemma card_Un_disjoint:
1340   assumes "finite A" and "finite B"
1341   assumes "A \<inter> B = {}"
1342   shows "card (A \<union> B) = card A + card B"
1343 using assms card_Un_Int [of A B] by simp
1345 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
1346 apply(cases "finite A")
1347  apply(cases "finite B")
1348   using le_iff_add card_Un_Int apply blast
1349  apply simp
1350 apply simp
1351 done
1353 lemma card_Diff_subset:
1354   assumes "finite B" and "B \<subseteq> A"
1355   shows "card (A - B) = card A - card B"
1356 proof (cases "finite A")
1357   case False with assms show ?thesis by simp
1358 next
1359   case True with assms show ?thesis by (induct B arbitrary: A) simp_all
1360 qed
1362 lemma card_Diff_subset_Int:
1363   assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
1364 proof -
1365   have "A - B = A - A \<inter> B" by auto
1366   thus ?thesis
1367     by (simp add: card_Diff_subset AB)
1368 qed
1370 lemma diff_card_le_card_Diff:
1371 assumes "finite B" shows "card A - card B \<le> card(A - B)"
1372 proof-
1373   have "card A - card B \<le> card A - card (A \<inter> B)"
1374     using card_mono[OF assms Int_lower2, of A] by arith
1375   also have "\<dots> = card(A-B)" using assms by(simp add: card_Diff_subset_Int)
1376   finally show ?thesis .
1377 qed
1379 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
1380 apply (rule Suc_less_SucD)
1381 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
1382 done
1384 lemma card_Diff2_less:
1385   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
1386 apply (case_tac "x = y")
1387  apply (simp add: card_Diff1_less del:card_Diff_insert)
1388 apply (rule less_trans)
1389  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
1390 done
1392 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
1393 apply (case_tac "x : A")
1394  apply (simp_all add: card_Diff1_less less_imp_le)
1395 done
1397 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
1398 by (erule psubsetI, blast)
1400 lemma card_le_inj:
1401   assumes fA: "finite A"
1402     and fB: "finite B"
1403     and c: "card A \<le> card B"
1404   shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
1405   using fA fB c
1406 proof (induct arbitrary: B rule: finite_induct)
1407   case empty
1408   then show ?case by simp
1409 next
1410   case (insert x s t)
1411   then show ?case
1412   proof (induct rule: finite_induct[OF "insert.prems"(1)])
1413     case 1
1414     then show ?case by simp
1415   next
1416     case (2 y t)
1417     from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
1418       by simp
1419     from "2.prems"(3) [OF "2.hyps"(1) cst]
1420     obtain f where "f ` s \<subseteq> t" "inj_on f s"
1421       by blast
1422     with "2.prems"(2) "2.hyps"(2) show ?case
1423       apply -
1424       apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
1425       apply (auto simp add: inj_on_def)
1426       done
1427   qed
1428 qed
1430 lemma card_subset_eq:
1431   assumes fB: "finite B"
1432     and AB: "A \<subseteq> B"
1433     and c: "card A = card B"
1434   shows "A = B"
1435 proof -
1436   from fB AB have fA: "finite A"
1437     by (auto intro: finite_subset)
1438   from fA fB have fBA: "finite (B - A)"
1439     by auto
1440   have e: "A \<inter> (B - A) = {}"
1441     by blast
1442   have eq: "A \<union> (B - A) = B"
1443     using AB by blast
1444   from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
1445     by arith
1446   then have "B - A = {}"
1447     unfolding card_eq_0_iff using fA fB by simp
1448   with AB show "A = B"
1449     by blast
1450 qed
1452 lemma insert_partition:
1453   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
1454   \<Longrightarrow> x \<inter> \<Union>F = {}"
1455 by auto
1457 lemma finite_psubset_induct[consumes 1, case_names psubset]:
1458   assumes fin: "finite A"
1459   and     major: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A"
1460   shows "P A"
1461 using fin
1462 proof (induct A taking: card rule: measure_induct_rule)
1463   case (less A)
1464   have fin: "finite A" by fact
1465   have ih: "\<And>B. \<lbrakk>card B < card A; finite B\<rbrakk> \<Longrightarrow> P B" by fact
1466   { fix B
1467     assume asm: "B \<subset> A"
1468     from asm have "card B < card A" using psubset_card_mono fin by blast
1469     moreover
1470     from asm have "B \<subseteq> A" by auto
1471     then have "finite B" using fin finite_subset by blast
1472     ultimately
1473     have "P B" using ih by simp
1474   }
1475   with fin show "P A" using major by blast
1476 qed
1478 lemma finite_induct_select[consumes 1, case_names empty select]:
1479   assumes "finite S"
1480   assumes "P {}"
1481   assumes select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
1482   shows "P S"
1483 proof -
1484   have "0 \<le> card S" by simp
1485   then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
1486   proof (induct rule: dec_induct)
1487     case base with \<open>P {}\<close> show ?case
1488       by (intro exI[of _ "{}"]) auto
1489   next
1490     case (step n)
1491     then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
1492       by auto
1493     with \<open>n < card S\<close> have "T \<subset> S" "P T"
1494       by auto
1495     with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
1496       by auto
1497     with step(2) T \<open>finite S\<close> show ?case
1498       by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
1499   qed
1500   with \<open>finite S\<close> show "P S"
1501     by (auto dest: card_subset_eq)
1502 qed
1504 lemma remove_induct [case_names empty infinite remove]:
1505   assumes empty: "P ({} :: 'a set)" and infinite: "\<not>finite B \<Longrightarrow> P B"
1506       and remove: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
1507   shows "P B"
1508 proof (cases "finite B")
1509   assume "\<not>finite B"
1510   thus ?thesis by (rule infinite)
1511 next
1512   define A where "A = B"
1513   assume "finite B"
1514   hence "finite A" "A \<subseteq> B" by (simp_all add: A_def)
1515   thus "P A"
1516   proof (induction "card A" arbitrary: A)
1517     case 0
1518     hence "A = {}" by auto
1519     with empty show ?case by simp
1520   next
1521     case (Suc n A)
1522     from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A" by (rule finite_subset)
1523     moreover from Suc.hyps have "A \<noteq> {}" by auto
1524     moreover note \<open>A \<subseteq> B\<close>
1525     moreover have "P (A - {x})" if x: "x \<in> A" for x
1526       using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
1527     ultimately show ?case by (rule remove)
1528   qed
1529 qed
1531 lemma finite_remove_induct [consumes 1, case_names empty remove]:
1532   assumes finite: "finite B" and empty: "P ({} :: 'a set)"
1533       and rm: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
1534   defines "B' \<equiv> B"
1535   shows   "P B'"
1536   by (induction B' rule: remove_induct) (simp_all add: assms)
1539 text\<open>main cardinality theorem\<close>
1540 lemma card_partition [rule_format]:
1541   "finite C ==>
1542      finite (\<Union>C) -->
1543      (\<forall>c\<in>C. card c = k) -->
1544      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
1545      k * card(C) = card (\<Union>C)"
1546 apply (erule finite_induct, simp)
1547 apply (simp add: card_Un_disjoint insert_partition
1548        finite_subset [of _ "\<Union>(insert x F)"])
1549 done
1551 lemma card_eq_UNIV_imp_eq_UNIV:
1552   assumes fin: "finite (UNIV :: 'a set)"
1553   and card: "card A = card (UNIV :: 'a set)"
1554   shows "A = (UNIV :: 'a set)"
1555 proof
1556   show "A \<subseteq> UNIV" by simp
1557   show "UNIV \<subseteq> A"
1558   proof
1559     fix x
1560     show "x \<in> A"
1561     proof (rule ccontr)
1562       assume "x \<notin> A"
1563       then have "A \<subset> UNIV" by auto
1564       with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
1565       with card show False by simp
1566     qed
1567   qed
1568 qed
1570 text\<open>The form of a finite set of given cardinality\<close>
1572 lemma card_eq_SucD:
1573 assumes "card A = Suc k"
1574 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
1575 proof -
1576   have fin: "finite A" using assms by (auto intro: ccontr)
1577   moreover have "card A \<noteq> 0" using assms by auto
1578   ultimately obtain b where b: "b \<in> A" by auto
1579   show ?thesis
1580   proof (intro exI conjI)
1581     show "A = insert b (A-{b})" using b by blast
1582     show "b \<notin> A - {b}" by blast
1583     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
1584       using assms b fin by(fastforce dest:mk_disjoint_insert)+
1585   qed
1586 qed
1588 lemma card_Suc_eq:
1589   "(card A = Suc k) =
1590    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
1591  apply(auto elim!: card_eq_SucD)
1592  apply(subst card.insert)
1594  done
1596 lemma card_1_singletonE:
1597     assumes "card A = 1" obtains x where "A = {x}"
1598   using assms by (auto simp: card_Suc_eq)
1600 lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
1601   unfolding is_singleton_def
1602   by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
1604 lemma card_le_Suc_iff: "finite A \<Longrightarrow>
1605   Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
1606 by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
1607   dest: subset_singletonD split: nat.splits if_splits)
1609 lemma finite_fun_UNIVD2:
1610   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1611   shows "finite (UNIV :: 'b set)"
1612 proof -
1613   from fin have "\<And>arbitrary. finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1614     by (rule finite_imageI)
1615   moreover have "\<And>arbitrary. UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1616     by (rule UNIV_eq_I) auto
1617   ultimately show "finite (UNIV :: 'b set)" by simp
1618 qed
1620 lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
1621   unfolding UNIV_unit by simp
1623 lemma infinite_arbitrarily_large:
1624   assumes "\<not> finite A"
1625   shows "\<exists>B. finite B \<and> card B = n \<and> B \<subseteq> A"
1626 proof (induction n)
1627   case 0 show ?case by (intro exI[of _ "{}"]) auto
1628 next
1629   case (Suc n)
1630   then guess B .. note B = this
1631   with \<open>\<not> finite A\<close> have "A \<noteq> B" by auto
1632   with B have "B \<subset> A" by auto
1633   hence "\<exists>x. x \<in> A - B" by (elim psubset_imp_ex_mem)
1634   then guess x .. note x = this
1635   with B have "finite (insert x B) \<and> card (insert x B) = Suc n \<and> insert x B \<subseteq> A"
1636     by auto
1637   thus "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
1638 qed
1640 subsubsection \<open>Cardinality of image\<close>
1642 lemma card_image_le: "finite A ==> card (f ` A) \<le> card A"
1643   by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
1645 lemma card_image:
1646   assumes "inj_on f A"
1647   shows "card (f ` A) = card A"
1648 proof (cases "finite A")
1649   case True then show ?thesis using assms by (induct A) simp_all
1650 next
1651   case False then have "\<not> finite (f ` A)" using assms by (auto dest: finite_imageD)
1652   with False show ?thesis by simp
1653 qed
1655 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
1656 by(auto simp: card_image bij_betw_def)
1658 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
1659 by (simp add: card_seteq card_image)
1661 lemma eq_card_imp_inj_on:
1662   assumes "finite A" "card(f ` A) = card A" shows "inj_on f A"
1663 using assms
1664 proof (induct rule:finite_induct)
1665   case empty show ?case by simp
1666 next
1667   case (insert x A)
1668   then show ?case using card_image_le [of A f]
1669     by (simp add: card_insert_if split: if_splits)
1670 qed
1672 lemma inj_on_iff_eq_card: "finite A \<Longrightarrow> inj_on f A \<longleftrightarrow> card(f ` A) = card A"
1673   by (blast intro: card_image eq_card_imp_inj_on)
1675 lemma card_inj_on_le:
1676   assumes "inj_on f A" "f ` A \<subseteq> B" "finite B" shows "card A \<le> card B"
1677 proof -
1678   have "finite A" using assms
1679     by (blast intro: finite_imageD dest: finite_subset)
1680   then show ?thesis using assms
1681    by (force intro: card_mono simp: card_image [symmetric])
1682 qed
1684 lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
1685   by (blast intro: card_image_le card_mono le_trans)
1687 lemma card_bij_eq:
1688   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
1689      finite A; finite B |] ==> card A = card B"
1690 by (auto intro: le_antisym card_inj_on_le)
1692 lemma bij_betw_finite:
1693   assumes "bij_betw f A B"
1694   shows "finite A \<longleftrightarrow> finite B"
1695 using assms unfolding bij_betw_def
1696 using finite_imageD[of f A] by auto
1698 lemma inj_on_finite:
1699 assumes "inj_on f A" "f ` A \<le> B" "finite B"
1700 shows "finite A"
1701 using assms finite_imageD finite_subset by blast
1703 lemma card_vimage_inj: "\<lbrakk> inj f; A \<subseteq> range f \<rbrakk> \<Longrightarrow> card (f -` A) = card A"
1704 by(auto 4 3 simp add: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on])
1706 subsubsection \<open>Pigeonhole Principles\<close>
1708 lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
1709 by (auto dest: card_image less_irrefl_nat)
1711 lemma pigeonhole_infinite:
1712 assumes  "~ finite A" and "finite(f`A)"
1713 shows "EX a0:A. ~finite{a:A. f a = f a0}"
1714 proof -
1715   have "finite(f`A) \<Longrightarrow> ~ finite A \<Longrightarrow> EX a0:A. ~finite{a:A. f a = f a0}"
1716   proof(induct "f`A" arbitrary: A rule: finite_induct)
1717     case empty thus ?case by simp
1718   next
1719     case (insert b F)
1720     show ?case
1721     proof cases
1722       assume "finite{a:A. f a = b}"
1723       hence "~ finite(A - {a:A. f a = b})" using \<open>\<not> finite A\<close> by simp
1724       also have "A - {a:A. f a = b} = {a:A. f a \<noteq> b}" by blast
1725       finally have "~ finite({a:A. f a \<noteq> b})" .
1726       from insert(3)[OF _ this]
1727       show ?thesis using insert(2,4) by simp (blast intro: rev_finite_subset)
1728     next
1729       assume 1: "~finite{a:A. f a = b}"
1730       hence "{a \<in> A. f a = b} \<noteq> {}" by force
1731       thus ?thesis using 1 by blast
1732     qed
1733   qed
1734   from this[OF assms(2,1)] show ?thesis .
1735 qed
1737 lemma pigeonhole_infinite_rel:
1738 assumes "~finite A" and "finite B" and "ALL a:A. EX b:B. R a b"
1739 shows "EX b:B. ~finite{a:A. R a b}"
1740 proof -
1741    let ?F = "%a. {b:B. R a b}"
1742    from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>]
1743    have "finite(?F ` A)" by(blast intro: rev_finite_subset)
1744    from pigeonhole_infinite[where f = ?F, OF assms(1) this]
1745    obtain a0 where "a0\<in>A" and 1: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
1746    obtain b0 where "b0 : B" and "R a0 b0" using \<open>a0:A\<close> assms(3) by blast
1747    { assume "finite{a:A. R a b0}"
1748      then have "finite {a\<in>A. ?F a = ?F a0}"
1749        using \<open>b0 : B\<close> \<open>R a0 b0\<close> by(blast intro: rev_finite_subset)
1750    }
1751    with 1 \<open>b0 : B\<close> show ?thesis by blast
1752 qed
1755 subsubsection \<open>Cardinality of sums\<close>
1757 lemma card_Plus:
1758   assumes "finite A" and "finite B"
1759   shows "card (A <+> B) = card A + card B"
1760 proof -
1761   have "Inl`A \<inter> Inr`B = {}" by fast
1762   with assms show ?thesis
1763     unfolding Plus_def
1764     by (simp add: card_Un_disjoint card_image)
1765 qed
1767 lemma card_Plus_conv_if:
1768   "card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)"
1769   by (auto simp add: card_Plus)
1771 text \<open>Relates to equivalence classes.  Based on a theorem of F. Kamm\"uller.\<close>
1773 lemma dvd_partition:
1774   assumes f: "finite (\<Union>C)" and "\<forall>c\<in>C. k dvd card c" "\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}"
1775     shows "k dvd card (\<Union>C)"
1776 proof -
1777   have "finite C"
1778     by (rule finite_UnionD [OF f])
1779   then show ?thesis using assms
1780   proof (induct rule: finite_induct)
1781     case empty show ?case by simp
1782   next
1783     case (insert c C)
1784     then show ?case
1785       apply simp
1786       apply (subst card_Un_disjoint)
1787       apply (auto simp add: disjoint_eq_subset_Compl)
1788       done
1789   qed
1790 qed
1792 subsubsection \<open>Relating injectivity and surjectivity\<close>
1794 lemma finite_surj_inj: assumes "finite A" "A \<subseteq> f ` A" shows "inj_on f A"
1795 proof -
1796   have "f ` A = A"
1797     by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le)
1798   then show ?thesis using assms
1800 qed
1802 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
1803 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
1804 by (blast intro: finite_surj_inj subset_UNIV)
1806 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
1807 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
1808 by(fastforce simp:surj_def dest!: endo_inj_surj)
1810 corollary infinite_UNIV_nat [iff]:
1811   "\<not> finite (UNIV :: nat set)"
1812 proof
1813   assume "finite (UNIV :: nat set)"
1814   with finite_UNIV_inj_surj [of Suc]
1815   show False by simp (blast dest: Suc_neq_Zero surjD)
1816 qed
1818 lemma infinite_UNIV_char_0:
1819   "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
1820 proof
1821   assume "finite (UNIV :: 'a set)"
1822   with subset_UNIV have "finite (range of_nat :: 'a set)"
1823     by (rule finite_subset)
1824   moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
1826   ultimately have "finite (UNIV :: nat set)"
1827     by (rule finite_imageD)
1828   then show False
1829     by simp
1830 qed
1832 hide_const (open) Finite_Set.fold
1835 subsection "Infinite Sets"
1837 text \<open>
1838   Some elementary facts about infinite sets, mostly by Stephan Merz.
1839   Beware! Because "infinite" merely abbreviates a negation, these
1840   lemmas may not work well with \<open>blast\<close>.
1841 \<close>
1843 abbreviation infinite :: "'a set \<Rightarrow> bool"
1844   where "infinite S \<equiv> \<not> finite S"
1846 text \<open>
1847   Infinite sets are non-empty, and if we remove some elements from an
1848   infinite set, the result is still infinite.
1849 \<close>
1851 lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
1852   by auto
1854 lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
1855   by simp
1857 lemma Diff_infinite_finite:
1858   assumes T: "finite T" and S: "infinite S"
1859   shows "infinite (S - T)"
1860   using T
1861 proof induct
1862   from S
1863   show "infinite (S - {})" by auto
1864 next
1865   fix T x
1866   assume ih: "infinite (S - T)"
1867   have "S - (insert x T) = (S - T) - {x}"
1868     by (rule Diff_insert)
1869   with ih
1870   show "infinite (S - (insert x T))"
1872 qed
1874 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
1875   by simp
1877 lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
1878   by simp
1880 lemma infinite_super:
1881   assumes T: "S \<subseteq> T" and S: "infinite S"
1882   shows "infinite T"
1883 proof
1884   assume "finite T"
1885   with T have "finite S" by (simp add: finite_subset)
1886   with S show False by simp
1887 qed
1889 proposition infinite_coinduct [consumes 1, case_names infinite]:
1890   assumes "X A"
1891   and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
1892   shows "infinite A"
1893 proof
1894   assume "finite A"
1895   then show False using \<open>X A\<close>
1896   proof (induction rule: finite_psubset_induct)
1897     case (psubset A)
1898     then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})"
1899       using local.step psubset.prems by blast
1900     then have "X (A - {x})"
1901       using psubset.hyps by blast
1902     show False
1903       apply (rule psubset.IH [where B = "A - {x}"])
1904       using \<open>x \<in> A\<close> apply blast
1905       by (simp add: \<open>X (A - {x})\<close>)
1906   qed
1907 qed
1909 text \<open>
1910   For any function with infinite domain and finite range there is some
1911   element that is the image of infinitely many domain elements.  In
1912   particular, any infinite sequence of elements from a finite set
1913   contains some element that occurs infinitely often.
1914 \<close>
1916 lemma inf_img_fin_dom':
1917   assumes img: "finite (f ` A)" and dom: "infinite A"
1918   shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
1919 proof (rule ccontr)
1920   have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
1921   moreover
1922   assume "\<not> ?thesis"
1923   with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
1924   ultimately have "finite A" by(rule finite_subset)
1925   with dom show False by contradiction
1926 qed
1928 lemma inf_img_fin_domE':
1929   assumes "finite (f ` A)" and "infinite A"
1930   obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
1931   using assms by (blast dest: inf_img_fin_dom')
1933 lemma inf_img_fin_dom:
1934   assumes img: "finite (f`A)" and dom: "infinite A"
1935   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
1936 using inf_img_fin_dom'[OF assms] by auto
1938 lemma inf_img_fin_domE:
1939   assumes "finite (f`A)" and "infinite A"
1940   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
1941   using assms by (blast dest: inf_img_fin_dom)
1943 proposition finite_image_absD:
1944     fixes S :: "'a::linordered_ring set"
1945     shows "finite (abs ` S) \<Longrightarrow> finite S"
1946   by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
1948 end