src/HOL/Finite.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10832 e33b47e4246d
child 11092 69c1abb9a129
permissions -rw-r--r--
improved theory reference in comment
wenzelm@9421
     1
(*  Title:      HOL/Finite.ML
clasohm@923
     2
    ID:         $Id$
nipkow@1531
     3
    Author:     Lawrence C Paulson & Tobias Nipkow
nipkow@1531
     4
    Copyright   1995  University of Cambridge & TU Muenchen
clasohm@923
     5
wenzelm@9421
     6
Finite sets and their cardinality.
clasohm@923
     7
*)
clasohm@923
     8
nipkow@3413
     9
section "finite";
nipkow@1531
    10
clasohm@923
    11
(*Discharging ~ x:y entails extra work*)
paulson@5316
    12
val major::prems = Goal 
nipkow@3413
    13
    "[| finite F;  P({}); \
nipkow@3413
    14
\       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
clasohm@923
    15
\    |] ==> P(F)";
nipkow@3413
    16
by (rtac (major RS Finites.induct) 1);
nipkow@3413
    17
by (excluded_middle_tac "a:A" 2);
clasohm@923
    18
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
clasohm@923
    19
by (REPEAT (ares_tac prems 1));
nipkow@3413
    20
qed "finite_induct";
nipkow@3413
    21
paulson@5316
    22
val major::subs::prems = Goal 
nipkow@3413
    23
    "[| finite F;  F <= A; \
nipkow@3413
    24
\       P({}); \
nipkow@3413
    25
\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
nipkow@3413
    26
\    |] ==> P(F)";
paulson@4386
    27
by (rtac (subs RS rev_mp) 1);
paulson@4386
    28
by (rtac (major RS finite_induct) 1);
paulson@4386
    29
by (ALLGOALS (blast_tac (claset() addIs prems)));
nipkow@3413
    30
qed "finite_subset_induct";
nipkow@3413
    31
nipkow@3413
    32
Addsimps Finites.intrs;
nipkow@3413
    33
AddSIs Finites.intrs;
clasohm@923
    34
clasohm@923
    35
(*The union of two finite sets is finite*)
paulson@5316
    36
Goal "[| finite F;  finite G |] ==> finite(F Un G)";
paulson@5316
    37
by (etac finite_induct 1);
paulson@5316
    38
by (ALLGOALS Asm_simp_tac);
nipkow@3413
    39
qed "finite_UnI";
clasohm@923
    40
clasohm@923
    41
(*Every subset of a finite set is finite*)
paulson@5143
    42
Goal "finite B ==> ALL A. A<=B --> finite A";
paulson@4304
    43
by (etac finite_induct 1);
oheimb@9399
    44
by (ALLGOALS (simp_tac (simpset() addsimps [subset_insert_iff])));
oheimb@9399
    45
by Safe_tac;
oheimb@9399
    46
 by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 1);
oheimb@9399
    47
 by (ALLGOALS Blast_tac);
paulson@4304
    48
val lemma = result();
paulson@4304
    49
paulson@5143
    50
Goal "[| A<=B;  finite B |] ==> finite A";
wenzelm@4423
    51
by (dtac lemma 1);
paulson@4304
    52
by (Blast_tac 1);
nipkow@3413
    53
qed "finite_subset";
clasohm@923
    54
wenzelm@5069
    55
Goal "finite(F Un G) = (finite F & finite G)";
paulson@4304
    56
by (blast_tac (claset() 
paulson@8554
    57
	         addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1);
nipkow@3413
    58
qed "finite_Un";
nipkow@3413
    59
AddIffs[finite_Un];
nipkow@1531
    60
paulson@8554
    61
(*The converse obviously fails*)
paulson@8554
    62
Goal "finite F | finite G ==> finite(F Int G)";
paulson@5413
    63
by (blast_tac (claset() addIs [finite_subset]) 1);
paulson@8554
    64
qed "finite_Int";
paulson@5413
    65
paulson@8554
    66
Addsimps [finite_Int];
paulson@8554
    67
AddIs [finite_Int];
paulson@5413
    68
wenzelm@5069
    69
Goal "finite(insert a A) = finite A";
paulson@1553
    70
by (stac insert_is_Un 1);
nipkow@3413
    71
by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
paulson@3427
    72
by (Blast_tac 1);
nipkow@3413
    73
qed "finite_insert";
nipkow@3413
    74
Addsimps[finite_insert];
nipkow@1531
    75
nipkow@3413
    76
(*The image of a finite set is finite *)
nipkow@10832
    77
Goal  "finite F ==> finite(h`F)";
nipkow@3413
    78
by (etac finite_induct 1);
clasohm@1264
    79
by (Simp_tac 1);
nipkow@3413
    80
by (Asm_simp_tac 1);
nipkow@3413
    81
qed "finite_imageI";
clasohm@923
    82
oheimb@8155
    83
Goal "finite (range g) ==> finite (range (%x. f (g x)))";
oheimb@8155
    84
by (Simp_tac 1);
oheimb@8155
    85
by (etac finite_imageI 1);
oheimb@8155
    86
qed "finite_range_imageI";
oheimb@8155
    87
paulson@5316
    88
val major::prems = Goal 
nipkow@3413
    89
    "[| finite c;  finite b;                                  \
clasohm@1465
    90
\       P(b);                                                   \
nipkow@3413
    91
\       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
clasohm@923
    92
\    |] ==> c<=b --> P(b-c)";
nipkow@3413
    93
by (rtac (major RS finite_induct) 1);
paulson@2031
    94
by (stac Diff_insert 2);
clasohm@923
    95
by (ALLGOALS (asm_simp_tac
paulson@5537
    96
                (simpset() addsimps prems@[Diff_subset RS finite_subset])));
nipkow@1531
    97
val lemma = result();
clasohm@923
    98
paulson@5316
    99
val prems = Goal 
nipkow@3413
   100
    "[| finite A;                                       \
nipkow@3413
   101
\       P(A);                                           \
nipkow@3413
   102
\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
clasohm@923
   103
\    |] ==> P({})";
clasohm@923
   104
by (rtac (Diff_cancel RS subst) 1);
nipkow@1531
   105
by (rtac (lemma RS mp) 1);
clasohm@923
   106
by (REPEAT (ares_tac (subset_refl::prems) 1));
nipkow@3413
   107
qed "finite_empty_induct";
nipkow@1531
   108
nipkow@1531
   109
paulson@1618
   110
(* finite B ==> finite (B - Ba) *)
paulson@1618
   111
bind_thm ("finite_Diff", Diff_subset RS finite_subset);
nipkow@1531
   112
Addsimps [finite_Diff];
nipkow@1531
   113
nipkow@5626
   114
Goal "finite(A - insert a B) = finite(A-B)";
paulson@6162
   115
