author  wenzelm 
Wed, 01 Aug 2012 15:32:36 +0200  
changeset 48632  c028cf680a3e 
parent 48619  558e4e77ce69 
child 48891  c0eafbd55de3 
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 
48109
0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

10 
uses ("Tools/set_comprehension_pointfree.ML") 
15131  11 
begin 
12396  12 

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

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

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

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

48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

20 
(* FIXME: move to Set theory *) 
48109
0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

21 
use "Tools/set_comprehension_pointfree.ML" 
0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

22 

0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

23 
simproc_setup finite_Collect ("finite (Collect P)") = 
48124  24 
{* K Set_Comprehension_Pointfree.simproc *} 
48109
0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

25 

48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

26 
(* FIXME: move to Set theory*) 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

27 
setup {* 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

28 
Code_Preproc.map_pre (fn ss => ss addsimprocs 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

29 
[Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}], 
48128  30 
proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}]) 
48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

31 
*} 
48109
0a58f7eefba2
Integrated set comprehension pointfree simproc.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48063
diff
changeset

32 

41656  33 
lemma finite_induct [case_names empty insert, induct set: finite]: 
34 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 

35 
assumes "finite F" 

36 
assumes "P {}" 

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

38 
shows "P F" 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

39 
using `finite F` 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

40 
proof induct 
41656  41 
show "P {}" by fact 
42 
fix x F assume F: "finite F" and P: "P F" 

43 
show "P (insert x F)" 

44 
proof cases 

45 
assume "x \<in> F" 

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

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

48 
next 

49 
assume "x \<notin> F" 

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

51 
qed 

52 
qed 

53 

54 

55 
subsubsection {* Choice principles *} 

12396  56 

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

60 
proof  

28823  61 
from assms have "A \<noteq> UNIV" by blast 
41656  62 
then show ?thesis by blast 
12396  63 
qed 
64 

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

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

70 
case empty then show ?case by simp 

29923  71 
next 
72 
case (insert a A) 

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

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

75 
proof 

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

77 
qed 

78 
qed 

79 

23878  80 

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

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

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

86 
using assms 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

87 
proof induct 
15392  88 
case empty 
41656  89 
show ?case 
90 
proof 

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

15510  92 
qed 
15392  93 
next 
94 
case (insert a A) 

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

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

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

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

15392  101 
thus ?case by blast 
102 
qed 

103 

104 
lemma nat_seg_image_imp_finite: 

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

15392  107 
case 0 thus ?case by simp 
108 
next 

109 
case (Suc n) 

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

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

112 
show ?case 

113 
proof cases 

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

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

116 
thus ?thesis using finB by simp 

117 
next 

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

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

120 
thus ?thesis using finB by simp 

121 
qed 

122 
qed 

123 

124 
lemma finite_conv_nat_seg_image: 

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

15392  127 

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

32988  131 
proof  
132 
from finite_imp_nat_seg_image_inj_on[OF `finite A`] 

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

134 
by (auto simp:bij_betw_def) 

33057  135 
let ?f = "the_inv_into {i. i<n} f" 
32988  136 
have "inj_on ?f A & ?f ` A = {i. i<n}" 
33057  137 
by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij]) 
32988  138 
thus ?thesis by blast 
139 
qed 

140 

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44835
diff
changeset

143 
by (fastforce simp: finite_conv_nat_seg_image) 
29920  144 

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

147 
by (simp add: le_eq_less_or_eq Collect_disj_eq) 

15392  148 

41656  149 

150 
subsubsection {* Finiteness and common set operations *} 

12396  151 

41656  152 
lemma rev_finite_subset: 
153 
"finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A" 

154 
proof (induct arbitrary: A rule: finite_induct) 

155 
case empty 

156 
then show ?case by simp 

157 
next 

158 
case (insert x F A) 

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

160 
show "finite A" 

161 
proof cases 

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

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

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

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

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

167 
finally show ?thesis . 

12396  168 
next 
41656  169 
show "A \<subseteq> F ==> ?thesis" by fact 
170 
assume "x \<notin> A" 

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

