author  haftmann 
Mon, 05 Sep 2011 07:49:31 +0200  
changeset 44831  4ea848959340 
parent 43991  f4a7697011c5 
child 44835  ff6b9eb9c5ef 
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 
38400
9bfcb1507c6b
import swap prevents strange failure of SML code generator for datatypes
haftmann
parents:
37770
diff
changeset

9 
imports Option Power 
15131  10 
begin 
12396  11 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

12 
subsection {* Predicate for finite sets *} 
12396  13 

41656  14 
inductive finite :: "'a set \<Rightarrow> bool" 
22262  15 
where 
16 
emptyI [simp, intro!]: "finite {}" 

41656  17 
 insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" 
18 

19 
lemma finite_induct [case_names empty insert, induct set: finite]: 

20 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 

21 
assumes "finite F" 

22 
assumes "P {}" 

23 
and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)" 

24 
shows "P F" 

25 
using `finite F` proof induct 

26 
show "P {}" by fact 

27 
fix x F assume F: "finite F" and P: "P F" 

28 
show "P (insert x F)" 

29 
proof cases 

30 
assume "x \<in> F" 

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

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

33 
next 

34 
assume "x \<notin> F" 

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

36 
qed 

37 
qed 

38 

39 

40 
subsubsection {* Choice principles *} 

12396  41 

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

45 
proof  

28823  46 
from assms have "A \<noteq> UNIV" by blast 
41656  47 
then show ?thesis by blast 
12396  48 
qed 
49 

41656  50 
text {* A finite choice principle. Does not need the SOME choice operator. *} 
15484  51 

29923  52 
lemma finite_set_choice: 
41656  53 
"finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)" 
54 
proof (induct rule: finite_induct) 

55 
case empty then show ?case by simp 

29923  56 
next 
57 
case (insert a A) 

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

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

60 
proof 

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

62 
qed 

63 
qed 

64 

23878  65 

41656  66 
subsubsection {* Finite sets are the images of initial segments of natural numbers *} 
15392  67 

15510  68 
lemma finite_imp_nat_seg_image_inj_on: 
41656  69 
assumes "finite A" 
70 
shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}" 

71 
using assms proof induct 

15392  72 
case empty 
41656  73 
show ?case 
74 
proof 

75 
show "\<exists>f. {} = f ` {i::nat. i < 0} \<and> inj_on f {i. i < 0}" by simp 

15510  76 
qed 
15392  77 
next 
78 
case (insert a A) 

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

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

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

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

15392  85 
thus ?case by blast 
86 
qed 

87 

88 
lemma nat_seg_image_imp_finite: 

41656  89 
"A = f ` {i::nat. i < n} \<Longrightarrow> finite A" 
90 
proof (induct n arbitrary: A) 

15392  91 
case 0 thus ?case by simp 
92 
next 

93 
case (Suc n) 

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

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

96 
show ?case 

97 
proof cases 

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

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

100 
thus ?thesis using finB by simp 

101 
next 

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

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

104 
thus ?thesis using finB by simp 

105 
qed 

106 
qed 

107 

108 
lemma finite_conv_nat_seg_image: 

41656  109 
"finite A \<longleftrightarrow> (\<exists>(n::nat) f. A = f ` {i::nat. i < n})" 
110 
by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 

15392  111 

32988  112 
lemma finite_imp_inj_to_nat_seg: 
41656  113 
assumes "finite A" 
114 
shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A" 

32988  115 
proof  
116 
from finite_imp_nat_seg_image_inj_on[OF `finite A`] 

117 
obtain f and n::nat where bij: "bij_betw f {i. i<n} A" 

118 
by (auto simp:bij_betw_def) 

33057  119 
let ?f = "the_inv_into {i. i<n} f" 
32988  120 
have "inj_on ?f A & ?f ` A = {i. i<n}" 
33057  121 
by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij]) 
32988  122 
thus ?thesis by blast 
123 
qed 

124 

41656  125 
lemma finite_Collect_less_nat [iff]: 
126 
"finite {n::nat. n < k}" 

127 
by (fastsimp simp: finite_conv_nat_seg_image) 

29920  128 

41656  129 
lemma finite_Collect_le_nat [iff]: 
130 
"finite {n::nat. n \<le> k}" 

131 
by (simp add: le_eq_less_or_eq Collect_disj_eq) 

15392  132 

41656  133 

134 
subsubsection {* Finiteness and common set operations *} 

12396  135 

41656  136 
lemma rev_finite_subset: 
137 
"finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A" 

138 
proof (induct arbitrary: A rule: finite_induct) 

139 
case empty 

140 
then show ?case by simp 

141 
next 

142 
case (insert x F A) 

143 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F \<Longrightarrow> finite (A  {x})" by fact+ 

144 
show "finite A" 

145 
proof cases 

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

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

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

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

150 
also have "insert x (A  {x}) = A" using x by (rule insert_Diff) 

151 
finally show ?thesis . 

12396  152 
next 
41656  153 
show "A \<subseteq> F ==> ?thesis" by fact 
154 
assume "x \<notin> A" 

155 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

12396  156 
qed 
157 
qed 

158 

41656  159 
lemma finite_subset: 
160 
"A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A" 

161 
by (rule rev_finite_subset) 

29901  162 

41656  163 
lemma finite_UnI: 
164 
assumes "finite F" and "finite G" 

165 
shows "finite (F \<union> G)" 

166 
using assms by induct simp_all 

31992  167 

41656  168 
lemma finite_Un [iff]: 
169 
"finite (F \<union> G) \<longleftrightarrow> finite F \<and> finite G" 

170 
by (blast intro: finite_UnI finite_subset [of _ "F \<union> G"]) 

31992  171 

