author  huffman 
Tue, 01 Jul 2008 20:26:48 +0200  
changeset 27430  1e25ac05cd87 
parent 27418  564117b58d73 
child 27611  2c01c0bdb385 
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 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26465
diff
changeset

10 
imports Divides Transitive_Closure 
15131  11 
begin 
12396  12 

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

23736  15 
inductive finite :: "'a set => bool" 
22262  16 
where 
17 
emptyI [simp, intro!]: "finite {}" 

18 
 insertI [simp, intro!]: "finite A ==> finite (insert a A)" 

12396  19 

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

23 
proof  

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

25 
thus ?thesis by blast 

26 
qed 

12396  27 

22262  28 
lemma finite_induct [case_names empty insert, induct set: finite]: 
12396  29 
"finite F ==> 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

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

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

34 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  35 
assume "finite F" 
36 
thus "P F" 

37 
proof induct 

23389  38 
show "P {}" by fact 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

39 
fix x F assume F: "finite F" and P: "P F" 
12396  40 
show "P (insert x F)" 
41 
proof cases 

42 
assume "x \<in> F" 

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

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

45 
next 

46 
assume "x \<notin> F" 

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

48 
qed 

49 
qed 

50 
qed 

51 

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

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

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

56 
\<Longrightarrow> P F" 

57 
using fin 

58 
proof induct 

59 
case empty thus ?case by simp 

60 
next 

61 
case (insert x F) 

62 
show ?case 

63 
proof cases 

23389  64 
assume "F = {}" 
65 
thus ?thesis using `P {x}` by simp 

15484  66 
next 
23389  67 
assume "F \<noteq> {}" 
68 
thus ?thesis using insert by blast 

15484  69 
qed 
70 
qed 

71 

12396  72 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 
23389  73 
assumes "finite F" and "F \<subseteq> A" 
74 
and empty: "P {}" 

75 
and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 

76 
shows "P F" 

12396  77 
proof  
23389  78 
from `finite F` and `F \<subseteq> A` 
79 
show ?thesis 

12396  80 
proof induct 
23389  81 
show "P {}" by fact 
82 
next 

83 
fix x F 

84 
assume "finite F" and "x \<notin> F" and 

85 
P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 

12396  86 
show "P (insert x F)" 
87 
proof (rule insert) 

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

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

90 
with P show "P F" . 

23389  91 
show "finite F" by fact 
92 
show "x \<notin> F" by fact 

12396  93 
qed 
94 
qed 

95 
qed 

96 

23878  97 

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

15510  100 
lemma finite_imp_nat_seg_image_inj_on: 
101 
assumes fin: "finite A" 

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

15392  103 
using fin 
104 
proof induct 

105 
case empty 

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

108 
qed 

15392  109 
next 
110 
case (insert a A) 

23389  111 
have notinA: "a \<notin> A" by fact 
15510  112 
from insert.hyps obtain n f 
113 
where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast 

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

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

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

15392  117 
thus ?case by blast 
118 
qed 

119 

120 
lemma nat_seg_image_imp_finite: 

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

122 
proof (induct n) 

123 
case 0 thus ?case by simp 

124 
next 

125 
case (Suc n) 

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

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

128 
show ?case 

129 
proof cases 

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

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

132 
thus ?thesis using finB by simp 

133 
next 

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

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

136 
thus ?thesis using finB by simp 

137 
qed 

138 
qed 

139 

140 
lemma finite_conv_nat_seg_image: 

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

15510  142 
by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 
15392  143 

26441  144 

15392  145 
subsubsection{* Finiteness and set theoretic constructions *} 
146 

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

22262  149 
by (induct set: finite) simp_all 
12396  150 

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

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

153 
proof  

154 
assume "finite B" 

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

156 
proof induct 

157 
case empty 

158 
thus ?case by simp 

159 
next 

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

160 
case (insert x F A) 
23389  161 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" by fact+ 
12396  162 
show "finite A" 
163 
proof cases 

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

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

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

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

23389  168 
also have "insert x (A  {x}) = A" using x by (rule insert_Diff) 
12396  169 
finally show ?thesis . 
170 
next 

23389  171 
show "A \<subseteq> F ==> ?thesis" by fact 
12396  172 
assume "x \<notin> A" 
173 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

174 
qed 

175 
qed 

176 
qed 

