1 (* Title: HOL/Finite_Set.thy
3 Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
4 Additions by Jeremy Avigad in Feb 2004
5 License: GPL (GNU GENERAL PUBLIC LICENSE)
8 header {* Finite sets *}
10 theory Finite_Set = Divides + Power + Inductive:
12 subsection {* Collection of finite sets *}
14 consts Finites :: "'a set set"
16 finite :: "'a set => bool"
18 "finite A" == "A : Finites"
22 emptyI [simp, intro!]: "{} : Finites"
23 insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
25 axclass finite \<subseteq> type
28 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
29 "[| ~finite(UNIV::'a set); finite A |] ==> \<exists>a::'a. a \<notin> A"
30 by(subgoal_tac "A \<noteq> UNIV", blast, blast)
33 lemma finite_induct [case_names empty insert, induct set: Finites]:
35 P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
36 -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
39 insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
44 fix F x assume F: "finite F" and P: "P F"
48 hence "insert x F = F" by (rule insert_absorb)
49 with P show ?thesis by (simp only:)
52 from F this P show ?thesis by (rule insert)
57 lemma finite_subset_induct [consumes 2, case_names empty insert]:
58 "finite F ==> F \<subseteq> A ==>
59 P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
62 assume "P {}" and insert:
63 "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
65 thus "F \<subseteq> A ==> P F"
68 fix F x assume "finite F" and "x \<notin> F"
69 and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
72 from i show "x \<in> A" by blast
73 from i have "F \<subseteq> A" by blast
79 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
80 -- {* The union of two finite sets is finite. *}
81 by (induct set: Finites) simp_all
83 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
84 -- {* Every subset of a finite set is finite. *}
87 thus "!!A. A \<subseteq> B ==> finite A"
93 have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
97 with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
98 with r have "finite (A - {x})" .
99 hence "finite (insert x (A - {x}))" ..
100 also have "insert x (A - {x}) = A" by (rule insert_Diff)
101 finally show ?thesis .
103 show "A \<subseteq> F ==> ?thesis" .
104 assume "x \<notin> A"
105 with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
110 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
111 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
113 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
114 -- {* The converse obviously fails. *}
115 by (blast intro: finite_subset)
117 lemma finite_insert [simp]: "finite (insert a A) = finite A"
118 apply (subst insert_is_Un)
119 apply (simp only: finite_Un, blast)
122 lemma finite_empty_induct:
124 P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
127 and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
131 presume c: "finite c" and b: "finite b"
132 and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
133 from c show "c \<subseteq> b ==> P (b - c)"
136 from P1 show ?case by simp
139 have "P (b - F - {x})"
141 from _ b show "finite (b - F)" by (rule finite_subset) blast
142 from insert show "x \<in> b - F" by simp
143 from insert show "P (b - F)" by simp
145 also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
149 show "A \<subseteq> A" ..
154 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
155 by (rule Diff_subset [THEN finite_subset])
157 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
158 apply (subst Diff_insert)
159 apply (case_tac "a : A - B")
160 apply (rule finite_insert [symmetric, THEN trans])
161 apply (subst insert_Diff, simp_all)
165 subsubsection {* Image and Inverse Image over Finite Sets *}
167 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
168 -- {* The image of a finite set is finite. *}
169 by (induct set: Finites) simp_all
171 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
172 apply (frule finite_imageI)
173 apply (erule finite_subset, assumption)
176 lemma finite_range_imageI:
177 "finite (range g) ==> finite (range (%x. f (g x)))"
178 apply (drule finite_imageI, simp)
181 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
183 have aux: "!!A. finite (A - {}) = finite A" by simp
186 thus "!!A. f`A = B ==> inj_on f A ==> finite A"
189 apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
191 apply (simp (no_asm_use) add: inj_on_def)
192 apply (blast dest!: aux [THEN iffD1], atomize)
193 apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
194 apply (frule subsetD [OF equalityD2 insertI1], clarify)
195 apply (rule_tac x = xa in bexI)
196 apply (simp_all add: inj_on_image_set_diff)
201 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
202 -- {* The inverse image of a singleton under an injective function
203 is included in a singleton. *}
204 apply (auto simp add: inj_on_def)
205 apply (blast intro: the_equality [symmetric])
208 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
209 -- {* The inverse image of a finite set under an injective function
211 apply (induct set: Finites, simp_all)
212 apply (subst vimage_insert)
213 apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
217 subsubsection {* The finite UNION of finite sets *}
219 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
220 by (induct set: Finites) simp_all
224 @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
227 @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
230 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
231 by (blast intro: finite_UN_I finite_subset)
234 subsubsection {* Sigma of finite sets *}
236 lemma finite_SigmaI [simp]:
237 "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
238 by (unfold Sigma_def) (blast intro!: finite_UN_I)
240 lemma finite_Prod_UNIV:
241 "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
242 apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
244 apply (erule finite_SigmaI, auto)
247 instance unit :: finite
249 have "finite {()}" by simp
250 also have "{()} = UNIV" by auto
251 finally show "finite (UNIV :: unit set)" .
254 instance * :: (finite, finite) finite
256 show "finite (UNIV :: ('a \<times> 'b) set)"
257 proof (rule finite_Prod_UNIV)
258 show "finite (UNIV :: 'a set)" by (rule finite)
259 show "finite (UNIV :: 'b set)" by (rule finite)
264 subsubsection {* The powerset of a finite set *}
266 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
268 assume "finite (Pow A)"
269 with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
270 thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
273 thus "finite (Pow A)"
274 by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
277 lemma finite_converse [iff]: "finite (r^-1) = finite r"
278 apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
281 apply (erule finite_imageD [unfolded inj_on_def])
282 apply (simp split add: split_split)
283 apply (erule finite_imageI)
284 apply (simp add: converse_def image_def, auto)
286 prefer 2 apply assumption
291 subsubsection {* Finiteness of transitive closure *}
293 text {* (Thanks to Sidi Ehmety) *}
295 lemma finite_Field: "finite r ==> finite (Field r)"
296 -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
297 apply (induct set: Finites)
298 apply (auto simp add: Field_def Domain_insert Range_insert)
301 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
303 apply (erule trancl_induct)
304 apply (auto simp add: Field_def)
307 lemma finite_trancl: "finite (r^+) = finite r"
310 apply (rule trancl_subset_Field2 [THEN finite_subset])
311 apply (rule finite_SigmaI)
313 apply (blast intro: r_into_trancl' finite_subset)
314 apply (auto simp add: finite_Field)
317 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
319 by (rule finite_SigmaI)
322 subsection {* Finite cardinality *}
325 This definition, although traditional, is ugly to work with: @{text
326 "card A == LEAST n. EX f. A = {f i | i. i < n}"}. Therefore we have
327 switched to an inductive one:
330 consts cardR :: "('a set \<times> nat) set"
334 EmptyI: "({}, 0) : cardR"
335 InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
338 card :: "'a set => nat"
339 "card A == THE n. (A, n) : cardR"
341 inductive_cases cardR_emptyE: "({}, n) : cardR"
342 inductive_cases cardR_insertE: "(insert a A,n) : cardR"
344 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
345 by (induct set: cardR) simp_all
347 lemma cardR_determ_aux1:
348 "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
349 apply (induct set: cardR, auto)
350 apply (simp add: insert_Diff_if, auto)
351 apply (drule cardR_SucD)
352 apply (blast intro!: cardR.intros)
355 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
356 by (drule cardR_determ_aux1) auto
358 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
359 apply (induct set: cardR)
360 apply (safe elim!: cardR_emptyE cardR_insertE)
361 apply (rename_tac B b m)
362 apply (case_tac "a = b")
363 apply (subgoal_tac "A = B")
364 prefer 2 apply (blast elim: equalityE, blast)
365 apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
367 apply (rule_tac x = "A Int B" in exI)
368 apply (blast elim: equalityE)
369 apply (frule_tac A = B in cardR_SucD)
370 apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
373 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
374 by (induct set: cardR) simp_all
376 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
377 by (induct set: Finites) (auto intro!: cardR.intros)
379 lemma card_equality: "(A,n) : cardR ==> card A = n"
380 by (unfold card_def) (blast intro: cardR_determ)
382 lemma card_empty [simp]: "card {} = 0"
383 by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
385 lemma card_insert_disjoint [simp]:
386 "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
388 assume x: "x \<notin> A"
389 hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
390 apply (auto intro!: cardR.intros)
391 apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
392 apply (force dest: cardR_imp_finite)
393 apply (blast intro!: cardR.intros intro: cardR_determ)
397 apply (simp add: card_def aux)
398 apply (rule the_equality)
399 apply (auto intro: finite_imp_cardR
400 cong: conj_cong simp: card_def [symmetric] card_equality)
404 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
406 apply (drule_tac a = x in mk_disjoint_insert, clarify)
407 apply (rotate_tac -1, auto)
410 lemma card_insert_if:
411 "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
412 by (simp add: insert_absorb)
414 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
415 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
416 apply(simp del:insert_Diff_single)
419 lemma card_Diff_singleton:
420 "finite A ==> x: A ==> card (A - {x}) = card A - 1"
421 by (simp add: card_Suc_Diff1 [symmetric])
423 lemma card_Diff_singleton_if:
424 "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
425 by (simp add: card_Diff_singleton)
427 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
428 by (simp add: card_insert_if card_Suc_Diff1)
430 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
431 by (simp add: card_insert_if)
433 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
434 apply (induct set: Finites, simp, clarify)
435 apply (subgoal_tac "finite A & A - {x} <= F")
436 prefer 2 apply (blast intro: finite_subset, atomize)
437 apply (drule_tac x = "A - {x}" in spec)
438 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
439 apply (case_tac "card A", auto)
442 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
443 apply (simp add: psubset_def linorder_not_le [symmetric])
444 apply (blast dest: card_seteq)
447 lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
448 apply (case_tac "A = B", simp)
449 apply (simp add: linorder_not_less [symmetric])
450 apply (blast dest: card_seteq intro: order_less_imp_le)
453 lemma card_Un_Int: "finite A ==> finite B
454 ==> card A + card B = card (A Un B) + card (A Int B)"
455 apply (induct set: Finites, simp)
456 apply (simp add: insert_absorb Int_insert_left)
459 lemma card_Un_disjoint: "finite A ==> finite B
460 ==> A Int B = {} ==> card (A Un B) = card A + card B"
461 by (simp add: card_Un_Int)
463 lemma card_Diff_subset:
464 "finite A ==> B <= A ==> card A - card B = card (A - B)"
465 apply (subgoal_tac "(A - B) Un B = A")
467 apply (rule nat_add_right_cancel [THEN iffD1])
468 apply (rule card_Un_disjoint [THEN subst])
469 apply (erule_tac [4] ssubst)
471 apply (simp_all add: add_commute not_less_iff_le
472 add_diff_inverse card_mono finite_subset)
475 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
476 apply (rule Suc_less_SucD)
477 apply (simp add: card_Suc_Diff1)
480 lemma card_Diff2_less:
481 "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
482 apply (case_tac "x = y")
483 apply (simp add: card_Diff1_less)
484 apply (rule less_trans)
485 prefer 2 apply (auto intro!: card_Diff1_less)
488 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
489 apply (case_tac "x : A")
490 apply (simp_all add: card_Diff1_less less_imp_le)
493 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
494 by (erule psubsetI, blast)
497 subsubsection {* Cardinality of image *}
499 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
500 apply (induct set: Finites, simp)
501 apply (simp add: le_SucI finite_imageI card_insert_if)
504 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
505 apply (induct set: Finites, simp_all, atomize, safe)
506 apply (unfold inj_on_def, blast)
507 apply (subst card_insert_disjoint)
508 apply (erule finite_imageI, blast, blast)
511 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
512 by (simp add: card_seteq card_image)
515 subsubsection {* Cardinality of the Powerset *}
517 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *)
518 apply (induct set: Finites)
519 apply (simp_all add: Pow_insert)
520 apply (subst card_Un_disjoint, blast)
521 apply (blast intro: finite_imageI, blast)
522 apply (subgoal_tac "inj_on (insert x) (Pow F)")
523 apply (simp add: card_image Pow_insert)
524 apply (unfold inj_on_def)
525 apply (blast elim!: equalityE)
529 \medskip Relates to equivalence classes. Based on a theorem of
530 F. Kammüller's. The @{prop "finite C"} premise is redundant.
534 "finite C ==> finite (Union C) ==>
535 ALL c : C. k dvd card c ==>
536 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
537 k dvd card (Union C)"
538 apply (induct set: Finites, simp_all, clarify)
539 apply (subst card_Un_disjoint)
540 apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
544 subsection {* A fold functional for finite sets *}
547 For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
548 f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
552 foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
554 inductive "foldSet f e"
556 emptyI [intro]: "({}, e) : foldSet f e"
557 insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
559 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
562 fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
563 "fold f e A == THE x. (A, x) : foldSet f e"
565 lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
566 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
568 lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
569 by (induct set: foldSet) auto
571 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
572 by (induct set: Finites) auto
575 subsubsection {* Left-commutative operations *}
578 fixes f :: "'b => 'a => 'a" (infixl "\<cdot>" 70)
579 assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
581 lemma (in LC) foldSet_determ_aux:
582 "ALL A x. card A < n --> (A, x) : foldSet f e -->
583 (ALL y. (A, y) : foldSet f e --> y = x)"
585 apply (auto simp add: less_Suc_eq)
586 apply (erule foldSet.cases, blast)
587 apply (erule foldSet.cases, blast, clarify)
588 txt {* force simplification of @{text "card A < card (insert ...)"}. *}
590 apply (simp add: less_Suc_eq_le)
592 apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
593 apply (subgoal_tac "Aa = Ab")
594 prefer 2 apply (blast elim!: equalityE, blast)
595 txt {* case @{prop "xa \<notin> xb"}. *}
596 apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
597 prefer 2 apply (blast elim!: equalityE, clarify)
598 apply (subgoal_tac "Aa = insert xb Ab - {xa}")
600 apply (subgoal_tac "card Aa <= card Ab")
602 apply (rule Suc_le_mono [THEN subst])
603 apply (simp add: card_Suc_Diff1)
604 apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
605 apply (blast intro: foldSet_imp_finite finite_Diff)
606 apply (frule (1) Diff1_foldSet)
607 apply (subgoal_tac "ya = f xb x")
608 prefer 2 apply (blast del: equalityCE)
609 apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
611 apply (subgoal_tac "yb = f xa x")
612 prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
613 apply (simp (no_asm_simp) add: left_commute)
616 lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
617 by (blast intro: foldSet_determ_aux [rule_format])
619 lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
620 by (unfold fold_def) (blast intro: foldSet_determ)
622 lemma fold_empty [simp]: "fold f e {} = e"
623 by (unfold fold_def) blast
625 lemma (in LC) fold_insert_aux: "x \<notin> A ==>
626 ((insert x A, v) : foldSet f e) =
627 (EX y. (A, y) : foldSet f e & v = f x y)"
629 apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
630 apply (fastsimp dest: foldSet_imp_finite)
631 apply (blast intro: foldSet_determ)
634 lemma (in LC) fold_insert:
635 "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
636 apply (unfold fold_def)
637 apply (simp add: fold_insert_aux)
638 apply (rule the_equality)
639 apply (auto intro: finite_imp_foldSet
640 cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
643 lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
644 apply (induct set: Finites, simp)
645 apply (simp add: left_commute fold_insert)
648 lemma (in LC) fold_nest_Un_Int:
649 "finite A ==> finite B
650 ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
651 apply (induct set: Finites, simp)
652 apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
655 lemma (in LC) fold_nest_Un_disjoint:
656 "finite A ==> finite B ==> A Int B = {}
657 ==> fold f e (A Un B) = fold f (fold f e B) A"
658 by (simp add: fold_nest_Un_Int)
660 declare foldSet_imp_finite [simp del]
661 empty_foldSetE [rule del] foldSet.intros [rule del]
662 -- {* Delete rules to do with @{text foldSet} relation. *}
666 subsubsection {* Commutative monoids *}
669 We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
670 instead of @{text "'b => 'a => 'a"}.
674 fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70)
676 assumes ident [simp]: "x \<cdot> e = x"
677 and commute: "x \<cdot> y = y \<cdot> x"
678 and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
680 lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
682 have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
683 also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
684 also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
685 finally show ?thesis .
688 lemmas (in ACe) AC = assoc commute left_commute
690 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
692 have "x \<cdot> e = x" by (rule ident)
693 thus ?thesis by (subst commute)
696 lemma (in ACe) fold_Un_Int:
697 "finite A ==> finite B ==>
698 fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
699 apply (induct set: Finites, simp)
700 apply (simp add: AC insert_absorb Int_insert_left
701 LC.fold_insert [OF LC.intro])
704 lemma (in ACe) fold_Un_disjoint:
705 "finite A ==> finite B ==> A Int B = {} ==>
706 fold f e (A Un B) = fold f e A \<cdot> fold f e B"
707 by (simp add: fold_Un_Int)
709 lemma (in ACe) fold_Un_disjoint2:
710 "finite A ==> finite B ==> A Int B = {} ==>
711 fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
715 thus "A Int B = {} ==>
716 fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
722 have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
724 also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
725 by (rule LC.fold_insert [OF LC.intro])
726 (insert b insert, auto simp add: left_commute)
727 also from insert have "fold (f o g) e (F \<union> B) =
728 fold (f o g) e F \<cdot> fold (f o g) e B" by blast
729 also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
731 also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
732 by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
733 auto simp add: left_commute)
739 subsection {* Generalized summation over a set *}
742 setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
743 "setsum f A == if finite A then fold (op + o f) 0 A else 0"
746 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_:_. _" [0, 51, 10] 10)
748 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
750 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
752 "\<Sum>i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *}
755 lemma setsum_empty [simp]: "setsum f {} = 0"
756 by (simp add: setsum_def)
758 lemma setsum_insert [simp]:
759 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
760 by (simp add: setsum_def
761 LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
763 lemma setsum_reindex [rule_format]: "finite B ==>
764 inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
765 apply (rule finite_induct, assumption, force)
766 apply (rule impI, auto)
767 apply (simp add: inj_on_def)
768 apply (subgoal_tac "f x \<notin> f ` F")
769 apply (subgoal_tac "finite (f ` F)")
770 apply (auto simp add: setsum_insert)
771 apply (simp add: inj_on_def)
774 lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
775 setsum f B = setsum id (f ` B)"
776 by (auto simp add: setsum_reindex id_o)
778 lemma setsum_reindex_cong: "finite A ==> inj_on f A ==>
779 B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
780 by (frule setsum_reindex, assumption, simp)
783 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
784 apply (case_tac "finite B")
785 prefer 2 apply (simp add: setsum_def, simp)
786 apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
788 apply (erule finite_induct, simp)
789 apply (simp add: subset_insert_iff, clarify)
790 apply (subgoal_tac "finite C")
791 prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
792 apply (subgoal_tac "C = insert x (C - {x})")
796 apply (erule (1) notE impE)
797 apply (simp add: Ball_def del:insert_Diff_single)
800 lemma setsum_0: "setsum (%i. 0) A = 0"
801 apply (case_tac "finite A")
802 prefer 2 apply (simp add: setsum_def)
803 apply (erule finite_induct, auto)
806 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
807 apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
808 apply (erule ssubst, rule setsum_0)
809 apply (rule setsum_cong, auto)
812 lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
813 -- {* Could allow many @{text "card"} proofs to be simplified. *}
814 by (induct set: Finites) auto
816 lemma setsum_Un_Int: "finite A ==> finite B
817 ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
818 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
819 apply (induct set: Finites, simp)
820 apply (simp add: plus_ac0 Int_insert_left insert_absorb)
823 lemma setsum_Un_disjoint: "finite A ==> finite B
824 ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
825 apply (subst setsum_Un_Int [symmetric], auto)
828 lemma setsum_UN_disjoint:
829 "finite I ==> (ALL i:I. finite (A i)) ==>
830 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
831 setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
832 apply (induct set: Finites, simp, atomize)
833 apply (subgoal_tac "ALL i:F. x \<noteq> i")
835 apply (subgoal_tac "A x Int UNION F A = {}")
837 apply (simp add: setsum_Un_disjoint)
840 lemma setsum_Union_disjoint:
841 "finite C ==> (ALL A:C. finite A) ==>
842 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
843 setsum f (Union C) = setsum (setsum f) C"
844 apply (frule setsum_UN_disjoint [of C id f])
845 apply (unfold Union_def id_def, assumption+)
848 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
849 (\<Sum> x:A. (\<Sum> y:B x. f x y)) =
850 (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
851 apply (subst Sigma_def)
852 apply (subst setsum_UN_disjoint)
855 apply (drule_tac x = i in bspec, assumption)
856 apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
857 apply (rule finite_surj)
859 apply (rule setsum_cong, rule refl)
860 apply (subst setsum_UN_disjoint)
861 apply (erule bspec, assumption)
865 lemma setsum_cartesian_product: "finite A ==> finite B ==>
866 (\<Sum> x:A. (\<Sum> y:B. f x y)) =
867 (\<Sum> z:A <*> B. f (fst z) (snd z))"
868 by (erule setsum_Sigma, auto);
870 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
871 apply (case_tac "finite A")
872 prefer 2 apply (simp add: setsum_def)
873 apply (erule finite_induct, auto)
874 apply (simp add: plus_ac0)
877 subsubsection {* Properties in more restricted classes of structures *}
879 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
880 apply (case_tac "finite A")
881 prefer 2 apply (simp add: setsum_def)
883 apply (erule finite_induct, auto)
886 lemma setsum_eq_0_iff [simp]:
887 "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
888 by (induct set: Finites) auto
890 lemma setsum_constant_nat [simp]:
891 "finite A ==> (\<Sum>x: A. y) = (card A) * y"
892 -- {* Later generalized to any semiring. *}
893 by (erule finite_induct, auto)
895 lemma setsum_Un: "finite A ==> finite B ==>
896 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
897 -- {* For the natural numbers, we have subtraction. *}
898 by (subst setsum_Un_Int [symmetric], auto)
900 lemma setsum_Un_ring: "finite A ==> finite B ==>
901 (setsum f (A Un B) :: 'a :: ring) =
902 setsum f A + setsum f B - setsum f (A Int B)"
903 by (subst setsum_Un_Int [symmetric], auto)
905 lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
906 (if a:A then setsum f A - f a else setsum f A)"
907 apply (case_tac "finite A")
908 prefer 2 apply (simp add: setsum_def)
909 apply (erule finite_induct)
910 apply (auto simp add: insert_Diff_if)
911 apply (drule_tac a = a in mk_disjoint_insert, auto)
914 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
916 by (induct set: Finites, auto)
918 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
919 setsum f A - setsum g A"
920 by (simp add: diff_minus setsum_addf setsum_negf)
922 lemma setsum_nonneg: "[| finite A;
923 \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
925 apply (induct set: Finites, auto)
926 apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
927 apply (blast intro: add_mono)
930 subsubsection {* Cardinality of unions and Sigma sets *}
932 lemma card_UN_disjoint:
933 "finite I ==> (ALL i:I. finite (A i)) ==>
934 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
935 card (UNION I A) = setsum (%i. card (A i)) I"
936 apply (subst card_eq_setsum)
937 apply (subst finite_UN, assumption+)
938 apply (subgoal_tac "setsum (%i. card (A i)) I =
939 setsum (%i. (setsum (%x. 1) (A i))) I")
941 apply (erule setsum_UN_disjoint, assumption+)
942 apply (rule setsum_cong)
946 lemma card_Union_disjoint:
947 "finite C ==> (ALL A:C. finite A) ==>
948 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
949 card (Union C) = setsum card C"
950 apply (frule card_UN_disjoint [of C id])
951 apply (unfold Union_def id_def, assumption+)
954 lemma SigmaI_insert: "y \<notin> A ==>
955 (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
958 lemma card_cartesian_product_singleton: "finite A ==>
959 card({x} <*> A) = card(A)"
960 apply (subgoal_tac "inj_on (%y .(x,y)) A")
961 apply (frule card_image, assumption)
962 apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
963 apply (auto simp add: inj_on_def)
966 lemma card_SigmaI [rule_format,simp]: "finite A ==>
967 (ALL a:A. finite (B a)) -->
968 card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
969 apply (erule finite_induct, auto)
970 apply (subst SigmaI_insert, assumption)
971 apply (subst card_Un_disjoint)
972 apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
975 lemma card_cartesian_product: "[| finite A; finite B |] ==>
976 card (A <*> B) = card(A) * card(B)"
980 subsection {* Generalized product over a set *}
983 setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
984 "setprod f A == if finite A then fold (op * o f) 1 A else 1"
987 "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
988 ("\<Prod>_:_. _" [0, 51, 10] 10)
991 "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
992 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
994 "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
995 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
997 "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
1000 lemma setprod_empty [simp]: "setprod f {} = 1"
1001 by (auto simp add: setprod_def)
1003 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1004 setprod f (insert a A) = f a * setprod f A"
1005 by (auto simp add: setprod_def LC_def LC.fold_insert
1006 times_ac1_left_commute)
1008 lemma setprod_reindex [rule_format]: "finite B ==>
1009 inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
1010 apply (rule finite_induct, assumption, force)
1011 apply (rule impI, auto)
1012 apply (simp add: inj_on_def)
1013 apply (subgoal_tac "f x \<notin> f ` F")
1014 apply (subgoal_tac "finite (f ` F)")
1015 apply (auto simp add: setprod_insert)
1016 apply (simp add: inj_on_def)
1019 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
1020 setprod f B = setprod id (f ` B)"
1021 by (auto simp add: setprod_reindex id_o)
1023 lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
1024 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1025 by (frule setprod_reindex, assumption, simp)
1028 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1029 apply (case_tac "finite B")
1030 prefer 2 apply (simp add: setprod_def, simp)
1031 apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
1033 apply (erule finite_induct, simp)
1034 apply (simp add: subset_insert_iff, clarify)
1035 apply (subgoal_tac "finite C")
1036 prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
1037 apply (subgoal_tac "C = insert x (C - {x})")
1038 prefer 2 apply blast
1039 apply (erule ssubst)
1041 apply (erule (1) notE impE)
1042 apply (simp add: Ball_def del:insert_Diff_single)
1045 lemma setprod_1: "setprod (%i. 1) A = 1"
1046 apply (case_tac "finite A")
1047 apply (erule finite_induct, auto simp add: times_ac1)
1048 apply (simp add: setprod_def)
1051 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
1052 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
1053 apply (erule ssubst, rule setprod_1)
1054 apply (rule setprod_cong, auto)
1057 lemma setprod_Un_Int: "finite A ==> finite B
1058 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1059 apply (induct set: Finites, simp)
1060 apply (simp add: times_ac1 insert_absorb)
1061 apply (simp add: times_ac1 Int_insert_left insert_absorb)
1064 lemma setprod_Un_disjoint: "finite A ==> finite B
1065 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1066 apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
1069 lemma setprod_UN_disjoint:
1070 "finite I ==> (ALL i:I. finite (A i)) ==>
1071 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1072 setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1073 apply (induct set: Finites, simp, atomize)
1074 apply (subgoal_tac "ALL i:F. x \<noteq> i")
1075 prefer 2 apply blast
1076 apply (subgoal_tac "A x Int UNION F A = {}")
1077 prefer 2 apply blast
1078 apply (simp add: setprod_Un_disjoint)
1081 lemma setprod_Union_disjoint:
1082 "finite C ==> (ALL A:C. finite A) ==>
1083 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
1084 setprod f (Union C) = setprod (setprod f) C"
1085 apply (frule setprod_UN_disjoint [of C id f])
1086 apply (unfold Union_def id_def, assumption+)
1089 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1090 (\<Prod> x:A. (\<Prod> y: B x. f x y)) =
1091 (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
1092 apply (subst Sigma_def)
1093 apply (subst setprod_UN_disjoint)
1096 apply (drule_tac x = i in bspec, assumption)
1097 apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
1098 apply (rule finite_surj)
1100 apply (rule setprod_cong, rule refl)
1101 apply (subst setprod_UN_disjoint)
1102 apply (erule bspec, assumption)
1106 lemma setprod_cartesian_product: "finite A ==> finite B ==>
1107 (\<Prod> x:A. (\<Prod> y: B. f x y)) =
1108 (\<Prod> z:(A <*> B). f (fst z) (snd z))"
1109 by (erule setprod_Sigma, auto)
1111 lemma setprod_timesf: "setprod (%x. f x * g x) A =
1112 (setprod f A * setprod g A)"
1113 apply (case_tac "finite A")
1114 prefer 2 apply (simp add: setprod_def times_ac1)
1115 apply (erule finite_induct, auto)
1116 apply (simp add: times_ac1)
1119 subsubsection {* Properties in more restricted classes of structures *}
1121 lemma setprod_eq_1_iff [simp]:
1122 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
1123 by (induct set: Finites) auto
1125 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
1127 apply (erule finite_induct)
1128 apply (auto simp add: power_Suc)
1131 lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
1133 apply (induct set: Finites, force, clarsimp)
1134 apply (erule disjE, auto)
1137 lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
1138 --> 0 \<le> setprod f A"
1139 apply (case_tac "finite A")
1140 apply (induct set: Finites, force, clarsimp)
1141 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
1142 apply (rule mult_mono, assumption+)
1143 apply (auto simp add: setprod_def)
1146 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
1147 --> 0 < setprod f A"
1148 apply (case_tac "finite A")
1149 apply (induct set: Finites, force, clarsimp)
1150 apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
1151 apply (rule mult_strict_mono, assumption+)
1152 apply (auto simp add: setprod_def)
1155 lemma setprod_nonzero [rule_format]:
1156 "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
1157 finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
1158 apply (erule finite_induct, auto)
1161 lemma setprod_zero_eq:
1162 "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
1163 finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
1164 apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
1167 lemma setprod_nonzero_field:
1168 "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
1169 apply (rule setprod_nonzero, auto)
1172 lemma setprod_zero_eq_field:
1173 "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
1174 apply (rule setprod_zero_eq, auto)
1177 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1178 (setprod f (A Un B) :: 'a ::{field})
1179 = setprod f A * setprod f B / setprod f (A Int B)"
1180 apply (subst setprod_Un_Int [symmetric], auto)
1181 apply (subgoal_tac "finite (A Int B)")
1182 apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
1183 apply (subst times_divide_eq_right [THEN sym], auto)
1186 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1187 (setprod f (A - {a}) :: 'a :: {field}) =
1188 (if a:A then setprod f A / f a else setprod f A)"
1189 apply (erule finite_induct)
1190 apply (auto simp add: insert_Diff_if)
1191 apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
1192 apply (erule ssubst)
1193 apply (subst times_divide_eq_right [THEN sym])
1194 apply (auto simp add: mult_ac)
1197 lemma setprod_inversef: "finite A ==>
1198 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
1199 setprod (inverse \<circ> f) A = inverse (setprod f A)"
1200 apply (erule finite_induct)
1204 lemma setprod_dividef:
1206 \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
1207 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1209 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1210 apply (erule ssubst)
1211 apply (subst divide_inverse)
1212 apply (subst setprod_timesf)
1213 apply (subst setprod_inversef, assumption+, rule refl)
1214 apply (rule setprod_cong, rule refl)
1215 apply (subst divide_inverse, auto)
1219 subsection{* Min and Max of finite linearly ordered sets *}
1221 text{* Seemed easier to define directly than via fold. *}
1223 lemma ex_Max: fixes S :: "('a::linorder)set"
1224 assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
1227 case empty thus ?case by simp
1232 assume "S = {}" thus ?thesis by simp
1234 assume nonempty: "S \<noteq> {}"
1235 then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
1238 assume "x \<le> m" thus ?thesis using m by blast
1240 assume "~ x \<le> m" thus ?thesis using m
1241 by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
1246 lemma ex_Min: fixes S :: "('a::linorder)set"
1247 assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
1250 case empty thus ?case by simp
1255 assume "S = {}" thus ?thesis by simp
1257 assume nonempty: "S \<noteq> {}"
1258 then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
1261 assume "m \<le> x" thus ?thesis using m by blast
1263 assume "~ m \<le> x" thus ?thesis using m
1264 by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
1270 Min :: "('a::linorder)set => 'a"
1271 "Min S == THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
1273 Max :: "('a::linorder)set => 'a"
1274 "Max S == THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
1276 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
1277 shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
1278 proof (unfold Min_def, rule theI')
1279 show "\<exists>!m. ?P m"
1280 proof (rule ex_ex1I)
1281 show "\<exists>m. ?P m" using ex_Min[OF a] by blast
1283 fix m1 m2 assume "?P m1" "?P m2"
1284 thus "m1 = m2" by (blast dest:order_antisym)
1288 lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
1289 shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
1290 proof (unfold Max_def, rule theI')
1291 show "\<exists>!m. ?P m"
1292 proof (rule ex_ex1I)
1293 show "\<exists>m. ?P m" using ex_Max[OF a] by blast
1295 fix m1 m2 assume "?P m1" "?P m2"
1296 thus "m1 = m2" by (blast dest:order_antisym)
1300 subsection {* Theorems about @{text "choose"} *}
1303 \medskip Basic theorem about @{text "choose"}. By Florian
1304 Kammüller, tidied by LCP.
1307 lemma card_s_0_eq_empty:
1308 "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
1309 apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
1310 apply (simp cong add: rev_conj_cong)
1313 lemma choose_deconstruct: "finite M ==> x \<notin> M
1314 ==> {s. s <= insert x M & card(s) = Suc k}
1315 = {s. s <= M & card(s) = Suc k} Un
1316 {s. EX t. t <= M & card(t) = k & s = insert x t}"
1318 apply (auto intro: finite_subset [THEN card_insert_disjoint])
1319 apply (drule_tac x = "xa - {x}" in spec)
1320 apply (subgoal_tac "x \<notin> xa", auto)
1321 apply (erule rev_mp, subst card_Diff_singleton)
1322 apply (auto intro: finite_subset)
1325 lemma card_inj_on_le:
1326 "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
1327 by (auto intro: card_mono simp add: card_image [symmetric])
1330 "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
1331 finite A; finite B |] ==> card A = card B"
1332 by (auto intro: le_anti_sym card_inj_on_le)
1334 text{*There are as many subsets of @{term A} having cardinality @{term k}
1335 as there are sets obtained from the former by inserting a fixed element
1336 @{term x} into each.*}
1338 "[|finite A; x \<notin> A|] ==>
1339 card {B. EX C. C <= A & card(C) = k & B = insert x C} =
1340 card {B. B <= A & card(B) = k}"
1341 apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
1342 apply (auto elim!: equalityE simp add: inj_on_def)
1343 apply (subst Diff_insert0, auto)
1344 txt {* finiteness of the two sets *}
1345 apply (rule_tac [2] B = "Pow (A)" in finite_subset)
1346 apply (rule_tac B = "Pow (insert x A)" in finite_subset)
1351 Main theorem: combinatorial statement about number of subsets of a set.
1355 "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1357 apply (simp add: card_s_0_eq_empty, atomize)
1358 apply (rotate_tac -1, erule finite_induct)
1359 apply (simp_all (no_asm_simp) cong add: conj_cong
1360 add: card_s_0_eq_empty choose_deconstruct)
1361 apply (subst card_Un_disjoint)
1362 prefer 4 apply (force simp add: constr_bij)
1363 prefer 3 apply force
1364 prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
1365 finite_subset [of _ "Pow (insert x F)", standard])
1366 apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
1370 "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1371 by (simp add: n_sub_lemma)