author  paulson 
Wed, 23 Sep 1998 10:12:01 +0200  
changeset 5537  c2bd39a2c0ee 
parent 5516  d80e9aeb4a2b 
child 5616  497eeeace3fc 
permissions  rwrr 
1465  1 
(* Title: HOL/Finite.thy 
923  2 
ID: $Id$ 
1531  3 
Author: Lawrence C Paulson & Tobias Nipkow 
4 
Copyright 1995 University of Cambridge & TU Muenchen 

923  5 

1531  6 
Finite sets and their cardinality 
923  7 
*) 
8 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

9 
section "finite"; 
1531  10 

923  11 
(*Discharging ~ x:y entails extra work*) 
5316  12 
val major::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

13 
"[ finite F; P({}); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

14 
\ !!F x. [ finite F; x ~: F; P(F) ] ==> P(insert x F) \ 
923  15 
\ ] ==> P(F)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

16 
by (rtac (major RS Finites.induct) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

17 
by (excluded_middle_tac "a:A" 2); 
923  18 
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) 
19 
by (REPEAT (ares_tac prems 1)); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

20 
qed "finite_induct"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

21 

5316  22 
val major::subs::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

23 
"[ finite F; F <= A; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

24 
\ P({}); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

25 
\ !!F a. [ finite F; a:A; a ~: F; P(F) ] ==> P(insert a F) \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

26 
\ ] ==> P(F)"; 
4386  27 
by (rtac (subs RS rev_mp) 1); 
28 
by (rtac (major RS finite_induct) 1); 

29 
by (ALLGOALS (blast_tac (claset() addIs prems))); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

30 
qed "finite_subset_induct"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

31 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

32 
Addsimps Finites.intrs; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

33 
AddSIs Finites.intrs; 
923  34 

35 
(*The union of two finite sets is finite*) 

5316  36 
Goal "[ finite F; finite G ] ==> finite(F Un G)"; 
37 
by (etac finite_induct 1); 

38 
by (ALLGOALS Asm_simp_tac); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

39 
qed "finite_UnI"; 
923  40 

41 
(*Every subset of a finite set is finite*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

42 
Goal "finite B ==> ALL A. A<=B > finite A"; 
4304  43 
by (etac finite_induct 1); 
44 
by (Simp_tac 1); 

4089  45 
by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1])); 
4304  46 
by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2); 
1264  47 
by (ALLGOALS Asm_simp_tac); 
4304  48 
val lemma = result(); 
49 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

