author  haftmann 
Tue, 24 Jul 2007 15:20:47 +0200  
changeset 23949  06a988643235 
parent 23878  bd651ecd4b8a 
child 24163  9e6a2a7da86a 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

3 
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

4 
with contributions by Jeremy Avigad 
12396  5 
*) 
6 

7 
header {* Finite sets *} 

8 

15131  9 
theory Finite_Set 
23878  10 
imports IntDef Divides 
15131  11 
begin 
12396  12 

15392  13 
subsection {* Definition and basic properties *} 
12396  14 

23736  15 
inductive finite :: "'a set => bool" 
22262  16 
where 
17 
emptyI [simp, intro!]: "finite {}" 

18 
 insertI [simp, intro!]: "finite A ==> finite (insert a A)" 

12396  19 

13737  20 
lemma ex_new_if_finite:  "does not depend on def of finite at all" 
14661  21 
assumes "\<not> finite (UNIV :: 'a set)" and "finite A" 
22 
shows "\<exists>a::'a. a \<notin> A" 

23 
proof  

24 
from prems have "A \<noteq> UNIV" by blast 

25 
thus ?thesis by blast 

26 
qed 

12396  27 

22262  28 
lemma finite_induct [case_names empty insert, induct set: finite]: 
12396  29 
"finite F ==> 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

30 
P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" 
12396  31 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 
32 
proof  

13421  33 
assume "P {}" and 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

34 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  35 
assume "finite F" 
36 
thus "P F" 

37 
proof induct 

23389  38 
show "P {}" by fact 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

39 
fix x F assume F: "finite F" and P: "P F" 
12396  40 
show "P (insert x F)" 
41 
proof cases 

42 
assume "x \<in> F" 

43 
hence "insert x F = F" by (rule insert_absorb) 

44 
with P show ?thesis by (simp only:) 

45 
next 

46 
assume "x \<notin> F" 

47 
from F this P show ?thesis by (rule insert) 

48 
qed 

49 
qed 

50 
qed 

51 

15484  52 
lemma finite_ne_induct[case_names singleton insert, consumes 2]: 
53 
assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow> 

54 
\<lbrakk> \<And>x. P{x}; 

55 
\<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk> 

56 
\<Longrightarrow> P F" 

57 
using fin 

58 
proof induct 

59 
case empty thus ?case by simp 

60 
next 

61 
case (insert x F) 

62 
show ?case 

63 
proof cases 

23389  64 
assume "F = {}" 
65 
thus ?thesis using `P {x}` by simp 

15484  66 
next 
23389  67 
assume "F \<noteq> {}" 
68 
thus ?thesis using insert by blast 

15484  69 
qed 
70 
qed 

71 

12396  72 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 
23389  73 
assumes "finite F" and "F \<subseteq> A" 
74 
and empty: "P {}" 

75 
and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 

76 
shows "P F" 

12396  77 
proof  
23389  78 
from `finite F` and `F \<subseteq> A` 
79 
show ?thesis 

12396  80 
proof induct 
23389  81 
show "P {}" by fact 
82 
next 

83 
fix x F 

84 
assume "finite F" and "x \<notin> F" and 

85 
P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 

12396  86 
show "P (insert x F)" 
87 
proof (rule insert) 

88 
from i show "x \<in> A" by blast 

89 
from i have "F \<subseteq> A" by blast 

90 
with P show "P F" . 

23389  91 
show "finite F" by fact 
92 
show "x \<notin> F" by fact 

12396  93 
qed 
94 
qed 

95 
qed 

96 

23878  97 

15392  98 
text{* Finite sets are the images of initial segments of natural numbers: *} 
99 

15510  100 
lemma finite_imp_nat_seg_image_inj_on: 
101 
assumes fin: "finite A" 

102 
shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}" 

15392  103 
using fin 
104 
proof induct 

105 
case empty 

15510  106 
show ?case 
107 
proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 

108 
qed 

15392  109 
next 
110 
case (insert a A) 

23389  111 
have notinA: "a \<notin> A" by fact 
15510  112 
from insert.hyps obtain n f 
113 
where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast 

114 
hence "insert a A = f(n:=a) ` {i. i < Suc n}" 

115 
"inj_on (f(n:=a)) {i. i < Suc n}" using notinA 

116 
by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq) 

15392  117 
thus ?case by blast 
118 
qed 

119 

120 
lemma nat_seg_image_imp_finite: 

121 
"!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A" 

122 
proof (induct n) 

123 
case 0 thus ?case by simp 

124 
next 

125 
case (Suc n) 

126 
let ?B = "f ` {i. i < n}" 

127 
have finB: "finite ?B" by(rule Suc.hyps[OF refl]) 

128 
show ?case 

129 
proof cases 

130 
assume "\<exists>k<n. f n = f k" 

131 
hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq) 

132 
thus ?thesis using finB by simp 

133 
next 

134 
assume "\<not>(\<exists> k<n. f n = f k)" 

135 
hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq) 

136 
thus ?thesis using finB by simp 

137 
qed 

138 
qed 

139 

140 
lemma finite_conv_nat_seg_image: 

141 
"finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})" 

15510  142 
by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 
15392  143 

144 
subsubsection{* Finiteness and set theoretic constructions *} 

145 

12396  146 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 
147 
 {* The union of two finite sets is finite. *} 

22262  148 
by (induct set: finite) simp_all 
12396  149 

150 
lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A" 

151 
 {* Every subset of a finite set is finite. *} 

152 
proof  

153 
assume "finite B" 

154 
thus "!!A. A \<subseteq> B ==> finite A" 

155 
proof induct 

156 
case empty 

157 
thus ?case by simp 

158 
next 

15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

