author  ballarin 
Mon, 18 Apr 2005 15:53:51 +0200  
changeset 15765  6472d4942992 
parent 15554  03d4347b071d 
child 15770  90b6433c6093 
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 
15512
ed1fa4617f52
Extracted generic lattice stuff to new Lattice_Locales.thy
nipkow
parents:
15510
diff
changeset

10 
imports Divides Power Inductive Lattice_Locales 
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 

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

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

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

65 
\<Longrightarrow> P F" 

66 
using fin 

67 
proof induct 

68 
case empty thus ?case by simp 

69 
next 

70 
case (insert x F) 

71 
show ?case 

72 
proof cases 

73 
assume "F = {}" thus ?thesis using insert(4) by simp 

74 
next 

75 
assume "F \<noteq> {}" thus ?thesis using insert by blast 

76 
qed 

77 
qed 

78 

12396  79 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 
80 
"finite F ==> F \<subseteq> A ==> 

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

81 
P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 
12396  82 
P F" 
83 
proof  

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

85 
"!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 
12396  86 
assume "finite F" 
87 
thus "F \<subseteq> A ==> P F" 

88 
proof induct 

89 
show "P {}" . 

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

90 
fix x F assume "finite F" and "x \<notin> F" 
12396  91 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 
92 
show "P (insert x F)" 

93 
proof (rule insert) 

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

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

96 
with P show "P F" . 

97 
qed 

98 
qed 

99 
qed 

100 

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

15510  103 
lemma finite_imp_nat_seg_image_inj_on: 
104 
assumes fin: "finite A" 

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

15392  106 
using fin 
107 
proof induct 

108 
case empty 

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

111 
qed 

15392  112 
next 
113 
case (insert a A) 

15510  114 
have notinA: "a \<notin> A" . 
115 
from insert.hyps obtain n f 

116 
where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast 

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

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

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

15392  120 
thus ?case by blast 
121 
qed 

122 

123 
lemma nat_seg_image_imp_finite: 

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

125 
proof (induct n) 

126 
case 0 thus ?case by simp 

127 
next 

128 
case (Suc n) 

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

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

131 
show ?case 

132 
proof cases 

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

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

135 
thus ?thesis using finB by simp 

136 
next 

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

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

139 
thus ?thesis using finB by simp 

140 
qed 

141 
qed 

142 

143 
lemma finite_conv_nat_seg_image: 

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

15510  145 
by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 
15392  146 

147 
subsubsection{* Finiteness and set theoretic constructions *} 

148 

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

151 
by (induct set: Finites) simp_all 

152 

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

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

155 
proof  

156 
assume "finite B" 

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

158 
proof induct 

159 
case empty 

160 
thus ?case by simp 

161 
next 

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

162 
case (insert x F A) 
12396  163 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 
164 
show "finite A" 

165 
proof cases 

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

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

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

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

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

171 
finally show ?thesis . 

172 
next 

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

174 
assume "x \<notin> A" 

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

176 
qed 

177 
qed 

178 
qed 

179 

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

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

182 

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

184 
 {* The converse obviously fails. *} 

185 
by (blast intro: finite_subset) 

186 

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

188 
apply (subst insert_is_Un) 

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

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

194 
by (induct rule:finite_induct) simp_all 

195 

12396  196 
lemma finite_empty_induct: 
197 
"finite A ==> 

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

199 
proof  

200 
assume "finite A" 

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

202 
have "P (A  A)" 

203 
proof  

204 
fix c b :: "'a set" 

205 
presume c: "finite c" and b: "finite b" 

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

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

208 
proof induct 

209 
case empty 

210 
from P1 show ?case by simp 

211 
next 

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

212 
case (insert x F) 
12396  213 
have "P (b  F  {x})" 
214 
proof (rule P2) 

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

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

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

218 
qed 

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

220 
finally show ?case . 

221 
qed 

222 
next 

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

224 
qed 

225 
thus "P {}" by simp 

226 
qed 

227 

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

229 
by (rule Diff_subset [THEN finite_subset]) 

230 

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

232 
apply (subst Diff_insert) 

233 
apply (case_tac "a : A  B") 

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

14208  235 
apply (subst insert_Diff, simp_all) 
12396  236 
done 
237 

238 

15392  239 
text {* Image and Inverse Image over Finite Sets *} 
13825  240 

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

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

243 
by (induct set: Finites) simp_all 

244 

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

245 
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

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

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

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

249 

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

14208  252 
apply (drule finite_imageI, simp) 
13825  253 
done 
254 

