author  nipkow 
Thu, 09 Dec 2004 18:30:59 +0100  
changeset 15392  290bc97038c7 
parent 15376  302ef111b621 
child 15402  97204f3b4705 
permissions  rwrr 
12396  1 
(* Title: HOL/Finite_Set.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 

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

4 
Additions by Jeremy Avigad in Feb 2004 
15376  5 

15392  6 
FIXME: define card via fold and derive as many lemmas as possible from fold. 
12396  7 
*) 
8 

9 
header {* Finite sets *} 

10 

15131  11 
theory Finite_Set 
15140  12 
imports Divides Power Inductive 
15131  13 
begin 
12396  14 

15392  15 
subsection {* Definition and basic properties *} 
12396  16 

17 
consts Finites :: "'a set set" 

13737  18 
syntax 
19 
finite :: "'a set => bool" 

20 
translations 

21 
"finite A" == "A : Finites" 

12396  22 

23 
inductive Finites 

24 
intros 

25 
emptyI [simp, intro!]: "{} : Finites" 

26 
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" 

27 

28 
axclass finite \<subseteq> type 

29 
finite: "finite UNIV" 

30 

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

34 
proof  

35 
from prems have "A \<noteq> UNIV" by blast 

36 
thus ?thesis by blast 

37 
qed 

12396  38 

39 
lemma finite_induct [case_names empty insert, induct set: Finites]: 

40 
"finite F ==> 

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

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

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

45 
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" 
12396  46 
assume "finite F" 
47 
thus "P F" 

48 
proof induct 

49 
show "P {}" . 

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

50 
fix x F assume F: "finite F" and P: "P F" 
12396  51 
show "P (insert x F)" 
52 
proof cases 

53 
assume "x \<in> F" 

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

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

56 
next 

57 
assume "x \<notin> F" 

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

59 
qed 

60 
qed 

61 
qed 

62 

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

64 
"finite F ==> F \<subseteq> A ==> 

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

65 
P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> 
12396  66 
P F" 
67 
proof  

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

69 
"!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" 
12396  70 
assume "finite F" 
71 
thus "F \<subseteq> A ==> P F" 

72 
proof induct 

73 
show "P {}" . 

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

74 
fix x F assume "finite F" and "x \<notin> F" 
12396  75 
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" 
76 
show "P (insert x F)" 

77 
proof (rule insert) 

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

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

80 
with P show "P F" . 

81 
qed 

82 
qed 

83 
qed 

84 

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

87 
lemma finite_imp_nat_seg_image: 

88 
assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}" 

89 
using fin 

90 
proof induct 

91 
case empty 

92 
show ?case 

93 
proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed 

94 
next 

95 
case (insert a A) 

96 
from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast 

97 
hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}" 

98 
by (auto simp add:image_def Ball_def) 

99 
thus ?case by blast 

100 
qed 

101 

102 
lemma nat_seg_image_imp_finite: 

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

104 
proof (induct n) 

105 
case 0 thus ?case by simp 

106 
next 

107 
case (Suc n) 

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

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

110 
show ?case 

111 
proof cases 

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

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

114 
thus ?thesis using finB by simp 

115 
next 

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

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

118 
thus ?thesis using finB by simp 

119 
qed 

120 
qed 

121 

122 
lemma finite_conv_nat_seg_image: 

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

124 
by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite) 

125 

126 
subsubsection{* Finiteness and set theoretic constructions *} 

127 

12396  128 
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" 
129 
 {* The union of two finite sets is finite. *} 

130 
by (induct set: Finites) simp_all 

131 

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

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

134 
proof  

135 
assume "finite B" 

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

137 
proof induct 

138 
case empty 

139 
thus ?case by simp 

140 
next 

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

141 
case (insert x F A) 
12396  142 
have A: "A \<subseteq> insert x F" and r: "A  {x} \<subseteq> F ==> finite (A  {x})" . 
143 
show "finite A" 

144 
proof cases 

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

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

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

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

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

150 
finally show ?thesis . 

151 
next 

152 
show "A \<subseteq> F ==> ?thesis" . 

153 
assume "x \<notin> A" 

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

155 
qed 

156 
qed 

157 
qed 

158 

159 
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" 

160 
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) 

161 

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

163 
 {* The converse obviously fails. *} 

164 
by (blast intro: finite_subset) 

165 

166 
lemma finite_insert [simp]: "finite (insert a A) = finite A" 

167 
apply (subst insert_is_Un) 

14208  168 
apply (simp only: finite_Un, blast) 
12396  169 
done 
170 

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

173 
by (induct rule:finite_induct) simp_all 

174 

12396  175 
lemma finite_empty_induct: 
176 
"finite A ==> 

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

178 
proof  

179 
assume "finite A" 

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

181 
have "P (A  A)" 

182 
proof  

183 
fix c b :: "'a set" 

184 
presume c: "finite c" and b: "finite b" 

185 
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y  {x})" 

186 
from c show "c \<subseteq> b ==> P (b  c)" 

187 
proof induct 

188 
case empty 

189 
from P1 show ?case by simp 

190 
next 

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

191 
case (insert x F) 
12396  192 
have "P (b  F  {x})" 
193 
proof (rule P2) 

194 
from _ b show "finite (b  F)" by (rule finite_subset) blast 

195 
from insert show "x \<in> b  F" by simp 

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

197 
qed 

198 
also have "b  F  {x} = b  insert x F" by (rule Diff_insert [symmetric]) 

199 
finally show ?case . 

200 
qed 

201 
next 

202 
show "A \<subseteq> A" .. 

203 
qed 

204 
thus "P {}" by simp 

205 
qed 

206 

207 
lemma finite_Diff [simp]: "finite B ==> finite (B  Ba)" 

208 
by (rule Diff_subset [THEN finite_subset]) 

209 

210 
lemma finite_Diff_insert [iff]: "finite (A  insert a B) = finite (A  B)" 

211 
apply (subst Diff_insert) 

212 
apply (case_tac "a : A  B") 

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

14208  214 
apply (subst insert_Diff, simp_all) 
12396  215 
done 
216 

217 

15392  218 
text {* Image and Inverse Image over Finite Sets *} 
13825  219 

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

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

222 
by (induct set: Finites) simp_all 

223 

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

224 
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

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

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

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

228 

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

14208  231 
apply (drule finite_imageI, simp) 
13825  232 
done 
233 