159 
case (insert x F A) 
23389  160 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" by fact+ 
12396  161 
show "finite A" 
162 
proof cases 

163 
assume x: "x \<in> A" 

164 
with A have "A  {x} \<subseteq> F" by (simp add: subset_insert_iff) 

165 
with r have "finite (A  {x})" . 

166 
hence "finite (insert x (A  {x}))" .. 

23389  167 
also have "insert x (A  {x}) = A" using x by (rule insert_Diff) 
12396  168 
finally show ?thesis . 
169 
next 

23389  170 
show "A \<subseteq> F ==> ?thesis" by fact 
12396  171 
assume "x \<notin> A" 
172 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

173 
qed 

174 
qed 

175 
qed 

176 

18423  177 
lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}" 
17761  178 
using finite_subset[of "{x \<in> A. P x}" "A"] by blast 
179 

12396  180 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 
181 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

182 

183 
lemma finite_Int [simp, intro]: "finite F  finite G ==> finite (F Int G)" 

184 
 {* The converse obviously fails. *} 

185 
by (blast intro: finite_subset) 

186 

187 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 

188 
apply (subst insert_is_Un) 

14208  189 
apply (simp only: finite_Un, blast) 
12396  190 
done 
191 

15281  192 
lemma finite_Union[simp, intro]: 
193 
"\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" 

194 
by (induct rule:finite_induct) simp_all 

195 

12396  196 
lemma finite_empty_induct: 
23389  197 
assumes "finite A" 
198 
and "P A" 

199 
and "!!a A. finite A ==> a:A ==> P A ==> P (A  {a})" 

200 
shows "P {}" 

12396  201 
proof  
202 
have "P (A  A)" 

203 
proof  

23389  204 
{ 
205 
fix c b :: "'a set" 

206 
assume c: "finite c" and b: "finite b" 

207 
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y  {x})" 

208 
have "c \<subseteq> b ==> P (b  c)" 

209 
using c 

210 
proof induct 

211 
case empty 

212 
from P1 show ?case by simp 

213 
next 

214 
case (insert x F) 

215 
have "P (b  F  {x})" 

216 
proof (rule P2) 

217 
from _ b show "finite (b  F)" by (rule finite_subset) blast 

218 
from insert show "x \<in> b  F" by simp 

219 
from insert show "P (b  F)" by simp 

220 
qed 

221 
also have "b  F  {x} = b  insert x F" by (rule Diff_insert [symmetric]) 

222 
finally show ?case . 

12396  223 
qed 
23389  224 
} 
225 
then show ?thesis by this (simp_all add: assms) 

12396  226 
qed 
23389  227 
then show ?thesis by simp 
12396  228 
qed 
229 

230 
lemma finite_Diff [simp]: "finite B ==> finite (B  Ba)" 

231 
by (rule Diff_subset [THEN finite_subset]) 

232 

233 
lemma finite_Diff_insert [iff]: "finite (A  insert a B) = finite (A  B)" 

234 
apply (subst Diff_insert) 

235 
apply (case_tac "a : A  B") 

236 
apply (rule finite_insert [symmetric, THEN trans]) 

14208  237 
apply (subst insert_Diff, simp_all) 
12396  238 
done 
239 

19870  240 
lemma finite_Diff_singleton [simp]: "finite (A  {a}) = finite A" 
241 
by simp 

242 

12396  243 

15392  244 
text {* Image and Inverse Image over Finite Sets *} 
13825  245 

246 
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" 

247 
 {* The image of a finite set is finite. *} 

22262  248 
by (induct set: finite) simp_all 
13825  249 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

250 
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

251 
apply (frule finite_imageI) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

252 
apply (erule finite_subset, assumption) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

253 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

254 

13825  255 
lemma finite_range_imageI: 
256 
"finite (range g) ==> finite (range (%x. f (g x)))" 

14208  257 
apply (drule finite_imageI, simp) 
13825  258 
done 
259 

12396  260 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
261 
proof  

262 
have aux: "!!A. finite (A  {}) = finite A" by simp 

263 
fix B :: "'a set" 

264 
assume "finite B" 

265 
thus "!!A. f`A = B ==> inj_on f A ==> finite A" 

266 
apply induct 

267 
apply simp 

268 
apply (subgoal_tac "EX y:A. f y = x & F = f ` (A  {y})") 

269 
apply clarify 

270 
apply (simp (no_asm_use) add: inj_on_def) 

14208  271 
apply (blast dest!: aux [THEN iffD1], atomize) 
12396  272 
apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) 
14208  273 
apply (frule subsetD [OF equalityD2 insertI1], clarify) 
12396  274 
apply (rule_tac x = xa in bexI) 
275 
apply (simp_all add: inj_on_image_set_diff) 

276 
done 

277 
qed (rule refl) 

278 

279 

13825  280 
lemma inj_vimage_singleton: "inj f ==> f`{a} \<subseteq> {THE x. f x = a}" 
281 
 {* The inverse image of a singleton under an injective function 

282 
is included in a singleton. *} 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

283 
apply (auto simp add: inj_on_def) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

284 
apply (blast intro: the_equality [symmetric]) 
13825  285 
done 
286 

287 
lemma finite_vimageI: "[finite F; inj h] ==> finite (h ` F)" 

288 
 {* The inverse image of a finite set under an injective function 

289 
is finite. *} 

22262  290 
apply (induct set: finite) 
21575  291 
apply simp_all 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

292 
apply (subst vimage_insert) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

293 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  294 
done 
295 

296 

15392  297 
text {* The finite UNION of finite sets *} 
12396  298 

299 
lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)" 

22262  300 
by (induct set: finite) simp_all 
12396  301 

