author  kuncar 
Tue, 09 Oct 2012 16:57:58 +0200  
changeset 49757  73ab6d4a9236 
parent 49739  13aa6d8268ec 
child 49758  718f10c8bbfc 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

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

3 
with contributions by Jeremy Avigad 
12396  4 
*) 
5 

6 
header {* Finite sets *} 

7 

15131  8 
theory Finite_Set 
38400
9bfcb1507c6b
import swap prevents strange failure of SML code generator for datatypes
haftmann
parents:
37770
diff
changeset

9 
imports Option Power 
15131  10 
begin 
12396  11 

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

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

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

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

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

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

21 

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

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

24 

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

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

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

27 
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

28 
[Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}], 
48128  29 
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

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

31 

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

34 
assumes "finite F" 

35 
assumes "P {}" 

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

37 
shows "P F" 

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

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

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

42 
show "P (insert x F)" 

43 
proof cases 

44 
assume "x \<in> F" 

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

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

47 
next 

48 
assume "x \<notin> F" 

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

50 
qed 

51 
qed 

52 

53 

54 
subsubsection {* Choice principles *} 

12396  55 

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

59 
proof  

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

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

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

69 
case empty then show ?case by simp 

29923  70 
next 
71 
case (insert a A) 

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

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

74 
proof 

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

76 
qed 

77 
qed 

78 

23878  79 

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

15510  82 
lemma finite_imp_nat_seg_image_inj_on: 
41656  83 
assumes "finite A" 
84 
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

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

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

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

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

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

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

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

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

15392  100 
thus ?case by blast 
101 
qed 

102 

103 
lemma nat_seg_image_imp_finite: 

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

15392  106 
case 0 thus ?case by simp 
107 
next 

108 
case (Suc n) 

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

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

111 
show ?case 

112 
proof cases 

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

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

115 
thus ?thesis using finB by simp 

116 
next 

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

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

119 
thus ?thesis using finB by simp 

120 
qed 

121 
qed 

122 

123 
lemma finite_conv_nat_seg_image: 

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

15392  126 

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

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

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

133 
by (auto simp:bij_betw_def) 

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

139 

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

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

142 
by (fastforce simp: finite_conv_nat_seg_image) 
29920  143 

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

146 
by (simp add: le_eq_less_or_eq Collect_disj_eq) 

15392  147 

41656  148 

149 
subsubsection {* Finiteness and common set operations *} 

12396  150 

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

153 
proof (induct arbitrary: A rule: finite_induct) 

154 
case empty 

155 
then show ?case by simp 

156 
next 

157 
case (insert x F A) 

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

159 
show "finite A" 

160 
proof cases 

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

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

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

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

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

166 
finally show ?thesis . 

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

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

12396  171 
qed 
172 
qed 

173 

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

176 
by (rule rev_finite_subset) 

29901  177 

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

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

181 
using assms by induct simp_all 

31992  182 

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

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

31992  186 

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

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

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

196 
by (blast intro: finite_subset) 

197 

198 
lemma finite_Collect_conjI [simp, intro]: 

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

200 
by (simp add: Collect_conj_eq) 

201 

202 
lemma finite_Collect_disjI [simp]: 

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

204 
by (simp add: Collect_disj_eq) 

205 

206 
lemma finite_Diff [simp, intro]: 

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

208 
by (rule finite_subset, rule Diff_subset) 

29901  209 

210 
lemma finite_Diff2 [simp]: 

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

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

29901  216 
finally show ?thesis .. 
217 
qed 

218 

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

221 
proof  

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

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

224 
ultimately show ?thesis by simp 

225 
qed 

226 

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

12396  230 

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

234 

235 
lemma finite_Union [simp, intro]: 

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

237 
by (induct rule: finite_induct) simp_all 

238 

239 
lemma finite_UN_I [intro]: 

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

241 
by (induct rule: finite_induct) simp_all 

29903  242 

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

245 
by (blast intro: finite_subset) 

246 

247 
lemma finite_Inter [intro]: 

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

249 
by (blast intro: Inter_lower finite_subset) 

12396  250 

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

253 
by (blast intro: INT_lower finite_subset) 

13825  254 

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

