author  hoelzl 
Thu, 15 Sep 2011 12:40:08 0400  
changeset 44937  22c0857b8aab 
parent 44921  58eef4843641 
child 46033  6fc579c917b8 
permissions  rwrr 
35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

1 
(* Title: HOL/Big_Operators.thy 
12396  2 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

3 
with contributions by Jeremy Avigad 
12396  4 
*) 
5 

35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

6 
header {* Big operators and finite (nonempty) sets *} 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

7 

35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

8 
theory Big_Operators 
35722
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

9 
imports Plain 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

10 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

11 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

12 
subsection {* Generic monoid operation over a set *} 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

13 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

14 
no_notation times (infixl "*" 70) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

15 
no_notation Groups.one ("1") 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

16 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

17 
locale comm_monoid_big = comm_monoid + 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

18 
fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

19 
assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

20 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

21 
sublocale comm_monoid_big < folding_image proof 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

22 
qed (simp add: F_eq) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

23 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

24 
context comm_monoid_big 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

25 
begin 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

26 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

27 
lemma infinite [simp]: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

28 
"\<not> finite A \<Longrightarrow> F g A = 1" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

29 
by (simp add: F_eq) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

30 

42986  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 

41 

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 

58 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

59 
end 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

60 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

61 
text {* for adhoc proofs for @{const fold_image} *} 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

62 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

63 
lemma (in comm_monoid_add) comm_monoid_mult: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36622
diff
changeset

64 
"class.comm_monoid_mult (op +) 0" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

65 
proof qed (auto intro: add_assoc add_commute) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

66 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

67 
notation times (infixl "*" 70) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

68 
notation Groups.one ("1") 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

69 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

70 

15402  71 
subsection {* Generalized summation over a set *} 
72 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

73 
definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

74 
"setsum f A = (if finite A then fold_image (op +) f 0 A else 0)" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

75 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

76 
sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

77 
qed (fact setsum_def) 
15402  78 

19535  79 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21249
diff
changeset

80 
Setsum ("\<Sum>_" [1000] 999) where 
19535  81 
"\<Sum>A == setsum (%x. x) A" 
82 

15402  83 
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is 
84 
written @{text"\<Sum>x\<in>A. e"}. *} 

85 

86 
syntax 

17189  87 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  88 
syntax (xsymbols) 
17189  89 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  90 
syntax (HTML output) 
17189  91 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  92 

93 
translations  {* Beware of argument permutation! *} 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

94 
"SUM i:A. b" == "CONST setsum (%i. b) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

95 
"\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A" 
15402  96 

97 
text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter 

98 
@{text"\<Sum>xP. e"}. *} 

99 

100 
syntax 

17189  101 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  102 
syntax (xsymbols) 
17189  103 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  104 
syntax (HTML output) 
17189  105 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  106 

107 
translations 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

108 
"SUM xP. t" => "CONST setsum (%x. t) {x. P}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

109 
"\<Sum>xP. t" => "CONST setsum (%x. t) {x. P}" 
15402  110 

111 
print_translation {* 

112 
let 

35115  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 

42284  117 
val x' = Syntax_Trans.mark_bound x; 
35115  118 
val t' = subst_bound (x', t); 
119 
val P' = subst_bound (x', P); 

42284  120 
in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end 
35115  121 
 setsum_tr' _ = raise Match; 