302 
text {* 

303 
Strengthen RHS to 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

304 
@{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}? 
12396  305 

306 
We'd need to prove 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

307 
@{prop "finite C ==> ALL A B. (UNION A B) <= C > finite {x. x:A & B x \<noteq> {}}"} 
12396  308 
by induction. *} 
309 

310 
lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))" 

311 
by (blast intro: finite_UN_I finite_subset) 

312 

313 

17022  314 
lemma finite_Plus: "[ finite A; finite B ] ==> finite (A <+> B)" 
315 
by (simp add: Plus_def) 

316 

15392  317 
text {* Sigma of finite sets *} 
12396  318 

319 
lemma finite_SigmaI [simp]: 

320 
"finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)" 

321 
by (unfold Sigma_def) (blast intro!: finite_UN_I) 

322 

15402  323 
lemma finite_cartesian_product: "[ finite A; finite B ] ==> 
324 
finite (A <*> B)" 

325 
by (rule finite_SigmaI) 

326 

12396  327 
lemma finite_Prod_UNIV: 
328 
"finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" 

329 
apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)") 

330 
apply (erule ssubst) 

14208  331 
apply (erule finite_SigmaI, auto) 
12396  332 
done 
333 

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

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

335 
"[ finite (A <*> B); B \<noteq> {} ] ==> finite A" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

337 
apply (drule_tac x=n in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

338 
apply (drule_tac x="fst o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

340 
prefer 2 apply (force dest!: equalityD2) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

341 
apply (drule equalityD1) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

342 
apply (rename_tac y x) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

343 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

344 
prefer 2 apply force 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

346 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

348 

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

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

350 
"[ finite (A <*> B); A \<noteq> {} ] ==> finite B" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

352 
apply (drule_tac x=n in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

353 
apply (drule_tac x="snd o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

355 
prefer 2 apply (force dest!: equalityD2) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

356 
apply (drule equalityD1) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

357 
apply (rename_tac x y) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

358 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

359 
prefer 2 apply force 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

361 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

363 

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

364 

15392  365 
text {* The powerset of a finite set *} 
12396  366 

367 
lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" 

368 
proof 

369 
assume "finite (Pow A)" 

370 
with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast 

371 
thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp 

372 
next 

373 
assume "finite A" 

374 
thus "finite (Pow A)" 

375 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

376 
qed 

377 

15392  378 

379 
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A" 

380 
by(blast intro: finite_subset[OF subset_Pow_Union]) 

381 

382 

12396  383 
lemma finite_converse [iff]: "finite (r^1) = finite r" 
384 
apply (subgoal_tac "r^1 = (%(x,y). (y,x))`r") 

385 
apply simp 

386 
apply (rule iffI) 

387 
apply (erule finite_imageD [unfolded inj_on_def]) 

388 
apply (simp split add: split_split) 

389 
apply (erule finite_imageI) 

14208  390 
apply (simp add: converse_def image_def, auto) 
12396  391 
apply (rule bexI) 
392 
prefer 2 apply assumption 

393 
apply simp 

394 
done 

395 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

396 

15392  397 
text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi 
398 
Ehmety) *} 

12396  399 

400 
lemma finite_Field: "finite r ==> finite (Field r)" 

401 
 {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} 

22262  402 
apply (induct set: finite) 
12396  403 
apply (auto simp add: Field_def Domain_insert Range_insert) 
404 
done 

405 

406 
lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" 

407 
apply clarify 

408 
apply (erule trancl_induct) 

409 
apply (auto simp add: Field_def) 

410 
done 

411 

412 
lemma finite_trancl: "finite (r^+) = finite r" 

413 
apply auto 

414 
prefer 2 

415 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

416 
apply (rule finite_SigmaI) 

417 
prefer 3 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
13595
diff
changeset

418 
apply (blast intro: r_into_trancl' finite_subset) 
12396  419 
apply (auto simp add: finite_Field) 
420 
done 

421 

422 

15392  423 
subsection {* A fold functional for finite sets *} 
424 

425 
text {* The intended behaviour is 

15480  426 
@{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"} 
15392  427 
if @{text f} is associativecommutative. For an application of @{text fold} 
428 
se the definitions of sums and products over finite sets. 

429 
*} 

430 

23736  431 
inductive 
22262  432 
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool" 
433 
for f :: "'a => 'a => 'a" 

434 
and g :: "'b => 'a" 

435 
and z :: 'a 

436 
where 

437 
emptyI [intro]: "foldSet f g z {} z" 

438 
 insertI [intro]: 

439 
"\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk> 

440 
\<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)" 

441 

23736  442 
inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x" 
15392  443 

444 
constdefs 

21733  445 
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" 
22262  446 
"fold f g z A == THE x. foldSet f g z A x" 
15392  447 

15498  448 
text{*A tempting alternative for the definiens is 
22262  449 
@{term "if finite A then THE x. foldSet f g e A x else e"}. 
15498  450 
It allows the removal of finiteness assumptions from the theorems 
451 
@{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. 

452 
The proofs become ugly, with @{text rule_format}. It is not worth the effort.*} 

453 

454 

15392  455 
lemma Diff1_foldSet: 
22262  456 
"foldSet f g z (A  {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)" 
15392  457 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
458 

22262  459 
lemma foldSet_imp_finite: "foldSet f g z A x==> finite A" 
15392  460 
by (induct set: foldSet) auto 
461 

22262  462 
lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x" 
463 
by (induct set: finite) auto 

15392  464 

465 

466 
subsubsection {* Commutative monoids *} 

15480  467 

22917  468 
(*FIXME integrate with Orderings.thy/OrderedGroup.thy*) 
15392  469 
locale ACf = 
470 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

471 
assumes commute: "x \<cdot> y = y \<cdot> x" 

472 
and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

22917  473 
begin 
474 

475 
lemma left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

15392  476 
proof  
477 
have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute) 

478 
also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 

479 
also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 

480 
finally show ?thesis . 

481 
qed 

482 

22917  483 
lemmas AC = assoc commute left_commute 
484 

485 
end 

486 

487 
locale ACe = ACf + 

488 
fixes e :: 'a 

489 
assumes ident [simp]: "x \<cdot> e = x" 

490 
begin 

491 

492 
lemma left_ident [simp]: "e \<cdot> x = x" 

15392  493 
proof  
494 
have "x \<cdot> e = x" by (rule ident) 

495 
thus ?thesis by (subst commute) 

496 
qed 

497 

22917  498 
end 
499 

500 
locale ACIf = ACf + 

501 
assumes idem: "x \<cdot> x = x" 

502 
begin 

503 

504 
lemma idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y" 

15497
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

505 
proof  
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

506 
have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc) 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

507 
also have "\<dots> = x \<cdot> y" by(simp add:idem) 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

508 
finally show ?thesis . 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

509 
qed 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

510 

22917  511 
lemmas ACI = AC idem idem2 
512 

513 
end 

514 

15402  515 

15392  516 
subsubsection{*From @{term foldSet} to @{term fold}*} 
517 

15510  518 
lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})" 
19868  519 
by (auto simp add: less_Suc_eq) 
15510  520 

