author  paulson 
Wed, 09 Feb 2005 18:32:28 +0100  
changeset 15510  9de204d7b699 
parent 15509  c54970704285 
child 15512  ed1fa4617f52 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

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

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

4 
Additions by Jeremy Avigad in Feb 2004 
12396  5 
*) 
6 

7 
header {* Finite sets *} 

8 

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

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

15 
consts Finites :: "'a set set" 

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

18 
translations 

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

12396  20 

21 
inductive Finites 

22 
intros 

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

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

25 

26 
axclass finite \<subseteq> type 

27 
finite: "finite UNIV" 

28 

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

32 
proof  

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

34 
thus ?thesis by blast 

35 
qed 

12396  36 

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

38 
"finite F ==> 

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

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

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

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

46 
proof induct 

47 
show "P {}" . 

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

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

51 
assume "x \<in> F" 

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

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

54 
next 

55 
assume "x \<notin> F" 

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

57 
qed 

58 
qed 

59 
qed 

60 

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 

15402  512 
text{* Instantiation of locales: *} 
513 

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

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

516 

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

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

519 

520 

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

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

523 

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

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

526 

527 

15392  528 
subsubsection{*From @{term foldSet} to @{term fold}*} 
529 

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

532 

533 
lemma insert_image_inj_on_eq: 

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

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

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

537 
apply (auto simp add: image_less_Suc inj_on_def) 

538 
apply (blast intro: less_trans) 

539 
done 

540 

541 
lemma insert_inj_onE: 

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

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

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

545 
proof (cases n) 

546 
case 0 thus ?thesis using aA by auto 

547 
next 

548 
case (Suc m) 

549 
have nSuc: "n = Suc m" . 

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

551 
have "a \<in> h ` {i. i < n}" using aA by blast 

552 
then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast 

553 
show ?thesis 

554 
proof cases 

555 
assume eq: "k=m" 

556 
show ?thesis 

557 
proof (intro exI conjI) 

558 
show "inj_on h {i::nat. i<m}" using inj_on 

559 
by (simp add: nSuc inj_on_def) 

560 
show "m<n" by (rule mlessn) 

561 
show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on 

562 
by (rules intro: insert_image_inj_on_eq) 

15479  563 
qed 
564 
next 

15510  565 
assume diff: "k~=m" 
566 
hence klessm: "k<m" using nSuc klessn by arith 

567 
have hdiff: "h k ~= h m" using diff inj_on klessn mlessn 

568 
by (auto simp add: inj_on_def) 

569 
let ?hm = "swap k m h" 

570 
have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn 

571 
by (simp add: inj_on_swap_iff inj_on) 

572 
hence inj_onhm_m: "inj_on ?hm {i. i < m}" 

573 
by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on) 

574 
show ?thesis 

575 
proof (intro exI conjI) 

576 
show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m) 

577 
show "m<n" by (simp add: nSuc) 

578 
show "A = ?hm ` {i. i < m}" 

579 
proof (rule insert_image_inj_on_eq) 

580 
show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n 

581 
by (simp add: nSuc) 

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

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

584 
using aA hkeq diff hdiff nSuc 

585 
by (auto simp add: swap_def image_less_Suc fun_upd_image klessm 

586 
inj_on_image_set_diff [OF inj_on]) 

15479  587 
qed 
588 
qed 

589 
qed 

590 
qed 

591 

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

15392  595 
\<Longrightarrow> x' = x" 
15510  596 
proof (induct n rule: less_induct) 
597 
case (less n) 

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

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

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

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

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

603 
show ?case 

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

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

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

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

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

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

612 
show "x'=x" 

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

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

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

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

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

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

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

622 
from insert_inj_onE [OF Beq notinB injh] 

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

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

625 
and lessB: "mB < n" by auto 

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

627 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

630 
and lessC: "mC < n" by auto 

631 
show "x'=x" 

15392  632 
proof cases 
15510  633 
assume "b=c" 
634 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

636 
by auto 

15392  637 
next 
638 
assume diff: "b \<noteq> c" 

639 
let ?D = "B  {c}" 

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

15510  641 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  642 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  643 
with AbB have "finite ?D" by simp 
15480  644 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  645 
using finite_imp_foldSet by rules 
15506  646 
moreover have cinB: "c \<in> B" using B by auto 
15480  647 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  648 
by(rule Diff1_foldSet) 
15510  649 
hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
650 
moreover have "g b \<cdot> d = v" 

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

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