12396  172 
qed 
173 
qed 

174 

41656  175 
lemma finite_subset: 
176 
"A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A" 

177 
by (rule rev_finite_subset) 

29901  178 

41656  179 
lemma finite_UnI: 
180 
assumes "finite F" and "finite G" 

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

182 
using assms by induct simp_all 

31992  183 

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

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

31992  187 

41656  188 
lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A" 
12396  189 
proof  
41656  190 
have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp 
191 
then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un) 

23389  192 
then show ?thesis by simp 
12396  193 
qed 
194 

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

197 
by (blast intro: finite_subset) 

198 

199 
lemma finite_Collect_conjI [simp, intro]: 

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

201 
by (simp add: Collect_conj_eq) 

202 

203 
lemma finite_Collect_disjI [simp]: 

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

205 
by (simp add: Collect_disj_eq) 

206 

207 
lemma finite_Diff [simp, intro]: 

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

209 
by (rule finite_subset, rule Diff_subset) 

29901  210 

211 
lemma finite_Diff2 [simp]: 

41656  212 
assumes "finite B" 
213 
shows "finite (A  B) \<longleftrightarrow> finite A" 

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

29901  217 
finally show ?thesis .. 
218 
qed 

219 

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

222 
proof  

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

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

225 
ultimately show ?thesis by simp 

226 
qed 

227 

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

12396  231 

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

235 

236 
lemma finite_Union [simp, intro]: 

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

238 
by (induct rule: finite_induct) simp_all 

239 

240 
lemma finite_UN_I [intro]: 

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

242 
by (induct rule: finite_induct) simp_all 

29903  243 

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

246 
by (blast intro: finite_subset) 

247 

248 
lemma finite_Inter [intro]: 

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

250 
by (blast intro: Inter_lower finite_subset) 

12396  251 

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

254 
by (blast intro: INT_lower finite_subset) 

13825  255 

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

258 
by (induct rule: finite_induct) simp_all 

13825  259 

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

262 
by (simp add: image_Collect [symmetric]) 

263 

41656  264 
lemma finite_imageD: 
42206  265 
assumes "finite (f ` A)" and "inj_on f A" 
266 
shows "finite A" 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

267 
using assms 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

268 
proof (induct "f ` A" arbitrary: A) 
42206  269 
case empty then show ?case by simp 
270 
next 

271 
case (insert x B) 

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

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

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

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

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

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

278 
then show "finite A" by simp 

279 
qed 

12396  280 

41656  281 
lemma finite_surj: 
282 
"finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B" 

283 
by (erule finite_subset) (rule finite_imageI) 

12396  284 

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

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

13825  288 

41656  289 
lemma finite_subset_image: 
290 
assumes "finite B" 

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

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

292 
using assms 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

293 
proof induct 
41656  294 
case empty then show ?case by simp 
295 
next 

296 
case insert then show ?case 

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

298 
blast 

299 
qed 

300 

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

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

305 
apply (subst vimage_insert) 
43991  306 
apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2) 
13825  307 
done 
308 

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

311 
using finite_vimage_IntI[of F h UNIV] by auto 

312 

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

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

314 
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

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

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

317 
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

318 
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

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

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

321 

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

322 
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

323 
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

324 

41656  325 
lemma finite_Collect_bex [simp]: 
326 
assumes "finite A" 

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

328 
proof  

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

330 
with assms show ?thesis by simp 

331 
qed 

12396  332 

41656  333 
lemma finite_Collect_bounded_ex [simp]: 
334 
assumes "finite {y. P y}" 

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

336 
proof  

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

338 
with assms show ?thesis by simp 

339 
qed 

29920  340 

41656  341 
lemma finite_Plus: 
342 
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)" 

343 
by (simp add: Plus_def) 

17022  344 

31080  345 
lemma finite_PlusD: 
346 
fixes A :: "'a set" and B :: "'b set" 

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

348 
shows "finite A" "finite B" 

349 
proof  

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

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