by (stac Diff_insert 1);
nipkow@5626
   116
by (case_tac "a : A-B" 1);
paulson@3457
   117
by (rtac (finite_insert RS sym RS trans) 1);
paulson@3368
   118
by (stac insert_Diff 1);
nipkow@5626
   119
by (ALLGOALS Asm_full_simp_tac);
nipkow@5626
   120
qed "finite_Diff_insert";
nipkow@5626
   121
AddIffs [finite_Diff_insert];
nipkow@5626
   122
paulson@8554
   123
(*lemma merely for classical reasoner in the proof below: force_tac can't
paulson@8554
   124
  prove it.*)
nipkow@5626
   125
Goal "finite(A-{}) = finite A";
nipkow@5626
   126
by (Simp_tac 1);
nipkow@5626
   127
val lemma = result();
paulson@3368
   128
paulson@4059
   129
(*Lemma for proving finite_imageD*)
nipkow@10832
   130
Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A";
paulson@1553
   131
by (etac finite_induct 1);
nipkow@3413
   132
 by (ALLGOALS Asm_simp_tac);
paulson@3708
   133
by (Clarify_tac 1);
nipkow@10832
   134
by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1);
paulson@3708
   135
 by (Clarify_tac 1);
oheimb@8081
   136
 by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
paulson@8554
   137
 by (blast_tac (claset() addSDs [lemma RS iffD1]) 1);
paulson@3368
   138
by (thin_tac "ALL A. ?PP(A)" 1);
nipkow@3413
   139
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
paulson@3708
   140
by (Clarify_tac 1);
paulson@3368
   141
by (res_inst_tac [("x","xa")] bexI 1);
paulson@4059
   142
by (ALLGOALS 
nipkow@4830
   143
    (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
paulson@3368
   144
val lemma = result();
paulson@3368
   145
nipkow@10832
   146
Goal "[| finite(f`A);  inj_on f A |] ==> finite A";
paulson@3457
   147
by (dtac lemma 1);
paulson@3368
   148
by (Blast_tac 1);
paulson@3368
   149
qed "finite_imageD";
paulson@3368
   150
nipkow@4014
   151
(** The finite UNION of finite sets **)
nipkow@4014
   152
paulson@9096
   153
Goal "finite A ==> (ALL a:A. finite(B a)) --> finite(UN a:A. B a)";
paulson@5316
   154
by (etac finite_induct 1);
paulson@4153
   155
by (ALLGOALS Asm_simp_tac);
paulson@9096
   156
bind_thm("finite_UN_I", ballI RSN (2, result() RS mp));
paulson@9096
   157
paulson@9096
   158
(*strengthen RHS to 
paulson@9096
   159
    ((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})  ?  
paulson@9096
   160
  we'd need to prove
paulson@9096
   161
    finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}
paulson@9096
   162
  by induction*)
paulson@9096
   163
Goal "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))";
paulson@9096
   164
by (blast_tac (claset() addIs [finite_UN_I, finite_subset]) 1);
paulson@9096
   165
qed "finite_UN";
paulson@9096
   166
Addsimps [finite_UN];
nipkow@4014
   167
nipkow@4014
   168
(** Sigma of finite sets **)
nipkow@4014
   169
wenzelm@5069
   170
Goalw [Sigma_def]
paulson@9096
   171
 "[| finite A; ALL a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
paulson@9096
   172
by (blast_tac (claset() addSIs [finite_UN_I]) 1);
nipkow@4014
   173
bind_thm("finite_SigmaI", ballI RSN (2,result()));
nipkow@4014
   174
Addsimps [finite_SigmaI];
paulson@3368
   175
oheimb@8262
   176
Goal "[| finite (UNIV::'a set); finite (UNIV::'b set)|] ==> finite (UNIV::('a * 'b) set)"; 
oheimb@8262
   177
by (subgoal_tac "(UNIV::('a * 'b) set) = Sigma UNIV (%x. UNIV)" 1);
oheimb@8262
   178
by  (etac ssubst 1);
oheimb@8262
   179
by  (etac finite_SigmaI 1);
oheimb@8262
   180
by  Auto_tac;
oheimb@8262
   181
qed "finite_Prod_UNIV";
oheimb@8262
   182
oheimb@8262
   183
Goal "finite (UNIV :: ('a::finite * 'b::finite) set)";
paulson@8320
   184
by (rtac (finite_Prod_UNIV) 1);
paulson@8320
   185
by (rtac finite 1);
paulson@8320
   186
by (rtac finite 1);
oheimb@8262
   187
qed "finite_Prod";
oheimb@8262
   188
wenzelm@9351
   189
Goal "finite (UNIV :: unit set)";
wenzelm@9351
   190
by (subgoal_tac "UNIV = {()}" 1);
wenzelm@9351
   191
by (etac ssubst 1);
wenzelm@9351
   192
by Auto_tac;
wenzelm@9351
   193
qed "finite_unit";
wenzelm@9351
   194
paulson@3368
   195
(** The powerset of a finite set **)
paulson@3368
   196
paulson@5143
   197
Goal "finite(Pow A) ==> finite A";
nipkow@10832
   198
by (subgoal_tac "finite ((%x.{x})`A)" 1);
paulson@3457
   199
by (rtac finite_subset 2);
paulson@3457
   200
by (assume_tac 3);
paulson@3368
   201
by (ALLGOALS
nipkow@4830
   202
    (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
paulson@3368
   203
val lemma = result();
paulson@3368
   204
wenzelm@5069
   205
Goal "finite(Pow A) = finite A";
paulson@3457
   206
by (rtac iffI 1);
paulson@3457
   207
by (etac lemma 1);
paulson@3368
   208
(*Opposite inclusion: finite A ==> finite (Pow A) *)
paulson@3340
   209
by (etac finite_induct 1);
paulson@3340
   210
by (ALLGOALS 
paulson@3340
   211
    (asm_simp_tac
wenzelm@4089
   212
     (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert])));
paulson@3368
   213
qed "finite_Pow_iff";
paulson@3368
   214
AddIffs [finite_Pow_iff];
paulson@3340
   215
wenzelm@5069
   216
Goal "finite(r^-1) = finite r";
nipkow@10832
   217
by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1);
paulson@3457
   218
 by (Asm_simp_tac 1);
paulson@3457
   219
 by (rtac iffI 1);
nipkow@4830
   220
  by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
nipkow@4830
   221
  by (simp_tac (simpset() addsplits [split_split]) 1);
paulson@3457
   222
 by (etac finite_imageI 1);
paulson@4746
   223
by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
paulson@4477
   224
by Auto_tac;
oheimb@5516
   225
by (rtac bexI 1);
oheimb@5516
   226
by  (assume_tac 2);
oheimb@4763
   227
by (Simp_tac 1);
paulson@4746
   228
qed "finite_converse";
paulson@4746
   229
AddIffs [finite_converse];
nipkow@1531
   230
paulson@8963
   231
Goal "finite (lessThan (k::nat))";
paulson@8963
   232
by (induct_tac "k" 1);
paulson@8963
   233
by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
paulson@8963
   234
by Auto_tac;
paulson@8963
   235
qed "finite_lessThan";
paulson@8963
   236
paulson@8963
   237
Goal "finite (atMost (k::nat))";
paulson@8963
   238
by (induct_tac "k" 1);
paulson@8963
   239
by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
paulson@8963
   240
by Auto_tac;
paulson@8963
   241
qed "finite_atMost";
paulson@8971
   242
AddIffs [finite_lessThan, finite_atMost];
paulson@8963
   243
nipkow@8889
   244
(* A bounded set of natural numbers is finite *)
paulson@9096
   245
Goal "(ALL i:N. i<(n::nat)) ==> finite N";
paulson@8963
   246
by (rtac finite_subset 1);
paulson@8963
   247
 by (rtac finite_lessThan 2);
paulson@8963
   248
by Auto_tac;
paulson@8963
   249
qed "bounded_nat_set_is_finite";
nipkow@8889
   250
paulson@10785
   251
(** Finiteness of transitive closure (thanks to Sidi Ehmety) **)
paulson@10785
   252
paulson@10785
   253
(*A finite relation has a finite field ( = domain U range) *)
paulson@10785
   254
Goal "finite r ==> finite (Field r)";
paulson@10785
   255
by (etac finite_induct 1);
paulson@10785
   256
by (auto_tac (claset(), 
paulson@10785
   257
              simpset() addsimps [Field_def, Domain_insert, Range_insert]));
paulson@10785
   258
qed "finite_Field";
paulson@10785
   259
paulson@10785
   260
Goal "r^+ <= Field r <*> Field r";
paulson@10785
   261
by (Clarify_tac 1);
paulson@10785
   262
by (etac trancl_induct 1);
paulson@10785
   263
by (auto_tac (claset(), simpset() addsimps [Field_def]));  
paulson@10785
   264
qed "trancl_subset_Field2";
paulson@10785
   265
paulson@10785
   266
Goal "finite (r^+) = finite r";
paulson@10785
   267
by Auto_tac;
paulson@10785
   268
by (rtac (trancl_subset_Field2 RS finite_subset) 2);
paulson@10785
   269
by (rtac finite_SigmaI 2);
paulson@10785
   270
by (blast_tac (claset() addIs [r_into_trancl, finite_subset]) 1);
paulson@10785
   271
by (auto_tac (claset(), simpset() addsimps [finite_Field]));  
paulson@10785
   272
qed "finite_trancl";
paulson@10785
   273
nipkow@8889
   274
nipkow@1548
   275
section "Finite cardinality -- 'card'";
nipkow@1531
   276
wenzelm@9108
   277
bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR");
wenzelm@9108
   278
bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR");
nipkow@1531
   279
nipkow@5626
   280
AddSEs [cardR_emptyE];
nipkow@5626
   281
AddSIs cardR.intrs;
nipkow@5626
   282
paulson@9096
   283
Goal "[| (A,n) : cardR |] ==> a : A --> (EX m. n = Suc m)";
paulson@6162
   284
by (etac cardR.induct 1);
paulson@6162
   285
 by (Blast_tac 1);
paulson@6162
   286
by (Blast_tac 1);
nipkow@5626
   287
qed "cardR_SucD";
nipkow@5626
   288
paulson@9096
   289
Goal "(A,m): cardR ==> (ALL n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
paulson@6162
   290
by (etac cardR.induct 1);
paulson@8911
   291
 by Auto_tac;
paulson@6162
   292
by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
paulson@8911
   293
by Auto_tac;
wenzelm@7499
   294
by (ftac cardR_SucD 1);
paulson@6162
   295
by (Blast_tac 1);
nipkow@5626
   296
val lemma = result();
nipkow@5626
   297
nipkow@5626
   298
Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
paulson@6162
   299
by (dtac lemma 1);
paulson@6162
   300
by (Asm_full_simp_tac 1);
nipkow@5626
   301
val lemma = result();
nipkow@5626
   302
paulson@9096
   303
Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR --> n=m)";
paulson@6162
   304
