author  ballarin 
Fri, 26 Aug 2005 10:01:06 +0200  
changeset 17149  e2b19c92ef51 
parent 17085  5b57f995a179 
child 17189  b15f8e094874 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

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

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

4 
with contributions by Jeremy Avigad 
12396  5 
*) 
6 

7 
header {* Finite sets *} 

8 

15131  9 
theory Finite_Set 
16760  10 
imports Power Inductive Lattice_Locales 
15131  11 
begin 
12396  12 

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

15 
consts Finites :: "'a set set" 

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

18 
translations 

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

12396  20 

21 
inductive Finites 

22 
intros 

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

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

25 

26 
axclass finite \<subseteq> type 

27 
finite: "finite UNIV" 

28 

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

32 
proof  

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

34 
thus ?thesis by blast 

35 
qed 

12396  36 

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

38 
"finite F ==> 

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

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

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

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

46 
proof induct 

47 
show "P {}" . 

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

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

51 
assume "x \<in> F" 

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

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

54 
next 

55 
assume "x \<notin> F" 

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

57 
qed 

58 
qed 

59 
qed 

60 

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

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

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

65 
\<Longrightarrow> P F" 

66 
using fin 

67 
proof induct 

68 
case empty thus ?case by simp 

69 
next 

70 
case (insert x F) 

71 
show ?case 

72 
proof cases 

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

74 
next 

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

76 
qed 

77 
qed 

78 

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

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

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

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

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

88 
proof induct 

89 
show "P {}" . 

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

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

93 
proof (rule insert) 

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

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

96 
with P show "P F" . 

97 
qed 

98 
qed 

99 
qed 

100 

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

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

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

15392  106 
using fin 
107 
proof induct 

108 
case empty 

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

111 
qed 

15392  112 
next 
113 
case (insert a A) 

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

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

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

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

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

15392  120 
thus ?case by blast 
121 
qed 

122 

123 
lemma nat_seg_image_imp_finite: 

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

125 
proof (induct n) 

126 
case 0 thus ?case by simp 

127 
next 

128 
case (Suc n) 

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

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

131 
show ?case 

132 
proof cases 

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

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

135 
thus ?thesis using finB by simp 

136 
next 

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

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

139 
thus ?thesis using finB by simp 

140 
qed 

141 
qed 

142 

143 
lemma finite_conv_nat_seg_image: 

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

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

147 
subsubsection{* Finiteness and set theoretic constructions *} 

148 

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

151 
by (induct set: Finites) simp_all 

152 

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

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

155 
proof  

156 
assume "finite B" 

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

158 
proof induct 

159 
case empty 

160 
thus ?case by simp 

161 
next 

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

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

165 
proof cases 

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

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

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

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

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

171 
finally show ?thesis . 

172 
next 

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

174 
assume "x \<notin> A" 

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

176 
qed 

177 
qed 

178 
qed 

179 

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

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

182 

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

184 
 {* The converse obviously fails. *} 

185 
by (blast intro: finite_subset) 

186 

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

188 
apply (subst insert_is_Un) 

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

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

194 
by (induct rule:finite_induct) simp_all 

195 

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

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

199 
proof  

200 
assume "finite A" 

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

202 
have "P (A  A)" 

203 
proof  

204 
fix c b :: "'a set" 

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

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

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

208 
proof induct 

209 
case empty 

210 
from P1 show ?case by simp 

211 
next 

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

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

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

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

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

218 
qed 

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

220 
finally show ?case . 

221 
qed 

222 
next 

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

224 
qed 

225 
thus "P {}" by simp 

226 
qed 

227 

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

229 
by (rule Diff_subset [THEN finite_subset]) 

230 

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

232 
apply (subst Diff_insert) 

233 
apply (case_tac "a : A  B") 

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

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

238 

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

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

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

243 
by (induct set: Finites) simp_all 

244 

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

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

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

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

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

249 

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

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

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

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

258 
fix B :: "'a set" 

259 
assume "finite B" 

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

261 
apply induct 

262 
apply simp 

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

264 
apply clarify 

265 
apply (simp (no_asm_use) add: inj_on_def) 

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

271 
done 

272 
qed (rule refl) 

273 

274 

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

277 
is included in a singleton. *} 

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

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

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

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

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

284 
is finite. *} 

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

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

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

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

290 

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

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

294 
by (induct set: Finites) simp_all 

295 

