author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 36176  3fe7e97ccca8 
child 36637  74a5c04bf29d 
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 
35719
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

9 
imports Power Option 
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 

23736  14 
inductive finite :: "'a set => bool" 
22262  15 
where 
16 
emptyI [simp, intro!]: "finite {}" 

17 
 insertI [simp, intro!]: "finite A ==> finite (insert a A)" 

12396  18 

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

22 
proof  

28823  23 
from assms have "A \<noteq> UNIV" by blast 
14661  24 
thus ?thesis by blast 
25 
qed 

12396  26 

22262  27 
lemma finite_induct [case_names empty insert, induct set: finite]: 
12396  28 
"finite F ==> 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

29 
P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" 
12396  30 
 {* Discharging @{text "x \<notin> F"} entails extra work. *} 
31 
proof  

13421  32 
assume "P {}" and 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

33 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  34 
assume "finite F" 
35 
thus "P F" 

36 
proof induct 

23389  37 
show "P {}" by fact 
15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

38 
fix x F assume F: "finite F" and P: "P F" 
12396  39 
show "P (insert x F)" 
40 
proof cases 

41 
assume "x \<in> F" 

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

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

44 
next 

45 
assume "x \<notin> F" 

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

47 
qed 

48 
qed 

49 
qed 

50 

15484  51 
lemma finite_ne_induct[case_names singleton insert, consumes 2]: 
52 
assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow> 

53 
\<lbrakk> \<And>x. P{x}; 

54 
\<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk> 

55 
\<Longrightarrow> P F" 

56 
using fin 

57 
proof induct 

58 
case empty thus ?case by simp 

59 
next 

60 
case (insert x F) 

61 
show ?case 

62 
proof cases 

23389  63 
assume "F = {}" 
64 
thus ?thesis using `P {x}` by simp 

15484  65 
next 
23389  66 
assume "F \<noteq> {}" 
67 
thus ?thesis using insert by blast 

15484  68 
qed 
69 
qed 

70 

12396  71 
lemma finite_subset_induct [consumes 2, case_names empty insert]: 
23389  72 
assumes "finite F" and "F \<subseteq> A" 
73 
and empty: "P {}" 

74 
and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 

75 
shows "P F" 

12396  76 
proof  
23389  77 
from `finite F` and `F \<subseteq> A` 
78 
show ?thesis 

12396  79 
proof induct 
23389  80 
show "P {}" by fact 
81 
next 

82 
fix x F 

83 
assume "finite F" and "x \<notin> F" and 

84 
P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 

12396  85 
show "P (insert x F)" 
86 
proof (rule insert) 

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

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

89 
with P show "P F" . 

23389  90 
show "finite F" by fact 
91 
show "x \<notin> F" by fact 

12396  92 
qed 
93 
qed 

94 
qed 

95 

32006  96 

29923  97 
text{* A finite choice principle. Does not need the SOME choice operator. *} 
98 
lemma finite_set_choice: 

99 
"finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)" 

100 
proof (induct set: finite) 

101 
case empty thus ?case by simp 

102 
next 

103 
case (insert a A) 

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

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

106 
proof 

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

108 
qed 

109 
qed 

110 

23878  111 

15392  112 
text{* Finite sets are the images of initial segments of natural numbers: *} 
113 

15510  114 
lemma finite_imp_nat_seg_image_inj_on: 
115 
assumes fin: "finite A" 

116 
shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}" 

15392  117 
using fin 
118 
proof induct 

119 
case empty 

15510  120 
show ?case 
121 
proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 

122 
qed 

15392  123 
next 
124 
case (insert a A) 

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

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

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

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

15392  131 
thus ?case by blast 
132 
qed 

133 

134 
lemma nat_seg_image_imp_finite: 

135 
"!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A" 

136 
proof (induct n) 

137 
case 0 thus ?case by simp 

138 
next 

139 
case (Suc n) 

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

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

142 
show ?case 

143 
proof cases 

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

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

146 
thus ?thesis using finB by simp 

147 
next 

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

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

150 
thus ?thesis using finB by simp 

151 
qed 

152 
qed 

153 

154 
lemma finite_conv_nat_seg_image: 

155 
"finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})" 

15510  156 
by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) 
15392  157 

32988  158 
lemma finite_imp_inj_to_nat_seg: 
159 
assumes "finite A" 

160 
shows "EX f n::nat. f`A = {i. i<n} & inj_on f A" 

161 
proof  

162 
from finite_imp_nat_seg_image_inj_on[OF `finite A`] 

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

164 
by (auto simp:bij_betw_def) 

33057  165 
let ?f = "the_inv_into {i. i<n} f" 
32988  166 
have "inj_on ?f A & ?f ` A = {i. i<n}" 
33057  167 
by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij]) 
32988  168 
thus ?thesis by blast 
169 
qed 

170 

29920  171 
lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" 
172 
by(fastsimp simp: finite_conv_nat_seg_image) 

173 

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

174 
text {* Finiteness and set theoretic constructions *} 
15392  175 

12396  176 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 
29901  177 
by (induct set: finite) simp_all 
12396  178 

179 
lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A" 

180 
 {* Every subset of a finite set is finite. *} 

181 
proof  

182 
assume "finite B" 

183 
thus "!!A. A \<subseteq> B ==> finite A" 

184 
proof induct 

185 
case empty 

186 
thus ?case by simp 

187 
next 

15327
0230a10582d3
changed the order of !!quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset

188 
case (insert x F A) 
23389  189 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" by fact+ 
12396  190 
show "finite A" 
191 
proof cases 

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

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

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

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

23389  196 
also have "insert x (A  {x}) = A" using x by (rule insert_Diff) 
12396  197 
finally show ?thesis . 
198 
next 

23389  199 
show "A \<subseteq> F ==> ?thesis" by fact 
12396  200 
assume "x \<notin> A" 
201 
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) 

202 
qed 

203 
qed 

204 
qed 

205 

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

206 
lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A" 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

207 
by (rule finite_subset) 
1b015caba46c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
huffman
parents:
34007
diff
changeset

208 

12396  209 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 
29901  210 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 
211 

29916  212 
lemma finite_Collect_disjI[simp]: 
29901  213 
"finite{x. P x  Q x} = (finite{x. P x} & finite{x. Q x})" 
214 
by(simp add:Collect_disj_eq) 

12396  215 

216 
lemma finite_Int [simp, intro]: "finite F  finite G ==> finite (F Int G)" 

217 
 {* The converse obviously fails. *} 

29901  218 
by (blast intro: finite_subset) 
219 

29916  220 
lemma finite_Collect_conjI [simp, intro]: 
29901  221 
"finite{x. P x}  finite{x. Q x} ==> finite{x. P x & Q x}" 
222 
 {* The converse obviously fails. *} 

223 
by(simp add:Collect_conj_eq) 

12396  224 

29920  225 
lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}" 
226 
by(simp add: le_eq_less_or_eq) 

227 

12396  228 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 
229 
apply (subst insert_is_Un) 

14208  230 
apply (simp only: finite_Un, blast) 
12396  231 
done 
232 

15281  233 
lemma finite_Union[simp, intro]: 
234 
"\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" 

235 
by (induct rule:finite_induct) simp_all 

236 

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

239 

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

241 
by (blast intro: INT_lower finite_subset) 

242 

12396  243 
lemma finite_empty_induct: 
23389  244 
assumes "finite A" 
245 
and "P A" 

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

247 
shows "P {}" 

12396  248 
proof  
249 
have "P (A  A)" 

250 
proof  

23389  251 
{ 
252 
fix c b :: "'a set" 

253 
assume c: "finite c" and b: "finite b" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

254 
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y  {x})" 
23389  255 
have "c \<subseteq> b ==> P (b  c)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

256 
using c 
23389  257 
proof induct 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

258 
case empty 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

259 
from P1 show ?case by simp 
23389  260 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

261 
case (insert x F) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

262 
have "P (b  F  {x})" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

263 
proof (rule P2) 
23389  264 
from _ b show "finite (b  F)" by (rule finite_subset) blast 
265 
from insert show "x \<in> b  F" by simp 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

267 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

268 
also have "b  F  {x} = b  insert x F" by (rule Diff_insert [symmetric]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32705
diff
changeset

269 
finally show ?case . 
12396  270 
qed 
23389  271 
} 
272 
then show ?thesis by this (simp_all add: assms) 

12396  273 
qed 
23389  274 
then show ?thesis by simp 
12396  275 
qed 
276 

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

279 

280 
lemma finite_Diff2 [simp]: 

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

282 
proof  

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

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