177 

18423  178 
lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}" 
17761  179 
using finite_subset[of "{x \<in> A. P x}" "A"] by blast 
180 

12396  181 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 
182 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

183 

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

185 
 {* The converse obviously fails. *} 

186 
by (blast intro: finite_subset) 

187 

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

189 
apply (subst insert_is_Un) 

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

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

195 
by (induct rule:finite_induct) simp_all 

196 

12396  197 
lemma finite_empty_induct: 
23389  198 
assumes "finite A" 
199 
and "P A" 

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

201 
shows "P {}" 

12396  202 
proof  
203 
have "P (A  A)" 

204 
proof  

23389  205 
{ 
206 
fix c b :: "'a set" 

207 
assume c: "finite c" and b: "finite b" 

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

209 
have "c \<subseteq> b ==> P (b  c)" 

210 
using c 

211 
proof induct 

212 
case empty 

213 
from P1 show ?case by simp 

214 
next 

215 
case (insert x F) 

216 
have "P (b  F  {x})" 

217 
proof (rule P2) 

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

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

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

221 
qed 

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

223 
finally show ?case . 

12396  224 
qed 
23389  225 
} 
226 
then show ?thesis by this (simp_all add: assms) 

12396  227 
qed 
23389  228 
then show ?thesis by simp 
12396  229 
qed 
230 

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

232 
by (rule Diff_subset [THEN finite_subset]) 

233 

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

235 
apply (subst Diff_insert) 

236 
apply (case_tac "a : A  B") 

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

14208  238 
apply (subst insert_Diff, simp_all) 
12396  239 
done 
240 

19870  241 
lemma finite_Diff_singleton [simp]: "finite (A  {a}) = finite A" 
242 
by simp 

243 

12396  244 

15392  245 
text {* Image and Inverse Image over Finite Sets *} 
13825  246 

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

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

22262  249 
by (induct set: finite) simp_all 
13825  250 

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

251 
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

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

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

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

255 

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

27418  258 
apply (drule finite_imageI, simp add: range_composition) 
13825  259 
done 
260 

12396  261 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
262 
proof  

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

264 
fix B :: "'a set" 

265 
assume "finite B" 

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

267 
apply induct 

268 
apply simp 

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

270 
apply clarify 

271 
apply (simp (no_asm_use) add: inj_on_def) 

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

277 
done 

278 
qed (rule refl) 

279 

280 

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

283 
is included in a singleton. *} 

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

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

285 
apply (blast intro: the_equality [symmetric]) 
13825  286 
done 
287 

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

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

290 
is finite. *} 

22262  291 
apply (induct set: finite) 
21575  292 
apply simp_all 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

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

294 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  295 
done 
296 

297 

15392  298 
text {* The finite UNION of finite sets *} 
12396  299 

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

22262  301 
by (induct set: finite) simp_all 
12396  302 