521 
lemma insert_image_inj_on_eq: 

522 
"[insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 

523 
inj_on h {i. i < Suc m}] 

524 
==> A = h ` {i. i < m}" 

525 
apply (auto simp add: image_less_Suc inj_on_def) 

526 
apply (blast intro: less_trans) 

527 
done 

528 

529 
lemma insert_inj_onE: 

530 
assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 

531 
and inj_on: "inj_on h {i::nat. i<n}" 

532 
shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n" 

533 
proof (cases n) 

534 
case 0 thus ?thesis using aA by auto 

535 
next 

536 
case (Suc m) 

23389  537 
have nSuc: "n = Suc m" by fact 
15510  538 
have mlessn: "m<n" by (simp add: nSuc) 
15532  539 
from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE) 
15520  540 
let ?hm = "swap k m h" 
541 
have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 

542 
by (simp add: inj_on_swap_iff inj_on) 

15510  543 
show ?thesis 
15520  544 
proof (intro exI conjI) 
545 
show "inj_on ?hm {i. i < m}" using inj_hm 

15510  546 
by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on) 
15520  547 
show "m<n" by (rule mlessn) 
548 
show "A = ?hm ` {i. i < m}" 

549 
proof (rule insert_image_inj_on_eq) 

550 
show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp 

551 
show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 

552 
show "insert (?hm m) A = ?hm ` {i. i < Suc m}" 

553 
using aA hkeq nSuc klessn 

554 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

555 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  556 
qed 
557 
qed 

558 
qed 

559 

15392  560 
lemma (in ACf) foldSet_determ_aux: 
15510  561 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
22262  562 
foldSet f g z A x; foldSet f g z A x' \<rbrakk> 
15392  563 
\<Longrightarrow> x' = x" 
15510  564 
proof (induct n rule: less_induct) 
565 
case (less n) 

566 
have IH: "!!m h A x x'. 

567 
\<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 

23389  568 
foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact 
22262  569 
have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'" 
23389  570 
and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+ 
15510  571 
show ?case 
572 
proof (rule foldSet.cases [OF Afoldx]) 

22262  573 
assume "A = {}" and "x = z" 
15510  574 
with Afoldx' show "x' = x" by blast 
15392  575 
next 
15510  576 
fix B b u 
22262  577 
assume AbB: "A = insert b B" and x: "x = g b \<cdot> u" 
578 
and notinB: "b \<notin> B" and Bu: "foldSet f g z B u" 