285 
finally show ?thesis .. 

286 
qed 

287 

288 
lemma finite_compl[simp]: 

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

290 
by(simp add:Compl_eq_Diff_UNIV) 

12396  291 

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

295 

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

298 
apply (case_tac "a : A  B") 

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

14208  300 
apply (subst insert_Diff, simp_all) 
12396  301 
done 
302 

303 

15392  304 
text {* Image and Inverse Image over Finite Sets *} 
13825  305 

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

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

22262  308 
by (induct set: finite) simp_all 
13825  309 

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

312 
by (simp add: image_Collect [symmetric]) 

313 

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

314 
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

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

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

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

318 

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

27418  321 
apply (drule finite_imageI, simp add: range_composition) 
13825  322 
done 
323 

12396  324 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
325 
proof  

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

327 
fix B :: "'a set" 

328 
assume "finite B" 

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

330 
apply induct 

331 
apply simp 

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

333 
apply clarify 

334 
apply (simp (no_asm_use) add: inj_on_def) 

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

340 
done 

341 
qed (rule refl) 

342 

343 

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

346 
is included in a singleton. *} 

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

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

348 
apply (blast intro: the_equality [symmetric]) 
13825  349 
done 
350 

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

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

353 
is finite. *} 

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

356 
apply (subst vimage_insert) 
35216  357 
apply (simp add: finite_subset [OF inj_vimage_singleton]) 
13825  358 
done 
359 

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

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

361 
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

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

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

364 
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

365 
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

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

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

368 

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

369 
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

370 
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

371 

13825  372 

15392  373 
text {* The finite UNION of finite sets *} 
12396  374 

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

22262  376 
by (induct set: finite) simp_all 
12396  377 

378 
text {* 

379 
Strengthen RHS to 

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

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

382 
We'd need to prove 

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

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

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

388 
by (blast intro: finite_UN_I finite_subset) 

12396  389 

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

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

393 
apply auto 

394 
done 

395 

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

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

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

399 
apply auto 

400 
done 

401 

402 

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

405 

31080  406 
lemma finite_PlusD: 
407 
fixes A :: "'a set" and B :: "'b set" 

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

409 
shows "finite A" "finite B" 

410 
proof  

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

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

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

414 
next 

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

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

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

418 
qed 

419 

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

421 
by(auto intro: finite_PlusD finite_Plus) 

422 

423 
lemma finite_Plus_UNIV_iff[simp]: 

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

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

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

427 

428 

15392  429 
text {* Sigma of finite sets *} 
12396  430 

431 
lemma finite_SigmaI [simp]: 

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

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

434 

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

437 
by (rule finite_SigmaI) 

438 

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

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

442 
apply (erule ssubst) 

14208  443 
apply (erule finite_SigmaI, auto) 
12396  444 
done 
445 

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

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

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

448 
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

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

450 
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

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

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

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

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

455 
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

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

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

458 
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

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

460 

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

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

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

463 
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

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

465 
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

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

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

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

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

470 
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

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

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

473 
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

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

475 

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

476 

15392  477 
text {* The powerset of a finite set *} 
12396  478 

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

480 
proof 

481 
assume "finite (Pow A)" 

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

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

484 
next 

485 
assume "finite A" 

486 
thus "finite (Pow A)" 

35216  487 
by induct (simp_all add: Pow_insert) 
12396  488 
qed 
489 

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

15392  492 

29918  493 

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

496 

497 

31441  498 
lemma finite_subset_image: 
499 
assumes "finite B" 

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

501 
using assms proof(induct) 

502 
case empty thus ?case by simp 

503 
next 

504 
case insert thus ?case 

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

506 
blast 

507 
qed 

508 

509 

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

511 

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

513 
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" 
27430  514 
begin 
515 

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

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

518 

27430  519 
end 
520 

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

521 
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

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

523 

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

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

525 
qed (simp add: UNIV_unit) 
26146  526 

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

527 
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

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

529 

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

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

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

532 

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

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

534 
qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) 
26146  535 

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

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

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

538 
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

539 

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

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

541 
qed (simp add: UNIV_option_conv) 
26146  542 

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

543 
lemma inj_graph: "inj (%f. {(x, y). y = f x})" 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
25571
diff
changeset

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

545 

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

548 
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

549 
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

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

553 
by (simp only: finite_Pow_iff finite) 

