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