41656  172 
lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A" 
12396  173 
proof  
41656  174 
have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp 
175 
then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un) 

23389  176 
then show ?thesis by simp 
12396  177 
qed 
178 

41656  179 
lemma finite_Int [simp, intro]: 
180 
"finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)" 

181 
by (blast intro: finite_subset) 

182 

183 
lemma finite_Collect_conjI [simp, intro]: 

184 
"finite {x. P x} \<or> finite {x. Q x} \<Longrightarrow> finite {x. P x \<and> Q x}" 

185 
by (simp add: Collect_conj_eq) 

186 

187 
lemma finite_Collect_disjI [simp]: 

188 
"finite {x. P x \<or> Q x} \<longleftrightarrow> finite {x. P x} \<and> finite {x. Q x}" 

189 
by (simp add: Collect_disj_eq) 

190 

191 
lemma finite_Diff [simp, intro]: 

192 
"finite A \<Longrightarrow> finite (A  B)" 

193 
by (rule finite_subset, rule Diff_subset) 

29901  194 

195 
lemma finite_Diff2 [simp]: 

41656  196 
assumes "finite B" 
197 
shows "finite (A  B) \<longleftrightarrow> finite A" 

29901  198 
proof  
41656  199 
have "finite A \<longleftrightarrow> finite((A  B) \<union> (A \<inter> B))" by (simp add: Un_Diff_Int) 
200 
also have "\<dots> \<longleftrightarrow> finite (A  B)" using `finite B` by simp 

29901  201 
finally show ?thesis .. 
202 
qed 

203 

41656  204 
lemma finite_Diff_insert [iff]: 
205 
"finite (A  insert a B) \<longleftrightarrow> finite (A  B)" 

206 
proof  

207 
have "finite (A  B) \<longleftrightarrow> finite (A  B  {a})" by simp 

208 
moreover have "A  insert a B = A  B  {a}" by auto 

209 
ultimately show ?thesis by simp 

210 
qed 

211 

29901  212 
lemma finite_compl[simp]: 
41656  213 
"finite (A :: 'a set) \<Longrightarrow> finite ( A) \<longleftrightarrow> finite (UNIV :: 'a set)" 
214 
by (simp add: Compl_eq_Diff_UNIV) 

12396  215 

29916  216 
lemma finite_Collect_not[simp]: 
41656  217 
"finite {x :: 'a. P x} \<Longrightarrow> finite {x. \<not> P x} \<longleftrightarrow> finite (UNIV :: 'a set)" 
218 
by (simp add: Collect_neg_eq) 

219 

220 
lemma finite_Union [simp, intro]: 

221 
"finite A \<Longrightarrow> (\<And>M. M \<in> A \<Longrightarrow> finite M) \<Longrightarrow> finite(\<Union>A)" 

222 
by (induct rule: finite_induct) simp_all 

223 

224 
lemma finite_UN_I [intro]: 

225 
"finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)" 

226 
by (induct rule: finite_induct) simp_all 

29903  227 

41656  228 
lemma finite_UN [simp]: 
229 
"finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))" 

230 
by (blast intro: finite_subset) 

231 

232 
lemma finite_Inter [intro]: 

233 
"\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)" 

234 
by (blast intro: Inter_lower finite_subset) 

12396  235 

41656  236 
lemma finite_INT [intro]: 
237 
"\<exists>x\<in>I. finite (A x) \<Longrightarrow> finite (\<Inter>x\<in>I. A x)" 

238 
by (blast intro: INT_lower finite_subset) 

13825  239 

41656  240 
lemma finite_imageI [simp, intro]: 
241 
"finite F \<Longrightarrow> finite (h ` F)" 

242 
by (induct rule: finite_induct) simp_all 

13825  243 

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

246 
by (simp add: image_Collect [symmetric]) 

247 

41656  248 
lemma finite_imageD: 
42206  249 
assumes "finite (f ` A)" and "inj_on f A" 
250 
shows "finite A" 

251 
using assms proof (induct "f ` A" arbitrary: A) 

252 
case empty then show ?case by simp 

253 
next 

254 
case (insert x B) 

255 
then have B_A: "insert x B = f ` A" by simp 

256 
then obtain y where "x = f y" and "y \<in> A" by blast 

257 
from B_A `x \<notin> B` have "B = f ` A  {x}" by blast 

258 
with B_A `x \<notin> B` `x = f y` `inj_on f A` `y \<in> A` have "B = f ` (A  {y})" by (simp add: inj_on_image_set_diff) 

259 
moreover from `inj_on f A` have "inj_on f (A  {y})" by (rule inj_on_diff) 

260 
ultimately have "finite (A  {y})" by (rule insert.hyps) 

261 
then show "finite A" by simp 

262 
qed 

12396  263 

41656  264 
lemma finite_surj: 
265 
"finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B" 

266 
by (erule finite_subset) (rule finite_imageI) 

12396  267 

41656  268 
lemma finite_range_imageI: 
269 
"finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))" 

270 
by (drule finite_imageI) (simp add: range_composition) 

13825  271 

41656  272 
lemma finite_subset_image: 
273 
assumes "finite B" 

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

275 
using assms proof induct 

276 
case empty then show ?case by simp 

277 
next 

278 
case insert then show ?case 

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

280 
blast 

281 
qed 

282 

43991  283 
lemma finite_vimage_IntI: 
284 
"finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h ` F \<inter> A)" 

41656  285 
apply (induct rule: finite_induct) 
21575  286 
apply simp_all 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

287 
apply (subst vimage_insert) 
43991  288 
apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2) 
13825  289 
done 
290 

43991  291 
lemma finite_vimageI: 
292 
"finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h ` F)" 