12396  255 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
256 
proof  

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

258 
fix B :: "'a set" 

259 
assume "finite B" 

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

261 
apply induct 

262 
apply simp 

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

264 
apply clarify 

265 
apply (simp (no_asm_use) add: inj_on_def) 

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

271 
done 

272 
qed (rule refl) 

273 

274 

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

277 
is included in a singleton. *} 

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

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

279 
apply (blast intro: the_equality [symmetric]) 
13825  280 
done 
281 

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

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

284 
is finite. *} 

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

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

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

287 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  288 
done 
289 

290 

15392  291 
text {* The finite UNION of finite sets *} 
12396  292 

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

294 
by (induct set: Finites) simp_all 

295 

296 
text {* 

297 
Strengthen RHS to 

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

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

300 
We'd need to prove 

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

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

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

305 
by (blast intro: finite_UN_I finite_subset) 

306 

307 

15392  308 
text {* Sigma of finite sets *} 
12396  309 

310 
lemma finite_SigmaI [simp]: 

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

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

313 

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

316 
by (rule finite_SigmaI) 

317 

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

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

321 
apply (erule ssubst) 

14208  322 
apply (erule finite_SigmaI, auto) 
12396  323 
done 
324 

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

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

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

327 
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

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

329 
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

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

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

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

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

334 
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

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

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

337 
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

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

339 

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

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

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

342 
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

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

344 
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

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

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

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

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

349 
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

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

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

352 
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

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

354 

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

355 

12396  356 
instance unit :: finite 
357 
proof 

358 
have "finite {()}" by simp 

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

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

361 
qed 

362 

363 
instance * :: (finite, finite) finite 

364 
proof 

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

366 
proof (rule finite_Prod_UNIV) 

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

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

369 
qed 

370 
qed 

371 

372 

15392  373 
text {* The powerset of a finite set *} 
12396  374 

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

376 
proof 

377 
assume "finite (Pow A)" 

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

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

380 
next 

381 
assume "finite A" 

382 
thus "finite (Pow A)" 

383 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

384 
qed 

385 

15392  386 

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

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

389 

390 

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

393 
apply simp 

394 
apply (rule iffI) 

395 
apply (erule finite_imageD [unfolded inj_on_def]) 

396 
apply (simp split add: split_split) 

397 
apply (erule finite_imageI) 

14208  398 
apply (simp add: converse_def image_def, auto) 
12396  399 
apply (rule bexI) 
400 
prefer 2 apply assumption 

401 
apply simp 

402 
done 

403 

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

404 

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

12396  407 

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

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

410 
apply (induct set: Finites) 

411 
apply (auto simp add: Field_def Domain_insert Range_insert) 

412 
done 

413 

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

415 
apply clarify 

416 
apply (erule trancl_induct) 

417 
apply (auto simp add: Field_def) 

418 
done 

419 

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

421 
apply auto 

422 
prefer 2 

423 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

424 
apply (rule finite_SigmaI) 

425 
prefer 3 

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

426 
apply (blast intro: r_into_trancl' finite_subset) 
12396  427 
apply (auto simp add: finite_Field) 
428 
done 

429 

430 

15392  431 
subsection {* A fold functional for finite sets *} 
432 

433 
text {* The intended behaviour is 

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

437 
*} 

438 

439 
consts 

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

441 

15480  442 
inductive "foldSet f g z" 
15392  443 
intros 
15480  444 
emptyI [intro]: "({}, z) : foldSet f g z" 
15506  445 
insertI [intro]: 
446 
"\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk> 

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

15392  448 

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

451 
constdefs 

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

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

15498  455 
text{*A tempting alternative for the definiens is 
456 
@{term "if finite A then THE x. (A, x) : foldSet f g e else e"}. 

457 
It allows the removal of finiteness assumptions from the theorems 

458 
@{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. 

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

460 

461 

15392  462 
lemma Diff1_foldSet: 
15480  463 
"(A  {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" 
15392  464 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
465 

15480  466 
lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" 
15392  467 
by (induct set: foldSet) auto 
468 

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

472 

473 
subsubsection {* Commutative monoids *} 

15480  474 

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

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

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

479 

480 
locale ACe = ACf + 

481 
fixes e :: 'a 

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

483 

15480  484 
locale ACIf = ACf + 
485 
assumes idem: "x \<cdot> x = x" 

486 

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

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

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

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

492 
finally show ?thesis . 

493 
qed 

494 

495 
lemmas (in ACf) AC = assoc commute left_commute 

496 

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

498 
proof  

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

500 
thus ?thesis by (subst commute) 

501 
qed 

502 

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

503 
lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y" 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

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

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

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

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

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

509 

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

510 
lemmas (in ACIf) ACI = AC idem idem2 
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

511 

15765  512 
text{* Interpretation of locales: *} 
513 

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

515 
by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute) 

15402  516 

15765  517 
interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] 
518 
apply  

519 
apply (fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute) 

520 
apply (fastsimp intro: ACe_axioms.intro mult_assoc ab_semigroup_mult.mult_commute) 

521 
done 

522 

523 
(* 

15402  524 
lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" 
525 
by(fastsimp intro: ACf.intro add_assoc add_commute) 

526 

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

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

529 

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

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

532 

15765  533 
lemma ACe_mult: "ACe (op * ) (1::'a::comm_monoid_mult)" 
15402  534 
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult) 
15765  535 
*) 
15402  536 

15392  537 
subsubsection{*From @{term foldSet} to @{term fold}*} 
538 

15510  539 
lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})" 
540 
by (auto simp add: less_Suc_eq) 