12396  234 
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" 
235 
proof  

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

237 
fix B :: "'a set" 

238 
assume "finite B" 

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

240 
apply induct 

241 
apply simp 

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

243 
apply clarify 

244 
apply (simp (no_asm_use) add: inj_on_def) 

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

250 
done 

251 
qed (rule refl) 

252 

253 

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

256 
is included in a singleton. *} 

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

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

258 
apply (blast intro: the_equality [symmetric]) 
13825  259 
done 
260 

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

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

263 
is finite. *} 

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

264 
apply (induct set: Finites, simp_all) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

265 
apply (subst vimage_insert) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

266 
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
13825  267 
done 
268 

269 

15392  270 
text {* The finite UNION of finite sets *} 
12396  271 

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

273 
by (induct set: Finites) simp_all 

274 

275 
text {* 

276 
Strengthen RHS to 

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

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

279 
We'd need to prove 

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

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

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

284 
by (blast intro: finite_UN_I finite_subset) 

285 

286 

15392  287 
text {* Sigma of finite sets *} 
12396  288 

289 
lemma finite_SigmaI [simp]: 

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

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

292 

293 
lemma finite_Prod_UNIV: 

294 
"finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" 

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

296 
apply (erule ssubst) 

14208  297 
apply (erule finite_SigmaI, auto) 
12396  298 
done 
299 

300 
instance unit :: finite 

301 
proof 

302 
have "finite {()}" by simp 

303 
also have "{()} = UNIV" by auto 

304 
finally show "finite (UNIV :: unit set)" . 

305 
qed 

306 

307 
instance * :: (finite, finite) finite 

308 
proof 

309 
show "finite (UNIV :: ('a \<times> 'b) set)" 

310 
proof (rule finite_Prod_UNIV) 

311 
show "finite (UNIV :: 'a set)" by (rule finite) 

312 
show "finite (UNIV :: 'b set)" by (rule finite) 

313 
qed 

314 
qed 

315 

316 

15392  317 
text {* The powerset of a finite set *} 
12396  318 

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

320 
proof 

321 
assume "finite (Pow A)" 

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

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

324 
next 

325 
assume "finite A" 

326 
thus "finite (Pow A)" 

327 
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) 

328 
qed 

329 

15392  330 

331 
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A" 

332 
by(blast intro: finite_subset[OF subset_Pow_Union]) 

333 

334 

12396  335 
lemma finite_converse [iff]: "finite (r^1) = finite r" 
336 
apply (subgoal_tac "r^1 = (%(x,y). (y,x))`r") 

337 
apply simp 

338 
apply (rule iffI) 

339 
apply (erule finite_imageD [unfolded inj_on_def]) 

340 
apply (simp split add: split_split) 

341 
apply (erule finite_imageI) 

14208  342 
apply (simp add: converse_def image_def, auto) 
12396  343 
apply (rule bexI) 
344 
prefer 2 apply assumption 

345 
apply simp 

346 
done 

347 

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

348 

15392  349 
text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi 
350 
Ehmety) *} 

12396  351 

352 
lemma finite_Field: "finite r ==> finite (Field r)" 

353 
 {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} 

354 
apply (induct set: Finites) 

355 
apply (auto simp add: Field_def Domain_insert Range_insert) 

356 
done 

357 

358 
lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" 

359 
apply clarify 

360 
apply (erule trancl_induct) 

361 
apply (auto simp add: Field_def) 

362 
done 

363 

364 
lemma finite_trancl: "finite (r^+) = finite r" 

365 
apply auto 

366 
prefer 2 

367 
apply (rule trancl_subset_Field2 [THEN finite_subset]) 

368 
apply (rule finite_SigmaI) 

369 
prefer 3 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
13595
diff
changeset

370 
apply (blast intro: r_into_trancl' finite_subset) 
12396  371 
apply (auto simp add: finite_Field) 
372 
done 

373 

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

374 
lemma finite_cartesian_product: "[ finite A; finite B ] ==> 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

375 
finite (A <*> B)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

376 
by (rule finite_SigmaI) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

377 

12396  378 

15392  379 
subsection {* A fold functional for finite sets *} 
380 

381 
text {* The intended behaviour is 

382 
@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"} 

383 
if @{text f} is associativecommutative. For an application of @{text fold} 

384 
se the definitions of sums and products over finite sets. 

385 
*} 

386 

387 
consts 

388 
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set" 

389 

390 
inductive "foldSet f g e" 

391 
intros 

392 
emptyI [intro]: "({}, e) : foldSet f g e" 

393 
insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk> 

394 
\<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e" 

395 

396 
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e" 

397 

398 
constdefs 

399 
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" 

400 
"fold f g e A == THE x. (A, x) : foldSet f g e" 

401 

402 
lemma Diff1_foldSet: 

403 
"(A  {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e" 

404 
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) 

405 

406 
lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A" 

407 
by (induct set: foldSet) auto 

408 

409 
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e" 

410 
by (induct set: Finites) auto 

411 

412 

413 
subsubsection {* Commutative monoids *} 

414 

415 
locale ACf = 

416 
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

417 
assumes commute: "x \<cdot> y = y \<cdot> x" 

418 
and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

419 

420 
locale ACe = ACf + 

421 
fixes e :: 'a 

422 
assumes ident [simp]: "x \<cdot> e = x" 

423 

424 
lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

425 
proof  

426 
have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute) 

427 
also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 

428 
also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 

429 
finally show ?thesis . 

430 
qed 

431 

432 
lemmas (in ACf) AC = assoc commute left_commute 

433 

434 
lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 

435 
proof  

436 
have "x \<cdot> e = x" by (rule ident) 

437 
thus ?thesis by (subst commute) 

438 
qed 

439 

440 
subsubsection{*From @{term foldSet} to @{term fold}*} 

441 

442 
lemma (in ACf) foldSet_determ_aux: 

443 
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> 

444 
\<Longrightarrow> x' = x" 

445 
proof (induct n) 

446 
case 0 thus ?case by auto 

447 
next 

448 
case (Suc n) 

449 
have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> 

450 
\<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}" 

451 
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . 

452 
show ?case 

453 
proof cases 

454 
assume "EX k<n. h n = h k" 

455 
hence card': "A = h ` {i. i < n}" 

456 
using card by (auto simp:image_def less_Suc_eq) 