15510  579 
show "x'=x" 
580 
proof (rule foldSet.cases [OF Afoldx']) 

22262  581 
assume "A = {}" and "x' = z" 
15510  582 
with AbB show "x' = x" by blast 
15392  583 
next 
15510  584 
fix C c v 
22262  585 
assume AcC: "A = insert c C" and x': "x' = g c \<cdot> v" 
586 
and notinC: "c \<notin> C" and Cv: "foldSet f g z C v" 

15510  587 
from A AbB have Beq: "insert b B = h`{i. i<n}" by simp 
588 
from insert_inj_onE [OF Beq notinB injh] 

589 
obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 

590 
and Beq: "B = hB ` {i. i < mB}" 

591 
and lessB: "mB < n" by auto 

592 
from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp 

593 
from insert_inj_onE [OF Ceq notinC injh] 

594 
obtain hC mC where inj_onC: "inj_on hC {i. i < mC}" 

595 
and Ceq: "C = hC ` {i. i < mC}" 

596 
and lessC: "mC < n" by auto 

597 
show "x'=x" 

15392  598 
proof cases 
15510  599 
assume "b=c" 
600 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

601 
ultimately show ?thesis using Bu Cv x x' IH[OF lessC Ceq inj_onC] 

602 
by auto 

15392  603 
next 
604 
assume diff: "b \<noteq> c" 

605 
let ?D = "B  {c}" 

606 
have B: "B = insert c ?D" and C: "C = insert b ?D" 

15510  607 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  608 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  609 
with AbB have "finite ?D" by simp 
22262  610 
then obtain d where Dfoldd: "foldSet f g z ?D d" 
17589  611 
using finite_imp_foldSet by iprover 
15506  612 
moreover have cinB: "c \<in> B" using B by auto 
22262  613 
ultimately have "foldSet f g z B (g c \<cdot> d)" 
15392  614 
by(rule Diff1_foldSet) 
15510  615 
hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
616 
moreover have "g b \<cdot> d = v" 

617 
proof (rule IH[OF lessC Ceq inj_onC Cv]) 

22262  618 
show "foldSet f g z C (g b \<cdot> d)" using C notinB Dfoldd 
15392  619 
by fastsimp 
620 
qed 

15510  621 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  622 
qed 
623 
qed 

624 
qed 

625 
qed 

626 

627 

628 
lemma (in ACf) foldSet_determ: 

22262  629 
"foldSet f g z A x ==> foldSet f g z A y ==> y = x" 
15510  630 
apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
631 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  632 
done 
633 

22262  634 
lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y" 
15392  635 
by (unfold fold_def) (blast intro: foldSet_determ) 
636 

637 
text{* The base case for @{text fold}: *} 

638 

15480  639 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  640 
by (unfold fold_def) blast 
641 

642 
lemma (in ACf) fold_insert_aux: "x \<notin> A ==> 

22262  643 
(foldSet f g z (insert x A) v) = 
644 
(EX y. foldSet f g z A y & v = f (g x) y)" 

15392  645 
apply auto 
646 
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) 

647 
apply (fastsimp dest: foldSet_imp_finite) 

648 
apply (blast intro: foldSet_determ) 

649 
done 

650 

651 
text{* The recursion equation for @{text fold}: *} 

652 

653 
lemma (in ACf) fold_insert[simp]: 

15480  654 
"finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)" 
15392  655 
apply (unfold fold_def) 
656 
apply (simp add: fold_insert_aux) 

657 
apply (rule the_equality) 

658 
apply (auto intro: finite_imp_foldSet 

659 
cong add: conj_cong simp add: fold_def [symmetric] fold_equality) 

660 
done 

661 

15535  662 
lemma (in ACf) fold_rec: 
663 
assumes fin: "finite A" and a: "a:A" 

664 
shows "fold f g z A = f (g a) (fold f g z (A  {a}))" 

665 
proof 

666 
have A: "A = insert a (A  {a})" using a by blast 

667 
hence "fold f g z A = fold f g z (insert a (A  {a}))" by simp 

668 
also have "\<dots> = f (g a) (fold f g z (A  {a}))" 

669 
by(rule fold_insert) (simp add:fin)+ 

670 
finally show ?thesis . 

671 
qed 

672 

15392  673 

15480  674 
text{* A simplified version for idempotent functions: *} 
675 

15509  676 
lemma (in ACIf) fold_insert_idem: 
15480  677 
assumes finA: "finite A" 
15508  678 
shows "fold f g z (insert a A) = g a \<cdot> fold f g z A" 
15480  679 
proof cases 
680 
assume "a \<in> A" 

681 
then obtain B where A: "A = insert a B" and disj: "a \<notin> B" 

682 
by(blast dest: mk_disjoint_insert) 

683 
show ?thesis 

684 
proof  

685 
from finA A have finB: "finite B" by(blast intro: finite_subset) 

686 
have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp 

687 
also have "\<dots> = (g a) \<cdot> (fold f g z B)" 

15506  688 
using finB disj by simp 
15480  689 
also have "\<dots> = g a \<cdot> fold f g z A" 
690 
using A finB disj by(simp add:idem assoc[symmetric]) 

691 
finally show ?thesis . 

692 
qed 

693 
next 

694 
assume "a \<notin> A" 

695 
with finA show ?thesis by simp 

696 
qed 

697 

15484  698 
lemma (in ACIf) foldI_conv_id: 
699 
"finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)" 

15509  700 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  701 

15392  702 
subsubsection{*Lemmas about @{text fold}*} 
703 

704 
lemma (in ACf) fold_commute: 

15487  705 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
22262  706 
apply (induct set: finite) 
21575  707 
apply simp 
15487  708 
apply (simp add: left_commute [of x]) 
15392  709 
done 
710 

711 
lemma (in ACf) fold_nest_Un_Int: 

712 
"finite A ==> finite B 

15480  713 
==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)" 
22262  714 
apply (induct set: finite) 
21575  715 
apply simp 
15392  716 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
717 
done 

718 

719 
lemma (in ACf) fold_nest_Un_disjoint: 

720 
"finite A ==> finite B ==> A Int B = {} 

15480  721 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  722 
by (simp add: fold_nest_Un_Int) 
723 

724 
lemma (in ACf) fold_reindex: 

15487  725 
assumes fin: "finite A" 
726 
shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A" 

15506  727 
using fin apply induct 
15392  728 
apply simp 
729 
apply simp 

730 
done 

731 

732 
lemma (in ACe) fold_Un_Int: 

733 
"finite A ==> finite B ==> 

734 
fold f g e A \<cdot> fold f g e B = 

735 
fold f g e (A Un B) \<cdot> fold f g e (A Int B)" 

22262  736 
apply (induct set: finite, simp) 
15392  737 
apply (simp add: AC insert_absorb Int_insert_left) 
738 
done 

739 

740 
corollary (in ACe) fold_Un_disjoint: 

741 
"finite A ==> finite B ==> A Int B = {} ==> 

742 
fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B" 

743 
by (simp add: fold_Un_Int) 

744 

745 
lemma (in ACe) fold_UN_disjoint: 

746 
"\<lbrakk> finite I; ALL i:I. finite (A i); 

747 
ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {} \<rbrakk> 

748 
\<Longrightarrow> fold f g e (UNION I A) = 

749 
fold f (%i. fold f g e (A i)) e I" 

22262  750 
apply (induct set: finite, simp, atomize) 
15392  751 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 
752 
prefer 2 apply blast 

753 
apply (subgoal_tac "A x Int UNION F A = {}") 

754 
prefer 2 apply blast 

755 
apply (simp add: fold_Un_disjoint) 

756 
done 

757 

15506  758 
text{*Fusion theorem, as described in 
759 
Graham Hutton's paper, 

760 
A Tutorial on the Universality and Expressiveness of Fold, 

761 
JFP 9:4 (355372), 1999.*} 

762 
lemma (in ACf) fold_fusion: 

763 
includes ACf g 

764 
shows 

765 
"finite A ==> 

766 
(!!x y. h (g x y) = f x (h y)) ==> 

767 
h (fold g j w A) = fold f j (h w) A" 

22262  768 
by (induct set: finite) simp_all 
15506  769 

15392  770 
lemma (in ACf) fold_cong: 
15480  771 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
772 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold f g z C = fold f h z C") 

15392  773 
apply simp 
774 
apply (erule finite_induct, simp) 

775 
apply (simp add: subset_insert_iff, clarify) 

776 
apply (subgoal_tac "finite C") 

777 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 

778 
apply (subgoal_tac "C = insert x (C  {x})") 

779 
prefer 2 apply blast 

780 
apply (erule ssubst) 

781 
apply (drule spec) 

782 
apply (erule (1) notE impE) 

783 
apply (simp add: Ball_def del: insert_Diff_single) 

784 
done 

785 

786 
lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 

787 
fold f (%x. fold f (g x) e (B x)) e A = 

788 
fold f (split g) e (SIGMA x:A. B x)" 

789 
apply (subst Sigma_def) 

15506  790 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  791 
apply blast 
792 
apply (erule fold_cong) 

15506  793 
apply (subst fold_UN_disjoint, simp, simp) 
15392  794 
apply blast 
15506  795 
apply simp 
15392  796 
done 
797 

798 
lemma (in ACe) fold_distrib: "finite A \<Longrightarrow> 

799 
fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)" 

15506  800 
apply (erule finite_induct, simp) 
15392  801 
apply (simp add:AC) 
802 
done 

803 

804 

22917  805 
text{* Interpretation of locales  see OrderedGroup.thy *} 
806 

807 
interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"] 

808 
by unfold_locales (auto intro: add_assoc add_commute) 

809 

810 
interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] 

811 
by unfold_locales (auto intro: mult_assoc mult_commute) 

812 

813 

15402  814 
subsection {* Generalized summation over a set *} 
815 

816 
constdefs 

817 
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" 

818 
"setsum f A == if finite A then fold (op +) f 0 A else 0" 

819 

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

821 
Setsum ("\<Sum>_" [1000] 999) where 
19535  822 
"\<Sum>A == setsum (%x. x) A" 
823 

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

826 

827 
syntax 

17189  828 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  829 
syntax (xsymbols) 
17189  830 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  831 
syntax (HTML output) 
17189  832 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  833 

834 
translations  {* Beware of argument permutation! *} 

835 
"SUM i:A. b" == "setsum (%i. b) A" 

836 
"\<Sum>i\<in>A. b" == "setsum (%i. b) A" 

837 

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

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

840 

841 
syntax 

17189  842 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  843 
syntax (xsymbols) 
17189  844 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  845 
syntax (HTML output) 
17189  846 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  847 

848 
translations 

849 
"SUM xP. t" => "setsum (%x. t) {x. P}" 

850 
"\<Sum>xP. t" => "setsum (%x. t) {x. P}" 

851 

852 
print_translation {* 

853 
let 

19535  854 
fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
855 
if x<>y then raise Match 

856 
else let val x' = Syntax.mark_bound x 

857 
val t' = subst_bound(x',t) 

858 
val P' = subst_bound(x',P) 

859 
in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end 

860 
in [("setsum", setsum_tr')] end 

15402  861 
*} 
862 

19535  863 

15402  864 
lemma setsum_empty [simp]: "setsum f {} = 0" 
865 
by (simp add: setsum_def) 

866 

867 
lemma setsum_insert [simp]: 

868 
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" 

15765  869 
by (simp add: setsum_def) 
15402  870 

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

871 
lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

872 
by (simp add: setsum_def) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

873 

15402  874 
lemma setsum_reindex: 
875 
"inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" 

15765  876 
by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD) 
15402  877 

878 
lemma setsum_reindex_id: 

879 
"inj_on f B ==> setsum f B = setsum id (f ` B)" 

880 
by (auto simp add: setsum_reindex) 

881 

882 
lemma setsum_cong: 

883 
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" 

15765  884 
by(fastsimp simp: setsum_def intro: AC_add.fold_cong) 
15402  885 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16632
diff
changeset

886 
lemma strong_setsum_cong[cong]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16632
diff
changeset

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

888 
==> setsum (%x. f x) A = setsum (%x. g x) B" 
16632
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

889 
by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong) 
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

890 

15554  891 
lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"; 
892 
by (rule setsum_cong[OF refl], auto); 

893 

15402  894 
lemma setsum_reindex_cong: 
15554  895 
"[inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)] 
15402  896 
==> setsum h B = setsum g A" 
897 
by (simp add: setsum_reindex cong: setsum_cong) 

898 

15542  899 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  900 
apply (clarsimp simp: setsum_def) 
15765  901 
apply (erule finite_induct, auto) 
15402  902 
done 
903 

15543  904 
lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0" 
905 
by(simp add:setsum_cong) 

15402  906 

907 
lemma setsum_Un_Int: "finite A ==> finite B ==> 

908 
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" 

909 
 {* The reversed orientation looks more natural, but LOOPS as a simprule! *} 

15765  910 
by(simp add: setsum_def AC_add.fold_Un_Int [symmetric]) 
15402  911 

912 
lemma setsum_Un_disjoint: "finite A ==> finite B 

913 
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" 

914 
by (subst setsum_Un_Int [symmetric], auto) 

915 

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

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

917 
the lhs need not be, since UNION I A could still be finite.*) 
15402  918 
lemma setsum_UN_disjoint: 
919 
"finite I ==> (ALL i:I. finite (A i)) ==> 

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

921 
setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))" 

15765  922 
by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong) 
15402  923 

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

924 
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

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

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

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

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

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

931 
prefer 2 apply (force dest: finite_UnionD simp add: setsum_def) 
15402  932 
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

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

934 
done 
15402  935 

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

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

937 
the rhs need not be, since SIGMA A B could still be finite.*) 
15402  938 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
17189  939 
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)" 
15765  940 
by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong) 
15402  941 

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

942 
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

943 
lemma setsum_cartesian_product: 
17189  944 
"(\<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

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

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

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

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

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

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

952 
done 
15402  953 

954 
lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" 

15765  955 
by(simp add:setsum_def AC_add.fold_distrib) 
15402  956 

957 

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

959 

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

961 
apply (case_tac "finite A") 

962 
prefer 2 apply (simp add: setsum_def) 

963 
apply (erule rev_mp) 

964 
apply (erule finite_induct, auto) 

965 
done 

966 

967 
lemma setsum_eq_0_iff [simp]: 

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

22262  969 
by (induct set: finite) auto 
15402  970 

971 
lemma setsum_Un_nat: "finite A ==> finite B ==> 

972 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 

973 
 {* For the natural numbers, we have subtraction. *} 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

974 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  975 

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

977 
(setsum f (A Un B) :: 'a :: ab_group_add) = 

978 
setsum f A + setsum f B  setsum f (A Int B)" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

979 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  980 

981 
lemma setsum_diff1_nat: "(setsum f (A  {a}) :: nat) = 

982 
(if a:A then setsum f A  f a else setsum f A)" 

983 
apply (case_tac "finite A") 

984 
prefer 2 apply (simp add: setsum_def) 

985 
apply (erule finite_induct) 

986 
apply (auto simp add: insert_Diff_if) 

987 
apply (drule_tac a = a in mk_disjoint_insert, auto) 

988 
done 

989 

990 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

992 
(if a:A then setsum f A  f a else setsum f A)" 

993 
by (erule finite_induct) (auto simp add: insert_Diff_if) 

994 

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

995 
lemma setsum_diff1'[rule_format]: "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A  {a}). f x)" 
8ab8e425410b
added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents:
15543
diff
changeset

996 
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))"]) 
8ab8e425410b
added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents:
15543
diff
changeset

997 
apply (auto simp add: insert_Diff_if add_ac) 
8ab8e425410b
added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents:
15543
diff
changeset

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

999 

15402  1000 
(* By Jeremy Siek: *) 
1001 

1002 
lemma setsum_diff_nat: 

19535  1003 
assumes "finite B" 
1004 
and "B \<subseteq> A" 

1005 
shows "(setsum f (A  B) :: nat) = (setsum f A)  (setsum f B)" 

1006 
using prems 

1007 
proof induct 

15402  1008 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 
1009 
next 

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

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

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

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

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

1015 
by (simp add: setsum_diff1_nat) 

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

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

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

1019 
by simp 

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

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

1022 
by simp 

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

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

1025 
by simp 

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

1027 
qed 

1028 

1029 
lemma setsum_diff: 

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

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

1032 
proof  

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

1034 
show ?thesis using finiteB le 

21575  1035 
proof induct 
19535  1036 
case empty 
1037 
thus ?case by auto 

1038 
next 

1039 
case (insert x F) 

1040 
thus ?case using le finiteB 

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

15402  1042 
qed 
19535  1043 
qed 
15402  1044 

1045 
lemma setsum_mono: 

1046 
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" 

1047 
shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" 

1048 
proof (cases "finite K") 

1049 
case True 

1050 
thus ?thesis using le 

19535  1051 
proof induct 
15402  1052 
case empty 
1053 
thus ?case by simp 

1054 
next 

1055 
case insert 

19535  1056 
thus ?case using add_mono by fastsimp 
15402  1057 
qed 
1058 
next 

1059 
case False 

1060 
thus ?thesis 

1061 
by (simp add: setsum_def) 

1062 
qed 

1063 

15554  1064 
lemma setsum_strict_mono: 
19535  1065 
fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" 
1066 
assumes "finite A" "A \<noteq> {}" 

1067 
and "!!x. x:A \<Longrightarrow> f x < g x" 

1068 
shows "setsum f A < setsum g A" 

1069 
using prems 

15554  1070 
proof (induct rule: finite_ne_induct) 
1071 
case singleton thus ?case by simp 

1072 
next 

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

1074 
qed 

1075 

15535  1076 
lemma setsum_negf: 
19535  1077 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  1078 
proof (cases "finite A") 
22262  1079 
case True thus ?thesis by (induct set: finite) auto 
15535  1080 
next 
1081 
case False thus ?thesis by (simp add: setsum_def) 

1082 
qed 

15402  1083 

15535  1084 
lemma setsum_subtractf: 
19535  1085 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
1086 
setsum f A  setsum g A" 

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

1089 
next 

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

1091 
qed 

15402  1092 

15535  1093 
lemma setsum_nonneg: 
19535  1094 
assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" 
1095 
shows "0 \<le> setsum f A" 

15535  1096 
proof (cases "finite A") 
1097 
case True thus ?thesis using nn 

21575  1098 
proof induct 
19535  1099 
case empty then show ?case by simp 
1100 
next 

