author  obua 
Mon, 28 Feb 2005 18:29:55 +0100  
changeset 15552  8ab8e425410b 
parent 15543  0024472afce7 
child 15554  03d4347b071d 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

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

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

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

7 
header {* Finite sets *} 

8 

15131  9 
theory Finite_Set 
15512
ed1fa4617f52
Extracted generic lattice stuff to new Lattice_Locales.thy
nipkow
parents:
15510
diff
changeset

10 
imports Divides Power Inductive Lattice_Locales 
15131  11 
begin 
12396  12 

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

15 
consts Finites :: "'a set set" 

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

18 
translations 

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

12396  20 

21 
inductive Finites 

22 
intros 

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

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

25 

26 
axclass finite \<subseteq> type 

27 
finite: "finite UNIV" 

28 

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

32 
proof  

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

34 
thus ?thesis by blast 

35 
qed 

12396  36 

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

38 
"finite F ==> 

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

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

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

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

46 
proof induct 

47 
show "P {}" . 

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

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

51 
assume "x \<in> F" 

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

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

54 
next 

55 
assume "x \<notin> F" 

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

57 
qed 

58 
qed 

59 
qed 

60 

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

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

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

65 
\<Longrightarrow> P F" 

66 
using fin 

67 
proof induct 

68 
case empty thus ?case by simp 

69 
next 

70 
case (insert x F) 

71 
show ?case 

72 
proof cases 

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

74 
next 

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

76 
qed 

77 
qed 

78 

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

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

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

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

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

88 
proof induct 

89 
show "P {}" . 

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

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

93 
proof (rule insert) 

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

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

96 
with P show "P F" . 

97 
qed 

98 
qed 

99 
qed 

100 

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

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

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

15392  106 
using fin 
107 
proof induct 

108 
case empty 

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

111 
qed 

15392  112 
next 
113 
case (insert a A) 

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

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

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

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

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

15392  120 
thus ?case by blast 
121 
qed 

122 

123 
lemma nat_seg_image_imp_finite: 

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

125 
proof (induct n) 

126 
case 0 thus ?case by simp 

127 
next 

128 
case (Suc n) 

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

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

131 
show ?case 

132 
proof cases 

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

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

135 
thus ?thesis using finB by simp 

136 
next 

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

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

139 
thus ?thesis using finB by simp 

140 
qed 

141 
qed 

142 

143 
lemma finite_conv_nat_seg_image: 

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

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

147 
subsubsection{* Finiteness and set theoretic constructions *} 

148 

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

151 
by (induct set: Finites) simp_all 

152 

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

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

155 
proof  

156 
assume "finite B" 

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

158 
proof induct 

159 
case empty 

160 
thus ?case by simp 

161 
next 

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

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

165 
proof cases 

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

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

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

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

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

171 
finally show ?thesis . 

172 
next 

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

174 
assume "x \<notin> A" 

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

176 
qed 

177 
qed 

178 
qed 

179 

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

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

182 

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

184 
 {* The converse obviously fails. *} 

185 
by (blast intro: finite_subset) 

186 

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

188 
apply (subst insert_is_Un) 

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

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

194 
by (induct rule:finite_induct) simp_all 

195 

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

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

199 
proof  

200 
assume "finite A" 

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

202 
have "P (A  A)" 

203 
proof  

204 
fix c b :: "'a set" 

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

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

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

208 
proof induct 

209 
case empty 

210 
from P1 show ?case by simp 

211 
next 

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

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

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

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

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

218 
qed 

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

220 
finally show ?case . 

221 
qed 

222 
next 

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

224 
qed 

225 
thus "P {}" by simp 

226 
qed 

227 

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

229 
by (rule Diff_subset [THEN finite_subset]) 

230 

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

232 
apply (subst Diff_insert) 

233 
apply (case_tac "a : A  B") 

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

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

238 

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

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

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

243 
by (induct set: Finites) simp_all 

244 

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

245 
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

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

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

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

249 

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

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

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

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

258 
fix B :: "'a set" 

259 
assume "finite B" 

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

261 
apply induct 

262 
apply simp 

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

264 
apply clarify 

265 
apply (simp (no_asm_use) add: inj_on_def) 

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

271 
done 

272 
qed (rule refl) 

273 

274 

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

277 
is included in a singleton. *} 

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

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

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

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

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