293 
using finite_vimage_IntI[of F h UNIV] by auto 

294 

34111
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

295 
lemma finite_vimageD: 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

296 
assumes fin: "finite (h ` F)" and surj: "surj h" 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

297 
shows "finite F" 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

298 
proof  
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

299 
have "finite (h ` (h ` F))" using fin by (rule finite_imageI) 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

300 
also have "h ` (h ` F) = F" using surj by (rule surj_image_vimage_eq) 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

301 
finally show "finite F" . 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

302 
qed 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

303 

1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

304 
lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h ` F) \<longleftrightarrow> finite F" 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

305 
unfolding bij_def by (auto elim: finite_vimageD finite_vimageI) 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

306 

41656  307 
lemma finite_Collect_bex [simp]: 
308 
assumes "finite A" 

309 
shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})" 

310 
proof  

311 
have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto 

312 
with assms show ?thesis by simp 

313 
qed 

12396  314 

41656  315 
lemma finite_Collect_bounded_ex [simp]: 
316 
assumes "finite {y. P y}" 

317 
shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})" 

318 
proof  

319 
have "{x. EX y. P y & Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})" by auto 

320 
with assms show ?thesis by simp 

321 
qed 

29920  322 

41656  323 
lemma finite_Plus: 
324 
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)" 

325 
by (simp add: Plus_def) 

17022  326 

31080  327 
lemma finite_PlusD: 
328 
fixes A :: "'a set" and B :: "'b set" 

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

330 
shows "finite A" "finite B" 

331 
proof  

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

41656  333 
then have "finite (Inl ` A :: ('a + 'b) set)" using fin by (rule finite_subset) 
334 
then show "finite A" by (rule finite_imageD) (auto intro: inj_onI) 

31080  335 
next 
336 
have "Inr ` B \<subseteq> A <+> B" by auto 

41656  337 
then have "finite (Inr ` B :: ('a + 'b) set)" using fin by (rule finite_subset) 
338 
then show "finite B" by (rule finite_imageD) (auto intro: inj_onI) 

31080  339 
qed 
340 

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

343 
by (auto intro: finite_PlusD finite_Plus) 

31080  344 

41656  345 
lemma finite_Plus_UNIV_iff [simp]: 
346 
"finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)" 

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

12396  348 

40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
40716
diff
changeset

349 
lemma finite_SigmaI [simp, intro]: 
41656  350 
"finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)" 
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
40716
diff
changeset

351 
by (unfold Sigma_def) blast 
12396  352 

41656  353 
lemma finite_cartesian_product: 
354 
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)" 

15402  355 
by (rule finite_SigmaI) 
356 

12396  357 
lemma finite_Prod_UNIV: 
41656  358 
"finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)" 
359 
by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product) 

12396  360 

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

361 
lemma finite_cartesian_productD1: 
42207  362 
assumes "finite (A \<times> B)" and "B \<noteq> {}" 
363 
shows "finite A" 

364 
proof  

365 
from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}" 

366 
by (auto simp add: finite_conv_nat_seg_image) 

367 
then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp 

368 
with `B \<noteq> {}` have "A = (fst \<circ> f) ` {i::nat. i < n}" 

369 
by (simp add: image_compose) 

370 
then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast 

371 
then show ?thesis 

372 
by (auto simp add: finite_conv_nat_seg_image) 

373 
qed 

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

374 

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

375 
lemma finite_cartesian_productD2: 
42207  376 
assumes "finite (A \<times> B)" and "A \<noteq> {}" 
377 
shows "finite B" 

378 
proof  

379 
from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}" 

380 
by (auto simp add: finite_conv_nat_seg_image) 

381 
then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp 

382 
with `A \<noteq> {}` have "B = (snd \<circ> f) ` {i::nat. i < n}" 

383 
by (simp add: image_compose) 

384 
then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast 

385 
then show ?thesis 

386 
by (auto simp add: finite_conv_nat_seg_image) 

387 
qed 

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

388 

41656  389 
lemma finite_Pow_iff [iff]: 
390 
"finite (Pow A) \<longleftrightarrow> finite A" 

12396  391 
proof 
392 
assume "finite (Pow A)" 

41656  393 
then have "finite ((%x. {x}) ` A)" by (blast intro: finite_subset) 
394 
then show "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp 

12396  395 
next 
396 
assume "finite A" 

41656  397 
then show "finite (Pow A)" 
35216  398 
by induct (simp_all add: Pow_insert) 
12396  399 
qed 
400 

41656  401 
corollary finite_Collect_subsets [simp, intro]: 
402 
"finite A \<Longrightarrow> finite {B. B \<subseteq> A}" 

403 
by (simp add: Pow_def [symmetric]) 

29918  404 

15392  405 
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A" 
41656  406 
by (blast intro: finite_subset [OF subset_Pow_Union]) 
15392  407 

408 

41656  409 
subsubsection {* Further induction rules on finite sets *} 
410 

411 
lemma finite_ne_induct [case_names singleton insert, consumes 2]: 

412 
assumes "finite F" and "F \<noteq> {}" 

413 
assumes "\<And>x. P {x}" 

414 
and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)" 

415 
shows "P F" 

416 
using assms proof induct 

417 
case empty then show ?case by simp 

418 
next 

419 
case (insert x F) then show ?case by cases auto 

420 
qed 

421 

422 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 

423 
assumes "finite F" and "F \<subseteq> A" 

424 
assumes empty: "P {}" 

425 
and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)" 

426 
shows "P F" 

427 
using `finite F` `F \<subseteq> A` proof induct 

428 
show "P {}" by fact 

31441  429 
next 
41656  430 
fix x F 
431 
assume "finite F" and "x \<notin> F" and 