257 
by (induct rule: finite_induct) simp_all 

13825  258 

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

261 
by (simp add: image_Collect [symmetric]) 

262 

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

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

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

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

270 
case (insert x B) 

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

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

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

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

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

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

277 
then show "finite A" by simp 

278 
qed 

12396  279 

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

282 
by (erule finite_subset) (rule finite_imageI) 

12396  283 

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

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

13825  287 

41656  288 
lemma finite_subset_image: 
289 
assumes "finite B" 

290 
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

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

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

295 
case insert then show ?case 

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

297 
blast 

298 
qed 

299 

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

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

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

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

310 
using finite_vimage_IntI[of F h UNIV] by auto 

311 

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

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

313 
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

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

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

316 
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

317 
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

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

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

320 

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

321 
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

322 
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

323 

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

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

327 
proof  

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

329 
with assms show ?thesis by simp 

330 
qed 

12396  331 

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

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

335 
proof  

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

337 
with assms show ?thesis by simp 

338 
qed 

29920  339 

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

342 
by (simp add: Plus_def) 

17022  343 

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

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

347 
shows "finite A" "finite B" 

348 
proof  

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

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

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

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

31080  356 
qed 
357 

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

360 
by (auto intro: finite_PlusD finite_Plus) 

31080  361 

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

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

12396  365 

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

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

368 
by (unfold Sigma_def) blast 
12396  369 

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

15402  372 
by (rule finite_SigmaI) 
373 

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

12396  377 

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

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

381 
proof  

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

383 
by (auto simp add: finite_conv_nat_seg_image) 

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

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

386 
by (simp add: image_compose) 

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

388 
then show ?thesis 

389 
by (auto simp add: finite_conv_nat_seg_image) 

390 
qed 

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

391 

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

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

395 
proof  

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

397 
by (auto simp add: finite_conv_nat_seg_image) 

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

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

400 
by (simp add: image_compose) 

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

402 
then show ?thesis 

403 
by (auto simp add: finite_conv_nat_seg_image) 

404 
qed 

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

405 

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

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

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

408 
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

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

410 

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

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

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

12396  417 
next 
418 
assume "finite A" 

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

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

425 
by (simp add: Pow_def [symmetric]) 

29918  426 

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

427 
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

428 
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

429 

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

433 

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

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

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

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

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

440 
shows "P F" 

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

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

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

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

446 
qed 

447 

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

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

450 
assumes empty: "P {}" 

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

452 
shows "P F" 

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

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

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

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

460 
show "P (insert x F)" 

461 
proof (rule insert) 

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

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

464 
with P show "P F" . 

465 
show "finite F" by fact 

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

467 
qed 

468 
qed 

469 

470 
lemma finite_empty_induct: 

471 
assumes "finite A" 

472 
assumes "P A" 

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

474 
shows "P {}" 

475 
proof  

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

477 
proof  

478 
fix B :: "'a set" 

479 
assume "B \<subseteq> A" 

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

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

482 
proof induct 

483 
case empty 

484 
from `P A` show ?case by simp 

485 
next 

486 
case (insert b B) 

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

488 
proof (rule remove) 

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

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

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

492 
qed 

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

494 
finally show ?case . 

495 
qed 

496 
qed 

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

498 
then show ?thesis by simp 

31441  499 
qed 
500 

501 

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

503 

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

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

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

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

510 

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

511 
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

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

513 

27430  514 
end 
515 

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

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

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

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

519 
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

520 
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

521 

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

524 
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

525 
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

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

529 
by (simp only: finite_Pow_iff finite) 

530 
ultimately show "finite (range ?graph)" 

531 
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

532 
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

533 
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

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 

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

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

537 
by default (simp add: UNIV_bool) 
44831  538 

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

541 

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

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

543 
by default (simp add: UNIV_unit) 
44831  544 

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

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

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

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

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

551 

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

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

553 
by default (simp add: UNIV_option_conv) 
44831  554 

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

555 

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

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