554 
ultimately show "finite (range ?graph)" 

555 
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

556 
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

557 
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

558 
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

559 

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

560 
instance "+" :: (finite, finite) finite proof 
99b6152aedf5
split off theory Big_Operators from theory Finite_Set
haftmann
parents:
35577
diff
changeset

561 
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) 
27981  562 

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

563 

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

564 
subsection {* A basic fold functional for finite sets *} 
15392  565 

566 
text {* The intended behaviour is 

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

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

568 
if @{text f} is ``leftcommutative'': 
15392  569 
*} 
570 

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

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

572 
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

573 
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

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

575 

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

576 
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

577 

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

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

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

580 

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

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

582 

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

583 
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

584 
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

585 
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

586 
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

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

588 

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

589 
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

590 

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

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

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

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

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

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

598 
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

599 

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

600 

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

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

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

603 
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

604 

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

605 
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

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

607 

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

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

609 
by (induct set: finite) auto 
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 

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

612 
subsubsection{*From @{const fold_graph} to @{term fold}*} 
15392  613 

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

614 
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

615 
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

616 

36045  617 
lemma fold_graph_insertE_aux: 
618 
"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'" 

619 
proof (induct set: fold_graph) 

620 
case (insertI x A y) show ?case 

621 
proof (cases "x = a") 

622 
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

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

626 
using insertI by auto 

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

628 
unfolding y by (rule fun_left_comm) 

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

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

631 
by (simp add: insert_Diff_if fold_graph.insertI) 

632 
from 1 2 show ?case by fast 

15392  633 
qed 
36045  634 
qed simp 
635 

636 
lemma fold_graph_insertE: 

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

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

639 
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

640 

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

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

642 
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x" 
36045  643 
proof (induct arbitrary: y set: fold_graph) 
644 
case (insertI x A y v) 

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

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

647 
by (rule fold_graph_insertE) 

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

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

650 
qed fast 

15392  651 

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

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

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

654 
by (unfold fold_def) (blast intro: fold_graph_determ) 
15392  655 

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

658 
apply (rule theI') 

659 
apply (rule ex_ex1I) 

660 
apply (erule finite_imp_fold_graph) 

661 
apply (erule (1) fold_graph_determ) 

662 
done 

663 

15392  664 
text{* The base case for @{text fold}: *} 
665 

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

666 
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

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

668 

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

669 
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

670 

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

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

672 
"finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)" 
36045  673 
apply (rule fold_equality) 
674 
apply (erule fold_graph.insertI) 

675 
apply (erule fold_graph_fold) 

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

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

677 

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

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

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

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

681 
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

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

683 
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

684 
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

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

686 

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

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

688 
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" 
35216  689 
by (simp add: fold_fun_comm) 
15392  690 

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

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

692 
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

693 
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

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

695 
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

696 
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

697 
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

698 
by (rule fold_insert) (simp add: `finite A`)+ 
15535  699 
finally show ?thesis . 
700 
qed 

701 

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

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

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

704 
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

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

706 
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

707 
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

708 
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

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

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

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

712 

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

713 
end 
15392  714 

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

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

717 
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

718 
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

719 
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

720 

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

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

722 
lemma fun_comp_idem : "f x o f x = f x" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

724 

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

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

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

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

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

730 
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

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

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

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

736 
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

737 

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

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

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

740 
by(simp add:fold_fun_comm) 
15484  741 

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

742 
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

743 

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

744 

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

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

746 

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

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

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

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

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

751 

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

752 
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

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

754 
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

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

756 

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

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

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

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

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

761 

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

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

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

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

765 
qed auto 
31992  766 

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

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

768 
"fun_left_comm_idem inf" 
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 
qed (auto simp add: inf_left_commute) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

771 

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

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

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

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

775 
qed (auto simp add: sup_left_commute) 
31992  776 

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

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

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

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

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

781 
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

782 
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

783 
qed 
31992  784 

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

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

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

787 
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

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

789 
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

790 
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

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

792 

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

793 
context complete_lattice 
31992  794 
begin 
795 

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

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

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

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

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

800 
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

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

802 
(simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm) 
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_Sup_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 (Sup A) = fold sup B A" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

808 
proof  
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 
from `finite A` show ?thesis by (induct A arbitrary: B) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

811 
(simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm) 
31992  812 
qed 
813 

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

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

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

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

817 
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

818 

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

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

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

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

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

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

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

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

826 
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

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

828 
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

829 
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

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

831 
by (induct A arbitrary: B) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

833 
qed 
31992  834 

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

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

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

837 
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

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

839 
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

840 
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

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

842 
by (induct A arbitrary: B) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

844 
qed 
31992  845 

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

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

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

848 
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

849 
using assms inf_INFI_fold_inf [of A top] by simp 
31992  850 

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

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

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

853 
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

854 
using assms sup_SUPR_fold_sup [of A bot] by simp 
31992  855 

856 
end 

857 

858 

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

859 
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

860 

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

861 
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

862 
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

863 

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

864 
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

865 
by(simp add:fold_image_def) 
15392  866 

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

868 
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

869 

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

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

871 
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

872 
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

873 
proof  
29223  874 
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

875 
by unfold_locales (simp add: mult_ac) 
31992  876 
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

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

878 

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

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

880 
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

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

884 
apply (simp add: mult_left_commute [of x]) 
15392  885 
done 
886 

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

887 
lemma fold_nest_Un_Int: 
15392  888 
"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

889 
==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)" 
22262  890 
apply (induct set: finite) 
21575  891 
apply simp 
15392  892 
apply (simp add: fold_commute Int_insert_left insert_absorb) 
893 
done 