31080  353 
next 
354 
have "Inr ` B \<subseteq> A <+> B" by auto 

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

31080  357 
qed 
358 

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

361 
by (auto intro: finite_PlusD finite_Plus) 

31080  362 

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

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

12396  366 

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

367 
lemma finite_SigmaI [simp, intro]: 
41656  368 
"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

369 
by (unfold Sigma_def) blast 
12396  370 

41656  371 
lemma finite_cartesian_product: 
372 
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)" 

15402  373 
by (rule finite_SigmaI) 
374 

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

12396  378 

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

379 
lemma finite_cartesian_productD1: 
42207  380 
assumes "finite (A \<times> B)" and "B \<noteq> {}" 
381 
shows "finite A" 

382 
proof  

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

384 
by (auto simp add: finite_conv_nat_seg_image) 

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

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

387 
by (simp add: image_compose) 

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

389 
then show ?thesis 

390 
by (auto simp add: finite_conv_nat_seg_image) 

391 
qed 

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

392 

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

393 
lemma finite_cartesian_productD2: 
42207  394 
assumes "finite (A \<times> B)" and "A \<noteq> {}" 
395 
shows "finite B" 

396 
proof  

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

398 
by (auto simp add: finite_conv_nat_seg_image) 

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

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

401 
by (simp add: image_compose) 

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

403 
then show ?thesis 

404 
by (auto simp add: finite_conv_nat_seg_image) 

405 
qed 

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

406 

48175
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

407 
lemma finite_prod: 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

408 
"finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)" 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

409 
by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

410 
dest: finite_cartesian_productD1 finite_cartesian_productD2) 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

411 

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

12396  414 
proof 
415 
assume "finite (Pow A)" 

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

12396  418 
next 
419 
assume "finite A" 

41656  420 
then show "finite (Pow A)" 
35216  421 
by induct (simp_all add: Pow_insert) 
12396  422 
qed 
423 

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

426 
by (simp add: Pow_def [symmetric]) 

29918  427 

48175
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

428 
lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)" 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

429 
by(simp only: finite_Pow_iff Pow_UNIV[symmetric]) 
fea68365c975
add finiteness lemmas for 'a * 'b and 'a set
Andreas Lochbihler
parents:
48128
diff
changeset

430 

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

434 

41656  435 
subsubsection {* Further induction rules on finite sets *} 
436 

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

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

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

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

441 
shows "P F" 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

442 
using assms 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

443 
proof induct 
41656  444 
case empty then show ?case by simp 
445 
next 

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

447 
qed 

448 

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

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

451 
assumes empty: "P {}" 

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

453 
shows "P F" 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

454 
using `finite F` `F \<subseteq> A` 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

455 
proof induct 
41656  456 
show "P {}" by fact 
31441  457 
next 
41656  458 
fix x F 
459 
assume "finite F" and "x \<notin> F" and 

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

461 
show "P (insert x F)" 

462 
proof (rule insert) 

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

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

465 
with P show "P F" . 

466 
show "finite F" by fact 

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

468 
qed 

469 
qed 

470 

471 
lemma finite_empty_induct: 

472 
assumes "finite A" 

473 
assumes "P A" 

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

475 
shows "P {}" 

476 
proof  

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

478 
proof  

479 
fix B :: "'a set" 

480 
assume "B \<subseteq> A" 

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

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

483 
proof induct 

484 
case empty 

485 
from `P A` show ?case by simp 

486 
next 

487 
case (insert b B) 

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

489 
proof (rule remove) 

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

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

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

493 
qed 

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

495 
finally show ?case . 

496 
qed 

497 
qed 

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

499 
then show ?thesis by simp 

31441  500 
qed 
501 

502 

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

504 

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

506 
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" 
27430  507 
begin 
508 

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

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

511 

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

512 
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

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

514 

27430  515 
end 
516 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

517 
instance prod :: (finite, finite) finite 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

518 
by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 
26146  519 

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

520 
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

521 
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

522 

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

525 
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

526 
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

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