by (etac cardR.induct 1);
paulson@6162
   305
 by (safe_tac (claset() addSEs [cardR_insertE]));
paulson@6162
   306
by (rename_tac "B b m" 1);
paulson@6162
   307
by (case_tac "a = b" 1);
paulson@6162
   308
 by (subgoal_tac "A = B" 1);
paulson@6162
   309
  by (blast_tac (claset() addEs [equalityE]) 2);
paulson@6162
   310
 by (Blast_tac 1);
paulson@9096
   311
by (subgoal_tac "EX C. A = insert b C & B = insert a C" 1);
paulson@6162
   312
 by (res_inst_tac [("x","A Int B")] exI 2);
paulson@6162
   313
 by (blast_tac (claset() addEs [equalityE]) 2);
paulson@6162
   314
by (forw_inst_tac [("A","B")] cardR_SucD 1);
paulson@6162
   315
by (blast_tac (claset() addDs [lemma]) 1);
nipkow@5626
   316
qed_spec_mp "cardR_determ";
nipkow@5626
   317
nipkow@5626
   318
Goal "(A,n) : cardR ==> finite(A)";
nipkow@5626
   319
by (etac cardR.induct 1);
nipkow@5626
   320
by Auto_tac;
nipkow@5626
   321
qed "cardR_imp_finite";
nipkow@5626
   322
nipkow@5626
   323
Goal "finite(A) ==> EX n. (A, n) : cardR";
nipkow@5626
   324
by (etac finite_induct 1);
nipkow@5626
   325
by Auto_tac;
nipkow@5626
   326
qed "finite_imp_cardR";
nipkow@5626
   327
nipkow@5626
   328
Goalw [card_def] "(A,n) : cardR ==> card A = n";
nipkow@5626
   329
by (blast_tac (claset() addIs [cardR_determ]) 1);
nipkow@5626
   330
qed "card_equality";
nipkow@5626
   331
nipkow@5626
   332
Goalw [card_def] "card {} = 0";
nipkow@5626
   333
by (Blast_tac 1);
nipkow@5626
   334
qed "card_empty";
nipkow@5626
   335
Addsimps [card_empty];
nipkow@5626
   336
nipkow@5626
   337
Goal "x ~: A ==> \
nipkow@5626
   338
\     ((insert x A, n) : cardR) =  \
nipkow@5626
   339
\     (EX m. (A, m) : cardR & n = Suc m)";
nipkow@5626
   340
