author  nipkow 
Sun, 12 Jul 2009 10:14:51 +0200  
changeset 31992  f8aed98faae7 
parent 31916  f3227bb306a4 
child 31993  2ce88db62a84 
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 

31992  221 
lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)" 
222 
by (blast intro: Inter_lower finite_subset) 

223 

224 
lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)" 

225 
by (blast intro: INT_lower finite_subset) 

226 

12396  227 
lemma finite_empty_induct: 
23389  228 
assumes "finite A" 
229 
and "P A" 

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

231 
shows "P {}" 

12396  232 
proof  
233 
have "P (A  A)" 

234 
proof  

23389  235 
{ 
236 
fix c b :: "'a set" 

237 
assume c: "finite c" and b: "finite b" 

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

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

240 
using c 

241 
proof induct 

242 
case empty 

243 
from P1 show ?case by simp 

244 
next 

245 
case (insert x F) 

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

247 
proof (rule P2) 

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

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

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

251 
qed 

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

253 
finally show ?case . 

12396  254 
qed 
23389  255 
} 
256 
then show ?thesis by this (simp_all add: assms) 

12396  257 
qed 
23389  258 
then show ?thesis by simp 
12396  259 
qed 
260 

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

263 

264 
lemma finite_Diff2 [simp]: 

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

266 
proof  

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

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

269 
finally show ?thesis .. 

270 
qed 

271 

272 
lemma finite_compl[simp]: 

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

274 
by(simp add:Compl_eq_Diff_UNIV) 

12396  275 

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

279 

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

282 
apply (case_tac "a : A  B") 

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

14208  284 
apply (subst insert_Diff, simp_all) 
12396  285 
done 
286 

287 

15392  288 
text {* Image and Inverse Image over Finite Sets *} 
13825  289 

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

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

22262  292 
by (induct set: finite) simp_all 
13825  293 

31768  294 
lemma finite_image_set [simp]: 
295 
"finite {x. P x} \<Longrightarrow> finite { f x  x. P x }" 

296 
by (simp add: image_Collect [symmetric]) 

297 

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

298 
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

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

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

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

302 

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

27418  305 
apply (drule finite_imageI, simp add: range_composition) 
13825  306 
done 
307 

12396  308 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
309 
proof  

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

311 
fix B :: "'a set" 

312 
assume "finite B" 

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

314 
apply induct 

315 
apply simp 

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

317 
apply clarify 

318 
apply (simp (no_asm_use) add: inj_on_def) 

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

324 
done 

325 
qed (rule refl) 

326 

327 

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

330 
is included in a singleton. *} 

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

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

332 
apply (blast intro: the_equality [symmetric]) 
13825  333 
done 
334 

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

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

337 
is finite. *} 

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

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

341 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  342 
done 
343 

344 

15392  345 
text {* The finite UNION of finite sets *} 
12396  346 

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

22262  348 
by (induct set: finite) simp_all 
12396  349 

350 
text {* 

351 
Strengthen RHS to 

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

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

354 
We'd need to prove 

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

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

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

360 
by (blast intro: finite_UN_I finite_subset) 

12396  361 

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

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

365 
apply auto 

366 
done 

367 

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

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

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

371 
apply auto 

372 
done 

373 

374 

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

377 

31080  378 
lemma finite_PlusD: 
379 
fixes A :: "'a set" and B :: "'b set" 

380 
assumes fin: "finite (A <+> B)" 

381 
shows "finite A" "finite B" 

382 
proof  

383 
have "Inl ` A \<subseteq> A <+> B" by auto 

384 
hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset) 

385 
thus "finite A" by(rule finite_imageD)(auto intro: inj_onI) 

386 
next 

387 
have "Inr ` B \<subseteq> A <+> B" by auto 

388 
hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset) 

389 
thus "finite B" by(rule finite_imageD)(auto intro: inj_onI) 

390 
qed 

391 

392 
lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B" 

393 
by(auto intro: finite_PlusD finite_Plus) 

394 

395 
lemma finite_Plus_UNIV_iff[simp]: 

396 
"finite (UNIV :: ('a + 'b) set) = 

397 
(finite (UNIV :: 'a set) & finite (UNIV :: 'b set))" 

398 
by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff) 

399 

400 

15392  401 
text {* Sigma of finite sets *} 
12396  402 

403 
lemma finite_SigmaI [simp]: 

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

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

406 

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

409 
by (rule finite_SigmaI) 

410 

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

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

414 
apply (erule ssubst) 

14208  415 
apply (erule finite_SigmaI, auto) 
12396  416 
done 
417 

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

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

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