122 
in [(@{const_syntax setsum}, setsum_tr')] end 

15402  123 
*} 
124 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

125 
lemma setsum_empty: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

126 
"setsum f {} = 0" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

127 
by (fact setsum.empty) 
15402  128 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

129 
lemma setsum_insert: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

130 
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

131 
by (fact setsum.insert) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

132 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

133 
lemma setsum_infinite: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

134 
"~ finite A ==> setsum f A = 0" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

135 
by (fact setsum.infinite) 
15402  136 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

137 
lemma (in comm_monoid_add) setsum_reindex: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

138 
assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

139 
proof  
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

140 
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

141 
from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

142 
qed 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

143 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

144 
lemma (in comm_monoid_add) setsum_reindex_id: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

145 
"inj_on f B ==> setsum f B = setsum id (f ` B)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

146 
by (simp add: setsum_reindex) 
15402  147 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

148 
lemma (in comm_monoid_add) setsum_reindex_nonzero: 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

149 
assumes fS: "finite S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

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" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

151 
shows "setsum h (f ` S) = setsum (h o f) S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

152 
using nz 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

153 
proof(induct rule: finite_induct[OF fS]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

154 
case 1 thus ?case by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

155 
next 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

156 
case (2 x F) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

157 
{assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

158 
then obtain y where y: "y \<in> F" "f x = f y" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

159 
from "2.hyps" y have xy: "x \<noteq> y" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

160 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

161 
from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

162 
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

163 
also have "\<dots> = setsum (h o f) (insert x F)" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

164 
unfolding setsum.insert[OF `finite F` `x\<notin>F`] 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

165 
using h0 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

166 
apply simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

167 
apply (rule "2.hyps"(3)) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

168 
apply (rule_tac y="y" in "2.prems") 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

169 
apply simp_all 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

170 
done 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

171 
finally have ?case .} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

172 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

173 
{assume fxF: "f x \<notin> f ` F" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

174 
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

175 
using fxF "2.hyps" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

176 
also have "\<dots> = setsum (h o f) (insert x F)" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

177 
unfolding setsum.insert[OF `finite F` `x\<notin>F`] 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

178 
apply simp 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

179 
apply (rule cong [OF refl [of "op + (h (f x))"]]) 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

180 
apply (rule "2.hyps"(3)) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

181 
apply (rule_tac y="y" in "2.prems") 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

182 
apply simp_all 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

183 
done 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

184 
finally have ?case .} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

185 
ultimately show ?case by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

186 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

187 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

188 
lemma (in comm_monoid_add) setsum_cong: 
15402  189 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

190 
by (cases "finite A") (auto intro: setsum.cong) 
15402  191 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

192 
lemma (in comm_monoid_add) strong_setsum_cong [cong]: 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16632
diff
changeset

193 
"A = B ==> (!!x. x:B =simp=> f x = g x) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16632
diff
changeset

194 
==> setsum (%x. f x) A = setsum (%x. g x) B" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

195 
by (rule setsum_cong) (simp_all add: simp_implies_def) 
16632
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

196 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

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" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

198 
by (auto intro: setsum_cong) 
15554  199 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

200 
lemma (in comm_monoid_add) setsum_reindex_cong: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

201 
"[inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

202 
==> setsum h B = setsum g A" 
41550  203 
by (simp add: setsum_reindex) 
15402  204 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

205 
lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

206 
by (cases "finite A") (erule finite_induct, auto) 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

207 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

208 
lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

209 
by (simp add:setsum_cong) 
15402  210 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

211 
lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==> 
15402  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! *} 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

214 
by (fact setsum.union_inter) 
15402  215 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

216 
lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B 
15402  217 
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

218 
by (fact setsum.union_disjoint) 
15402  219 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

220 
lemma setsum_mono_zero_left: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

221 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

222 
and z: "\<forall>i \<in> T  S. f i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

223 
shows "setsum f S = setsum f T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

224 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

225 
have eq: "T = S \<union> (T  S)" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

226 
have d: "S \<inter> (T  S) = {}" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

227 
from fT ST have f: "finite S" "finite (T  S)" by (auto intro: finite_subset) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

228 
show ?thesis 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

229 
by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

230 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

231 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

232 
lemma setsum_mono_zero_right: 
30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

233 
"finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T  S. f i = 0 \<Longrightarrow> setsum f T = setsum f S" 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

234 
by(blast intro!: setsum_mono_zero_left[symmetric]) 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

235 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

236 
lemma setsum_mono_zero_cong_left: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

237 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

238 
and z: "\<forall>i \<in> T  S. g i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

239 
and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

240 
shows "setsum f S = setsum g T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

241 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

242 
have eq: "T = S \<union> (T  S)" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

243 
have d: "S \<inter> (T  S) = {}" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

244 
from fT ST have f: "finite S" "finite (T  S)" by (auto intro: finite_subset) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

245 
show ?thesis 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

246 
using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

247 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

248 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

249 
lemma setsum_mono_zero_cong_right: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

250 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

251 
and z: "\<forall>i \<in> T  S. f i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

252 
and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

253 
shows "setsum f T = setsum g S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

254 
using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

255 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

256 
lemma setsum_delta: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

257 
assumes fS: "finite S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

258 
shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

259 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

260 
let ?f = "(\<lambda>k. if k=a then b k else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

261 
{assume a: "a \<notin> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

262 
hence "\<forall> k\<in> S. ?f k = 0" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

263 
hence ?thesis using a by simp} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

264 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

265 
{assume a: "a \<in> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

266 
let ?A = "S  {a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

267 
let ?B = "{a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

268 
have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

269 
have dj: "?A \<inter> ?B = {}" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

270 
from fS have fAB: "finite ?A" "finite ?B" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

271 
have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

272 
using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

273 
by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

274 
then have ?thesis using a by simp} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

275 
ultimately show ?thesis by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

276 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

277 
lemma setsum_delta': 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

278 
assumes fS: "finite S" shows 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

279 
"setsum (\<lambda>k. if a = k then b k else 0) S = 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

280 
(if a\<in> S then b a else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

281 
using setsum_delta[OF fS, of a b, symmetric] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

282 
by (auto intro: setsum_cong) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

283 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

284 
lemma setsum_restrict_set: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

285 
assumes fA: "finite A" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

286 
shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

287 
proof 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

288 
from fA have fab: "finite (A \<inter> B)" by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

289 
have aba: "A \<inter> B \<subseteq> A" by blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

290 
let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

291 
from setsum_mono_zero_left[OF fA aba, of ?g] 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

292 
show ?thesis by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

293 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

294 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

295 
lemma setsum_cases: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

296 
assumes fA: "finite A" 
35577  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})" 

42986  299 
using setsum.If_cases[OF fA] . 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

300 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

301 
(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

302 
the lhs need not be, since UNION I A could still be finite.*) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

303 
lemma (in comm_monoid_add) setsum_UN_disjoint: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

304 
assumes "finite I" and "ALL i:I. finite (A i)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

305 
and "ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

306 
shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

307 
proof  
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

308 
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) 
41550  309 
from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

310 
qed 
15402  311 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

312 
text{*No need to assume that @{term C} is finite. If infinite, the rhs is 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

313 
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} 
15402  314 
lemma setsum_Union_disjoint: 
44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

315 
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

316 
shows "setsum f (Union C) = setsum (setsum f) C" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

317 
proof cases 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

318 
assume "finite C" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

319 
from setsum_UN_disjoint[OF this assms] 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

320 
show ?thesis 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

321 
by (simp add: SUP_def) 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

