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