420 
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

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

422 
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

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

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

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

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

427 
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

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

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

430 
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

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

432 

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

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

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

435 
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

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

437 
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

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

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

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

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

442 
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

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

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

445 
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

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

447 

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

448 

15392  449 
text {* The powerset of a finite set *} 
12396  450 

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

452 
proof 

453 
assume "finite (Pow A)" 

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

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

456 
next 

457 
assume "finite A" 

458 
thus "finite (Pow A)" 

459 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

460 
qed 

461 

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

15392  464 

29918  465 

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

468 

469 

31441  470 
lemma finite_subset_image: 
471 
assumes "finite B" 

472 
shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C" 

473 
using assms proof(induct) 

474 
case empty thus ?case by simp 

475 
next 

476 
case insert thus ?case 

477 
by (clarsimp simp del: image_insert simp add: image_insert[symmetric]) 

478 
blast 

479 
qed 

480 

481 

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

483 

c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour 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 
setup {* Sign.add_path "finite" *}  {*FIXME: name tweaking*} 
29797  485 
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

486 
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

487 
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

488 
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

489 

27430  490 
context finite 
491 
begin 

492 

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

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

495 

27430  496 
end 
497 

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

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

500 

26146  501 
instance unit :: finite 
502 
by default (simp add: UNIV_unit) 

503 

504 
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

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

506 

26146  507 
instance bool :: finite 
508 
by default (simp add: UNIV_bool) 

509 

510 
instance * :: (finite, finite) finite 

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

512 

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

513 
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

514 
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

515 

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

518 
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

519 
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

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

523 
by (simp only: finite_Pow_iff finite) 

524 
ultimately show "finite (range ?graph)" 

525 
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

526 
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

527 
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

528 
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

529 

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

532 

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

533 

15392  534 
subsection {* A fold functional for finite sets *} 
535 

536 
text {* The intended behaviour is 

31916
f3227bb306a4
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
wenzelm
parents:
31907
diff
changeset

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

538 
if @{text f} is ``leftcommutative'': 
15392  539 
*} 
540 

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

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

542 
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

543 
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

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

545 

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

546 
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

547 

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

548 
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

549 
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

550 

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

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

552 

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

553 
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

554 
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

555 
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

556 
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

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

558 

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

559 
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

560 

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

561 
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

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

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

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

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

568 
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

569 

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

570 

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

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

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

573 
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

574 

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

575 
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

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

577 

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

578 
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

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

580 

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

581 

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

582 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  583 

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

587 
lemma insert_image_inj_on_eq: 

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

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

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

591 
apply (auto simp add: image_less_Suc inj_on_def) 

592 
apply (blast intro: less_trans) 

593 
done 

594 

595 
lemma insert_inj_onE: 

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

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

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

599 
proof (cases n) 

600 
case 0 thus ?thesis using aA by auto 

601 
next 

602 
case (Suc m) 

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

15510  609 
show ?thesis 
15520  610 
proof (intro exI conjI) 
611 
show "inj_on ?hm {i. i < m}" using inj_hm 

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

615 
proof (rule insert_image_inj_on_eq) 

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

619 
using aA hkeq nSuc klessn 

620 
by (auto simp add: swap_def image_less_Suc fun_upd_image 

621 
less_Suc_eq inj_on_image_set_diff [OF inj_on]) 

15479  622 
qed 
623 
qed 

624 
qed 

625 

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

626 
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

627 
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

628 

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

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

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

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

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

635 
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

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

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

638 
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

639 
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

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

641 
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

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

643 
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

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

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

646 
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

647 
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

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

649 
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

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

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

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

654 
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

655 
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

656 
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

657 
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

658 
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

659 
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

660 
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

661 
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

662 
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

663 
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

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

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

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

667 
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

668 
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

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

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

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

673 
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

674 
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

675 
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

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

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

683 
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

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

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

687 
using fun_left_comm [of c b] x x' by (auto simp add: o_def) 
15392  688 
qed 
689 
qed 

690 
qed 

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

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

692 

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

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

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

695 
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

696 
apply (blast intro: fold_graph_determ_aux [rule_format]) 
15392  697 
done 
698 

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

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

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

701 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  702 

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

704 

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

705 
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

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

707 

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

708 
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

709 

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

710 
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

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

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

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

714 
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

715 
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

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

717 
done 
15392  718 

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

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

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

721 
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

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

723 
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

724 
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

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

726 

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

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

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

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

730 
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

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

732 
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

733 
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

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

735 

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

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

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