541 

542 
lemma insert_image_inj_on_eq: 

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

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

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

546 
apply (auto simp add: image_less_Suc inj_on_def) 

547 
apply (blast intro: less_trans) 

548 
done 

549 

550 
lemma insert_inj_onE: 

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

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

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

554 
proof (cases n) 

555 
case 0 thus ?thesis using aA by auto 

556 
next 

557 
case (Suc m) 

558 
have nSuc: "n = Suc m" . 

559 
have mlessn: "m<n" by (simp add: nSuc) 

15532  560 
from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE) 
15520  561 
let ?hm = "swap k m h" 
562 
have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 

563 
by (simp add: inj_on_swap_iff inj_on) 

15510  564 
show ?thesis 
15520  565 
proof (intro exI conjI) 
566 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

570 
proof (rule insert_image_inj_on_eq) 

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

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

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

574 
using aA hkeq nSuc klessn 

575 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

576 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  577 
qed 
578 
qed 

579 
qed 

580 

15392  581 
lemma (in ACf) foldSet_determ_aux: 
15510  582 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
583 
(A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk> 

15392  584 
\<Longrightarrow> x' = x" 
15510  585 
proof (induct n rule: less_induct) 
586 
case (less n) 

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

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

589 
(A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" . 

590 
have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z" 

591 
and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" . 

592 
show ?case 

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

594 
assume "(A, x) = ({}, z)" 

595 
with Afoldx' show "x' = x" by blast 

15392  596 
next 
15510  597 
fix B b u 
598 
assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B" 

599 
and Bu: "(B,u) \<in> foldSet f g z" 

600 
hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto 

601 
show "x'=x" 

602 
proof (rule foldSet.cases [OF Afoldx']) 

603 
assume "(A, x') = ({}, z)" 

604 
with AbB show "x' = x" by blast 

15392  605 
next 
15510  606 
fix C c v 
607 
assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C" 

608 
and Cv: "(C,v) \<in> foldSet f g z" 

609 
hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto 

610 
from A AbB have Beq: "insert b B = h`{i. i<n}" by simp 

611 
from insert_inj_onE [OF Beq notinB injh] 

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

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

614 
and lessB: "mB < n" by auto 

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

616 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

619 
and lessC: "mC < n" by auto 

620 
show "x'=x" 

15392  621 
proof cases 
15510  622 
assume "b=c" 
623 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

625 
by auto 

15392  626 
next 
627 
assume diff: "b \<noteq> c" 

628 
let ?D = "B  {c}" 

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

15510  630 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  631 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  632 
with AbB have "finite ?D" by simp 
15480  633 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  634 
using finite_imp_foldSet by rules 
15506  635 
moreover have cinB: "c \<in> B" using B by auto 
15480  636 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  637 
by(rule Diff1_foldSet) 
15510  638 
hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
639 
moreover have "g b \<cdot> d = v" 

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

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

15392  642 
by fastsimp 
643 
qed 

15510  644 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  645 
qed 
646 
qed 

647 
qed 

648 
qed 

649 

650 

651 
lemma (in ACf) foldSet_determ: 

15510  652 
"(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x" 
653 
apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 

654 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  655 
done 
656 

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

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

661 

15480  662 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  663 
by (unfold fold_def) blast 
664 

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

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

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

670 
apply (fastsimp dest: foldSet_imp_finite) 

671 
apply (blast intro: foldSet_determ) 

672 
done 

673 

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

675 

676 
lemma (in ACf) fold_insert[simp]: 

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

680 
apply (rule the_equality) 

681 
apply (auto intro: finite_imp_foldSet 

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

683 
done 

684 

15535  685 
lemma (in ACf) fold_rec: 
686 
assumes fin: "finite A" and a: "a:A" 

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

688 
proof 

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

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

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

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

693 
finally show ?thesis . 

694 
qed 

695 

15392  696 

15480  697 
text{* A simplified version for idempotent functions: *} 
698 

15509  699 
lemma (in ACIf) fold_insert_idem: 
15480  700 
assumes finA: "finite A" 
15508  701 
shows "fold f g z (insert a A) = g a \<cdot> fold f g z A" 
15480  702 
proof cases 
703 
assume "a \<in> A" 

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

705 
by(blast dest: mk_disjoint_insert) 

706 
show ?thesis 

707 
proof  

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

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

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

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

714 
finally show ?thesis . 

715 
qed 

716 
next 

717 
assume "a \<notin> A" 

718 
with finA show ?thesis by simp 

719 
qed 

720 

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

15509  723 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  724 

15392  725 
subsubsection{*Lemmas about @{text fold}*} 
726 

727 
lemma (in ACf) fold_commute: 

15487  728 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
15392  729 
apply (induct set: Finites, simp) 
15487  730 
apply (simp add: left_commute [of x]) 
15392  731 
done 
732 

733 
lemma (in ACf) fold_nest_Un_Int: 

734 
"finite A ==> finite B 

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

738 
done 

739 

740 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  742 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  743 
by (simp add: fold_nest_Un_Int) 
744 

745 
lemma (in ACf) fold_reindex: 

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

15506  748 
using fin apply induct 
15392  749 
apply simp 
750 
apply simp 

751 
done 

752 

753 
lemma (in ACe) fold_Un_Int: 

754 
"finite A ==> finite B ==> 

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

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

757 
apply (induct set: Finites, simp) 

758 
apply (simp add: AC insert_absorb Int_insert_left) 

759 
done 

760 

761 
corollary (in ACe) fold_Un_disjoint: 

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

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

764 
by (simp add: fold_Un_Int) 

765 

766 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

773 
prefer 2 apply blast 

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

775 
prefer 2 apply blast 

776 
apply (simp add: fold_Un_disjoint) 

777 
done 

778 

15506  779 
text{*Fusion theorem, as described in 
780 
Graham Hutton's paper, 

781 
A Tutorial on the Universality and Expressiveness of Fold, 

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

783 
lemma (in ACf) fold_fusion: 

784 
includes ACf g 

785 
shows 

786 
"finite A ==> 

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

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

789 
by (induct set: Finites, simp_all) 

790 

15392  791 
lemma (in ACf) fold_cong: 
15480  792 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
793 
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  794 
apply simp 
795 
apply (erule finite_induct, simp) 

796 
apply (simp add: subset_insert_iff, clarify) 

797 
apply (subgoal_tac "finite C") 

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

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

800 
prefer 2 apply blast 

801 
apply (erule ssubst) 

802 
apply (drule spec) 

803 
apply (erule (1) notE impE) 

804 
apply (simp add: Ball_def del: insert_Diff_single) 

805 
done 

806 

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

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

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

810 
apply (subst Sigma_def) 

15506  811 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  812 
apply blast 
813 
apply (erule fold_cong) 

15506  814 
apply (subst fold_UN_disjoint, simp, simp) 
15392  815 
apply blast 
15506  816 
apply simp 
15392  817 
done 
818 

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

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

15506  821 
apply (erule finite_induct, simp) 
15392  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" 

15765  890 
by (simp add: setsum_def) 
15402  891 

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

892 
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

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

894 

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

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

899 
lemma setsum_reindex_id: 

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

901 
by (auto simp add: setsum_reindex) 

902 

903 
lemma setsum_cong: 

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

15765  905 
by(fastsimp simp: setsum_def intro: AC_add.fold_cong) 
15402  906 

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

909 

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

914 

15542  915 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  916 
apply (clarsimp simp: setsum_def) 
15765  917 
apply (erule finite_induct, auto) 
15402  918 
done 
919 

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

15402  922 

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

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

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

15765  926 
by(simp add: setsum_def AC_add.fold_Un_Int [symmetric]) 
15402  927 

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

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

930 
by (subst setsum_Un_Int [symmetric], auto) 

931 

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

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

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

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

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

15765  938 
by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong) 
15402  939 

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

940 
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

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

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

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

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

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

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

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

950 
done 
15402  951 

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

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

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

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

15765  957 
by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong) 
15402  958 

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

959 
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

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

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

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

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

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

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

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

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

969 
done 
15402  970 

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

15765  972 
by(simp add:setsum_def AC_add.fold_distrib) 
15402  973 

974 

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

976 

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

978 
apply (case_tac "finite A") 

979 
prefer 2 apply (simp add: setsum_def) 

980 
apply (erule rev_mp) 

981 
apply (erule finite_induct, auto) 

982 
done 

983 

984 
lemma setsum_eq_0_iff [simp]: 

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

986 
by (induct set: Finites) auto 

987 

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

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

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

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

992 

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

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

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

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

997 

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

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

1000 
apply (case_tac "finite A") 

1001 
prefer 2 apply (simp add: setsum_def) 

1002 
apply (erule finite_induct) 

1003 
apply (auto simp add: insert_Diff_if) 

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

1005 
done 

1006 

1007 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1011 

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

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

1013 
apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A  {a}). f x))"]) 
8ab8e425410b
added setsum_diff1' which holds in more general cases than setsum_diff1
obua
parents:
15543
diff
changeset

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

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

1016 

15402  1017 
(* By Jeremy Siek: *) 
1018 

1019 
lemma setsum_diff_nat: 

1020 
assumes finB: "finite B" 

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

1022 
using finB 

1023 
proof (induct) 

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

1025 
next 

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

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

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

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

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

1031 
by (simp add: setsum_diff1_nat) 

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

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

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

1035 
by simp 

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

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

1038 
by simp 

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

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

1041 
by simp 

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

1043 
qed 

1044 

1045 
lemma setsum_diff: 

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

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

1048 
proof  

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

1050 
show ?thesis using finiteB le 

1051 
proof (induct) 

1052 
case empty 

1053 
thus ?case by auto 

1054 
next 

1055 
case (insert x F) 

1056 
thus ?case using le finiteB 

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

1058 
qed 

1059 
qed 

1060 

1061 
lemma setsum_mono: 

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

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

1064 
proof (cases "finite K") 

1065 
case True 

1066 
thus ?thesis using le 

1067 
proof (induct) 

1068 
case empty 

1069 
thus ?case by simp 

1070 
next 

1071 
case insert 

1072 
thus ?case using add_mono 

1073 
by force 

1074 
qed 

1075 
next 

1076 
case False 

1077 
thus ?thesis 

1078 
by (simp add: setsum_def) 

1079 
qed 

1080 

15554  1081 
lemma setsum_strict_mono: 
1082 
fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" 

1083 
assumes fin_ne: "finite A" "A \<noteq> {}" 

1084 
shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A" 

1085 
using fin_ne 

1086 
proof (induct rule: finite_ne_induct) 

1087 
case singleton thus ?case by simp 

1088 
next 

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

1090 
qed 

1091 

15535  1092 
lemma setsum_negf: 
1093 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 

1094 
proof (cases "finite A") 

1095 
case True thus ?thesis by (induct set: Finites, auto) 

1096 
next 

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

1098 
qed 

15402  1099 

15535  1100 
lemma setsum_subtractf: 
1101 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 

15402  1102 
setsum f A  setsum g A" 
15535  1103 
proof (cases "finite A") 
1104 
case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) 