432 
P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A" 

433 
show "P (insert x F)" 

434 
proof (rule insert) 

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

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

437 
with P show "P F" . 

438 
show "finite F" by fact 

439 
show "x \<notin> F" by fact 

440 
qed 

441 
qed 

442 

443 
lemma finite_empty_induct: 

444 
assumes "finite A" 

445 
assumes "P A" 

446 
and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A  {a})" 

447 
shows "P {}" 

448 
proof  

449 
have "\<And>B. B \<subseteq> A \<Longrightarrow> P (A  B)" 

450 
proof  

451 
fix B :: "'a set" 

452 
assume "B \<subseteq> A" 

453 
with `finite A` have "finite B" by (rule rev_finite_subset) 

454 
from this `B \<subseteq> A` show "P (A  B)" 

455 
proof induct 

456 
case empty 

457 
from `P A` show ?case by simp 

458 
next 

459 
case (insert b B) 

460 
have "P (A  B  {b})" 

461 
proof (rule remove) 

462 
from `finite A` show "finite (A  B)" by induct auto 

463 
from insert show "b \<in> A  B" by simp 

464 
from insert show "P (A  B)" by simp 

465 
qed 

466 
also have "A  B  {b} = A  insert b B" by (rule Diff_insert [symmetric]) 

467 
finally show ?case . 

468 
qed 

469 
qed 

470 
then have "P (A  A)" by blast 

471 
then show ?thesis by simp 

31441  472 
qed 
473 

474 

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

476 

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

478 
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" 
27430  479 
begin 
480 

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

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

483 

43866
8a50dc70cbff
moving UNIV = ... equations to their proper theories
haftmann
parents:
42875
diff
changeset

484 
lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True" 
40922
4d0f96a54e76
adding code equation for finiteness of finite types
bulwahn
parents:
40786
diff
changeset

485 
by simp 
4d0f96a54e76
adding code equation for finiteness of finite types
bulwahn
parents:
40786
diff
changeset

486 

27430  487 
end 
488 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37466
diff
changeset

489 
instance prod :: (finite, finite) finite proof 
35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

490 
qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 
26146  491 

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

492 
lemma inj_graph: "inj (%f. {(x, y). y = f x})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

493 
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff) 
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

494 

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

497 
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

498 
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

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

502 
by (simp only: finite_Pow_iff finite) 

503 
ultimately show "finite (range ?graph)" 

504 
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

505 
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

506 
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

507 
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

508 

44831  509 
instance bool :: finite proof 
510 
qed (simp add: UNIV_bool) 

511 

512 
instance unit :: finite proof 

513 
qed (simp add: UNIV_unit) 

514 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37466
diff
changeset

515 
instance sum :: (finite, finite) finite proof 
35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

516 
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 
27981  517 

44831  518 
lemma finite_option_UNIV [simp]: 
519 
"finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" 

520 
by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) 

521 

522 
instance option :: (finite) finite proof 

523 
qed (simp add: UNIV_option_conv) 

524 

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

525 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

526 
subsection {* A basic fold functional for finite sets *} 
15392  527 

528 
text {* The intended behaviour is 

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

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

530 
if @{text f} is ``leftcommutative'': 
15392  531 
*} 
532 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

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

534 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

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

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

537 

42809
5b45125b15ba
use pointfree characterisation for fold_set locale
haftmann
parents:
42715
diff
changeset

538 
lemma fun_left_comm: "f x (f y z) = f y (f x z)" 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

539 
using comp_fun_commute by (simp add: fun_eq_iff) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

540 

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

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

542 

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

543 
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

544 
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

545 
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

546 
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

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

548 

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

549 
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

550 

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

551 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where 
37767  552 
"fold f z A = (THE y. fold_graph f z A y)" 
15392  553 

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

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

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

558 
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

559 

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

560 
lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x" 
41656  561 
by (induct rule: finite_induct) auto 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

562 

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

563 

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

564 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  565 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

566 
context comp_fun_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

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

568 

36045  569 
lemma fold_graph_insertE_aux: 
570 
"fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A  {a}) y'" 

571 
proof (induct set: fold_graph) 

572 
case (insertI x A y) show ?case 

573 
proof (cases "x = a") 

574 
assume "x = a" with insertI show ?case by auto 

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

575 
next 
36045  576 
assume "x \<noteq> a" 
577 
then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A  {a}) y'" 

578 
using insertI by auto 

42875  579 
have "f x y = f a (f x y')" 
36045  580 
unfolding y by (rule fun_left_comm) 
42875  581 
moreover have "fold_graph f z (insert x A  {a}) (f x y')" 
36045  582 
using y' and `x \<noteq> a` and `x \<notin> A` 
583 
by (simp add: insert_Diff_if fold_graph.insertI) 

42875  584 
ultimately show ?case by fast 
15392  585 
qed 
36045  586 
qed simp 
587 

588 
lemma fold_graph_insertE: 

589 
assumes "fold_graph f z (insert x A) v" and "x \<notin> A" 

590 
obtains y where "v = f x y" and "fold_graph f z A y" 

591 
using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1]) 

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

592 

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

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

594 
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 
36045  595 
proof (induct arbitrary: y set: fold_graph) 
596 
case (insertI x A y v) 

597 
from `fold_graph f z (insert x A) v` and `x \<notin> A` 

598 
obtain y' where "v = f x y'" and "fold_graph f z A y'" 

599 
by (rule fold_graph_insertE) 

600 
from `fold_graph f z A y'` have "y' = y" by (rule insertI) 

601 
with `v = f x y'` show "v = f x y" by simp 

602 
qed fast 

15392  603 

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

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

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

606 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  607 

42272  608 
lemma fold_graph_fold: 
609 
assumes "finite A" 

