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