1105 
next 

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

1107 
qed 

15402  1108 

15535  1109 
lemma setsum_nonneg: 
1110 
assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" 

1111 
shows "0 \<le> setsum f A" 

1112 
proof (cases "finite A") 

1113 
case True thus ?thesis using nn 

15402  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 

15535  1118 
next 
1119 
case False thus ?thesis by (simp add: setsum_def) 

1120 
qed 

15402  1121 

15535  1122 
lemma setsum_nonpos: 
1123 
assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" 

1124 
shows "setsum f A \<le> 0" 

1125 
proof (cases "finite A") 

1126 
case True thus ?thesis using np 

15402  1127 
apply (induct set: Finites, auto) 
1128 
apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp) 

1129 
apply (blast intro: add_mono) 

1130 
done 

15535  1131 
next 
1132 
case False thus ?thesis by (simp add: setsum_def) 

1133 
qed 

15402  1134 

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

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

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

1139 
proof  

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

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

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

1143 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1145 
finally show ?thesis . 

1146 
qed 

15542  1147 

15402  1148 
lemma setsum_mult: 
1149 
fixes f :: "'a => ('b::semiring_0_cancel)" 

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

1151 
proof (cases "finite A") 

1152 
case True 

1153 
thus ?thesis 

1154 
proof (induct) 