1101 
case (insert x F) 

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

1103 
with insert show ?case by simp 

1104 
qed 

15535  1105 
next 
1106 
case False thus ?thesis by (simp add: setsum_def) 

1107 
qed 

15402  1108 

15535  1109 
lemma setsum_nonpos: 
19535  1110 
assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" 
1111 
shows "setsum f A \<le> 0" 

15535  1112 
proof (cases "finite A") 
1113 
case True thus ?thesis using np 

21575  1114 
proof induct 
19535  1115 
case empty then show ?case by simp 
1116 
next 

1117 
case (insert x F) 

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

1119 
with insert show ?case by simp 

1120 
qed 

15535  1121 
next 
1122 
case False thus ?thesis by (simp add: setsum_def) 

1123 
qed 

15402  1124 

15539  1125 
lemma setsum_mono2: 
1126 
fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}" 

1127 
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> BA \<Longrightarrow> 0 \<le> f b" 

1128 
shows "setsum f A \<le> setsum f B" 

1129 
proof  

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

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

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

1133 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1135 
finally show ?thesis . 

1136 
qed 

15542  1137 

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

1138 
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

1139 
ALL x: B  A. 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

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

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

1142 
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

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

1144 
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

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

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

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

1148 
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

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

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

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

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

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

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

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

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

1157 

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

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

1162 
case True 

1163 
thus ?thesis 

21575  1164 
proof induct 
15402  1165 
case empty thus ?case by simp 
1166 
next 

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

1168 
qed 

1169 
next 

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

1171 
qed 

1172 

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

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

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

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

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

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

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

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

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

1181 
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

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

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

1184 
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

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

1186 

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

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

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

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

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

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

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

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

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

1195 
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

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

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

1198 
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

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

1200 

15535  1201 
lemma setsum_abs[iff]: 
15402  1202 
fixes f :: "'a => ('b::lordered_ab_group_abs)" 
1203 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 

15535  1204 
proof (cases "finite A") 
1205 
case True 

1206 
thus ?thesis 

21575  1207 
proof induct 
15535  1208 
case empty thus ?case by simp 
1209 
next 

1210 
case (insert x A) 

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

1212 
qed 

15402  1213 
next 
15535  1214 
case False thus ?thesis by (simp add: setsum_def) 
15402  1215 
qed 
1216 

15535  1217 
lemma setsum_abs_ge_zero[iff]: 
15402  1218 
fixes f :: "'a => ('b::lordered_ab_group_abs)" 
1219 
shows "0 \<le> setsum (%i. abs(f i)) A" 

15535  1220 
proof (cases "finite A") 
1221 
case True 

1222 
thus ?thesis 

21575  1223 
proof induct 
15535  1224 
case empty thus ?case by simp 
1225 
next 

21733  1226 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  1227 
qed 
15402  1228 
next 
15535  1229 
case False thus ?thesis by (simp add: setsum_def) 
15402  1230 
qed 
1231 

15539  1232 
lemma abs_setsum_abs[simp]: 
1233 
fixes f :: "'a => ('b::lordered_ab_group_abs)" 

1234 
shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" 

1235 
proof (cases "finite A") 

1236 
case True 

1237 
thus ?thesis 

21575  1238 
proof induct 
15539  1239 
case empty thus ?case by simp 
1240 
next 

1241 
case (insert a A) 

1242 
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 

1243 
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

1244 
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

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

1248 
qed 

1249 
next 

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

1251 
qed 

1252 

15402  1253 

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

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

1255 

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

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

1257 
"inj_on (%(i, j). (j, i)) (A \<times> B)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1258 
by (unfold inj_on_def) fast 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1259 

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

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

1261 
"(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

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

1263 

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

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

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

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

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

1270 
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

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

1272 
done 
17189  1273 
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

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

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

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

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

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

1279 

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

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

1284 

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

1285 

15402  1286 
subsection {* Generalized product over a set *} 
1287 

1288 
constdefs 

1289 
setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" 

1290 
"setprod f A == if finite A then fold (op *) f 1 A else 1" 

1291 

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

1293 
Setprod ("\<Prod>_" [1000] 999) where 
19535  1294 
"\<Prod>A == setprod (%x. x) A" 
1295 

15402  1296 
syntax 
17189  1297 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) 
15402  1298 
syntax (xsymbols) 
17189  1299 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
15402  1300 
syntax (HTML output) 
17189  1301 
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 
16550  1302 

1303 
translations  {* Beware of argument permutation! *} 

1304 
"PROD i:A. b" == "setprod (%i. b) A" 

1305 
"\<Prod>i\<in>A. b" == "setprod (%i. b) A" 

1306 

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

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

1309 

1310 
syntax 

17189  1311 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ / _./ _)" [0,0,10] 10) 
16550  1312 
syntax (xsymbols) 
17189  1313 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  1314 
syntax (HTML output) 
17189  1315 
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 
16550  1316 

15402  1317 
translations 
16550  1318 
"PROD xP. t" => "setprod (%x. t) {x. P}" 
1319 
"\<Prod>xP. t" => "setprod (%x. t) {x. P}" 

1320 

15402  1321 

1322 
lemma setprod_empty [simp]: "setprod f {} = 1" 

1323 
by (auto simp add: setprod_def) 

1324 

1325 
lemma setprod_insert [simp]: "[ finite A; a \<notin> A ] ==> 

1326 
setprod f (insert a A) = f a * setprod f A" 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19870
diff
changeset

1327 
by (simp add: setprod_def) 
15402  1328 

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

1329 
lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1330 
by (simp add: setprod_def) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

1331 

15402  1332 
lemma setprod_reindex: 
1333 
"inj_on f B ==> setprod h (f ` B) = setprod (h 