303 
text {* 

304 
Strengthen RHS to 

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

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

307 
We'd need to prove 

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

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

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

312 
by (blast intro: finite_UN_I finite_subset) 

313 

314 

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

317 

15392  318 
text {* Sigma of finite sets *} 
12396  319 

320 
lemma finite_SigmaI [simp]: 

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

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

323 

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

326 
by (rule finite_SigmaI) 

327 

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

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

331 
apply (erule ssubst) 

14208  332 
apply (erule finite_SigmaI, auto) 
12396  333 
done 
334 

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

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

336 
"[ finite (A <*> B); B \<noteq> {} ] ==> finite A" 
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="fst 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 y x) 
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 
lemma finite_cartesian_productD2: 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

352 
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

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

354 
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

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

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

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

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

359 
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

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

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

362 
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

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

364 

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

365 

15392  366 
text {* The powerset of a finite set *} 
12396  367 

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

369 
proof 

370 
assume "finite (Pow A)" 

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

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

373 
next 

374 
assume "finite A" 

375 
thus "finite (Pow A)" 

376 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

377 
qed 

378 

15392  379 

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

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

382 

383 

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

386 
apply simp 

387 
apply (rule iffI) 

388 
apply (erule finite_imageD [unfolded inj_on_def]) 

389 
apply (simp split add: split_split) 

390 
apply (erule finite_imageI) 

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

394 
apply simp 

395 
done 

396 

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

397 

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

12396  400 

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

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

22262  403 
apply (induct set: finite) 
12396  404 
apply (auto simp add: Field_def Domain_insert Range_insert) 
405 
done 

406 

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

408 
apply clarify 

409 
apply (erule trancl_induct) 

410 
apply (auto simp add: Field_def) 

411 
done 

412 

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

414 
apply auto 

415 
prefer 2 

416 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

417 
apply (rule finite_SigmaI) 

418 
prefer 3 

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

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

422 

423 

26441  424 
subsection {* Class @{text finite} *} 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

425 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

426 
setup {* Sign.add_path "finite" *}  {*FIXME: name tweaking*} 
26441  427 
class finite = itself + 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

428 
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

429 
setup {* Sign.parent_path *} 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

430 
hide const finite 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

431 

27430  432 
context finite 
433 
begin 

434 

435 
lemma finite [simp]: "finite (A \<Colon> 'a set)" 

26441  436 
by (rule subset_UNIV finite_UNIV finite_subset)+ 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

437 

27430  438 
end 
439 

26146  440 
lemma UNIV_unit [noatp]: 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

441 
"UNIV = {()}" by auto 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

442 

26146  443 
instance unit :: finite 
444 
by default (simp add: UNIV_unit) 

445 

446 
lemma UNIV_bool [noatp]: 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

447 
"UNIV = {False, True}" by auto 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

448 

26146  449 
instance bool :: finite 
450 
by default (simp add: UNIV_bool) 

451 

452 
instance * :: (finite, finite) finite 

453 
by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 

454 

455 
instance "+" :: (finite, finite) finite 

456 
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 

457 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

458 
lemma inj_graph: "inj (%f. {(x, y). y = f x})" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

459 
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

460 

26146  461 
instance "fun" :: (finite, finite) finite 
462 
proof 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

463 
show "finite (UNIV :: ('a => 'b) set)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

464 
proof (rule finite_imageD) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

465 
let ?graph = "%f::'a => 'b. {(x, y). y = f x}" 
26792  466 
have "range ?graph \<subseteq> Pow UNIV" by simp 
467 
moreover have "finite (Pow (UNIV :: ('a * 'b) set))" 

468 
by (simp only: finite_Pow_iff finite) 

469 
ultimately show "finite (range ?graph)" 

470 
by (rule finite_subset) 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

471 
show "inj ?graph" by (rule inj_graph) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

472 
qed 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

473 
qed 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

474 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

475 

15392  476 
subsection {* A fold functional for finite sets *} 
477 

478 
text {* The intended behaviour is 

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

482 
*} 

483 

23736  484 
inductive 
22262  485 
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool" 
486 
for f :: "'a => 'a => 'a" 

487 
and g :: "'b => 'a" 

488 
and z :: 'a 

489 
where 

490 
emptyI [intro]: "foldSet f g z {} z" 

491 
 insertI [intro]: 

492 
"\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk> 

493 
\<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)" 

494 

23736  495 
inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x" 
15392  496 

497 
constdefs 

21733  498 
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" 
22262  499 
"fold f g z A == THE x. foldSet f g z A x" 
15392  500 

15498  501 
text{*A tempting alternative for the definiens is 
22262  502 
@{term "if finite A then THE x. foldSet f g e A x else e"}. 
15498  503 
It allows the removal of finiteness assumptions from the theorems 
504 
@{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. 

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

506 

507 

15392  508 
lemma Diff1_foldSet: 
22262  509 
"foldSet f g z (A  {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)" 
15392  510 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 
511 

22262  512 
lemma foldSet_imp_finite: "foldSet f g z A x==> finite A" 
15392  513 
by (induct set: foldSet) auto 
514 

22262  515 
lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x" 
516 
by (induct set: finite) auto 

15392  517 

518 

519 
subsubsection{*From @{term foldSet} to @{term fold}*} 

520 

15510  521 
lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})" 
19868  522 
by (auto simp add: less_Suc_eq) 
15510  523 

524 
lemma insert_image_inj_on_eq: 

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

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

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

528 
apply (auto simp add: image_less_Suc inj_on_def) 

529 
apply (blast intro: less_trans) 

530 
done 

531 

532 
lemma insert_inj_onE: 

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

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

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

536 
proof (cases n) 

537 
case 0 thus ?thesis using aA by auto 

538 
next 

539 
case (Suc m) 