by Auto_tac;
nipkow@5626
   341
by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1);
nipkow@5626
   342
by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1);
nipkow@5626
   343
by (blast_tac (claset() addIs [cardR_determ]) 1);
nipkow@5626
   344
val lemma = result();
nipkow@5626
   345
nipkow@5626
   346
Goalw [card_def]
nipkow@5626
   347
     "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
nipkow@5626
   348
by (asm_simp_tac (simpset() addsimps [lemma]) 1);
paulson@9969
   349
by (rtac some_equality 1);
nipkow@5626
   350
by (auto_tac (claset() addIs [finite_imp_cardR],
nipkow@5626
   351
	      simpset() addcongs [conj_cong]
nipkow@5626
   352
		        addsimps [symmetric card_def,
nipkow@5626
   353
				  card_equality]));
nipkow@5626
   354
qed "card_insert_disjoint";
nipkow@5626
   355
Addsimps [card_insert_disjoint];
nipkow@5626
   356
nipkow@5626
   357
(* Delete rules to do with cardR relation: obsolete *)
nipkow@5626
   358
Delrules [cardR_emptyE];
nipkow@5626
   359
Delrules cardR.intrs;
nipkow@5626
   360
oheimb@7958
   361
Goal "finite A ==> (card A = 0) = (A = {})";
oheimb@7958
   362
by Auto_tac;
oheimb@7958
   363
by (dres_inst_tac [("a","x")] mk_disjoint_insert 1);
oheimb@7958
   364
by (Clarify_tac 1);
oheimb@7958
   365
by (rotate_tac ~1 1);
oheimb@7958
   366
by Auto_tac;
oheimb@7958
   367
qed "card_0_eq";
oheimb@7958
   368
Addsimps[card_0_eq];
oheimb@7958
   369
nipkow@5626
   370
Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))";
nipkow@5626
   371
by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
nipkow@5626
   372
qed "card_insert_if";
nipkow@5626
   373
paulson@7821
   374
Goal "[| finite A; x: A |] ==> Suc (card (A-{x})) = card A";
nipkow@5626
   375
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
nipkow@5626
   376
by (assume_tac 1);
nipkow@5626
   377
by (Asm_simp_tac 1);
nipkow@5626
   378
qed "card_Suc_Diff1";
nipkow@5626
   379
paulson@7821
   380
Goal "[| finite A; x: A |] ==> card (A-{x}) = card A - 1";
paulson@7821
   381
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1 RS sym]) 1);
paulson@7821
   382
qed "card_Diff_singleton";
paulson@7821
   383
paulson@9074
   384
Goal "finite A ==> card (A-{x}) = (if x:A then card A - 1 else card A)";
paulson@9074
   385
by (asm_simp_tac (simpset() addsimps [card_Diff_singleton]) 1);
paulson@9074
   386
qed "card_Diff_singleton_if";
paulson@9074
   387
nipkow@5626
   388
Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
nipkow@5626
   389
by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1);
nipkow@5626
   390
qed "card_insert";
paulson@3352
   391
paulson@5143
   392
Goal "finite A ==> card A <= card (insert x A)";
nipkow@5626
   393
by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1);
paulson@4768
   394
qed "card_insert_le";
paulson@4768
   395
paulson@9074
   396
Goal "finite B ==> ALL A. A <= B --> card B <= card A --> A = B";
paulson@3352
   397
by (etac finite_induct 1);
oheimb@9338
   398
 by (Simp_tac 1);
paulson@3708
   399
by (Clarify_tac 1);
paulson@9074
   400
by (subgoal_tac "finite A & A-{x} <= F" 1);
paulson@9074
   401
 by (blast_tac (claset() addIs [finite_subset]) 2); 
paulson@9074
   402
by (dres_inst_tac [("x","A-{x}")] spec 1); 
paulson@9074
   403
by (asm_full_simp_tac (simpset() addsimps [card_Diff_singleton_if]
paulson@9074
   404
                                 addsplits [split_if_asm]) 1); 
paulson@9074
   405
by (case_tac "card A" 1);
paulson@9074
   406
by Auto_tac; 
paulson@9074
   407
qed_spec_mp "card_seteq";
paulson@3352
   408
paulson@9074
   409
Goalw [psubset_def] "[| finite B;  A < B |] ==> card A < card B";
paulson@9074
   410
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
paulson@9074
   411
by (blast_tac (claset() addDs [card_seteq]) 1); 
paulson@9074
   412
qed "psubset_card_mono" ;
paulson@9074
   413
paulson@9074
   414
Goal "[| finite B;  A <= B |] ==> card A <= card B";
paulson@9074
   415
by (case_tac "A=B" 1);
paulson@9074
   416
 by (Asm_simp_tac 1); 
paulson@9074
   417
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
paulson@9074
   418
by (blast_tac (claset() addDs [card_seteq] addIs [order_less_imp_le]) 1); 
paulson@9074
   419
qed "card_mono" ;
paulson@5416
   420
paulson@5416
   421
Goal "[| finite A; finite B |] \
paulson@5416
   422
\     ==> card A + card B = card (A Un B) + card (A Int B)";
paulson@3352
   423
by (etac finite_induct 1);
paulson@5416
   424
by (Simp_tac 1);
paulson@5416
   425
by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1);
paulson@5416
   426
qed "card_Un_Int";
paulson@5416
   427
paulson@5416
   428
Goal "[| finite A; finite B; A Int B = {} |] \
paulson@5416
   429
\     ==> card (A Un B) = card A + card B";
paulson@5416
   430
by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1);
paulson@5416
   431
qed "card_Un_disjoint";
paulson@3352
   432
paulson@5143
   433
Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
paulson@3352
   434
by (subgoal_tac "(A-B) Un B = A" 1);
paulson@3352
   435
by (Blast_tac 2);
paulson@3457
   436
by (rtac (add_right_cancel RS iffD1) 1);
paulson@3457
   437
by (rtac (card_Un_disjoint RS subst) 1);
paulson@3457
   438
by (etac ssubst 4);
paulson@3352
   439
by (Blast_tac 3);
paulson@3352
   440
by (ALLGOALS 
paulson@3352
   441
    (asm_simp_tac
wenzelm@4089
   442
     (simpset() addsimps [add_commute, not_less_iff_le, 
paulson@5416
   443
			  add_diff_inverse, card_mono, finite_subset])));
paulson@3352
   444
qed "card_Diff_subset";
nipkow@1531
   445
paulson@5143
   446
Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
paulson@2031
   447
by (rtac Suc_less_SucD 1);
nipkow@5626
   448
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
nipkow@5626
   449
qed "card_Diff1_less";
paulson@1618
   450
paulson@10375
   451