558 
text {* The intended behaviour is 

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

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

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

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

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

564 
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

565 
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

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

567 

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

568 
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

569 
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

570 

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

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

572 

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

573 
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

574 
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

575 
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

576 
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

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

578 

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

579 
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

580 

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

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

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

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

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

588 
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

589 

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

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

592 

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 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  595 

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

596 
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

597 
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

598 

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

601 
proof (induct set: fold_graph) 

602 
case (insertI x A y) show ?case 

603 
proof (cases "x = a") 

604 
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

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

608 
using insertI by auto 

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

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

618 
lemma fold_graph_insertE: 

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

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

621 
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

622 

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

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

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

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

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

629 
by (rule fold_graph_insertE) 

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

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

632 
qed fast 

15392  633 

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

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

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

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

42272  638 
lemma fold_graph_fold: 
639 
assumes "finite A" 

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

641 
proof  

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

643 
moreover note fold_graph_determ 

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

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

646 
then show ?thesis by (unfold fold_def) 

647 
qed 

36045  648 

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

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

651 
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

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

653 

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

654 
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

655 

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

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

659 
proof (rule fold_equality) 

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

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

662 
qed 

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

663 

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

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

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

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

667 
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

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

669 
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

670 
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

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

672 

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

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

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

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

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

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

681 
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

682 
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

683 
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

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

687 

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

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

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

690 
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

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

692 
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

693 
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

694 
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

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

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

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

698 

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

701 
lemma fold_image: 

702 
assumes "finite A" and "inj_on g A" 

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

704 
using assms 

705 
proof induction 

706 
case (insert a F) 

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

708 
from insert show ?case by auto 

709 
qed (simp) 

710 

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

711 
end 
15392  712 

49724  713 
lemma fold_cong: 
714 
assumes "comp_fun_commute f" "comp_fun_commute g" 

715 
assumes "finite A" and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x" 

716 
and "A = B" and "s = t" 

717 
shows "Finite_Set.fold f s A = Finite_Set.fold g t B" 

718 
proof  

719 
have "Finite_Set.fold f s A = Finite_Set.fold g s A" 

720 
using `finite A` cong proof (induct A) 

721 
case empty then show ?case by simp 

722 
next 

723 
case (insert x A) 

724 
interpret f: comp_fun_commute f by (fact `comp_fun_commute f`) 

725 
interpret g: comp_fun_commute g by (fact `comp_fun_commute g`) 

726 
from insert show ?case by simp 

727 
qed 

728 
with assms show ?thesis by simp 

729 
qed 

730 

731 

15480  732 
text{* A simplified version for idempotent functions: *} 
733 

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

734 
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

735 
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

736 
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

737 

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

738 
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

739 
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

740 

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

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

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

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

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

746 
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

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

749 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  750 
qed 
751 

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

752 
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

753 

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

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

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

756 
by(simp add:fold_fun_comm) 
15484  757 

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

758 
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

759 

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

760 

49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

761 
subsubsection {* Liftings to @{text comp_fun_commute} etc. *} 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

762 

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

763 
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

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

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

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

767 

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

768 
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

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

770 
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

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

772 

49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

773 
lemma (in comp_fun_commute) comp_fun_commute_funpow: 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

774 
"comp_fun_commute (\<lambda>x. f x ^^ g x)" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

775 
proof 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

776 
fix y x 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

777 
show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

778 
proof (cases "x = y") 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

779 
case True then show ?thesis by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

780 
next 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

781 
case False show ?thesis 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

782 
proof (induct "g x" arbitrary: g) 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

783 
case 0 then show ?case by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

784 
next 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

785 
case (Suc n g) 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

786 
have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

787 
proof (induct "g y" arbitrary: g) 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

788 
case 0 then show ?case by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

789 
next 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

790 
case (Suc n g) 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

791 
def h \<equiv> "\<lambda>z. g z  1" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

792 
with Suc have "n = h y" by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

793 
with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

794 
by auto 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

795 
from Suc h_def have "g y = Suc (h y)" by simp 
49739  796 
then show ?case by (simp add: comp_assoc hyp) 
49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

797 
(simp add: o_assoc comp_fun_commute) 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

798 
qed 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

799 
def h \<equiv> "\<lambda>z. if z = x then g x  1 else g z" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

800 
with Suc have "n = h x" by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

801 
with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y" 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

802 
by auto 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

803 
with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

804 
from Suc h_def have "g x = Suc (h x)" by simp 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

805 
then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) 
49739  806 
(simp add: comp_assoc hyp1) 
49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

