author  nipkow 
Sun, 30 Jan 2005 20:48:50 +0100  
changeset 15480  cb3612cc41a3 
parent 15479  fbc473ea9d3c 
child 15483  704b3ce6d0f7 
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 
12396  5 
*) 
6 

7 
header {* Finite sets *} 

8 

15131  9 
theory Finite_Set 
15140  10 
imports Divides Power Inductive 
15131  11 
begin 
12396  12 

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

15 
consts Finites :: "'a set set" 

13737  16 
syntax 
17 
finite :: "'a set => bool" 

18 
translations 

19 
"finite A" == "A : Finites" 

12396  20 

21 
inductive Finites 

22 
intros 

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

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

25 

26 
axclass finite \<subseteq> type 

27 
finite: "finite UNIV" 

28 

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

32 
proof  

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

34 
thus ?thesis by blast 

35 
qed 

12396  36 

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

38 
"finite F ==> 

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

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

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

43 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  44 
assume "finite F" 
45 
thus "P F" 

46 
proof induct 

47 
show "P {}" . 

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

48 
fix x F assume F: "finite F" and P: "P F" 
12396  49 
show "P (insert x F)" 
50 
proof cases 

51 
assume "x \<in> F" 

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

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

54 
next 

55 
assume "x \<notin> F" 

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

57 
qed 

58 
qed 

59 
qed 

60 

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

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

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

63 
P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 
12396  64 
P F" 
65 
proof  

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

67 
"!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 
12396  68 
assume "finite F" 
69 
thus "F \<subseteq> A ==> P F" 

70 
proof induct 

71 
show "P {}" . 

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

72 
fix x F assume "finite F" and "x \<notin> F" 
12396  73 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 
74 
show "P (insert x F)" 

75 
proof (rule insert) 

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

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

78 
with P show "P F" . 

79 
qed 

80 
qed 

81 
qed 

82 

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

85 
lemma finite_imp_nat_seg_image: 

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

87 
using fin 

88 
proof induct 

89 
case empty 

90 
show ?case 

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

92 
next 

93 
case (insert a A) 

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

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

96 
by (auto simp add:image_def Ball_def) 

97 
thus ?case by blast 

98 
qed 

99 

100 
lemma nat_seg_image_imp_finite: 

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

102 
proof (induct n) 

103 
case 0 thus ?case by simp 

104 
next 

105 
case (Suc n) 

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

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

108 
show ?case 

109 
proof cases 

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

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

112 
thus ?thesis using finB by simp 

113 
next 

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

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

116 
thus ?thesis using finB by simp 

117 
qed 

118 
qed 

119 

120 
lemma finite_conv_nat_seg_image: 

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

122 
by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite) 

123 

124 
subsubsection{* Finiteness and set theoretic constructions *} 

125 

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

128 
by (induct set: Finites) simp_all 

129 

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

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

132 
proof  

133 
assume "finite B" 

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

135 
proof induct 

136 
case empty 

137 
thus ?case by simp 

138 
next 

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

139 
case (insert x F A) 
12396  140 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 
141 
show "finite A" 

142 
proof cases 

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

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

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

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

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

148 
finally show ?thesis . 

149 
next 

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

151 
assume "x \<notin> A" 

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

153 
qed 

154 
qed 

155 
qed 

156 

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

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

159 

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

161 
 {* The converse obviously fails. *} 

162 
by (blast intro: finite_subset) 

163 

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

165 
apply (subst insert_is_Un) 

14208  166 
apply (simp only: finite_Un, blast) 
12396  167 
done 
168 

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

171 
by (induct rule:finite_induct) simp_all 

172 

12396  173 
lemma finite_empty_induct: 
174 
"finite A ==> 

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

176 
proof  

177 
assume "finite A" 

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

179 
have "P (A  A)" 

180 
proof  

181 
fix c b :: "'a set" 

182 
presume c: "finite c" and b: "finite b" 

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

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

185 
proof induct 

186 
case empty 

187 
from P1 show ?case by simp 

188 
next 

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

189 
case (insert x F) 
12396  190 
have "P (b  F  {x})" 
191 
proof (rule P2) 

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

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

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