23389  540 
have nSuc: "n = Suc m" by fact 
15510  541 
have mlessn: "m<n" by (simp add: nSuc) 
15532  542 
from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE) 
27165  543 
let ?hm = "Fun.swap k m h" 
15520  544 
have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
545 
by (simp add: inj_on_swap_iff inj_on) 

15510  546 
show ?thesis 
15520  547 
proof (intro exI conjI) 
548 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

552 
proof (rule insert_image_inj_on_eq) 

27165  553 
show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp 
15520  554 
show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
555 
show "insert (?hm m) A = ?hm ` {i. i < Suc m}" 

556 
using aA hkeq nSuc klessn 

557 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

558 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  559 
qed 
560 
qed 

561 
qed 

562 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

563 
context ab_semigroup_mult 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

564 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

565 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

566 
lemma foldSet_determ_aux: 
15510  567 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

568 
foldSet times g z A x; foldSet times g z A x' \<rbrakk> 
15392  569 
\<Longrightarrow> x' = x" 
15510  570 
proof (induct n rule: less_induct) 
571 
case (less n) 

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

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

574 
foldSet times g z A x; foldSet times g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

575 
have Afoldx: "foldSet times g z A x" and Afoldx': "foldSet times g z A x'" 
23389  576 
and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+ 
15510  577 
show ?case 
578 
proof (rule foldSet.cases [OF Afoldx]) 

22262  579 
assume "A = {}" and "x = z" 
15510  580 
with Afoldx' show "x' = x" by blast 
15392  581 
next 
15510  582 
fix B b u 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

583 
assume AbB: "A = insert b B" and x: "x = g b * u" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