1155 
case empty thus ?case by simp 

1156 
next 

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

1158 
qed 

1159 
next 

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

1161 
qed 

1162 

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

15535  1166 
proof (cases "finite A") 
1167 
case True 

1168 
thus ?thesis 

1169 
proof (induct) 

1170 
case empty thus ?case by simp 

1171 
next 

1172 
case (insert x A) 

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

1174 
qed 

15402  1175 
next 
15535  1176 
case False thus ?thesis by (simp add: setsum_def) 
15402  1177 
qed 
1178 

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

15535  1182 
proof (cases "finite A") 
1183 
case True 

1184 
thus ?thesis 

1185 
proof (induct) 

1186 
case empty thus ?case by simp 

1187 
next 

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

1189 
qed 

15402  1190 
next 
15535  1191 
case False thus ?thesis by (simp add: setsum_def) 
15402  1192 
qed 
1193 

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

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

1197 
proof (cases "finite A") 

1198 
case True 

1199 
thus ?thesis 

1200 
proof (induct) 

1201 
case empty thus ?case by simp 

1202 
next 

1203 
case (insert a A) 

1204 
hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp 

1205 
also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp 

1206 
also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp 

1207 
also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp 

1208 
finally show ?case . 

1209 
qed 

1210 
next 

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

1212 
qed 

