author  nipkow 
Wed, 19 Nov 2008 17:54:55 +0100  
changeset 28853  69eb69659bf3 
parent 28823  dcbef866c9e2 
child 29025  8c8859c0d734 
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 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

482 
@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

483 
if @{text f} is ``leftcommutative'': 
15392  484 
*} 
485 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

486 
locale fun_left_comm = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

487 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

488 
assumes fun_left_comm: "f x (f y z) = f y (f x z)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

489 
begin 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

490 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

491 
text{* On a functional level it looks much nicer: *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

492 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

493 
lemma fun_comp_comm: "f x \<circ> f y = f y \<circ> f x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

494 
by (simp add: fun_left_comm expand_fun_eq) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

495 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

496 
end 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

497 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

498 
inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

499 
for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

500 
emptyI [intro]: "fold_graph f z {} z"  
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

501 
insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

502 
\<Longrightarrow> fold_graph f z (insert x A) (f x y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

503 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

504 
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

505 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

506 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

507 
[code del]: "fold f z A = (THE y. fold_graph f z A y)" 
15392  508 

15498  509 
text{*A tempting alternative for the definiens is 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

510 
@{term "if finite A then THE y. fold_graph f z A y else e"}. 
15498  511 
It allows the removal of finiteness assumptions from the theorems 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

512 
@{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}. 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

513 
The proofs become ugly. It is not worth the effort. (???) *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

514 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

515 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

516 
lemma Diff1_fold_graph: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

517 
"fold_graph f z (A  {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

518 
by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

519 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

520 
lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

521 
by (induct set: fold_graph) auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

522 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

523 
lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

524 
by (induct set: finite) auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

525 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

526 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

527 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  528 

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

532 
lemma insert_image_inj_on_eq: 

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

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

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

536 
apply (auto simp add: image_less_Suc inj_on_def) 

537 
apply (blast intro: less_trans) 

538 
done 

539 

540 
lemma insert_inj_onE: 

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

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

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

544 
proof (cases n) 

545 
case 0 thus ?thesis using aA by auto 

546 
next 

547 
case (Suc m) 

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

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

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

560 
proof (rule insert_image_inj_on_eq) 

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

564 
using aA hkeq nSuc klessn 

565 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

566 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  567 
qed 
568 
qed 

569 
qed 

570 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

571 
context fun_left_comm 
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

572 
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

573 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

574 
lemma fold_graph_determ_aux: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

575 
"A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

576 
\<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x' 
15392  577 
\<Longrightarrow> x' = x" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

578 
proof (induct n arbitrary: A x x' h rule: less_induct) 
15510  579 
case (less n) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

580 
have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

581 
\<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

582 
\<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

583 
have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

584 
and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+ 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

585 
show ?case 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

586 
proof (rule fold_graph.cases [OF Afoldx]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

587 
assume "A = {}" and "x = z" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

588 
with Afoldx' show "x' = x" by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

589 
next 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

590 
fix B b u 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

591 
assume AbB: "A = insert b B" and x: "x = f b u" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

592 
and notinB: "b \<notin> B" and Bu: "fold_graph f z B u" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

593 
show "x'=x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

594 
proof (rule fold_graph.cases [OF Afoldx']) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

595 
assume "A = {}" and "x' = z" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

596 
with AbB show "x' = x" by blast 
15392  597 
next 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

598 
fix C c v 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

599 
assume AcC: "A = insert c C" and x': "x' = f c v" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

600 
and notinC: "c \<notin> C" and Cv: "fold_graph f z C v" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

601 
from A AbB have Beq: "insert b B = h`{i. i<n}" by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

602 
from insert_inj_onE [OF Beq notinB injh] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

603 
obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

604 
and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

605 
from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

606 
from insert_inj_onE [OF Ceq notinC injh] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

607 
obtain hC mC where inj_onC: "inj_on hC {i. i < mC}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

608 
and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

609 
show "x'=x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

610 
proof cases 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

611 
assume "b=c" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

612 
then moreover have "B = C" using AbB AcC notinB notinC by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

613 
ultimately show ?thesis using Bu Cv x x' IH [OF lessC Ceq inj_onC] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

614 
by auto 
15392  615 
next 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

616 
assume diff: "b \<noteq> c" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

617 
let ?D = "B  {c}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

618 
have B: "B = insert c ?D" and C: "C = insert b ?D" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

619 
using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

620 
have "finite A" by(rule fold_graph_imp_finite [OF Afoldx]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

621 
with AbB have "finite ?D" by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

622 
then obtain d where Dfoldd: "fold_graph f z ?D d" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

623 
using finite_imp_fold_graph by iprover 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

624 
moreover have cinB: "c \<in> B" using B by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

625 
ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

626 
hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

627 
moreover have "f b d = v" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

628 
proof (rule IH[OF lessC Ceq inj_onC Cv]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

629 
show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp 
15392  630 
qed 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

631 
ultimately show ?thesis 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

632 
using fun_left_comm [of c b] x x' by (auto simp add: o_def) 
15392  633 
qed 
634 
qed 

635 
qed 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

636 
qed 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

637 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

638 
lemma fold_graph_determ: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

639 
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

640 
apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

641 
apply (blast intro: fold_graph_determ_aux [rule_format]) 
15392  642 
done 
643 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

644 
lemma fold_equality: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

645 
"fold_graph f z A y \<Longrightarrow> fold f z A = y" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

646 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  647 

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

649 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

650 
lemma (in ) fold_empty [simp]: "fold f z {} = z" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

651 
by (unfold fold_def) blast 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

652 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

653 
text{* The various recursion equations for @{const fold}: *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

654 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

655 
lemma fold_insert_aux: "x \<notin> A 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

656 
\<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow> 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

657 
(\<exists>y. fold_graph f z A y \<and> v = f x y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

658 
apply auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

659 
apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

660 
apply (fastsimp dest: fold_graph_imp_finite) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

661 
apply (blast intro: fold_graph_determ) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

662 
done 
15392  663 

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

664 
lemma fold_insert [simp]: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

665 
"finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

666 
apply (simp add: fold_def fold_insert_aux) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

667 
apply (rule the_equality) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

668 
apply (auto intro: finite_imp_fold_graph 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

669 
cong add: conj_cong simp add: fold_def[symmetric] fold_equality) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

670 
done 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

671 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

672 
lemma fold_fun_comm: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

673 
"finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

674 
proof (induct rule: finite_induct) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

675 
case empty then show ?case by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

676 
next 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

677 
case (insert y A) then show ?case 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

678 
by (simp add: fun_left_comm[of x]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

679 
qed 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

680 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

681 
lemma fold_insert2: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

682 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

683 
by (simp add: fold_insert fold_fun_comm) 
15392  684 

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

685 
lemma fold_rec: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

686 
assumes "finite A" and "x \<in> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

687 
shows "fold f z A = f x (fold f z (A  {x}))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

688 
proof  
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

689 
have A: "A = insert x (A  {x})" using `x \<in> A` by blast 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

690 
then have "fold f z A = fold f z (insert x (A  {x}))" by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

691 
also have "\<dots> = f x (fold f z (A  {x}))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

692 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  693 
finally show ?thesis . 
694 
qed 

695 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

696 
lemma fold_insert_remove: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

697 
assumes "finite A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

698 
shows "fold f z (insert x A) = f x (fold f z (A  {x}))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

699 
proof  
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

700 
from `finite A` have "finite (insert x A)" by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

701 
moreover have "x \<in> insert x A" by auto 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

702 
ultimately have "fold f z (insert x A) = f x (fold f z (insert x A  {x}))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

703 
by (rule fold_rec) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

704 
then show ?thesis by simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

705 
qed 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

706 

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

707 
end 
15392  708 

15480  709 
text{* A simplified version for idempotent functions: *} 
710 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

711 
locale fun_left_comm_idem = fun_left_comm + 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

712 
assumes fun_left_idem: "f x (f x z) = f x z" 
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 
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

714 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

715 
text{* The nice version: *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

716 
lemma fun_comp_idem : "f x o f x = f x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

717 
by (simp add: fun_left_idem expand_fun_eq) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

718 

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

719 
lemma fold_insert_idem: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

720 
assumes fin: "finite A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

721 
shows "fold f z (insert x A) = f x (fold f z A)" 
15480  722 
proof cases 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

723 
assume "x \<in> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

724 
then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

725 
then show ?thesis using assms by (simp add:fun_left_idem) 
15480  726 
next 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

727 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  728 
qed 
729 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

730 
declare fold_insert[simp del] fold_insert_idem[simp] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

731 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

732 
lemma fold_insert_idem2: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

733 
"finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

734 
by(simp add:fold_fun_comm) 
15484  735 

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

736 
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

737 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

738 
subsubsection{* The derived combinator @{text fold_image} *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

739 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

740 
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

741 
where "fold_image f g = fold (%x y. f (g x) y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

742 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

743 
lemma fold_image_empty[simp]: "fold_image f g z {} = z" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

744 
by(simp add:fold_image_def) 
15392  745 

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

747 
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

748 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

749 
lemma fold_image_insert[simp]: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

750 
assumes "finite A" and "a \<notin> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

751 
shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

752 
proof  
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

753 
interpret I: fun_left_comm ["%x y. (g x) * y"] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

754 
by unfold_locales (simp add: mult_ac) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

755 
show ?thesis using assms by(simp add:fold_image_def I.fold_insert) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

756 
qed 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

757 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

759 
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

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

763 
apply (simp add: mult_left_commute [of x]) 
15392  764 
done 
765 

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

766 
lemma fold_nest_Un_Int: 
15392  767 
"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

768 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  769 
apply (induct set: finite) 
21575  770 
apply simp 
15392  771 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
772 
done 

773 

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

774 
lemma fold_nest_Un_disjoint: 
15392  775 
"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

776 
==> fold times g z (A Un B) = fold times g (fold times g z B) A" 
15392  777 
by (simp add: fold_nest_Un_Int) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

778 
*) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

779 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

780 
lemma fold_image_reindex: 
15487  781 
assumes fin: "finite A" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

782 
shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A" 
15506  783 
using fin apply induct 
15392  784 
apply simp 
785 
apply simp 

786 
done 

787 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

789 
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

790 
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

791 
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

792 
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

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

794 

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

795 
lemma fold_fusion: 
27611  796 
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

797 
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

798 
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

799 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  800 
proof  
801 
interpret ab_semigroup_mult [g] by fact 

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

803 
qed 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

804 
*) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

805 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

806 
lemma fold_image_cong: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

807 
"finite A \<Longrightarrow> 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

808 
(!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

809 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold_image times g z C = fold_image times h z C") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

810 
apply simp 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

811 
apply (erule finite_induct, simp) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

812 
apply (simp add: subset_insert_iff, clarify) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

813 
apply (subgoal_tac "finite C") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

814 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

815 
apply (subgoal_tac "C = insert x (C  {x})") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

816 
prefer 2 apply blast 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

817 
apply (erule ssubst) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

818 
apply (drule spec) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

819 
apply (erule (1) notE impE) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

820 
apply (simp add: Ball_def del: insert_Diff_single) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

821 
done 
15392  822 

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

823 
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

824 

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

825 
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

826 
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

827 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

829 
"finite A ==> finite B ==> 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

830 
fold_image times g 1 A * fold_image times g 1 B = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

831 
fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

832 
by (induct set: finite) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

833 
(auto simp add: mult_ac insert_absorb Int_insert_left) 
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

834 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour 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 
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

836 
"finite A ==> finite B ==> A Int B = {} ==> 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

837 
fold_image times g 1 (A Un B) = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

838 
fold_image times g 1 A * fold_image times g 1 B" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

839 
by (simp add: fold_image_Un_Int) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

840 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

841 
lemma fold_image_UN_disjoint: 
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

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

843 
ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {} \<rbrakk> 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

844 
\<Longrightarrow> fold_image times g 1 (UNION I A) = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

845 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

846 
apply (induct set: finite, simp, atomize) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

847 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

848 
prefer 2 apply blast 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

849 
apply (subgoal_tac "A x Int UNION F A = {}") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

850 
prefer 2 apply blast 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

851 
apply (simp add: fold_Un_disjoint) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

852 
done 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

853 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

854 
lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

855 
fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

856 
fold_image times (split g) 1 (SIGMA x:A. B x)" 
15392  857 
apply (subst Sigma_def) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

858 
apply (subst fold_image_UN_disjoint, assumption, simp) 
15392  859 
apply blast 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

860 
apply (erule fold_image_cong) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

861 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  862 
apply blast 
15506  863 
apply simp 
15392  864 
done 
865 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

866 
lemma fold_image_distrib: "finite A \<Longrightarrow> 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

867 
fold_image times (%x. g x * h x) 1 A = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

868 
fold_image times g 1 A * fold_image times h 1 A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

869 
by (erule finite_induct) (simp_all add: mult_ac) 
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

870 

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

871 
end 
22917  872 

873 

15402  874 
subsection {* Generalized summation over a set *} 
875 

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

876 
interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"] 
28823  877 
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

878 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

879 
definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

880 
where "setsum f A == if finite A then fold_image (op +) f 0 A else 0" 
15402  881 

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

883 
Setsum ("\<Sum>_" [1000] 999) where 
19535  884 
"\<Sum>A == setsum (%x. x) A" 
885 

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

888 

889 
syntax 

17189  890 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  891 
syntax (xsymbols) 
17189  892 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  893 
syntax (HTML output) 
17189  894 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  895 

896 
translations  {* Beware of argument permutation! *} 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

897 
"SUM i:A. b" == "CONST setsum (%i. b) A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

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

902 

903 
syntax 

17189  904 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  905 
syntax (xsymbols) 
17189  906 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  907 
syntax (HTML output) 
17189  908 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  909 

910 
translations 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

911 
"SUM xP. t" => "CONST setsum (%x. t) {x. P}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

914 
print_translation {* 

915 
let 

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

918 
else let val x' = Syntax.mark_bound x 

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

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

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

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

15402  923 
*} 
924 

19535  925 

15402  926 
lemma setsum_empty [simp]: "setsum f {} = 0" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

927 
by (simp add: setsum_def) 
15402  928 

929 
lemma setsum_insert [simp]: 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

930 
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

931 
by (simp add: setsum_def) 
15402  932 

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

933 
lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

935 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

938 
by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD) 
15402  939 

940 
lemma setsum_reindex_id: 

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

942 
by (auto simp add: setsum_reindex) 

943 

944 
lemma setsum_cong: 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

946 
by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong) 
15402  947 

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

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

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

950 
==> setsum (%x. f x) A = setsum (%x. g x) B" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

952 

15554  953 
lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"; 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

954 
by (rule setsum_cong[OF refl], auto); 
15554  955 

15402  956 
lemma setsum_reindex_cong: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

957 
"[inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

958 
==> setsum h B = setsum g A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

959 
by (simp add: setsum_reindex cong: setsum_cong) 
15402  960 

15542  961 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  962 
apply (clarsimp simp: setsum_def) 
15765  963 
apply (erule finite_induct, auto) 
15402  964 
done 
965 

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

15402  968 

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

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

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

972 
by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric]) 
15402  973 

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

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

976 
by (subst setsum_Un_Int [symmetric], auto) 

977 

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

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

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

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

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

984 
by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong) 
15402  985 

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

986 
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

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

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

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

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

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

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

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

996 
done 
15402  997 

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

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

999 
the rhs need not be, since SIGMA A B could still be finite.*) 
15402  1000 
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 
17189  1001 
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1002 
by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong) 
15402  1003 

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

1004 
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

1005 
lemma setsum_cartesian_product: 
17189  1006 
"(\<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

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

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

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

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

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

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

1014 
done 
15402  1015 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1017 
by(simp add:setsum_def comm_monoid_add.fold_image_distrib) 
15402  1018 

1019 

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

1021 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1023 
apply (case_tac "finite A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1024 
prefer 2 apply (simp add: setsum_def) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1025 
apply (erule rev_mp) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1026 
apply (erule finite_induct, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1027 
done 
15402  1028 

1029 
lemma setsum_eq_0_iff [simp]: 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1031 
by (induct set: finite) auto 
15402  1032 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1034 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 
15402  1035 
 {* For the natural numbers, we have subtraction. *} 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1036 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  1037 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1039 
(setsum f (A Un B) :: 'a :: ab_group_add) = 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1040 
setsum f A + setsum f B  setsum f (A Int B)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1041 
by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps) 
15402  1042 

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1044 
(if a:A then setsum f A  f a else setsum f A)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1045 
apply (case_tac "finite A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1046 
prefer 2 apply (simp add: setsum_def) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1047 
apply (erule finite_induct) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1048 
apply (auto simp add: insert_Diff_if) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1049 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1050 
done 
15402  1051 

1052 
lemma setsum_diff1: "finite A \<Longrightarrow> 

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

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

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1055 
by (erule finite_induct) (auto simp add: insert_Diff_if) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1056 

69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1057 
lemma setsum_diff1'[rule_format]: 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1058 
"finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A  {a}). f x)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1059 
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))"]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1060 
apply (auto simp add: insert_Diff_if add_ac) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1062 

15402  1063 
(* By Jeremy Siek: *) 
1064 

1065 
lemma setsum_diff_nat: 

28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1066 
assumes "finite B" and "B \<subseteq> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1067 
shows "(setsum f (A  B) :: nat) = (setsum f A)  (setsum f B)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1068 
using assms 
19535  1069 
proof induct 
15402  1070 
show "setsum f (A  {}) = (setsum f A)  (setsum f {})" by simp 
1071 
next 

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

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

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

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

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

1077 
by (simp add: setsum_diff1_nat) 

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

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

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

1081 
by simp 

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

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

1084 
by simp 

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

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

1087 
by simp 

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

1089 
qed 

1090 

1091 
lemma setsum_diff: 

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

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

1094 
proof  

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

1096 
show ?thesis using finiteB le 

21575  1097 
proof induct 
19535  1098 
case empty 
1099 
thus ?case by auto 

1100 
next 

1101 
case (insert x F) 

1102 
thus ?case using le finiteB 

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

15402  1104 
qed 
19535  1105 
qed 
15402  1106 

1107 
lemma setsum_mono: 

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

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

1110 
proof (cases "finite K") 

1111 
case True 

1112 
thus ?thesis using le 

19535  1113 
proof induct 
15402  1114 
case empty 
1115 
thus ?case by simp 

1116 
next 

1117 
case insert 

19535  1118 
thus ?case using add_mono by fastsimp 
15402  1119 
qed 
1120 
next 

1121 
case False 

1122 
thus ?thesis 

1123 
by (simp add: setsum_def) 

1124 
qed 

1125 

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

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

1130 
shows "setsum f A < setsum g A" 

1131 
using prems 

15554  1132 
proof (induct rule: finite_ne_induct) 
1133 
case singleton thus ?case by simp 

1134 
next 

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

1136 
qed 

1137 

15535  1138 
lemma setsum_negf: 
19535  1139 
"setsum (%x.  (f x)::'a::ab_group_add) A =  setsum f A" 
15535  1140 
proof (cases "finite A") 
22262  1141 
case True thus ?thesis by (induct set: finite) auto 
15535  1142 
next 
1143 
case False thus ?thesis by (simp add: setsum_def) 

1144 
qed 

15402  1145 

15535  1146 
lemma setsum_subtractf: 
19535  1147 
"setsum (%x. ((f x)::'a::ab_group_add)  g x) A = 
1148 
setsum f A  setsum g A" 

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

1151 
next 

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

1153 
qed 

15402  1154 

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

15535  1158 
proof (cases "finite A") 
1159 
case True thus ?thesis using nn 

21575  1160 
proof induct 
19535  1161 
case empty then show ?case by simp 
1162 
next 

1163 
case (insert x F) 

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

1165 
with insert show ?case by simp 

1166 
qed 

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

1169 
qed 

15402  1170 

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

15535  1174 
proof (cases "finite A") 
1175 
case True thus ?thesis using np 

21575  1176 
proof induct 
19535  1177 
case empty then show ?case by simp 
1178 
next 

1179 
case (insert x F) 

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

1181 
with insert show ?case by simp 

1182 
qed 

15535  1183 
next 
1184 
case False thus ?thesis by (simp add: setsum_def) 

1185 
qed 

15402  1186 

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

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

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

1191 
proof  

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

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

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

1195 
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) 

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

1197 
finally show ?thesis . 

1198 
qed 

15542  1199 

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

1200 
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

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

1202 
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

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

1204 
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

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

1206 
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

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

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

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

1210 
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

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

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

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

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

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

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

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

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

1219 

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

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

1224 
case True 

1225 
thus ?thesis 

21575  1226 
proof induct 
15402  1227 
case empty thus ?case by simp 
1228 
next 

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

1230 
qed 

1231 
next 

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

1233 
qed 

1234 

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

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

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

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

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

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

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

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

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

1243 
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

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

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

1246 
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

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

1248 

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

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

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

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

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

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

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

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

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

1257 
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

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

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

1260 
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

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

1262 

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

1264 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1265 
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" 
15535  1266 
proof (cases "finite A") 
1267 
case True 

1268 
thus ?thesis 

21575  1269 
proof induct 
15535  1270 
case empty thus ?case by simp 
1271 
next 

1272 
case (insert x A) 

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

1274 
qed 

15402  1275 
next 
15535  1276 
case False thus ?thesis by (simp add: setsum_def) 
15402  1277 
qed 
1278 

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

1280 
fixes f :: "'a => ('b::pordered_ab_group_add_abs)" 
15402  1281 
shows "0 \<le> setsum (%i. abs(f i)) A" 
15535  1282 
proof (cases "finite A") 
1283 
case True 

1284 
thus ?thesis 

21575  1285 
proof induct 
15535  1286 
case empty thus ?case by simp 
1287 
next 

21733  1288 
case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) 
15535  1289 
qed 
15402  1290 
next 
15535  1291 
case False thus ?thesis by (simp add: setsum_def) 
15402  1292 
qed 
1293 

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

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

1298 
case True 

1299 
thus ?thesis 

21575  1300 
proof induct 
15539  1301 
case empty thus ?case by simp 
1302 
next 

1303 
case (insert a A) 

1304 
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 

1305 
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

1306 
also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning 