author  nipkow 
Thu, 17 Mar 2011 09:58:13 +0100  
changeset 41988  c2583bbb92f5 
parent 41987  4ad8f1dc2e0b 
child 42206  0920f709610f 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

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

3 
with contributions by Jeremy Avigad 
12396  4 
*) 
5 

6 
header {* Finite sets *} 

7 

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

9 
imports Option Power 
15131  10 
begin 
12396  11 

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

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

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

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

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

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

21 
assumes "finite F" 

22 
assumes "P {}" 

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

24 
shows "P F" 

25 
using `finite F` proof induct 

26 
show "P {}" by fact 

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

28 
show "P (insert x F)" 

29 
proof cases 

30 
assume "x \<in> F" 

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

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

33 
next 

34 
assume "x \<notin> F" 

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

36 
qed 

37 
qed 

38 

39 

40 
subsubsection {* Choice principles *} 

12396  41 

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

45 
proof  

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

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

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

55 
case empty then show ?case by simp 

29923  56 
next 
57 
case (insert a A) 

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

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

60 
proof 

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

62 
qed 

63 
qed 

64 

23878  65 

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

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

71 
using assms proof induct 

15392  72 
case empty 
41656  73 
show ?case 
74 
proof 

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

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

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

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

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

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

15392  85 
thus ?case by blast 
86 
qed 

87 

88 
lemma nat_seg_image_imp_finite: 

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

15392  91 
case 0 thus ?case by simp 
92 
next 

93 
case (Suc n) 

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

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

96 
show ?case 

97 
proof cases 

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

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

100 
thus ?thesis using finB by simp 

101 
next 

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

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

104 
thus ?thesis using finB by simp 

105 
qed 

106 
qed 

107 

108 
lemma finite_conv_nat_seg_image: 

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

15392  111 

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

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

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

118 
by (auto simp:bij_betw_def) 

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

124 

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

127 
by (fastsimp simp: finite_conv_nat_seg_image) 

29920  128 

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

131 
by (simp add: le_eq_less_or_eq Collect_disj_eq) 

15392  132 

41656  133 

134 
subsubsection {* Finiteness and common set operations *} 

12396  135 

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

138 
proof (induct arbitrary: A rule: finite_induct) 

139 
case empty 

140 
then show ?case by simp 

141 
next 

142 
case (insert x F A) 

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

144 
show "finite A" 

145 
proof cases 

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

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

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

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

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

151 
finally show ?thesis . 

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

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

12396  156 
qed 
157 
qed 

158 

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

161 
by (rule rev_finite_subset) 

29901  162 

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

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

166 
using assms by induct simp_all 

31992  167 

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

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

31992  171 

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

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

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

181 
by (blast intro: finite_subset) 

182 

183 
lemma finite_Collect_conjI [simp, intro]: 

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

185 
by (simp add: Collect_conj_eq) 

186 

187 
lemma finite_Collect_disjI [simp]: 

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

189 
by (simp add: Collect_disj_eq) 

190 

191 
lemma finite_Diff [simp, intro]: 

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

193 
by (rule finite_subset, rule Diff_subset) 

29901  194 

195 
lemma finite_Diff2 [simp]: 

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

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

29901  201 
finally show ?thesis .. 
202 
qed 

203 

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

206 
proof  

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

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

209 
ultimately show ?thesis by simp 

210 
qed 

211 

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

12396  215 

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

219 

220 
lemma finite_Union [simp, intro]: 

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

222 
by (induct rule: finite_induct) simp_all 

223 

224 
lemma finite_UN_I [intro]: 

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

226 
by (induct rule: finite_induct) simp_all 

29903  227 

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

230 
by (blast intro: finite_subset) 

231 

232 
lemma finite_Inter [intro]: 

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

234 
by (blast intro: Inter_lower finite_subset) 

12396  235 

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

238 
by (blast intro: INT_lower finite_subset) 

13825  239 

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

242 
by (induct rule: finite_induct) simp_all 

