author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 36622  e393a91f86df 
child 36977  71c8973a604b 
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 

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

31 
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

32 

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

33 
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

34 

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

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

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

37 
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

38 

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

39 
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

40 
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

41 

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

42 

15402  43 
subsection {* Generalized summation over a set *} 
44 

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

45 
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

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

47 

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

48 
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

49 
qed (fact setsum_def) 
15402  50 

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

52 
Setsum ("\<Sum>_" [1000] 999) where 
19535  53 
"\<Sum>A == setsum (%x. x) A" 
54 

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

57 

58 
syntax 

17189  59 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  60 
syntax (xsymbols) 
17189  61 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  62 
syntax (HTML output) 
17189  63 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  64 

65 
translations  {* Beware of argument permutation! *} 

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

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

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

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

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

71 

72 
syntax 

17189  73 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  74 
syntax (xsymbols) 
17189  75 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  76 
syntax (HTML output) 
17189  77 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  78 

79 
translations 

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

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

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

83 
print_translation {* 

84 
let 

35115  85 
fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = 
86 
if x <> y then raise Match 

87 
else 

88 
let 

89 
val x' = Syntax.mark_bound x; 

90 
val t' = subst_bound (x', t); 

91 
val P' = subst_bound (x', P); 

92 
in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end 

93 
 setsum_tr' _ = raise Match; 

