author  nipkow 
Wed, 01 Apr 2009 16:03:00 +0200  
changeset 30837  3d4832d9f7e4 
parent 30729  461ee3e49ad3 
child 30842  d007dee0c372 
child 30843  3419ca741dbf 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
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

3 
with contributions by Jeremy Avigad 
12396  4 
*) 
5 

6 
header {* Finite sets *} 

7 

15131  8 
theory Finite_Set 
29609  9 
imports Nat Product_Type Power 
15131  10 
begin 
12396  11 

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

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

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

12396  18 

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

22 
proof  

28823  23 
from assms have "A \<noteq> UNIV" by blast 
14661  24 
thus ?thesis by blast 
25 
qed 

12396  26 

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

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

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

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

36 
proof induct 

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

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

41 
assume "x \<in> F" 

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

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

44 
next 

45 
assume "x \<notin> F" 

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

47 
qed 

48 
qed 

49 
qed 

50 

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

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

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

55 
\<Longrightarrow> P F" 

56 
using fin 

57 
proof induct 

58 
case empty thus ?case by simp 

59 
next 

60 
case (insert x F) 

61 
show ?case 

62 
proof cases 

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

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

15484  68 
qed 
69 
qed 

70 

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

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

75 
shows "P F" 

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

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

82 
fix x F 

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

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

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

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

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

89 
with P show "P F" . 

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

12396  92 
qed 
93 
qed 

94 
qed 

95 

29923  96 
text{* A finite choice principle. Does not need the SOME choice operator. *} 
97 
lemma finite_set_choice: 

98 
"finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)" 

99 
proof (induct set: finite) 

100 
case empty thus ?case by simp 

101 
next 

102 
case (insert a A) 

103 
then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto 

104 
show ?case (is "EX f. ?P f") 

105 
proof 

106 
show "?P(%x. if x = a then b else f x)" using f ab by auto 

107 
qed 

108 
qed 

109 

23878  110 

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

15510  113 
lemma finite_imp_nat_seg_image_inj_on: 
114 
assumes fin: "finite A" 

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

15392  116 
using fin 
117 
proof induct 

118 
case empty 

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

121 
qed 

15392  122 
next 
123 
case (insert a A) 

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

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

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

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

15392  130 
thus ?case by blast 
131 
qed 

132 

133 
lemma nat_seg_image_imp_finite: 

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

135 
proof (induct n) 

136 
case 0 thus ?case by simp 

137 
next 

138 
case (Suc n) 

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

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

141 
show ?case 

142 
proof cases 

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

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

145 
thus ?thesis using finB by simp 

146 
next 

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

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

149 
thus ?thesis using finB by simp 

150 
qed 

151 
qed 

152 

153 
lemma finite_conv_nat_seg_image: 

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

15510  155 
by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 
15392  156 

29920  157 
lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" 
158 
by(fastsimp simp: finite_conv_nat_seg_image) 

159 

26441  160 

15392  161 
subsubsection{* Finiteness and set theoretic constructions *} 
162 

12396  163 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 
29901  164 
by (induct set: finite) simp_all 
12396  165 

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

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

168 
proof  

169 
assume "finite B" 

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

171 
proof induct 

172 
case empty 

173 
thus ?case by simp 

174 
next 

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

175 
case (insert x F A) 
23389  176 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" by fact+ 
12396  177 
show "finite A" 
178 
proof cases 

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

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

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

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

23389  183 
also have "insert x (A  {x}) = A" using x by (rule insert_Diff) 
12396  184 
finally show ?thesis . 
185 
next 

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

189 
qed 

190 
qed 

191 
qed 

192 

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

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

29916  196 
lemma finite_Collect_disjI[simp]: 
29901  197 
"finite{x. P x  Q x} = (finite{x. P x} & finite{x. Q x})" 
198 
by(simp add:Collect_disj_eq) 

12396  199 

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

201 
 {* The converse obviously fails. *} 

29901  202 
by (blast intro: finite_subset) 
203 

