renamed theory Finite to Finite_Set and converted;
authorwenzelm
Thu Dec 06 00:38:55 2001 +0100 (2001-12-06)
changeset 123962298d5b8e530
parent 12395 d6913de7655f
child 12397 6766aa05e4eb
renamed theory Finite to Finite_Set and converted;
src/HOL/Finite.ML
src/HOL/Finite.thy
src/HOL/Finite_Set.ML
src/HOL/Finite_Set.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Finite.ML	Thu Dec 06 00:37:59 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,903 +0,0 @@
     1.4 -(*  Title:      HOL/Finite.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson & Tobias Nipkow
     1.7 -    Copyright   1995  University of Cambridge & TU Muenchen
     1.8 -
     1.9 -Finite sets and their cardinality.
    1.10 -*)
    1.11 -
    1.12 -section "finite";
    1.13 -
    1.14 -(*Discharging ~ x:y entails extra work*)
    1.15 -val major::prems = Goal 
    1.16 -    "[| finite F;  P({}); \
    1.17 -\       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
    1.18 -\    |] ==> P(F)";
    1.19 -by (rtac (major RS Finites.induct) 1);
    1.20 -by (excluded_middle_tac "a:A" 2);
    1.21 -by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
    1.22 -by (REPEAT (ares_tac prems 1));
    1.23 -qed "finite_induct";
    1.24 -
    1.25 -val major::subs::prems = Goal 
    1.26 -    "[| finite F;  F <= A; \
    1.27 -\       P({}); \
    1.28 -\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    1.29 -\    |] ==> P(F)";
    1.30 -by (rtac (subs RS rev_mp) 1);
    1.31 -by (rtac (major RS finite_induct) 1);
    1.32 -by (ALLGOALS (blast_tac (claset() addIs prems)));
    1.33 -qed "finite_subset_induct";
    1.34 -
    1.35 -Addsimps Finites.intrs;
    1.36 -AddSIs Finites.intrs;
    1.37 -
    1.38 -(*The union of two finite sets is finite*)
    1.39 -Goal "[| finite F;  finite G |] ==> finite(F Un G)";
    1.40 -by (etac finite_induct 1);
    1.41 -by (ALLGOALS Asm_simp_tac);
    1.42 -qed "finite_UnI";
    1.43 -
    1.44 -(*Every subset of a finite set is finite*)
    1.45 -Goal "finite B ==> ALL A. A<=B --> finite A";
    1.46 -by (etac finite_induct 1);
    1.47 -by (ALLGOALS (simp_tac (simpset() addsimps [subset_insert_iff])));
    1.48 -by Safe_tac;
    1.49 - by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 1);
    1.50 - by (ALLGOALS Blast_tac);
    1.51 -val lemma = result();
    1.52 -
    1.53 -Goal "[| A<=B;  finite B |] ==> finite A";
    1.54 -by (dtac lemma 1);
    1.55 -by (Blast_tac 1);
    1.56 -qed "finite_subset";
    1.57 -
    1.58 -Goal "finite(F Un G) = (finite F & finite G)";
    1.59 -by (blast_tac (claset() 
    1.60 -	         addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1);
    1.61 -qed "finite_Un";
    1.62 -AddIffs[finite_Un];
    1.63 -
    1.64 -(*The converse obviously fails*)
    1.65 -Goal "finite F | finite G ==> finite(F Int G)";
    1.66 -by (blast_tac (claset() addIs [finite_subset]) 1);
    1.67 -qed "finite_Int";
    1.68 -
    1.69 -Addsimps [finite_Int];
    1.70 -AddIs [finite_Int];
    1.71 -
    1.72 -Goal "finite(insert a A) = finite A";
    1.73 -by (stac insert_is_Un 1);
    1.74 -by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
    1.75 -by (Blast_tac 1);
    1.76 -qed "finite_insert";
    1.77 -Addsimps[finite_insert];
    1.78 -
    1.79 -(*The image of a finite set is finite *)
    1.80 -Goal  "finite F ==> finite(h`F)";
    1.81 -by (etac finite_induct 1);
    1.82 -by (Simp_tac 1);
    1.83 -by (Asm_simp_tac 1);
    1.84 -qed "finite_imageI";
    1.85 -
    1.86 -Goal "finite (range g) ==> finite (range (%x. f (g x)))";
    1.87 -by (Simp_tac 1);
    1.88 -by (etac finite_imageI 1);
    1.89 -qed "finite_range_imageI";
    1.90 -
    1.91 -val major::prems = Goal 
    1.92 -    "[| finite c;  finite b;                                  \
    1.93 -\       P(b);                                                   \
    1.94 -\       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
    1.95 -\    |] ==> c<=b --> P(b-c)";
    1.96 -by (rtac (major RS finite_induct) 1);
    1.97 -by (stac Diff_insert 2);
    1.98 -by (ALLGOALS (asm_simp_tac
    1.99 -                (simpset() addsimps prems@[Diff_subset RS finite_subset])));
   1.100 -val lemma = result();
   1.101 -
   1.102 -val prems = Goal 
   1.103 -    "[| finite A;                                       \
   1.104 -\       P(A);                                           \
   1.105 -\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   1.106 -\    |] ==> P({})";
   1.107 -by (rtac (Diff_cancel RS subst) 1);
   1.108 -by (rtac (lemma RS mp) 1);
   1.109 -by (REPEAT (ares_tac (subset_refl::prems) 1));
   1.110 -qed "finite_empty_induct";
   1.111 -
   1.112 -
   1.113 -(* finite B ==> finite (B - Ba) *)
   1.114 -bind_thm ("finite_Diff", Diff_subset RS finite_subset);
   1.115 -Addsimps [finite_Diff];
   1.116 -
   1.117 -Goal "finite(A - insert a B) = finite(A-B)";
   1.118 -by (stac Diff_insert 1);
   1.119 -by (case_tac "a : A-B" 1);
   1.120 -by (rtac (finite_insert RS sym RS trans) 1);
   1.121 -by (stac insert_Diff 1);
   1.122 -by (ALLGOALS Asm_full_simp_tac);
   1.123 -qed "finite_Diff_insert";
   1.124 -AddIffs [finite_Diff_insert];
   1.125 -
   1.126 -(*lemma merely for classical reasoner in the proof below: force_tac can't
   1.127 -  prove it.*)
   1.128 -Goal "finite(A-{}) = finite A";
   1.129 -by (Simp_tac 1);
   1.130 -val lemma = result();
   1.131 -
   1.132 -(*Lemma for proving finite_imageD*)
   1.133 -Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A";
   1.134 -by (etac finite_induct 1);
   1.135 - by (ALLGOALS Asm_simp_tac);
   1.136 -by (Clarify_tac 1);
   1.137 -by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1);
   1.138 - by (Clarify_tac 1);
   1.139 - by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
   1.140 - by (blast_tac (claset() addSDs [lemma RS iffD1]) 1);
   1.141 -by (thin_tac "ALL A. ?PP(A)" 1);
   1.142 -by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
   1.143 -by (Clarify_tac 1);
   1.144 -by (res_inst_tac [("x","xa")] bexI 1);
   1.145 -by (ALLGOALS 
   1.146 -    (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
   1.147 -val lemma = result();
   1.148 -
   1.149 -Goal "[| finite(f`A);  inj_on f A |] ==> finite A";
   1.150 -by (dtac lemma 1);
   1.151 -by (Blast_tac 1);
   1.152 -qed "finite_imageD";
   1.153 -
   1.154 -(** The finite UNION of finite sets **)
   1.155 -
   1.156 -Goal "finite A ==> (ALL a:A. finite(B a)) --> finite(UN a:A. B a)";
   1.157 -by (etac finite_induct 1);
   1.158 -by (ALLGOALS Asm_simp_tac);
   1.159 -bind_thm("finite_UN_I", ballI RSN (2, result() RS mp));
   1.160 -
   1.161 -(*strengthen RHS to 
   1.162 -    ((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})  ?  
   1.163 -  we'd need to prove
   1.164 -    finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}
   1.165 -  by induction*)
   1.166 -Goal "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))";
   1.167 -by (blast_tac (claset() addIs [finite_UN_I, finite_subset]) 1);
   1.168 -qed "finite_UN";
   1.169 -Addsimps [finite_UN];
   1.170 -
   1.171 -(** Sigma of finite sets **)
   1.172 -
   1.173 -Goalw [Sigma_def]
   1.174 - "[| finite A; ALL a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
   1.175 -by (blast_tac (claset() addSIs [finite_UN_I]) 1);
   1.176 -bind_thm("finite_SigmaI", ballI RSN (2,result()));
   1.177 -Addsimps [finite_SigmaI];
   1.178 -
   1.179 -Goal "[| finite (UNIV::'a set); finite (UNIV::'b set)|] ==> finite (UNIV::('a * 'b) set)"; 
   1.180 -by (subgoal_tac "(UNIV::('a * 'b) set) = Sigma UNIV (%x. UNIV)" 1);
   1.181 -by  (etac ssubst 1);
   1.182 -by  (etac finite_SigmaI 1);
   1.183 -by  Auto_tac;
   1.184 -qed "finite_Prod_UNIV";
   1.185 -
   1.186 -Goal "finite (UNIV :: ('a::finite * 'b::finite) set)";
   1.187 -by (rtac (finite_Prod_UNIV) 1);
   1.188 -by (rtac finite 1);
   1.189 -by (rtac finite 1);
   1.190 -qed "finite_Prod";
   1.191 -
   1.192 -Goal "finite (UNIV :: unit set)";
   1.193 -by (subgoal_tac "UNIV = {()}" 1);
   1.194 -by (etac ssubst 1);
   1.195 -by Auto_tac;
   1.196 -qed "finite_unit";
   1.197 -
   1.198 -(** The powerset of a finite set **)
   1.199 -
   1.200 -Goal "finite(Pow A) ==> finite A";
   1.201 -by (subgoal_tac "finite ((%x.{x})`A)" 1);
   1.202 -by (rtac finite_subset 2);
   1.203 -by (assume_tac 3);
   1.204 -by (ALLGOALS
   1.205 -    (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
   1.206 -val lemma = result();
   1.207 -
   1.208 -Goal "finite(Pow A) = finite A";
   1.209 -by (rtac iffI 1);
   1.210 -by (etac lemma 1);
   1.211 -(*Opposite inclusion: finite A ==> finite (Pow A) *)
   1.212 -by (etac finite_induct 1);
   1.213 -by (ALLGOALS 
   1.214 -    (asm_simp_tac
   1.215 -     (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert])));
   1.216 -qed "finite_Pow_iff";
   1.217 -AddIffs [finite_Pow_iff];
   1.218 -
   1.219 -Goal "finite(r^-1) = finite r";
   1.220 -by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1);
   1.221 - by (Asm_simp_tac 1);
   1.222 - by (rtac iffI 1);
   1.223 -  by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
   1.224 -  by (simp_tac (simpset() addsplits [split_split]) 1);
   1.225 - by (etac finite_imageI 1);
   1.226 -by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
   1.227 -by Auto_tac;
   1.228 -by (rtac bexI 1);
   1.229 -by  (assume_tac 2);
   1.230 -by (Simp_tac 1);
   1.231 -qed "finite_converse";
   1.232 -AddIffs [finite_converse];
   1.233 -
   1.234 -Goal "finite (lessThan (k::nat))";
   1.235 -by (induct_tac "k" 1);
   1.236 -by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
   1.237 -by Auto_tac;
   1.238 -qed "finite_lessThan";
   1.239 -
   1.240 -Goal "finite (atMost (k::nat))";
   1.241 -by (induct_tac "k" 1);
   1.242 -by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
   1.243 -by Auto_tac;
   1.244 -qed "finite_atMost";
   1.245 -AddIffs [finite_lessThan, finite_atMost];
   1.246 -
   1.247 -(* A bounded set of natural numbers is finite *)
   1.248 -Goal "(ALL i:N. i<(n::nat)) ==> finite N";
   1.249 -by (rtac finite_subset 1);
   1.250 - by (rtac finite_lessThan 2);
   1.251 -by Auto_tac;
   1.252 -qed "bounded_nat_set_is_finite";
   1.253 -
   1.254 -(** Finiteness of transitive closure (thanks to Sidi Ehmety) **)
   1.255 -
   1.256 -(*A finite relation has a finite field ( = domain U range) *)
   1.257 -Goal "finite r ==> finite (Field r)";
   1.258 -by (etac finite_induct 1);
   1.259 -by (auto_tac (claset(), 
   1.260 -              simpset() addsimps [Field_def, Domain_insert, Range_insert]));
   1.261 -qed "finite_Field";
   1.262 -
   1.263 -Goal "r^+ <= Field r <*> Field r";
   1.264 -by (Clarify_tac 1);
   1.265 -by (etac trancl_induct 1);
   1.266 -by (auto_tac (claset(), simpset() addsimps [Field_def]));  
   1.267 -qed "trancl_subset_Field2";
   1.268 -
   1.269 -Goal "finite (r^+) = finite r";
   1.270 -by Auto_tac;
   1.271 -by (rtac (trancl_subset_Field2 RS finite_subset) 2);
   1.272 -by (rtac finite_SigmaI 2);
   1.273 -by (blast_tac (claset() addIs [r_into_trancl, finite_subset]) 1);
   1.274 -by (auto_tac (claset(), simpset() addsimps [finite_Field]));  
   1.275 -qed "finite_trancl";
   1.276 -
   1.277 -
   1.278 -section "Finite cardinality -- 'card'";
   1.279 -
   1.280 -bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR");
   1.281 -bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR");
   1.282 -
   1.283 -AddSEs [cardR_emptyE];
   1.284 -AddSIs cardR.intrs;
   1.285 -
   1.286 -Goal "[| (A,n) : cardR |] ==> a : A --> (EX m. n = Suc m)";
   1.287 -by (etac cardR.induct 1);
   1.288 - by (Blast_tac 1);
   1.289 -by (Blast_tac 1);
   1.290 -qed "cardR_SucD";
   1.291 -
   1.292 -Goal "(A,m): cardR ==> (ALL n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
   1.293 -by (etac cardR.induct 1);
   1.294 - by Auto_tac;
   1.295 -by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
   1.296 -by Auto_tac;
   1.297 -by (ftac cardR_SucD 1);
   1.298 -by (Blast_tac 1);
   1.299 -val lemma = result();
   1.300 -
   1.301 -Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
   1.302 -by (dtac lemma 1);
   1.303 -by (Asm_full_simp_tac 1);
   1.304 -val lemma = result();
   1.305 -
   1.306 -Goal "(A,m): cardR ==> (ALL n. (A,n) : cardR --> n=m)";
   1.307 -by (etac cardR.induct 1);
   1.308 - by (safe_tac (claset() addSEs [cardR_insertE]));
   1.309 -by (rename_tac "B b m" 1 THEN case_tac "a = b" 1);
   1.310 - by (subgoal_tac "A = B" 1);
   1.311 -  by (blast_tac (claset() addEs [equalityE]) 2);
   1.312 - by (Blast_tac 1);
   1.313 -by (subgoal_tac "EX C. A = insert b C & B = insert a C" 1);
   1.314 - by (res_inst_tac [("x","A Int B")] exI 2);
   1.315 - by (blast_tac (claset() addEs [equalityE]) 2);
   1.316 -by (forw_inst_tac [("A","B")] cardR_SucD 1);
   1.317 -by (blast_tac (claset() addDs [lemma]) 1);
   1.318 -qed_spec_mp "cardR_determ";
   1.319 -
   1.320 -Goal "(A,n) : cardR ==> finite(A)";
   1.321 -by (etac cardR.induct 1);
   1.322 -by Auto_tac;
   1.323 -qed "cardR_imp_finite";
   1.324 -
   1.325 -Goal "finite(A) ==> EX n. (A, n) : cardR";
   1.326 -by (etac finite_induct 1);
   1.327 -by Auto_tac;
   1.328 -qed "finite_imp_cardR";
   1.329 -
   1.330 -Goalw [card_def] "(A,n) : cardR ==> card A = n";
   1.331 -by (blast_tac (claset() addIs [cardR_determ]) 1);
   1.332 -qed "card_equality";
   1.333 -
   1.334 -Goalw [card_def] "card {} = 0";
   1.335 -by (Blast_tac 1);
   1.336 -qed "card_empty";
   1.337 -Addsimps [card_empty];
   1.338 -
   1.339 -Goal "x ~: A \
   1.340 -\     ==> ((insert x A, n) : cardR)  =  (EX m. (A, m) : cardR & n = Suc m)";
   1.341 -by Auto_tac;
   1.342 -by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1);
   1.343 -by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1);
   1.344 -by (blast_tac (claset() addIs [cardR_determ]) 1);
   1.345 -val lemma = result();
   1.346 -
   1.347 -Goalw [card_def]
   1.348 -     "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
   1.349 -by (asm_simp_tac (simpset() addsimps [lemma]) 1);
   1.350 -by (rtac the_equality 1);
   1.351 -by (auto_tac (claset() addIs [finite_imp_cardR],
   1.352 -	      simpset() addcongs [conj_cong]
   1.353 -		        addsimps [symmetric card_def,
   1.354 -				  card_equality]));
   1.355 -qed "card_insert_disjoint";
   1.356 -Addsimps [card_insert_disjoint];
   1.357 -
   1.358 -(* Delete rules to do with cardR relation: obsolete *)
   1.359 -Delrules [cardR_emptyE];
   1.360 -Delrules cardR.intrs;
   1.361 -
   1.362 -Goal "finite A ==> (card A = 0) = (A = {})";
   1.363 -by Auto_tac;
   1.364 -by (dres_inst_tac [("a","x")] mk_disjoint_insert 1);
   1.365 -by (Clarify_tac 1);
   1.366 -by (rotate_tac ~1 1);
   1.367 -by Auto_tac;
   1.368 -qed "card_0_eq";
   1.369 -Addsimps[card_0_eq];
   1.370 -
   1.371 -Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))";
   1.372 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
   1.373 -qed "card_insert_if";
   1.374 -
   1.375 -Goal "[| finite A; x: A |] ==> Suc (card (A-{x})) = card A";
   1.376 -by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
   1.377 -by (assume_tac 1);
   1.378 -by (Asm_simp_tac 1);
   1.379 -qed "card_Suc_Diff1";
   1.380 -
   1.381 -Goal "[| finite A; x: A |] ==> card (A-{x}) = card A - 1";
   1.382 -by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1 RS sym]) 1);
   1.383 -qed "card_Diff_singleton";
   1.384 -
   1.385 -Goal "finite A ==> card (A-{x}) = (if x:A then card A - 1 else card A)";
   1.386 -by (asm_simp_tac (simpset() addsimps [card_Diff_singleton]) 1);
   1.387 -qed "card_Diff_singleton_if";
   1.388 -
   1.389 -Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   1.390 -by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1);
   1.391 -qed "card_insert";
   1.392 -
   1.393 -Goal "finite A ==> card A <= card (insert x A)";
   1.394 -by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1);
   1.395 -qed "card_insert_le";
   1.396 -
   1.397 -Goal "finite B ==> ALL A. A <= B --> card B <= card A --> A = B";
   1.398 -by (etac finite_induct 1);
   1.399 - by (Simp_tac 1);
   1.400 -by (Clarify_tac 1);
   1.401 -by (subgoal_tac "finite A & A-{x} <= F" 1);
   1.402 - by (blast_tac (claset() addIs [finite_subset]) 2); 
   1.403 -by (dres_inst_tac [("x","A-{x}")] spec 1); 
   1.404 -by (asm_full_simp_tac (simpset() addsimps [card_Diff_singleton_if]
   1.405 -                                 addsplits [split_if_asm]) 1); 
   1.406 -by (case_tac "card A" 1);
   1.407 -by Auto_tac; 
   1.408 -qed_spec_mp "card_seteq";
   1.409 -
   1.410 -Goalw [psubset_def] "[| finite B;  A < B |] ==> card A < card B";
   1.411 -by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
   1.412 -by (blast_tac (claset() addDs [card_seteq]) 1); 
   1.413 -qed "psubset_card_mono" ;
   1.414 -
   1.415 -Goal "[| finite B;  A <= B |] ==> card A <= card B";
   1.416 -by (case_tac "A=B" 1);
   1.417 - by (Asm_simp_tac 1); 
   1.418 -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
   1.419 -by (blast_tac (claset() addDs [card_seteq] addIs [order_less_imp_le]) 1); 
   1.420 -qed "card_mono" ;
   1.421 -
   1.422 -Goal "[| finite A; finite B |] \
   1.423 -\     ==> card A + card B = card (A Un B) + card (A Int B)";
   1.424 -by (etac finite_induct 1);
   1.425 -by (Simp_tac 1);
   1.426 -by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1);
   1.427 -qed "card_Un_Int";
   1.428 -
   1.429 -Goal "[| finite A; finite B; A Int B = {} |] \
   1.430 -\     ==> card (A Un B) = card A + card B";
   1.431 -by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1);
   1.432 -qed "card_Un_disjoint";
   1.433 -
   1.434 -Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
   1.435 -by (subgoal_tac "(A-B) Un B = A" 1);
   1.436 -by (Blast_tac 2);
   1.437 -by (rtac (add_right_cancel RS iffD1) 1);
   1.438 -by (rtac (card_Un_disjoint RS subst) 1);
   1.439 -by (etac ssubst 4);
   1.440 -by (Blast_tac 3);
   1.441 -by (ALLGOALS 
   1.442 -    (asm_simp_tac
   1.443 -     (simpset() addsimps [add_commute, not_less_iff_le, 
   1.444 -			  add_diff_inverse, card_mono, finite_subset])));
   1.445 -qed "card_Diff_subset";
   1.446 -
   1.447 -Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
   1.448 -by (rtac Suc_less_SucD 1);
   1.449 -by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
   1.450 -qed "card_Diff1_less";
   1.451 -
   1.452 -Goal "[| finite A; x: A; y: A |] ==> card(A-{x}-{y}) < card A"; 
   1.453 -by (case_tac "x=y" 1);
   1.454 -by (asm_simp_tac (simpset() addsimps [card_Diff1_less]) 1);
   1.455 -by (rtac less_trans 1);
   1.456 -by (ALLGOALS (force_tac (claset() addSIs [card_Diff1_less], simpset())));
   1.457 -qed "card_Diff2_less";
   1.458 -
   1.459 -Goal "finite A ==> card(A-{x}) <= card A";
   1.460 -by (case_tac "x: A" 1);
   1.461 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le])));
   1.462 -qed "card_Diff1_le";
   1.463 -
   1.464 -Goal "[| finite B; A <= B; card A < card B |] ==> A < B";
   1.465 -by (etac psubsetI 1);
   1.466 -by (Blast_tac 1);
   1.467 -qed "card_psubset";
   1.468 -
   1.469 -(*** Cardinality of image ***)
   1.470 -
   1.471 -Goal "finite A ==> card (f ` A) <= card A";
   1.472 -by (etac finite_induct 1);
   1.473 - by (Simp_tac 1);
   1.474 -by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI, 
   1.475 -				      card_insert_if]) 1);
   1.476 -qed "card_image_le";
   1.477 -
   1.478 -Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A";
   1.479 -by (etac finite_induct 1);
   1.480 -by (ALLGOALS Asm_simp_tac);
   1.481 -by Safe_tac;
   1.482 -by (rewtac inj_on_def);
   1.483 -by (Blast_tac 1);
   1.484 -by (stac card_insert_disjoint 1);
   1.485 -by (etac finite_imageI 1);
   1.486 -by (Blast_tac 1);
   1.487 -by (Blast_tac 1);
   1.488 -qed_spec_mp "card_image";
   1.489 -
   1.490 -Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A";
   1.491 -by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
   1.492 -qed "endo_inj_surj";
   1.493 -
   1.494 -(*** Cardinality of the Powerset ***)
   1.495 -
   1.496 -Goal "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A";  (* FIXME numeral 2 (!?) *)
   1.497 -by (etac finite_induct 1);
   1.498 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
   1.499 -by (stac card_Un_disjoint 1);
   1.500 -by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
   1.501 -by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
   1.502 -by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
   1.503 -by (rewtac inj_on_def);
   1.504 -by (blast_tac (claset() addSEs [equalityE]) 1);
   1.505 -qed "card_Pow";
   1.506 -
   1.507 -
   1.508 -(*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   1.509 -  The "finite C" premise is redundant*)
   1.510 -Goal "finite C ==> finite (Union C) --> \
   1.511 -\          (ALL c : C. k dvd card c) -->  \
   1.512 -\          (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
   1.513 -\          --> k dvd card(Union C)";
   1.514 -by (etac finite_induct 1);
   1.515 -by (ALLGOALS Asm_simp_tac);
   1.516 -by (Clarify_tac 1);
   1.517 -by (stac card_Un_disjoint 1);
   1.518 -by (ALLGOALS
   1.519 -    (asm_full_simp_tac (simpset()
   1.520 -			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
   1.521 -by (thin_tac "ALL c:F. ?PP(c)" 1);
   1.522 -by (thin_tac "ALL c:F. ?PP(c) & ?QQ(c)" 1);
   1.523 -by (Clarify_tac 1);
   1.524 -by (ball_tac 1);
   1.525 -by (Blast_tac 1);
   1.526 -qed_spec_mp "dvd_partition";
   1.527 -
   1.528 -
   1.529 -(*** foldSet ***)
   1.530 -
   1.531 -bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e");
   1.532 -
   1.533 -AddSEs [empty_foldSetE];
   1.534 -AddIs foldSet.intrs;
   1.535 -
   1.536 -Goal "[| (A-{x},y) : foldSet f e;  x: A |] ==> (A, f x y) : foldSet f e";
   1.537 -by (etac (insert_Diff RS subst) 1 THEN resolve_tac foldSet.intrs 1);
   1.538 -by Auto_tac;
   1.539 -qed "Diff1_foldSet";
   1.540 -
   1.541 -Goal "(A, x) : foldSet f e ==> finite(A)";
   1.542 -by (eresolve_tac [foldSet.induct] 1);
   1.543 -by Auto_tac;
   1.544 -qed "foldSet_imp_finite";
   1.545 -
   1.546 -Addsimps [foldSet_imp_finite];
   1.547 -
   1.548 -
   1.549 -Goal "finite(A) ==> EX x. (A, x) : foldSet f e";
   1.550 -by (etac finite_induct 1);
   1.551 -by Auto_tac;
   1.552 -qed "finite_imp_foldSet";
   1.553 -
   1.554 -
   1.555 -Open_locale "LC"; 
   1.556 -
   1.557 -val f_lcomm = thm "lcomm";
   1.558 -
   1.559 -
   1.560 -Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
   1.561 -\            (ALL y. (A, y) : foldSet f e --> y=x)";
   1.562 -by (induct_tac "n" 1);
   1.563 -by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
   1.564 -by (etac foldSet.elim 1);
   1.565 -by (Blast_tac 1);
   1.566 -by (etac foldSet.elim 1);
   1.567 -by (Blast_tac 1);
   1.568 -by (Clarify_tac 1);
   1.569 -(*force simplification of "card A < card (insert ...)"*)
   1.570 -by (etac rev_mp 1);
   1.571 -by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
   1.572 -by (rtac impI 1);
   1.573 -(** LEVEL 10 **)
   1.574 -by (rename_tac "Aa xa ya Ab xb yb" 1 THEN case_tac "xa=xb" 1);
   1.575 - by (subgoal_tac "Aa = Ab" 1);
   1.576 - by (blast_tac (claset() addSEs [equalityE]) 2);
   1.577 - by (Blast_tac 1);
   1.578 -(*case xa ~= xb*)
   1.579 -by (subgoal_tac "Aa-{xb} = Ab-{xa} & xb : Aa & xa : Ab" 1);
   1.580 - by (blast_tac (claset() addSEs [equalityE]) 2);
   1.581 -by (Clarify_tac 1);
   1.582 -by (subgoal_tac "Aa = insert xb Ab - {xa}" 1);
   1.583 - by (Blast_tac 2);
   1.584 -(** LEVEL 20 **)
   1.585 -by (subgoal_tac "card Aa <= card Ab" 1);
   1.586 - by (rtac (Suc_le_mono RS subst) 2);
   1.587 - by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2);
   1.588 -by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] 
   1.589 -    (finite_imp_foldSet RS exE) 1);
   1.590 -by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1);
   1.591 -by (ftac Diff1_foldSet 1 THEN assume_tac 1);
   1.592 -by (subgoal_tac "ya = f xb x" 1);
   1.593 - by (blast_tac (claset() delrules [equalityCE]) 2);
   1.594 -by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1);
   1.595 - by (Asm_full_simp_tac 2);
   1.596 -by (subgoal_tac "yb = f xa x" 1);
   1.597 - by (blast_tac (claset() delrules [equalityCE]
   1.598 -			addDs [Diff1_foldSet]) 2);
   1.599 -by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
   1.600 -val lemma = result();
   1.601 -
   1.602 -
   1.603 -Goal "[| (A, x) : foldSet f e;  (A, y) : foldSet f e |] ==> y=x";
   1.604 -by (blast_tac (claset() addIs [ObjectLogic.rulify lemma]) 1);
   1.605 -qed "foldSet_determ";
   1.606 -
   1.607 -Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
   1.608 -by (blast_tac (claset() addIs [foldSet_determ]) 1);
   1.609 -qed "fold_equality";
   1.610 -
   1.611 -Goalw [fold_def] "fold f e {} = e";
   1.612 -by (Blast_tac 1);
   1.613 -qed "fold_empty";
   1.614 -Addsimps [fold_empty];
   1.615 -
   1.616 -
   1.617 -Goal "x ~: A ==> \
   1.618 -\     ((insert x A, v) : foldSet f e) =  \
   1.619 -\     (EX y. (A, y) : foldSet f e & v = f x y)";
   1.620 -by Auto_tac;
   1.621 -by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1);
   1.622 -by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1);
   1.623 -by (blast_tac (claset() addIs [foldSet_determ]) 1);
   1.624 -val lemma = result();
   1.625 -
   1.626 -Goalw [fold_def]
   1.627 -     "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
   1.628 -by (asm_simp_tac (simpset() addsimps [lemma]) 1);
   1.629 -by (rtac the_equality 1);
   1.630 -by (auto_tac (claset() addIs [finite_imp_foldSet],
   1.631 -	      simpset() addcongs [conj_cong]
   1.632 -		        addsimps [symmetric fold_def,
   1.633 -				  fold_equality]));
   1.634 -qed "fold_insert";
   1.635 -
   1.636 -Goal "finite A ==> ALL e. f x (fold f e A) = fold f (f x e) A";
   1.637 -by (etac finite_induct 1);
   1.638 -by (Simp_tac 1);
   1.639 -by (asm_simp_tac (simpset() addsimps [f_lcomm, fold_insert]) 1);
   1.640 -qed_spec_mp "fold_commute";
   1.641 -
   1.642 -Goal "[| finite A; finite B |] \
   1.643 -\     ==> fold f (fold f e B) A  =  fold f (fold f e (A Int B)) (A Un B)";
   1.644 -by (etac finite_induct 1);
   1.645 -by (Simp_tac 1);
   1.646 -by (asm_simp_tac (simpset() addsimps [fold_insert, fold_commute, 
   1.647 -	                              Int_insert_left, insert_absorb]) 1);
   1.648 -qed "fold_nest_Un_Int";
   1.649 -
   1.650 -Goal "[| finite A; finite B; A Int B = {} |] \
   1.651 -\     ==> fold f e (A Un B)  =  fold f (fold f e B) A";
   1.652 -by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
   1.653 -qed "fold_nest_Un_disjoint";
   1.654 -
   1.655 -(* Delete rules to do with foldSet relation: obsolete *)
   1.656 -Delsimps [foldSet_imp_finite];
   1.657 -Delrules [empty_foldSetE];
   1.658 -Delrules foldSet.intrs;
   1.659 -
   1.660 -Close_locale "LC";
   1.661 -
   1.662 -Open_locale "ACe"; 
   1.663 -
   1.664 -(*We enter a more restrictive framework, with f :: ['a,'a] => 'a
   1.665 -    instead of ['b,'a] => 'a 
   1.666 -  At present, none of these results are used!*)
   1.667 -
   1.668 -val f_ident   = thm "ident";
   1.669 -val f_commute = thm "commute";
   1.670 -val f_assoc   = thm "assoc";
   1.671 -
   1.672 -
   1.673 -Goal "f x (f y z) = f y (f x z)";
   1.674 -by (rtac (f_commute RS trans) 1);
   1.675 -by (rtac (f_assoc RS trans) 1);
   1.676 -by (rtac (f_commute RS arg_cong) 1);
   1.677 -qed "f_left_commute";
   1.678 -
   1.679 -val f_ac = [f_assoc, f_commute, f_left_commute];
   1.680 -
   1.681 -Goal "f e x = x";
   1.682 -by (stac f_commute 1);
   1.683 -by (rtac f_ident 1);
   1.684 -qed "f_left_ident";
   1.685 -
   1.686 -val f_idents = [f_left_ident, f_ident];
   1.687 -
   1.688 -Goal "[| finite A; finite B |] \
   1.689 -\     ==> f (fold f e A) (fold f e B) =  \
   1.690 -\         f (fold f e (A Un B)) (fold f e (A Int B))";
   1.691 -by (etac finite_induct 1);
   1.692 -by (simp_tac (simpset() addsimps f_idents) 1);
   1.693 -by (asm_simp_tac (simpset() addsimps f_ac @ f_idents @
   1.694 -           [export fold_insert,insert_absorb, Int_insert_left]) 1);
   1.695 -qed "fold_Un_Int";
   1.696 -
   1.697 -Goal "[| finite A; finite B; A Int B = {} |] \
   1.698 -\     ==> fold f e (A Un B) = f (fold f e A) (fold f e B)";
   1.699 -by (asm_simp_tac (simpset() addsimps fold_Un_Int::f_idents) 1);
   1.700 -qed "fold_Un_disjoint";
   1.701 -
   1.702 -Goal
   1.703 - "[| finite A; finite B |] ==> A Int B = {} --> \
   1.704 -\      fold (f o g) e (A Un B) = f (fold (f o g) e A) (fold (f o g) e B)";
   1.705 -by (etac finite_induct 1);
   1.706 -by (simp_tac (simpset() addsimps f_idents) 1);
   1.707 -by (asm_full_simp_tac (simpset() addsimps f_ac @ f_idents @
   1.708 -           [export fold_insert,insert_absorb, Int_insert_left]) 1);
   1.709 -qed "fold_Un_disjoint2";
   1.710 -
   1.711 -Close_locale "ACe";
   1.712 -
   1.713 -
   1.714 -(*** setsum: generalized summation over a set ***)
   1.715 -
   1.716 -Goalw [setsum_def] "setsum f {} = 0";
   1.717 -by (Simp_tac 1);
   1.718 -qed "setsum_empty";
   1.719 -Addsimps [setsum_empty];
   1.720 -
   1.721 -Goalw [setsum_def]
   1.722 - "!!f. [| finite F; a ~: F |] ==> \
   1.723 -\      setsum f (insert a F) = f a + setsum f F";
   1.724 -by (asm_simp_tac (simpset() addsimps [export fold_insert,
   1.725 -				      thm "plus_ac0_left_commute"]) 1);
   1.726 -qed "setsum_insert";
   1.727 -Addsimps [setsum_insert];
   1.728 -
   1.729 -Goal "setsum (%i. 0) A = 0";
   1.730 -by (case_tac "finite A" 1);
   1.731 - by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); 
   1.732 -by (etac finite_induct 1);
   1.733 -by Auto_tac;
   1.734 -qed "setsum_0";
   1.735 -
   1.736 -Goal "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))";
   1.737 -by (etac finite_induct 1);
   1.738 -by Auto_tac;
   1.739 -qed "setsum_eq_0_iff";
   1.740 -Addsimps [setsum_eq_0_iff];
   1.741 -
   1.742 -Goal "setsum f A = Suc n ==> EX a:A. 0 < f a";
   1.743 -by (case_tac "finite A" 1);
   1.744 - by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
   1.745 -by (etac rev_mp 1);
   1.746 -by (etac finite_induct 1);
   1.747 -by Auto_tac;
   1.748 -qed "setsum_SucD";
   1.749 -
   1.750 -(*Could allow many "card" proofs to be simplified*)
   1.751 -Goal "finite A ==> card A = setsum (%x. 1) A";
   1.752 -by (etac finite_induct 1);
   1.753 -by Auto_tac;
   1.754 -qed "card_eq_setsum";
   1.755 -
   1.756 -(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
   1.757 -Goal "!!g. [| finite A; finite B |] \
   1.758 -\     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B";
   1.759 -by (etac finite_induct 1);
   1.760 -by (Simp_tac 1);
   1.761 -by (asm_full_simp_tac (simpset() addsimps (thms "plus_ac0") @ 
   1.762 -                                          [Int_insert_left, insert_absorb]) 1);
   1.763 -qed "setsum_Un_Int";
   1.764 -
   1.765 -Goal "[| finite A; finite B; A Int B = {} |] \
   1.766 -\     ==> setsum g (A Un B) = setsum g A + setsum g B";
   1.767 -by (stac (setsum_Un_Int RS sym) 1);
   1.768 -by Auto_tac;
   1.769 -qed "setsum_Un_disjoint";
   1.770 -
   1.771 -Goal "!!f::'a=>'b::plus_ac0. finite I \
   1.772 -\     ==> (ALL i:I. finite (A i)) --> \
   1.773 -\         (ALL i:I. ALL j:I. i~=j --> A i Int A j = {}) --> \
   1.774 -\         setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"; 
   1.775 -by (etac finite_induct 1);
   1.776 - by (Simp_tac 1);
   1.777 -by (Clarify_tac 1); 
   1.778 -by (subgoal_tac "ALL i:F. x ~= i" 1);
   1.779 - by (Blast_tac 2); 
   1.780 -by (subgoal_tac "A x Int UNION F A = {}" 1);
   1.781 - by (Blast_tac 2); 
   1.782 -by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
   1.783 -qed_spec_mp "setsum_UN_disjoint";
   1.784 -
   1.785 -Goal "setsum (%x. f x + g x) A = (setsum f A + setsum g A)";
   1.786 -by (case_tac "finite A" 1);
   1.787 - by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
   1.788 -by (etac finite_induct 1);
   1.789 -by Auto_tac;
   1.790 -by (simp_tac (simpset() addsimps (thms "plus_ac0")) 1);
   1.791 -qed "setsum_addf";
   1.792 -
   1.793 -(** For the natural numbers, we have subtraction **)
   1.794 -
   1.795 -Goal "[| finite A; finite B |] \
   1.796 -\     ==> (setsum f (A Un B) :: nat) = \
   1.797 -\         setsum f A + setsum f B - setsum f (A Int B)";
   1.798 -by (stac (setsum_Un_Int RS sym) 1);
   1.799 -by Auto_tac;
   1.800 -qed "setsum_Un";
   1.801 -
   1.802 -Goal "(setsum f (A-{a}) :: nat) = \
   1.803 -\     (if a:A then setsum f A - f a else setsum f A)";
   1.804 -by (case_tac "finite A" 1);
   1.805 - by (asm_full_simp_tac (simpset() addsimps [setsum_def]) 2); 
   1.806 -by (etac finite_induct 1);
   1.807 -by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
   1.808 -by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   1.809 -by Auto_tac;
   1.810 -qed_spec_mp "setsum_diff1";
   1.811 -
   1.812 -val prems = Goal
   1.813 -    "[| A = B; !!x. x:B ==> f x = g x|] \
   1.814 -\    ==> setsum f A = setsum g B";
   1.815 -by (case_tac "finite B" 1);
   1.816 - by (asm_simp_tac (simpset() addsimps [setsum_def]@prems) 2); 
   1.817 -by (simp_tac (simpset() addsimps prems) 1);
   1.818 -by (subgoal_tac 
   1.819 -    "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C" 1);
   1.820 - by (asm_simp_tac (simpset() addsimps prems) 1); 
   1.821 -by (etac finite_induct 1);
   1.822 - by (Simp_tac 1);
   1.823 -by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); 
   1.824 -by (Clarify_tac 1); 
   1.825 -by (subgoal_tac "finite C" 1);
   1.826 - by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2); 
   1.827 -by (subgoal_tac "C = insert x (C-{x})" 1); 
   1.828 - by (Blast_tac 2); 
   1.829 -by (etac ssubst 1); 
   1.830 -by (dtac spec 1); 
   1.831 -by (mp_tac 1);
   1.832 -by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1); 
   1.833 -qed "setsum_cong";
   1.834 -
   1.835 -
   1.836 -(*** Basic theorem about "choose".  By Florian Kammueller, tidied by LCP ***)
   1.837 -
   1.838 -Goal "finite A ==> card {B. B <= A & card B = 0} = 1";
   1.839 -by (asm_simp_tac (simpset() addcongs [conj_cong]
   1.840 -	 	            addsimps [finite_subset RS card_0_eq]) 1);
   1.841 -by (simp_tac (simpset() addcongs [rev_conj_cong]) 1);
   1.842 -qed "card_s_0_eq_empty";
   1.843 -
   1.844 -Goal "[| finite M; x ~: M |] \
   1.845 -\  ==> {s. s <= insert x M & card(s) = Suc k} \
   1.846 -\      = {s. s <= M & card(s) = Suc k} Un \
   1.847 -\        {s. EX t. t <= M & card(t) = k & s = insert x t}";
   1.848 -by Safe_tac;
   1.849 -by (auto_tac (claset() addIs [finite_subset RS card_insert_disjoint], 
   1.850 -	      simpset()));
   1.851 -by (dres_inst_tac [("x","xa - {x}")] spec 1);
   1.852 -by (subgoal_tac ("x ~: xa") 1);
   1.853 -by Auto_tac;
   1.854 -by (etac rev_mp 1 THEN stac card_Diff_singleton 1);
   1.855 -by (auto_tac (claset() addIs [finite_subset], simpset()));
   1.856 -qed "choose_deconstruct";
   1.857 -
   1.858 -Goal "[| finite(A); finite(B);  f`A <= B;  inj_on f A |] \
   1.859 -\     ==> card A <= card B";
   1.860 -by (auto_tac (claset() addIs [card_mono], 
   1.861 -	      simpset() addsimps [card_image RS sym]));
   1.862 -qed "card_inj_on_le";
   1.863 -
   1.864 -Goal "[| finite A; finite B; \
   1.865 -\        f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \
   1.866 -\     ==> card(A) = card(B)";
   1.867 -by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
   1.868 -qed "card_bij_eq";
   1.869 -
   1.870 -Goal "[| finite A; x ~: A |]  \
   1.871 -\     ==> card{B. EX C. C <= A & card(C) = k & B = insert x C} = \
   1.872 -\         card {B. B <= A & card(B) = k}";
   1.873 -by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1);
   1.874 -by (res_inst_tac [("B","Pow(insert x A)")] finite_subset 1);
   1.875 -by (res_inst_tac [("B","Pow(A)")] finite_subset 3);
   1.876 -by (REPEAT(Fast_tac 1));
   1.877 -(* arity *)
   1.878 -by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def]));
   1.879 -by (stac Diff_insert0 1);
   1.880 -by Auto_tac;
   1.881 -qed "constr_bij";
   1.882 -
   1.883 -(* Main theorem: combinatorial theorem about number of subsets of a set *)
   1.884 -Goal "(ALL A. finite A --> card {B. B <= A & card B = k} = (card A choose k))";
   1.885 -by (induct_tac "k" 1);
   1.886 - by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1);
   1.887 -(* first 0 case finished *)
   1.888 -(* prepare finite set induction *)
   1.889 -by (rtac allI 1 THEN rtac impI 1);
   1.890 -(* second induction *)
   1.891 -by (etac finite_induct 1);
   1.892 -by (ALLGOALS
   1.893 -    (asm_simp_tac (simpset() addcongs [conj_cong] 
   1.894 -                     addsimps [card_s_0_eq_empty, choose_deconstruct])));
   1.895 -by (stac card_Un_disjoint 1);
   1.896 -   by (force_tac (claset(), simpset() addsimps [constr_bij]) 4);
   1.897 -  by (Force_tac 3);
   1.898 - by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2, 
   1.899 -			 inst "B" "Pow (insert ?x ?F)" finite_subset]) 2);
   1.900 -by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2 
   1.901 -			       RSN (2, finite_subset)]) 1);
   1.902 -qed "n_sub_lemma";
   1.903 -
   1.904 -Goal "finite A ==> card {B. B <= A & card(B) = k} = ((card A) choose k)";
   1.905 -by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1);
   1.906 -qed "n_subsets";
     2.1 --- a/src/HOL/Finite.thy	Thu Dec 06 00:37:59 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,87 +0,0 @@
     2.4 -(*  Title:      HOL/Finite.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson & Tobias Nipkow
     2.7 -    Copyright   1995  University of Cambridge & TU Muenchen
     2.8 -
     2.9 -Finite sets, their cardinality, and a fold functional.
    2.10 -*)
    2.11 -
    2.12 -Finite = Divides + Power + Inductive + SetInterval +
    2.13 -
    2.14 -consts Finites :: 'a set set
    2.15 -
    2.16 -inductive "Finites"
    2.17 -  intrs
    2.18 -    emptyI  "{} : Finites"
    2.19 -    insertI "A : Finites ==> insert a A : Finites"
    2.20 -
    2.21 -syntax finite :: 'a set => bool
    2.22 -translations  "finite A"  ==  "A : Finites"
    2.23 -
    2.24 -axclass	finite < type
    2.25 -  finite "finite UNIV"
    2.26 -
    2.27 -(* This definition, although traditional, is ugly to work with
    2.28 -constdefs
    2.29 -  card :: 'a set => nat
    2.30 -  "card A == LEAST n. ? f. A = {f i |i. i<n}"
    2.31 -Therefore we have switched to an inductive one:
    2.32 -*)
    2.33 -
    2.34 -consts cardR :: "('a set * nat) set"
    2.35 -
    2.36 -inductive cardR
    2.37 -intrs
    2.38 -  EmptyI  "({},0) : cardR"
    2.39 -  InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
    2.40 -
    2.41 -constdefs
    2.42 - card :: 'a set => nat
    2.43 - "card A == THE n. (A,n) : cardR"
    2.44 -
    2.45 -(*
    2.46 -A "fold" functional for finite sets.  For n non-negative we have
    2.47 -    fold f e {x1,...,xn} = f x1 (... (f xn e))
    2.48 -where f is at least left-commutative.
    2.49 -*)
    2.50 -
    2.51 -consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
    2.52 -
    2.53 -inductive "foldSet f e"
    2.54 -  intrs
    2.55 -    emptyI   "({}, e) : foldSet f e"
    2.56 -
    2.57 -    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
    2.58 -	      ==> (insert x A, f x y) : foldSet f e"
    2.59 -
    2.60 -constdefs
    2.61 -  fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    2.62 -  "fold f e A == THE x. (A,x) : foldSet f e"
    2.63 -
    2.64 -  setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
    2.65 -  "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
    2.66 -
    2.67 -syntax
    2.68 -  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_:_. _" [0, 51, 10] 10)
    2.69 -syntax (xsymbols)
    2.70 -  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
    2.71 -translations
    2.72 -  "\\<Sum>i:A. b" == "setsum (%i. b) A"  (* Beware of argument permutation! *)
    2.73 -
    2.74 -
    2.75 -locale LC =
    2.76 -  fixes
    2.77 -    f    :: ['b,'a] => 'a
    2.78 -  assumes
    2.79 -    lcomm    "f x (f y z) = f y (f x z)"
    2.80 -
    2.81 -locale ACe =
    2.82 -  fixes 
    2.83 -    f    :: ['a,'a] => 'a
    2.84 -    e    :: 'a
    2.85 -  assumes
    2.86 -    ident    "f x e = x"
    2.87 -    commute  "f x y = f y x"
    2.88 -    assoc    "f (f x y) z = f x (f y z)"
    2.89 -
    2.90 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Finite_Set.ML	Thu Dec 06 00:38:55 2001 +0100
     3.3 @@ -0,0 +1,128 @@
     3.4 +
     3.5 +(* legacy ML bindings *)
     3.6 +
     3.7 +structure Finites =
     3.8 +struct
     3.9 +  val intrs = thms "Finites.intros";
    3.10 +  val elims = thms "Finites.cases";
    3.11 +  val elim = thm "Finites.cases";
    3.12 +  val induct = thm "Finites.induct";
    3.13 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
    3.14 +  val [emptyI, insertI] = thms "Finites.intros";
    3.15 +end;
    3.16 +
    3.17 +structure cardR =
    3.18 +struct
    3.19 +  val intrs = thms "cardR.intros";
    3.20 +  val elims = thms "cardR.cases";
    3.21 +  val elim = thm "cardR.cases";
    3.22 +  val induct = thm "cardR.induct";
    3.23 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.cardR";
    3.24 +  val [EmptyI, InsertI] = thms "cardR.intros";
    3.25 +end;
    3.26 +
    3.27 +structure foldSet =
    3.28 +struct
    3.29 +  val intrs = thms "foldSet.intros";
    3.30 +  val elims = thms "foldSet.cases";
    3.31 +  val elim = thm "foldSet.cases";
    3.32 +  val induct = thm "foldSet.induct";
    3.33 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
    3.34 +  val [emptyI, insertI] = thms "foldSet.intros";
    3.35 +end;
    3.36 +
    3.37 +val Diff1_foldSet = thm "Diff1_foldSet";
    3.38 +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
    3.39 +val cardR_SucD = thm "cardR_SucD";
    3.40 +val cardR_determ = thm "cardR_determ";
    3.41 +val cardR_emptyE = thm "cardR_emptyE";
    3.42 +val cardR_imp_finite = thm "cardR_imp_finite";
    3.43 +val cardR_insertE = thm "cardR_insertE";
    3.44 +val card_0_eq = thm "card_0_eq";
    3.45 +val card_Diff1_le = thm "card_Diff1_le";
    3.46 +val card_Diff1_less = thm "card_Diff1_less";
    3.47 +val card_Diff2_less = thm "card_Diff2_less";
    3.48 +val card_Diff_singleton = thm "card_Diff_singleton";
    3.49 +val card_Diff_singleton_if = thm "card_Diff_singleton_if";
    3.50 +val card_Diff_subset = thm "card_Diff_subset";
    3.51 +val card_Pow = thm "card_Pow";
    3.52 +val card_Suc_Diff1 = thm "card_Suc_Diff1";
    3.53 +val card_Un_Int = thm "card_Un_Int";
    3.54 +val card_Un_disjoint = thm "card_Un_disjoint";
    3.55 +val card_bij_eq = thm "card_bij_eq";
    3.56 +val card_def = thm "card_def";
    3.57 +val card_empty = thm "card_empty";
    3.58 +val card_eq_setsum = thm "card_eq_setsum";
    3.59 +val card_equality = thm "card_equality";
    3.60 +val card_image = thm "card_image";
    3.61 +val card_image_le = thm "card_image_le";
    3.62 +val card_inj_on_le = thm "card_inj_on_le";
    3.63 +val card_insert = thm "card_insert";
    3.64 +val card_insert_disjoint = thm "card_insert_disjoint";
    3.65 +val card_insert_if = thm "card_insert_if";
    3.66 +val card_insert_le = thm "card_insert_le";
    3.67 +val card_mono = thm "card_mono";
    3.68 +val card_psubset = thm "card_psubset";
    3.69 +val card_s_0_eq_empty = thm "card_s_0_eq_empty";
    3.70 +val card_seteq = thm "card_seteq";
    3.71 +val choose_deconstruct = thm "choose_deconstruct";
    3.72 +val constr_bij = thm "constr_bij";
    3.73 +val dvd_partition = thm "dvd_partition";
    3.74 +val empty_foldSetE = thm "empty_foldSetE";
    3.75 +val endo_inj_surj = thm "endo_inj_surj";
    3.76 +val finite = thm "finite";
    3.77 +val finiteI = thm "finiteI";
    3.78 +val finite_Diff = thm "finite_Diff";
    3.79 +val finite_Diff_insert = thm "finite_Diff_insert";
    3.80 +val finite_Field = thm "finite_Field";
    3.81 +val finite_Int = thm "finite_Int";
    3.82 +val finite_Pow_iff = thm "finite_Pow_iff";
    3.83 +val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    3.84 +val finite_SigmaI = thm "finite_SigmaI";
    3.85 +val finite_UN = thm "finite_UN";
    3.86 +val finite_UN_I = thm "finite_UN_I";
    3.87 +val finite_Un = thm "finite_Un";
    3.88 +val finite_UnI = thm "finite_UnI";
    3.89 +val finite_atMost = thm "finite_atMost";
    3.90 +val finite_converse = thm "finite_converse";
    3.91 +val finite_empty_induct = thm "finite_empty_induct";
    3.92 +val finite_imageD = thm "finite_imageD";
    3.93 +val finite_imageI = thm "finite_imageI";
    3.94 +val finite_imp_cardR = thm "finite_imp_cardR";
    3.95 +val finite_imp_foldSet = thm "finite_imp_foldSet";
    3.96 +val finite_induct = thm "finite_induct";
    3.97 +val finite_insert = thm "finite_insert";
    3.98 +val finite_lessThan = thm "finite_lessThan";
    3.99 +val finite_range_imageI = thm "finite_range_imageI";
   3.100 +val finite_subset = thm "finite_subset";
   3.101 +val finite_subset_induct = thm "finite_subset_induct";
   3.102 +val finite_trancl = thm "finite_trancl";
   3.103 +val foldSet_determ = thm "foldSet_determ";
   3.104 +val foldSet_imp_finite = thm "foldSet_imp_finite";
   3.105 +val fold_Un_Int = thm "fold_Un_Int";
   3.106 +val fold_Un_disjoint = thm "fold_Un_disjoint";
   3.107 +val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
   3.108 +val fold_commute = thm "fold_commute";
   3.109 +val fold_def = thm "fold_def";
   3.110 +val fold_empty = thm "fold_empty";
   3.111 +val fold_equality = thm "fold_equality";
   3.112 +val fold_insert = thm "fold_insert";
   3.113 +val fold_nest_Un_Int = thm "fold_nest_Un_Int";
   3.114 +val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
   3.115 +val n_sub_lemma = thm "n_sub_lemma";
   3.116 +val n_subsets = thm "n_subsets";
   3.117 +val psubset_card_mono = thm "psubset_card_mono";
   3.118 +val setsum_0 = thm "setsum_0";
   3.119 +val setsum_SucD = thm "setsum_SucD";
   3.120 +val setsum_UN_disjoint = thm "setsum_UN_disjoint";
   3.121 +val setsum_Un = thm "setsum_Un";
   3.122 +val setsum_Un_Int = thm "setsum_Un_Int";
   3.123 +val setsum_Un_disjoint = thm "setsum_Un_disjoint";
   3.124 +val setsum_addf = thm "setsum_addf";
   3.125 +val setsum_cong = thm "setsum_cong";
   3.126 +val setsum_def = thm "setsum_def";
   3.127 +val setsum_diff1 = thm "setsum_diff1";
   3.128 +val setsum_empty = thm "setsum_empty";
   3.129 +val setsum_eq_0_iff = thm "setsum_eq_0_iff";
   3.130 +val setsum_insert = thm "setsum_insert";
   3.131 +val trancl_subset_Field2 = thm "trancl_subset_Field2";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 06 00:38:55 2001 +0100
     4.3 @@ -0,0 +1,947 @@
     4.4 +(*  Title:      HOL/Finite_Set.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.8 +*)
     4.9 +
    4.10 +header {* Finite sets *}
    4.11 +
    4.12 +theory Finite_Set = Divides + Power + Inductive + SetInterval:
    4.13 +
    4.14 +subsection {* Collection of finite sets *}
    4.15 +
    4.16 +consts Finites :: "'a set set"
    4.17 +
    4.18 +inductive Finites
    4.19 +  intros
    4.20 +    emptyI [simp, intro!]: "{} : Finites"
    4.21 +    insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    4.22 +
    4.23 +syntax
    4.24 +  finite :: "'a set => bool"
    4.25 +translations
    4.26 +  "finite A" == "A : Finites"
    4.27 +
    4.28 +axclass finite \<subseteq> type
    4.29 +  finite: "finite UNIV"
    4.30 +
    4.31 +
    4.32 +lemma finite_induct [case_names empty insert, induct set: Finites]:
    4.33 +  "finite F ==>
    4.34 +    P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    4.35 +  -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    4.36 +proof -
    4.37 +  assume "P {}" and insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    4.38 +  assume "finite F"
    4.39 +  thus "P F"
    4.40 +  proof induct
    4.41 +    show "P {}" .
    4.42 +    fix F x assume F: "finite F" and P: "P F"
    4.43 +    show "P (insert x F)"
    4.44 +    proof cases
    4.45 +      assume "x \<in> F"
    4.46 +      hence "insert x F = F" by (rule insert_absorb)
    4.47 +      with P show ?thesis by (simp only:)
    4.48 +    next
    4.49 +      assume "x \<notin> F"
    4.50 +      from F this P show ?thesis by (rule insert)
    4.51 +    qed
    4.52 +  qed
    4.53 +qed
    4.54 +
    4.55 +lemma finite_subset_induct [consumes 2, case_names empty insert]:
    4.56 +  "finite F ==> F \<subseteq> A ==>
    4.57 +    P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    4.58 +    P F"
    4.59 +proof -
    4.60 +  assume "P {}" and insert: "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    4.61 +  assume "finite F"
    4.62 +  thus "F \<subseteq> A ==> P F"
    4.63 +  proof induct
    4.64 +    show "P {}" .
    4.65 +    fix F x assume "finite F" and "x \<notin> F"
    4.66 +      and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    4.67 +    show "P (insert x F)"
    4.68 +    proof (rule insert)
    4.69 +      from i show "x \<in> A" by blast
    4.70 +      from i have "F \<subseteq> A" by blast
    4.71 +      with P show "P F" .
    4.72 +    qed
    4.73 +  qed
    4.74 +qed
    4.75 +
    4.76 +lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
    4.77 +  -- {* The union of two finite sets is finite. *}
    4.78 +  by (induct set: Finites) simp_all
    4.79 +
    4.80 +lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
    4.81 +  -- {* Every subset of a finite set is finite. *}
    4.82 +proof -
    4.83 +  assume "finite B"
    4.84 +  thus "!!A. A \<subseteq> B ==> finite A"
    4.85 +  proof induct
    4.86 +    case empty
    4.87 +    thus ?case by simp
    4.88 +  next
    4.89 +    case (insert F x A)
    4.90 +    have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
    4.91 +    show "finite A"
    4.92 +    proof cases
    4.93 +      assume x: "x \<in> A"
    4.94 +      with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
    4.95 +      with r have "finite (A - {x})" .
    4.96 +      hence "finite (insert x (A - {x}))" ..
    4.97 +      also have "insert x (A - {x}) = A" by (rule insert_Diff)
    4.98 +      finally show ?thesis .
    4.99 +    next
   4.100 +      show "A \<subseteq> F ==> ?thesis" .
   4.101 +      assume "x \<notin> A"
   4.102 +      with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   4.103 +    qed
   4.104 +  qed
   4.105 +qed
   4.106 +
   4.107 +lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   4.108 +  by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   4.109 +
   4.110 +lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   4.111 +  -- {* The converse obviously fails. *}
   4.112 +  by (blast intro: finite_subset)
   4.113 +
   4.114 +lemma finite_insert [simp]: "finite (insert a A) = finite A"
   4.115 +  apply (subst insert_is_Un)
   4.116 +  apply (simp only: finite_Un)
   4.117 +  apply blast
   4.118 +  done
   4.119 +
   4.120 +lemma finite_imageI: "finite F ==> finite (h ` F)"
   4.121 +  -- {* The image of a finite set is finite. *}
   4.122 +  by (induct set: Finites) simp_all
   4.123 +
   4.124 +lemma finite_range_imageI:
   4.125 +    "finite (range g) ==> finite (range (%x. f (g x)))"
   4.126 +  apply (drule finite_imageI)
   4.127 +  apply simp
   4.128 +  done
   4.129 +
   4.130 +lemma finite_empty_induct:
   4.131 +  "finite A ==>
   4.132 +  P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   4.133 +proof -
   4.134 +  assume "finite A"
   4.135 +    and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   4.136 +  have "P (A - A)"
   4.137 +  proof -
   4.138 +    fix c b :: "'a set"
   4.139 +    presume c: "finite c" and b: "finite b"
   4.140 +      and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   4.141 +    from c show "c \<subseteq> b ==> P (b - c)"
   4.142 +    proof induct
   4.143 +      case empty
   4.144 +      from P1 show ?case by simp
   4.145 +    next
   4.146 +      case (insert F x)
   4.147 +      have "P (b - F - {x})"
   4.148 +      proof (rule P2)
   4.149 +        from _ b show "finite (b - F)" by (rule finite_subset) blast
   4.150 +        from insert show "x \<in> b - F" by simp
   4.151 +        from insert show "P (b - F)" by simp
   4.152 +      qed
   4.153 +      also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   4.154 +      finally show ?case .
   4.155 +    qed
   4.156 +  next
   4.157 +    show "A \<subseteq> A" ..
   4.158 +  qed
   4.159 +  thus "P {}" by simp
   4.160 +qed
   4.161 +
   4.162 +lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   4.163 +  by (rule Diff_subset [THEN finite_subset])
   4.164 +
   4.165 +lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   4.166 +  apply (subst Diff_insert)
   4.167 +  apply (case_tac "a : A - B")
   4.168 +   apply (rule finite_insert [symmetric, THEN trans])
   4.169 +   apply (subst insert_Diff)
   4.170 +    apply simp_all
   4.171 +  done
   4.172 +
   4.173 +
   4.174 +lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   4.175 +proof -
   4.176 +  have aux: "!!A. finite (A - {}) = finite A" by simp
   4.177 +  fix B :: "'a set"
   4.178 +  assume "finite B"
   4.179 +  thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   4.180 +    apply induct
   4.181 +     apply simp
   4.182 +    apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   4.183 +     apply clarify
   4.184 +     apply (simp (no_asm_use) add: inj_on_def)
   4.185 +     apply (blast dest!: aux [THEN iffD1])
   4.186 +    apply atomize
   4.187 +    apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   4.188 +    apply (frule subsetD [OF equalityD2 insertI1])
   4.189 +    apply clarify
   4.190 +    apply (rule_tac x = xa in bexI)
   4.191 +     apply (simp_all add: inj_on_image_set_diff)
   4.192 +    done
   4.193 +qed (rule refl)
   4.194 +
   4.195 +
   4.196 +subsubsection {* The finite UNION of finite sets *}
   4.197 +
   4.198 +lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   4.199 +  by (induct set: Finites) simp_all
   4.200 +
   4.201 +text {*
   4.202 +  Strengthen RHS to
   4.203 +  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
   4.204 +
   4.205 +  We'd need to prove
   4.206 +  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
   4.207 +  by induction. *}
   4.208 +
   4.209 +lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   4.210 +  by (blast intro: finite_UN_I finite_subset)
   4.211 +
   4.212 +
   4.213 +subsubsection {* Sigma of finite sets *}
   4.214 +
   4.215 +lemma finite_SigmaI [simp]:
   4.216 +    "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   4.217 +  by (unfold Sigma_def) (blast intro!: finite_UN_I)
   4.218 +
   4.219 +lemma finite_Prod_UNIV:
   4.220 +    "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   4.221 +  apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   4.222 +   apply (erule ssubst)
   4.223 +   apply (erule finite_SigmaI)
   4.224 +   apply auto
   4.225 +  done
   4.226 +
   4.227 +instance unit :: finite
   4.228 +proof
   4.229 +  have "finite {()}" by simp
   4.230 +  also have "{()} = UNIV" by auto
   4.231 +  finally show "finite (UNIV :: unit set)" .
   4.232 +qed
   4.233 +
   4.234 +instance * :: (finite, finite) finite
   4.235 +proof
   4.236 +  show "finite (UNIV :: ('a \<times> 'b) set)"
   4.237 +  proof (rule finite_Prod_UNIV)
   4.238 +    show "finite (UNIV :: 'a set)" by (rule finite)
   4.239 +    show "finite (UNIV :: 'b set)" by (rule finite)
   4.240 +  qed
   4.241 +qed
   4.242 +
   4.243 +
   4.244 +subsubsection {* The powerset of a finite set *}
   4.245 +
   4.246 +lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   4.247 +proof
   4.248 +  assume "finite (Pow A)"
   4.249 +  with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   4.250 +  thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   4.251 +next
   4.252 +  assume "finite A"
   4.253 +  thus "finite (Pow A)"
   4.254 +    by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   4.255 +qed
   4.256 +
   4.257 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
   4.258 +  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   4.259 +   apply simp
   4.260 +   apply (rule iffI)
   4.261 +    apply (erule finite_imageD [unfolded inj_on_def])
   4.262 +    apply (simp split add: split_split)
   4.263 +   apply (erule finite_imageI)
   4.264 +  apply (simp add: converse_def image_def)
   4.265 +  apply auto
   4.266 +  apply (rule bexI)
   4.267 +   prefer 2 apply assumption
   4.268 +  apply simp
   4.269 +  done
   4.270 +
   4.271 +lemma finite_lessThan [iff]: (fixes k :: nat) "finite {..k(}"
   4.272 +  by (induct k) (simp_all add: lessThan_Suc)
   4.273 +
   4.274 +lemma finite_atMost [iff]: (fixes k :: nat) "finite {..k}"
   4.275 +  by (induct k) (simp_all add: atMost_Suc)
   4.276 +
   4.277 +lemma bounded_nat_set_is_finite:
   4.278 +    "(ALL i:N. i < (n::nat)) ==> finite N"
   4.279 +  -- {* A bounded set of natural numbers is finite. *}
   4.280 +  apply (rule finite_subset)
   4.281 +   apply (rule_tac [2] finite_lessThan)
   4.282 +  apply auto
   4.283 +  done
   4.284 +
   4.285 +
   4.286 +subsubsection {* Finiteness of transitive closure *}
   4.287 +
   4.288 +text {* (Thanks to Sidi Ehmety) *}
   4.289 +
   4.290 +lemma finite_Field: "finite r ==> finite (Field r)"
   4.291 +  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   4.292 +  apply (induct set: Finites)
   4.293 +   apply (auto simp add: Field_def Domain_insert Range_insert)
   4.294 +  done
   4.295 +
   4.296 +lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   4.297 +  apply clarify
   4.298 +  apply (erule trancl_induct)
   4.299 +   apply (auto simp add: Field_def)
   4.300 +  done
   4.301 +
   4.302 +lemma finite_trancl: "finite (r^+) = finite r"
   4.303 +  apply auto
   4.304 +   prefer 2
   4.305 +   apply (rule trancl_subset_Field2 [THEN finite_subset])
   4.306 +   apply (rule finite_SigmaI)
   4.307 +    prefer 3
   4.308 +    apply (blast intro: r_into_trancl finite_subset)
   4.309 +   apply (auto simp add: finite_Field)
   4.310 +  done
   4.311 +
   4.312 +
   4.313 +subsection {* Finite cardinality *}
   4.314 +
   4.315 +text {*
   4.316 +  This definition, although traditional, is ugly to work with: @{text
   4.317 +  "card A == LEAST n. EX f. A = {f i | i. i < n}"}.  Therefore we have
   4.318 +  switched to an inductive one:
   4.319 +*}
   4.320 +
   4.321 +consts cardR :: "('a set \<times> nat) set"
   4.322 +
   4.323 +inductive cardR
   4.324 +  intros
   4.325 +    EmptyI: "({}, 0) : cardR"
   4.326 +    InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
   4.327 +
   4.328 +constdefs
   4.329 +  card :: "'a set => nat"
   4.330 +  "card A == THE n. (A, n) : cardR"
   4.331 +
   4.332 +inductive_cases cardR_emptyE: "({}, n) : cardR"
   4.333 +inductive_cases cardR_insertE: "(insert a A,n) : cardR"
   4.334 +
   4.335 +lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
   4.336 +  by (induct set: cardR) simp_all
   4.337 +
   4.338 +lemma cardR_determ_aux1:
   4.339 +    "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
   4.340 +  apply (induct set: cardR)
   4.341 +   apply auto
   4.342 +  apply (simp add: insert_Diff_if)
   4.343 +  apply auto
   4.344 +  apply (drule cardR_SucD)
   4.345 +  apply (blast intro!: cardR.intros)
   4.346 +  done
   4.347 +
   4.348 +lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
   4.349 +  by (drule cardR_determ_aux1) auto
   4.350 +
   4.351 +lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
   4.352 +  apply (induct set: cardR)
   4.353 +   apply (safe elim!: cardR_emptyE cardR_insertE)
   4.354 +  apply (rename_tac B b m)
   4.355 +  apply (case_tac "a = b")
   4.356 +   apply (subgoal_tac "A = B")
   4.357 +    prefer 2 apply (blast elim: equalityE)
   4.358 +   apply blast
   4.359 +  apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
   4.360 +   prefer 2
   4.361 +   apply (rule_tac x = "A Int B" in exI)
   4.362 +   apply (blast elim: equalityE)
   4.363 +  apply (frule_tac A = B in cardR_SucD)
   4.364 +  apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
   4.365 +  done
   4.366 +
   4.367 +lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
   4.368 +  by (induct set: cardR) simp_all
   4.369 +
   4.370 +lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
   4.371 +  by (induct set: Finites) (auto intro!: cardR.intros)
   4.372 +
   4.373 +lemma card_equality: "(A,n) : cardR ==> card A = n"
   4.374 +  by (unfold card_def) (blast intro: cardR_determ)
   4.375 +
   4.376 +lemma card_empty [simp]: "card {} = 0"
   4.377 +  by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
   4.378 +
   4.379 +lemma card_insert_disjoint [simp]:
   4.380 +  "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
   4.381 +proof -
   4.382 +  assume x: "x \<notin> A"
   4.383 +  hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
   4.384 +    apply (auto intro!: cardR.intros)
   4.385 +    apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
   4.386 +     apply (force dest: cardR_imp_finite)
   4.387 +    apply (blast intro!: cardR.intros intro: cardR_determ)
   4.388 +    done
   4.389 +  assume "finite A"
   4.390 +  thus ?thesis
   4.391 +    apply (simp add: card_def aux)
   4.392 +    apply (rule the_equality)
   4.393 +     apply (auto intro: finite_imp_cardR
   4.394 +       cong: conj_cong simp: card_def [symmetric] card_equality)
   4.395 +    done
   4.396 +qed
   4.397 +
   4.398 +lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
   4.399 +  apply auto
   4.400 +  apply (drule_tac a = x in mk_disjoint_insert)
   4.401 +  apply clarify
   4.402 +  apply (rotate_tac -1)
   4.403 +  apply auto
   4.404 +  done
   4.405 +
   4.406 +lemma card_insert_if:
   4.407 +    "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
   4.408 +  by (simp add: insert_absorb)
   4.409 +
   4.410 +lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
   4.411 +  apply (rule_tac t = A in insert_Diff [THEN subst])
   4.412 +   apply assumption
   4.413 +  apply simp
   4.414 +  done
   4.415 +
   4.416 +lemma card_Diff_singleton:
   4.417 +    "finite A ==> x: A ==> card (A - {x}) = card A - 1"
   4.418 +  by (simp add: card_Suc_Diff1 [symmetric])
   4.419 +
   4.420 +lemma card_Diff_singleton_if:
   4.421 +    "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
   4.422 +  by (simp add: card_Diff_singleton)
   4.423 +
   4.424 +lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
   4.425 +  by (simp add: card_insert_if card_Suc_Diff1)
   4.426 +
   4.427 +lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
   4.428 +  by (simp add: card_insert_if)
   4.429 +
   4.430 +lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   4.431 +  apply (induct set: Finites)
   4.432 +   apply simp
   4.433 +  apply clarify
   4.434 +  apply (subgoal_tac "finite A & A - {x} <= F")
   4.435 +   prefer 2 apply (blast intro: finite_subset)
   4.436 +  apply atomize
   4.437 +  apply (drule_tac x = "A - {x}" in spec)
   4.438 +  apply (simp add: card_Diff_singleton_if split add: split_if_asm)
   4.439 +  apply (case_tac "card A")
   4.440 +   apply auto
   4.441 +  done
   4.442 +
   4.443 +lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
   4.444 +  apply (simp add: psubset_def linorder_not_le [symmetric])
   4.445 +  apply (blast dest: card_seteq)
   4.446 +  done
   4.447 +
   4.448 +lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
   4.449 +  apply (case_tac "A = B")
   4.450 +   apply simp
   4.451 +  apply (simp add: linorder_not_less [symmetric])
   4.452 +  apply (blast dest: card_seteq intro: order_less_imp_le)
   4.453 +  done
   4.454 +
   4.455 +lemma card_Un_Int: "finite A ==> finite B
   4.456 +    ==> card A + card B = card (A Un B) + card (A Int B)"
   4.457 +  apply (induct set: Finites)
   4.458 +   apply simp
   4.459 +  apply (simp add: insert_absorb Int_insert_left)
   4.460 +  done
   4.461 +
   4.462 +lemma card_Un_disjoint: "finite A ==> finite B
   4.463 +    ==> A Int B = {} ==> card (A Un B) = card A + card B"
   4.464 +  by (simp add: card_Un_Int)
   4.465 +
   4.466 +lemma card_Diff_subset:
   4.467 +    "finite A ==> B <= A ==> card A - card B = card (A - B)"
   4.468 +  apply (subgoal_tac "(A - B) Un B = A")
   4.469 +   prefer 2 apply blast
   4.470 +  apply (rule add_right_cancel [THEN iffD1])
   4.471 +  apply (rule card_Un_disjoint [THEN subst])
   4.472 +     apply (erule_tac [4] ssubst)
   4.473 +     prefer 3 apply blast
   4.474 +    apply (simp_all add: add_commute not_less_iff_le
   4.475 +      add_diff_inverse card_mono finite_subset)
   4.476 +  done
   4.477 +
   4.478 +lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
   4.479 +  apply (rule Suc_less_SucD)
   4.480 +  apply (simp add: card_Suc_Diff1)
   4.481 +  done
   4.482 +
   4.483 +lemma card_Diff2_less:
   4.484 +    "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
   4.485 +  apply (case_tac "x = y")
   4.486 +   apply (simp add: card_Diff1_less)
   4.487 +  apply (rule less_trans)
   4.488 +   prefer 2 apply (auto intro!: card_Diff1_less)
   4.489 +  done
   4.490 +
   4.491 +lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
   4.492 +  apply (case_tac "x : A")
   4.493 +   apply (simp_all add: card_Diff1_less less_imp_le)
   4.494 +  done
   4.495 +
   4.496 +lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
   4.497 +  apply (erule psubsetI)
   4.498 +  apply blast
   4.499 +  done
   4.500 +
   4.501 +
   4.502 +subsubsection {* Cardinality of image *}
   4.503 +
   4.504 +lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   4.505 +  apply (induct set: Finites)
   4.506 +   apply simp
   4.507 +  apply (simp add: le_SucI finite_imageI card_insert_if)
   4.508 +  done
   4.509 +
   4.510 +lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   4.511 +  apply (induct set: Finites)
   4.512 +   apply simp_all
   4.513 +  apply atomize
   4.514 +  apply safe
   4.515 +   apply (unfold inj_on_def)
   4.516 +   apply blast
   4.517 +  apply (subst card_insert_disjoint)
   4.518 +    apply (erule finite_imageI)
   4.519 +   apply blast
   4.520 +  apply blast
   4.521 +  done
   4.522 +
   4.523 +lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   4.524 +  by (simp add: card_seteq card_image)
   4.525 +
   4.526 +
   4.527 +subsubsection {* Cardinality of the Powerset *}
   4.528 +
   4.529 +lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   4.530 +  apply (induct set: Finites)
   4.531 +   apply (simp_all add: Pow_insert)
   4.532 +  apply (subst card_Un_disjoint)
   4.533 +     apply blast
   4.534 +    apply (blast intro: finite_imageI)
   4.535 +   apply blast
   4.536 +  apply (subgoal_tac "inj_on (insert x) (Pow F)")
   4.537 +   apply (simp add: card_image Pow_insert)
   4.538 +  apply (unfold inj_on_def)
   4.539 +  apply (blast elim!: equalityE)
   4.540 +  done
   4.541 +
   4.542 +text {*
   4.543 +  \medskip Relates to equivalence classes.  Based on a theorem of
   4.544 +  F. Kammüller's.  The @{prop "finite C"} premise is redundant.
   4.545 +*}
   4.546 +
   4.547 +lemma dvd_partition:
   4.548 +  "finite C ==> finite (Union C) ==>
   4.549 +    ALL c : C. k dvd card c ==>
   4.550 +    (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
   4.551 +  k dvd card (Union C)"
   4.552 +  apply (induct set: Finites)
   4.553 +   apply simp_all
   4.554 +  apply clarify
   4.555 +  apply (subst card_Un_disjoint)
   4.556 +  apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   4.557 +  done
   4.558 +
   4.559 +
   4.560 +subsection {* A fold functional for finite sets *}
   4.561 +
   4.562 +text {*
   4.563 +  For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
   4.564 +  f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
   4.565 +*}
   4.566 +
   4.567 +consts
   4.568 +  foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
   4.569 +
   4.570 +inductive "foldSet f e"
   4.571 +  intros
   4.572 +    emptyI [intro]: "({}, e) : foldSet f e"
   4.573 +    insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
   4.574 +
   4.575 +inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
   4.576 +
   4.577 +constdefs
   4.578 +  fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
   4.579 +  "fold f e A == THE x. (A, x) : foldSet f e"
   4.580 +
   4.581 +lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
   4.582 +  apply (erule insert_Diff [THEN subst], rule foldSet.intros)
   4.583 +   apply auto
   4.584 +  done
   4.585 +
   4.586 +lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
   4.587 +  by (induct set: foldSet) auto
   4.588 +
   4.589 +lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
   4.590 +  by (induct set: Finites) auto
   4.591 +
   4.592 +
   4.593 +subsubsection {* Left-commutative operations *}
   4.594 +
   4.595 +locale LC =
   4.596 +  fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
   4.597 +  assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   4.598 +
   4.599 +lemma (in LC) foldSet_determ_aux:
   4.600 +  "ALL A x. card A < n --> (A, x) : foldSet f e -->
   4.601 +    (ALL y. (A, y) : foldSet f e --> y = x)"
   4.602 +  apply (induct n)
   4.603 +   apply (auto simp add: less_Suc_eq)
   4.604 +  apply (erule foldSet.cases)
   4.605 +   apply blast
   4.606 +  apply (erule foldSet.cases)
   4.607 +   apply blast
   4.608 +  apply clarify
   4.609 +  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   4.610 +  apply (erule rev_mp)
   4.611 +  apply (simp add: less_Suc_eq_le)
   4.612 +  apply (rule impI)
   4.613 +  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   4.614 +   apply (subgoal_tac "Aa = Ab")
   4.615 +    prefer 2 apply (blast elim!: equalityE)
   4.616 +   apply blast
   4.617 +  txt {* case @{prop "xa \<notin> xb"}. *}
   4.618 +  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   4.619 +   prefer 2 apply (blast elim!: equalityE)
   4.620 +  apply clarify
   4.621 +  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   4.622 +   prefer 2 apply blast
   4.623 +  apply (subgoal_tac "card Aa <= card Ab")
   4.624 +   prefer 2
   4.625 +   apply (rule Suc_le_mono [THEN subst])
   4.626 +   apply (simp add: card_Suc_Diff1)
   4.627 +  apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
   4.628 +  apply (blast intro: foldSet_imp_finite finite_Diff)
   4.629 +  apply (frule (1) Diff1_foldSet)
   4.630 +  apply (subgoal_tac "ya = f xb x")
   4.631 +   prefer 2 apply (blast del: equalityCE)
   4.632 +  apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
   4.633 +   prefer 2 apply simp
   4.634 +  apply (subgoal_tac "yb = f xa x")
   4.635 +   prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
   4.636 +  apply (simp (no_asm_simp) add: left_commute)
   4.637 +  done
   4.638 +
   4.639 +lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
   4.640 +  by (blast intro: foldSet_determ_aux [rule_format])
   4.641 +
   4.642 +lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
   4.643 +  by (unfold fold_def) (blast intro: foldSet_determ)
   4.644 +
   4.645 +lemma fold_empty [simp]: "fold f e {} = e"
   4.646 +  by (unfold fold_def) blast
   4.647 +
   4.648 +lemma (in LC) fold_insert_aux: "x \<notin> A ==>
   4.649 +    ((insert x A, v) : foldSet f e) =
   4.650 +    (EX y. (A, y) : foldSet f e & v = f x y)"
   4.651 +  apply auto
   4.652 +  apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   4.653 +   apply (fastsimp dest: foldSet_imp_finite)
   4.654 +  apply (blast intro: foldSet_determ)
   4.655 +  done
   4.656 +
   4.657 +lemma (in LC) fold_insert:
   4.658 +    "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
   4.659 +  apply (unfold fold_def)
   4.660 +  apply (simp add: fold_insert_aux)
   4.661 +  apply (rule the_equality)
   4.662 +  apply (auto intro: finite_imp_foldSet
   4.663 +    cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   4.664 +  done
   4.665 +
   4.666 +lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
   4.667 +  apply (induct set: Finites)
   4.668 +   apply simp
   4.669 +  apply (simp add: left_commute fold_insert)
   4.670 +  done
   4.671 +
   4.672 +lemma (in LC) fold_nest_Un_Int:
   4.673 +  "finite A ==> finite B
   4.674 +    ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
   4.675 +  apply (induct set: Finites)
   4.676 +   apply simp
   4.677 +  apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
   4.678 +  done
   4.679 +
   4.680 +lemma (in LC) fold_nest_Un_disjoint:
   4.681 +  "finite A ==> finite B ==> A Int B = {}
   4.682 +    ==> fold f e (A Un B) = fold f (fold f e B) A"
   4.683 +  by (simp add: fold_nest_Un_Int)
   4.684 +
   4.685 +declare foldSet_imp_finite [simp del]
   4.686 +    empty_foldSetE [rule del]  foldSet.intros [rule del]
   4.687 +  -- {* Delete rules to do with @{text foldSet} relation. *}
   4.688 +
   4.689 +
   4.690 +
   4.691 +subsubsection {* Commutative monoids *}
   4.692 +
   4.693 +text {*
   4.694 +  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   4.695 +  instead of @{text "'b => 'a => 'a"}.
   4.696 +*}
   4.697 +
   4.698 +locale ACe =
   4.699 +  fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   4.700 +    and e :: 'a
   4.701 +  assumes ident [simp]: "x \<cdot> e = x"
   4.702 +    and commute: "x \<cdot> y = y \<cdot> x"
   4.703 +    and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   4.704 +
   4.705 +lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   4.706 +proof -
   4.707 +  have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   4.708 +  also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   4.709 +  also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   4.710 +  finally show ?thesis .
   4.711 +qed
   4.712 +
   4.713 +lemma (in ACe)
   4.714 +    AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   4.715 +  by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)
   4.716 +
   4.717 +lemma (in ACe [simp]) left_ident: "e \<cdot> x = x"
   4.718 +proof -
   4.719 +  have "x \<cdot> e = x" by (rule ident)
   4.720 +  thus ?thesis by (subst commute)
   4.721 +qed
   4.722 +
   4.723 +lemma (in ACe) fold_Un_Int:
   4.724 +  "finite A ==> finite B ==>
   4.725 +    fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   4.726 +  apply (induct set: Finites)
   4.727 +   apply simp
   4.728 +  apply (simp add: AC fold_insert insert_absorb Int_insert_left)
   4.729 +  done
   4.730 +
   4.731 +lemma (in ACe) fold_Un_disjoint:
   4.732 +  "finite A ==> finite B ==> A Int B = {} ==>
   4.733 +    fold f e (A Un B) = fold f e A \<cdot> fold f e B"
   4.734 +  by (simp add: fold_Un_Int)
   4.735 +
   4.736 +lemma (in ACe) fold_Un_disjoint2:
   4.737 +  "finite A ==> finite B ==> A Int B = {} ==>
   4.738 +    fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   4.739 +proof -
   4.740 +  assume b: "finite B"
   4.741 +  assume "finite A"
   4.742 +  thus "A Int B = {} ==>
   4.743 +    fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
   4.744 +  proof induct
   4.745 +    case empty
   4.746 +    thus ?case by simp
   4.747 +  next
   4.748 +    case (insert F x)
   4.749 +    have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
   4.750 +      by simp
   4.751 +    also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
   4.752 +      by (rule fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
   4.753 +    also from insert have "fold (f \<circ> g) e (F \<union> B) =
   4.754 +      fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
   4.755 +    also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
   4.756 +      by (simp add: AC)
   4.757 +    also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
   4.758 +      by (rule fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
   4.759 +    finally show ?case .
   4.760 +  qed
   4.761 +qed
   4.762 +
   4.763 +
   4.764 +subsection {* Generalized summation over a set *}
   4.765 +
   4.766 +constdefs
   4.767 +  setsum :: "('a => 'b) => 'a set => 'b::plus_ac0"
   4.768 +  "setsum f A == if finite A then fold (op + o f) 0 A else 0"
   4.769 +
   4.770 +syntax
   4.771 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
   4.772 +syntax (xsymbols)
   4.773 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
   4.774 +translations
   4.775 +  "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
   4.776 +
   4.777 +
   4.778 +lemma setsum_empty [simp]: "setsum f {} = 0"
   4.779 +  by (simp add: setsum_def)
   4.780 +
   4.781 +lemma setsum_insert [simp]:
   4.782 +    "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   4.783 +  by (simp add: setsum_def fold_insert plus_ac0_left_commute)
   4.784 +
   4.785 +lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   4.786 +  apply (case_tac "finite A")
   4.787 +   prefer 2 apply (simp add: setsum_def)
   4.788 +  apply (erule finite_induct)
   4.789 +   apply auto
   4.790 +  done
   4.791 +
   4.792 +lemma setsum_eq_0_iff [simp]:
   4.793 +    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   4.794 +  by (induct set: Finites) auto
   4.795 +
   4.796 +lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   4.797 +  apply (case_tac "finite A")
   4.798 +   prefer 2 apply (simp add: setsum_def)
   4.799 +  apply (erule rev_mp)
   4.800 +  apply (erule finite_induct)
   4.801 +   apply auto
   4.802 +  done
   4.803 +
   4.804 +lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
   4.805 +  -- {* Could allow many @{text "card"} proofs to be simplified. *}
   4.806 +  by (induct set: Finites) auto
   4.807 +
   4.808 +lemma setsum_Un_Int: "finite A ==> finite B
   4.809 +    ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   4.810 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   4.811 +  apply (induct set: Finites)
   4.812 +   apply simp
   4.813 +  apply (simp add: plus_ac0 Int_insert_left insert_absorb)
   4.814 +  done
   4.815 +
   4.816 +lemma setsum_Un_disjoint: "finite A ==> finite B
   4.817 +  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   4.818 +  apply (subst setsum_Un_Int [symmetric])
   4.819 +    apply auto
   4.820 +  done
   4.821 +
   4.822 +lemma setsum_UN_disjoint: (fixes f :: "'a => 'b::plus_ac0")
   4.823 +  "finite I ==> (ALL i:I. finite (A i)) ==>
   4.824 +      (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   4.825 +    setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
   4.826 +  apply (induct set: Finites)
   4.827 +   apply simp
   4.828 +  apply atomize
   4.829 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   4.830 +   prefer 2 apply blast
   4.831 +  apply (subgoal_tac "A x Int UNION F A = {}")
   4.832 +   prefer 2 apply blast
   4.833 +  apply (simp add: setsum_Un_disjoint)
   4.834 +  done
   4.835 +
   4.836 +lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   4.837 +  apply (case_tac "finite A")
   4.838 +   prefer 2 apply (simp add: setsum_def)
   4.839 +  apply (erule finite_induct)
   4.840 +   apply auto
   4.841 +  apply (simp add: plus_ac0)
   4.842 +  done
   4.843 +
   4.844 +lemma setsum_Un: "finite A ==> finite B ==>
   4.845 +    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   4.846 +  -- {* For the natural numbers, we have subtraction. *}
   4.847 +  apply (subst setsum_Un_Int [symmetric])
   4.848 +    apply auto
   4.849 +  done
   4.850 +
   4.851 +lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   4.852 +    (if a:A then setsum f A - f a else setsum f A)"
   4.853 +  apply (case_tac "finite A")
   4.854 +   prefer 2 apply (simp add: setsum_def)
   4.855 +  apply (erule finite_induct)
   4.856 +   apply (auto simp add: insert_Diff_if)
   4.857 +  apply (drule_tac a = a in mk_disjoint_insert)
   4.858 +  apply auto
   4.859 +  done
   4.860 +
   4.861 +lemma setsum_cong:
   4.862 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   4.863 +  apply (case_tac "finite B")
   4.864 +   prefer 2 apply (simp add: setsum_def)
   4.865 +  apply simp
   4.866 +  apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
   4.867 +   apply simp
   4.868 +  apply (erule finite_induct)
   4.869 +  apply simp
   4.870 +  apply (simp add: subset_insert_iff)
   4.871 +  apply clarify
   4.872 +  apply (subgoal_tac "finite C")
   4.873 +   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   4.874 +  apply (subgoal_tac "C = insert x (C - {x})")
   4.875 +   prefer 2 apply blast
   4.876 +  apply (erule ssubst)
   4.877 +  apply (drule spec)
   4.878 +  apply (erule (1) notE impE)
   4.879 +  apply (simp add: Ball_def)
   4.880 +  done
   4.881 +
   4.882 +
   4.883 +text {*
   4.884 +  \medskip Basic theorem about @{text "choose"}.  By Florian
   4.885 +  Kammüller, tidied by LCP.
   4.886 +*}
   4.887 +
   4.888 +lemma card_s_0_eq_empty:
   4.889 +    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
   4.890 +  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   4.891 +  apply (simp cong add: rev_conj_cong)
   4.892 +  done
   4.893 +
   4.894 +lemma choose_deconstruct: "finite M ==> x \<notin> M
   4.895 +  ==> {s. s <= insert x M & card(s) = Suc k}
   4.896 +       = {s. s <= M & card(s) = Suc k} Un
   4.897 +         {s. EX t. t <= M & card(t) = k & s = insert x t}"
   4.898 +  apply safe
   4.899 +   apply (auto intro: finite_subset [THEN card_insert_disjoint])
   4.900 +  apply (drule_tac x = "xa - {x}" in spec)
   4.901 +  apply (subgoal_tac "x ~: xa")
   4.902 +   apply auto
   4.903 +  apply (erule rev_mp, subst card_Diff_singleton)
   4.904 +  apply (auto intro: finite_subset)
   4.905 +  done
   4.906 +
   4.907 +lemma card_inj_on_le:
   4.908 +    "finite A ==> finite B ==> f ` A \<subseteq> B ==> inj_on f A ==> card A <= card B"
   4.909 +  by (auto intro: card_mono simp add: card_image [symmetric])
   4.910 +
   4.911 +lemma card_bij_eq: "finite A ==> finite B ==>
   4.912 +  f ` A \<subseteq> B ==> inj_on f A ==> g ` B \<subseteq> A ==> inj_on g B ==> card A = card B"
   4.913 +  by (auto intro: le_anti_sym card_inj_on_le)
   4.914 +
   4.915 +lemma constr_bij: "finite A ==> x \<notin> A ==>
   4.916 +  card {B. EX C. C <= A & card(C) = k & B = insert x C} =
   4.917 +    card {B. B <= A & card(B) = k}"
   4.918 +  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
   4.919 +       apply (rule_tac B = "Pow (insert x A) " in finite_subset)
   4.920 +        apply (rule_tac [3] B = "Pow (A) " in finite_subset)
   4.921 +         apply fast+
   4.922 +     txt {* arity *}
   4.923 +     apply (auto elim!: equalityE simp add: inj_on_def)
   4.924 +  apply (subst Diff_insert0)
   4.925 +  apply auto
   4.926 +  done
   4.927 +
   4.928 +text {*
   4.929 +  Main theorem: combinatorial statement about number of subsets of a set.
   4.930 +*}
   4.931 +
   4.932 +lemma n_sub_lemma:
   4.933 +  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   4.934 +  apply (induct k)
   4.935 +   apply (simp add: card_s_0_eq_empty)
   4.936 +  apply atomize
   4.937 +  apply (rotate_tac -1, erule finite_induct)
   4.938 +   apply (simp_all (no_asm_simp) cong add: conj_cong add: card_s_0_eq_empty choose_deconstruct)
   4.939 +  apply (subst card_Un_disjoint)
   4.940 +     prefer 4 apply (force simp add: constr_bij)
   4.941 +    prefer 3 apply force
   4.942 +   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
   4.943 +     finite_subset [of _ "Pow (insert x F)", standard])
   4.944 +  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   4.945 +  done
   4.946 +
   4.947 +theorem n_subsets: "finite A ==> card {B. B <= A & card(B) = k} = (card A choose k)"
   4.948 +  by (simp add: n_sub_lemma)
   4.949 +
   4.950 +end
     5.1 --- a/src/HOL/IsaMakefile	Thu Dec 06 00:37:59 2001 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Thu Dec 06 00:38:55 2001 +0100
     5.3 @@ -78,7 +78,7 @@
     5.4    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
     5.5    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     5.6    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
     5.7 -  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
     5.8 +  Divides.thy Finite_Set.ML Finite_Set.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
     5.9    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
    5.10    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    5.11    Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \