author  haftmann 
Thu, 18 Mar 2010 13:56:31 +0100  
changeset 35816  2449e026483d 
parent 35722  69419a09a7ff 
child 35831  e31ec41a551b 
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: 
2449e026483d
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35722
diff
changeset

36 
"comm_monoid_mult (op +) 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

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 

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

558 
fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}" 
15539  559 
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> BA \<Longrightarrow> 0 \<le> f b" 
560 
shows "setsum f A \<le> setsum f B" 

561 
proof  

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

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

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

565 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

567 
finally show ?thesis . 

568 
qed 

15542  569 

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

570 
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

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

572 
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

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

574 
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

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

576 
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

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

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

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

580 
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

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

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

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

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

585 
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

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

587 

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

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

592 
case True 

593 
thus ?thesis 

21575  594 
proof induct 
15402  595 
case empty thus ?case by simp 
596 
next 

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

598 
qed 

599 
next 

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

601 
qed 

602 

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

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

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

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

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

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

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

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

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

611 
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

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

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

614 
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

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

616 

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

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

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

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

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

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

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

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

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

625 
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

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

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

628 
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

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

630 

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

632 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15402  633 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  634 
proof (cases "finite A") 
635 
case True 

636 
thus ?thesis 

21575  637 
proof induct 
15535  638 
case empty thus ?case by simp 
639 
next 

640 
case (insert x A) 

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

642 
qed 

15402  643 
next 
15535  644 
case False thus ?thesis by (simp add: setsum_def) 
15402  645 
qed 
646 

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

648 
fixes f :: "'a => ('b::ordered_ab_group_add_abs)" 
15402  649 
shows "0 \<le> setsum (%i. abs(f i)) A" 
15535  650 
proof (cases "finite A") 
651 
case True 

652 
thus ?thesis 

21575  653 
proof induct 
15535  654 
case empty thus ?case by simp 
655 
next 

21733  656 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  657 
qed 
15402  658 
next 
15535  659 
case False thus ?thesis by (simp add: setsum_def) 
15402  660 
qed 
661 

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

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

666 
case True 

667 
thus ?thesis 

21575  668 
proof induct 
15539  669 
case empty thus ?case by simp 
670 
next 

671 
case (insert a A) 

672 
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 

673 
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

674 
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

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

678 
qed 

679 
next 

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

681 
qed 

682 

31080  683 
lemma setsum_Plus: 
684 
fixes A :: "'a set" and B :: "'b set" 

685 
assumes fin: "finite A" "finite B" 

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

687 
proof  

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

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

690 
by(auto intro: finite_imageI) 

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

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

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

694 
qed 

695 

696 

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

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

698 

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

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

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

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

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

705 
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

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

707 
done 
17189  708 
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

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

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

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

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

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

714 

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

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

719 

34223  720 
lemma setsum_mult_setsum_if_inj: 
721 
fixes f :: "'a => ('b::semiring_0)" 

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

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

724 
by(auto simp: setsum_product setsum_cartesian_product 

725 
intro!: setsum_reindex_cong[symmetric]) 

726 

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

727 
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

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

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

730 
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

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

732 

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

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

734 
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

735 
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

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

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

738 
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

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

740 
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

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

742 

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

743 

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

744 
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

745 

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

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

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

748 
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

749 

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

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

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

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

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

754 
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

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

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

757 
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

758 
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

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

760 

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

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

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

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

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

765 
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

766 
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

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

768 

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

769 
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

770 
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

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

772 
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

773 
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

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

775 
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

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

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

778 
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

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

780 

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

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

782 

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

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

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

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

786 
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

787 

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

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

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

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

793 

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

794 
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

795 
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

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

797 

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

798 
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

799 
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

800 

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

801 

15402  802 
subsection {* Generalized product over a set *} 
803 

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

804 
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

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

806 

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

807 
sublocale comm_monoid_add < setprod!: comm_monoid_big "op *" 1 setprod 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

808 
qed (fact setprod_def) 
15402  809 

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

811 
Setprod ("\<Prod>_" [1000] 999) where 
19535  812 
"\<Prod>A == setprod (%x. x) A" 
813 