195 
qed 

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

197 
finally show ?case . 

198 
qed 

199 
next 

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

201 
qed 

202 
thus "P {}" by simp 

203 
qed 

204 

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

206 
by (rule Diff_subset [THEN finite_subset]) 

207 

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

209 
apply (subst Diff_insert) 

210 
apply (case_tac "a : A  B") 

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

14208  212 
apply (subst insert_Diff, simp_all) 
12396  213 
done 
214 

215 

15392  216 
text {* Image and Inverse Image over Finite Sets *} 
13825  217 

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

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

220 
by (induct set: Finites) simp_all 

221 

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

222 
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

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

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

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

226 

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

14208  229 
apply (drule finite_imageI, simp) 
13825  230 
done 
231 

12396  232 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
233 
proof  

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

235 
fix B :: "'a set" 

236 
assume "finite B" 

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

238 
apply induct 

239 
apply simp 

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

241 
apply clarify 

242 
apply (simp (no_asm_use) add: inj_on_def) 

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

248 
done 

249 
qed (rule refl) 

250 

251 

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

254 
is included in a singleton. *} 

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

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

256 
apply (blast intro: the_equality [symmetric]) 
13825  257 
done 
258 

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

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

261 
is finite. *} 

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

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

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

264 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  265 
done 
266 

267 

15392  268 
text {* The finite UNION of finite sets *} 
12396  269 

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

271 
by (induct set: Finites) simp_all 

272 