610 
shows "fold_graph f z A (fold f z A)" 

611 
proof  

612 
from assms have "\<exists>x. fold_graph f z A x" by (rule finite_imp_fold_graph) 

613 
moreover note fold_graph_determ 

614 
ultimately have "\<exists>!x. fold_graph f z A x" by (rule ex_ex1I) 

615 
then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI') 

616 
then show ?thesis by (unfold fold_def) 

617 
qed 

36045  618 

15392  619 
text{* The base case for @{text fold}: *} 
620 

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

621 
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

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

623 

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

624 
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

625 

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

626 
lemma fold_insert [simp]: 
42875  627 
assumes "finite A" and "x \<notin> A" 
628 
shows "fold f z (insert x A) = f x (fold f z A)" 

629 
proof (rule fold_equality) 

630 
from `finite A` have "fold_graph f z A (fold f z A)" by (rule fold_graph_fold) 

631 
with `x \<notin> A`show "fold_graph f z (insert x A) (f x (fold f z A))" by (rule fold_graph.insertI) 

632 
qed 

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

633 

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

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

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

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

637 
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

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

639 
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

640 
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

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

642 

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

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

644 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
35216  645 
by (simp add: fold_fun_comm) 
15392  646 

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

647 
lemma fold_rec: 
42875  648 
assumes "finite A" and "x \<in> A" 
649 
shows "fold f z A = f x (fold f z (A  {x}))" 

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

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

651 
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

652 
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

653 
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

654 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  655 
finally show ?thesis . 
656 
qed 

657 

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

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

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

660 
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

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

662 
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

663 
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

664 
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

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

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

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

668 

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

669 
end 
15392  670 

15480  671 
text{* A simplified version for idempotent functions: *} 
672 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

673 
locale comp_fun_idem = comp_fun_commute + 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

674 
assumes comp_fun_idem: "f x o f x = f x" 
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

675 
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

676 

42869
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

677 
lemma fun_left_idem: "f x (f x z) = f x z" 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

678 
using comp_fun_idem by (simp add: fun_eq_iff) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

679 

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

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

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

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

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

685 
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

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

688 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  689 
qed 
690 

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

691 
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

692 

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

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

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

695 
by(simp add:fold_fun_comm) 
15484  696 

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

697 
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

698 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

699 

d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

700 
subsubsection {* Expressing set operations via @{const fold} *} 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

701 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

702 
lemma (in comp_fun_commute) comp_comp_fun_commute: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

703 
"comp_fun_commute (f \<circ> g)" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

704 
proof 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

705 
qed (simp_all add: comp_fun_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

706 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

707 
lemma (in comp_fun_idem) comp_comp_fun_idem: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

708 
"comp_fun_idem (f \<circ> g)" 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

709 
by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales) 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

710 
(simp_all add: comp_fun_idem) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

711 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

712 
lemma comp_fun_idem_insert: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

713 
"comp_fun_idem insert" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

714 
proof 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

715 
qed auto 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

716 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

717 
lemma comp_fun_idem_remove: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

718 
"comp_fun_idem (\<lambda>x A. A  {x})" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

719 
proof 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

720 
qed auto 
31992  721 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

722 
lemma (in semilattice_inf) comp_fun_idem_inf: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

723 
"comp_fun_idem inf" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

724 
proof 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

725 
qed (auto simp add: inf_left_commute) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

726 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

727 
lemma (in semilattice_sup) comp_fun_idem_sup: 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

728 
"comp_fun_idem sup" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

729 
proof 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

730 
qed (auto simp add: sup_left_commute) 
31992  731 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

732 
lemma union_fold_insert: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

733 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

734 
shows "A \<union> B = fold insert B A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

735 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

736 
interpret comp_fun_idem insert by (fact comp_fun_idem_insert) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

737 
from `finite A` show ?thesis by (induct A arbitrary: B) simp_all 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

738 
qed 
31992  739 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

740 
lemma minus_fold_remove: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

741 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

742 
shows "B  A = fold (\<lambda>x A. A  {x}) B A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

743 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

744 
interpret comp_fun_idem "\<lambda>x A. A  {x}" by (fact comp_fun_idem_remove) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

745 
from `finite A` show ?thesis by (induct A arbitrary: B) auto 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

746 
qed 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

747 

d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

748 
context complete_lattice 
31992  749 
begin 
750 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

751 
lemma inf_Inf_fold_inf: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

752 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

753 
shows "inf B (Inf A) = fold inf B A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

754 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

755 
interpret comp_fun_idem inf by (fact comp_fun_idem_inf) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

756 
from `finite A` show ?thesis by (induct A arbitrary: B) 
41550  757 
(simp_all add: Inf_insert inf_commute fold_fun_comm) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

758 
qed 
31992  759 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

760 
lemma sup_Sup_fold_sup: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

761 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

762 
shows "sup B (Sup A) = fold sup B A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

763 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

764 
interpret comp_fun_idem sup by (fact comp_fun_idem_sup) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

765 
from `finite A` show ?thesis by (induct A arbitrary: B) 
41550  766 
(simp_all add: Sup_insert sup_commute fold_fun_comm) 
31992  767 
qed 
768 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

769 
lemma Inf_fold_inf: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

770 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

771 
shows "Inf A = fold inf top A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

772 
using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

773 

d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

774 
lemma Sup_fold_sup: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

775 
assumes "finite A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

776 
shows "Sup A = fold sup bot A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

777 
using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) 
31992  778 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

779 
lemma inf_INFI_fold_inf: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

780 
assumes "finite A" 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

781 
shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

782 
proof (rule sym) 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

783 
interpret comp_fun_idem inf by (fact comp_fun_idem_inf) 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