530 
by (simp only: finite_Pow_iff finite) 

531 
ultimately show "finite (range ?graph)" 

532 
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

533 
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

534 
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

535 
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

536 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

537 
instance bool :: finite 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

538 
by default (simp add: UNIV_bool) 
44831  539 

45962  540 
instance set :: (finite) finite 
541 
by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) 

542 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

543 
instance unit :: finite 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

544 
by default (simp add: UNIV_unit) 
44831  545 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

546 
instance sum :: (finite, finite) finite 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

547 
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 
27981  548 

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

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

552 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

553 
instance option :: (finite) finite 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

554 
by default (simp add: UNIV_option_conv) 
44831  555 

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

556 

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

557 
subsection {* A basic fold functional for finite sets *} 
15392  558 

559 
text {* The intended behaviour is 

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

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

561 
if @{text f} is ``leftcommutative'': 
15392  562 
*} 
563 

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

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

565 
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

566 
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

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

568 

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

569 
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

570 
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

571 

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

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

573 

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

574 
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

575 
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

576 
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

577 
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

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

579 

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

580 
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

581 

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

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

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

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

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

589 
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

590 

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

591 
lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x" 
41656  592 
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

593 

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

594 

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

595 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  596 

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

597 
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

598 
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

599 

36045  600 
lemma fold_graph_insertE_aux: 
601 
"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'" 

602 
proof (induct set: fold_graph) 

603 
case (insertI x A y) show ?case 

604 
proof (cases "x = a") 

605 
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

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

609 
using insertI by auto 

42875  610 
have "f x y = f a (f x y')" 
36045  611 
unfolding y by (rule fun_left_comm) 
42875  612 
moreover have "fold_graph f z (insert x A  {a}) (f x y')" 
36045  613 
using y' and `x \<noteq> a` and `x \<notin> A` 
614 
by (simp add: insert_Diff_if fold_graph.insertI) 

42875  615 
ultimately show ?case by fast 
15392  616 
qed 
36045  617 
qed simp 
618 

619 
lemma fold_graph_insertE: 

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

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

622 
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

623 

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

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

625 
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 
36045  626 
proof (induct arbitrary: y set: fold_graph) 
627 
case (insertI x A y v) 

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

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

630 
by (rule fold_graph_insertE) 

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

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

633 
qed fast 

15392  634 

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

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

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

637 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  638 

42272  639 
lemma fold_graph_fold: 
640 
assumes "finite A" 

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

642 
proof  

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

644 
moreover note fold_graph_determ 

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

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

647 
then show ?thesis by (unfold fold_def) 

648 
qed 

36045  649 

15392  650 
text{* The base case for @{text fold}: *} 
651 

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

652 
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

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

654 

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

655 
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

656 

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

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

660 
proof (rule fold_equality) 

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

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

663 
qed 

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

664 

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

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

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

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

668 
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

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

670 
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

671 
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

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

673 

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

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

675 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
35216  676 
by (simp add: fold_fun_comm) 
15392  677 

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

678 
lemma fold_rec: 
42875  679 
assumes "finite A" and "x \<in> A" 
680 
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

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

682 
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

683 
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

684 
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

685 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  686 
finally show ?thesis . 
687 
qed 

688 

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

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

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

691 
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

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

693 
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

694 
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

695 
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

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

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

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

699 

48619  700 
text{* Other properties of @{const fold}: *} 
701 

702 
lemma fold_image: 

703 
assumes "finite A" and "inj_on g A" 

704 
shows "fold f x (g ` A) = fold (f \<circ> g) x A" 

705 
using assms 

706 
proof induction 

707 
case (insert a F) 

708 
interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute) 

709 
from insert show ?case by auto 

710 
qed (simp) 

711 

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

712 
end 
15392  713 

15480  714 
text{* A simplified version for idempotent functions: *} 
715 

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

716 
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

717 
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

718 
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

719 

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

720 
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

721 
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

722 

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

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

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

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

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

728 
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

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

731 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  732 
qed 
733 

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

