1465
|
1 |
(* Title: HOL/Finite.thy
|
923
|
2 |
ID: $Id$
|
1531
|
3 |
Author: Lawrence C Paulson & Tobias Nipkow
|
|
4 |
Copyright 1995 University of Cambridge & TU Muenchen
|
923
|
5 |
|
1531
|
6 |
Finite sets and their cardinality
|
923
|
7 |
*)
|
|
8 |
|
|
9 |
open Finite;
|
|
10 |
|
1548
|
11 |
section "The finite powerset operator -- Fin";
|
1531
|
12 |
|
923
|
13 |
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
|
1465
|
14 |
by (rtac lfp_mono 1);
|
923
|
15 |
by (REPEAT (ares_tac basic_monos 1));
|
|
16 |
qed "Fin_mono";
|
|
17 |
|
|
18 |
goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
|
|
19 |
by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
|
|
20 |
qed "Fin_subset_Pow";
|
|
21 |
|
|
22 |
(* A : Fin(B) ==> A <= B *)
|
|
23 |
val FinD = Fin_subset_Pow RS subsetD RS PowD;
|
|
24 |
|
|
25 |
(*Discharging ~ x:y entails extra work*)
|
|
26 |
val major::prems = goal Finite.thy
|
|
27 |
"[| F:Fin(A); P({}); \
|
1465
|
28 |
\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \
|
923
|
29 |
\ |] ==> P(F)";
|
|
30 |
by (rtac (major RS Fin.induct) 1);
|
|
31 |
by (excluded_middle_tac "a:b" 2);
|
|
32 |
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)
|
|
33 |
by (REPEAT (ares_tac prems 1));
|
|
34 |
qed "Fin_induct";
|
|
35 |
|
1264
|
36 |
Addsimps Fin.intrs;
|
923
|
37 |
|
|
38 |
(*The union of two finite sets is finite*)
|
|
39 |
val major::prems = goal Finite.thy
|
|
40 |
"[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)";
|
|
41 |
by (rtac (major RS Fin_induct) 1);
|
1264
|
42 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
|
923
|
43 |
qed "Fin_UnI";
|
|
44 |
|
|
45 |
(*Every subset of a finite set is finite*)
|
|
46 |
val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)";
|
|
47 |
by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
|
1465
|
48 |
rtac mp, etac spec,
|
|
49 |
rtac subs]);
|
923
|
50 |
by (rtac (fin RS Fin_induct) 1);
|
1264
|
51 |
by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
|
923
|
52 |
by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
|
|
53 |
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
|
1264
|
54 |
by (ALLGOALS Asm_simp_tac);
|
923
|
55 |
qed "Fin_subset";
|
|
56 |
|
1531
|
57 |
goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
|
1553
|
58 |
by (fast_tac (set_cs addIs [Fin_UnI] addDs
|
1531
|
59 |
[Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
|
|
60 |
qed "subset_Fin";
|
|
61 |
Addsimps[subset_Fin];
|
|
62 |
|
|
63 |
goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
|
1553
|
64 |
by (stac insert_is_Un 1);
|
|
65 |
by (Simp_tac 1);
|
|
66 |
by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
|
1531
|
67 |
qed "insert_Fin";
|
|
68 |
Addsimps[insert_Fin];
|
|
69 |
|
923
|
70 |
(*The image of a finite set is finite*)
|
|
71 |
val major::_ = goal Finite.thy
|
|
72 |
"F: Fin(A) ==> h``F : Fin(h``A)";
|
|
73 |
by (rtac (major RS Fin_induct) 1);
|
1264
|
74 |
by (Simp_tac 1);
|
|
75 |
by (asm_simp_tac
|
|
76 |
(!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
|
923
|
77 |
qed "Fin_imageI";
|
|
78 |
|
|
79 |
val major::prems = goal Finite.thy
|
1465
|
80 |
"[| c: Fin(A); b: Fin(A); \
|
|
81 |
\ P(b); \
|
923
|
82 |
\ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
|
|
83 |
\ |] ==> c<=b --> P(b-c)";
|
|
84 |
by (rtac (major RS Fin_induct) 1);
|
|
85 |
by (rtac (Diff_insert RS ssubst) 2);
|
|
86 |
by (ALLGOALS (asm_simp_tac
|
1264
|
87 |
(!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
|
1531
|
88 |
val lemma = result();
|
923
|
89 |
|
|
90 |
val prems = goal Finite.thy
|
1465
|
91 |
"[| b: Fin(A); \
|
|
92 |
\ P(b); \
|
923
|
93 |
\ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
|
|
94 |
\ |] ==> P({})";
|
|
95 |
by (rtac (Diff_cancel RS subst) 1);
|
1531
|
96 |
by (rtac (lemma RS mp) 1);
|
923
|
97 |
by (REPEAT (ares_tac (subset_refl::prems) 1));
|
|
98 |
qed "Fin_empty_induct";
|
1531
|
99 |
|
|
100 |
|
1548
|
101 |
section "The predicate 'finite'";
|
1531
|
102 |
|
|
103 |
val major::prems = goalw Finite.thy [finite_def]
|
|
104 |
"[| finite F; P({}); \
|
|
105 |
\ !!F x. [| finite F; x~:F; P(F) |] ==> P(insert x F) \
|
|
106 |
\ |] ==> P(F)";
|
|
107 |
by (rtac (major RS Fin_induct) 1);
|
|
108 |
by (REPEAT (ares_tac prems 1));
|
|
109 |
qed "finite_induct";
|
|
110 |
|
|
111 |
|
|
112 |
goalw Finite.thy [finite_def] "finite {}";
|
1553
|
113 |
by (Simp_tac 1);
|
1531
|
114 |
qed "finite_emptyI";
|
|
115 |
Addsimps [finite_emptyI];
|
|
116 |
|
|
117 |
goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
|
1553
|
118 |
by (Asm_simp_tac 1);
|
1531
|
119 |
qed "finite_insertI";
|
|
120 |
|
|
121 |
(*The union of two finite sets is finite*)
|
|
122 |
goalw Finite.thy [finite_def]
|
|
123 |
"!!F. [| finite F; finite G |] ==> finite(F Un G)";
|
1553
|
124 |
by (Asm_simp_tac 1);
|
1531
|
125 |
qed "finite_UnI";
|
|
126 |
|
|
127 |
goalw Finite.thy [finite_def] "!!A. [| A<=B; finite B |] ==> finite A";
|
1553
|
128 |
by (etac Fin_subset 1);
|
|
129 |
by (assume_tac 1);
|
1531
|
130 |
qed "finite_subset";
|
|
131 |
|
|
132 |
goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
|
1553
|
133 |
by (Simp_tac 1);
|
1531
|
134 |
qed "subset_finite";
|
|
135 |
Addsimps[subset_finite];
|
|
136 |
|
|
137 |
goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
|
1553
|
138 |
by (Simp_tac 1);
|
1531
|
139 |
qed "insert_finite";
|
|
140 |
Addsimps[insert_finite];
|
|
141 |
|
|
142 |
goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
|
1553
|
143 |
by (etac finite_induct 1);
|
|
144 |
by (Simp_tac 1);
|
|
145 |
by (asm_simp_tac (!simpset addsimps [insert_Diff_if]
|
1531
|
146 |
setloop split_tac[expand_if]) 1);
|
|
147 |
qed "finite_Diff";
|
|
148 |
Addsimps [finite_Diff];
|
|
149 |
|
|
150 |
(*The image of a finite set is finite*)
|
|
151 |
goal Finite.thy "!!F. finite F ==> finite(h``F)";
|
1553
|
152 |
by (etac finite_induct 1);
|
|
153 |
by (ALLGOALS Asm_simp_tac);
|
1531
|
154 |
qed "finite_imageI";
|
|
155 |
|
|
156 |
val major::prems = goalw Finite.thy [finite_def]
|
|
157 |
"[| finite A; \
|
|
158 |
\ P(A); \
|
|
159 |
\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \
|
|
160 |
\ |] ==> P({})";
|
|
161 |
by (rtac (major RS Fin_empty_induct) 1);
|
|
162 |
by (REPEAT (ares_tac (subset_refl::prems) 1));
|
|
163 |
qed "finite_empty_induct";
|
|
164 |
|
|
165 |
|
1548
|
166 |
section "Finite cardinality -- 'card'";
|
1531
|
167 |
|
|
168 |
goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
|
1553
|
169 |
by (fast_tac eq_cs 1);
|
1531
|
170 |
val Collect_conv_insert = result();
|
|
171 |
|
|
172 |
goalw Finite.thy [card_def] "card {} = 0";
|
1553
|
173 |
by (rtac Least_equality 1);
|
|
174 |
by (ALLGOALS Asm_full_simp_tac);
|
1531
|
175 |
qed "card_empty";
|
|
176 |
Addsimps [card_empty];
|
|
177 |
|
|
178 |
val [major] = goal Finite.thy
|
|
179 |
"finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
|
1553
|
180 |
by (rtac (major RS finite_induct) 1);
|
|
181 |
by (res_inst_tac [("x","0")] exI 1);
|
|
182 |
by (Simp_tac 1);
|
|
183 |
by (etac exE 1);
|
|
184 |
by (etac exE 1);
|
|
185 |
by (hyp_subst_tac 1);
|
|
186 |
by (res_inst_tac [("x","Suc n")] exI 1);
|
|
187 |
by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
|
|
188 |
by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]
|
1548
|
189 |
addcongs [rev_conj_cong]) 1);
|
1531
|
190 |
qed "finite_has_card";
|
|
191 |
|
|
192 |
goal Finite.thy
|
|
193 |
"!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
|
|
194 |
\ ? m::nat. m<n & (? g. A = {g i|i.i<m})";
|
1553
|
195 |
by (res_inst_tac [("n","n")] natE 1);
|
|
196 |
by (hyp_subst_tac 1);
|
|
197 |
by (Asm_full_simp_tac 1);
|
|
198 |
by (rename_tac "m" 1);
|
|
199 |
by (hyp_subst_tac 1);
|
|
200 |
by (case_tac "? a. a:A" 1);
|
|
201 |
by (res_inst_tac [("x","0")] exI 2);
|
|
202 |
by (Simp_tac 2);
|
|
203 |
by (fast_tac eq_cs 2);
|
|
204 |
by (etac exE 1);
|
|
205 |
by (Simp_tac 1);
|
|
206 |
by (rtac exI 1);
|
|
207 |
by (rtac conjI 1);
|
1531
|
208 |
br disjI2 1;
|
|
209 |
br refl 1;
|
1553
|
210 |
by (etac equalityE 1);
|
|
211 |
by (asm_full_simp_tac
|
1531
|
212 |
(!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
|
1553
|
213 |
by (SELECT_GOAL(safe_tac eq_cs)1);
|
|
214 |
by (Asm_full_simp_tac 1);
|
|
215 |
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
|
|
216 |
by (SELECT_GOAL(safe_tac eq_cs)1);
|
|
217 |
by (subgoal_tac "x ~= f m" 1);
|
|
218 |
by (fast_tac set_cs 2);
|
|
219 |
by (subgoal_tac "? k. f k = x & k<m" 1);
|
|
220 |
by (best_tac set_cs 2);
|
|
221 |
by (SELECT_GOAL(safe_tac HOL_cs)1);
|
|
222 |
by (res_inst_tac [("x","k")] exI 1);
|
|
223 |
by (Asm_simp_tac 1);
|
|
224 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
225 |
by (best_tac set_cs 1);
|
1531
|
226 |
bd sym 1;
|
1553
|
227 |
by (rotate_tac ~1 1);
|
|
228 |
by (Asm_full_simp_tac 1);
|
|
229 |
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
|
|
230 |
by (SELECT_GOAL(safe_tac eq_cs)1);
|
|
231 |
by (subgoal_tac "x ~= f m" 1);
|
|
232 |
by (fast_tac set_cs 2);
|
|
233 |
by (subgoal_tac "? k. f k = x & k<m" 1);
|
|
234 |
by (best_tac set_cs 2);
|
|
235 |
by (SELECT_GOAL(safe_tac HOL_cs)1);
|
|
236 |
by (res_inst_tac [("x","k")] exI 1);
|
|
237 |
by (Asm_simp_tac 1);
|
|
238 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
239 |
by (best_tac set_cs 1);
|
|
240 |
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
|
|
241 |
by (SELECT_GOAL(safe_tac eq_cs)1);
|
|
242 |
by (subgoal_tac "x ~= f i" 1);
|
|
243 |
by (fast_tac set_cs 2);
|
|
244 |
by (case_tac "x = f m" 1);
|
|
245 |
by (res_inst_tac [("x","i")] exI 1);
|
|
246 |
by (Asm_simp_tac 1);
|
|
247 |
by (subgoal_tac "? k. f k = x & k<m" 1);
|
|
248 |
by (best_tac set_cs 2);
|
|
249 |
by (SELECT_GOAL(safe_tac HOL_cs)1);
|
|
250 |
by (res_inst_tac [("x","k")] exI 1);
|
|
251 |
by (Asm_simp_tac 1);
|
|
252 |
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
253 |
by (best_tac set_cs 1);
|
1531
|
254 |
val lemma = result();
|
|
255 |
|
|
256 |
goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
|
|
257 |
\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
|
1553
|
258 |
by (rtac Least_equality 1);
|
1531
|
259 |
bd finite_has_card 1;
|
|
260 |
be exE 1;
|
1553
|
261 |
by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
|
1531
|
262 |
be exE 1;
|
1553
|
263 |
by (res_inst_tac
|
1531
|
264 |
[("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
|
1553
|
265 |
by (simp_tac
|
1548
|
266 |
(!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
|
1531
|
267 |
be subst 1;
|
|
268 |
br refl 1;
|
1553
|
269 |
by (rtac notI 1);
|
|
270 |
by (etac exE 1);
|
|
271 |
by (dtac lemma 1);
|
1531
|
272 |
ba 1;
|
1553
|
273 |
by (etac exE 1);
|
|
274 |
by (etac conjE 1);
|
|
275 |
by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
|
|
276 |
by (dtac le_less_trans 1 THEN atac 1);
|
|
277 |
by (Asm_full_simp_tac 1);
|
|
278 |
by (etac disjE 1);
|
|
279 |
by (etac less_asym 1 THEN atac 1);
|
|
280 |
by (hyp_subst_tac 1);
|
|
281 |
by (Asm_full_simp_tac 1);
|
1531
|
282 |
val lemma = result();
|
|
283 |
|
|
284 |
goalw Finite.thy [card_def]
|
|
285 |
"!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
|
1553
|
286 |
by (etac lemma 1);
|
|
287 |
by (assume_tac 1);
|
1531
|
288 |
qed "card_insert_disjoint";
|
|
289 |
|
|
290 |
val [major] = goal Finite.thy
|
|
291 |
"finite A ==> card(insert x A) = Suc(card(A-{x}))";
|
1553
|
292 |
by (case_tac "x:A" 1);
|
|
293 |
by (asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
|
|
294 |
by (dtac mk_disjoint_insert 1);
|
|
295 |
by (etac exE 1);
|
|
296 |
by (Asm_simp_tac 1);
|
|
297 |
by (rtac card_insert_disjoint 1);
|
|
298 |
by (rtac (major RSN (2,finite_subset)) 1);
|
|
299 |
by (fast_tac set_cs 1);
|
|
300 |
by (fast_tac HOL_cs 1);
|
|
301 |
by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
|
1531
|
302 |
qed "card_insert";
|
|
303 |
Addsimps [card_insert];
|
|
304 |
|
|
305 |
|
|
306 |
goal Finite.thy "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
|
1553
|
307 |
by (etac finite_induct 1);
|
|
308 |
by (Simp_tac 1);
|
|
309 |
by (strip_tac 1);
|
|
310 |
by (case_tac "x:B" 1);
|
|
311 |
by (dtac mk_disjoint_insert 1);
|
|
312 |
by (SELECT_GOAL(safe_tac HOL_cs)1);
|
|
313 |
by (rotate_tac ~1 1);
|
|
314 |
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
|
|
315 |
by (rotate_tac ~1 1);
|
|
316 |
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
|
1531
|
317 |
qed_spec_mp "card_mono";
|