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