322 
qed (force dest: finite_UnionD simp add: setsum_def) 
15402  323 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

324 
(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

325 
the rhs need not be, since SIGMA A B could still be finite.*) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

326 
lemma (in comm_monoid_add) setsum_Sigma: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

327 
assumes "finite A" and "ALL x:A. finite (B x)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

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)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

329 
proof  
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

330 
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) 
41550  331 
from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

332 
qed 
15402  333 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

334 
text{*Here we can eliminate the finiteness assumptions, by cases.*} 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

335 
lemma setsum_cartesian_product: 
17189  336 
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)" 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

337 
apply (cases "finite A") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

338 
apply (cases "finite B") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

339 
apply (simp add: setsum_Sigma) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

340 
apply (cases "A={}", simp) 
15543  341 
apply (simp) 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

342 
apply (auto simp add: setsum_def 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

343 
dest: finite_cartesian_productD1 finite_cartesian_productD2) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

344 
done 
15402  345 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

346 
lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

347 
by (cases "finite A") (simp_all add: setsum.distrib) 
15402  348 

349 

350 
subsubsection {* Properties in more restricted classes of structures *} 

351 

352 
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

353 
apply (case_tac "finite A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

354 
prefer 2 apply (simp add: setsum_def) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

355 
apply (erule rev_mp) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

356 
apply (erule finite_induct, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

357 
done 
15402  358 

359 
lemma setsum_eq_0_iff [simp]: 

360 
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

361 
by (induct set: finite) auto 
15402  362 

30859  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) 

366 
apply (auto simp add:add_is_1) 

367 
done 

368 

369 
lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]] 

370 

15402  371 
lemma setsum_Un_nat: "finite A ==> finite B ==> 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

372 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 
15402  373 
 {* For the natural numbers, we have subtraction. *} 
29667  374 
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) 
15402  375 

376 
lemma setsum_Un: "finite A ==> finite B ==> 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

377 
(setsum f (A Un B) :: 'a :: ab_group_add) = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

378 
setsum f A + setsum f B  setsum f (A Int B)" 
29667  379 
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) 
15402  380 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

381 
lemma (in comm_monoid_add) setsum_eq_general_reverses: 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

382 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

383 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

384 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

385 
shows "setsum f S = setsum g T" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

386 
proof  
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

387 
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

388 
show ?thesis 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

389 
apply (simp add: setsum_def fS fT) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

390 
apply (rule fold_image_eq_general_inverses) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

391 
apply (rule fS) 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

392 
apply (erule kh) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

393 
apply (erule hk) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

394 
done 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

395 
qed 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

396 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

397 
lemma (in comm_monoid_add) setsum_Un_zero: 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

398 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

399 
and I0: "\<forall>x \<in> S\<inter>T. f x = 0" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

400 
shows "setsum f (S \<union> T) = setsum f S + setsum f T" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

401 
proof  
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

402 
interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

403 
show ?thesis 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

404 
using fS fT 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

405 
apply (simp add: setsum_def) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

406 
apply (rule fold_image_Un_one) 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

407 
using I0 by auto 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

408 
qed 
30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

409 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

410 
lemma setsum_UNION_zero: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

411 
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

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" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

413 
shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

414 
using fSS f0 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

415 
proof(induct rule: finite_induct[OF fS]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

416 
case 1 thus ?case by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

417 
next 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

418 
case (2 T F) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

419 
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
35216  420 
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto 
421 
from fTF have fUF: "finite (\<Union>F)" by auto 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

422 
from "2.prems" TF fTF 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

423 
show ?case 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

424 
by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

425 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

426 

15402  427 
lemma setsum_diff1_nat: "(setsum f (A  {a}) :: nat) = 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

428 
(if a:A then setsum f A  f a else setsum f A)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

429 
apply (case_tac "finite A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

430 
prefer 2 apply (simp add: setsum_def) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

431 
apply (erule finite_induct) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

432 
apply (auto simp add: insert_Diff_if) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

433 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

434 
done 
15402  435 

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)" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

439 
by (erule finite_induct) (auto simp add: insert_Diff_if) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

440 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

441 
lemma setsum_diff1'[rule_format]: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

442 
"finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A  {a}). f x)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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))"]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

444 
apply (auto simp add: insert_Diff_if add_ac) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

445 
done 
15552
8ab8e425410b
added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents:
15543
diff
changeset

446 

31438  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 

450 

15402  451 
(* By Jeremy Siek: *) 
452 

453 
lemma setsum_diff_nat: 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

454 
assumes "finite B" and "B \<subseteq> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

455 
shows "(setsum f (A  B) :: nat) = (setsum f A)  (setsum f B)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

456 
using assms 
19535  457 
proof induct 
15402  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 

478 

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 

21575  485 
proof induct 
19535  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) 

15402  492 
qed 
19535  493 
qed 
15402  494 

495 
lemma setsum_mono: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

496 
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))" 
15402  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 

19535  501 
proof induct 
15402  502 
case empty 
503 
thus ?case by simp 

504 
next 

505 
case insert 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44845
diff
changeset

506 
thus ?case using add_mono by fastforce 
15402  507 
qed 
508 
next 

509 
case False 

510 
thus ?thesis 

511 
by (simp add: setsum_def) 

512 
qed 

513 

15554  514 
lemma setsum_strict_mono: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

515 
fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}" 
19535  516 
assumes "finite A" "A \<noteq> {}" 
517 
and "!!x. x:A \<Longrightarrow> f x < g x" 

518 
shows "setsum f A < setsum g A" 

