src/HOL/Finite.ML
 changeset 1531 e5eb247ad13c parent 1465 5d7a7e439cec child 1548 afe750876848
```     1.1 --- a/src/HOL/Finite.ML	Mon Mar 04 12:28:48 1996 +0100
1.2 +++ b/src/HOL/Finite.ML	Mon Mar 04 14:37:33 1996 +0100
1.3 @@ -1,13 +1,15 @@
1.4  (*  Title:      HOL/Finite.thy
1.5      ID:         \$Id\$
1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 -    Copyright   1994  University of Cambridge
1.8 +    Author:     Lawrence C Paulson & Tobias Nipkow
1.9 +    Copyright   1995  University of Cambridge & TU Muenchen
1.10
1.11 -Finite powerset operator
1.12 +Finite sets and their cardinality
1.13  *)
1.14
1.15  open Finite;
1.16
1.17 +(*** Fin ***)
1.18 +
1.19  goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
1.20  by (rtac lfp_mono 1);
1.21  by (REPEAT (ares_tac basic_monos 1));
1.22 @@ -31,8 +33,6 @@
1.23  by (REPEAT (ares_tac prems 1));
1.24  qed "Fin_induct";
1.25
1.26 -(** Simplification for Fin **)
1.27 -
1.29
1.30  (*The union of two finite sets is finite*)
1.31 @@ -54,6 +54,19 @@
1.32  by (ALLGOALS Asm_simp_tac);
1.33  qed "Fin_subset";
1.34
1.35 +goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
1.37 +                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
1.38 +qed "subset_Fin";
1.40 +
1.41 +goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
1.42 +by(stac insert_is_Un 1);
1.43 +by(Simp_tac 1);
1.45 +qed "insert_Fin";
1.47 +
1.48  (*The image of a finite set is finite*)
1.49  val major::_ = goal Finite.thy
1.50      "F: Fin(A) ==> h``F : Fin(h``A)";
1.51 @@ -72,7 +85,7 @@
1.52  by (rtac (Diff_insert RS ssubst) 2);
1.53  by (ALLGOALS (asm_simp_tac
1.54                  (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
1.55 -qed "Fin_empty_induct_lemma";
1.56 +val lemma = result();
1.57
1.58  val prems = goal Finite.thy
1.59      "[| b: Fin(A);                                              \
1.60 @@ -80,6 +93,227 @@
1.61  \       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
1.62  \    |] ==> P({})";
1.63  by (rtac (Diff_cancel RS subst) 1);
1.64 -by (rtac (Fin_empty_induct_lemma RS mp) 1);
1.65 +by (rtac (lemma RS mp) 1);
1.66  by (REPEAT (ares_tac (subset_refl::prems) 1));
1.67  qed "Fin_empty_induct";
1.68 +
1.69 +
1.70 +(*** finite ***)
1.71 +
1.72 +val major::prems = goalw Finite.thy [finite_def]
1.73 +    "[| finite F;  P({}); \
1.74 +\       !!F x. [| finite F;  x~:F;  P(F) |] ==> P(insert x F) \
1.75 +\    |] ==> P(F)";
1.76 +by (rtac (major RS Fin_induct) 1);
1.77 +by (REPEAT (ares_tac prems 1));
1.78 +qed "finite_induct";
1.79 +
1.80 +
1.81 +goalw Finite.thy [finite_def] "finite {}";
1.82 +by(Simp_tac 1);
1.83 +qed "finite_emptyI";
1.85 +
1.86 +goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
1.87 +by(Asm_simp_tac 1);
1.88 +qed "finite_insertI";
1.89 +
1.90 +(*The union of two finite sets is finite*)
1.91 +goalw Finite.thy [finite_def]
1.92 +    "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
1.93 +by(Asm_simp_tac 1);
1.94 +qed "finite_UnI";
1.95 +
1.96 +goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
1.97 +be Fin_subset 1;
1.98 +ba 1;
1.99 +qed "finite_subset";
1.100 +
1.101 +goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
1.102 +by(Simp_tac 1);
1.103 +qed "subset_finite";
1.105 +
1.106 +goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
1.107 +by(Simp_tac 1);
1.108 +qed "insert_finite";
1.110 +
1.111 +goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
1.112 +be finite_induct 1;
1.113 +by(Simp_tac 1);
1.115 +                          setloop split_tac[expand_if]) 1);
1.116 +qed "finite_Diff";
1.118 +
1.119 +(*The image of a finite set is finite*)
1.120 +goal Finite.thy "!!F. finite F ==> finite(h``F)";
1.121 +be finite_induct 1;
1.122 +by(ALLGOALS Asm_simp_tac);
1.123 +qed "finite_imageI";
1.124 +
1.125 +val major::prems = goalw Finite.thy [finite_def]
1.126 +    "[| finite A;                                       \
1.127 +\       P(A);                                           \
1.128 +\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
1.129 +\    |] ==> P({})";
1.130 +by (rtac (major RS Fin_empty_induct) 1);
1.131 +by (REPEAT (ares_tac (subset_refl::prems) 1));
1.132 +qed "finite_empty_induct";
1.133 +
1.134 +
1.135 +(*** Cardinality ***)
1.136 +
1.137 +goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
1.138 +by(fast_tac eq_cs 1);
1.139 +val Collect_conv_insert = result();
1.140 +
1.141 +goalw Finite.thy [card_def] "card {} = 0";
1.142 +br Least_equality 1;
1.143 +by(ALLGOALS Asm_full_simp_tac);
1.144 +qed "card_empty";
1.146 +
1.148 +
1.149 +val [major] = goal Finite.thy
1.150 +  "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
1.151 +br (major RS finite_induct) 1;
1.152 + by(res_inst_tac [("x","0")] exI 1);
1.153 + by(Simp_tac 1);
1.154 +be exE 1;
1.155 +be exE 1;
1.156 +by(hyp_subst_tac 1);
1.157 +by(res_inst_tac [("x","Suc n")] exI 1);
1.158 +by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
1.161 +qed "finite_has_card";
1.162 +
1.163 +goal Finite.thy
1.164 +  "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
1.165 +\  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
1.166 +by(res_inst_tac [("n","n")] natE 1);
1.167 + by(hyp_subst_tac 1);
1.168 + by(Asm_full_simp_tac 1);
1.169 +by(rename_tac "m" 1);
1.170 +by(hyp_subst_tac 1);
1.171 +by(case_tac "? a. a:A" 1);
1.172 + by(res_inst_tac [("x","0")] exI 2);
1.173 + by(Simp_tac 2);
1.174 + by(fast_tac eq_cs 2);
1.175 +be exE 1;
1.176 +by(Simp_tac 1);
1.177 +br exI 1;
1.178 +br conjI 1;
1.179 + br disjI2 1;
1.180 + br refl 1;
1.181 +be equalityE 1;
1.182 +by(asm_full_simp_tac
1.183 +     (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
1.184 +by(SELECT_GOAL(safe_tac eq_cs)1);
1.185 +  by(Asm_full_simp_tac 1);
1.186 +  by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
1.187 +  by(SELECT_GOAL(safe_tac eq_cs)1);
1.188 +   by(subgoal_tac "x ~= f m" 1);
1.189 +    by(fast_tac set_cs 2);
1.190 +   by(subgoal_tac "? k. f k = x & k<m" 1);
1.191 +    by(best_tac set_cs 2);
1.192 +   by(SELECT_GOAL(safe_tac HOL_cs)1);
1.193 +   by(res_inst_tac [("x","k")] exI 1);
1.194 +   by(Asm_simp_tac 1);
1.195 +  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
1.196 +  by(best_tac set_cs 1);
1.197 + bd sym 1;
1.198 + by(rotate_tac ~1 1);
1.199 + by(Asm_full_simp_tac 1);
1.200 + by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
1.201 + by(SELECT_GOAL(safe_tac eq_cs)1);
1.202 +  by(subgoal_tac "x ~= f m" 1);
1.203 +   by(fast_tac set_cs 2);
1.204 +  by(subgoal_tac "? k. f k = x & k<m" 1);
1.205 +   by(best_tac set_cs 2);
1.206 +  by(SELECT_GOAL(safe_tac HOL_cs)1);
1.207 +  by(res_inst_tac [("x","k")] exI 1);
1.208 +  by(Asm_simp_tac 1);
1.209 + by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
1.210 + by(best_tac set_cs 1);
1.211 +by(res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
1.212 +by(SELECT_GOAL(safe_tac eq_cs)1);
1.213 + by(subgoal_tac "x ~= f i" 1);
1.214 +  by(fast_tac set_cs 2);
1.215 + by(case_tac "x = f m" 1);
1.216 +  by(res_inst_tac [("x","i")] exI 1);
1.217 +  by(Asm_simp_tac 1);
1.218 + by(subgoal_tac "? k. f k = x & k<m" 1);
1.219 +  by(best_tac set_cs 2);
1.220 + by(SELECT_GOAL(safe_tac HOL_cs)1);
1.221 + by(res_inst_tac [("x","k")] exI 1);
1.222 + by(Asm_simp_tac 1);
1.223 +by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
1.224 +by(best_tac set_cs 1);
1.225 +val lemma = result();
1.226 +
1.227 +goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
1.228 +\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
1.229 +br Least_equality 1;
1.230 + bd finite_has_card 1;
1.231 + be exE 1;
1.232 + by(dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
1.233 + be exE 1;
1.234 + by(res_inst_tac
1.235 +   [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
1.236 + by(simp_tac
1.238 + be subst 1;
1.239 + br refl 1;
1.240 +br notI 1;
1.241 +be exE 1;
1.242 +bd lemma 1;
1.243 + ba 1;
1.244 +be exE 1;
1.245 +be conjE 1;
1.246 +by(dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
1.247 +by(dtac le_less_trans 1 THEN atac 1);
1.248 +by(Asm_full_simp_tac 1);
1.249 +be disjE 1;
1.250 +by(etac less_asym 1 THEN atac 1);
1.251 +by(hyp_subst_tac 1);
1.252 +by(Asm_full_simp_tac 1);
1.253 +val lemma = result();
1.254 +
1.255 +goalw Finite.thy [card_def]
1.256 +  "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
1.257 +be lemma 1;
1.258 +ba 1;
1.259 +qed "card_insert_disjoint";
1.260 +
1.261 +val [major] = goal Finite.thy
1.262 +  "finite A ==> card(insert x A) = Suc(card(A-{x}))";
1.263 +by(case_tac "x:A" 1);
1.264 +by(asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
1.265 +bd mk_disjoint_insert 1;
1.266 +be exE 1;
1.267 +by(Asm_simp_tac 1);
1.268 +br card_insert_disjoint 1;
1.269 +br (major RSN (2,finite_subset)) 1;
1.270 +by(fast_tac set_cs 1);
1.271 +by(fast_tac HOL_cs 1);
1.272 +by(asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
1.273 +qed "card_insert";
1.275 +
1.276 +
1.277 +goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
1.278 +be finite_induct 1;
1.279 +by(Simp_tac 1);
1.280 +by(strip_tac 1);
1.281 +by(case_tac "x:B" 1);
1.282 + bd mk_disjoint_insert 1;
1.283 + by(SELECT_GOAL(safe_tac HOL_cs)1);
1.284 + by(rotate_tac ~1 1);
1.285 + by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.286 +by(rotate_tac ~1 1);
1.287 +by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.288 +qed_spec_mp "card_mono";
```