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