734 
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

735 

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

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

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

738 
by(simp add:fold_fun_comm) 
15484  739 

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

740 
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

741 

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

742 

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

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

744 

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

745 
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

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

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

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

749 

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

750 
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

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

752 
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

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

754 

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

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

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

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

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

759 

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

760 
lemma comp_fun_idem_remove: 
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

761 
"comp_fun_idem Set.remove" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

763 
qed auto 
31992  764 

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

765 
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

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

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

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

769 

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

770 
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

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

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

773 
qed (auto simp add: sup_left_commute) 
31992  774 

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

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

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

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

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

779 
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

780 
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

781 
qed 
31992  782 

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

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

784 
assumes "finite A" 
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

785 
shows "B  A = fold Set.remove B A" 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

786 
proof  
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

787 
interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove) 
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

788 
from `finite A` have "fold Set.remove B A = B  A" by (induct A arbitrary: B) auto 
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

789 
then show ?thesis .. 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

791 

48619  792 
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" 
793 
where "filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A" 

794 

795 
lemma comp_fun_commute_filter_fold: "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')" 

796 
proof  

797 
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) 

798 
show ?thesis by default (auto simp: fun_eq_iff) 

799 
qed 

800 

801 
lemma inter_filter: 

802 
assumes "finite B" 

803 
shows "A \<inter> B = filter (\<lambda>x. x \<in> A) B" 

804 
using assms 

805 
by (induct B) (auto simp: filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold]) 

806 

807 
lemma project_filter: 

808 
assumes "finite A" 

809 
shows "Set.project P A = filter P A" 

810 
using assms 

811 
by (induct A) 

812 
(auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold]) 

813 

814 
lemma image_fold_insert: 

815 
assumes "finite A" 

816 
shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A" 

817 
using assms 

818 
proof  

819 
interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto 

820 
show ?thesis using assms by (induct A) auto 

821 
qed 

822 

823 
lemma Ball_fold: 

824 
assumes "finite A" 

825 
shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A" 

826 
using assms 

827 
proof  

828 
interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto 

829 
show ?thesis using assms by (induct A) auto 

830 
qed 

831 

832 
lemma Bex_fold: 

833 
assumes "finite A" 

834 
shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A" 

835 
using assms 

836 
proof  

837 
interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto 

838 
show ?thesis using assms by (induct A) auto 

839 
qed 

840 

841 
lemma comp_fun_commute_Pow_fold: 

842 
"comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)" 

843 
by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast 

844 

845 
lemma Pow_fold: 

846 
assumes "finite A" 

847 
shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A" 

848 
using assms 

849 
proof  

850 
interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A" by (rule comp_fun_commute_Pow_fold) 

851 
show ?thesis using assms by (induct A) (auto simp: Pow_insert) 

852 
qed 

853 

854 
lemma fold_union_pair: 

855 
assumes "finite B" 

856 
shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B" 

857 
proof  

858 
interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto 

859 
show ?thesis using assms by (induct B arbitrary: A) simp_all 

860 
qed 

861 

862 
lemma comp_fun_commute_product_fold: 

863 
assumes "finite B" 

864 
shows "comp_fun_commute (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B)" 

865 
by default (auto simp: fold_union_pair[symmetric] assms) 

866 

867 
lemma product_fold: 

868 
assumes "finite A" 

869 
assumes "finite B" 

870 
shows "A \<times> B = fold (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B) {} A" 

871 
using assms unfolding Sigma_def 

872 
by (induct A) 

873 
(simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair) 

874 

875 

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

876 
context complete_lattice 
31992  877 
begin 
878 

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

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

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

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

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

883 
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

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

886 
qed 
31992  887 

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

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

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

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

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

892 
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

893 
from `finite A` show ?thesis by (induct A arbitrary: B) 
44919  894 
(simp_all add: sup_commute fold_fun_comm) 
31992  895 
qed 
896 

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

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

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

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

900 
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

901 

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

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

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

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

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

46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

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

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