50 
Goal "[ A<=B; finite B ] ==> finite A"; 
4423  51 
by (dtac lemma 1); 
4304  52 
by (Blast_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

53 
qed "finite_subset"; 
923  54 

5069  55 
Goal "finite(F Un G) = (finite F & finite G)"; 
4304  56 
by (blast_tac (claset() 
5413  57 
addIs [read_instantiate [("B", "?X Un ?Y")] finite_subset, 
4304  58 
finite_UnI]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

59 
qed "finite_Un"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

60 
AddIffs[finite_Un]; 
1531  61 

5413  62 
Goal "finite F ==> finite(F Int G)"; 
63 
by (blast_tac (claset() addIs [finite_subset]) 1); 

64 
qed "finite_Int1"; 

65 

66 
Goal "finite G ==> finite(F Int G)"; 

67 
by (blast_tac (claset() addIs [finite_subset]) 1); 

68 
qed "finite_Int2"; 

69 

70 
Addsimps[finite_Int1, finite_Int2]; 

71 
AddIs[finite_Int1, finite_Int2]; 

72 

73 

5069  74 
Goal "finite(insert a A) = finite A"; 
1553  75 
by (stac insert_is_Un 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

76 
by (simp_tac (HOL_ss addsimps [finite_Un]) 1); 
3427
e7cef2081106
Removed a few redundant additions of simprules or classical rules
paulson
parents:
3416
diff
changeset

77 
by (Blast_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

78 
qed "finite_insert"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

79 
Addsimps[finite_insert]; 
1531  80 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

81 
(*The image of a finite set is finite *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

82 
Goal "finite F ==> finite(h``F)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

83 
by (etac finite_induct 1); 
1264  84 
by (Simp_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

85 
by (Asm_simp_tac 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

86 
qed "finite_imageI"; 
923  87 

5316  88 
val major::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

89 
"[ finite c; finite b; \ 
1465  90 
\ P(b); \ 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

91 
\ !!x y. [ finite y; x:y; P(y) ] ==> P(y{x}) \ 
923  92 
\ ] ==> c<=b > P(bc)"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

93 
by (rtac (major RS finite_induct) 1); 
2031  94 
by (stac Diff_insert 2); 
923  95 
by (ALLGOALS (asm_simp_tac 
5537  96 
(simpset() addsimps prems@[Diff_subset RS finite_subset]))); 
1531  97 
val lemma = result(); 
923  98 

5316  99 
val prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

100 
"[ finite A; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

101 
\ P(A); \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

102 
\ !!a A. [ finite A; a:A; P(A) ] ==> P(A{a}) \ 
923  103 
\ ] ==> P({})"; 
104 
by (rtac (Diff_cancel RS subst) 1); 

1531  105 
by (rtac (lemma RS mp) 1); 
923  106 
by (REPEAT (ares_tac (subset_refl::prems) 1)); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

107 
qed "finite_empty_induct"; 
1531  108 

109 

1618  110 
(* finite B ==> finite (B  Ba) *) 
111 
bind_thm ("finite_Diff", Diff_subset RS finite_subset); 

1531  112 
Addsimps [finite_Diff]; 
113 

5069  114 
Goal "finite(A{a}) = finite(A)"; 
3368  115 
by (case_tac "a:A" 1); 
3457  116 
by (rtac (finite_insert RS sym RS trans) 1); 
3368  117 
by (stac insert_Diff 1); 
118 
by (ALLGOALS Asm_simp_tac); 

119 
qed "finite_Diff_singleton"; 

120 
AddIffs [finite_Diff_singleton]; 

121 

4059  122 
(*Lemma for proving finite_imageD*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

123 
Goal "finite B ==> !A. f``A = B > inj_on f A > finite A"; 
1553  124 
by (etac finite_induct 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

125 
by (ALLGOALS Asm_simp_tac); 
3708  126 
by (Clarify_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

127 
by (subgoal_tac "EX y:A. f y = x & F = f``(A{y})" 1); 
3708  128 
by (Clarify_tac 1); 
4830  129 
by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

130 
by (Blast_tac 1); 
3368  131 
by (thin_tac "ALL A. ?PP(A)" 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

132 
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); 
3708  133 
by (Clarify_tac 1); 
3368  134 
by (res_inst_tac [("x","xa")] bexI 1); 
4059  135 
by (ALLGOALS 
4830  136 
(asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff]))); 
3368  137 
val lemma = result(); 
138 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

139 
Goal "[ finite(f``A); inj_on f A ] ==> finite A"; 
3457  140 
by (dtac lemma 1); 
3368  141 
by (Blast_tac 1); 
142 
qed "finite_imageD"; 

143 

4014  144 
(** The finite UNION of finite sets **) 
145 

5316  146 
Goal "finite A ==> (!a:A. finite(B a)) > finite(UN a:A. B a)"; 
147 
by (etac finite_induct 1); 

4153  148 
by (ALLGOALS Asm_simp_tac); 
4014  149 
bind_thm("finite_UnionI", ballI RSN (2, result() RS mp)); 
150 
Addsimps [finite_UnionI]; 

151 

152 
(** Sigma of finite sets **) 

153 

5069  154 
Goalw [Sigma_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

155 
"[ finite A; !a:A. finite(B a) ] ==> finite(SIGMA a:A. B a)"; 
4153  156 
by (blast_tac (claset() addSIs [finite_UnionI]) 1); 
4014  157 
bind_thm("finite_SigmaI", ballI RSN (2,result())); 
158 
Addsimps [finite_SigmaI]; 

3368  159 

160 
(** The powerset of a finite set **) 

161 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

162 
Goal "finite(Pow A) ==> finite A"; 
3368  163 
by (subgoal_tac "finite ((%x.{x})``A)" 1); 
3457  164 
by (rtac finite_subset 2); 
165 
by (assume_tac 3); 

3368  166 
by (ALLGOALS 
4830  167 
(fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD]))); 
3368  168 
val lemma = result(); 
169 

5069  170 
Goal "finite(Pow A) = finite A"; 
3457  171 
by (rtac iffI 1); 
172 
by (etac lemma 1); 

3368  173 
(*Opposite inclusion: finite A ==> finite (Pow A) *) 
3340  174 
by (etac finite_induct 1); 
175 
by (ALLGOALS 

176 
(asm_simp_tac 

4089  177 
(simpset() addsimps [finite_UnI, finite_imageI, Pow_insert]))); 
3368  178 
qed "finite_Pow_iff"; 
179 
AddIffs [finite_Pow_iff]; 

3340  180 

5069  181 
Goal "finite(r^1) = finite r"; 
3457  182 
by (subgoal_tac "r^1 = (%(x,y).(y,x))``r" 1); 
183 
by (Asm_simp_tac 1); 

184 
by (rtac iffI 1); 

4830  185 
by (etac (rewrite_rule [inj_on_def] finite_imageD) 1); 
186 
by (simp_tac (simpset() addsplits [split_split]) 1); 

3457  187 
by (etac finite_imageI 1); 
4746  188 
by (simp_tac (simpset() addsimps [converse_def,image_def]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

189 
by Auto_tac; 
5516  190 
by (rtac bexI 1); 
191 
by (assume_tac 2); 

4763  192 
by (Simp_tac 1); 
4746  193 
qed "finite_converse"; 
194 
AddIffs [finite_converse]; 

1531  195 

1548  196 
section "Finite cardinality  'card'"; 
1531  197 

5316  198 
Goal "{f i i. (P i  i=n)} = insert (f n) {f ii. P i}"; 
2922  199 
by (Blast_tac 1); 
1531  200 
val Collect_conv_insert = result(); 
201 

5069  202 
Goalw [card_def] "card {} = 0"; 
1553  203 
by (rtac Least_equality 1); 
204 
by (ALLGOALS Asm_full_simp_tac); 

1531  205 
qed "card_empty"; 
206 
Addsimps [card_empty]; 

207 

5316  208 
Goal "finite A ==> ? (n::nat) f. A = {f i i. i<n}"; 
209 
by (etac finite_induct 1); 

1553  210 
by (res_inst_tac [("x","0")] exI 1); 
211 
by (Simp_tac 1); 

212 
by (etac exE 1); 

213 
by (etac exE 1); 

214 
by (hyp_subst_tac 1); 

215 
by (res_inst_tac [("x","Suc n")] exI 1); 

216 
by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1); 

4089  217 
by (asm_simp_tac (simpset() addsimps [Collect_conv_insert, less_Suc_eq] 
1548  218 
addcongs [rev_conj_cong]) 1); 
1531  219 
qed "finite_has_card"; 
220 

5278  221 
Goal "[ x ~: A; insert x A = {f ii. i<n} ] \ 
222 
\ ==> ? m::nat. m<n & (? g. A = {g ii. i<m})"; 

5183  223 
by (exhaust_tac "n" 1); 
1553  224 
by (hyp_subst_tac 1); 
225 
by (Asm_full_simp_tac 1); 

226 
by (rename_tac "m" 1); 

227 
by (hyp_subst_tac 1); 

228 
by (case_tac "? a. a:A" 1); 

229 
by (res_inst_tac [("x","0")] exI 2); 

230 
by (Simp_tac 2); 

2922  231 
by (Blast_tac 2); 
1553  232 
by (etac exE 1); 
4089  233 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
1553  234 
by (rtac exI 1); 
1782  235 
by (rtac (refl RS disjI2 RS conjI) 1); 
1553  236 
by (etac equalityE 1); 
237 
by (asm_full_simp_tac 

4089  238 
(simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1); 
4153  239 
by Safe_tac; 
1553  240 
by (Asm_full_simp_tac 1); 
241 
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1); 

4153  242 
by (SELECT_GOAL Safe_tac 1); 
1553  243 
by (subgoal_tac "x ~= f m" 1); 
2922  244 
by (Blast_tac 2); 
1553  245 
by (subgoal_tac "? k. f k = x & k<m" 1); 
2922  246 
by (Blast_tac 2); 
4153  247 
by (SELECT_GOAL Safe_tac 1); 
1553  248 
by (res_inst_tac [("x","k")] exI 1); 
249 
by (Asm_simp_tac 1); 

4686  250 
by (Simp_tac 1); 
2922  251 
by (Blast_tac 1); 
3457  252 
by (dtac sym 1); 
1553  253 
by (rotate_tac ~1 1); 
254 
by (Asm_full_simp_tac 1); 

255 
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1); 

4153  256 
by (SELECT_GOAL Safe_tac 1); 
1553  257 
by (subgoal_tac "x ~= f m" 1); 
2922  258 
by (Blast_tac 2); 
1553  259 
by (subgoal_tac "? k. f k = x & k<m" 1); 
2922  260 
by (Blast_tac 2); 
4153  261 
by (SELECT_GOAL Safe_tac 1); 
1553  262 
by (res_inst_tac [("x","k")] exI 1); 
263 
by (Asm_simp_tac 1); 

4686  264 
by (Simp_tac 1); 
2922  265 
by (Blast_tac 1); 
1553  266 
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1); 
4153  267 
by (SELECT_GOAL Safe_tac 1); 
1553  268 
by (subgoal_tac "x ~= f i" 1); 
2922  269 
by (Blast_tac 2); 
1553  270 
by (case_tac "x = f m" 1); 
271 
by (res_inst_tac [("x","i")] exI 1); 

272 
by (Asm_simp_tac 1); 

273 
by (subgoal_tac "? k. f k = x & k<m" 1); 

2922  274 
by (Blast_tac 2); 
4153  275 
by (SELECT_GOAL Safe_tac 1); 
1553  276 
by (res_inst_tac [("x","k")] exI 1); 
277 
by (Asm_simp_tac 1); 

4686  278 
by (Simp_tac 1); 
2922  279 
by (Blast_tac 1); 
1531  280 
val lemma = result(); 
281 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

282 
Goal "[ finite A; x ~: A ] ==> \ 
3842  283 
\ (LEAST n. ? f. insert x A = {f ii. i<n}) = Suc(LEAST n. ? f. A={f ii. i<n})"; 
1553  284 
by (rtac Least_equality 1); 
3457  285 
by (dtac finite_has_card 1); 
286 
by (etac exE 1); 

3842  287 
by (dres_inst_tac [("P","%n.? f. A={f ii. i<n}")] LeastI 1); 
3457  288 
by (etac exE 1); 
1553  289 
by (res_inst_tac 
1531  290 
[("x","%i. if i<(LEAST n. ? f. A={f i i. i < n}) then f i else x")] exI 1); 
1553  291 
by (simp_tac 
4089  292 
(simpset() addsimps [Collect_conv_insert, less_Suc_eq] 
2031  293 
addcongs [rev_conj_cong]) 1); 
3457  294 
by (etac subst 1); 
295 
by (rtac refl 1); 

1553  296 
by (rtac notI 1); 
297 
by (etac exE 1); 

298 
by (dtac lemma 1); 

3457  299 
by (assume_tac 1); 
1553  300 
by (etac exE 1); 
301 
by (etac conjE 1); 

302 
by (dres_inst_tac [("P","%x. ? g. A = {g i i. i < x}")] Least_le 1); 

303 
by (dtac le_less_trans 1 THEN atac 1); 

4089  304 
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1); 
1553  305 
by (etac disjE 1); 
306 
by (etac less_asym 1 THEN atac 1); 

307 
by (hyp_subst_tac 1); 

308 
by (Asm_full_simp_tac 1); 

1531  309 
val lemma = result(); 
310 

5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

311 
Goalw [card_def] "[ finite A; x ~: A ] ==> card(insert x A) = Suc(card A)"; 
1553  312 
by (etac lemma 1); 
313 
by (assume_tac 1); 

1531  314 
qed "card_insert_disjoint"; 
3352  315 
Addsimps [card_insert_disjoint]; 
316 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

317 
Goal "finite A ==> card A <= card (insert x A)"; 
4768
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

318 
by (case_tac "x: A" 1); 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

319 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

320 
qed "card_insert_le"; 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

321 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

322 
Goal "finite A ==> !B. B <= A > card(B) <= card(A)"; 
3352  323 
by (etac finite_induct 1); 
324 
by (Simp_tac 1); 

3708  325 
by (Clarify_tac 1); 
3352  326 
by (case_tac "x:B" 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

327 
by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); 
5476  328 
by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2); 
4775  329 
by (fast_tac (claset() addss 
5477  330 
(simpset() addsimps [subset_insert_iff, finite_subset] 
331 
delsimps [insert_subset])) 1); 

3352  332 
qed_spec_mp "card_mono"; 
333 

5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

334 

9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

335 
Goal "[ finite A; finite B ] \ 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

336 
\ ==> card A + card B = card (A Un B) + card (A Int B)"; 
3352  337 
by (etac finite_induct 1); 
5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

338 
by (Simp_tac 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

339 
by (asm_simp_tac (simpset() addsimps [insert_absorb, Int_insert_left]) 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

340 
qed "card_Un_Int"; 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

341 

9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

342 
Goal "[ finite A; finite B; A Int B = {} ] \ 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

343 
\ ==> card (A Un B) = card A + card B"; 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

344 
by (asm_simp_tac (simpset() addsimps [card_Un_Int]) 1); 
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

345 
qed "card_Un_disjoint"; 
3352  346 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

347 
Goal "[ finite A; B<=A ] ==> card A  card B = card (A  B)"; 
3352  348 
by (subgoal_tac "(AB) Un B = A" 1); 
349 
by (Blast_tac 2); 

3457  350 
by (rtac (add_right_cancel RS iffD1) 1); 
351 
by (rtac (card_Un_disjoint RS subst) 1); 

352 
by (etac ssubst 4); 

3352  353 
by (Blast_tac 3); 
354 
by (ALLGOALS 

355 
(asm_simp_tac 

4089  356 
(simpset() addsimps [add_commute, not_less_iff_le, 
5416
9f029e382b5d
New law card_Un_Int. Removed card_insert from simpset
paulson
parents:
5413
diff
changeset

357 
add_diff_inverse, card_mono, finite_subset]))); 
3352  358 
qed "card_Diff_subset"; 
1531  359 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

360 
Goal "[ finite A; x: A ] ==> Suc(card(A{x})) = card A"; 
1618  361 
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); 
362 
by (assume_tac 1); 

3352  363 
by (Asm_simp_tac 1); 
1618  364 
qed "card_Suc_Diff"; 
365 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

366 
Goal "[ finite A; x: A ] ==> card(A{x}) < card A"; 
2031  367 
by (rtac Suc_less_SucD 1); 
4089  368 
by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); 
1618  369 
qed "card_Diff"; 
370 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

371 
Goal "finite A ==> card(A{x}) <= card A"; 
4768
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

372 
by (case_tac "x: A" 1); 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

373 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le]))); 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

