author  nipkow 
Sun, 12 Dec 2004 16:25:47 +0100  
changeset 15402  97204f3b4705 
parent 15392  290bc97038c7 
child 15409  a063687d24eb 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

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

4 
Additions by Jeremy Avigad in Feb 2004 
15376  5 

15402  6 
Get rid of a couple of superfluous finiteness assumptions in lemmas 
7 
about setsum and card  see FIXME. 

8 
NB: the analogous lemmas for setprod should also be simplified! 

12396  9 
*) 
10 

11 
header {* Finite sets *} 

12 

15131  13 
theory Finite_Set 
15140  14 
imports Divides Power Inductive 
15131  15 
begin 
12396  16 

15392  17 
subsection {* Definition and basic properties *} 
12396  18 

19 
consts Finites :: "'a set set" 

13737  20 
syntax 
21 
finite :: "'a set => bool" 

22 
translations 

23 
"finite A" == "A : Finites" 

12396  24 

25 
inductive Finites 

26 
intros 

27 
emptyI [simp, intro!]: "{} : Finites" 

28 
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" 

29 

30 
axclass finite \<subseteq> type 

31 
finite: "finite UNIV" 

32 

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

36 
proof  

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

38 
thus ?thesis by blast 

39 
qed 

12396  40 

41 
lemma finite_induct [case_names empty insert, induct set: Finites]: 

42 
"finite F ==> 

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

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

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

47 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  48 
assume "finite F" 
49 
thus "P F" 

50 
proof induct 

51 
show "P {}" . 

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

52 
fix x F assume F: "finite F" and P: "P F" 
12396  53 
show "P (insert x F)" 
54 
proof cases 

55 
assume "x \<in> F" 

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

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

58 
next 

59 
assume "x \<notin> F" 

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

61 
qed 

62 
qed 

63 
qed 

64 

65 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 

66 
"finite F ==> F \<subseteq> A ==> 

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

67 
P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 
12396  68 
P F" 
69 
proof  

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

71 
"!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 
12396  72 
assume "finite F" 
73 
thus "F \<subseteq> A ==> P F" 

74 
proof induct 

75 
show "P {}" . 

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

76 
fix x F assume "finite F" and "x \<notin> F" 
12396  77 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 
78 
show "P (insert x F)" 

79 
proof (rule insert) 

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

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

82 
with P show "P F" . 

83 
qed 

84 
qed 

85 
qed 

86 

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

89 
lemma finite_imp_nat_seg_image: 

90 
assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}" 

91 
using fin 

92 
proof induct 

93 
case empty 

94 
show ?case 

95 
proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed 

96 
next 

97 
case (insert a A) 

98 
from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast 

99 
hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}" 

100 
by (auto simp add:image_def Ball_def) 

101 
thus ?case by blast 

102 
qed 

103 

104 
lemma nat_seg_image_imp_finite: 

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

106 
proof (induct n) 

107 
case 0 thus ?case by simp 

108 
next 

109 
case (Suc n) 

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

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

112 
show ?case 

113 
proof cases 

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

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

116 
thus ?thesis using finB by simp 

117 
next 

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

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

120 
thus ?thesis using finB by simp 

121 
qed 

122 
qed 

123 

124 
lemma finite_conv_nat_seg_image: 

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

126 
by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite) 

127 

128 
subsubsection{* Finiteness and set theoretic constructions *} 

129 

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

132 
by (induct set: Finites) simp_all 

133 

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

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

136 
proof  

137 
assume "finite B" 

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

139 
proof induct 

140 
case empty 

141 
thus ?case by simp 

142 
next 

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

143 
case (insert x F A) 
12396  144 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 
145 
show "finite A" 

146 
proof cases 

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

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

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

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

151 
also have "insert x (A  {x}) = A" by (rule insert_Diff) 

152 
finally show ?thesis . 

153 
next 

154 
show "A \<subseteq> F ==> ?thesis" . 

155 
assume "x \<notin> A" 

156 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

157 
qed 

158 
qed 

159 
qed 

160 

161 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 

162 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

163 

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

165 
 {* The converse obviously fails. *} 

166 
by (blast intro: finite_subset) 

167 

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

169 
apply (subst insert_is_Un) 

14208  170 
apply (simp only: finite_Un, blast) 
12396  171 
done 
172 

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

175 
by (induct rule:finite_induct) simp_all 

176 

12396  177 
lemma finite_empty_induct: 
178 
"finite A ==> 

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

180 
proof  

181 
assume "finite A" 

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

183 
have "P (A  A)" 

184 
proof  

185 
fix c b :: "'a set" 

186 
presume c: "finite c" and b: "finite b" 

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

188 
from c show "c \<subseteq> b ==> P (b  c)" 

189 
proof induct 

190 
case empty 

191 
from P1 show ?case by simp 

192 
next 

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

193 
case (insert x F) 
12396  194 
have "P (b  F  {x})" 
195 
proof (rule P2) 

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

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

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

199 
qed 

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

201 
finally show ?case . 

202 
qed 

203 
next 

204 
show "A \<subseteq> A" .. 