94 
in [(@{const_syntax setsum}, setsum_tr')] end 

15402  95 
*} 
96 

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

97 
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

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

99 
by (fact setsum.empty) 
15402  100 

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

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

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

103 
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

104 

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

105 
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

106 
"~ 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

107 
by (fact setsum.infinite) 
15402  108 

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

109 
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

110 
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

111 
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

112 
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

113 
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

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

115 

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

116 
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

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

118 
by (simp add: setsum_reindex) 
15402  119 

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

120 
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

121 
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

122 
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

123 
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

124 
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

125 
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

126 
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

127 
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

128 
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

129 
{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

130 
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

131 
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

132 

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

133 
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

134 
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

135 
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

136 
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

137 
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

138 
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

139 
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

140 
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

141 
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

142 
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

143 
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

144 
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

145 
{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

146 
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

147 
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

148 
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

149 
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

150 
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

151 
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

152 
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

153 
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

154 
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

155 
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

156 
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

157 
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

158 
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

159 

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

160 
lemma (in comm_monoid_add) setsum_cong: 
15402  161 
"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

162 
by (cases "finite A") (auto intro: setsum.cong) 
15402  163 

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 
lemma (in comm_monoid_add) strong_setsum_cong [cong]: 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16632
diff
changeset

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

166 
==> 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

167 
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

168 

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

169 
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

170 
by (auto intro: setsum_cong) 
15554  171 

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

172 
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

173 
"[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

174 
==> setsum h B = setsum g 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

175 
by (simp add: setsum_reindex cong: setsum_cong) 
15402  176 

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

178 
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

179 

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

180 
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

181 
by (simp add:setsum_cong) 
15402  182 

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

183 
lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==> 
15402  184 
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" 
185 
 {* 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

186 
by (fact setsum.union_inter) 
15402  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_Un_disjoint: "finite A ==> finite B 
15402  189 
==> 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

190 
by (fact setsum.union_disjoint) 
15402  191 

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

192 
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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

201 
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

202 
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

203 

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

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

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

206 
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

207 

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

208 
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

209 
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

210 
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

211 
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

212 
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

213 
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

214 
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

215 
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

216 
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

217 
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

218 
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

219 
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

220 

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

222 
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

223 
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

224 
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

225 
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

226 
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

227 

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

229 
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

230 
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

231 
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

232 
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

233 
{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

234 
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

235 
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

236 
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

237 
{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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
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

244 
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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

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

252 
(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

253 
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

254 
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

255 

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

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

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

258 
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

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

260 
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

261 
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

262 
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

263 
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

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

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

266 

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

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

268 
assumes fA: "finite A" 
35577  269 
shows "setsum (\<lambda>x. if P x then f x else g x) A = 
270 
setsum f (A \<inter> {x. P x}) + setsum g (A \<inter>  {x. P x})" 

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

271 
proof 
35577  272 
have a: "A = A \<inter> {x. P x} \<union> A \<inter> {x. P x}" 
273 
"(A \<inter> {x. P x}) \<inter> (A \<inter> {x. P x}) = {}" 

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

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

275 
from fA 
35577  276 
have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> {x. P x})" by auto 
277 
let ?g = "\<lambda>x. if P x then f x else g x" 

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

278 
from setsum_Un_disjoint[OF f a(2), of ?g] a(1) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

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

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

281 

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

282 

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

283 
(*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

284 
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

285 
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

286 
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

287 
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

288 
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

289 
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

290 
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

291 
from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

292 
qed 
15402  293 

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

294 
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

295 
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} 
15402  296 
lemma setsum_Union_disjoint: 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

297 
"[ (ALL A:C. finite A); 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

298 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ] 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

299 
==> setsum f (Union C) = setsum (setsum f) C" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

301 
prefer 2 apply (force dest: finite_UnionD simp add: setsum_def) 
15402  302 
apply (frule setsum_UN_disjoint [of C id f]) 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

303 
apply (unfold Union_def id_def, assumption+) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

304 
done 
15402  305 

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

306 
(*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

307 
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

308 
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

309 
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

310 
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

311 
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

312 
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

313 
from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong) 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

314 
qed 
15402  315 

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

316 
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

317 
lemma setsum_cartesian_product: 
17189  318 
"(\<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

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

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

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

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

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

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

326 
done 
15402  327 

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

328 
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

329 
by (cases "finite A") (simp_all add: setsum.distrib) 
15402  330 

331 

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

333 

334 
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

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

336 
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

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

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

339 
done 
15402  340 

341 
lemma setsum_eq_0_iff [simp]: 

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

343 
by (induct set: finite) auto 
15402  344 

30859  345 
lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow> 
346 
(setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))" 

347 
apply(erule finite_induct) 

348 
apply (auto simp add:add_is_1) 

349 
done 

350 

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

352 

15402  353 
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

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

358 
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

359 
(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

360 
setsum f A + setsum f B  setsum f (A Int B)" 
29667  361 
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) 
15402  362 

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

363 
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

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

365 
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

366 
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

367 
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

368 
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

369 
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

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

371 
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

372 
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

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

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

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

376 
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

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

378 

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

379 
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

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

381 
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

382 
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

383 
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

384 
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

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

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

387 
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

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

389 
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

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

391 

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

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

393 
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

394 
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

395 
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

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

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

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

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

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

401 
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
35216  402 
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto 
403 
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

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

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

406 
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

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

408 

15402  409 
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

410 
(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

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

412 
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

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

414 
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

415 
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

416 
done 
15402  417 

418 
lemma setsum_diff1: "finite A \<Longrightarrow> 

419 
(setsum f (A  {a}) :: ('a::ab_group_add)) = 

420 
(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

421 
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

422 

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

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

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

425 
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

426 
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

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

428 

31438  429 
lemma setsum_diff1_ring: assumes "finite A" "a \<in> A" 
430 
shows "setsum f (A  {a}) = setsum f A  (f a::'a::ring)" 

431 
unfolding setsum_diff1'[OF assms] by auto 

432 

15402  433 
(* By Jeremy Siek: *) 
434 

435 
lemma setsum_diff_nat: 

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

436 
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

437 
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

438 
using assms 
19535  439 
proof induct 
15402  440 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 
441 
next 

442 
fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" 

443 
and xFinA: "insert x F \<subseteq> A" 

444 
and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A  F) = setsum f A  setsum f F" 

445 
from xnotinF xFinA have xinAF: "x \<in> (A  F)" by simp 

446 
from xinAF have A: "setsum f ((A  F)  {x}) = setsum f (A  F)  f x" 

447 
by (simp add: setsum_diff1_nat) 

448 
from xFinA have "F \<subseteq> A" by simp 

449 
with IH have "setsum f (A  F) = setsum f A  setsum f F" by simp 

450 
with A have B: "setsum f ((A  F)  {x}) = setsum f A  setsum f F  f x" 

451 
by simp 

452 
from xnotinF have "A  insert x F = (A  F)  {x}" by auto 

453 
with B have C: "setsum f (A  insert x F) = setsum f A  setsum f F  f x" 

454 
by simp 

455 
from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp 

456 
with C have "setsum f (A  insert x F) = setsum f A  setsum f (insert x F)" 

457 
by simp 

458 
thus "setsum f (A  insert x F) = setsum f A  setsum f (insert x F)" by simp 

459 
qed 

460 

461 
lemma setsum_diff: 

462 
assumes le: "finite A" "B \<subseteq> A" 

463 
shows "setsum f (A  B) = setsum f A  ((setsum f B)::('a::ab_group_add))" 

464 
proof  

465 
from le have finiteB: "finite B" using finite_subset by auto 

466 
show ?thesis using finiteB le 

21575  467 
proof induct 
19535  468 
case empty 
469 
thus ?case by auto 

470 
next 

471 
case (insert x F) 

472 
thus ?case using le finiteB 

473 
by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) 

15402  474 
qed 
19535  475 
qed 
15402  476 

477 
lemma setsum_mono: 

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

478 
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))" 
15402  479 
shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" 
480 
proof (cases "finite K") 

481 
case True 

482 
thus ?thesis using le 

19535  483 
proof induct 
15402  484 
case empty 
485 
thus ?case by simp 

486 
next 

487 
case insert 

19535  488 
thus ?case using add_mono by fastsimp 
15402  489 
qed 
490 
next 

491 
case False 

492 
thus ?thesis 

493 
by (simp add: setsum_def) 

494 
qed 

495 

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

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

500 
shows "setsum f A < setsum g A" 

501 
using prems 

15554  502 
proof (induct rule: finite_ne_induct) 
503 
case singleton thus ?case by simp 

504 
next 

505 
case insert thus ?case by (auto simp: add_strict_mono) 

506 
qed 

507 

15535  508 
lemma setsum_negf: 
19535  509 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  510 
proof (cases "finite A") 
22262  511 
case True thus ?thesis by (induct set: finite) auto 
15535  512 
next 
513 
case False thus ?thesis by (simp add: setsum_def) 

514 
qed 

15402  515 

15535  516 
lemma setsum_subtractf: 
19535  517 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
518 
setsum f A  setsum g A" 

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

521 
next 

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

523 
qed 

15402  524 

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

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

21575  530 
proof induct 
19535  531 
case empty then show ?case by simp 
532 
next 

533 
case (insert x F) 

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

535 
with insert show ?case by simp 

536 
qed 

15535  537 
next 
538 
case False thus ?thesis by (simp add: setsum_def) 

539 
qed 

15402  540 

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

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

21575  546 
proof induct 
19535  547 
case empty then show ?case by simp 
548 
next 

549 
case (insert x F) 

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

551 
with insert show ?case by simp 

552 
qed 

15535  553 
next 
554 
case False thus ?thesis by (simp add: setsum_def) 

555 
qed 

15402  556 

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

557 
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

558 
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

559 
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

560 
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

561 
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

562 
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

563 
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

564 
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

565 
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

566 
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

567 
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

568 
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

569 

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

570 
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

571 
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

572 
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

573 
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

574 
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

575 
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

576 

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

581 
proof  

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

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

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

585 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

587 
finally show ?thesis . 

588 
qed 

15542  589 

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

590 
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

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

592 
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

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

594 
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

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

596 
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

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

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

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

600 
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

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

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

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

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

605 
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

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

607 

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

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

612 
case True 

613 
thus ?thesis 

21575  614 
proof induct 
15402  615 
case empty thus ?case by simp 
616 
next 

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

618 
qed 

619 
next 

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

621 
qed 

622 

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

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

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

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

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

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

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

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

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

631 
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

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

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

634 
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

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

636 

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

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

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

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

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

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

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

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

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

645 
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

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

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

648 
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

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

650 

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

652 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15402  653 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  654 
proof (cases "finite A") 
655 
case True 

656 
thus ?thesis 

21575  657 
proof induct 
15535  658 
case empty thus ?case by simp 
659 
next 

660 
case (insert x A) 

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

662 
qed 

15402  663 
next 
15535  664 
case False thus ?thesis by (simp add: setsum_def) 
15402  665 
qed 
666 

15535  667 
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

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

672 
thus ?thesis 

21575  673 
proof induct 
15535  674 
case empty thus ?case by simp 
675 
next 

21733  676 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  677 
qed 
15402  678 
next 
15535  679 
case False thus ?thesis by (simp add: setsum_def) 
15402  680 
qed 
681 

15539  682 
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

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

686 
case True 

687 
thus ?thesis 

21575  688 
proof induct 
15539  689 
case empty thus ?case by simp 
690 
next 

691 
case (insert a A) 

692 
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 

693 
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

694 
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

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

698 
qed 

699 
next 

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

701 
qed 

702 

31080  703 
lemma setsum_Plus: 
704 
fixes A :: "'a set" and B :: "'b set" 

705 
assumes fin: "finite A" "finite B" 

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

707 
proof  

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

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

710 
by(auto intro: finite_imageI) 

711 
moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto 

712 
moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI) 

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

714 
qed 

715 

716 

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

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

718 

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

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

720 
"(\<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

721 
proof (simp add: setsum_cartesian_product) 
17189  722 
have "(\<Sum>(x,y) \<in> A <*> B. f x y) = 
723 
(\<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

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

725 
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

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

727 
done 
17189  728 
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

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

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

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

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

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

734 

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

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

739 

34223  740 
lemma setsum_mult_setsum_if_inj: 
741 
fixes f :: "'a => ('b::semiring_0)" 

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

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

744 
by(auto simp: setsum_product setsum_cartesian_product 

745 
intro!: setsum_reindex_cong[symmetric]) 

746 

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

747 
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

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

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

750 
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

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

752 

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

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

754 
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

755 
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

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

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

758 
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

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

760 
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

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

762 

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

763 

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

764 
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

765 

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

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

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

768 
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

769 

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

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

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

772 
(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

773 
==> 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

774 
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

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

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

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

778 
apply (simp cong: setsum_cong) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

779 
done 
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 
lemma card_Union_disjoint: 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

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

783 
(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

784 
==> 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

785 
apply (frule card_UN_disjoint [of C id]) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

786 
apply (unfold Union_def id_def, assumption+) 
69419a09a7ff
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
haftmann
parents:
35719
diff
changeset

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

788 

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

789 
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

790 
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

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

792 
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

793 
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

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

795 
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

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

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

798 
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

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

800 

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

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

802 

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

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

804 
"\<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

805 
\<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

806 
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

807 

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

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

809 
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

810 
(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

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

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

813 

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

814 
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

815 
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

816 
(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

817 

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

818 
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

819 
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

820 

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

821 

15402  822 
subsection {* Generalized product over a set *} 
823 

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

824 
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

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

826 

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

827 
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

828 
qed (fact setprod_def) 
15402  829 

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

831 
Setprod ("\<Prod>_" [1000] 999) where 
19535  832 
"\<Prod>A == setprod (%x. x) A" 
833 

15402  834 
syntax 
17189  835 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) 
15402  836 
syntax (xsymbols) 
17189  837 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
15402  838 
syntax (HTML output) 
17189  839 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
16550  840 

841 
translations  {* Beware of argument permutation! *} 

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

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

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

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

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

847 

848 
syntax 

17189  849 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ / _./ _)" [0,0,10] 10) 
16550  850 
syntax (xsymbols) 
17189  851 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  852 
syntax (HTML output) 
17189  853 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  854 

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

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

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

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

859 
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

860 
by (fact setprod.empty) 
15402  861 

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

862 
lemma setprod_insert: "[ finite A; a \<notin> A ] ==> 
15402  863 
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

864 
by (fact setprod.insert) 
15402  865 

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

866 
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

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

868 

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

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

871 
by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD) 
15402  872 

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

874 
by (auto simp add: setprod_reindex) 

875 

876 
lemma setprod_cong: 

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

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

878 
by(fastsimp simp: setprod_def intro: fold_image_cong) 
15402  879 

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

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

881 
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

882 
by(fastsimp 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

883 

15402  884 
lemma setprod_reindex_cong: "inj_on f A ==> 
885 
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

886 
by (frule setprod_reindex, simp) 
15402  887 

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

888 
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

889 
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

890 
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

891 
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

892 
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

893 
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

894 
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

895 
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

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

897 
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

898 
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

899 

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

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

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

902 
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

903 
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

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

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

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

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

908 

15402  909 

910 
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

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

912 
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

913 
done 
15402  914 

915 
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

916 
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

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

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

919 
done 
15402  920 

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

922 
==> 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

923 
by(simp add: setprod_def fold_image_Un_Int[symmetric]) 
15402  924 

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

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

927 
by (subst setprod_Un_Int [symmetric], auto) 

928 

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

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

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

931 
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

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

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

934 
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

935 
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

936 
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

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

938 
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

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

940 

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

941 
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

942 

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

943 
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

944 
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

945 
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

946 
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

947 
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

948 
{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

949 
hence "\<forall> k\<in> S. ?f k = 1" 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

950 
hence ?thesis using a 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

951 
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

952 
{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

953 
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

954 
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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
then have ?thesis using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_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

963 
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

964 
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

965 

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

967 
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

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

969 
(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

970 
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

971 
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

972 

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 

15402  974 
lemma setprod_UN_disjoint: 
975 
"finite I ==> (ALL i:I. finite (A i)) ==> 

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

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

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

978 
by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong) 
15402  979 

980 
lemma setprod_Union_disjoint: 

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

981 
"[ (ALL A:C. finite A); 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

982 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ] 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

983 
==> setprod f (Union C) = setprod (setprod f) C" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

985 
prefer 2 apply (force dest: finite_UnionD simp add: setprod_def) 
15402  986 
apply (frule setprod_UN_disjoint [of C id f]) 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

987 
apply (unfold Union_def id_def, assumption+) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

988 
done 
15402  989 

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

16550  991 
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) = 
17189  992 
(\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

993 
by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong) 
15402  994 

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

995 
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

996 
lemma setprod_cartesian_product: 
17189  997 
"(\<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

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

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

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

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

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

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

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

1005 
done 
15402  1006 

1007 
lemma setprod_timesf: 

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

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

1009 
by(simp add:setprod_def fold_image_distrib) 
15402  1010 

1011 

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

1013 

1014 
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

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

1016 
by (induct set: finite) auto 
15402  1017 

1018 
lemma setprod_zero: 

23277  1019 
"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

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

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

1022 
done 
15402  1023 

1024 
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

1025 
"(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

1026 
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

1027 

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

1028 
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

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

1030 
by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) 
15402  1031 

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

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

1035 
by (erule finite_induct, auto simp:no_zero_divisors) 

1036 

1037 
lemma setprod_pos_nat: 

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

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

15402  1040 

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

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

1044 

15402  1045 
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

1046 
(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

1047 
= setprod f A * setprod f B / setprod f (A Int B)" 
30843  1048 
by (subst setprod_Un_Int [symmetric], auto) 
15402  1049 

1050 
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

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

1052 
(if a:A then setprod f A / f a else setprod f A)" 
36303  1053 
by (erule finite_induct) (auto simp add: insert_Diff_if) 
15402  1054 

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

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

1057 
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

1058 
by (erule finite_induct) auto 
15402  1059 

1060 
lemma setprod_dividef: 

36409  1061 
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

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

1063 
==> 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

1064 
apply (subgoal_tac 
15402  1065 
"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

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

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

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

1069 
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

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

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

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

1073 

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

1076 
apply (cases "finite A") 

1077 
apply (induct set: finite) 

1078 
apply (auto simp add: dvd_def) 

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

1080 
apply (simp add: algebra_simps) 

1081 
done 

1082 

1083 
lemma setprod_dvd_setprod_subset: 

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

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

1086 
apply (unfold dvd_def, blast) 

1087 
apply (subst setprod_Un_disjoint [symmetric]) 

1088 
apply (auto elim: finite_subset intro: setprod_cong) 

1089 
done 

1090 

1091 
lemma setprod_dvd_setprod_subset2: 

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

1093 
setprod f A dvd setprod g B" 

1094 
apply (rule dvd_trans) 

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

1096 
apply (erule (1) setprod_dvd_setprod_subset) 

1097 
done 

1098 

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

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

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

1102 

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

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

1105 
apply (cases "finite A") 

1106 
apply (induct set: finite) 

1107 
apply auto 

1108 
done 

1109 

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

1110 
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

1111 
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

1112 
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

1113 
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

1114 
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

1115 
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

1116 
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

1117 
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

1118 
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

1119 
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

1120 
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

1121 
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

1122 
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

1123 
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

1124 
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

1125 
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

1126 

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

1127 
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

1128 
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

1129 
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

1130 
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

1131 
case True thus ?thesis 
35216  1132 
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

1133 
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

1134 

31017  1135 
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

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

1138 
done 
15402  1139 

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

1140 
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

1141 
assumes fS: "finite S" 
31017  1142 
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

1143 
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

1144 
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

1145 
{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

1146 
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

1147 
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

1148 
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

1149 
{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

1150 
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

1151 
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

1152 
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

1153 
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

1154 
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

1155 
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

1156 
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

1157 
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

1158 
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

1159 
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

1160 
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

1161 
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

1162 
then have ?thesis using a cA 
36349  1163 
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

1164 
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

1165 
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

1166 

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 

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

1168 
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

1169 

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

1170 
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

1171 
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

1172 

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

1173 
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

1174 
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

1175 
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

1176 

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

1177 
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

1178 
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

1179 

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

1180 
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

1181 
notation Groups.one ("1") 
22917  1182 

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

1183 
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

1184 
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

1185 

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

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

1188 

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

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

1191 

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

1193 

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

1195 
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

1196 

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

1198 
qed (simp add: Sup_fin_def) 
22917  1199 

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

1200 
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

1201 
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

1202 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36622
diff
changeset

1203 
lemma ab_semigroup_idem_mult_inf: 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36622
diff
changeset

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

1205 
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

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 
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b 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

1208 
by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_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

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

1211 
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

1212 

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

1214 
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

1215 
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

1216 
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

1217 
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

1218 
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

1219 
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

1220 
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

1221 
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

1222 
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

1223 
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

1224 
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

1225 

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

1226 
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 (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1227 
assumes "finite A" "A \<noteq> {}" 
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

1228 
shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" 
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

1229 
proof  
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29223
diff
changeset

1230 
interpret ab_semigroup_idem_mult 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

1231 
by (rule ab_semigroup_idem_mult_inf) 
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

1232 
show ?thesis using assms by (induct rule: finite_ne_induct) simp_all 
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

1233 
qed 
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

1234 

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

1235 
lemma fold1_belowI: 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1236 
assumes "finite A" 
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

1237 
and "a \<in> A" 
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

1238 
shows "fold1 inf A \<le> a" 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1239 
proof  
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1240 
from assms have "A \<noteq> {}" by auto 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1241 
from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1242 
proof (induct rule: finite_ne_induct) 