296 
text {* 

297 
Strengthen RHS to 

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

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

300 
We'd need to prove 

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

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

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

305 
by (blast intro: finite_UN_I finite_subset) 

306 

307 

17022  308 
lemma finite_Plus: "[ finite A; finite B ] ==> finite (A <+> B)" 
309 
by (simp add: Plus_def) 

310 

15392  311 
text {* Sigma of finite sets *} 
12396  312 

313 
lemma finite_SigmaI [simp]: 

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

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

316 

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

319 
by (rule finite_SigmaI) 

320 

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

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

324 
apply (erule ssubst) 

14208  325 
apply (erule finite_SigmaI, auto) 
12396  326 
done 
327 

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

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

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

330 
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

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

332 
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

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

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

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

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

337 
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

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

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

340 
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

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

342 

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

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

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

345 
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

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

347 
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

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

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

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

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

352 
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

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

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

355 
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

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

357 

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

358 

15392  359 
text {* The powerset of a finite set *} 
12396  360 

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

362 
proof 

363 
assume "finite (Pow A)" 

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

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

366 
next 

367 
assume "finite A" 

368 
thus "finite (Pow A)" 

369 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

370 
qed 

371 

15392  372 

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

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

375 

376 

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

379 
apply simp 

380 
apply (rule iffI) 

381 
apply (erule finite_imageD [unfolded inj_on_def]) 

382 
apply (simp split add: split_split) 

383 
apply (erule finite_imageI) 

14208  384 
apply (simp add: converse_def image_def, auto) 
12396  385 
apply (rule bexI) 
386 
prefer 2 apply assumption 

387 
apply simp 

388 
done 

389 

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

390 

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

12396  393 

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

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

396 
apply (induct set: Finites) 

397 
apply (auto simp add: Field_def Domain_insert Range_insert) 

398 
done 

399 

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

401 
apply clarify 

402 
apply (erule trancl_induct) 

403 
apply (auto simp add: Field_def) 

404 
done 

405 

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

407 
apply auto 

408 
prefer 2 

409 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

410 
apply (rule finite_SigmaI) 

411 
prefer 3 

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

412 
apply (blast intro: r_into_trancl' finite_subset) 
12396  413 
apply (auto simp add: finite_Field) 
414 
done 

415 

416 

15392  417 
subsection {* A fold functional for finite sets *} 
418 

419 
text {* The intended behaviour is 

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

423 
*} 

424 

425 
consts 

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

427 

15480  428 
inductive "foldSet f g z" 
15392  429 
intros 
15480  430 
emptyI [intro]: "({}, z) : foldSet f g z" 
15506  431 
insertI [intro]: 
432 
"\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk> 

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

15392  434 

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

437 
constdefs 

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

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

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

443 
It allows the removal of finiteness assumptions from the theorems 

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

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

446 

447 

15392  448 
lemma Diff1_foldSet: 
15480  449 
"(A  {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" 
15392  450 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
451 

15480  452 
lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" 
15392  453 
by (induct set: foldSet) auto 
454 

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

458 

459 
subsubsection {* Commutative monoids *} 

15480  460 

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

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

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

465 

466 
locale ACe = ACf + 

467 
fixes e :: 'a 

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

469 

15480  470 
locale ACIf = ACf + 
471 
assumes idem: "x \<cdot> x = x" 

472 

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

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

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

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

478 
finally show ?thesis . 

479 
qed 

480 

481 
lemmas (in ACf) AC = assoc commute left_commute 

482 

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

484 
proof  

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

486 
thus ?thesis by (subst commute) 

487 
qed 

488 

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

489 
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

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

491 
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

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

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

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

495 

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

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

497 

15765  498 
text{* Interpretation of locales: *} 
499 

500 
interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"] 

501 
by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute) 

15402  502 

15765  503 
interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] 
504 
apply  

15780  505 
apply (fast intro: ACf.intro mult_assoc mult_commute) 
506 
apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute) 

15765  507 
done 
508 

15402  509 

15392  510 
subsubsection{*From @{term foldSet} to @{term fold}*} 
511 

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

514 

515 
lemma insert_image_inj_on_eq: 

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

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

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

519 
apply (auto simp add: image_less_Suc inj_on_def) 

520 
apply (blast intro: less_trans) 

521 
done 

522 

523 
lemma insert_inj_onE: 

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

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

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

527 
proof (cases n) 

528 
case 0 thus ?thesis using aA by auto 

529 
next 

530 
case (Suc m) 

531 
have nSuc: "n = Suc m" . 

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

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

536 
by (simp add: inj_on_swap_iff inj_on) 

15510  537 
show ?thesis 
15520  538 
proof (intro exI conjI) 
539 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

543 
proof (rule insert_image_inj_on_eq) 

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

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

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

547 
using aA hkeq nSuc klessn 

548 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

549 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  550 
qed 
551 
qed 

552 
qed 

553 

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

15392  557 
\<Longrightarrow> x' = x" 
15510  558 
proof (induct n rule: less_induct) 
559 
case (less n) 

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

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

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

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

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

565 
show ?case 

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

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

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

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

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

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

574 
show "x'=x" 

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

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

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

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

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

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

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

584 
from insert_inj_onE [OF Beq notinB injh] 

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

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

587 
and lessB: "mB < n" by auto 

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

589 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

592 
and lessC: "mC < n" by auto 

593 
show "x'=x" 

15392  594 
proof cases 
15510  595 
assume "b=c" 
596 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

598 
by auto 

15392  599 
next 
600 
assume diff: "b \<noteq> c" 

601 
let ?D = "B  {c}" 

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

15510  603 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  604 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  605 
with AbB have "finite ?D" by simp 
15480  606 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" 
15392  607 
using finite_imp_foldSet by rules 
15506  608 
moreover have cinB: "c \<in> B" using B by auto 
15480  609 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" 
15392  610 
by(rule Diff1_foldSet) 
15510  611 
hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
612 
moreover have "g b \<cdot> d = v" 

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

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

15392  615 
by fastsimp 
616 
qed 

15510  617 
ultimately show ?thesis using x x' by (auto simp: AC) 
15392  618 
qed 
619 
qed 

620 
qed 

621 
qed 

622 

623 

624 
lemma (in ACf) foldSet_determ: 

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

627 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  628 
done 
629 

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

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

634 

15480  635 
lemma fold_empty [simp]: "fold f g z {} = z" 
15392  636 
by (unfold fold_def) blast 
637 

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

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

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

643 
apply (fastsimp dest: foldSet_imp_finite) 

644 
apply (blast intro: foldSet_determ) 

645 
done 

646 

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

648 

649 
lemma (in ACf) fold_insert[simp]: 

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

653 
apply (rule the_equality) 