205 
qed 

206 
thus "P {}" by simp 

207 
qed 

208 

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

210 
by (rule Diff_subset [THEN finite_subset]) 

211 

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

213 
apply (subst Diff_insert) 

214 
apply (case_tac "a : A  B") 

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

14208  216 
apply (subst insert_Diff, simp_all) 
12396  217 
done 
218 

219 

15392  220 
text {* Image and Inverse Image over Finite Sets *} 
13825  221 

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

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

224 
by (induct set: Finites) simp_all 

225 

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

226 
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

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

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

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

230 

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

14208  233 
apply (drule finite_imageI, simp) 
13825  234 
done 
235 

12396  236 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
237 
proof  

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

239 
fix B :: "'a set" 

240 
assume "finite B" 

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

242 
apply induct 

243 
apply simp 

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

245 
apply clarify 

246 
apply (simp (no_asm_use) add: inj_on_def) 

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

252 
done 

253 
qed (rule refl) 

254 

255 

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

258 
is included in a singleton. *} 

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

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

260 
apply (blast intro: the_equality [symmetric]) 
13825  261 
done 
262 

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

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

265 
is finite. *} 

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

266 
apply (induct set: Finites, simp_all) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

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

268 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  269 
done 
270 

271 

15392  272 
text {* The finite UNION of finite sets *} 
12396  273 

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

275 
by (induct set: Finites) simp_all 

276 

277 
text {* 

278 
Strengthen RHS to 

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

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

281 
We'd need to prove 

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

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

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

286 
by (blast intro: finite_UN_I finite_subset) 

287 

288 

15392  289 
text {* Sigma of finite sets *} 
12396  290 

291 
lemma finite_SigmaI [simp]: 

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

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

294 

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

297 
by (rule finite_SigmaI) 

298 

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

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

302 
apply (erule ssubst) 

14208  303 
apply (erule finite_SigmaI, auto) 
12396  304 
done 
305 

306 
instance unit :: finite 

307 
proof 

308 
have "finite {()}" by simp 

309 
also have "{()} = UNIV" by auto 

310 
finally show "finite (UNIV :: unit set)" . 

311 
qed 

312 

313 
instance * :: (finite, finite) finite 

314 
proof 

315 
show "finite (UNIV :: ('a \<times> 'b) set)" 

316 
proof (rule finite_Prod_UNIV) 

317 
show "finite (UNIV :: 'a set)" by (rule finite) 

318 
show "finite (UNIV :: 'b set)" by (rule finite) 

319 
qed 

320 
qed 

321 

322 

15392  323 
text {* The powerset of a finite set *} 
12396  324 

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

326 
proof 

327 
assume "finite (Pow A)" 

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

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

330 
next 

331 
assume "finite A" 

332 
thus "finite (Pow A)" 

333 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

334 
qed 

335 

15392  336 

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

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

339 

340 

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

343 
apply simp 

344 
apply (rule iffI) 

345 
apply (erule finite_imageD [unfolded inj_on_def]) 

346 
apply (simp split add: split_split) 

347 
apply (erule finite_imageI) 

14208  348 
apply (simp add: converse_def image_def, auto) 
12396  349 
apply (rule bexI) 
350 
prefer 2 apply assumption 

351 
apply simp 

352 
done 

353 

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

354 

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

12396  357 

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

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

360 
apply (induct set: Finites) 

361 
apply (auto simp add: Field_def Domain_insert Range_insert) 

362 
done 

363 

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

365 
apply clarify 

366 
apply (erule trancl_induct) 

367 
apply (auto simp add: Field_def) 

368 
done 

369 

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

371 
apply auto 

372 
prefer 2 

373 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

374 
apply (rule finite_SigmaI) 

375 
prefer 3 

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

376 
apply (blast intro: r_into_trancl' finite_subset) 
12396  377 
apply (auto simp add: finite_Field) 
378 
done 

379 

380 

15392  381 
subsection {* A fold functional for finite sets *} 
382 

383 
text {* The intended behaviour is 

384 
@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"} 

385 
if @{text f} is associativecommutative. For an application of @{text fold} 

386 
se the definitions of sums and products over finite sets. 

387 
*} 

388 

389 
consts 

390 
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set" 

391 

392 
inductive "foldSet f g e" 

393 
intros 

394 
emptyI [intro]: "({}, e) : foldSet f g e" 

395 
insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk> 

396 
\<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e" 

397 

398 
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e" 

399 

400 
constdefs 

401 
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" 

402 
"fold f g e A == THE x. (A, x) : foldSet f g e" 

403 

404 
lemma Diff1_foldSet: 

405 
"(A  {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e" 

406 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 

407 

408 
lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A" 

409 
by (induct set: foldSet) auto 

410 

411 
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e" 

412 
by (induct set: Finites) auto 

413 

414 

415 
subsubsection {* Commutative monoids *} 

416 

417 
locale ACf = 

418 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

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

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

421 

422 
locale ACe = ACf + 

423 
fixes e :: 'a 

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

425 

426 
lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

427 
proof  

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

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

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

431 
finally show ?thesis . 

432 
qed 

433 

434 
lemmas (in ACf) AC = assoc commute left_commute 

435 

436 
lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 

437 
proof  

438 
have "x \<cdot> e = x" by (rule ident) 

439 
thus ?thesis by (subst commute) 

440 
qed 

441 

15402  442 
text{* Instantiation of locales: *} 
443 

444 
lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" 

445 
by(fastsimp intro: ACf.intro add_assoc add_commute) 

446 

447 
lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)" 

448 
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add) 