29916  204 
lemma finite_Collect_conjI [simp, intro]: 
29901  205 
"finite{x. P x}  finite{x. Q x} ==> finite{x. P x & Q x}" 
206 
 {* The converse obviously fails. *} 

207 
by(simp add:Collect_conj_eq) 

12396  208 

29920  209 
lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}" 
210 
by(simp add: le_eq_less_or_eq) 

211 

12396  212 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 
213 
apply (subst insert_is_Un) 

14208  214 
apply (simp only: finite_Un, blast) 
12396  215 
done 
216 

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

219 
by (induct rule:finite_induct) simp_all 

220 

12396  221 
lemma finite_empty_induct: 
23389  222 
assumes "finite A" 
223 
and "P A" 

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

225 
shows "P {}" 

12396  226 
proof  
227 
have "P (A  A)" 

228 
proof  

23389  229 
{ 
230 
fix c b :: "'a set" 

231 
assume c: "finite c" and b: "finite b" 

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

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

234 
using c 

235 
proof induct 

236 
case empty 

237 
from P1 show ?case by simp 

238 
next 

239 
case (insert x F) 

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

241 
proof (rule P2) 

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

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

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

245 
qed 

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

247 
finally show ?case . 

12396  248 
qed 
23389  249 
} 
250 
then show ?thesis by this (simp_all add: assms) 

12396  251 
qed 
23389  252 
then show ?thesis by simp 
12396  253 
qed 
254 

29901  255 
lemma finite_Diff [simp]: "finite A ==> finite (A  B)" 
256 
by (rule Diff_subset [THEN finite_subset]) 

257 

258 
lemma finite_Diff2 [simp]: 

259 
assumes "finite B" shows "finite (A  B) = finite A" 

260 
proof  

261 
have "finite A \<longleftrightarrow> finite((AB) Un (A Int B))" by(simp add: Un_Diff_Int) 

262 
also have "\<dots> \<longleftrightarrow> finite(AB)" using `finite B` by(simp) 

263 
finally show ?thesis .. 

264 
qed 

265 

266 
lemma finite_compl[simp]: 

267 
"finite(A::'a set) \<Longrightarrow> finite(A) = finite(UNIV::'a set)" 

268 
by(simp add:Compl_eq_Diff_UNIV) 

12396  269 

29916  270 
lemma finite_Collect_not[simp]: 
29903  271 
"finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)" 
272 
by(simp add:Collect_neg_eq) 

273 

12396  274 
lemma finite_Diff_insert [iff]: "finite (A  insert a B) = finite (A  B)" 
275 
apply (subst Diff_insert) 

276 
apply (case_tac "a : A  B") 

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

14208  278 
apply (subst insert_Diff, simp_all) 
12396  279 
done 
280 

281 

15392  282 
text {* Image and Inverse Image over Finite Sets *} 
13825  283 

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

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

22262  286 
by (induct set: finite) simp_all 
13825  287 

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

288 
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

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

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

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

292 

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

27418  295 
apply (drule finite_imageI, simp add: range_composition) 
13825  296 
done 
297 

12396  298 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
299 
proof  

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

301 
fix B :: "'a set" 

302 
assume "finite B" 

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

304 
apply induct 

305 
apply simp 

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

307 
apply clarify 

308 
apply (simp (no_asm_use) add: inj_on_def) 

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

314 
done 

315 
qed (rule refl) 

316 

317 

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

320 
is included in a singleton. *} 

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

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

322 
apply (blast intro: the_equality [symmetric]) 
13825  323 
done 
324 

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

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

327 
is finite. *} 

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

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

331 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  332 
done 
333 

334 

15392  335 
text {* The finite UNION of finite sets *} 
12396  336 

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

22262  338 
by (induct set: finite) simp_all 
12396  339 

340 
text {* 

341 
Strengthen RHS to 

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

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

344 
We'd need to prove 

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

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

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

350 
by (blast intro: finite_UN_I finite_subset) 

12396  351 

29920  352 
lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow> 
353 
finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})" 