584 
and notinB: "b \<notin> B" and Bu: "foldSet times g z B u" 
15510  585 
show "x'=x" 
586 
proof (rule foldSet.cases [OF Afoldx']) 

22262  587 
assume "A = {}" and "x' = z" 
15510  588 
with AbB show "x' = x" by blast 
15392  589 
next 
15510  590 
fix C c v 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

591 
assume AcC: "A = insert c C" and x': "x' = g c * v" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

592 
and notinC: "c \<notin> C" and Cv: "foldSet times g z C v" 
15510  593 
from A AbB have Beq: "insert b B = h`{i. i<n}" by simp 
594 
from insert_inj_onE [OF Beq notinB injh] 

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

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

597 
and lessB: "mB < n" by auto 

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

599 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

602 
and lessC: "mC < n" by auto 

603 
show "x'=x" 

15392  604 
proof cases 
15510  605 
assume "b=c" 
606 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

608 
by auto 

15392  609 
next 
610 
assume diff: "b \<noteq> c" 

611 
let ?D = "B  {c}" 

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

15510  613 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  614 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  615 
with AbB have "finite ?D" by simp 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

616 
then obtain d where Dfoldd: "foldSet times g z ?D d" 
17589  617 
using finite_imp_foldSet by iprover 
15506  618 
moreover have cinB: "c \<in> B" using B by auto 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

619 
ultimately have "foldSet times g z B (g c * d)" 
15392  620 
by(rule Diff1_foldSet) 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

621 
then have "g c * d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

622 
then have "u = g c * d" .. 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

623 
moreover have "v = g b * d" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

624 
proof (rule sym, rule IH [OF lessC Ceq inj_onC Cv]) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

625 
show "foldSet times g z C (g b * d)" using C notinB Dfoldd 
15392  626 
by fastsimp 
627 
qed 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

628 
ultimately show ?thesis using x x' 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

629 
by (simp add: mult_left_commute) 
15392  630 
qed 
631 
qed 

632 
qed 

633 
qed 

634 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

635 
lemma foldSet_determ: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

636 
"foldSet times g z A x ==> foldSet times g z A y ==> y = x" 
15510  637 
apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
638 
apply (blast intro: foldSet_determ_aux [rule_format]) 

15392  639 
done 
640 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

641 
lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y" 
15392  642 
by (unfold fold_def) (blast intro: foldSet_determ) 
643 

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

645 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

646 
lemma (in ) fold_empty [simp]: "fold f g z {} = z" 
15392  647 
by (unfold fold_def) blast 
648 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

649 
lemma fold_insert_aux: "x \<notin> A ==> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

650 
(foldSet times g z (insert x A) v) = 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

651 
(EX y. foldSet times g z A y & v = g x * y)" 
15392  652 
apply auto 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

653 
apply (rule_tac A1 = A and f1 = times in finite_imp_foldSet [THEN exE]) 
15392  654 
apply (fastsimp dest: foldSet_imp_finite) 
655 
apply (blast intro: foldSet_determ) 

656 
done 

657 

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

659 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

660 
lemma fold_insert [simp]: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

661 
"finite A ==> x \<notin> A ==> fold times g z (insert x A) = g x * fold times g z A" 
15392  662 
apply (unfold fold_def) 
663 
apply (simp add: fold_insert_aux) 

664 
apply (rule the_equality) 

665 
apply (auto intro: finite_imp_foldSet 

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

667 
done 

668 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

669 
lemma fold_rec: 
15535  670 
assumes fin: "finite A" and a: "a:A" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

671 
shows "fold times g z A = g a * fold times g z (A  {a})" 
15535  672 
proof 
673 
have A: "A = insert a (A  {a})" using a by blast 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

674 
hence "fold times g z A = fold times g z (insert a (A  {a}))" by simp 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

675 
also have "\<dots> = g a * fold times g z (A  {a})" 
15535  676 
by(rule fold_insert) (simp add:fin)+ 
677 
finally show ?thesis . 

678 
qed 

679 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

680 
end 
15392  681 

15480  682 
text{* A simplified version for idempotent functions: *} 
683 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

684 
context ab_semigroup_idem_mult 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

685 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

686 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

687 
lemma fold_insert_idem: 
15480  688 
assumes finA: "finite A" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

689 
shows "fold times g z (insert a A) = g a * fold times g z A" 
15480  690 
proof cases 
691 
assume "a \<in> A" 

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

693 
by(blast dest: mk_disjoint_insert) 

694 
show ?thesis 

695 
proof  

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

697 
have "fold times g z (insert a A) = fold times g z (insert a B)" using A by simp 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

698 
also have "\<dots> = g a * fold times g z B" 
15506  699 
using finB disj by simp 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

700 
also have "\<dots> = g a * fold times g z A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

701 
using A finB disj 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

702 
by (simp add: mult_idem mult_assoc [symmetric]) 
15480  703 
finally show ?thesis . 
704 
qed 

705 
next 

706 
assume "a \<notin> A" 

707 
with finA show ?thesis by simp 

708 
qed 

709 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

710 
lemma foldI_conv_id: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

711 
"finite A \<Longrightarrow> fold times g z A = fold times id z (g ` A)" 
15509  712 
by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert) 
15484  713 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

714 
end 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

715 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

718 
context ab_semigroup_mult 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

719 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

720 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

721 
lemma fold_commute: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

722 
"finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" 
22262  723 
apply (induct set: finite) 
21575  724 
apply simp 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

725 
apply (simp add: mult_left_commute [of x]) 
15392  726 
done 
727 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

728 
lemma fold_nest_Un_Int: 
15392  729 
"finite A ==> finite B 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

730 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  731 
apply (induct set: finite) 
21575  732 
apply simp 
15392  733 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
734 
done 

735 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

736 
lemma fold_nest_Un_disjoint: 
15392  737 
"finite A ==> finite B ==> A Int B = {} 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

738 
==> fold times g z (A Un B) = fold times g (fold times g z B) A" 
15392  739 
by (simp add: fold_nest_Un_Int) 
740 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

741 
lemma fold_reindex: 
15487  742 
assumes fin: "finite A" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

743 
shows "inj_on h A \<Longrightarrow> fold times g z (h ` A) = fold times (g \<circ> h) z A" 
15506  744 
using fin apply induct 
15392  745 
apply simp 
746 
apply simp 

747 
done 

748 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

749 
text{* 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

750 
Fusion theorem, as described in Graham Hutton's paper, 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

751 
A Tutorial on the Universality and Expressiveness of Fold, 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

752 
JFP 9:4 (355372), 1999. 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

753 
*} 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

754 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

755 
lemma fold_fusion: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

756 
includes ab_semigroup_mult g 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

757 
assumes fin: "finite A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

758 
and hyp: "\<And>x y. h (g x y) = times x (h y)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

759 
shows "h (fold g j w A) = fold times j (h w) A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

760 
using fin hyp by (induct set: finite) simp_all 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

761 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

762 
lemma fold_cong: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

763 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

764 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold times g z C = fold times h z C") 
15392  765 
apply simp 
766 
apply (erule finite_induct, simp) 

767 
apply (simp add: subset_insert_iff, clarify) 

768 
apply (subgoal_tac "finite C") 

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

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

771 
prefer 2 apply blast 

772 
apply (erule ssubst) 

773 
apply (drule spec) 

774 
apply (erule (1) notE impE) 

775 
apply (simp add: Ball_def del: insert_Diff_single) 

776 
done 

777 

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

778 
end 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

779 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

780 
context comm_monoid_mult 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

781 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

782 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

783 
lemma fold_Un_Int: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

784 
"finite A ==> finite B ==> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

785 
fold times g 1 A * fold times g 1 B = 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

786 
fold times g 1 (A Un B) * fold times g 1 (A Int B)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

787 
by (induct set: finite) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

788 
(auto simp add: mult_ac insert_absorb Int_insert_left) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

789 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

790 
corollary fold_Un_disjoint: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

791 
"finite A ==> finite B ==> A Int B = {} ==> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

792 
fold times g 1 (A Un B) = fold times g 1 A * fold times g 1 B" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

793 
by (simp add: fold_Un_Int) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

794 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

795 
lemma fold_UN_disjoint: 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

796 
"\<lbrakk> finite I; ALL i:I. finite (A i); 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

797 
ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {} \<rbrakk> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

798 
\<Longrightarrow> fold times g 1 (UNION I A) = 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

799 
fold times (%i. fold times g 1 (A i)) 1 I" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

800 
apply (induct set: finite, simp, atomize) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

801 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

802 
prefer 2 apply blast 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

803 
apply (subgoal_tac "A x Int UNION F A = {}") 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

804 
prefer 2 apply blast 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

805 
apply (simp add: fold_Un_disjoint) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

806 
done 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

807 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

808 
lemma fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

809 
fold times (%x. fold times (g x) 1 (B x)) 1 A = 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

810 
fold times (split g) 1 (SIGMA x:A. B x)" 
15392  811 
apply (subst Sigma_def) 
15506  812 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  813 
apply blast 
814 
apply (erule fold_cong) 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

820 
lemma fold_distrib: "finite A \<Longrightarrow> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

821 
fold times (%x. g x * h x) 1 A = fold times g 1 A * fold times h 1 A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

822 
by (erule finite_induct) (simp_all add: mult_ac) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

823 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

824 
end 
22917  825 

826 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

829 
interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"] 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

830 
by unfold_locales (auto intro: add_assoc add_commute) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

831 

15402  832 
constdefs 
833 
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" 

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

835 

19535  836 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21249
diff
changeset

837 
Setsum ("\<Sum>_" [1000] 999) where 
19535  838 
"\<Sum>A == setsum (%x. x) A" 
839 

15402  840 
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is 
841 
written @{text"\<Sum>x\<in>A. e"}. *} 

842 

843 
syntax 

17189  844 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  845 
syntax (xsymbols) 
17189  846 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  847 
syntax (HTML output) 
17189  848 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  849 

850 
translations  {* Beware of argument permutation! *} 

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

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

853 

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

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

856 

857 
syntax 

17189  858 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  859 
syntax (xsymbols) 
17189  860 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  861 
syntax (HTML output) 
17189  862 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  863 

864 
translations 

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

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

867 

868 
print_translation {* 

869 
let 

19535  870 
fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
871 
if x<>y then raise Match 

872 
else let val x' = Syntax.mark_bound x 

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

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

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

876 
in [("setsum", setsum_tr')] end 

15402  877 
*} 
878 

19535  879 

15402  880 
lemma setsum_empty [simp]: "setsum f {} = 0" 
881 
by (simp add: setsum_def) 

882 

883 
lemma setsum_insert [simp]: 

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

15765  885 
by (simp add: setsum_def) 
15402  886 

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

887 
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

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

889 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

892 
by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD) 
15402  893 

894 
lemma setsum_reindex_id: 

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

896 
by (auto simp add: setsum_reindex) 

897 

898 
lemma setsum_cong: 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

900 
by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong) 
15402  901 

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

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

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

904 
==> setsum (%x. f x) A = setsum (%x. g x) B" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

906 

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

909 

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

914 

15542  915 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  916 
apply (clarsimp simp: setsum_def) 
15765  917 
apply (erule finite_induct, auto) 
15402  918 
done 
919 

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

15402  922 

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

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

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

926 
by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric]) 
15402  927 

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

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

930 
by (subst setsum_Un_Int [symmetric], auto) 

931 

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

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

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

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

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

938 
by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong) 
15402  939 

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

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

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

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

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

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

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

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

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

950 
done 
15402  951 

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

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

953 
the rhs need not be, since SIGMA A B could still be finite.*) 
15402  954 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
17189  955 
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

956 
by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong) 
15402  957 

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

958 
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

959 
lemma setsum_cartesian_product: 
17189  960 
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)" 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

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

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

968 
done 
15402  969 

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

26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

971 
by(simp add:setsum_def comm_monoid_add.fold_distrib) 
15402  972 

973 

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

975 

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

977 
apply (case_tac "finite A") 

978 
prefer 2 apply (simp add: setsum_def) 

979 
apply (erule rev_mp) 

980 
apply (erule finite_induct, auto) 

981 
done 

982 

983 
lemma setsum_eq_0_iff [simp]: 

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

22262  985 
by (induct set: finite) auto 
15402  986 

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

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

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

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

990 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  991 

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

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

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

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

995 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  996 

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

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

999 
apply (case_tac "finite A") 

1000 
prefer 2 apply (simp add: setsum_def) 

1001 
apply (erule finite_induct) 

1002 
apply (auto simp add: insert_Diff_if) 

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

