author  paulson 
Fri, 04 Feb 2005 18:34:34 +0100  
changeset 15498  3988e90613d4 
parent 15497  53bca254719a 
child 15500  dd4ab096f082 
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 

103 
lemma finite_imp_nat_seg_image: 

104 
assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}" 

105 
using fin 

106 
proof induct 

107 
case empty 

108 
show ?case 

109 
proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed 

110 
next 

111 
case (insert a A) 

112 
from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast 

113 
hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}" 

114 
by (auto simp add:image_def Ball_def) 

115 
thus ?case by blast 

116 
qed 

117 

118 
lemma nat_seg_image_imp_finite: 

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

120 
proof (induct n) 

121 
case 0 thus ?case by simp 

122 
next 

123 
case (Suc n) 

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

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

126 
show ?case 

127 
proof cases 

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

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

130 
thus ?thesis using finB by simp 

131 
next 

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

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

134 
thus ?thesis using finB by simp 

135 
qed 

136 
qed 

137 

138 
lemma finite_conv_nat_seg_image: 

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

140 
by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite) 

141 

142 
subsubsection{* Finiteness and set theoretic constructions *} 

143 

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

146 
by (induct set: Finites) simp_all 

147 

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

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

150 
proof  

151 
assume "finite B" 

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

153 
proof induct 

154 
case empty 

155 
thus ?case by simp 

156 
next 

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

157 
case (insert x F A) 
12396  158 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 
159 
show "finite A" 

160 
proof cases 

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

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

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

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

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

166 
finally show ?thesis . 

167 
next 

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

169 
assume "x \<notin> A" 

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

171 
qed 

172 
qed 

173 
qed 

174 

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

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

177 

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

179 
 {* The converse obviously fails. *} 

180 
by (blast intro: finite_subset) 

181 

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

183 
apply (subst insert_is_Un) 

14208  184 
apply (simp only: finite_Un, blast) 
12396  185 
done 
186 

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

189 
by (induct rule:finite_induct) simp_all 

190 

12396  191 
lemma finite_empty_induct: 
192 
"finite A ==> 

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

194 
proof  

195 
assume "finite A" 

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

197 
have "P (A  A)" 

198 
proof  

199 
fix c b :: "'a set" 

200 
presume c: "finite c" and b: "finite b" 

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

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

203 
proof induct 

204 
case empty 

205 
from P1 show ?case by simp 

206 
next 

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

207 
case (insert x F) 
12396  208 
have "P (b  F  {x})" 
209 
proof (rule P2) 

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

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

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

213 
qed 

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

215 
finally show ?case . 

216 
qed 

217 
next 

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

219 
qed 

220 
thus "P {}" by simp 

221 
qed 

222 

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

224 
by (rule Diff_subset [THEN finite_subset]) 

225 

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

227 
apply (subst Diff_insert) 

228 
apply (case_tac "a : A  B") 

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

14208  230 
apply (subst insert_Diff, simp_all) 
12396  231 
done 
232 

233 

15392  234 
text {* Image and Inverse Image over Finite Sets *} 
13825  235 

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

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

238 
by (induct set: Finites) simp_all 

239 

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

240 
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

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

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

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

244 

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

14208  247 
apply (drule finite_imageI, simp) 
13825  248 
done 
249 

12396  250 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
251 
proof  

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

253 
fix B :: "'a set" 

254 
assume "finite B" 

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

256 
apply induct 

257 
apply simp 

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

259 
apply clarify 

260 
apply (simp (no_asm_use) add: inj_on_def) 

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

266 
done 

267 
qed (rule refl) 

268 

269 

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

272 
is included in a singleton. *} 

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

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

274 
apply (blast intro: the_equality [symmetric]) 
13825  275 
done 
276 

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

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

279 
is finite. *} 

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

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

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

282 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  283 
done 
284 

285 

15392  286 
text {* The finite UNION of finite sets *} 
12396  287 

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

289 
by (induct set: Finites) simp_all 

290 