354 
apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})") 

355 
apply auto 

356 
done 

357 

358 
lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow> 

359 
finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})" 

360 
apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})") 

361 
apply auto 

362 
done 

363 

364 

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

367 

15392  368 
text {* Sigma of finite sets *} 
12396  369 

370 
lemma finite_SigmaI [simp]: 

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

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

373 

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

376 
by (rule finite_SigmaI) 

377 

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

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

381 
apply (erule ssubst) 

14208  382 
apply (erule finite_SigmaI, auto) 
12396  383 
done 
384 

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

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

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

387 
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

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

389 
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

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

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

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

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

394 
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

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

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

397 
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

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

399 

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

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

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

402 
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

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

404 
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

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

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

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

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

409 
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

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

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

412 
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

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

414 

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

415 

15392  416 
text {* The powerset of a finite set *} 
12396  417 

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

419 
proof 

420 
assume "finite (Pow A)" 

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

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

423 
next 

424 
assume "finite A" 

425 
thus "finite (Pow A)" 

426 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

427 
qed 

428 

29916  429 
lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}" 
430 
by(simp add: Pow_def[symmetric]) 

15392  431 

29918  432 

15392  433 
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A" 
434 
by(blast intro: finite_subset[OF subset_Pow_Union]) 

435 

436 

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

438 

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

439 
setup {* Sign.add_path "finite" *}  {*FIXME: name tweaking*} 
29797  440 
class 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

441 
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

442 
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

443 
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

444 

27430  445 
context finite 
446 
begin 

447 

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

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

450 

27430  451 
end 
452 

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

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

455 

26146  456 
instance unit :: finite 
457 
by default (simp add: UNIV_unit) 

458 

459 
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

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

461 

26146  462 
instance bool :: finite 
463 
by default (simp add: UNIV_bool) 

464 

465 
instance * :: (finite, finite) finite 

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

467 

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

469 
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

470 

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

473 
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

474 
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

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

478 
by (simp only: finite_Pow_iff finite) 

479 
ultimately show "finite (range ?graph)" 

480 
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

481 
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

482 
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

483 
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

484 

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

487 

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

488 

15392  489 
subsection {* A fold functional for finite sets *} 
490 

491 
text {* The intended behaviour is 

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

493 
if @{text f} is ``leftcommutative'': 
15392  494 
*} 
495 

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

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

497 
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

498 
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

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

500 

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

501 
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

502 

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

503 
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

504 
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

505 

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

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

507 

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

508 
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

509 
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

510 
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

511 
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

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

513 

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

514 
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

515 

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

516 
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

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

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

520 
@{term "if finite A then THE y. fold_graph f z A y else e"}. 
15498  521 
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

