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.28  Addsimps Fin.intrs;
    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.36 +by(fast_tac (set_cs addIs [Fin_UnI] addDs
    1.37 +                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    1.38 +qed "subset_Fin";
    1.39 +Addsimps[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.44 +by(fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    1.45 +qed "insert_Fin";
    1.46 +Addsimps[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.84 +Addsimps [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.104 +Addsimps[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.109 +Addsimps[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.114 +by(asm_simp_tac (!simpset addsimps [insert_Diff_if]
   1.115 +                          setloop split_tac[expand_if]) 1);
   1.116 +qed "finite_Diff";
   1.117 +Addsimps [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.145 +Addsimps [card_empty];
   1.146 +
   1.147 +(*Addsimps [Collect_conv_insert];*)
   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.159 +by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
   1.160 +                          addcongs [Collect_cong1]) 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.237 +    (!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);
   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.274 +Addsimps [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";