src/HOL/Finite_Set.thy
author obua
Tue Nov 23 15:50:27 2004 +0100 (2004-11-23)
changeset 15314 55eec5c6d401
parent 15311 2ca1c66a6758
child 15315 a358e31572d9
permissions -rw-r--r--
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
     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: "(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 (* By Jeremy Siek: *)
   975 
   976 lemma setsum_diff: 
   977   assumes finB: "finite B"
   978   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   979 using finB
   980 proof (induct)
   981   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   982 next
   983   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   984     and xFinA: "insert x F \<subseteq> A"
   985     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   986   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   987   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   988     by (simp add: setsum_diff1)
   989   from xFinA have "F \<subseteq> A" by simp
   990   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   991   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   992     by simp
   993   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   994   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   995     by simp
   996   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   997   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   998     by simp
   999   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1000 qed
  1001 
  1002 lemma setsum_mono:
  1003   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1004   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1005 proof (cases "finite K")
  1006   case True
  1007   thus ?thesis using le
  1008   proof (induct)
  1009     case empty
  1010     thus ?case by simp
  1011   next
  1012     case insert
  1013     thus ?case using add_mono 
  1014       by force
  1015   qed
  1016 next
  1017   case False
  1018   thus ?thesis
  1019     by (simp add: setsum_def)
  1020 qed
  1021 
  1022 lemma finite_setsum_diff1: "finite A \<Longrightarrow> (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) =
  1023     (if a:A then setsum f A - f a else setsum f A)"
  1024   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1025 
  1026 lemma finite_setsum_diff:
  1027   assumes le: "finite A" "B \<subseteq> A"
  1028   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
  1029 proof -
  1030   from le have finiteB: "finite B" using finite_subset by auto
  1031   show ?thesis using le finiteB
  1032     proof (induct rule: Finites.induct[OF finiteB])
  1033       case 1
  1034       thus ?case by auto
  1035     next
  1036       case 2
  1037       thus ?case using le 
  1038 	apply auto
  1039 	apply (subst Diff_insert)
  1040 	apply (subst finite_setsum_diff1)
  1041 	apply (auto simp add: insert_absorb)
  1042 	done
  1043     qed
  1044   qed
  1045 
  1046 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
  1047   - setsum f A"
  1048   by (induct set: Finites, auto)
  1049 
  1050 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1051   setsum f A - setsum g A"
  1052   by (simp add: diff_minus setsum_addf setsum_negf)
  1053 
  1054 lemma setsum_nonneg: "[| finite A;
  1055     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
  1056     0 \<le> setsum f A";
  1057   apply (induct set: Finites, auto)
  1058   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1059   apply (blast intro: add_mono)
  1060   done
  1061 
  1062 lemma setsum_nonpos: "[| finite A;
  1063     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
  1064     setsum f A \<le> 0";
  1065   apply (induct set: Finites, auto)
  1066   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1067   apply (blast intro: add_mono)
  1068   done
  1069 
  1070 lemma setsum_mult: 
  1071   fixes f :: "'a => ('b::semiring_0_cancel)"
  1072   shows "r * setsum f A = setsum (%n. r * f n) A"
  1073 proof (cases "finite A")
  1074   case True
  1075   thus ?thesis
  1076   proof (induct)
  1077     case empty thus ?case by simp
  1078   next
  1079     case (insert A x) thus ?case by (simp add: right_distrib)
  1080   qed
  1081 next
  1082   case False thus ?thesis by (simp add: setsum_def)
  1083 qed
  1084 
  1085 lemma setsum_abs: 
  1086   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1087   assumes fin: "finite A" 
  1088   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1089 using fin 
  1090 proof (induct) 
  1091   case empty thus ?case by simp
  1092 next
  1093   case (insert A x)
  1094   thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1095 qed
  1096 
  1097 lemma setsum_abs_ge_zero: 
  1098   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1099   assumes fin: "finite A" 
  1100   shows "0 \<le> setsum (%i. abs(f i)) A"
  1101 using fin 
  1102 proof (induct) 
  1103   case empty thus ?case by simp
  1104 next
  1105   case (insert A x) thus ?case by (auto intro: order_trans)
  1106 qed
  1107 
  1108 subsubsection {* Cardinality of unions and Sigma sets *}
  1109 
  1110 lemma card_UN_disjoint:
  1111     "finite I ==> (ALL i:I. finite (A i)) ==>
  1112         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1113       card (UNION I A) = setsum (%i. card (A i)) I"
  1114   apply (subst card_eq_setsum)
  1115   apply (subst finite_UN, assumption+)
  1116   apply (subgoal_tac
  1117            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1118   apply (simp add: setsum_UN_disjoint) 
  1119   apply (simp add: setsum_constant_nat cong: setsum_cong) 
  1120   done
  1121 
  1122 lemma card_Union_disjoint:
  1123   "finite C ==> (ALL A:C. finite A) ==>
  1124         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1125       card (Union C) = setsum card C"
  1126   apply (frule card_UN_disjoint [of C id])
  1127   apply (unfold Union_def id_def, assumption+)
  1128   done
  1129 
  1130 lemma SigmaI_insert: "y \<notin> A ==>
  1131   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1132   by auto
  1133 
  1134 lemma card_cartesian_product_singleton: "finite A ==>
  1135     card({x} <*> A) = card(A)"
  1136   apply (subgoal_tac "inj_on (%y .(x,y)) A")
  1137   apply (frule card_image, assumption)
  1138   apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
  1139   apply (auto simp add: inj_on_def)
  1140   done
  1141 
  1142 lemma card_SigmaI [rule_format,simp]: "finite A ==>
  1143   (ALL a:A. finite (B a)) -->
  1144   card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1145   apply (erule finite_induct, auto)
  1146   apply (subst SigmaI_insert, assumption)
  1147   apply (subst card_Un_disjoint)
  1148   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
  1149   done
  1150 
  1151 lemma card_cartesian_product:
  1152      "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
  1153   by (simp add: setsum_constant_nat)
  1154 
  1155 
  1156 
  1157 subsection {* Generalized product over a set *}
  1158 
  1159 constdefs
  1160   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1161   "setprod f A == if finite A then fold (op * o f) 1 A else 1"
  1162 
  1163 syntax
  1164   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  1165 
  1166 syntax (xsymbols)
  1167   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1168 syntax (HTML output)
  1169   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1170 translations
  1171   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  1172 
  1173 lemma setprod_empty [simp]: "setprod f {} = 1"
  1174   by (auto simp add: setprod_def)
  1175 
  1176 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1177     setprod f (insert a A) = f a * setprod f A"
  1178   by (auto simp add: setprod_def LC_def LC.fold_insert
  1179       mult_left_commute)
  1180 
  1181 lemma setprod_reindex [rule_format]:
  1182      "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
  1183 by (rule finite_induct, auto)
  1184 
  1185 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
  1186     setprod f B = setprod id (f ` B)"
  1187 by (auto simp add: setprod_reindex id_o)
  1188 
  1189 lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
  1190     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1191   by (frule setprod_reindex, assumption, simp)
  1192 
  1193 lemma setprod_cong:
  1194   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1195   apply (case_tac "finite B")
  1196    prefer 2 apply (simp add: setprod_def, simp)
  1197   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
  1198    apply simp
  1199   apply (erule finite_induct, simp)
  1200   apply (simp add: subset_insert_iff, clarify)
  1201   apply (subgoal_tac "finite C")
  1202    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
  1203   apply (subgoal_tac "C = insert x (C - {x})")
  1204    prefer 2 apply blast
  1205   apply (erule ssubst)
  1206   apply (drule spec)
  1207   apply (erule (1) notE impE)
  1208   apply (simp add: Ball_def del:insert_Diff_single)
  1209   done
  1210 
  1211 lemma setprod_1: "setprod (%i. 1) A = 1"
  1212   apply (case_tac "finite A")
  1213   apply (erule finite_induct, auto simp add: mult_ac)
  1214   apply (simp add: setprod_def)
  1215   done
  1216 
  1217 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1218   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1219   apply (erule ssubst, rule setprod_1)
  1220   apply (rule setprod_cong, auto)
  1221   done
  1222 
  1223 lemma setprod_Un_Int: "finite A ==> finite B
  1224     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1225   apply (induct set: Finites, simp)
  1226   apply (simp add: mult_ac insert_absorb)
  1227   apply (simp add: mult_ac Int_insert_left insert_absorb)
  1228   done
  1229 
  1230 lemma setprod_Un_disjoint: "finite A ==> finite B
  1231   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1232   apply (subst setprod_Un_Int [symmetric], auto simp add: mult_ac)
  1233   done
  1234 
  1235 lemma setprod_UN_disjoint:
  1236     "finite I ==> (ALL i:I. finite (A i)) ==>
  1237         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1238       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1239   apply (induct set: Finites, simp, atomize)
  1240   apply (subgoal_tac "ALL i:F. x \<noteq> i")
  1241    prefer 2 apply blast
  1242   apply (subgoal_tac "A x Int UNION F A = {}")
  1243    prefer 2 apply blast
  1244   apply (simp add: setprod_Un_disjoint)
  1245   done
  1246 
  1247 lemma setprod_Union_disjoint:
  1248   "finite C ==> (ALL A:C. finite A) ==>
  1249         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1250       setprod f (Union C) = setprod (setprod f) C"
  1251   apply (frule setprod_UN_disjoint [of C id f])
  1252   apply (unfold Union_def id_def, assumption+)
  1253   done
  1254 
  1255 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1256     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  1257     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1258   apply (subst Sigma_def)
  1259   apply (subst setprod_UN_disjoint)
  1260   apply assumption
  1261   apply (rule ballI)
  1262   apply (drule_tac x = i in bspec, assumption)
  1263   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
  1264   apply (rule finite_surj)
  1265   apply auto
  1266   apply (rule setprod_cong, rule refl)
  1267   apply (subst setprod_UN_disjoint)
  1268   apply (erule bspec, assumption)
  1269   apply auto
  1270   done
  1271 
  1272 lemma setprod_cartesian_product: "finite A ==> finite B ==>
  1273     (\<Prod>x:A. (\<Prod>y: B. f x y)) =
  1274     (\<Prod>z:(A <*> B). f (fst z) (snd z))"
  1275   by (erule setprod_Sigma, auto)
  1276 
  1277 lemma setprod_timesf: "setprod (%x. f x * g x) A =
  1278     (setprod f A * setprod g A)"
  1279   apply (case_tac "finite A")
  1280    prefer 2 apply (simp add: setprod_def mult_ac)
  1281   apply (erule finite_induct, auto)
  1282   apply (simp add: mult_ac)
  1283   done
  1284 
  1285 subsubsection {* Properties in more restricted classes of structures *}
  1286 
  1287 lemma setprod_eq_1_iff [simp]:
  1288     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1289   by (induct set: Finites) auto
  1290 
  1291 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
  1292   apply (erule finite_induct)
  1293   apply (auto simp add: power_Suc)
  1294   done
  1295 
  1296 lemma setprod_zero:
  1297      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1298   apply (induct set: Finites, force, clarsimp)
  1299   apply (erule disjE, auto)
  1300   done
  1301 
  1302 lemma setprod_nonneg [rule_format]:
  1303      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1304   apply (case_tac "finite A")
  1305   apply (induct set: Finites, force, clarsimp)
  1306   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1307   apply (rule mult_mono, assumption+)
  1308   apply (auto simp add: setprod_def)
  1309   done
  1310 
  1311 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1312      --> 0 < setprod f A"
  1313   apply (case_tac "finite A")
  1314   apply (induct set: Finites, force, clarsimp)
  1315   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1316   apply (rule mult_strict_mono, assumption+)
  1317   apply (auto simp add: setprod_def)
  1318   done
  1319 
  1320 lemma setprod_nonzero [rule_format]:
  1321     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1322       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1323   apply (erule finite_induct, auto)
  1324   done
  1325 
  1326 lemma setprod_zero_eq:
  1327     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1328      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1329   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1330   done
  1331 
  1332 lemma setprod_nonzero_field:
  1333     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1334   apply (rule setprod_nonzero, auto)
  1335   done
  1336 
  1337 lemma setprod_zero_eq_field:
  1338     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1339   apply (rule setprod_zero_eq, auto)
  1340   done
  1341 
  1342 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1343     (setprod f (A Un B) :: 'a ::{field})
  1344       = setprod f A * setprod f B / setprod f (A Int B)"
  1345   apply (subst setprod_Un_Int [symmetric], auto)
  1346   apply (subgoal_tac "finite (A Int B)")
  1347   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1348   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1349   done
  1350 
  1351 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1352     (setprod f (A - {a}) :: 'a :: {field}) =
  1353       (if a:A then setprod f A / f a else setprod f A)"
  1354   apply (erule finite_induct)
  1355    apply (auto simp add: insert_Diff_if)
  1356   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1357   apply (erule ssubst)
  1358   apply (subst times_divide_eq_right [THEN sym])
  1359   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1360   done
  1361 
  1362 lemma setprod_inversef: "finite A ==>
  1363     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1364       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1365   apply (erule finite_induct)
  1366   apply (simp, simp)
  1367   done
  1368 
  1369 lemma setprod_dividef:
  1370      "[|finite A;
  1371         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1372       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1373   apply (subgoal_tac
  1374          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1375   apply (erule ssubst)
  1376   apply (subst divide_inverse)
  1377   apply (subst setprod_timesf)
  1378   apply (subst setprod_inversef, assumption+, rule refl)
  1379   apply (rule setprod_cong, rule refl)
  1380   apply (subst divide_inverse, auto)
  1381   done
  1382 
  1383 
  1384 subsection{* Min and Max of finite linearly ordered sets *}
  1385 
  1386 text{* Seemed easier to define directly than via fold. *}
  1387 
  1388 lemma ex_Max: fixes S :: "('a::linorder)set"
  1389   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
  1390 using fin
  1391 proof (induct)
  1392   case empty thus ?case by simp
  1393 next
  1394   case (insert S x)
  1395   show ?case
  1396   proof (cases)
  1397     assume "S = {}" thus ?thesis by simp
  1398   next
  1399     assume nonempty: "S \<noteq> {}"
  1400     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
  1401     show ?thesis
  1402     proof (cases)
  1403       assume "x \<le> m" thus ?thesis using m by blast
  1404     next
  1405       assume "~ x \<le> m" thus ?thesis using m
  1406         by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  1407     qed
  1408   qed
  1409 qed
  1410 
  1411 lemma ex_Min: fixes S :: "('a::linorder)set"
  1412   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
  1413 using fin
  1414 proof (induct)
  1415   case empty thus ?case by simp
  1416 next
  1417   case (insert S x)
  1418   show ?case
  1419   proof (cases)
  1420     assume "S = {}" thus ?thesis by simp
  1421   next
  1422     assume nonempty: "S \<noteq> {}"
  1423     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
  1424     show ?thesis
  1425     proof (cases)
  1426       assume "m \<le> x" thus ?thesis using m by blast
  1427     next
  1428       assume "~ m \<le> x" thus ?thesis using m
  1429         by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
  1430     qed
  1431   qed
  1432 qed
  1433 
  1434 constdefs
  1435   Min :: "('a::linorder)set => 'a"
  1436   "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
  1437 
  1438   Max :: "('a::linorder)set => 'a"
  1439   "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
  1440 
  1441 lemma Min [simp]:
  1442   assumes a: "finite S"  "S \<noteq> {}"
  1443   shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
  1444 proof (unfold Min_def, rule theI')
  1445   show "\<exists>!m. ?P m"
  1446   proof (rule ex_ex1I)
  1447     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
  1448   next
  1449     fix m1 m2 assume "?P m1" and "?P m2"
  1450     thus "m1 = m2" by (blast dest: order_antisym)
  1451   qed
  1452 qed
  1453 
  1454 lemma Max [simp]:
  1455   assumes a: "finite S"  "S \<noteq> {}"
  1456   shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
  1457 proof (unfold Max_def, rule theI')
  1458   show "\<exists>!m. ?P m"
  1459   proof (rule ex_ex1I)
  1460     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
  1461   next
  1462     fix m1 m2 assume "?P m1" "?P m2"
  1463     thus "m1 = m2" by (blast dest: order_antisym)
  1464   qed
  1465 qed
  1466 
  1467 
  1468 subsection {* Theorems about @{text "choose"} *}
  1469 
  1470 text {*
  1471   \medskip Basic theorem about @{text "choose"}.  By Florian
  1472   Kamm\"uller, tidied by LCP.
  1473 *}
  1474 
  1475 lemma card_s_0_eq_empty:
  1476     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1477   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1478   apply (simp cong add: rev_conj_cong)
  1479   done
  1480 
  1481 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1482   ==> {s. s <= insert x M & card(s) = Suc k}
  1483        = {s. s <= M & card(s) = Suc k} Un
  1484          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1485   apply safe
  1486    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1487   apply (drule_tac x = "xa - {x}" in spec)
  1488   apply (subgoal_tac "x \<notin> xa", auto)
  1489   apply (erule rev_mp, subst card_Diff_singleton)
  1490   apply (auto intro: finite_subset)
  1491   done
  1492 
  1493 lemma card_inj_on_le:
  1494     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1495 apply (subgoal_tac "finite A") 
  1496  apply (force intro: card_mono simp add: card_image [symmetric])
  1497 apply (blast intro: finite_imageD dest: finite_subset) 
  1498 done
  1499 
  1500 lemma card_bij_eq:
  1501     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1502        finite A; finite B |] ==> card A = card B"
  1503   by (auto intro: le_anti_sym card_inj_on_le)
  1504 
  1505 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1506  as there are sets obtained from the former by inserting a fixed element
  1507  @{term x} into each.*}
  1508 lemma constr_bij:
  1509    "[|finite A; x \<notin> A|] ==>
  1510     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1511     card {B. B <= A & card(B) = k}"
  1512   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1513        apply (auto elim!: equalityE simp add: inj_on_def)
  1514     apply (subst Diff_insert0, auto)
  1515    txt {* finiteness of the two sets *}
  1516    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1517    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1518    apply fast+
  1519   done
  1520 
  1521 text {*
  1522   Main theorem: combinatorial statement about number of subsets of a set.
  1523 *}
  1524 
  1525 lemma n_sub_lemma:
  1526   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1527   apply (induct k)
  1528    apply (simp add: card_s_0_eq_empty, atomize)
  1529   apply (rotate_tac -1, erule finite_induct)
  1530    apply (simp_all (no_asm_simp) cong add: conj_cong
  1531      add: card_s_0_eq_empty choose_deconstruct)
  1532   apply (subst card_Un_disjoint)
  1533      prefer 4 apply (force simp add: constr_bij)
  1534     prefer 3 apply force
  1535    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1536      finite_subset [of _ "Pow (insert x F)", standard])
  1537   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1538   done
  1539 
  1540 theorem n_subsets:
  1541     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1542   by (simp add: n_sub_lemma)
  1543 
  1544 end