src/HOL/Finite.ML
author oheimb
Mon Sep 06 18:19:12 1999 +0200 (1999-09-06)
changeset 7497 a18f3bce7198
parent 6162 484adda70b65
child 7499 23e090051cb8
permissions -rw-r--r--
strengthened card_seteq
     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 section "finite";
    10 
    11 (*Discharging ~ x:y entails extra work*)
    12 val major::prems = Goal 
    13     "[| finite F;  P({}); \
    14 \       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
    15 \    |] ==> P(F)";
    16 by (rtac (major RS Finites.induct) 1);
    17 by (excluded_middle_tac "a:A" 2);
    18 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
    19 by (REPEAT (ares_tac prems 1));
    20 qed "finite_induct";
    21 
    22 val major::subs::prems = Goal 
    23     "[| finite F;  F <= A; \
    24 \       P({}); \
    25 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    26 \    |] ==> P(F)";
    27 by (rtac (subs RS rev_mp) 1);
    28 by (rtac (major RS finite_induct) 1);
    29 by (ALLGOALS (blast_tac (claset() addIs prems)));
    30 qed "finite_subset_induct";
    31 
    32 Addsimps Finites.intrs;
    33 AddSIs Finites.intrs;
    34 
    35 (*The union of two finite sets is finite*)
    36 Goal "[| finite F;  finite G |] ==> finite(F Un G)";
    37 by (etac finite_induct 1);
    38 by (ALLGOALS Asm_simp_tac);
    39 qed "finite_UnI";
    40 
    41 (*Every subset of a finite set is finite*)
    42 Goal "finite B ==> ALL A. A<=B --> finite A";
    43 by (etac finite_induct 1);
    44 by (Simp_tac 1);
    45 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
    46 by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2);
    47 by (ALLGOALS Asm_simp_tac);
    48 val lemma = result();
    49 
    50 Goal "[| A<=B;  finite B |] ==> finite A";
    51 by (dtac lemma 1);
    52 by (Blast_tac 1);
    53 qed "finite_subset";
    54 
    55 Goal "finite(F Un G) = (finite F & finite G)";
    56 by (blast_tac (claset() 
    57 	         addIs [read_instantiate [("B", "?X Un ?Y")] finite_subset, 
    58 			finite_UnI]) 1);
    59 qed "finite_Un";
    60 AddIffs[finite_Un];
    61 
    62 Goal "finite F ==> finite(F Int G)";
    63 by (blast_tac (claset() addIs [finite_subset]) 1);
    64 qed "finite_Int1";
    65 
    66 Goal "finite G ==> finite(F Int G)";
    67 by (blast_tac (claset() addIs [finite_subset]) 1);
    68 qed "finite_Int2";
    69 
    70 Addsimps[finite_Int1, finite_Int2];
    71 AddIs[finite_Int1, finite_Int2];
    72 
    73 
    74 Goal "finite(insert a A) = finite A";
    75 by (stac insert_is_Un 1);
    76 by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
    77 by (Blast_tac 1);
    78 qed "finite_insert";
    79 Addsimps[finite_insert];
    80 
    81 (*The image of a finite set is finite *)
    82 Goal  "finite F ==> finite(h``F)";
    83 by (etac finite_induct 1);
    84 by (Simp_tac 1);
    85 by (Asm_simp_tac 1);
    86 qed "finite_imageI";
    87 
    88 val major::prems = Goal 
    89     "[| finite c;  finite b;                                  \
    90 \       P(b);                                                   \
    91 \       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
    92 \    |] ==> c<=b --> P(b-c)";
    93 by (rtac (major RS finite_induct) 1);
    94 by (stac Diff_insert 2);
    95 by (ALLGOALS (asm_simp_tac
    96                 (simpset() addsimps prems@[Diff_subset RS finite_subset])));
    97 val lemma = result();
    98 
    99 val prems = Goal 
   100     "[| finite A;                                       \
   101 \       P(A);                                           \
   102 \       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   103 \    |] ==> P({})";
   104 by (rtac (Diff_cancel RS subst) 1);
   105 by (rtac (lemma RS mp) 1);
   106 by (REPEAT (ares_tac (subset_refl::prems) 1));
   107 qed "finite_empty_induct";
   108 
   109 
   110 (* finite B ==> finite (B - Ba) *)
   111 bind_thm ("finite_Diff", Diff_subset RS finite_subset);
   112 Addsimps [finite_Diff];
   113 
   114 Goal "finite(A - insert a B) = finite(A-B)";
   115 by (stac Diff_insert 1);
   116 by (case_tac "a : A-B" 1);
   117 by (rtac (finite_insert RS sym RS trans) 1);
   118 by (stac insert_Diff 1);
   119 by (ALLGOALS Asm_full_simp_tac);
   120 qed "finite_Diff_insert";
   121 AddIffs [finite_Diff_insert];
   122 
   123 (* lemma merely for classical reasoner *)
   124 Goal "finite(A-{}) = finite A";
   125 by (Simp_tac 1);
   126 val lemma = result();
   127 AddSIs [lemma RS iffD2];
   128 AddSDs [lemma RS iffD1];
   129 
   130 (*Lemma for proving finite_imageD*)
   131 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A";
   132 by (etac finite_induct 1);
   133  by (ALLGOALS Asm_simp_tac);
   134 by (Clarify_tac 1);
   135 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
   136  by (Clarify_tac 1);
   137  by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
   138  by (Blast_tac 1);
   139 by (thin_tac "ALL A. ?PP(A)" 1);
   140 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
   141 by (Clarify_tac 1);
   142 by (res_inst_tac [("x","xa")] bexI 1);
   143 by (ALLGOALS 
   144     (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
   145 val lemma = result();
   146 
   147 Goal "[| finite(f``A);  inj_on f A |] ==> finite A";
   148 by (dtac lemma 1);
   149 by (Blast_tac 1);
   150 qed "finite_imageD";
   151 
   152 (** The finite UNION of finite sets **)
   153 
   154 Goal "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
   155 by (etac finite_induct 1);
   156 by (ALLGOALS Asm_simp_tac);
   157 bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
   158 Addsimps [finite_UnionI];
   159 
   160 (** Sigma of finite sets **)
   161 
   162 Goalw [Sigma_def]
   163  "[| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
   164 by (blast_tac (claset() addSIs [finite_UnionI]) 1);
   165 bind_thm("finite_SigmaI", ballI RSN (2,result()));
   166 Addsimps [finite_SigmaI];
   167 
   168 (** The powerset of a finite set **)
   169 
   170 Goal "finite(Pow A) ==> finite A";
   171 by (subgoal_tac "finite ((%x.{x})``A)" 1);
   172 by (rtac finite_subset 2);
   173 by (assume_tac 3);
   174 by (ALLGOALS
   175     (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
   176 val lemma = result();
   177 
   178 Goal "finite(Pow A) = finite A";
   179 by (rtac iffI 1);
   180 by (etac lemma 1);
   181 (*Opposite inclusion: finite A ==> finite (Pow A) *)
   182 by (etac finite_induct 1);
   183 by (ALLGOALS 
   184     (asm_simp_tac
   185      (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert])));
   186 qed "finite_Pow_iff";
   187 AddIffs [finite_Pow_iff];
   188 
   189 Goal "finite(r^-1) = finite r";
   190 by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
   191  by (Asm_simp_tac 1);
   192  by (rtac iffI 1);
   193   by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
   194   by (simp_tac (simpset() addsplits [split_split]) 1);
   195  by (etac finite_imageI 1);
   196 by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
   197 by Auto_tac;
   198 by (rtac bexI 1);
   199 by  (assume_tac 2);
   200 by (Simp_tac 1);
   201 qed "finite_converse";
   202 AddIffs [finite_converse];
   203 
   204 section "Finite cardinality -- 'card'";
   205 
   206 (* Ugly proofs for the traditional definition 
   207 
   208 Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
   209 by (Blast_tac 1);
   210 val Collect_conv_insert = result();
   211 
   212 Goalw [card_def] "card {} = 0";
   213 by (rtac Least_equality 1);
   214 by (ALLGOALS Asm_full_simp_tac);
   215 qed "card_empty";
   216 Addsimps [card_empty];
   217 
   218 Goal "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
   219 by (etac finite_induct 1);
   220  by (res_inst_tac [("x","0")] exI 1);
   221  by (Simp_tac 1);
   222 by (etac exE 1);
   223 by (etac exE 1);
   224 by (hyp_subst_tac 1);
   225 by (res_inst_tac [("x","Suc n")] exI 1);
   226 by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
   227 by (asm_simp_tac (simpset() addsimps [Collect_conv_insert, less_Suc_eq]
   228                           addcongs [rev_conj_cong]) 1);
   229 qed "finite_has_card";
   230 
   231 Goal "[| x ~: A; insert x A = {f i|i. i<n} |]  \
   232 \     ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
   233 by (exhaust_tac "n" 1);
   234  by (hyp_subst_tac 1);
   235  by (Asm_full_simp_tac 1);
   236 by (rename_tac "m" 1);
   237 by (hyp_subst_tac 1);
   238 by (case_tac "? a. a:A" 1);
   239  by (res_inst_tac [("x","0")] exI 2);
   240  by (Simp_tac 2);
   241  by (Blast_tac 2);
   242 by (etac exE 1);
   243 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   244 by (rtac exI 1);
   245 by (rtac (refl RS disjI2 RS conjI) 1);
   246 by (etac equalityE 1);
   247 by (asm_full_simp_tac
   248      (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
   249 by Safe_tac;
   250   by (Asm_full_simp_tac 1);
   251   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   252   by (SELECT_GOAL Safe_tac 1);
   253    by (subgoal_tac "x ~= f m" 1);
   254     by (Blast_tac 2);
   255    by (subgoal_tac "? k. f k = x & k<m" 1);
   256     by (Blast_tac 2);
   257    by (SELECT_GOAL Safe_tac 1);
   258    by (res_inst_tac [("x","k")] exI 1);
   259    by (Asm_simp_tac 1);
   260   by (Simp_tac 1);
   261   by (Blast_tac 1);
   262  by (dtac sym 1);
   263  by (rotate_tac ~1 1);
   264  by (Asm_full_simp_tac 1);
   265  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   266  by (SELECT_GOAL Safe_tac 1);
   267   by (subgoal_tac "x ~= f m" 1);
   268    by (Blast_tac 2);
   269   by (subgoal_tac "? k. f k = x & k<m" 1);
   270    by (Blast_tac 2);
   271   by (SELECT_GOAL Safe_tac 1);
   272   by (res_inst_tac [("x","k")] exI 1);
   273   by (Asm_simp_tac 1);
   274  by (Simp_tac 1);
   275  by (Blast_tac 1);
   276 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   277 by (SELECT_GOAL Safe_tac 1);
   278  by (subgoal_tac "x ~= f i" 1);
   279   by (Blast_tac 2);
   280  by (case_tac "x = f m" 1);
   281   by (res_inst_tac [("x","i")] exI 1);
   282   by (Asm_simp_tac 1);
   283  by (subgoal_tac "? k. f k = x & k<m" 1);
   284   by (Blast_tac 2);
   285  by (SELECT_GOAL Safe_tac 1);
   286  by (res_inst_tac [("x","k")] exI 1);
   287  by (Asm_simp_tac 1);
   288 by (Simp_tac 1);
   289 by (Blast_tac 1);
   290 val lemma = result();
   291 
   292 Goal "[| finite A; x ~: A |] ==> \
   293 \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
   294 by (rtac Least_equality 1);
   295  by (dtac finite_has_card 1);
   296  by (etac exE 1);
   297  by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1);
   298  by (etac exE 1);
   299  by (res_inst_tac
   300    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
   301  by (simp_tac
   302     (simpset() addsimps [Collect_conv_insert, less_Suc_eq] 
   303               addcongs [rev_conj_cong]) 1);
   304  by (etac subst 1);
   305  by (rtac refl 1);
   306 by (rtac notI 1);
   307 by (etac exE 1);
   308 by (dtac lemma 1);
   309  by (assume_tac 1);
   310 by (etac exE 1);
   311 by (etac conjE 1);
   312 by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   313 by (dtac le_less_trans 1 THEN atac 1);
   314 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   315 by (etac disjE 1);
   316 by (etac less_asym 1 THEN atac 1);
   317 by (hyp_subst_tac 1);
   318 by (Asm_full_simp_tac 1);
   319 val lemma = result();
   320 
   321 Goalw [card_def] "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
   322 by (etac lemma 1);
   323 by (assume_tac 1);
   324 qed "card_insert_disjoint";
   325 Addsimps [card_insert_disjoint];
   326 *)
   327 
   328 val cardR_emptyE = cardR.mk_cases "({},n) : cardR";
   329 AddSEs [cardR_emptyE];
   330 val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR";
   331 AddSIs cardR.intrs;
   332 
   333 Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
   334 by (etac cardR.induct 1);
   335  by (Blast_tac 1);
   336 by (Blast_tac 1);
   337 qed "cardR_SucD";
   338 
   339 Goal "(A,m): cardR ==> (!n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
   340 by (etac cardR.induct 1);
   341  by (Auto_tac);
   342 by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
   343 by (Auto_tac);
   344 by (forward_tac [cardR_SucD] 1);
   345 by (Blast_tac 1);
   346 val lemma = result();
   347 
   348 Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
   349 by (dtac lemma 1);
   350 by (Asm_full_simp_tac 1);
   351 val lemma = result();
   352 
   353 Goal "(A,m): cardR ==> (!n. (A,n) : cardR --> n=m)";
   354 by (etac cardR.induct 1);
   355  by (safe_tac (claset() addSEs [cardR_insertE]));
   356 by (rename_tac "B b m" 1);
   357 by (case_tac "a = b" 1);
   358  by (subgoal_tac "A = B" 1);
   359   by (blast_tac (claset() addEs [equalityE]) 2);
   360  by (Blast_tac 1);
   361 by (subgoal_tac "? C. A = insert b C & B = insert a C" 1);
   362  by (res_inst_tac [("x","A Int B")] exI 2);
   363  by (blast_tac (claset() addEs [equalityE]) 2);
   364 by (forw_inst_tac [("A","B")] cardR_SucD 1);
   365 by (blast_tac (claset() addDs [lemma]) 1);
   366 qed_spec_mp "cardR_determ";
   367 
   368 Goal "(A,n) : cardR ==> finite(A)";
   369 by (etac cardR.induct 1);
   370 by Auto_tac;
   371 qed "cardR_imp_finite";
   372 
   373 Goal "finite(A) ==> EX n. (A, n) : cardR";
   374 by (etac finite_induct 1);
   375 by Auto_tac;
   376 qed "finite_imp_cardR";
   377 
   378 Goalw [card_def] "(A,n) : cardR ==> card A = n";
   379 by (blast_tac (claset() addIs [cardR_determ]) 1);
   380 qed "card_equality";
   381 
   382 Goalw [card_def] "card {} = 0";
   383 by (Blast_tac 1);
   384 qed "card_empty";
   385 Addsimps [card_empty];
   386 
   387 Goal "x ~: A ==> \
   388 \     ((insert x A, n) : cardR) =  \
   389 \     (EX m. (A, m) : cardR & n = Suc m)";
   390 by Auto_tac;
   391 by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1);
   392 by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1);
   393 by (blast_tac (claset() addIs [cardR_determ]) 1);
   394 val lemma = result();
   395 
   396 Goalw [card_def]
   397      "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
   398 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
   399 by (rtac select_equality 1);
   400 by (auto_tac (claset() addIs [finite_imp_cardR],
   401 	      simpset() addcongs [conj_cong]
   402 		        addsimps [symmetric card_def,
   403 				  card_equality]));
   404 qed "card_insert_disjoint";
   405 Addsimps [card_insert_disjoint];
   406 
   407 (* Delete rules to do with cardR relation: obsolete *)
   408 Delrules [cardR_emptyE];
   409 Delrules cardR.intrs;
   410 
   411 Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))";
   412 by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   413 qed "card_insert_if";
   414 
   415 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
   416 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
   417 by (assume_tac 1);
   418 by (Asm_simp_tac 1);
   419 qed "card_Suc_Diff1";
   420 
   421 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   422 by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1);
   423 qed "card_insert";
   424 
   425 Goal "finite A ==> card A <= card (insert x A)";
   426 by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1);
   427 qed "card_insert_le";
   428 
   429 Goal  "finite A ==> !B. B <= A --> card(B) <= card(A)";
   430 by (etac finite_induct 1);
   431 by (Simp_tac 1);
   432 by (Clarify_tac 1);
   433 by (case_tac "x:B" 1);
   434  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
   435  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
   436 by (fast_tac (claset() addss
   437 	      (simpset() addsimps [subset_insert_iff, finite_subset]
   438 			 delsimps [insert_subset])) 1);
   439 qed_spec_mp "card_mono";
   440 
   441 
   442 Goal "[| finite A; finite B |] \
   443 \     ==> card A + card B = card (A Un B) + card (A Int B)";
   444 by (etac finite_induct 1);
   445 by (Simp_tac 1);
   446 by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1);
   447 qed "card_Un_Int";
   448 
   449 Goal "[| finite A; finite B; A Int B = {} |] \
   450 \     ==> card (A Un B) = card A + card B";
   451 by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1);
   452 qed "card_Un_disjoint";
   453 
   454 Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
   455 by (subgoal_tac "(A-B) Un B = A" 1);
   456 by (Blast_tac 2);
   457 by (rtac (add_right_cancel RS iffD1) 1);
   458 by (rtac (card_Un_disjoint RS subst) 1);
   459 by (etac ssubst 4);
   460 by (Blast_tac 3);
   461 by (ALLGOALS 
   462     (asm_simp_tac
   463      (simpset() addsimps [add_commute, not_less_iff_le, 
   464 			  add_diff_inverse, card_mono, finite_subset])));
   465 qed "card_Diff_subset";
   466 
   467 Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
   468 by (rtac Suc_less_SucD 1);
   469 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
   470 qed "card_Diff1_less";
   471 
   472 Goal "finite A ==> card(A-{x}) <= card A";
   473 by (case_tac "x: A" 1);
   474 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le])));
   475 qed "card_Diff1_le";
   476 
   477 Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)";
   478 by (etac finite_induct 1);
   479 by (Simp_tac 1);
   480 by (Clarify_tac 1);
   481 by (case_tac "x:A" 1);
   482 (*1*)
   483 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
   484 by (Clarify_tac 1);
   485 by (rotate_tac ~3 1);
   486 by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1);
   487 by (Blast_tac 1);
   488 (*2*)
   489 by (eres_inst_tac [("P","?a<?b")] notE 1);
   490 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
   491 by (case_tac "A=F" 1);
   492 by (ALLGOALS Asm_simp_tac);
   493 qed_spec_mp "psubset_card" ;
   494 
   495 Goal "!!X. [| A <= B; card B <= card A; finite B |] ==> A = B";
   496 by (case_tac "A < B" 1);
   497 by (datac psubset_card 1 1);
   498 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [psubset_eq])));
   499 qed "card_seteq";
   500 
   501 Goal "[| finite B; A <= B; card A < card B |] ==> A < B";
   502 by (etac psubsetI 1);
   503 by (Blast_tac 1);
   504 qed "card_psubset";
   505 
   506 (*** Cardinality of image ***)
   507 
   508 Goal "finite A ==> card (f `` A) <= card A";
   509 by (etac finite_induct 1);
   510 by (Simp_tac 1);
   511 by (asm_simp_tac (simpset() addsimps [finite_imageI,card_insert_if]) 1);
   512 qed "card_image_le";
   513 
   514 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
   515 by (etac finite_induct 1);
   516 by (ALLGOALS Asm_simp_tac);
   517 by Safe_tac;
   518 by (rewtac inj_on_def);
   519 by (Blast_tac 1);
   520 by (stac card_insert_disjoint 1);
   521 by (etac finite_imageI 1);
   522 by (Blast_tac 1);
   523 by (Blast_tac 1);
   524 qed_spec_mp "card_image";
   525 
   526 Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A";
   527 by (etac card_seteq 1);
   528 by (dtac (card_image RS sym) 1);
   529 by Auto_tac;
   530 qed "endo_inj_surj";
   531 
   532 (*** Cardinality of the Powerset ***)
   533 
   534 Goal "finite A ==> card (Pow A) = 2 ^ card A";
   535 by (etac finite_induct 1);
   536 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
   537 by (stac card_Un_disjoint 1);
   538 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
   539 by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
   540 by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
   541 by (rewtac inj_on_def);
   542 by (blast_tac (claset() addSEs [equalityE]) 1);
   543 qed "card_Pow";
   544 Addsimps [card_Pow];
   545 
   546 
   547 (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   548   The "finite C" premise is redundant*)
   549 Goal "finite C ==> finite (Union C) --> \
   550 \          (! c : C. k dvd card c) -->  \
   551 \          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
   552 \          --> k dvd card(Union C)";
   553 by (etac finite_induct 1);
   554 by (ALLGOALS Asm_simp_tac);
   555 by (Clarify_tac 1);
   556 by (stac card_Un_disjoint 1);
   557 by (ALLGOALS
   558     (asm_full_simp_tac (simpset()
   559 			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
   560 by (thin_tac "!c:F. ?PP(c)" 1);
   561 by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
   562 by (Clarify_tac 1);
   563 by (ball_tac 1);
   564 by (Blast_tac 1);
   565 qed_spec_mp "dvd_partition";
   566 
   567 
   568 (*** foldSet ***)
   569 
   570 val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e";
   571 
   572 AddSEs [empty_foldSetE];
   573 AddIs foldSet.intrs;
   574 
   575 Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
   576 by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
   577 by Auto_tac;
   578 qed "Diff1_foldSet";
   579 
   580 Goal "(A, x) : foldSet f e ==> finite(A)";
   581 by (eresolve_tac [foldSet.induct] 1);
   582 by Auto_tac;
   583 qed "foldSet_imp_finite";
   584 
   585 Addsimps [foldSet_imp_finite];
   586 
   587 
   588 Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
   589 by (etac finite_induct 1);
   590 by Auto_tac;
   591 qed "finite_imp_foldSet";
   592 
   593 
   594 Open_locale "LC"; 
   595 
   596 val f_lcomm = thm "lcomm";
   597 
   598 
   599 Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
   600 \            (ALL y. (A, y) : foldSet f e --> y=x)";
   601 by (induct_tac "n" 1);
   602 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
   603 by (etac foldSet.elim 1);
   604 by (Blast_tac 1);
   605 by (etac foldSet.elim 1);
   606 by (Blast_tac 1);
   607 by (Clarify_tac 1);
   608 (*force simplification of "card A < card (insert ...)"*)
   609 by (etac rev_mp 1);
   610 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
   611 by (rtac impI 1);
   612 (** LEVEL 10 **)
   613 by (rename_tac "Aa xa ya Ab xb yb" 1);
   614  by (case_tac "xa=xb" 1);
   615  by (subgoal_tac "Aa = Ab" 1);
   616  by (blast_tac (claset() addEs [equalityE]) 2);
   617  by (Blast_tac 1);
   618 (*case xa ~= xb*)
   619 by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
   620  by (blast_tac (claset() addEs [equalityE]) 2);
   621 by (Clarify_tac 1);
   622 by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
   623  by (blast_tac (claset() addEs [equalityE]) 2);
   624 (** LEVEL 20 **)
   625 by (subgoal_tac "card Aa <= card Ab" 1);
   626  by (rtac (Suc_le_mono RS subst) 2);
   627  by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2);
   628 by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
   629     (finite_imp_foldSet RS exE) 1);
   630 by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
   631 by (forward_tac [Diff1_foldSet] 1 THEN assume_tac 1);
   632 by (subgoal_tac "ya = f xb x" 1);
   633  by (Blast_tac 2);
   634 by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
   635  by (Asm_full_simp_tac 2);
   636 by (subgoal_tac "yb = f xa x" 1);
   637  by (blast_tac (claset() addDs [Diff1_foldSet]) 2);
   638 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
   639 val lemma = result();
   640 
   641 
   642 Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
   643 by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
   644 qed "foldSet_determ";
   645 
   646 Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
   647 by (blast_tac (claset() addIs [foldSet_determ]) 1);
   648 qed "fold_equality";
   649 
   650 Goalw [fold_def] "fold f e {} = e";
   651 by (Blast_tac 1);
   652 qed "fold_empty";
   653 Addsimps [fold_empty];
   654 
   655 
   656 Goal "x ~: A ==> \
   657 \     ((insert x A, v) : foldSet f e) =  \
   658 \     (EX y. (A, y) : foldSet f e & v = f x y)";
   659 by Auto_tac;
   660 by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
   661 by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
   662 by (blast_tac (claset() addIs [foldSet_determ]) 1);
   663 val lemma = result();
   664 
   665 Goalw [fold_def]
   666      "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
   667 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
   668 by (rtac select_equality 1);
   669 by (auto_tac (claset() addIs [finite_imp_foldSet],
   670 	      simpset() addcongs [conj_cong]
   671 		        addsimps [symmetric fold_def,
   672 				  fold_equality]));
   673 qed "fold_insert";
   674 
   675 (* Delete rules to do with foldSet relation: obsolete *)
   676 Delsimps [foldSet_imp_finite];
   677 Delrules [empty_foldSetE];
   678 Delrules foldSet.intrs;
   679 
   680 Close_locale "LC";
   681 
   682 Open_locale "ACe"; 
   683 
   684 val f_ident   = thm "ident";
   685 val f_commute = thm "commute";
   686 val f_assoc   = thm "assoc";
   687 
   688 
   689 Goal "f x (f y z) = f y (f x z)";
   690 by (rtac (f_commute RS trans) 1);
   691 by (rtac (f_assoc RS trans) 1);
   692 by (rtac (f_commute RS arg_cong) 1);
   693 qed "f_left_commute";
   694 
   695 val f_ac = [f_assoc, f_commute, f_left_commute];
   696 
   697 Goal "f e x = x";
   698 by (stac f_commute 1);
   699 by (rtac f_ident 1);
   700 qed "f_left_ident";
   701 
   702 val f_idents = [f_left_ident, f_ident];
   703 
   704 Goal "[| finite A; finite B |] \
   705 \     ==> f (fold f e A) (fold f e B) =  \
   706 \         f (fold f e (A Un B)) (fold f e (A Int B))";
   707 by (etac finite_induct 1);
   708 by (simp_tac (simpset() addsimps f_idents) 1);
   709 by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @
   710            [export fold_insert,insert_absorb, Int_insert_left]) 1);
   711 qed "fold_Un_Int";
   712 
   713 Goal "[| finite A; finite B; A Int B = {} |] \
   714 \     ==> fold f e (A Un B) = f (fold f e A) (fold f e B)";
   715 by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1);
   716 qed "fold_Un_disjoint";
   717 
   718 Goal
   719  "[| finite A; finite B |] ==> A Int B = {} --> \
   720 \ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)";
   721 by (etac finite_induct 1);
   722 by (simp_tac (simpset() addsimps f_idents) 1);
   723 by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @
   724            [export fold_insert,insert_absorb, Int_insert_left]) 1);
   725 qed "fold_Un_disjoint2";
   726 
   727 Close_locale "ACe";
   728 
   729 Delrules ([empty_foldSetE] @ foldSet.intrs);
   730 Delsimps [foldSet_imp_finite];
   731 
   732 (*** setsum ***)
   733 
   734 Goalw [setsum_def] "setsum f {} = 0";
   735 by (Simp_tac 1);
   736 qed "setsum_empty";
   737 Addsimps [setsum_empty];
   738 
   739 Goalw [setsum_def]
   740  "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
   741 by (asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
   742 qed "setsum_insert";
   743 Addsimps [setsum_insert];
   744 
   745 Goalw [setsum_def]
   746  "[| finite A; finite B; A Int B = {} |] ==> \
   747 \ setsum f (A Un B) = setsum f A + setsum f B";
   748 by (asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
   749 qed_spec_mp "setsum_disj_Un";
   750 
   751 Goal "[| finite F |] ==> \
   752 \     setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
   753 by (etac finite_induct 1);
   754 by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
   755 by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   756 by (Auto_tac);
   757 qed_spec_mp "setsum_diff1";