src/HOL/Finite.ML
 author nipkow Mon Mar 04 14:37:33 1996 +0100 (1996-03-04) changeset 1531 e5eb247ad13c parent 1465 5d7a7e439cec child 1548 afe750876848 permissions -rw-r--r--
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
1 (*  Title:      HOL/Finite.thy
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson & Tobias Nipkow
4     Copyright   1995  University of Cambridge & TU Muenchen
6 Finite sets and their cardinality
7 *)
9 open Finite;
11 (*** Fin ***)
13 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
14 by (rtac lfp_mono 1);
15 by (REPEAT (ares_tac basic_monos 1));
16 qed "Fin_mono";
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";
22 (* A : Fin(B) ==> A <= B *)
23 val FinD = Fin_subset_Pow RS subsetD RS PowD;
25 (*Discharging ~ x:y entails extra work*)
26 val major::prems = goal Finite.thy
27     "[| F:Fin(A);  P({}); \
28 \       !!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
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";
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);
42 by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
43 qed "Fin_UnI";
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)",
48             rtac mp, etac spec,
49             rtac subs]);
50 by (rtac (fin RS Fin_induct) 1);
51 by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
52 by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
53 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
54 by (ALLGOALS Asm_simp_tac);
55 qed "Fin_subset";
57 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
59                 [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
60 qed "subset_Fin";
63 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
64 by(stac insert_is_Un 1);
65 by(Simp_tac 1);
67 qed "insert_Fin";
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);
74 by (Simp_tac 1);
75 by (asm_simp_tac
76     (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
77 qed "Fin_imageI";
79 val major::prems = goal Finite.thy
80     "[| c: Fin(A);  b: Fin(A);                                  \
81 \       P(b);                                                   \
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
87                 (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
88 val lemma = result();
90 val prems = goal Finite.thy
91     "[| b: Fin(A);                                              \
92 \       P(b);                                                   \
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);
96 by (rtac (lemma RS mp) 1);
97 by (REPEAT (ares_tac (subset_refl::prems) 1));
98 qed "Fin_empty_induct";
101 (*** finite ***)
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";
112 goalw Finite.thy [finite_def] "finite {}";
113 by(Simp_tac 1);
114 qed "finite_emptyI";
117 goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
118 by(Asm_simp_tac 1);
119 qed "finite_insertI";
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)";
124 by(Asm_simp_tac 1);
125 qed "finite_UnI";
127 goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
128 be Fin_subset 1;
129 ba 1;
130 qed "finite_subset";
132 goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
133 by(Simp_tac 1);
134 qed "subset_finite";
137 goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
138 by(Simp_tac 1);
139 qed "insert_finite";
142 goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
143 be finite_induct 1;
144 by(Simp_tac 1);
146                           setloop split_tac[expand_if]) 1);
147 qed "finite_Diff";
150 (*The image of a finite set is finite*)
151 goal Finite.thy "!!F. finite F ==> finite(h``F)";
152 be finite_induct 1;
153 by(ALLGOALS Asm_simp_tac);
154 qed "finite_imageI";
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";
166 (*** Cardinality ***)
168 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
169 by(fast_tac eq_cs 1);
170 val Collect_conv_insert = result();
172 goalw Finite.thy [card_def] "card {} = 0";
173 br Least_equality 1;
174 by(ALLGOALS Asm_full_simp_tac);
175 qed "card_empty";
180 val [major] = goal Finite.thy
181   "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
182 br (major RS finite_induct) 1;
183  by(res_inst_tac [("x","0")] exI 1);
184  by(Simp_tac 1);
185 be exE 1;
186 be exE 1;
187 by(hyp_subst_tac 1);
188 by(res_inst_tac [("x","Suc n")] exI 1);
189 by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
192 qed "finite_has_card";
194 goal Finite.thy
195   "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
196 \  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
197 by(res_inst_tac [("n","n")] natE 1);
198  by(hyp_subst_tac 1);
199  by(Asm_full_simp_tac 1);
200 by(rename_tac "m" 1);
201 by(hyp_subst_tac 1);
202 by(case_tac "? a. a:A" 1);
203  by(res_inst_tac [("x","0")] exI 2);
204  by(Simp_tac 2);
205  by(fast_tac eq_cs 2);
206 be exE 1;
207 by(Simp_tac 1);
208 br exI 1;
209 br conjI 1;
210  br disjI2 1;
211  br refl 1;
212 be equalityE 1;
213 by(asm_full_simp_tac
215 by(SELECT_GOAL(safe_tac eq_cs)1);
216   by(Asm_full_simp_tac 1);
217   by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
218   by(SELECT_GOAL(safe_tac eq_cs)1);
219    by(subgoal_tac "x ~= f m" 1);
220     by(fast_tac set_cs 2);
221    by(subgoal_tac "? k. f k = x & k<m" 1);
222     by(best_tac set_cs 2);
223    by(SELECT_GOAL(safe_tac HOL_cs)1);
224    by(res_inst_tac [("x","k")] exI 1);
225    by(Asm_simp_tac 1);
226   by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
227   by(best_tac set_cs 1);
228  bd sym 1;
229  by(rotate_tac ~1 1);
230  by(Asm_full_simp_tac 1);
231  by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
232  by(SELECT_GOAL(safe_tac eq_cs)1);
233   by(subgoal_tac "x ~= f m" 1);
234    by(fast_tac set_cs 2);
235   by(subgoal_tac "? k. f k = x & k<m" 1);
236    by(best_tac set_cs 2);
237   by(SELECT_GOAL(safe_tac HOL_cs)1);
238   by(res_inst_tac [("x","k")] exI 1);
239   by(Asm_simp_tac 1);
240  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
241  by(best_tac set_cs 1);
242 by(res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
243 by(SELECT_GOAL(safe_tac eq_cs)1);
244  by(subgoal_tac "x ~= f i" 1);
245   by(fast_tac set_cs 2);
246  by(case_tac "x = f m" 1);
247   by(res_inst_tac [("x","i")] exI 1);
248   by(Asm_simp_tac 1);
249  by(subgoal_tac "? k. f k = x & k<m" 1);
250   by(best_tac set_cs 2);
251  by(SELECT_GOAL(safe_tac HOL_cs)1);
252  by(res_inst_tac [("x","k")] exI 1);
253  by(Asm_simp_tac 1);
254 by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
255 by(best_tac set_cs 1);
256 val lemma = result();
258 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
259 \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
260 br Least_equality 1;
261  bd finite_has_card 1;
262  be exE 1;
263  by(dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
264  be exE 1;
265  by(res_inst_tac
266    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
267  by(simp_tac
269  be subst 1;
270  br refl 1;
271 br notI 1;
272 be exE 1;
273 bd lemma 1;
274  ba 1;
275 be exE 1;
276 be conjE 1;
277 by(dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
278 by(dtac le_less_trans 1 THEN atac 1);
279 by(Asm_full_simp_tac 1);
280 be disjE 1;
281 by(etac less_asym 1 THEN atac 1);
282 by(hyp_subst_tac 1);
283 by(Asm_full_simp_tac 1);
284 val lemma = result();
286 goalw Finite.thy [card_def]
287   "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
288 be lemma 1;
289 ba 1;
290 qed "card_insert_disjoint";
292 val [major] = goal Finite.thy
293   "finite A ==> card(insert x A) = Suc(card(A-{x}))";
294 by(case_tac "x:A" 1);
295 by(asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
296 bd mk_disjoint_insert 1;
297 be exE 1;
298 by(Asm_simp_tac 1);
299 br card_insert_disjoint 1;
300 br (major RSN (2,finite_subset)) 1;
301 by(fast_tac set_cs 1);
302 by(fast_tac HOL_cs 1);
303 by(asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
304 qed "card_insert";