807 
qed 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

808 
qed 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

809 
qed 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

810 

bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

811 

bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

812 
subsubsection {* Expressing set operations via @{const fold} *} 
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
48891
diff
changeset

813 

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

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

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

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

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

818 

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

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

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

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

822 
qed auto 
31992  823 

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

824 
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

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

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

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

828 

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

829 
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

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

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

832 
qed (auto simp add: sup_left_commute) 
31992  833 

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

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

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

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

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

838 
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

839 
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

840 
qed 
31992  841 

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

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

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

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

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

846 
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

847 
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

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

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

850 

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

853 

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

855 
proof  

856 
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) 

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

858 
qed 

859 

860 
lemma inter_filter: 

861 
assumes "finite B" 

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

863 
using assms 

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

865 

866 
lemma project_filter: 

867 
assumes "finite A" 

49757
73ab6d4a9236
rename Set.project to Set.filter  more appropriate name
kuncar
parents:
49739
diff
changeset

868 
shows "Set.filter P A = filter P A" 
48619  869 
using assms 
870 
by (induct A) 

49757
73ab6d4a9236
rename Set.project to Set.filter  more appropriate name
kuncar
parents:
49739
diff
changeset

871 
(auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold]) 
48619  872 

873 
lemma image_fold_insert: 

874 
assumes "finite A" 

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

876 
using assms 

877 
proof  

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

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

880 
qed 

881 

882 
lemma Ball_fold: 

883 
assumes "finite A" 

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

885 
using assms 

886 
proof  

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

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

889 
qed 

890 

891 
lemma Bex_fold: 

892 
assumes "finite A" 

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

894 
using assms 

895 
proof  

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

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

898 
qed 

899 

900 
lemma comp_fun_commute_Pow_fold: 

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

902 
by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast 

903 

904 
lemma Pow_fold: 

905 
assumes "finite A" 

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

907 
using assms 

908 
proof  

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

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

911 
qed 

912 

913 
lemma fold_union_pair: 

914 
assumes "finite B" 

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

916 
proof  

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

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

919 
qed 

920 

921 
lemma comp_fun_commute_product_fold: 

922 
assumes "finite B" 

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

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

925 

926 
lemma product_fold: 

927 
assumes "finite A" 

928 
assumes "finite B" 

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

930 
using assms unfolding Sigma_def 

931 
by (induct A) 

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

933 

934 

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

935 
context complete_lattice 
31992  936 
begin 
937 

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

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

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

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

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

942 
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

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

945 
qed 
31992  946 

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

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

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

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

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

951 
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

952 
from `finite A` show ?thesis by (induct A arbitrary: B) 
44919  953 
(simp_all add: sup_commute fold_fun_comm) 
31992  954 
qed 
955 

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

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

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

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

959 
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

960 

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

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

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

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

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

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

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

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

968 
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

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

970 
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

971 
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

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

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

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

975 
qed 
31992  976 

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

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

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

979 
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

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

981 
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

982 
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

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

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

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

986 
qed 
31992  987 

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

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

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

990 
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

991 
using assms inf_INF_fold_inf [of A top] by simp 
31992  992 

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

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

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

995 
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

996 
using assms sup_SUP_fold_sup [of A bot] by simp 
31992  997 

998 
end 

999 

1000 

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

1001 
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

1002 

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

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

1005 

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

1006 
lemma fold_image_empty[simp]: "fold_image f g z {} = z" 
42875  1007 
by (simp add:fold_image_def) 
15392  1008 

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

1009 
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

1010 
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

1011 

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

1012 
lemma fold_image_insert[simp]: 
42875  1013 
assumes "finite A" and "a \<notin> A" 
1014 
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

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

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

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

1018 
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

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

1020 

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

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

1024 
using assms by induct auto 

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

1025 

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

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

1029 
proof  

1030 
from `finite A` 

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

1032 
proof (induct arbitrary: C) 

1033 
case empty then show ?case by simp 

1034 
next 

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

1036 
apply (simp add: subset_insert_iff, clarify) 

1037 
apply (subgoal_tac "finite C") 

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