457 
show ?thesis by(rule IH[OF card' Afoldx Afoldy]) 

458 
next 

459 
assume new: "\<not>(EX k<n. h n = h k)" 

460 
show ?thesis 

461 
proof (rule foldSet.cases[OF Afoldx]) 

462 
assume "(A, x) = ({}, e)" 

463 
thus "x' = x" using Afoldy by (auto) 

464 
next 

465 
fix B b y 

466 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

467 
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" 

468 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 

469 
show ?thesis 

470 
proof (rule foldSet.cases[OF Afoldy]) 

471 
assume "(A,x') = ({}, e)" 

472 
thus ?thesis using A1 by auto 

473 
next 

474 
fix C c z 

475 
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" 

476 
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" 

477 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto 

478 
let ?h = "%i. if h i = b then h n else h i" 

479 
have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 

480 
(* move down? *) 

481 
have less: "B = ?h`{i. i<n}" (is "_ = ?r") 

482 
proof 

483 
show "B \<subseteq> ?r" 

484 
proof 

485 
fix u assume "u \<in> B" 

486 
hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+ 

487 
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" 

488 
using card by(auto simp:image_def) 

489 
show "u \<in> ?r" 

490 
proof cases 

491 
assume "i\<^isub>u < n" 

492 
thus ?thesis using unotb by(fastsimp) 

493 
next 

494 
assume "\<not> i\<^isub>u < n" 

495 
with below have [simp]: "i\<^isub>u = n" by arith 

496 
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k" 

497 
using A1 card by blast 

498 
have "i\<^isub>k < n" 

499 
proof (rule ccontr) 

500 
assume "\<not> i\<^isub>k < n" 

501 
hence "i\<^isub>k = n" using i\<^isub>k by arith 

502 
thus False using unotb by simp 

503 
qed 

504 
thus ?thesis by(auto simp add:image_def) 

505 
qed 

506 
qed 

507 
next 

508 
show "?r \<subseteq> B" 

509 
proof 

510 
fix u assume "u \<in> ?r" 

511 
then obtain i\<^isub>u where below: "i\<^isub>u < n" and 

512 
or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

513 
by(auto simp:image_def) 

514 
from or show "u \<in> B" 

515 
proof 

516 
assume [simp]: "b = h i\<^isub>u \<and> u = h n" 

517 
have "u \<in> A" using card by auto 

518 
moreover have "u \<noteq> b" using new below by auto 

519 
ultimately show "u \<in> B" using A1 by blast 

520 
next 

521 
assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" 

522 
moreover hence "u \<in> A" using card below by auto 

523 
ultimately show "u \<in> B" using A1 by blast 

524 
qed 

525 
qed 

526 
qed 

527 
show ?thesis 

528 
proof cases 

529 
assume "b = c" 

530 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

531 
ultimately show ?thesis using IH[OF less] y z x x' by auto 

532 
next 

533 
assume diff: "b \<noteq> c" 

534 
let ?D = "B  {c}" 

535 
have B: "B = insert c ?D" and C: "C = insert b ?D" 

536 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

537 
have "finite ?D" using finA A1 by simp 

538 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" 

539 
using finite_imp_foldSet by rules 

540 
moreover have cinB: "c \<in> B" using B by(auto) 

541 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" 

542 
by(rule Diff1_foldSet) 

543 
hence "g c \<cdot> d = y" by(rule IH[OF less y]) 

544 
moreover have "g b \<cdot> d = z" 

545 
proof (rule IH[OF _ z]) 

546 
let ?h = "%i. if h i = c then h n else h i" 

547 
show "C = ?h`{i. i<n}" (is "_ = ?r") 

548 
proof 

549 
show "C \<subseteq> ?r" 

550 
proof 

551 
fix u assume "u \<in> C" 

552 
hence uinA: "u \<in> A" and unotc: "u \<noteq> c" 

553 
using A2 notinC by blast+ 

554 
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" 

555 
using card by(auto simp:image_def) 

556 
show "u \<in> ?r" 

557 
proof cases 

558 
assume "i\<^isub>u < n" 

559 
thus ?thesis using unotc by(fastsimp) 

560 
next 

561 
assume "\<not> i\<^isub>u < n" 

562 
with below have [simp]: "i\<^isub>u = n" by arith 

563 
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k" 

564 
using A2 card by blast 

565 
have "i\<^isub>k < n" 

566 
proof (rule ccontr) 

567 
assume "\<not> i\<^isub>k < n" 

568 
hence "i\<^isub>k = n" using i\<^isub>k by arith 

569 
thus False using unotc by simp 

570 
qed 

571 
thus ?thesis by(auto simp add:image_def) 

572 
qed 

573 
qed 

574 
next 

575 
show "?r \<subseteq> C" 

576 
proof 

577 
fix u assume "u \<in> ?r" 

578 
then obtain i\<^isub>u where below: "i\<^isub>u < n" and 

579 
or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" 

580 
by(auto simp:image_def) 

581 
from or show "u \<in> C" 

582 
proof 

583 
assume [simp]: "c = h i\<^isub>u \<and> u = h n" 

584 
have "u \<in> A" using card by auto 

585 
moreover have "u \<noteq> c" using new below by auto 

586 
ultimately show "u \<in> C" using A2 by blast 

587 
next 

588 
assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" 

589 
moreover hence "u \<in> A" using card below by auto 

590 
ultimately show "u \<in> C" using A2 by blast 

591 
qed 

592 
qed 

593 
qed 

594 
next 

595 
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd 

596 
by fastsimp 

597 
qed 

598 
ultimately show ?thesis using x x' by(auto simp:AC) 

599 
qed 

600 
qed 

601 
qed 

602 
qed 

603 
qed 

604 

605 
(* The same proof, but using card 

606 
lemma (in ACf) foldSet_determ_aux: 

607 
"!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> 

608 
\<Longrightarrow> x' = x" 

609 
proof (induct n) 

610 
case 0 thus ?case by simp 

611 
next 

612 
case (Suc n) 

613 
have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> 

614 
\<Longrightarrow> x' = x" and card: "card A < Suc n" 

615 
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . 

616 
from card have "card A < n \<or> card A = n" by arith 

617 
thus ?case 

618 
proof 

619 
assume less: "card A < n" 

620 
show ?thesis by(rule IH[OF less Afoldx Afoldy]) 

621 
next 

622 
assume cardA: "card A = n" 

623 
show ?thesis 

624 
proof (rule foldSet.cases[OF Afoldx]) 

625 
assume "(A, x) = ({}, e)" 

626 
thus "x' = x" using Afoldy by (auto) 

627 
next 

628 
fix B b y 

629 
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" 

630 
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" 

631 
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto 

632 
show ?thesis 

633 
proof (rule foldSet.cases[OF Afoldy]) 

634 
assume "(A,x') = ({}, e)" 

635 
thus ?thesis using A1 by auto 

636 
next 

637 
fix C c z 

638 
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" 

639 
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" 

640 
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto 

641 
have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx]) 

642 
with cardA A1 notinB have less: "card B < n" by simp 

643 
show ?thesis 

644 
proof cases 

645 
assume "b = c" 

646 
then moreover have "B = C" using A1 A2 notinB notinC by auto 

647 
ultimately show ?thesis using IH[OF less] y z x x' by auto 

648 
next 

649 
assume diff: "b \<noteq> c" 

650 
let ?D = "B  {c}" 

651 
have B: "B = insert c ?D" and C: "C = insert b ?D" 

652 
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ 

653 
have "finite ?D" using finA A1 by simp 

654 
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" 

655 
using finite_imp_foldSet by rules 

656 
moreover have cinB: "c \<in> B" using B by(auto) 

657 
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" 

658 
by(rule Diff1_foldSet) 

659 
hence "g c \<cdot> d = y" by(rule IH[OF less y]) 

660 
moreover have "g b \<cdot> d = z" 

661 
proof (rule IH[OF _ z]) 

662 
show "card C < n" using C cardA A1 notinB finA cinB 

663 
by(auto simp:card_Diff1_less) 

664 
next 

665 
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd 

666 
by fastsimp 

667 
qed 

668 
ultimately show ?thesis using x x' by(auto simp:AC) 

669 
qed 

670 
qed 

671 
qed 

672 
qed 

673 
qed 

674 
*) 

675 

676 
lemma (in ACf) foldSet_determ: 

677 
"(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x" 

678 
apply(frule foldSet_imp_finite) 

679 
apply(simp add:finite_conv_nat_seg_image) 

680 
apply(blast intro: foldSet_determ_aux [rule_format]) 

681 
done 

682 

683 
lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y" 

684 
by (unfold fold_def) (blast intro: foldSet_determ) 

685 

686 
text{* The base case for @{text fold}: *} 

687 

688 
lemma fold_empty [simp]: "fold f g e {} = e" 

689 
by (unfold fold_def) blast 

690 

691 
lemma (in ACf) fold_insert_aux: "x \<notin> A ==> 

692 
((insert x A, v) : foldSet f g e) = 

693 
(EX y. (A, y) : foldSet f g e & v = f (g x) y)" 

694 
apply auto 

695 
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) 

696 
apply (fastsimp dest: foldSet_imp_finite) 

697 
apply (blast intro: foldSet_determ) 

698 
done 

699 

700 
text{* The recursion equation for @{text fold}: *} 

701 

702 
lemma (in ACf) fold_insert[simp]: 

703 
"finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)" 

704 
apply (unfold fold_def) 

705 
apply (simp add: fold_insert_aux) 

706 
apply (rule the_equality) 

707 
apply (auto intro: finite_imp_foldSet 

708 
cong add: conj_cong simp add: fold_def [symmetric] fold_equality) 

709 
done 

710 

711 
text{* Its definitional form: *} 

712 

713 
corollary (in ACf) fold_insert_def: 

714 
"\<lbrakk> F \<equiv> fold f g e; finite A; x \<notin> A \<rbrakk> \<Longrightarrow> F (insert x A) = f (g x) (F A)" 

715 
by(simp) 

716 

717 
declare 

718 
empty_foldSetE [rule del] foldSet.intros [rule del] 

719 
 {* Delete rules to do with @{text foldSet} relation. *} 

720 

721 
subsubsection{*Lemmas about @{text fold}*} 

722 

723 
lemma (in ACf) fold_commute: 

724 
"finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)" 

725 
apply (induct set: Finites, simp) 

726 
apply (simp add: left_commute) 

727 
done 

728 

729 
lemma (in ACf) fold_nest_Un_Int: 

730 
"finite A ==> finite B 

731 
==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)" 

732 
apply (induct set: Finites, simp) 

733 
apply (simp add: fold_commute Int_insert_left insert_absorb) 

734 
done 

735 

736 
lemma (in ACf) fold_nest_Un_disjoint: 

737 
"finite A ==> finite B ==> A Int B = {} 

738 
==> fold f g e (A Un B) = fold f g (fold f g e B) A" 

739 
by (simp add: fold_nest_Un_Int) 

740 

741 
lemma (in ACf) fold_reindex: 

742 
assumes fin: "finite B" 

743 
shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B" 

744 
using fin apply (induct) 

745 
apply simp 

746 
apply simp 

747 
done 

748 

749 
lemma (in ACe) fold_Un_Int: 

750 
"finite A ==> finite B ==> 

751 
fold f g e A \<cdot> fold f g e B = 

752 
fold f g e (A Un B) \<cdot> fold f g e (A Int B)" 

753 
apply (induct set: Finites, simp) 

754 
apply (simp add: AC insert_absorb Int_insert_left) 

755 
done 

756 

757 
corollary (in ACe) fold_Un_disjoint: 

758 
"finite A ==> finite B ==> A Int B = {} ==> 

759 
fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B" 

760 
by (simp add: fold_Un_Int) 

761 

762 
lemma (in ACe) fold_UN_disjoint: 

763 
"\<lbrakk> finite I; ALL i:I. finite (A i); 

764 
ALL i:I. ALL j:I. i \<noteq> j > A i Int A j = {} \<rbrakk> 

765 
\<Longrightarrow> fold f g e (UNION I A) = 

766 
fold f (%i. fold f g e (A i)) e I" 

767 
apply (induct set: Finites, simp, atomize) 

768 
apply (subgoal_tac "ALL i:F. x \<noteq> i") 

769 
prefer 2 apply blast 

770 
apply (subgoal_tac "A x Int UNION F A = {}") 

771 
prefer 2 apply blast 

772 
apply (simp add: fold_Un_disjoint) 

773 
done 

774 

775 
lemma (in ACf) fold_cong: 

776 
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A" 

777 
apply (subgoal_tac "ALL C. C <= A > (ALL x:C. g x = h x) > fold f g a C = fold f h a C") 

778 
apply simp 

779 
apply (erule finite_induct, simp) 

780 
apply (simp add: subset_insert_iff, clarify) 

781 
apply (subgoal_tac "finite C") 

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

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

784 
prefer 2 apply blast 

785 
apply (erule ssubst) 

786 
apply (drule spec) 

787 
apply (erule (1) notE impE) 

788 
apply (simp add: Ball_def del: insert_Diff_single) 

789 
done 

790 

791 
lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==> 

792 
fold f (%x. fold f (g x) e (B x)) e A = 

793 
fold f (split g) e (SIGMA x:A. B x)" 

794 
apply (subst Sigma_def) 

795 
apply (subst fold_UN_disjoint) 

796 
apply assumption 

797 
apply simp 

798 
apply blast 

799 
apply (erule fold_cong) 

800 
apply (subst fold_UN_disjoint) 

801 
apply simp 

802 
apply simp 

803 
apply blast 

804 
apply (simp) 

805 
done 

806 

807 
lemma (in ACe) fold_distrib: "finite A \<Longrightarrow> 

808 
fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)" 

809 
apply (erule finite_induct) 

810 
apply simp 

811 
apply (simp add:AC) 

812 
done 

813 

814 

12396  815 
subsection {* Finite cardinality *} 
816 

817 
text {* 

818 
This definition, although traditional, is ugly to work with: @{text 

819 
"card A == LEAST n. EX f. A = {f i  i. i < n}"}. Therefore we have 

820 
switched to an inductive one: 

821 
*} 

822 

823 
consts cardR :: "('a set \<times> nat) set" 

824 

825 
inductive cardR 

826 
intros 

827 
EmptyI: "({}, 0) : cardR" 

828 
InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR" 

829 

830 
constdefs 

831 
card :: "'a set => nat" 

832 
"card A == THE n. (A, n) : cardR" 

833 

834 
inductive_cases cardR_emptyE: "({}, n) : cardR" 

835 
inductive_cases cardR_insertE: "(insert a A,n) : cardR" 

836 

837 
lemma cardR_SucD: "(A, n) : cardR ==> a : A > (EX m. n = Suc m)" 

838 
by (induct set: cardR) simp_all 

839 

840 
lemma cardR_determ_aux1: 

841 
"(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A  {a}, n) : cardR)" 

14208  842 
apply (induct set: cardR, auto) 
843 
apply (simp add: insert_Diff_if, auto) 

12396  844 
apply (drule cardR_SucD) 
845 
apply (blast intro!: cardR.intros) 

846 
done 

847 

848 
lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR" 

849 
by (drule cardR_determ_aux1) auto 

850 

851 
lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)" 

852 
apply (induct set: cardR) 

853 
apply (safe elim!: cardR_emptyE cardR_insertE) 

854 
apply (rename_tac B b m) 

855 
apply (case_tac "a = b") 

856 
apply (subgoal_tac "A = B") 

14208  857 
prefer 2 apply (blast elim: equalityE, blast) 
12396  858 
apply (subgoal_tac "EX C. A = insert b C & B = insert a C") 
859 
prefer 2 

860 
apply (rule_tac x = "A Int B" in exI) 

861 
apply (blast elim: equalityE) 

862 
apply (frule_tac A = B in cardR_SucD) 

863 
apply (blast intro!: cardR.intros dest!: cardR_determ_aux2) 

864 
done 

865 

866 
lemma cardR_imp_finite: "(A, n) : cardR ==> finite A" 

867 
by (induct set: cardR) simp_all 

868 

869 
lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR" 

870 
by (induct set: Finites) (auto intro!: cardR.intros) 

871 

872 
lemma card_equality: "(A,n) : cardR ==> card A = n" 

873 
by (unfold card_def) (blast intro: cardR_determ) 

874 

875 
lemma card_empty [simp]: "card {} = 0" 

876 
by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE) 

877 

878 
lemma card_insert_disjoint [simp]: 

879 
"finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" 

880 
proof  

881 
assume x: "x \<notin> A" 

882 
hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)" 

883 
apply (auto intro!: cardR.intros) 

884 
apply (rule_tac A1 = A in finite_imp_cardR [THEN exE]) 

885 
apply (force dest: cardR_imp_finite) 

886 
apply (blast intro!: cardR.intros intro: cardR_determ) 

887 
done 

888 
assume "finite A" 

889 
thus ?thesis 

890 
apply (simp add: card_def aux) 

891 
apply (rule the_equality) 

892 
apply (auto intro: finite_imp_cardR 

893 
cong: conj_cong simp: card_def [symmetric] card_equality) 

894 
done 

895 
qed 

896 

897 
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" 

898 
apply auto 

14208  899 
apply (drule_tac a = x in mk_disjoint_insert, clarify) 
900 
apply (rotate_tac 1, auto) 

12396  901 
done 
902 

903 
lemma card_insert_if: 

904 
"finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" 

905 
by (simp add: insert_absorb) 

906 

907 
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A  {x})) = card A" 

14302  908 
apply(rule_tac t = A in insert_Diff [THEN subst], assumption) 
909 
apply(simp del:insert_Diff_single) 

910 
done 

12396  911 

912 
lemma card_Diff_singleton: 

913 
"finite A ==> x: A ==> card (A  {x}) = card A  1" 

914 
by (simp add: card_Suc_Diff1 [symmetric]) 

915 

916 
lemma card_Diff_singleton_if: 

917 
"finite A ==> card (A{x}) = (if x : A then card A  1 else card A)" 

918 
by (simp add: card_Diff_singleton) 

919 

920 
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A  {x}))" 

921 
by (simp add: card_insert_if card_Suc_Diff1) 

922 

923 
lemma card_insert_le: "finite A ==> card A <= card (insert x A)" 

924 
by (simp add: card_insert_if) 

925 

926 
lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" 

14208  927 
apply (induct set: Finites, simp, clarify) 
12396  928 
apply (subgoal_tac "finite A & A  {x} <= F") 
14208  929 
prefer 2 apply (blast intro: finite_subset, atomize) 
12396  930 
apply (drule_tac x = "A  {x}" in spec) 
931 
apply (simp add: card_Diff_singleton_if split add: split_if_asm) 

14208  932 
apply (case_tac "card A", auto) 
12396  933 
done 
934 

935 
lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" 