909 
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

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

911 
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

912 
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

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

914 
by (induct A arbitrary: B) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44919
diff
changeset

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

916 
qed 
31992  917 

46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

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

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

920 
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

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

922 
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

923 
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

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

925 
by (induct A arbitrary: B) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44919
diff
changeset

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

927 
qed 
31992  928 

46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

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

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

931 
shows "INFI A f = fold (inf \<circ> f) top A" 
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

932 
using assms inf_INF_fold_inf [of A top] by simp 
31992  933 

46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

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

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

936 
shows "SUPR A f = fold (sup \<circ> f) bot A" 
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46033
diff
changeset

937 
using assms sup_SUP_fold_sup [of A bot] by simp 
31992  938 

939 
end 

940 

941 

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

942 
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

943 

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

944 
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" 
42875  945 
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

946 

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

947 
lemma fold_image_empty[simp]: "fold_image f g z {} = z" 
42875  948 
by (simp add:fold_image_def) 
15392  949 

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

950 
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

951 
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

952 

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

953 
lemma fold_image_insert[simp]: 
42875  954 
assumes "finite A" and "a \<notin> A" 
955 
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

956 
proof  
46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

957 
interpret comp_fun_commute "%x y. (g x) * y" 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

958 
by default (simp add: fun_eq_iff mult_ac) 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

959 
from assms show ?thesis 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

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

961 

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

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

965 
using assms by induct auto 

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

966 

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

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

970 
proof  

971 
from `finite A` 

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

973 
proof (induct arbitrary: C) 

974 
case empty then show ?case by simp 

975 
next 

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

977 
apply (simp add: subset_insert_iff, clarify) 

978 
apply (subgoal_tac "finite C") 

48125
602dc0215954
tuned proofs  prefer direct "rotated" instead of oldstyle COMP;
wenzelm
parents:
48124
diff
changeset

979 
prefer 2 apply (blast dest: finite_subset [rotated]) 
42875  980 
apply (subgoal_tac "C = insert x (C  {x})") 
981 
prefer 2 apply blast 

982 
apply (erule ssubst) 

983 
apply (simp add: Ball_def del: insert_Diff_single) 

984 
done 

985 
qed 

986 
with g_h show ?thesis by simp 

987 
qed 

15392  988 

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

989 
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

990 

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

991 
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

992 
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

993 

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

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

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

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

998 

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

999 
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

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

1001 
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

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

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

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

1006 

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

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

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

1009 
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

1010 
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

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

1012 
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

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

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

1015 
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

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

1017 

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

1018 
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

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

1020 
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

1021 
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

1022 
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

1023 

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

1024 
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

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

1026 
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

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

1028 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
41656  1029 
apply (induct rule: finite_induct) 
1030 
apply simp 

1031 
apply atomize 

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

1032 
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

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

1034 
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

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

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

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

1038 

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

1039 
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

1040 
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

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

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

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

1046 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  1047 
apply blast 
15506  1048 
apply simp 
15392  1049 
done 
1050 

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

1051 
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

1052 
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

1053 
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

1054 
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

1055 

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

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

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

1058 
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

1059 
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

1060 
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

1061 
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

1062 

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

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

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

1065 
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

1066 
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

1067 
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

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

1069 
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

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

1071 
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

1072 
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

1073 
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

1074 
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

1075 
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

1076 
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

1077 
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

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

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

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

1081 

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

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

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

1084 
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

1085 
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

1086 
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

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

1088 
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

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

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

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

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

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

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

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

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

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

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

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

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

1101 

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

1102 
end 
22917  1103 

25162  1104 

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

1105 
subsection {* A fold functional for nonempty sets *} 
15392  1106 

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

12396  1108 

23736  1109 
inductive 
22262  1110 
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" 
1111 
for f :: "'a => 'a => 'a" 

1112 
where 

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

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

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

1116 
definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where 
22262  1117 
"fold1 f A == THE x. fold1Set f A x" 
15506  1118 

1119 
lemma fold1Set_nonempty: 