1004 
done 

1005 

1006 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1010 

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

1011 
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

1012 
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

1013 
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

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

1015 

15402  1016 
(* By Jeremy Siek: *) 
1017 

1018 
lemma setsum_diff_nat: 

19535  1019 
assumes "finite B" 
1020 
and "B \<subseteq> A" 

1021 
shows "(setsum f (A  B) :: nat) = (setsum f A)  (setsum f B)" 

1022 
using prems 

1023 
proof induct 

15402  1024 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 
1025 
next 

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

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

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

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

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

1031 
by (simp add: setsum_diff1_nat) 

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

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

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

1035 
by simp 

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

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

1038 
by simp 

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

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

1041 
by simp 

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

1043 
qed 

1044 

1045 
lemma setsum_diff: 

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

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

1048 
proof  

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

1050 
show ?thesis using finiteB le 

21575  1051 
proof induct 
19535  1052 
case empty 
1053 
thus ?case by auto 

1054 
next 

1055 
case (insert x F) 

1056 
thus ?case using le finiteB 

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

15402  1058 
qed 
19535  1059 
qed 
15402  1060 

1061 
lemma setsum_mono: 

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

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

1064 
proof (cases "finite K") 

1065 
case True 

1066 
thus ?thesis using le 

19535  1067 
proof induct 
15402  1068 
case empty 
1069 
thus ?case by simp 

1070 
next 

1071 
case insert 

19535  1072 
thus ?case using add_mono by fastsimp 
15402  1073 
qed 
1074 
next 

1075 
case False 

1076 
thus ?thesis 

1077 
by (simp add: setsum_def) 

1078 
qed 

1079 

15554  1080 
lemma setsum_strict_mono: 
19535  1081 
fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" 
1082 
assumes "finite A" "A \<noteq> {}" 

1083 
and "!!x. x:A \<Longrightarrow> f x < g x" 

1084 
shows "setsum f A < setsum g A" 

1085 
using prems 

15554  1086 
proof (induct rule: finite_ne_induct) 
1087 
case singleton thus ?case by simp 

1088 
next 

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

1090 
qed 

1091 

15535  1092 
lemma setsum_negf: 
19535  1093 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  1094 
proof (cases "finite A") 
22262  1095 
case True thus ?thesis by (induct set: finite) auto 
15535  1096 
next 
1097 
case False thus ?thesis by (simp add: setsum_def) 

1098 
qed 

15402  1099 

15535  1100 
lemma setsum_subtractf: 
19535  1101 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
1102 
setsum f A  setsum g A" 

15535  1103 
proof (cases "finite A") 
1104 
case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) 

1105 
next 

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

1107 
qed 

15402  1108 

15535  1109 
lemma setsum_nonneg: 
19535  1110 
assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" 
1111 
shows "0 \<le> setsum f A" 

