src/HOL/Big_Operators.thy
 author nipkow Wed Aug 15 12:18:30 2012 +0200 (2012-08-15) changeset 48819 6cf7a9d8bbaf parent 46904 f30e941b4512 child 48820 bfd136281c13 permissions -rw-r--r--
abstracted lemmas
1 (*  Title:      HOL/Big_Operators.thy
2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
3                 with contributions by Jeremy Avigad
4 *)
6 header {* Big operators and finite (non-empty) sets *}
8 theory Big_Operators
9 imports Plain
10 begin
12 subsection {* Generic monoid operation over a set *}
14 no_notation times (infixl "*" 70)
15 no_notation Groups.one ("1")
17 locale comm_monoid_big = comm_monoid +
18   fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
19   assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
21 sublocale comm_monoid_big < folding_image proof
22 qed (simp add: F_eq)
24 context comm_monoid_big
25 begin
27 lemma infinite [simp]:
28   "\<not> finite A \<Longrightarrow> F g A = 1"
29   by (simp add: F_eq)
31 lemma F_cong:
32   assumes "A = B" "\<And>x. x \<in> B \<Longrightarrow> h x = g x"
33   shows "F h A = F g B"
34 proof cases
35   assume "finite A"
36   with assms show ?thesis unfolding `A = B` by (simp cong: cong)
37 next
38   assume "\<not> finite A"
39   then show ?thesis unfolding `A = B` by simp
40 qed
42 lemma F_unit[simp]: "F (%i. 1) A = 1"
43 by (cases "finite A") (erule finite_induct, auto)
45 lemma F_unit': "ALL a:A. g a = 1 ==> F g A = 1"
46 by (simp add:F_cong)
48 lemma If_cases:
49   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
50   assumes fA: "finite A"
51   shows "F (\<lambda>x. if P x then h x else g x) A =
52          F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
53 proof-
54   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
55           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
56     by blast+
57   from fA
58   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
59   let ?g = "\<lambda>x. if P x then h x else g x"
60   from union_disjoint[OF f a(2), of ?g] a(1)
61   show ?thesis
62     by (subst (1 2) F_cong) simp_all
63 qed
65 end
67 text {* for ad-hoc proofs for @{const fold_image} *}
69 lemma (in comm_monoid_add) comm_monoid_mult:
70   "class.comm_monoid_mult (op +) 0"
71 proof qed (auto intro: add_assoc add_commute)
73 notation times (infixl "*" 70)
74 notation Groups.one ("1")
77 subsection {* Generalized summation over a set *}
79 definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
80   "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
82 sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
83 qed (fact setsum_def)
85 abbreviation
86   Setsum  ("\<Sum>_"  999) where
87   "\<Sum>A == setsum (%x. x) A"
89 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
90 written @{text"\<Sum>x\<in>A. e"}. *}
92 syntax
93   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
94 syntax (xsymbols)
95   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
96 syntax (HTML output)
97   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
99 translations -- {* Beware of argument permutation! *}
100   "SUM i:A. b" == "CONST setsum (%i. b) A"
101   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
103 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
104  @{text"\<Sum>x|P. e"}. *}
106 syntax
107   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
108 syntax (xsymbols)
109   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
110 syntax (HTML output)
111   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
113 translations
114   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
115   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
117 print_translation {*
118 let
119   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) \$ Abs (y, Ty, P)] =
120         if x <> y then raise Match
121         else
122           let
123             val x' = Syntax_Trans.mark_bound x;
124             val t' = subst_bound (x', t);
125             val P' = subst_bound (x', P);
126           in Syntax.const @{syntax_const "_qsetsum"} \$ Syntax_Trans.mark_bound x \$ P' \$ t' end
127     | setsum_tr' _ = raise Match;
128 in [(@{const_syntax setsum}, setsum_tr')] end
129 *}
131 lemma setsum_empty:
132   "setsum f {} = 0"
133   by (fact setsum.empty)
135 lemma setsum_insert:
136   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
137   by (fact setsum.insert)
139 lemma setsum_infinite:
140   "~ finite A ==> setsum f A = 0"
141   by (fact setsum.infinite)
143 lemma (in comm_monoid_add) setsum_reindex:
144   assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
145 proof -
146   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
147   from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
148 qed
150 lemma (in comm_monoid_add) setsum_reindex_id:
151   "inj_on f B ==> setsum f B = setsum id (f ` B)"
152   by (simp add: setsum_reindex)
154 lemma (in comm_monoid_add) setsum_reindex_nonzero:
155   assumes fS: "finite S"
156   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"
157   shows "setsum h (f ` S) = setsum (h o f) S"
158 using nz
159 proof(induct rule: finite_induct[OF fS])
160   case 1 thus ?case by simp
161 next
162   case (2 x F)
163   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
164     then obtain y where y: "y \<in> F" "f x = f y" by auto
165     from "2.hyps" y have xy: "x \<noteq> y" by auto
167     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
168     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
169     also have "\<dots> = setsum (h o f) (insert x F)"
170       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
171       using h0
172       apply simp
173       apply (rule "2.hyps"(3))
174       apply (rule_tac y="y" in  "2.prems")
175       apply simp_all
176       done
177     finally have ?case .}
178   moreover
179   {assume fxF: "f x \<notin> f ` F"
180     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
181       using fxF "2.hyps" by simp
182     also have "\<dots> = setsum (h o f) (insert x F)"
183       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
184       apply simp
185       apply (rule cong [OF refl [of "op + (h (f x))"]])
186       apply (rule "2.hyps"(3))
187       apply (rule_tac y="y" in  "2.prems")
188       apply simp_all
189       done
190     finally have ?case .}
191   ultimately show ?case by blast
192 qed
194 lemma (in comm_monoid_add) setsum_cong:
195   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
196   by (cases "finite A") (auto intro: setsum.cong)
198 lemma (in comm_monoid_add) strong_setsum_cong [cong]:
199   "A = B ==> (!!x. x:B =simp=> f x = g x)
200    ==> setsum (%x. f x) A = setsum (%x. g x) B"
201   by (rule setsum_cong) (simp_all add: simp_implies_def)
203 lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
204   by (auto intro: setsum_cong)
206 lemma (in comm_monoid_add) setsum_reindex_cong:
207    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
208     ==> setsum h B = setsum g A"
209   by (simp add: setsum_reindex)
211 lemmas setsum_0 = setsum.F_unit
212 lemmas setsum_0' = setsum.F_unit'
214 lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
215   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
216   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
217   by (fact setsum.union_inter)
219 lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
220   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
221   by (fact setsum.union_disjoint)
223 lemma setsum_mono_zero_left:
224   assumes fT: "finite T" and ST: "S \<subseteq> T"
225   and z: "\<forall>i \<in> T - S. f i = 0"
226   shows "setsum f S = setsum f T"
227 proof-
228   have eq: "T = S \<union> (T - S)" using ST by blast
229   have d: "S \<inter> (T - S) = {}" using ST by blast
230   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
231   show ?thesis
232   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
233 qed
235 lemma setsum_mono_zero_right:
236   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
237 by(blast intro!: setsum_mono_zero_left[symmetric])
239 lemma setsum_mono_zero_cong_left:
240   assumes fT: "finite T" and ST: "S \<subseteq> T"
241   and z: "\<forall>i \<in> T - S. g i = 0"
242   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
243   shows "setsum f S = setsum g T"
244 proof-
245   have eq: "T = S \<union> (T - S)" using ST by blast
246   have d: "S \<inter> (T - S) = {}" using ST by blast
247   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
248   show ?thesis
249     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
250 qed
252 lemma setsum_mono_zero_cong_right:
253   assumes fT: "finite T" and ST: "S \<subseteq> T"
254   and z: "\<forall>i \<in> T - S. f i = 0"
255   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
256   shows "setsum f T = setsum g S"
257 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
259 lemma setsum_delta:
260   assumes fS: "finite S"
261   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
262 proof-
263   let ?f = "(\<lambda>k. if k=a then b k else 0)"
264   {assume a: "a \<notin> S"
265     hence "\<forall> k\<in> S. ?f k = 0" by simp
266     hence ?thesis  using a by simp}
267   moreover
268   {assume a: "a \<in> S"
269     let ?A = "S - {a}"
270     let ?B = "{a}"
271     have eq: "S = ?A \<union> ?B" using a by blast
272     have dj: "?A \<inter> ?B = {}" by simp
273     from fS have fAB: "finite ?A" "finite ?B" by auto
274     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
275       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
276       by simp
277     then have ?thesis  using a by simp}
278   ultimately show ?thesis by blast
279 qed
280 lemma setsum_delta':
281   assumes fS: "finite S" shows
282   "setsum (\<lambda>k. if a = k then b k else 0) S =
283      (if a\<in> S then b a else 0)"
284   using setsum_delta[OF fS, of a b, symmetric]
285   by (auto intro: setsum_cong)
287 lemma setsum_restrict_set:
288   assumes fA: "finite A"
289   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
290 proof-
291   from fA have fab: "finite (A \<inter> B)" by auto
292   have aba: "A \<inter> B \<subseteq> A" by blast
293   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
294   from setsum_mono_zero_left[OF fA aba, of ?g]
295   show ?thesis by simp
296 qed
298 lemma setsum_cases:
299   assumes fA: "finite A"
300   shows "setsum (\<lambda>x. if P x then f x else g x) A =
301          setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
302   using setsum.If_cases[OF fA] .
304 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
305   the lhs need not be, since UNION I A could still be finite.*)
306 lemma (in comm_monoid_add) setsum_UN_disjoint:
307   assumes "finite I" and "ALL i:I. finite (A i)"
308     and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
309   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
310 proof -
311   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
312   from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
313 qed
315 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
316 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
317 lemma setsum_Union_disjoint:
318   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
319   shows "setsum f (Union C) = setsum (setsum f) C"
320 proof cases
321   assume "finite C"
322   from setsum_UN_disjoint[OF this assms]
323   show ?thesis
324     by (simp add: SUP_def)
325 qed (force dest: finite_UnionD simp add: setsum_def)
327 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
328   the rhs need not be, since SIGMA A B could still be finite.*)
329 lemma (in comm_monoid_add) setsum_Sigma:
330   assumes "finite A" and  "ALL x:A. finite (B x)"
331   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
332 proof -
333   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
334   from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
335 qed
337 text{*Here we can eliminate the finiteness assumptions, by cases.*}
338 lemma setsum_cartesian_product:
339    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
340 apply (cases "finite A")
341  apply (cases "finite B")
342   apply (simp add: setsum_Sigma)
343  apply (cases "A={}", simp)
344  apply (simp)
345 apply (auto simp add: setsum_def
346             dest: finite_cartesian_productD1 finite_cartesian_productD2)
347 done
349 lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
350   by (cases "finite A") (simp_all add: setsum.distrib)
353 subsubsection {* Properties in more restricted classes of structures *}
355 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
356 apply (case_tac "finite A")
357  prefer 2 apply (simp add: setsum_def)
358 apply (erule rev_mp)
359 apply (erule finite_induct, auto)
360 done
362 lemma setsum_eq_0_iff [simp]:
363     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
364 by (induct set: finite) auto
366 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
367   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
368 apply(erule finite_induct)
370 done
372 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
374 lemma setsum_Un_nat: "finite A ==> finite B ==>
375   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
376   -- {* For the natural numbers, we have subtraction. *}
377 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
379 lemma setsum_Un: "finite A ==> finite B ==>
380   (setsum f (A Un B) :: 'a :: ab_group_add) =
381    setsum f A + setsum f B - setsum f (A Int B)"
382 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
384 lemma (in comm_monoid_add) setsum_eq_general_reverses:
385   assumes fS: "finite S" and fT: "finite T"
386   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
387   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
388   shows "setsum f S = setsum g T"
389 proof -
390   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
391   show ?thesis
392   apply (simp add: setsum_def fS fT)
393   apply (rule fold_image_eq_general_inverses)
394   apply (rule fS)
395   apply (erule kh)
396   apply (erule hk)
397   done
398 qed
400 lemma (in comm_monoid_add) setsum_Un_zero:
401   assumes fS: "finite S" and fT: "finite T"
402   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
403   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
404 proof -
405   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
406   show ?thesis
407   using fS fT
408   apply (simp add: setsum_def)
409   apply (rule fold_image_Un_one)
410   using I0 by auto
411 qed
413 lemma setsum_UNION_zero:
414   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
415   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"
416   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
417   using fSS f0
418 proof(induct rule: finite_induct[OF fS])
419   case 1 thus ?case by simp
420 next
421   case (2 T F)
422   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
423     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
424   from fTF have fUF: "finite (\<Union>F)" by auto
425   from "2.prems" TF fTF
426   show ?case
427     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
428 qed
430 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
431   (if a:A then setsum f A - f a else setsum f A)"
432 apply (case_tac "finite A")
433  prefer 2 apply (simp add: setsum_def)
434 apply (erule finite_induct)
435  apply (auto simp add: insert_Diff_if)
436 apply (drule_tac a = a in mk_disjoint_insert, auto)
437 done
439 lemma setsum_diff1: "finite A \<Longrightarrow>
440   (setsum f (A - {a}) :: ('a::ab_group_add)) =
441   (if a:A then setsum f A - f a else setsum f A)"
442 by (erule finite_induct) (auto simp add: insert_Diff_if)
444 lemma setsum_diff1'[rule_format]:
445   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
446 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))"])
447 apply (auto simp add: insert_Diff_if add_ac)
448 done
450 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
451   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
452 unfolding setsum_diff1'[OF assms] by auto
454 (* By Jeremy Siek: *)
456 lemma setsum_diff_nat:
457 assumes "finite B" and "B \<subseteq> A"
458 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
459 using assms
460 proof induct
461   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
462 next
463   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
464     and xFinA: "insert x F \<subseteq> A"
465     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
466   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
467   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
468     by (simp add: setsum_diff1_nat)
469   from xFinA have "F \<subseteq> A" by simp
470   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
471   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
472     by simp
473   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
474   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
475     by simp
476   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
477   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
478     by simp
479   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
480 qed
482 lemma setsum_diff:
483   assumes le: "finite A" "B \<subseteq> A"
484   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
485 proof -
486   from le have finiteB: "finite B" using finite_subset by auto
487   show ?thesis using finiteB le
488   proof induct
489     case empty
490     thus ?case by auto
491   next
492     case (insert x F)
493     thus ?case using le finiteB
494       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
495   qed
496 qed
498 lemma setsum_mono:
499   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
500   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
501 proof (cases "finite K")
502   case True
503   thus ?thesis using le
504   proof induct
505     case empty
506     thus ?case by simp
507   next
508     case insert
509     thus ?case using add_mono by fastforce
510   qed
511 next
512   case False
513   thus ?thesis
514     by (simp add: setsum_def)
515 qed
517 lemma setsum_strict_mono:
518   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
519   assumes "finite A"  "A \<noteq> {}"
520     and "!!x. x:A \<Longrightarrow> f x < g x"
521   shows "setsum f A < setsum g A"
522   using assms
523 proof (induct rule: finite_ne_induct)
524   case singleton thus ?case by simp
525 next
526   case insert thus ?case by (auto simp: add_strict_mono)
527 qed
529 lemma setsum_strict_mono_ex1:
530 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
531 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
532 shows "setsum f A < setsum g A"
533 proof-
534   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
535   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
536     by(simp add:insert_absorb[OF `a:A`])
537   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
538     using `finite A` by(subst setsum_Un_disjoint) auto
539   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
540     by(rule setsum_mono)(simp add: assms(2))
541   also have "setsum f {a} < setsum g {a}" using a by simp
542   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
543     using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
544   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
545   finally show ?thesis by (metis add_right_mono add_strict_left_mono)
546 qed
548 lemma setsum_negf:
549   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
550 proof (cases "finite A")
551   case True thus ?thesis by (induct set: finite) auto
552 next
553   case False thus ?thesis by (simp add: setsum_def)
554 qed
556 lemma setsum_subtractf:
557   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
558     setsum f A - setsum g A"
559 proof (cases "finite A")
560   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
561 next
562   case False thus ?thesis by (simp add: setsum_def)
563 qed
565 lemma setsum_nonneg:
566   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
567   shows "0 \<le> setsum f A"
568 proof (cases "finite A")
569   case True thus ?thesis using nn
570   proof induct
571     case empty then show ?case by simp
572   next
573     case (insert x F)
574     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
575     with insert show ?case by simp
576   qed
577 next
578   case False thus ?thesis by (simp add: setsum_def)
579 qed
581 lemma setsum_nonpos:
582   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
583   shows "setsum f A \<le> 0"
584 proof (cases "finite A")
585   case True thus ?thesis using np
586   proof induct
587     case empty then show ?case by simp
588   next
589     case (insert x F)
590     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
591     with insert show ?case by simp
592   qed
593 next
594   case False thus ?thesis by (simp add: setsum_def)
595 qed
597 lemma setsum_nonneg_leq_bound:
598   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
599   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
600   shows "f i \<le> B"
601 proof -
602   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
603     using assms by (auto intro!: setsum_nonneg)
604   moreover
605   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
606     using assms by (simp add: setsum_diff1)
607   ultimately show ?thesis by auto
608 qed
610 lemma setsum_nonneg_0:
611   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
612   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
613   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
614   shows "f i = 0"
615   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
617 lemma setsum_mono2:
618 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
619 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
620 shows "setsum f A \<le> setsum f B"
621 proof -
622   have "setsum f A \<le> setsum f A + setsum f (B-A)"
623     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
624   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
625     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
626   also have "A \<union> (B-A) = B" using sub by blast
627   finally show ?thesis .
628 qed
630 lemma setsum_mono3: "finite B ==> A <= B ==>
631     ALL x: B - A.
633         setsum f A <= setsum f B"
634   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
635   apply (erule ssubst)
636   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
637   apply simp
638   apply (rule add_left_mono)
639   apply (erule setsum_nonneg)
640   apply (subst setsum_Un_disjoint [THEN sym])
641   apply (erule finite_subset, assumption)
642   apply (rule finite_subset)
643   prefer 2
644   apply assumption
645   apply (auto simp add: sup_absorb2)
646 done
648 lemma setsum_right_distrib:
649   fixes f :: "'a => ('b::semiring_0)"
650   shows "r * setsum f A = setsum (%n. r * f n) A"
651 proof (cases "finite A")
652   case True
653   thus ?thesis
654   proof induct
655     case empty thus ?case by simp
656   next
657     case (insert x A) thus ?case by (simp add: right_distrib)
658   qed
659 next
660   case False thus ?thesis by (simp add: setsum_def)
661 qed
663 lemma setsum_left_distrib:
664   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
665 proof (cases "finite A")
666   case True
667   then show ?thesis
668   proof induct
669     case empty thus ?case by simp
670   next
671     case (insert x A) thus ?case by (simp add: left_distrib)
672   qed
673 next
674   case False thus ?thesis by (simp add: setsum_def)
675 qed
677 lemma setsum_divide_distrib:
678   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
679 proof (cases "finite A")
680   case True
681   then show ?thesis
682   proof induct
683     case empty thus ?case by simp
684   next
685     case (insert x A) thus ?case by (simp add: add_divide_distrib)
686   qed
687 next
688   case False thus ?thesis by (simp add: setsum_def)
689 qed
691 lemma setsum_abs[iff]:
692   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
693   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
694 proof (cases "finite A")
695   case True
696   thus ?thesis
697   proof induct
698     case empty thus ?case by simp
699   next
700     case (insert x A)
701     thus ?case by (auto intro: abs_triangle_ineq order_trans)
702   qed
703 next
704   case False thus ?thesis by (simp add: setsum_def)
705 qed
707 lemma setsum_abs_ge_zero[iff]:
708   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
709   shows "0 \<le> setsum (%i. abs(f i)) A"
710 proof (cases "finite A")
711   case True
712   thus ?thesis
713   proof induct
714     case empty thus ?case by simp
715   next
716     case (insert x A) thus ?case by auto
717   qed
718 next
719   case False thus ?thesis by (simp add: setsum_def)
720 qed
722 lemma abs_setsum_abs[simp]:
723   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
724   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
725 proof (cases "finite A")
726   case True
727   thus ?thesis
728   proof induct
729     case empty thus ?case by simp
730   next
731     case (insert a A)
732     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
733     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
734     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
735       by (simp del: abs_of_nonneg)
736     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
737     finally show ?case .
738   qed
739 next
740   case False thus ?thesis by (simp add: setsum_def)
741 qed
743 lemma setsum_Plus:
744   fixes A :: "'a set" and B :: "'b set"
745   assumes fin: "finite A" "finite B"
746   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
747 proof -
748   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
749   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
750     by auto
751   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
752   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
753   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
754 qed
757 text {* Commuting outer and inner summation *}
759 lemma setsum_commute:
760   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
761 proof (simp add: setsum_cartesian_product)
762   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
763     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
764     (is "?s = _")
765     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
766     apply (simp add: split_def)
767     done
768   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
769     (is "_ = ?t")
770     apply (simp add: swap_product)
771     done
772   finally show "?s = ?t" .
773 qed
775 lemma setsum_product:
776   fixes f :: "'a => ('b::semiring_0)"
777   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
778   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
780 lemma setsum_mult_setsum_if_inj:
781 fixes f :: "'a => ('b::semiring_0)"
782 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
783   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
784 by(auto simp: setsum_product setsum_cartesian_product
785         intro!:  setsum_reindex_cong[symmetric])
787 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
788 apply (cases "finite A")
789 apply (erule finite_induct)
790 apply (auto simp add: algebra_simps)
791 done
793 lemma setsum_bounded:
794   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
795   shows "setsum f A \<le> of_nat(card A) * K"
796 proof (cases "finite A")
797   case True
798   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
799 next
800   case False thus ?thesis by (simp add: setsum_def)
801 qed
804 subsubsection {* Cardinality as special case of @{const setsum} *}
806 lemma card_eq_setsum:
807   "card A = setsum (\<lambda>x. 1) A"
808   by (simp only: card_def setsum_def)
810 lemma card_UN_disjoint:
811   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
812     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
813   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
814 proof -
815   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
816   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
817 qed
819 lemma card_Union_disjoint:
820   "finite C ==> (ALL A:C. finite A) ==>
821    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
822    ==> card (Union C) = setsum card C"
823 apply (frule card_UN_disjoint [of C id])
824 apply (simp_all add: SUP_def id_def)
825 done
827 text{*The image of a finite set can be expressed using @{term fold_image}.*}
828 lemma image_eq_fold_image:
829   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
830 proof (induct rule: finite_induct)
831   case empty then show ?case by simp
832 next
833   interpret ab_semigroup_mult "op Un"
834     proof qed auto
835   case insert
836   then show ?case by simp
837 qed
839 subsubsection {* Cardinality of products *}
841 lemma card_SigmaI [simp]:
842   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
843   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
844 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
846 (*
847 lemma SigmaI_insert: "y \<notin> A ==>
848   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
849   by auto
850 *)
852 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
853   by (cases "finite A \<and> finite B")
854     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
856 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
857 by (simp add: card_cartesian_product)
860 subsection {* Generalized product over a set *}
862 definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
863   "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
865 sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof
866 qed (fact setprod_def)
868 abbreviation
869   Setprod  ("\<Prod>_"  999) where
870   "\<Prod>A == setprod (%x. x) A"
872 syntax
873   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
874 syntax (xsymbols)
875   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
876 syntax (HTML output)
877   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
879 translations -- {* Beware of argument permutation! *}
880   "PROD i:A. b" == "CONST setprod (%i. b) A"
881   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
883 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
884  @{text"\<Prod>x|P. e"}. *}
886 syntax
887   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
888 syntax (xsymbols)
889   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
890 syntax (HTML output)
891   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
893 translations
894   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
895   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
897 lemma setprod_empty: "setprod f {} = 1"
898   by (fact setprod.empty)
900 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
901     setprod f (insert a A) = f a * setprod f A"
902   by (fact setprod.insert)
904 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
905   by (fact setprod.infinite)
907 lemma setprod_reindex:
908    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
909 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
911 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
912 by (auto simp add: setprod_reindex)
914 lemma setprod_cong:
915   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
916 by(fastforce simp: setprod_def intro: fold_image_cong)
918 lemma strong_setprod_cong[cong]:
919   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
920 by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
922 lemma setprod_reindex_cong: "inj_on f A ==>
923     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
924 by (frule setprod_reindex, simp)
926 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
927   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
928   shows "setprod h B = setprod g A"
929 proof-
930     have "setprod h B = setprod (h o f) A"
931       by (simp add: B setprod_reindex[OF i, of h])
932     then show ?thesis apply simp
933       apply (rule setprod_cong)
934       apply simp
935       by (simp add: eq)
936 qed
938 lemma setprod_Un_one:
939   assumes fS: "finite S" and fT: "finite T"
940   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
941   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
942   using fS fT
943   apply (simp add: setprod_def)
944   apply (rule fold_image_Un_one)
945   using I0 by auto
948 lemmas setprod_1 = setprod.F_unit
949 lemmas setprod_1' = setprod.F_unit'
952 lemma setprod_Un_Int: "finite A ==> finite B
953     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
954 by(simp add: setprod_def fold_image_Un_Int[symmetric])
956 lemma setprod_Un_disjoint: "finite A ==> finite B
957   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
958 by (subst setprod_Un_Int [symmetric], auto)
960 lemma setprod_mono_one_left:
961   assumes fT: "finite T" and ST: "S \<subseteq> T"
962   and z: "\<forall>i \<in> T - S. f i = 1"
963   shows "setprod f S = setprod f T"
964 proof-
965   have eq: "T = S \<union> (T - S)" using ST by blast
966   have d: "S \<inter> (T - S) = {}" using ST by blast
967   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
968   show ?thesis
969   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
970 qed
972 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
974 lemma setprod_delta:
975   assumes fS: "finite S"
976   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
977 proof-
978   let ?f = "(\<lambda>k. if k=a then b k else 1)"
979   {assume a: "a \<notin> S"
980     hence "\<forall> k\<in> S. ?f k = 1" by simp
981     hence ?thesis  using a by (simp add: setprod_1) }
982   moreover
983   {assume a: "a \<in> S"
984     let ?A = "S - {a}"
985     let ?B = "{a}"
986     have eq: "S = ?A \<union> ?B" using a by blast
987     have dj: "?A \<inter> ?B = {}" by simp
988     from fS have fAB: "finite ?A" "finite ?B" by auto
989     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
990     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
991       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
992       by simp
993     then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
994   ultimately show ?thesis by blast
995 qed
997 lemma setprod_delta':
998   assumes fS: "finite S" shows
999   "setprod (\<lambda>k. if a = k then b k else 1) S =
1000      (if a\<in> S then b a else 1)"
1001   using setprod_delta[OF fS, of a b, symmetric]
1002   by (auto intro: setprod_cong)
1005 lemma setprod_UN_disjoint:
1006     "finite I ==> (ALL i:I. finite (A i)) ==>
1007         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1008       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1009   by (simp add: setprod_def fold_image_UN_disjoint)
1011 lemma setprod_Union_disjoint:
1012   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
1013   shows "setprod f (Union C) = setprod (setprod f) C"
1014 proof cases
1015   assume "finite C"
1016   from setprod_UN_disjoint[OF this assms]
1017   show ?thesis
1018     by (simp add: SUP_def)
1019 qed (force dest: finite_UnionD simp add: setprod_def)
1021 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1022     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
1023     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1024 by(simp add:setprod_def fold_image_Sigma split_def)
1026 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1027 lemma setprod_cartesian_product:
1028      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
1029 apply (cases "finite A")
1030  apply (cases "finite B")
1031   apply (simp add: setprod_Sigma)
1032  apply (cases "A={}", simp)
1033  apply (simp add: setprod_1)
1034 apply (auto simp add: setprod_def
1035             dest: finite_cartesian_productD1 finite_cartesian_productD2)
1036 done
1038 lemma setprod_timesf:
1039      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
1040 by(simp add:setprod_def fold_image_distrib)
1043 subsubsection {* Properties in more restricted classes of structures *}
1045 lemma setprod_eq_1_iff [simp]:
1046   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
1047 by (induct set: finite) auto
1049 lemma setprod_zero:
1050      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
1051 apply (induct set: finite, force, clarsimp)
1052 apply (erule disjE, auto)
1053 done
1055 lemma setprod_nonneg [rule_format]:
1056    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
1057 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
1059 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
1060   --> 0 < setprod f A"
1061 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
1063 lemma setprod_zero_iff[simp]: "finite A ==>
1064   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
1065   (EX x: A. f x = 0)"
1066 by (erule finite_induct, auto simp:no_zero_divisors)
1068 lemma setprod_pos_nat:
1069   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
1070 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1072 lemma setprod_pos_nat_iff[simp]:
1073   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
1074 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1076 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1077   (setprod f (A Un B) :: 'a ::{field})
1078    = setprod f A * setprod f B / setprod f (A Int B)"
1079 by (subst setprod_Un_Int [symmetric], auto)
1081 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1082   (setprod f (A - {a}) :: 'a :: {field}) =
1083   (if a:A then setprod f A / f a else setprod f A)"
1084   by (erule finite_induct) (auto simp add: insert_Diff_if)
1086 lemma setprod_inversef:
1087   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
1088   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
1089 by (erule finite_induct) auto
1091 lemma setprod_dividef:
1092   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
1093   shows "finite A
1094     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1095 apply (subgoal_tac
1096          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1097 apply (erule ssubst)
1098 apply (subst divide_inverse)
1099 apply (subst setprod_timesf)
1100 apply (subst setprod_inversef, assumption+, rule refl)
1101 apply (rule setprod_cong, rule refl)
1102 apply (subst divide_inverse, auto)
1103 done
1105 lemma setprod_dvd_setprod [rule_format]:
1106     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
1107   apply (cases "finite A")
1108   apply (induct set: finite)
1109   apply (auto simp add: dvd_def)
1110   apply (rule_tac x = "k * ka" in exI)
1111   apply (simp add: algebra_simps)
1112 done
1114 lemma setprod_dvd_setprod_subset:
1115   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
1116   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
1117   apply (unfold dvd_def, blast)
1118   apply (subst setprod_Un_disjoint [symmetric])
1119   apply (auto elim: finite_subset intro: setprod_cong)
1120 done
1122 lemma setprod_dvd_setprod_subset2:
1123   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
1124       setprod f A dvd setprod g B"
1125   apply (rule dvd_trans)
1126   apply (rule setprod_dvd_setprod, erule (1) bspec)
1127   apply (erule (1) setprod_dvd_setprod_subset)
1128 done
1130 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
1131     (f i ::'a::comm_semiring_1) dvd setprod f A"
1132 by (induct set: finite) (auto intro: dvd_mult)
1134 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
1135     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
1136   apply (cases "finite A")
1137   apply (induct set: finite)
1138   apply auto
1139 done
1141 lemma setprod_mono:
1142   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
1143   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
1144   shows "setprod f A \<le> setprod g A"
1145 proof (cases "finite A")
1146   case True
1147   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
1148   proof (induct A rule: finite_subset_induct)
1149     case (insert a F)
1150     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
1151       unfolding setprod_insert[OF insert(1,3)]
1152       using assms[rule_format,OF insert(2)] insert
1153       by (auto intro: mult_mono mult_nonneg_nonneg)
1154   qed auto
1155   thus ?thesis by simp
1156 qed auto
1158 lemma abs_setprod:
1159   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
1160   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
1161 proof (cases "finite A")
1162   case True thus ?thesis
1163     by induct (auto simp add: field_simps abs_mult)
1164 qed auto
1166 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
1167 apply (erule finite_induct)
1168 apply auto
1169 done
1171 lemma setprod_gen_delta:
1172   assumes fS: "finite S"
1173   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
1174 proof-
1175   let ?f = "(\<lambda>k. if k=a then b k else c)"
1176   {assume a: "a \<notin> S"
1177     hence "\<forall> k\<in> S. ?f k = c" by simp
1178     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
1179   moreover
1180   {assume a: "a \<in> S"
1181     let ?A = "S - {a}"
1182     let ?B = "{a}"
1183     have eq: "S = ?A \<union> ?B" using a by blast
1184     have dj: "?A \<inter> ?B = {}" by simp
1185     from fS have fAB: "finite ?A" "finite ?B" by auto
1186     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
1187       apply (rule setprod_cong) by auto
1188     have cA: "card ?A = card S - 1" using fS a by auto
1189     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
1190     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1191       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1192       by simp
1193     then have ?thesis using a cA
1194       by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
1195   ultimately show ?thesis by blast
1196 qed
1199 subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
1201 no_notation times (infixl "*" 70)
1202 no_notation Groups.one ("1")
1204 locale semilattice_big = semilattice +
1205   fixes F :: "'a set \<Rightarrow> 'a"
1206   assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
1208 sublocale semilattice_big < folding_one_idem proof
1209 qed (simp_all add: F_eq)
1211 notation times (infixl "*" 70)
1212 notation Groups.one ("1")
1214 context lattice
1215 begin
1217 definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_"  900) where
1218   "Inf_fin = fold1 inf"
1220 definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_"  900) where
1221   "Sup_fin = fold1 sup"
1223 end
1225 sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
1226 qed (simp add: Inf_fin_def)
1228 sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
1229 qed (simp add: Sup_fin_def)
1231 context semilattice_inf
1232 begin
1234 lemma ab_semigroup_idem_mult_inf:
1235   "class.ab_semigroup_idem_mult inf"
1236 proof qed (rule inf_assoc inf_commute inf_idem)+
1238 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold inf b (insert a A) = inf a (Finite_Set.fold inf b A)"
1239 by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
1241 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> Finite_Set.fold inf c A"
1242 by (induct pred: finite) (auto intro: le_infI1)
1244 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> Finite_Set.fold inf b A \<le> inf a b"
1245 proof(induct arbitrary: a pred:finite)
1246   case empty thus ?case by simp
1247 next
1248   case (insert x A)
1249   show ?case
1250   proof cases
1251     assume "A = {}" thus ?thesis using insert by simp
1252   next
1253     assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
1254   qed
1255 qed
1257 lemma below_fold1_iff:
1258   assumes "finite A" "A \<noteq> {}"
1259   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1260 proof -
1261   interpret ab_semigroup_idem_mult inf
1262     by (rule ab_semigroup_idem_mult_inf)
1263   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
1264 qed
1266 lemma fold1_belowI:
1267   assumes "finite A"
1268     and "a \<in> A"
1269   shows "fold1 inf A \<le> a"
1270 proof -
1271   from assms have "A \<noteq> {}" by auto
1272   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
1273   proof (induct rule: finite_ne_induct)
1274     case singleton thus ?case by simp
1275   next
1276     interpret ab_semigroup_idem_mult inf
1277       by (rule ab_semigroup_idem_mult_inf)
1278     case (insert x F)
1279     from insert(5) have "a = x \<or> a \<in> F" by simp
1280     thus ?case
1281     proof
1282       assume "a = x" thus ?thesis using insert
1283         by (simp add: mult_ac)
1284     next
1285       assume "a \<in> F"
1286       hence bel: "fold1 inf F \<le> a" by (rule insert)
1287       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
1288         using insert by (simp add: mult_ac)
1289       also have "inf (fold1 inf F) a = fold1 inf F"
1290         using bel by (auto intro: antisym)
1291       also have "inf x \<dots> = fold1 inf (insert x F)"
1292         using insert by (simp add: mult_ac)
1293       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
1294       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
1295       ultimately show ?thesis by simp
1296     qed
1297   qed
1298 qed
1300 end
1302 context semilattice_sup
1303 begin
1305 lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
1306 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
1308 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold sup b (insert a A) = sup a (Finite_Set.fold sup b A)"
1309 by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
1311 lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> Finite_Set.fold sup c A \<le> sup b c"
1312 by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
1314 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> Finite_Set.fold sup b A"
1315 by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
1317 end
1319 context lattice
1320 begin
1322 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
1323 apply(unfold Sup_fin_def Inf_fin_def)
1324 apply(subgoal_tac "EX a. a:A")
1325 prefer 2 apply blast
1326 apply(erule exE)
1327 apply(rule order_trans)
1328 apply(erule (1) fold1_belowI)
1329 apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
1330 done
1332 lemma sup_Inf_absorb [simp]:
1333   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
1334 apply(subst sup_commute)
1335 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
1336 done
1338 lemma inf_Sup_absorb [simp]:
1339   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
1340 by (simp add: Sup_fin_def inf_absorb1
1341   semilattice_inf.fold1_belowI [OF dual_semilattice])
1343 end
1345 context distrib_lattice
1346 begin
1348 lemma sup_Inf1_distrib:
1349   assumes "finite A"
1350     and "A \<noteq> {}"
1351   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
1352 proof -
1353   interpret ab_semigroup_idem_mult inf
1354     by (rule ab_semigroup_idem_mult_inf)
1355   from assms show ?thesis
1356     by (simp add: Inf_fin_def image_def
1357       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
1358         (rule arg_cong [where f="fold1 inf"], blast)
1359 qed
1361 lemma sup_Inf2_distrib:
1362   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1363   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}"
1364 using A proof (induct rule: finite_ne_induct)
1365   case singleton thus ?case
1366     by (simp add: sup_Inf1_distrib [OF B])
1367 next
1368   interpret ab_semigroup_idem_mult inf
1369     by (rule ab_semigroup_idem_mult_inf)
1370   case (insert x A)
1371   have finB: "finite {sup x b |b. b \<in> B}"
1372     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
1373   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
1374   proof -
1375     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
1376       by blast
1377     thus ?thesis by(simp add: insert(1) B(1))
1378   qed
1379   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1380   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)"
1381     using insert by simp
1382   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)
1383   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})"
1384     using insert by(simp add:sup_Inf1_distrib[OF B])
1385   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})"
1386     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
1387     using B insert
1388     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
1389   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
1390     by blast
1391   finally show ?case .
1392 qed
1394 lemma inf_Sup1_distrib:
1395   assumes "finite A" and "A \<noteq> {}"
1396   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
1397 proof -
1398   interpret ab_semigroup_idem_mult sup
1399     by (rule ab_semigroup_idem_mult_sup)
1400   from assms show ?thesis
1401     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
1402       (rule arg_cong [where f="fold1 sup"], blast)
1403 qed
1405 lemma inf_Sup2_distrib:
1406   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1407   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}"
1408 using A proof (induct rule: finite_ne_induct)
1409   case singleton thus ?case
1410     by(simp add: inf_Sup1_distrib [OF B])
1411 next
1412   case (insert x A)
1413   have finB: "finite {inf x b |b. b \<in> B}"
1414     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
1415   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
1416   proof -
1417     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
1418       by blast
1419     thus ?thesis by(simp add: insert(1) B(1))
1420   qed
1421   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1422   interpret ab_semigroup_idem_mult sup
1423     by (rule ab_semigroup_idem_mult_sup)
1424   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)"
1425     using insert by simp
1426   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)
1427   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})"
1428     using insert by(simp add:inf_Sup1_distrib[OF B])
1429   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})"
1430     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
1431     using B insert
1432     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
1433   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
1434     by blast
1435   finally show ?case .
1436 qed
1438 end
1440 context complete_lattice
1441 begin
1443 lemma Inf_fin_Inf:
1444   assumes "finite A" and "A \<noteq> {}"
1445   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
1446 proof -
1447   interpret ab_semigroup_idem_mult inf
1448     by (rule ab_semigroup_idem_mult_inf)
1449   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
1450   moreover with `finite A` have "finite B" by simp
1451   ultimately show ?thesis
1452     by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
1453 qed
1455 lemma Sup_fin_Sup:
1456   assumes "finite A" and "A \<noteq> {}"
1457   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
1458 proof -
1459   interpret ab_semigroup_idem_mult sup
1460     by (rule ab_semigroup_idem_mult_sup)
1461   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
1462   moreover with `finite A` have "finite B" by simp
1463   ultimately show ?thesis
1464   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
1465 qed
1467 end
1470 subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
1472 definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
1473   "Min = fold1 min"
1475 definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
1476   "Max = fold1 max"
1478 sublocale linorder < Min!: semilattice_big min Min proof
1479 qed (simp add: Min_def)
1481 sublocale linorder < Max!: semilattice_big max Max proof
1482 qed (simp add: Max_def)
1484 context linorder
1485 begin
1487 lemmas Min_singleton = Min.singleton
1488 lemmas Max_singleton = Max.singleton
1490 lemma Min_insert:
1491   assumes "finite A" and "A \<noteq> {}"
1492   shows "Min (insert x A) = min x (Min A)"
1493   using assms by simp
1495 lemma Max_insert:
1496   assumes "finite A" and "A \<noteq> {}"
1497   shows "Max (insert x A) = max x (Max A)"
1498   using assms by simp
1500 lemma Min_Un:
1501   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1502   shows "Min (A \<union> B) = min (Min A) (Min B)"
1503   using assms by (rule Min.union_idem)
1505 lemma Max_Un:
1506   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1507   shows "Max (A \<union> B) = max (Max A) (Max B)"
1508   using assms by (rule Max.union_idem)
1510 lemma hom_Min_commute:
1511   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
1512     and "finite N" and "N \<noteq> {}"
1513   shows "h (Min N) = Min (h ` N)"
1514   using assms by (rule Min.hom_commute)
1516 lemma hom_Max_commute:
1517   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
1518     and "finite N" and "N \<noteq> {}"
1519   shows "h (Max N) = Max (h ` N)"
1520   using assms by (rule Max.hom_commute)
1522 lemma ab_semigroup_idem_mult_min:
1523   "class.ab_semigroup_idem_mult min"
1524   proof qed (auto simp add: min_def)
1526 lemma ab_semigroup_idem_mult_max:
1527   "class.ab_semigroup_idem_mult max"
1528   proof qed (auto simp add: max_def)
1530 lemma max_lattice:
1531   "class.semilattice_inf max (op \<ge>) (op >)"
1532   by (fact min_max.dual_semilattice)
1534 lemma dual_max:
1535   "ord.max (op \<ge>) = min"
1536   by (auto simp add: ord.max_def min_def fun_eq_iff)
1538 lemma dual_min:
1539   "ord.min (op \<ge>) = max"
1540   by (auto simp add: ord.min_def max_def fun_eq_iff)
1542 lemma strict_below_fold1_iff:
1543   assumes "finite A" and "A \<noteq> {}"
1544   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1545 proof -
1546   interpret ab_semigroup_idem_mult min
1547     by (rule ab_semigroup_idem_mult_min)
1548   from assms show ?thesis
1549   by (induct rule: finite_ne_induct)
1550     (simp_all add: fold1_insert)
1551 qed
1553 lemma fold1_below_iff:
1554   assumes "finite A" and "A \<noteq> {}"
1555   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1556 proof -
1557   interpret ab_semigroup_idem_mult min
1558     by (rule ab_semigroup_idem_mult_min)
1559   from assms show ?thesis
1560   by (induct rule: finite_ne_induct)
1561     (simp_all add: fold1_insert min_le_iff_disj)
1562 qed
1564 lemma fold1_strict_below_iff:
1565   assumes "finite A" and "A \<noteq> {}"
1566   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1567 proof -
1568   interpret ab_semigroup_idem_mult min
1569     by (rule ab_semigroup_idem_mult_min)
1570   from assms show ?thesis
1571   by (induct rule: finite_ne_induct)
1572     (simp_all add: fold1_insert min_less_iff_disj)
1573 qed
1575 lemma fold1_antimono:
1576   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
1577   shows "fold1 min B \<le> fold1 min A"
1578 proof cases
1579   assume "A = B" thus ?thesis by simp
1580 next
1581   interpret ab_semigroup_idem_mult min
1582     by (rule ab_semigroup_idem_mult_min)
1583   assume neq: "A \<noteq> B"
1584   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
1585   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
1586   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
1587   proof -
1588     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
1589     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
1590     moreover have "(B-A) \<noteq> {}" using assms neq by blast
1591     moreover have "A Int (B-A) = {}" using assms by blast
1592     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
1593   qed
1594   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
1595   finally show ?thesis .
1596 qed
1598 lemma Min_in [simp]:
1599   assumes "finite A" and "A \<noteq> {}"
1600   shows "Min A \<in> A"
1601 proof -
1602   interpret ab_semigroup_idem_mult min
1603     by (rule ab_semigroup_idem_mult_min)
1604   from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
1605 qed
1607 lemma Max_in [simp]:
1608   assumes "finite A" and "A \<noteq> {}"
1609   shows "Max A \<in> A"
1610 proof -
1611   interpret ab_semigroup_idem_mult max
1612     by (rule ab_semigroup_idem_mult_max)
1613   from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
1614 qed
1616 lemma Min_le [simp]:
1617   assumes "finite A" and "x \<in> A"
1618   shows "Min A \<le> x"
1619   using assms by (simp add: Min_def min_max.fold1_belowI)
1621 lemma Max_ge [simp]:
1622   assumes "finite A" and "x \<in> A"
1623   shows "x \<le> Max A"
1624   by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
1626 lemma Min_ge_iff [simp, no_atp]:
1627   assumes "finite A" and "A \<noteq> {}"
1628   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1629   using assms by (simp add: Min_def min_max.below_fold1_iff)
1631 lemma Max_le_iff [simp, no_atp]:
1632   assumes "finite A" and "A \<noteq> {}"
1633   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
1634   by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
1636 lemma Min_gr_iff [simp, no_atp]:
1637   assumes "finite A" and "A \<noteq> {}"
1638   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1639   using assms by (simp add: Min_def strict_below_fold1_iff)
1641 lemma Max_less_iff [simp, no_atp]:
1642   assumes "finite A" and "A \<noteq> {}"
1643   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
1644   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
1645     linorder.strict_below_fold1_iff [OF dual_linorder] assms)
1647 lemma Min_le_iff [no_atp]:
1648   assumes "finite A" and "A \<noteq> {}"
1649   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1650   using assms by (simp add: Min_def fold1_below_iff)
1652 lemma Max_ge_iff [no_atp]:
1653   assumes "finite A" and "A \<noteq> {}"
1654   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
1655   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
1656     linorder.fold1_below_iff [OF dual_linorder] assms)
1658 lemma Min_less_iff [no_atp]:
1659   assumes "finite A" and "A \<noteq> {}"
1660   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1661   using assms by (simp add: Min_def fold1_strict_below_iff)
1663 lemma Max_gr_iff [no_atp]:
1664   assumes "finite A" and "A \<noteq> {}"
1665   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
1666   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
1667     linorder.fold1_strict_below_iff [OF dual_linorder] assms)
1669 lemma Min_eqI:
1670   assumes "finite A"
1671   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
1672     and "x \<in> A"
1673   shows "Min A = x"
1674 proof (rule antisym)
1675   from `x \<in> A` have "A \<noteq> {}" by auto
1676   with assms show "Min A \<ge> x" by simp
1677 next
1678   from assms show "x \<ge> Min A" by simp
1679 qed
1681 lemma Max_eqI:
1682   assumes "finite A"
1683   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
1684     and "x \<in> A"
1685   shows "Max A = x"
1686 proof (rule antisym)
1687   from `x \<in> A` have "A \<noteq> {}" by auto
1688   with assms show "Max A \<le> x" by simp
1689 next
1690   from assms show "x \<le> Max A" by simp
1691 qed
1693 lemma Min_antimono:
1694   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
1695   shows "Min N \<le> Min M"
1696   using assms by (simp add: Min_def fold1_antimono)
1698 lemma Max_mono:
1699   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
1700   shows "Max M \<le> Max N"
1701   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
1702     linorder.fold1_antimono [OF dual_linorder] assms)
1704 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
1705  assumes fin: "finite A"
1706  and   empty: "P {}"
1707  and  insert: "(!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))"
1708  shows "P A"
1709 using fin empty insert
1710 proof (induct rule: finite_psubset_induct)
1711   case (psubset A)
1712   have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact
1713   have fin: "finite A" by fact
1714   have empty: "P {}" by fact
1715   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
1716   show "P A"
1717   proof (cases "A = {}")
1718     assume "A = {}"
1719     then show "P A" using `P {}` by simp
1720   next
1721     let ?B = "A - {Max A}"
1722     let ?A = "insert (Max A) ?B"
1723     have "finite ?B" using `finite A` by simp
1724     assume "A \<noteq> {}"
1725     with `finite A` have "Max A : A" by auto
1726     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
1727     then have "P ?B" using `P {}` step IH[of ?B] by blast
1728     moreover
1729     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
1730     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
1731   qed
1732 qed
1734 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
1735  "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
1736 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
1738 end
1741 begin
1744   fixes k
1745   assumes "finite N" and "N \<noteq> {}"
1746   shows "k + Min N = Min {k + m | m. m \<in> N}"
1747 proof -
1748   have "\<And>x y. k + min x y = min (k + x) (k + y)"
1749     by (simp add: min_def not_le)
1750       (blast intro: antisym less_imp_le add_left_mono)
1751   with assms show ?thesis
1752     using hom_Min_commute [of "plus k" N]
1753     by simp (blast intro: arg_cong [where f = Min])
1754 qed
1757   fixes k
1758   assumes "finite N" and "N \<noteq> {}"
1759   shows "k + Max N = Max {k + m | m. m \<in> N}"
1760 proof -
1761   have "\<And>x y. k + max x y = max (k + x) (k + y)"
1762     by (simp add: max_def not_le)
1763       (blast intro: antisym less_imp_le add_left_mono)
1764   with assms show ?thesis
1765     using hom_Max_commute [of "plus k" N]
1766     by simp (blast intro: arg_cong [where f = Max])
1767 qed
1769 end