author  nipkow 
Fri, 08 Jul 2005 11:38:30 +0200  
changeset 16760  5c5f051aaaaa 
parent 16733  236dfafbeb63 
child 16775  c1b87ef4a1c3 
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 
16760  10 
imports 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 

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

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

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

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

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

898 

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

901 

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

906 

15542  907 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  908 
apply (clarsimp simp: setsum_def) 
15765  909 
apply (erule finite_induct, auto) 
15402  910 
done 
911 

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

15402  914 

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

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

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

15765  918 
by(simp add: setsum_def AC_add.fold_Un_Int [symmetric]) 
15402  919 

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

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

922 
by (subst setsum_Un_Int [symmetric], auto) 

923 

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

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

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

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

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

15765  930 
by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong) 
15402  931 

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

932 
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

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

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

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

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

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

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

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

942 
done 
15402  943 

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

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

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

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

15765  949 
by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong) 
15402  950 

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

951 
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

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

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

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

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

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

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

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

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

961 
done 
15402  962 

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

15765  964 
by(simp add:setsum_def AC_add.fold_distrib) 
15402  965 

966 

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

968 

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

970 
apply (case_tac "finite A") 

971 
prefer 2 apply (simp add: setsum_def) 

972 
apply (erule rev_mp) 

973 
apply (erule finite_induct, auto) 

974 
done 

975 

976 
lemma setsum_eq_0_iff [simp]: 

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

978 
by (induct set: Finites) auto 

979 

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

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

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

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

984 

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

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

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

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

989 

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

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

992 
apply (case_tac "finite A") 

993 
prefer 2 apply (simp add: setsum_def) 

994 
apply (erule finite_induct) 

995 
apply (auto simp add: insert_Diff_if) 

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

997 
done 

998 

999 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1003 

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

1004 
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

1005 
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

1006 
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

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

1008 

15402  1009 
(* By Jeremy Siek: *) 
1010 

1011 
lemma setsum_diff_nat: 

1012 
assumes finB: "finite B" 

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

1014 
using finB 

1015 
proof (induct) 

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

1017 
next 

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

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

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

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

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

1023 
by (simp add: setsum_diff1_nat) 

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

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

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

1027 
by simp 

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

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

1030 
by simp 

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

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

1033 
by simp 

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

1035 
qed 

1036 

1037 
lemma setsum_diff: 

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

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

1040 
proof  

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

1042 
show ?thesis using finiteB le 

1043 
proof (induct) 

1044 
case empty 

1045 
thus ?case by auto 

1046 
next 

1047 
case (insert x F) 

1048 
thus ?case using le finiteB 

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

1050 
qed 

1051 
qed 

1052 

1053 
lemma setsum_mono: 

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

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

1056 
proof (cases "finite K") 

1057 
case True 

1058 
thus ?thesis using le 

1059 
proof (induct) 

1060 
case empty 

1061 
thus ?case by simp 

1062 
next 

1063 
case insert 

1064 
thus ?case using add_mono 

1065 
by force 

1066 
qed 

1067 
next 

1068 
case False 

1069 
thus ?thesis 

1070 
by (simp add: setsum_def) 

1071 
qed 

1072 

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

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

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

1077 
using fin_ne 

1078 
proof (induct rule: finite_ne_induct) 

1079 
case singleton thus ?case by simp 

1080 
next 

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

1082 
qed 

1083 

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

1086 
proof (cases "finite A") 

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

1088 
next 

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

1090 
qed 

15402  1091 

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

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

1097 
next 

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

1099 
qed 

15402  1100 

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

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

1104 
proof (cases "finite A") 

1105 
case True thus ?thesis using nn 

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

1108 
apply (blast intro: add_mono) 

1109 
done 

15535  1110 
next 
1111 
case False thus ?thesis by (simp add: setsum_def) 

1112 
qed 

15402  1113 

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

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

1117 
proof (cases "finite A") 

1118 
case True thus ?thesis using np 

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

1121 
apply (blast intro: add_mono) 

1122 
done 

15535  1123 
next 
1124 
case False thus ?thesis by (simp add: setsum_def) 

1125 
qed 

15402  1126 

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

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

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

1131 
proof  

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

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

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

1135 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1137 
finally show ?thesis . 

1138 
qed 

15542  1139 

15837  1140 
(* FIXME: this is distributitivty, name as such! *) 
1141 

15402  1142 
lemma setsum_mult: 
1143 
fixes f :: "'a => ('b::semiring_0_cancel)" 

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