15402  814 
syntax 
17189  815 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) 
15402  816 
syntax (xsymbols) 
17189  817 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
15402  818 
syntax (HTML output) 
17189  819 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
16550  820 

821 
translations  {* Beware of argument permutation! *} 

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

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

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

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

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

827 

828 
syntax 

17189  829 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ / _./ _)" [0,0,10] 10) 
16550  830 
syntax (xsymbols) 
17189  831 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  832 
syntax (HTML output) 
17189  833 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  834 

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

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

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

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

839 
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

840 
by (fact setprod.empty) 
15402  841 

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

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

844 
by (fact setprod.insert) 
15402  845 

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

846 
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

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

848 

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

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

851 
by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD) 
15402  852 

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

854 
by (auto simp add: setprod_reindex) 

855 

856 
lemma setprod_cong: 

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

858 
by(fastsimp simp: setprod_def intro: fold_image_cong) 
15402  859 

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

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

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

862 
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

863 

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

866 
by (frule setprod_reindex, simp) 
15402  867 

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

868 
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

869 
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

870 
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

871 
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

872 
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

873 
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

874 
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

875 
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

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

877 
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

878 
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

879 

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

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

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

882 
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

883 
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

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

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

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

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

888 

15402  889 

890 
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

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

892 
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

893 
done 
15402  894 

895 
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

896 
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

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

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

899 
done 
15402  900 

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

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

903 
by(simp add: setprod_def fold_image_Un_Int[symmetric]) 
15402  904 

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

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

907 
by (subst setprod_Un_Int [symmetric], auto) 

908 

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

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

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

911 
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

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

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

914 
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

915 
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

916 
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

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

918 
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

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

920 

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

921 
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

922 

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

923 
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

924 
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

925 
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

926 
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

927 
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

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

929 
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

930 
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

931 
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

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

933 
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

934 
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

935 
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

936 
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

937 
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

938 
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

939 
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

940 
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

941 
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

942 
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

943 
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

944 
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

945 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_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 
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

947 
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

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

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

950 
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

951 
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

952 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_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 

15402  954 
lemma setprod_UN_disjoint: 
955 
"finite I ==> (ALL i:I. finite (A i)) ==> 

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

957 
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

958 
by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong) 
15402  959 

960 
lemma setprod_Union_disjoint: 

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

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

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

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

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

965 
prefer 2 apply (force dest: finite_UnionD simp add: setprod_def) 
15402  966 
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

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

968 
done 
15402  969 

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

16550  971 
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) = 
17189  972 
(\<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

973 
by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong) 
15402  974 

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

975 
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

976 
lemma setprod_cartesian_product: 
17189  977 
"(\<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

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

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

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

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

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

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

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

985 
done 
15402  986 

987 
lemma setprod_timesf: 

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

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

989 
by(simp add:setprod_def fold_image_distrib) 
15402  990 

991 

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

993 

994 
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

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

996 
by (induct set: finite) auto 
15402  997 

998 
lemma setprod_zero: 

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

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

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

1002 
done 
15402  1003 

1004 
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

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

1006 
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

1007 

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

1008 
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

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

1010 
by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) 
15402  1011 

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

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

1015 
by (erule finite_induct, auto simp:no_zero_divisors) 

1016 

1017 
lemma setprod_pos_nat: 

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

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

15402  1020 

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

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

1024 

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

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

1027 
= setprod f A * setprod f B / setprod f (A Int B)" 
30843  1028 
by (subst setprod_Un_Int [symmetric], auto) 
15402  1029 

1030 
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

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

1032 
(if a:A then setprod f A / f a else setprod f A)" 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23398
diff
changeset

1033 
by (erule finite_induct) (auto simp add: insert_Diff_if) 
15402  1034 

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

1035 
lemma setprod_inversef: 
b41d61c768e2
Removed unnecessary conditions concerning nonzero divisors
paulson
parents:
31465
diff
changeset

1036 
fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" 
b41d61c768e2
Removed unnecessary conditions concerning nonzero divisors
paulson
parents:
31465
diff
changeset

1037 
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

1038 
by (erule finite_induct) auto 
15402  1039 