41550  519 
using assms 
15554  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 

525 

15535  526 
lemma setsum_negf: 
19535  527 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  528 
proof (cases "finite A") 
22262  529 
case True thus ?thesis by (induct set: finite) auto 
15535  530 
next 
531 
case False thus ?thesis by (simp add: setsum_def) 

532 
qed 

15402  533 

15535  534 
lemma setsum_subtractf: 
19535  535 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
536 
setsum f A  setsum g A" 

15535  537 
proof (cases "finite A") 
538 
case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) 

539 
next 

540 
case False thus ?thesis by (simp add: setsum_def) 

541 
qed 

15402  542 

15535  543 
lemma setsum_nonneg: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

544 
assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" 
19535  545 
shows "0 \<le> setsum f A" 
15535  546 
proof (cases "finite A") 
547 
case True thus ?thesis using nn 

21575  548 
proof induct 
19535  549 
case empty then show ?case by simp 
550 
next 

551 
case (insert x F) 

552 
then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono) 

553 
with insert show ?case by simp 

554 
qed 

15535  555 
next 
556 
case False thus ?thesis by (simp add: setsum_def) 

557 
qed 

15402  558 

15535  559 
lemma setsum_nonpos: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

560 
assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})" 
19535  561 
shows "setsum f A \<le> 0" 
15535  562 
proof (cases "finite A") 
563 
case True thus ?thesis using np 

21575  564 
proof induct 
19535  565 
case empty then show ?case by simp 
566 
next 

567 
case (insert x F) 

568 
then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono) 

569 
with insert show ?case by simp 

570 
qed 

15535  571 
next 
572 
case False thus ?thesis by (simp add: setsum_def) 

573 
qed 

15402  574 

36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

575 
lemma setsum_nonneg_leq_bound: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

576 
fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

577 
assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

578 
shows "f i \<le> B" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

579 
proof  
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

580 
have "0 \<le> (\<Sum> i \<in> s  {i}. f i)" and "0 \<le> f i" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

581 
using assms by (auto intro!: setsum_nonneg) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

582 
moreover 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

583 
have "(\<Sum> i \<in> s  {i}. f i) + f i = B" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

584 
using assms by (simp add: setsum_diff1) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

585 
ultimately show ?thesis by auto 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

586 
qed 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

587 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

588 
lemma setsum_nonneg_0: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

589 
fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

590 
assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

591 
and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

592 
shows "f i = 0" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

593 
using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36409
diff
changeset

594 

15539  595 
lemma setsum_mono2: 
36303  596 
fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add" 
15539  597 
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> BA \<Longrightarrow> 0 \<le> f b" 
598 
shows "setsum f A \<le> setsum f B" 

599 
proof  

600 
have "setsum f A \<le> setsum f A + setsum f (BA)" 

601 
by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) 

602 
also have "\<dots> = setsum f (A \<union> (BA))" using fin finite_subset[OF sub fin] 

603 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

604 
also have "A \<union> (BA) = B" using sub by blast 

605 
finally show ?thesis . 

606 
qed 

15542  607 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

608 
lemma setsum_mono3: "finite B ==> A <= B ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

609 
ALL x: B  A. 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

610 
0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==> 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

611 
setsum f A <= setsum f B" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

612 
apply (subgoal_tac "setsum f B = setsum f A + setsum f (B  A)") 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

613 
apply (erule ssubst) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

614 
apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B  A)") 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

615 
apply simp 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

616 
apply (rule add_left_mono) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

617 
apply (erule setsum_nonneg) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

618 
apply (subst setsum_Un_disjoint [THEN sym]) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

619 
apply (erule finite_subset, assumption) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

620 
apply (rule finite_subset) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

621 
prefer 2 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

622 
apply assumption 
32698
be4b248616c0
inf/sup_absorb are no default simp rules any longer
haftmann
parents:
32697
diff
changeset

623 
apply (auto simp add: sup_absorb2) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

624 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

625 

19279  626 
lemma setsum_right_distrib: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

627 
fixes f :: "'a => ('b::semiring_0)" 
15402  628 
shows "r * setsum f A = setsum (%n. r * f n) A" 
629 
proof (cases "finite A") 

630 
case True 

631 
thus ?thesis 

21575  632 
proof induct 
15402  633 
case empty thus ?case by simp 
634 
next 

635 
case (insert x A) thus ?case by (simp add: right_distrib) 

636 
qed 

637 
next 

638 
case False thus ?thesis by (simp add: setsum_def) 

639 
qed 

640 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

641 
lemma setsum_left_distrib: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

642 
"setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)" 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

643 
proof (cases "finite A") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

644 
case True 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

645 
then show ?thesis 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

646 
proof induct 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

647 
case empty thus ?case by simp 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

648 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

649 
case (insert x A) thus ?case by (simp add: left_distrib) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

650 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

651 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