449 

450 

451 
lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)" 

452 
by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute) 

453 

454 
lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)" 

455 
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult) 

456 

457 

15392  458 
subsubsection{*From @{term foldSet} to @{term fold}*} 
459 

460 
lemma (in ACf) foldSet_determ_aux: 

461 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> 

462 
\<Longrightarrow> x' = x" 

463 
proof (induct n) 

464 
case 0 thus ?case by auto 

465 
next 

466 
case (Suc n) 

467 
have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> 

468 
\<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}" 

469 
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . 

470 
show ?case 

471 
proof cases 

472 
assume "EX k<n. h n = h k" 

473 
hence card': "A = h ` {i. i < n}" 

474 
using card by (auto simp:image_def less_Suc_eq) 

475 
show ?thesis by(rule IH[OF card' Afoldx Afoldy]) 

476 
next 

477 
assume new: "\<not>(EX k<n. h n = h k)" 

478 
show ?thesis 

479 
proof (rule foldSet.cases[OF Afoldx]) 

480 
assume "(A, x) = ({}, e)" 

481 
thus "x' = x" using Afoldy by (auto) 

482 
next 

483 
fix B b y 

484 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

485 
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" 

486 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 

487 
show ?thesis 

488 
proof (rule foldSet.cases[OF Afoldy]) 

489 
assume "(A,x') = ({}, e)" 

490 
thus ?thesis using A1 by auto 

491 
next 

492 
fix C c z 

493 
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" 

494 
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" 

495 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto 

496 
let ?h = "%i. if h i = b then h n else h i" 

497 
have less: "B = ?h`{i. i<n}" (is "_ = ?r") 

498 
proof 

499 
show "B \<subseteq> ?r" 

500 
proof 

501 
fix u assume "u \<in> B" 

502 
hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+ 

503 
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" 

504 
using card by(auto simp:image_def) 

505 
show "u \<in> ?r" 

506 
proof cases 

507 
assume "i\<^isub>u < n" 

508 
thus ?thesis using unotb by(fastsimp) 

509 
next 

510 
assume "\<not> i\<^isub>u < n" 

511 
with below have [simp]: "i\<^isub>u = n" by arith 

512 
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k" 

513 
using A1 card by blast 

514 
have "i\<^isub>k < n" 

515 
proof (rule ccontr) 

516 
assume "\<not> i\<^isub>k < n" 

517 
hence "i\<^isub>k = n" using i\<^isub>k by arith 

518 
thus False using unotb by simp 

519 
qed 

520 
thus ?thesis by(auto simp add:image_def) 

521 
qed 

522 
qed 

523 
next 

524 
show "?r \<subseteq> B" 

525 
proof 

526 
fix u assume "u \<in> ?r" 

527 
then obtain i\<^isub>u where below: "i\<^isub>u < n" and 

528 
or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

529 
by(auto simp:image_def) 

530 
from or show "u \<in> B" 

531 
proof 

532 
assume [simp]: "b = h i\<^isub>u \<and> u = h n" 

533 
have "u \<in> A" using card by auto 

534 
moreover have "u \<noteq> b" using new below by auto 

535 
ultimately show "u \<in> B" using A1 by blast 

536 
next 

537 
assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

538 
moreover hence "u \<in> A" using card below by auto 

539 
ultimately show "u \<in> B" using A1 by blast 

540 
qed 

541 
qed 

542 
qed 

543 
show ?thesis 

544 
proof cases 

545 
assume "b = c" 

546 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

547 
ultimately show ?thesis using IH[OF less] y z x x' by auto 

548 
next 

549 
assume diff: "b \<noteq> c" 

550 
let ?D = "B  {c}" 

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

552 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

15402  553 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
554 
with A1 have "finite ?D" by simp 

15392  555 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" 
556 
using finite_imp_foldSet by rules 

557 
moreover have cinB: "c \<in> B" using B by(auto) 

558 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" 

559 
by(rule Diff1_foldSet) 

560 
hence "g c \<cdot> d = y" by(rule IH[OF less y]) 

561 
moreover have "g b \<cdot> d = z" 

562 
proof (rule IH[OF _ z]) 

563 
let ?h = "%i. if h i = c then h n else h i" 

564 
show "C = ?h`{i. i<n}" (is "_ = ?r") 

565 
proof 

566 
show "C \<subseteq> ?r" 

567 
proof 

568 
fix u assume "u \<in> C" 

569 
hence uinA: "u \<in> A" and unotc: "u \<noteq> c" 

570 
using A2 notinC by blast+ 

571 
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" 

572 
using card by(auto simp:image_def) 

573 
show "u \<in> ?r" 

574 
proof cases 

575 
assume "i\<^isub>u < n" 

576 
thus ?thesis using unotc by(fastsimp) 

577 
next 

578 
assume "\<not> i\<^isub>u < n" 

579 
with below have [simp]: "i\<^isub>u = n" by arith 

580 
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k" 

581 
using A2 card by blast 

582 
have "i\<^isub>k < n" 

583 
proof (rule ccontr) 

584 
assume "\<not> i\<^isub>k < n" 

585 
hence "i\<^isub>k = n" using i\<^isub>k by arith 

586 
thus False using unotc by simp 

587 
qed 

588 
thus ?thesis by(auto simp add:image_def) 

589 
qed 

590 
qed 

591 
next 

592 
show "?r \<subseteq> C" 

593 
proof 

594 
fix u assume "u \<in> ?r" 

595 
then obtain i\<^isub>u where below: "i\<^isub>u < n" and 

596 
or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" 

597 
by(auto simp:image_def) 

598 
from or show "u \<in> C" 

599 
proof 

600 
assume [simp]: "c = h i\<^isub>u \<and> u = h n" 

601 
have "u \<in> A" using card by auto 

602 
moreover have "u \<noteq> c" using new below by auto 

603 
ultimately show "u \<in> C" using A2 by blast 

604 
next 

605 
assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" 

606 
moreover hence "u \<in> A" using card below by auto 

607 
ultimately show "u \<in> C" using A2 by blast 

608 
qed 

609 
qed 

610 
qed 

611 
next 

612 
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd 

613 
by fastsimp 

614 
qed 

615 
ultimately show ?thesis using x x' by(auto simp:AC) 

616 
qed 

617 
qed 

618 
qed 

619 
qed 

620 
qed 

621 

622 
(* The same proof, but using card 

623 
lemma (in ACf) foldSet_determ_aux: 

624 
"!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> 

625 
\<Longrightarrow> x' = x" 

626 
proof (induct n) 

627 
case 0 thus ?case by simp 

628 
next 

629 
case (Suc n) 

630 
have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> 

631 
\<Longrightarrow> x' = x" and card: "card A < Suc n" 

632 
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . 

633 
from card have "card A < n \<or> card A = n" by arith 

634 
thus ?case 

635 
proof 

636 
assume less: "card A < n" 

637 
show ?thesis by(rule IH[OF less Afoldx Afoldy]) 

638 
next 

639 
assume cardA: "card A = n" 

640 
show ?thesis 

641 
proof (rule foldSet.cases[OF Afoldx]) 

642 
assume "(A, x) = ({}, e)" 

643 
thus "x' = x" using Afoldy by (auto) 

644 
next 

645 
fix B b y 

646 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

647 
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" 

648 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 

649 
show ?thesis 

650 
proof (rule foldSet.cases[OF Afoldy]) 

651 
assume "(A,x') = ({}, e)" 

652 
thus ?thesis using A1 by auto 

653 
next 

654 
fix C c z 

655 
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" 

656 
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" 

657 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto 

658 
have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 

659 
with cardA A1 notinB have less: "card B < n" by simp 

660 
show ?thesis 

661 
proof cases 

662 
assume "b = c" 

663 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

664 
ultimately show ?thesis using IH[OF less] y z x x' by auto 

665 
next 

666 
assume diff: "b \<noteq> c" 

667 
let ?D = "B  {c}" 

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

669 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

670 
have "finite ?D" using finA A1 by simp 

671 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" 

672 
using finite_imp_foldSet by rules 

673 
moreover have cinB: "c \<in> B" using B by(auto) 

674 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" 

675 
by(rule Diff1_foldSet) 

676 
hence "g c \<cdot> d = y" by(rule IH[OF less y]) 

677 
moreover have "g b \<cdot> d = z" 

678 
proof (rule IH[OF _ z]) 

679 
show "card C < n" using C cardA A1 notinB finA cinB 

680 
by(auto simp:card_Diff1_less) 

681 
next 

682 
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd 

683 
by fastsimp 

684 
qed 

685 
ultimately show ?thesis using x x' by(auto simp:AC) 

686 
qed 

687 
qed 

688 
qed 

689 
qed 

690 
qed 

691 
*) 

692 

693 
lemma (in ACf) foldSet_determ: 

694 
"(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x" 

695 
apply(frule foldSet_imp_finite) 

696 
apply(simp add:finite_conv_nat_seg_image) 

697 
apply(blast intro: foldSet_determ_aux [rule_format]) 

698 
done 

699 

700 
lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y" 

701 
by (unfold fold_def) (blast intro: foldSet_determ) 

702 

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

704 

705 
lemma fold_empty [simp]: "fold f g e {} = e" 

706 
by (unfold fold_def) blast 

707 

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

709 
((insert x A, v) : foldSet f g e) = 

710 
(EX y. (A, y) : foldSet f g e & v = f (g x) y)" 

711 
apply auto 

712 
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) 

713 
apply (fastsimp dest: foldSet_imp_finite) 

714 
apply (blast intro: foldSet_determ) 

715 
done 

716 

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

718 

719 
lemma (in ACf) fold_insert[simp]: 

720 
"finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)" 

721 
apply (unfold fold_def) 

722 
apply (simp add: fold_insert_aux) 

723 
apply (rule the_equality) 

724 
apply (auto intro: finite_imp_foldSet 

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

726 
done 

727 

728 
declare 

729 
empty_foldSetE [rule del] foldSet.intros [rule del] 

730 
 {* Delete rules to do with @{text foldSet} relation. *} 

731 

732 
subsubsection{*Lemmas about @{text fold}*} 

733 

734 
lemma (in ACf) fold_commute: 

735 
"finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)" 

736 
apply (induct set: Finites, simp) 

737 
apply (simp add: left_commute) 

738 
done 

739 

740 
lemma (in ACf) fold_nest_Un_Int: 

741 
"finite A ==> finite B 

742 
==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)" 

743 
apply (induct set: Finites, simp) 

744 
apply (simp add: fold_commute Int_insert_left insert_absorb) 

745 
done 

746 

747 
lemma (in ACf) fold_nest_Un_disjoint: 

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

749 
==> fold f g e (A Un B) = fold f g (fold f g e B) A" 

750 
by (simp add: fold_nest_Un_Int) 

751 

752 
lemma (in ACf) fold_reindex: 

753 
assumes fin: "finite B" 

754 
shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B" 

755 
using fin apply (induct) 

756 
apply simp 

757 
apply simp 

758 
done 

759 

760 
lemma (in ACe) fold_Un_Int: 

761 
"finite A ==> finite B ==> 

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

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

764 
apply (induct set: Finites, simp) 

765 
apply (simp add: AC insert_absorb Int_insert_left) 

766 
done 

767 

768 
corollary (in ACe) fold_Un_disjoint: 

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

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

771 
by (simp add: fold_Un_Int) 

772 

773 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

778 
apply (induct set: Finites, simp, atomize) 

779 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 

780 
prefer 2 apply blast 

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

782 
prefer 2 apply blast 

783 
apply (simp add: fold_Un_disjoint) 

784 
done 

785 

786 
lemma (in ACf) fold_cong: 

787 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A" 

788 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold f g a C = fold f h a C") 

789 
apply simp 

790 
apply (erule finite_induct, simp) 

791 
apply (simp add: subset_insert_iff, clarify) 

792 
apply (subgoal_tac "finite C") 

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

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

795 
prefer 2 apply blast 

796 
apply (erule ssubst) 

797 
apply (drule spec) 

798 
apply (erule (1) notE impE) 

799 
apply (simp add: Ball_def del: insert_Diff_single) 

800 
done 

801 

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

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

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

805 
apply (subst Sigma_def) 

806 
apply (subst fold_UN_disjoint) 

807 
apply assumption 

808 
apply simp 

809 
apply blast 

810 
apply (erule fold_cong) 

811 
apply (subst fold_UN_disjoint) 

812 
apply simp 

813 
apply simp 

814 
apply blast 

815 
apply (simp) 

816 
done 

817 

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

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

820 
apply (erule finite_induct) 

821 
apply simp 

822 
apply (simp add:AC) 

823 
done 

824 

825 

15402  826 
subsection {* Generalized summation over a set *} 
827 

828 
constdefs 

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

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

831 

832 
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is 

833 
written @{text"\<Sum>x\<in>A. e"}. *} 