738 
by (simp add: fold_insert fold_fun_comm) 
15392  739 

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

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

741 
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

742 
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

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

744 
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

745 
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

746 
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

747 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  748 
finally show ?thesis . 
749 
qed 

750 

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

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

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

753 
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

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

755 
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

756 
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

757 
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

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

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

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

761 

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

762 
end 
15392  763 

15480  764 
text{* A simplified version for idempotent functions: *} 
765 

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

766 
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

767 
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

768 
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

769 

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

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

771 
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

772 
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

773 

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

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

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

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

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

779 
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

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

782 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  783 
qed 
784 

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

785 
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

786 

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

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

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

789 
by(simp add:fold_fun_comm) 
15484  790 

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

791 
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

792 

31992  793 
context ab_semigroup_idem_mult 
794 
begin 

795 

796 
lemma fun_left_comm_idem: "fun_left_comm_idem(op *)" 

797 
apply unfold_locales 

798 
apply (simp add: mult_ac) 

799 
apply (simp add: mult_idem mult_assoc[symmetric]) 

800 
done 

801 

802 
end 

803 

804 
context lower_semilattice 

805 
begin 

806 

807 
lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf" 

808 
proof qed (rule inf_assoc inf_commute inf_idem)+ 

809 

810 
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)" 

811 
by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]]) 

812 

813 
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A" 

814 
by (induct pred:finite) auto 

815 

816 
lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b" 

817 
proof(induct arbitrary: a pred:finite) 

818 
case empty thus ?case by simp 

819 
next 

820 
case (insert x A) 

821 
show ?case 

822 
proof cases 

823 
assume "A = {}" thus ?thesis using insert by simp 

824 
next 

825 
assume "A \<noteq> {}" thus ?thesis using insert by auto 

826 
qed 

827 
qed 

828 

829 
end 

830 

831 
context upper_semilattice 

832 
begin 

833 

834 
lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup" 

835 
by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_lattice) 

836 

837 
lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)" 

838 
by(rule lower_semilattice.fold_inf_insert)(rule dual_lattice) 

839 

840 
lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c" 

841 
by(rule lower_semilattice.inf_le_fold_inf)(rule dual_lattice) 

842 

843 
lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A" 

844 
by(rule lower_semilattice.fold_inf_le_inf)(rule dual_lattice) 

845 

846 
end 

847 

848 

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

849 
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

850 

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

851 
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

852 
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

853 

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

854 
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

855 
by(simp add:fold_image_def) 
15392  856 

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

857 
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

858 
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

859 

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

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

861 
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

862 
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

863 
proof  
29223  864 
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

865 
by unfold_locales (simp add: mult_ac) 
31992  866 
show ?thesis using assms by(simp add:fold_image_def) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

868 

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

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

870 
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

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

874 
apply (simp add: mult_left_commute [of x]) 
15392  875 
done 
876 

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

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

879 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  880 
apply (induct set: finite) 
21575  881 
apply simp 
15392  882 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
883 
done 

884 

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

885 
lemma fold_nest_Un_disjoint: 
15392  886 
"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

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

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

890 

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

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

893 
shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A" 
31992  894 
using fin by induct auto 
15392  895 

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

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

897 
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

898 
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

899 
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

900 
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

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

902 

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

903 
lemma fold_fusion: 
27611  904 
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

905 
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

906 
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

907 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  908 
proof  
29223  909 
class_interpret ab_semigroup_mult [g] by fact 
27611  910 
show ?thesis using fin hyp by (induct set: finite) simp_all 
911 
qed 

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

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

913 

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

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

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

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

917 
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

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

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

920 
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

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

922 
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

923 
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

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

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

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

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

928 
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

929 
done 
15392  930 

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

931 
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

932 

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

934 
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

935 

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

936 
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

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

938 
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

939 
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

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

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

942 

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

943 
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

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

945 
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

946 
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

947 
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

948 

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

949 
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

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

951 
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

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

953 
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

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

955 
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

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

957 
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

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

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

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

961 

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

962 
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

963 
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

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

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

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

969 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  970 
apply blast 
15506  971 
apply simp 
15392  972 
done 
973 

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

974 
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

975 
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

976 
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

977 
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

978 

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

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

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

981 
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

982 
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

983 
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

984 
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

985 

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

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

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

988 
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

989 
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

990 
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

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

992 
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

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

994 
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

995 
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

996 
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

997 
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

998 
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

999 
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

1000 
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

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

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

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

1004 

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

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

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

1007 
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

1008 
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

1009 
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

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