15392  653 
by fastsimp 
654 
qed 

15510  655 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  656 
qed 
657 
qed 

658 
qed 

659 
qed 

660 

661 

662 
lemma (in ACf) foldSet_determ: 

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

665 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  666 
done 
667 

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

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

672 

15480  673 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  674 
by (unfold fold_def) blast 
675 

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

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

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

681 
apply (fastsimp dest: foldSet_imp_finite) 

682 
apply (blast intro: foldSet_determ) 

683 
done 

684 

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

686 

687 
lemma (in ACf) fold_insert[simp]: 

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

691 
apply (rule the_equality) 

692 
apply (auto intro: finite_imp_foldSet 

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

694 
done 

695 

696 

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

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

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

705 
by(blast dest: mk_disjoint_insert) 

706 
show ?thesis 

707 
proof  

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

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

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

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

714 
finally show ?thesis . 

715 
qed 

716 
next 

717 
assume "a \<notin> A" 

718 
with finA show ?thesis by simp 

719 
qed 

720 

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

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

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

727 
lemma (in ACf) fold_commute: 

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

733 
lemma (in ACf) fold_nest_Un_Int: 

734 
"finite A ==> finite B 

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

738 
done 

739 

740 
lemma (in ACf) fold_nest_Un_disjoint: 

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

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

745 
lemma (in ACf) fold_reindex: 

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

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

751 
done 

752 

753 
lemma (in ACe) fold_Un_Int: 

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

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

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

757 
apply (induct set: Finites, simp) 

758 
apply (simp add: AC insert_absorb Int_insert_left) 

759 
done 

760 

761 
corollary (in ACe) fold_Un_disjoint: 

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

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

764 
by (simp add: fold_Un_Int) 

765 

766 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

773 
prefer 2 apply blast 

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

775 
prefer 2 apply blast 

776 
apply (simp add: fold_Un_disjoint) 

777 
done 

778 

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

781 
A Tutorial on the Universality and Expressiveness of Fold, 

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

783 
lemma (in ACf) fold_fusion: 

784 
includes ACf g 

785 
shows 

786 
"finite A ==> 

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

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

789 
by (induct set: Finites, simp_all) 

790 

15392  791 
lemma (in ACf) fold_cong: 
15480  792 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
793 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold f g z C = fold f h z C") 

15392  794 
apply simp 
795 
apply (erule finite_induct, simp) 

796 
apply (simp add: subset_insert_iff, clarify) 

797 
apply (subgoal_tac "finite C") 

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

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

800 
prefer 2 apply blast 

801 
apply (erule ssubst) 

802 
apply (drule spec) 

803 
apply (erule (1) notE impE) 

804 
apply (simp add: Ball_def del: insert_Diff_single) 

805 
done 

806 

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

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

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

810 
apply (subst Sigma_def) 

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

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

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

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

15506  821 
apply (erule finite_induct, simp) 
15392  822 
apply (simp add:AC) 
823 
done 

824 

825 

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

828 
constdefs 

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

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

831 

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

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

834 

835 
syntax 

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

837 
syntax (xsymbols) 

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

839 
syntax (HTML output) 

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

841 

842 
translations  {* Beware of argument permutation! *} 

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

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

845 

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

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

848 

849 
syntax 

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

851 
syntax (xsymbols) 

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

853 
syntax (HTML output) 

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

855 

856 
translations 

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

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

859 

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

861 

862 
syntax 

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

864 

865 
parse_translation {* 

866 
let 

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

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

869 
*} 

870 

871 
print_translation {* 

872 
let 

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

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

875 
if x<>y then raise Match 

876 
else let val x' = Syntax.mark_bound x 

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

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

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

880 
in 

881 
[("setsum", setsum_tr')] 

882 
end 

883 
*} 

884 

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

886 
by (simp add: setsum_def) 

887 

888 
lemma setsum_insert [simp]: 

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

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

891 

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

892 
lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0" 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

894 

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

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

898 

899 
lemma setsum_reindex_id: 

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

901 
by (auto simp add: setsum_reindex) 

902 

903 
lemma setsum_cong: 

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

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

906 

907 
lemma setsum_reindex_cong: 

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

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

910 
by (simp add: setsum_reindex cong: setsum_cong) 

911 

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

913 
apply (clarsimp simp: setsum_def) 

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

915 
done 

916 

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

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

919 
apply (erule ssubst, rule setsum_0) 

920 
apply (rule setsum_cong, auto) 

921 
done 

922 

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

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

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

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

927 

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

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

930 
by (subst setsum_Un_Int [symmetric], auto) 

931 

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

932 
(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

939 

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

940 
text{*No need to assume that @{term C} is finite. If infinite, the rhs is 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

944 
(ALL A:C. ALL B:C. A \<noteq> B > A Int B = {}) ] 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

950 
done 
15402  951 

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

952 
(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

958 

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

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

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

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

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

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

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

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

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

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

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

969 
done 
15402  970 

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

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

973 

974 

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

976 

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

978 
apply (case_tac "finite A") 

979 
prefer 2 apply (simp add: setsum_def) 

980 
apply (erule rev_mp) 

981 
apply (erule finite_induct, auto) 

982 
done 

983 

984 
lemma setsum_eq_0_iff [simp]: 

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

986 
by (induct set: Finites) auto 

987 

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

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

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

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

992 

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

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

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

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

997 

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

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

1000 
apply (case_tac "finite A") 

1001 
prefer 2 apply (simp add: setsum_def) 

1002 
apply (erule finite_induct) 

1003 
apply (auto simp add: insert_Diff_if) 

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

1005 
done 

1006 

1007 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1011 

1012 
(* By Jeremy Siek: *) 

1013 

1014 
lemma setsum_diff_nat: 

1015 
assumes finB: "finite B" 

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

1017 
using finB 

1018 
proof (induct) 

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

1020 
next 

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

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

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

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

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

1026 
by (simp add: setsum_diff1_nat) 

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

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

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

1030 
by simp 

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

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

1033 
by simp 

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

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

1036 
by simp 

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

1038 
qed 

1039 

1040 
lemma setsum_diff: 

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

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

1043 
proof  

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

1045 
show ?thesis using finiteB le 

1046 
proof (induct) 

1047 
case empty 

1048 
thus ?case by auto 

1049 
next 

1050 
case (insert x F) 

1051 
thus ?case using le finiteB 

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

1053 
qed 

1054 
qed 

1055 

1056 
lemma setsum_mono: 

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

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

1059 
proof (cases "finite K") 

1060 
case True 

1061 
thus ?thesis using le 

1062 
proof (induct) 

1063 
case empty 

1064 
thus ?case by simp 

1065 
next 

1066 
case insert 

1067 
thus ?case using add_mono 

1068 
by force 

1069 
qed 

1070 
next 

1071 
case False 

1072 
thus ?thesis 

1073 
by (simp add: setsum_def) 

1074 
qed 

1075 

1076 
lemma setsum_mono2_nat: 

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

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

1079 
proof  

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

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

1082 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1084 
finally show ?thesis . 

1085 
qed 

1086 

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

1088 
 setsum f A" 

1089 
by (induct set: Finites, auto) 

1090 

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

1092 
setsum f A  setsum g A" 

1093 
by (simp add: diff_minus setsum_addf setsum_negf) 

1094 

1095 
lemma setsum_nonneg: "[ finite A; 

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

1097 
0 \<le> setsum f A"; 

1098 
apply (induct set: Finites, auto) 

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

1100 
apply (blast intro: add_mono) 

1101 
done 

1102 

1103 
lemma setsum_nonpos: "[ finite A; 

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

1105 
setsum f A \<le> 0"; 

1106 
apply (induct set: Finites, auto) 

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

1108 
apply (blast intro: add_mono) 

1109 
done 

1110 

1111 
lemma setsum_mult: 

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

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

1114 
proof (cases "finite A") 

1115 
case True 

1116 
thus ?thesis 

1117 
proof (induct) 

1118 
case empty thus ?case by simp 

1119 
next 

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

1121 
qed 

1122 
next 

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

1124 
qed 

1125 

1126 
lemma setsum_abs: 

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

1128 
assumes fin: "finite A" 

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

1130 
using fin 

1131 
proof (induct) 

1132 
case empty thus ?case by simp 

1133 
next 

1134 
case (insert x A) 

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

1136 
qed 

1137 

1138 
lemma setsum_abs_ge_zero: 

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

1140 
assumes fin: "finite A" 

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

1142 
using fin 

1143 
proof (induct) 

1144 
case empty thus ?case by simp 

1145 
next 

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

1147 
qed 

1148 

1149 

1150 
subsection {* Generalized product over a set *} 

1151 

1152 
constdefs 

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

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

1155 

1156 
syntax 

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

1158 

1159 
syntax (xsymbols) 

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

1161 
syntax (HTML output) 

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

1163 
translations 

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

1165 

1166 
syntax 

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

1168 

1169 
parse_translation {* 

1170 
let 

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

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

1173 
*} 

1174 
print_translation {* 

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

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

1177 
in 

1178 
[("setprod", setprod_tr')] 

1179 
end 

1180 
*} 

1181 

1182 

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

1184 
by (auto simp add: setprod_def) 

1185 

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

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

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

1189 

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

1190 
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

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

1192 

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

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

1196 

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

1198 
by (auto simp add: setprod_reindex) 

1199 

1200 
lemma setprod_cong: 

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

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

1203 

1204 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1206 
by (frule setprod_reindex, simp) 

1207 

1208 

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

1210 
apply (case_tac "finite A") 

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

1212 
done 

1213 

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

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

1216 
apply (erule ssubst, rule setprod_1) 

1217 
apply (rule setprod_cong, auto) 

1218 
done 

1219 

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

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

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

1223 

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

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

1226 
by (subst setprod_Un_Int [symmetric], auto) 

1227 

1228 
lemma setprod_UN_disjoint: 

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

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

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

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

1233 

1234 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1242 
done 
15402  1243 

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

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

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

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

1248 

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

1249 
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

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

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

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

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

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

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

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

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

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

1259 
done 
15402  1260 

1261 
lemma setprod_timesf: 

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

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

1265 

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

1267 

1268 
lemma setprod_eq_1_iff [simp]: 

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

1270 
by (induct set: Finites) auto 

1271 

1272 
lemma setprod_zero: 

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

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

1275 
apply (erule disjE, auto) 

1276 
done 

1277 

1278 
lemma setprod_nonneg [rule_format]: 

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

1280 
apply (case_tac "finite A") 

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

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

1283 
apply (rule mult_mono, assumption+) 

1284 
apply (auto simp add: setprod_def) 

1285 
done 

1286 

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

1288 
> 0 < setprod f A" 

1289 
apply (case_tac "finite A") 

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

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

1292 
apply (rule mult_strict_mono, assumption+) 

1293 
apply (auto simp add: setprod_def) 

1294 
done 

1295 

1296 
lemma setprod_nonzero [rule_format]: 

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

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

1299 
apply (erule finite_induct, auto) 

1300 
done 

1301 

1302 
lemma setprod_zero_eq: 

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

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

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

1306 
done 

1307 

1308 
lemma setprod_nonzero_field: 

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

1310 
apply (rule setprod_nonzero, auto) 

1311 
done 

1312 

1313 
lemma setprod_zero_eq_field: 

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

1315 
apply (rule setprod_zero_eq, auto) 

1316 
done 

1317 

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

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

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

1321 
apply (subst setprod_Un_Int [symmetric], auto) 

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

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

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

1325 
done 

1326 

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

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

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

1330 
apply (erule finite_induct) 

1331 
apply (auto simp add: insert_Diff_if) 

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

1333 
apply (erule ssubst) 

1334 
apply (subst times_divide_eq_right [THEN sym]) 

1335 
apply (auto simp add: mult_ac times_divide_eq_right divide_self) 

1336 
done 

1337 

1338 
lemma setprod_inversef: "finite A ==> 

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

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

1341 
apply (erule finite_induct) 

1342 
apply (simp, simp) 

1343 
done 

1344 

1345 
lemma setprod_dividef: 

1346 
"[finite A; 

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

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

1349 
apply (subgoal_tac 

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

1351 
apply (erule ssubst) 

1352 
apply (subst divide_inverse) 

1353 
apply (subst setprod_timesf) 

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

1355 
apply (rule setprod_cong, rule refl) 

1356 
apply (subst divide_inverse, auto) 

1357 
done 

1358 

12396  1359 
subsection {* Finite cardinality *} 
1360 

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

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

12396  1364 
*} 
1365 

1366 
constdefs 

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

15402  1368 
"card A == setsum (%x. 1::nat) A" 
12396  1369 

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

15402  1371 
by (simp add: card_def) 
1372 

15409