834 

835 
syntax 

836 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 

837 
syntax (xsymbols) 

838 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 

839 
syntax (HTML output) 

840 
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 

841 

842 
translations  {* Beware of argument permutation! *} 

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

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

845 

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

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

848 

849 
syntax 

850 
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 

851 
syntax (xsymbols) 

852 
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 

853 
syntax (HTML output) 

854 
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 

855 

856 
translations 

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

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

859 

860 
text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *} 

861 

862 
syntax 

863 
"_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999) 

864 

865 
parse_translation {* 

866 
let 

867 
fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A 

868 
in [("_Setsum", Setsum_tr)] end; 

869 
*} 

870 

871 
print_translation {* 

872 
let 

873 
fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A 

874 
 setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 

875 
if x<>y then raise Match 

876 
else let val x' = Syntax.mark_bound x 

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

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

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

880 
in 

881 
[("setsum", setsum_tr')] 

882 
end 

883 
*} 

884 

885 
lemma setsum_empty [simp]: "setsum f {} = 0" 

886 
by (simp add: setsum_def) 

887 

888 
lemma setsum_insert [simp]: 

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

890 
by (simp add: setsum_def ACf.fold_insert [OF ACf_add]) 

891 

892 
lemma setsum_reindex: 

893 
"inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" 

894 
by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD) 

895 

896 
lemma setsum_reindex_id: 

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

898 
by (auto simp add: setsum_reindex) 

899 

900 
lemma setsum_cong: 

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

902 
by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add]) 