652 
case False thus ?thesis by (simp add: setsum_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

653 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

654 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

655 
lemma setsum_divide_distrib: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

656 
"setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

657 
proof (cases "finite A") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

658 
case True 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

659 
then show ?thesis 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

660 
proof induct 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

661 
case empty thus ?case by simp 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

662 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

663 
case (insert x A) thus ?case by (simp add: add_divide_distrib) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

664 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

665 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

666 
case False thus ?thesis by (simp add: setsum_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

667 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

668 

15535  669 
lemma setsum_abs[iff]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

670 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15402  671 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  672 
proof (cases "finite A") 
673 
case True 

674 
thus ?thesis 

21575  675 
proof induct 
15535  676 
case empty thus ?case by simp 
677 
next 

678 
case (insert x A) 

679 
thus ?case by (auto intro: abs_triangle_ineq order_trans) 

680 
qed 

15402  681 
next 
15535  682 
case False thus ?thesis by (simp add: setsum_def) 
15402  683 
qed 
684 

15535  685 
lemma setsum_abs_ge_zero[iff]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

686 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15402  687 
shows "0 \<le> setsum (%i. abs(f i)) A" 
15535  688 
proof (cases "finite A") 
689 
case True 

690 
thus ?thesis 

21575  691 
proof induct 
15535  692 
case empty thus ?case by simp 
693 
next 

36977
71c8973a604b
declare add_nonneg_nonneg [simp]; remove nowredundant lemmas realpow_two_le_order(2)
huffman
parents:
36635
diff
changeset

694 
case (insert x A) thus ?case by auto 
15535  695 
qed 
15402  696 
next 
15535  697 
case False thus ?thesis by (simp add: setsum_def) 
15402  698 
qed 
699 

15539  700 
lemma abs_setsum_abs[simp]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

701 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15539  702 
shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" 
703 
proof (cases "finite A") 

704 
case True 

705 
thus ?thesis 

21575  706 
proof induct 
15539  707 
case empty thus ?case by simp 
708 
next 

709 
case (insert a A) 

710 
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 

711 
also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

712 
also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

713 
by (simp del: abs_of_nonneg) 
15539  714 
also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp 
715 
finally show ?case . 

716 
qed 

717 
next 

718 
case False thus ?thesis by (simp add: setsum_def) 

719 
qed 

720 

31080  721 
lemma setsum_Plus: 
722 
fixes A :: "'a set" and B :: "'b set" 

723 
assumes fin: "finite A" "finite B" 

724 
shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B" 

725 
proof  

726 
have "A <+> B = Inl ` A \<union> Inr ` B" by auto 

727 
moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)" 

40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
39302
diff
changeset

728 
by auto 
31080  729 
moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto 
730 
moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI) 

731 
ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex) 

732 
qed 

733 

734 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

735 
text {* Commuting outer and inner summation *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

736 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

737 
lemma setsum_commute: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

738 
"(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

739 
proof (simp add: setsum_cartesian_product) 
17189  740 
have "(\<Sum>(x,y) \<in> A <*> B. f x y) = 
741 
(\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)" 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

742 
(is "?s = _") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

743 
apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

744 
apply (simp add: split_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

745 
done 
17189  746 
also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)" 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

747 
(is "_ = ?t") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

748 
apply (simp add: swap_product) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

749 
done 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

750 
finally show "?s = ?t" . 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

751 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

752 

19279  753 
lemma setsum_product: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

754 
fixes f :: "'a => ('b::semiring_0)" 
19279  755 
shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" 
756 
by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute) 

757 

34223  758 
lemma setsum_mult_setsum_if_inj: 
759 
fixes f :: "'a => ('b::semiring_0)" 

760 
shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==> 

761 
setsum f A * setsum g B = setsum id {f a * g ba b. a:A & b:B}" 

762 
by(auto simp: setsum_product setsum_cartesian_product 

763 
intro!: setsum_reindex_cong[symmetric]) 

764 

35722
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

765 
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

766 
apply (cases "finite A") 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

767 
apply (erule finite_induct) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

768 
apply (auto simp add: algebra_simps) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

769 
done 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

770 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

771 
lemma setsum_bounded: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

772 
assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

773 
shows "setsum f A \<le> of_nat(card A) * K" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

774 
proof (cases "finite A") 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

775 
case True 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

776 
thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

777 
next 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

778 
case False thus ?thesis by (simp add: setsum_def) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

779 
qed 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

780 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

781 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

782 
subsubsection {* Cardinality as special case of @{const setsum} *} 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

783 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

784 
lemma card_eq_setsum: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

785 
"card A = setsum (\<lambda>x. 1) A" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

786 
by (simp only: card_def setsum_def) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

787 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

788 
lemma card_UN_disjoint: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

789 
"finite I ==> (ALL i:I. finite (A i)) ==> 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

790 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

791 
==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

792 
apply (simp add: card_eq_setsum del: setsum_constant) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