Goal "[| finite A; x: A; y: A |] ==> card(A-{x}-{y}) < card A"; 
paulson@10375
   452
by (case_tac "x=y" 1);
paulson@10375
   453
by (asm_simp_tac (simpset() addsimps [card_Diff1_less]) 1);
paulson@10375
   454
by (rtac less_trans 1);
paulson@10375
   455
by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], simpset())));
paulson@10375
   456
qed "card_Diff2_less";
paulson@10375
   457
paulson@5143
   458
Goal "finite A ==> card(A-{x}) <= card A";
paulson@4768
   459
by (case_tac "x: A" 1);
nipkow@5626
   460
by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le])));
nipkow@5626
   461
qed "card_Diff1_le";
nipkow@1531
   462
nipkow@5626
   463
Goal "[| finite B; A <= B; card A < card B |] ==> A < B";
nipkow@5626
   464
by (etac psubsetI 1);
nipkow@5626
   465
by (Blast_tac 1);
nipkow@5626
   466
qed "card_psubset";
nipkow@5626
   467
nipkow@5626
   468
(*** Cardinality of image ***)
nipkow@5626
   469
nipkow@10832
   470
Goal "finite A ==> card (f ` A) <= card A";
nipkow@5626
   471
by (etac finite_induct 1);
paulson@9074
   472
 by (Simp_tac 1);
paulson@9074
   473
by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
paulson@9074
   474
				      card_insert_if]) 1);
nipkow@5626
   475
qed "card_image_le";
nipkow@5626
   476
nipkow@10832
   477
Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A";
nipkow@5626
   478
by (etac finite_induct 1);
nipkow@5626
   479
by (ALLGOALS Asm_simp_tac);
nipkow@5626
   480
by Safe_tac;
nipkow@5626
   481
by (rewtac inj_on_def);
nipkow@5626
   482
by (Blast_tac 1);
nipkow@5626
   483
by (stac card_insert_disjoint 1);
nipkow@5626
   484
by (etac finite_imageI 1);
nipkow@5626
   485
by (Blast_tac 1);
nipkow@5626
   486
by (Blast_tac 1);
nipkow@5626
   487
qed_spec_mp "card_image";
nipkow@5626
   488
nipkow@10832
   489
Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A";
paulson@9074
   490
by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
nipkow@5626
   491
qed "endo_inj_surj";
nipkow@5626
   492
nipkow@5626
   493
(*** Cardinality of the Powerset ***)
nipkow@5626
   494
nipkow@5626
   495
Goal "finite A ==> card (Pow A) = 2 ^ card A";
nipkow@5626
   496
by (etac finite_induct 1);
nipkow@5626
   497
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
nipkow@5626
   498
by (stac card_Un_disjoint 1);
nipkow@5626
   499
by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
nipkow@5626
   500
by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
nipkow@5626
   501
by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
nipkow@5626
   502
by (rewtac inj_on_def);
nipkow@5626
   503
by (blast_tac (claset() addSEs [equalityE]) 1);
nipkow@5626
   504
qed "card_Pow";
nipkow@5626
   505
paulson@3368
   506
wenzelm@3430
   507
(*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
paulson@3368
   508
  The "finite C" premise is redundant*)
paulson@5143
   509
Goal "finite C ==> finite (Union C) --> \
paulson@9096
   510
\          (ALL c : C. k dvd card c) -->  \
paulson@9096
   511