1038 
prefer 2 apply (blast dest: finite_subset [rotated]) 
42875  1039 
apply (subgoal_tac "C = insert x (C  {x})") 
1040 
prefer 2 apply blast 

1041 
apply (erule ssubst) 

1042 
apply (simp add: Ball_def del: insert_Diff_single) 

1043 
done 

1044 
qed 

1045 
with g_h show ?thesis by simp 

1046 
qed 

15392  1047 

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

1048 
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

1049 

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

1050 
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

1051 
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

1052 

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

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

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

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

1057 

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

1058 
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

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

1060 
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

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

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

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

1065 

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

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

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

1068 
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

1069 
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

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

1071 
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

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

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

1074 
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

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

1076 

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

1077 
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

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

1079 
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

1080 
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

1081 
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

1082 

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

1083 
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

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

1085 
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

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

1087 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
41656  1088 
apply (induct rule: finite_induct) 
1089 
apply simp 

1090 
apply atomize 

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

1091 
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

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

1093 
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

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

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

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

1097 

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

1098 
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

1099 
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

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

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

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

1105 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  1106 
apply blast 
15506  1107 
apply simp 
15392  1108 
done 
1109 

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

1110 
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

1111 
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

1112 
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

1113 
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

1114 

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

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

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

1117 
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

1118 
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

1119 
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

1120 
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

1121 

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

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

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

1124 
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

1125 
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

1126 
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

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

1128 
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

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

1130 
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

1131 
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

1132 
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

1133 
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

1134 
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

1135 
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

1136 
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

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

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

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

1140 

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

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

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

1143 
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

1144 
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

1145 
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

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

1147 
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

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

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

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

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

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

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

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

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

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

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

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

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

1160 

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

1161 
end 
22917  1162 

25162  1163 

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

1164 
subsection {* A fold functional for nonempty sets *} 
15392  1165 

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

12396  1167 

23736  1168 
inductive 
22262  1169 
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" 
1170 
for f :: "'a => 'a => 'a" 

1171 
where 

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

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

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

1175 
definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where 
22262  1176 
"fold1 f A == THE x. fold1Set f A x" 
15506  1177 

1178 
lemma fold1Set_nonempty: 

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

1180 
by(erule fold1Set.cases, simp_all) 
15392  1181 

23736  1182 
inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x" 
1183 

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

22262  1185 

1186 

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

35216  1188 
by (blast elim: fold_graph.cases) 
15392  1189 

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

1191 
by (unfold fold1_def) blast 
12396  1192 

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

1196 
apply (auto dest: finite_imp_fold_graph [of _ f]) 
15508  1197 
done 
15506  1198 

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

1199 
text{*First, some lemmas about @{const fold_graph}.*} 
15392  1200 

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

1201 
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

1202 
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

1203 

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

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

1205 
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

1206 

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

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

1208 
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

1209 
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

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

1211 
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

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

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

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

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

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

1222 

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

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

1224 
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

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

1227 
proof (induct rule: fold_graph.induct) 
15508  1228 
case emptyI thus ?case by simp 
1229 
next 

22262  1230 
case (insertI x A y) 
15521  1231 
have "a = x \<or> a \<in> A" using insertI by simp 
1232 
thus ?case 

1233 
proof 

1234 
assume "a = x" 

1235 
with insertI show ?thesis 

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

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

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

1239 
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

1240 
using insertI by force 
15521  1241 
moreover 
1242 
have "insert x (insert b (A  {a})) = insert b (insert x A  {a})" 

1243 
using ainA insertI by blast 

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

1244 
ultimately show ?thesis by simp 
15508  1245 
qed 
1246 
qed 

1247 

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

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

1249 
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

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

1251 
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

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

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

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

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

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

1261 
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

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

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

1265 
qed 
15508  1266 

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

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

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

1270 
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

1271 
apply (drule_tac x="A{x}" in spec, auto) 
15508  1272 
done 
1273 

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

1274 
lemma fold1_insert: 
15521  1275 
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

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

1278 
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

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

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

1282 
by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
15521  1283 
qed 
1284 

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

1285 
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

1286 

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

1287 
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

1288 
begin 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of th 