793 
apply (subgoal_tac 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

794 
"setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

795 
apply (simp add: setsum_UN_disjoint del: setsum_constant) 
41550  796 
apply simp 
35722
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

797 
done 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

798 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

799 
lemma card_Union_disjoint: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

800 
"finite C ==> (ALL A:C. finite A) ==> 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

801 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

802 
==> card (Union C) = setsum card C" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

803 
apply (frule card_UN_disjoint [of C id]) 
44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

804 
apply (simp_all add: SUP_def id_def) 
35722
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

805 
done 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

806 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

807 
text{*The image of a finite set can be expressed using @{term fold_image}.*} 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

808 
lemma image_eq_fold_image: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

809 
"finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

810 
proof (induct rule: finite_induct) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

811 
case empty then show ?case by simp 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

812 
next 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

813 
interpret ab_semigroup_mult "op Un" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

814 
proof qed auto 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

815 
case insert 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

816 
then show ?case by simp 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

817 
qed 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

818 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

819 
subsubsection {* Cardinality of products *} 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

820 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

821 
lemma card_SigmaI [simp]: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

822 
"\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk> 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

823 
\<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

824 
by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

825 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

826 
(* 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

827 
lemma SigmaI_insert: "y \<notin> A ==> 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

828 
(SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

829 
by auto 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

830 
*) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

831 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

832 
lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

833 
by (cases "finite A \<and> finite B") 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

834 
(auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

835 

69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

836 
lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)" 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

837 
by (simp add: card_cartesian_product) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

838 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

839 

15402  840 
subsection {* Generalized product over a set *} 
841 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

842 
definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

843 
"setprod f A = (if finite A then fold_image (op *) f 1 A else 1)" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

844 

35938
93faaa15c3d5
sublocale comm_monoid_add < setprod > sublocale comm_monoid_mult < setprod
huffman
parents:
35831
diff
changeset

845 
sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

846 
qed (fact setprod_def) 
15402  847 

19535  848 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21249
diff
changeset

849 
Setprod ("\<Prod>_" [1000] 999) where 
19535  850 
"\<Prod>A == setprod (%x. x) A" 
851 

15402  852 
syntax 
17189  853 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) 
15402  854 
syntax (xsymbols) 
17189  855 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
15402  856 
syntax (HTML output) 
17189  857 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
16550  858 

859 
translations  {* Beware of argument permutation! *} 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

860 
"PROD i:A. b" == "CONST setprod (%i. b) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

861 
"\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
16550  862 

863 
text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter 

864 
@{text"\<Prod>xP. e"}. *} 

865 

866 
syntax 

17189  867 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ / _./ _)" [0,0,10] 10) 
16550  868 
syntax (xsymbols) 
17189  869 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  870 
syntax (HTML output) 
17189  871 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  872 

15402  873 
translations 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

874 
"PROD xP. t" => "CONST setprod (%x. t) {x. P}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

875 
"\<Prod>xP. t" => "CONST setprod (%x. t) {x. P}" 
16550  876 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

877 
lemma setprod_empty: "setprod f {} = 1" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

878 
by (fact setprod.empty) 
15402  879 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

880 
lemma setprod_insert: "[ finite A; a \<notin> A ] ==> 
15402  881 
setprod f (insert a A) = f a * setprod f A" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

882 
by (fact setprod.insert) 
15402  883 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

884 
lemma setprod_infinite: "~ finite A ==> setprod f A = 1" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

885 
by (fact setprod.infinite) 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

886 

15402  887 
lemma setprod_reindex: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

888 
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

889 
by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD) 
15402  890 

891 
lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)" 

892 
by (auto simp add: setprod_reindex) 

893 

894 
lemma setprod_cong: 

895 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44845
diff
changeset

896 
by(fastforce simp: setprod_def intro: fold_image_cong) 
15402  897 

30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

898 
lemma strong_setprod_cong[cong]: 
16632
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

899 
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44845
diff
changeset

900 
by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong) 
16632
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

901 

15402  902 
lemma setprod_reindex_cong: "inj_on f A ==> 
903 
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

904 
by (frule setprod_reindex, simp) 
15402  905 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

906 
lemma strong_setprod_reindex_cong: assumes i: "inj_on f A" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

907 
and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

908 
shows "setprod h B = setprod g A" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

909 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

910 
have "setprod h B = setprod (h o f) A" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

911 
by (simp add: B setprod_reindex[OF i, of h]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

912 
then show ?thesis apply simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

913 
apply (rule setprod_cong) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

914 
apply simp 
30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

915 
by (simp add: eq) 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

916 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

917 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

918 
lemma setprod_Un_one: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

919 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

920 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

921 
shows "setprod f (S \<union> T) = setprod f S * setprod f T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

922 
using fS fT 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

923 
apply (simp add: setprod_def) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

924 
apply (rule fold_image_Un_one) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

925 
using I0 by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

926 

15402  927 

928 
lemma setprod_1: "setprod (%i. 1) A = 1" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

929 
apply (case_tac "finite A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

930 
apply (erule finite_induct, auto simp add: mult_ac) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

931 
done 
15402  932 

933 
lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

934 
apply (subgoal_tac "setprod f F = setprod (%x. 1) F") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

935 
apply (erule ssubst, rule setprod_1) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

936 
apply (rule setprod_cong, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

937 
done 
15402  938 

939 
lemma setprod_Un_Int: "finite A ==> finite B 

940 
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

941 
by(simp add: setprod_def fold_image_Un_Int[symmetric]) 
15402  942 

943 
lemma setprod_Un_disjoint: "finite A ==> finite B 

944 
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" 

945 
by (subst setprod_Un_Int [symmetric], auto) 

946 

30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

947 
lemma setprod_mono_one_left: 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

948 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

949 
and z: "\<forall>i \<in> T  S. f i = 1" 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

950 
shows "setprod f S = setprod f T" 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

951 
proof 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

952 
have eq: "T = S \<union> (T  S)" using ST by blast 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

953 
have d: "S \<inter> (T  S) = {}" using ST by blast 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

954 
from fT ST have f: "finite S" "finite (T  S)" by (auto intro: finite_subset) 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

955 
show ?thesis 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

956 
by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z]) 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

957 
qed 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

958 

3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

959 
lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym] 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

960 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

961 
lemma setprod_delta: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

962 
assumes fS: "finite S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

963 
shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

964 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

965 
let ?f = "(\<lambda>k. if k=a then b k else 1)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

966 
{assume a: "a \<notin> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

967 
hence "\<forall> k\<in> S. ?f k = 1" by simp 
41550  968 
hence ?thesis using a by (simp add: setprod_1) } 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