374 
qed "card_Diff_le"; 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

375 

3389
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

376 

3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

377 
(*** Cardinality of the Powerset ***) 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

378 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

379 
Goal "finite A ==> card(insert x A) = Suc(card(A{x}))"; 
1553  380 
by (case_tac "x:A" 1); 
4768
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

381 
by (ALLGOALS 
c342d63173e9
New theorems card_Diff_le and card_insert_le; tidied
paulson
parents:
4763
diff
changeset

382 
(asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb]))); 
1531  383 
qed "card_insert"; 
384 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

385 
Goal "finite(A) ==> inj_on f A > card (f `` A) = card A"; 
3340  386 
by (etac finite_induct 1); 
387 
by (ALLGOALS Asm_simp_tac); 

3724  388 
by Safe_tac; 
4830  389 
by (rewtac inj_on_def); 
3340  390 
by (Blast_tac 1); 
391 
by (stac card_insert_disjoint 1); 

392 
by (etac finite_imageI 1); 

393 
by (Blast_tac 1); 

394 
by (Blast_tac 1); 

395 
qed_spec_mp "card_image"; 

396 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

397 
Goal "finite A ==> card (Pow A) = 2 ^ card A"; 
3389
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

398 
by (etac finite_induct 1); 
4089  399 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); 
3389
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