936 
apply (simp add: psubset_def linorder_not_le [symmetric]) 

937 
apply (blast dest: card_seteq) 

938 
done 

939 

940 
lemma card_mono: "finite B ==> A <= B ==> card A <= card B" 

14208  941 
apply (case_tac "A = B", simp) 
12396  942 
apply (simp add: linorder_not_less [symmetric]) 
943 
apply (blast dest: card_seteq intro: order_less_imp_le) 

944 
done 

945 

946 
lemma card_Un_Int: "finite A ==> finite B 

947 
==> card A + card B = card (A Un B) + card (A Int B)" 

14208  948 
apply (induct set: Finites, simp) 
12396  949 
apply (simp add: insert_absorb Int_insert_left) 
950 
done 

951 

952 
lemma card_Un_disjoint: "finite A ==> finite B 

953 
==> A Int B = {} ==> card (A Un B) = card A + card B" 

954 
by (simp add: card_Un_Int) 

955 

956 
lemma card_Diff_subset: 

957 
"finite A ==> B <= A ==> card A  card B = card (A  B)" 

958 
apply (subgoal_tac "(A  B) Un B = A") 

959 
prefer 2 apply blast 

14331  960 
apply (rule nat_add_right_cancel [THEN iffD1]) 
12396  961 
apply (rule card_Un_disjoint [THEN subst]) 
962 
apply (erule_tac [4] ssubst) 

963 
prefer 3 apply blast 

964 
apply (simp_all add: add_commute not_less_iff_le 

965 
add_diff_inverse card_mono finite_subset) 

966 
done 

967 

968 
lemma card_Diff1_less: "finite A ==> x: A ==> card (A  {x}) < card A" 

969 
apply (rule Suc_less_SucD) 

970 
apply (simp add: card_Suc_Diff1) 

971 
done 

972 

973 
lemma card_Diff2_less: 

974 
"finite A ==> x: A ==> y: A ==> card (A  {x}  {y}) < card A" 

975 
apply (case_tac "x = y") 

976 
apply (simp add: card_Diff1_less) 

977 
apply (rule less_trans) 

978 
prefer 2 apply (auto intro!: card_Diff1_less) 

979 
done 

980 

981 
lemma card_Diff1_le: "finite A ==> card (A  {x}) <= card A" 

982 
apply (case_tac "x : A") 

983 
apply (simp_all add: card_Diff1_less less_imp_le) 

984 
done 

985 

986 
lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" 

14208  987 
by (erule psubsetI, blast) 
12396  988 

14889  989 
lemma insert_partition: 
990 
"[ x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 > c1 \<inter> c2 = {}] 

991 
==> x \<inter> \<Union> F = {}" 

992 
by auto 

993 

994 
(* main cardinality theorem *) 

995 
lemma card_partition [rule_format]: 

996 
"finite C ==> 

997 
finite (\<Union> C) > 

998 
(\<forall>c\<in>C. card c = k) > 

999 
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 > c1 \<inter> c2 = {}) > 

1000 
k * card(C) = card (\<Union> C)" 

1001 
apply (erule finite_induct, simp) 

1002 
apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 

1003 
finite_subset [of _ "\<Union> (insert x F)"]) 

1004 
done 

1005 

12396  1006 

1007 
subsubsection {* Cardinality of image *} 

1008 

1009 
lemma card_image_le: "finite A ==> card (f ` A) <= card A" 

14208  1010 
apply (induct set: Finites, simp) 
12396  1011 
apply (simp add: le_SucI finite_imageI card_insert_if) 
1012 
done 

1013 

1014 
lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A" 

15111  1015 
by (induct set: Finites, simp_all) 
12396  1016 

1017 
lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A" 

1018 
by (simp add: card_seteq card_image) 

1019 

15111  1020 
lemma eq_card_imp_inj_on: 
1021 
"[ finite A; card(f ` A) = card A ] ==> inj_on f A" 

1022 
apply(induct rule:finite_induct) 

1023 
apply simp 

1024 
apply(frule card_image_le[where f = f]) 

1025 
apply(simp add:card_insert_if split:if_splits) 

1026 
done 

1027 

1028 
lemma inj_on_iff_eq_card: 

1029 
"finite A ==> inj_on f A = (card(f ` A) = card A)" 

1030 
by(blast intro: card_image eq_card_imp_inj_on) 

1031 

12396  1032 

1033 
subsubsection {* Cardinality of the Powerset *} 

1034 

1035 
lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) 

1036 
apply (induct set: Finites) 

1037 
apply (simp_all add: Pow_insert) 

14208  1038 
apply (subst card_Un_disjoint, blast) 
1039 
apply (blast intro: finite_imageI, blast) 

12396  1040 
apply (subgoal_tac "inj_on (insert x) (Pow F)") 
1041 
apply (simp add: card_image Pow_insert) 

1042 
apply (unfold inj_on_def) 

1043 
apply (blast elim!: equalityE) 

1044 
done 

1045 

15392  1046 
text {* Relates to equivalence classes. Based on a theorem of 
1047 
F. Kammüller's. *} 

12396  1048 

1049 
lemma dvd_partition: 

15392  1050 
"finite (Union C) ==> 
12396  1051 
ALL c : C. k dvd card c ==> 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset

1052 
(ALL c1: C. ALL c2: C. c1 \<noteq> c2 > c1 Int c2 = {}) ==> 
12396  1053 
k dvd card (Union C)" 
15392  1054 
apply(frule finite_UnionD) 
1055 
apply(rotate_tac 1) 

14208  1056 
apply (induct set: Finites, simp_all, clarify) 
12396  1057 
apply (subst card_Un_disjoint) 
1058 
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) 

1059 
done 

1060 

1061 

15392  1062 
subsubsection {* Theorems about @{text "choose"} *} 
12396  1063 

1064 
text {* 

15392  1065 
\medskip Basic theorem about @{text "choose"}. By Florian 
1066 
Kamm\"uller, tidied by LCP. 

12396  1067 
*} 
1068 

15392  1069 
lemma card_s_0_eq_empty: 
1070 
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1" 

1071 
apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) 

1072 
apply (simp cong add: rev_conj_cong) 

1073 
done 

12396  1074 

15392  1075 
lemma choose_deconstruct: "finite M ==> x \<notin> M 
1076 
==> {s. s <= insert x M & card(s) = Suc k} 

1077 
= {s. s <= M & card(s) = Suc k} Un 

1078 
{s. EX t. t <= M & card(t) = k & s = insert x t}" 

1079 
apply safe 

1080 
apply (auto intro: finite_subset [THEN card_insert_disjoint]) 

1081 
apply (drule_tac x = "xa  {x}" in spec) 

1082 
apply (subgoal_tac "x \<notin> xa", auto) 

1083 
apply (erule rev_mp, subst card_Diff_singleton) 

1084 
apply (auto intro: finite_subset) 

12396  1085 
done 
1086 

15392  1087 
lemma card_inj_on_le: 
1088 
"[inj_on f A; f ` A \<subseteq> B; finite B ] ==> card A \<le> card B" 

1089 
apply (subgoal_tac "finite A") 

1090 
apply (force intro: card_mono simp add: card_image [symmetric]) 

1091 
apply (blast intro: finite_imageD dest: finite_subset) 

1092 
done 

12396  1093 

15392  1094 
lemma card_bij_eq: 
1095 
"[inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 

1096 
finite A; finite B ] ==> card A = card B" 

1097 
by (auto intro: le_anti_sym card_inj_on_le) 

12396  1098 

15392  1099 
text{*There are as many subsets of @{term A} having cardinality @{term k} 
1100 
as there are sets obtained from the former by inserting a fixed element 

1101 
@{term x} into each.*} 

1102 
lemma constr_bij: 

1103 
"[finite A; x \<notin> A] ==> 

1104 
card {B. EX C. C <= A & card(C) = k & B = insert x C} = 

1105 
card {B. B <= A & card(B) = k}" 

1106 
apply (rule_tac f = "%s. s  {x}" and g = "insert x" in card_bij_eq) 

1107 
apply (auto elim!: equalityE simp add: inj_on_def) 

1108 
apply (subst Diff_insert0, auto) 

1109 
txt {* finiteness of the two sets *} 

1110 
apply (rule_tac [2] B = "Pow (A)" in finite_subset) 

1111 
apply (rule_tac B = "Pow (insert x A)" in finite_subset) 

1112 
apply fast+ 

12396  1113 
done 
1114 

15392  1115 
text {* 
1116 
Main theorem: combinatorial statement about number of subsets of a set. 

1117 
*} 

12396  1118 

15392  1119 
lemma n_sub_lemma: 
1120 
"!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" 

1121 
apply (induct k) 

1122 
apply (simp add: card_s_0_eq_empty, atomize) 

1123 
apply (rotate_tac 1, erule finite_induct) 

1124 
apply (simp_all (no_asm_simp) cong add: conj_cong 

1125 
add: card_s_0_eq_empty choose_deconstruct) 

1126 
apply (subst card_Un_disjoint) 

1127 
prefer 4 apply (force simp add: constr_bij) 

1128 
prefer 3 apply force 

1129 
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] 

1130 
finite_subset [of _ "Pow (insert x F)", standard]) 

1131 
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) 

12396  1132 
done 
1133 

15392  1134 
theorem n_subsets: 
1135 
"finite A ==> card {B. B <= A & card B = k} = (card A choose k)" 

1136 
by (simp add: n_sub_lemma) 

1137 

1138 

1139 
subsection{* A fold functional for nonempty sets *} 

1140 

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

12396  1142 

15392  1143 
consts 
1144 
foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set" 

1145 

1146 
inductive "foldSet1 f" 

1147 
intros 

1148 
foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f" 

1149 
foldSet1_insertI [intro]: 

1150 
"\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk> 

1151 
\<Longrightarrow> (insert a A, f a x) : foldSet1 f" 

12396  1152 

15392  1153 
constdefs 
1154 
fold1 :: "('a => 'a => 'a) => 'a set => 'a" 

1155 
"fold1 f A == THE x. (A, x) : foldSet1 f" 

1156 

1157 
lemma foldSet1_nonempty: 

1158 
"(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}" 

1159 
by(erule foldSet1.cases, simp_all) 

1160 

12396  1161 

15392  1162 
inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f" 
1163 

1164 
lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)" 

1165 
apply(rule iffI) 

1166 
prefer 2 apply fast 

1167 
apply (erule foldSet1.cases) 

1168 
apply blast 

1169 
apply (erule foldSet1.cases) 

1170 
apply blast 

1171 
apply blast 

15376  1172 
done 
12396  1173 

15392  1174 
lemma Diff1_foldSet1: 
1175 
"(A  {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f" 

1176 
by (erule insert_Diff [THEN subst], rule foldSet1.intros, 

1177 
auto dest!:foldSet1_nonempty) 

12396  1178 

15392  1179 
lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A" 
1180 
by (induct set: foldSet1) auto 

12396  1181 

15392  1182 
lemma finite_nonempty_imp_foldSet1: 
1183 
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f" 

1184 
by (induct set: Finites) auto 

15376  1185 

15392  1186 
lemma (in ACf) foldSet1_determ_aux: 
1187 
"!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x" 

1188 
proof (induct n) 

1189 
case 0 thus ?case by simp 

1190 
next 

1191 
case (Suc n) 

1192 
have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk> 

1193 
\<Longrightarrow> y = x" and card: "card A < Suc n" 

1194 
and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" . 

1195 
from card have "card A < n \<or> card A = n" by arith 

1196 
thus ?case 

1197 
proof 

1198 
assume less: "card A < n" 

1199 
show ?thesis by(rule IH[OF less Afoldx Afoldy]) 

1200 
next 

1201 
assume cardA: "card A = n" 

1202 
show ?thesis 

1203 
proof (rule foldSet1.cases[OF Afoldx]) 

1204 
fix a assume "(A, x) = ({a}, a)" 

1205 
thus "y = x" using Afoldy by (simp add:foldSet1_sing) 

1206 
next 

1207 
fix Ax ax x' 

1208 
assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')" 

1209 
and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax" 

1210 
and Axnon: "Ax \<noteq> {}" 

1211 
hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto 

1212 
show ?thesis 

1213 
proof (rule foldSet1.cases[OF Afoldy]) 

1214 
fix ay assume "(A, y) = ({ay}, ay)" 

1215 
thus ?thesis using eq1 x' Axnon notinx 

1216 
by (fastsimp simp:foldSet1_sing) 

1217 
next 

1218 
fix Ay ay y' 

1219 
assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')" 

1220 
and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay" 