522 
@{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

523 
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

524 

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

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

528 
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

529 

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

530 
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

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

532 

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

533 
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

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

535 

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

536 

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

537 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  538 

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

542 
lemma insert_image_inj_on_eq: 

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

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

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

546 
apply (auto simp add: image_less_Suc inj_on_def) 

547 
apply (blast intro: less_trans) 

548 
done 

549 

550 
lemma insert_inj_onE: 

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

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

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

554 
proof (cases n) 

555 
case 0 thus ?thesis using aA by auto 

556 
next 

557 
case (Suc m) 

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

15510  564 
show ?thesis 
15520  565 
proof (intro exI conjI) 
566 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

570 
proof (rule insert_image_inj_on_eq) 

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

574 
using aA hkeq nSuc klessn 

575 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

576 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  577 
qed 
578 
qed 

579 
qed 

580 

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

581 
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

582 
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

583 

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

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

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

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

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

590 
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

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

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

593 
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

594 
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

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

596 
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

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

598 
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

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

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

601 
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

602 
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

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

604 
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

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

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

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

609 
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

610 
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

611 
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

612 
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

613 
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

614 
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

615 
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

616 
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

617 
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

618 
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

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

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

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

622 
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

623 
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

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

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

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

628 
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

629 
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

630 
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

631 
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

632 
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

633 
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

634 
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

635 
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

636 
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

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

638 
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

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

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

642 
using fun_left_comm [of c b] x x' by (auto simp add: o_def) 
15392  643 
qed 
644 
qed 

645 
qed 

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

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

647 

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

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

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

650 
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

651 
apply (blast intro: fold_graph_determ_aux [rule_format]) 
15392  652 
done 
653 

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

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

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

656 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  657 

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

659 

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

660 
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

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

662 

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

663 
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

664 

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

665 
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

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

667 
(\<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

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

669 
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

670 
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

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

672 
done 
15392  673 

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

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

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

676 
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

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

678 
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

679 
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

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

681 

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

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

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

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

685 
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

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

687 
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

688 
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

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

690 

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

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

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

693 
by (simp add: fold_insert fold_fun_comm) 
15392  694 

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

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

696 
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

697 
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

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

699 
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

700 
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

701 
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

702 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  703 
finally show ?thesis . 
704 
qed 

705 

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

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

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

708 
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

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

710 
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

711 
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

712 
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

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

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

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

716 

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

717 
end 
15392  718 

15480  719 
text{* A simplified version for idempotent functions: *} 
720 

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

721 
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

722 
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

723 
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

724 

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

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

726 
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

727 
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

728 

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

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

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

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

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

734 
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

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

737 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  738 
qed 
739 

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

740 
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

741 

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

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

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

744 
by(simp add:fold_fun_comm) 
15484  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 
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

747 

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

748 
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

749 

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

750 
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

751 
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

752 

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

753 
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

754 
by(simp add:fold_image_def) 
15392  755 

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

756 
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

757 
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

758 

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

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

760 
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

761 
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

762 
proof  
29223  763 
interpret I: fun_left_comm "%x y. (g x) * y" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

764 
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

765 
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

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

767 

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

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

769 
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

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

773 
apply (simp add: mult_left_commute [of x]) 
15392  774 
done 
775 

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

778 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  779 
apply (induct set: finite) 
21575  780 
apply simp 
15392  781 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
782 
done 

783 

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

784 
lemma fold_nest_Un_disjoint: 
15392  785 
"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

786 
==> fold times g z (A Un B) = fold times g (fold times g z B) A" 
15392  787 
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

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

789 

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

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

792 
shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A" 
15506  793 
using fin apply induct 
15392  794 
apply simp 
795 
apply simp 

796 
done 

797 

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

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

799 
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

800 
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

801 
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

802 
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

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

804 

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

805 
lemma fold_fusion: 
27611  806 
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

807 
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

808 
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

809 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  810 
proof  
29223  811 
class_interpret ab_semigroup_mult [g] by fact 
27611  812 
show ?thesis using fin hyp by (induct set: finite) simp_all 
813 
qed 

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

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

815 

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

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

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

818 
(!!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

819 
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

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

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

822 
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

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

824 
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

825 
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

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

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

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

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

830 
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

831 
done 
15392  832 

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

833 
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

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

836 
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

837 

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

838 
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

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

840 
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

841 
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

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

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

844 

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

845 
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

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

847 
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

848 
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

849 
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

850 

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

851 
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

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

853 
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

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

855 
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

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

857 
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

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

859 
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

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

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

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

863 

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

864 
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

865 
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

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

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

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

871 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  872 
apply blast 
15506  873 
apply simp 
15392  874 
done 
875 

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

876 
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

877 
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

878 
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

879 
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

880 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

881 
lemma fold_image_related: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

882 
assumes Re: "R e e" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

883 
and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

884 
and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

885 
shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

886 
using fS by (rule finite_subset_induct) (insert assms, auto) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

887 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

888 
lemma fold_image_eq_general: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

889 
assumes fS: "finite S" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

890 
and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

891 
and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

892 
shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

893 
proof 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

894 
from h f12 have hS: "h ` S = S'" by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

895 
{fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

896 
from f12 h H have "x = y" by auto } 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

897 
hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

898 
from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

899 
from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

900 
also have "\<dots> = fold_image (op *) (f2 o h) e S" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

901 
using fold_image_reindex[OF fS hinj, of f2 e] . 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

902 
also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e] 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

903 
by blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

904 
finally show ?thesis .. 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

905 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

906 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

907 
lemma fold_image_eq_general_inverses: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

908 
assumes fS: "finite S" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

909 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

910 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

911 
shows "fold_image (op *) f e S = fold_image (op *) g e T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

912 
(* metis solves it, but not yet available here *) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

913 
apply (rule fold_image_eq_general[OF fS, of T h g f e]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

914 
apply (rule ballI) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

915 
apply (frule kh) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

916 
apply (rule ex1I[]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

917 
apply blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

918 
apply clarsimp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

919 
apply (drule hk) apply simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

920 
apply (rule sym) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

921 
apply (erule conjunct1[OF conjunct2[OF hk]]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

922 
apply (rule ballI) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

923 
apply (drule hk) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

924 
apply blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

925 
done 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

926 

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

927 
end 
22917  928 

15402  929 
subsection {* Generalized summation over a set *} 
930 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30325
diff
changeset

931 
interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +" 
28823  932 
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

933 

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

934 
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

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

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

938 
Setsum ("\<Sum>_" [1000] 999) where 
19535  939 
"\<Sum>A == setsum (%x. x) A" 
940 

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

943 

944 
syntax 

17189  945 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  946 
syntax (xsymbols) 
17189  947 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  948 
syntax (HTML output) 
17189  949 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  950 

951 
translations  {* Beware of argument permutation! *} 

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

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

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

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

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

957 

958 
syntax 

17189  959 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  960 
syntax (xsymbols) 
17189  961 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  962 
syntax (HTML output) 
17189  963 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  964 

965 
translations 

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

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

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

969 
print_translation {* 

970 
let 

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

973 
else let val x' = Syntax.mark_bound x 

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

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

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

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

15402  978 
*} 
979 

19535  980 

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

982 
by (simp add: setsum_def) 
15402  983 

984 
lemma setsum_insert [simp]: 

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

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

986 
by (simp add: setsum_def) 
15402  987 

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

988 
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

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

990 

15402  991 
lemma setsum_reindex: 
992 
"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

993 
by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD) 
15402  994 

995 
lemma setsum_reindex_id: 

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

997 
by (auto simp add: setsum_reindex) 

998 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

999 
lemma setsum_reindex_nonzero: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1000 
assumes fS: "finite S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1001 
and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1002 
shows "setsum h (f ` S) = setsum (h o f) S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1003 
using nz 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1004 
proof(induct rule: finite_induct[OF fS]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1005 
case 1 thus ?case by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1006 
next 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1007 
case (2 x F) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1008 
{assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1009 
then obtain y where y: "y \<in> F" "f x = f y" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1010 
from "2.hyps" y have xy: "x \<noteq> y" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1011 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1012 
from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1013 
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1014 
also have "\<dots> = setsum (h o f) (insert x F)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1015 
unfolding setsum_insert[OF `finite F` `x\<notin>F`] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1016 
using h0 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1017 
apply simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1018 
apply (rule "2.hyps"(3)) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1019 
apply (rule_tac y="y" in "2.prems") 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1020 
apply simp_all 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1021 
done 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1022 
finally have ?case .} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1023 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1024 
{assume fxF: "f x \<notin> f ` F" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1025 
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1026 
using fxF "2.hyps" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1027 
also have "\<dots> = setsum (h o f) (insert x F)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1028 
unfolding setsum_insert[OF `finite F` `x\<notin>F`] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1029 
apply simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1030 
apply (rule cong[OF refl[of "op + (h (f x))"]]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1031 
apply (rule "2.hyps"(3)) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1032 
apply (rule_tac y="y" in "2.prems") 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1033 
apply simp_all 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1034 
done 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1035 
finally have ?case .} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1036 
ultimately show ?case by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1037 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1038 

15402  1039 
lemma setsum_cong: 
1040 
"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

1041 
by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong) 
15402  1042 

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

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

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

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

1046 
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

1047 

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

1049 
by (rule setsum_cong[OF refl], auto); 
15554  1050 

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

1052 
"[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

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

1054 
by (simp add: setsum_reindex cong: setsum_cong) 
15402  1055 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1056 

15542  1057 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  1058 
apply (clarsimp simp: setsum_def) 
15765  1059 
apply (erule finite_induct, auto) 
15402  1060 
done 
1061 

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

15402  1064 

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

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

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

1068 
by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric]) 
15402  1069 

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

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

1072 
by (subst setsum_Un_Int [symmetric], auto) 

1073 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1074 
lemma setsum_mono_zero_left: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1075 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1076 
and z: "\<forall>i \<in> T  S. f i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1077 
shows "setsum f S = setsum f T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1078 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1079 
have eq: "T = S \<union> (T  S)" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1080 
have d: "S \<inter> (T  S) = {}" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1081 
from fT ST have f: "finite S" "finite (T  S)" by (auto intro: finite_subset) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1082 
show ?thesis 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1083 
by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1084 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1085 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1086 
lemma setsum_mono_zero_right: 
30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

1087 
"finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T  S. f i = 0 \<Longrightarrow> setsum f T = setsum f S" 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30729
diff
changeset

1088 
by(blast intro!: setsum_mono_zero_left[symmetric]) 
29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1089 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1090 
lemma setsum_mono_zero_cong_left: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1091 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1092 
and z: "\<forall>i \<in> T  S. g i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1093 
and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1094 
shows "setsum f S = setsum g T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1095 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1096 
have eq: "T = S \<union> (T  S)" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1097 
have d: "S \<inter> (T  S) = {}" using ST by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1098 
from fT ST have f: "finite S" "finite (T  S)" by (auto intro: finite_subset) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1099 
show ?thesis 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1100 
using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1101 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1102 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1103 
lemma setsum_mono_zero_cong_right: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1104 
assumes fT: "finite T" and ST: "S \<subseteq> T" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1105 
and z: "\<forall>i \<in> T  S. f i = 0" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1106 
and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1107 
shows "setsum f T = setsum g S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1108 
using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1109 

3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1110 
lemma setsum_delta: 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1111 
assumes fS: "finite S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1112 
shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1113 
proof 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1114 
let ?f = "(\<lambda>k. if k=a then b k else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1115 
{assume a: "a \<notin> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1116 
hence "\<forall> k\<in> S. ?f k = 0" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1117 
hence ?thesis using a by simp} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1118 
moreover 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1119 
{assume a: "a \<in> S" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1120 
let ?A = "S  {a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1121 
let ?B = "{a}" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1122 
have eq: "S = ?A \<union> ?B" using a by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1123 
have dj: "?A \<inter> ?B = {}" by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1124 
from fS have fAB: "finite ?A" "finite ?B" by auto 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1125 
have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1126 
using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1127 
by simp 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1128 
then have ?thesis using a by simp} 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1129 
ultimately show ?thesis by blast 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1130 
qed 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1131 
lemma setsum_delta': 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1132 
assumes fS: "finite S" shows 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1133 
"setsum (\<lambda>k. if a = k then b k else 0) S = 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1134 
(if a\<in> S then b a else 0)" 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1135 
using setsum_delta[OF fS, of a b, symmetric] 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1136 
by (auto intro: setsum_cong) 
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1137 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1138 
lemma setsum_restrict_set: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1139 
assumes fA: "finite A" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1140 
shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1141 
proof 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1142 
from fA have fab: "finite (A \<inter> B)" by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1143 
have aba: "A \<inter> B \<subseteq> A" by blast 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1144 
let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1145 
from setsum_mono_zero_left[OF fA aba, of ?g] 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1146 
show ?thesis by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1147 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1148 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1149 
lemma setsum_cases: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1150 
assumes fA: "finite A" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1151 
shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A = 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1152 
setsum f (A \<inter> B) + setsum g (A \<inter>  B)" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1153 
proof 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1154 
have a: "A = A \<inter> B \<union> A \<inter> B" "(A \<inter> B) \<inter> (A \<inter> B) = {}" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1155 
by blast+ 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1156 
from fA 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1157 
have f: "finite (A \<inter> B)" "finite (A \<inter> B)" by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1158 
let ?g = "\<lambda>x. if x \<in> B then f x else g x" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1159 
from setsum_Un_disjoint[OF f a(2), of ?g] a(1) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1160 
show ?thesis by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1161 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1162 

29674
3857d7eba390
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
chaieb
parents:
29609
diff
changeset

1163 

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

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

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

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

1169 
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

1170 
by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong) 
15402  1171 

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

1172 
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

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

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

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

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

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

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

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

1182 
done 
15402  1183 

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

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

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

1188 
by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong) 
15402  1189 

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

1190 
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

1191 
lemma setsum_cartesian_product: 
17189  1192 
"(\<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

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

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

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

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

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

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

1200 
done 
15402  1201 

1202 
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

1203 
by(simp add:setsum_def comm_monoid_add.fold_image_distrib) 
15402  1204 

1205 

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

1207 

1208 
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

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

1210 
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

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

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

1213 
done 
15402  1214 

1215 
lemma setsum_eq_0_iff [simp]: 

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

1217 
by (induct set: finite) auto 
15402  1218 

1219 
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

1220 
(setsum f (A Un B) :: nat) = setsum f A + setsum f B  setsum f (A Int B)" 
15402  1221 
 {* For the natural numbers, we have subtraction. *} 
29667  1222 
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) 
15402  1223 

