author  haftmann 
Mon, 17 Nov 2008 17:00:55 +0100  
changeset 28823  dcbef866c9e2 
parent 27981  feb0c01cf0fb 
child 28853  69eb69659bf3 
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 
27981  10 
imports Datatype 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  

28823  24 
from assms have "A \<noteq> UNIV" by blast 
14661  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 

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

455 
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

456 
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

457 

26146  458 
instance "fun" :: (finite, finite) finite 
459 
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

460 
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

461 
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

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

465 
by (simp only: finite_Pow_iff finite) 

466 
ultimately show "finite (range ?graph)" 

467 
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

468 
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

469 
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

470 
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

471 

27981  472 
instance "+" :: (finite, finite) finite 
473 
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 

474 

475 
instance option :: (finite) finite 

476 
by default (simp add: insert_None_conv_UNIV [symmetric]) 

477 

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

478 

15392  479 
subsection {* A fold functional for finite sets *} 
480 

481 
text {* The intended behaviour is 

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

485 
*} 

486 

23736  487 
inductive 
22262  488 
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool" 
489 
for f :: "'a => 'a => 'a" 

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

491 
and z :: 'a 

492 
where 

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

494 
 insertI [intro]: 

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

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

497 

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

500 
constdefs 

21733  501 
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" 
22262  502 
"fold f g z A == THE x. foldSet f g z A x" 
15392  503 

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

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

509 

510 

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

22262  515 
lemma foldSet_imp_finite: "foldSet f g z A x==> finite A" 
15392  516 
by (induct set: foldSet) auto 
517 

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

15392  520 

521 

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

523 

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

527 
lemma insert_image_inj_on_eq: 

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

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

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

531 
apply (auto simp add: image_less_Suc inj_on_def) 

532 
apply (blast intro: less_trans) 

533 
done 

534 

535 
lemma insert_inj_onE: 

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

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

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

539 
proof (cases n) 

540 
case 0 thus ?thesis using aA by auto 

541 
next 

542 
case (Suc m) 

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

15510  549 
show ?thesis 
15520  550 
proof (intro exI conjI) 
551 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

555 
proof (rule insert_image_inj_on_eq) 

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

559 
using aA hkeq nSuc klessn 

560 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

561 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  562 
qed 
563 
qed 

564 
qed 

565 

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

566 
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

567 
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

568 

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

569 
lemma foldSet_determ_aux: 
15510  570 
"!!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

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

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

576 
\<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

577 
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

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

22262  582 
assume "A = {}" and "x = z" 
15510  583 
with Afoldx' show "x' = x" by blast 
15392  584 
next 
15510  585 
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

586 
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

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

22262  590 
assume "A = {}" and "x' = z" 
15510  591 
with AbB show "x' = x" by blast 
15392  592 
next 
15510  593 
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

594 
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

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

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

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

600 
and lessB: "mB < n" by auto 

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

602 
from insert_inj_onE [OF Ceq notinC injh] 

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

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

605 
and lessC: "mC < n" by auto 

606 
show "x'=x" 

15392  607 
proof cases 
15510  608 
assume "b=c" 
609 
then moreover have "B = C" using AbB AcC notinB notinC by auto 

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

611 
by auto 

15392  612 
next 
613 
assume diff: "b \<noteq> c" 

614 
let ?D = "B  {c}" 

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

15510  616 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
15402  617 
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 
15510  618 
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

619 
then obtain d where Dfoldd: "foldSet times g z ?D d" 
17589  620 
using finite_imp_foldSet by iprover 
15506  621 
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

622 
ultimately have "foldSet times g z B (g c * d)" 
15392  623 
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

624 
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

625 
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

626 
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

627 
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

628 
show "foldSet times g z C (g b * d)" using C notinB Dfoldd 
15392  629 
by fastsimp 
630 
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

631 
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

632 
by (simp add: mult_left_commute) 
15392  633 
qed 
634 
qed 

635 
qed 

636 
qed 

637 

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

638 
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

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

15392  642 
done 
643 

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

644 
lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y" 
15392  645 
by (unfold fold_def) (blast intro: foldSet_determ) 
646 

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

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 (in ) fold_empty [simp]: "fold f g z {} = z" 
15392  650 
by (unfold fold_def) blast 
651 

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

652 
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

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

654 
(EX y. foldSet times g z A y & v = g x * y)" 
15392  655 
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

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

659 
done 

660 

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

662 

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

663 
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

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

667 
apply (rule the_equality) 

668 
apply (auto intro: finite_imp_foldSet 

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

670 
done 

671 

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

672 
lemma fold_rec: 
15535  673 
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

674 
shows "fold times g z A = g a * fold times g z (A  {a})" 
15535  675 
proof 
676 
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

677 
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

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

681 
qed 

682 

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

683 
end 
15392  684 

15480  685 
text{* A simplified version for idempotent functions: *} 
686 

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

687 
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

688 
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

689 

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

690 
lemma fold_insert_idem: 
15480  691 
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

692 
shows "fold times g z (insert a A) = g a * fold times g z A" 
15480  693 
proof cases 
694 
assume "a \<in> A" 

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

696 
by(blast dest: mk_disjoint_insert) 

697 
show ?thesis 

698 
proof  

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

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

701 
also have "\<dots> = g a * fold times g z B" 
15506  702 
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

703 
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

704 
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

705 
by (simp add: mult_idem mult_assoc [symmetric]) 
15480  706 
finally show ?thesis . 
707 
qed 

708 
next 

709 
assume "a \<notin> A" 

710 
with finA show ?thesis by simp 

711 
qed 

712 

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

713 
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

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

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

717 
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

718 

15392  719 
subsubsection{*Lemmas about @{text fold}*} 
720 

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

721 
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

722 
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

723 

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

724 
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

725 
"finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" 
22262  726 
apply (induct set: finite) 
21575  727 
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

728 
apply (simp add: mult_left_commute [of x]) 
15392  729 
done 
730 

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

731 
lemma fold_nest_Un_Int: 
15392  732 
"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

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

738 

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

739 
lemma fold_nest_Un_disjoint: 
15392  740 
"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

741 
==> fold times g z (A Un B) = fold times g (fold times g z B) A" 
15392  742 
by (simp add: fold_nest_Un_Int) 
743 

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

744 
lemma fold_reindex: 
15487  745 
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

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

750 
done 

751 

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

752 
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

753 
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

754 
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

755 
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

756 
*} 
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 

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 
lemma fold_fusion: 
27611  759 
assumes "ab_semigroup_mult g" 
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

760 
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

761 
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

762 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  763 
proof  
764 
interpret ab_semigroup_mult [g] by fact 

765 
show ?thesis using fin hyp by (induct set: finite) simp_all 

766 
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

767 

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

768 
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

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

770 
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  771 
apply simp 
772 
apply (erule finite_induct, simp) 

773 
apply (simp add: subset_insert_iff, clarify) 

774 
apply (subgoal_tac "finite C") 

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

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

777 
prefer 2 apply blast 

778 
apply (erule ssubst) 

779 
apply (drule spec) 

780 
apply (erule (1) notE impE) 

781 
apply (simp add: Ball_def del: insert_Diff_single) 

782 
done 

783 

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

784 
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

785 

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

787 
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

788 

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

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

791 
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

792 
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

793 
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

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

795 

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

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

798 
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

799 
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

800 

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

802 
"\<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

803 
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

804 
\<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

805 
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

806 
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

807 
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

808 
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

809 
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

810 
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

811 
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

812 
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

813 

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

814 
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

815 
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

816 
fold times (split g) 1 (SIGMA x:A. B x)" 
15392  817 
apply (subst Sigma_def) 
15506  818 
apply (subst fold_UN_disjoint, assumption, simp) 
15392  819 
apply blast 
820 
apply (erule fold_cong) 

15506  821 
apply (subst fold_UN_disjoint, simp, simp) 
15392  822 
apply blast 
15506  823 
apply simp 
15392  824 
done 
825 

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

826 
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

827 
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

828 
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

829 

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 
end 
22917  831 

832 

15402  833 
subsection {* Generalized summation over a set *} 
834 

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

835 
interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"] 
28823  836 
proof qed (auto intro: add_assoc add_commute) 
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

837 

15402  838 
constdefs 
839 
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" 

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