784 
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem) 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

785 
from `finite A` show "?fold = ?inf" 
42869
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

786 
by (induct A arbitrary: B) 
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

787 
(simp_all add: INFI_def Inf_insert inf_left_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

788 
qed 
31992  789 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

790 
lemma sup_SUPR_fold_sup: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

791 
assumes "finite A" 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

792 
shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

793 
proof (rule sym) 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

794 
interpret comp_fun_idem sup by (fact comp_fun_idem_sup) 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

795 
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem) 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

796 
from `finite A` show "?fold = ?sup" 
42869
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

797 
by (induct A arbitrary: B) 
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

798 
(simp_all add: SUPR_def Sup_insert sup_left_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

799 
qed 
31992  800 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

801 
lemma INFI_fold_inf: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

802 
assumes "finite A" 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

803 
shows "INFI A f = fold (inf \<circ> f) top A" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

804 
using assms inf_INFI_fold_inf [of A top] by simp 
31992  805 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

806 
lemma SUPR_fold_sup: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

807 
assumes "finite A" 
42873
da1253ff1764
pointfree characterization of operations on finite sets
haftmann
parents:
42871
diff
changeset

808 
shows "SUPR A f = fold (sup \<circ> f) bot A" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

809 
using assms sup_SUPR_fold_sup [of A bot] by simp 
31992  810 

811 
end 

812 

813 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

815 

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

816 
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" 
42875  817 
where "fold_image f g = fold (\<lambda>x y. f (g x) y)" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

818 

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

819 
lemma fold_image_empty[simp]: "fold_image f g z {} = z" 
42875  820 
by (simp add:fold_image_def) 
15392  821 

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

822 
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

823 
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

824 

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

825 
lemma fold_image_insert[simp]: 
42875  826 
assumes "finite A" and "a \<notin> A" 
827 
shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" 

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

828 
proof  
42875  829 
interpret comp_fun_commute "%x y. (g x) * y" proof 
42809
5b45125b15ba
use pointfree characterisation for fold_set locale
haftmann
parents:
42715
diff
changeset

830 
qed (simp add: fun_eq_iff mult_ac) 
5b45125b15ba
use pointfree characterisation for fold_set locale
haftmann
parents:
42715
diff
changeset

831 
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

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

833 

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

834 
lemma fold_image_reindex: 
42875  835 
assumes "finite A" 
836 
shows "inj_on h A \<Longrightarrow> fold_image times g z (h ` A) = fold_image times (g \<circ> h) z A" 

837 
using assms by induct auto 

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

838 

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

839 
lemma fold_image_cong: 
42875  840 
assumes "finite A" and g_h: "\<And>x. x\<in>A \<Longrightarrow> g x = h x" 
841 
shows "fold_image times g z A = fold_image times h z A" 

842 
proof  

843 
from `finite A` 

844 
have "\<And>C. C <= A > (ALL x:C. g x = h x) > fold_image times g z C = fold_image times h z C" 

845 
proof (induct arbitrary: C) 

846 
case empty then show ?case by simp 

847 
next 

848 
case (insert x F) then show ?case apply  

849 
apply (simp add: subset_insert_iff, clarify) 

850 
apply (subgoal_tac "finite C") 

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

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

853 
prefer 2 apply blast 

854 
apply (erule ssubst) 

855 
apply (simp add: Ball_def del: insert_Diff_single) 

856 
done 

857 
qed 

858 
with g_h show ?thesis by simp 

859 
qed 

15392  860 

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

861 
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

862 

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

863 
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

864 
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

865 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

866 
lemma fold_image_1: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

867 
"finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" 
41656  868 
apply (induct rule: finite_induct) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

869 
apply simp by auto 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

870 

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

871 
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

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

873 
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

874 
fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)" 
41656  875 
apply (induct rule: finite_induct) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

878 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

879 
lemma fold_image_Un_one: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

880 
assumes fS: "finite S" and fT: "finite T" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

881 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

882 
shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

883 
proof 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

884 
have "fold_image op * f 1 (S \<inter> T) = 1" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

885 
apply (rule fold_image_1) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

886 
using fS fT I0 by auto 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

887 
with fold_image_Un_Int[OF fS fT] show ?thesis by simp 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

888 
qed 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

889 

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

890 
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

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

892 
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

893 
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

894 
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

895 

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

896 
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

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

898 
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

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

900 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
41656  901 
apply (induct rule: finite_induct) 
902 
apply simp 

903 
apply atomize 

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

904 
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

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

906 
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

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

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

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

910 

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

911 
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

912 
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

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

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

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

918 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  919 
apply blast 
15506  920 
apply simp 
15392  921 
done 
922 

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

923 
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

924 
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

925 
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

926 
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

927 

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

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

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

930 
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

931 
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

932 
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

933 
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

934 

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

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

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

937 
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

938 
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

939 
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

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

941 
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

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

943 
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

944 
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

945 
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

946 
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

947 
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

948 
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

949 
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

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

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

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

953 

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

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

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

956 
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

957 
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

958 
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

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

960 
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

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

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

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

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

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

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

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

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

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

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

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

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

973 

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

974 
end 
22917  975 

25162  976 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

977 
subsection {* A fold functional for nonempty sets *} 
15392  978 

979 
text{* Does not require start value. *} 

12396  980 

23736  981 
inductive 
22262  982 
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" 
983 
for f :: "'a => 'a => 'a" 

984 
where 

15506  985 
fold1Set_insertI [intro]: 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

986 
"\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x" 
12396  987 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35267
diff
changeset

988 
definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where 
22262  989 
"fold1 f A == THE x. fold1Set f A x" 
15506  990 

991 
lemma fold1Set_nonempty: 