969 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

970 
{assume a: "a \<in> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

971 
let ?A = "S  {a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

972 
let ?B = "{a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

973 
have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

974 
have dj: "?A \<inter> ?B = {}" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

975 
from fS have fAB: "finite ?A" "finite ?B" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

976 
have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

977 
have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

978 
using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

979 
by simp 
41550  980 
then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)} 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

981 
ultimately show ?thesis by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

982 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

983 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

984 
lemma setprod_delta': 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

985 
assumes fS: "finite S" shows 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

986 
"setprod (\<lambda>k. if a = k then b k else 1) S = 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

987 
(if a\<in> S then b a else 1)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

988 
using setprod_delta[OF fS, of a b, symmetric] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

989 
by (auto intro: setprod_cong) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

990 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

991 

15402  992 
lemma setprod_UN_disjoint: 
993 
"finite I ==> (ALL i:I. finite (A i)) ==> 

994 
(ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {}) ==> 

995 
setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" 

41550  996 
by (simp add: setprod_def fold_image_UN_disjoint) 
15402  997 

998 
lemma setprod_Union_disjoint: 

44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

999 
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1000 
shows "setprod f (Union C) = setprod (setprod f) C" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1001 
proof cases 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1002 
assume "finite C" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1003 
from setprod_UN_disjoint[OF this assms] 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1004 
show ?thesis 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1005 
by (simp add: SUP_def) 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44921
diff
changeset

1006 
qed (force dest: finite_UnionD simp add: setprod_def) 
15402  1007 

1008 
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 

16550  1009 
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) = 
17189  1010 
(\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)" 
41550  1011 
by(simp add:setprod_def fold_image_Sigma split_def) 
15402  1012 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1013 
text{*Here we can eliminate the finiteness assumptions, by cases.*} 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1014 
lemma setprod_cartesian_product: 
17189  1015 
"(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)" 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1016 
apply (cases "finite A") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1017 
apply (cases "finite B") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1018 
apply (simp add: setprod_Sigma) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1019 
apply (cases "A={}", simp) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1020 
apply (simp add: setprod_1) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1021 
apply (auto simp add: setprod_def 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1022 
dest: finite_cartesian_productD1 finite_cartesian_productD2) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1023 
done 
15402  1024 

1025 
lemma setprod_timesf: 

15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1026 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1027 
by(simp add:setprod_def fold_image_distrib) 
15402  1028 

1029 

1030 
subsubsection {* Properties in more restricted classes of structures *} 

1031 

1032 
lemma setprod_eq_1_iff [simp]: 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1033 
"finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1034 
by (induct set: finite) auto 
15402  1035 

1036 
lemma setprod_zero: 

23277  1037 
"finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1038 
apply (induct set: finite, force, clarsimp) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1039 
apply (erule disjE, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1040 
done 
15402  1041 

1042 
lemma setprod_nonneg [rule_format]: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

1043 
"(ALL x: A. (0::'a::linordered_semidom) \<le> f x) > 0 \<le> setprod f A" 
30841
0813afc97522
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents:
30729
diff
changeset

1044 
by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg) 
0813afc97522
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents:
30729
diff
changeset

1045 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

1046 
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1047 
> 0 < setprod f A" 
30841
0813afc97522
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
huffman
parents:
30729
diff
changeset

1048 
by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) 
15402  1049 

30843  1050 
lemma setprod_zero_iff[simp]: "finite A ==> 
1051 
(setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) = 

1052 
(EX x: A. f x = 0)" 

1053 
by (erule finite_induct, auto simp:no_zero_divisors) 

1054 

1055 
lemma setprod_pos_nat: 

1056 
"finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0" 

1057 
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) 

15402  1058 

30863  1059 
lemma setprod_pos_nat_iff[simp]: 
1060 
"finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))" 

1061 
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) 

1062 

