1 (* Title: HOL/Finite.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson & Tobias Nipkow |
|
4 Copyright 1995 University of Cambridge & TU Muenchen |
|
5 |
|
6 Finite sets and their cardinality. |
|
7 *) |
|
8 |
|
9 section "finite"; |
|
10 |
|
11 (*Discharging ~ x:y entails extra work*) |
|
12 val major::prems = Goal |
|
13 "[| finite F; P({}); \ |
|
14 \ !!F x. [| finite F; x ~: F; P(F) |] ==> P(insert x F) \ |
|
15 \ |] ==> P(F)"; |
|
16 by (rtac (major RS Finites.induct) 1); |
|
17 by (excluded_middle_tac "a:A" 2); |
|
18 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
|
19 by (REPEAT (ares_tac prems 1)); |
|
20 qed "finite_induct"; |
|
21 |
|
22 val major::subs::prems = Goal |
|
23 "[| finite F; F <= A; \ |
|
24 \ P({}); \ |
|
25 \ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \ |
|
26 \ |] ==> P(F)"; |
|
27 by (rtac (subs RS rev_mp) 1); |
|
28 by (rtac (major RS finite_induct) 1); |
|
29 by (ALLGOALS (blast_tac (claset() addIs prems))); |
|
30 qed "finite_subset_induct"; |
|
31 |
|
32 Addsimps Finites.intrs; |
|
33 AddSIs Finites.intrs; |
|
34 |
|
35 (*The union of two finite sets is finite*) |
|
36 Goal "[| finite F; finite G |] ==> finite(F Un G)"; |
|
37 by (etac finite_induct 1); |
|
38 by (ALLGOALS Asm_simp_tac); |
|
39 qed "finite_UnI"; |
|
40 |
|
41 (*Every subset of a finite set is finite*) |
|
42 Goal "finite B ==> ALL A. A<=B --> finite A"; |
|
43 by (etac finite_induct 1); |
|
44 by (ALLGOALS (simp_tac (simpset() addsimps [subset_insert_iff]))); |
|
45 by Safe_tac; |
|
46 by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 1); |
|
47 by (ALLGOALS Blast_tac); |
|
48 val lemma = result(); |
|
49 |
|
50 Goal "[| A<=B; finite B |] ==> finite A"; |
|
51 by (dtac lemma 1); |
|
52 by (Blast_tac 1); |
|
53 qed "finite_subset"; |
|
54 |
|
55 Goal "finite(F Un G) = (finite F & finite G)"; |
|
56 by (blast_tac (claset() |
|
57 addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1); |
|
58 qed "finite_Un"; |
|
59 AddIffs[finite_Un]; |
|
60 |
|
61 (*The converse obviously fails*) |
|
62 Goal "finite F | finite G ==> finite(F Int G)"; |
|
63 by (blast_tac (claset() addIs [finite_subset]) 1); |
|
64 qed "finite_Int"; |
|
65 |
|
66 Addsimps [finite_Int]; |
|
67 AddIs [finite_Int]; |
|
68 |
|
69 Goal "finite(insert a A) = finite A"; |
|
70 by (stac insert_is_Un 1); |
|
71 by (simp_tac (HOL_ss addsimps [finite_Un]) 1); |
|
72 by (Blast_tac 1); |
|
73 qed "finite_insert"; |
|
74 Addsimps[finite_insert]; |
|
75 |
|
76 (*The image of a finite set is finite *) |
|
77 Goal "finite F ==> finite(h`F)"; |
|
78 by (etac finite_induct 1); |
|
79 by (Simp_tac 1); |
|
80 by (Asm_simp_tac 1); |
|
81 qed "finite_imageI"; |
|
82 |
|
83 Goal "finite (range g) ==> finite (range (%x. f (g x)))"; |
|
84 by (Simp_tac 1); |
|
85 by (etac finite_imageI 1); |
|
86 qed "finite_range_imageI"; |
|
87 |
|
88 val major::prems = Goal |
|
89 "[| finite c; finite b; \ |
|
90 \ P(b); \ |
|
91 \ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \ |
|
92 \ |] ==> c<=b --> P(b-c)"; |
|
93 by (rtac (major RS finite_induct) 1); |
|
94 by (stac Diff_insert 2); |
|
95 by (ALLGOALS (asm_simp_tac |
|
96 (simpset() addsimps prems@[Diff_subset RS finite_subset]))); |
|
97 val lemma = result(); |
|
98 |
|
99 val prems = Goal |
|
100 "[| finite A; \ |
|
101 \ P(A); \ |
|
102 \ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \ |
|
103 \ |] ==> P({})"; |
|
104 by (rtac (Diff_cancel RS subst) 1); |
|
105 by (rtac (lemma RS mp) 1); |
|
106 by (REPEAT (ares_tac (subset_refl::prems) 1)); |
|
107 qed "finite_empty_induct"; |
|
108 |
|
109 |
|
110 (* finite B ==> finite (B - Ba) *) |
|
111 bind_thm ("finite_Diff", Diff_subset RS finite_subset); |
|
112 Addsimps [finite_Diff]; |
|
113 |
|
114 Goal "finite(A - insert a B) = finite(A-B)"; |
|
115 by (stac Diff_insert 1); |
|
116 by (case_tac "a : A-B" 1); |
|
117 by (rtac (finite_insert RS sym RS trans) 1); |
|
118 by (stac insert_Diff 1); |
|
119 by (ALLGOALS Asm_full_simp_tac); |
|
120 qed "finite_Diff_insert"; |
|
121 AddIffs [finite_Diff_insert]; |
|
122 |
|
123 (*lemma merely for classical reasoner in the proof below: force_tac can't |
|
124 prove it.*) |
|
125 Goal "finite(A-{}) = finite A"; |
|
126 by (Simp_tac 1); |
|
127 val lemma = result(); |
|
128 |
|
129 (*Lemma for proving finite_imageD*) |
|
130 Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A"; |
|
131 by (etac finite_induct 1); |
|
132 by (ALLGOALS Asm_simp_tac); |
|
133 by (Clarify_tac 1); |
|
134 by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1); |
|
135 by (Clarify_tac 1); |
|
136 by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); |
|
137 by (blast_tac (claset() addSDs [lemma RS iffD1]) 1); |
|
138 by (thin_tac "ALL A. ?PP(A)" 1); |
|
139 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); |
|
140 by (Clarify_tac 1); |
|
141 by (res_inst_tac [("x","xa")] bexI 1); |
|
142 by (ALLGOALS |
|
143 (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); |
|
144 val lemma = result(); |
|
145 |
|
146 Goal "[| finite(f`A); inj_on f A |] ==> finite A"; |
|
147 by (dtac lemma 1); |
|
148 by (Blast_tac 1); |
|
149 qed "finite_imageD"; |
|
150 |
|
151 (** The finite UNION of finite sets **) |
|
152 |
|
153 Goal "finite A ==> (ALL a:A. finite(B a)) --> finite(UN a:A. B a)"; |
|
154 by (etac finite_induct 1); |
|
155 by (ALLGOALS Asm_simp_tac); |
|
156 bind_thm("finite_UN_I", ballI RSN (2, result() RS mp)); |
|
157 |
|
158 (*strengthen RHS to |
|
159 ((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}}) ? |
|
160 we'd need to prove |
|
161 finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}} |
|
162 by induction*) |
|
163 Goal "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"; |
|
164 by (blast_tac (claset() addIs [finite_UN_I, finite_subset]) 1); |
|
165 qed "finite_UN"; |
|
166 Addsimps [finite_UN]; |
|
167 |
|
168 (** Sigma of finite sets **) |
|
169 |
|
170 Goalw [Sigma_def] |
|
171 "[| finite A; ALL a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)"; |
|
172 by (blast_tac (claset() addSIs [finite_UN_I]) 1); |
|
173 bind_thm("finite_SigmaI", ballI RSN (2,result())); |
|
174 Addsimps [finite_SigmaI]; |
|
175 |
|
176 Goal "[| finite (UNIV::'a set); finite (UNIV::'b set)|] ==> finite (UNIV::('a * 'b) set)"; |
|
177 by (subgoal_tac "(UNIV::('a * 'b) set) = Sigma UNIV (%x. UNIV)" 1); |
|
178 by (etac ssubst 1); |
|
179 by (etac finite_SigmaI 1); |
|
180 by Auto_tac; |
|
181 qed "finite_Prod_UNIV"; |
|
182 |
|
183 Goal "finite (UNIV :: ('a::finite * 'b::finite) set)"; |
|
184 by (rtac (finite_Prod_UNIV) 1); |
|
185 by (rtac finite 1); |
|
186 by (rtac finite 1); |
|
187 qed "finite_Prod"; |
|
188 |
|
189 Goal "finite (UNIV :: unit set)"; |
|
190 by (subgoal_tac "UNIV = {()}" 1); |
|
191 by (etac ssubst 1); |
|
192 by Auto_tac; |
|
193 qed "finite_unit"; |
|
194 |
|
195 (** The powerset of a finite set **) |
|
196 |
|
197 Goal "finite(Pow A) ==> finite A"; |
|
198 by (subgoal_tac "finite ((%x.{x})`A)" 1); |
|
199 by (rtac finite_subset 2); |
|
200 by (assume_tac 3); |
|
201 by (ALLGOALS |
|
202 (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); |
|
203 val lemma = result(); |
|
204 |
|
205 Goal "finite(Pow A) = finite A"; |
|
206 by (rtac iffI 1); |
|
207 by (etac lemma 1); |
|
208 (*Opposite inclusion: finite A ==> finite (Pow A) *) |
|
209 by (etac finite_induct 1); |
|
210 by (ALLGOALS |
|
211 (asm_simp_tac |
|
212 (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert]))); |
|
213 qed "finite_Pow_iff"; |
|
214 AddIffs [finite_Pow_iff]; |
|
215 |
|
216 Goal "finite(r^-1) = finite r"; |
|
217 by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1); |
|
218 by (Asm_simp_tac 1); |
|
219 by (rtac iffI 1); |
|
220 by (etac (rewrite_rule [inj_on_def] finite_imageD) 1); |
|
221 by (simp_tac (simpset() addsplits [split_split]) 1); |
|
222 by (etac finite_imageI 1); |
|
223 by (simp_tac (simpset() addsimps [converse_def,image_def]) 1); |
|
224 by Auto_tac; |
|
225 by (rtac bexI 1); |
|
226 by (assume_tac 2); |
|
227 by (Simp_tac 1); |
|
228 qed "finite_converse"; |
|
229 AddIffs [finite_converse]; |
|
230 |
|
231 Goal "finite (lessThan (k::nat))"; |
|
232 by (induct_tac "k" 1); |
|
233 by (simp_tac (simpset() addsimps [lessThan_Suc]) 2); |
|
234 by Auto_tac; |
|
235 qed "finite_lessThan"; |
|
236 |
|
237 Goal "finite (atMost (k::nat))"; |
|
238 by (induct_tac "k" 1); |
|
239 by (simp_tac (simpset() addsimps [atMost_Suc]) 2); |
|
240 by Auto_tac; |
|
241 qed "finite_atMost"; |
|
242 AddIffs [finite_lessThan, finite_atMost]; |
|
243 |
|
244 (* A bounded set of natural numbers is finite *) |
|
245 Goal "(ALL i:N. i<(n::nat)) ==> finite N"; |
|
246 by (rtac finite_subset 1); |
|
247 by (rtac finite_lessThan 2); |
|
248 by Auto_tac; |
|
249 qed "bounded_nat_set_is_finite"; |
|
250 |
|
251 (** Finiteness of transitive closure (thanks to Sidi Ehmety) **) |
|
252 |
|
253 (*A finite relation has a finite field ( = domain U range) *) |
|
254 Goal "finite r ==> finite (Field r)"; |
|
255 by (etac finite_induct 1); |
|
256 by (auto_tac (claset(), |
|
257 simpset() addsimps [Field_def, Domain_insert, Range_insert])); |
|
258 qed "finite_Field"; |
|
259 |
|
260 Goal "r^+ <= Field r <*> Field r"; |
|
261 by (Clarify_tac 1); |
|
262 by (etac trancl_induct 1); |
|
263 by (auto_tac (claset(), simpset() addsimps [Field_def])); |
|
264 qed "trancl_subset_Field2"; |
|
265 |
|
266 Goal "finite (r^+) = finite r"; |
|
267 by Auto_tac; |
|
268 by (rtac (trancl_subset_Field2 RS finite_subset) 2); |
|
269 by (rtac finite_SigmaI 2); |
|
270 by (blast_tac (claset() addIs [r_into_trancl, finite_subset]) 1); |
|
271 by (auto_tac (claset(), simpset() addsimps [finite_Field])); |
|
272 qed "finite_trancl"; |
|
273 |
|
274 |
|
275 section "Finite cardinality -- 'card'"; |
|
276 |
|
277 bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR"); |
|
278 bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR"); |
|
279 |
|
280 AddSEs [cardR_emptyE]; |
|
281 AddSIs cardR.intrs; |
|
282 |
|
283 Goal "[| (A,n) : cardR |] ==> a : A --> (EX m. n = Suc m)"; |
|
284 by (etac cardR.induct 1); |
|
285 by (Blast_tac 1); |
|
286 by (Blast_tac 1); |
|
287 qed "cardR_SucD"; |
|
288 |
|
289 Goal "(A,m): cardR ==> (ALL n a. m = Suc n --> a:A --> (A-{a},n) : cardR)"; |
|
290 by (etac cardR.induct 1); |
|
291 by Auto_tac; |
|
292 by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1); |
|
293 by Auto_tac; |
|
294 by (ftac cardR_SucD 1); |
|
295 by (Blast_tac 1); |
|
296 val lemma = result(); |
|
297 |
|
298 Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR"; |
|
299 by (dtac lemma 1); |
|
300 by (Asm_full_simp_tac 1); |
|
301 val lemma = result(); |
|
302 |
|
303 Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR --> n=m)"; |
|
304 by (etac cardR.induct 1); |
|
305 by (safe_tac (claset() addSEs [cardR_insertE])); |
|
306 by (rename_tac "B b m" 1 THEN case_tac "a = b" 1); |
|
307 by (subgoal_tac "A = B" 1); |
|
308 by (blast_tac (claset() addEs [equalityE]) 2); |
|
309 by (Blast_tac 1); |
|
310 by (subgoal_tac "EX C. A = insert b C & B = insert a C" 1); |
|
311 by (res_inst_tac [("x","A Int B")] exI 2); |
|
312 by (blast_tac (claset() addEs [equalityE]) 2); |
|
313 by (forw_inst_tac [("A","B")] cardR_SucD 1); |
|
314 by (blast_tac (claset() addDs [lemma]) 1); |
|
315 qed_spec_mp "cardR_determ"; |
|
316 |
|
317 Goal "(A,n) : cardR ==> finite(A)"; |
|
318 by (etac cardR.induct 1); |
|
319 by Auto_tac; |
|
320 qed "cardR_imp_finite"; |
|
321 |
|
322 Goal "finite(A) ==> EX n. (A, n) : cardR"; |
|
323 by (etac finite_induct 1); |
|
324 by Auto_tac; |
|
325 qed "finite_imp_cardR"; |
|
326 |
|
327 Goalw [card_def] "(A,n) : cardR ==> card A = n"; |
|
328 by (blast_tac (claset() addIs [cardR_determ]) 1); |
|
329 qed "card_equality"; |
|
330 |
|
331 Goalw [card_def] "card {} = 0"; |
|
332 by (Blast_tac 1); |
|
333 qed "card_empty"; |
|
334 Addsimps [card_empty]; |
|
335 |
|
336 Goal "x ~: A \ |
|
337 \ ==> ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"; |
|
338 by Auto_tac; |
|
339 by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1); |
|
340 by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1); |
|
341 by (blast_tac (claset() addIs [cardR_determ]) 1); |
|
342 val lemma = result(); |
|
343 |
|
344 Goalw [card_def] |
|
345 "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)"; |
|
346 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
|
347 by (rtac the_equality 1); |
|
348 by (auto_tac (claset() addIs [finite_imp_cardR], |
|
349 simpset() addcongs [conj_cong] |
|
350 addsimps [symmetric card_def, |
|
351 card_equality])); |
|
352 qed "card_insert_disjoint"; |
|
353 Addsimps [card_insert_disjoint]; |
|
354 |
|
355 (* Delete rules to do with cardR relation: obsolete *) |
|
356 Delrules [cardR_emptyE]; |
|
357 Delrules cardR.intrs; |
|
358 |
|
359 Goal "finite A ==> (card A = 0) = (A = {})"; |
|
360 by Auto_tac; |
|
361 by (dres_inst_tac [("a","x")] mk_disjoint_insert 1); |
|
362 by (Clarify_tac 1); |
|
363 by (rotate_tac ~1 1); |
|
364 by Auto_tac; |
|
365 qed "card_0_eq"; |
|
366 Addsimps[card_0_eq]; |
|
367 |
|
368 Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))"; |
|
369 by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); |
|
370 qed "card_insert_if"; |
|
371 |
|
372 Goal "[| finite A; x: A |] ==> Suc (card (A-{x})) = card A"; |
|
373 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); |
|
374 by (assume_tac 1); |
|
375 by (Asm_simp_tac 1); |
|
376 qed "card_Suc_Diff1"; |
|
377 |
|
378 Goal "[| finite A; x: A |] ==> card (A-{x}) = card A - 1"; |
|
379 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1 RS sym]) 1); |
|
380 qed "card_Diff_singleton"; |
|
381 |
|
382 Goal "finite A ==> card (A-{x}) = (if x:A then card A - 1 else card A)"; |
|
383 by (asm_simp_tac (simpset() addsimps [card_Diff_singleton]) 1); |
|
384 qed "card_Diff_singleton_if"; |
|
385 |
|
386 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))"; |
|
387 by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1); |
|
388 qed "card_insert"; |
|
389 |
|
390 Goal "finite A ==> card A <= card (insert x A)"; |
|
391 by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1); |
|
392 qed "card_insert_le"; |
|
393 |
|
394 Goal "finite B ==> ALL A. A <= B --> card B <= card A --> A = B"; |
|
395 by (etac finite_induct 1); |
|
396 by (Simp_tac 1); |
|
397 by (Clarify_tac 1); |
|
398 by (subgoal_tac "finite A & A-{x} <= F" 1); |
|
399 by (blast_tac (claset() addIs [finite_subset]) 2); |
|
400 by (dres_inst_tac [("x","A-{x}")] spec 1); |
|
401 by (asm_full_simp_tac (simpset() addsimps [card_Diff_singleton_if] |
|
402 addsplits [split_if_asm]) 1); |
|
403 by (case_tac "card A" 1); |
|
404 by Auto_tac; |
|
405 qed_spec_mp "card_seteq"; |
|
406 |
|
407 Goalw [psubset_def] "[| finite B; A < B |] ==> card A < card B"; |
|
408 by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
409 by (blast_tac (claset() addDs [card_seteq]) 1); |
|
410 qed "psubset_card_mono" ; |
|
411 |
|
412 Goal "[| finite B; A <= B |] ==> card A <= card B"; |
|
413 by (case_tac "A=B" 1); |
|
414 by (Asm_simp_tac 1); |
|
415 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
|
416 by (blast_tac (claset() addDs [card_seteq] addIs [order_less_imp_le]) 1); |
|
417 qed "card_mono" ; |
|
418 |
|
419 Goal "[| finite A; finite B |] \ |
|
420 \ ==> card A + card B = card (A Un B) + card (A Int B)"; |
|
421 by (etac finite_induct 1); |
|
422 by (Simp_tac 1); |
|
423 by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1); |
|
424 qed "card_Un_Int"; |
|
425 |
|
426 Goal "[| finite A; finite B; A Int B = {} |] \ |
|
427 \ ==> card (A Un B) = card A + card B"; |
|
428 by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1); |
|
429 qed "card_Un_disjoint"; |
|
430 |
|
431 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)"; |
|
432 by (subgoal_tac "(A-B) Un B = A" 1); |
|
433 by (Blast_tac 2); |
|
434 by (rtac (add_right_cancel RS iffD1) 1); |
|
435 by (rtac (card_Un_disjoint RS subst) 1); |
|
436 by (etac ssubst 4); |
|
437 by (Blast_tac 3); |
|
438 by (ALLGOALS |
|
439 (asm_simp_tac |
|
440 (simpset() addsimps [add_commute, not_less_iff_le, |
|
441 add_diff_inverse, card_mono, finite_subset]))); |
|
442 qed "card_Diff_subset"; |
|
443 |
|
444 Goal "[| finite A; x: A |] ==> card(A-{x}) < card A"; |
|
445 by (rtac Suc_less_SucD 1); |
|
446 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); |
|
447 qed "card_Diff1_less"; |
|
448 |
|
449 Goal "[| finite A; x: A; y: A |] ==> card(A-{x}-{y}) < card A"; |
|
450 by (case_tac "x=y" 1); |
|
451 by (asm_simp_tac (simpset() addsimps [card_Diff1_less]) 1); |
|
452 by (rtac less_trans 1); |
|
453 by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], simpset()))); |
|
454 qed "card_Diff2_less"; |
|
455 |
|
456 Goal "finite A ==> card(A-{x}) <= card A"; |
|
457 by (case_tac "x: A" 1); |
|
458 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le]))); |
|
459 qed "card_Diff1_le"; |
|
460 |
|
461 Goal "[| finite B; A <= B; card A < card B |] ==> A < B"; |
|
462 by (etac psubsetI 1); |
|
463 by (Blast_tac 1); |
|
464 qed "card_psubset"; |
|
465 |
|
466 (*** Cardinality of image ***) |
|
467 |
|
468 Goal "finite A ==> card (f ` A) <= card A"; |
|
469 by (etac finite_induct 1); |
|
470 by (Simp_tac 1); |
|
471 by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, |
|
472 card_insert_if]) 1); |
|
473 qed "card_image_le"; |
|
474 |
|
475 Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A"; |
|
476 by (etac finite_induct 1); |
|
477 by (ALLGOALS Asm_simp_tac); |
|
478 by Safe_tac; |
|
479 by (rewtac inj_on_def); |
|
480 by (Blast_tac 1); |
|
481 by (stac card_insert_disjoint 1); |
|
482 by (etac finite_imageI 1); |
|
483 by (Blast_tac 1); |
|
484 by (Blast_tac 1); |
|
485 qed_spec_mp "card_image"; |
|
486 |
|
487 Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A"; |
|
488 by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1); |
|
489 qed "endo_inj_surj"; |
|
490 |
|
491 (*** Cardinality of the Powerset ***) |
|
492 |
|
493 Goal "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"; (* FIXME numeral 2 (!?) *) |
|
494 by (etac finite_induct 1); |
|
495 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); |
|
496 by (stac card_Un_disjoint 1); |
|
497 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); |
|
498 by (subgoal_tac "inj_on (insert x) (Pow F)" 1); |
|
499 by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1); |
|
500 by (rewtac inj_on_def); |
|
501 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
502 qed "card_Pow"; |
|
503 |
|
504 |
|
505 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
|
506 The "finite C" premise is redundant*) |
|
507 Goal "finite C ==> finite (Union C) --> \ |
|
508 \ (ALL c : C. k dvd card c) --> \ |
|
509 \ (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
|
510 \ --> k dvd card(Union C)"; |
|
511 by (etac finite_induct 1); |
|
512 by (ALLGOALS Asm_simp_tac); |
|
513 by (Clarify_tac 1); |
|
514 by (stac card_Un_disjoint 1); |
|
515 by (ALLGOALS |
|
516 (asm_full_simp_tac (simpset() |
|
517 addsimps [dvd_add, disjoint_eq_subset_Compl]))); |
|
518 by (thin_tac "ALL c:F. ?PP(c)" 1); |
|
519 by (thin_tac "ALL c:F. ?PP(c) & ?QQ(c)" 1); |
|
520 by (Clarify_tac 1); |
|
521 by (ball_tac 1); |
|
522 by (Blast_tac 1); |
|
523 qed_spec_mp "dvd_partition"; |
|
524 |
|
525 |
|
526 (*** foldSet ***) |
|
527 |
|
528 bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e"); |
|
529 |
|
530 AddSEs [empty_foldSetE]; |
|
531 AddIs foldSet.intrs; |
|
532 |
|
533 Goal "[| (A-{x},y) : foldSet f e; x: A |] ==> (A, f x y) : foldSet f e"; |
|
534 by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1); |
|
535 by Auto_tac; |
|
536 qed "Diff1_foldSet"; |
|
537 |
|
538 Goal "(A, x) : foldSet f e ==> finite(A)"; |
|
539 by (eresolve_tac [foldSet.induct] 1); |
|
540 by Auto_tac; |
|
541 qed "foldSet_imp_finite"; |
|
542 |
|
543 Addsimps [foldSet_imp_finite]; |
|
544 |
|
545 |
|
546 Goal "finite(A) ==> EX x. (A, x) : foldSet f e"; |
|
547 by (etac finite_induct 1); |
|
548 by Auto_tac; |
|
549 qed "finite_imp_foldSet"; |
|
550 |
|
551 |
|
552 Open_locale "LC"; |
|
553 |
|
554 val f_lcomm = thm "lcomm"; |
|
555 |
|
556 |
|
557 Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \ |
|
558 \ (ALL y. (A, y) : foldSet f e --> y=x)"; |
|
559 by (induct_tac "n" 1); |
|
560 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); |
|
561 by (etac foldSet.elim 1); |
|
562 by (Blast_tac 1); |
|
563 by (etac foldSet.elim 1); |
|
564 by (Blast_tac 1); |
|
565 by (Clarify_tac 1); |
|
566 (*force simplification of "card A < card (insert ...)"*) |
|
567 by (etac rev_mp 1); |
|
568 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1); |
|
569 by (rtac impI 1); |
|
570 (** LEVEL 10 **) |
|
571 by (rename_tac "Aa xa ya Ab xb yb" 1 THEN case_tac "xa=xb" 1); |
|
572 by (subgoal_tac "Aa = Ab" 1); |
|
573 by (blast_tac (claset() addSEs [equalityE]) 2); |
|
574 by (Blast_tac 1); |
|
575 (*case xa ~= xb*) |
|
576 by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1); |
|
577 by (blast_tac (claset() addSEs [equalityE]) 2); |
|
578 by (Clarify_tac 1); |
|
579 by (subgoal_tac "Aa = insert xb Ab - {xa}" 1); |
|
580 by (Blast_tac 2); |
|
581 (** LEVEL 20 **) |
|
582 by (subgoal_tac "card Aa <= card Ab" 1); |
|
583 by (rtac (Suc_le_mono RS subst) 2); |
|
584 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2); |
|
585 by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] |
|
586 (finite_imp_foldSet RS exE) 1); |
|
587 by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1); |
|
588 by (ftac Diff1_foldSet 1 THEN assume_tac 1); |
|
589 by (subgoal_tac "ya = f xb x" 1); |
|
590 by (blast_tac (claset() delrules [equalityCE]) 2); |
|
591 by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1); |
|
592 by (Asm_full_simp_tac 2); |
|
593 by (subgoal_tac "yb = f xa x" 1); |
|
594 by (blast_tac (claset() delrules [equalityCE] |
|
595 addDs [Diff1_foldSet]) 2); |
|
596 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); |
|
597 val lemma = result(); |
|
598 |
|
599 |
|
600 Goal "[| (A, x) : foldSet f e; (A, y) : foldSet f e |] ==> y=x"; |
|
601 by (blast_tac (claset() addIs [ObjectLogic.rulify lemma]) 1); |
|
602 qed "foldSet_determ"; |
|
603 |
|
604 Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y"; |
|
605 by (blast_tac (claset() addIs [foldSet_determ]) 1); |
|
606 qed "fold_equality"; |
|
607 |
|
608 Goalw [fold_def] "fold f e {} = e"; |
|
609 by (Blast_tac 1); |
|
610 qed "fold_empty"; |
|
611 Addsimps [fold_empty]; |
|
612 |
|
613 |
|
614 Goal "x ~: A ==> \ |
|
615 \ ((insert x A, v) : foldSet f e) = \ |
|
616 \ (EX y. (A, y) : foldSet f e & v = f x y)"; |
|
617 by Auto_tac; |
|
618 by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1); |
|
619 by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1); |
|
620 by (blast_tac (claset() addIs [foldSet_determ]) 1); |
|
621 val lemma = result(); |
|
622 |
|
623 Goalw [fold_def] |
|
624 "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)"; |
|
625 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
|
626 by (rtac the_equality 1); |
|
627 by (auto_tac (claset() addIs [finite_imp_foldSet], |
|
628 simpset() addcongs [conj_cong] |
|
629 addsimps [symmetric fold_def, |
|
630 fold_equality])); |
|
631 qed "fold_insert"; |
|
632 |
|
633 Goal "finite A ==> ALL e. f x (fold f e A) = fold f (f x e) A"; |
|
634 by (etac finite_induct 1); |
|
635 by (Simp_tac 1); |
|
636 by (asm_simp_tac (simpset() addsimps [f_lcomm, fold_insert]) 1); |
|
637 qed_spec_mp "fold_commute"; |
|
638 |
|
639 Goal "[| finite A; finite B |] \ |
|
640 \ ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"; |
|
641 by (etac finite_induct 1); |
|
642 by (Simp_tac 1); |
|
643 by (asm_simp_tac (simpset() addsimps [fold_insert, fold_commute, |
|
644 Int_insert_left, insert_absorb]) 1); |
|
645 qed "fold_nest_Un_Int"; |
|
646 |
|
647 Goal "[| finite A; finite B; A Int B = {} |] \ |
|
648 \ ==> fold f e (A Un B) = fold f (fold f e B) A"; |
|
649 by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1); |
|
650 qed "fold_nest_Un_disjoint"; |
|
651 |
|
652 (* Delete rules to do with foldSet relation: obsolete *) |
|
653 Delsimps [foldSet_imp_finite]; |
|
654 Delrules [empty_foldSetE]; |
|
655 Delrules foldSet.intrs; |
|
656 |
|
657 Close_locale "LC"; |
|
658 |
|
659 Open_locale "ACe"; |
|
660 |
|
661 (*We enter a more restrictive framework, with f :: ['a,'a] => 'a |
|
662 instead of ['b,'a] => 'a |
|
663 At present, none of these results are used!*) |
|
664 |
|
665 val f_ident = thm "ident"; |
|
666 val f_commute = thm "commute"; |
|
667 val f_assoc = thm "assoc"; |
|
668 |
|
669 |
|
670 Goal "f x (f y z) = f y (f x z)"; |
|
671 by (rtac (f_commute RS trans) 1); |
|
672 by (rtac (f_assoc RS trans) 1); |
|
673 by (rtac (f_commute RS arg_cong) 1); |
|
674 qed "f_left_commute"; |
|
675 |
|
676 val f_ac = [f_assoc, f_commute, f_left_commute]; |
|
677 |
|
678 Goal "f e x = x"; |
|
679 by (stac f_commute 1); |
|
680 by (rtac f_ident 1); |
|
681 qed "f_left_ident"; |
|
682 |
|
683 val f_idents = [f_left_ident, f_ident]; |
|
684 |
|
685 Goal "[| finite A; finite B |] \ |
|
686 \ ==> f (fold f e A) (fold f e B) = \ |
|
687 \ f (fold f e (A Un B)) (fold f e (A Int B))"; |
|
688 by (etac finite_induct 1); |
|
689 by (simp_tac (simpset() addsimps f_idents) 1); |
|
690 by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @ |
|
691 [export fold_insert,insert_absorb, Int_insert_left]) 1); |
|
692 qed "fold_Un_Int"; |
|
693 |
|
694 Goal "[| finite A; finite B; A Int B = {} |] \ |
|
695 \ ==> fold f e (A Un B) = f (fold f e A) (fold f e B)"; |
|
696 by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1); |
|
697 qed "fold_Un_disjoint"; |
|
698 |
|
699 Goal |
|
700 "[| finite A; finite B |] ==> A Int B = {} --> \ |
|
701 \ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)"; |
|
702 by (etac finite_induct 1); |
|
703 by (simp_tac (simpset() addsimps f_idents) 1); |
|
704 by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @ |
|
705 [export fold_insert,insert_absorb, Int_insert_left]) 1); |
|
706 qed "fold_Un_disjoint2"; |
|
707 |
|
708 Close_locale "ACe"; |
|
709 |
|
710 |
|
711 (*** setsum: generalized summation over a set ***) |
|
712 |
|
713 Goalw [setsum_def] "setsum f {} = 0"; |
|
714 by (Simp_tac 1); |
|
715 qed "setsum_empty"; |
|
716 Addsimps [setsum_empty]; |
|
717 |
|
718 Goalw [setsum_def] |
|
719 "!!f. [| finite F; a ~: F |] ==> \ |
|
720 \ setsum f (insert a F) = f a + setsum f F"; |
|
721 by (asm_simp_tac (simpset() addsimps [export fold_insert, |
|
722 thm "plus_ac0_left_commute"]) 1); |
|
723 qed "setsum_insert"; |
|
724 Addsimps [setsum_insert]; |
|
725 |
|
726 Goal "setsum (%i. 0) A = 0"; |
|
727 by (case_tac "finite A" 1); |
|
728 by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
729 by (etac finite_induct 1); |
|
730 by Auto_tac; |
|
731 qed "setsum_0"; |
|
732 |
|
733 Goal "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"; |
|
734 by (etac finite_induct 1); |
|
735 by Auto_tac; |
|
736 qed "setsum_eq_0_iff"; |
|
737 Addsimps [setsum_eq_0_iff]; |
|
738 |
|
739 Goal "setsum f A = Suc n ==> EX a:A. 0 < f a"; |
|
740 by (case_tac "finite A" 1); |
|
741 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
742 by (etac rev_mp 1); |
|
743 by (etac finite_induct 1); |
|
744 by Auto_tac; |
|
745 qed "setsum_SucD"; |
|
746 |
|
747 (*Could allow many "card" proofs to be simplified*) |
|
748 Goal "finite A ==> card A = setsum (%x. 1) A"; |
|
749 by (etac finite_induct 1); |
|
750 by Auto_tac; |
|
751 qed "card_eq_setsum"; |
|
752 |
|
753 (*The reversed orientation looks more natural, but LOOPS as a simprule!*) |
|
754 Goal "!!g. [| finite A; finite B |] \ |
|
755 \ ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"; |
|
756 by (etac finite_induct 1); |
|
757 by (Simp_tac 1); |
|
758 by (asm_full_simp_tac (simpset() addsimps (thms "plus_ac0") @ |
|
759 [Int_insert_left, insert_absorb]) 1); |
|
760 qed "setsum_Un_Int"; |
|
761 |
|
762 Goal "[| finite A; finite B; A Int B = {} |] \ |
|
763 \ ==> setsum g (A Un B) = setsum g A + setsum g B"; |
|
764 by (stac (setsum_Un_Int RS sym) 1); |
|
765 by Auto_tac; |
|
766 qed "setsum_Un_disjoint"; |
|
767 |
|
768 Goal "!!f::'a=>'b::plus_ac0. finite I \ |
|
769 \ ==> (ALL i:I. finite (A i)) --> \ |
|
770 \ (ALL i:I. ALL j:I. i~=j --> A i Int A j = {}) --> \ |
|
771 \ setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; |
|
772 by (etac finite_induct 1); |
|
773 by (Simp_tac 1); |
|
774 by (Clarify_tac 1); |
|
775 by (subgoal_tac "ALL i:F. x ~= i" 1); |
|
776 by (Blast_tac 2); |
|
777 by (subgoal_tac "A x Int UNION F A = {}" 1); |
|
778 by (Blast_tac 2); |
|
779 by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1); |
|
780 qed_spec_mp "setsum_UN_disjoint"; |
|
781 |
|
782 Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"; |
|
783 by (case_tac "finite A" 1); |
|
784 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
785 by (etac finite_induct 1); |
|
786 by Auto_tac; |
|
787 by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1); |
|
788 qed "setsum_addf"; |
|
789 |
|
790 (** For the natural numbers, we have subtraction **) |
|
791 |
|
792 Goal "[| finite A; finite B |] \ |
|
793 \ ==> (setsum f (A Un B) :: nat) = \ |
|
794 \ setsum f A + setsum f B - setsum f (A Int B)"; |
|
795 by (stac (setsum_Un_Int RS sym) 1); |
|
796 by Auto_tac; |
|
797 qed "setsum_Un"; |
|
798 |
|
799 Goal "(setsum f (A-{a}) :: nat) = \ |
|
800 \ (if a:A then setsum f A - f a else setsum f A)"; |
|
801 by (case_tac "finite A" 1); |
|
802 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
803 by (etac finite_induct 1); |
|
804 by (auto_tac (claset(), simpset() addsimps [insert_Diff_if])); |
|
805 by (dres_inst_tac [("a","a")] mk_disjoint_insert 1); |
|
806 by Auto_tac; |
|
807 qed_spec_mp "setsum_diff1"; |
|
808 |
|
809 val prems = Goal |
|
810 "[| A = B; !!x. x:B ==> f x = g x|] \ |
|
811 \ ==> setsum f A = setsum g B"; |
|
812 by (case_tac "finite B" 1); |
|
813 by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); |
|
814 by (simp_tac (simpset() addsimps prems) 1); |
|
815 by (subgoal_tac |
|
816 "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C" 1); |
|
817 by (asm_simp_tac (simpset() addsimps prems) 1); |
|
818 by (etac finite_induct 1); |
|
819 by (Simp_tac 1); |
|
820 by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); |
|
821 by (Clarify_tac 1); |
|
822 by (subgoal_tac "finite C" 1); |
|
823 by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2); |
|
824 by (subgoal_tac "C = insert x (C-{x})" 1); |
|
825 by (Blast_tac 2); |
|
826 by (etac ssubst 1); |
|
827 by (dtac spec 1); |
|
828 by (mp_tac 1); |
|
829 by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1); |
|
830 qed "setsum_cong"; |
|
831 |
|
832 |
|
833 (*** Basic theorem about "choose". By Florian Kammueller, tidied by LCP ***) |
|
834 |
|
835 Goal "finite A ==> card {B. B <= A & card B = 0} = 1"; |
|
836 by (asm_simp_tac (simpset() addcongs [conj_cong] |
|
837 addsimps [finite_subset RS card_0_eq]) 1); |
|
838 by (simp_tac (simpset() addcongs [rev_conj_cong]) 1); |
|
839 qed "card_s_0_eq_empty"; |
|
840 |
|
841 Goal "[| finite M; x ~: M |] \ |
|
842 \ ==> {s. s <= insert x M & card(s) = Suc k} \ |
|
843 \ = {s. s <= M & card(s) = Suc k} Un \ |
|
844 \ {s. EX t. t <= M & card(t) = k & s = insert x t}"; |
|
845 by Safe_tac; |
|
846 by (auto_tac (claset() addIs [finite_subset RS card_insert_disjoint], |
|
847 simpset())); |
|
848 by (dres_inst_tac [("x","xa - {x}")] spec 1); |
|
849 by (subgoal_tac ("x ~: xa") 1); |
|
850 by Auto_tac; |
|
851 by (etac rev_mp 1 THEN stac card_Diff_singleton 1); |
|
852 by (auto_tac (claset() addIs [finite_subset], simpset())); |
|
853 qed "choose_deconstruct"; |
|
854 |
|
855 Goal "[| finite(A); finite(B); f`A <= B; inj_on f A |] \ |
|
856 \ ==> card A <= card B"; |
|
857 by (auto_tac (claset() addIs [card_mono], |
|
858 simpset() addsimps [card_image RS sym])); |
|
859 qed "card_inj_on_le"; |
|
860 |
|
861 Goal "[| finite A; finite B; \ |
|
862 \ f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \ |
|
863 \ ==> card(A) = card(B)"; |
|
864 by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset())); |
|
865 qed "card_bij_eq"; |
|
866 |
|
867 Goal "[| finite A; x ~: A |] \ |
|
868 \ ==> card{B. EX C. C <= A & card(C) = k & B = insert x C} = \ |
|
869 \ card {B. B <= A & card(B) = k}"; |
|
870 by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1); |
|
871 by (res_inst_tac [("B","Pow(insert x A)")] finite_subset 1); |
|
872 by (res_inst_tac [("B","Pow(A)")] finite_subset 3); |
|
873 by (REPEAT(Fast_tac 1)); |
|
874 (* arity *) |
|
875 by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def])); |
|
876 by (stac Diff_insert0 1); |
|
877 by Auto_tac; |
|
878 qed "constr_bij"; |
|
879 |
|
880 (* Main theorem: combinatorial theorem about number of subsets of a set *) |
|
881 Goal "(ALL A. finite A --> card {B. B <= A & card B = k} = (card A choose k))"; |
|
882 by (induct_tac "k" 1); |
|
883 by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); |
|
884 (* first 0 case finished *) |
|
885 (* prepare finite set induction *) |
|
886 by (rtac allI 1 THEN rtac impI 1); |
|
887 (* second induction *) |
|
888 by (etac finite_induct 1); |
|
889 by (ALLGOALS |
|
890 (asm_simp_tac (simpset() addcongs [conj_cong] |
|
891 addsimps [card_s_0_eq_empty, choose_deconstruct]))); |
|
892 by (stac card_Un_disjoint 1); |
|
893 by (force_tac (claset(), simpset() addsimps [constr_bij]) 4); |
|
894 by (Force_tac 3); |
|
895 by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2, |
|
896 inst "B" "Pow (insert ?x ?F)" finite_subset]) 2); |
|
897 by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2 |
|
898 RSN (2, finite_subset)]) 1); |
|
899 qed "n_sub_lemma"; |
|
900 |
|
901 Goal "finite A ==> card {B. B <= A & card(B) = k} = ((card A) choose k)"; |
|
902 by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1); |
|
903 qed "n_subsets"; |
|