1145 
proof (cases "finite A") 

1146 
case True 

1147 
thus ?thesis 

1148 
proof (induct) 

1149 
case empty thus ?case by simp 

1150 
next 

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

1152 
qed 

1153 
next 

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

1155 
qed 

1156 

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

15535  1160 
proof (cases "finite A") 
1161 
case True 

1162 
thus ?thesis 

1163 
proof (induct) 

1164 
case empty thus ?case by simp 

1165 
next 

1166 
case (insert x A) 

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

1168 
qed 

15402  1169 
next 
15535  1170 
case False thus ?thesis by (simp add: setsum_def) 
15402  1171 
qed 
1172 

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

15535  1176 
proof (cases "finite A") 
1177 
case True 

1178 
thus ?thesis 

1179 
proof (induct) 

1180 
case empty thus ?case by simp 

1181 
next 

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

1183 
qed 

15402  1184 
next 
15535  1185 
case False thus ?thesis by (simp add: setsum_def) 
15402  1186 
qed 
1187 

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

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

1191 
proof (cases "finite A") 

1192 
case True 

1193 
thus ?thesis 

1194 
proof (induct) 

1195 
case empty thus ?case by simp 

1196 
next 

1197 
case (insert a A) 

1198 
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 

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

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

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

1202 
finally show ?case . 

1203 
qed 

1204 
next 

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

1206 
qed 

1207 

15402  1208 

1209 
subsection {* Generalized product over a set *} 

1210 

1211 
constdefs 

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

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

1214 

1215 
syntax 

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

1219 
syntax (HTML output) 

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

16550  1221 

1222 
translations  {* Beware of argument permutation! *} 

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

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

1225 

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

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

1228 

1229 
syntax 

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

1231 
syntax (xsymbols) 

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

1233 
syntax (HTML output) 

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

1235 

15402  1236 
translations 
16550  1237 
"PROD xP. t" => "setprod (%x. t) {x. P}" 
1238 
"\<Prod>xP. t" => "setprod (%x. t) {x. P}" 

1239 

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

15402  1241 

1242 
syntax 

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

1244 

1245 
parse_translation {* 

1246 
let 

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

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

1249 
*} 

1250 
print_translation {* 

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

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

1253 
in 

1254 
[("setprod", setprod_tr')] 

1255 
end 

1256 
*} 

1257 

1258 

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

1260 
by (auto simp add: setprod_def) 

1261 

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

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

15765  1264 
by (simp add: setprod_def) 
15402  1265 

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

1266 
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

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

1268 

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

15765  1271 
by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD) 
15402  1272 

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

1274 
by (auto simp add: setprod_reindex) 

1275 

1276 
lemma setprod_cong: 

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

15765  1278 
by(fastsimp simp: setprod_def intro: AC_mult.fold_cong) 
15402  1279 

16632
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

1280 
lemma strong_setprod_cong: 
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

1281 
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" 
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

1282 
by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong) 
ad2895beef79
Added strong_setsum_cong and strong_setprod_cong.
berghofe
parents:
16550
diff
changeset

1283 

15402  1284 
lemma setprod_reindex_cong: "inj_on f A ==> 
1285 
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" 

1286 
by (frule setprod_reindex, simp) 

1287 

1288 

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

1290 
apply (case_tac "finite A") 

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

1292 
done 

1293 

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

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

1296 
apply (erule ssubst, rule setprod_1) 

1297 
apply (rule setprod_cong, auto) 

1298 
done 

1299 

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

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

15765  1302 
by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric]) 
15402  1303 

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

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

1306 
by (subst setprod_Un_Int [symmetric], auto) 

1307 

1308 
lemma setprod_UN_disjoint: 

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

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

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

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

1314 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1322 
done 
15402  1323 

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

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

15765  1327 
by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong) 
15402  1328 

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

1329 
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

1330 
lemma setprod_cartesian_product: 
16550  1331 
"(\<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

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

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

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

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

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

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

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

1339 
done 
15402  1340 

1341 
lemma setprod_timesf: 

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

1342 
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" 
15765  1343 
by(simp add:setprod_def AC_mult.fold_distrib) 
15402  1344 

1345 

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

1347 

1348 
lemma setprod_eq_1_iff [simp]: 

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

1350 
by (induct set: Finites) auto 

1351 

1352 
lemma setprod_zero: 

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

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

1355 
apply (erule disjE, auto) 

1356 
done 

1357 

1358 
lemma setprod_nonneg [rule_format]: 

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