400 
by (stac card_Un_disjoint 1); 
4089  401 
by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1])); 
4830  402 
by (subgoal_tac "inj_on (insert x) (Pow F)" 1); 
4089  403 
by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1); 
4830  404 
by (rewtac inj_on_def); 
4089  405 
by (blast_tac (claset() addSEs [equalityE]) 1); 
3389
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

406 
qed "card_Pow"; 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

407 
Addsimps [card_Pow]; 
3340  408 

3389
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

409 

3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

410 
(*Proper subsets*) 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

411 
Goalw [psubset_def] "finite B ==> !A. A < B > card(A) < card(B)"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

412 
by (etac finite_induct 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

413 
by (Simp_tac 1); 
3708  414 
by (Clarify_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

415 
by (case_tac "x:A" 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

416 
(*1*) 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

417 
by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); 
4775  418 
by (Clarify_tac 1); 
419 
by (rotate_tac ~3 1); 

420 
by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1); 

3708  421 
by (Blast_tac 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

422 
(*2*) 
3708  423 
by (eres_inst_tac [("P","?a<?b")] notE 1); 
4775  424 
by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

425 
by (case_tac "A=F" 1); 
3708  426 
by (ALLGOALS Asm_simp_tac); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

427 
qed_spec_mp "psubset_card" ; 
3368  428 

429 

3430  430 
(*Relates to equivalence classes. Based on a theorem of F. Kammueller's. 
3368  431 
The "finite C" premise is redundant*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

432 
Goal "finite C ==> finite (Union C) > \ 
3368  433 
\ (! c : C. k dvd card c) > \ 
434 
\ (! c1: C. ! c2: C. c1 ~= c2 > c1 Int c2 = {}) \ 

435 
\ > k dvd card(Union C)"; 

436 
by (etac finite_induct 1); 

437 
by (ALLGOALS Asm_simp_tac); 

3708  438 
by (Clarify_tac 1); 
3368  439 
by (stac card_Un_disjoint 1); 
440 
by (ALLGOALS 

4089  441 
(asm_full_simp_tac (simpset() 
3368  442 
addsimps [dvd_add, disjoint_eq_subset_Compl]))); 
443 
by (thin_tac "!c:F. ?PP(c)" 1); 

444 
by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1); 

3708  445 
by (Clarify_tac 1); 
3368  446 
by (ball_tac 1); 
447 
by (Blast_tac 1); 

448 
qed_spec_mp "dvd_partition"; 

449 