903 

904 
lemma setsum_reindex_cong: 

905 
"[inj_on f A; B = f ` A; !!a. g a = h (f a)] 

906 
==> setsum h B = setsum g A" 

907 
by (simp add: setsum_reindex cong: setsum_cong) 

908 

909 
lemma setsum_0: "setsum (%i. 0) A = 0" 

910 
apply (clarsimp simp: setsum_def) 

911 
apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add]) 

912 
done 

913 

914 
lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0" 

915 
apply (subgoal_tac "setsum f F = setsum (%x. 0) F") 

916 
apply (erule ssubst, rule setsum_0) 

917 
apply (rule setsum_cong, auto) 

918 
done 

919 

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

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

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

923 
by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric]) 

924 

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

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

927 
by (subst setsum_Un_Int [symmetric], auto) 

928 

929 
(* FIXME get rid of finite I. If infinite, rhs is directly 0, and UNION I A 

930 
is also infinite and hence also 0 *) 

931 
lemma setsum_UN_disjoint: 

932 
"finite I ==> (ALL i:I. finite (A i)) ==> 

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

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

935 
by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong) 

936 

937 

938 
(* FIXME get rid of finite C. If infinite, rhs is directly 0, and Union C 

939 
is also infinite and hence also 0 *) 

940 
lemma setsum_Union_disjoint: 

941 
"finite C ==> (ALL A:C. finite A) ==> 

942 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ==> 

943 
setsum f (Union C) = setsum (setsum f) C" 

944 
apply (frule setsum_UN_disjoint [of C id f]) 

945 
apply (unfold Union_def id_def, assumption+) 

946 
done 

947 

948 
(* FIXME get rid of finite A. If infinite, lhs is directly 0, and SIGMA A B 

949 
is either infinite or empty, and in both cases the rhs is also 0 *) 

950 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 

951 
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = 

952 
(\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))" 

953 
by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong) 

954 

955 
lemma setsum_cartesian_product: "finite A ==> finite B ==> 

956 
(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = 

957 
(\<Sum>z\<in>A <*> B. f (fst z) (snd z))" 

958 
by (erule setsum_Sigma, auto) 

959 

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

961 
by(simp add:setsum_def ACe.fold_distrib[OF ACe_add]) 

962 

963 

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

965 

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

967 
apply (case_tac "finite A") 

968 
prefer 2 apply (simp add: setsum_def) 

969 
apply (erule rev_mp) 

970 
apply (erule finite_induct, auto) 

971 
done 

972 

973 
lemma setsum_eq_0_iff [simp]: 

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

975 
by (induct set: Finites) auto 

976 

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

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

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

980 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) 

981 

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

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

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

985 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) 

986 

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

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

989 
apply (case_tac "finite A") 

990 
prefer 2 apply (simp add: setsum_def) 

991 
apply (erule finite_induct) 

992 
apply (auto simp add: insert_Diff_if) 

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

994 
done 

995 

996 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1000 

1001 
(* By Jeremy Siek: *) 

1002 

1003 
lemma setsum_diff_nat: 

1004 
assumes finB: "finite B" 

1005 
shows "B \<subseteq> A \<Longrightarrow> (setsum f (A  B) :: nat) = (setsum f A)  (setsum f B)" 

1006 
using finB 

1007 
proof (induct) 

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 

1035 
proof (induct) 

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) 

1042 
qed 

1043 
qed 

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 

1051 
proof (induct) 

1052 
case empty 

1053 
thus ?case by simp 

1054 
next 

1055 
case insert 

1056 
thus ?case using add_mono 

1057 
by force 

1058 
qed 

1059 
next 

1060 
case False 

1061 
thus ?thesis 

1062 
by (simp add: setsum_def) 

1063 
qed 

1064 

1065 
lemma setsum_mono2_nat: 

1066 
assumes fin: "finite B" and sub: "A \<subseteq> B" 

1067 
shows "setsum f A \<le> (setsum f B :: nat)" 

1068 
proof  

1069 
have "setsum f A \<le> setsum f A + setsum f (BA)" by arith 

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

1071 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1073 
finally show ?thesis . 

1074 
qed 

1075 

1076 
lemma setsum_negf: "finite A ==> setsum (%x.  (f x)::'a::ab_group_add) A = 

1077 
 setsum f A" 

1078 
by (induct set: Finites, auto) 

1079 

1080 
lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 

1081 
setsum f A  setsum g A" 

1082 
by (simp add: diff_minus setsum_addf setsum_negf) 

1083 

1084 
lemma setsum_nonneg: "[ finite A; 

1085 
\<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x ] ==> 

1086 
0 \<le> setsum f A"; 

1087 
apply (induct set: Finites, auto) 

1088 
apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp) 

1089 
apply (blast intro: add_mono) 

1090 
done 

1091 

1092 
lemma setsum_nonpos: "[ finite A; 

1093 
\<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) ] ==> 

1094 
setsum f A \<le> 0"; 

1095 
apply (induct set: Finites, auto) 

1096 
apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp) 

1097 
apply (blast intro: add_mono) 

1098 
done 

1099 

1100 
lemma setsum_mult: 

1101 
fixes f :: "'a => ('b::semiring_0_cancel)" 

1102 
shows "r * setsum f A = setsum (%n. r * f n) A" 

1103 
proof (cases "finite A") 

1104 
case True 

1105 
thus ?thesis 

1106 
proof (induct) 

1107 
case empty thus ?case by simp 

1108 
next 

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

1110 
qed 

1111 
next 

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

1113 
qed 

1114 

1115 
lemma setsum_abs: 

1116 
fixes f :: "'a => ('b::lordered_ab_group_abs)" 

1117 
assumes fin: "finite A" 

1118 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 

1119 
using fin 

1120 
proof (induct) 

1121 
case empty thus ?case by simp 

1122 
next 

1123 
case (insert x A) 

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

1125 
qed 

1126 

1127 
lemma setsum_abs_ge_zero: 

1128 
fixes f :: "'a => ('b::lordered_ab_group_abs)" 

1129 
assumes fin: "finite A" 

1130 
shows "0 \<le> setsum (%i. abs(f i)) A" 

1131 
using fin 

1132 
proof (induct) 

1133 
case empty thus ?case by simp 

1134 
next 

1135 
case (insert x A) thus ?case by (auto intro: order_trans) 

1136 
qed 

1137 

1138 

1139 
subsection {* Generalized product over a set *} 

1140 

1141 
constdefs 

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

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

1144 

1145 
syntax 

1146 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10) 

1147 

1148 
syntax (xsymbols) 

1149 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 

1150 
syntax (HTML output) 

1151 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 

1152 
translations 

1153 
"\<Prod>i:A. b" == "setprod (%i. b) A"  {* Beware of argument permutation! *} 

1154 

1155 
syntax 

1156 
"_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999) 

1157 

1158 
parse_translation {* 

1159 
let 

1160 
fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A 

1161 
in [("_Setprod", Setprod_tr)] end; 

1162 
*} 

1163 
print_translation {* 

1164 
let fun setprod_tr' [Abs(x,Tx,t), A] = 

1165 
if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match 

1166 
in 

1167 
[("setprod", setprod_tr')] 

1168 
end 

1169 
*} 

1170 

1171 

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

1173 
by (auto simp add: setprod_def) 

1174 

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

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

1177 
by (simp add: setprod_def ACf.fold_insert [OF ACf_mult]) 

1178 

1179 
lemma setprod_reindex: 

1180 
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" 

1181 
by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD) 

1182 

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

1184 
by (auto simp add: setprod_reindex) 

1185 

1186 
lemma setprod_cong: 

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

1188 
by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult]) 

1189 

1190 
lemma setprod_reindex_cong: "inj_on f A ==> 

1191 
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" 

1192 
by (frule setprod_reindex, simp) 

1193 

1194 

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

1196 
apply (case_tac "finite A") 

1197 
apply (erule finite_induct, auto simp add: mult_ac) 

1198 
apply (simp add: setprod_def) 

1199 
done 

1200 

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

1202 
apply (subgoal_tac "setprod f F = setprod (%x. 1) F") 

1203 
apply (erule ssubst, rule setprod_1) 

1204 
apply (rule setprod_cong, auto) 

1205 
done 

1206 

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

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

1209 
by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric]) 

1210 

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

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

1213 
by (subst setprod_Un_Int [symmetric], auto) 

1214 

1215 
lemma setprod_UN_disjoint: 

1216 
"finite I ==> (ALL i:I. finite (A i)) ==> 

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

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

1219 
by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong) 

1220 

1221 
lemma setprod_Union_disjoint: 

1222 
"finite C ==> (ALL A:C. finite A) ==> 

1223 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ==> 

1224 
setprod f (Union C) = setprod (setprod f) C" 

1225 
apply (frule setprod_UN_disjoint [of C id f]) 

1226 
apply (unfold Union_def id_def, assumption+) 

1227 
done 

1228 

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

1230 
(\<Prod>x:A. (\<Prod>y: B x. f x y)) = 

1231 
(\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))" 

1232 
by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong) 

1233 

1234 
lemma setprod_cartesian_product: "finite A ==> finite B ==> 

1235 
(\<Prod>x:A. (\<Prod>y: B. f x y)) = 

1236 
(\<Prod>z:(A <*> B). f (fst z) (snd z))" 

1237 
by (erule setprod_Sigma, auto) 

1238 

1239 
lemma setprod_timesf: 

1240 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 

1241 
by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult]) 

1242 

1243 

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

1245 

1246 
lemma setprod_eq_1_iff [simp]: 

1247 
"finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" 

1248 
by (induct set: Finites) auto 

1249 

1250 
lemma setprod_zero: 

1251 
"finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" 

1252 
apply (induct set: Finites, force, clarsimp) 

1253 
apply (erule disjE, auto) 

1254 
done 

1255 

1256 
lemma setprod_nonneg [rule_format]: 

1257 
"(ALL x: A. (0::'a::ordered_idom) \<le> f x) > 0 \<le> setprod f A" 

1258 
apply (case_tac "finite A") 

1259 
apply (induct set: Finites, force, clarsimp) 

1260 
apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) 

1261 
apply (rule mult_mono, assumption+) 

1262 
apply (auto simp add: setprod_def) 

1263 
done 

1264 

