src/HOL/Finite_Set.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63982 4c4049e3bad8 child 67443 3abf6a722518 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
1 (*  Title:      HOL/Finite_Set.thy
2     Author:     Tobias Nipkow
3     Author:     Lawrence C Paulson
4     Author:     Markus Wenzel
5     Author:     Jeremy Avigad
6     Author:     Andrei Popescu
7 *)
9 section \<open>Finite sets\<close>
11 theory Finite_Set
12   imports Product_Type Sum_Type Fields
13 begin
15 subsection \<open>Predicate for finite sets\<close>
17 context notes [[inductive_internals]]
18 begin
20 inductive finite :: "'a set \<Rightarrow> bool"
21   where
22     emptyI [simp, intro!]: "finite {}"
23   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
25 end
27 simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
29 declare [[simproc del: finite_Collect]]
31 lemma finite_induct [case_names empty insert, induct set: finite]:
32   \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
33   assumes "finite F"
34   assumes "P {}"
35     and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
36   shows "P F"
37   using \<open>finite F\<close>
38 proof induct
39   show "P {}" by fact
40 next
41   fix x F
42   assume F: "finite F" and P: "P F"
43   show "P (insert x F)"
44   proof cases
45     assume "x \<in> F"
46     then have "insert x F = F" by (rule insert_absorb)
47     with P show ?thesis by (simp only:)
48   next
49     assume "x \<notin> F"
50     from F this P show ?thesis by (rule insert)
51   qed
52 qed
54 lemma infinite_finite_induct [case_names infinite empty insert]:
55   assumes infinite: "\<And>A. \<not> finite A \<Longrightarrow> P A"
56     and empty: "P {}"
57     and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
58   shows "P A"
59 proof (cases "finite A")
60   case False
61   with infinite show ?thesis .
62 next
63   case True
64   then show ?thesis by (induct A) (fact empty insert)+
65 qed
68 subsubsection \<open>Choice principles\<close>
70 lemma ex_new_if_finite: \<comment> "does not depend on def of finite at all"
71   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
72   shows "\<exists>a::'a. a \<notin> A"
73 proof -
74   from assms have "A \<noteq> UNIV" by blast
75   then show ?thesis by blast
76 qed
78 text \<open>A finite choice principle. Does not need the SOME choice operator.\<close>
80 lemma finite_set_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
81 proof (induct rule: finite_induct)
82   case empty
83   then show ?case by simp
84 next
85   case (insert a A)
86   then obtain f b where f: "\<forall>x\<in>A. P x (f x)" and ab: "P a b"
87     by auto
88   show ?case (is "\<exists>f. ?P f")
89   proof
90     show "?P (\<lambda>x. if x = a then b else f x)"
91       using f ab by auto
92   qed
93 qed
96 subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close>
98 lemma finite_imp_nat_seg_image_inj_on:
99   assumes "finite A"
100   shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
101   using assms
102 proof induct
103   case empty
104   show ?case
105   proof
106     show "\<exists>f. {} = f ` {i::nat. i < 0} \<and> inj_on f {i. i < 0}"
107       by simp
108   qed
109 next
110   case (insert a A)
111   have notinA: "a \<notin> A" by fact
112   from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}"
113     by blast
114   then have "insert a A = f(n:=a) ` {i. i < Suc n}" and "inj_on (f(n:=a)) {i. i < Suc n}"
115     using notinA by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
116   then show ?case by blast
117 qed
119 lemma nat_seg_image_imp_finite: "A = f ` {i::nat. i < n} \<Longrightarrow> finite A"
120 proof (induct n arbitrary: A)
121   case 0
122   then show ?case by simp
123 next
124   case (Suc n)
125   let ?B = "f ` {i. i < n}"
126   have finB: "finite ?B" by (rule Suc.hyps[OF refl])
127   show ?case
128   proof (cases "\<exists>k<n. f n = f k")
129     case True
130     then have "A = ?B"
131       using Suc.prems by (auto simp:less_Suc_eq)
132     then show ?thesis
133       using finB by simp
134   next
135     case False
136     then have "A = insert (f n) ?B"
137       using Suc.prems by (auto simp:less_Suc_eq)
138     then show ?thesis using finB by simp
139   qed
140 qed
142 lemma finite_conv_nat_seg_image: "finite A \<longleftrightarrow> (\<exists>n f. A = f ` {i::nat. i < n})"
143   by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
145 lemma finite_imp_inj_to_nat_seg:
146   assumes "finite A"
147   shows "\<exists>f n. f ` A = {i::nat. i < n} \<and> inj_on f A"
148 proof -
149   from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
150   obtain f and n :: nat where bij: "bij_betw f {i. i<n} A"
151     by (auto simp: bij_betw_def)
152   let ?f = "the_inv_into {i. i<n} f"
153   have "inj_on ?f A \<and> ?f ` A = {i. i<n}"
154     by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
155   then show ?thesis by blast
156 qed
158 lemma finite_Collect_less_nat [iff]: "finite {n::nat. n < k}"
159   by (fastforce simp: finite_conv_nat_seg_image)
161 lemma finite_Collect_le_nat [iff]: "finite {n::nat. n \<le> k}"
162   by (simp add: le_eq_less_or_eq Collect_disj_eq)
165 subsubsection \<open>Finiteness and common set operations\<close>
167 lemma rev_finite_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A"
168 proof (induct arbitrary: A rule: finite_induct)
169   case empty
170   then show ?case by simp
171 next
172   case (insert x F A)
173   have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F \<Longrightarrow> finite (A - {x})"
174     by fact+
175   show "finite A"
176   proof cases
177     assume x: "x \<in> A"
178     with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
179     with r have "finite (A - {x})" .
180     then have "finite (insert x (A - {x}))" ..
181     also have "insert x (A - {x}) = A"
182       using x by (rule insert_Diff)
183     finally show ?thesis .
184   next
185     show ?thesis when "A \<subseteq> F"
186       using that by fact
187     assume "x \<notin> A"
188     with A show "A \<subseteq> F"
189       by (simp add: subset_insert_iff)
190   qed
191 qed
193 lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
194   by (rule rev_finite_subset)
196 lemma finite_UnI:
197   assumes "finite F" and "finite G"
198   shows "finite (F \<union> G)"
199   using assms by induct simp_all
201 lemma finite_Un [iff]: "finite (F \<union> G) \<longleftrightarrow> finite F \<and> finite G"
202   by (blast intro: finite_UnI finite_subset [of _ "F \<union> G"])
204 lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A"
205 proof -
206   have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp
207   then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un)
208   then show ?thesis by simp
209 qed
211 lemma finite_Int [simp, intro]: "finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)"
212   by (blast intro: finite_subset)
214 lemma finite_Collect_conjI [simp, intro]:
215   "finite {x. P x} \<or> finite {x. Q x} \<Longrightarrow> finite {x. P x \<and> Q x}"
216   by (simp add: Collect_conj_eq)
218 lemma finite_Collect_disjI [simp]:
219   "finite {x. P x \<or> Q x} \<longleftrightarrow> finite {x. P x} \<and> finite {x. Q x}"
220   by (simp add: Collect_disj_eq)
222 lemma finite_Diff [simp, intro]: "finite A \<Longrightarrow> finite (A - B)"
223   by (rule finite_subset, rule Diff_subset)
225 lemma finite_Diff2 [simp]:
226   assumes "finite B"
227   shows "finite (A - B) \<longleftrightarrow> finite A"
228 proof -
229   have "finite A \<longleftrightarrow> finite ((A - B) \<union> (A \<inter> B))"
230     by (simp add: Un_Diff_Int)
231   also have "\<dots> \<longleftrightarrow> finite (A - B)"
232     using \<open>finite B\<close> by simp
233   finally show ?thesis ..
234 qed
236 lemma finite_Diff_insert [iff]: "finite (A - insert a B) \<longleftrightarrow> finite (A - B)"
237 proof -
238   have "finite (A - B) \<longleftrightarrow> finite (A - B - {a})" by simp
239   moreover have "A - insert a B = A - B - {a}" by auto
240   ultimately show ?thesis by simp
241 qed
243 lemma finite_compl [simp]:
244   "finite (A :: 'a set) \<Longrightarrow> finite (- A) \<longleftrightarrow> finite (UNIV :: 'a set)"
245   by (simp add: Compl_eq_Diff_UNIV)
247 lemma finite_Collect_not [simp]:
248   "finite {x :: 'a. P x} \<Longrightarrow> finite {x. \<not> P x} \<longleftrightarrow> finite (UNIV :: 'a set)"
249   by (simp add: Collect_neg_eq)
251 lemma finite_Union [simp, intro]:
252   "finite A \<Longrightarrow> (\<And>M. M \<in> A \<Longrightarrow> finite M) \<Longrightarrow> finite (\<Union>A)"
253   by (induct rule: finite_induct) simp_all
255 lemma finite_UN_I [intro]:
256   "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
257   by (induct rule: finite_induct) simp_all
259 lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
260   by (blast intro: finite_subset)
262 lemma finite_Inter [intro]: "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
263   by (blast intro: Inter_lower finite_subset)
265 lemma finite_INT [intro]: "\<exists>x\<in>I. finite (A x) \<Longrightarrow> finite (\<Inter>x\<in>I. A x)"
266   by (blast intro: INT_lower finite_subset)
268 lemma finite_imageI [simp, intro]: "finite F \<Longrightarrow> finite (h ` F)"
269   by (induct rule: finite_induct) simp_all
271 lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow> finite {f x |x. P x}"
272   by (simp add: image_Collect [symmetric])
274 lemma finite_image_set2:
275   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y |x y. P x \<and> Q y}"
276   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
278 lemma finite_imageD:
279   assumes "finite (f ` A)" and "inj_on f A"
280   shows "finite A"
281   using assms
282 proof (induct "f ` A" arbitrary: A)
283   case empty
284   then show ?case by simp
285 next
286   case (insert x B)
287   then have B_A: "insert x B = f ` A"
288     by simp
289   then obtain y where "x = f y" and "y \<in> A"
290     by blast
291   from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
292     by blast
293   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})"
294     by (simp add: inj_on_image_set_diff Set.Diff_subset)
295   moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
296     by (rule inj_on_diff)
297   ultimately have "finite (A - {y})"
298     by (rule insert.hyps)
299   then show "finite A"
300     by simp
301 qed
303 lemma finite_image_iff: "inj_on f A \<Longrightarrow> finite (f ` A) \<longleftrightarrow> finite A"
304   using finite_imageD by blast
306 lemma finite_surj: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
307   by (erule finite_subset) (rule finite_imageI)
309 lemma finite_range_imageI: "finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))"
310   by (drule finite_imageI) (simp add: range_composition)
312 lemma finite_subset_image:
313   assumes "finite B"
314   shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
315   using assms
316 proof induct
317   case empty
318   then show ?case by simp
319 next
320   case insert
321   then show ?case
322     by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast  (* slow *)
323 qed
325 lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
326   apply (induct rule: finite_induct)
327    apply simp_all
328   apply (subst vimage_insert)
329   apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
330   done
332 lemma finite_finite_vimage_IntI:
333   assumes "finite F"
334     and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
335   shows "finite (h -` F \<inter> A)"
336 proof -
337   have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
338     by blast
339   show ?thesis
340     by (simp only: * assms finite_UN_I)
341 qed
343 lemma finite_vimageI: "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
344   using finite_vimage_IntI[of F h UNIV] by auto
346 lemma finite_vimageD': "finite (f -` A) \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> finite A"
347   by (auto simp add: subset_image_iff intro: finite_subset[rotated])
349 lemma finite_vimageD: "finite (h -` F) \<Longrightarrow> surj h \<Longrightarrow> finite F"
350   by (auto dest: finite_vimageD')
352 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
353   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
355 lemma finite_Collect_bex [simp]:
356   assumes "finite A"
357   shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
358 proof -
359   have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto
360   with assms show ?thesis by simp
361 qed
363 lemma finite_Collect_bounded_ex [simp]:
364   assumes "finite {y. P y}"
365   shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})"
366 proof -
367   have "{x. \<exists>y. P y \<and> Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})"
368     by auto
369   with assms show ?thesis
370     by simp
371 qed
373 lemma finite_Plus: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)"
374   by (simp add: Plus_def)
376 lemma finite_PlusD:
377   fixes A :: "'a set" and B :: "'b set"
378   assumes fin: "finite (A <+> B)"
379   shows "finite A" "finite B"
380 proof -
381   have "Inl ` A \<subseteq> A <+> B"
382     by auto
383   then have "finite (Inl ` A :: ('a + 'b) set)"
384     using fin by (rule finite_subset)
385   then show "finite A"
386     by (rule finite_imageD) (auto intro: inj_onI)
387 next
388   have "Inr ` B \<subseteq> A <+> B"
389     by auto
390   then have "finite (Inr ` B :: ('a + 'b) set)"
391     using fin by (rule finite_subset)
392   then show "finite B"
393     by (rule finite_imageD) (auto intro: inj_onI)
394 qed
396 lemma finite_Plus_iff [simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
397   by (auto intro: finite_PlusD finite_Plus)
399 lemma finite_Plus_UNIV_iff [simp]:
400   "finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
401   by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)
403 lemma finite_SigmaI [simp, intro]:
404   "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (SIGMA a:A. B a)"
405   unfolding Sigma_def by blast
407 lemma finite_SigmaI2:
408   assumes "finite {x\<in>A. B x \<noteq> {}}"
409   and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
410   shows "finite (Sigma A B)"
411 proof -
412   from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)"
413     by auto
414   also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B"
415     by auto
416   finally show ?thesis .
417 qed
419 lemma finite_cartesian_product: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
420   by (rule finite_SigmaI)
422 lemma finite_Prod_UNIV:
423   "finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)"
424   by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
426 lemma finite_cartesian_productD1:
427   assumes "finite (A \<times> B)" and "B \<noteq> {}"
428   shows "finite A"
429 proof -
430   from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
431     by (auto simp add: finite_conv_nat_seg_image)
432   then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}"
433     by simp
434   with \<open>B \<noteq> {}\<close> have "A = (fst \<circ> f) ` {i::nat. i < n}"
435     by (simp add: image_comp)
436   then have "\<exists>n f. A = f ` {i::nat. i < n}"
437     by blast
438   then show ?thesis
439     by (auto simp add: finite_conv_nat_seg_image)
440 qed
442 lemma finite_cartesian_productD2:
443   assumes "finite (A \<times> B)" and "A \<noteq> {}"
444   shows "finite B"
445 proof -
446   from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
447     by (auto simp add: finite_conv_nat_seg_image)
448   then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}"
449     by simp
450   with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}"
451     by (simp add: image_comp)
452   then have "\<exists>n f. B = f ` {i::nat. i < n}"
453     by blast
454   then show ?thesis
455     by (auto simp add: finite_conv_nat_seg_image)
456 qed
458 lemma finite_cartesian_product_iff:
459   "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
460   by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
462 lemma finite_prod:
463   "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
464   using finite_cartesian_product_iff[of UNIV UNIV] by simp
466 lemma finite_Pow_iff [iff]: "finite (Pow A) \<longleftrightarrow> finite A"
467 proof
468   assume "finite (Pow A)"
469   then have "finite ((\<lambda>x. {x}) ` A)"
470     by (blast intro: finite_subset)  (* somewhat slow *)
471   then show "finite A"
472     by (rule finite_imageD [unfolded inj_on_def]) simp
473 next
474   assume "finite A"
475   then show "finite (Pow A)"
476     by induct (simp_all add: Pow_insert)
477 qed
479 corollary finite_Collect_subsets [simp, intro]: "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
480   by (simp add: Pow_def [symmetric])
482 lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)"
483   by (simp only: finite_Pow_iff Pow_UNIV[symmetric])
485 lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A"
486   by (blast intro: finite_subset [OF subset_Pow_Union])
488 lemma finite_set_of_finite_funs:
489   assumes "finite A" "finite B"
490   shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
491 proof -
492   let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}"
493   have "?F ` ?S \<subseteq> Pow(A \<times> B)"
494     by auto
495   from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
496     by simp
497   have 2: "inj_on ?F ?S"
498     by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
499   show ?thesis
500     by (rule finite_imageD [OF 1 2])
501 qed
503 lemma not_finite_existsD:
504   assumes "\<not> finite {a. P a}"
505   shows "\<exists>a. P a"
506 proof (rule classical)
507   assume "\<not> ?thesis"
508   with assms show ?thesis by auto
509 qed
512 subsubsection \<open>Further induction rules on finite sets\<close>
514 lemma finite_ne_induct [case_names singleton insert, consumes 2]:
515   assumes "finite F" and "F \<noteq> {}"
516   assumes "\<And>x. P {x}"
517     and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F  \<Longrightarrow> P (insert x F)"
518   shows "P F"
519   using assms
520 proof induct
521   case empty
522   then show ?case by simp
523 next
524   case (insert x F)
525   then show ?case by cases auto
526 qed
528 lemma finite_subset_induct [consumes 2, case_names empty insert]:
529   assumes "finite F" and "F \<subseteq> A"
530     and empty: "P {}"
531     and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
532   shows "P F"
533   using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
534 proof induct
535   show "P {}" by fact
536 next
537   fix x F
538   assume "finite F" and "x \<notin> F" and P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
539   show "P (insert x F)"
540   proof (rule insert)
541     from i show "x \<in> A" by blast
542     from i have "F \<subseteq> A" by blast
543     with P show "P F" .
544     show "finite F" by fact
545     show "x \<notin> F" by fact
546   qed
547 qed
549 lemma finite_empty_induct:
550   assumes "finite A"
551     and "P A"
552     and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
553   shows "P {}"
554 proof -
555   have "P (A - B)" if "B \<subseteq> A" for B :: "'a set"
556   proof -
557     from \<open>finite A\<close> that have "finite B"
558       by (rule rev_finite_subset)
559     from this \<open>B \<subseteq> A\<close> show "P (A - B)"
560     proof induct
561       case empty
562       from \<open>P A\<close> show ?case by simp
563     next
564       case (insert b B)
565       have "P (A - B - {b})"
566       proof (rule remove)
567         from \<open>finite A\<close> show "finite (A - B)"
568           by induct auto
569         from insert show "b \<in> A - B"
570           by simp
571         from insert show "P (A - B)"
572           by simp
573       qed
574       also have "A - B - {b} = A - insert b B"
575         by (rule Diff_insert [symmetric])
576       finally show ?case .
577     qed
578   qed
579   then have "P (A - A)" by blast
580   then show ?thesis by simp
581 qed
583 lemma finite_update_induct [consumes 1, case_names const update]:
584   assumes finite: "finite {a. f a \<noteq> c}"
585     and const: "P (\<lambda>a. c)"
586     and 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))"
587   shows "P f"
588   using finite
589 proof (induct "{a. f a \<noteq> c}" arbitrary: f)
590   case empty
591   with const show ?case by simp
592 next
593   case (insert a A)
594   then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c"
595     by auto
596   with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}"
597     by simp
598   have "(f(a := c)) a = c"
599     by simp
600   from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))"
601     by simp
602   with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close>
603   have "P ((f(a := c))(a := f a))"
604     by (rule update)
605   then show ?case by simp
606 qed
608 lemma finite_subset_induct' [consumes 2, case_names empty insert]:
609   assumes "finite F" and "F \<subseteq> A"
610     and empty: "P {}"
611     and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
612   shows "P F"
613   using assms(1,2)
614 proof induct
615   show "P {}" by fact
616 next
617   fix x F
618   assume "finite F" and "x \<notin> F" and
619     P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
620   show "P (insert x F)"
621   proof (rule insert)
622     from i show "x \<in> A" by blast
623     from i have "F \<subseteq> A" by blast
624     with P show "P F" .
625     show "finite F" by fact
626     show "x \<notin> F" by fact
627     show "F \<subseteq> A" by fact
628   qed
629 qed
632 subsection \<open>Class \<open>finite\<close>\<close>
634 class finite =
635   assumes finite_UNIV: "finite (UNIV :: 'a set)"
636 begin
638 lemma finite [simp]: "finite (A :: 'a set)"
639   by (rule subset_UNIV finite_UNIV finite_subset)+
641 lemma finite_code [code]: "finite (A :: 'a set) \<longleftrightarrow> True"
642   by simp
644 end
646 instance prod :: (finite, finite) finite
647   by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
649 lemma inj_graph: "inj (\<lambda>f. {(x, y). y = f x})"
650   by (rule inj_onI) (auto simp add: set_eq_iff fun_eq_iff)
652 instance "fun" :: (finite, finite) finite
653 proof
654   show "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
655   proof (rule finite_imageD)
656     let ?graph = "\<lambda>f::'a \<Rightarrow> 'b. {(x, y). y = f x}"
657     have "range ?graph \<subseteq> Pow UNIV"
658       by simp
659     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
660       by (simp only: finite_Pow_iff finite)
661     ultimately show "finite (range ?graph)"
662       by (rule finite_subset)
663     show "inj ?graph"
664       by (rule inj_graph)
665   qed
666 qed
668 instance bool :: finite
669   by standard (simp add: UNIV_bool)
671 instance set :: (finite) finite
672   by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
674 instance unit :: finite
675   by standard (simp add: UNIV_unit)
677 instance sum :: (finite, finite) finite
678   by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
681 subsection \<open>A basic fold functional for finite sets\<close>
683 text \<open>The intended behaviour is
684   \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
685   if \<open>f\<close> is ``left-commutative'':
686 \<close>
688 locale comp_fun_commute =
689   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
690   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
691 begin
693 lemma fun_left_comm: "f y (f x z) = f x (f y z)"
694   using comp_fun_commute by (simp add: fun_eq_iff)
696 lemma commute_left_comp: "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
697   by (simp add: o_assoc comp_fun_commute)
699 end
701 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
702   for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b
703   where
704     emptyI [intro]: "fold_graph f z {} z"
705   | insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
707 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
709 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
710   where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"
712 text \<open>
713   A tempting alternative for the definiens is
714   @{term "if finite A then THE y. fold_graph f z A y else e"}.
715   It allows the removal of finiteness assumptions from the theorems
716   \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
717   The proofs become ugly. It is not worth the effort. (???)
718 \<close>
720 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
721   by (induct rule: finite_induct) auto
724 subsubsection \<open>From @{const fold_graph} to @{term fold}\<close>
726 context comp_fun_commute
727 begin
729 lemma fold_graph_finite:
730   assumes "fold_graph f z A y"
731   shows "finite A"
732   using assms by induct simp_all
734 lemma fold_graph_insertE_aux:
735   "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'"
736 proof (induct set: fold_graph)
737   case emptyI
738   then show ?case by simp
739 next
740   case (insertI x A y)
741   show ?case
742   proof (cases "x = a")
743     case True
744     with insertI show ?thesis by auto
745   next
746     case False
747     then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
748       using insertI by auto
749     have "f x y = f a (f x y')"
750       unfolding y by (rule fun_left_comm)
751     moreover have "fold_graph f z (insert x A - {a}) (f x y')"
752       using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close>
753       by (simp add: insert_Diff_if fold_graph.insertI)
754     ultimately show ?thesis
755       by fast
756   qed
757 qed
759 lemma fold_graph_insertE:
760   assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
761   obtains y where "v = f x y" and "fold_graph f z A y"
762   using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
764 lemma fold_graph_determ: "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
765 proof (induct arbitrary: y set: fold_graph)
766   case emptyI
767   then show ?case by fast
768 next
769   case (insertI x A y v)
770   from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
771   obtain y' where "v = f x y'" and "fold_graph f z A y'"
772     by (rule fold_graph_insertE)
773   from \<open>fold_graph f z A y'\<close> have "y' = y"
774     by (rule insertI)
775   with \<open>v = f x y'\<close> show "v = f x y"
776     by simp
777 qed
779 lemma fold_equality: "fold_graph f z A y \<Longrightarrow> fold f z A = y"
780   by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)
782 lemma fold_graph_fold:
783   assumes "finite A"
784   shows "fold_graph f z A (fold f z A)"
785 proof -
786   from assms have "\<exists>x. fold_graph f z A x"
787     by (rule finite_imp_fold_graph)
788   moreover note fold_graph_determ
789   ultimately have "\<exists>!x. fold_graph f z A x"
790     by (rule ex_ex1I)
791   then have "fold_graph f z A (The (fold_graph f z A))"
792     by (rule theI')
793   with assms show ?thesis
794     by (simp add: fold_def)
795 qed
797 text \<open>The base case for \<open>fold\<close>:\<close>
799 lemma (in -) fold_infinite [simp]: "\<not> finite A \<Longrightarrow> fold f z A = z"
800   by (auto simp: fold_def)
802 lemma (in -) fold_empty [simp]: "fold f z {} = z"
803   by (auto simp: fold_def)
805 text \<open>The various recursion equations for @{const fold}:\<close>
807 lemma fold_insert [simp]:
808   assumes "finite A" and "x \<notin> A"
809   shows "fold f z (insert x A) = f x (fold f z A)"
810 proof (rule fold_equality)
811   fix z
812   from \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
813     by (rule fold_graph_fold)
814   with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
815     by (rule fold_graph.insertI)
816   then show "fold_graph f z (insert x A) (f x (fold f z A))"
817     by simp
818 qed
820 declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
821   \<comment> \<open>No more proofs involve these.\<close>
823 lemma fold_fun_left_comm: "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
824 proof (induct rule: finite_induct)
825   case empty
826   then show ?case by simp
827 next
828   case insert
829   then show ?case
830     by (simp add: fun_left_comm [of x])
831 qed
833 lemma fold_insert2: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A)  = fold f (f x z) A"
834   by (simp add: fold_fun_left_comm)
836 lemma fold_rec:
837   assumes "finite A" and "x \<in> A"
838   shows "fold f z A = f x (fold f z (A - {x}))"
839 proof -
840   have A: "A = insert x (A - {x})"
841     using \<open>x \<in> A\<close> by blast
842   then have "fold f z A = fold f z (insert x (A - {x}))"
843     by simp
844   also have "\<dots> = f x (fold f z (A - {x}))"
845     by (rule fold_insert) (simp add: \<open>finite A\<close>)+
846   finally show ?thesis .
847 qed
849 lemma fold_insert_remove:
850   assumes "finite A"
851   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
852 proof -
853   from \<open>finite A\<close> have "finite (insert x A)"
854     by auto
855   moreover have "x \<in> insert x A"
856     by auto
857   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
858     by (rule fold_rec)
859   then show ?thesis
860     by simp
861 qed
863 lemma fold_set_union_disj:
864   assumes "finite A" "finite B" "A \<inter> B = {}"
865   shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
866   using assms(2,1,3) by induct simp_all
868 end
870 text \<open>Other properties of @{const fold}:\<close>
872 lemma fold_image:
873   assumes "inj_on g A"
874   shows "fold f z (g ` A) = fold (f \<circ> g) z A"
875 proof (cases "finite A")
876   case False
877   with assms show ?thesis
878     by (auto dest: finite_imageD simp add: fold_def)
879 next
880   case True
881   have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
882   proof
883     fix w
884     show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
885     proof
886       assume ?P
887       then show ?Q
888         using assms
889       proof (induct "g ` A" w arbitrary: A)
890         case emptyI
891         then show ?case by (auto intro: fold_graph.emptyI)
892       next
893         case (insertI x A r B)
894         from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
895           where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
896           by (rule inj_img_insertE)
897         from insertI.prems have "fold_graph (f \<circ> g) z A' r"
898           by (auto intro: insertI.hyps)
899         with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
900           by (rule fold_graph.insertI)
901         then show ?case
902           by simp
903       qed
904     next
905       assume ?Q
906       then show ?P
907         using assms
908       proof induct
909         case emptyI
910         then show ?case
911           by (auto intro: fold_graph.emptyI)
912       next
913         case (insertI x A r)
914         from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
915           by auto
916         moreover from insertI have "fold_graph f z (g ` A) r"
917           by simp
918         ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
919           by (rule fold_graph.insertI)
920         then show ?case
921           by simp
922       qed
923     qed
924   qed
925   with True assms show ?thesis
926     by (auto simp add: fold_def)
927 qed
929 lemma fold_cong:
930   assumes "comp_fun_commute f" "comp_fun_commute g"
931     and "finite A"
932     and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
933     and "s = t" and "A = B"
934   shows "fold f s A = fold g t B"
935 proof -
936   have "fold f s A = fold g s A"
937     using \<open>finite A\<close> cong
938   proof (induct A)
939     case empty
940     then show ?case by simp
941   next
942     case insert
943     interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
944     interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
945     from insert show ?case by simp
946   qed
947   with assms show ?thesis by simp
948 qed
951 text \<open>A simplified version for idempotent functions:\<close>
953 locale comp_fun_idem = comp_fun_commute +
954   assumes comp_fun_idem: "f x \<circ> f x = f x"
955 begin
957 lemma fun_left_idem: "f x (f x z) = f x z"
958   using comp_fun_idem by (simp add: fun_eq_iff)
960 lemma fold_insert_idem:
961   assumes fin: "finite A"
962   shows "fold f z (insert x A)  = f x (fold f z A)"
963 proof cases
964   assume "x \<in> A"
965   then obtain B where "A = insert x B" and "x \<notin> B"
966     by (rule set_insert)
967   then show ?thesis
968     using assms by (simp add: comp_fun_idem fun_left_idem)
969 next
970   assume "x \<notin> A"
971   then show ?thesis
972     using assms by simp
973 qed
975 declare fold_insert [simp del] fold_insert_idem [simp]
977 lemma fold_insert_idem2: "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
978   by (simp add: fold_fun_left_comm)
980 end
983 subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
985 lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \<circ> g)"
986   by standard (simp_all add: comp_fun_commute)
988 lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \<circ> g)"
989   by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
990     (simp_all add: comp_fun_idem)
992 lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
993 proof
994   show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" for x y
995   proof (cases "x = y")
996     case True
997     then show ?thesis by simp
998   next
999     case False
1000     show ?thesis
1001     proof (induct "g x" arbitrary: g)
1002       case 0
1003       then show ?case by simp
1004     next
1005       case (Suc n g)
1006       have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y"
1007       proof (induct "g y" arbitrary: g)
1008         case 0
1009         then show ?case by simp
1010       next
1011         case (Suc n g)
1012         define h where "h z = g z - 1" for z
1013         with Suc have "n = h y"
1014           by simp
1015         with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
1016           by auto
1017         from Suc h_def have "g y = Suc (h y)"
1018           by simp
1019         then show ?case
1020           by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute)
1021       qed
1022       define h where "h z = (if z = x then g x - 1 else g z)" for z
1023       with Suc have "n = h x"
1024         by simp
1025       with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
1026         by auto
1027       with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y"
1028         by simp
1029       from Suc h_def have "g x = Suc (h x)"
1030         by simp
1031       then show ?case
1032         by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1)
1033     qed
1034   qed
1035 qed
1038 subsubsection \<open>Expressing set operations via @{const fold}\<close>
1040 lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
1041   by standard rule
1043 lemma comp_fun_idem_insert: "comp_fun_idem insert"
1044   by standard auto
1046 lemma comp_fun_idem_remove: "comp_fun_idem Set.remove"
1047   by standard auto
1049 lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf"
1050   by standard (auto simp add: inf_left_commute)
1052 lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup"
1053   by standard (auto simp add: sup_left_commute)
1055 lemma union_fold_insert:
1056   assumes "finite A"
1057   shows "A \<union> B = fold insert B A"
1058 proof -
1059   interpret comp_fun_idem insert
1060     by (fact comp_fun_idem_insert)
1061   from \<open>finite A\<close> show ?thesis
1062     by (induct A arbitrary: B) simp_all
1063 qed
1065 lemma minus_fold_remove:
1066   assumes "finite A"
1067   shows "B - A = fold Set.remove B A"
1068 proof -
1069   interpret comp_fun_idem Set.remove
1070     by (fact comp_fun_idem_remove)
1071   from \<open>finite A\<close> have "fold Set.remove B A = B - A"
1072     by (induct A arbitrary: B) auto  (* slow *)
1073   then show ?thesis ..
1074 qed
1076 lemma comp_fun_commute_filter_fold:
1077   "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
1078 proof -
1079   interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
1080   show ?thesis by standard (auto simp: fun_eq_iff)
1081 qed
1083 lemma Set_filter_fold:
1084   assumes "finite A"
1085   shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
1086   using assms
1087   by induct
1088     (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
1090 lemma inter_Set_filter:
1091   assumes "finite B"
1092   shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B"
1093   using assms
1094   by induct (auto simp: Set.filter_def)
1096 lemma image_fold_insert:
1097   assumes "finite A"
1098   shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
1099 proof -
1100   interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A"
1101     by standard auto
1102   show ?thesis
1103     using assms by (induct A) auto
1104 qed
1106 lemma Ball_fold:
1107   assumes "finite A"
1108   shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
1109 proof -
1110   interpret comp_fun_commute "\<lambda>k s. s \<and> P k"
1111     by standard auto
1112   show ?thesis
1113     using assms by (induct A) auto
1114 qed
1116 lemma Bex_fold:
1117   assumes "finite A"
1118   shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
1119 proof -
1120   interpret comp_fun_commute "\<lambda>k s. s \<or> P k"
1121     by standard auto
1122   show ?thesis
1123     using assms by (induct A) auto
1124 qed
1126 lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
1127   by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast  (* somewhat slow *)
1129 lemma Pow_fold:
1130   assumes "finite A"
1131   shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A"
1132 proof -
1133   interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A"
1134     by (rule comp_fun_commute_Pow_fold)
1135   show ?thesis
1136     using assms by (induct A) (auto simp: Pow_insert)
1137 qed
1139 lemma fold_union_pair:
1140   assumes "finite B"
1141   shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
1142 proof -
1143   interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)"
1144     by standard auto
1145   show ?thesis
1146     using assms by (induct arbitrary: A) simp_all
1147 qed
1149 lemma comp_fun_commute_product_fold:
1150   "finite B \<Longrightarrow> comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
1151   by standard (auto simp: fold_union_pair [symmetric])
1153 lemma product_fold:
1154   assumes "finite A" "finite B"
1155   shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A"
1156   using assms unfolding Sigma_def
1157   by (induct A)
1158     (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
1160 context complete_lattice
1161 begin
1163 lemma inf_Inf_fold_inf:
1164   assumes "finite A"
1165   shows "inf (Inf A) B = fold inf B A"
1166 proof -
1167   interpret comp_fun_idem inf
1168     by (fact comp_fun_idem_inf)
1169   from \<open>finite A\<close> fold_fun_left_comm show ?thesis
1170     by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff)
1171 qed
1173 lemma sup_Sup_fold_sup:
1174   assumes "finite A"
1175   shows "sup (Sup A) B = fold sup B A"
1176 proof -
1177   interpret comp_fun_idem sup
1178     by (fact comp_fun_idem_sup)
1179   from \<open>finite A\<close> fold_fun_left_comm show ?thesis
1180     by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff)
1181 qed
1183 lemma Inf_fold_inf: "finite A \<Longrightarrow> Inf A = fold inf top A"
1184   using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
1186 lemma Sup_fold_sup: "finite A \<Longrightarrow> Sup A = fold sup bot A"
1187   using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
1189 lemma inf_INF_fold_inf:
1190   assumes "finite A"
1191   shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
1192 proof -
1193   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
1194   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
1195   from \<open>finite A\<close> have "?fold = ?inf"
1196     by (induct A arbitrary: B) (simp_all add: inf_left_commute)
1197   then show ?thesis ..
1198 qed
1200 lemma sup_SUP_fold_sup:
1201   assumes "finite A"
1202   shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
1203 proof -
1204   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
1205   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
1206   from \<open>finite A\<close> have "?fold = ?sup"
1207     by (induct A arbitrary: B) (simp_all add: sup_left_commute)
1208   then show ?thesis ..
1209 qed
1211 lemma INF_fold_inf: "finite A \<Longrightarrow> INFIMUM A f = fold (inf \<circ> f) top A"
1212   using inf_INF_fold_inf [of A top] by simp
1214 lemma SUP_fold_sup: "finite A \<Longrightarrow> SUPREMUM A f = fold (sup \<circ> f) bot A"
1215   using sup_SUP_fold_sup [of A bot] by simp
1217 end
1220 subsection \<open>Locales as mini-packages for fold operations\<close>
1222 subsubsection \<open>The natural case\<close>
1224 locale folding =
1225   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
1226   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
1227 begin
1229 interpretation fold?: comp_fun_commute f
1230   by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
1232 definition F :: "'a set \<Rightarrow> 'b"
1233   where eq_fold: "F A = fold f z A"
1235 lemma empty [simp]:"F {} = z"
1236   by (simp add: eq_fold)
1238 lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
1239   by (simp add: eq_fold)
1241 lemma insert [simp]:
1242   assumes "finite A" and "x \<notin> A"
1243   shows "F (insert x A) = f x (F A)"
1244 proof -
1245   from fold_insert assms
1246   have "fold f z (insert x A) = f x (fold f z A)" by simp
1247   with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
1248 qed
1250 lemma remove:
1251   assumes "finite A" and "x \<in> A"
1252   shows "F A = f x (F (A - {x}))"
1253 proof -
1254   from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
1255     by (auto dest: mk_disjoint_insert)
1256   moreover from \<open>finite A\<close> A have "finite B" by simp
1257   ultimately show ?thesis by simp
1258 qed
1260 lemma insert_remove: "finite A \<Longrightarrow> F (insert x A) = f x (F (A - {x}))"
1261   by (cases "x \<in> A") (simp_all add: remove insert_absorb)
1263 end
1266 subsubsection \<open>With idempotency\<close>
1268 locale folding_idem = folding +
1269   assumes comp_fun_idem: "f x \<circ> f x = f x"
1270 begin
1272 declare insert [simp del]
1274 interpretation fold?: comp_fun_idem f
1275   by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
1277 lemma insert_idem [simp]:
1278   assumes "finite A"
1279   shows "F (insert x A) = f x (F A)"
1280 proof -
1281   from fold_insert_idem assms
1282   have "fold f z (insert x A) = f x (fold f z A)" by simp
1283   with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
1284 qed
1286 end
1289 subsection \<open>Finite cardinality\<close>
1291 text \<open>
1292   The traditional definition
1293   @{prop "card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}"}
1294   is ugly to work with.
1295   But now that we have @{const fold} things are easy:
1296 \<close>
1298 global_interpretation card: folding "\<lambda>_. Suc" 0
1299   defines card = "folding.F (\<lambda>_. Suc) 0"
1300   by standard rule
1302 lemma card_infinite: "\<not> finite A \<Longrightarrow> card A = 0"
1303   by (fact card.infinite)
1305 lemma card_empty: "card {} = 0"
1306   by (fact card.empty)
1308 lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
1309   by (fact card.insert)
1311 lemma card_insert_if: "finite A \<Longrightarrow> card (insert x A) = (if x \<in> A then card A else Suc (card A))"
1312   by auto (simp add: card.insert_remove card.remove)
1314 lemma card_ge_0_finite: "card A > 0 \<Longrightarrow> finite A"
1315   by (rule ccontr) simp
1317 lemma card_0_eq [simp]: "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
1318   by (auto dest: mk_disjoint_insert)
1320 lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
1321   by (rule ccontr) simp
1323 lemma card_eq_0_iff: "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
1324   by auto
1326 lemma card_range_greater_zero: "finite (range f) \<Longrightarrow> card (range f) > 0"
1327   by (rule ccontr) (simp add: card_eq_0_iff)
1329 lemma card_gt_0_iff: "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
1330   by (simp add: neq0_conv [symmetric] card_eq_0_iff)
1332 lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
1333   apply (rule insert_Diff [THEN subst, where t = A])
1334    apply assumption
1335   apply (simp del: insert_Diff_single)
1336   done
1338 lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
1339   apply (cases "finite y")
1340    apply (cases "x \<in> y")
1341     apply (auto simp: insert_absorb)
1342   done
1344 lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
1345   by (simp add: card_Suc_Diff1 [symmetric])
1347 lemma card_Diff_singleton_if:
1348   "finite A \<Longrightarrow> card (A - {x}) = (if x \<in> A then card A - 1 else card A)"
1349   by (simp add: card_Diff_singleton)
1351 lemma card_Diff_insert[simp]:
1352   assumes "finite A" and "a \<in> A" and "a \<notin> B"
1353   shows "card (A - insert a B) = card (A - B) - 1"
1354 proof -
1355   have "A - insert a B = (A - B) - {a}"
1356     using assms by blast
1357   then show ?thesis
1358     using assms by (simp add: card_Diff_singleton)
1359 qed
1361 lemma card_insert: "finite A \<Longrightarrow> card (insert x A) = Suc (card (A - {x}))"
1362   by (fact card.insert_remove)
1364 lemma card_insert_le: "finite A \<Longrightarrow> card A \<le> card (insert x A)"
1365   by (simp add: card_insert_if)
1367 lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n"
1368   by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
1370 lemma card_Collect_le_nat[simp]: "card {i::nat. i \<le> n} = Suc n"
1371   using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le)
1373 lemma card_mono:
1374   assumes "finite B" and "A \<subseteq> B"
1375   shows "card A \<le> card B"
1376 proof -
1377   from assms have "finite A"
1378     by (auto intro: finite_subset)
1379   then show ?thesis
1380     using assms
1381   proof (induct A arbitrary: B)
1382     case empty
1383     then show ?case by simp
1384   next
1385     case (insert x A)
1386     then have "x \<in> B"
1387       by simp
1388     from insert have "A \<subseteq> B - {x}" and "finite (B - {x})"
1389       by auto
1390     with insert.hyps have "card A \<le> card (B - {x})"
1391       by auto
1392     with \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case
1393       by simp (simp only: card.remove)
1394   qed
1395 qed
1397 lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
1398   apply (induct rule: finite_induct)
1399    apply simp
1400   apply clarify
1401   apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
1402    prefer 2 apply (blast intro: finite_subset, atomize)
1403   apply (drule_tac x = "A - {x}" in spec)
1404   apply (simp add: card_Diff_singleton_if split: if_split_asm)
1405   apply (case_tac "card A", auto)
1406   done
1408 lemma psubset_card_mono: "finite B \<Longrightarrow> A < B \<Longrightarrow> card A < card B"
1409   apply (simp add: psubset_eq linorder_not_le [symmetric])
1410   apply (blast dest: card_seteq)
1411   done
1413 lemma card_Un_Int:
1414   assumes "finite A" "finite B"
1415   shows "card A + card B = card (A \<union> B) + card (A \<inter> B)"
1416   using assms
1417 proof (induct A)
1418   case empty
1419   then show ?case by simp
1420 next
1421   case insert
1422   then show ?case
1423     by (auto simp add: insert_absorb Int_insert_left)
1424 qed
1426 lemma card_Un_disjoint: "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> card (A \<union> B) = card A + card B"
1427   using card_Un_Int [of A B] by simp
1429 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
1430   apply (cases "finite A")
1431    apply (cases "finite B")
1432     apply (use le_iff_add card_Un_Int in blast)
1433    apply simp
1434   apply simp
1435   done
1437 lemma card_Diff_subset:
1438   assumes "finite B"
1439     and "B \<subseteq> A"
1440   shows "card (A - B) = card A - card B"
1441   using assms
1442 proof (cases "finite A")
1443   case False
1444   with assms show ?thesis
1445     by simp
1446 next
1447   case True
1448   with assms show ?thesis
1449     by (induct B arbitrary: A) simp_all
1450 qed
1452 lemma card_Diff_subset_Int:
1453   assumes "finite (A \<inter> B)"
1454   shows "card (A - B) = card A - card (A \<inter> B)"
1455 proof -
1456   have "A - B = A - A \<inter> B" by auto
1457   with assms show ?thesis
1458     by (simp add: card_Diff_subset)
1459 qed
1461 lemma diff_card_le_card_Diff:
1462   assumes "finite B"
1463   shows "card A - card B \<le> card (A - B)"
1464 proof -
1465   have "card A - card B \<le> card A - card (A \<inter> B)"
1466     using card_mono[OF assms Int_lower2, of A] by arith
1467   also have "\<dots> = card (A - B)"
1468     using assms by (simp add: card_Diff_subset_Int)
1469   finally show ?thesis .
1470 qed
1472 lemma card_Diff1_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) < card A"
1473   by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert)
1475 lemma card_Diff2_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> card (A - {x} - {y}) < card A"
1476   apply (cases "x = y")
1477    apply (simp add: card_Diff1_less del:card_Diff_insert)
1478   apply (rule less_trans)
1479    prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert)
1480   done
1482 lemma card_Diff1_le: "finite A \<Longrightarrow> card (A - {x}) \<le> card A"
1483   by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
1485 lemma card_psubset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> card A < card B \<Longrightarrow> A < B"
1486   by (erule psubsetI) blast
1488 lemma card_le_inj:
1489   assumes fA: "finite A"
1490     and fB: "finite B"
1491     and c: "card A \<le> card B"
1492   shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
1493   using fA fB c
1494 proof (induct arbitrary: B rule: finite_induct)
1495   case empty
1496   then show ?case by simp
1497 next
1498   case (insert x s t)
1499   then show ?case
1500   proof (induct rule: finite_induct [OF insert.prems(1)])
1501     case 1
1502     then show ?case by simp
1503   next
1504     case (2 y t)
1505     from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
1506       by simp
1507     from "2.prems"(3) [OF "2.hyps"(1) cst]
1508     obtain f where "f ` s \<subseteq> t" "inj_on f s"
1509       by blast
1510     with "2.prems"(2) "2.hyps"(2) show ?case
1511       apply -
1512       apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
1513       apply (auto simp add: inj_on_def)
1514       done
1515   qed
1516 qed
1518 lemma card_subset_eq:
1519   assumes fB: "finite B"
1520     and AB: "A \<subseteq> B"
1521     and c: "card A = card B"
1522   shows "A = B"
1523 proof -
1524   from fB AB have fA: "finite A"
1525     by (auto intro: finite_subset)
1526   from fA fB have fBA: "finite (B - A)"
1527     by auto
1528   have e: "A \<inter> (B - A) = {}"
1529     by blast
1530   have eq: "A \<union> (B - A) = B"
1531     using AB by blast
1532   from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
1533     by arith
1534   then have "B - A = {}"
1535     unfolding card_eq_0_iff using fA fB by simp
1536   with AB show "A = B"
1537     by blast
1538 qed
1540 lemma insert_partition:
1541   "x \<notin> F \<Longrightarrow> \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> x \<inter> \<Union>F = {}"
1542   by auto  (* somewhat slow *)
1544 lemma finite_psubset_induct [consumes 1, case_names psubset]:
1545   assumes finite: "finite A"
1546     and major: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A"
1547   shows "P A"
1548   using finite
1549 proof (induct A taking: card rule: measure_induct_rule)
1550   case (less A)
1551   have fin: "finite A" by fact
1552   have ih: "card B < card A \<Longrightarrow> finite B \<Longrightarrow> P B" for B by fact
1553   have "P B" if "B \<subset> A" for B
1554   proof -
1555     from that have "card B < card A"
1556       using psubset_card_mono fin by blast
1557     moreover
1558     from that have "B \<subseteq> A"
1559       by auto
1560     then have "finite B"
1561       using fin finite_subset by blast
1562     ultimately show ?thesis using ih by simp
1563   qed
1564   with fin show "P A" using major by blast
1565 qed
1567 lemma finite_induct_select [consumes 1, case_names empty select]:
1568   assumes "finite S"
1569     and "P {}"
1570     and select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
1571   shows "P S"
1572 proof -
1573   have "0 \<le> card S" by simp
1574   then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
1575   proof (induct rule: dec_induct)
1576     case base with \<open>P {}\<close>
1577     show ?case
1578       by (intro exI[of _ "{}"]) auto
1579   next
1580     case (step n)
1581     then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
1582       by auto
1583     with \<open>n < card S\<close> have "T \<subset> S" "P T"
1584       by auto
1585     with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
1586       by auto
1587     with step(2) T \<open>finite S\<close> show ?case
1588       by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
1589   qed
1590   with \<open>finite S\<close> show "P S"
1591     by (auto dest: card_subset_eq)
1592 qed
1594 lemma remove_induct [case_names empty infinite remove]:
1595   assumes empty: "P ({} :: 'a set)"
1596     and infinite: "\<not> finite B \<Longrightarrow> P B"
1597     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"
1598   shows "P B"
1599 proof (cases "finite B")
1600   case False
1601   then show ?thesis by (rule infinite)
1602 next
1603   case True
1604   define A where "A = B"
1605   with True have "finite A" "A \<subseteq> B"
1606     by simp_all
1607   then show "P A"
1608   proof (induct "card A" arbitrary: A)
1609     case 0
1610     then have "A = {}" by auto
1611     with empty show ?case by simp
1612   next
1613     case (Suc n A)
1614     from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A"
1615       by (rule finite_subset)
1616     moreover from Suc.hyps have "A \<noteq> {}" by auto
1617     moreover note \<open>A \<subseteq> B\<close>
1618     moreover have "P (A - {x})" if x: "x \<in> A" for x
1619       using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
1620     ultimately show ?case by (rule remove)
1621   qed
1622 qed
1624 lemma finite_remove_induct [consumes 1, case_names empty remove]:
1625   fixes P :: "'a set \<Rightarrow> bool"
1626   assumes "finite B"
1627     and "P {}"
1628     and "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
1629   defines "B' \<equiv> B"
1630   shows "P B'"
1631   by (induct B' rule: remove_induct) (simp_all add: assms)
1634 text \<open>Main cardinality theorem.\<close>
1635 lemma card_partition [rule_format]:
1636   "finite C \<Longrightarrow> finite (\<Union>C) \<Longrightarrow> (\<forall>c\<in>C. card c = k) \<Longrightarrow>
1637     (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow>
1638     k * card C = card (\<Union>C)"
1639 proof (induct rule: finite_induct)
1640   case empty
1641   then show ?case by simp
1642 next
1643   case (insert x F)
1644   then show ?case
1645     by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert _ _)"])
1646 qed
1648 lemma card_eq_UNIV_imp_eq_UNIV:
1649   assumes fin: "finite (UNIV :: 'a set)"
1650     and card: "card A = card (UNIV :: 'a set)"
1651   shows "A = (UNIV :: 'a set)"
1652 proof
1653   show "A \<subseteq> UNIV" by simp
1654   show "UNIV \<subseteq> A"
1655   proof
1656     show "x \<in> A" for x
1657     proof (rule ccontr)
1658       assume "x \<notin> A"
1659       then have "A \<subset> UNIV" by auto
1660       with fin have "card A < card (UNIV :: 'a set)"
1661         by (fact psubset_card_mono)
1662       with card show False by simp
1663     qed
1664   qed
1665 qed
1667 text \<open>The form of a finite set of given cardinality\<close>
1669 lemma card_eq_SucD:
1670   assumes "card A = Suc k"
1671   shows "\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {})"
1672 proof -
1673   have fin: "finite A"
1674     using assms by (auto intro: ccontr)
1675   moreover have "card A \<noteq> 0"
1676     using assms by auto
1677   ultimately obtain b where b: "b \<in> A"
1678     by auto
1679   show ?thesis
1680   proof (intro exI conjI)
1681     show "A = insert b (A - {b})"
1682       using b by blast
1683     show "b \<notin> A - {b}"
1684       by blast
1685     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
1686       using assms b fin by (fastforce dest: mk_disjoint_insert)+
1687   qed
1688 qed
1690 lemma card_Suc_eq:
1691   "card A = Suc k \<longleftrightarrow>
1692     (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
1693   apply (auto elim!: card_eq_SucD)
1694   apply (subst card.insert)
1695     apply (auto simp add: intro:ccontr)
1696   done
1698 lemma card_1_singletonE:
1699   assumes "card A = 1"
1700   obtains x where "A = {x}"
1701   using assms by (auto simp: card_Suc_eq)
1703 lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
1704   unfolding is_singleton_def
1705   by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
1707 lemma card_le_Suc_iff:
1708   "finite A \<Longrightarrow> Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
1709   by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
1710     dest: subset_singletonD split: nat.splits if_splits)
1712 lemma finite_fun_UNIVD2:
1713   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1714   shows "finite (UNIV :: 'b set)"
1715 proof -
1716   from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" for arbitrary
1717     by (rule finite_imageI)
1718   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)" for arbitrary
1719     by (rule UNIV_eq_I) auto
1720   ultimately show "finite (UNIV :: 'b set)"
1721     by simp
1722 qed
1724 lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
1725   unfolding UNIV_unit by simp
1727 lemma infinite_arbitrarily_large:
1728   assumes "\<not> finite A"
1729   shows "\<exists>B. finite B \<and> card B = n \<and> B \<subseteq> A"
1730 proof (induction n)
1731   case 0
1732   show ?case by (intro exI[of _ "{}"]) auto
1733 next
1734   case (Suc n)
1735   then obtain B where B: "finite B \<and> card B = n \<and> B \<subseteq> A" ..
1736   with \<open>\<not> finite A\<close> have "A \<noteq> B" by auto
1737   with B have "B \<subset> A" by auto
1738   then have "\<exists>x. x \<in> A - B"
1739     by (elim psubset_imp_ex_mem)
1740   then obtain x where x: "x \<in> A - B" ..
1741   with B have "finite (insert x B) \<and> card (insert x B) = Suc n \<and> insert x B \<subseteq> A"
1742     by auto
1743   then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
1744 qed
1747 subsubsection \<open>Cardinality of image\<close>
1749 lemma card_image_le: "finite A \<Longrightarrow> card (f ` A) \<le> card A"
1750   by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
1752 lemma card_image: "inj_on f A \<Longrightarrow> card (f ` A) = card A"
1753 proof (induct A rule: infinite_finite_induct)
1754   case (infinite A)
1755   then have "\<not> finite (f ` A)" by (auto dest: finite_imageD)
1756   with infinite show ?case by simp
1757 qed simp_all
1759 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
1760   by (auto simp: card_image bij_betw_def)
1762 lemma endo_inj_surj: "finite A \<Longrightarrow> f ` A \<subseteq> A \<Longrightarrow> inj_on f A \<Longrightarrow> f ` A = A"
1763   by (simp add: card_seteq card_image)
1765 lemma eq_card_imp_inj_on:
1766   assumes "finite A" "card(f ` A) = card A"
1767   shows "inj_on f A"
1768   using assms
1769 proof (induct rule:finite_induct)
1770   case empty
1771   show ?case by simp
1772 next
1773   case (insert x A)
1774   then show ?case
1775     using card_image_le [of A f] by (simp add: card_insert_if split: if_splits)
1776 qed
1778 lemma inj_on_iff_eq_card: "finite A \<Longrightarrow> inj_on f A \<longleftrightarrow> card (f ` A) = card A"
1779   by (blast intro: card_image eq_card_imp_inj_on)
1781 lemma card_inj_on_le:
1782   assumes "inj_on f A" "f ` A \<subseteq> B" "finite B"
1783   shows "card A \<le> card B"
1784 proof -
1785   have "finite A"
1786     using assms by (blast intro: finite_imageD dest: finite_subset)
1787   then show ?thesis
1788     using assms by (force intro: card_mono simp: card_image [symmetric])
1789 qed
1791 lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
1792   by (blast intro: card_image_le card_mono le_trans)
1794 lemma card_bij_eq:
1795   "inj_on f A \<Longrightarrow> f ` A \<subseteq> B \<Longrightarrow> inj_on g B \<Longrightarrow> g ` B \<subseteq> A \<Longrightarrow> finite A \<Longrightarrow> finite B
1796     \<Longrightarrow> card A = card B"
1797   by (auto intro: le_antisym card_inj_on_le)
1799 lemma bij_betw_finite: "bij_betw f A B \<Longrightarrow> finite A \<longleftrightarrow> finite B"
1800   unfolding bij_betw_def using finite_imageD [of f A] by auto
1802 lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
1803   using finite_imageD finite_subset by blast
1805 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A"
1806   by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
1807       intro: card_image[symmetric, OF subset_inj_on])
1810 subsubsection \<open>Pigeonhole Principles\<close>
1812 lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A "
1813   by (auto dest: card_image less_irrefl_nat)
1815 lemma pigeonhole_infinite:
1816   assumes "\<not> finite A" and "finite (f`A)"
1817   shows "\<exists>a0\<in>A. \<not> finite {a\<in>A. f a = f a0}"
1818   using assms(2,1)
1819 proof (induct "f`A" arbitrary: A rule: finite_induct)
1820   case empty
1821   then show ?case by simp
1822 next
1823   case (insert b F)
1824   show ?case
1825   proof (cases "finite {a\<in>A. f a = b}")
1826     case True
1827     with \<open>\<not> finite A\<close> have "\<not> finite (A - {a\<in>A. f a = b})"
1828       by simp
1829     also have "A - {a\<in>A. f a = b} = {a\<in>A. f a \<noteq> b}"
1830       by blast
1831     finally have "\<not> finite {a\<in>A. f a \<noteq> b}" .
1832     from insert(3)[OF _ this] insert(2,4) show ?thesis
1833       by simp (blast intro: rev_finite_subset)
1834   next
1835     case False
1836     then have "{a \<in> A. f a = b} \<noteq> {}" by force
1837     with False show ?thesis by blast
1838   qed
1839 qed
1841 lemma pigeonhole_infinite_rel:
1842   assumes "\<not> finite A"
1843     and "finite B"
1844     and "\<forall>a\<in>A. \<exists>b\<in>B. R a b"
1845   shows "\<exists>b\<in>B. \<not> finite {a:A. R a b}"
1846 proof -
1847   let ?F = "\<lambda>a. {b\<in>B. R a b}"
1848   from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>] have "finite (?F ` A)"
1849     by (blast intro: rev_finite_subset)
1850   from pigeonhole_infinite [where f = ?F, OF assms(1) this]
1851   obtain a0 where "a0 \<in> A" and infinite: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
1852   obtain b0 where "b0 \<in> B" and "R a0 b0"
1853     using \<open>a0 \<in> A\<close> assms(3) by blast
1854   have "finite {a\<in>A. ?F a = ?F a0}" if "finite {a\<in>A. R a b0}"
1855     using \<open>b0 \<in> B\<close> \<open>R a0 b0\<close> that by (blast intro: rev_finite_subset)
1856   with infinite \<open>b0 \<in> B\<close> show ?thesis
1857     by blast
1858 qed
1861 subsubsection \<open>Cardinality of sums\<close>
1863 lemma card_Plus:
1864   assumes "finite A" "finite B"
1865   shows "card (A <+> B) = card A + card B"
1866 proof -
1867   have "Inl`A \<inter> Inr`B = {}" by fast
1868   with assms show ?thesis
1869     by (simp add: Plus_def card_Un_disjoint card_image)
1870 qed
1872 lemma card_Plus_conv_if:
1873   "card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)"
1874   by (auto simp add: card_Plus)
1876 text \<open>Relates to equivalence classes.  Based on a theorem of F. Kammüller.\<close>
1878 lemma dvd_partition:
1879   assumes f: "finite (\<Union>C)"
1880     and "\<forall>c\<in>C. k dvd card c" "\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}"
1881   shows "k dvd card (\<Union>C)"
1882 proof -
1883   have "finite C"
1884     by (rule finite_UnionD [OF f])
1885   then show ?thesis
1886     using assms
1887   proof (induct rule: finite_induct)
1888     case empty
1889     show ?case by simp
1890   next
1891     case insert
1892     then show ?case
1893       apply simp
1894       apply (subst card_Un_disjoint)
1895          apply (auto simp add: disjoint_eq_subset_Compl)
1896       done
1897   qed
1898 qed
1901 subsubsection \<open>Relating injectivity and surjectivity\<close>
1903 lemma finite_surj_inj:
1904   assumes "finite A" "A \<subseteq> f ` A"
1905   shows "inj_on f A"
1906 proof -
1907   have "f ` A = A"
1908     by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le)
1909   then show ?thesis using assms
1910     by (simp add: eq_card_imp_inj_on)
1911 qed
1913 lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
1914   for f :: "'a \<Rightarrow> 'a"
1915   by (blast intro: finite_surj_inj subset_UNIV)
1917 lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
1918   for f :: "'a \<Rightarrow> 'a"
1919   by (fastforce simp:surj_def dest!: endo_inj_surj)
1921 corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
1922 proof
1923   assume "finite (UNIV :: nat set)"
1924   with finite_UNIV_inj_surj [of Suc] show False
1925     by simp (blast dest: Suc_neq_Zero surjD)
1926 qed
1928 lemma infinite_UNIV_char_0: "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
1929 proof
1930   assume "finite (UNIV :: 'a set)"
1931   with subset_UNIV have "finite (range of_nat :: 'a set)"
1932     by (rule finite_subset)
1933   moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
1934     by (simp add: inj_on_def)
1935   ultimately have "finite (UNIV :: nat set)"
1936     by (rule finite_imageD)
1937   then show False
1938     by simp
1939 qed
1941 hide_const (open) Finite_Set.fold
1944 subsection \<open>Infinite Sets\<close>
1946 text \<open>
1947   Some elementary facts about infinite sets, mostly by Stephan Merz.
1948   Beware! Because "infinite" merely abbreviates a negation, these
1949   lemmas may not work well with \<open>blast\<close>.
1950 \<close>
1952 abbreviation infinite :: "'a set \<Rightarrow> bool"
1953   where "infinite S \<equiv> \<not> finite S"
1955 text \<open>
1956   Infinite sets are non-empty, and if we remove some elements from an
1957   infinite set, the result is still infinite.
1958 \<close>
1960 lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
1961   by auto
1963 lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
1964   by simp
1966 lemma Diff_infinite_finite:
1967   assumes "finite T" "infinite S"
1968   shows "infinite (S - T)"
1969   using \<open>finite T\<close>
1970 proof induct
1971   from \<open>infinite S\<close> show "infinite (S - {})"
1972     by auto
1973 next
1974   fix T x
1975   assume ih: "infinite (S - T)"
1976   have "S - (insert x T) = (S - T) - {x}"
1977     by (rule Diff_insert)
1978   with ih show "infinite (S - (insert x T))"
1979     by (simp add: infinite_remove)
1980 qed
1982 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
1983   by simp
1985 lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
1986   by simp
1988 lemma infinite_super:
1989   assumes "S \<subseteq> T"
1990     and "infinite S"
1991   shows "infinite T"
1992 proof
1993   assume "finite T"
1994   with \<open>S \<subseteq> T\<close> have "finite S" by (simp add: finite_subset)
1995   with \<open>infinite S\<close> show False by simp
1996 qed
1998 proposition infinite_coinduct [consumes 1, case_names infinite]:
1999   assumes "X A"
2000     and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
2001   shows "infinite A"
2002 proof
2003   assume "finite A"
2004   then show False
2005     using \<open>X A\<close>
2006   proof (induction rule: finite_psubset_induct)
2007     case (psubset A)
2008     then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})"
2009       using local.step psubset.prems by blast
2010     then have "X (A - {x})"
2011       using psubset.hyps by blast
2012     show False
2013       apply (rule psubset.IH [where B = "A - {x}"])
2014        apply (use \<open>x \<in> A\<close> in blast)
2015       apply (simp add: \<open>X (A - {x})\<close>)
2016       done
2017   qed
2018 qed
2020 text \<open>
2021   For any function with infinite domain and finite range there is some
2022   element that is the image of infinitely many domain elements.  In
2023   particular, any infinite sequence of elements from a finite set
2024   contains some element that occurs infinitely often.
2025 \<close>
2027 lemma inf_img_fin_dom':
2028   assumes img: "finite (f ` A)"
2029     and dom: "infinite A"
2030   shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
2031 proof (rule ccontr)
2032   have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
2033   moreover assume "\<not> ?thesis"
2034   with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
2035   ultimately have "finite A" by (rule finite_subset)
2036   with dom show False by contradiction
2037 qed
2039 lemma inf_img_fin_domE':
2040   assumes "finite (f ` A)" and "infinite A"
2041   obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
2042   using assms by (blast dest: inf_img_fin_dom')
2044 lemma inf_img_fin_dom:
2045   assumes img: "finite (f`A)" and dom: "infinite A"
2046   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
2047   using inf_img_fin_dom'[OF assms] by auto
2049 lemma inf_img_fin_domE:
2050   assumes "finite (f`A)" and "infinite A"
2051   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
2052   using assms by (blast dest: inf_img_fin_dom)
2054 proposition finite_image_absD: "finite (abs ` S) \<Longrightarrow> finite S"
2055   for S :: "'a::linordered_ring set"
2056   by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
2058 end