654 
apply (auto intro: finite_imp_foldSet 

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

656 
done 

657 

15535  658 
lemma (in ACf) fold_rec: 
659 
assumes fin: "finite A" and a: "a:A" 

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

661 
proof 

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

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

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

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

666 
finally show ?thesis . 

667 
qed 

668 

15392  669 

15480  670 
text{* A simplified version for idempotent functions: *} 
671 

15509  672 
lemma (in ACIf) fold_insert_idem: 
15480  673 
assumes finA: "finite A" 
15508  674 
shows "fold f g z (insert a A) = g a \<cdot> fold f g z A" 
15480  675 
proof cases 
676 
assume "a \<in> A" 

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

678 
by(blast dest: mk_disjoint_insert) 

679 
show ?thesis 

680 
proof  

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

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

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

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

687 
finally show ?thesis . 

688 
qed 

689 
next 

690 
assume "a \<notin> A" 

691 
with finA show ?thesis by simp 

692 
qed 

693 

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

15509  696 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  697 

15392  698 
subsubsection{*Lemmas about @{text fold}*} 
699 

700 
lemma (in ACf) fold_commute: 

15487  701 
"finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" 
15392  702 
apply (induct set: Finites, simp) 
15487  703 
apply (simp add: left_commute [of x]) 
15392  704 
done 
705 

706 
lemma (in ACf) fold_nest_Un_Int: 

707 
"finite A ==> finite B 

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

711 
done 

712 

713 
lemma (in ACf) fold_nest_Un_disjoint: 

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

15480  715 
==> fold f g z (A Un B) = fold f g (fold f g z B) A" 
15392  716 
by (simp add: fold_nest_Un_Int) 
717 

718 
lemma (in ACf) fold_reindex: 

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

15506  721 
using fin apply induct 
15392  722 
apply simp 
723 
apply simp 

724 
done 

725 

726 
lemma (in ACe) fold_Un_Int: 

727 
"finite A ==> finite B ==> 

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

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

730 
apply (induct set: Finites, simp) 

731 
apply (simp add: AC insert_absorb Int_insert_left) 

732 
done 

733 

734 
corollary (in ACe) fold_Un_disjoint: 

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

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

737 
by (simp add: fold_Un_Int) 

738 

739 
lemma (in ACe) fold_UN_disjoint: 

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

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

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

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

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

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

746 
prefer 2 apply blast 

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

748 
prefer 2 apply blast 

749 
apply (simp add: fold_Un_disjoint) 

750 
done 

751 

15506  752 
text{*Fusion theorem, as described in 
753 
Graham Hutton's paper, 

754 
A Tutorial on the Universality and Expressiveness of Fold, 

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

756 
lemma (in ACf) fold_fusion: 

757 
includes ACf g 

758 
shows 

759 
"finite A ==> 

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

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

762 
by (induct set: Finites, simp_all) 

763 

15392  764 
lemma (in ACf) fold_cong: 
15480  765 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" 
766 
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  767 
apply simp 
768 
apply (erule finite_induct, simp) 

769 
apply (simp add: subset_insert_iff, clarify) 

770 
apply (subgoal_tac "finite C") 

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

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

773 
prefer 2 apply blast 

774 
apply (erule ssubst) 

775 
apply (drule spec) 

776 
apply (erule (1) notE impE) 

777 
apply (simp add: Ball_def del: insert_Diff_single) 

778 
done 

779 

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

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

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

783 
apply (subst Sigma_def) 

15506  784 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  785 
apply blast 
786 
apply (erule fold_cong) 

15506  787 
apply (subst fold_UN_disjoint, simp, simp) 
15392  788 
apply blast 
15506  789 
apply simp 
15392  790 
done 
791 

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

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

15506  794 
apply (erule finite_induct, simp) 
15392  795 
apply (simp add:AC) 
796 
done 

797 

798 

15402  799 
subsection {* Generalized summation over a set *} 
800 

801 
constdefs 

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

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

804 

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

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

807 

808 
syntax 

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

810 
syntax (xsymbols) 

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

812 
syntax (HTML output) 

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

814 

815 
translations  {* Beware of argument permutation! *} 

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

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

818 

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

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

821 

822 
syntax 

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

824 
syntax (xsymbols) 

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

826 
syntax (HTML output) 

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

828 

829 
translations 

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

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

832 

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

834 

835 
syntax 

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

837 

838 
parse_translation {* 

839 
let 

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

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

842 
*} 

843 

844 
print_translation {* 

845 
let 

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

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

848 
if x<>y then raise Match 

849 
else let val x' = Syntax.mark_bound x 

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

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

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

853 
in 

854 
[("setsum", setsum_tr')] 

855 
end 

856 
*} 

857 

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

859 
by (simp add: setsum_def) 

860 

861 
lemma setsum_insert [simp]: 

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

15765  863 
by (simp add: setsum_def) 
15402  864 

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

865 
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

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

867 

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

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

872 
lemma setsum_reindex_id: 

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

874 
by (auto simp add: setsum_reindex) 

875 

876 
lemma setsum_cong: 

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

15765  878 
by(fastsimp simp: setsum_def intro: AC_add.fold_cong) 
15402  879 

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

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

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

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

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

884 

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

887 

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

892 

15542  893 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  894 
apply (clarsimp simp: setsum_def) 
15765  895 
apply (erule finite_induct, auto) 
15402  896 
done 
897 

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

15402  900 

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

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

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

15765  904 
by(simp add: setsum_def AC_add.fold_Un_Int [symmetric]) 
15402  905 

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

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

908 
by (subst setsum_Un_Int [symmetric], auto) 

909 

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

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

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

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

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

15765  916 
by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong) 
15402  917 

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

918 
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

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

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

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

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

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

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

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

928 
done 
15402  929 

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

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

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

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

15765  935 
by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong) 
15402  936 

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

937 
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

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

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

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

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

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

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

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

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

947 
done 
15402  948 

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

15765  950 
by(simp add:setsum_def AC_add.fold_distrib) 
15402  951 

952 

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

954 

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

956 
apply (case_tac "finite A") 

957 
prefer 2 apply (simp add: setsum_def) 

958 
apply (erule rev_mp) 

959 
apply (erule finite_induct, auto) 

960 
done 

961 

962 
lemma setsum_eq_0_iff [simp]: 

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

964 
by (induct set: Finites) auto 

965 

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

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

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

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

970 

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

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

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

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

975 

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

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

978 
apply (case_tac "finite A") 

979 
prefer 2 apply (simp add: setsum_def) 

980 
apply (erule finite_induct) 

981 
apply (auto simp add: insert_Diff_if) 

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

983 
done 

984 

985 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

989 

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

990 
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

991 
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

992 
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

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

994 

15402  995 
(* By Jeremy Siek: *) 
996 

997 
lemma setsum_diff_nat: 

998 
assumes finB: "finite B" 

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

1000 
using finB 

1001 
proof (induct) 

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

1003 
next 

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

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

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

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

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

1009 
by (simp add: setsum_diff1_nat) 

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

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

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

1013 
by simp 

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

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

1016 
by simp 

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

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

1019 
by simp 

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

1021 
qed 

1022 

1023 
lemma setsum_diff: 

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

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

1026 
proof  

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

1028 
show ?thesis using finiteB le 

1029 
proof (induct) 

1030 
case empty 

1031 
thus ?case by auto 

1032 
next 

1033 
case (insert x F) 

1034 
thus ?case using le finiteB 

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

1036 
qed 

1037 
qed 

1038 

1039 
lemma setsum_mono: 

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

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

1042 
proof (cases "finite K") 

1043 
case True 

1044 
thus ?thesis using le 

1045 
proof (induct) 

1046 
case empty 

1047 
thus ?case by simp 

1048 
next 

1049 
case insert 

1050 
thus ?case using add_mono 

1051 
by force 

1052 
qed 

1053 
next 

1054 
case False 

1055 
thus ?thesis 

1056 
by (simp add: setsum_def) 

1057 
qed 

1058 

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

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

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

1063 
using fin_ne 

1064 
proof (induct rule: finite_ne_induct) 

1065 
case singleton thus ?case by simp 

1066 
next 

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

1068 
qed 

1069 

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

1072 
proof (cases "finite A") 

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

1074 
next 

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

1076 
qed 

15402  1077 

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

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

1083 
next 

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

1085 
qed 

15402  1086 

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

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

1090 
proof (cases "finite A") 

1091 
case True thus ?thesis using nn 

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

1094 
apply (blast intro: add_mono) 

1095 
done 

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

1098 
qed 

15402  1099 

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

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

1103 
proof (cases "finite A") 

1104 
case True thus ?thesis using np 

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

1107 
apply (blast intro: add_mono) 

1108 
done 

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

1111 
qed 

15402  1112 

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

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

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

1117 
proof  

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

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

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

1121 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1123 
finally show ?thesis . 

1124 
qed 

15542  1125 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1126 
lemma setsum_mono3: "finite B ==> A <= B ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1127 
ALL x: B  A. 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1128 
0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==> 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1129 
setsum f A <= setsum f B" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1130 
apply (subgoal_tac "setsum f B = setsum f A + setsum f (B  A)") 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1131 
apply (erule ssubst) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1132 
apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B  A)") 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1133 
apply simp 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1134 
apply (rule add_left_mono) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1135 
apply (erule setsum_nonneg) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1136 
apply (subst setsum_Un_disjoint [THEN sym]) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1137 
apply (erule finite_subset, assumption) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1138 
apply (rule finite_subset) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1139 
prefer 2 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1140 
apply assumption 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1141 
apply auto 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1142 
apply (rule setsum_cong) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1143 
apply auto 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1144 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1145 

15837  1146 
(* FIXME: this is distributitivty, name as such! *) 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1147 
(* suggested name: setsum_right_distrib (CB) *) 
15837  1148 

15402  1149 
lemma setsum_mult: 
1150 
fixes f :: "'a => ('b::semiring_0_cancel)" 

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

1152 
proof (cases "finite A") 

1153 
case True 

1154 
thus ?thesis 

1155 
proof (induct) 

1156 
case empty thus ?case by simp 

1157 
next 

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

1159 
qed 

1160 
next 

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

1162 
qed 

1163 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1164 
lemma setsum_left_distrib: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1165 
"setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1166 
proof (cases "finite A") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1167 
case True 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1168 
then show ?thesis 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1169 
proof induct 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1170 
case empty thus ?case by simp 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1171 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1172 
case (insert x A) thus ?case by (simp add: left_distrib) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1173 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1174 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1175 
case False thus ?thesis by (simp add: setsum_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1176 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1177 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1178 
lemma setsum_divide_distrib: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1179 
"setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1180 
proof (cases "finite A") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1181 
case True 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1182 
then show ?thesis 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1183 
proof induct 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1184 
case empty thus ?case by simp 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1185 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1186 
case (insert x A) thus ?case by (simp add: add_divide_distrib) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1187 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1188 
next 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1189 
case False thus ?thesis by (simp add: setsum_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1190 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1191 

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

15535  1195 
proof (cases "finite A") 
1196 
case True 

1197 
thus ?thesis 

1198 
proof (induct) 

1199 
case empty thus ?case by simp 

1200 
next 

1201 
case (insert x A) 

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

1203 
qed 

15402  1204 
next 
15535  1205 
case False thus ?thesis by (simp add: setsum_def) 
15402  1206 
qed 
1207 

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

15535  1211 
proof (cases "finite A") 
1212 
case True 

1213 
thus ?thesis 

1214 
proof (induct) 

1215 
case empty thus ?case by simp 

1216 
next 

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

1218 
qed 

15402  1219 
next 
15535  1220 
case False thus ?thesis by (simp add: setsum_def) 
15402  1221 
qed 
1222 

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

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

1226 
proof (cases "finite A") 

1227 
case True 

1228 
thus ?thesis 

1229 
proof (induct) 

1230 
case empty thus ?case by simp 

1231 
next 

1232 
case (insert a A) 

1233 
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 

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

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1235 
also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16760
diff
changeset

1236 
by (simp del: abs_of_nonneg) 
15539  1237 
also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp 
1238 
finally show ?case . 

1239 
qed 

1240 
next 

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

1242 
qed 

1243 

15402  1244 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1245 
text {* Commuting outer and inner summation *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1246 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1247 
lemma swap_inj_on: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1248 
"inj_on (%(i, j). (j, i)) (A \<times> B)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1249 
by (unfold inj_on_def) fast 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1250 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1251 
lemma swap_product: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1252 
"(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1253 
by (simp add: split_def image_def) blast 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1254 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1255 
lemma setsum_commute: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1256 
"(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1257 
proof (simp add: setsum_cartesian_product) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1258 
have "(\<Sum>z\<in>A \<times> B. f (fst z) (snd z)) = 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1259 
(\<Sum>z\<in>(%(i, j). (j, i)) ` (A \<times> B). f (snd z) (fst z))" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1260 
(is "?s = _") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1261 
apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1262 
apply (simp add: split_def) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1263 
done 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1264 
also have "... = (\<Sum>z\<in>B \<times> A. f (snd z) (fst z))" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1265 
(is "_ = ?t") 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1266 
apply (simp add: swap_product) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1267 
done 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1268 
finally show "?s = ?t" . 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1269 
qed 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1270 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

1271 

15402  1272 
subsection {* Generalized product over a set *} 
1273 

1274 
constdefs 

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

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

1277 

1278 
syntax 

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

1282 
syntax (HTML output) 

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

16550  1284 

1285 
translations  {* Beware of argument permutation! *} 

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

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

1288 

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

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

1291 

1292 
syntax 

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

1294 
syntax (xsymbols) 

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

1296 
syntax (HTML output) 

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

1298 

15402  1299 
translations 
16550  1300 
"PROD xP. t" => "setprod (%x. t) {x. P}" 
1301 
"\<Prod>xP. t" => "setprod (%x. t) {x. P}" 

1302 

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

15402  1304 

1305 
syntax 

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

1307 

1308 
parse_translation {* 

1309 
let 

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

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

1312 
*} 

1313 
print_translation {* 

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

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

1316 
in 

1317 
[("setprod", setprod_tr')] 

1318 
end 

1319 
*} 

1320 

1321 

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

1323 
by (auto simp add: setprod_def) 

1324 

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

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

15765  1327 
by (simp add: setprod_def) 
15402  1328 

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

1329 
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

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

1331 

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

15765  1334 
by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD) 
15402  1335 

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

1337 
by (auto simp add: setprod_reindex) 

1338 

1339 
lemma setprod_cong: 

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

15765  1341 
by(fastsimp simp: setprod_def intro: AC_mult.fold_cong) 
15402  1342 

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

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

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

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

1346 

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

1349 
by (frule setprod_reindex, simp) 

1350 

1351 

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

1353 
apply (case_tac "finite A") 

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

1355 
done 