1265 
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) 

1266 
> 0 < setprod f A" 

1267 
apply (case_tac "finite A") 

1268 
apply (induct set: Finites, force, clarsimp) 

1269 
apply (subgoal_tac "0 * 0 < f x * setprod f F", force) 

1270 
apply (rule mult_strict_mono, assumption+) 

1271 
apply (auto simp add: setprod_def) 

1272 
done 

1273 

1274 
lemma setprod_nonzero [rule_format]: 

1275 
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 > x = 0  y = 0) ==> 

1276 
finite A ==> (ALL x: A. f x \<noteq> (0::'a)) > setprod f A \<noteq> 0" 

1277 
apply (erule finite_induct, auto) 

1278 
done 

1279 

1280 
lemma setprod_zero_eq: 

1281 
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 > x = 0  y = 0) ==> 

1282 
finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" 

1283 
apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) 

1284 
done 

1285 

1286 
lemma setprod_nonzero_field: 

1287 
"finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0" 

1288 
apply (rule setprod_nonzero, auto) 

1289 
done 

1290 

1291 
lemma setprod_zero_eq_field: 

1292 
"finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)" 

1293 
apply (rule setprod_zero_eq, auto) 

1294 
done 

1295 

1296 
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> 

1297 
(setprod f (A Un B) :: 'a ::{field}) 

1298 
= setprod f A * setprod f B / setprod f (A Int B)" 

1299 
apply (subst setprod_Un_Int [symmetric], auto) 

1300 
apply (subgoal_tac "finite (A Int B)") 

1301 
apply (frule setprod_nonzero_field [of "A Int B" f], assumption) 

1302 
apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self) 

1303 
done 

1304 

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

1306 
(setprod f (A  {a}) :: 'a :: {field}) = 

1307 
(if a:A then setprod f A / f a else setprod f A)" 

1308 
apply (erule finite_induct) 

1309 
apply (auto simp add: insert_Diff_if) 

1310 
apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") 

1311 
apply (erule ssubst) 

1312 
apply (subst times_divide_eq_right [THEN sym]) 

1313 
apply (auto simp add: mult_ac times_divide_eq_right divide_self) 

1314 
done 

1315 

1316 
lemma setprod_inversef: "finite A ==> 

1317 
ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> 

1318 
setprod (inverse \<circ> f) A = inverse (setprod f A)" 

1319 
apply (erule finite_induct) 

1320 
apply (simp, simp) 

1321 
done 

1322 

1323 
lemma setprod_dividef: 

1324 
"[finite A; 

1325 
\<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})] 

1326 
==> setprod (%x. f x / g x) A = setprod f A / setprod g A" 

1327 
apply (subgoal_tac 

1328 
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") 

1329 
apply (erule ssubst) 

1330 
apply (subst divide_inverse) 

1331 
apply (subst setprod_timesf) 

1332 
apply (subst setprod_inversef, assumption+, rule refl) 

1333 
apply (rule setprod_cong, rule refl) 

1334 
apply (subst divide_inverse, auto) 

1335 
done 

1336 

12396  1337 
subsection {* Finite cardinality *} 
1338 

15402  1339 
text {* This definition, although traditional, is ugly to work with: 
1340 
@{text "card A == LEAST n. EX f. A = {f i  i. i < n}"}. 

1341 
But now that we have @{text setsum} things are easy: 

12396  1342 
*} 
1343 

1344 
constdefs 

1345 
card :: "'a set => nat" 

15402  1346 
"card A == setsum (%x. 1::nat) A" 
12396  1347 

1348 
lemma card_empty [simp]: "card {} = 0" 

15402  1349 
by (simp add: card_def) 
1350 

1351 
lemma card_eq_setsum: "card A = setsum (%x. 1) A" 

1352 
by (simp add: card_def) 

12396  1353 

1354 
lemma card_insert_disjoint [simp]: 

1355 
"finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" 

15402  1356 
by(simp add: card_def ACf.fold_insert[OF ACf_add]) 
1357 

1358 
lemma card_insert_if: 

1359 
"finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" 

1360 
by (simp add: insert_absorb) 

12396  1361 

1362 
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" 

1363 
apply auto 

14208  1364 
apply (drule_tac a = x in mk_disjoint_insert, clarify) 
15402  1365 
apply (auto) 
12396  1366 
done 
1367 

1368 
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A  {x})) = card A" 

14302  1369 
apply(rule_tac t = A in insert_Diff [THEN subst], assumption) 
1370 
apply(simp del:insert_Diff_single) 

1371 
done 

12396  1372 

1373 
lemma card_Diff_singleton: 

1374 
"finite A ==> x: A ==> card (A  {x}) = card A  1" 

1375 
by (simp add: card_Suc_Diff1 [symmetric]) 

1376 

1377 
lemma card_Diff_singleton_if: 

1378 
"finite A ==> card (A{x}) = (if x : A then card A  1 else card A)" 

1379 
by (simp add: card_Diff_singleton) 

1380 

1381 
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A  {x}))" 

1382 
by (simp add: card_insert_if card_Suc_Diff1) 

1383 
