src/HOL/Finite_Set.thy
 author kleing Wed Apr 14 14:13:05 2004 +0200 (2004-04-14) changeset 14565 c6dc17aab88a parent 14504 7a3d80e276d4 child 14661 9ead82084de8 permissions -rw-r--r--
use more symbols in HTML output
```     1 (*  Title:      HOL/Finite_Set.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
```
```     4                 Additions by Jeremy Avigad in Feb 2004
```
```     5     License:    GPL (GNU GENERAL PUBLIC LICENSE)
```
```     6 *)
```
```     7
```
```     8 header {* Finite sets *}
```
```     9
```
```    10 theory Finite_Set = Divides + Power + Inductive:
```
```    11
```
```    12 subsection {* Collection of finite sets *}
```
```    13
```
```    14 consts Finites :: "'a set set"
```
```    15 syntax
```
```    16   finite :: "'a set => bool"
```
```    17 translations
```
```    18   "finite A" == "A : Finites"
```
```    19
```
```    20 inductive Finites
```
```    21   intros
```
```    22     emptyI [simp, intro!]: "{} : Finites"
```
```    23     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
```
```    24
```
```    25 axclass finite \<subseteq> type
```
```    26   finite: "finite UNIV"
```
```    27
```
```    28 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
```
```    29  "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
```
```    30 by(subgoal_tac "A \<noteq> UNIV", blast, blast)
```
```    31
```
```    32
```
```    33 lemma finite_induct [case_names empty insert, induct set: Finites]:
```
```    34   "finite F ==>
```
```    35     P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
```
```    36   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
```
```    37 proof -
```
```    38   assume "P {}" and
```
```    39     insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
```
```    40   assume "finite F"
```
```    41   thus "P F"
```
```    42   proof induct
```
```    43     show "P {}" .
```
```    44     fix F x assume F: "finite F" and P: "P F"
```
```    45     show "P (insert x F)"
```
```    46     proof cases
```
```    47       assume "x \<in> F"
```
```    48       hence "insert x F = F" by (rule insert_absorb)
```
```    49       with P show ?thesis by (simp only:)
```
```    50     next
```
```    51       assume "x \<notin> F"
```
```    52       from F this P show ?thesis by (rule insert)
```
```    53     qed
```
```    54   qed
```
```    55 qed
```
```    56
```
```    57 lemma finite_subset_induct [consumes 2, case_names empty insert]:
```
```    58   "finite F ==> F \<subseteq> A ==>
```
```    59     P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
```
```    60     P F"
```
```    61 proof -
```
```    62   assume "P {}" and insert:
```
```    63     "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
```
```    64   assume "finite F"
```
```    65   thus "F \<subseteq> A ==> P F"
```
```    66   proof induct
```
```    67     show "P {}" .
```
```    68     fix F x assume "finite F" and "x \<notin> F"
```
```    69       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
```
```    70     show "P (insert x F)"
```
```    71     proof (rule insert)
```
```    72       from i show "x \<in> A" by blast
```
```    73       from i have "F \<subseteq> A" by blast
```
```    74       with P show "P F" .
```
```    75     qed
```
```    76   qed
```
```    77 qed
```
```    78
```
```    79 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
```
```    80   -- {* The union of two finite sets is finite. *}
```
```    81   by (induct set: Finites) simp_all
```
```    82
```
```    83 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
```
```    84   -- {* Every subset of a finite set is finite. *}
```
```    85 proof -
```
```    86   assume "finite B"
```
```    87   thus "!!A. A \<subseteq> B ==> finite A"
```
```    88   proof induct
```
```    89     case empty
```
```    90     thus ?case by simp
```
```    91   next
```
```    92     case (insert F x A)
```
```    93     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
```
```    94     show "finite A"
```
```    95     proof cases
```
```    96       assume x: "x \<in> A"
```
```    97       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
```
```    98       with r have "finite (A - {x})" .
```
```    99       hence "finite (insert x (A - {x}))" ..
```
```   100       also have "insert x (A - {x}) = A" by (rule insert_Diff)
```
```   101       finally show ?thesis .
```
```   102     next
```
```   103       show "A \<subseteq> F ==> ?thesis" .
```
```   104       assume "x \<notin> A"
```
```   105       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
```
```   106     qed
```
```   107   qed
```
```   108 qed
```
```   109
```
```   110 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
```
```   111   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
```
```   112
```
```   113 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
```
```   114   -- {* The converse obviously fails. *}
```
```   115   by (blast intro: finite_subset)
```
```   116
```
```   117 lemma finite_insert [simp]: "finite (insert a A) = finite A"
```
```   118   apply (subst insert_is_Un)
```
```   119   apply (simp only: finite_Un, blast)
```
```   120   done
```
```   121
```
```   122 lemma finite_empty_induct:
```
```   123   "finite A ==>
```
```   124   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
```
```   125 proof -
```
```   126   assume "finite A"
```
```   127     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
```
```   128   have "P (A - A)"
```
```   129   proof -
```
```   130     fix c b :: "'a set"
```
```   131     presume c: "finite c" and b: "finite b"
```
```   132       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
```
```   133     from c show "c \<subseteq> b ==> P (b - c)"
```
```   134     proof induct
```
```   135       case empty
```
```   136       from P1 show ?case by simp
```
```   137     next
```
```   138       case (insert F x)
```
```   139       have "P (b - F - {x})"
```
```   140       proof (rule P2)
```
```   141         from _ b show "finite (b - F)" by (rule finite_subset) blast
```
```   142         from insert show "x \<in> b - F" by simp
```
```   143         from insert show "P (b - F)" by simp
```
```   144       qed
```
```   145       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
```
```   146       finally show ?case .
```
```   147     qed
```
```   148   next
```
```   149     show "A \<subseteq> A" ..
```
```   150   qed
```
```   151   thus "P {}" by simp
```
```   152 qed
```
```   153
```
```   154 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
```
```   155   by (rule Diff_subset [THEN finite_subset])
```
```   156
```
```   157 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
```
```   158   apply (subst Diff_insert)
```
```   159   apply (case_tac "a : A - B")
```
```   160    apply (rule finite_insert [symmetric, THEN trans])
```
```   161    apply (subst insert_Diff, simp_all)
```
```   162   done
```
```   163
```
```   164
```
```   165 subsubsection {* Image and Inverse Image over Finite Sets *}
```
```   166
```
```   167 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
```
```   168   -- {* The image of a finite set is finite. *}
```
```   169   by (induct set: Finites) simp_all
```
```   170
```
```   171 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
```
```   172   apply (frule finite_imageI)
```
```   173   apply (erule finite_subset, assumption)
```
```   174   done
```
```   175
```
```   176 lemma finite_range_imageI:
```
```   177     "finite (range g) ==> finite (range (%x. f (g x)))"
```
```   178   apply (drule finite_imageI, simp)
```
```   179   done
```
```   180
```
```   181 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
```
```   182 proof -
```
```   183   have aux: "!!A. finite (A - {}) = finite A" by simp
```
```   184   fix B :: "'a set"
```
```   185   assume "finite B"
```
```   186   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
```
```   187     apply induct
```
```   188      apply simp
```
```   189     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
```
```   190      apply clarify
```
```   191      apply (simp (no_asm_use) add: inj_on_def)
```
```   192      apply (blast dest!: aux [THEN iffD1], atomize)
```
```   193     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
```
```   194     apply (frule subsetD [OF equalityD2 insertI1], clarify)
```
```   195     apply (rule_tac x = xa in bexI)
```
```   196      apply (simp_all add: inj_on_image_set_diff)
```
```   197     done
```
```   198 qed (rule refl)
```
```   199
```
```   200
```
```   201 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
```
```   202   -- {* The inverse image of a singleton under an injective function
```
```   203          is included in a singleton. *}
```
```   204   apply (auto simp add: inj_on_def)
```
```   205   apply (blast intro: the_equality [symmetric])
```
```   206   done
```
```   207
```
```   208 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
```
```   209   -- {* The inverse image of a finite set under an injective function
```
```   210          is finite. *}
```
```   211   apply (induct set: Finites, simp_all)
```
```   212   apply (subst vimage_insert)
```
```   213   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
```
```   214   done
```
```   215
```
```   216
```
```   217 subsubsection {* The finite UNION of finite sets *}
```
```   218
```
```   219 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
```
```   220   by (induct set: Finites) simp_all
```
```   221
```
```   222 text {*
```
```   223   Strengthen RHS to
```
```   224   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
```
```   225
```
```   226   We'd need to prove
```
```   227   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
```
```   228   by induction. *}
```
```   229
```
```   230 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
```
```   231   by (blast intro: finite_UN_I finite_subset)
```
```   232
```
```   233
```
```   234 subsubsection {* Sigma of finite sets *}
```
```   235
```
```   236 lemma finite_SigmaI [simp]:
```
```   237     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
```
```   238   by (unfold Sigma_def) (blast intro!: finite_UN_I)
```
```   239
```
```   240 lemma finite_Prod_UNIV:
```
```   241     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
```
```   242   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
```
```   243    apply (erule ssubst)
```
```   244    apply (erule finite_SigmaI, auto)
```
```   245   done
```
```   246
```
```   247 instance unit :: finite
```
```   248 proof
```
```   249   have "finite {()}" by simp
```
```   250   also have "{()} = UNIV" by auto
```
```   251   finally show "finite (UNIV :: unit set)" .
```
```   252 qed
```
```   253
```
```   254 instance * :: (finite, finite) finite
```
```   255 proof
```
```   256   show "finite (UNIV :: ('a \<times> 'b) set)"
```
```   257   proof (rule finite_Prod_UNIV)
```
```   258     show "finite (UNIV :: 'a set)" by (rule finite)
```
```   259     show "finite (UNIV :: 'b set)" by (rule finite)
```
```   260   qed
```
```   261 qed
```
```   262
```
```   263
```
```   264 subsubsection {* The powerset of a finite set *}
```
```   265
```
```   266 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
```
```   267 proof
```
```   268   assume "finite (Pow A)"
```
```   269   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
```
```   270   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
```
```   271 next
```
```   272   assume "finite A"
```
```   273   thus "finite (Pow A)"
```
```   274     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
```
```   275 qed
```
```   276
```
```   277 lemma finite_converse [iff]: "finite (r^-1) = finite r"
```
```   278   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
```
```   279    apply simp
```
```   280    apply (rule iffI)
```
```   281     apply (erule finite_imageD [unfolded inj_on_def])
```
```   282     apply (simp split add: split_split)
```
```   283    apply (erule finite_imageI)
```
```   284   apply (simp add: converse_def image_def, auto)
```
```   285   apply (rule bexI)
```
```   286    prefer 2 apply assumption
```
```   287   apply simp
```
```   288   done
```
```   289
```
```   290
```
```   291 subsubsection {* Finiteness of transitive closure *}
```
```   292
```
```   293 text {* (Thanks to Sidi Ehmety) *}
```
```   294
```
```   295 lemma finite_Field: "finite r ==> finite (Field r)"
```
```   296   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
```
```   297   apply (induct set: Finites)
```
```   298    apply (auto simp add: Field_def Domain_insert Range_insert)
```
```   299   done
```
```   300
```
```   301 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
```
```   302   apply clarify
```
```   303   apply (erule trancl_induct)
```
```   304    apply (auto simp add: Field_def)
```
```   305   done
```
```   306
```
```   307 lemma finite_trancl: "finite (r^+) = finite r"
```
```   308   apply auto
```
```   309    prefer 2
```
```   310    apply (rule trancl_subset_Field2 [THEN finite_subset])
```
```   311    apply (rule finite_SigmaI)
```
```   312     prefer 3
```
```   313     apply (blast intro: r_into_trancl' finite_subset)
```
```   314    apply (auto simp add: finite_Field)
```
```   315   done
```
```   316
```
```   317 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
```
```   318     finite (A <*> B)"
```
```   319   by (rule finite_SigmaI)
```
```   320
```
```   321
```
```   322 subsection {* Finite cardinality *}
```
```   323
```
```   324 text {*
```
```   325   This definition, although traditional, is ugly to work with: @{text
```
```   326   "card A == LEAST n. EX f. A = {f i | i. i < n}"}.  Therefore we have
```
```   327   switched to an inductive one:
```
```   328 *}
```
```   329
```
```   330 consts cardR :: "('a set \<times> nat) set"
```
```   331
```
```   332 inductive cardR
```
```   333   intros
```
```   334     EmptyI: "({}, 0) : cardR"
```
```   335     InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
```
```   336
```
```   337 constdefs
```
```   338   card :: "'a set => nat"
```
```   339   "card A == THE n. (A, n) : cardR"
```
```   340
```
```   341 inductive_cases cardR_emptyE: "({}, n) : cardR"
```
```   342 inductive_cases cardR_insertE: "(insert a A,n) : cardR"
```
```   343
```
```   344 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
```
```   345   by (induct set: cardR) simp_all
```
```   346
```
```   347 lemma cardR_determ_aux1:
```
```   348     "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
```
```   349   apply (induct set: cardR, auto)
```
```   350   apply (simp add: insert_Diff_if, auto)
```
```   351   apply (drule cardR_SucD)
```
```   352   apply (blast intro!: cardR.intros)
```
```   353   done
```
```   354
```
```   355 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
```
```   356   by (drule cardR_determ_aux1) auto
```
```   357
```
```   358 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
```
```   359   apply (induct set: cardR)
```
```   360    apply (safe elim!: cardR_emptyE cardR_insertE)
```
```   361   apply (rename_tac B b m)
```
```   362   apply (case_tac "a = b")
```
```   363    apply (subgoal_tac "A = B")
```
```   364     prefer 2 apply (blast elim: equalityE, blast)
```
```   365   apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
```
```   366    prefer 2
```
```   367    apply (rule_tac x = "A Int B" in exI)
```
```   368    apply (blast elim: equalityE)
```
```   369   apply (frule_tac A = B in cardR_SucD)
```
```   370   apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
```
```   371   done
```
```   372
```
```   373 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
```
```   374   by (induct set: cardR) simp_all
```
```   375
```
```   376 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
```
```   377   by (induct set: Finites) (auto intro!: cardR.intros)
```
```   378
```
```   379 lemma card_equality: "(A,n) : cardR ==> card A = n"
```
```   380   by (unfold card_def) (blast intro: cardR_determ)
```
```   381
```
```   382 lemma card_empty [simp]: "card {} = 0"
```
```   383   by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
```
```   384
```
```   385 lemma card_insert_disjoint [simp]:
```
```   386   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
```
```   387 proof -
```
```   388   assume x: "x \<notin> A"
```
```   389   hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
```
```   390     apply (auto intro!: cardR.intros)
```
```   391     apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
```
```   392      apply (force dest: cardR_imp_finite)
```
```   393     apply (blast intro!: cardR.intros intro: cardR_determ)
```
```   394     done
```
```   395   assume "finite A"
```
```   396   thus ?thesis
```
```   397     apply (simp add: card_def aux)
```
```   398     apply (rule the_equality)
```
```   399      apply (auto intro: finite_imp_cardR
```
```   400        cong: conj_cong simp: card_def [symmetric] card_equality)
```
```   401     done
```
```   402 qed
```
```   403
```
```   404 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
```
```   405   apply auto
```
```   406   apply (drule_tac a = x in mk_disjoint_insert, clarify)
```
```   407   apply (rotate_tac -1, auto)
```
```   408   done
```
```   409
```
```   410 lemma card_insert_if:
```
```   411     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
```
```   412   by (simp add: insert_absorb)
```
```   413
```
```   414 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
```
```   415 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
```
```   416 apply(simp del:insert_Diff_single)
```
```   417 done
```
```   418
```
```   419 lemma card_Diff_singleton:
```
```   420     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
```
```   421   by (simp add: card_Suc_Diff1 [symmetric])
```
```   422
```
```   423 lemma card_Diff_singleton_if:
```
```   424     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
```
```   425   by (simp add: card_Diff_singleton)
```
```   426
```
```   427 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
```
```   428   by (simp add: card_insert_if card_Suc_Diff1)
```
```   429
```
```   430 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
```
```   431   by (simp add: card_insert_if)
```
```   432
```
```   433 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
```
```   434   apply (induct set: Finites, simp, clarify)
```
```   435   apply (subgoal_tac "finite A & A - {x} <= F")
```
```   436    prefer 2 apply (blast intro: finite_subset, atomize)
```
```   437   apply (drule_tac x = "A - {x}" in spec)
```
```   438   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
```
```   439   apply (case_tac "card A", auto)
```
```   440   done
```
```   441
```
```   442 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
```
```   443   apply (simp add: psubset_def linorder_not_le [symmetric])
```
```   444   apply (blast dest: card_seteq)
```
```   445   done
```
```   446
```
```   447 lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
```
```   448   apply (case_tac "A = B", simp)
```
```   449   apply (simp add: linorder_not_less [symmetric])
```
```   450   apply (blast dest: card_seteq intro: order_less_imp_le)
```
```   451   done
```
```   452
```
```   453 lemma card_Un_Int: "finite A ==> finite B
```
```   454     ==> card A + card B = card (A Un B) + card (A Int B)"
```
```   455   apply (induct set: Finites, simp)
```
```   456   apply (simp add: insert_absorb Int_insert_left)
```
```   457   done
```
```   458
```
```   459 lemma card_Un_disjoint: "finite A ==> finite B
```
```   460     ==> A Int B = {} ==> card (A Un B) = card A + card B"
```
```   461   by (simp add: card_Un_Int)
```
```   462
```
```   463 lemma card_Diff_subset:
```
```   464     "finite A ==> B <= A ==> card A - card B = card (A - B)"
```
```   465   apply (subgoal_tac "(A - B) Un B = A")
```
```   466    prefer 2 apply blast
```
```   467   apply (rule nat_add_right_cancel [THEN iffD1])
```
```   468   apply (rule card_Un_disjoint [THEN subst])
```
```   469      apply (erule_tac [4] ssubst)
```
```   470      prefer 3 apply blast
```
```   471     apply (simp_all add: add_commute not_less_iff_le
```
```   472       add_diff_inverse card_mono finite_subset)
```
```   473   done
```
```   474
```
```   475 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
```
```   476   apply (rule Suc_less_SucD)
```
```   477   apply (simp add: card_Suc_Diff1)
```
```   478   done
```
```   479
```
```   480 lemma card_Diff2_less:
```
```   481     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
```
```   482   apply (case_tac "x = y")
```
```   483    apply (simp add: card_Diff1_less)
```
```   484   apply (rule less_trans)
```
```   485    prefer 2 apply (auto intro!: card_Diff1_less)
```
```   486   done
```
```   487
```
```   488 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
```
```   489   apply (case_tac "x : A")
```
```   490    apply (simp_all add: card_Diff1_less less_imp_le)
```
```   491   done
```
```   492
```
```   493 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
```
```   494 by (erule psubsetI, blast)
```
```   495
```
```   496
```
```   497 subsubsection {* Cardinality of image *}
```
```   498
```
```   499 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
```
```   500   apply (induct set: Finites, simp)
```
```   501   apply (simp add: le_SucI finite_imageI card_insert_if)
```
```   502   done
```
```   503
```
```   504 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
```
```   505   apply (induct set: Finites, simp_all, atomize, safe)
```
```   506    apply (unfold inj_on_def, blast)
```
```   507   apply (subst card_insert_disjoint)
```
```   508     apply (erule finite_imageI, blast, blast)
```
```   509   done
```
```   510
```
```   511 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
```
```   512   by (simp add: card_seteq card_image)
```
```   513
```
```   514
```
```   515 subsubsection {* Cardinality of the Powerset *}
```
```   516
```
```   517 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
```
```   518   apply (induct set: Finites)
```
```   519    apply (simp_all add: Pow_insert)
```
```   520   apply (subst card_Un_disjoint, blast)
```
```   521     apply (blast intro: finite_imageI, blast)
```
```   522   apply (subgoal_tac "inj_on (insert x) (Pow F)")
```
```   523    apply (simp add: card_image Pow_insert)
```
```   524   apply (unfold inj_on_def)
```
```   525   apply (blast elim!: equalityE)
```
```   526   done
```
```   527
```
```   528 text {*
```
```   529   \medskip Relates to equivalence classes.  Based on a theorem of
```
```   530   F. Kammüller's.  The @{prop "finite C"} premise is redundant.
```
```   531 *}
```
```   532
```
```   533 lemma dvd_partition:
```
```   534   "finite C ==> finite (Union C) ==>
```
```   535     ALL c : C. k dvd card c ==>
```
```   536     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
```
```   537   k dvd card (Union C)"
```
```   538   apply (induct set: Finites, simp_all, clarify)
```
```   539   apply (subst card_Un_disjoint)
```
```   540   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
```
```   541   done
```
```   542
```
```   543
```
```   544 subsection {* A fold functional for finite sets *}
```
```   545
```
```   546 text {*
```
```   547   For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
```
```   548   f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
```
```   549 *}
```
```   550
```
```   551 consts
```
```   552   foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
```
```   553
```
```   554 inductive "foldSet f e"
```
```   555   intros
```
```   556     emptyI [intro]: "({}, e) : foldSet f e"
```
```   557     insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
```
```   558
```
```   559 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
```
```   560
```
```   561 constdefs
```
```   562   fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
```
```   563   "fold f e A == THE x. (A, x) : foldSet f e"
```
```   564
```
```   565 lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
```
```   566 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
```
```   567
```
```   568 lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
```
```   569   by (induct set: foldSet) auto
```
```   570
```
```   571 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
```
```   572   by (induct set: Finites) auto
```
```   573
```
```   574
```
```   575 subsubsection {* Left-commutative operations *}
```
```   576
```
```   577 locale LC =
```
```   578   fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
```
```   579   assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
```
```   580
```
```   581 lemma (in LC) foldSet_determ_aux:
```
```   582   "ALL A x. card A < n --> (A, x) : foldSet f e -->
```
```   583     (ALL y. (A, y) : foldSet f e --> y = x)"
```
```   584   apply (induct n)
```
```   585    apply (auto simp add: less_Suc_eq)
```
```   586   apply (erule foldSet.cases, blast)
```
```   587   apply (erule foldSet.cases, blast, clarify)
```
```   588   txt {* force simplification of @{text "card A < card (insert ...)"}. *}
```
```   589   apply (erule rev_mp)
```
```   590   apply (simp add: less_Suc_eq_le)
```
```   591   apply (rule impI)
```
```   592   apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
```
```   593    apply (subgoal_tac "Aa = Ab")
```
```   594     prefer 2 apply (blast elim!: equalityE, blast)
```
```   595   txt {* case @{prop "xa \<notin> xb"}. *}
```
```   596   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
```
```   597    prefer 2 apply (blast elim!: equalityE, clarify)
```
```   598   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
```
```   599    prefer 2 apply blast
```
```   600   apply (subgoal_tac "card Aa <= card Ab")
```
```   601    prefer 2
```
```   602    apply (rule Suc_le_mono [THEN subst])
```
```   603    apply (simp add: card_Suc_Diff1)
```
```   604   apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
```
```   605   apply (blast intro: foldSet_imp_finite finite_Diff)
```
```   606   apply (frule (1) Diff1_foldSet)
```
```   607   apply (subgoal_tac "ya = f xb x")
```
```   608    prefer 2 apply (blast del: equalityCE)
```
```   609   apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
```
```   610    prefer 2 apply simp
```
```   611   apply (subgoal_tac "yb = f xa x")
```
```   612    prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
```
```   613   apply (simp (no_asm_simp) add: left_commute)
```
```   614   done
```
```   615
```
```   616 lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
```
```   617   by (blast intro: foldSet_determ_aux [rule_format])
```
```   618
```
```   619 lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
```
```   620   by (unfold fold_def) (blast intro: foldSet_determ)
```
```   621
```
```   622 lemma fold_empty [simp]: "fold f e {} = e"
```
```   623   by (unfold fold_def) blast
```
```   624
```
```   625 lemma (in LC) fold_insert_aux: "x \<notin> A ==>
```
```   626     ((insert x A, v) : foldSet f e) =
```
```   627     (EX y. (A, y) : foldSet f e & v = f x y)"
```
```   628   apply auto
```
```   629   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
```
```   630    apply (fastsimp dest: foldSet_imp_finite)
```
```   631   apply (blast intro: foldSet_determ)
```
```   632   done
```
```   633
```
```   634 lemma (in LC) fold_insert:
```
```   635     "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
```
```   636   apply (unfold fold_def)
```
```   637   apply (simp add: fold_insert_aux)
```
```   638   apply (rule the_equality)
```
```   639   apply (auto intro: finite_imp_foldSet
```
```   640     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
```
```   641   done
```
```   642
```
```   643 lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
```
```   644   apply (induct set: Finites, simp)
```
```   645   apply (simp add: left_commute fold_insert)
```
```   646   done
```
```   647
```
```   648 lemma (in LC) fold_nest_Un_Int:
```
```   649   "finite A ==> finite B
```
```   650     ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
```
```   651   apply (induct set: Finites, simp)
```
```   652   apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
```
```   653   done
```
```   654
```
```   655 lemma (in LC) fold_nest_Un_disjoint:
```
```   656   "finite A ==> finite B ==> A Int B = {}
```
```   657     ==> fold f e (A Un B) = fold f (fold f e B) A"
```
```   658   by (simp add: fold_nest_Un_Int)
```
```   659
```
```   660 declare foldSet_imp_finite [simp del]
```
```   661     empty_foldSetE [rule del]  foldSet.intros [rule del]
```
```   662   -- {* Delete rules to do with @{text foldSet} relation. *}
```
```   663
```
```   664
```
```   665
```
```   666 subsubsection {* Commutative monoids *}
```
```   667
```
```   668 text {*
```
```   669   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
```
```   670   instead of @{text "'b => 'a => 'a"}.
```
```   671 *}
```
```   672
```
```   673 locale ACe =
```
```   674   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
```
```   675     and e :: 'a
```
```   676   assumes ident [simp]: "x \<cdot> e = x"
```
```   677     and commute: "x \<cdot> y = y \<cdot> x"
```
```   678     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
```
```   679
```
```   680 lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
```
```   681 proof -
```
```   682   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
```
```   683   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
```
```   684   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
```
```   685   finally show ?thesis .
```
```   686 qed
```
```   687
```
```   688 lemmas (in ACe) AC = assoc commute left_commute
```
```   689
```
```   690 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
```
```   691 proof -
```
```   692   have "x \<cdot> e = x" by (rule ident)
```
```   693   thus ?thesis by (subst commute)
```
```   694 qed
```
```   695
```
```   696 lemma (in ACe) fold_Un_Int:
```
```   697   "finite A ==> finite B ==>
```
```   698     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
```
```   699   apply (induct set: Finites, simp)
```
```   700   apply (simp add: AC insert_absorb Int_insert_left
```
```   701     LC.fold_insert [OF LC.intro])
```
```   702   done
```
```   703
```
```   704 lemma (in ACe) fold_Un_disjoint:
```
```   705   "finite A ==> finite B ==> A Int B = {} ==>
```
```   706     fold f e (A Un B) = fold f e A \<cdot> fold f e B"
```
```   707   by (simp add: fold_Un_Int)
```
```   708
```
```   709 lemma (in ACe) fold_Un_disjoint2:
```
```   710   "finite A ==> finite B ==> A Int B = {} ==>
```
```   711     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
```
```   712 proof -
```
```   713   assume b: "finite B"
```
```   714   assume "finite A"
```
```   715   thus "A Int B = {} ==>
```
```   716     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
```
```   717   proof induct
```
```   718     case empty
```
```   719     thus ?case by simp
```
```   720   next
```
```   721     case (insert F x)
```
```   722     have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
```
```   723       by simp
```
```   724     also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
```
```   725       by (rule LC.fold_insert [OF LC.intro])
```
```   726         (insert b insert, auto simp add: left_commute)
```
```   727     also from insert have "fold (f o g) e (F \<union> B) =
```
```   728       fold (f o g) e F \<cdot> fold (f o g) e B" by blast
```
```   729     also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
```
```   730       by (simp add: AC)
```
```   731     also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
```
```   732       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
```
```   733 	auto simp add: left_commute)
```
```   734     finally show ?case .
```
```   735   qed
```
```   736 qed
```
```   737
```
```   738
```
```   739 subsection {* Generalized summation over a set *}
```
```   740
```
```   741 constdefs
```
```   742   setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
```
```   743   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
```
```   744
```
```   745 syntax
```
```   746   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
```
```   747 syntax (xsymbols)
```
```   748   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
```
```   749 syntax (HTML output)
```
```   750   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
```
```   751 translations
```
```   752   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
```
```   753
```
```   754
```
```   755 lemma setsum_empty [simp]: "setsum f {} = 0"
```
```   756   by (simp add: setsum_def)
```
```   757
```
```   758 lemma setsum_insert [simp]:
```
```   759     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
```
```   760   by (simp add: setsum_def
```
```   761     LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
```
```   762
```
```   763 lemma setsum_reindex [rule_format]: "finite B ==>
```
```   764                   inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
```
```   765 apply (rule finite_induct, assumption, force)
```
```   766 apply (rule impI, auto)
```
```   767 apply (simp add: inj_on_def)
```
```   768 apply (subgoal_tac "f x \<notin> f ` F")
```
```   769 apply (subgoal_tac "finite (f ` F)")
```
```   770 apply (auto simp add: setsum_insert)
```
```   771 apply (simp add: inj_on_def)
```
```   772   done
```
```   773
```
```   774 lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
```
```   775     setsum f B = setsum id (f ` B)"
```
```   776 by (auto simp add: setsum_reindex id_o)
```
```   777
```
```   778 lemma setsum_reindex_cong: "finite A ==> inj_on f A ==>
```
```   779     B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
```
```   780   by (frule setsum_reindex, assumption, simp)
```
```   781
```
```   782 lemma setsum_cong:
```
```   783   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
```
```   784   apply (case_tac "finite B")
```
```   785    prefer 2 apply (simp add: setsum_def, simp)
```
```   786   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
```
```   787    apply simp
```
```   788   apply (erule finite_induct, simp)
```
```   789   apply (simp add: subset_insert_iff, clarify)
```
```   790   apply (subgoal_tac "finite C")
```
```   791    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```   792   apply (subgoal_tac "C = insert x (C - {x})")
```
```   793    prefer 2 apply blast
```
```   794   apply (erule ssubst)
```
```   795   apply (drule spec)
```
```   796   apply (erule (1) notE impE)
```
```   797   apply (simp add: Ball_def del:insert_Diff_single)
```
```   798   done
```
```   799
```
```   800 lemma setsum_0: "setsum (%i. 0) A = 0"
```
```   801   apply (case_tac "finite A")
```
```   802    prefer 2 apply (simp add: setsum_def)
```
```   803   apply (erule finite_induct, auto)
```
```   804   done
```
```   805
```
```   806 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
```
```   807   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
```
```   808   apply (erule ssubst, rule setsum_0)
```
```   809   apply (rule setsum_cong, auto)
```
```   810   done
```
```   811
```
```   812 lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
```
```   813   -- {* Could allow many @{text "card"} proofs to be simplified. *}
```
```   814   by (induct set: Finites) auto
```
```   815
```
```   816 lemma setsum_Un_Int: "finite A ==> finite B
```
```   817     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
```
```   818   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
```
```   819   apply (induct set: Finites, simp)
```
```   820   apply (simp add: plus_ac0 Int_insert_left insert_absorb)
```
```   821   done
```
```   822
```
```   823 lemma setsum_Un_disjoint: "finite A ==> finite B
```
```   824   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
```
```   825   apply (subst setsum_Un_Int [symmetric], auto)
```
```   826   done
```
```   827
```
```   828 lemma setsum_UN_disjoint:
```
```   829     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```   830         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```   831       setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
```
```   832   apply (induct set: Finites, simp, atomize)
```
```   833   apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```   834    prefer 2 apply blast
```
```   835   apply (subgoal_tac "A x Int UNION F A = {}")
```
```   836    prefer 2 apply blast
```
```   837   apply (simp add: setsum_Un_disjoint)
```
```   838   done
```
```   839
```
```   840 lemma setsum_Union_disjoint:
```
```   841   "finite C ==> (ALL A:C. finite A) ==>
```
```   842         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```   843       setsum f (Union C) = setsum (setsum f) C"
```
```   844   apply (frule setsum_UN_disjoint [of C id f])
```
```   845   apply (unfold Union_def id_def, assumption+)
```
```   846   done
```
```   847
```
```   848 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   849     (\<Sum> x:A. (\<Sum> y:B x. f x y)) =
```
```   850     (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
```
```   851   apply (subst Sigma_def)
```
```   852   apply (subst setsum_UN_disjoint)
```
```   853   apply assumption
```
```   854   apply (rule ballI)
```
```   855   apply (drule_tac x = i in bspec, assumption)
```
```   856   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
```
```   857   apply (rule finite_surj)
```
```   858   apply auto
```
```   859   apply (rule setsum_cong, rule refl)
```
```   860   apply (subst setsum_UN_disjoint)
```
```   861   apply (erule bspec, assumption)
```
```   862   apply auto
```
```   863   done
```
```   864
```
```   865 lemma setsum_cartesian_product: "finite A ==> finite B ==>
```
```   866     (\<Sum> x:A. (\<Sum> y:B. f x y)) =
```
```   867     (\<Sum> z:A <*> B. f (fst z) (snd z))"
```
```   868   by (erule setsum_Sigma, auto);
```
```   869
```
```   870 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
```
```   871   apply (case_tac "finite A")
```
```   872    prefer 2 apply (simp add: setsum_def)
```
```   873   apply (erule finite_induct, auto)
```
```   874   apply (simp add: plus_ac0)
```
```   875   done
```
```   876
```
```   877 subsubsection {* Properties in more restricted classes of structures *}
```
```   878
```
```   879 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
```
```   880   apply (case_tac "finite A")
```
```   881    prefer 2 apply (simp add: setsum_def)
```
```   882   apply (erule rev_mp)
```
```   883   apply (erule finite_induct, auto)
```
```   884   done
```
```   885
```
```   886 lemma setsum_eq_0_iff [simp]:
```
```   887     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
```
```   888   by (induct set: Finites) auto
```
```   889
```
```   890 lemma setsum_constant_nat [simp]:
```
```   891     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
```
```   892   -- {* Later generalized to any semiring. *}
```
```   893   by (erule finite_induct, auto)
```
```   894
```
```   895 lemma setsum_Un: "finite A ==> finite B ==>
```
```   896     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
```
```   897   -- {* For the natural numbers, we have subtraction. *}
```
```   898   by (subst setsum_Un_Int [symmetric], auto)
```
```   899
```
```   900 lemma setsum_Un_ring: "finite A ==> finite B ==>
```
```   901     (setsum f (A Un B) :: 'a :: ring) =
```
```   902       setsum f A + setsum f B - setsum f (A Int B)"
```
```   903   by (subst setsum_Un_Int [symmetric], auto)
```
```   904
```
```   905 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
```
```   906     (if a:A then setsum f A - f a else setsum f A)"
```
```   907   apply (case_tac "finite A")
```
```   908    prefer 2 apply (simp add: setsum_def)
```
```   909   apply (erule finite_induct)
```
```   910    apply (auto simp add: insert_Diff_if)
```
```   911   apply (drule_tac a = a in mk_disjoint_insert, auto)
```
```   912   done
```
```   913
```
```   914 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
```
```   915   - setsum f A"
```
```   916   by (induct set: Finites, auto)
```
```   917
```
```   918 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
```
```   919   setsum f A - setsum g A"
```
```   920   by (simp add: diff_minus setsum_addf setsum_negf)
```
```   921
```
```   922 lemma setsum_nonneg: "[| finite A;
```
```   923     \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
```
```   924     0 \<le>  setsum f A";
```
```   925   apply (induct set: Finites, auto)
```
```   926   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
```
```   927   apply (blast intro: add_mono)
```
```   928   done
```
```   929
```
```   930 subsubsection {* Cardinality of unions and Sigma sets *}
```
```   931
```
```   932 lemma card_UN_disjoint:
```
```   933     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```   934         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```   935       card (UNION I A) = setsum (%i. card (A i)) I"
```
```   936   apply (subst card_eq_setsum)
```
```   937   apply (subst finite_UN, assumption+)
```
```   938   apply (subgoal_tac "setsum (%i. card (A i)) I =
```
```   939       setsum (%i. (setsum (%x. 1) (A i))) I")
```
```   940   apply (erule ssubst)
```
```   941   apply (erule setsum_UN_disjoint, assumption+)
```
```   942   apply (rule setsum_cong)
```
```   943   apply simp+
```
```   944   done
```
```   945
```
```   946 lemma card_Union_disjoint:
```
```   947   "finite C ==> (ALL A:C. finite A) ==>
```
```   948         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```   949       card (Union C) = setsum card C"
```
```   950   apply (frule card_UN_disjoint [of C id])
```
```   951   apply (unfold Union_def id_def, assumption+)
```
```   952   done
```
```   953
```
```   954 lemma SigmaI_insert: "y \<notin> A ==>
```
```   955   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
```
```   956   by auto
```
```   957
```
```   958 lemma card_cartesian_product_singleton: "finite A ==>
```
```   959     card({x} <*> A) = card(A)"
```
```   960   apply (subgoal_tac "inj_on (%y .(x,y)) A")
```
```   961   apply (frule card_image, assumption)
```
```   962   apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
```
```   963   apply (auto simp add: inj_on_def)
```
```   964   done
```
```   965
```
```   966 lemma card_SigmaI [rule_format,simp]: "finite A ==>
```
```   967   (ALL a:A. finite (B a)) -->
```
```   968   card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
```
```   969   apply (erule finite_induct, auto)
```
```   970   apply (subst SigmaI_insert, assumption)
```
```   971   apply (subst card_Un_disjoint)
```
```   972   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
```
```   973   done
```
```   974
```
```   975 lemma card_cartesian_product: "[| finite A; finite B |] ==>
```
```   976   card (A <*> B) = card(A) * card(B)"
```
```   977   by simp
```
```   978
```
```   979
```
```   980 subsection {* Generalized product over a set *}
```
```   981
```
```   982 constdefs
```
```   983   setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
```
```   984   "setprod f A == if finite A then fold (op * o f) 1 A else 1"
```
```   985
```
```   986 syntax
```
```   987   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
```
```   988                 ("\<Prod>_:_. _" [0, 51, 10] 10)
```
```   989
```
```   990 syntax (xsymbols)
```
```   991   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
```
```   992                 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
```
```   993 syntax (HTML output)
```
```   994   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
```
```   995                 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
```
```   996 translations
```
```   997   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
```
```   998
```
```   999
```
```  1000 lemma setprod_empty [simp]: "setprod f {} = 1"
```
```  1001   by (auto simp add: setprod_def)
```
```  1002
```
```  1003 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
```
```  1004     setprod f (insert a A) = f a * setprod f A"
```
```  1005   by (auto simp add: setprod_def LC_def LC.fold_insert
```
```  1006       times_ac1_left_commute)
```
```  1007
```
```  1008 lemma setprod_reindex [rule_format]: "finite B ==>
```
```  1009                   inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
```
```  1010 apply (rule finite_induct, assumption, force)
```
```  1011 apply (rule impI, auto)
```
```  1012 apply (simp add: inj_on_def)
```
```  1013 apply (subgoal_tac "f x \<notin> f ` F")
```
```  1014 apply (subgoal_tac "finite (f ` F)")
```
```  1015 apply (auto simp add: setprod_insert)
```
```  1016 apply (simp add: inj_on_def)
```
```  1017   done
```
```  1018
```
```  1019 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
```
```  1020     setprod f B = setprod id (f ` B)"
```
```  1021 by (auto simp add: setprod_reindex id_o)
```
```  1022
```
```  1023 lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
```
```  1024     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
```
```  1025   by (frule setprod_reindex, assumption, simp)
```
```  1026
```
```  1027 lemma setprod_cong:
```
```  1028   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
```
```  1029   apply (case_tac "finite B")
```
```  1030    prefer 2 apply (simp add: setprod_def, simp)
```
```  1031   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
```
```  1032    apply simp
```
```  1033   apply (erule finite_induct, simp)
```
```  1034   apply (simp add: subset_insert_iff, clarify)
```
```  1035   apply (subgoal_tac "finite C")
```
```  1036    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```  1037   apply (subgoal_tac "C = insert x (C - {x})")
```
```  1038    prefer 2 apply blast
```
```  1039   apply (erule ssubst)
```
```  1040   apply (drule spec)
```
```  1041   apply (erule (1) notE impE)
```
```  1042   apply (simp add: Ball_def del:insert_Diff_single)
```
```  1043   done
```
```  1044
```
```  1045 lemma setprod_1: "setprod (%i. 1) A = 1"
```
```  1046   apply (case_tac "finite A")
```
```  1047   apply (erule finite_induct, auto simp add: times_ac1)
```
```  1048   apply (simp add: setprod_def)
```
```  1049   done
```
```  1050
```
```  1051 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
```
```  1052   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
```
```  1053   apply (erule ssubst, rule setprod_1)
```
```  1054   apply (rule setprod_cong, auto)
```
```  1055   done
```
```  1056
```
```  1057 lemma setprod_Un_Int: "finite A ==> finite B
```
```  1058     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
```
```  1059   apply (induct set: Finites, simp)
```
```  1060   apply (simp add: times_ac1 insert_absorb)
```
```  1061   apply (simp add: times_ac1 Int_insert_left insert_absorb)
```
```  1062   done
```
```  1063
```
```  1064 lemma setprod_Un_disjoint: "finite A ==> finite B
```
```  1065   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
```
```  1066   apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
```
```  1067   done
```
```  1068
```
```  1069 lemma setprod_UN_disjoint:
```
```  1070     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1071         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1072       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
```
```  1073   apply (induct set: Finites, simp, atomize)
```
```  1074   apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```  1075    prefer 2 apply blast
```
```  1076   apply (subgoal_tac "A x Int UNION F A = {}")
```
```  1077    prefer 2 apply blast
```
```  1078   apply (simp add: setprod_Un_disjoint)
```
```  1079   done
```
```  1080
```
```  1081 lemma setprod_Union_disjoint:
```
```  1082   "finite C ==> (ALL A:C. finite A) ==>
```
```  1083         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```  1084       setprod f (Union C) = setprod (setprod f) C"
```
```  1085   apply (frule setprod_UN_disjoint [of C id f])
```
```  1086   apply (unfold Union_def id_def, assumption+)
```
```  1087   done
```
```  1088
```
```  1089 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1090     (\<Prod> x:A. (\<Prod> y: B x. f x y)) =
```
```  1091     (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
```
```  1092   apply (subst Sigma_def)
```
```  1093   apply (subst setprod_UN_disjoint)
```
```  1094   apply assumption
```
```  1095   apply (rule ballI)
```
```  1096   apply (drule_tac x = i in bspec, assumption)
```
```  1097   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
```
```  1098   apply (rule finite_surj)
```
```  1099   apply auto
```
```  1100   apply (rule setprod_cong, rule refl)
```
```  1101   apply (subst setprod_UN_disjoint)
```
```  1102   apply (erule bspec, assumption)
```
```  1103   apply auto
```
```  1104   done
```
```  1105
```
```  1106 lemma setprod_cartesian_product: "finite A ==> finite B ==>
```
```  1107     (\<Prod> x:A. (\<Prod> y: B. f x y)) =
```
```  1108     (\<Prod> z:(A <*> B). f (fst z) (snd z))"
```
```  1109   by (erule setprod_Sigma, auto)
```
```  1110
```
```  1111 lemma setprod_timesf: "setprod (%x. f x * g x) A =
```
```  1112     (setprod f A * setprod g A)"
```
```  1113   apply (case_tac "finite A")
```
```  1114    prefer 2 apply (simp add: setprod_def times_ac1)
```
```  1115   apply (erule finite_induct, auto)
```
```  1116   apply (simp add: times_ac1)
```
```  1117   done
```
```  1118
```
```  1119 subsubsection {* Properties in more restricted classes of structures *}
```
```  1120
```
```  1121 lemma setprod_eq_1_iff [simp]:
```
```  1122     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
```
```  1123   by (induct set: Finites) auto
```
```  1124
```
```  1125 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
```
```  1126     y^(card A)"
```
```  1127   apply (erule finite_induct)
```
```  1128   apply (auto simp add: power_Suc)
```
```  1129   done
```
```  1130
```
```  1131 lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
```
```  1132     setprod f A = 0"
```
```  1133   apply (induct set: Finites, force, clarsimp)
```
```  1134   apply (erule disjE, auto)
```
```  1135   done
```
```  1136
```
```  1137 lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
```
```  1138      --> 0 \<le> setprod f A"
```
```  1139   apply (case_tac "finite A")
```
```  1140   apply (induct set: Finites, force, clarsimp)
```
```  1141   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
```
```  1142   apply (rule mult_mono, assumption+)
```
```  1143   apply (auto simp add: setprod_def)
```
```  1144   done
```
```  1145
```
```  1146 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
```
```  1147      --> 0 < setprod f A"
```
```  1148   apply (case_tac "finite A")
```
```  1149   apply (induct set: Finites, force, clarsimp)
```
```  1150   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
```
```  1151   apply (rule mult_strict_mono, assumption+)
```
```  1152   apply (auto simp add: setprod_def)
```
```  1153   done
```
```  1154
```
```  1155 lemma setprod_nonzero [rule_format]:
```
```  1156     "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
```
```  1157       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
```
```  1158   apply (erule finite_induct, auto)
```
```  1159   done
```
```  1160
```
```  1161 lemma setprod_zero_eq:
```
```  1162     "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
```
```  1163      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
```
```  1164   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
```
```  1165   done
```
```  1166
```
```  1167 lemma setprod_nonzero_field:
```
```  1168     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
```
```  1169   apply (rule setprod_nonzero, auto)
```
```  1170   done
```
```  1171
```
```  1172 lemma setprod_zero_eq_field:
```
```  1173     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
```
```  1174   apply (rule setprod_zero_eq, auto)
```
```  1175   done
```
```  1176
```
```  1177 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
```
```  1178     (setprod f (A Un B) :: 'a ::{field})
```
```  1179       = setprod f A * setprod f B / setprod f (A Int B)"
```
```  1180   apply (subst setprod_Un_Int [symmetric], auto)
```
```  1181   apply (subgoal_tac "finite (A Int B)")
```
```  1182   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
```
```  1183   apply (subst times_divide_eq_right [THEN sym], auto)
```
```  1184   done
```
```  1185
```
```  1186 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
```
```  1187     (setprod f (A - {a}) :: 'a :: {field}) =
```
```  1188       (if a:A then setprod f A / f a else setprod f A)"
```
```  1189   apply (erule finite_induct)
```
```  1190    apply (auto simp add: insert_Diff_if)
```
```  1191   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
```
```  1192   apply (erule ssubst)
```
```  1193   apply (subst times_divide_eq_right [THEN sym])
```
```  1194   apply (auto simp add: mult_ac)
```
```  1195   done
```
```  1196
```
```  1197 lemma setprod_inversef: "finite A ==>
```
```  1198     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
```
```  1199       setprod (inverse \<circ> f) A = inverse (setprod f A)"
```
```  1200   apply (erule finite_induct)
```
```  1201   apply (simp, simp)
```
```  1202   done
```
```  1203
```
```  1204 lemma setprod_dividef:
```
```  1205      "[|finite A;
```
```  1206         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
```
```  1207       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
```
```  1208   apply (subgoal_tac
```
```  1209          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
```
```  1210   apply (erule ssubst)
```
```  1211   apply (subst divide_inverse)
```
```  1212   apply (subst setprod_timesf)
```
```  1213   apply (subst setprod_inversef, assumption+, rule refl)
```
```  1214   apply (rule setprod_cong, rule refl)
```
```  1215   apply (subst divide_inverse, auto)
```
```  1216   done
```
```  1217
```
```  1218
```
```  1219 subsection{* Min and Max of finite linearly ordered sets *}
```
```  1220
```
```  1221 text{* Seemed easier to define directly than via fold. *}
```
```  1222
```
```  1223 lemma ex_Max: fixes S :: "('a::linorder)set"
```
```  1224   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
```
```  1225 using fin
```
```  1226 proof (induct)
```
```  1227   case empty thus ?case by simp
```
```  1228 next
```
```  1229   case (insert S x)
```
```  1230   show ?case
```
```  1231   proof (cases)
```
```  1232     assume "S = {}" thus ?thesis by simp
```
```  1233   next
```
```  1234     assume nonempty: "S \<noteq> {}"
```
```  1235     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
```
```  1236     show ?thesis
```
```  1237     proof (cases)
```
```  1238       assume "x \<le> m" thus ?thesis using m by blast
```
```  1239     next
```
```  1240       assume "~ x \<le> m" thus ?thesis using m
```
```  1241 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
```
```  1242     qed
```
```  1243   qed
```
```  1244 qed
```
```  1245
```
```  1246 lemma ex_Min: fixes S :: "('a::linorder)set"
```
```  1247   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
```
```  1248 using fin
```
```  1249 proof (induct)
```
```  1250   case empty thus ?case by simp
```
```  1251 next
```
```  1252   case (insert S x)
```
```  1253   show ?case
```
```  1254   proof (cases)
```
```  1255     assume "S = {}" thus ?thesis by simp
```
```  1256   next
```
```  1257     assume nonempty: "S \<noteq> {}"
```
```  1258     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
```
```  1259     show ?thesis
```
```  1260     proof (cases)
```
```  1261       assume "m \<le> x" thus ?thesis using m by blast
```
```  1262     next
```
```  1263       assume "~ m \<le> x" thus ?thesis using m
```
```  1264 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
```
```  1265     qed
```
```  1266   qed
```
```  1267 qed
```
```  1268
```
```  1269 constdefs
```
```  1270  Min :: "('a::linorder)set => 'a"
```
```  1271 "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
```
```  1272
```
```  1273  Max :: "('a::linorder)set => 'a"
```
```  1274 "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
```
```  1275
```
```  1276 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
```
```  1277                  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
```
```  1278 proof (unfold Min_def, rule theI')
```
```  1279   show "\<exists>!m. ?P m"
```
```  1280   proof (rule ex_ex1I)
```
```  1281     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
```
```  1282   next
```
```  1283     fix m1 m2 assume "?P m1" "?P m2"
```
```  1284     thus "m1 = m2" by (blast dest:order_antisym)
```
```  1285   qed
```
```  1286 qed
```
```  1287
```
```  1288 lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
```
```  1289                  shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
```
```  1290 proof (unfold Max_def, rule theI')
```
```  1291   show "\<exists>!m. ?P m"
```
```  1292   proof (rule ex_ex1I)
```
```  1293     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
```
```  1294   next
```
```  1295     fix m1 m2 assume "?P m1" "?P m2"
```
```  1296     thus "m1 = m2" by (blast dest:order_antisym)
```
```  1297   qed
```
```  1298 qed
```
```  1299
```
```  1300 subsection {* Theorems about @{text "choose"} *}
```
```  1301
```
```  1302 text {*
```
```  1303   \medskip Basic theorem about @{text "choose"}.  By Florian
```
```  1304   Kammüller, tidied by LCP.
```
```  1305 *}
```
```  1306
```
```  1307 lemma card_s_0_eq_empty:
```
```  1308     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
```
```  1309   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
```
```  1310   apply (simp cong add: rev_conj_cong)
```
```  1311   done
```
```  1312
```
```  1313 lemma choose_deconstruct: "finite M ==> x \<notin> M
```
```  1314   ==> {s. s <= insert x M & card(s) = Suc k}
```
```  1315        = {s. s <= M & card(s) = Suc k} Un
```
```  1316          {s. EX t. t <= M & card(t) = k & s = insert x t}"
```
```  1317   apply safe
```
```  1318    apply (auto intro: finite_subset [THEN card_insert_disjoint])
```
```  1319   apply (drule_tac x = "xa - {x}" in spec)
```
```  1320   apply (subgoal_tac "x \<notin> xa", auto)
```
```  1321   apply (erule rev_mp, subst card_Diff_singleton)
```
```  1322   apply (auto intro: finite_subset)
```
```  1323   done
```
```  1324
```
```  1325 lemma card_inj_on_le:
```
```  1326     "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
```
```  1327   by (auto intro: card_mono simp add: card_image [symmetric])
```
```  1328
```
```  1329 lemma card_bij_eq:
```
```  1330     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
```
```  1331        finite A; finite B |] ==> card A = card B"
```
```  1332   by (auto intro: le_anti_sym card_inj_on_le)
```
```  1333
```
```  1334 text{*There are as many subsets of @{term A} having cardinality @{term k}
```
```  1335  as there are sets obtained from the former by inserting a fixed element
```
```  1336  @{term x} into each.*}
```
```  1337 lemma constr_bij:
```
```  1338    "[|finite A; x \<notin> A|] ==>
```
```  1339     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
```
```  1340     card {B. B <= A & card(B) = k}"
```
```  1341   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
```
```  1342        apply (auto elim!: equalityE simp add: inj_on_def)
```
```  1343     apply (subst Diff_insert0, auto)
```
```  1344    txt {* finiteness of the two sets *}
```
```  1345    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
```
```  1346    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
```
```  1347    apply fast+
```
```  1348   done
```
```  1349
```
```  1350 text {*
```
```  1351   Main theorem: combinatorial statement about number of subsets of a set.
```
```  1352 *}
```
```  1353
```
```  1354 lemma n_sub_lemma:
```
```  1355   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
```
```  1356   apply (induct k)
```
```  1357    apply (simp add: card_s_0_eq_empty, atomize)
```
```  1358   apply (rotate_tac -1, erule finite_induct)
```
```  1359    apply (simp_all (no_asm_simp) cong add: conj_cong
```
```  1360      add: card_s_0_eq_empty choose_deconstruct)
```
```  1361   apply (subst card_Un_disjoint)
```
```  1362      prefer 4 apply (force simp add: constr_bij)
```
```  1363     prefer 3 apply force
```
```  1364    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
```
```  1365      finite_subset [of _ "Pow (insert x F)", standard])
```
```  1366   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
```
```  1367   done
```
```  1368
```
```  1369 theorem n_subsets:
```
```  1370     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
```
```  1371   by (simp add: n_sub_lemma)
```
```  1372
```
```  1373
```
```  1374 end
```