284 
is finite. *} 

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

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

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

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

290 

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

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

294 
by (induct set: Finites) simp_all 

295 

296 
text {* 

297 
Strengthen RHS to 

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

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

300 
We'd need to prove 

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

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

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

305 
by (blast intro: finite_UN_I finite_subset) 

306 

307 

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

310 
lemma finite_SigmaI [simp]: 

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

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

313 

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

316 
by (rule finite_SigmaI) 

317 

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

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

321 
apply (erule ssubst) 

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

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

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

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

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

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

329 
apply (drule_tac x="fst o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

334 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

337 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

339 

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

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

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

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

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

344 
apply (drule_tac x="snd o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

349 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

352 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

354 

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

355 

12396  356 
instance unit :: finite 
357 
proof 

358 
have "finite {()}" by simp 

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

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

361 
qed 

362 

363 
instance * :: (finite, finite) finite 

364 
proof 

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

366 
proof (rule finite_Prod_UNIV) 

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

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

369 
qed 

370 
qed 

371 

372 

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

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

376 
proof 

377 
assume "finite (Pow A)" 

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

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

380 
next 

381 
assume "finite A" 

382 
thus "finite (Pow A)" 

383 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

384 
qed 

385 

15392  386 

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

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

389 

390 

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

393 
apply simp 

394 
apply (rule iffI) 

395 
apply (erule finite_imageD [unfolded inj_on_def]) 

396 
apply (simp split add: split_split) 

397 
apply (erule finite_imageI) 

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

401 
apply simp 

402 
done 

403 

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

404 

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

12396  407 

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

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

410 
apply (induct set: Finites) 

411 
apply (auto simp add: Field_def Domain_insert Range_insert) 

412 
done 

413 

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

415 
apply clarify 

416 
apply (erule trancl_induct) 

417 
apply (auto simp add: Field_def) 

418 
done 

419 

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

421 
apply auto 

422 
prefer 2 

423 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

424 
apply (rule finite_SigmaI) 

425 
prefer 3 

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

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

429 

430 

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

433 
text {* The intended behaviour is 

15480  434 
@{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"} 
15392  435 
if @{text f} is associativecommutative. For an application of @{text fold} 
436 
se the definitions of sums and products over finite sets. 

437 
*} 

438 

439 
consts 

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

441 

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

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

15392  448 

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

451 
constdefs 

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

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

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

457 
It allows the removal of finiteness assumptions from the theorems 

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

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

460 

461 

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

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

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

472 

473 
subsubsection {* Commutative monoids *} 

15480  474 

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

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

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

479 

480 
locale ACe = ACf + 

481 
fixes e :: 'a 

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

483 

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

486 

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

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

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

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

492 
finally show ?thesis . 

493 
qed 

494 

495 
lemmas (in ACf) AC = assoc commute left_commute 

496 

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

498 
proof  

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

500 
thus ?thesis by (subst commute) 

501 
qed 

502 

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

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

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

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

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

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

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

509 

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

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

511 

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) 

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

554 
by (simp add: inj_on_swap_iff inj_on) 

15510  555 
show ?thesis 
15520  556 
proof (intro exI conjI) 
557 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

561 
proof (rule insert_image_inj_on_eq) 

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

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

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

565 
using aA hkeq nSuc klessn 

566 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

567 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  568 
qed 
569 
qed 

570 
qed 

571 

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

15392  575 
\<Longrightarrow> x' = x" 
15510  576 
proof (induct n rule: less_induct) 
577 
case (less n) 

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

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

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

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

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

583 
show ?case 

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

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

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

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

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

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

592 
show "x'=x" 

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

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

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

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

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

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

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

602 
from insert_inj_onE [OF Beq notinB injh] 

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

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

605 
and lessB: "mB < n" by auto 

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

607 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

610 
and lessC: "mC < n" by auto 

611 
show "x'=x" 

15392  612 
proof cases 
15510  613 
assume "b=c" 
614 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

616 
by auto 

15392  617 
next 
618 
assume diff: "b \<noteq> c" 

619 
let ?D = "B  {c}" 

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

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

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

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

15392  633 
by fastsimp 
634 
qed 

15510  635 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  636 
qed 
637 
qed 

638 
qed 

639 
qed 

640 

641 

642 
lemma (in ACf) foldSet_determ: 

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

645 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  646 
done 
647 

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

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

652 

15480  653 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  654 
by (unfold fold_def) blast 
655 

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

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

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

661 
apply (fastsimp dest: foldSet_imp_finite) 

662 
apply (blast intro: foldSet_determ) 

663 
done 

664 

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

666 

667 
lemma (in ACf) fold_insert[simp]: 

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

671 
apply (rule the_equality) 

672 
apply (auto intro: finite_imp_foldSet 

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

674 
done 

675 

15535  676 
lemma (in ACf) fold_rec: 
677 
assumes fin: "finite A" and a: "a:A" 

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

679 
proof 

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

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

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

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

684 
finally show ?thesis . 

685 
qed 

686 

15392  687 

15480  688 
text{* A simplified version for idempotent functions: *} 
689 

15509  690 
lemma (in ACIf) fold_insert_idem: 
15480  691 
assumes finA: "finite A" 
15508  692 
shows "fold f g z (insert a A) = g a \<cdot> fold f g z A" 
15480  693 
proof cases 
694 
assume "a \<in> A" 

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

696 
by(blast dest: mk_disjoint_insert) 

697 
show ?thesis 

698 
proof  

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

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

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

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

705 
finally show ?thesis . 

706 
qed 

707 
next 

708 
assume "a \<notin> A" 

709 
with finA show ?thesis by simp 

710 
qed 

711 

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

15509  714 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  715 

15392  716 
subsubsection{*Lemmas about @{text fold}*} 
717 

718 
lemma (in ACf) fold_commute: 

15487  719 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
15392  720 
apply (induct set: Finites, simp) 
15487  721 
apply (simp add: left_commute [of x]) 
15392  722 
done 
723 

724 
lemma (in ACf) fold_nest_Un_Int: 

725 
"finite A ==> finite B 

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

729 
done 

730 

731 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  733 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  734 
by (simp add: fold_nest_Un_Int) 
735 

736 
lemma (in ACf) fold_reindex: 

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

15506  739 
using fin apply induct 
15392  740 
apply simp 
741 
apply simp 

742 
done 

743 

744 
lemma (in ACe) fold_Un_Int: 

745 
"finite A ==> finite B ==> 

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

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

748 
apply (induct set: Finites, simp) 

749 
apply (simp add: AC insert_absorb Int_insert_left) 

750 
done 

751 

752 
corollary (in ACe) fold_Un_disjoint: 

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

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

755 
by (simp add: fold_Un_Int) 

756 

757 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

764 
prefer 2 apply blast 

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

766 
prefer 2 apply blast 

767 
apply (simp add: fold_Un_disjoint) 

768 
done 

769 

15506  770 
text{*Fusion theorem, as described in 
771 
Graham Hutton's paper, 

772 
A Tutorial on the Universality and Expressiveness of Fold, 

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

774 
lemma (in ACf) fold_fusion: 

775 
includes ACf g 

776 
shows 

777 
"finite A ==> 

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

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

780 
by (induct set: Finites, simp_all) 

781 

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

787 
apply (simp add: subset_insert_iff, clarify) 

788 
apply (subgoal_tac "finite C") 

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

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

791 
prefer 2 apply blast 

792 
apply (erule ssubst) 

793 
apply (drule spec) 

794 
apply (erule (1) notE impE) 

795 
apply (simp add: Ball_def del: insert_Diff_single) 

796 
done 

797 

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

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

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

801 
apply (subst Sigma_def) 

15506  802 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  803 
apply blast 
804 
apply (erule fold_cong) 

15506  805 
apply (subst fold_UN_disjoint, simp, simp) 
15392  806 
apply blast 
15506  807 
apply simp 
15392  808 
done 
809 

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

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

15506  812 
apply (erule finite_induct, simp) 
15392  813 
apply (simp add:AC) 
814 
done 

815 

816 

15402  817 
subsection {* Generalized summation over a set *} 
818 

819 
constdefs 

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

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

822 

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

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

825 

826 
syntax 

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

828 
syntax (xsymbols) 

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

830 
syntax (HTML output) 

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

832 

833 
translations  {* Beware of argument permutation! *} 

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

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

836 

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

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

839 

840 
syntax 

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

842 
syntax (xsymbols) 

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

844 
syntax (HTML output) 

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

846 

847 
translations 

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

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

850 

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

852 

853 
syntax 

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

855 

856 
parse_translation {* 

857 
let 

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

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

860 
*} 

861 

862 
print_translation {* 

863 
let 

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

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

866 
if x<>y then raise Match 

867 
else let val x' = Syntax.mark_bound x 

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

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

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

871 
in 

872 
[("setsum", setsum_tr')] 

873 
end 

874 
*} 

875 

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

877 
by (simp add: setsum_def) 

878 

879 
lemma setsum_insert [simp]: 

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

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

882 

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

883 
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

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

885 

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

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

889 

890 
lemma setsum_reindex_id: 

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

892 
by (auto simp add: setsum_reindex) 

893 

894 
lemma setsum_cong: 

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

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

897 

898 
lemma setsum_reindex_cong: 

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

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

901 
by (simp add: setsum_reindex cong: setsum_cong) 

902 

15542  903 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  904 
apply (clarsimp simp: setsum_def) 
905 
apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add]) 

906 
done 

907 

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

15402  910 

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

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

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

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

915 

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

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

918 
by (subst setsum_Un_Int [symmetric], auto) 

919 

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

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

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

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

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

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

927 

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

928 
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

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

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

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

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

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

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

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

938 
done 
15402  939 

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

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

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

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

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

946 

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

947 
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

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

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

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

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

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

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

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

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

957 
done 
15402  958 

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

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

961 

962 

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

964 

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

966 
apply (case_tac "finite A") 

967 
prefer 2 apply (simp add: setsum_def) 

968 
apply (erule rev_mp) 

969 
apply (erule finite_induct, auto) 

970 
done 

971 

972 
lemma setsum_eq_0_iff [simp]: 

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

974 
by (induct set: Finites) auto 

975 

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

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

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

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

980 

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

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

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

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

985 

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

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

988 
apply (case_tac "finite A") 

989 
prefer 2 apply (simp add: setsum_def) 

990 
apply (erule finite_induct) 

991 
apply (auto simp add: insert_Diff_if) 

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

993 
done 

994 

995 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

999 

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

1000 
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

1001 
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

1002 
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

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

1004 

15402  1005 
(* By Jeremy Siek: *) 
1006 

1007 
lemma setsum_diff_nat: 

1008 
assumes finB: "finite B" 

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

1010 
using finB 

1011 
proof (induct) 

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

1013 
next 

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

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

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

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

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

1019 
by (simp add: setsum_diff1_nat) 

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

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

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

1023 
by simp 

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

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

1026 
by simp 

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

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

1029 
by simp 

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

1031 
qed 

1032 

1033 
lemma setsum_diff: 

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

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

1036 
proof  

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

1038 
show ?thesis using finiteB le 

1039 
proof (induct) 

1040 
case empty 

1041 
thus ?case by auto 

1042 
next 

1043 
case (insert x F) 

1044 
thus ?case using le finiteB 

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

1046 
qed 

1047 
qed 

1048 

1049 
lemma setsum_mono: 

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

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

1052 
proof (cases "finite K") 

1053 
case True 

1054 
thus ?thesis using le 

1055 
proof (induct) 

1056 
case empty 

1057 
thus ?case by simp 

1058 
next 

1059 
case insert 

1060 
thus ?case using add_mono 

1061 
by force 

1062 
qed 

1063 
next 

1064 
case False 

1065 
thus ?thesis 

1066 
by (simp add: setsum_def) 

1067 
qed 

1068 

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

1071 
proof (cases "finite A") 

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

1073 
next 

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

1075 
qed 

15402  1076 

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

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

1082 
next 

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

1084 
qed 

15402  1085 

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

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

1089 
proof (cases "finite A") 

1090 
case True thus ?thesis using nn 

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

1093 
apply (blast intro: add_mono) 

1094 
done 

15535  1095 
next 
1096 
case False thus ?thesis by (simp add: setsum_def) 

1097 
qed 

15402  1098 

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

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

1102 
proof (cases "finite A") 

1103 
case True thus ?thesis using np 

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

1106 
apply (blast intro: add_mono) 

1107 
done 

15535  1108 
next 
1109 
case False thus ?thesis by (simp add: setsum_def) 

1110 
qed 

15402  1111 

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

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

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

1116 
proof  

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

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

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

1120 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1122 
finally show ?thesis . 

1123 
qed 

15542  1124 

15402  1125 
lemma setsum_mult: 
1126 
fixes f :: "'a => ('b::semiring_0_cancel)" 

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

1128 
proof (cases "finite A") 

1129 
case True 

1130 
thus ?thesis 

1131 
proof (induct) 

1132 
case empty thus ?case by simp 

1133 
next 

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

1135 
qed 

1136 
next 

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

1138 
qed 

1139 

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

15535  1143 
proof (cases "finite A") 
1144 
case True 

1145 
thus ?thesis 

1146 
proof (induct) 

1147 
case empty thus ?case by simp 

1148 
next 

1149 
case (insert x A) 

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

1151 
qed 

15402  1152 
next 
15535  1153 
case False thus ?thesis by (simp add: setsum_def) 
15402  1154 
qed 
1155 

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

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

1161 
thus ?thesis 

1162 
proof (induct) 

1163 
case empty thus ?case by simp 

1164 
next 

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

1166 
qed 

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

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

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

1174 
proof (cases "finite A") 

1175 
case True 

1176 
thus ?thesis 

1177 
proof (induct) 

1178 
case empty thus ?case by simp 

1179 
next 

1180 
case (insert a A) 

1181 
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 

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

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

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

1185 
finally show ?case . 

1186 
qed 

1187 
next 

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

1189 
qed 

1190 

15402  1191 

1192 
subsection {* Generalized product over a set *} 

1193 

1194 
constdefs 

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

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

1197 

1198 
syntax 

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

1200 

1201 
syntax (xsymbols) 

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

1203 
syntax (HTML output) 

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

1205 
translations 

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

1207 

1208 
syntax 

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

1210 

1211 
parse_translation {* 

1212 
let 

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

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

1215 
*} 

1216 
print_translation {* 

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

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

1219 
in 

1220 
[("setprod", setprod_tr')] 

1221 
end 

1222 
*} 

1223 

1224 

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

1226 
by (auto simp add: setprod_def) 

1227 

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

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

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

1231 

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

1232 
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

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

1234 

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

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

1238 

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

1240 
by (auto simp add: setprod_reindex) 

1241 

1242 
lemma setprod_cong: 

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

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

1245 

1246 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1248 
by (frule setprod_reindex, simp) 

1249 

1250 

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

1252 
apply (case_tac "finite A") 

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

1254 
done 

1255 

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

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

1258 
apply (erule ssubst, rule setprod_1) 

1259 
apply (rule setprod_cong, auto) 

1260 
done 

1261 

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

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

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

1265 

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

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

1268 
by (subst setprod_Un_Int [symmetric], auto) 

1269 

1270 
lemma setprod_UN_disjoint: 

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

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

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

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

1275 

1276 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1284 
done 
15402  1285 

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

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

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

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

1290 

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

1291 
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

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

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

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

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

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

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

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

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

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

1301 
done 
15402  1302 

1303 
lemma setprod_timesf: 

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

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

1307 

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

1309 

1310 
lemma setprod_eq_1_iff [simp]: 

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

1312 
by (induct set: Finites) auto 

1313 

1314 
lemma setprod_zero: 

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

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

1317 
apply (erule disjE, auto) 

1318 
done 

1319 

1320 
lemma setprod_nonneg [rule_format]: 

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

1322 
apply (case_tac "finite A") 

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

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

1325 
apply (rule mult_mono, assumption+) 

1326 
apply (auto simp add: setprod_def) 

1327 
done 

1328 

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

1330 
> 0 < setprod f A" 

1331 
apply (case_tac "finite A") 

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

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

1334 
apply (rule mult_strict_mono, assumption+) 

1335 
apply (auto simp add: setprod_def) 

1336 
done 

1337 

1338 
lemma setprod_nonzero [rule_format]: 

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

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

1341 
apply (erule finite_induct, auto) 

1342 
done 

1343 

1344 
lemma setprod_zero_eq: 

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

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

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

1348 
done 

1349 

1350 
lemma setprod_nonzero_field: 

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

1352 
apply (rule setprod_nonzero, auto) 

1353 
done 

1354 

1355 
lemma setprod_zero_eq_field: 

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

1357 
apply (rule setprod_zero_eq, auto) 

1358 
done 

1359 

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

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

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

1363 
apply (subst setprod_Un_Int [symmetric], auto) 

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

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

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

1367 
done 