1011 
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

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

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

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

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

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

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

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

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

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

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

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

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

1024 

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

1025 
end 
22917  1026 

15402  1027 
subsection {* Generalized summation over a set *} 
1028 

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

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

1031 

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

1032 
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

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

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

1036 
Setsum ("\<Sum>_" [1000] 999) where 
19535  1037 
"\<Sum>A == setsum (%x. x) A" 
1038 

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

1041 

1042 
syntax 

17189  1043 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) 
15402  1044 
syntax (xsymbols) 
17189  1045 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  1046 
syntax (HTML output) 
17189  1047 
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) 
15402  1048 

1049 
translations  {* Beware of argument permutation! *} 

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

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

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

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

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

1055 

1056 
syntax 

17189  1057 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ / _./ _)" [0,0,10] 10) 
15402  1058 
syntax (xsymbols) 
17189  1059 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  1060 
syntax (HTML output) 
17189  1061 
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_  (_)./ _)" [0,0,10] 10) 
15402  1062 

1063 
translations 

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

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

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

1067 
print_translation {* 

1068 
let 

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

1071 
else let val x' = Syntax.mark_bound x 

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

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

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

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

15402  1076 
*} 
1077 

19535  1078 

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

1080 
by (simp add: setsum_def) 
15402  1081 

1082 
lemma setsum_insert [simp]: 

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

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

1084 
by (simp add: setsum_def) 
15402  1085 

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

1086 
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

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

1088 

15402  1089 
lemma setsum_reindex: 
1090 
"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

1091 
by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD) 
15402  1092 

1093 
lemma setsum_reindex_id: 

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

1095 
by (auto simp add: setsum_reindex) 

1096 

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

1097 
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

1098 
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

1099 
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

1100 
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

1101 
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

1102 
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

1103 
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

1104 
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

1105 
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

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

1107 
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

1108 
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

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

1111 
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

1112 
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

1113 
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

1114 
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

1115 
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

1116 
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

1117 
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

1118 
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

1119 
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

1120 
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

1121 
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

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

1123 
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

1124 
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

1125 
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

1126 
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

1127 
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

1128 
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

1129 
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

1130 
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

1131 
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

1132 
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

1133 
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

1134 
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

1135 
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

1136 

15402  1137 
lemma setsum_cong: 
1138 
"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

1139 
by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong) 
15402  1140 

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

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

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

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

1144 
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

1145 

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

1147 
by (rule setsum_cong[OF refl], auto); 
15554  1148 

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

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

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

1152 
by (simp add: setsum_reindex cong: setsum_cong) 
15402  1153 

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

1154 

15542  1155 
lemma setsum_0[simp]: "setsum (%i. 0) A = 0" 
15402  1156 
apply (clarsimp simp: setsum_def) 
15765  1157 
apply (erule finite_induct, auto) 
15402  1158 
done 
1159 

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

15402  1162 

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

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

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

1166 
by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric]) 
15402  1167 

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

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

1170 
by (subst setsum_Un_Int [symmetric], auto) 

1171 

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

1172 
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

1173 
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

1174 
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

1175 
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

1176 
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

1177 
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

1178 
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

1179 
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

1180 
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

1181 
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

1182 
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

1183 

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

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

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

1186 
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

1187 

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

1188 
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

1189 
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

1190 
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

1191 
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

1192 
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

1193 
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

1194 
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

1195 
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

1196 
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

1197 
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

1198 
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

1199 
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

1200 

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

1201 
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

1202 
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

1203 
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

1204 
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

1205 
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

1206 
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

1207 

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

1208 
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

1209 
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

1210 
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

1211 
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

1212 
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

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

1214 
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

1215 
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

1216 
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

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

1218 
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

1219 
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

1220 
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

1221 
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

1222 
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

1223 
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

1224 
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

1225 
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

1226 
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

1227 
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

1228 
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

1229 
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

1230 
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

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

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

1233 
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

1234 
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

1235 

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

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

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

1238 
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

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

1240 
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

1241 
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

1242 
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

1243 
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

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

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

1246 

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

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

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

1249 
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

1250 
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

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

1252 
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

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

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

1255 
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

1256 
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

1257 
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

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

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

1260 

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

1261 

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

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

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

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

1267 
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

1268 
by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong) 
15402  1269 

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

1270 
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

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

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

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

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

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

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

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

1280 
done 
15402  1281 

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

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

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

1286 
by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong) 
15402  1287 

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

1288 
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

1289 
lemma setsum_cartesian_product: 
17189  1290 
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)" 
15409