1224 
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

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

1226 
setsum f A + setsum f B  setsum f (A Int B)" 
29667  1227 
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) 
15402  1228 

30260
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1229 
lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1230 
apply (induct set: finite) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1231 
apply simp by (auto simp add: fold_image_insert) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1232 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1233 
lemma (in comm_monoid_mult) fold_image_Un_one: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1234 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1235 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1236 
shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1237 
proof 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1238 
have "fold_image op * f 1 (S \<inter> T) = 1" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1239 
apply (rule fold_image_1) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1240 
using fS fT I0 by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1241 
with fold_image_Un_Int[OF fS fT] show ?thesis by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1242 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1243 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1244 
lemma setsum_eq_general_reverses: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1245 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1246 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1247 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1248 
shows "setsum f S = setsum g T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1249 
apply (simp add: setsum_def fS fT) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1250 
apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1251 
apply (erule kh) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1252 
apply (erule hk) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1253 
done 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1254 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1255 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1256 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1257 
lemma setsum_Un_zero: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1258 
assumes fS: "finite S" and fT: "finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1259 
and I0: "\<forall>x \<in> S\<inter>T. f x = 0" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1260 
shows "setsum f (S \<union> T) = setsum f S + setsum f T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1261 
using fS fT 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1262 
apply (simp add: setsum_def) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1263 
apply (rule comm_monoid_add.fold_image_Un_one) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1264 
using I0 by auto 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1265 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1266 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1267 
lemma setsum_UNION_zero: 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1268 
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1269 
and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1270 
shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1271 
using fSS f0 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1272 
proof(induct rule: finite_induct[OF fS]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1273 
case 1 thus ?case by simp 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1274 
next 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1275 
case (2 T F) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1276 
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1277 
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1278 
from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1279 
from "2.prems" TF fTF 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1280 
show ?case 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1281 
by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f]) 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1282 
qed 
be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1283 

be39acd3ac85
Added general theorems for fold_image, setsum and set_prod
chaieb
parents:
29966
diff
changeset

1284 

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

1286 
(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.
nipk 