1221 
and Aynon: "Ay \<noteq> {}" 

1222 
hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto 

1223 
have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx]) 

1224 
with cardA A1 notinx have less: "card Ax < n" by simp 

1225 
show ?thesis 

1226 
proof cases 

1227 
assume "ax = ay" 

1228 
then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto 

1229 
ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto 

1230 
next 

1231 
assume diff: "ax \<noteq> ay" 

1232 
let ?B = "Ax  {ay}" 

1233 
have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B" 

1234 
using A1 A2 notinx notiny diff by(blast elim!:equalityE)+ 

1235 
show ?thesis 

1236 
proof cases 

1237 
assume "?B = {}" 

1238 
with Ax Ay show ?thesis using x' y' x y by(simp add:commute) 

1239 
next 

1240 
assume Bnon: "?B \<noteq> {}" 

1241 
moreover have "finite ?B" using finA A1 by simp 

1242 
ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f" 

1243 
using finite_nonempty_imp_foldSet1 by(blast) 

1244 
moreover have ayinAx: "ay \<in> Ax" using Ax by(auto) 

1245 
ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1) 

1246 
hence "ay\<cdot>b = x'" by(rule IH[OF less x']) 

1247 
moreover have "ax\<cdot>b = y'" 

1248 
proof (rule IH[OF _ y']) 

1249 
show "card Ay < n" using Ay cardA A1 notinx finA ayinAx 

1250 
by(auto simp:card_Diff1_less) 

1251 
next 

1252 
show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon 

1253 
by fastsimp 

1254 
qed 

1255 
ultimately show ?thesis using x y by(auto simp:AC) 

1256 
qed 

1257 
qed 

1258 
qed 

1259 
qed 

1260 
qed 

12396  1261 
qed 
1262 

15392  1263 

1264 
lemma (in ACf) foldSet1_determ: 

1265 
"(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x" 

1266 
by (blast intro: foldSet1_determ_aux [rule_format]) 

1267 

1268 
lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y" 

1269 
by (unfold fold1_def) (blast intro: foldSet1_determ) 

1270 

1271 
lemma fold1_singleton: "fold1 f {a} = a" 

1272 
by (unfold fold1_def) blast 

12396  1273 

15392  1274 
lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> 
1275 
((insert x A, v) : foldSet1 f) = 

1276 
(EX y. (A, y) : foldSet1 f & v = f x y)" 

1277 
apply auto 

1278 
apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE]) 

1279 
apply (fastsimp dest: foldSet1_imp_finite) 

1280 
apply blast 

1281 
apply (blast intro: foldSet1_determ) 

1282 
done 

15376  1283 

15392  1284 
lemma (in ACf) fold1_insert: 
1285 
"finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)" 

1286 
apply (unfold fold1_def) 

1287 
apply (simp add: foldSet1_insert_aux) 

1288 
apply (rule the_equality) 

1289 
apply (auto intro: finite_nonempty_imp_foldSet1 

1290 
cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality) 

1291 
done 

15376  1292 

15392  1293 
locale ACIf = ACf + 
1294 
assumes idem: "x \<cdot> x = x" 

12396  1295 

15392  1296 
lemma (in ACIf) fold1_insert2: 
1297 
assumes finA: "finite A" and nonA: "A \<noteq> {}" 

1298 
shows "fold1 f (insert a A) = f a (fold1 f A)" 

1299 
proof cases 

1300 
assume "a \<in> A" 

1301 
then obtain B where A: "A = insert a B" and disj: "a \<notin> B" 

1302 
by(blast dest: mk_disjoint_insert) 

1303 
show ?thesis 

1304 
proof cases 

1305 
assume "B = {}" 

1306 
thus ?thesis using A by(simp add:idem fold1_singleton) 

1307 
next 

1308 
assume nonB: "B \<noteq> {}" 

1309 
from finA A have finB: "finite B" by(blast intro: finite_subset) 

1310 
have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp 

1311 
also have "\<dots> = f a (fold1 f B)" 

1312 
using finB nonB disj by(simp add: fold1_insert) 

1313 
also have "\<dots> = f a (fold1 f A)" 

1314 
using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric]) 

1315 
finally show ?thesis . 

1316 
qed 

1317 
next 

1318 
assume "a \<notin> A" 

1319 
with finA nonA show ?thesis by(simp add:fold1_insert) 

1320 
qed 

1321 

15376  1322 

15392  1323 
text{* Now the recursion rules for definitions: *} 
1324 

1325 
lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a" 

1326 
by(simp add:fold1_singleton) 

1327 

1328 
lemma (in ACf) fold1_insert_def: 

1329 
"\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" 

1330 
by(simp add:fold1_insert) 

1331 

1332 
lemma (in ACIf) fold1_insert2_def: 

1333 
"\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" 

1334 
by(simp add:fold1_insert2) 

1335 

15376  1336 

15392  1337 
subsection{*Min and Max*} 
1338 

1339 
text{* As an application of @{text fold1} we define the minimal and 

1340 
maximal element of a (nonempty) set over a linear order. First we 

1341 
show that @{text min} and @{text max} are ACI: *} 

1342 

1343 
lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" 

1344 
apply(rule ACf.intro) 

1345 
apply(auto simp:min_def) 

1346 
done 

1347 

1348 
lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" 

1349 
apply(rule ACIf.intro[OF ACf_min]) 

1350 
apply(rule ACIf_axioms.intro) 

1351 
apply(auto simp:min_def) 

15376  1352 
done 
1353 

15392  1354 
lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" 
1355 
apply(rule ACf.intro) 

1356 
apply(auto simp:max_def) 

1357 
done 

1358 

1359 
lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" 

1360 
apply(rule ACIf.intro[OF ACf_max]) 

1361 
apply(rule ACIf_axioms.intro) 

1362 
apply(auto simp:max_def) 

15376  1363 
done 
12396  1364 

15392  1365 
text{* Now we make the definitions: *} 
1366 

1367 
constdefs 

1368 
Min :: "('a::linorder)set => 'a" 

1369 
"Min == fold1 min" 

1370 

1371 
Max :: "('a::linorder)set => 'a" 

1372 
"Max == fold1 max" 

1373 

1374 
text{* Now we instantiate the recursiuon equations and declare them 

1375 
simplification rules: *} 

1376 

1377 
declare 

1378 
fold1_singleton_def[OF Min_def, simp] 
