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