15535  1112 
proof (cases "finite A") 
1113 
case True thus ?thesis using nn 

21575  1114 
proof induct 
19535  1115 
case empty then show ?case by simp 
1116 
next 

1117 
case (insert x F) 

1118 
then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono) 

1119 
with insert show ?case by simp 

1120 
qed 

15535  1121 
next 
1122 
case False thus ?thesis by (simp add: setsum_def) 

1123 
qed 

15402  1124 

15535  1125 
lemma setsum_nonpos: 
19535  1126 
assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" 
1127 
shows "setsum f A \<le> 0" 

15535  1128 
proof (cases "finite A") 
1129 
case True thus ?thesis using np 

21575  1130 
proof induct 
19535  1131 
case empty then show ?case by simp 
1132 
next 

1133 
case (insert x F) 

1134 
then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono) 

1135 
with insert show ?case by simp 

1136 
qed 

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

1139 
qed 

15402  1140 

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

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

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

1145 
proof  

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

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

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

1149 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1151 
finally show ?thesis . 

1152 
qed 

15542  1153 

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

1154 
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

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

1156 
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

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

1158 
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

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

1160 
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

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

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

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

1164 
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

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

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

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

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

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

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

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

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

1173 

19279  1174 
lemma setsum_right_distrib: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

1175 
fixes f :: "'a => ('b::semiring_0)" 
15402  1176 
shows "r * setsum f A = setsum (%n. r * f n) A" 
1177 
proof (cases "finite A") 

1178 
case True 

1179 
thus ?thesis 

21575  1180 
proof induct 
15402  1181 
case empty thus ?case by simp 
1182 
next 

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

1184 
qed 

1185 
next 

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

1187 
qed 

1188 

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

1189 
lemma setsum_left_distrib: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

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

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

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

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

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

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

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

1197 
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

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

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

1200 
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

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

1202 

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

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

1204 
"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

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

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

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

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

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

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

1211 
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

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

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

1214 
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

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

1216 

15535  1217 
lemma setsum_abs[iff]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25205
diff
changeset

1218 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1219 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  1220 
proof (cases "finite A") 
1221 
case True 

1222 
thus ?thesis 

21575  1223 
proof induct 
15535  1224 
case empty thus ?case by simp 
1225 
next 

1226 
case (insert x A) 

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

1228 
qed 

15402  1229 
next 
15535  1230 
case False thus ?thesis by (simp add: setsum_def) 
15402  1231 
qed 
1232 

15535  1233 
lemma setsum_abs_ge_zero[iff]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25205
diff
changeset

1234 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1235 
shows "0 \<le> setsum (%i. abs(f i)) A" 
15535  1236 
proof (cases "finite A") 
1237 
case True 

1238 
thus ?thesis 

21575  1239 
proof induct 
15535  1240 
case empty thus ?case by simp 
1241 
next 

21733  1242 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  1243 
qed 
15402  1244 
next 
15535  1245 
case False thus ?thesis by (simp add: setsum_def) 
15402  1246 
qed 
1247 

15539  1248 
lemma abs_setsum_abs[simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25205
diff
changeset

1249 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15539  1250 
shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" 
1251 
proof (cases "finite A") 

1252 
case True 

1253 
thus ?thesis 

21575  1254 
proof induct 
15539  1255 
case empty thus ?case by simp 
1256 
next 

1257 
case (insert a A) 

1258 
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 

1259 
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

1260 
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

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

1264 
qed 

1265 
next 

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

1267 
qed 

1268 

15402  1269 

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

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

1271 

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

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

1273 
"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

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

1275 

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

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

1277 
"(%(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

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

1279 

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

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

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

1282 
proof (simp add: setsum_cartesian_product) 
17189  1283 
have "(\<Sum>(x,y) \<in> A <*> B. f x y) = 
1284 
(\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)" 

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

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

1286 
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

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

1288 
done 
17189  1289 
also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)" 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
17085
diff
changeset

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

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

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

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

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

1295 

19279  1296 
lemma setsum_product: 
22934
64ecb3d6790a
generalize setsum lemmas from semiring_0_cancel to semiring_0
huffman
parents:
22917
diff
changeset

1297 
fixes f :: "'a => ('b::semiring_0)" 
19279  1298 
shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" 
1299 
by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute) 