894 

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

895 
lemma fold_nest_Un_disjoint: 
15392  896 
"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

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

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

900 

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

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

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

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

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

907 
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

908 
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

909 
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

910 
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

911 
*} 
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour 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 
lemma fold_fusion: 
27611  914 
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

915 
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

916 
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

917 
shows "h (fold g j w A) = fold times j (h w) A" 
27611  918 
proof  
29223  919 
class_interpret ab_semigroup_mult [g] by fact 
27611  920 
show ?thesis using fin hyp by (induct set: finite) simp_all 
921 
qed 

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

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

923 

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

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

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

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

927 
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

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

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

930 
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

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

932 
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

933 
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

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

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

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

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

938 
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

939 
done 
15392  940 

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

941 
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

942 

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

943 
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

944 
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

945 

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

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

947 
"finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

948 
apply (induct set: finite) 
d8b8527102f5
added locales folding_one_(idem); various streamlining and tuning
haftmann
parents:
35796
diff
changeset

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

950 

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

951 
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

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

953 
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

954 
fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

957 

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

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

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

960 
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

961 
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

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

963 
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

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

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

966 
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

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

968 

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

969 
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

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

971 
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

972 
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

973 
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

974 

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

975 
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

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

977 
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

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

979 
fold_image times (%i. fold_image times g 1 (A i)) 1 I" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

981 
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

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

983 
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

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

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

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

987 

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

988 
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

989 
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

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

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

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

995 
apply (subst fold_image_UN_disjoint, simp, simp) 
15392  996 
apply blast 
15506  997 
apply simp 
15392  998 
done 
999 

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

1000 
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

1001 
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

1002 
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

1003 
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

1004 

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

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

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

1007 
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

1008 
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

1009 
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

1010 
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

1011 

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

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

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

1014 
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

1015 
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

1016 
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

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

1018 
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

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

1020 
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

1021 
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

1022 
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

1023 
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

1024 
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

1025 
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

1026 
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

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

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

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

1030 

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

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

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

1033 
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

1034 
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

1035 
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

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

1037 
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

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

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

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

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

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

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

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

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

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

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

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

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

1050 

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

1051 
end 
22917  1052 

25162  1053 

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

1054 
subsection {* A fold functional for nonempty sets *} 
15392  1055 

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

12396  1057 

23736  1058 
inductive 
22262  1059 
fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" 
1060 
for f :: "'a => 'a => 'a" 

1061 
where 

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

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

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

1065 
definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where 
22262  1066 
"fold1 f A == THE x. fold1Set f A x" 
15506  1067 

1068 
lemma fold1Set_nonempty: 

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

1070 
by(erule fold1Set.cases, simp_all) 
15392  1071 

23736  1072 
inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x" 
1073 

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

22262  1075 

1076 

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

35216  1078 
by (blast elim: fold_graph.cases) 
15392  1079 

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

1081 
by (unfold fold1_def) blast 
12396  1082 

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

1086 
apply (auto dest: finite_imp_fold_graph [of _ f]) 
15508  1087 
done 
15506  1088 

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