273 
text {* 

274 
Strengthen RHS to 

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

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

277 
We'd need to prove 

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

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

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

282 
by (blast intro: finite_UN_I finite_subset) 

283 

284 

15392  285 
text {* Sigma of finite sets *} 
12396  286 

287 
lemma finite_SigmaI [simp]: 

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

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

290 

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

293 
by (rule finite_SigmaI) 

294 

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

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

298 
apply (erule ssubst) 

14208  299 
apply (erule finite_SigmaI, auto) 
12396  300 
done 
301 

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

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

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

304 
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

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

306 
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

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

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

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

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

311 
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

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

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

314 
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

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

316 

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

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

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

319 
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

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

321 
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

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

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

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

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

326 
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

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

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

329 
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

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

331 

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

332 

12396  333 
instance unit :: finite 
334 
proof 

335 
have "finite {()}" by simp 

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

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

338 
qed 

339 

340 
instance * :: (finite, finite) finite 

341 
proof 

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

343 
proof (rule finite_Prod_UNIV) 

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

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

346 
qed 

347 
qed 

348 

349 

15392  350 
text {* The powerset of a finite set *} 
12396  351 

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

353 
proof 

354 
assume "finite (Pow A)" 

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

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

357 
next 

358 
assume "finite A" 

359 
thus "finite (Pow A)" 

360 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

361 
qed 

362 

15392  363 

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

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

366 

367 

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

370 
apply simp 

371 
apply (rule iffI) 

372 
apply (erule finite_imageD [unfolded inj_on_def]) 

373 
apply (simp split add: split_split) 

374 
apply (erule finite_imageI) 

14208  375 
apply (simp add: converse_def image_def, auto) 
12396  376 
apply (rule bexI) 
377 
prefer 2 apply assumption 

378 
apply simp 

379 
done 

380 

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

381 

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

12396  384 

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

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

387 
apply (induct set: Finites) 

388 
apply (auto simp add: Field_def Domain_insert Range_insert) 

389 
done 

390 

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

392 
apply clarify 

393 
apply (erule trancl_induct) 

394 
apply (auto simp add: Field_def) 

395 
done 

396 

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

398 
apply auto 

399 
prefer 2 

400 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

401 
apply (rule finite_SigmaI) 

402 
prefer 3 

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

403 
apply (blast intro: r_into_trancl' finite_subset) 
12396  404 
apply (auto simp add: finite_Field) 
405 
done 

406 

407 

15392  408 
subsection {* A fold functional for finite sets *} 
409 

410 
text {* The intended behaviour is 

15480  411 
@{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  412 
if @{text f} is associativecommutative. For an application of @{text fold} 
413 
se the definitions of sums and products over finite sets. 

414 
*} 

415 

416 
consts 

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

418 

15480  419 
inductive "foldSet f g z" 
15392  420 
intros 
15480  421 
emptyI [intro]: "({}, z) : foldSet f g z" 
422 
insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk> 

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

15392  424 

15480  425 
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z" 
15392  426 

427 
constdefs 

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

15480  429 
"fold f g z A == THE x. (A, x) : foldSet f g z" 
15392  430 

431 
lemma Diff1_foldSet: 

15480  432 
"(A  {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" 
15392  433 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
434 

15480  435 
lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" 
15392  436 
by (induct set: foldSet) auto 
437 

15480  438 
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z" 
15392  439 
by (induct set: Finites) auto 
440 

441 

442 
subsubsection {* Commutative monoids *} 

15480  443 

15392  444 
locale ACf = 
445 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

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

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

448 

449 
locale ACe = ACf + 

450 
fixes e :: 'a 

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

452 

15480  453 
locale ACIf = ACf + 
454 
assumes idem: "x \<cdot> x = x" 

455 

15392  456 
lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 
457 
proof  

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

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

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

461 
finally show ?thesis . 

462 
qed 

463 

464 
lemmas (in ACf) AC = assoc commute left_commute 

465 

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

467 
proof  

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

469 
thus ?thesis by (subst commute) 

470 
qed 

471 

15402  472 
text{* Instantiation of locales: *} 
473 

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

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

476 

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

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

479 

480 

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

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

483 

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

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

486 

487 

15392  488 
subsubsection{*From @{term foldSet} to @{term fold}*} 
489 

15479  490 
(* only used in the next lemma, but in there twice *) 
491 
lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and 

492 
card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)" 

493 
shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h") 

494 
proof 

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

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

497 
proof 

498 
show "B \<subseteq> ?r" 

499 
proof 

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

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

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

503 
using card by(auto simp:image_def) 

504 
show "u \<in> ?r" 

505 
proof cases 

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

507 
thus ?thesis using unotb by(fastsimp) 

508 
next 

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

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

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

512 
using A1 card by blast 

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

514 
proof (rule ccontr) 

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

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

517 
thus False using unotb by simp 

518 
qed 

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

520 
qed 

521 
qed 

522 
next 

523 
show "?r \<subseteq> B" 

524 
proof 

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

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

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

528 
by(auto simp:image_def) 

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

530 
proof 

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

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

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

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

535 
next 

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

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

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

539 
qed 

540 
qed 

541 
qed 

542 
qed 

543 

15392  544 
lemma (in ACf) foldSet_determ_aux: 
15480  545 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk> 
15392  546 
\<Longrightarrow> x' = x" 
547 
proof (induct n) 

548 
case 0 thus ?case by auto 

549 
next 

550 
case (Suc n) 

15480  551 
have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g z; (A,x') \<in> foldSet f g z\<rbrakk> 
15392  552 
\<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}" 
15480  553 
and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" . 
15392  554 
show ?case 
555 
proof cases 

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

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

558 
using card by (auto simp:image_def less_Suc_eq) 

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

560 
next 

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

562 
show ?thesis 

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

15480  564 
assume "(A, x) = ({}, z)" 
15392  565 
thus "x' = x" using Afoldy by (auto) 
566 
next 

567 
fix B b y 

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

15480  569 
and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B" 
15392  570 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 
571 
show ?thesis 

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

15480  573 
assume "(A,x') = ({}, z)" 
15392  574 
thus ?thesis using A1 by auto 
575 
next 

15480  576 
fix C c r 
577 
assume eq2: "(A,x') = (insert c C, g c \<cdot> r)" 

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

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

15479  580 
obtain hB where lessB: "B = hB ` {i. i<n}" 
581 
using card_lemma[OF A1 notinB card new] by auto 

582 
obtain hC where lessC: "C = hC ` {i. i<n}" 

583 
using card_lemma[OF A2 notinC card new] by auto 

15392  584 
show ?thesis 
585 
proof cases 

586 
assume "b = c" 

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

15480  588 
ultimately show ?thesis using IH[OF lessB] y r x x' by auto 
15392  589 
next 
590 
assume diff: "b \<noteq> c" 

591 
let ?D = "B  {c}" 

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

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

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

15480  596 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  597 
using finite_imp_foldSet by rules 
598 
moreover have cinB: "c \<in> B" using B by(auto) 

15480  599 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  600 
by(rule Diff1_foldSet) 
15479  601 
hence "g c \<cdot> d = y" by(rule IH[OF lessB y]) 
15480  602 
moreover have "g b \<cdot> d = r" 
603 
proof (rule IH[OF lessC r]) 

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

15392  605 
by fastsimp 
606 
qed 

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

608 
qed 

609 
qed 

610 
qed 

611 
qed 

612 
qed 

613 

614 
(* The same proof, but using card 

615 
lemma (in ACf) foldSet_determ_aux: 

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

617 
\<Longrightarrow> x' = x" 

618 
proof (induct n) 

619 
case 0 thus ?case by simp 

620 
next 

621 
case (Suc n) 

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

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

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

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

626 
thus ?case 

627 
proof 

628 
assume less: "card A < n" 

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

630 
next 

631 
assume cardA: "card A = n" 

632 
show ?thesis 

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

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

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

636 
next 

637 
fix B b y 

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

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

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

641 
show ?thesis 

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

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

644 
thus ?thesis using A1 by auto 

645 
next 

646 
fix C c z 

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

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

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

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

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

652 
show ?thesis 

653 
proof cases 

654 
assume "b = c" 

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

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

657 
next 

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

659 
let ?D = "B  {c}" 

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

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

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

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

664 
using finite_imp_foldSet by rules 

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

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

667 
by(rule Diff1_foldSet) 

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

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

670 
proof (rule IH[OF _ z]) 

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

672 
by(auto simp:card_Diff1_less) 

673 
next 

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

675 
by fastsimp 

676 
qed 

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

678 
qed 

679 
qed 

680 
qed 

681 
qed 

682 
qed 

683 
*) 

684 

685 
lemma (in ACf) foldSet_determ: 

15480  686 
"(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x" 
15392  687 
apply(frule foldSet_imp_finite) 
688 
apply(simp add:finite_conv_nat_seg_image) 

689 
apply(blast intro: foldSet_determ_aux [rule_format]) 

690 
done 

691 

15480  692 
lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y" 
15392  693 
by (unfold fold_def) (blast intro: foldSet_determ) 
694 

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

696 

15480  697 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  698 
by (unfold fold_def) blast 
699 

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

15480  701 
((insert x A, v) : foldSet f g z) = 
702 
(EX y. (A, y) : foldSet f g z & v = f (g x) y)" 

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

705 
apply (fastsimp dest: foldSet_imp_finite) 

706 
apply (blast intro: foldSet_determ) 

707 
done 

708 

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

710 

711 
lemma (in ACf) fold_insert[simp]: 

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

715 
apply (rule the_equality) 

716 
apply (auto intro: finite_imp_foldSet 

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

718 
done 

719 

720 
declare 

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

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

723 

15480  724 
text{* A simplified version for idempotent functions: *} 
725 

726 
lemma (in ACIf) fold_insert2: 

727 
assumes finA: "finite A" 

728 
shows "fold (op \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A" 

729 
proof cases 

730 
assume "a \<in> A" 

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

732 
by(blast dest: mk_disjoint_insert) 

733 
show ?thesis 

734 
proof  

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

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

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

738 
using finB disj by(simp) 

739 
also have "\<dots> = g a \<cdot> fold f g z A" 

740 
using A finB disj by(simp add:idem assoc[symmetric]) 

741 
finally show ?thesis . 

742 
qed 

743 
next 

744 
assume "a \<notin> A" 

745 
with finA show ?thesis by simp 

746 
qed 

747 

15392  748 
subsubsection{*Lemmas about @{text fold}*} 
749 

750 
lemma (in ACf) fold_commute: 

15480  751 
"finite A ==> (!!z. f (g x) (fold f g z A) = fold f g (f (g x) z) A)" 
15392  752 
apply (induct set: Finites, simp) 
753 
apply (simp add: left_commute) 

754 
done 

755 

756 
lemma (in ACf) fold_nest_Un_Int: 

757 
"finite A ==> finite B 

15480  758 
==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)" 
15392  759 
apply (induct set: Finites, simp) 
760 
apply (simp add: fold_commute Int_insert_left insert_absorb) 

761 
done 

762 

763 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  765 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  766 
by (simp add: fold_nest_Un_Int) 
767 

768 
lemma (in ACf) fold_reindex: 

769 
assumes fin: "finite B" 

15480  770 
shows "inj_on h B \<Longrightarrow> fold f g z (h ` B) = fold f (g \<circ> h) z B" 
15392  771 
using fin apply (induct) 
772 
apply simp 

773 
apply simp 

774 
done 

775 

776 
lemma (in ACe) fold_Un_Int: 

777 
"finite A ==> finite B ==> 

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

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

780 
apply (induct set: Finites, simp) 

781 
apply (simp add: AC insert_absorb Int_insert_left) 

782 
done 

783 

784 
corollary (in ACe) fold_Un_disjoint: 

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

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

787 
by (simp add: fold_Un_Int) 

788 

789 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

796 
prefer 2 apply blast 

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

798 
prefer 2 apply blast 

799 
apply (simp add: fold_Un_disjoint) 

800 
done 

801 

802 
lemma (in ACf) fold_cong: 

15480  803 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
804 
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  805 
apply simp 
806 
apply (erule finite_induct, simp) 

807 
apply (simp add: subset_insert_iff, clarify) 

808 
apply (subgoal_tac "finite C") 

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

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

811 
prefer 2 apply blast 

812 
apply (erule ssubst) 

813 
apply (drule spec) 

814 
apply (erule (1) notE impE) 

815 
apply (simp add: Ball_def del: insert_Diff_single) 

816 
done 

817 

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

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

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

821 
apply (subst Sigma_def) 

822 
apply (subst fold_UN_disjoint) 

823 
apply assumption 

824 
apply simp 

825 
apply blast 

826 
apply (erule fold_cong) 

827 
apply (subst fold_UN_disjoint) 

828 
apply simp 

829 
apply simp 

830 
apply blast 

831 
apply (simp) 

832 
done 

833 

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

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

836 
apply (erule finite_induct) 

837 
apply simp 

838 
apply (simp add:AC) 

839 
done 

840 

841 

15402  842 
subsection {* Generalized summation over a set *} 
843 

844 
constdefs 

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

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

847 

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

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

850 

851 
syntax 

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

853 
syntax (xsymbols) 

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

855 
syntax (HTML output) 

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

857 

858 
translations  {* Beware of argument permutation! *} 

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

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

861 

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

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

864 

865 
syntax 

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

867 
syntax (xsymbols) 

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

869 
syntax (HTML output) 

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

871 

872 
translations 

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

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

875 

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

877 

878 
syntax 

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

880 

881 
parse_translation {* 

882 
let 

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

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

885 
*} 

886 

887 
print_translation {* 

888 
let 

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

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

891 
if x<>y then raise Match 

892 
else let val x' = Syntax.mark_bound x 

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

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

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

896 
in 

897 
[("setsum", setsum_tr')] 

898 
end 

899 
*} 

900 

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

902 
by (simp add: setsum_def) 

903 

904 
lemma setsum_insert [simp]: 

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

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

907 

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

908 
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

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

910 

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

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

914 

915 
lemma setsum_reindex_id: 

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

917 
by (auto simp add: setsum_reindex) 

918 

919 
lemma setsum_cong: 

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

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

922 

923 
lemma setsum_reindex_cong: 

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

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

926 
by (simp add: setsum_reindex cong: setsum_cong) 

927 

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

929 
apply (clarsimp simp: setsum_def) 

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

931 
done 

932 

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

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

935 
apply (erule ssubst, rule setsum_0) 

936 
apply (rule setsum_cong, auto) 

937 
done 

938 

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

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

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

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

943 

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

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

946 
by (subst setsum_Un_Int [symmetric], auto) 

947 

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

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

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

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

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

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

955 

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

956 
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

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

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

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

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

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

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

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

966 
done 
15402  967 

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

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

969 
the rhs need not be, since SIGMA A B could still be finite.*) 
15402  970 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
971 
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = 

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

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

974 

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

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

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

977 
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

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

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

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

985 
done 
15402  986 

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

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

989 

990 

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

992 

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

994 
apply (case_tac "finite A") 

995 
prefer 2 apply (simp add: setsum_def) 

996 
apply (erule rev_mp) 

997 
apply (erule finite_induct, auto) 

998 
done 

999 

1000 
lemma setsum_eq_0_iff [simp]: 

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

1002 
by (induct set: Finites) auto 

1003 

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

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

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

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

1008 

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

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

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

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

1013 

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

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

1016 
apply (case_tac "finite A") 

1017 
prefer 2 apply (simp add: setsum_def) 

1018 
apply (erule finite_induct) 

1019 
apply (auto simp add: insert_Diff_if) 

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

1021 
done 

1022 

1023 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1027 

1028 
(* By Jeremy Siek: *) 

1029 

1030 
lemma setsum_diff_nat: 

1031 
assumes finB: "finite B" 

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

1033 
using finB 

1034 
proof (induct) 

1035 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 

1036 
next 

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

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

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

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

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

1042 
by (simp add: setsum_diff1_nat) 

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

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

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

1046 
by simp 

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

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

1049 
by simp 

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

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

1052 
by simp 

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

1054 
qed 

1055 

1056 
lemma setsum_diff: 

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

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

1059 
proof  

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

1061 
show ?thesis using finiteB le 

1062 
proof (induct) 

1063 
case empty 

1064 
thus ?case by auto 

1065 
next 

1066 
case (insert x F) 

1067 
thus ?case using le finiteB 

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

1069 
qed 

1070 
qed 

1071 

1072 
lemma setsum_mono: 

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

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

1075 
proof (cases "finite K") 

1076 
case True 

1077 
thus ?thesis using le 

1078 
proof (induct) 

1079 
case empty 

1080 
thus ?case by simp 

1081 
next 

1082 
case insert 

1083 
thus ?case using add_mono 

1084 
by force 

1085 
qed 

1086 
next 

1087 
case False 

1088 
thus ?thesis 

1089 
by (simp add: setsum_def) 

1090 
qed 

1091 

1092 
lemma setsum_mono2_nat: 

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

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

1095 
proof  

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

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

1098 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1100 
finally show ?thesis . 

1101 
qed 

1102 

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

1104 
 setsum f A" 

1105 
by (induct set: Finites, auto) 

1106 

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

1108 
setsum f A  setsum g A" 

1109 
by (simp add: diff_minus setsum_addf setsum_negf) 

1110 

1111 
lemma setsum_nonneg: "[ finite A; 

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

1113 
0 \<le> setsum f A"; 

1114 
apply (induct set: Finites, auto) 

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

1116 
apply (blast intro: add_mono) 

1117 
done 

1118 

1119 
lemma setsum_nonpos: "[ finite A; 

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

1121 
setsum f A \<le> 0"; 

1122 
apply (induct set: Finites, auto) 

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

1124 
apply (blast intro: add_mono) 

1125 
done 

1126 

1127 
lemma setsum_mult: 

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

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

1130 
proof (cases "finite A") 

1131 
case True 

1132 
thus ?thesis 

1133 
proof (induct) 

1134 
case empty thus ?case by simp 

1135 
next 

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

1137 
qed 

1138 
next 

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

1140 
qed 

1141 

1142 
lemma setsum_abs: 

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

1144 
assumes fin: "finite A" 

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

1146 
using fin 

1147 
proof (induct) 

1148 
case empty thus ?case by simp 

1149 
next 

1150 
case (insert x A) 

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

1152 
qed 

1153 

1154 
lemma setsum_abs_ge_zero: 

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

1156 
assumes fin: "finite A" 

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

1158 
using fin 

1159 
proof (induct) 

1160 
case empty thus ?case by simp 

1161 
next 

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

1163 
qed 

1164 

1165 

1166 
subsection {* Generalized product over a set *} 

1167 

1168 
constdefs 

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

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

1171 

1172 
syntax 

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

1174 

1175 
syntax (xsymbols) 

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

1177 
syntax (HTML output) 

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

1179 
translations 

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

1181 

1182 
syntax 

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

1184 

1185 
parse_translation {* 

1186 
let 

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

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

1189 
*} 

1190 
print_translation {* 

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

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

1193 
in 

1194 
[("setprod", setprod_tr')] 

1195 
end 

1196 
*} 

1197 

1198 

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

1200 
by (auto simp add: setprod_def) 

1201 

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

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

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

1205 

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

1206 
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

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

1208 

15402  1209 
lemma setprod_reindex: 
1210 
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" 

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

1212 

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

1214 
by (auto simp add: setprod_reindex) 

1215 

1216 
lemma setprod_cong: 

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

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

1219 

1220 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1222 
by (frule setprod_reindex, simp) 

1223 

1224 

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

1226 
apply (case_tac "finite A") 

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

1228 
done 

1229 

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

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

1232 
apply (erule ssubst, rule setprod_1) 

1233 
apply (rule setprod_cong, auto) 

1234 
done 

1235 

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

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

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

1239 

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

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

1242 
by (subst setprod_Un_Int [symmetric], auto) 

1243 

1244 
lemma setprod_UN_disjoint: 

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

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

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

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

1249 

1250 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1258 
done 
15402  1259 

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

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

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

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

1264 

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

1265 
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

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

1267 
"(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

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

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

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

1275 
done 
15402  1276 

1277 
lemma setprod_timesf: 

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

1278 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 
15402  1279 
by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult]) 
1280 

1281 

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

1283 

1284 
lemma setprod_eq_1_iff [simp]: 

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

1286 
by (induct set: Finites) auto 

1287 

1288 
lemma setprod_zero: 

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

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

1291 
apply (erule disjE, auto) 

1292 
done 

1293 

1294 
lemma setprod_nonneg [rule_format]: 

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

1296 
apply (case_tac "finite A") 

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

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

1299 
apply (rule mult_mono, assumption+) 

1300 
apply (auto simp add: setprod_def) 

1301 
done 

1302 

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

1304 
> 0 < setprod f A" 

1305 
apply (case_tac "finite A") 

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

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

1308 
apply (rule mult_strict_mono, assumption+) 

1309 
apply (auto simp add: setprod_def) 

1310 
done 

1311 

1312 
lemma setprod_nonzero [rule_format]: 

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

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

1315 
apply (erule finite_induct, auto) 

1316 
done 

1317 

1318 
lemma setprod_zero_eq: 

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

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

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

1322 
done 

1323 

1324 
lemma setprod_nonzero_field: 

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

1326 
apply (rule setprod_nonzero, auto) 

1327 
done 

1328 

1329 
lemma setprod_zero_eq_field: 

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

1331 
apply (rule setprod_zero_eq, auto) 

1332 
done 

1333 

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

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

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

1337 
apply (subst setprod_Un_Int [symmetric], auto) 

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

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

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

1341 
done 

1342 

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

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

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

1346 
apply (erule finite_induct) 

1347 
apply (auto simp add: insert_Diff_if) 

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

1349 
apply (erule ssubst) 

1350 
apply (subst times_divide_eq_right [THEN sym]) 

1351 
apply (auto simp add: mult_ac times_divide_eq_right divide_self) 

1352 
done 

1353 

1354 
lemma setprod_inversef: "finite A ==> 

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

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

1357 
apply (erule finite_induct) 

1358 
apply (simp, simp) 

1359 
done 

1360 

1361 
lemma setprod_dividef: 

1362 
"[finite A; 

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

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

1365 
apply (subgoal_tac 

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

1367 
apply (erule ssubst) 

1368 
apply (subst divide_inverse) 

1369 
apply (subst setprod_timesf) 

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

1371 
apply (rule setprod_cong, rule refl) 

1372 
apply (subst divide_inverse, auto) 

1373 
done 

1374 

12396  1 