841 

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

843 
Setsum ("\<Sum>_" [1000] 999) where 
19535  844 
"\<Sum>A == setsum (%x. x) A" 
845 

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

848 

849 
syntax 

17189  850 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  851 
syntax (xsymbols) 
17189  852 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  853 
syntax (HTML output) 
17189  854 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  855 

856 
translations  {* Beware of argument permutation! *} 

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

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

859 

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

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

862 

863 
syntax 

17189  864 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  865 
syntax (xsymbols) 
17189  866 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  867 
syntax (HTML output) 
17189  868 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  869 

870 
translations 

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

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

873 

874 
print_translation {* 

875 
let 

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

878 
else let val x' = Syntax.mark_bound x 

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

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

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

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

15402  883 
*} 
884 

19535  885 

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

888 

889 
lemma setsum_insert [simp]: 

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

15765  891 
by (simp add: setsum_def) 
15402  892 

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

893 
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

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

895 

15402  896 
lemma setsum_reindex: 
897 
"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

898 
by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD) 
15402  899 

900 
lemma setsum_reindex_id: 

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

902 
by (auto simp add: setsum_reindex) 

903 

904 
lemma setsum_cong: 

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

906 
by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong) 
15402  907 

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

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

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

910 
==> 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

911 
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

912 

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

915 

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

920 

15542  921 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  922 
apply (clarsimp simp: setsum_def) 
15765  923 
apply (erule finite_induct, auto) 
15402  924 
done 
925 

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

15402  928 

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

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

931 
 {* 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

932 
by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric]) 
15402  933 

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

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

936 
by (subst setsum_Un_Int [symmetric], auto) 

937 

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

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

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

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

943 
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

944 
by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong) 
15402  945 

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

946 
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

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

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

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

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

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

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

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

956 
done 
15402  957 

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

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

959 
the rhs need not be, since SIGMA A B could still be finite.*) 
15402  960 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
17189  961 
(\<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

962 
by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong) 
15402  963 

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

964 
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

965 
lemma setsum_cartesian_product: 
17189  966 
"(\<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

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

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

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

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

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

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

974 
done 
15402  975 

976 
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

977 
by(simp add:setsum_def comm_monoid_add.fold_distrib) 
15402  978 

979 

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

981 

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

983 
apply (case_tac "finite A") 

984 
prefer 2 apply (simp add: setsum_def) 

985 
apply (erule rev_mp) 

986 
apply (erule finite_induct, auto) 

987 
done 

988 

989 
lemma setsum_eq_0_iff [simp]: 

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

22262  991 
by (induct set: finite) auto 
15402  992 

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

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

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

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

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

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

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

1000 
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

1001 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  1002 

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

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

1005 
apply (case_tac "finite A") 

1006 
prefer 2 apply (simp add: setsum_def) 

1007 
apply (erule finite_induct) 

1008 
apply (auto simp add: insert_Diff_if) 

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

1010 
done 

1011 

1012 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

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

1016 

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

1017 
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

1018 
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

1019 
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

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

1021 

15402  1022 
(* By Jeremy Siek: *) 
1023 

1024 
lemma setsum_diff_nat: 

19535  1025 
assumes "finite B" 
1026 
and "B \<subseteq> A" 

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

1028 
using prems 

1029 
proof induct 

15402  1030 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 
1031 
next 

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

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

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

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

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

1037 
by (simp add: setsum_diff1_nat) 

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

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

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

1041 
by simp 

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

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

1044 
by simp 

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

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

1047 
by simp 

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

1049 
qed 

1050 

1051 
lemma setsum_diff: 

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

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

1054 
proof  

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

1056 
show ?thesis using finiteB le 

21575  1057 
proof induct 
19535  1058 
case empty 
1059 
thus ?case by auto 

1060 
next 

1061 
case (insert x F) 

1062 
thus ?case using le finiteB 

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

15402  1064 
qed 
19535  1065 
qed 
15402  1066 

1067 
lemma setsum_mono: 

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

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

1070 
proof (cases "finite K") 

1071 
case True 

1072 
thus ?thesis using le 

19535  1073 
proof induct 
15402  1074 
case empty 
1075 
thus ?case by simp 

1076 
next 