22917  992 
"fold1Set f A x \<Longrightarrow> A \<noteq> {}" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

993 
by(erule fold1Set.cases, simp_all) 
15392  994 

23736  995 
inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x" 
996 

997 
inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x" 

22262  998 

999 

1000 
lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)" 

35216  1001 
by (blast elim: fold_graph.cases) 
15392  1002 

22917  1003 
lemma fold1_singleton [simp]: "fold1 f {a} = a" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1004 
by (unfold fold1_def) blast 
12396  1005 

15508  1006 
lemma finite_nonempty_imp_fold1Set: 
22262  1007 
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x" 
15508  1008 
apply (induct A rule: finite_induct) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1009 
apply (auto dest: finite_imp_fold_graph [of _ f]) 
15508  1010 
done 
15506  1011 

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

1012 
text{*First, some lemmas about @{const fold_graph}.*} 
15392  1013 

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

1014 
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

1015 
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

1016 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1017 
lemma comp_fun_commute: "comp_fun_commute (op *)" proof 
42809
5b45125b15ba
use pointfree characterisation for fold_set locale
haftmann
parents:
42715
diff
changeset

1018 
qed (simp add: fun_eq_iff mult_ac) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1019 

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

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

1021 
assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1022 
shows "fold_graph times z (insert b A) (z * y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1023 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1024 
interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1026 
proof (induct rule: fold_graph.induct) 
36045  1027 
case emptyI show ?case by (subst mult_commute [of z b], fast) 
15508  1028 
next 
22262  1029 
case (insertI x A y) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1030 
have "fold_graph times z (insert x (insert b A)) (x * (z * y))" 
15521  1031 
using insertI by force {*how does @{term id} get unfolded?*} 
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

1032 
thus ?case by (simp add: insert_commute mult_ac) 
15508  1033 
qed 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1035 

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

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

1037 
assumes fold: "fold_graph times b A x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1038 
shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A{a})) x" 
15508  1039 
using fold 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1040 
proof (induct rule: fold_graph.induct) 
15508  1041 
case emptyI thus ?case by simp 
1042 
next 

22262  1043 
case (insertI x A y) 
15521  1044 
have "a = x \<or> a \<in> A" using insertI by simp 
1045 
thus ?case 

1046 
proof 

1047 
assume "a = x" 

1048 
with insertI show ?thesis 

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

1049 
by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap) 
15521  1050 
next 
1051 
assume ainA: "a \<in> A" 

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

1052 
hence "fold_graph times a (insert x (insert b (A  {a}))) (x * y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1053 
using insertI by force 
15521  1054 
moreover 
1055 
have "insert x (insert b (A  {a})) = insert b (insert x A  {a})" 

1056 
using ainA insertI by blast 

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

1057 
ultimately show ?thesis by simp 
15508  1058 
qed 
1059 
qed 

1060 

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

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

1062 
assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1063 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1064 
interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1066 
apply (simp add: fold1_def fold_def) 
15508  1067 
apply (rule the_equality) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1068 
apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times]) 
15508  1069 
apply (rule sym, clarify) 
1070 
apply (case_tac "Aa=A") 

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

1072 
apply (subgoal_tac "fold_graph times a A x") 
35216  1073 
apply (best intro: fold_graph_determ) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1074 
apply (subgoal_tac "insert aa (Aa  {a}) = A") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1076 
apply (auto dest: fold_graph_permute_diff [where a=a]) 
15508  1077 
done 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1078 
qed 
15508  1079 

15521  1080 
lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)" 
1081 
apply safe 

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

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

1083 
apply (drule_tac x=x in spec) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1084 
apply (drule_tac x="A{x}" in spec, auto) 
15508  1085 
done 
1086 

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

1087 
lemma fold1_insert: 
15521  1088 
assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1089 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1090 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1091 
interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule comp_fun_commute) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1092 
from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
15521  1093 
by (auto simp add: nonempty_iff) 
1094 
with A show ?thesis 

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

1095 
by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
15521  1096 
qed 
1097 

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

1098 
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

1099 

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

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

1101 
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

1102 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1103 
lemma comp_fun_idem: "comp_fun_idem (op *)" proof 
42869
43b0f61f56d0
use pointfree characterization for locale fun_left_comm_idem
haftmann
parents:
42809
diff
changeset

1104 
qed (simp_all add: fun_eq_iff mult_left_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

1105 

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

1106 
lemma fold1_insert_idem [simp]: 
15521  1107 
assumes nonempty: "A \<noteq> {}" and A: "finite A" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1108 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1109 
proof  
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1110 
interpret comp_fun_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

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

1112 
from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
15521  1113 
by (auto simp add: nonempty_iff) 
1114 
show ?thesis 

1115 
proof cases 

41550  1116 
assume a: "a = x" 
1117 
show ?thesis 

15521  1118 
proof cases 
1119 
assume "A' = {}" 

41550  1120 
with A' a show ?thesis by simp 
15521  1121 
next 
1122 
assume "A' \<noteq> {}" 

41550  1123 
with A A' a show ?thesis 
35216  1124 
by (simp add: fold1_insert mult_assoc [symmetric]) 
15521  1125 
qed 
1126 
next 

1127 
assume "a \<noteq> x" 

41550  1128 
with A A' show ?thesis 
35216  1129 
by (simp add: insert_commute fold1_eq_fold) 
15521  1130 
qed 
1131 
qed 

15506  1132 

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

1133 
lemma hom_fold1_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

1134 
assumes hom: "!!x y. h (x * y) = h 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

1135 
and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)" 
22917  1136 
using N proof (induct rule: finite_ne_induct) 
1137 
case singleton thus ?case by simp 

1138 
next 

1139 
case (insert n N) 

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

