author  nipkow 
Thu, 23 Jun 2005 19:40:03 +0200  
changeset 16550  e14b89d6ef13 
parent 15837  7a567dcd4cda 
child 16632  ad2895beef79 
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  

15780  519 
apply (fast intro: ACf.intro mult_assoc mult_commute) 
520 
apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute) 

15765  521 
done 
522 

15402  523 

15392  524 
subsubsection{*From @{term foldSet} to @{term fold}*} 
525 

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

528 

529 
lemma insert_image_inj_on_eq: 

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

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

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

533 
apply (auto simp add: image_less_Suc inj_on_def) 

534 
apply (blast intro: less_trans) 

535 
done 

536 

537 
lemma insert_inj_onE: 

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

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

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

541 
proof (cases n) 

542 
case 0 thus ?thesis using aA by auto 

543 
next 

544 
case (Suc m) 

545 
have nSuc: "n = Suc m" . 

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

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

550 
by (simp add: inj_on_swap_iff inj_on) 

15510  551 
show ?thesis 
15520  552 
proof (intro exI conjI) 
553 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

557 
proof (rule insert_image_inj_on_eq) 

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

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

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

561 
using aA hkeq nSuc klessn 

562 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

563 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  564 
qed 
565 
qed 

566 
qed 

567 

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

15392  571 
\<Longrightarrow> x' = x" 
15510  572 
proof (induct n rule: less_induct) 
573 
case (less n) 

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

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

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

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

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

579 
show ?case 

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

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

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

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

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

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

588 
show "x'=x" 

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

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

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

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

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

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

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

598 
from insert_inj_onE [OF Beq notinB injh] 

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

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

601 
and lessB: "mB < n" by auto 

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

603 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

606 
and lessC: "mC < n" by auto 

607 
show "x'=x" 

15392  608 
proof cases 
15510  609 
assume "b=c" 
610 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

612 
by auto 

15392  613 
next 
614 
assume diff: "b \<noteq> c" 

615 
let ?D = "B  {c}" 

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

15510  617 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  618 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  619 
with AbB have "finite ?D" by simp 
15480  620 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  621 
using finite_imp_foldSet by rules 
15506  622 
moreover have cinB: "c \<in> B" using B by auto 
15480  623 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  624 
by(rule Diff1_foldSet) 
15510  625 
hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
626 
moreover have "g b \<cdot> d = v" 

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

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

15392  629 
by fastsimp 
630 
qed 

15510  631 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  632 
qed 
633 
qed 

634 
qed 

635 
qed 

636 

637 

638 
lemma (in ACf) foldSet_determ: 

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

641 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  642 
done 
643 

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

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

648 

15480  649 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  650 
by (unfold fold_def) blast 
651 

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

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

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

657 
apply (fastsimp dest: foldSet_imp_finite) 

658 
apply (blast intro: foldSet_determ) 

659 
done 

660 

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

662 

663 
lemma (in ACf) fold_insert[simp]: 

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

667 
apply (rule the_equality) 