1077 
case insert 

19535  1078 
thus ?case using add_mono by fastsimp 
15402  1079 
qed 
1080 
next 

1081 
case False 

1082 
thus ?thesis 

1083 
by (simp add: setsum_def) 

1084 
qed 

1085 

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

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

1090 
shows "setsum f A < setsum g A" 

1091 
using prems 

15554  1092 
proof (induct rule: finite_ne_induct) 
1093 
case singleton thus ?case by simp 

1094 
next 

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

1096 
qed 

1097 

15535  1098 
lemma setsum_negf: 
19535  1099 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  1100 
proof (cases "finite A") 
22262  1101 
case True thus ?thesis by (induct set: finite) auto 
15535  1102 
next 
1103 
case False thus ?thesis by (simp add: setsum_def) 

1104 
qed 

15402  1105 

15535  1106 
lemma setsum_subtractf: 
19535  1107 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
1108 
setsum f A  setsum g A" 

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

1111 
next 

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

1113 
qed 

15402  1114 

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

15535  1118 
proof (cases "finite A") 
1119 
case True thus ?thesis using nn 

21575  1120 
proof induct 
19535  1121 
case empty then show ?case by simp 
1122 
next 

1123 
case (insert x F) 

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

1125 
with insert show ?case by simp 

1126 
qed 

15535  1127 
next 
1128 
case False thus ?thesis by (simp add: setsum_def) 

1129 
qed 

15402  1130 

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

15535  1134 
proof (cases "finite A") 
1135 
case True thus ?thesis using np 

21575  1136 
proof induct 
19535  1137 
case empty then show ?case by simp 
1138 
next 

1139 
case (insert x F) 

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

1141 
with insert show ?case by simp 

1142 
qed 

15535  1143 
next 
1144 
case False thus ?thesis by (simp add: setsum_def) 

1145 
qed 

15402  1146 

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

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

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

1151 
proof  

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

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

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

1155 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1157 
finally show ?thesis . 

1158 
qed 

15542  1159 

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

1160 
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

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

1162 
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

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

1164 
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

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

1166 
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

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

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

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

1170 
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

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

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

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

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

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

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

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

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

1179 

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

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

1184 
case True 

1185 
thus ?thesis 

21575  1186 
proof induct 
15402  1187 
case empty thus ?case by simp 
1188 
next 

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

1190 
qed 

1191 
next 

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

1193 
qed 

1194 

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

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

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

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

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

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

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

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

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

1203 
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

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

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

1206 
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

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

1208 

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

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

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

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

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

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

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

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

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

1217 
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

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

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

1220 
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

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

1222 

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

1224 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1225 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  1226 
proof (cases "finite A") 
1227 
case True 

1228 
thus ?thesis 

21575  1229 
proof induct 
15535  1230 
case empty thus ?case by simp 
1231 
next 

1232 
case (insert x A) 

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

1234 
qed 

15402  1235 
next 
15535  1236 
case False thus ?thesis by (simp add: setsum_def) 
15402  1237 
qed 
1238 

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

1240 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1241 
shows "0 \<le> setsum (%i. abs(f i)) A" 
15535  1242 
proof (cases "finite A") 
1243 
case True 

1244 
thus ?thesis 

21575  1245 
proof induct 
15535  1246 
case empty thus ?case by simp 
1247 
next 

21733  1248 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  1249 
qed 
15402  1250 
next 
15535  1251 
case False thus ?thesis by (simp add: setsum_def) 
15402  1252 
qed 
1253 

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

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

1258 
case True 

1259 
thus ?thesis 

21575  1260 
proof induct 
15539  1261 
case empty thus ?case by simp 
1262 
next 

1263 
case (insert a A) 

1264 
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 

1265 
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

1266 
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

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

1270 
qed 

1271 
next 

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

1273 
qed 

1274 

15402  1275 

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

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

1277 

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

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

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

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

1281 

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

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

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

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

1285 

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

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

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

1288 
proof (simp add: setsum_cartesian_product) 
17189  1289 
have "(\<Sum>(x,y) \<in> A <*> B. f x y) = 
1290 
(\<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

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

1292 
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

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

1294 
done 
17189  1295 
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

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

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

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

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