1040 
lemma setprod_dividef: 

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

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

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

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

1044 
apply (subgoal_tac 
15402  1045 
"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

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

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

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

1049 
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

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

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

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

1053 

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

1056 
apply (cases "finite A") 

1057 
apply (induct set: finite) 

1058 
apply (auto simp add: dvd_def) 

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

1060 
apply (simp add: algebra_simps) 

1061 
done 

1062 

1063 
lemma setprod_dvd_setprod_subset: 

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

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

1066 
apply (unfold dvd_def, blast) 

1067 
apply (subst setprod_Un_disjoint [symmetric]) 

1068 
apply (auto elim: finite_subset intro: setprod_cong) 

1069 
done 

1070 

1071 
lemma setprod_dvd_setprod_subset2: 

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

1073 
setprod f A dvd setprod g B" 

1074 
apply (rule dvd_trans) 

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

1076 
apply (erule (1) setprod_dvd_setprod_subset) 

1077 
done 

1078 

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

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

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

1082 

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

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

1085 
apply (cases "finite A") 

1086 
apply (induct set: finite) 

1087 
apply auto 

1088 
done 

1089 

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

1090 
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

1091 
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

1092 
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

1093 
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

1094 
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

1095 
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

1096 
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

1097 
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

1098 
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

1099 
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

1100 
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

1101 
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

1102 
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

1103 
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

1104 
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

1105 
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

1106 

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

1107 
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

1108 
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

1109 
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

1110 
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

1111 
case True thus ?thesis 
35216  1112 
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

1113 
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

1114 

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

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

1118 
done 
15402  1119 

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

1120 
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

1121 
assumes fS: "finite S" 
31017  1122 
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

1123 
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

1124 
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

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

1126 
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

1127 
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

1128 
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

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

1130 
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

1131 
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

1132 
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

1133 
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

1134 
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

1135 
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

1136 
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

1137 
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

1138 
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

1139 
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

1140 
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

1141 
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

1142 
then have ?thesis using a cA 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_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 
by (simp add: fA1 ring_simps 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

1144 
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

1145 
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

1146 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_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 

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

1148 
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

1149 

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

1150 
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

1151 
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

1152 

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

1153 
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

1154 
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

1155 
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

1156 

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

1157 
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

1158 
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

1159 

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

1160 
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

1161 
notation Groups.one ("1") 
22917  1162 

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

1163 
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

1164 
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

1165 

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

1166 
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

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

1168 

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

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

1171 

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

1173 

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

1175 
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

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

1178 
qed (simp add: Sup_fin_def) 
22917  1179 

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

1180 
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

1181 
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

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 
lemma ab_semigroup_idem_mult_inf: "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

1184 
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

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

1187 
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

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

1190 
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

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

1193 
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

1194 
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

1195 
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

1196 
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

1197 
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

1198 
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

1199 
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

1200 
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

1201 
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

1202 
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

1203 
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

1204 

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

1205 
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

1206 
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

1207 
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

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

1209 
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

1210 
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

1211 
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

1212 
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

1213 

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

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

1215 
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

1216 
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

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

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

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

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

1221 
proof (induct rule: finite_ne_induct) 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1222 
case singleton thus ?case by simp 
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

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

1224 
interpret ab_semigroup_idem_mult inf 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1225 
by (rule ab_semigroup_idem_mult_inf) 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1226 
case (insert x F) 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1227 
from insert(5) have "a = x \<or> a \<in> F" by simp 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1228 
thus ?case 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

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

1230 
assume "a = x" thus ?thesis using insert 
29667  1231 
by (simp add: mult_ac) 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1232 
next 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1233 
assume "a \<in> F" 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1234 
hence bel: "fold1 inf F \<le> a" by (rule insert) 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1235 
have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)" 
29667  1236 
using insert by (simp add: mult_ac) 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1237 
also have "inf (fold1 inf F) a = fold1 inf F" 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1238 
using bel by (auto intro: antisym) 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1239 
also have "inf x \<dots> = fold1 inf (insert x F)" 
29667  1240 
using insert by (simp add: mult_ac) 
26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1241 
finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" . 
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26748
diff
changeset

1242 
moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp 