668 
apply (auto intro: finite_imp_foldSet 

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

670 
done 

671 

15535  672 
lemma (in ACf) fold_rec: 
673 
assumes fin: "finite A" and a: "a:A" 

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

675 
proof 

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

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

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

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

680 
finally show ?thesis . 

681 
qed 

682 

15392  683 

15480  684 
text{* A simplified version for idempotent functions: *} 
685 

15509  686 
lemma (in ACIf) fold_insert_idem: 
15480  687 
assumes finA: "finite A" 
15508  688 
shows "fold f g z (insert a A) = g a \<cdot> fold f g z A" 
15480  689 
proof cases 
690 
assume "a \<in> A" 

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

692 
by(blast dest: mk_disjoint_insert) 

693 
show ?thesis 

694 
proof  

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

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

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

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

701 
finally show ?thesis . 

702 
qed 

703 
next 

704 
assume "a \<notin> A" 

705 
with finA show ?thesis by simp 

706 
qed 

707 

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

15509  710 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  711 

15392  712 
subsubsection{*Lemmas about @{text fold}*} 
713 

714 
lemma (in ACf) fold_commute: 

15487  715 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
15392  716 
apply (induct set: Finites, simp) 
15487  717 
apply (simp add: left_commute [of x]) 
15392  718 
done 
719 

720 
lemma (in ACf) fold_nest_Un_Int: 

721 
"finite A ==> finite B 

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

725 
done 

726 

727 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  729 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  730 
by (simp add: fold_nest_Un_Int) 
731 

732 
lemma (in ACf) fold_reindex: 

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

15506  735 
using fin apply induct 
15392  736 
apply simp 
737 
apply simp 

738 
done 

739 

740 
lemma (in ACe) fold_Un_Int: 

741 
"finite A ==> finite B ==> 

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

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

744 
apply (induct set: Finites, simp) 

745 
apply (simp add: AC insert_absorb Int_insert_left) 

746 
done 

747 

748 
corollary (in ACe) fold_Un_disjoint: 

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

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

751 
by (simp add: fold_Un_Int) 

752 

753 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

760 
prefer 2 apply blast 

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

762 
prefer 2 apply blast 

763 
apply (simp add: fold_Un_disjoint) 

764 
done 

765 

15506  766 
text{*Fusion theorem, as described in 
767 
Graham Hutton's paper, 

768 
A Tutorial on the Universality and Expressiveness of Fold, 

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

770 
lemma (in ACf) fold_fusion: 

771 
includes ACf g 

772 
shows 

773 
"finite A ==> 

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

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

776 
by (induct set: Finites, simp_all) 

777 

15392  778 
lemma (in ACf) fold_cong: 
15480  779 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
780 
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  781 
apply simp 
782 
apply (erule finite_induct, simp) 

783 
apply (simp add: subset_insert_iff, clarify) 

784 
apply (subgoal_tac "finite C") 

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

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

787 
prefer 2 apply blast 

788 
apply (erule ssubst) 

789 
apply (drule spec) 

790 
apply (erule (1) notE impE) 

791 
apply (simp add: Ball_def del: insert_Diff_single) 

792 
done 

793 

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

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

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

797 
apply (subst Sigma_def) 

15506  798 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  799 
apply blast 
800 
apply (erule fold_cong) 

15506  801 
apply (subst fold_UN_disjoint, simp, simp) 
15392  802 
apply blast 
15506  803 
apply simp 
15392  804 
done 
805 

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

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

15506  808 
apply (erule finite_induct, simp) 
15392  809 
apply (simp add:AC) 
810 
done 

811 

812 

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

815 
constdefs 

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

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

818 

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

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

821 

822 
syntax 

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

824 
syntax (xsymbols) 

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

826 
syntax (HTML output) 

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

828 

829 
translations  {* Beware of argument permutation! *} 

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

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

832 

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

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

835 

836 
syntax 

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

838 
syntax (xsymbols) 

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

840 
syntax (HTML output) 

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

842 

843 
translations 

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

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

846 

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

848 

849 
syntax 

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

851 

852 
parse_translation {* 

853 
let 

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

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

856 
*} 

857 

858 
print_translation {* 

859 
let 

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

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

862 
if x<>y then raise Match 

863 
else let val x' = Syntax.mark_bound x 

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

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

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

867 
in 

868 
[("setsum", setsum_tr')] 

869 
end 

870 
*} 

871 

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

873 
by (simp add: setsum_def) 

874 

875 
lemma setsum_insert [simp]: 

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

15765  877 
by (simp add: setsum_def) 
15402  878 

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

879 
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

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

881 

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

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

886 
lemma setsum_reindex_id: 

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

888 
by (auto simp add: setsum_reindex) 

889 

890 
lemma setsum_cong: 

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

15765  892 
by(fastsimp simp: setsum_def intro: AC_add.fold_cong) 
15402  893 

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

896 

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

901 

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

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

15402  909 

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

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

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

15765  913 
by(simp add: setsum_def AC_add.fold_Un_Int [symmetric]) 
15402  914 

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

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

917 
by (subst setsum_Un_Int [symmetric], auto) 

918 

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

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

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

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

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

15765  925 
by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong) 
15402  926 

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

927 
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

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

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

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

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

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

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

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

937 
done 
15402  938 

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

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

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

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

15765  944 
by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong) 
15402  945 

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

946 
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

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

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

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

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

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

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

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

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

956 
done 
15402  957 

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

15765  959 
by(simp add:setsum_def AC_add.fold_distrib) 
15402  960 

961 

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

963 

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

965 
apply (case_tac "finite A") 

966 
prefer 2 apply (simp add: setsum_def) 

967 
apply (erule rev_mp) 

968 
apply (erule finite_induct, auto) 

969 
done 

970 

971 
lemma setsum_eq_0_iff [simp]: 

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

973 
by (induct set: Finites) auto 

974 

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

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

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

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

979 

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

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

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

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

984 

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

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

987 
apply (case_tac "finite A") 

988 
prefer 2 apply (simp add: setsum_def) 

989 
apply (erule finite_induct) 

990 
apply (auto simp add: insert_Diff_if) 

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

992 
done 

993 

994 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

998 

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

999 
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

1000 
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

1001 
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

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

1003 

15402  1004 
(* By Jeremy Siek: *) 
1005 

1006 
lemma setsum_diff_nat: 

1007 
assumes finB: "finite B" 

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

1009 
using finB 

1010 
proof (induct) 

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

1012 
next 

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

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

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

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

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

1018 
by (simp add: setsum_diff1_nat) 

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

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

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

1022 
by simp 

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

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

1025 
by simp 

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

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

1028 
by simp 

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

1030 
qed 

1031 

1032 
lemma setsum_diff: 

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

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

1035 
proof  

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

1037 
show ?thesis using finiteB le 

1038 
proof (induct) 

1039 
case empty 

1040 
thus ?case by auto 

1041 
next 

1042 
case (insert x F) 

1043 
thus ?case using le finiteB 

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

1045 
qed 

1046 
qed 

1047 

1048 
lemma setsum_mono: 

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

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

1051 
proof (cases "finite K") 

1052 
case True 

1053 
thus ?thesis using le 

1054 
proof (induct) 

1055 
case empty 

1056 
thus ?case by simp 

1057 
next 

1058 
case insert 

1059 
thus ?case using add_mono 

1060 
by force 

1061 
qed 

1062 
next 

1063 
case False 

1064 
thus ?thesis 

1065 
by (simp add: setsum_def) 

1066 
qed 

1067 

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

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

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

1072 
using fin_ne 

1073 
proof (induct rule: finite_ne_induct) 

1074 
case singleton thus ?case by simp 

1075 
next 

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

1077 
qed 

1078 

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

1081 
proof (cases "finite A") 

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

1083 
next 

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

1085 
qed 

15402  1086 

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

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

1092 
next 

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

1094 
qed 

15402  1095 

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

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

1099 
proof (cases "finite A") 

1100 
case True thus ?thesis using nn 

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

1103 
apply (blast intro: add_mono) 

1104 
done 

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

1107 
qed 

15402  1108 

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

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

1112 
proof (cases "finite A") 

1113 
case True thus ?thesis using np 

15402  1114 
apply (induct set: Finites, auto) 
1115 
apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", 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 

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

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

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

1126 
proof  

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

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

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

1130 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1132 
finally show ?thesis . 

1133 
qed 

15542  1134 

15837  1135 
(* FIXME: this is distributitivty, name as such! *) 
1136 

15402  1137 
lemma setsum_mult: 
1138 
fixes f :: "'a => ('b::semiring_0_cancel)" 

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

1140 
proof (cases "finite A") 

1141 
case True 

1142 
thus ?thesis 

1143 
proof (induct) 

1144 
case empty thus ?case by simp 

1145 
next 

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

1147 
qed 

1148 
next 

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

1150 
qed 

1151 

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

15535  1155 
proof (cases "finite A") 
1156 
case True 

1157 
thus ?thesis 

1158 
proof (induct) 

1159 
case empty thus ?case by simp 

1160 
next 

1161 
case (insert x A) 

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

1163 
qed 

15402  1164 
next 
15535  1165 
case False thus ?thesis by (simp add: setsum_def) 
15402  1166 
qed 
1167 

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

15535  1171 
proof (cases "finite A") 
1172 
case True 

1173 
thus ?thesis 

1174 
proof (induct) 

1175 
case empty thus ?case by simp 

1176 
next 

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

1178 
qed 

15402  1179 
next 
15535  1180 
case False thus ?thesis by (simp add: setsum_def) 
15402  1181 
qed 
1182 

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

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

1186 
proof (cases "finite A") 

1187 
case True 

1188 
thus ?thesis 

1189 
proof (induct) 

1190 
case empty thus ?case by simp 

1191 
next 

1192 
case (insert a A) 

1193 
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 

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

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

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

1197 
finally show ?case . 

1198 
qed 

1199 
next 

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

1201 
qed 

1202 

15402  1203 

1204 
subsection {* Generalized product over a set *} 

1205 

1206 
constdefs 

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

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

1209 

1210 
syntax 

16550  1211 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) 
15402  1212 
syntax (xsymbols) 
1213 
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) 