1089 
text{*First, some lemmas about @{const fold_graph}.*} 
15392  1090 

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

1091 
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

1092 
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

1093 

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

1094 
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

1095 
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

1096 

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

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

1098 
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

1099 
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

1100 
proof  
29223  1101 
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

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

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

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

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

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

1112 

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

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

1114 
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

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

1117 
proof (induct rule: fold_graph.induct) 
15508  1118 
case emptyI thus ?case by simp 
1119 
next 

22262  1120 
case (insertI x A y) 
15521  1121 
have "a = x \<or> a \<in> A" using insertI by simp 
1122 
thus ?case 

1123 
proof 

1124 
assume "a = x" 

1125 
with insertI show ?thesis 

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

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

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

1129 
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

1130 
using insertI by force 
15521  1131 
moreover 
1132 
have "insert x (insert b (A  {a})) = insert b (insert x A  {a})" 

1133 
using ainA insertI by blast 

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

1134 
ultimately show ?thesis by simp 
15508  1135 
qed 
1136 
qed 

1137 

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

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

1139 
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

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 assms show ?thesis 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28823
diff
changeset

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

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

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

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

1151 
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

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

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

1155 
qed 
15508  1156 

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

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

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

1160 
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

1161 
apply (drule_tac x="A{x}" in spec, auto) 
15508  1162 
done 
1163 

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

1164 
lemma fold1_insert: 
15521  1165 
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

1166 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1167 
proof  
29223  1168 
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

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

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

1172 
by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
15521  1173 
qed 
1174 

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

1175 
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

1176 

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

1177 
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

1178 
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

1179 

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

1180 
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

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

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

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

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

1185 

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

1186 
lemma fold1_insert_idem [simp]: 
15521  1187 
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

1188 
shows "fold1 times (insert x A) = x * fold1 times A" 
15521  1189 
proof  
29223  1190 
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

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

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

1195 
proof cases 

1196 
assume "a = x" 

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

1197 
thus ?thesis 
15521  1198 
proof cases 
1199 
assume "A' = {}" 

35216  1200 
with prems show ?thesis by simp 
15521  1201 
next 
1202 
assume "A' \<noteq> {}" 

1203 
with prems show ?thesis 

35216  1204 
by (simp add: fold1_insert mult_assoc [symmetric]) 
15521  1205 
qed 
1206 
next 

1207 
assume "a \<noteq> x" 

1208 
with prems show ?thesis 

35216  1209 
by (simp add: insert_commute fold1_eq_fold) 
15521  1210 
qed 
1211 
qed 

15506  1212 

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

1213 
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

1214 
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

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

1218 
next 

1219 
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

1220 
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

1221 
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

1222 
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

1223 
also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))" 
22917  1224 
using insert by(simp) 
1225 
also have "insert (h n) (h ` N) = h ` insert n N" by simp 

1226 
finally show ?case . 

1227 
qed 

1228 

32679  1229 
lemma fold1_eq_fold_idem: 
1230 
assumes "finite A" 

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

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

1233 
case False 

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

1235 
next 

1236 
interpret fun_left_comm_idem times by (fact fun_left_comm_idem) 

1237 
case True then obtain b B 

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

1239 
with assms have "finite B" by auto 

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

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

1242 
then show ?thesis 

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

1244 
qed 

1245 

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

1246 
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

1247 

15506  1248 

15508  1249 
text{* Now the recursion rules for definitions: *} 
1250 

22917  1251 
lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a" 
35216  1252 
by simp 
15508  1253 

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

1254 
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

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

1256 
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

1257 

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

1258 
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

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

1260 
by simp 
15508  1261 

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

1263 

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

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

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

1266 
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

1267 
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

1268 

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

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

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

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

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

1273 
apply (auto dest: fold_graph_permute_diff) 
15506  1274 
done 
15376  1275 

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

1276 
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

1277 
"fold1Set times A x ==> fold1Set times A y ==> y = x" 
15506  1278 
proof (clarify elim!: fold1Set.cases) 
1279 
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

1280 
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

1281 
assume By: "fold_graph times id b B y" 
15506  1282 
assume anotA: "a \<notin> A" 
1283 
assume bnotB: "b \<notin> B" 

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

1285 
show "y=x" 

1286 
proof cases 

1287 
assume same: "a=b" 

1288 
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

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

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

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

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