\          (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
paulson@3368
   512
\          --> k dvd card(Union C)";
paulson@3368
   513
by (etac finite_induct 1);
paulson@3368
   514
by (ALLGOALS Asm_simp_tac);
paulson@3708
   515
by (Clarify_tac 1);
paulson@3368
   516
by (stac card_Un_disjoint 1);
paulson@3368
   517
by (ALLGOALS
wenzelm@4089
   518
    (asm_full_simp_tac (simpset()
paulson@3368
   519
			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
paulson@9096
   520
by (thin_tac "ALL c:F. ?PP(c)" 1);
paulson@9096
   521
by (thin_tac "ALL c:F. ?PP(c) & ?QQ(c)" 1);
paulson@3708
   522
by (Clarify_tac 1);
paulson@3368
   523
by (ball_tac 1);
paulson@3368
   524
by (Blast_tac 1);
paulson@3368
   525
qed_spec_mp "dvd_partition";
paulson@3368
   526
nipkow@5616
   527
nipkow@5616
   528
(*** foldSet ***)
nipkow@5616
   529
wenzelm@9108
   530
bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e");
nipkow@5616
   531
nipkow@5616
   532
AddSEs [empty_foldSetE];
nipkow@5616
   533
AddIs foldSet.intrs;
nipkow@5616
   534
nipkow@5616
   535
Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
nipkow@5616
   536
by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
nipkow@5616
   537
by Auto_tac;
nipkow@5626
   538
qed "Diff1_foldSet";
nipkow@5616
   539
nipkow@5616
   540
Goal "(A, x) : foldSet f e ==> finite(A)";
nipkow@5616
   541
by (eresolve_tac [foldSet.induct] 1);
nipkow@5616
   542
by Auto_tac;
nipkow@5616
   543
qed "foldSet_imp_finite";
nipkow@5616
   544
nipkow@5616
   545
Addsimps [foldSet_imp_finite];
nipkow@5616
   546
nipkow@5616
   547
nipkow@5616
   548
Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
nipkow@5616
   549
by (etac finite_induct 1);
nipkow@5616
   550
by Auto_tac;
nipkow@5616
   551
qed "finite_imp_foldSet";
nipkow@5616
   552
nipkow@5616
   553
nipkow@5616
   554
Open_locale "LC"; 
nipkow@5616
   555
paulson@5782
   556
val f_lcomm = thm "lcomm";
nipkow@5616
   557
nipkow@5616
   558
nipkow@5616
   559
Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
nipkow@5616
   560
\            (ALL y. (A, y) : foldSet f e --> y=x)";
nipkow@5616
   561
by (induct_tac "n" 1);
nipkow@5616
   562
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
nipkow@5616
   563
by (etac foldSet.elim 1);
nipkow@5616
   564
by (Blast_tac 1);
nipkow@5616
   565
by (etac foldSet.elim 1);
nipkow@5616
   566
by (Blast_tac 1);
nipkow@5616
   567
by (Clarify_tac 1);
nipkow@5616
   568
(*force simplification of "card A < card (insert ...)"*)
nipkow@5616
   569
by (etac rev_mp 1);
nipkow@5616
   570
by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
nipkow@5616
   571
by (rtac impI 1);
nipkow@5616
   572
(** LEVEL 10 **)
nipkow@5616
   573
by (rename_tac "Aa xa ya Ab xb yb" 1);
nipkow@5616
   574
 by (case_tac "xa=xb" 1);
nipkow@5616
   575
 by (subgoal_tac "Aa = Ab" 1);
paulson@9837
   576
 by (blast_tac (claset() addSEs [equalityE]) 2);
nipkow@5616
   577
 by (Blast_tac 1);
nipkow@5616
   578
(*case xa ~= xb*)
nipkow@5616
   579
by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
paulson@9837
   580
 by (blast_tac (claset() addSEs [equalityE]) 2);
nipkow@5616
   581
by (Clarify_tac 1);
nipkow@5616
   582
by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
paulson@9837
   583
 by (Blast_tac 2);
nipkow@5616
   584
(** LEVEL 20 **)
nipkow@5616
   585
by (subgoal_tac "card Aa <= card Ab" 1);
nipkow@5616
   586
 by (rtac (Suc_le_mono RS subst) 2);
nipkow@5626
   587
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2);
nipkow@5616
   588
by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
nipkow@5616
   589
    (finite_imp_foldSet RS exE) 1);
nipkow@5616
   590
by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
wenzelm@7499
   591
by (ftac Diff1_foldSet 1 THEN assume_tac 1);
nipkow@5616
   592
by (subgoal_tac "ya = f xb x" 1);
paulson@9837
   593
 by (blast_tac (claset() delrules [equalityCE]) 2);
nipkow@5616
   594
by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
nipkow@5616
   595
 by (Asm_full_simp_tac 2);
nipkow@5616
   596
by (subgoal_tac "yb = f xa x" 1);
paulson@9837
   597
 by (blast_tac (claset() delrules [equalityCE]
paulson@9837
   598
			addDs [Diff1_foldSet]) 2);
nipkow@5616
   599
by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
nipkow@5616
   600
val lemma = result();
nipkow@5616
   601
nipkow@5616
   602
nipkow@5616
   603
Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
nipkow@9736
   604
by (blast_tac (claset() addIs [rulify lemma]) 1);
nipkow@5616
   605
qed "foldSet_determ";
nipkow@5616
   606
nipkow@5616
   607
Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
nipkow@5616
   608
by (blast_tac (claset() addIs [foldSet_determ]) 1);
nipkow@5616
   609
qed "fold_equality";
nipkow@5616
   610
nipkow@5616
   611
Goalw [fold_def] "fold f e {} = e";
nipkow@5616
   612
by (Blast_tac 1);
nipkow@5616
   613
qed "fold_empty";
nipkow@5616
   614
Addsimps [fold_empty];
nipkow@5616
   615
nipkow@5626
   616
nipkow@5616
   617
Goal "x ~: A ==> \
nipkow@5616
   618
\     ((insert x A, v) : foldSet f e) =  \
nipkow@5616
   619
\     (EX y. (A, y) : foldSet f e & v = f x y)";
nipkow@5616
   620
by Auto_tac;
nipkow@5616
   621
by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
nipkow@5616
   622
by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
nipkow@5616
   623
by (blast_tac (claset() addIs [foldSet_determ]) 1);
nipkow@5616
   624
val lemma = result();
nipkow@5616
   625
nipkow@5616
   626
Goalw [fold_def]
nipkow@5616
   627
     "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
nipkow@5616
   628
by (asm_simp_tac (simpset() addsimps [lemma]) 1);
paulson@9969
   629
by (rtac some_equality 1);
nipkow@5616
   630
by (auto_tac (claset() addIs [finite_imp_foldSet],
nipkow@5616
   631
	      simpset() addcongs [conj_cong]
nipkow@5616
   632
		        addsimps [symmetric fold_def,
nipkow@5616
   633
				  fold_equality]));
nipkow@5616
   634
qed "fold_insert";
nipkow@5616
   635
paulson@8911
   636
Goal "finite A ==> ALL e. f x (fold f e A) = fold f (f x e) A";
paulson@8911
   637
by (etac finite_induct 1);
paulson@8911
   638
by (Simp_tac 1);
paulson@8911
   639
by (asm_simp_tac (simpset() addsimps [f_lcomm, fold_insert]) 1);
paulson@8911
   640
qed_spec_mp "fold_commute";
paulson@8911
   641
paulson@8911
   642
Goal "[| finite A; finite B |] \
paulson@8911
   643
\     ==> fold f (fold f e B) A  =  fold f (fold f e (A Int B)) (A Un B)";
paulson@8911
   644
by (etac finite_induct 1);
paulson@8911
   645
by (Simp_tac 1);
paulson@8911
   646
by (asm_simp_tac (simpset() addsimps [fold_insert, fold_commute, 
paulson@8911
   647
	                              Int_insert_left, insert_absorb]) 1);
paulson@8911
   648
qed "fold_nest_Un_Int";
paulson@8911
   649
paulson@8911
   650
Goal "[| finite A; finite B; A Int B = {} |] \
paulson@8911
   651
\     ==> fold f e (A Un B)  =  fold f (fold f e B) A";
paulson@8911
   652
by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
paulson@8911
   653
qed "fold_nest_Un_disjoint";
paulson@8911
   654
nipkow@5626
   655
(* Delete rules to do with foldSet relation: obsolete *)
nipkow@5626
   656
Delsimps [foldSet_imp_finite];
nipkow@5626
   657
Delrules [empty_foldSetE];
nipkow@5626
   658
Delrules foldSet.intrs;
nipkow@5626
   659
paulson@6024
   660
Close_locale "LC";
nipkow@5616
   661
nipkow@5616
   662
Open_locale "ACe"; 
nipkow@5616
   663
paulson@8911
   664
(*We enter a more restrictive framework, with f :: ['a,'a] => 'a
paulson@8911
   665
    instead of ['b,'a] => 'a 
paulson@8911
   666
  At present, none of these results are used!*)
paulson@8911
   667
paulson@5782
   668
val f_ident   = thm "ident";
paulson@5782
   669
val f_commute = thm "commute";
paulson@5782
   670
val f_assoc   = thm "assoc";
nipkow@5616
   671
nipkow@5616
   672
nipkow@5616
   673
Goal "f x (f y z) = f y (f x z)";
nipkow@5616
   674
by (rtac (f_commute RS trans) 1);
nipkow@5616
   675
by (rtac (f_assoc RS trans) 1);
nipkow@5616
   676
by (rtac (f_commute RS arg_cong) 1);
nipkow@5616
   677
qed "f_left_commute";
nipkow@5616
   678
nipkow@5616
   679
val f_ac = [f_assoc, f_commute, f_left_commute];
nipkow@5616
   680
nipkow@5616
   681
Goal "f e x = x";
nipkow@5616
   682
by (stac f_commute 1);
nipkow@5616
   683
by (rtac f_ident 1);
nipkow@5616
   684
qed "f_left_ident";
nipkow@5616
   685
nipkow@5616
   686
val f_idents = [f_left_ident, f_ident];
nipkow@5616
   687
nipkow@5616
   688
Goal "[| finite A; finite B |] \
nipkow@5616
   689
\     ==> f (fold f e A) (fold f e B) =  \
nipkow@5616
   690
\         f (fold f e (A Un B)) (fold f e (A Int B))";
nipkow@5616
   691
by (etac finite_induct 1);
nipkow@5616
   692
by (simp_tac (simpset() addsimps f_idents) 1);
nipkow@5616
   693
by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @
nipkow@5616
   694
           [export fold_insert,insert_absorb, Int_insert_left]) 1);