1214 
syntax (HTML output) 

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

16550  1216 

1217 
translations  {* Beware of argument permutation! *} 

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

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

1220 

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

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

1223 

1224 
syntax 

1225 
"_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ / _./ _)" [0,0,10] 10) 

1226 
syntax (xsymbols) 

1227 
"_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 

1228 
syntax (HTML output) 

1229 
"_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_  (_)./ _)" [0,0,10] 10) 

1230 

15402  1231 
translations 
16550  1232 
"PROD xP. t" => "setprod (%x. t) {x. P}" 
1233 
"\<Prod>xP. t" => "setprod (%x. t) {x. P}" 

1234 

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

15402  1236 

1237 
syntax 

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

1239 

1240 
parse_translation {* 

1241 
let 

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

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

1244 
*} 

1245 
print_translation {* 

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

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

1248 
in 

1249 
[("setprod", setprod_tr')] 

1250 
end 

1251 
*} 

1252 

1253 

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

1255 
by (auto simp add: setprod_def) 

1256 

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

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

15765  1259 
by (simp add: setprod_def) 
15402  1260 

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

1261 
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

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

1263 

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

15765  1266 
by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD) 
15402  1267 

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

1269 
by (auto simp add: setprod_reindex) 

1270 

1271 
lemma setprod_cong: 

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

15765  1273 
by(fastsimp simp: setprod_def intro: AC_mult.fold_cong) 
15402  1274 

1275 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1277 
by (frule setprod_reindex, simp) 

1278 

1279 

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

1281 
apply (case_tac "finite A") 

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

1283 
done 

1284 

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

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

1287 
apply (erule ssubst, rule setprod_1) 

1288 
apply (rule setprod_cong, auto) 

1289 
done 

1290 

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

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

15765  1293 
by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric]) 
15402  1294 

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

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