1213 

15402  1214 

1215 
subsection {* Generalized product over a set *} 

1216 

1217 
constdefs 

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

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

1220 

1221 
syntax 

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

1223 

1224 
syntax (xsymbols) 

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

1226 
syntax (HTML output) 

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

1228 
translations 

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

1230 

1231 
syntax 

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

1233 

1234 
parse_translation {* 

1235 
let 

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

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

1238 
*} 

1239 
print_translation {* 

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

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

1242 
in 

1243 
[("setprod", setprod_tr')] 

1244 
end 

1245 
*} 

1246 

1247 

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

1249 
by (auto simp add: setprod_def) 

1250 

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

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

15765  1253 
by (simp add: setprod_def) 
15402  1254 

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

1255 
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

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

1257 

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

15765  1260 
by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD) 
15402  1261 

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

1263 
by (auto simp add: setprod_reindex) 

1264 

1265 
lemma setprod_cong: 

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

15765  1267 
by(fastsimp simp: setprod_def intro: AC_mult.fold_cong) 
15402  1268 

1269 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1271 
by (frule setprod_reindex, simp) 

1272 

1273 

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

1275 
apply (case_tac "finite A") 

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

1277 
done 

1278 

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

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

1281 
apply (erule ssubst, rule setprod_1) 

1282 
apply (rule setprod_cong, auto) 

1283 
done 

1284 

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

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

15765  1287 
by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric]) 
15402  1288 

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

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

1291 
by (subst setprod_Un_Int [symmetric], auto) 

1292 

1293 
lemma setprod_UN_disjoint: 

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

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

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

15765  1297 
by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong) 
15402  1298 

1299 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1307 
done 
15402  1308 

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

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

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

15765  1312 
by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong) 
15402  1313 

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

1314 
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

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

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

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

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

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

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

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

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

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

1324 
done 
15402  1325 

1326 
lemma setprod_timesf: 

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

1327 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 
15765  1328 
by(simp add:setprod_def AC_mult.fold_distrib) 
15402  1329 

1330 

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

1332 

1333 
lemma setprod_eq_1_iff [simp]: 

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

1335 
by (induct set: Finites) auto 

1336 

1337 
lemma setprod_zero: 

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

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

1340 
apply (erule disjE, auto) 

1341 
done 

1342 

1343 
lemma setprod_nonneg [rule_format]: 

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

1345 
apply (case_tac "finite A") 

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

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

1348 
apply (rule mult_mono, assumption+) 

1349 
apply (auto simp add: setprod_def) 

1350 
done 

1351 

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

1353 
> 0 < setprod f A" 

1354 
apply (case_tac "finite A") 

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

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

1357 
apply (rule mult_strict_mono, assumption+) 

1358 
apply (auto simp add: setprod_def) 

1359 
done 

1360 

1361 
lemma setprod_nonzero [rule_format]: 