1140 
then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1141 
also have "\<dots> = h n * h (fold1 times N)" by(rule hom) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1142 
also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1143 
also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))" 
22917  1144 
using insert by(simp) 
1145 
also have "insert (h n) (h ` N) = h ` insert n N" by simp 

1146 
finally show ?case . 

1147 
qed 

1148 

32679  1149 
lemma fold1_eq_fold_idem: 
1150 
assumes "finite A" 

1151 
shows "fold1 times (insert a A) = fold times a A" 

1152 
proof (cases "a \<in> A") 

1153 
case False 

1154 
with assms show ?thesis by (simp add: fold1_eq_fold) 

1155 
next 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1156 
interpret comp_fun_idem times by (fact comp_fun_idem) 
32679  1157 
case True then obtain b B 
1158 
where A: "A = insert a B" and "a \<notin> B" by (rule set_insert) 

1159 
with assms have "finite B" by auto 

1160 
then have "fold times a (insert a B) = fold times (a * a) B" 

1161 
using `a \<notin> B` by (rule fold_insert2) 

1162 
then show ?thesis 

1163 
using `a \<notin> B` `finite B` by (simp add: fold1_eq_fold A) 

1164 
qed 

1165 

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

1166 
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

1167 

15506  1168 

15508  1169 
text{* Now the recursion rules for definitions: *} 
1170 

22917  1171 
lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a" 
35216  1172 
by simp 
15508  1173 

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

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

1175 
"\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g 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

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

1177 

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

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

1179 
"\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g 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

1180 
by simp 
15508  1181 

1182 
subsubsection{* Determinacy for @{term fold1Set} *} 

1183 

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

1184 
(*Not actually used!!*) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

1186 
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

1187 
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

1188 

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

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

1190 
"[fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A] 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1191 
==> fold_graph times id a (insert b A) x" 
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

1192 
apply (cases "a=b") 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1193 
apply (auto dest: fold_graph_permute_diff) 
15506  1194 
done 
15376  1195 

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

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

1197 
"fold1Set times A x ==> fold1Set times A y ==> y = x" 
15506  1198 
proof (clarify elim!: fold1Set.cases) 
1199 
fix A x B y a b 

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

1200 
assume Ax: "fold_graph times id a A x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1201 
assume By: "fold_graph times id b B y" 
15506  1202 
assume anotA: "a \<notin> A" 
1203 
assume bnotB: "b \<notin> B" 

1204 
assume eq: "insert a A = insert b B" 

1205 
show "y=x" 

1206 
proof cases 

1207 
assume same: "a=b" 

1208 
hence "A=B" using anotA bnotB eq by (blast elim!: equalityE) 

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

1209 
thus ?thesis using Ax By same by (blast intro: fold_graph_determ) 
15392  1210 
next 
15506  1211 
assume diff: "a\<noteq>b" 
1212 
let ?D = "B  {a}" 

1213 
have B: "B = insert a ?D" and A: "A = insert b ?D" 

1214 
and aB: "a \<in> B" and bA: "b \<in> A" 

1215 
using eq anotA bnotB diff by (blast elim!:equalityE)+ 

1216 
with aB bnotB By 

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

1217 
have "fold_graph times id a (insert b ?D) y" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1218 
by (auto intro: fold_graph_permute simp add: insert_absorb) 
15506  1219 
moreover 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1220 
have "fold_graph times id a (insert b ?D) x" 
15506  1221 
by (simp add: A [symmetric] Ax) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1222 
ultimately show ?thesis by (blast intro: fold_graph_determ) 
15392  1223 
qed 
12396  1224 
qed 
1225 

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

1226 
lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y" 
15506  1227 
by (unfold fold1_def) (blast intro: fold1Set_determ) 
1228 

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

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

1230 
*) 
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

1231 

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

1233 
empty_fold_graphE [rule del] fold_graph.intros [rule del] 
15506  1234 
empty_fold1SetE [rule del] insert_fold1SetE [rule del] 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19870
diff
changeset

1235 
 {* No more proofs involve these relations. *} 
15376  1236 

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

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

1238 

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

1239 
context ab_semigroup_mult 
22917  1240 
begin 
1241 

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

1242 
lemma fold1_Un: 
15484  1243 
assumes A: "finite A" "A \<noteq> {}" 
1244 
shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow> 

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

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

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

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

1248 

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

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

1250 
assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,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

1251 
shows "fold1 times A \<in> A" 
15484  1252 
using A 
1253 
proof (induct rule:finite_ne_induct) 

15506  1254 
case singleton thus ?case by simp 
15484  1255 
next 
1256 
case insert thus ?case using elem by (force simp add:fold1_insert) 

1257 
qed 

1258 

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

1259 
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

1260 

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

1261 
lemma (in ab_semigroup_idem_mult) fold1_Un2: 
15497
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

1262 
assumes A: "finite A" "A \<noteq> {}" 
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

1263 
shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1264 
fold1 times (A Un B) = fold1 times A * fold1 times B" 
15497
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

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

1266 
proof(induct rule:finite_ne_induct) 
15497
53bca254719a
Added semilattice locales and reorganized fold1 lemmas
nipkow
parents:
15487
diff
changeset

1267 
case singleton thus ?case by simp 
15484  1268 
next 
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

1269 
case insert thus ?case by (simp add: mult_assoc) 
18423  1270 
qed 
1271 

1272 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

1273 
subsection {* Locales as minipackages for fold operations *} 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33960
diff
changeset

1274 

35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

1275 
subsubsection {* The natural case *} 
35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

1276 

99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

1277 
locale folding = 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

1278 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

1279 
fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b" 
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42869
diff
changeset

1280 
assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y" 
35722 