src/HOL/Finite_Set.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 30260 be39acd3ac85 child 30325 b3ae84c6e509 permissions -rw-r--r--
1 (*  Title:      HOL/Finite_Set.thy
2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
3                 with contributions by Jeremy Avigad
4 *)
6 header {* Finite sets *}
8 theory Finite_Set
9 imports Nat Product_Type Power
10 begin
12 subsection {* Definition and basic properties *}
14 inductive finite :: "'a set => bool"
15   where
16     emptyI [simp, intro!]: "finite {}"
17   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
19 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
20   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
21   shows "\<exists>a::'a. a \<notin> A"
22 proof -
23   from assms have "A \<noteq> UNIV" by blast
24   thus ?thesis by blast
25 qed
27 lemma finite_induct [case_names empty insert, induct set: finite]:
28   "finite F ==>
29     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
30   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
31 proof -
32   assume "P {}" and
33     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
34   assume "finite F"
35   thus "P F"
36   proof induct
37     show "P {}" by fact
38     fix x F assume F: "finite F" and P: "P F"
39     show "P (insert x F)"
40     proof cases
41       assume "x \<in> F"
42       hence "insert x F = F" by (rule insert_absorb)
43       with P show ?thesis by (simp only:)
44     next
45       assume "x \<notin> F"
46       from F this P show ?thesis by (rule insert)
47     qed
48   qed
49 qed
51 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
52 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
53  \<lbrakk> \<And>x. P{x};
54    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
55  \<Longrightarrow> P F"
56 using fin
57 proof induct
58   case empty thus ?case by simp
59 next
60   case (insert x F)
61   show ?case
62   proof cases
63     assume "F = {}"
64     thus ?thesis using `P {x}` by simp
65   next
66     assume "F \<noteq> {}"
67     thus ?thesis using insert by blast
68   qed
69 qed
71 lemma finite_subset_induct [consumes 2, case_names empty insert]:
72   assumes "finite F" and "F \<subseteq> A"
73     and empty: "P {}"
74     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
75   shows "P F"
76 proof -
77   from `finite F` and `F \<subseteq> A`
78   show ?thesis
79   proof induct
80     show "P {}" by fact
81   next
82     fix x F
83     assume "finite F" and "x \<notin> F" and
84       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
85     show "P (insert x F)"
86     proof (rule insert)
87       from i show "x \<in> A" by blast
88       from i have "F \<subseteq> A" by blast
89       with P show "P F" .
90       show "finite F" by fact
91       show "x \<notin> F" by fact
92     qed
93   qed
94 qed
96 text{* A finite choice principle. Does not need the SOME choice operator. *}
97 lemma finite_set_choice:
98   "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
99 proof (induct set: finite)
100   case empty thus ?case by simp
101 next
102   case (insert a A)
103   then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
104   show ?case (is "EX f. ?P f")
105   proof
106     show "?P(%x. if x = a then b else f x)" using f ab by auto
107   qed
108 qed
111 text{* Finite sets are the images of initial segments of natural numbers: *}
113 lemma finite_imp_nat_seg_image_inj_on:
114   assumes fin: "finite A"
115   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
116 using fin
117 proof induct
118   case empty
119   show ?case
120   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp
121   qed
122 next
123   case (insert a A)
124   have notinA: "a \<notin> A" by fact
125   from insert.hyps obtain n f
126     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
127   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
128         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
129     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
130   thus ?case by blast
131 qed
133 lemma nat_seg_image_imp_finite:
134   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
135 proof (induct n)
136   case 0 thus ?case by simp
137 next
138   case (Suc n)
139   let ?B = "f ` {i. i < n}"
140   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
141   show ?case
142   proof cases
143     assume "\<exists>k<n. f n = f k"
144     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
145     thus ?thesis using finB by simp
146   next
147     assume "\<not>(\<exists> k<n. f n = f k)"
148     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
149     thus ?thesis using finB by simp
150   qed
151 qed
153 lemma finite_conv_nat_seg_image:
154   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
155 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
157 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
158 by(fastsimp simp: finite_conv_nat_seg_image)
161 subsubsection{* Finiteness and set theoretic constructions *}
163 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
164 by (induct set: finite) simp_all
166 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
167   -- {* Every subset of a finite set is finite. *}
168 proof -
169   assume "finite B"
170   thus "!!A. A \<subseteq> B ==> finite A"
171   proof induct
172     case empty
173     thus ?case by simp
174   next
175     case (insert x F A)
176     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
177     show "finite A"
178     proof cases
179       assume x: "x \<in> A"
180       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
181       with r have "finite (A - {x})" .
182       hence "finite (insert x (A - {x}))" ..
183       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
184       finally show ?thesis .
185     next
186       show "A \<subseteq> F ==> ?thesis" by fact
187       assume "x \<notin> A"
188       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
189     qed
190   qed
191 qed
193 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
194 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
196 lemma finite_Collect_disjI[simp]:
197   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
200 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
201   -- {* The converse obviously fails. *}
202 by (blast intro: finite_subset)
204 lemma finite_Collect_conjI [simp, intro]:
205   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
206   -- {* The converse obviously fails. *}
209 lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
212 lemma finite_insert [simp]: "finite (insert a A) = finite A"
213   apply (subst insert_is_Un)
214   apply (simp only: finite_Un, blast)
215   done
217 lemma finite_Union[simp, intro]:
218  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
219 by (induct rule:finite_induct) simp_all
221 lemma finite_empty_induct:
222   assumes "finite A"
223     and "P A"
224     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
225   shows "P {}"
226 proof -
227   have "P (A - A)"
228   proof -
229     {
230       fix c b :: "'a set"
231       assume c: "finite c" and b: "finite b"
232 	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
233       have "c \<subseteq> b ==> P (b - c)"
234 	using c
235       proof induct
236 	case empty
237 	from P1 show ?case by simp
238       next
239 	case (insert x F)
240 	have "P (b - F - {x})"
241 	proof (rule P2)
242           from _ b show "finite (b - F)" by (rule finite_subset) blast
243           from insert show "x \<in> b - F" by simp
244           from insert show "P (b - F)" by simp
245 	qed
246 	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
247 	finally show ?case .
248       qed
249     }
250     then show ?thesis by this (simp_all add: assms)
251   qed
252   then show ?thesis by simp
253 qed
255 lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
256 by (rule Diff_subset [THEN finite_subset])
258 lemma finite_Diff2 [simp]:
259   assumes "finite B" shows "finite (A - B) = finite A"
260 proof -
261   have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
262   also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
263   finally show ?thesis ..
264 qed
266 lemma finite_compl[simp]:
267   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
270 lemma finite_Collect_not[simp]:
271   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
274 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
275   apply (subst Diff_insert)
276   apply (case_tac "a : A - B")
277    apply (rule finite_insert [symmetric, THEN trans])
278    apply (subst insert_Diff, simp_all)
279   done
282 text {* Image and Inverse Image over Finite Sets *}
284 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
285   -- {* The image of a finite set is finite. *}
286   by (induct set: finite) simp_all
288 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
289   apply (frule finite_imageI)
290   apply (erule finite_subset, assumption)
291   done
293 lemma finite_range_imageI:
294     "finite (range g) ==> finite (range (%x. f (g x)))"
295   apply (drule finite_imageI, simp add: range_composition)
296   done
298 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
299 proof -
300   have aux: "!!A. finite (A - {}) = finite A" by simp
301   fix B :: "'a set"
302   assume "finite B"
303   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
304     apply induct
305      apply simp
306     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
307      apply clarify
308      apply (simp (no_asm_use) add: inj_on_def)
309      apply (blast dest!: aux [THEN iffD1], atomize)
310     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
311     apply (frule subsetD [OF equalityD2 insertI1], clarify)
312     apply (rule_tac x = xa in bexI)
314     done
315 qed (rule refl)
318 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
319   -- {* The inverse image of a singleton under an injective function
320          is included in a singleton. *}
321   apply (auto simp add: inj_on_def)
322   apply (blast intro: the_equality [symmetric])
323   done
325 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
326   -- {* The inverse image of a finite set under an injective function
327          is finite. *}
328   apply (induct set: finite)
329    apply simp_all
330   apply (subst vimage_insert)
331   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
332   done
335 text {* The finite UNION of finite sets *}
337 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
338   by (induct set: finite) simp_all
340 text {*
341   Strengthen RHS to
342   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
344   We'd need to prove
345   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
346   by induction. *}
348 lemma finite_UN [simp]:
349   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
350 by (blast intro: finite_UN_I finite_subset)
352 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
353   finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
354 apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
355  apply auto
356 done
358 lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
359   finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
360 apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
361  apply auto
362 done
365 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
368 text {* Sigma of finite sets *}
370 lemma finite_SigmaI [simp]:
371     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
372   by (unfold Sigma_def) (blast intro!: finite_UN_I)
374 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
375     finite (A <*> B)"
376   by (rule finite_SigmaI)
378 lemma finite_Prod_UNIV:
379     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
380   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
381    apply (erule ssubst)
382    apply (erule finite_SigmaI, auto)
383   done
385 lemma finite_cartesian_productD1:
386      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
387 apply (auto simp add: finite_conv_nat_seg_image)
388 apply (drule_tac x=n in spec)
389 apply (drule_tac x="fst o f" in spec)
390 apply (auto simp add: o_def)
391  prefer 2 apply (force dest!: equalityD2)
392 apply (drule equalityD1)
393 apply (rename_tac y x)
394 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
395  prefer 2 apply force
396 apply clarify
397 apply (rule_tac x=k in image_eqI, auto)
398 done
400 lemma finite_cartesian_productD2:
401      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
402 apply (auto simp add: finite_conv_nat_seg_image)
403 apply (drule_tac x=n in spec)
404 apply (drule_tac x="snd o f" in spec)
405 apply (auto simp add: o_def)
406  prefer 2 apply (force dest!: equalityD2)
407 apply (drule equalityD1)
408 apply (rename_tac x y)
409 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
410  prefer 2 apply force
411 apply clarify
412 apply (rule_tac x=k in image_eqI, auto)
413 done
416 text {* The powerset of a finite set *}
418 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
419 proof
420   assume "finite (Pow A)"
421   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
422   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
423 next
424   assume "finite A"
425   thus "finite (Pow A)"
426     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
427 qed
429 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
433 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
434 by(blast intro: finite_subset[OF subset_Pow_Union])
437 subsection {* Class @{text finite}  *}
439 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
440 class finite =
441   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
442 setup {* Sign.parent_path *}
443 hide const finite
445 context finite
446 begin
448 lemma finite [simp]: "finite (A \<Colon> 'a set)"
449   by (rule subset_UNIV finite_UNIV finite_subset)+
451 end
453 lemma UNIV_unit [noatp]:
454   "UNIV = {()}" by auto
456 instance unit :: finite
457   by default (simp add: UNIV_unit)
459 lemma UNIV_bool [noatp]:
460   "UNIV = {False, True}" by auto
462 instance bool :: finite
463   by default (simp add: UNIV_bool)
465 instance * :: (finite, finite) finite
466   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
468 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
469   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
471 instance "fun" :: (finite, finite) finite
472 proof
473   show "finite (UNIV :: ('a => 'b) set)"
474   proof (rule finite_imageD)
475     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
476     have "range ?graph \<subseteq> Pow UNIV" by simp
477     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
478       by (simp only: finite_Pow_iff finite)
479     ultimately show "finite (range ?graph)"
480       by (rule finite_subset)
481     show "inj ?graph" by (rule inj_graph)
482   qed
483 qed
485 instance "+" :: (finite, finite) finite
486   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
489 subsection {* A fold functional for finite sets *}
491 text {* The intended behaviour is
492 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
493 if @{text f} is ``left-commutative'':
494 *}
496 locale fun_left_comm =
497   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
498   assumes fun_left_comm: "f x (f y z) = f y (f x z)"
499 begin
501 text{* On a functional level it looks much nicer: *}
503 lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
504 by (simp add: fun_left_comm expand_fun_eq)
506 end
508 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
509 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
510   emptyI [intro]: "fold_graph f z {} z" |
511   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
512       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
514 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
516 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
517 [code del]: "fold f z A = (THE y. fold_graph f z A y)"
519 text{*A tempting alternative for the definiens is
520 @{term "if finite A then THE y. fold_graph f z A y else e"}.
521 It allows the removal of finiteness assumptions from the theorems
522 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
523 The proofs become ugly. It is not worth the effort. (???) *}
526 lemma Diff1_fold_graph:
527   "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
528 by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
530 lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
531 by (induct set: fold_graph) auto
533 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
534 by (induct set: finite) auto
537 subsubsection{*From @{const fold_graph} to @{term fold}*}
539 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
540   by (auto simp add: less_Suc_eq)
542 lemma insert_image_inj_on_eq:
543      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
544         inj_on h {i. i < Suc m}|]
545       ==> A = h ` {i. i < m}"
546 apply (auto simp add: image_less_Suc inj_on_def)
547 apply (blast intro: less_trans)
548 done
550 lemma insert_inj_onE:
551   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
552       and inj_on: "inj_on h {i::nat. i<n}"
553   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
554 proof (cases n)
555   case 0 thus ?thesis using aA by auto
556 next
557   case (Suc m)
558   have nSuc: "n = Suc m" by fact
559   have mlessn: "m<n" by (simp add: nSuc)
560   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
561   let ?hm = "Fun.swap k m h"
562   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
563     by (simp add: inj_on_swap_iff inj_on)
564   show ?thesis
565   proof (intro exI conjI)
566     show "inj_on ?hm {i. i < m}" using inj_hm
567       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
568     show "m<n" by (rule mlessn)
569     show "A = ?hm ` {i. i < m}"
570     proof (rule insert_image_inj_on_eq)
571       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
572       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
573       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
574 	using aA hkeq nSuc klessn
575 	by (auto simp add: swap_def image_less_Suc fun_upd_image
576 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
577     qed
578   qed
579 qed
581 context fun_left_comm
582 begin
584 lemma fold_graph_determ_aux:
585   "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
586    \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
587    \<Longrightarrow> x' = x"
588 proof (induct n arbitrary: A x x' h rule: less_induct)
589   case (less n)
590   have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
591       \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
592       \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
593   have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
594     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
595   show ?case
596   proof (rule fold_graph.cases [OF Afoldx])
597     assume "A = {}" and "x = z"
598     with Afoldx' show "x' = x" by auto
599   next
600     fix B b u
601     assume AbB: "A = insert b B" and x: "x = f b u"
602       and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
603     show "x'=x"
604     proof (rule fold_graph.cases [OF Afoldx'])
605       assume "A = {}" and "x' = z"
606       with AbB show "x' = x" by blast
607     next
608       fix C c v
609       assume AcC: "A = insert c C" and x': "x' = f c v"
610         and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
611       from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
612       from insert_inj_onE [OF Beq notinB injh]
613       obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
614         and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto
615       from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
616       from insert_inj_onE [OF Ceq notinC injh]
617       obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
618         and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto
619       show "x'=x"
620       proof cases
621         assume "b=c"
622 	then moreover have "B = C" using AbB AcC notinB notinC by auto
623 	ultimately show ?thesis  using Bu Cv x x' IH [OF lessC Ceq inj_onC]
624           by auto
625       next
626 	assume diff: "b \<noteq> c"
627 	let ?D = "B - {c}"
628 	have B: "B = insert c ?D" and C: "C = insert b ?D"
629 	  using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
630 	have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
631 	with AbB have "finite ?D" by simp
632 	then obtain d where Dfoldd: "fold_graph f z ?D d"
633 	  using finite_imp_fold_graph by iprover
634 	moreover have cinB: "c \<in> B" using B by auto
635 	ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
636 	hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu])
637         moreover have "f b d = v"
638 	proof (rule IH[OF lessC Ceq inj_onC Cv])
639 	  show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
640 	qed
641 	ultimately show ?thesis
642           using fun_left_comm [of c b] x x' by (auto simp add: o_def)
643       qed
644     qed
645   qed
646 qed
648 lemma fold_graph_determ:
649   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
650 apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
651 apply (blast intro: fold_graph_determ_aux [rule_format])
652 done
654 lemma fold_equality:
655   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
656 by (unfold fold_def) (blast intro: fold_graph_determ)
658 text{* The base case for @{text fold}: *}
660 lemma (in -) fold_empty [simp]: "fold f z {} = z"
661 by (unfold fold_def) blast
663 text{* The various recursion equations for @{const fold}: *}
665 lemma fold_insert_aux: "x \<notin> A
666   \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
667       (\<exists>y. fold_graph f z A y \<and> v = f x y)"
668 apply auto
669 apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
670  apply (fastsimp dest: fold_graph_imp_finite)
671 apply (blast intro: fold_graph_determ)
672 done
674 lemma fold_insert [simp]:
675   "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
676 apply (simp add: fold_def fold_insert_aux)
677 apply (rule the_equality)
678  apply (auto intro: finite_imp_fold_graph
680 done
682 lemma fold_fun_comm:
683   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
684 proof (induct rule: finite_induct)
685   case empty then show ?case by simp
686 next
687   case (insert y A) then show ?case
688     by (simp add: fun_left_comm[of x])
689 qed
691 lemma fold_insert2:
692   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
693 by (simp add: fold_insert fold_fun_comm)
695 lemma fold_rec:
696 assumes "finite A" and "x \<in> A"
697 shows "fold f z A = f x (fold f z (A - {x}))"
698 proof -
699   have A: "A = insert x (A - {x})" using `x \<in> A` by blast
700   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
701   also have "\<dots> = f x (fold f z (A - {x}))"
702     by (rule fold_insert) (simp add: `finite A`)+
703   finally show ?thesis .
704 qed
706 lemma fold_insert_remove:
707   assumes "finite A"
708   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
709 proof -
710   from `finite A` have "finite (insert x A)" by auto
711   moreover have "x \<in> insert x A" by auto
712   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
713     by (rule fold_rec)
714   then show ?thesis by simp
715 qed
717 end
719 text{* A simplified version for idempotent functions: *}
721 locale fun_left_comm_idem = fun_left_comm +
722   assumes fun_left_idem: "f x (f x z) = f x z"
723 begin
725 text{* The nice version: *}
726 lemma fun_comp_idem : "f x o f x = f x"
727 by (simp add: fun_left_idem expand_fun_eq)
729 lemma fold_insert_idem:
730   assumes fin: "finite A"
731   shows "fold f z (insert x A) = f x (fold f z A)"
732 proof cases
733   assume "x \<in> A"
734   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
735   then show ?thesis using assms by (simp add:fun_left_idem)
736 next
737   assume "x \<notin> A" then show ?thesis using assms by simp
738 qed
740 declare fold_insert[simp del] fold_insert_idem[simp]
742 lemma fold_insert_idem2:
743   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
746 end
748 subsubsection{* The derived combinator @{text fold_image} *}
750 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
751 where "fold_image f g = fold (%x y. f (g x) y)"
753 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
756 context ab_semigroup_mult
757 begin
759 lemma fold_image_insert[simp]:
760 assumes "finite A" and "a \<notin> A"
761 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
762 proof -
763   interpret I: fun_left_comm "%x y. (g x) * y"
764     by unfold_locales (simp add: mult_ac)
765   show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
766 qed
768 (*
769 lemma fold_commute:
770   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
771   apply (induct set: finite)
772    apply simp
773   apply (simp add: mult_left_commute [of x])
774   done
776 lemma fold_nest_Un_Int:
777   "finite A ==> finite B
778     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
779   apply (induct set: finite)
780    apply simp
781   apply (simp add: fold_commute Int_insert_left insert_absorb)
782   done
784 lemma fold_nest_Un_disjoint:
785   "finite A ==> finite B ==> A Int B = {}
786     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
788 *)
790 lemma fold_image_reindex:
791 assumes fin: "finite A"
792 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
793 using fin apply induct
794  apply simp
795 apply simp
796 done
798 (*
799 text{*
800   Fusion theorem, as described in Graham Hutton's paper,
801   A Tutorial on the Universality and Expressiveness of Fold,
802   JFP 9:4 (355-372), 1999.
803 *}
805 lemma fold_fusion:
806   assumes "ab_semigroup_mult g"
807   assumes fin: "finite A"
808     and hyp: "\<And>x y. h (g x y) = times x (h y)"
809   shows "h (fold g j w A) = fold times j (h w) A"
810 proof -
811   class_interpret ab_semigroup_mult [g] by fact
812   show ?thesis using fin hyp by (induct set: finite) simp_all
813 qed
814 *)
816 lemma fold_image_cong:
817   "finite A \<Longrightarrow>
818   (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
819 apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z 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 end
835 context comm_monoid_mult
836 begin
838 lemma fold_image_Un_Int:
839   "finite A ==> finite B ==>
840     fold_image times g 1 A * fold_image times g 1 B =
841     fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
842 by (induct set: finite)
843    (auto simp add: mult_ac insert_absorb Int_insert_left)
845 corollary fold_Un_disjoint:
846   "finite A ==> finite B ==> A Int B = {} ==>
847    fold_image times g 1 (A Un B) =
848    fold_image times g 1 A * fold_image times g 1 B"
851 lemma fold_image_UN_disjoint:
852   "\<lbrakk> finite I; ALL i:I. finite (A i);
853      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
854    \<Longrightarrow> fold_image times g 1 (UNION I A) =
855        fold_image times (%i. fold_image times g 1 (A i)) 1 I"
856 apply (induct set: finite, simp, atomize)
857 apply (subgoal_tac "ALL i:F. x \<noteq> i")
858  prefer 2 apply blast
859 apply (subgoal_tac "A x Int UNION F A = {}")
860  prefer 2 apply blast
862 done
864 lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
865   fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =
866   fold_image times (split g) 1 (SIGMA x:A. B x)"
867 apply (subst Sigma_def)
868 apply (subst fold_image_UN_disjoint, assumption, simp)
869  apply blast
870 apply (erule fold_image_cong)
871 apply (subst fold_image_UN_disjoint, simp, simp)
872  apply blast
873 apply simp
874 done
876 lemma fold_image_distrib: "finite A \<Longrightarrow>
877    fold_image times (%x. g x * h x) 1 A =
878    fold_image times g 1 A *  fold_image times h 1 A"
879 by (erule finite_induct) (simp_all add: mult_ac)
881 lemma fold_image_related:
882   assumes Re: "R e e"
883   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
884   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
885   shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
886   using fS by (rule finite_subset_induct) (insert assms, auto)
888 lemma  fold_image_eq_general:
889   assumes fS: "finite S"
890   and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y"
891   and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
892   shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
893 proof-
894   from h f12 have hS: "h ` S = S'" by auto
895   {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
896     from f12 h H  have "x = y" by auto }
897   hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
898   from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
899   from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
900   also have "\<dots> = fold_image (op *) (f2 o h) e S"
901     using fold_image_reindex[OF fS hinj, of f2 e] .
902   also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
903     by blast
904   finally show ?thesis ..
905 qed
907 lemma fold_image_eq_general_inverses:
908   assumes fS: "finite S"
909   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
910   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
911   shows "fold_image (op *) f e S = fold_image (op *) g e T"
912   (* metis solves it, but not yet available here *)
913   apply (rule fold_image_eq_general[OF fS, of T h g f e])
914   apply (rule ballI)
915   apply (frule kh)
916   apply (rule ex1I[])
917   apply blast
918   apply clarsimp
919   apply (drule hk) apply simp
920   apply (rule sym)
921   apply (erule conjunct1[OF conjunct2[OF hk]])
922   apply (rule ballI)
923   apply (drule  hk)
924   apply blast
925   done
927 end
929 subsection {* Generalized summation over a set *}
934 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
935 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
937 abbreviation
938   Setsum  ("\<Sum>_" [1000] 999) where
939   "\<Sum>A == setsum (%x. x) A"
941 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
942 written @{text"\<Sum>x\<in>A. e"}. *}
944 syntax
945   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
946 syntax (xsymbols)
947   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
948 syntax (HTML output)
949   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
951 translations -- {* Beware of argument permutation! *}
952   "SUM i:A. b" == "CONST setsum (%i. b) A"
953   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
955 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
956  @{text"\<Sum>x|P. e"}. *}
958 syntax
959   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
960 syntax (xsymbols)
961   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
962 syntax (HTML output)
963   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
965 translations
966   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
967   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
969 print_translation {*
970 let
971   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
972     if x<>y then raise Match
973     else let val x' = Syntax.mark_bound x
974              val t' = subst_bound(x',t)
975              val P' = subst_bound(x',P)
976          in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end
977 in [("setsum", setsum_tr')] end
978 *}
981 lemma setsum_empty [simp]: "setsum f {} = 0"
984 lemma setsum_insert [simp]:
985   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
988 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
991 lemma setsum_reindex:
992      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
995 lemma setsum_reindex_id:
996      "inj_on f B ==> setsum f B = setsum id (f ` B)"
997 by (auto simp add: setsum_reindex)
999 lemma setsum_reindex_nonzero:
1000   assumes fS: "finite S"
1001   and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
1002   shows "setsum h (f ` S) = setsum (h o f) S"
1003 using nz
1004 proof(induct rule: finite_induct[OF fS])
1005   case 1 thus ?case by simp
1006 next
1007   case (2 x F)
1008   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
1009     then obtain y where y: "y \<in> F" "f x = f y" by auto
1010     from "2.hyps" y have xy: "x \<noteq> y" by auto
1012     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
1013     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
1014     also have "\<dots> = setsum (h o f) (insert x F)"
1015       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
1016       using h0
1017       apply simp
1018       apply (rule "2.hyps"(3))
1019       apply (rule_tac y="y" in  "2.prems")
1020       apply simp_all
1021       done
1022     finally have ?case .}
1023   moreover
1024   {assume fxF: "f x \<notin> f ` F"
1025     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
1026       using fxF "2.hyps" by simp
1027     also have "\<dots> = setsum (h o f) (insert x F)"
1028       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
1029       apply simp
1030       apply (rule cong[OF refl[of "op + (h (f x))"]])
1031       apply (rule "2.hyps"(3))
1032       apply (rule_tac y="y" in  "2.prems")
1033       apply simp_all
1034       done
1035     finally have ?case .}
1036   ultimately show ?case by blast
1037 qed
1039 lemma setsum_cong:
1040   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
1041 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
1043 lemma strong_setsum_cong[cong]:
1044   "A = B ==> (!!x. x:B =simp=> f x = g x)
1045    ==> setsum (%x. f x) A = setsum (%x. g x) B"
1046 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
1048 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
1049 by (rule setsum_cong[OF refl], auto);
1051 lemma setsum_reindex_cong:
1052    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
1053     ==> setsum h B = setsum g A"
1054 by (simp add: setsum_reindex cong: setsum_cong)
1057 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
1058 apply (clarsimp simp: setsum_def)
1059 apply (erule finite_induct, auto)
1060 done
1062 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
1065 lemma setsum_Un_Int: "finite A ==> finite B ==>
1066   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
1067   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1070 lemma setsum_Un_disjoint: "finite A ==> finite B
1071   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
1072 by (subst setsum_Un_Int [symmetric], auto)
1074 lemma setsum_mono_zero_left:
1075   assumes fT: "finite T" and ST: "S \<subseteq> T"
1076   and z: "\<forall>i \<in> T - S. f i = 0"
1077   shows "setsum f S = setsum f T"
1078 proof-
1079   have eq: "T = S \<union> (T - S)" using ST by blast
1080   have d: "S \<inter> (T - S) = {}" using ST by blast
1081   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
1082   show ?thesis
1083   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
1084 qed
1086 lemma setsum_mono_zero_right:
1087   assumes fT: "finite T" and ST: "S \<subseteq> T"
1088   and z: "\<forall>i \<in> T - S. f i = 0"
1089   shows "setsum f T = setsum f S"
1090 using setsum_mono_zero_left[OF fT ST z] by simp
1092 lemma setsum_mono_zero_cong_left:
1093   assumes fT: "finite T" and ST: "S \<subseteq> T"
1094   and z: "\<forall>i \<in> T - S. g i = 0"
1095   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
1096   shows "setsum f S = setsum g T"
1097 proof-
1098   have eq: "T = S \<union> (T - S)" using ST by blast
1099   have d: "S \<inter> (T - S) = {}" using ST by blast
1100   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
1101   show ?thesis
1102     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
1103 qed
1105 lemma setsum_mono_zero_cong_right:
1106   assumes fT: "finite T" and ST: "S \<subseteq> T"
1107   and z: "\<forall>i \<in> T - S. f i = 0"
1108   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
1109   shows "setsum f T = setsum g S"
1110 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
1112 lemma setsum_delta:
1113   assumes fS: "finite S"
1114   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
1115 proof-
1116   let ?f = "(\<lambda>k. if k=a then b k else 0)"
1117   {assume a: "a \<notin> S"
1118     hence "\<forall> k\<in> S. ?f k = 0" by simp
1119     hence ?thesis  using a by simp}
1120   moreover
1121   {assume a: "a \<in> S"
1122     let ?A = "S - {a}"
1123     let ?B = "{a}"
1124     have eq: "S = ?A \<union> ?B" using a by blast
1125     have dj: "?A \<inter> ?B = {}" by simp
1126     from fS have fAB: "finite ?A" "finite ?B" by auto
1127     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
1128       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1129       by simp
1130     then have ?thesis  using a by simp}
1131   ultimately show ?thesis by blast
1132 qed
1133 lemma setsum_delta':
1134   assumes fS: "finite S" shows
1135   "setsum (\<lambda>k. if a = k then b k else 0) S =
1136      (if a\<in> S then b a else 0)"
1137   using setsum_delta[OF fS, of a b, symmetric]
1138   by (auto intro: setsum_cong)
1140 lemma setsum_restrict_set:
1141   assumes fA: "finite A"
1142   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
1143 proof-
1144   from fA have fab: "finite (A \<inter> B)" by auto
1145   have aba: "A \<inter> B \<subseteq> A" by blast
1146   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
1147   from setsum_mono_zero_left[OF fA aba, of ?g]
1148   show ?thesis by simp
1149 qed
1151 lemma setsum_cases:
1152   assumes fA: "finite A"
1153   shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
1154          setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
1155 proof-
1156   have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}"
1157     by blast+
1158   from fA
1159   have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
1160   let ?g = "\<lambda>x. if x \<in> B then f x else g x"
1161   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
1162   show ?thesis by simp
1163 qed
1166 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
1167   the lhs need not be, since UNION I A could still be finite.*)
1168 lemma setsum_UN_disjoint:
1169     "finite I ==> (ALL i:I. finite (A i)) ==>
1170         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1171       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
1174 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
1175 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
1176 lemma setsum_Union_disjoint:
1177   "[| (ALL A:C. finite A);
1178       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
1179    ==> setsum f (Union C) = setsum (setsum f) C"
1180 apply (cases "finite C")
1181  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
1182   apply (frule setsum_UN_disjoint [of C id f])
1183  apply (unfold Union_def id_def, assumption+)
1184 done
1186 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
1187   the rhs need not be, since SIGMA A B could still be finite.*)
1188 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1189     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1192 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1193 lemma setsum_cartesian_product:
1194    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
1195 apply (cases "finite A")
1196  apply (cases "finite B")
1198  apply (cases "A={}", simp)
1199  apply (simp)
1200 apply (auto simp add: setsum_def
1201             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1202 done
1204 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
1208 subsubsection {* Properties in more restricted classes of structures *}
1210 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
1211 apply (case_tac "finite A")
1212  prefer 2 apply (simp add: setsum_def)
1213 apply (erule rev_mp)
1214 apply (erule finite_induct, auto)
1215 done
1217 lemma setsum_eq_0_iff [simp]:
1218     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
1219 by (induct set: finite) auto
1221 lemma setsum_Un_nat: "finite A ==> finite B ==>
1222   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1223   -- {* For the natural numbers, we have subtraction. *}
1224 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1226 lemma setsum_Un: "finite A ==> finite B ==>
1227   (setsum f (A Un B) :: 'a :: ab_group_add) =
1228    setsum f A + setsum f B - setsum f (A Int B)"
1229 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1231 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
1232   apply (induct set: finite)
1233   apply simp by (auto simp add: fold_image_insert)
1235 lemma (in comm_monoid_mult) fold_image_Un_one:
1236   assumes fS: "finite S" and fT: "finite T"
1237   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
1238   shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
1239 proof-
1240   have "fold_image op * f 1 (S \<inter> T) = 1"
1241     apply (rule fold_image_1)
1242     using fS fT I0 by auto
1243   with fold_image_Un_Int[OF fS fT] show ?thesis by simp
1244 qed
1246 lemma setsum_eq_general_reverses:
1247   assumes fS: "finite S" and fT: "finite T"
1248   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
1249   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
1250   shows "setsum f S = setsum g T"
1251   apply (simp add: setsum_def fS fT)
1253   apply (erule kh)
1254   apply (erule hk)
1255   done
1259 lemma setsum_Un_zero:
1260   assumes fS: "finite S" and fT: "finite T"
1261   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
1262   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
1263   using fS fT
1266   using I0 by auto
1269 lemma setsum_UNION_zero:
1270   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
1271   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
1272   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
1273   using fSS f0
1274 proof(induct rule: finite_induct[OF fS])
1275   case 1 thus ?case by simp
1276 next
1277   case (2 T F)
1278   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
1279     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
1280   from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
1281   from "2.prems" TF fTF
1282   show ?case
1283     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
1284 qed
1287 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
1288   (if a:A then setsum f A - f a else setsum f A)"
1289 apply (case_tac "finite A")
1290  prefer 2 apply (simp add: setsum_def)
1291 apply (erule finite_induct)
1292  apply (auto simp add: insert_Diff_if)
1293 apply (drule_tac a = a in mk_disjoint_insert, auto)
1294 done
1296 lemma setsum_diff1: "finite A \<Longrightarrow>
1297   (setsum f (A - {a}) :: ('a::ab_group_add)) =
1298   (if a:A then setsum f A - f a else setsum f A)"
1299 by (erule finite_induct) (auto simp add: insert_Diff_if)
1301 lemma setsum_diff1'[rule_format]:
1302   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
1303 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
1305 done
1307 (* By Jeremy Siek: *)
1309 lemma setsum_diff_nat:
1310 assumes "finite B" and "B \<subseteq> A"
1311 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
1312 using assms
1313 proof induct
1314   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
1315 next
1316   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
1317     and xFinA: "insert x F \<subseteq> A"
1318     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
1319   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
1320   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
1322   from xFinA have "F \<subseteq> A" by simp
1323   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
1324   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
1325     by simp
1326   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
1327   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
1328     by simp
1329   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
1330   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
1331     by simp
1332   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
1333 qed
1335 lemma setsum_diff:
1336   assumes le: "finite A" "B \<subseteq> A"
1337   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
1338 proof -
1339   from le have finiteB: "finite B" using finite_subset by auto
1340   show ?thesis using finiteB le
1341   proof induct
1342     case empty
1343     thus ?case by auto
1344   next
1345     case (insert x F)
1346     thus ?case using le finiteB
1347       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
1348   qed
1349 qed
1351 lemma setsum_mono:
1352   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
1353   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
1354 proof (cases "finite K")
1355   case True
1356   thus ?thesis using le
1357   proof induct
1358     case empty
1359     thus ?case by simp
1360   next
1361     case insert
1362     thus ?case using add_mono by fastsimp
1363   qed
1364 next
1365   case False
1366   thus ?thesis
1368 qed
1370 lemma setsum_strict_mono:
1372   assumes "finite A"  "A \<noteq> {}"
1373     and "!!x. x:A \<Longrightarrow> f x < g x"
1374   shows "setsum f A < setsum g A"
1375   using prems
1376 proof (induct rule: finite_ne_induct)
1377   case singleton thus ?case by simp
1378 next
1379   case insert thus ?case by (auto simp: add_strict_mono)
1380 qed
1382 lemma setsum_negf:
1383   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
1384 proof (cases "finite A")
1385   case True thus ?thesis by (induct set: finite) auto
1386 next
1387   case False thus ?thesis by (simp add: setsum_def)
1388 qed
1390 lemma setsum_subtractf:
1391   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1392     setsum f A - setsum g A"
1393 proof (cases "finite A")
1395 next
1396   case False thus ?thesis by (simp add: setsum_def)
1397 qed
1399 lemma setsum_nonneg:
1401   shows "0 \<le> setsum f A"
1402 proof (cases "finite A")
1403   case True thus ?thesis using nn
1404   proof induct
1405     case empty then show ?case by simp
1406   next
1407     case (insert x F)
1408     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
1409     with insert show ?case by simp
1410   qed
1411 next
1412   case False thus ?thesis by (simp add: setsum_def)
1413 qed
1415 lemma setsum_nonpos:
1417   shows "setsum f A \<le> 0"
1418 proof (cases "finite A")
1419   case True thus ?thesis using np
1420   proof induct
1421     case empty then show ?case by simp
1422   next
1423     case (insert x F)
1424     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
1425     with insert show ?case by simp
1426   qed
1427 next
1428   case False thus ?thesis by (simp add: setsum_def)
1429 qed
1431 lemma setsum_mono2:
1433 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
1434 shows "setsum f A \<le> setsum f B"
1435 proof -
1436   have "setsum f A \<le> setsum f A + setsum f (B-A)"
1438   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1440   also have "A \<union> (B-A) = B" using sub by blast
1441   finally show ?thesis .
1442 qed
1444 lemma setsum_mono3: "finite B ==> A <= B ==>
1445     ALL x: B - A.
1447         setsum f A <= setsum f B"
1448   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
1449   apply (erule ssubst)
1450   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
1451   apply simp
1453   apply (erule setsum_nonneg)
1454   apply (subst setsum_Un_disjoint [THEN sym])
1455   apply (erule finite_subset, assumption)
1456   apply (rule finite_subset)
1457   prefer 2
1458   apply assumption
1459   apply auto
1460   apply (rule setsum_cong)
1461   apply auto
1462 done
1464 lemma setsum_right_distrib:
1465   fixes f :: "'a => ('b::semiring_0)"
1466   shows "r * setsum f A = setsum (%n. r * f n) A"
1467 proof (cases "finite A")
1468   case True
1469   thus ?thesis
1470   proof induct
1471     case empty thus ?case by simp
1472   next
1473     case (insert x A) thus ?case by (simp add: right_distrib)
1474   qed
1475 next
1476   case False thus ?thesis by (simp add: setsum_def)
1477 qed
1479 lemma setsum_left_distrib:
1480   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
1481 proof (cases "finite A")
1482   case True
1483   then show ?thesis
1484   proof induct
1485     case empty thus ?case by simp
1486   next
1487     case (insert x A) thus ?case by (simp add: left_distrib)
1488   qed
1489 next
1490   case False thus ?thesis by (simp add: setsum_def)
1491 qed
1493 lemma setsum_divide_distrib:
1494   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
1495 proof (cases "finite A")
1496   case True
1497   then show ?thesis
1498   proof induct
1499     case empty thus ?case by simp
1500   next
1502   qed
1503 next
1504   case False thus ?thesis by (simp add: setsum_def)
1505 qed
1507 lemma setsum_abs[iff]:
1508   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
1509   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
1510 proof (cases "finite A")
1511   case True
1512   thus ?thesis
1513   proof induct
1514     case empty thus ?case by simp
1515   next
1516     case (insert x A)
1517     thus ?case by (auto intro: abs_triangle_ineq order_trans)
1518   qed
1519 next
1520   case False thus ?thesis by (simp add: setsum_def)
1521 qed
1523 lemma setsum_abs_ge_zero[iff]:
1524   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
1525   shows "0 \<le> setsum (%i. abs(f i)) A"
1526 proof (cases "finite A")
1527   case True
1528   thus ?thesis
1529   proof induct
1530     case empty thus ?case by simp
1531   next
1532     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
1533   qed
1534 next
1535   case False thus ?thesis by (simp add: setsum_def)
1536 qed
1538 lemma abs_setsum_abs[simp]:
1539   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
1540   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
1541 proof (cases "finite A")
1542   case True
1543   thus ?thesis
1544   proof induct
1545     case empty thus ?case by simp
1546   next
1547     case (insert a A)
1548     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
1549     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
1550     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
1551       by (simp del: abs_of_nonneg)
1552     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
1553     finally show ?case .
1554   qed
1555 next
1556   case False thus ?thesis by (simp add: setsum_def)
1557 qed
1560 text {* Commuting outer and inner summation *}
1562 lemma swap_inj_on:
1563   "inj_on (%(i, j). (j, i)) (A \<times> B)"
1564   by (unfold inj_on_def) fast
1566 lemma swap_product:
1567   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
1568   by (simp add: split_def image_def) blast
1570 lemma setsum_commute:
1571   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
1573   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
1574     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
1575     (is "?s = _")
1576     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
1578     done
1579   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
1580     (is "_ = ?t")
1582     done
1583   finally show "?s = ?t" .
1584 qed
1586 lemma setsum_product:
1587   fixes f :: "'a => ('b::semiring_0)"
1588   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
1589   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
1592 subsection {* Generalized product over a set *}
1594 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
1595 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
1597 abbreviation
1598   Setprod  ("\<Prod>_" [1000] 999) where
1599   "\<Prod>A == setprod (%x. x) A"
1601 syntax
1602   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
1603 syntax (xsymbols)
1604   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1605 syntax (HTML output)
1606   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1608 translations -- {* Beware of argument permutation! *}
1609   "PROD i:A. b" == "CONST setprod (%i. b) A"
1610   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
1612 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
1613  @{text"\<Prod>x|P. e"}. *}
1615 syntax
1616   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
1617 syntax (xsymbols)
1618   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
1619 syntax (HTML output)
1620   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
1622 translations
1623   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
1624   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
1627 lemma setprod_empty [simp]: "setprod f {} = 1"
1628 by (auto simp add: setprod_def)
1630 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1631     setprod f (insert a A) = f a * setprod f A"
1634 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
1637 lemma setprod_reindex:
1638    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
1639 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
1641 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
1642 by (auto simp add: setprod_reindex)
1644 lemma setprod_cong:
1645   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1646 by(fastsimp simp: setprod_def intro: fold_image_cong)
1648 lemma strong_setprod_cong:
1649   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
1650 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
1652 lemma setprod_reindex_cong: "inj_on f A ==>
1653     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1654 by (frule setprod_reindex, simp)
1656 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
1657   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
1658   shows "setprod h B = setprod g A"
1659 proof-
1660     have "setprod h B = setprod (h o f) A"
1661       by (simp add: B setprod_reindex[OF i, of h])
1662     then show ?thesis apply simp
1663       apply (rule setprod_cong)
1664       apply simp
1665       by (erule eq[symmetric])
1666 qed
1668 lemma setprod_Un_one:
1669   assumes fS: "finite S" and fT: "finite T"
1670   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
1671   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
1672   using fS fT
1674   apply (rule fold_image_Un_one)
1675   using I0 by auto
1678 lemma setprod_1: "setprod (%i. 1) A = 1"
1679 apply (case_tac "finite A")
1680 apply (erule finite_induct, auto simp add: mult_ac)
1681 done
1683 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
1684 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
1685 apply (erule ssubst, rule setprod_1)
1686 apply (rule setprod_cong, auto)
1687 done
1689 lemma setprod_Un_Int: "finite A ==> finite B
1690     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1693 lemma setprod_Un_disjoint: "finite A ==> finite B
1694   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1695 by (subst setprod_Un_Int [symmetric], auto)
1697 lemma setprod_delta:
1698   assumes fS: "finite S"
1699   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
1700 proof-
1701   let ?f = "(\<lambda>k. if k=a then b k else 1)"
1702   {assume a: "a \<notin> S"
1703     hence "\<forall> k\<in> S. ?f k = 1" by simp
1704     hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
1705   moreover
1706   {assume a: "a \<in> S"
1707     let ?A = "S - {a}"
1708     let ?B = "{a}"
1709     have eq: "S = ?A \<union> ?B" using a by blast
1710     have dj: "?A \<inter> ?B = {}" by simp
1711     from fS have fAB: "finite ?A" "finite ?B" by auto
1712     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
1713     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1714       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1715       by simp
1716     then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
1717   ultimately show ?thesis by blast
1718 qed
1720 lemma setprod_delta':
1721   assumes fS: "finite S" shows
1722   "setprod (\<lambda>k. if a = k then b k else 1) S =
1723      (if a\<in> S then b a else 1)"
1724   using setprod_delta[OF fS, of a b, symmetric]
1725   by (auto intro: setprod_cong)
1728 lemma setprod_UN_disjoint:
1729     "finite I ==> (ALL i:I. finite (A i)) ==>
1730         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1731       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1732 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
1734 lemma setprod_Union_disjoint:
1735   "[| (ALL A:C. finite A);
1736       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
1737    ==> setprod f (Union C) = setprod (setprod f) C"
1738 apply (cases "finite C")
1739  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
1740   apply (frule setprod_UN_disjoint [of C id f])
1741  apply (unfold Union_def id_def, assumption+)
1742 done
1744 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1745     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
1746     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1747 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
1749 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1750 lemma setprod_cartesian_product:
1751      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
1752 apply (cases "finite A")
1753  apply (cases "finite B")
1755  apply (cases "A={}", simp)
1757 apply (auto simp add: setprod_def
1758             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1759 done
1761 lemma setprod_timesf:
1762      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
1766 subsubsection {* Properties in more restricted classes of structures *}
1768 lemma setprod_eq_1_iff [simp]:
1769   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
1770 by (induct set: finite) auto
1772 lemma setprod_zero:
1773      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
1774 apply (induct set: finite, force, clarsimp)
1775 apply (erule disjE, auto)
1776 done
1778 lemma setprod_nonneg [rule_format]:
1779    "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
1780 apply (case_tac "finite A")
1781 apply (induct set: finite, force, clarsimp)
1782 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
1783 apply (rule mult_mono, assumption+)
1784 apply (auto simp add: setprod_def)
1785 done
1787 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
1788   --> 0 < setprod f A"
1789 apply (case_tac "finite A")
1790 apply (induct set: finite, force, clarsimp)
1791 apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
1792 apply (rule mult_strict_mono, assumption+)
1793 apply (auto simp add: setprod_def)
1794 done
1796 lemma setprod_nonzero [rule_format]:
1797   "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
1798     finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
1799 by (erule finite_induct, auto)
1801 lemma setprod_zero_eq:
1802     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
1803      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
1804 by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
1806 lemma setprod_nonzero_field:
1807     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
1808 by (rule setprod_nonzero, auto)
1810 lemma setprod_zero_eq_field:
1811     "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
1812 by (rule setprod_zero_eq, auto)
1814 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1815   (setprod f (A Un B) :: 'a ::{field})
1816    = setprod f A * setprod f B / setprod f (A Int B)"
1817 apply (subst setprod_Un_Int [symmetric], auto)
1818 apply (subgoal_tac "finite (A Int B)")
1819 apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
1820 apply (subst times_divide_eq_right [THEN sym], auto)
1821 done
1823 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1824   (setprod f (A - {a}) :: 'a :: {field}) =
1825   (if a:A then setprod f A / f a else setprod f A)"
1826 by (erule finite_induct) (auto simp add: insert_Diff_if)
1828 lemma setprod_inversef: "finite A ==>
1829   ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
1830   setprod (inverse \<circ> f) A = inverse (setprod f A)"
1831 by (erule finite_induct) auto
1833 lemma setprod_dividef:
1834    "[|finite A;
1835       \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
1836     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1837 apply (subgoal_tac
1838          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1839 apply (erule ssubst)
1840 apply (subst divide_inverse)
1841 apply (subst setprod_timesf)
1842 apply (subst setprod_inversef, assumption+, rule refl)
1843 apply (rule setprod_cong, rule refl)
1844 apply (subst divide_inverse, auto)
1845 done
1847 lemma setprod_dvd_setprod [rule_format]:
1848     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
1849   apply (cases "finite A")
1850   apply (induct set: finite)
1851   apply (auto simp add: dvd_def)
1852   apply (rule_tac x = "k * ka" in exI)
1854 done
1856 lemma setprod_dvd_setprod_subset:
1857   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
1858   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
1859   apply (unfold dvd_def, blast)
1860   apply (subst setprod_Un_disjoint [symmetric])
1861   apply (auto elim: finite_subset intro: setprod_cong)
1862 done
1864 lemma setprod_dvd_setprod_subset2:
1865   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
1866       setprod f A dvd setprod g B"
1867   apply (rule dvd_trans)
1868   apply (rule setprod_dvd_setprod, erule (1) bspec)
1869   apply (erule (1) setprod_dvd_setprod_subset)
1870 done
1872 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
1873     (f i ::'a::comm_semiring_1) dvd setprod f A"
1874 by (induct set: finite) (auto intro: dvd_mult)
1876 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
1877     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
1878   apply (cases "finite A")
1879   apply (induct set: finite)
1880   apply auto
1881 done
1884 subsection {* Finite cardinality *}
1886 text {* This definition, although traditional, is ugly to work with:
1887 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
1888 But now that we have @{text setsum} things are easy:
1889 *}
1891 definition card :: "'a set \<Rightarrow> nat"
1892 where "card A = setsum (\<lambda>x. 1) A"
1894 lemma card_empty [simp]: "card {} = 0"
1897 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1900 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
1903 lemma card_insert_disjoint [simp]:
1904   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
1907 lemma card_insert_if:
1908   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
1911 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
1912 apply auto
1913 apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
1914 done
1916 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
1917 by auto
1920 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
1921 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1922 apply(simp del:insert_Diff_single)
1923 done
1925 lemma card_Diff_singleton:
1926   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
1927 by (simp add: card_Suc_Diff1 [symmetric])
1929 lemma card_Diff_singleton_if:
1930   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
1933 lemma card_Diff_insert[simp]:
1934 assumes "finite A" and "a:A" and "a ~: B"
1935 shows "card(A - insert a B) = card(A - B) - 1"
1936 proof -
1937   have "A - insert a B = (A - B) - {a}" using assms by blast
1938   then show ?thesis using assms by(simp add:card_Diff_singleton)
1939 qed
1941 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
1942 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
1944 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
1947 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
1948 by (simp add: card_def setsum_mono2)
1950 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1951 apply (induct set: finite, simp, clarify)
1952 apply (subgoal_tac "finite A & A - {x} <= F")
1953  prefer 2 apply (blast intro: finite_subset, atomize)
1954 apply (drule_tac x = "A - {x}" in spec)
1956 apply (case_tac "card A", auto)
1957 done
1959 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
1960 apply (simp add: psubset_eq linorder_not_le [symmetric])
1961 apply (blast dest: card_seteq)
1962 done
1964 lemma card_Un_Int: "finite A ==> finite B
1965     ==> card A + card B = card (A Un B) + card (A Int B)"
1968 lemma card_Un_disjoint: "finite A ==> finite B
1969     ==> A Int B = {} ==> card (A Un B) = card A + card B"
1972 lemma card_Diff_subset:
1973   "finite B ==> B <= A ==> card (A - B) = card A - card B"
1976 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
1977 apply (rule Suc_less_SucD)
1978 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
1979 done
1981 lemma card_Diff2_less:
1982   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
1983 apply (case_tac "x = y")
1984  apply (simp add: card_Diff1_less del:card_Diff_insert)
1985 apply (rule less_trans)
1986  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
1987 done
1989 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
1990 apply (case_tac "x : A")
1991  apply (simp_all add: card_Diff1_less less_imp_le)
1992 done
1994 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
1995 by (erule psubsetI, blast)
1997 lemma insert_partition:
1998   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
1999   \<Longrightarrow> x \<inter> \<Union> F = {}"
2000 by auto
2002 text{* main cardinality theorem *}
2003 lemma card_partition [rule_format]:
2004   "finite C ==>
2005      finite (\<Union> C) -->
2006      (\<forall>c\<in>C. card c = k) -->
2007      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
2008      k * card(C) = card (\<Union> C)"
2009 apply (erule finite_induct, simp)
2010 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
2011        finite_subset [of _ "\<Union> (insert x F)"])
2012 done
2015 text{*The form of a finite set of given cardinality*}
2017 lemma card_eq_SucD:
2018 assumes "card A = Suc k"
2019 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
2020 proof -
2021   have fin: "finite A" using assms by (auto intro: ccontr)
2022   moreover have "card A \<noteq> 0" using assms by auto
2023   ultimately obtain b where b: "b \<in> A" by auto
2024   show ?thesis
2025   proof (intro exI conjI)
2026     show "A = insert b (A-{b})" using b by blast
2027     show "b \<notin> A - {b}" by blast
2028     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
2029       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
2030   qed
2031 qed
2033 lemma card_Suc_eq:
2034   "(card A = Suc k) =
2035    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
2036 apply(rule iffI)
2037  apply(erule card_eq_SucD)
2038 apply(auto)
2039 apply(subst card_insert)
2040  apply(auto intro:ccontr)
2041 done
2043 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
2044 apply (cases "finite A")
2045 apply (erule finite_induct)
2046 apply (auto simp add: algebra_simps)
2047 done
2049 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
2050 apply (erule finite_induct)
2051 apply (auto simp add: power_Suc)
2052 done
2054 lemma setprod_gen_delta:
2055   assumes fS: "finite S"
2056   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)"
2057 proof-
2058   let ?f = "(\<lambda>k. if k=a then b k else c)"
2059   {assume a: "a \<notin> S"
2060     hence "\<forall> k\<in> S. ?f k = c" by simp
2061     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
2062   moreover
2063   {assume a: "a \<in> S"
2064     let ?A = "S - {a}"
2065     let ?B = "{a}"
2066     have eq: "S = ?A \<union> ?B" using a by blast
2067     have dj: "?A \<inter> ?B = {}" by simp
2068     from fS have fAB: "finite ?A" "finite ?B" by auto
2069     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
2070       apply (rule setprod_cong) by auto
2071     have cA: "card ?A = card S - 1" using fS a by auto
2072     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
2073     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
2074       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
2075       by simp
2076     then have ?thesis using a cA
2077       by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
2078   ultimately show ?thesis by blast
2079 qed
2082 lemma setsum_bounded:
2083   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
2084   shows "setsum f A \<le> of_nat(card A) * K"
2085 proof (cases "finite A")
2086   case True
2087   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
2088 next
2089   case False thus ?thesis by (simp add: setsum_def)
2090 qed
2093 subsubsection {* Cardinality of unions *}
2095 lemma card_UN_disjoint:
2096   "finite I ==> (ALL i:I. finite (A i)) ==>
2097    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
2098    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
2099 apply (simp add: card_def del: setsum_constant)
2100 apply (subgoal_tac
2101          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
2102 apply (simp add: setsum_UN_disjoint del: setsum_constant)
2103 apply (simp cong: setsum_cong)
2104 done
2106 lemma card_Union_disjoint:
2107   "finite C ==> (ALL A:C. finite A) ==>
2108    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
2109    ==> card (Union C) = setsum card C"
2110 apply (frule card_UN_disjoint [of C id])
2111 apply (unfold Union_def id_def, assumption+)
2112 done
2115 subsubsection {* Cardinality of image *}
2117 text{*The image of a finite set can be expressed using @{term fold_image}.*}
2118 lemma image_eq_fold_image:
2119   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
2120 proof (induct rule: finite_induct)
2121   case empty then show ?case by simp
2122 next
2123   interpret ab_semigroup_mult "op Un"
2124     proof qed auto
2125   case insert
2126   then show ?case by simp
2127 qed
2129 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
2130 apply (induct set: finite)
2131  apply simp
2132 apply (simp add: le_SucI finite_imageI card_insert_if)
2133 done
2135 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
2136 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
2138 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
2139 by (simp add: card_seteq card_image)
2141 lemma eq_card_imp_inj_on:
2142   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
2143 apply (induct rule:finite_induct)
2144 apply simp
2145 apply(frule card_image_le[where f = f])
2147 done
2149 lemma inj_on_iff_eq_card:
2150   "finite A ==> inj_on f A = (card(f ` A) = card A)"
2151 by(blast intro: card_image eq_card_imp_inj_on)
2154 lemma card_inj_on_le:
2155   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
2156 apply (subgoal_tac "finite A")
2157  apply (force intro: card_mono simp add: card_image [symmetric])
2158 apply (blast intro: finite_imageD dest: finite_subset)
2159 done
2161 lemma card_bij_eq:
2162   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
2163      finite A; finite B |] ==> card A = card B"
2164 by (auto intro: le_anti_sym card_inj_on_le)
2167 subsubsection {* Cardinality of products *}
2169 (*
2170 lemma SigmaI_insert: "y \<notin> A ==>
2171   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
2172   by auto
2173 *)
2175 lemma card_SigmaI [simp]:
2176   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
2177   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
2180 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
2181 apply (cases "finite A")
2182 apply (cases "finite B")
2183 apply (auto simp add: card_eq_0_iff
2184             dest: finite_cartesian_productD1 finite_cartesian_productD2)
2185 done
2187 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
2191 subsubsection {* Cardinality of sums *}
2193 lemma card_Plus:
2194   assumes "finite A" and "finite B"
2195   shows "card (A <+> B) = card A + card B"
2196 proof -
2197   have "Inl`A \<inter> Inr`B = {}" by fast
2198   with assms show ?thesis
2199     unfolding Plus_def
2200     by (simp add: card_Un_disjoint card_image)
2201 qed
2204 subsubsection {* Cardinality of the Powerset *}
2206 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
2207 apply (induct set: finite)
2209 apply (subst card_Un_disjoint, blast)
2210   apply (blast intro: finite_imageI, blast)
2211 apply (subgoal_tac "inj_on (insert x) (Pow F)")
2212  apply (simp add: card_image Pow_insert)
2213 apply (unfold inj_on_def)
2214 apply (blast elim!: equalityE)
2215 done
2217 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
2219 lemma dvd_partition:
2220   "finite (Union C) ==>
2221     ALL c : C. k dvd card c ==>
2222     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
2223   k dvd card (Union C)"
2224 apply(frule finite_UnionD)
2225 apply(rotate_tac -1)
2226 apply (induct set: finite, simp_all, clarify)
2227 apply (subst card_Un_disjoint)
2229 done
2232 subsubsection {* Relating injectivity and surjectivity *}
2234 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
2235 apply(rule eq_card_imp_inj_on, assumption)
2236 apply(frule finite_imageI)
2237 apply(drule (1) card_seteq)
2238  apply(erule card_image_le)
2239 apply simp
2240 done
2242 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
2243 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
2244 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
2246 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
2247 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
2248 by(fastsimp simp:surj_def dest!: endo_inj_surj)
2250 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
2251 proof
2252   assume "finite(UNIV::nat set)"
2253   with finite_UNIV_inj_surj[of Suc]
2254   show False by simp (blast dest: Suc_neq_Zero surjD)
2255 qed
2257 lemma infinite_UNIV_char_0:
2258   "\<not> finite (UNIV::'a::semiring_char_0 set)"
2259 proof
2260   assume "finite (UNIV::'a set)"
2261   with subset_UNIV have "finite (range of_nat::'a set)"
2262     by (rule finite_subset)
2263   moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
2265   ultimately have "finite (UNIV::nat set)"
2266     by (rule finite_imageD)
2267   then show "False"
2269 qed
2271 subsection{* A fold functional for non-empty sets *}
2273 text{* Does not require start value. *}
2275 inductive
2276   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
2277   for f :: "'a => 'a => 'a"
2278 where
2279   fold1Set_insertI [intro]:
2280    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
2282 constdefs
2283   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
2284   "fold1 f A == THE x. fold1Set f A x"
2286 lemma fold1Set_nonempty:
2287   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
2288 by(erule fold1Set.cases, simp_all)
2290 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
2292 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
2295 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
2296 by (blast intro: fold_graph.intros elim: fold_graph.cases)
2298 lemma fold1_singleton [simp]: "fold1 f {a} = a"
2299 by (unfold fold1_def) blast
2301 lemma finite_nonempty_imp_fold1Set:
2302   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
2303 apply (induct A rule: finite_induct)
2304 apply (auto dest: finite_imp_fold_graph [of _ f])
2305 done
2307 text{*First, some lemmas about @{const fold_graph}.*}
2309 context ab_semigroup_mult
2310 begin
2312 lemma fun_left_comm: "fun_left_comm(op *)"
2313 by unfold_locales (simp add: mult_ac)
2315 lemma fold_graph_insert_swap:
2316 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
2317 shows "fold_graph times z (insert b A) (z * y)"
2318 proof -
2319   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2320 from assms show ?thesis
2321 proof (induct rule: fold_graph.induct)
2322   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
2323 next
2324   case (insertI x A y)
2325     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
2326       using insertI by force  --{*how does @{term id} get unfolded?*}
2327     thus ?case by (simp add: insert_commute mult_ac)
2328 qed
2329 qed
2331 lemma fold_graph_permute_diff:
2332 assumes fold: "fold_graph times b A x"
2333 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
2334 using fold
2335 proof (induct rule: fold_graph.induct)
2336   case emptyI thus ?case by simp
2337 next
2338   case (insertI x A y)
2339   have "a = x \<or> a \<in> A" using insertI by simp
2340   thus ?case
2341   proof
2342     assume "a = x"
2343     with insertI show ?thesis
2344       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
2345   next
2346     assume ainA: "a \<in> A"
2347     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
2348       using insertI by force
2349     moreover
2350     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
2351       using ainA insertI by blast
2352     ultimately show ?thesis by simp
2353   qed
2354 qed
2356 lemma fold1_eq_fold:
2357 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
2358 proof -
2359   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2360   from assms show ?thesis
2361 apply (simp add: fold1_def fold_def)
2362 apply (rule the_equality)
2363 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
2364 apply (rule sym, clarify)
2365 apply (case_tac "Aa=A")
2366  apply (best intro: the_equality fold_graph_determ)
2367 apply (subgoal_tac "fold_graph times a A x")
2368  apply (best intro: the_equality fold_graph_determ)
2369 apply (subgoal_tac "insert aa (Aa - {a}) = A")
2370  prefer 2 apply (blast elim: equalityE)
2371 apply (auto dest: fold_graph_permute_diff [where a=a])
2372 done
2373 qed
2375 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
2376 apply safe
2377  apply simp
2378  apply (drule_tac x=x in spec)
2379  apply (drule_tac x="A-{x}" in spec, auto)
2380 done
2382 lemma fold1_insert:
2383   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
2384   shows "fold1 times (insert x A) = x * fold1 times A"
2385 proof -
2386   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2387   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
2388     by (auto simp add: nonempty_iff)
2389   with A show ?thesis
2390     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
2391 qed
2393 end
2395 context ab_semigroup_idem_mult
2396 begin
2398 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
2399 apply unfold_locales
2401 apply (simp add: mult_idem mult_assoc[symmetric])
2402 done
2405 lemma fold1_insert_idem [simp]:
2406   assumes nonempty: "A \<noteq> {}" and A: "finite A"
2407   shows "fold1 times (insert x A) = x * fold1 times A"
2408 proof -
2409   interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
2410     by (rule fun_left_comm_idem)
2411   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
2412     by (auto simp add: nonempty_iff)
2413   show ?thesis
2414   proof cases
2415     assume "a = x"
2416     thus ?thesis
2417     proof cases
2418       assume "A' = {}"
2419       with prems show ?thesis by (simp add: mult_idem)
2420     next
2421       assume "A' \<noteq> {}"
2422       with prems show ?thesis
2423 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
2424     qed
2425   next
2426     assume "a \<noteq> x"
2427     with prems show ?thesis
2428       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
2429   qed
2430 qed
2432 lemma hom_fold1_commute:
2433 assumes hom: "!!x y. h (x * y) = h x * h y"
2434 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
2435 using N proof (induct rule: finite_ne_induct)
2436   case singleton thus ?case by simp
2437 next
2438   case (insert n N)
2439   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
2440   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
2441   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
2442   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
2443     using insert by(simp)
2444   also have "insert (h n) (h ` N) = h ` insert n N" by simp
2445   finally show ?case .
2446 qed
2448 end
2451 text{* Now the recursion rules for definitions: *}
2453 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
2456 lemma (in ab_semigroup_mult) fold1_insert_def:
2457   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
2460 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
2461   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
2462 by simp
2464 subsubsection{* Determinacy for @{term fold1Set} *}
2466 (*Not actually used!!*)
2467 (*
2468 context ab_semigroup_mult
2469 begin
2471 lemma fold_graph_permute:
2472   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
2473    ==> fold_graph times id a (insert b A) x"
2474 apply (cases "a=b")
2475 apply (auto dest: fold_graph_permute_diff)
2476 done
2478 lemma fold1Set_determ:
2479   "fold1Set times A x ==> fold1Set times A y ==> y = x"
2480 proof (clarify elim!: fold1Set.cases)
2481   fix A x B y a b
2482   assume Ax: "fold_graph times id a A x"
2483   assume By: "fold_graph times id b B y"
2484   assume anotA:  "a \<notin> A"
2485   assume bnotB:  "b \<notin> B"
2486   assume eq: "insert a A = insert b B"
2487   show "y=x"
2488   proof cases
2489     assume same: "a=b"
2490     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
2491     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
2492   next
2493     assume diff: "a\<noteq>b"
2494     let ?D = "B - {a}"
2495     have B: "B = insert a ?D" and A: "A = insert b ?D"
2496      and aB: "a \<in> B" and bA: "b \<in> A"
2497       using eq anotA bnotB diff by (blast elim!:equalityE)+
2498     with aB bnotB By
2499     have "fold_graph times id a (insert b ?D) y"
2500       by (auto intro: fold_graph_permute simp add: insert_absorb)
2501     moreover
2502     have "fold_graph times id a (insert b ?D) x"
2503       by (simp add: A [symmetric] Ax)
2504     ultimately show ?thesis by (blast intro: fold_graph_determ)
2505   qed
2506 qed
2508 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
2509   by (unfold fold1_def) (blast intro: fold1Set_determ)
2511 end
2512 *)
2514 declare
2515   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
2516   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
2517   -- {* No more proofs involve these relations. *}
2519 subsubsection {* Lemmas about @{text fold1} *}
2521 context ab_semigroup_mult
2522 begin
2524 lemma fold1_Un:
2525 assumes A: "finite A" "A \<noteq> {}"
2526 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
2527        fold1 times (A Un B) = fold1 times A * fold1 times B"
2528 using A by (induct rule: finite_ne_induct)
2531 lemma fold1_in:
2532   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
2533   shows "fold1 times A \<in> A"
2534 using A
2535 proof (induct rule:finite_ne_induct)
2536   case singleton thus ?case by simp
2537 next
2538   case insert thus ?case using elem by (force simp add:fold1_insert)
2539 qed
2541 end
2543 lemma (in ab_semigroup_idem_mult) fold1_Un2:
2544 assumes A: "finite A" "A \<noteq> {}"
2545 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
2546        fold1 times (A Un B) = fold1 times A * fold1 times B"
2547 using A
2548 proof(induct rule:finite_ne_induct)
2549   case singleton thus ?case by simp
2550 next
2551   case insert thus ?case by (simp add: mult_assoc)
2552 qed
2555 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
2557 text{*
2558   As an application of @{text fold1} we define infimum
2559   and supremum in (not necessarily complete!) lattices
2560   over (non-empty) sets by means of @{text fold1}.
2561 *}
2563 context lower_semilattice
2564 begin
2566 lemma ab_semigroup_idem_mult_inf:
2567   "ab_semigroup_idem_mult inf"
2568   proof qed (rule inf_assoc inf_commute inf_idem)+
2570 lemma below_fold1_iff:
2571   assumes "finite A" "A \<noteq> {}"
2572   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2573 proof -
2574   interpret ab_semigroup_idem_mult inf
2575     by (rule ab_semigroup_idem_mult_inf)
2576   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
2577 qed
2579 lemma fold1_belowI:
2580   assumes "finite A"
2581     and "a \<in> A"
2582   shows "fold1 inf A \<le> a"
2583 proof -
2584   from assms have "A \<noteq> {}" by auto
2585   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
2586   proof (induct rule: finite_ne_induct)
2587     case singleton thus ?case by simp
2588   next
2589     interpret ab_semigroup_idem_mult inf
2590       by (rule ab_semigroup_idem_mult_inf)
2591     case (insert x F)
2592     from insert(5) have "a = x \<or> a \<in> F" by simp
2593     thus ?case
2594     proof
2595       assume "a = x" thus ?thesis using insert
2597     next
2598       assume "a \<in> F"
2599       hence bel: "fold1 inf F \<le> a" by (rule insert)
2600       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
2601         using insert by (simp add: mult_ac)
2602       also have "inf (fold1 inf F) a = fold1 inf F"
2603         using bel by (auto intro: antisym)
2604       also have "inf x \<dots> = fold1 inf (insert x F)"
2605         using insert by (simp add: mult_ac)
2606       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
2607       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
2608       ultimately show ?thesis by simp
2609     qed
2610   qed
2611 qed
2613 end
2615 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
2616   "ab_semigroup_idem_mult sup"
2617   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
2618     (rule dual_lattice)
2620 context lattice
2621 begin
2623 definition
2624   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
2625 where
2626   "Inf_fin = fold1 inf"
2628 definition
2629   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
2630 where
2631   "Sup_fin = fold1 sup"
2633 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
2634 apply(unfold Sup_fin_def Inf_fin_def)
2635 apply(subgoal_tac "EX a. a:A")
2636 prefer 2 apply blast
2637 apply(erule exE)
2638 apply(rule order_trans)
2639 apply(erule (1) fold1_belowI)
2640 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
2641 done
2643 lemma sup_Inf_absorb [simp]:
2644   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
2645 apply(subst sup_commute)
2646 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
2647 done
2649 lemma inf_Sup_absorb [simp]:
2650   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
2651 by (simp add: Sup_fin_def inf_absorb1
2652   lower_semilattice.fold1_belowI [OF dual_lattice])
2654 end
2656 context distrib_lattice
2657 begin
2659 lemma sup_Inf1_distrib:
2660   assumes "finite A"
2661     and "A \<noteq> {}"
2662   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
2663 proof -
2664   interpret ab_semigroup_idem_mult inf
2665     by (rule ab_semigroup_idem_mult_inf)
2666   from assms show ?thesis
2667     by (simp add: Inf_fin_def image_def
2668       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
2669         (rule arg_cong [where f="fold1 inf"], blast)
2670 qed
2672 lemma sup_Inf2_distrib:
2673   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
2674   shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
2675 using A proof (induct rule: finite_ne_induct)
2676   case singleton thus ?case
2677     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
2678 next
2679   interpret ab_semigroup_idem_mult inf
2680     by (rule ab_semigroup_idem_mult_inf)
2681   case (insert x A)
2682   have finB: "finite {sup x b |b. b \<in> B}"
2683     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
2684   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
2685   proof -
2686     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
2687       by blast
2688     thus ?thesis by(simp add: insert(1) B(1))
2689   qed
2690   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
2691   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
2692     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
2693   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
2694   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
2695     using insert by(simp add:sup_Inf1_distrib[OF B])
2696   also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
2697     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
2698     using B insert
2699     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
2700   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
2701     by blast
2702   finally show ?case .
2703 qed
2705 lemma inf_Sup1_distrib:
2706   assumes "finite A" and "A \<noteq> {}"
2707   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
2708 proof -
2709   interpret ab_semigroup_idem_mult sup
2710     by (rule ab_semigroup_idem_mult_sup)
2711   from assms show ?thesis
2712     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
2713       (rule arg_cong [where f="fold1 sup"], blast)
2714 qed
2716 lemma inf_Sup2_distrib:
2717   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
2718   shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
2719 using A proof (induct rule: finite_ne_induct)
2720   case singleton thus ?case
2721     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
2722 next
2723   case (insert x A)
2724   have finB: "finite {inf x b |b. b \<in> B}"
2725     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
2726   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
2727   proof -
2728     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
2729       by blast
2730     thus ?thesis by(simp add: insert(1) B(1))
2731   qed
2732   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
2733   interpret ab_semigroup_idem_mult sup
2734     by (rule ab_semigroup_idem_mult_sup)
2735   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
2736     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
2737   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
2738   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
2739     using insert by(simp add:inf_Sup1_distrib[OF B])
2740   also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
2741     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
2742     using B insert
2743     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
2744   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
2745     by blast
2746   finally show ?case .
2747 qed
2749 end
2751 context complete_lattice
2752 begin
2754 text {*
2755   Coincidence on finite sets in complete lattices:
2756 *}
2758 lemma Inf_fin_Inf:
2759   assumes "finite A" and "A \<noteq> {}"
2760   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
2761 proof -
2762     interpret ab_semigroup_idem_mult inf
2763     by (rule ab_semigroup_idem_mult_inf)
2764   from assms show ?thesis
2765   unfolding Inf_fin_def by (induct A set: finite)
2767 qed
2769 lemma Sup_fin_Sup:
2770   assumes "finite A" and "A \<noteq> {}"
2771   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
2772 proof -
2773   interpret ab_semigroup_idem_mult sup
2774     by (rule ab_semigroup_idem_mult_sup)
2775   from assms show ?thesis
2776   unfolding Sup_fin_def by (induct A set: finite)
2778 qed
2780 end
2783 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
2785 text{*
2786   As an application of @{text fold1} we define minimum
2787   and maximum in (not necessarily complete!) linear orders
2788   over (non-empty) sets by means of @{text fold1}.
2789 *}
2791 context linorder
2792 begin
2794 lemma ab_semigroup_idem_mult_min:
2795   "ab_semigroup_idem_mult min"
2796   proof qed (auto simp add: min_def)
2798 lemma ab_semigroup_idem_mult_max:
2799   "ab_semigroup_idem_mult max"
2800   proof qed (auto simp add: max_def)
2802 lemma min_lattice:
2803   "lower_semilattice (op \<le>) (op <) min"
2804   proof qed (auto simp add: min_def)
2806 lemma max_lattice:
2807   "lower_semilattice (op \<ge>) (op >) max"
2808   proof qed (auto simp add: max_def)
2810 lemma dual_max:
2811   "ord.max (op \<ge>) = min"
2812   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
2814 lemma dual_min:
2815   "ord.min (op \<ge>) = max"
2816   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
2818 lemma strict_below_fold1_iff:
2819   assumes "finite A" and "A \<noteq> {}"
2820   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
2821 proof -
2822   interpret ab_semigroup_idem_mult min
2823     by (rule ab_semigroup_idem_mult_min)
2824   from assms show ?thesis
2825   by (induct rule: finite_ne_induct)
2827 qed
2829 lemma fold1_below_iff:
2830   assumes "finite A" and "A \<noteq> {}"
2831   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
2832 proof -
2833   interpret ab_semigroup_idem_mult min
2834     by (rule ab_semigroup_idem_mult_min)
2835   from assms show ?thesis
2836   by (induct rule: finite_ne_induct)
2838 qed
2840 lemma fold1_strict_below_iff:
2841   assumes "finite A" and "A \<noteq> {}"
2842   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
2843 proof -
2844   interpret ab_semigroup_idem_mult min
2845     by (rule ab_semigroup_idem_mult_min)
2846   from assms show ?thesis
2847   by (induct rule: finite_ne_induct)
2849 qed
2851 lemma fold1_antimono:
2852   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
2853   shows "fold1 min B \<le> fold1 min A"
2854 proof cases
2855   assume "A = B" thus ?thesis by simp
2856 next
2857   interpret ab_semigroup_idem_mult min
2858     by (rule ab_semigroup_idem_mult_min)
2859   assume "A \<noteq> B"
2860   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
2861   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
2862   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
2863   proof -
2864     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
2865     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
2866     moreover have "(B-A) \<noteq> {}" using prems by blast
2867     moreover have "A Int (B-A) = {}" using prems by blast
2868     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
2869   qed
2870   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
2871   finally show ?thesis .
2872 qed
2874 definition
2875   Min :: "'a set \<Rightarrow> 'a"
2876 where
2877   "Min = fold1 min"
2879 definition
2880   Max :: "'a set \<Rightarrow> 'a"
2881 where
2882   "Max = fold1 max"
2884 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
2885 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
2887 lemma Min_insert [simp]:
2888   assumes "finite A" and "A \<noteq> {}"
2889   shows "Min (insert x A) = min x (Min A)"
2890 proof -
2891   interpret ab_semigroup_idem_mult min
2892     by (rule ab_semigroup_idem_mult_min)
2893   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
2894 qed
2896 lemma Max_insert [simp]:
2897   assumes "finite A" and "A \<noteq> {}"
2898   shows "Max (insert x A) = max x (Max A)"
2899 proof -
2900   interpret ab_semigroup_idem_mult max
2901     by (rule ab_semigroup_idem_mult_max)
2902   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
2903 qed
2905 lemma Min_in [simp]:
2906   assumes "finite A" and "A \<noteq> {}"
2907   shows "Min A \<in> A"
2908 proof -
2909   interpret ab_semigroup_idem_mult min
2910     by (rule ab_semigroup_idem_mult_min)
2911   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
2912 qed
2914 lemma Max_in [simp]:
2915   assumes "finite A" and "A \<noteq> {}"
2916   shows "Max A \<in> A"
2917 proof -
2918   interpret ab_semigroup_idem_mult max
2919     by (rule ab_semigroup_idem_mult_max)
2920   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
2921 qed
2923 lemma Min_Un:
2924   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2925   shows "Min (A \<union> B) = min (Min A) (Min B)"
2926 proof -
2927   interpret ab_semigroup_idem_mult min
2928     by (rule ab_semigroup_idem_mult_min)
2929   from assms show ?thesis
2930     by (simp add: Min_def fold1_Un2)
2931 qed
2933 lemma Max_Un:
2934   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2935   shows "Max (A \<union> B) = max (Max A) (Max B)"
2936 proof -
2937   interpret ab_semigroup_idem_mult max
2938     by (rule ab_semigroup_idem_mult_max)
2939   from assms show ?thesis
2940     by (simp add: Max_def fold1_Un2)
2941 qed
2943 lemma hom_Min_commute:
2944   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
2945     and "finite N" and "N \<noteq> {}"
2946   shows "h (Min N) = Min (h ` N)"
2947 proof -
2948   interpret ab_semigroup_idem_mult min
2949     by (rule ab_semigroup_idem_mult_min)
2950   from assms show ?thesis
2951     by (simp add: Min_def hom_fold1_commute)
2952 qed
2954 lemma hom_Max_commute:
2955   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
2956     and "finite N" and "N \<noteq> {}"
2957   shows "h (Max N) = Max (h ` N)"
2958 proof -
2959   interpret ab_semigroup_idem_mult max
2960     by (rule ab_semigroup_idem_mult_max)
2961   from assms show ?thesis
2962     by (simp add: Max_def hom_fold1_commute [of h])
2963 qed
2965 lemma Min_le [simp]:
2966   assumes "finite A" and "x \<in> A"
2967   shows "Min A \<le> x"
2968 proof -
2969   interpret lower_semilattice "op \<le>" "op <" min
2970     by (rule min_lattice)
2971   from assms show ?thesis by (simp add: Min_def fold1_belowI)
2972 qed
2974 lemma Max_ge [simp]:
2975   assumes "finite A" and "x \<in> A"
2976   shows "x \<le> Max A"
2977 proof -
2978   interpret lower_semilattice "op \<ge>" "op >" max
2979     by (rule max_lattice)
2980   from assms show ?thesis by (simp add: Max_def fold1_belowI)
2981 qed
2983 lemma Min_ge_iff [simp, noatp]:
2984   assumes "finite A" and "A \<noteq> {}"
2985   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2986 proof -
2987   interpret lower_semilattice "op \<le>" "op <" min
2988     by (rule min_lattice)
2989   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
2990 qed
2992 lemma Max_le_iff [simp, noatp]:
2993   assumes "finite A" and "A \<noteq> {}"
2994   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
2995 proof -
2996   interpret lower_semilattice "op \<ge>" "op >" max
2997     by (rule max_lattice)
2998   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
2999 qed
3001 lemma Min_gr_iff [simp, noatp]:
3002   assumes "finite A" and "A \<noteq> {}"
3003   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
3004 proof -
3005   interpret lower_semilattice "op \<le>" "op <" min
3006     by (rule min_lattice)
3007   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
3008 qed
3010 lemma Max_less_iff [simp, noatp]:
3011   assumes "finite A" and "A \<noteq> {}"
3012   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
3013 proof -
3014   note Max = Max_def
3015   interpret linorder "op \<ge>" "op >"
3016     by (rule dual_linorder)
3017   from assms show ?thesis
3018     by (simp add: Max strict_below_fold1_iff [folded dual_max])
3019 qed
3021 lemma Min_le_iff [noatp]:
3022   assumes "finite A" and "A \<noteq> {}"
3023   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
3024 proof -
3025   interpret lower_semilattice "op \<le>" "op <" min
3026     by (rule min_lattice)
3027   from assms show ?thesis
3028     by (simp add: Min_def fold1_below_iff)
3029 qed
3031 lemma Max_ge_iff [noatp]:
3032   assumes "finite A" and "A \<noteq> {}"
3033   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
3034 proof -
3035   note Max = Max_def
3036   interpret linorder "op \<ge>" "op >"
3037     by (rule dual_linorder)
3038   from assms show ?thesis
3039     by (simp add: Max fold1_below_iff [folded dual_max])
3040 qed
3042 lemma Min_less_iff [noatp]:
3043   assumes "finite A" and "A \<noteq> {}"
3044   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
3045 proof -
3046   interpret lower_semilattice "op \<le>" "op <" min
3047     by (rule min_lattice)
3048   from assms show ?thesis
3049     by (simp add: Min_def fold1_strict_below_iff)
3050 qed
3052 lemma Max_gr_iff [noatp]:
3053   assumes "finite A" and "A \<noteq> {}"
3054   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
3055 proof -
3056   note Max = Max_def
3057   interpret linorder "op \<ge>" "op >"
3058     by (rule dual_linorder)
3059   from assms show ?thesis
3060     by (simp add: Max fold1_strict_below_iff [folded dual_max])
3061 qed
3063 lemma Min_antimono:
3064   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
3065   shows "Min N \<le> Min M"
3066 proof -
3067   interpret distrib_lattice "op \<le>" "op <" min max
3068     by (rule distrib_lattice_min_max)
3069   from assms show ?thesis by (simp add: Min_def fold1_antimono)
3070 qed
3072 lemma Max_mono:
3073   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
3074   shows "Max M \<le> Max N"
3075 proof -
3076   note Max = Max_def
3077   interpret linorder "op \<ge>" "op >"
3078     by (rule dual_linorder)
3079   from assms show ?thesis
3080     by (simp add: Max fold1_antimono [folded dual_max])
3081 qed
3083 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
3084  "finite A \<Longrightarrow> P {} \<Longrightarrow>
3085   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
3086   \<Longrightarrow> P A"
3087 proof (induct A rule: measure_induct_rule[where f=card])
3088   fix A :: "'a set"
3089   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
3090                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
3091                   \<Longrightarrow> P B"
3092   and "finite A" and "P {}"
3093   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
3094   show "P A"
3095   proof (cases "A = {}")
3096     assume "A = {}" thus "P A" using `P {}` by simp
3097   next
3098     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
3099     assume "A \<noteq> {}"
3100     with `finite A` have "Max A : A" by auto
3101     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
3102     note card_Diff1_less[OF `finite A` `Max A : A`]
3103     moreover have "finite ?B" using `finite A` by simp
3104     ultimately have "P ?B" using `P {}` step IH by blast
3105     moreover have "\<forall>a\<in>?B. a < Max A"
3106       using Max_ge [OF `finite A`] by fastsimp
3107     ultimately show "P A"
3108       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
3109   qed
3110 qed
3112 end
3115 begin
3118   fixes k
3119   assumes "finite N" and "N \<noteq> {}"
3120   shows "k + Min N = Min {k + m | m. m \<in> N}"
3121 proof -
3122   have "\<And>x y. k + min x y = min (k + x) (k + y)"
3123     by (simp add: min_def not_le)
3124       (blast intro: antisym less_imp_le add_left_mono)
3125   with assms show ?thesis
3126     using hom_Min_commute [of "plus k" N]
3127     by simp (blast intro: arg_cong [where f = Min])
3128 qed