src/HOL/Finite.ML
author paulson
Fri Dec 11 10:41:53 1998 +0100 (1998-12-11)
changeset 6024 cb87f103d114
parent 5782 7559f116cb10
child 6141 a6922171b396
permissions -rw-r--r--
new Close_locale synatx
     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 be 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 be 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 bd 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 be 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 "[| finite B; A <= B; card A = card B |] ==> A = B";
   496 by (case_tac "A < B" 1);
   497 by ((dtac psubset_card 1) THEN (atac 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 (REPEAT (ares_tac [card_seteq,card_image] 1));
   528 qed "endo_inj_surj";
   529 
   530 (*** Cardinality of the Powerset ***)
   531 
   532 Goal "finite A ==> card (Pow A) = 2 ^ card A";
   533 by (etac finite_induct 1);
   534 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
   535 by (stac card_Un_disjoint 1);
   536 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
   537 by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
   538 by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
   539 by (rewtac inj_on_def);
   540 by (blast_tac (claset() addSEs [equalityE]) 1);
   541 qed "card_Pow";
   542 Addsimps [card_Pow];
   543 
   544 
   545 (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   546   The "finite C" premise is redundant*)
   547 Goal "finite C ==> finite (Union C) --> \
   548 \          (! c : C. k dvd card c) -->  \
   549 \          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
   550 \          --> k dvd card(Union C)";
   551 by (etac finite_induct 1);
   552 by (ALLGOALS Asm_simp_tac);
   553 by (Clarify_tac 1);
   554 by (stac card_Un_disjoint 1);
   555 by (ALLGOALS
   556     (asm_full_simp_tac (simpset()
   557 			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
   558 by (thin_tac "!c:F. ?PP(c)" 1);
   559 by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
   560 by (Clarify_tac 1);
   561 by (ball_tac 1);
   562 by (Blast_tac 1);
   563 qed_spec_mp "dvd_partition";
   564 
   565 
   566 (*** foldSet ***)
   567 
   568 val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
   569 
   570 AddSEs [empty_foldSetE];
   571 AddIs foldSet.intrs;
   572 
   573 Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
   574 by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
   575 by Auto_tac;
   576 qed "Diff1_foldSet";
   577 
   578 Goal "(A, x) : foldSet f e ==> finite(A)";
   579 by (eresolve_tac [foldSet.induct] 1);
   580 by Auto_tac;
   581 qed "foldSet_imp_finite";
   582 
   583 Addsimps [foldSet_imp_finite];
   584 
   585 
   586 Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
   587 by (etac finite_induct 1);
   588 by Auto_tac;
   589 qed "finite_imp_foldSet";
   590 
   591 
   592 Open_locale "LC"; 
   593 
   594 val f_lcomm = thm "lcomm";
   595 
   596 
   597 Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
   598 \            (ALL y. (A, y) : foldSet f e --> y=x)";
   599 by (induct_tac "n" 1);
   600 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
   601 by (etac foldSet.elim 1);
   602 by (Blast_tac 1);
   603 by (etac foldSet.elim 1);
   604 by (Blast_tac 1);
   605 by (Clarify_tac 1);
   606 (*force simplification of "card A < card (insert ...)"*)
   607 by (etac rev_mp 1);
   608 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
   609 by (rtac impI 1);
   610 (** LEVEL 10 **)
   611 by (rename_tac "Aa xa ya Ab xb yb" 1);
   612  by (case_tac "xa=xb" 1);
   613  by (subgoal_tac "Aa = Ab" 1);
   614  by (blast_tac (claset() addEs [equalityE]) 2);
   615  by (Blast_tac 1);
   616 (*case xa ~= xb*)
   617 by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
   618  by (blast_tac (claset() addEs [equalityE]) 2);
   619 by (Clarify_tac 1);
   620 by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
   621  by (blast_tac (claset() addEs [equalityE]) 2);
   622 (** LEVEL 20 **)
   623 by (subgoal_tac "card Aa <= card Ab" 1);
   624  by (rtac (Suc_le_mono RS subst) 2);
   625  by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2);
   626 by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
   627     (finite_imp_foldSet RS exE) 1);
   628 by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
   629 by (forward_tac [Diff1_foldSet] 1 THEN assume_tac 1);
   630 by (subgoal_tac "ya = f xb x" 1);
   631  by (Blast_tac 2);
   632 by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
   633  by (Asm_full_simp_tac 2);
   634 by (subgoal_tac "yb = f xa x" 1);
   635  by (blast_tac (claset() addDs [Diff1_foldSet]) 2);
   636 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
   637 val lemma = result();
   638 
   639 
   640 Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
   641 by (blast_tac (claset() addIs [normalize_thm [RSspec, RSmp] lemma]) 1);
   642 qed "foldSet_determ";
   643 
   644 Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
   645 by (blast_tac (claset() addIs [foldSet_determ]) 1);
   646 qed "fold_equality";
   647 
   648 Goalw [fold_def] "fold f e {} = e";
   649 by (Blast_tac 1);
   650 qed "fold_empty";
   651 Addsimps [fold_empty];
   652 
   653 
   654 Goal "x ~: A ==> \
   655 \     ((insert x A, v) : foldSet f e) =  \
   656 \     (EX y. (A, y) : foldSet f e & v = f x y)";
   657 by Auto_tac;
   658 by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
   659 by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
   660 by (blast_tac (claset() addIs [foldSet_determ]) 1);
   661 val lemma = result();
   662 
   663 Goalw [fold_def]
   664      "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
   665 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
   666 by (rtac select_equality 1);
   667 by (auto_tac (claset() addIs [finite_imp_foldSet],
   668 	      simpset() addcongs [conj_cong]
   669 		        addsimps [symmetric fold_def,
   670 				  fold_equality]));
   671 qed "fold_insert";
   672 
   673 (* Delete rules to do with foldSet relation: obsolete *)
   674 Delsimps [foldSet_imp_finite];
   675 Delrules [empty_foldSetE];
   676 Delrules foldSet.intrs;
   677 
   678 Close_locale "LC";
   679 
   680 Open_locale "ACe"; 
   681 
   682 val f_ident   = thm "ident";
   683 val f_commute = thm "commute";
   684 val f_assoc   = thm "assoc";
   685 
   686 
   687 Goal "f x (f y z) = f y (f x z)";
   688 by (rtac (f_commute RS trans) 1);
   689 by (rtac (f_assoc RS trans) 1);
   690 by (rtac (f_commute RS arg_cong) 1);
   691 qed "f_left_commute";
   692 
   693 val f_ac = [f_assoc, f_commute, f_left_commute];
   694 
   695 Goal "f e x = x";
   696 by (stac f_commute 1);
   697 by (rtac f_ident 1);
   698 qed "f_left_ident";
   699 
   700 val f_idents = [f_left_ident, f_ident];
   701 
   702 Goal "[| finite A; finite B |] \
   703 \     ==> f (fold f e A) (fold f e B) =  \
   704 \         f (fold f e (A Un B)) (fold f e (A Int B))";
   705 by (etac finite_induct 1);
   706 by (simp_tac (simpset() addsimps f_idents) 1);
   707 by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @
   708            [export fold_insert,insert_absorb, Int_insert_left]) 1);
   709 qed "fold_Un_Int";
   710 
   711 Goal "[| finite A; finite B; A Int B = {} |] \
   712 \     ==> fold f e (A Un B) = f (fold f e A) (fold f e B)";
   713 by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1);
   714 qed "fold_Un_disjoint";
   715 
   716 Goal
   717  "[| finite A; finite B |] ==> A Int B = {} --> \
   718 \ fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)";
   719 by (etac finite_induct 1);
   720 by (simp_tac (simpset() addsimps f_idents) 1);
   721 by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @
   722            [export fold_insert,insert_absorb, Int_insert_left]) 1);
   723 qed "fold_Un_disjoint2";
   724 
   725 Close_locale "ACe";
   726 
   727 Delrules ([empty_foldSetE] @ foldSet.intrs);
   728 Delsimps [foldSet_imp_finite];
   729 
   730 (*** setsum ***)
   731 
   732 Goalw [setsum_def] "setsum f {} = 0";
   733 by(Simp_tac 1);
   734 qed "setsum_empty";
   735 Addsimps [setsum_empty];
   736 
   737 Goalw [setsum_def]
   738  "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
   739 by(asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
   740 qed "setsum_insert";
   741 Addsimps [setsum_insert];
   742 
   743 Goalw [setsum_def]
   744  "[| finite A; finite B; A Int B = {} |] ==> \
   745 \ setsum f (A Un B) = setsum f A + setsum f B";
   746 by(asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
   747 qed_spec_mp "setsum_disj_Un";
   748 
   749 Goal "[| finite F |] ==> \
   750 \     setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
   751 be finite_induct 1;
   752 by(auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
   753 by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   754 by(Auto_tac);
   755 qed_spec_mp "setsum_diff1";