13825  243 

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

246 
by (simp add: image_Collect [symmetric]) 

247 

41656  248 
lemma finite_imageD: 
249 
"finite (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> finite A" 

12396  250 
proof  
251 
have aux: "!!A. finite (A  {}) = finite A" by simp 

252 
fix B :: "'a set" 

253 
assume "finite B" 

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

255 
apply induct 

256 
apply simp 

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

258 
apply clarify 

259 
apply (simp (no_asm_use) add: inj_on_def) 

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

265 
done 

266 
qed (rule refl) 

267 

41656  268 
lemma finite_surj: 
269 
"finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B" 

270 
by (erule finite_subset) (rule finite_imageI) 

12396  271 

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

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

13825  275 

41656  276 
lemma finite_subset_image: 
277 
assumes "finite B" 

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

279 
using assms proof induct 

280 
case empty then show ?case by simp 

281 
next 

282 
case insert then show ?case 

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

284 
blast 

285 
qed 

286 

287 
lemma finite_vimageI: 

288 
"finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h ` F)" 

289 
apply (induct rule: finite_induct) 

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

291 
apply (subst vimage_insert) 
35216  292 
apply (simp add: finite_subset [OF inj_vimage_singleton]) 
13825  293 
done 
294 

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

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

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

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

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

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

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

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

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

303 

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

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

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

306 

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

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

310 
proof  

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

312 
with assms show ?thesis by simp 

313 
qed 

12396  314 

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

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

318 
proof  

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

320 
with assms show ?thesis by simp 

321 
qed 

29920  322 

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

325 
by (simp add: Plus_def) 

17022  326 

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

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

330 
shows "finite A" "finite B" 

331 
proof  

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

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

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

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

31080  339 
qed 
340 

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

343 
by (auto intro: finite_PlusD finite_Plus) 

31080  344 

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

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

12396  348 

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

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

351 
by (unfold Sigma_def) blast 
12396  352 

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

15402  355 
by (rule finite_SigmaI) 
356 

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

12396  360 

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

361 
lemma finite_cartesian_productD1: 
41656  362 
"finite (A \<times> B) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> finite A" 
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