nipkow@5616
   695
qed "fold_Un_Int";
nipkow@5616
   696
nipkow@5616
   697
Goal "[| finite A; finite B; A Int B = {} |] \
nipkow@5616
   698
\     ==> fold f e (A Un B) = f (fold f e A) (fold f e B)";
nipkow@5616
   699
by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1);
nipkow@5616
   700
qed "fold_Un_disjoint";
nipkow@5616
   701
nipkow@5616
   702
Goal
nipkow@5616
   703
 "[| finite A; finite B |] ==> A Int B = {} --> \
paulson@9096
   704
\      fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)";
nipkow@5616
   705
by (etac finite_induct 1);
nipkow@5616
   706
by (simp_tac (simpset() addsimps f_idents) 1);
nipkow@5616
   707
by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @
nipkow@5616
   708
           [export fold_insert,insert_absorb, Int_insert_left]) 1);
nipkow@5616
   709
qed "fold_Un_disjoint2";
nipkow@5616
   710
paulson@6024
   711
Close_locale "ACe";
nipkow@5616
   712
nipkow@5616
   713
paulson@8981
   714
(*** setsum: generalized summation over a set ***)
nipkow@5616
   715
nipkow@5616
   716
Goalw [setsum_def] "setsum f {} = 0";
paulson@6162
   717
by (Simp_tac 1);
nipkow@5616
   718
qed "setsum_empty";
nipkow@5616
   719
Addsimps [setsum_empty];
nipkow@5616
   720
nipkow@5616
   721
Goalw [setsum_def]
nipkow@5616
   722
 "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
paulson@8963
   723
by (asm_simp_tac (simpset() addsimps [export fold_insert,
paulson@8963
   724
				      thm "plus_ac0_left_commute"]) 1);
nipkow@5616
   725
qed "setsum_insert";
nipkow@5616
   726
Addsimps [setsum_insert];
nipkow@5616
   727
paulson@9086
   728
Goal "setsum (%i. 0) A = 0";
paulson@9086
   729
by (case_tac "finite A" 1);
paulson@9086
   730
 by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
paulson@9002
   731
by (etac finite_induct 1);
paulson@9002
   732
by Auto_tac;
paulson@9002
   733
qed "setsum_0";
paulson@9002
   734
paulson@9086
   735
Goal "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))";
paulson@9002
   736
by (etac finite_induct 1);
paulson@9002
   737
by Auto_tac;
paulson@9002
   738
qed "setsum_eq_0_iff";
paulson@9002
   739
Addsimps [setsum_eq_0_iff];
paulson@9002
   740
paulson@9086
   741
Goal "setsum f A = Suc n ==> EX a:A. 0 < f a";
paulson@9086
   742
by (case_tac "finite A" 1);
paulson@9086
   743
 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
paulson@9002
   744
by (etac rev_mp 1);
paulson@9002
   745
by (etac finite_induct 1);
paulson@9002
   746
by Auto_tac;
paulson@9002
   747
qed "setsum_SucD";
paulson@9002
   748
paulson@8911
   749
(*Could allow many "card" proofs to be simplified*)
paulson@8911
   750
Goal "finite A ==> card A = setsum (%x. 1) A";
paulson@8911
   751
by (etac finite_induct 1);
paulson@8911
   752
by Auto_tac;
paulson@8911
   753
qed "card_eq_setsum";
nipkow@5616
   754
paulson@9002
   755
(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
paulson@8911
   756
Goal "[| finite A; finite B |] \
paulson@8911
   757
\     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
paulson@8911
   758
by (etac finite_induct 1);
paulson@8911
   759
by (Simp_tac 1);
paulson@8963
   760
by (asm_full_simp_tac (simpset() addsimps (thms "plus_ac0") @ 
paulson@8963
   761
                                          [Int_insert_left, insert_absorb]) 1);
paulson@8911
   762
qed "setsum_Un_Int";
paulson@8911
   763
paulson@8981
   764
Goal "[| finite A; finite B; A Int B = {} |] \
paulson@8981
   765
\     ==> setsum g (A Un B) = setsum g A + setsum g B";  
paulson@8981
   766
by (stac (setsum_Un_Int RS sym) 1);
paulson@8981
   767
by Auto_tac;
paulson@8981
   768
qed "setsum_Un_disjoint";
paulson@8981
   769
paulson@9086
   770
Goal "finite I \
paulson@9096
   771
\     ==> (ALL i:I. finite (A i)) --> \
paulson@9096
   772
\         (ALL i:I. ALL j:I. i~=j --> A i Int A j = {}) --> \
paulson@9096
   773
\         setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 
paulson@8981
   774
by (etac finite_induct 1);
paulson@9096
   775
 by (Simp_tac 1);
paulson@9096
   776
by (Clarify_tac 1); 
paulson@9096
   777
by (subgoal_tac "ALL i:F. x ~= i" 1);
paulson@9096
   778
 by (Blast_tac 2); 
paulson@9096
   779
by (subgoal_tac "A x Int UNION F A = {}" 1);
paulson@9096
   780
 by (Blast_tac 2); 
paulson@8981
   781
by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
paulson@8981
   782
qed_spec_mp "setsum_UN_disjoint";
paulson@8981
   783
paulson@9086
   784
Goal "setsum (%x. f x + g x) A = setsum f A + setsum g A";
paulson@9086
   785
by (case_tac "finite A" 1);
paulson@9086
   786
 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
paulson@8981
   787
by (etac finite_induct 1);
paulson@8981
   788
by Auto_tac;
paulson@8981
   789
by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1);
paulson@8981
   790
qed "setsum_addf";
paulson@8981
   791
paulson@8981
   792
(** For the natural numbers, we have subtraction **)
paulson@8981
   793
paulson@8911
   794
Goal "[| finite A; finite B |] \
paulson@8963
   795
\     ==> (setsum f (A Un B) :: nat) = \
paulson@8963
   796
\         setsum f A + setsum f B - setsum f (A Int B)";
paulson@8911
   797
by (stac (setsum_Un_Int RS sym) 1);
paulson@8911
   798
by Auto_tac;
paulson@8911
   799
qed "setsum_Un";
paulson@8911
   800
