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*) 8 9section \<open>Finite sets\<close> 10 11theory Finite_Set 12 imports Product_Type Sum_Type Fields 13begin 14 15subsection \<open>Predicate for finite sets\<close> 16 17context notes [[inductive_internals]] 18begin 19 20inductive finite :: "'a set \<Rightarrow> bool" 21 where 22 emptyI [simp, intro!]: "finite {}" 23 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" 24 25end 26 27simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close> 28 29declare [[simproc del: finite_Collect]] 30 31lemma 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> 38proof induct 39 show "P {}" by fact 40next 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 52qed 53 54lemma 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" 59proof (cases "finite A") 60 case False 61 with infinite show ?thesis . 62next 63 case True 64 then show ?thesis by (induct A) (fact empty insert)+ 65qed 66 67 68subsubsection \<open>Choice principles\<close> 69 70lemma ex_new_if_finite: \<comment> \<open>does not depend on def of finite at all\<close> 71 assumes "\<not> finite (UNIV :: 'a set)" and "finite A" 72 shows "\<exists>a::'a. a \<notin> A" 73proof - 74 from assms have "A \<noteq> UNIV" by blast 75 then show ?thesis by blast 76qed 77 78text \<open>A finite choice principle. Does not need the SOME choice operator.\<close> 79 80lemma 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)" 81proof (induct rule: finite_induct) 82 case empty 83 then show ?case by simp 84next 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 93qed 94 95 96subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close> 97 98lemma 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 102proof 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 109next 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 117qed 118 119lemma nat_seg_image_imp_finite: "A = f ` {i::nat. i < n} \<Longrightarrow> finite A" 120proof (induct n arbitrary: A) 121 case 0 122 then show ?case by simp 123next 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 140qed 141 142lemma 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) 144 145lemma 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" 148proof - 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 156qed 157 158lemma finite_Collect_less_nat [iff]: "finite {n::nat. n < k}" 159 by (fastforce simp: finite_conv_nat_seg_image) 160 161lemma finite_Collect_le_nat [iff]: "finite {n::nat. n \<le> k}" 162 by (simp add: le_eq_less_or_eq Collect_disj_eq) 163 164 165subsection \<open>Finiteness and common set operations\<close> 166 167lemma rev_finite_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A" 168proof (induct arbitrary: A rule: finite_induct) 169 case empty 170 then show ?case by simp 171next 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 191qed 192 193lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A" 194 by (rule rev_finite_subset) 195 196lemma finite_UnI: 197 assumes "finite F" and "finite G" 198 shows "finite (F \<union> G)" 199 using assms by induct simp_all 200 201lemma 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"]) 203 204lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A" 205proof - 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 209qed 210 211lemma finite_Int [simp, intro]: "finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)" 212 by (blast intro: finite_subset) 213 214lemma 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) 217 218lemma 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) 221 222lemma finite_Diff [simp, intro]: "finite A \<Longrightarrow> finite (A - B)" 223 by (rule finite_subset, rule Diff_subset) 224 225lemma finite_Diff2 [simp]: 226 assumes "finite B" 227 shows "finite (A - B) \<longleftrightarrow> finite A" 228proof - 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 .. 234qed 235 236lemma finite_Diff_insert [iff]: "finite (A - insert a B) \<longleftrightarrow> finite (A - B)" 237proof - 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 241qed 242 243lemma finite_compl [simp]: 244 "finite (A :: 'a set) \<Longrightarrow> finite (- A) \<longleftrightarrow> finite (UNIV :: 'a set)" 245 by (simp add: Compl_eq_Diff_UNIV) 246 247lemma 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) 250 251lemma 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 254 255lemma 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 258 259lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (\<Union>(B ` A)) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))" 260 by (blast intro: finite_subset) 261 262lemma finite_Inter [intro]: "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)" 263 by (blast intro: Inter_lower finite_subset) 264 265lemma 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) 267 268lemma finite_imageI [simp, intro]: "finite F \<Longrightarrow> finite (h ` F)" 269 by (induct rule: finite_induct) simp_all 270 271lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow> finite {f x |x. P x}" 272 by (simp add: image_Collect [symmetric]) 273 274lemma 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 277 278lemma finite_imageD: 279 assumes "finite (f ` A)" and "inj_on f A" 280 shows "finite A" 281 using assms 282proof (induct "f ` A" arbitrary: A) 283 case empty 284 then show ?case by simp 285next 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) 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 301qed 302 303lemma finite_image_iff: "inj_on f A \<Longrightarrow> finite (f ` A) \<longleftrightarrow> finite A" 304 using finite_imageD by blast 305 306lemma finite_surj: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B" 307 by (erule finite_subset) (rule finite_imageI) 308 309lemma finite_range_imageI: "finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))" 310 by (drule finite_imageI) (simp add: range_composition) 311 312lemma 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 316proof induct 317 case empty 318 then show ?case by simp 319next 320 case insert 321 then show ?case 322 by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast 323qed 324 325lemma all_subset_image: "(\<forall>B. B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. B \<subseteq> A \<longrightarrow> P(f ` B))" 326 by (safe elim!: subset_imageE) (use image_mono in \<open>blast+\<close>) (* slow *) 327 328lemma all_finite_subset_image: 329 "(\<forall>B. finite B \<and> B \<subseteq> f ` A \<longrightarrow> P B) \<longleftrightarrow> (\<forall>B. finite B \<and> B \<subseteq> A \<longrightarrow> P (f ` B))" 330proof safe 331 fix B :: "'a set" 332 assume B: "finite B" "B \<subseteq> f ` A" and P: "\<forall>B. finite B \<and> B \<subseteq> A \<longrightarrow> P (f ` B)" 333 show "P B" 334 using finite_subset_image [OF B] P by blast 335qed blast 336 337lemma ex_finite_subset_image: 338 "(\<exists>B. finite B \<and> B \<subseteq> f ` A \<and> P B) \<longleftrightarrow> (\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B))" 339proof safe 340 fix B :: "'a set" 341 assume B: "finite B" "B \<subseteq> f ` A" and "P B" 342 show "\<exists>B. finite B \<and> B \<subseteq> A \<and> P (f ` B)" 343 using finite_subset_image [OF B] \<open>P B\<close> by blast 344qed blast 345 346lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)" 347proof (induct rule: finite_induct) 348 case (insert x F) 349 then show ?case 350 by (simp add: vimage_insert [of h x F] finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2) 351qed simp 352 353lemma finite_finite_vimage_IntI: 354 assumes "finite F" 355 and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)" 356 shows "finite (h -` F \<inter> A)" 357proof - 358 have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)" 359 by blast 360 show ?thesis 361 by (simp only: * assms finite_UN_I) 362qed 363 364lemma finite_vimageI: "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)" 365 using finite_vimage_IntI[of F h UNIV] by auto 366 367lemma finite_vimageD': "finite (f -` A) \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> finite A" 368 by (auto simp add: subset_image_iff intro: finite_subset[rotated]) 369 370lemma finite_vimageD: "finite (h -` F) \<Longrightarrow> surj h \<Longrightarrow> finite F" 371 by (auto dest: finite_vimageD') 372 373lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F" 374 unfolding bij_def by (auto elim: finite_vimageD finite_vimageI) 375 376lemma finite_Collect_bex [simp]: 377 assumes "finite A" 378 shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})" 379proof - 380 have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto 381 with assms show ?thesis by simp 382qed 383 384lemma finite_Collect_bounded_ex [simp]: 385 assumes "finite {y. P y}" 386 shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})" 387proof - 388 have "{x. \<exists>y. P y \<and> Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})" 389 by auto 390 with assms show ?thesis 391 by simp 392qed 393 394lemma finite_Plus: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)" 395 by (simp add: Plus_def) 396 397lemma finite_PlusD: 398 fixes A :: "'a set" and B :: "'b set" 399 assumes fin: "finite (A <+> B)" 400 shows "finite A" "finite B" 401proof - 402 have "Inl ` A \<subseteq> A <+> B" 403 by auto 404 then have "finite (Inl ` A :: ('a + 'b) set)" 405 using fin by (rule finite_subset) 406 then show "finite A" 407 by (rule finite_imageD) (auto intro: inj_onI) 408next 409 have "Inr ` B \<subseteq> A <+> B" 410 by auto 411 then have "finite (Inr ` B :: ('a + 'b) set)" 412 using fin by (rule finite_subset) 413 then show "finite B" 414 by (rule finite_imageD) (auto intro: inj_onI) 415qed 416 417lemma finite_Plus_iff [simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B" 418 by (auto intro: finite_PlusD finite_Plus) 419 420lemma finite_Plus_UNIV_iff [simp]: 421 "finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)" 422 by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff) 423 424lemma finite_SigmaI [simp, intro]: 425 "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (SIGMA a:A. B a)" 426 unfolding Sigma_def by blast 427 428lemma finite_SigmaI2: 429 assumes "finite {x\<in>A. B x \<noteq> {}}" 430 and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)" 431 shows "finite (Sigma A B)" 432proof - 433 from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)" 434 by auto 435 also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" 436 by auto 437 finally show ?thesis . 438qed 439 440lemma finite_cartesian_product: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)" 441 by (rule finite_SigmaI) 442 443lemma finite_Prod_UNIV: 444 "finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)" 445 by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product) 446 447lemma finite_cartesian_productD1: 448 assumes "finite (A \<times> B)" and "B \<noteq> {}" 449 shows "finite A" 450proof - 451 from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}" 452 by (auto simp add: finite_conv_nat_seg_image) 453 then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" 454 by simp 455 with \<open>B \<noteq> {}\<close> have "A = (fst \<circ> f) ` {i::nat. i < n}" 456 by (simp add: image_comp) 457 then have "\<exists>n f. A = f ` {i::nat. i < n}" 458 by blast 459 then show ?thesis 460 by (auto simp add: finite_conv_nat_seg_image) 461qed 462 463lemma finite_cartesian_productD2: 464 assumes "finite (A \<times> B)" and "A \<noteq> {}" 465 shows "finite B" 466proof - 467 from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}" 468 by (auto simp add: finite_conv_nat_seg_image) 469 then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" 470 by simp 471 with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}" 472 by (simp add: image_comp) 473 then have "\<exists>n f. B = f ` {i::nat. i < n}" 474 by blast 475 then show ?thesis 476 by (auto simp add: finite_conv_nat_seg_image) 477qed 478 479lemma finite_cartesian_product_iff: 480 "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))" 481 by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product) 482 483lemma finite_prod: 484 "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)" 485 using finite_cartesian_product_iff[of UNIV UNIV] by simp 486 487lemma finite_Pow_iff [iff]: "finite (Pow A) \<longleftrightarrow> finite A" 488proof 489 assume "finite (Pow A)" 490 then have "finite ((\<lambda>x. {x}) ` A)" 491 by (blast intro: finite_subset) (* somewhat slow *) 492 then show "finite A" 493 by (rule finite_imageD [unfolded inj_on_def]) simp 494next 495 assume "finite A" 496 then show "finite (Pow A)" 497 by induct (simp_all add: Pow_insert) 498qed 499 500corollary finite_Collect_subsets [simp, intro]: "finite A \<Longrightarrow> finite {B. B \<subseteq> A}" 501 by (simp add: Pow_def [symmetric]) 502 503lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)" 504 by (simp only: finite_Pow_iff Pow_UNIV[symmetric]) 505 506lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A" 507 by (blast intro: finite_subset [OF subset_Pow_Union]) 508 509lemma finite_bind: 510 assumes "finite S" 511 assumes "\<forall>x \<in> S. finite (f x)" 512 shows "finite (Set.bind S f)" 513using assms by (simp add: bind_UNION) 514 515lemma finite_filter [simp]: "finite S \<Longrightarrow> finite (Set.filter P S)" 516unfolding Set.filter_def by simp 517 518lemma finite_set_of_finite_funs: 519 assumes "finite A" "finite B" 520 shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S") 521proof - 522 let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}" 523 have "?F ` ?S \<subseteq> Pow(A \<times> B)" 524 by auto 525 from finite_subset[OF this] assms have 1: "finite (?F ` ?S)" 526 by simp 527 have 2: "inj_on ?F ?S" 528 by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff) (* somewhat slow *) 529 show ?thesis 530 by (rule finite_imageD [OF 1 2]) 531qed 532 533lemma not_finite_existsD: 534 assumes "\<not> finite {a. P a}" 535 shows "\<exists>a. P a" 536proof (rule classical) 537 assume "\<not> ?thesis" 538 with assms show ?thesis by auto 539qed 540 541 542subsection \<open>Further induction rules on finite sets\<close> 543 544lemma finite_ne_induct [case_names singleton insert, consumes 2]: 545 assumes "finite F" and "F \<noteq> {}" 546 assumes "\<And>x. P {x}" 547 and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)" 548 shows "P F" 549 using assms 550proof induct 551 case empty 552 then show ?case by simp 553next 554 case (insert x F) 555 then show ?case by cases auto 556qed 557 558lemma finite_subset_induct [consumes 2, case_names empty insert]: 559 assumes "finite F" and "F \<subseteq> A" 560 and empty: "P {}" 561 and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)" 562 shows "P F" 563 using \<open>finite F\<close> \<open>F \<subseteq> A\<close> 564proof induct 565 show "P {}" by fact 566next 567 fix x F 568 assume "finite F" and "x \<notin> F" and P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A" 569 show "P (insert x F)" 570 proof (rule insert) 571 from i show "x \<in> A" by blast 572 from i have "F \<subseteq> A" by blast 573 with P show "P F" . 574 show "finite F" by fact 575 show "x \<notin> F" by fact 576 qed 577qed 578 579lemma finite_empty_induct: 580 assumes "finite A" 581 and "P A" 582 and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})" 583 shows "P {}" 584proof - 585 have "P (A - B)" if "B \<subseteq> A" for B :: "'a set" 586 proof - 587 from \<open>finite A\<close> that have "finite B" 588 by (rule rev_finite_subset) 589 from this \<open>B \<subseteq> A\<close> show "P (A - B)" 590 proof induct 591 case empty 592 from \<open>P A\<close> show ?case by simp 593 next 594 case (insert b B) 595 have "P (A - B - {b})" 596 proof (rule remove) 597 from \<open>finite A\<close> show "finite (A - B)" 598 by induct auto 599 from insert show "b \<in> A - B" 600 by simp 601 from insert show "P (A - B)" 602 by simp 603 qed 604 also have "A - B - {b} = A - insert b B" 605 by (rule Diff_insert [symmetric]) 606 finally show ?case . 607 qed 608 qed 609 then have "P (A - A)" by blast 610 then show ?thesis by simp 611qed 612 613lemma finite_update_induct [consumes 1, case_names const update]: 614 assumes finite: "finite {a. f a \<noteq> c}" 615 and const: "P (\<lambda>a. c)" 616 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))" 617 shows "P f" 618 using finite 619proof (induct "{a. f a \<noteq> c}" arbitrary: f) 620 case empty 621 with const show ?case by simp 622next 623 case (insert a A) 624 then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c" 625 by auto 626 with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}" 627 by simp 628 have "(f(a := c)) a = c" 629 by simp 630 from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))" 631 by simp 632 with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close> 633 have "P ((f(a := c))(a := f a))" 634 by (rule update) 635 then show ?case by simp 636qed 637 638lemma finite_subset_induct' [consumes 2, case_names empty insert]: 639 assumes "finite F" and "F \<subseteq> A" 640 and empty: "P {}" 641 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)" 642 shows "P F" 643 using assms(1,2) 644proof induct 645 show "P {}" by fact 646next 647 fix x F 648 assume "finite F" and "x \<notin> F" and 649 P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A" 650 show "P (insert x F)" 651 proof (rule insert) 652 from i show "x \<in> A" by blast 653 from i have "F \<subseteq> A" by blast 654 with P show "P F" . 655 show "finite F" by fact 656 show "x \<notin> F" by fact 657 show "F \<subseteq> A" by fact 658 qed 659qed 660 661 662subsection \<open>Class \<open>finite\<close>\<close> 663 664class finite = 665 assumes finite_UNIV: "finite (UNIV :: 'a set)" 666begin 667 668lemma finite [simp]: "finite (A :: 'a set)" 669 by (rule subset_UNIV finite_UNIV finite_subset)+ 670 671lemma finite_code [code]: "finite (A :: 'a set) \<longleftrightarrow> True" 672 by simp 673 674end 675 676instance prod :: (finite, finite) finite 677 by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 678 679lemma inj_graph: "inj (\<lambda>f. {(x, y). y = f x})" 680 by (rule inj_onI) (auto simp add: set_eq_iff fun_eq_iff) 681 682instance "fun" :: (finite, finite) finite 683proof 684 show "finite (UNIV :: ('a \<Rightarrow> 'b) set)" 685 proof (rule finite_imageD) 686 let ?graph = "\<lambda>f::'a \<Rightarrow> 'b. {(x, y). y = f x}" 687 have "range ?graph \<subseteq> Pow UNIV" 688 by simp 689 moreover have "finite (Pow (UNIV :: ('a * 'b) set))" 690 by (simp only: finite_Pow_iff finite) 691 ultimately show "finite (range ?graph)" 692 by (rule finite_subset) 693 show "inj ?graph" 694 by (rule inj_graph) 695 qed 696qed 697 698instance bool :: finite 699 by standard (simp add: UNIV_bool) 700 701instance set :: (finite) finite 702 by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) 703 704instance unit :: finite 705 by standard (simp add: UNIV_unit) 706 707instance sum :: (finite, finite) finite 708 by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 709 710 711subsection \<open>A basic fold functional for finite sets\<close> 712 713text \<open>The intended behaviour is 714 \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close> 715 if \<open>f\<close> is ``left-commutative'': 716\<close> 717 718locale comp_fun_commute = 719 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 720 assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y" 721begin 722 723lemma fun_left_comm: "f y (f x z) = f x (f y z)" 724 using comp_fun_commute by (simp add: fun_eq_iff) 725 726lemma commute_left_comp: "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)" 727 by (simp add: o_assoc comp_fun_commute) 728 729end 730 731inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" 732 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b 733 where 734 emptyI [intro]: "fold_graph f z {} z" 735 | insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)" 736 737inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" 738 739lemma fold_graph_closed_lemma: 740 "fold_graph f z A x \<and> x \<in> B" 741 if "fold_graph g z A x" 742 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b" 743 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B" 744 "z \<in> B" 745 using that(1-3) 746proof (induction rule: fold_graph.induct) 747 case (insertI x A y) 748 have "fold_graph f z A y" "y \<in> B" 749 unfolding atomize_conj 750 by (rule insertI.IH) (auto intro: insertI.prems) 751 then have "g x y \<in> B" and f_eq: "f x y = g x y" 752 by (auto simp: insertI.prems) 753 moreover have "fold_graph f z (insert x A) (f x y)" 754 by (rule fold_graph.insertI; fact) 755 ultimately 756 show ?case 757 by (simp add: f_eq) 758qed (auto intro!: that) 759 760lemma fold_graph_closed_eq: 761 "fold_graph f z A = fold_graph g z A" 762 if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b" 763 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B" 764 "z \<in> B" 765 using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that 766 by auto 767 768definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" 769 where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)" 770 771lemma fold_closed_eq: "fold f z A = fold g z A" 772 if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b" 773 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B" 774 "z \<in> B" 775 unfolding Finite_Set.fold_def 776 by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that) 777 778text \<open> 779 A tempting alternative for the definiens is 780 \<^term>\<open>if finite A then THE y. fold_graph f z A y else e\<close>. 781 It allows the removal of finiteness assumptions from the theorems 782 \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>. 783 The proofs become ugly. It is not worth the effort. (???) 784\<close> 785 786lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x" 787 by (induct rule: finite_induct) auto 788 789 790subsubsection \<open>From \<^const>\<open>fold_graph\<close> to \<^term>\<open>fold\<close>\<close> 791 792context comp_fun_commute 793begin 794 795lemma fold_graph_finite: 796 assumes "fold_graph f z A y" 797 shows "finite A" 798 using assms by induct simp_all 799 800lemma fold_graph_insertE_aux: 801 "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'" 802proof (induct set: fold_graph) 803 case emptyI 804 then show ?case by simp 805next 806 case (insertI x A y) 807 show ?case 808 proof (cases "x = a") 809 case True 810 with insertI show ?thesis by auto 811 next 812 case False 813 then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'" 814 using insertI by auto 815 have "f x y = f a (f x y')" 816 unfolding y by (rule fun_left_comm) 817 moreover have "fold_graph f z (insert x A - {a}) (f x y')" 818 using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close> 819 by (simp add: insert_Diff_if fold_graph.insertI) 820 ultimately show ?thesis 821 by fast 822 qed 823qed 824 825lemma fold_graph_insertE: 826 assumes "fold_graph f z (insert x A) v" and "x \<notin> A" 827 obtains y where "v = f x y" and "fold_graph f z A y" 828 using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1]) 829 830lemma fold_graph_determ: "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 831proof (induct arbitrary: y set: fold_graph) 832 case emptyI 833 then show ?case by fast 834next 835 case (insertI x A y v) 836 from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close> 837 obtain y' where "v = f x y'" and "fold_graph f z A y'" 838 by (rule fold_graph_insertE) 839 from \<open>fold_graph f z A y'\<close> have "y' = y" 840 by (rule insertI) 841 with \<open>v = f x y'\<close> show "v = f x y" 842 by simp 843qed 844 845lemma fold_equality: "fold_graph f z A y \<Longrightarrow> fold f z A = y" 846 by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite) 847 848lemma fold_graph_fold: 849 assumes "finite A" 850 shows "fold_graph f z A (fold f z A)" 851proof - 852 from assms have "\<exists>x. fold_graph f z A x" 853 by (rule finite_imp_fold_graph) 854 moreover note fold_graph_determ 855 ultimately have "\<exists>!x. fold_graph f z A x" 856 by (rule ex_ex1I) 857 then have "fold_graph f z A (The (fold_graph f z A))" 858 by (rule theI') 859 with assms show ?thesis 860 by (simp add: fold_def) 861qed 862 863text \<open>The base case for \<open>fold\<close>:\<close> 864 865lemma (in -) fold_infinite [simp]: "\<not> finite A \<Longrightarrow> fold f z A = z" 866 by (auto simp: fold_def) 867 868lemma (in -) fold_empty [simp]: "fold f z {} = z" 869 by (auto simp: fold_def) 870 871text \<open>The various recursion equations for \<^const>\<open>fold\<close>:\<close> 872 873lemma fold_insert [simp]: 874 assumes "finite A" and "x \<notin> A" 875 shows "fold f z (insert x A) = f x (fold f z A)" 876proof (rule fold_equality) 877 fix z 878 from \<open>finite A\<close> have "fold_graph f z A (fold f z A)" 879 by (rule fold_graph_fold) 880 with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))" 881 by (rule fold_graph.insertI) 882 then show "fold_graph f z (insert x A) (f x (fold f z A))" 883 by simp 884qed 885 886declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del] 887 \<comment> \<open>No more proofs involve these.\<close> 888 889lemma fold_fun_left_comm: "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A" 890proof (induct rule: finite_induct) 891 case empty 892 then show ?case by simp 893next 894 case insert 895 then show ?case 896 by (simp add: fun_left_comm [of x]) 897qed 898 899lemma fold_insert2: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 900 by (simp add: fold_fun_left_comm) 901 902lemma fold_rec: 903 assumes "finite A" and "x \<in> A" 904 shows "fold f z A = f x (fold f z (A - {x}))" 905proof - 906 have A: "A = insert x (A - {x})" 907 using \<open>x \<in> A\<close> by blast 908 then have "fold f z A = fold f z (insert x (A - {x}))" 909 by simp 910 also have "\<dots> = f x (fold f z (A - {x}))" 911 by (rule fold_insert) (simp add: \<open>finite A\<close>)+ 912 finally show ?thesis . 913qed 914 915lemma fold_insert_remove: 916 assumes "finite A" 917 shows "fold f z (insert x A) = f x (fold f z (A - {x}))" 918proof - 919 from \<open>finite A\<close> have "finite (insert x A)" 920 by auto 921 moreover have "x \<in> insert x A" 922 by auto 923 ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))" 924 by (rule fold_rec) 925 then show ?thesis 926 by simp 927qed 928 929lemma fold_set_union_disj: 930 assumes "finite A" "finite B" "A \<inter> B = {}" 931 shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B" 932 using assms(2,1,3) by induct simp_all 933 934end 935 936text \<open>Other properties of \<^const>\<open>fold\<close>:\<close> 937 938lemma fold_image: 939 assumes "inj_on g A" 940 shows "fold f z (g ` A) = fold (f \<circ> g) z A" 941proof (cases "finite A") 942 case False 943 with assms show ?thesis 944 by (auto dest: finite_imageD simp add: fold_def) 945next 946 case True 947 have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A" 948 proof 949 fix w 950 show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q") 951 proof 952 assume ?P 953 then show ?Q 954 using assms 955 proof (induct "g ` A" w arbitrary: A) 956 case emptyI 957 then show ?case by (auto intro: fold_graph.emptyI) 958 next 959 case (insertI x A r B) 960 from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A' 961 where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'" 962 by (rule inj_img_insertE) 963 from insertI.prems have "fold_graph (f \<circ> g) z A' r" 964 by (auto intro: insertI.hyps) 965 with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)" 966 by (rule fold_graph.insertI) 967 then show ?case 968 by simp 969 qed 970 next 971 assume ?Q 972 then show ?P 973 using assms 974 proof induct 975 case emptyI 976 then show ?case 977 by (auto intro: fold_graph.emptyI) 978 next 979 case (insertI x A r) 980 from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A" 981 by auto 982 moreover from insertI have "fold_graph f z (g ` A) r" 983 by simp 984 ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)" 985 by (rule fold_graph.insertI) 986 then show ?case 987 by simp 988 qed 989 qed 990 qed 991 with True assms show ?thesis 992 by (auto simp add: fold_def) 993qed 994 995lemma fold_cong: 996 assumes "comp_fun_commute f" "comp_fun_commute g" 997 and "finite A" 998 and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x" 999 and "s = t" and "A = B" 1000 shows "fold f s A = fold g t B" 1001proof - 1002 have "fold f s A = fold g s A" 1003 using \<open>finite A\<close> cong 1004 proof (induct A) 1005 case empty 1006 then show ?case by simp 1007 next 1008 case insert 1009 interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>) 1010 interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>) 1011 from insert show ?case by simp 1012 qed 1013 with assms show ?thesis by simp 1014qed 1015 1016 1017text \<open>A simplified version for idempotent functions:\<close> 1018 1019locale comp_fun_idem = comp_fun_commute + 1020 assumes comp_fun_idem: "f x \<circ> f x = f x" 1021begin 1022 1023lemma fun_left_idem: "f x (f x z) = f x z" 1024 using comp_fun_idem by (simp add: fun_eq_iff) 1025 1026lemma fold_insert_idem: 1027 assumes fin: "finite A" 1028 shows "fold f z (insert x A) = f x (fold f z A)" 1029proof cases 1030 assume "x \<in> A" 1031 then obtain B where "A = insert x B" and "x \<notin> B" 1032 by (rule set_insert) 1033 then show ?thesis 1034 using assms by (simp add: comp_fun_idem fun_left_idem) 1035next 1036 assume "x \<notin> A" 1037 then show ?thesis 1038 using assms by simp 1039qed 1040 1041declare fold_insert [simp del] fold_insert_idem [simp] 1042 1043lemma fold_insert_idem2: "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 1044 by (simp add: fold_fun_left_comm) 1045 1046end 1047 1048 1049subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close> 1050 1051lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \<circ> g)" 1052 by standard (simp_all add: comp_fun_commute) 1053 1054lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \<circ> g)" 1055 by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales) 1056 (simp_all add: comp_fun_idem) 1057 1058lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)" 1059proof 1060 show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" for x y 1061 proof (cases "x = y") 1062 case True 1063 then show ?thesis by simp 1064 next 1065 case False 1066 show ?thesis 1067 proof (induct "g x" arbitrary: g) 1068 case 0 1069 then show ?case by simp 1070 next 1071 case (Suc n g) 1072 have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y" 1073 proof (induct "g y" arbitrary: g) 1074 case 0 1075 then show ?case by simp 1076 next 1077 case (Suc n g) 1078 define h where "h z = g z - 1" for z 1079 with Suc have "n = h y" 1080 by simp 1081 with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y" 1082 by auto 1083 from Suc h_def have "g y = Suc (h y)" 1084 by simp 1085 then show ?case 1086 by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute) 1087 qed 1088 define h where "h z = (if z = x then g x - 1 else g z)" for z 1089 with Suc have "n = h x" 1090 by simp 1091 with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y" 1092 by auto 1093 with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" 1094 by simp 1095 from Suc h_def have "g x = Suc (h x)" 1096 by simp 1097 then show ?case 1098 by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1) 1099 qed 1100 qed 1101qed 1102 1103 1104subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close> 1105 1106lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)" 1107 by standard rule 1108 1109lemma comp_fun_idem_insert: "comp_fun_idem insert" 1110 by standard auto 1111 1112lemma comp_fun_idem_remove: "comp_fun_idem Set.remove" 1113 by standard auto 1114 1115lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf" 1116 by standard (auto simp add: inf_left_commute) 1117 1118lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup" 1119 by standard (auto simp add: sup_left_commute) 1120 1121lemma union_fold_insert: 1122 assumes "finite A" 1123 shows "A \<union> B = fold insert B A" 1124proof - 1125 interpret comp_fun_idem insert 1126 by (fact comp_fun_idem_insert) 1127 from \<open>finite A\<close> show ?thesis 1128 by (induct A arbitrary: B) simp_all 1129qed 1130 1131lemma minus_fold_remove: 1132 assumes "finite A" 1133 shows "B - A = fold Set.remove B A" 1134proof - 1135 interpret comp_fun_idem Set.remove 1136 by (fact comp_fun_idem_remove) 1137 from \<open>finite A\<close> have "fold Set.remove B A = B - A" 1138 by (induct A arbitrary: B) auto (* slow *) 1139 then show ?thesis .. 1140qed 1141 1142lemma comp_fun_commute_filter_fold: 1143 "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')" 1144proof - 1145 interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) 1146 show ?thesis by standard (auto simp: fun_eq_iff) 1147qed 1148 1149lemma Set_filter_fold: 1150 assumes "finite A" 1151 shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A" 1152 using assms 1153 by induct 1154 (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold]) 1155 1156lemma inter_Set_filter: 1157 assumes "finite B" 1158 shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B" 1159 using assms 1160 by induct (auto simp: Set.filter_def) 1161 1162lemma image_fold_insert: 1163 assumes "finite A" 1164 shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A" 1165proof - 1166 interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" 1167 by standard auto 1168 show ?thesis 1169 using assms by (induct A) auto 1170qed 1171 1172lemma Ball_fold: 1173 assumes "finite A" 1174 shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A" 1175proof - 1176 interpret comp_fun_commute "\<lambda>k s. s \<and> P k" 1177 by standard auto 1178 show ?thesis 1179 using assms by (induct A) auto 1180qed 1181 1182lemma Bex_fold: 1183 assumes "finite A" 1184 shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A" 1185proof - 1186 interpret comp_fun_commute "\<lambda>k s. s \<or> P k" 1187 by standard auto 1188 show ?thesis 1189 using assms by (induct A) auto 1190qed 1191 1192lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)" 1193 by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast (* somewhat slow *) 1194 1195lemma Pow_fold: 1196 assumes "finite A" 1197 shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A" 1198proof - 1199 interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A" 1200 by (rule comp_fun_commute_Pow_fold) 1201 show ?thesis 1202 using assms by (induct A) (auto simp: Pow_insert) 1203qed 1204 1205lemma fold_union_pair: 1206 assumes "finite B" 1207 shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B" 1208proof - 1209 interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" 1210 by standard auto 1211 show ?thesis 1212 using assms by (induct arbitrary: A) simp_all 1213qed 1214 1215lemma comp_fun_commute_product_fold: 1216 "finite B \<Longrightarrow> comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)" 1217 by standard (auto simp: fold_union_pair [symmetric]) 1218 1219lemma product_fold: 1220 assumes "finite A" "finite B" 1221 shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A" 1222 using assms unfolding Sigma_def 1223 by (induct A) 1224 (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair) 1225 1226context complete_lattice 1227begin 1228 1229lemma inf_Inf_fold_inf: 1230 assumes "finite A" 1231 shows "inf (Inf A) B = fold inf B A" 1232proof - 1233 interpret comp_fun_idem inf 1234 by (fact comp_fun_idem_inf) 1235 from \<open>finite A\<close> fold_fun_left_comm show ?thesis 1236 by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff) 1237qed 1238 1239lemma sup_Sup_fold_sup: 1240 assumes "finite A" 1241 shows "sup (Sup A) B = fold sup B A" 1242proof - 1243 interpret comp_fun_idem sup 1244 by (fact comp_fun_idem_sup) 1245 from \<open>finite A\<close> fold_fun_left_comm show ?thesis 1246 by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff) 1247qed 1248 1249lemma Inf_fold_inf: "finite A \<Longrightarrow> Inf A = fold inf top A" 1250 using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) 1251 1252lemma Sup_fold_sup: "finite A \<Longrightarrow> Sup A = fold sup bot A" 1253 using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) 1254 1255lemma inf_INF_fold_inf: 1256 assumes "finite A" 1257 shows "inf B (\<Sqinter>(f ` A)) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 1258proof - 1259 interpret comp_fun_idem inf by (fact comp_fun_idem_inf) 1260 interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem) 1261 from \<open>finite A\<close> have "?fold = ?inf" 1262 by (induct A arbitrary: B) (simp_all add: inf_left_commute) 1263 then show ?thesis .. 1264qed 1265 1266lemma sup_SUP_fold_sup: 1267 assumes "finite A" 1268 shows "sup B (\<Squnion>(f ` A)) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 1269proof - 1270 interpret comp_fun_idem sup by (fact comp_fun_idem_sup) 1271 interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem) 1272 from \<open>finite A\<close> have "?fold = ?sup" 1273 by (induct A arbitrary: B) (simp_all add: sup_left_commute) 1274 then show ?thesis .. 1275qed 1276 1277lemma INF_fold_inf: "finite A \<Longrightarrow> \<Sqinter>(f ` A) = fold (inf \<circ> f) top A" 1278 using inf_INF_fold_inf [of A top] by simp 1279 1280lemma SUP_fold_sup: "finite A \<Longrightarrow> \<Squnion>(f ` A) = fold (sup \<circ> f) bot A" 1281 using sup_SUP_fold_sup [of A bot] by simp 1282 1283end 1284 1285 1286subsection \<open>Locales as mini-packages for fold operations\<close> 1287 1288subsubsection \<open>The natural case\<close> 1289 1290locale folding = 1291 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b" 1292 assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y" 1293begin 1294 1295interpretation fold?: comp_fun_commute f 1296 by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>) 1297 1298definition F :: "'a set \<Rightarrow> 'b" 1299 where eq_fold: "F A = fold f z A" 1300 1301lemma empty [simp]:"F {} = z" 1302 by (simp add: eq_fold) 1303 1304lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z" 1305 by (simp add: eq_fold) 1306 1307lemma insert [simp]: 1308 assumes "finite A" and "x \<notin> A" 1309 shows "F (insert x A) = f x (F A)" 1310proof - 1311 from fold_insert assms 1312 have "fold f z (insert x A) = f x (fold f z A)" by simp 1313 with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff) 1314qed 1315 1316lemma remove: 1317 assumes "finite A" and "x \<in> A" 1318 shows "F A = f x (F (A - {x}))" 1319proof - 1320 from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B" 1321 by (auto dest: mk_disjoint_insert) 1322 moreover from \<open>finite A\<close> A have "finite B" by simp 1323 ultimately show ?thesis by simp 1324qed 1325 1326lemma insert_remove: "finite A \<Longrightarrow> F (insert x A) = f x (F (A - {x}))" 1327 by (cases "x \<in> A") (simp_all add: remove insert_absorb) 1328 1329end 1330 1331 1332subsubsection \<open>With idempotency\<close> 1333 1334locale folding_idem = folding + 1335 assumes comp_fun_idem: "f x \<circ> f x = f x" 1336begin 1337 1338declare insert [simp del] 1339 1340interpretation fold?: comp_fun_idem f 1341 by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) 1342 1343lemma insert_idem [simp]: 1344 assumes "finite A" 1345 shows "F (insert x A) = f x (F A)" 1346proof - 1347 from fold_insert_idem assms 1348 have "fold f z (insert x A) = f x (fold f z A)" by simp 1349 with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff) 1350qed 1351 1352end 1353 1354 1355subsection \<open>Finite cardinality\<close> 1356 1357text \<open> 1358 The traditional definition 1359 \<^prop>\<open>card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}\<close> 1360 is ugly to work with. 1361 But now that we have \<^const>\<open>fold\<close> things are easy: 1362\<close> 1363 1364global_interpretation card: folding "\<lambda>_. Suc" 0 1365 defines card = "folding.F (\<lambda>_. Suc) 0" 1366 by standard rule 1367 1368lemma card_infinite: "\<not> finite A \<Longrightarrow> card A = 0" 1369 by (fact card.infinite) 1370 1371lemma card_empty: "card {} = 0" 1372 by (fact card.empty) 1373 1374lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)" 1375 by (fact card.insert) 1376 1377lemma card_insert_if: "finite A \<Longrightarrow> card (insert x A) = (if x \<in> A then card A else Suc (card A))" 1378 by auto (simp add: card.insert_remove card.remove) 1379 1380lemma card_ge_0_finite: "card A > 0 \<Longrightarrow> finite A" 1381 by (rule ccontr) simp 1382 1383lemma card_0_eq [simp]: "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}" 1384 by (auto dest: mk_disjoint_insert) 1385 1386lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0" 1387 by (rule ccontr) simp 1388 1389lemma card_eq_0_iff: "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A" 1390 by auto 1391 1392lemma card_range_greater_zero: "finite (range f) \<Longrightarrow> card (range f) > 0" 1393 by (rule ccontr) (simp add: card_eq_0_iff) 1394 1395lemma card_gt_0_iff: "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A" 1396 by (simp add: neq0_conv [symmetric] card_eq_0_iff) 1397 1398lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A" 1399 apply (rule insert_Diff [THEN subst, where t = A]) 1400 apply assumption 1401 apply (simp del: insert_Diff_single) 1402 done 1403 1404lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n" 1405 apply (cases "finite y") 1406 apply (cases "x \<in> y") 1407 apply (auto simp: insert_absorb) 1408 done 1409 1410lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1" 1411 by (simp add: card_Suc_Diff1 [symmetric]) 1412 1413lemma card_Diff_singleton_if: 1414 "finite A \<Longrightarrow> card (A - {x}) = (if x \<in> A then card A - 1 else card A)" 1415 by (simp add: card_Diff_singleton) 1416 1417lemma card_Diff_insert[simp]: 1418 assumes "finite A" and "a \<in> A" and "a \<notin> B" 1419 shows "card (A - insert a B) = card (A - B) - 1" 1420proof - 1421 have "A - insert a B = (A - B) - {a}" 1422 using assms by blast 1423 then show ?thesis 1424 using assms by (simp add: card_Diff_singleton) 1425qed 1426 1427lemma card_insert: "finite A \<Longrightarrow> card (insert x A) = Suc (card (A - {x}))" 1428 by (fact card.insert_remove) 1429 1430lemma card_insert_le: "finite A \<Longrightarrow> card A \<le> card (insert x A)" 1431 by (simp add: card_insert_if) 1432 1433lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n" 1434 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq) 1435 1436lemma card_Collect_le_nat[simp]: "card {i::nat. i \<le> n} = Suc n" 1437 using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le) 1438 1439lemma card_mono: 1440 assumes "finite B" and "A \<subseteq> B" 1441 shows "card A \<le> card B" 1442proof - 1443 from assms have "finite A" 1444 by (auto intro: finite_subset) 1445 then show ?thesis 1446 using assms 1447 proof (induct A arbitrary: B) 1448 case empty 1449 then show ?case by simp 1450 next 1451 case (insert x A) 1452 then have "x \<in> B" 1453 by simp 1454 from insert have "A \<subseteq> B - {x}" and "finite (B - {x})" 1455 by auto 1456 with insert.hyps have "card A \<le> card (B - {x})" 1457 by auto 1458 with \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case 1459 by simp (simp only: card.remove) 1460 qed 1461qed 1462 1463lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)" 1464 apply (induct rule: finite_induct) 1465 apply simp 1466 apply clarify 1467 apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F") 1468 prefer 2 apply (blast intro: finite_subset, atomize) 1469 apply (drule_tac x = "A - {x}" in spec) 1470 apply (simp add: card_Diff_singleton_if split: if_split_asm) 1471 apply (case_tac "card A", auto) 1472 done 1473 1474lemma psubset_card_mono: "finite B \<Longrightarrow> A < B \<Longrightarrow> card A < card B" 1475 apply (simp add: psubset_eq linorder_not_le [symmetric]) 1476 apply (blast dest: card_seteq) 1477 done 1478 1479lemma card_Un_Int: 1480 assumes "finite A" "finite B" 1481 shows "card A + card B = card (A \<union> B) + card (A \<inter> B)" 1482 using assms 1483proof (induct A) 1484 case empty 1485 then show ?case by simp 1486next 1487 case insert 1488 then show ?case 1489 by (auto simp add: insert_absorb Int_insert_left) 1490qed 1491 1492lemma card_Un_disjoint: "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> card (A \<union> B) = card A + card B" 1493 using card_Un_Int [of A B] by simp 1494 1495lemma card_Un_le: "card (A \<union> B) \<le> card A + card B" 1496proof (cases "finite A \<and> finite B") 1497 case True 1498 then show ?thesis 1499 using le_iff_add card_Un_Int [of A B] by auto 1500qed auto 1501 1502lemma card_Diff_subset: 1503 assumes "finite B" 1504 and "B \<subseteq> A" 1505 shows "card (A - B) = card A - card B" 1506 using assms 1507proof (cases "finite A") 1508 case False 1509 with assms show ?thesis 1510 by simp 1511next 1512 case True 1513 with assms show ?thesis 1514 by (induct B arbitrary: A) simp_all 1515qed 1516 1517lemma card_Diff_subset_Int: 1518 assumes "finite (A \<inter> B)" 1519 shows "card (A - B) = card A - card (A \<inter> B)" 1520proof - 1521 have "A - B = A - A \<inter> B" by auto 1522 with assms show ?thesis 1523 by (simp add: card_Diff_subset) 1524qed 1525 1526lemma diff_card_le_card_Diff: 1527 assumes "finite B" 1528 shows "card A - card B \<le> card (A - B)" 1529proof - 1530 have "card A - card B \<le> card A - card (A \<inter> B)" 1531 using card_mono[OF assms Int_lower2, of A] by arith 1532 also have "\<dots> = card (A - B)" 1533 using assms by (simp add: card_Diff_subset_Int) 1534 finally show ?thesis . 1535qed 1536 1537lemma card_le_sym_Diff: 1538 assumes "finite A" "finite B" "card A \<le> card B" 1539 shows "card(A - B) \<le> card(B - A)" 1540proof - 1541 have "card(A - B) = card A - card (A \<inter> B)" using assms(1,2) by(simp add: card_Diff_subset_Int) 1542 also have "\<dots> \<le> card B - card (A \<inter> B)" using assms(3) by linarith 1543 also have "\<dots> = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) 1544 finally show ?thesis . 1545qed 1546 1547lemma card_less_sym_Diff: 1548 assumes "finite A" "finite B" "card A < card B" 1549 shows "card(A - B) < card(B - A)" 1550proof - 1551 have "card(A - B) = card A - card (A \<inter> B)" using assms(1,2) by(simp add: card_Diff_subset_Int) 1552 also have "\<dots> < card B - card (A \<inter> B)" using assms(1,3) by (simp add: card_mono diff_less_mono) 1553 also have "\<dots> = card(B - A)" using assms(1,2) by(simp add: card_Diff_subset_Int Int_commute) 1554 finally show ?thesis . 1555qed 1556 1557lemma card_Diff1_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) < card A" 1558 by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert) 1559 1560lemma card_Diff2_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> card (A - {x} - {y}) < card A" 1561 apply (cases "x = y") 1562 apply (simp add: card_Diff1_less del:card_Diff_insert) 1563 apply (rule less_trans) 1564 prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert) 1565 done 1566 1567lemma card_Diff1_le: "finite A \<Longrightarrow> card (A - {x}) \<le> card A" 1568 by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le) 1569 1570lemma card_psubset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> card A < card B \<Longrightarrow> A < B" 1571 by (erule psubsetI) blast 1572 1573lemma card_le_inj: 1574 assumes fA: "finite A" 1575 and fB: "finite B" 1576 and c: "card A \<le> card B" 1577 shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A" 1578 using fA fB c 1579proof (induct arbitrary: B rule: finite_induct) 1580 case empty 1581 then show ?case by simp 1582next 1583 case (insert x s t) 1584 then show ?case 1585 proof (induct rule: finite_induct [OF insert.prems(1)]) 1586 case 1 1587 then show ?case by simp 1588 next 1589 case (2 y t) 1590 from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t" 1591 by simp 1592 from "2.prems"(3) [OF "2.hyps"(1) cst] 1593 obtain f where "f ` s \<subseteq> t" "inj_on f s" 1594 by blast 1595 with "2.prems"(2) "2.hyps"(2) show ?case 1596 apply - 1597 apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"]) 1598 apply (auto simp add: inj_on_def) 1599 done 1600 qed 1601qed 1602 1603lemma card_subset_eq: 1604 assumes fB: "finite B" 1605 and AB: "A \<subseteq> B" 1606 and c: "card A = card B" 1607 shows "A = B" 1608proof - 1609 from fB AB have fA: "finite A" 1610 by (auto intro: finite_subset) 1611 from fA fB have fBA: "finite (B - A)" 1612 by auto 1613 have e: "A \<inter> (B - A) = {}" 1614 by blast 1615 have eq: "A \<union> (B - A) = B" 1616 using AB by blast 1617 from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0" 1618 by arith 1619 then have "B - A = {}" 1620 unfolding card_eq_0_iff using fA fB by simp 1621 with AB show "A = B" 1622 by blast 1623qed 1624 1625lemma insert_partition: 1626 "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 = {}" 1627 by auto (* somewhat slow *) 1628 1629lemma finite_psubset_induct [consumes 1, case_names psubset]: 1630 assumes finite: "finite A" 1631 and major: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A" 1632 shows "P A" 1633 using finite 1634proof (induct A taking: card rule: measure_induct_rule) 1635 case (less A) 1636 have fin: "finite A" by fact 1637 have ih: "card B < card A \<Longrightarrow> finite B \<Longrightarrow> P B" for B by fact 1638 have "P B" if "B \<subset> A" for B 1639 proof - 1640 from that have "card B < card A" 1641 using psubset_card_mono fin by blast 1642 moreover 1643 from that have "B \<subseteq> A" 1644 by auto 1645 then have "finite B" 1646 using fin finite_subset by blast 1647 ultimately show ?thesis using ih by simp 1648 qed 1649 with fin show "P A" using major by blast 1650qed 1651 1652lemma finite_induct_select [consumes 1, case_names empty select]: 1653 assumes "finite S" 1654 and "P {}" 1655 and select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)" 1656 shows "P S" 1657proof - 1658 have "0 \<le> card S" by simp 1659 then have "\<exists>T \<subseteq> S. card T = card S \<and> P T" 1660 proof (induct rule: dec_induct) 1661 case base with \<open>P {}\<close> 1662 show ?case 1663 by (intro exI[of _ "{}"]) auto 1664 next 1665 case (step n) 1666 then obtain T where T: "T \<subseteq> S" "card T = n" "P T" 1667 by auto 1668 with \<open>n < card S\<close> have "T \<subset> S" "P T" 1669 by auto 1670 with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)" 1671 by auto 1672 with step(2) T \<open>finite S\<close> show ?case 1673 by (intro exI[of _ "insert s T"]) (auto dest: finite_subset) 1674 qed 1675 with \<open>finite S\<close> show "P S" 1676 by (auto dest: card_subset_eq) 1677qed 1678 1679lemma remove_induct [case_names empty infinite remove]: 1680 assumes empty: "P ({} :: 'a set)" 1681 and infinite: "\<not> finite B \<Longrightarrow> P B" 1682 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" 1683 shows "P B" 1684proof (cases "finite B") 1685 case False 1686 then show ?thesis by (rule infinite) 1687next 1688 case True 1689 define A where "A = B" 1690 with True have "finite A" "A \<subseteq> B" 1691 by simp_all 1692 then show "P A" 1693 proof (induct "card A" arbitrary: A) 1694 case 0 1695 then have "A = {}" by auto 1696 with empty show ?case by simp 1697 next 1698 case (Suc n A) 1699 from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A" 1700 by (rule finite_subset) 1701 moreover from Suc.hyps have "A \<noteq> {}" by auto 1702 moreover note \<open>A \<subseteq> B\<close> 1703 moreover have "P (A - {x})" if x: "x \<in> A" for x 1704 using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto 1705 ultimately show ?case by (rule remove) 1706 qed 1707qed 1708 1709lemma finite_remove_induct [consumes 1, case_names empty remove]: 1710 fixes P :: "'a set \<Rightarrow> bool" 1711 assumes "finite B" 1712 and "P {}" 1713 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" 1714 defines "B' \<equiv> B" 1715 shows "P B'" 1716 by (induct B' rule: remove_induct) (simp_all add: assms) 1717 1718 1719text \<open>Main cardinality theorem.\<close> 1720lemma card_partition [rule_format]: 1721 "finite C \<Longrightarrow> finite (\<Union>C) \<Longrightarrow> (\<forall>c\<in>C. card c = k) \<Longrightarrow> 1722 (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow> 1723 k * card C = card (\<Union>C)" 1724proof (induct rule: finite_induct) 1725 case empty 1726 then show ?case by simp 1727next 1728 case (insert x F) 1729 then show ?case 1730 by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert _ _)"]) 1731qed 1732 1733lemma card_eq_UNIV_imp_eq_UNIV: 1734 assumes fin: "finite (UNIV :: 'a set)" 1735 and card: "card A = card (UNIV :: 'a set)" 1736 shows "A = (UNIV :: 'a set)" 1737proof 1738 show "A \<subseteq> UNIV" by simp 1739 show "UNIV \<subseteq> A" 1740 proof 1741 show "x \<in> A" for x 1742 proof (rule ccontr) 1743 assume "x \<notin> A" 1744 then have "A \<subset> UNIV" by auto 1745 with fin have "card A < card (UNIV :: 'a set)" 1746 by (fact psubset_card_mono) 1747 with card show False by simp 1748 qed 1749 qed 1750qed 1751 1752text \<open>The form of a finite set of given cardinality\<close> 1753 1754lemma card_eq_SucD: 1755 assumes "card A = Suc k" 1756 shows "\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {})" 1757proof - 1758 have fin: "finite A" 1759 using assms by (auto intro: ccontr) 1760 moreover have "card A \<noteq> 0" 1761 using assms by auto 1762 ultimately obtain b where b: "b \<in> A" 1763 by auto 1764 show ?thesis 1765 proof (intro exI conjI) 1766 show "A = insert b (A - {b})" 1767 using b by blast 1768 show "b \<notin> A - {b}" 1769 by blast 1770 show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}" 1771 using assms b fin by (fastforce dest: mk_disjoint_insert)+ 1772 qed 1773qed 1774 1775lemma card_Suc_eq: 1776 "card A = Suc k \<longleftrightarrow> 1777 (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))" 1778 apply (auto elim!: card_eq_SucD) 1779 apply (subst card.insert) 1780 apply (auto simp add: intro:ccontr) 1781 done 1782 1783lemma card_1_singletonE: 1784 assumes "card A = 1" 1785 obtains x where "A = {x}" 1786 using assms by (auto simp: card_Suc_eq) 1787 1788lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1" 1789 unfolding is_singleton_def 1790 by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def) 1791 1792lemma card_1_singleton_iff: "card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})" 1793 by (simp add: card_Suc_eq) 1794 1795lemma card_le_Suc0_iff_eq: 1796 assumes "finite A" 1797 shows "card A \<le> Suc 0 \<longleftrightarrow> (\<forall>a1 \<in> A. \<forall>a2 \<in> A. a1 = a2)" (is "?C = ?A") 1798proof 1799 assume ?C thus ?A using assms by (auto simp: le_Suc_eq dest: card_eq_SucD) 1800next 1801 assume ?A 1802 show ?C 1803 proof cases 1804 assume "A = {}" thus ?C using \<open>?A\<close> by simp 1805 next 1806 assume "A \<noteq> {}" 1807 then obtain a where "A = {a}" using \<open>?A\<close> by blast 1808 thus ?C by simp 1809 qed 1810qed 1811 1812lemma card_le_Suc_iff: 1813 "Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)" 1814apply(cases "finite A") 1815 apply (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff 1816 dest: subset_singletonD split: nat.splits if_splits) 1817by auto 1818 1819lemma finite_fun_UNIVD2: 1820 assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)" 1821 shows "finite (UNIV :: 'b set)" 1822proof - 1823 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" for arbitrary 1824 by (rule finite_imageI) 1825 moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)" for arbitrary 1826 by (rule UNIV_eq_I) auto 1827 ultimately show "finite (UNIV :: 'b set)" 1828 by simp 1829qed 1830 1831lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1" 1832 unfolding UNIV_unit by simp 1833 1834lemma infinite_arbitrarily_large: 1835 assumes "\<not> finite A" 1836 shows "\<exists>B. finite B \<and> card B = n \<and> B \<subseteq> A" 1837proof (induction n) 1838 case 0 1839 show ?case by (intro exI[of _ "{}"]) auto 1840next 1841 case (Suc n) 1842 then obtain B where B: "finite B \<and> card B = n \<and> B \<subseteq> A" .. 1843 with \<open>\<not> finite A\<close> have "A \<noteq> B" by auto 1844 with B have "B \<subset> A" by auto 1845 then have "\<exists>x. x \<in> A - B" 1846 by (elim psubset_imp_ex_mem) 1847 then obtain x where x: "x \<in> A - B" .. 1848 with B have "finite (insert x B) \<and> card (insert x B) = Suc n \<and> insert x B \<subseteq> A" 1849 by auto 1850 then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" .. 1851qed 1852 1853text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets 1854and to show that their cardinalities are uniformly bounded. This possibility is formalized in 1855the next criterion.\<close> 1856 1857lemma finite_if_finite_subsets_card_bdd: 1858 assumes "\<And>G. G \<subseteq> F \<Longrightarrow> finite G \<Longrightarrow> card G \<le> C" 1859 shows "finite F \<and> card F \<le> C" 1860proof (cases "finite F") 1861 case False 1862 obtain n::nat where n: "n > max C 0" by auto 1863 obtain G where G: "G \<subseteq> F" "card G = n" using infinite_arbitrarily_large[OF False] by auto 1864 hence "finite G" using \<open>n > max C 0\<close> using card_infinite gr_implies_not0 by blast 1865 hence False using assms G n not_less by auto 1866 thus ?thesis .. 1867next 1868 case True thus ?thesis using assms[of F] by auto 1869qed 1870 1871 1872subsubsection \<open>Cardinality of image\<close> 1873 1874lemma card_image_le: "finite A \<Longrightarrow> card (f ` A) \<le> card A" 1875 by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if) 1876 1877lemma card_image: "inj_on f A \<Longrightarrow> card (f ` A) = card A" 1878proof (induct A rule: infinite_finite_induct) 1879 case (infinite A) 1880 then have "\<not> finite (f ` A)" by (auto dest: finite_imageD) 1881 with infinite show ?case by simp 1882qed simp_all 1883 1884lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B" 1885 by (auto simp: card_image bij_betw_def) 1886 1887lemma endo_inj_surj: "finite A \<Longrightarrow> f ` A \<subseteq> A \<Longrightarrow> inj_on f A \<Longrightarrow> f ` A = A" 1888 by (simp add: card_seteq card_image) 1889 1890lemma eq_card_imp_inj_on: 1891 assumes "finite A" "card(f ` A) = card A" 1892 shows "inj_on f A" 1893 using assms 1894proof (induct rule:finite_induct) 1895 case empty 1896 show ?case by simp 1897next 1898 case (insert x A) 1899 then show ?case 1900 using card_image_le [of A f] by (simp add: card_insert_if split: if_splits) 1901qed 1902 1903lemma inj_on_iff_eq_card: "finite A \<Longrightarrow> inj_on f A \<longleftrightarrow> card (f ` A) = card A" 1904 by (blast intro: card_image eq_card_imp_inj_on) 1905 1906lemma card_inj_on_le: 1907 assumes "inj_on f A" "f ` A \<subseteq> B" "finite B" 1908 shows "card A \<le> card B" 1909proof - 1910 have "finite A" 1911 using assms by (blast intro: finite_imageD dest: finite_subset) 1912 then show ?thesis 1913 using assms by (force intro: card_mono simp: card_image [symmetric]) 1914qed 1915 1916lemma inj_on_iff_card_le: 1917 "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> (\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)" 1918using card_inj_on_le[of _ A B] card_le_inj[of A B] by blast 1919 1920lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A" 1921 by (blast intro: card_image_le card_mono le_trans) 1922 1923lemma card_bij_eq: 1924 "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 1925 \<Longrightarrow> card A = card B" 1926 by (auto intro: le_antisym card_inj_on_le) 1927 1928lemma bij_betw_finite: "bij_betw f A B \<Longrightarrow> finite A \<longleftrightarrow> finite B" 1929 unfolding bij_betw_def using finite_imageD [of f A] by auto 1930 1931lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A" 1932 using finite_imageD finite_subset by blast 1933 1934lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A" 1935 by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq 1936 intro: card_image[symmetric, OF subset_inj_on]) 1937 1938 1939subsubsection \<open>Pigeonhole Principles\<close> 1940 1941lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A " 1942 by (auto dest: card_image less_irrefl_nat) 1943 1944lemma pigeonhole_infinite: 1945 assumes "\<not> finite A" and "finite (f`A)" 1946 shows "\<exists>a0\<in>A. \<not> finite {a\<in>A. f a = f a0}" 1947 using assms(2,1) 1948proof (induct "f`A" arbitrary: A rule: finite_induct) 1949 case empty 1950 then show ?case by simp 1951next 1952 case (insert b F) 1953 show ?case 1954 proof (cases "finite {a\<in>A. f a = b}") 1955 case True 1956 with \<open>\<not> finite A\<close> have "\<not> finite (A - {a\<in>A. f a = b})" 1957 by simp 1958 also have "A - {a\<in>A. f a = b} = {a\<in>A. f a \<noteq> b}" 1959 by blast 1960 finally have "\<not> finite {a\<in>A. f a \<noteq> b}" . 1961 from insert(3)[OF _ this] insert(2,4) show ?thesis 1962 by simp (blast intro: rev_finite_subset) 1963 next 1964 case False 1965 then have "{a \<in> A. f a = b} \<noteq> {}" by force 1966 with False show ?thesis by blast 1967 qed 1968qed 1969 1970lemma pigeonhole_infinite_rel: 1971 assumes "\<not> finite A" 1972 and "finite B" 1973 and "\<forall>a\<in>A. \<exists>b\<in>B. R a b" 1974 shows "\<exists>b\<in>B. \<not> finite {a:A. R a b}" 1975proof - 1976 let ?F = "\<lambda>a. {b\<in>B. R a b}" 1977 from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>] have "finite (?F ` A)" 1978 by (blast intro: rev_finite_subset) 1979 from pigeonhole_infinite [where f = ?F, OF assms(1) this] 1980 obtain a0 where "a0 \<in> A" and infinite: "\<not> finite {a\<in>A. ?F a = ?F a0}" .. 1981 obtain b0 where "b0 \<in> B" and "R a0 b0" 1982 using \<open>a0 \<in> A\<close> assms(3) by blast 1983 have "finite {a\<in>A. ?F a = ?F a0}" if "finite {a\<in>A. R a b0}" 1984 using \<open>b0 \<in> B\<close> \<open>R a0 b0\<close> that by (blast intro: rev_finite_subset) 1985 with infinite \<open>b0 \<in> B\<close> show ?thesis 1986 by blast 1987qed 1988 1989 1990subsubsection \<open>Cardinality of sums\<close> 1991 1992lemma card_Plus: 1993 assumes "finite A" "finite B" 1994 shows "card (A <+> B) = card A + card B" 1995proof - 1996 have "Inl`A \<inter> Inr`B = {}" by fast 1997 with assms show ?thesis 1998 by (simp add: Plus_def card_Un_disjoint card_image) 1999qed 2000 2001lemma card_Plus_conv_if: 2002 "card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)" 2003 by (auto simp add: card_Plus) 2004 2005text \<open>Relates to equivalence classes. Based on a theorem of F. Kamm��ller.\<close> 2006 2007lemma dvd_partition: 2008 assumes f: "finite (\<Union>C)" 2009 and "\<forall>c\<in>C. k dvd card c" "\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}" 2010 shows "k dvd card (\<Union>C)" 2011proof - 2012 have "finite C" 2013 by (rule finite_UnionD [OF f]) 2014 then show ?thesis 2015 using assms 2016 proof (induct rule: finite_induct) 2017 case empty 2018 show ?case by simp 2019 next 2020 case insert 2021 then show ?case 2022 apply simp 2023 apply (subst card_Un_disjoint) 2024 apply (auto simp add: disjoint_eq_subset_Compl) 2025 done 2026 qed 2027qed 2028 2029 2030subsubsection \<open>Relating injectivity and surjectivity\<close> 2031 2032lemma finite_surj_inj: 2033 assumes "finite A" "A \<subseteq> f ` A" 2034 shows "inj_on f A" 2035proof - 2036 have "f ` A = A" 2037 by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le) 2038 then show ?thesis using assms 2039 by (simp add: eq_card_imp_inj_on) 2040qed 2041 2042lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f" 2043 for f :: "'a \<Rightarrow> 'a" 2044 by (blast intro: finite_surj_inj subset_UNIV) 2045 2046lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" 2047 for f :: "'a \<Rightarrow> 'a" 2048 by (fastforce simp:surj_def dest!: endo_inj_surj) 2049 2050lemma surjective_iff_injective_gen: 2051 assumes fS: "finite S" 2052 and fT: "finite T" 2053 and c: "card S = card T" 2054 and ST: "f ` S \<subseteq> T" 2055 shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S" 2056 (is "?lhs \<longleftrightarrow> ?rhs") 2057proof 2058 assume h: "?lhs" 2059 { 2060 fix x y 2061 assume x: "x \<in> S" 2062 assume y: "y \<in> S" 2063 assume f: "f x = f y" 2064 from x fS have S0: "card S \<noteq> 0" 2065 by auto 2066 have "x = y" 2067 proof (rule ccontr) 2068 assume xy: "\<not> ?thesis" 2069 have th: "card S \<le> card (f ` (S - {y}))" 2070 unfolding c 2071 proof (rule card_mono) 2072 show "finite (f ` (S - {y}))" 2073 by (simp add: fS) 2074 have "\<lbrakk>x \<noteq> y; x \<in> S; z \<in> S; f x = f y\<rbrakk> 2075 \<Longrightarrow> \<exists>x \<in> S. x \<noteq> y \<and> f z = f x" for z 2076 by (case_tac "z = y \<longrightarrow> z = x") auto 2077 then show "T \<subseteq> f ` (S - {y})" 2078 using h xy x y f by fastforce 2079 qed 2080 also have " \<dots> \<le> card (S - {y})" 2081 by (simp add: card_image_le fS) 2082 also have "\<dots> \<le> card S - 1" using y fS by simp 2083 finally show False using S0 by arith 2084 qed 2085 } 2086 then show ?rhs 2087 unfolding inj_on_def by blast 2088next 2089 assume h: ?rhs 2090 have "f ` S = T" 2091 by (simp add: ST c card_image card_subset_eq fT h) 2092 then show ?lhs by blast 2093qed 2094 2095hide_const (open) Finite_Set.fold 2096 2097 2098subsection \<open>Infinite Sets\<close> 2099 2100text \<open> 2101 Some elementary facts about infinite sets, mostly by Stephan Merz. 2102 Beware! Because "infinite" merely abbreviates a negation, these 2103 lemmas may not work well with \<open>blast\<close>. 2104\<close> 2105 2106abbreviation infinite :: "'a set \<Rightarrow> bool" 2107 where "infinite S \<equiv> \<not> finite S" 2108 2109text \<open> 2110 Infinite sets are non-empty, and if we remove some elements from an 2111 infinite set, the result is still infinite. 2112\<close> 2113 2114lemma infinite_UNIV_nat [iff]: "infinite (UNIV :: nat set)" 2115proof 2116 assume "finite (UNIV :: nat set)" 2117 with finite_UNIV_inj_surj [of Suc] show False 2118 by simp (blast dest: Suc_neq_Zero surjD) 2119qed 2120 2121lemma infinite_UNIV_char_0: "infinite (UNIV :: 'a::semiring_char_0 set)" 2122proof 2123 assume "finite (UNIV :: 'a set)" 2124 with subset_UNIV have "finite (range of_nat :: 'a set)" 2125 by (rule finite_subset) 2126 moreover have "inj (of_nat :: nat \<Rightarrow> 'a)" 2127 by (simp add: inj_on_def) 2128 ultimately have "finite (UNIV :: nat set)" 2129 by (rule finite_imageD) 2130 then show False 2131 by simp 2132qed 2133 2134lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}" 2135 by auto 2136 2137lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})" 2138 by simp 2139 2140lemma Diff_infinite_finite: 2141 assumes "finite T" "infinite S" 2142 shows "infinite (S - T)" 2143 using \<open>finite T\<close> 2144proof induct 2145 from \<open>infinite S\<close> show "infinite (S - {})" 2146 by auto 2147next 2148 fix T x 2149 assume ih: "infinite (S - T)" 2150 have "S - (insert x T) = (S - T) - {x}" 2151 by (rule Diff_insert) 2152 with ih show "infinite (S - (insert x T))" 2153 by (simp add: infinite_remove) 2154qed 2155 2156lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)" 2157 by simp 2158 2159lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" 2160 by simp 2161 2162lemma infinite_super: 2163 assumes "S \<subseteq> T" 2164 and "infinite S" 2165 shows "infinite T" 2166proof 2167 assume "finite T" 2168 with \<open>S \<subseteq> T\<close> have "finite S" by (simp add: finite_subset) 2169 with \<open>infinite S\<close> show False by simp 2170qed 2171 2172proposition infinite_coinduct [consumes 1, case_names infinite]: 2173 assumes "X A" 2174 and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})" 2175 shows "infinite A" 2176proof 2177 assume "finite A" 2178 then show False 2179 using \<open>X A\<close> 2180 proof (induction rule: finite_psubset_induct) 2181 case (psubset A) 2182 then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})" 2183 using local.step psubset.prems by blast 2184 then have "X (A - {x})" 2185 using psubset.hyps by blast 2186 show False 2187 apply (rule psubset.IH [where B = "A - {x}"]) 2188 apply (use \<open>x \<in> A\<close> in blast) 2189 apply (simp add: \<open>X (A - {x})\<close>) 2190 done 2191 qed 2192qed 2193 2194text \<open> 2195 For any function with infinite domain and finite range there is some 2196 element that is the image of infinitely many domain elements. In 2197 particular, any infinite sequence of elements from a finite set 2198 contains some element that occurs infinitely often. 2199\<close> 2200 2201lemma inf_img_fin_dom': 2202 assumes img: "finite (f ` A)" 2203 and dom: "infinite A" 2204 shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)" 2205proof (rule ccontr) 2206 have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto 2207 moreover assume "\<not> ?thesis" 2208 with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast 2209 ultimately have "finite A" by (rule finite_subset) 2210 with dom show False by contradiction 2211qed 2212 2213lemma inf_img_fin_domE': 2214 assumes "finite (f ` A)" and "infinite A" 2215 obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)" 2216 using assms by (blast dest: inf_img_fin_dom') 2217 2218lemma inf_img_fin_dom: 2219 assumes img: "finite (f`A)" and dom: "infinite A" 2220 shows "\<exists>y \<in> f`A. infinite (f -` {y})" 2221 using inf_img_fin_dom'[OF assms] by auto 2222 2223lemma inf_img_fin_domE: 2224 assumes "finite (f`A)" and "infinite A" 2225 obtains y where "y \<in> f`A" and "infinite (f -` {y})" 2226 using assms by (blast dest: inf_img_fin_dom) 2227 2228proposition finite_image_absD: "finite (abs ` S) \<Longrightarrow> finite S" 2229 for S :: "'a::linordered_ring set" 2230 by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) 2231 2232subsection \<open>The finite powerset operator\<close> 2233 2234definition Fpow :: "'a set \<Rightarrow> 'a set set" 2235where "Fpow A \<equiv> {X. X \<subseteq> A \<and> finite X}" 2236 2237lemma Fpow_mono: "A \<subseteq> B \<Longrightarrow> Fpow A \<subseteq> Fpow B" 2238unfolding Fpow_def by auto 2239 2240lemma empty_in_Fpow: "{} \<in> Fpow A" 2241unfolding Fpow_def by auto 2242 2243lemma Fpow_not_empty: "Fpow A \<noteq> {}" 2244using empty_in_Fpow by blast 2245 2246lemma Fpow_subset_Pow: "Fpow A \<subseteq> Pow A" 2247unfolding Fpow_def by auto 2248 2249lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}" 2250unfolding Fpow_def Pow_def by blast 2251 2252lemma inj_on_image_Fpow: 2253 assumes "inj_on f A" 2254 shows "inj_on (image f) (Fpow A)" 2255 using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"] 2256 inj_on_image_Pow by blast 2257 2258lemma image_Fpow_mono: 2259 assumes "f ` A \<subseteq> B" 2260 shows "(image f) ` (Fpow A) \<subseteq> Fpow B" 2261 using assms by(unfold Fpow_def, auto) 2262 2263end 2264