src/HOL/Finite.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4304 af2a2cd9fa51
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/Finite.thy
     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 open Finite;
    10 
    11 section "finite";
    12 
    13 (*
    14 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    15 by (rtac lfp_mono 1);
    16 by (REPEAT (ares_tac basic_monos 1));
    17 qed "Fin_mono";
    18 
    19 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
    20 by (blast_tac (claset() addSIs [lfp_lowerbound]) 1);
    21 qed "Fin_subset_Pow";
    22 
    23 (* A : Fin(B) ==> A <= B *)
    24 val FinD = Fin_subset_Pow RS subsetD RS PowD;
    25 *)
    26 
    27 (*Discharging ~ x:y entails extra work*)
    28 val major::prems = goal Finite.thy 
    29     "[| finite F;  P({}); \
    30 \       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
    31 \    |] ==> P(F)";
    32 by (rtac (major RS Finites.induct) 1);
    33 by (excluded_middle_tac "a:A" 2);
    34 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
    35 by (REPEAT (ares_tac prems 1));
    36 qed "finite_induct";
    37 
    38 val major::prems = goal Finite.thy 
    39     "[| finite F; \
    40 \       P({}); \
    41 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    42 \    |] ==> F <= A --> P(F)";
    43 by (rtac (major RS finite_induct) 1);
    44 by (ALLGOALS (blast_tac (claset() addIs prems)));
    45 val lemma = result();
    46 
    47 val prems = goal Finite.thy 
    48     "[| finite F;  F <= A; \
    49 \       P({}); \
    50 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    51 \    |] ==> P(F)";
    52 by (blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
    53 qed "finite_subset_induct";
    54 
    55 Addsimps Finites.intrs;
    56 AddSIs Finites.intrs;
    57 
    58 (*The union of two finite sets is finite*)
    59 val major::prems = goal Finite.thy
    60     "[| finite F;  finite G |] ==> finite(F Un G)";
    61 by (rtac (major RS finite_induct) 1);
    62 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    63 qed "finite_UnI";
    64 
    65 (*Every subset of a finite set is finite*)
    66 val [subs,fin] = goal Finite.thy "[| A<=B;  finite B |] ==> finite A";
    67 by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
    68             rtac mp, etac spec,
    69             rtac subs]);
    70 by (rtac (fin RS finite_induct) 1);
    71 by (simp_tac (simpset() addsimps [subset_Un_eq]) 1);
    72 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
    73 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    74 by (ALLGOALS Asm_simp_tac);
    75 qed "finite_subset";
    76 
    77 goal Finite.thy "finite(F Un G) = (finite F & finite G)";
    78 by (blast_tac (claset() addIs [finite_UnI] addDs
    79                 [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
    80 qed "finite_Un";
    81 AddIffs[finite_Un];
    82 
    83 goal Finite.thy "finite(insert a A) = finite A";
    84 by (stac insert_is_Un 1);
    85 by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
    86 by (Blast_tac 1);
    87 qed "finite_insert";
    88 Addsimps[finite_insert];
    89 
    90 (*The image of a finite set is finite *)
    91 goal Finite.thy  "!!F. finite F ==> finite(h``F)";
    92 by (etac finite_induct 1);
    93 by (Simp_tac 1);
    94 by (Asm_simp_tac 1);
    95 qed "finite_imageI";
    96 
    97 val major::prems = goal Finite.thy 
    98     "[| finite c;  finite b;                                  \
    99 \       P(b);                                                   \
   100 \       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
   101 \    |] ==> c<=b --> P(b-c)";
   102 by (rtac (major RS finite_induct) 1);
   103 by (stac Diff_insert 2);
   104 by (ALLGOALS (asm_simp_tac
   105                 (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
   106 val lemma = result();
   107 
   108 val prems = goal Finite.thy 
   109     "[| finite A;                                       \
   110 \       P(A);                                           \
   111 \       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   112 \    |] ==> P({})";
   113 by (rtac (Diff_cancel RS subst) 1);
   114 by (rtac (lemma RS mp) 1);
   115 by (REPEAT (ares_tac (subset_refl::prems) 1));
   116 qed "finite_empty_induct";
   117 
   118 
   119 (* finite B ==> finite (B - Ba) *)
   120 bind_thm ("finite_Diff", Diff_subset RS finite_subset);
   121 Addsimps [finite_Diff];
   122 
   123 goal Finite.thy "finite(A-{a}) = finite(A)";
   124 by (case_tac "a:A" 1);
   125 by (rtac (finite_insert RS sym RS trans) 1);
   126 by (stac insert_Diff 1);
   127 by (ALLGOALS Asm_simp_tac);
   128 qed "finite_Diff_singleton";
   129 AddIffs [finite_Diff_singleton];
   130 
   131 (*Lemma for proving finite_imageD*)
   132 goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
   133 by (etac finite_induct 1);
   134  by (ALLGOALS Asm_simp_tac);
   135 by (Clarify_tac 1);
   136 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
   137  by (Clarify_tac 1);
   138  by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1);
   139  by (Blast_tac 1);
   140 by (thin_tac "ALL A. ?PP(A)" 1);
   141 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
   142 by (Clarify_tac 1);
   143 by (res_inst_tac [("x","xa")] bexI 1);
   144 by (ALLGOALS 
   145     (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff])));
   146 val lemma = result();
   147 
   148 goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
   149 by (dtac lemma 1);
   150 by (Blast_tac 1);
   151 qed "finite_imageD";
   152 
   153 (** The finite UNION of finite sets **)
   154 
   155 val [prem] = goal Finite.thy
   156  "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
   157 by (rtac (prem RS finite_induct) 1);
   158 by (ALLGOALS Asm_simp_tac);
   159 bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
   160 Addsimps [finite_UnionI];
   161 
   162 (** Sigma of finite sets **)
   163 
   164 goalw Finite.thy [Sigma_def]
   165  "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
   166 by (blast_tac (claset() addSIs [finite_UnionI]) 1);
   167 bind_thm("finite_SigmaI", ballI RSN (2,result()));
   168 Addsimps [finite_SigmaI];
   169 
   170 (** The powerset of a finite set **)
   171 
   172 goal Finite.thy "!!A. finite(Pow A) ==> finite A";
   173 by (subgoal_tac "finite ((%x.{x})``A)" 1);
   174 by (rtac finite_subset 2);
   175 by (assume_tac 3);
   176 by (ALLGOALS
   177     (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
   178 val lemma = result();
   179 
   180 goal Finite.thy "finite(Pow A) = finite A";
   181 by (rtac iffI 1);
   182 by (etac lemma 1);
   183 (*Opposite inclusion: finite A ==> finite (Pow A) *)
   184 by (etac finite_induct 1);
   185 by (ALLGOALS 
   186     (asm_simp_tac
   187      (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert])));
   188 qed "finite_Pow_iff";
   189 AddIffs [finite_Pow_iff];
   190 
   191 goal Finite.thy "finite(r^-1) = finite r";
   192 by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
   193  by (Asm_simp_tac 1);
   194  by (rtac iffI 1);
   195   by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
   196   by (simp_tac (simpset() addsplits [expand_split]) 1);
   197  by (etac finite_imageI 1);
   198 by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
   199 by (Auto_tac());
   200  by (rtac bexI 1);
   201  by (assume_tac 2);
   202  by (Simp_tac 1);
   203 by (split_all_tac 1);
   204 by (Asm_full_simp_tac 1);
   205 qed "finite_inverse";
   206 AddIffs [finite_inverse];
   207 
   208 section "Finite cardinality -- 'card'";
   209 
   210 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
   211 by (Blast_tac 1);
   212 val Collect_conv_insert = result();
   213 
   214 goalw Finite.thy [card_def] "card {} = 0";
   215 by (rtac Least_equality 1);
   216 by (ALLGOALS Asm_full_simp_tac);
   217 qed "card_empty";
   218 Addsimps [card_empty];
   219 
   220 val [major] = goal Finite.thy
   221   "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
   222 by (rtac (major RS finite_induct) 1);
   223  by (res_inst_tac [("x","0")] exI 1);
   224  by (Simp_tac 1);
   225 by (etac exE 1);
   226 by (etac exE 1);
   227 by (hyp_subst_tac 1);
   228 by (res_inst_tac [("x","Suc n")] exI 1);
   229 by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
   230 by (asm_simp_tac (simpset() addsimps [Collect_conv_insert, less_Suc_eq]
   231                           addcongs [rev_conj_cong]) 1);
   232 qed "finite_has_card";
   233 
   234 goal Finite.thy
   235   "!!A.[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
   236 \  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
   237 by (res_inst_tac [("n","n")] natE 1);
   238  by (hyp_subst_tac 1);
   239  by (Asm_full_simp_tac 1);
   240 by (rename_tac "m" 1);
   241 by (hyp_subst_tac 1);
   242 by (case_tac "? a. a:A" 1);
   243  by (res_inst_tac [("x","0")] exI 2);
   244  by (Simp_tac 2);
   245  by (Blast_tac 2);
   246 by (etac exE 1);
   247 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   248 by (rtac exI 1);
   249 by (rtac (refl RS disjI2 RS conjI) 1);
   250 by (etac equalityE 1);
   251 by (asm_full_simp_tac
   252      (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
   253 by Safe_tac;
   254   by (Asm_full_simp_tac 1);
   255   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   256   by (SELECT_GOAL Safe_tac 1);
   257    by (subgoal_tac "x ~= f m" 1);
   258     by (Blast_tac 2);
   259    by (subgoal_tac "? k. f k = x & k<m" 1);
   260     by (Blast_tac 2);
   261    by (SELECT_GOAL Safe_tac 1);
   262    by (res_inst_tac [("x","k")] exI 1);
   263    by (Asm_simp_tac 1);
   264   by (simp_tac (simpset() addsplits [expand_if]) 1);
   265   by (Blast_tac 1);
   266  by (dtac sym 1);
   267  by (rotate_tac ~1 1);
   268  by (Asm_full_simp_tac 1);
   269  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   270  by (SELECT_GOAL Safe_tac 1);
   271   by (subgoal_tac "x ~= f m" 1);
   272    by (Blast_tac 2);
   273   by (subgoal_tac "? k. f k = x & k<m" 1);
   274    by (Blast_tac 2);
   275   by (SELECT_GOAL Safe_tac 1);
   276   by (res_inst_tac [("x","k")] exI 1);
   277   by (Asm_simp_tac 1);
   278  by (simp_tac (simpset() addsplits [expand_if]) 1);
   279  by (Blast_tac 1);
   280 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   281 by (SELECT_GOAL Safe_tac 1);
   282  by (subgoal_tac "x ~= f i" 1);
   283   by (Blast_tac 2);
   284  by (case_tac "x = f m" 1);
   285   by (res_inst_tac [("x","i")] exI 1);
   286   by (Asm_simp_tac 1);
   287  by (subgoal_tac "? k. f k = x & k<m" 1);
   288   by (Blast_tac 2);
   289  by (SELECT_GOAL Safe_tac 1);
   290  by (res_inst_tac [("x","k")] exI 1);
   291  by (Asm_simp_tac 1);
   292 by (simp_tac (simpset() addsplits [expand_if]) 1);
   293 by (Blast_tac 1);
   294 val lemma = result();
   295 
   296 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
   297 \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
   298 by (rtac Least_equality 1);
   299  by (dtac finite_has_card 1);
   300  by (etac exE 1);
   301  by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1);
   302  by (etac exE 1);
   303  by (res_inst_tac
   304    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
   305  by (simp_tac
   306     (simpset() addsimps [Collect_conv_insert, less_Suc_eq] 
   307               addcongs [rev_conj_cong]) 1);
   308  by (etac subst 1);
   309  by (rtac refl 1);
   310 by (rtac notI 1);
   311 by (etac exE 1);
   312 by (dtac lemma 1);
   313  by (assume_tac 1);
   314 by (etac exE 1);
   315 by (etac conjE 1);
   316 by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   317 by (dtac le_less_trans 1 THEN atac 1);
   318 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   319 by (etac disjE 1);
   320 by (etac less_asym 1 THEN atac 1);
   321 by (hyp_subst_tac 1);
   322 by (Asm_full_simp_tac 1);
   323 val lemma = result();
   324 
   325 goalw Finite.thy [card_def]
   326   "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
   327 by (etac lemma 1);
   328 by (assume_tac 1);
   329 qed "card_insert_disjoint";
   330 Addsimps [card_insert_disjoint];
   331 
   332 goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
   333 by (etac finite_induct 1);
   334 by (Simp_tac 1);
   335 by (Clarify_tac 1);
   336 by (case_tac "x:B" 1);
   337  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
   338  by (SELECT_GOAL Safe_tac 1);
   339  by (rotate_tac ~1 1);
   340  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
   341 by (rotate_tac ~1 1);
   342 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
   343 qed_spec_mp "card_mono";
   344 
   345 goal Finite.thy "!!A B. [| finite A; finite B |]\
   346 \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
   347 by (etac finite_induct 1);
   348 by (ALLGOALS 
   349     (asm_simp_tac (simpset() addsimps [Int_insert_left]
   350 	                    addsplits [expand_if])));
   351 qed_spec_mp "card_Un_disjoint";
   352 
   353 goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
   354 by (subgoal_tac "(A-B) Un B = A" 1);
   355 by (Blast_tac 2);
   356 by (rtac (add_right_cancel RS iffD1) 1);
   357 by (rtac (card_Un_disjoint RS subst) 1);
   358 by (etac ssubst 4);
   359 by (Blast_tac 3);
   360 by (ALLGOALS 
   361     (asm_simp_tac
   362      (simpset() addsimps [add_commute, not_less_iff_le, 
   363 			 add_diff_inverse, card_mono, finite_subset])));
   364 qed "card_Diff_subset";
   365 
   366 goal Finite.thy "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
   367 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
   368 by (assume_tac 1);
   369 by (Asm_simp_tac 1);
   370 qed "card_Suc_Diff";
   371 
   372 goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
   373 by (rtac Suc_less_SucD 1);
   374 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
   375 qed "card_Diff";
   376 
   377 
   378 (*** Cardinality of the Powerset ***)
   379 
   380 val [major] = goal Finite.thy
   381   "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   382 by (case_tac "x:A" 1);
   383 by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   384 by (dtac mk_disjoint_insert 1);
   385 by (etac exE 1);
   386 by (Asm_simp_tac 1);
   387 by (rtac card_insert_disjoint 1);
   388 by (rtac (major RSN (2,finite_subset)) 1);
   389 by (Blast_tac 1);
   390 by (Blast_tac 1);
   391 by (asm_simp_tac (simpset() addsimps [major RS card_insert_disjoint]) 1);
   392 qed "card_insert";
   393 Addsimps [card_insert];
   394 
   395 goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
   396 by (etac finite_induct 1);
   397 by (ALLGOALS Asm_simp_tac);
   398 by Safe_tac;
   399 by (rewtac inj_onto_def);
   400 by (Blast_tac 1);
   401 by (stac card_insert_disjoint 1);
   402 by (etac finite_imageI 1);
   403 by (Blast_tac 1);
   404 by (Blast_tac 1);
   405 qed_spec_mp "card_image";
   406 
   407 goal thy "!!A. finite A ==> card (Pow A) = 2 ^ card A";
   408 by (etac finite_induct 1);
   409 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
   410 by (stac card_Un_disjoint 1);
   411 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
   412 by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
   413 by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
   414 by (rewtac inj_onto_def);
   415 by (blast_tac (claset() addSEs [equalityE]) 1);
   416 qed "card_Pow";
   417 Addsimps [card_Pow];
   418 
   419 
   420 (*Proper subsets*)
   421 goalw Finite.thy [psubset_def]
   422 "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
   423 by (etac finite_induct 1);
   424 by (Simp_tac 1);
   425 by (Clarify_tac 1);
   426 by (case_tac "x:A" 1);
   427 (*1*)
   428 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
   429 by (etac exE 1);
   430 by (etac conjE 1);
   431 by (hyp_subst_tac 1);
   432 by (rotate_tac ~1 1);
   433 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
   434 by (Blast_tac 1);
   435 (*2*)
   436 by (rotate_tac ~1 1);
   437 by (eres_inst_tac [("P","?a<?b")] notE 1);
   438 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
   439 by (case_tac "A=F" 1);
   440 by (ALLGOALS Asm_simp_tac);
   441 qed_spec_mp "psubset_card" ;
   442 
   443 
   444 (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   445   The "finite C" premise is redundant*)
   446 goal thy "!!C. finite C ==> finite (Union C) --> \
   447 \          (! c : C. k dvd card c) -->  \
   448 \          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
   449 \          --> k dvd card(Union C)";
   450 by (etac finite_induct 1);
   451 by (ALLGOALS Asm_simp_tac);
   452 by (Clarify_tac 1);
   453 by (stac card_Un_disjoint 1);
   454 by (ALLGOALS
   455     (asm_full_simp_tac (simpset()
   456 			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
   457 by (thin_tac "!c:F. ?PP(c)" 1);
   458 by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
   459 by (Clarify_tac 1);
   460 by (ball_tac 1);
   461 by (Blast_tac 1);
   462 qed_spec_mp "dvd_partition";
   463