365 
apply (drule_tac x="fst o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

370 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

373 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

375 

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

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

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

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

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

380 
apply (drule_tac x="snd o f" in spec) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

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

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

385 
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

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

388 
apply (rule_tac x=k in image_eqI, auto) 
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset

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

390 

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

12396  393 
proof 
394 
assume "finite (Pow A)" 

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

12396  397 
next 
398 
assume "finite A" 

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

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

405 
by (simp add: Pow_def [symmetric]) 

29918  406 

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

410 

41656  411 
subsubsection {* Further induction rules on finite sets *} 
412 

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

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

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

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

417 
shows "P F" 

418 
using assms proof induct 

419 
case empty then show ?case by simp 

420 
next 

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

422 
qed 

423 

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

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

426 
assumes empty: "P {}" 

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

428 
shows "P F" 

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

430 
show "P {}" by fact 

31441  431 
next 
41656  432 
fix x F 
433 
assume "finite F" and "x \<notin> F" and 

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

435 
show "P (insert x F)" 

436 
proof (rule insert) 

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

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

439 
with P show "P F" . 

440 
show "finite F" by fact 

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

442 
qed 

443 
qed 

444 

445 
lemma finite_empty_induct: 

446 
assumes "finite A" 

447 
assumes "P A" 

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

449 
shows "P {}" 

450 
proof  

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

452 
proof  

453 
fix B :: "'a set" 

454 
assume "B \<subseteq> A" 

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

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

457 
proof induct 

458 
case empty 

459 
from `P A` show ?case by simp 

460 
next 

461 
case (insert b B) 

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

463 
proof (rule remove) 

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

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

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

467 
qed 

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

469 
finally show ?case . 

470 
qed 

471 
qed 

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

473 
then show ?thesis by simp 

31441  474 
qed 
475 

476 

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

478 

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

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

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

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

485 

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

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

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

488 

27430  489 
end 
490 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35796
diff
changeset

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

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

493 

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

494 
instance unit :: finite proof 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

495 
qed (simp add: UNIV_unit) 
26146  496 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35796
diff
changeset

497 
lemma UNIV_bool [no_atp]: 
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

498 
"UNIV = {False, True}" by auto 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

499 

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

500 
instance bool :: finite proof 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

501 
qed (simp add: UNIV_bool) 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

502 

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

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

504 
qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 
26146  505 

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

506 
lemma finite_option_UNIV [simp]: 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

507 
"finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

508 
by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

509 

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

510 
instance option :: (finite) finite proof 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

511 
qed (simp add: UNIV_option_conv) 
26146  512 

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

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

514 
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

515 

26146  516 
instance "fun" :: (finite, finite) finite 
517 
proof 

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

518 
show "finite (UNIV :: ('a => 'b) set)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

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

523 
by (simp only: finite_Pow_iff finite) 

524 
ultimately show "finite (range ?graph)" 

525 
by (rule finite_subset) 

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

526 
show "inj ?graph" by (rule inj_graph) 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

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

529 

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

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

531 
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 
27981  532 

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

533 

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

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

536 
text {* The intended behaviour is 

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

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

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

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

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

542 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

543 
assumes fun_left_comm: "f x (f y z) = f y (f x z)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

545 

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

546 
text{* On a functional level it looks much nicer: *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

547 

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

548 
lemma fun_comp_comm: "f x \<circ> f y = f y \<circ> f x" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

550 

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

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

552 

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

553 
inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

554 
for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

555 
emptyI [intro]: "fold_graph f z {} z"  
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

556 
insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

557 
\<Longrightarrow> fold_graph f z (insert x A) (f x y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

558 

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

559 
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

560 

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

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

15498  564 
text{*A tempting alternative for the definiens is 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

565 
@{term "if finite A then THE y. fold_graph f z A y else e"}. 
15498  566 
It allows the removal of finiteness assumptions from the theorems 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

567 
@{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}. 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

568 
The proofs become ugly. It is not worth the effort. (???) *} 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

569 

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

570 

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

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

572 
"fold_graph f z (A  {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

573 
by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

574 

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

575 
lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

577 

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

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

580 

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

581 

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

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

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

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

585 
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

586 

36045  587 
lemma fold_graph_insertE_aux: 
588 
"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'" 

589 
proof (induct set: fold_graph) 

590 
case (insertI x A y) show ?case 

591 
proof (cases "x = a") 

592 
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

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

596 
using insertI by auto 

597 
have 1: "f x y = f a (f x y')" 

598 
unfolding y by (rule fun_left_comm) 

599 
have 2: "fold_graph f z (insert x A  {a}) (f x y')" 

600 
using y' and `x \<noteq> a` and `x \<notin> A` 

601 
by (simp add: insert_Diff_if fold_graph.insertI) 

602 
from 1 2 show ?case by fast 

15392  603 
qed 
36045  604 
qed simp 
605 

606 
lemma fold_graph_insertE: 

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

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

609 
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

610 

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

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

612 
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 
36045  613 
proof (induct arbitrary: y set: fold_graph) 
614 
case (insertI x A y v) 

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

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

617 
by (rule fold_graph_insertE) 

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

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

620 
qed fast 

15392  621 

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

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

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

624 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  625 

36045  626 
lemma fold_graph_fold: "finite A \<Longrightarrow> fold_graph f z A (fold f z A)" 
627 
unfolding fold_def 

628 
apply (rule theI') 

629 
apply (rule ex_ex1I) 

630 
apply (erule finite_imp_fold_graph) 

631 
apply (erule (1) fold_graph_determ) 

632 
done 

633 

15392  634 
text{* The base case for @{text fold}: *} 
635 

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

636 
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

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

638 

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

639 
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

640 

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

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

642 
"finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)" 
36045  643 
apply (rule fold_equality) 
644 
apply (erule fold_graph.insertI) 

645 
apply (erule fold_graph_fold) 

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

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

647 

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

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

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

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

651 
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

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

653 
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

654 
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

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

656 

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

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

658 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
35216  659 
by (simp add: fold_fun_comm) 
15392  660 

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

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

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

663 
shows "fold f z A = f x (fold f z (A  {x}))" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

665 
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

666 
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

667 
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

668 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  669 
finally show ?thesis . 
670 
qed 

671 

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

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

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

674 
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

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

676 
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

677 
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

678 
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

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

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

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

682 

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

683 
end 
15392  684 

15480  685 
text{* A simplified version for idempotent functions: *} 
686 

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

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

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

689 
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

690 

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

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

692 
lemma fun_comp_idem : "f x o f x = 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

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

694 

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

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

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

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

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

700 
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

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

703 
assume "x \<notin> A" then show ?thesis using assms by simp 
15480  704 
qed 
705 

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

706 
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

707 

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

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

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

710 
by(simp add:fold_fun_comm) 
15484  711 

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

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

713 

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

714 

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

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

716 

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

717 
lemma (in fun_left_comm) fun_left_comm_apply: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

718 
"fun_left_comm (\<lambda>x. f (g x))" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

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

721 

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

722 
lemma (in fun_left_comm_idem) fun_left_comm_idem_apply: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

723 
"fun_left_comm_idem (\<lambda>x. f (g x))" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

724 
by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

726 

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

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

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

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

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

731 

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

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

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

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

735 
qed auto 
31992  736 

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

737 
lemma (in semilattice_inf) fun_left_comm_idem_inf: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

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

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

741 

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

742 
lemma (in semilattice_sup) fun_left_comm_idem_sup: 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

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

745 
qed (auto simp add: sup_left_commute) 
31992  746 

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

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

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

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

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

751 
interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

752 
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

753 
qed 
31992  754 

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

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

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

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

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

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

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

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

762 

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

763 
context complete_lattice 
31992  764 
begin 
765 

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

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

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

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

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

770 
interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

773 
qed 
31992  774 

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

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

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

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

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

779 
interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

780 
from `finite A` show ?thesis by (induct A arbitrary: B) 
41550  781 
(simp_all add: Sup_insert sup_commute fold_fun_comm) 
31992  782 
qed 
783 

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

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

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

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

787 
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

788 

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

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

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

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

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

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

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

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

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

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

798 
interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

799 
interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

800 
from `finite A` show "?fold = ?inf" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

801 
by (induct A arbitrary: B) 
41550  802 
(simp_all add: INFI_def Inf_insert inf_left_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

803 
qed 
31992  804 

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

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

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

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

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

809 
interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

810 
interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

811 
from `finite A` show "?fold = ?sup" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

812 
by (induct A arbitrary: B) 
41550  813 
(simp_all add: SUPR_def Sup_insert sup_left_commute) 
35817
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

814 
qed 
31992  815 

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

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

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

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

819 
using assms inf_INFI_fold_inf [of A top] by simp 
31992  820 

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

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

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

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

824 
using assms sup_SUPR_fold_sup [of A bot] by simp 
31992  825 

826 
end 

827 

828 

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

829 
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

830 

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

831 
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

832 
where "fold_image f g = fold (%x y. f (g x) y)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

833 

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

834 
lemma fold_image_empty[simp]: "fold_image f g z {} = z" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

835 
by(simp add:fold_image_def) 
15392  836 

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

837 
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

838 
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

839 

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

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

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

842 
shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

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

848 

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

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

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

851 
"finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" 
22262  852 
apply (induct set: finite) 
21575  853 
apply simp 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

854 
apply (simp add: mult_left_commute [of x]) 
15392  855 
done 
856 

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

857 
lemma fold_nest_Un_Int: 
15392  858 
"finite A ==> finite B 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

859 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  860 
apply (induct set: finite) 
21575  861 
apply simp 
15392  862 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
863 
done 

864 

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

865 
lemma fold_nest_Un_disjoint: 
15392  866 
"finite A ==> finite B ==> A Int B = {} 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

867 
==> fold times g z (A Un B) = fold times g (fold times g z B) A" 
15392  868 
by (simp add: fold_nest_Un_Int) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

870 

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

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

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

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

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

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

878 
Fusion theorem, as described in Graham Hutton's paper, 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

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

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

882 

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

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

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

886 
and hyp: "\<And>x y. h (g x y) = times x (h y)" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

887 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  888 
proof  
29223  889 
class_interpret ab_semigroup_mult [g] by fact 
27611  890 
show ?thesis using fin hyp by (induct set: finite) simp_all 
891 
qed 

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

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

893 

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

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

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

896 
(!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

897 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold_image times g z C = fold_image times h z C") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

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

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

902 
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

903 
apply (subgoal_tac "C = insert x (C  {x})") 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

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

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

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

909 
done 
15392  910 

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

911 
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

912 

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

913 
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

914 
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

915 

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

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

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

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

920 

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

921 
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

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

923 
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

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

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

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

928 

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

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

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

931 
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

932 
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

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

934 
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

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

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

937 
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

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

939 

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

940 
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

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

942 
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

943 
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

944 
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

945 

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

946 
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

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

948 
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

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

950 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
41656  951 
apply (induct rule: finite_induct) 
952 
apply simp 

953 
apply atomize 

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

954 
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

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

956 
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

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

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

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

960 

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

961 
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

962 
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

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

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

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

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

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

973 
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

974 
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

975 
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

976 
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

977 

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

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

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

980 
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

981 
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

982 
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

983 
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

984 

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

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

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

987 
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

988 
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

989 
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

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

991 
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

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

993 
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

994 
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

995 
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

996 
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

997 
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

998 
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

999 
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

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

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

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

1003 

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

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

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

1006 
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

1007 
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

1008 
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

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

1010 
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

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

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

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

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

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

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

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

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

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

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

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

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

1023 

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

1024 
end 
22917  1025 

25162  1026 

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

1027 
subsection {* A fold functional for nonempty sets *} 
15392  1028 

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

12396  1030 

23736  1031 
inductive 
22262  1032 
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" 
1033 
for f :: "'a => 'a => 'a" 

1034 
where 

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

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

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

1038 
definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where 
22262  1039 
"fold1 f A == THE x. fold1Set f A x" 
15506  1040 

1041 
lemma fold1Set_nonempty: 

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

1043 
by(erule fold1Set.cases, simp_all) 
15392  1044 

23736  1045 
inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x" 
1046 

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

22262  1048 

1049 

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

35216  1051 
by (blast elim: fold_graph.cases) 
15392  1052 

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

1054 
by (unfold fold1_def) blast 
12396  1055 

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

1059 
apply (auto dest: finite_imp_fold_graph [of _ f]) 
15508  1060 
done 
15506  1061 

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

1062 
text{*First, some lemmas about @{const fold_graph}.*} 
15392  1063 

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

1064 
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

1065 
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

1066 

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

1067 
lemma fun_left_comm: "fun_left_comm(op *)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1068 
by unfold_locales (simp add: mult_ac) 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

1069 

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

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

1071 
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

1072 
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

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

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

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

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

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

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

1085 

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

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

1087 
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

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

1090 
proof (induct rule: fold_graph.induct) 
15508  1091 
case emptyI thus ?case by simp 
1092 
next 

22262  1093 
case (insertI x A y) 
15521  1094 
have "a = x \<or> a \<in> A" using insertI by simp 
1095 
thus ?case 

1096 
proof 

1097 
assume "a = x" 

1098 
with insertI show ?thesis 

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

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

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

1102 
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

1103 
using insertI by force 
15521  1104 
moreover 
1105 
have "insert x (insert b (A  {a})) = insert b (insert x A  {a})" 

1106 
using ainA insertI by blast 

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

1107 
ultimately show ?thesis by simp 
15508  1108 
qed 
1109 
qed 

1110 

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

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

1112 
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

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

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

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

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

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

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

1124 
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

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

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

1128 
qed 
15508  1129 

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

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

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

1133 
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

1134 
apply (drule_tac x="A{x}" in spec, auto) 
15508  1135 
done 
1136 

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

1137 
lemma fold1_insert: 
15521  1138 
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

1139 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1140 
proof  
29223  1141 
interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm) 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

1145 
by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
15521  1146 
qed 
1147 

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

1148 
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

1149 

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

1150 
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

1151 
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

1152 

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

1153 
lemma fun_left_comm_idem: "fun_left_comm_idem(op *)" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

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

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

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

1158 

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

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

1161 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1162 
proof  
29223  1163 
interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

1168 
proof cases 

41550  1169 
assume a: "a = x" 
1170 
show ?thesis 

15521  1171 
proof cases 
1172 
assume "A' = {}" 

41550  1173 
with A' a show ?thesis by simp 
15521  1174 
next 
1175 
assume "A' \<noteq> {}" 

41550  1176 
with A A' a show ?thesis 
35216  1177 
by (simp add: fold1_insert mult_assoc [symmetric]) 
15521  1178 
qed 
1179 
next 

1180 
assume "a \<noteq> x" 

41550  1181 
with A A' show ?thesis 
35216  1182 
by (simp add: insert_commute fold1_eq_fold) 
15521  1183 
qed 
1184 
qed 

15506  1185 

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

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

1187 
assumes hom: "!!x y. h (x * y) = h x * h y" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

1191 
next 

1192 
case (insert n N) 

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

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

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

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

1196 
also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))" 
22917  1197 
using insert by(simp) 
1198 
also have "insert (h n) (h ` N) = h ` insert n N" by simp 

1199 
finally show ?case . 

1200 
qed 

1201 

32679  1202 
lemma fold1_eq_fold_idem: 
1203 
assumes "finite A" 

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

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

1206 
case False 

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

1208 
next 

1209 
interpret fun_left_comm_idem times by (fact fun_left_comm_idem) 

1210 
case True then obtain b B 

1211 
where A: "A = insert a B" and "a \<notin> B" by (rule set_insert) 

1212 
with assms have "finite B" by auto 

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

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

1215 
then show ?thesis 

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

1217 
qed 

1218 

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

1220 

15506  1221 

15508  1222 
text{* Now the recursion rules for definitions: *} 
1223 

22917  1224 
lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a" 
35216  1225 
by simp 
15508  1226 

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

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

1228 
"\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

1230 

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

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

1232 
"\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

1233 
by simp 
15508  1234 

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

1236 

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

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

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

1239 
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

1240 
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

1241 

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

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

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

1244 
==> fold_graph times id a (insert b A) x" 
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

1246 
apply (auto dest: fold_graph_permute_diff) 
15506  1247 
done 
15376  1248 

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

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

1250 
"fold1Set times A x ==> fold1Set times A y ==> y = x" 
15506  1251 
proof (clarify elim!: fold1Set.cases) 
1252 
fix A x B y a b 

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

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

1254 
assume By: "fold_graph times id b B y" 
15506  1255 
assume anotA: "a \<notin> A" 
1256 
assume bnotB: "b \<notin> B" 

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

1258 
show "y=x" 

1259 
proof cases 

1260 
assume same: "a=b" 

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

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

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

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

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

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

1269 
with aB bnotB By 

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

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

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

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

1275 
ultimately show ?thesis by (blast intro: fold_graph_determ) 
15392  1276 
qed 
12396  1277 
qed 
1278 

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

1279 
lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y" 
15506  1280 
by (unfold fold1_def) (blast intro: fold1Set_determ) 
1281 

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

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

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

1284 

15506 