291 
text {* 

292 
Strengthen RHS to 

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

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

295 
We'd need to prove 

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

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

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

300 
by (blast intro: finite_UN_I finite_subset) 

301 

302 

15392  303 
text {* Sigma of finite sets *} 
12396  304 

305 
lemma finite_SigmaI [simp]: 

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

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

308 

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

311 
by (rule finite_SigmaI) 

312 

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

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

316 
apply (erule ssubst) 

14208  317 
apply (erule finite_SigmaI, auto) 
12396  318 
done 
319 

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

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

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

322 
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

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

324 
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

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

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

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

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

329 
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

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

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

332 
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

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

334 

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

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

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

337 
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

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

339 
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

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

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

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

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

344 
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

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

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

347 
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

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

349 

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

350 

12396  351 
instance unit :: finite 
352 
proof 

353 
have "finite {()}" by simp 

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

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

356 
qed 

357 

358 
instance * :: (finite, finite) finite 

359 
proof 

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

361 
proof (rule finite_Prod_UNIV) 

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

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

364 
qed 

365 
qed 

366 

367 

15392  368 
text {* The powerset of a finite set *} 
12396  369 

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

371 
proof 

372 
assume "finite (Pow A)" 

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

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

375 
next 

376 
assume "finite A" 

377 
thus "finite (Pow A)" 

378 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

379 
qed 

380 

15392  381 

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

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

384 

385 

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

388 
apply simp 

389 
apply (rule iffI) 

390 
apply (erule finite_imageD [unfolded inj_on_def]) 

391 
apply (simp split add: split_split) 

392 
apply (erule finite_imageI) 

14208  393 
apply (simp add: converse_def image_def, auto) 
12396  394 
apply (rule bexI) 
395 
prefer 2 apply assumption 

396 
apply simp 

397 
done 

398 

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

399 

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

12396  402 

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

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

405 
apply (induct set: Finites) 

406 
apply (auto simp add: Field_def Domain_insert Range_insert) 

407 
done 

408 

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

410 
apply clarify 

411 
apply (erule trancl_induct) 

412 
apply (auto simp add: Field_def) 

413 
done 

414 

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

416 
apply auto 

417 
prefer 2 

418 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

419 
apply (rule finite_SigmaI) 

420 
prefer 3 

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

421 
apply (blast intro: r_into_trancl' finite_subset) 
12396  422 
apply (auto simp add: finite_Field) 
423 
done 

424 

425 

15392  426 
subsection {* A fold functional for finite sets *} 
427 

428 
text {* The intended behaviour is 

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

432 
*} 

433 

434 
consts 

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

436 

15480  437 
inductive "foldSet f g z" 
15392  438 
intros 
15480  439 
emptyI [intro]: "({}, z) : foldSet f g z" 
440 
insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk> 

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

15392  442 

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

445 
constdefs 

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

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

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

451 
It allows the removal of finiteness assumptions from the theorems 

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

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

454 

455 

15392  456 
lemma Diff1_foldSet: 
15480  457 
"(A  {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" 
15392  458 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
459 

15480  460 
lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" 
15392  461 
by (induct set: foldSet) auto 
462 

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

466 

467 
subsubsection {* Commutative monoids *} 

15480  468 

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

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

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

473 

474 
locale ACe = ACf + 

475 
fixes e :: 'a 

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

477 

15480  478 
locale ACIf = ACf + 
479 
assumes idem: "x \<cdot> x = x" 

480 

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

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

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

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

486 
finally show ?thesis . 

487 
qed 

488 

489 
lemmas (in ACf) AC = assoc commute left_commute 

490 

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

492 
proof  

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

494 
thus ?thesis by (subst commute) 

495 
qed 

496 

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

497 
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

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

499 
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

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

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

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

503 

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

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

505 

15402  506 
text{* Instantiation of locales: *} 
507 

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

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

510 

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

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

513 

514 

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

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

517 

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

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

520 

521 

15392  522 
subsubsection{*From @{term foldSet} to @{term fold}*} 
523 

15479  524 
(* only used in the next lemma, but in there twice *) 
525 
lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and 

526 
card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)" 

527 
shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h") 

528 
proof 

529 
let ?h = "%i. if h i = b then h n else h i" 

530 
show "B = ?h`{i. i<n}" (is "_ = ?r") 

531 
proof 

532 
show "B \<subseteq> ?r" 

533 
proof 

534 
fix u assume "u \<in> B" 

535 
hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+ 

536 
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" 

537 
using card by(auto simp:image_def) 

538 
show "u \<in> ?r" 

539 
proof cases 

540 
assume "i\<^isub>u < n" 

541 
thus ?thesis using unotb by(fastsimp) 

542 
next 

543 
assume "\<not> i\<^isub>u < n" 

544 
with below have [simp]: "i\<^isub>u = n" by arith 

545 
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k" 

546 
using A1 card by blast 

547 
have "i\<^isub>k < n" 

548 
proof (rule ccontr) 

549 
assume "\<not> i\<^isub>k < n" 

550 
hence "i\<^isub>k = n" using i\<^isub>k by arith 

551 
thus False using unotb by simp 

552 
qed 

553 
thus ?thesis by(auto simp add:image_def) 

554 
qed 

555 
qed 

556 
next 

557 
show "?r \<subseteq> B" 

558 
proof 

559 
fix u assume "u \<in> ?r" 

560 
then obtain i\<^isub>u where below: "i\<^isub>u < n" and 

561 
or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

562 
by(auto simp:image_def) 

563 
from or show "u \<in> B" 

564 
proof 

565 
assume [simp]: "b = h i\<^isub>u \<and> u = h n" 

566 
have "u \<in> A" using card by auto 

567 
moreover have "u \<noteq> b" using new below by auto 

568 
ultimately show "u \<in> B" using A1 by blast 

569 
next 

570 
assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

571 
moreover hence "u \<in> A" using card below by auto 

572 
ultimately show "u \<in> B" using A1 by blast 

573 
qed 

574 
qed 

575 
qed 

576 
qed 

577 

15392  578 
lemma (in ACf) foldSet_determ_aux: 
15480  579 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk> 
15392  580 
\<Longrightarrow> x' = x" 
581 
proof (induct n) 

582 
case 0 thus ?case by auto 

583 
next 

584 
case (Suc n) 

15480  585 
have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g z; (A,x') \<in> foldSet f g z\<rbrakk> 
15392  586 
\<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}" 
15480  587 
and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" . 
15392  588 
show ?case 
589 
proof cases 

15487  590 
assume "EX k<n. h n = h k" 
591 
{*@{term h} is not injective, so the cardinality has not increased*} 

15392  592 
hence card': "A = h ` {i. i < n}" 
593 
using card by (auto simp:image_def less_Suc_eq) 

594 
show ?thesis by(rule IH[OF card' Afoldx Afoldy]) 

595 
next 

596 
assume new: "\<not>(EX k<n. h n = h k)" 

597 
show ?thesis 

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

15487  599 
assume "(A, x) = ({}, z)" {*fold of a singleton set*} 
15392  600 
thus "x' = x" using Afoldy by (auto) 
601 
next 

602 
fix B b y 

603 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

15480  604 
and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B" 
15392  605 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 
606 
show ?thesis 

607 
proof (rule foldSet.cases[OF Afoldy]) 

15480  608 
assume "(A,x') = ({}, z)" 
15392  609 
thus ?thesis using A1 by auto 
610 
next 

15480  611 
fix C c r 
612 
assume eq2: "(A,x') = (insert c C, g c \<cdot> r)" 

613 
and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C" 

614 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto 

15479  615 
obtain hB where lessB: "B = hB ` {i. i<n}" 
616 
using card_lemma[OF A1 notinB card new] by auto 

617 
obtain hC where lessC: "C = hC ` {i. i<n}" 

618 
using card_lemma[OF A2 notinC card new] by auto 

15392  619 
show ?thesis 
620 
proof cases 

621 
assume "b = c" 

622 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

15480  623 
ultimately show ?thesis using IH[OF lessB] y r x x' by auto 
15392  624 
next 
625 
assume diff: "b \<noteq> c" 

626 
let ?D = "B  {c}" 

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

628 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

15402  629 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
630 
with A1 have "finite ?D" by simp 

15480  631 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  632 
using finite_imp_foldSet by rules 
633 
moreover have cinB: "c \<in> B" using B by(auto) 

15480  634 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  635 
by(rule Diff1_foldSet) 
15479  636 
hence "g c \<cdot> d = y" by(rule IH[OF lessB y]) 
15480  637 
moreover have "g b \<cdot> d = r" 
638 
proof (rule IH[OF lessC r]) 

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

15392  640 
by fastsimp 
641 
qed 

642 
ultimately show ?thesis using x x' by(auto simp:AC) 

643 
qed 

644 
qed 

645 
qed 

646 
qed 

647 
qed 

648 

649 
(* The same proof, but using card 

650 
lemma (in ACf) foldSet_determ_aux: 

651 
"!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> 

652 
\<Longrightarrow> x' = x" 

653 
proof (induct n) 

654 
case 0 thus ?case by simp 

655 
next 

656 
case (Suc n) 

657 
have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> 

658 
\<Longrightarrow> x' = x" and card: "card A < Suc n" 

659 
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . 

660 
from card have "card A < n \<or> card A = n" by arith 

661 
thus ?case 

662 
proof 

663 
assume less: "card A < n" 

664 
show ?thesis by(rule IH[OF less Afoldx Afoldy]) 

665 
next 

666 
assume cardA: "card A = n" 

667 
show ?thesis 

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

669 
assume "(A, x) = ({}, e)" 

670 
thus "x' = x" using Afoldy by (auto) 

671 
next 

672 
fix B b y 

673 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

674 
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" 

675 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 

676 
show ?thesis 

677 
proof (rule foldSet.cases[OF Afoldy]) 

678 
assume "(A,x') = ({}, e)" 

679 
thus ?thesis using A1 by auto 

680 
next 

681 
fix C c z 

682 
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" 

683 
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" 

684 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto 

685 
have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 

686 
with cardA A1 notinB have less: "card B < n" by simp 

687 
show ?thesis 

688 
proof cases 

689 
assume "b = c" 

690 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

691 
ultimately show ?thesis using IH[OF less] y z x x' by auto 

692 
next 

693 
assume diff: "b \<noteq> c" 

694 
let ?D = "B  {c}" 

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

696 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

697 
have "finite ?D" using finA A1 by simp 

698 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" 

699 
using finite_imp_foldSet by rules 

700 
moreover have cinB: "c \<in> B" using B by(auto) 

701 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" 

702 
by(rule Diff1_foldSet) 

703 
hence "g c \<cdot> d = y" by(rule IH[OF less y]) 

704 
moreover have "g b \<cdot> d = z" 

705 
proof (rule IH[OF _ z]) 

706 
show "card C < n" using C cardA A1 notinB finA cinB 

707 
by(auto simp:card_Diff1_less) 

708 
next 

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

710 
by fastsimp 

711 
qed 

712 
ultimately show ?thesis using x x' by(auto simp:AC) 

713 
qed 

714 
qed 

715 
qed 

716 
qed 

717 
qed 

718 
*) 

719 

720 
lemma (in ACf) foldSet_determ: 

15480  721 
"(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x" 
15392  722 
apply(frule foldSet_imp_finite) 
723 
apply(simp add:finite_conv_nat_seg_image) 

724 
apply(blast intro: foldSet_determ_aux [rule_format]) 

725 
done 

726 

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

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

731 

15480  732 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  733 
by (unfold fold_def) blast 
734 

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

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

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

740 
apply (fastsimp dest: foldSet_imp_finite) 

741 
apply (blast intro: foldSet_determ) 

742 
done 

743 

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

745 

746 
lemma (in ACf) fold_insert[simp]: 

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

750 
apply (rule the_equality) 

751 
apply (auto intro: finite_imp_foldSet 

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

753 
done 

754 

755 
declare 

756 
empty_foldSetE [rule del] foldSet.intros [rule del] 

757 
 {* Delete rules to do with @{text foldSet} relation. *} 

758 

15480  759 
text{* A simplified version for idempotent functions: *} 
760 

761 
lemma (in ACIf) fold_insert2: 

762 
assumes finA: "finite A" 

763 
shows "fold (op \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A" 

764 
proof cases 

765 
assume "a \<in> A" 

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

767 
by(blast dest: mk_disjoint_insert) 

768 
show ?thesis 

769 
proof  

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

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

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

773 
using finB disj by(simp) 

774 
also have "\<dots> = g a \<cdot> fold f g z A" 

775 
using A finB disj by(simp add:idem assoc[symmetric]) 

776 
finally show ?thesis . 

777 
qed 

778 
next 

779 
assume "a \<notin> A" 

780 
with finA show ?thesis by simp 

781 
qed 

782 

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

785 
by(erule finite_induct)(simp_all add: fold_insert2 del: fold_insert) 

786 

15392  787 
subsubsection{*Lemmas about @{text fold}*} 
788 

789 
lemma (in ACf) fold_commute: 

15487  790 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
15392  791 
apply (induct set: Finites, simp) 
15487  792 
apply (simp add: left_commute [of x]) 
15392  793 
done 
794 

795 
lemma (in ACf) fold_nest_Un_Int: 

796 
"finite A ==> finite B 

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

800 
done 

801 

802 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  804 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  805 
by (simp add: fold_nest_Un_Int) 
806 

807 
lemma (in ACf) fold_reindex: 

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

15392  810 
using fin apply (induct) 
811 
apply simp 

812 
apply simp 

813 
done 

814 

815 
lemma (in ACe) fold_Un_Int: 

816 
"finite A ==> finite B ==> 

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

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

819 
apply (induct set: Finites, simp) 

820 
apply (simp add: AC insert_absorb Int_insert_left) 

821 
done 

822 

823 
corollary (in ACe) fold_Un_disjoint: 

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

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

826 
by (simp add: fold_Un_Int) 

827 

828 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

835 
prefer 2 apply blast 

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

837 
prefer 2 apply blast 

838 
apply (simp add: fold_Un_disjoint) 

839 
done 

840 

841 
lemma (in ACf) fold_cong: 

15480  842 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
843 
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  844 
apply simp 
845 
apply (erule finite_induct, simp) 

846 
apply (simp add: subset_insert_iff, clarify) 

847 
apply (subgoal_tac "finite C") 

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

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

850 
prefer 2 apply blast 

851 
apply (erule ssubst) 

852 
apply (drule spec) 

853 
apply (erule (1) notE impE) 

854 
apply (simp add: Ball_def del: insert_Diff_single) 

855 
done 

856 

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

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

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

860 
apply (subst Sigma_def) 

861 
apply (subst fold_UN_disjoint) 

862 
apply assumption 

863 
apply simp 

864 
apply blast 

865 
apply (erule fold_cong) 

866 
apply (subst fold_UN_disjoint) 

867 
apply simp 

868 
apply simp 

869 
apply blast 

870 
apply (simp) 

871 
done 

872 

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

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

875 
apply (erule finite_induct) 

876 
apply simp 

877 
apply (simp add:AC) 

878 
done 

879 

880 

15402  881 
subsection {* Generalized summation over a set *} 
882 

883 
constdefs 

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

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

886 

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

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

889 

890 
syntax 

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

892 
syntax (xsymbols) 

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

894 
syntax (HTML output) 

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

896 

897 
translations  {* Beware of argument permutation! *} 

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

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

900 

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

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

903 

904 
syntax 

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

906 
syntax (xsymbols) 

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

908 
syntax (HTML output) 

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

910 

911 
translations 

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

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

914 

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

916 

917 
syntax 

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

919 

920 
parse_translation {* 

921 
let 

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

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

924 
*} 

925 

926 
print_translation {* 

927 
let 

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

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

930 
if x<>y then raise Match 

931 
else let val x' = Syntax.mark_bound x 

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

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

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

935 
in 

936 
[("setsum", setsum_tr')] 

937 
end 

938 
*} 

939 

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

941 
by (simp add: setsum_def) 

942 

943 
lemma setsum_insert [simp]: 

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

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

946 

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

947 
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

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

949 

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

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

953 

954 
lemma setsum_reindex_id: 

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

956 
by (auto simp add: setsum_reindex) 

957 

958 
lemma setsum_cong: 

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

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

961 

962 
lemma setsum_reindex_cong: 

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

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

965 
by (simp add: setsum_reindex cong: setsum_cong) 

966 

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

968 
apply (clarsimp simp: setsum_def) 

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

970 
done 

971 

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

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

974 
apply (erule ssubst, rule setsum_0) 

975 
apply (rule setsum_cong, auto) 

976 
done 

977 

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

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

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

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

982 

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

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

985 
by (subst setsum_Un_Int [symmetric], auto) 

986 

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

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

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

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

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

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

994 

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

995 
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

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

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

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

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

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

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

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

1005 
done 
15402  1006 

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

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

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

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

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

1013 

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

1014 
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

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

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

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

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

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

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

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

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

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

1024 
done 
15402  1025 

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

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

1028 

1029 

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

1031 

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

1033 
apply (case_tac "finite A") 

1034 
prefer 2 apply (simp add: setsum_def) 

1035 
apply (erule rev_mp) 

1036 
apply (erule finite_induct, auto) 

1037 
done 

1038 

1039 
lemma setsum_eq_0_iff [simp]: 

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

1041 
by (induct set: Finites) auto 

1042 

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

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

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

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

1047 

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

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

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

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

1052 

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

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

1055 
apply (case_tac "finite A") 

1056 
prefer 2 apply (simp add: setsum_def) 

1057 
apply (erule finite_induct) 

1058 
apply (auto simp add: insert_Diff_if) 

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

1060 
done 

1061 

1062 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1066 

1067 
(* By Jeremy Siek: *) 

1068 

1069 
lemma setsum_diff_nat: 

1070 
assumes finB: "finite B" 

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

1072 
using finB 

1073 
proof (induct) 

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

1075 
next 

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

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

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

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

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

1081 
by (simp add: setsum_diff1_nat) 

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

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

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

1085 
by simp 

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

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

1088 
by simp 

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

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

1091 
by simp 

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

1093 
qed 

1094 

1095 
lemma setsum_diff: 

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

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

1098 
proof  

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

1100 
show ?thesis using finiteB le 

1101 
proof (induct) 

1102 
case empty 

1103 
thus ?case by auto 

1104 
next 

1105 
case (insert x F) 

1106 
thus ?case using le finiteB 

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

1108 
qed 

1109 
qed 

1110 

1111 
lemma setsum_mono: 

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

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

1114 
proof (cases "finite K") 

1115 
case True 

1116 
thus ?thesis using le 

1117 
proof (induct) 

1118 
case empty 

1119 
thus ?case by simp 

1120 
next 

1121 
case insert 

1122 
thus ?case using add_mono 

1123 
by force 

1124 
qed 

1125 
next 

1126 
case False 

1127 
thus ?thesis 

1128 
by (simp add: setsum_def) 

1129 
qed 

1130 

1131 
lemma setsum_mono2_nat: 

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

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

1134 
proof  

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

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

1137 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1139 
finally show ?thesis . 

1140 
qed 

1141 

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

1143 
 setsum f A" 

1144 
by (induct set: Finites, auto) 

1145 

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

1147 
setsum f A  setsum g A" 

1148 
by (simp add: diff_minus setsum_addf setsum_negf) 

1149 

1150 
lemma setsum_nonneg: "[ finite A; 

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

1152 
0 \<le> setsum f A"; 

1153 
apply (induct set: Finites, auto) 

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

1155 
apply (blast intro: add_mono) 

1156 
done 

1157 

1158 
lemma setsum_nonpos: "[ finite A; 

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

1160 
setsum f A \<le> 0"; 

1161 
apply (induct set: Finites, auto) 

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

1163 
apply (blast intro: add_mono) 

1164 
done 

1165 

1166 
lemma setsum_mult: 

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

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

1169 
proof (cases "finite A") 

1170 
case True 

1171 
thus ?thesis 

1172 
proof (induct) 

1173 
case empty thus ?case by simp 

1174 
next 

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

1176 
qed 

1177 
next 

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

1179 
qed 

1180 

1181 
lemma setsum_abs: 

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

1183 
assumes fin: "finite A" 

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

1185 
using fin 

1186 
proof (induct) 

1187 
case empty thus ?case by simp 

1188 
next 

1189 
case (insert x A) 

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

1191 
qed 

1192 

1193 
lemma setsum_abs_ge_zero: 

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

1195 
assumes fin: "finite A" 

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

1197 
using fin 

1198 
proof (induct) 

1199 
case empty thus ?case by simp 

1200 
next 

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

1202 
qed 

1203 

1204 

1205 
subsection {* Generalized product over a set *} 

1206 

1207 
constdefs 

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

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

1210 

1211 
syntax 

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

1213 

1214 
syntax (xsymbols) 

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

1216 
syntax (HTML output) 

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

1218 
translations 

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

1220 

1221 
syntax 

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

1223 

1224 
parse_translation {* 

1225 
let 

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

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

1228 
*} 

1229 
print_translation {* 

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

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

1232 
in 

1233 
[("setprod", setprod_tr')] 

1234 
end 

1235 
*} 

1236 

1237 

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

1239 
by (auto simp add: setprod_def) 

1240 

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

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

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

1244 

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

1245 
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

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

1247 

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

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

1251 

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

1253 
by (auto simp add: setprod_reindex) 

1254 

1255 
lemma setprod_cong: 

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

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

1258 

1259 
lemma setprod_reindex_cong: "inj_on f A ==> 

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

1261 
by (frule setprod_reindex, simp) 

1262 

1263 

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

1265 
apply (case_tac "finite A") 

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

1267 
done 

1268 

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

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

1271 
apply (erule ssubst, rule setprod_1) 

1272 
apply (rule setprod_cong, auto) 

1273 
done 

1274 

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

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

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

1278 

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

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

1281 
by (subst setprod_Un_Int [symmetric], auto) 

1282 

1283 
lemma setprod_UN_disjoint: 

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

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

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

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

1288 

1289 
lemma setprod_Union_disjoint: 

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

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

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

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

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

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

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

1297 
done 
15402  1298 

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

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

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

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

1303 

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

1304 
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

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

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

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

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

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

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

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

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

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

1314 
done 
15402  1315 

1316 
lemma setprod_timesf: 

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

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

1320 

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

1322 

1323 
lemma setprod_eq_1_iff [simp]: 

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

1325 
by (induct set: Finites) auto 

1326 

1327 
lemma setprod_zero: 

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

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

1330 
apply (erule disjE, auto) 

1331 
done 

1332 

1333 
lemma setprod_nonneg [rule_format]: 

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

1335 
apply (case_tac "finite A") 

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

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

1338 
apply (rule mult_mono, assumption+) 

1339 
apply (auto simp add: setprod_def) 

1340 
done 

1341 

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

1343 
> 0 < setprod f A" 

1344 
apply (case_tac "finite A") 

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

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

1347 
apply (rule mult_strict_mono, assumption+) 

1348 
apply (auto simp add: setprod_def) 

1349 
done 

1350 

1351 
lemma setprod_nonzero [rule_format]: 

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

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

1354 
apply (erule finite_induct, auto) 

1355 
done 

1356 

1357 
lemma setprod_zero_eq: 

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

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

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

1361 
done 

1362 

1363 
lemma setprod_nonzero_field: 

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

1365 
apply (rule setprod_nonzero, auto) 

1366 
done 

1367 

1368 
lemma setprod_zero_eq_field: 

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

1370 
apply (rule setprod_zero_eq, auto) 

1371 
done 

1372 

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

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