paulson@9086
   801
Goal "(setsum f (A-{a}) :: nat) = \
paulson@9086
   802
\     (if a:A then setsum f A - f a else setsum f A)";
paulson@9086
   803
by (case_tac "finite A" 1);
paulson@9086
   804
 by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
paulson@6162
   805
by (etac finite_induct 1);
paulson@6162
   806
by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
paulson@6162
   807
by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
paulson@8911
   808
by Auto_tac;
nipkow@5616
   809
qed_spec_mp "setsum_diff1";
paulson@7834
   810
paulson@9086
   811
val prems = Goal
paulson@9086
   812
    "[| A = B; !!x. x:B ==> f x = g x|] ==> setsum f A = setsum g B";
paulson@9086
   813
by (case_tac "finite B" 1);
paulson@9086
   814
 by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
paulson@9086
   815
by (simp_tac (simpset() addsimps prems) 1);
paulson@9086
   816
by (subgoal_tac 
paulson@9086
   817
    "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C" 1);
oheimb@9399
   818
 by (asm_simp_tac (simpset() addsimps prems) 1); 
paulson@9086
   819
by (etac finite_induct 1);
oheimb@9338
   820
 by (Simp_tac 1);
oheimb@9399
   821
by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); 
paulson@9086
   822
by (Clarify_tac 1); 
paulson@9086
   823
by (subgoal_tac "finite C" 1);
paulson@9086
   824
 by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2); 
paulson@9086
   825
by (subgoal_tac "C = insert x (C-{x})" 1); 
paulson@9086
   826
 by (Blast_tac 2); 
paulson@9086
   827
by (etac ssubst 1); 
paulson@9086
   828
by (dtac spec 1); 
paulson@9086
   829
by (mp_tac 1);
oheimb@9399
   830
by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1); 
paulson@9086
   831
qed "setsum_cong";
paulson@9086
   832
paulson@7834
   833
paulson@7834
   834
(*** Basic theorem about "choose".  By Florian Kammueller, tidied by LCP ***)
paulson@7834
   835
paulson@7834
   836
Goal "finite A ==> card {B. B <= A & card B = 0} = 1";
paulson@7834
   837
by (asm_simp_tac (simpset() addcongs [conj_cong]
paulson@10098
   838
	 	            addsimps [finite_subset RS card_0_eq]) 1);
paulson@7834
   839
by (simp_tac (simpset() addcongs [rev_conj_cong]) 1);
paulson@7834
   840
qed "card_s_0_eq_empty";
paulson@7834
   841
paulson@7834
   842
Goal "[| finite M; x ~: M |] \
paulson@7834
   843
\  ==> {s. s <= insert x M & card(s) = Suc k} \
paulson@7834
   844
\      = {s. s <= M & card(s) = Suc k} Un \
paulson@7834
   845
\        {s. EX t. t <= M & card(t) = k & s = insert x t}";
paulson@7834
   846
by Safe_tac;
paulson@7834
   847
by (auto_tac (claset() addIs [finite_subset RS card_insert_disjoint], 
paulson@7834
   848
	      simpset()));
paulson@7834
   849
by (dres_inst_tac [("x","xa - {x}")] spec 1);
paulson@7834
   850
by (subgoal_tac ("x ~: xa") 1);
paulson@7834
   851
by Auto_tac;
paulson@7834
   852
by (etac rev_mp 1 THEN stac card_Diff_singleton 1);
oheimb@7958
   853
by (auto_tac (claset() addIs [finite_subset], simpset()));
paulson@7834
   854
qed "choose_deconstruct";
paulson@7834
   855
nipkow@10832
   856
Goal "[| finite(A); finite(B);  f`A <= B;  inj_on f A |] \
paulson@7834
   857
\     ==> card A <= card B";
paulson@7834
   858
by (auto_tac (claset() addIs [card_mono], 
nipkow@8140
   859
	      simpset() addsimps [card_image RS sym]));
paulson@7834
   860
qed "card_inj_on_le";
paulson@7834
   861
paulson@7834
   862
Goal "[| finite A; finite B; \
nipkow@10832
   863
\        f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \
paulson@7834
   864
\     ==> card(A) = card(B)";
paulson@7834
   865
by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
paulson@7834
   866
qed "card_bij_eq";
paulson@7834
   867
paulson@10098
   868
Goal "[| finite A; x ~: A |]  \
paulson@10098
   869
\     ==> card{B. EX C. C <= A & card(C) = k & B = insert x C} = \
paulson@10098
   870
\         card {B. B <= A & card(B) = k}";
nipkow@8140
   871
by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1);
paulson@10098
   872
by (res_inst_tac [("B","Pow(insert x A)")] finite_subset 1);
paulson@10098
   873
by (res_inst_tac [("B","Pow(A)")] finite_subset 3);
paulson@8320
   874
by (REPEAT(Fast_tac 1));
paulson@7834
   875
(* arity *)
nipkow@8140
   876
by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def]));
paulson@7834
   877
by (stac Diff_insert0 1);
paulson@7834
   878
by Auto_tac;
paulson@7834
   879
qed "constr_bij";
paulson@7834
   880
paulson@7834
   881
(* Main theorem: combinatorial theorem about number of subsets of a set *)
paulson@10098
   882
Goal "(ALL A. finite A --> card {B. B <= A & card B = k} = (card A choose k))";
paulson@7834
   883
by (induct_tac "k" 1);
paulson@9074
   884
 by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1);
paulson@7834
   885
(* first 0 case finished *)
paulson@7842
   886
(* prepare finite set induction *)
paulson@7842
   887
by (rtac allI 1 THEN rtac impI 1);
paulson@7834
   888
(* second induction *)
paulson@7834
   889
by (etac finite_induct 1);
paulson@7842
   890
by (ALLGOALS
paulson@9074
   891
    (asm_simp_tac (simpset() addcongs [conj_cong] 
paulson@10098
   892
                     addsimps [card_s_0_eq_empty, choose_deconstruct])));
paulson@7834
   893
by (stac card_Un_disjoint 1);
paulson@9074
   894
   by (force_tac (claset(), simpset() addsimps [constr_bij]) 4);
paulson@9074
   895
  by (Force_tac 3);
paulson@9074
   896
 by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2, 
paulson@9074
   897
			 inst "B" "Pow (insert ?x ?F)" finite_subset]) 2);
paulson@9074
   898
by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2 
paulson@9074
   899
			       RSN (2, finite_subset)]) 1);
paulson@7834
   900
qed "n_sub_lemma";
paulson@7834
   901
paulson@10098
   902
Goal "finite A ==> card {B. B <= A & card(B) = k} = ((card A) choose k)";
paulson@7834
   903
by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1);
paulson@7834
   904
qed "n_subsets";