1297 
by (subst setprod_Un_Int [symmetric], auto) 

1298 

1299 
lemma setprod_UN_disjoint: 

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

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

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

15765  1303 
by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong) 
15402  1304 

1305 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1313 
done 
15402  1314 

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

16550  1316 
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) = 
1317 
(\<Prod>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))" 

15765  1318 
by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong) 
15402  1319 

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

1320 
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

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

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

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

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

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

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

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

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

1330 
done 
15402  1331 

1332 
lemma setprod_timesf: 

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

1333 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 
15765  1334 
by(simp add:setprod_def AC_mult.fold_distrib) 
15402  1335 

1336 

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

1338 

1339 
lemma setprod_eq_1_iff [simp]: 

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

1341 
by (induct set: Finites) auto 

1342 

1343 
lemma setprod_zero: 

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

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

1346 
apply (erule disjE, auto) 

1347 
done 

1348 

1349 
lemma setprod_nonneg [rule_format]: 

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

1351 
apply (case_tac "finite A") 

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

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

1354 
apply (rule mult_mono, assumption+) 

1355 
apply (auto simp add: setprod_def) 

1356 
done 

1357 

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

1359 
> 0 < setprod f A" 

1360 
apply (case_tac "finite A") 

97204f3b4705
REorganized Finite_Set
nipk&# 