15402  1063 
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1064 
(setprod f (A Un B) :: 'a ::{field}) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1065 
= setprod f A * setprod f B / setprod f (A Int B)" 
30843  1066 
by (subst setprod_Un_Int [symmetric], auto) 
15402  1067 

1068 
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1069 
(setprod f (A  {a}) :: 'a :: {field}) = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1070 
(if a:A then setprod f A / f a else setprod f A)" 
36303  1071 
by (erule finite_induct) (auto simp add: insert_Diff_if) 
15402  1072 

31906
b41d61c768e2
Removed unnecessary conditions concerning nonzero divisors
paulson
parents:
31465
diff
changeset

1073 
lemma setprod_inversef: 
36409  1074 
fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero" 
31906
b41d61c768e2
Removed unnecessary conditions concerning nonzero divisors
paulson
parents:
31465
diff
changeset

1075 
shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1076 
by (erule finite_induct) auto 
15402  1077 

1078 
lemma setprod_dividef: 

36409  1079 
fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero" 
31916
f3227bb306a4
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
wenzelm
parents:
31907
diff
changeset

1080 
shows "finite A 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1081 
==> setprod (%x. f x / g x) A = setprod f A / setprod g A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1082 
apply (subgoal_tac 
15402  1083 
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1084 
apply (erule ssubst) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1085 
apply (subst divide_inverse) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1086 
apply (subst setprod_timesf) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1087 
apply (subst setprod_inversef, assumption+, rule refl) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1088 
apply (rule setprod_cong, rule refl) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1089 
apply (subst divide_inverse, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1090 
done 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1091 

29925  1092 
lemma setprod_dvd_setprod [rule_format]: 
1093 
"(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A" 

1094 
apply (cases "finite A") 

1095 
apply (induct set: finite) 

1096 
apply (auto simp add: dvd_def) 

1097 
apply (rule_tac x = "k * ka" in exI) 

1098 
apply (simp add: algebra_simps) 

1099 
done 

1100 

1101 
lemma setprod_dvd_setprod_subset: 

1102 
"finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B" 

1103 
apply (subgoal_tac "setprod f B = setprod f A * setprod f (B  A)") 

1104 
apply (unfold dvd_def, blast) 

1105 
apply (subst setprod_Un_disjoint [symmetric]) 

1106 
apply (auto elim: finite_subset intro: setprod_cong) 

1107 
done 

1108 

1109 
lemma setprod_dvd_setprod_subset2: 

1110 
"finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 

1111 
setprod f A dvd setprod g B" 

1112 
apply (rule dvd_trans) 

1113 
apply (rule setprod_dvd_setprod, erule (1) bspec) 

1114 
apply (erule (1) setprod_dvd_setprod_subset) 

1115 
done 

1116 

1117 
lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 

1118 
(f i ::'a::comm_semiring_1) dvd setprod f A" 

1119 
by (induct set: finite) (auto intro: dvd_mult) 

1120 

1121 
lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 

1122 
(d::'a::comm_semiring_1) dvd (SUM x : A. f x)" 

1123 
apply (cases "finite A") 

1124 
apply (induct set: finite) 

1125 
apply auto 

1126 
done 

1127 

35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1128 
lemma setprod_mono: 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1129 
fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1130 
assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1131 
shows "setprod f A \<le> setprod g A" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1132 
proof (cases "finite A") 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1133 
case True 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1134 
hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A] 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1135 
proof (induct A rule: finite_subset_induct) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1136 
case (insert a F) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1137 
thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1138 
unfolding setprod_insert[OF insert(1,3)] 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1139 
using assms[rule_format,OF insert(2)] insert 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1140 
by (auto intro: mult_mono mult_nonneg_nonneg) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1141 
qed auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1142 
thus ?thesis by simp 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1143 
qed auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1144 

28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1145 
lemma abs_setprod: 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1146 
fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1147 
shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1148 
proof (cases "finite A") 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1149 
case True thus ?thesis 
35216  1150 
by induct (auto simp add: field_simps abs_mult) 
35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1151 
qed auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1152 

31017  1153 
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1154 
apply (erule finite_induct) 
35216  1155 
apply auto 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1156 
done 
15402  1157 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1158 
lemma setprod_gen_delta: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1159 
assumes fS: "finite S" 
31017  1160 
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)" 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1161 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1162 
let ?f = "(\<lambda>k. if k=a then b k else c)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1163 
{assume a: "a \<notin> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1164 
hence "\<forall> k\<in> S. ?f k = c" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1165 
hence ?thesis using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) } 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1166 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1167 
{assume a: "a \<in> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1168 
let ?A = "S  {a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1169 
let ?B = "{a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1170 
have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1171 
have dj: "?A \<inter> ?B = {}" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1172 
from fS have fAB: "finite ?A" "finite ?B" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1173 
have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1174 
apply (rule setprod_cong) by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1175 
have cA: "card ?A = card S  1" using fS a by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1176 
have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1177 
have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1178 
using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1179 
by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1180 
then have ?thesis using a cA 
36349  1181 
by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)} 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1182 
ultimately show ?thesis by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1183 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1184 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1185 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1186 
subsection {* Versions of @{const inf} and @{const sup} on nonempty sets *} 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1187 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1188 
no_notation times (infixl "*" 70) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1189 
no_notation Groups.one ("1") 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1190 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1191 
locale semilattice_big = semilattice + 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1192 
fixes F :: "'a set \<Rightarrow> 'a" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1193 
assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1194 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1195 
sublocale semilattice_big < folding_one_idem proof 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1196 
qed (simp_all add: F_eq) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1197 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1198 
notation times (infixl "*" 70) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1199 
notation Groups.one ("1") 
22917  1200 

35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1201 
context lattice 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1202 
begin 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1203 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1204 
definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1205 
"Inf_fin = fold1 inf" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1206 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1207 
definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1208 
"Sup_fin = fold1 sup" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1209 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1210 
end 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1211 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1212 
sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1213 
qed (simp add: Inf_fin_def) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1214 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1215 
sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1216 
qed (simp add: Sup_fin_def) 
22917  1217 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34223
diff
changeset

1218 
context semilattice_inf 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1219 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1220 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36622
diff
changeset

1221 
lemma ab_semigroup_idem_mult_inf: 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36622
diff
changeset

1222 
"class.ab_semigroup_idem_mult inf" 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1223 
proof qed (rule inf_assoc inf_commute inf_idem)+ 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1224 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1225 
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)" 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42284
diff
changeset

1226 
by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]]) 
35816
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1227 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1228 
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1229 
by (induct pred: finite) (auto intro: le_infI1) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1230 

2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1231 
lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b" 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1232 
proof(induct arbitrary: a pred:finite) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1233 
case empty thus ?case by simp 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1234 
next 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1235 
case (insert x A) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1236 
show ?case 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1237 
proof cases 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1238 
assume "A = {}" thus ?thesis using insert by simp 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1239 
next 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1240 
assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1241 
qed 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1242 
qed 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

1243 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1244 
lemma below_fold1_iff: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (re 