src/HOL/Finite_Set.thy
 author paulson Tue Dec 14 10:45:16 2004 +0100 (2004-12-14) changeset 15409 a063687d24eb parent 15402 97204f3b4705 child 15447 177ffdbabf80 permissions -rw-r--r--
new and stronger lemmas and improved simplification for finite sets
1 (*  Title:      HOL/Finite_Set.thy
2     ID:         \$Id\$
3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
6 Get rid of a couple of superfluous finiteness assumptions in lemmas
7 about setsum and card - see FIXME.
8 NB: the analogous lemmas for setprod should also be simplified!
9 *)
11 header {* Finite sets *}
13 theory Finite_Set
14 imports Divides Power Inductive
15 begin
17 subsection {* Definition and basic properties *}
19 consts Finites :: "'a set set"
20 syntax
21   finite :: "'a set => bool"
22 translations
23   "finite A" == "A : Finites"
25 inductive Finites
26   intros
27     emptyI [simp, intro!]: "{} : Finites"
28     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
30 axclass finite \<subseteq> type
31   finite: "finite UNIV"
33 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
34   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
35   shows "\<exists>a::'a. a \<notin> A"
36 proof -
37   from prems have "A \<noteq> UNIV" by blast
38   thus ?thesis by blast
39 qed
41 lemma finite_induct [case_names empty insert, induct set: Finites]:
42   "finite F ==>
43     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
44   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
45 proof -
46   assume "P {}" and
47     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
48   assume "finite F"
49   thus "P F"
50   proof induct
51     show "P {}" .
52     fix x F assume F: "finite F" and P: "P F"
53     show "P (insert x F)"
54     proof cases
55       assume "x \<in> F"
56       hence "insert x F = F" by (rule insert_absorb)
57       with P show ?thesis by (simp only:)
58     next
59       assume "x \<notin> F"
60       from F this P show ?thesis by (rule insert)
61     qed
62   qed
63 qed
65 lemma finite_subset_induct [consumes 2, case_names empty insert]:
66   "finite F ==> F \<subseteq> A ==>
67     P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
68     P F"
69 proof -
70   assume "P {}" and insert:
71     "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
72   assume "finite F"
73   thus "F \<subseteq> A ==> P F"
74   proof induct
75     show "P {}" .
76     fix x F assume "finite F" and "x \<notin> F"
77       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
78     show "P (insert x F)"
79     proof (rule insert)
80       from i show "x \<in> A" by blast
81       from i have "F \<subseteq> A" by blast
82       with P show "P F" .
83     qed
84   qed
85 qed
87 text{* Finite sets are the images of initial segments of natural numbers: *}
89 lemma finite_imp_nat_seg_image:
90 assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
91 using fin
92 proof induct
93   case empty
94   show ?case
95   proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
96 next
97   case (insert a A)
98   from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
99   hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
100     by (auto simp add:image_def Ball_def)
101   thus ?case by blast
102 qed
104 lemma nat_seg_image_imp_finite:
105   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
106 proof (induct n)
107   case 0 thus ?case by simp
108 next
109   case (Suc n)
110   let ?B = "f ` {i. i < n}"
111   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
112   show ?case
113   proof cases
114     assume "\<exists>k<n. f n = f k"
115     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
116     thus ?thesis using finB by simp
117   next
118     assume "\<not>(\<exists> k<n. f n = f k)"
119     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
120     thus ?thesis using finB by simp
121   qed
122 qed
124 lemma finite_conv_nat_seg_image:
125   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
126 by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
128 subsubsection{* Finiteness and set theoretic constructions *}
130 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
131   -- {* The union of two finite sets is finite. *}
132   by (induct set: Finites) simp_all
134 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
135   -- {* Every subset of a finite set is finite. *}
136 proof -
137   assume "finite B"
138   thus "!!A. A \<subseteq> B ==> finite A"
139   proof induct
140     case empty
141     thus ?case by simp
142   next
143     case (insert x F A)
144     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
145     show "finite A"
146     proof cases
147       assume x: "x \<in> A"
148       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
149       with r have "finite (A - {x})" .
150       hence "finite (insert x (A - {x}))" ..
151       also have "insert x (A - {x}) = A" by (rule insert_Diff)
152       finally show ?thesis .
153     next
154       show "A \<subseteq> F ==> ?thesis" .
155       assume "x \<notin> A"
156       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
157     qed
158   qed
159 qed
161 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
162   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
164 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
165   -- {* The converse obviously fails. *}
166   by (blast intro: finite_subset)
168 lemma finite_insert [simp]: "finite (insert a A) = finite A"
169   apply (subst insert_is_Un)
170   apply (simp only: finite_Un, blast)
171   done
173 lemma finite_Union[simp, intro]:
174  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
175 by (induct rule:finite_induct) simp_all
177 lemma finite_empty_induct:
178   "finite A ==>
179   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
180 proof -
181   assume "finite A"
182     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
183   have "P (A - A)"
184   proof -
185     fix c b :: "'a set"
186     presume c: "finite c" and b: "finite b"
187       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
188     from c show "c \<subseteq> b ==> P (b - c)"
189     proof induct
190       case empty
191       from P1 show ?case by simp
192     next
193       case (insert x F)
194       have "P (b - F - {x})"
195       proof (rule P2)
196         from _ b show "finite (b - F)" by (rule finite_subset) blast
197         from insert show "x \<in> b - F" by simp
198         from insert show "P (b - F)" by simp
199       qed
200       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
201       finally show ?case .
202     qed
203   next
204     show "A \<subseteq> A" ..
205   qed
206   thus "P {}" by simp
207 qed
209 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
210   by (rule Diff_subset [THEN finite_subset])
212 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
213   apply (subst Diff_insert)
214   apply (case_tac "a : A - B")
215    apply (rule finite_insert [symmetric, THEN trans])
216    apply (subst insert_Diff, simp_all)
217   done
220 text {* Image and Inverse Image over Finite Sets *}
222 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
223   -- {* The image of a finite set is finite. *}
224   by (induct set: Finites) simp_all
226 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
227   apply (frule finite_imageI)
228   apply (erule finite_subset, assumption)
229   done
231 lemma finite_range_imageI:
232     "finite (range g) ==> finite (range (%x. f (g x)))"
233   apply (drule finite_imageI, simp)
234   done
236 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
237 proof -
238   have aux: "!!A. finite (A - {}) = finite A" by simp
239   fix B :: "'a set"
240   assume "finite B"
241   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
242     apply induct
243      apply simp
244     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
245      apply clarify
246      apply (simp (no_asm_use) add: inj_on_def)
247      apply (blast dest!: aux [THEN iffD1], atomize)
248     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
249     apply (frule subsetD [OF equalityD2 insertI1], clarify)
250     apply (rule_tac x = xa in bexI)
252     done
253 qed (rule refl)
256 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
257   -- {* The inverse image of a singleton under an injective function
258          is included in a singleton. *}
259   apply (auto simp add: inj_on_def)
260   apply (blast intro: the_equality [symmetric])
261   done
263 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
264   -- {* The inverse image of a finite set under an injective function
265          is finite. *}
266   apply (induct set: Finites, simp_all)
267   apply (subst vimage_insert)
268   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
269   done
272 text {* The finite UNION of finite sets *}
274 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
275   by (induct set: Finites) simp_all
277 text {*
278   Strengthen RHS to
279   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
281   We'd need to prove
282   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
283   by induction. *}
285 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
286   by (blast intro: finite_UN_I finite_subset)
289 text {* Sigma of finite sets *}
291 lemma finite_SigmaI [simp]:
292     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
293   by (unfold Sigma_def) (blast intro!: finite_UN_I)
295 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
296     finite (A <*> B)"
297   by (rule finite_SigmaI)
299 lemma finite_Prod_UNIV:
300     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
301   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
302    apply (erule ssubst)
303    apply (erule finite_SigmaI, auto)
304   done
306 lemma finite_cartesian_productD1:
307      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
308 apply (auto simp add: finite_conv_nat_seg_image)
309 apply (drule_tac x=n in spec)
310 apply (drule_tac x="fst o f" in spec)
311 apply (auto simp add: o_def)
312  prefer 2 apply (force dest!: equalityD2)
313 apply (drule equalityD1)
314 apply (rename_tac y x)
315 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
316  prefer 2 apply force
317 apply clarify
318 apply (rule_tac x=k in image_eqI, auto)
319 done
321 lemma finite_cartesian_productD2:
322      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
323 apply (auto simp add: finite_conv_nat_seg_image)
324 apply (drule_tac x=n in spec)
325 apply (drule_tac x="snd o f" in spec)
326 apply (auto simp add: o_def)
327  prefer 2 apply (force dest!: equalityD2)
328 apply (drule equalityD1)
329 apply (rename_tac x y)
330 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
331  prefer 2 apply force
332 apply clarify
333 apply (rule_tac x=k in image_eqI, auto)
334 done
337 instance unit :: finite
338 proof
339   have "finite {()}" by simp
340   also have "{()} = UNIV" by auto
341   finally show "finite (UNIV :: unit set)" .
342 qed
344 instance * :: (finite, finite) finite
345 proof
346   show "finite (UNIV :: ('a \<times> 'b) set)"
347   proof (rule finite_Prod_UNIV)
348     show "finite (UNIV :: 'a set)" by (rule finite)
349     show "finite (UNIV :: 'b set)" by (rule finite)
350   qed
351 qed
354 text {* The powerset of a finite set *}
356 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
357 proof
358   assume "finite (Pow A)"
359   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
360   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
361 next
362   assume "finite A"
363   thus "finite (Pow A)"
364     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
365 qed
368 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
369 by(blast intro: finite_subset[OF subset_Pow_Union])
372 lemma finite_converse [iff]: "finite (r^-1) = finite r"
373   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
374    apply simp
375    apply (rule iffI)
376     apply (erule finite_imageD [unfolded inj_on_def])
377     apply (simp split add: split_split)
378    apply (erule finite_imageI)
379   apply (simp add: converse_def image_def, auto)
380   apply (rule bexI)
381    prefer 2 apply assumption
382   apply simp
383   done
386 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
387 Ehmety) *}
389 lemma finite_Field: "finite r ==> finite (Field r)"
390   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
391   apply (induct set: Finites)
392    apply (auto simp add: Field_def Domain_insert Range_insert)
393   done
395 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
396   apply clarify
397   apply (erule trancl_induct)
398    apply (auto simp add: Field_def)
399   done
401 lemma finite_trancl: "finite (r^+) = finite r"
402   apply auto
403    prefer 2
404    apply (rule trancl_subset_Field2 [THEN finite_subset])
405    apply (rule finite_SigmaI)
406     prefer 3
407     apply (blast intro: r_into_trancl' finite_subset)
408    apply (auto simp add: finite_Field)
409   done
412 subsection {* A fold functional for finite sets *}
414 text {* The intended behaviour is
415 @{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"}
416 if @{text f} is associative-commutative. For an application of @{text fold}
417 se the definitions of sums and products over finite sets.
418 *}
420 consts
421   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
423 inductive "foldSet f g e"
424 intros
425 emptyI [intro]: "({}, e) : foldSet f g e"
426 insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk>
427  \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e"
429 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e"
431 constdefs
432   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
433   "fold f g e A == THE x. (A, x) : foldSet f g e"
435 lemma Diff1_foldSet:
436   "(A - {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e"
437 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
439 lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A"
440   by (induct set: foldSet) auto
442 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e"
443   by (induct set: Finites) auto
446 subsubsection {* Commutative monoids *}
448 locale ACf =
449   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
450   assumes commute: "x \<cdot> y = y \<cdot> x"
451     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
453 locale ACe = ACf +
454   fixes e :: 'a
455   assumes ident [simp]: "x \<cdot> e = x"
457 lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
458 proof -
459   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
460   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
461   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
462   finally show ?thesis .
463 qed
465 lemmas (in ACf) AC = assoc commute left_commute
467 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
468 proof -
469   have "x \<cdot> e = x" by (rule ident)
470   thus ?thesis by (subst commute)
471 qed
473 text{* Instantiation of locales: *}
475 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
479 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
482 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
483 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
485 lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
486 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
489 subsubsection{*From @{term foldSet} to @{term fold}*}
491 lemma (in ACf) foldSet_determ_aux:
492   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
493    \<Longrightarrow> x' = x"
494 proof (induct n)
495   case 0 thus ?case by auto
496 next
497   case (Suc n)
498   have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
499            \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
500   and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
501   show ?case
502   proof cases
503     assume "EX k<n. h n = h k"
504     hence card': "A = h ` {i. i < n}"
505       using card by (auto simp:image_def less_Suc_eq)
506     show ?thesis by(rule IH[OF card' Afoldx Afoldy])
507   next
508     assume new: "\<not>(EX k<n. h n = h k)"
509     show ?thesis
510     proof (rule foldSet.cases[OF Afoldx])
511       assume "(A, x) = ({}, e)"
512       thus "x' = x" using Afoldy by (auto)
513     next
514       fix B b y
515       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
516 	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
517       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
518       show ?thesis
519       proof (rule foldSet.cases[OF Afoldy])
520 	assume "(A,x') = ({}, e)"
521 	thus ?thesis using A1 by auto
522       next
523 	fix C c z
524 	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
525 	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
526 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
527 	let ?h = "%i. if h i = b then h n else h i"
528 	have less: "B = ?h`{i. i<n}" (is "_ = ?r")
529 	proof
530 	  show "B \<subseteq> ?r"
531 	  proof
532 	    fix u assume "u \<in> B"
533 	    hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
534 	    then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
535 	      using card by(auto simp:image_def)
536 	    show "u \<in> ?r"
537 	    proof cases
538 	      assume "i\<^isub>u < n"
539 	      thus ?thesis using unotb by(fastsimp)
540 	    next
541 	      assume "\<not> i\<^isub>u < n"
542 	      with below have [simp]: "i\<^isub>u = n" by arith
543 	      obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
544 		using A1 card by blast
545 	      have "i\<^isub>k < n"
546 	      proof (rule ccontr)
547 		assume "\<not> i\<^isub>k < n"
548 		hence "i\<^isub>k = n" using i\<^isub>k by arith
549 		thus False using unotb by simp
550 	      qed
551 	      thus ?thesis by(auto simp add:image_def)
552 	    qed
553 	  qed
554 	next
555 	  show "?r \<subseteq> B"
556 	  proof
557 	    fix u assume "u \<in> ?r"
558 	    then obtain i\<^isub>u where below: "i\<^isub>u < n" and
559               or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
560 	      by(auto simp:image_def)
561 	    from or show "u \<in> B"
562 	    proof
563 	      assume [simp]: "b = h i\<^isub>u \<and> u = h n"
564 	      have "u \<in> A" using card by auto
565               moreover have "u \<noteq> b" using new below by auto
566 	      ultimately show "u \<in> B" using A1 by blast
567 	    next
568 	      assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
569 	      moreover hence "u \<in> A" using card below by auto
570 	      ultimately show "u \<in> B" using A1 by blast
571 	    qed
572 	  qed
573 	qed
574 	show ?thesis
575 	proof cases
576 	  assume "b = c"
577 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
578 	  ultimately show ?thesis using IH[OF less] y z x x' by auto
579 	next
580 	  assume diff: "b \<noteq> c"
581 	  let ?D = "B - {c}"
582 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
583 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
584 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
585 	  with A1 have "finite ?D" by simp
586 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
587 	    using finite_imp_foldSet by rules
588 	  moreover have cinB: "c \<in> B" using B by(auto)
589 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
590 	    by(rule Diff1_foldSet)
591 	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
592           moreover have "g b \<cdot> d = z"
593 	  proof (rule IH[OF _ z])
594 	    let ?h = "%i. if h i = c then h n else h i"
595 	    show "C = ?h`{i. i<n}" (is "_ = ?r")
596 	    proof
597 	      show "C \<subseteq> ?r"
598 	      proof
599 		fix u assume "u \<in> C"
600 		hence uinA: "u \<in> A" and unotc: "u \<noteq> c"
601 		  using A2 notinC by blast+
602 		then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
603 		  using card by(auto simp:image_def)
604 		show "u \<in> ?r"
605 		proof cases
606 		  assume "i\<^isub>u < n"
607 		  thus ?thesis using unotc by(fastsimp)
608 		next
609 		  assume "\<not> i\<^isub>u < n"
610 		  with below have [simp]: "i\<^isub>u = n" by arith
611 		  obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k"
612 		    using A2 card by blast
613 		  have "i\<^isub>k < n"
614 		  proof (rule ccontr)
615 		    assume "\<not> i\<^isub>k < n"
616 		    hence "i\<^isub>k = n" using i\<^isub>k by arith
617 		    thus False using unotc by simp
618 		  qed
619 		  thus ?thesis by(auto simp add:image_def)
620 		qed
621 	      qed
622 	    next
623 	      show "?r \<subseteq> C"
624 	      proof
625 		fix u assume "u \<in> ?r"
626 		then obtain i\<^isub>u where below: "i\<^isub>u < n" and
627 		  or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
628 		  by(auto simp:image_def)
629 		from or show "u \<in> C"
630 		proof
631 		  assume [simp]: "c = h i\<^isub>u \<and> u = h n"
632 		  have "u \<in> A" using card by auto
633 		  moreover have "u \<noteq> c" using new below by auto
634 		  ultimately show "u \<in> C" using A2 by blast
635 		next
636 		  assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
637 		  moreover hence "u \<in> A" using card below by auto
638 		  ultimately show "u \<in> C" using A2 by blast
639 		qed
640 	      qed
641 	    qed
642 	  next
643 	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
644 	      by fastsimp
645 	  qed
646 	  ultimately show ?thesis using x x' by(auto simp:AC)
647 	qed
648       qed
649     qed
650   qed
651 qed
653 (* The same proof, but using card
654 lemma (in ACf) foldSet_determ_aux:
655   "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
656    \<Longrightarrow> x' = x"
657 proof (induct n)
658   case 0 thus ?case by simp
659 next
660   case (Suc n)
661   have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
662            \<Longrightarrow> x' = x" and card: "card A < Suc n"
663   and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
664   from card have "card A < n \<or> card A = n" by arith
665   thus ?case
666   proof
667     assume less: "card A < n"
668     show ?thesis by(rule IH[OF less Afoldx Afoldy])
669   next
670     assume cardA: "card A = n"
671     show ?thesis
672     proof (rule foldSet.cases[OF Afoldx])
673       assume "(A, x) = ({}, e)"
674       thus "x' = x" using Afoldy by (auto)
675     next
676       fix B b y
677       assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
678 	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
679       hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
680       show ?thesis
681       proof (rule foldSet.cases[OF Afoldy])
682 	assume "(A,x') = ({}, e)"
683 	thus ?thesis using A1 by auto
684       next
685 	fix C c z
686 	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
687 	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
688 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
689 	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
690 	with cardA A1 notinB have less: "card B < n" by simp
691 	show ?thesis
692 	proof cases
693 	  assume "b = c"
694 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
695 	  ultimately show ?thesis using IH[OF less] y z x x' by auto
696 	next
697 	  assume diff: "b \<noteq> c"
698 	  let ?D = "B - {c}"
699 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
700 	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
701 	  have "finite ?D" using finA A1 by simp
702 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
703 	    using finite_imp_foldSet by rules
704 	  moreover have cinB: "c \<in> B" using B by(auto)
705 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
706 	    by(rule Diff1_foldSet)
707 	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
708           moreover have "g b \<cdot> d = z"
709 	  proof (rule IH[OF _ z])
710 	    show "card C < n" using C cardA A1 notinB finA cinB
711 	      by(auto simp:card_Diff1_less)
712 	  next
713 	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
714 	      by fastsimp
715 	  qed
716 	  ultimately show ?thesis using x x' by(auto simp:AC)
717 	qed
718       qed
719     qed
720   qed
721 qed
722 *)
724 lemma (in ACf) foldSet_determ:
725   "(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x"
726 apply(frule foldSet_imp_finite)
728 apply(blast intro: foldSet_determ_aux [rule_format])
729 done
731 lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y"
732   by (unfold fold_def) (blast intro: foldSet_determ)
734 text{* The base case for @{text fold}: *}
736 lemma fold_empty [simp]: "fold f g e {} = e"
737   by (unfold fold_def) blast
739 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
740     ((insert x A, v) : foldSet f g e) =
741     (EX y. (A, y) : foldSet f g e & v = f (g x) y)"
742   apply auto
743   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
744    apply (fastsimp dest: foldSet_imp_finite)
745   apply (blast intro: foldSet_determ)
746   done
748 text{* The recursion equation for @{text fold}: *}
750 lemma (in ACf) fold_insert[simp]:
751     "finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)"
752   apply (unfold fold_def)
754   apply (rule the_equality)
755   apply (auto intro: finite_imp_foldSet
757   done
759 declare
760   empty_foldSetE [rule del]  foldSet.intros [rule del]
761   -- {* Delete rules to do with @{text foldSet} relation. *}
765 lemma (in ACf) fold_commute:
766   "finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)"
767   apply (induct set: Finites, simp)
769   done
771 lemma (in ACf) fold_nest_Un_Int:
772   "finite A ==> finite B
773     ==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)"
774   apply (induct set: Finites, simp)
775   apply (simp add: fold_commute Int_insert_left insert_absorb)
776   done
778 lemma (in ACf) fold_nest_Un_disjoint:
779   "finite A ==> finite B ==> A Int B = {}
780     ==> fold f g e (A Un B) = fold f g (fold f g e B) A"
783 lemma (in ACf) fold_reindex:
784 assumes fin: "finite B"
785 shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B"
786 using fin apply (induct)
787  apply simp
788 apply simp
789 done
791 lemma (in ACe) fold_Un_Int:
792   "finite A ==> finite B ==>
793     fold f g e A \<cdot> fold f g e B =
794     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
795   apply (induct set: Finites, simp)
796   apply (simp add: AC insert_absorb Int_insert_left)
797   done
799 corollary (in ACe) fold_Un_disjoint:
800   "finite A ==> finite B ==> A Int B = {} ==>
801     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
804 lemma (in ACe) fold_UN_disjoint:
805   "\<lbrakk> finite I; ALL i:I. finite (A i);
806      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
807    \<Longrightarrow> fold f g e (UNION I A) =
808        fold f (%i. fold f g e (A i)) e I"
809   apply (induct set: Finites, simp, atomize)
810   apply (subgoal_tac "ALL i:F. x \<noteq> i")
811    prefer 2 apply blast
812   apply (subgoal_tac "A x Int UNION F A = {}")
813    prefer 2 apply blast
815   done
817 lemma (in ACf) fold_cong:
818   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A"
819   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g a C = fold f h a C")
820    apply simp
821   apply (erule finite_induct, simp)
822   apply (simp add: subset_insert_iff, clarify)
823   apply (subgoal_tac "finite C")
824    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
825   apply (subgoal_tac "C = insert x (C - {x})")
826    prefer 2 apply blast
827   apply (erule ssubst)
828   apply (drule spec)
829   apply (erule (1) notE impE)
830   apply (simp add: Ball_def del: insert_Diff_single)
831   done
833 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
834   fold f (%x. fold f (g x) e (B x)) e A =
835   fold f (split g) e (SIGMA x:A. B x)"
836 apply (subst Sigma_def)
837 apply (subst fold_UN_disjoint)
838    apply assumption
839   apply simp
840  apply blast
841 apply (erule fold_cong)
842 apply (subst fold_UN_disjoint)
843    apply simp
844   apply simp
845  apply blast
846 apply (simp)
847 done
849 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
850    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
851 apply (erule finite_induct)
852  apply simp
854 done
857 subsection {* Generalized summation over a set *}
859 constdefs
860   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
861   "setsum f A == if finite A then fold (op +) f 0 A else 0"
863 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
864 written @{text"\<Sum>x\<in>A. e"}. *}
866 syntax
867   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
868 syntax (xsymbols)
869   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
870 syntax (HTML output)
871   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
873 translations -- {* Beware of argument permutation! *}
874   "SUM i:A. b" == "setsum (%i. b) A"
875   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
877 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
878  @{text"\<Sum>x|P. e"}. *}
880 syntax
881   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
882 syntax (xsymbols)
883   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
884 syntax (HTML output)
885   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
887 translations
888   "SUM x|P. t" => "setsum (%x. t) {x. P}"
889   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
891 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
893 syntax
894   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
896 parse_translation {*
897   let
898     fun Setsum_tr [A] = Syntax.const "setsum" \$ Abs ("", dummyT, Bound 0) \$ A
899   in [("_Setsum", Setsum_tr)] end;
900 *}
902 print_translation {*
903 let
904   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" \$ A
905     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
906        if x<>y then raise Match
907        else let val x' = Syntax.mark_bound x
908                 val t' = subst_bound(x',t)
909                 val P' = subst_bound(x',P)
910             in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end
911 in
912 [("setsum", setsum_tr')]
913 end
914 *}
916 lemma setsum_empty [simp]: "setsum f {} = 0"
919 lemma setsum_insert [simp]:
920     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
923 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
926 lemma setsum_reindex:
927      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
930 lemma setsum_reindex_id:
931      "inj_on f B ==> setsum f B = setsum id (f ` B)"
932 by (auto simp add: setsum_reindex)
934 lemma setsum_cong:
935   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
936 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
938 lemma setsum_reindex_cong:
939      "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|]
940       ==> setsum h B = setsum g A"
941   by (simp add: setsum_reindex cong: setsum_cong)
943 lemma setsum_0: "setsum (%i. 0) A = 0"
944 apply (clarsimp simp: setsum_def)
945 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
946 done
948 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
949   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
950   apply (erule ssubst, rule setsum_0)
951   apply (rule setsum_cong, auto)
952   done
954 lemma setsum_Un_Int: "finite A ==> finite B ==>
955   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
956   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
959 lemma setsum_Un_disjoint: "finite A ==> finite B
960   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
961 by (subst setsum_Un_Int [symmetric], auto)
963 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
964   the lhs need not be, since UNION I A could still be finite.*)
965 lemma setsum_UN_disjoint:
966     "finite I ==> (ALL i:I. finite (A i)) ==>
967         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
968       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
971 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
972 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
973 lemma setsum_Union_disjoint:
974   "[| (ALL A:C. finite A);
975       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
976    ==> setsum f (Union C) = setsum (setsum f) C"
977 apply (cases "finite C")
978  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
979   apply (frule setsum_UN_disjoint [of C id f])
980  apply (unfold Union_def id_def, assumption+)
981 done
983 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
984   the rhs need not be, since SIGMA A B could still be finite.*)
985 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
986     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
987     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
990 text{*Here we can eliminate the finiteness assumptions, by cases.*}
991 lemma setsum_cartesian_product:
992    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
993 apply (cases "finite A")
994  apply (cases "finite B")
996  apply (cases "A={}", simp)
998 apply (auto simp add: setsum_def
999             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1000 done
1002 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
1006 subsubsection {* Properties in more restricted classes of structures *}
1008 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
1009   apply (case_tac "finite A")
1010    prefer 2 apply (simp add: setsum_def)
1011   apply (erule rev_mp)
1012   apply (erule finite_induct, auto)
1013   done
1015 lemma setsum_eq_0_iff [simp]:
1016     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
1017   by (induct set: Finites) auto
1019 lemma setsum_Un_nat: "finite A ==> finite B ==>
1020     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1021   -- {* For the natural numbers, we have subtraction. *}
1022   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
1024 lemma setsum_Un: "finite A ==> finite B ==>
1025     (setsum f (A Un B) :: 'a :: ab_group_add) =
1026       setsum f A + setsum f B - setsum f (A Int B)"
1027   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
1029 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
1030     (if a:A then setsum f A - f a else setsum f A)"
1031   apply (case_tac "finite A")
1032    prefer 2 apply (simp add: setsum_def)
1033   apply (erule finite_induct)
1034    apply (auto simp add: insert_Diff_if)
1035   apply (drule_tac a = a in mk_disjoint_insert, auto)
1036   done
1038 lemma setsum_diff1: "finite A \<Longrightarrow>
1039   (setsum f (A - {a}) :: ('a::ab_group_add)) =
1040   (if a:A then setsum f A - f a else setsum f A)"
1041   by (erule finite_induct) (auto simp add: insert_Diff_if)
1043 (* By Jeremy Siek: *)
1045 lemma setsum_diff_nat:
1046   assumes finB: "finite B"
1047   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
1048 using finB
1049 proof (induct)
1050   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
1051 next
1052   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
1053     and xFinA: "insert x F \<subseteq> A"
1054     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
1055   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
1056   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
1058   from xFinA have "F \<subseteq> A" by simp
1059   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
1060   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
1061     by simp
1062   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
1063   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
1064     by simp
1065   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
1066   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
1067     by simp
1068   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
1069 qed
1071 lemma setsum_diff:
1072   assumes le: "finite A" "B \<subseteq> A"
1073   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
1074 proof -
1075   from le have finiteB: "finite B" using finite_subset by auto
1076   show ?thesis using finiteB le
1077     proof (induct)
1078       case empty
1079       thus ?case by auto
1080     next
1081       case (insert x F)
1082       thus ?case using le finiteB
1083 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
1084     qed
1085   qed
1087 lemma setsum_mono:
1088   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
1089   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
1090 proof (cases "finite K")
1091   case True
1092   thus ?thesis using le
1093   proof (induct)
1094     case empty
1095     thus ?case by simp
1096   next
1097     case insert
1099       by force
1100   qed
1101 next
1102   case False
1103   thus ?thesis
1105 qed
1107 lemma setsum_mono2_nat:
1108   assumes fin: "finite B" and sub: "A \<subseteq> B"
1109 shows "setsum f A \<le> (setsum f B :: nat)"
1110 proof -
1111   have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
1112   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1114   also have "A \<union> (B-A) = B" using sub by blast
1115   finally show ?thesis .
1116 qed
1118 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
1119   - setsum f A"
1120   by (induct set: Finites, auto)
1122 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1123   setsum f A - setsum g A"
1126 lemma setsum_nonneg: "[| finite A;
1128     0 \<le> setsum f A";
1129   apply (induct set: Finites, auto)
1130   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
1132   done
1134 lemma setsum_nonpos: "[| finite A;
1136     setsum f A \<le> 0";
1137   apply (induct set: Finites, auto)
1138   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
1140   done
1142 lemma setsum_mult:
1143   fixes f :: "'a => ('b::semiring_0_cancel)"
1144   shows "r * setsum f A = setsum (%n. r * f n) A"
1145 proof (cases "finite A")
1146   case True
1147   thus ?thesis
1148   proof (induct)
1149     case empty thus ?case by simp
1150   next
1151     case (insert x A) thus ?case by (simp add: right_distrib)
1152   qed
1153 next
1154   case False thus ?thesis by (simp add: setsum_def)
1155 qed
1157 lemma setsum_abs:
1158   fixes f :: "'a => ('b::lordered_ab_group_abs)"
1159   assumes fin: "finite A"
1160   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
1161 using fin
1162 proof (induct)
1163   case empty thus ?case by simp
1164 next
1165   case (insert x A)
1166   thus ?case by (auto intro: abs_triangle_ineq order_trans)
1167 qed
1169 lemma setsum_abs_ge_zero:
1170   fixes f :: "'a => ('b::lordered_ab_group_abs)"
1171   assumes fin: "finite A"
1172   shows "0 \<le> setsum (%i. abs(f i)) A"
1173 using fin
1174 proof (induct)
1175   case empty thus ?case by simp
1176 next
1177   case (insert x A) thus ?case by (auto intro: order_trans)
1178 qed
1181 subsection {* Generalized product over a set *}
1183 constdefs
1184   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
1185   "setprod f A == if finite A then fold (op *) f 1 A else 1"
1187 syntax
1188   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
1190 syntax (xsymbols)
1191   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1192 syntax (HTML output)
1193   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1194 translations
1195   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
1197 syntax
1198   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
1200 parse_translation {*
1201   let
1202     fun Setprod_tr [A] = Syntax.const "setprod" \$ Abs ("", dummyT, Bound 0) \$ A
1203   in [("_Setprod", Setprod_tr)] end;
1204 *}
1205 print_translation {*
1206 let fun setprod_tr' [Abs(x,Tx,t), A] =
1207     if t = Bound 0 then Syntax.const "_Setprod" \$ A else raise Match
1208 in
1209 [("setprod", setprod_tr')]
1210 end
1211 *}
1214 lemma setprod_empty [simp]: "setprod f {} = 1"
1215   by (auto simp add: setprod_def)
1217 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1218     setprod f (insert a A) = f a * setprod f A"
1219 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
1221 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
1224 lemma setprod_reindex:
1225      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
1226 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
1228 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
1229 by (auto simp add: setprod_reindex)
1231 lemma setprod_cong:
1232   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1233 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
1235 lemma setprod_reindex_cong: "inj_on f A ==>
1236     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1237   by (frule setprod_reindex, simp)
1240 lemma setprod_1: "setprod (%i. 1) A = 1"
1241   apply (case_tac "finite A")
1242   apply (erule finite_induct, auto simp add: mult_ac)
1243   done
1245 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
1246   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
1247   apply (erule ssubst, rule setprod_1)
1248   apply (rule setprod_cong, auto)
1249   done
1251 lemma setprod_Un_Int: "finite A ==> finite B
1252     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1253 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
1255 lemma setprod_Un_disjoint: "finite A ==> finite B
1256   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1257 by (subst setprod_Un_Int [symmetric], auto)
1259 lemma setprod_UN_disjoint:
1260     "finite I ==> (ALL i:I. finite (A i)) ==>
1261         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1262       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1263 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
1265 lemma setprod_Union_disjoint:
1266   "[| (ALL A:C. finite A);
1267       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
1268    ==> setprod f (Union C) = setprod (setprod f) C"
1269 apply (cases "finite C")
1270  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
1271   apply (frule setprod_UN_disjoint [of C id f])
1272  apply (unfold Union_def id_def, assumption+)
1273 done
1275 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1276     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
1277     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
1278 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
1280 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1281 lemma setprod_cartesian_product:
1282      "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
1283 apply (cases "finite A")
1284  apply (cases "finite B")
1286  apply (cases "A={}", simp)
1288 apply (auto simp add: setprod_def
1289             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1290 done
1292 lemma setprod_timesf:
1293      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
1297 subsubsection {* Properties in more restricted classes of structures *}
1299 lemma setprod_eq_1_iff [simp]:
1300     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
1301   by (induct set: Finites) auto
1303 lemma setprod_zero:
1304      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
1305   apply (induct set: Finites, force, clarsimp)
1306   apply (erule disjE, auto)
1307   done
1309 lemma setprod_nonneg [rule_format]:
1310      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
1311   apply (case_tac "finite A")
1312   apply (induct set: Finites, force, clarsimp)
1313   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
1314   apply (rule mult_mono, assumption+)
1315   apply (auto simp add: setprod_def)
1316   done
1318 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
1319      --> 0 < setprod f A"
1320   apply (case_tac "finite A")
1321   apply (induct set: Finites, force, clarsimp)
1322   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
1323   apply (rule mult_strict_mono, assumption+)
1324   apply (auto simp add: setprod_def)
1325   done
1327 lemma setprod_nonzero [rule_format]:
1328     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
1329       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
1330   apply (erule finite_induct, auto)
1331   done
1333 lemma setprod_zero_eq:
1334     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
1335      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
1336   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
1337   done
1339 lemma setprod_nonzero_field:
1340     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
1341   apply (rule setprod_nonzero, auto)
1342   done
1344 lemma setprod_zero_eq_field:
1345     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
1346   apply (rule setprod_zero_eq, auto)
1347   done
1349 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1350     (setprod f (A Un B) :: 'a ::{field})
1351       = setprod f A * setprod f B / setprod f (A Int B)"
1352   apply (subst setprod_Un_Int [symmetric], auto)
1353   apply (subgoal_tac "finite (A Int B)")
1354   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
1355   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
1356   done
1358 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1359     (setprod f (A - {a}) :: 'a :: {field}) =
1360       (if a:A then setprod f A / f a else setprod f A)"
1361   apply (erule finite_induct)
1362    apply (auto simp add: insert_Diff_if)
1363   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
1364   apply (erule ssubst)
1365   apply (subst times_divide_eq_right [THEN sym])
1366   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
1367   done
1369 lemma setprod_inversef: "finite A ==>
1370     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
1371       setprod (inverse \<circ> f) A = inverse (setprod f A)"
1372   apply (erule finite_induct)
1373   apply (simp, simp)
1374   done
1376 lemma setprod_dividef:
1377      "[|finite A;
1378         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
1379       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1380   apply (subgoal_tac
1381          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1382   apply (erule ssubst)
1383   apply (subst divide_inverse)
1384   apply (subst setprod_timesf)
1385   apply (subst setprod_inversef, assumption+, rule refl)
1386   apply (rule setprod_cong, rule refl)
1387   apply (subst divide_inverse, auto)
1388   done
1390 subsection {* Finite cardinality *}
1392 text {* This definition, although traditional, is ugly to work with:
1393 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
1394 But now that we have @{text setsum} things are easy:
1395 *}
1397 constdefs
1398   card :: "'a set => nat"
1399   "card A == setsum (%x. 1::nat) A"
1401 lemma card_empty [simp]: "card {} = 0"
1404 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1407 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
1410 lemma card_insert_disjoint [simp]:
1411   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
1414 lemma card_insert_if:
1415     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
1418 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
1419   apply auto
1420   apply (drule_tac a = x in mk_disjoint_insert, clarify)
1421   apply (auto)
1422   done
1424 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
1425 by auto
1427 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
1428 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1429 apply(simp del:insert_Diff_single)
1430 done
1432 lemma card_Diff_singleton:
1433     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
1434   by (simp add: card_Suc_Diff1 [symmetric])
1436 lemma card_Diff_singleton_if:
1437     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
1440 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
1441   by (simp add: card_insert_if card_Suc_Diff1)
1443 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
1446 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
1447 by (simp add: card_def setsum_mono2_nat)
1449 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1450   apply (induct set: Finites, simp, clarify)
1451   apply (subgoal_tac "finite A & A - {x} <= F")
1452    prefer 2 apply (blast intro: finite_subset, atomize)
1453   apply (drule_tac x = "A - {x}" in spec)
1455   apply (case_tac "card A", auto)
1456   done
1458 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
1459   apply (simp add: psubset_def linorder_not_le [symmetric])
1460   apply (blast dest: card_seteq)
1461   done
1463 lemma card_Un_Int: "finite A ==> finite B
1464     ==> card A + card B = card (A Un B) + card (A Int B)"
1467 lemma card_Un_disjoint: "finite A ==> finite B
1468     ==> A Int B = {} ==> card (A Un B) = card A + card B"
1471 lemma card_Diff_subset:
1472   "finite B ==> B <= A ==> card (A - B) = card A - card B"
1475 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
1476   apply (rule Suc_less_SucD)
1478   done
1480 lemma card_Diff2_less:
1481     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
1482   apply (case_tac "x = y")
1484   apply (rule less_trans)
1485    prefer 2 apply (auto intro!: card_Diff1_less)
1486   done
1488 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
1489   apply (case_tac "x : A")
1490    apply (simp_all add: card_Diff1_less less_imp_le)
1491   done
1493 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
1494 by (erule psubsetI, blast)
1496 lemma insert_partition:
1497   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
1498   \<Longrightarrow> x \<inter> \<Union> F = {}"
1499 by auto
1501 (* main cardinality theorem *)
1502 lemma card_partition [rule_format]:
1503      "finite C ==>
1504         finite (\<Union> C) -->
1505         (\<forall>c\<in>C. card c = k) -->
1506         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
1507         k * card(C) = card (\<Union> C)"
1508 apply (erule finite_induct, simp)
1509 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
1510        finite_subset [of _ "\<Union> (insert x F)"])
1511 done
1514 lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
1515   -- {* Generalized to any @{text comm_semiring_1_cancel} in
1516         @{text IntDef} as @{text setsum_constant}. *}
1517 apply (cases "finite A")
1518 apply (erule finite_induct, auto)
1519 done
1521 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
1522   apply (erule finite_induct)
1523   apply (auto simp add: power_Suc)
1524   done
1527 subsubsection {* Cardinality of unions *}
1529 lemma card_UN_disjoint:
1530     "finite I ==> (ALL i:I. finite (A i)) ==>
1531         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1532       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
1534   apply (subgoal_tac
1535            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
1537   apply (simp add: setsum_constant_nat cong: setsum_cong)
1538   done
1540 lemma card_Union_disjoint:
1541   "finite C ==> (ALL A:C. finite A) ==>
1542         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
1543       card (Union C) = setsum card C"
1544   apply (frule card_UN_disjoint [of C id])
1545   apply (unfold Union_def id_def, assumption+)
1546   done
1548 subsubsection {* Cardinality of image *}
1550 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
1551   apply (induct set: Finites, simp)
1552   apply (simp add: le_SucI finite_imageI card_insert_if)
1553   done
1555 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
1558 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
1559   by (simp add: card_seteq card_image)
1561 lemma eq_card_imp_inj_on:
1562   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
1563 apply(induct rule:finite_induct)
1564  apply simp
1565 apply(frule card_image_le[where f = f])
1567 done
1569 lemma inj_on_iff_eq_card:
1570   "finite A ==> inj_on f A = (card(f ` A) = card A)"
1571 by(blast intro: card_image eq_card_imp_inj_on)
1574 lemma card_inj_on_le:
1575     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
1576 apply (subgoal_tac "finite A")
1577  apply (force intro: card_mono simp add: card_image [symmetric])
1578 apply (blast intro: finite_imageD dest: finite_subset)
1579 done
1581 lemma card_bij_eq:
1582     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
1583        finite A; finite B |] ==> card A = card B"
1584   by (auto intro: le_anti_sym card_inj_on_le)
1587 subsubsection {* Cardinality of products *}
1589 (*
1590 lemma SigmaI_insert: "y \<notin> A ==>
1591   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
1592   by auto
1593 *)
1595 lemma card_SigmaI [simp]:
1596   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
1597   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
1600 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
1601 apply (cases "finite A")
1602 apply (cases "finite B")
1604 apply (auto simp add: card_eq_0_iff
1605             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1606 done
1608 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
1613 subsubsection {* Cardinality of the Powerset *}
1615 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
1616   apply (induct set: Finites)
1618   apply (subst card_Un_disjoint, blast)
1619     apply (blast intro: finite_imageI, blast)
1620   apply (subgoal_tac "inj_on (insert x) (Pow F)")
1621    apply (simp add: card_image Pow_insert)
1622   apply (unfold inj_on_def)
1623   apply (blast elim!: equalityE)
1624   done
1626 text {* Relates to equivalence classes.  Based on a theorem of
1627 F. Kammüller's.  *}
1629 lemma dvd_partition:
1630   "finite (Union C) ==>
1631     ALL c : C. k dvd card c ==>
1632     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
1633   k dvd card (Union C)"
1634 apply(frule finite_UnionD)
1635 apply(rotate_tac -1)
1636   apply (induct set: Finites, simp_all, clarify)
1637   apply (subst card_Un_disjoint)
1639   done
1642 subsubsection {* Theorems about @{text "choose"} *}
1644 text {*
1645   \medskip Basic theorem about @{text "choose"}.  By Florian
1646   Kamm\"uller, tidied by LCP.
1647 *}
1649 lemma card_s_0_eq_empty:
1650     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
1652   apply (simp cong add: rev_conj_cong)
1653   done
1655 lemma choose_deconstruct: "finite M ==> x \<notin> M
1656   ==> {s. s <= insert x M & card(s) = Suc k}
1657        = {s. s <= M & card(s) = Suc k} Un
1658          {s. EX t. t <= M & card(t) = k & s = insert x t}"
1659   apply safe
1660    apply (auto intro: finite_subset [THEN card_insert_disjoint])
1661   apply (drule_tac x = "xa - {x}" in spec)
1662   apply (subgoal_tac "x \<notin> xa", auto)
1663   apply (erule rev_mp, subst card_Diff_singleton)
1664   apply (auto intro: finite_subset)
1665   done
1667 text{*There are as many subsets of @{term A} having cardinality @{term k}
1668  as there are sets obtained from the former by inserting a fixed element
1669  @{term x} into each.*}
1670 lemma constr_bij:
1671    "[|finite A; x \<notin> A|] ==>
1672     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
1673     card {B. B <= A & card(B) = k}"
1674   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
1675        apply (auto elim!: equalityE simp add: inj_on_def)
1676     apply (subst Diff_insert0, auto)
1677    txt {* finiteness of the two sets *}
1678    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
1679    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
1680    apply fast+
1681   done
1683 text {*
1684   Main theorem: combinatorial statement about number of subsets of a set.
1685 *}
1687 lemma n_sub_lemma:
1688   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1689   apply (induct k)
1690    apply (simp add: card_s_0_eq_empty, atomize)
1691   apply (rotate_tac -1, erule finite_induct)
1692    apply (simp_all (no_asm_simp) cong add: conj_cong
1694   apply (subst card_Un_disjoint)
1695      prefer 4 apply (force simp add: constr_bij)
1696     prefer 3 apply force
1697    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
1698      finite_subset [of _ "Pow (insert x F)", standard])
1699   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
1700   done
1702 theorem n_subsets:
1703     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1707 subsection{* A fold functional for non-empty sets *}
1709 text{* Does not require start value. *}
1711 consts
1712   foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
1714 inductive "foldSet1 f"
1715 intros
1716 foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
1717 foldSet1_insertI [intro]:
1718  "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
1719   \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
1721 constdefs
1722   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
1723   "fold1 f A == THE x. (A, x) : foldSet1 f"
1725 lemma foldSet1_nonempty:
1726  "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
1727 by(erule foldSet1.cases, simp_all)
1730 inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
1732 lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
1733 apply(rule iffI)
1734  prefer 2 apply fast
1735 apply (erule foldSet1.cases)
1736  apply blast
1737 apply (erule foldSet1.cases)
1738  apply blast
1739 apply blast
1740 done
1742 lemma Diff1_foldSet1:
1743   "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
1744 by (erule insert_Diff [THEN subst], rule foldSet1.intros,
1745     auto dest!:foldSet1_nonempty)
1747 lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
1748   by (induct set: foldSet1) auto
1750 lemma finite_nonempty_imp_foldSet1:
1751   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
1752   by (induct set: Finites) auto
1754 lemma (in ACf) foldSet1_determ_aux:
1755   "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
1756 proof (induct n)
1757   case 0 thus ?case by simp
1758 next
1759   case (Suc n)
1760   have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
1761            \<Longrightarrow> y = x" and card: "card A < Suc n"
1762   and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
1763   from card have "card A < n \<or> card A = n" by arith
1764   thus ?case
1765   proof
1766     assume less: "card A < n"
1767     show ?thesis by(rule IH[OF less Afoldx Afoldy])
1768   next
1769     assume cardA: "card A = n"
1770     show ?thesis
1771     proof (rule foldSet1.cases[OF Afoldx])
1772       fix a assume "(A, x) = ({a}, a)"
1773       thus "y = x" using Afoldy by (simp add:foldSet1_sing)
1774     next
1775       fix Ax ax x'
1776       assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
1777 	and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
1778 	and Axnon: "Ax \<noteq> {}"
1779       hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
1780       show ?thesis
1781       proof (rule foldSet1.cases[OF Afoldy])
1782 	fix ay assume "(A, y) = ({ay}, ay)"
1783 	thus ?thesis using eq1 x' Axnon notinx
1784 	  by (fastsimp simp:foldSet1_sing)
1785       next
1786 	fix Ay ay y'
1787 	assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
1788 	  and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
1789 	  and Aynon: "Ay \<noteq> {}"
1790 	hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
1791 	have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
1792 	with cardA A1 notinx have less: "card Ax < n" by simp
1793 	show ?thesis
1794 	proof cases
1795 	  assume "ax = ay"
1796 	  then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
1797 	  ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
1798 	next
1799 	  assume diff: "ax \<noteq> ay"
1800 	  let ?B = "Ax - {ay}"
1801 	  have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
1802 	    using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
1803 	  show ?thesis
1804 	  proof cases
1805 	    assume "?B = {}"
1806 	    with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
1807 	  next
1808 	    assume Bnon: "?B \<noteq> {}"
1809 	    moreover have "finite ?B" using finA A1 by simp
1810 	    ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
1811 	      using finite_nonempty_imp_foldSet1 by(blast)
1812 	    moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
1813 	    ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
1814 	    hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
1815             moreover have "ax\<cdot>b = y'"
1816 	    proof (rule IH[OF _ y'])
1817 	      show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
1818 		by(auto simp:card_Diff1_less)
1819 	    next
1820 	      show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
1821 		by fastsimp
1822 	    qed
1823 	    ultimately show ?thesis using x y by(auto simp:AC)
1824 	  qed
1825 	qed
1826       qed
1827     qed
1828   qed
1829 qed
1832 lemma (in ACf) foldSet1_determ:
1833   "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
1834 by (blast intro: foldSet1_determ_aux [rule_format])
1836 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
1837   by (unfold fold1_def) (blast intro: foldSet1_determ)
1839 lemma fold1_singleton: "fold1 f {a} = a"
1840   by (unfold fold1_def) blast
1842 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>
1843     ((insert x A, v) : foldSet1 f) =
1844     (EX y. (A, y) : foldSet1 f & v = f x y)"
1845 apply auto
1846 apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
1847   apply (fastsimp dest: foldSet1_imp_finite)
1848  apply blast
1849 apply (blast intro: foldSet1_determ)
1850 done
1852 lemma (in ACf) fold1_insert:
1853   "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
1854 apply (unfold fold1_def)
1856 apply (rule the_equality)
1857 apply (auto intro: finite_nonempty_imp_foldSet1
1859 done
1861 locale ACIf = ACf +
1862   assumes idem: "x \<cdot> x = x"
1864 lemma (in ACIf) fold1_insert2:
1865 assumes finA: "finite A" and nonA: "A \<noteq> {}"
1866 shows "fold1 f (insert a A) = f a (fold1 f A)"
1867 proof cases
1868   assume "a \<in> A"
1869   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
1870     by(blast dest: mk_disjoint_insert)
1871   show ?thesis
1872   proof cases
1873     assume "B = {}"
1874     thus ?thesis using A by(simp add:idem fold1_singleton)
1875   next
1876     assume nonB: "B \<noteq> {}"
1877     from finA A have finB: "finite B" by(blast intro: finite_subset)
1878     have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
1879     also have "\<dots> = f a (fold1 f B)"
1880       using finB nonB disj by(simp add: fold1_insert)
1881     also have "\<dots> = f a (fold1 f A)"
1882       using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
1883     finally show ?thesis .
1884   qed
1885 next
1886   assume "a \<notin> A"
1887   with finA nonA show ?thesis by(simp add:fold1_insert)
1888 qed
1891 text{* Now the recursion rules for definitions: *}
1893 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
1896 lemma (in ACf) fold1_insert_def:
1897   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
1900 lemma (in ACIf) fold1_insert2_def:
1901   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
1905 subsection{*Min and Max*}
1907 text{* As an application of @{text fold1} we define the minimal and
1908 maximal element of a (non-empty) set over a linear order. First we
1909 show that @{text min} and @{text max} are ACI: *}
1911 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1912 apply(rule ACf.intro)
1913 apply(auto simp:min_def)
1914 done
1916 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1917 apply(rule ACIf.intro[OF ACf_min])
1918 apply(rule ACIf_axioms.intro)
1919 apply(auto simp:min_def)
1920 done
1922 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1923 apply(rule ACf.intro)
1924 apply(auto simp:max_def)
1925 done
1927 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1928 apply(rule ACIf.intro[OF ACf_max])
1929 apply(rule ACIf_axioms.intro)
1930 apply(auto simp:max_def)
1931 done
1933 text{* Now we make the definitions: *}
1935 constdefs
1936   Min :: "('a::linorder)set => 'a"
1937   "Min  ==  fold1 min"
1939   Max :: "('a::linorder)set => 'a"
1940   "Max  ==  fold1 max"
1942 text{* Now we instantiate the recursion equations and declare them
1943 simplification rules: *}
1945 declare
1946   fold1_singleton_def[OF Min_def, simp]
1947   ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
1948   fold1_singleton_def[OF Max_def, simp]
1949   ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
1951 text{* Now we prove some properties by induction: *}
1953 lemma Min_in [simp]:
1954   assumes a: "finite S"
1955   shows "S \<noteq> {} \<Longrightarrow> Min S \<in> S"
1956 using a
1957 proof induct
1958   case empty thus ?case by simp
1959 next
1960   case (insert x S)
1961   show ?case
1962   proof cases
1963     assume "S = {}" thus ?thesis by simp
1964   next
1965     assume "S \<noteq> {}" thus ?thesis using insert by (simp add:min_def)
1966   qed
1967 qed
1969 lemma Min_le [simp]:
1970   assumes a: "finite S"
1971   shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> Min S \<le> x"
1972 using a
1973 proof induct
1974   case empty thus ?case by simp
1975 next
1976   case (insert y S)
1977   show ?case
1978   proof cases
1979     assume "S = {}" thus ?thesis using insert by simp
1980   next
1981     assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:min_def)
1982   qed
1983 qed
1985 lemma Max_in [simp]:
1986   assumes a: "finite S"
1987   shows "S \<noteq> {} \<Longrightarrow> Max S \<in> S"
1988 using a
1989 proof induct
1990   case empty thus ?case by simp
1991 next
1992   case (insert x S)
1993   show ?case
1994   proof cases
1995     assume "S = {}" thus ?thesis by simp
1996   next
1997     assume "S \<noteq> {}" thus ?thesis using insert by (simp add:max_def)
1998   qed
1999 qed
2001 lemma Max_le [simp]:
2002   assumes a: "finite S"
2003   shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> x \<le> Max S"
2004 using a
2005 proof induct
2006   case empty thus ?case by simp
2007 next
2008   case (insert y S)
2009   show ?case
2010   proof cases
2011     assume "S = {}" thus ?thesis using insert by simp
2012   next
2013     assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def)
2014   qed
2015 qed
2018 end