22917  1120 
"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

1121 
by(erule fold1Set.cases, simp_all) 
15392  1122 

23736  1123 
inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x" 
1124 

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

22262  1126 

1127 

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

35216  1129 
by (blast elim: fold_graph.cases) 
15392  1130 

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

1132 
by (unfold fold1_def) blast 
12396  1133 

15508  1134 
lemma finite_nonempty_imp_fold1Set: 
22262  1135 
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x" 
15508  1136 
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

1137 
apply (auto dest: finite_imp_fold_graph [of _ f]) 
15508  1138 
done 
15506  1139 

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

1140 
text{*First, some lemmas about @{const fold_graph}.*} 
15392  1141 

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

1142 
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

1143 
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

1144 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

1145 
lemma comp_fun_commute: "comp_fun_commute (op *)" 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

1146 
by default (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

1147 

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

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

1149 
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

1150 
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

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

1152 
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

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

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

1158 
have "fold_graph times z (insert x (insert b A)) (x * (z * y))" 
15521  1159 
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

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

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

1163 

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

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

1165 
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

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

1168 
proof (induct rule: fold_graph.induct) 
15508  1169 
case emptyI thus ?case by simp 
1170 
next 

22262  1171 
case (insertI x A y) 
15521  1172 
have "a = x \<or> a \<in> A" using insertI by simp 
1173 
thus ?case 

1174 
proof 

1175 
assume "a = x" 

1176 
with insertI show ?thesis 

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

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

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

1180 
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

1181 
using insertI by force 
15521  1182 
moreover 
1183 
have "insert x (insert b (A  {a})) = insert b (insert x A  {a})" 

1184 
using ainA insertI by blast 

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

1185 
ultimately show ?thesis by simp 
15508  1186 
qed 
1187 
qed 

1188 

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

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

1190 
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

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

1192 
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

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

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

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

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

1200 
apply (subgoal_tac "fold_graph times a A x") 
35216  1201 
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

1202 
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

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

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

1206 
qed 
15508  1207 

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

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

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

1211 
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

1212 
apply (drule_tac x="A{x}" in spec, auto) 
15508  1213 
done 
1214 

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

1215 
lemma fold1_insert: 
15521  1216 
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

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

1219 
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

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

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

1223 
by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
15521  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 
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

1227 

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

1228 
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

1229 
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

1230 

46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

1231 
lemma comp_fun_idem: "comp_fun_idem (op *)" 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

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

1233 

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

1234 
lemma fold1_insert_idem [simp]: 
15521  1235 
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

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

1238 
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

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

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

1243 
proof cases 

41550  1244 
assume a: "a = x" 
1245 
show ?thesis 

15521  1246 
proof cases 
1247 
assume "A' = {}" 

41550  1248 
with A' a show ?thesis by simp 
15521  1249 
next 
1250 
assume "A' \<noteq> {}" 

41550  1251 
with A A' a show ?thesis 
35216  1252 
by (simp add: fold1_insert mult_assoc [symmetric]) 
15521  1253 
qed 
1254 
next 

1255 
assume "a \<noteq> x" 

41550  1256 
with A A' show ?thesis 
35216  1257 
by (simp add: insert_commute fold1_eq_fold) 
15521  1258 
qed 
1259 
qed 

15506  1260 

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

1261 
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

1262 
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

1263 
and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)" 
46898
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

1264 
using N 
1570b30ee040
tuned proofs  eliminated pointless chaining of facts after 'interpret';
wenzelm
parents:
46146
diff
changeset

1265 
proof (induct rule: finite_ne_induct) 
22917  1266 
case singleton thus ?case by simp 
1267 
next 

1268 
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

1269 
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

1270 
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

1271 
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

1272 
also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))" 
22917  1273 
using insert by(simp) 
1274 
also have "insert (h n) (h ` N) = h ` insert n N" by simp 

1275 
finally show ?case . 

1276 
qed 

1277 

32679  1278 
lemma fold1_eq_fold_idem: 
096306d7391d
idempotency 