author  nipkow 
Thu, 05 Jun 1997 14:39:22 +0200  
changeset 3413  c1f63cc3a768 
parent 3389  3150eba724a1 
child 3415  c068bd2f0bbd 
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 

9 
open Finite; 

10 

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

11 
section "finite"; 
1531  12 

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

13 
(* 
923  14 
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; 
1465  15 
by (rtac lfp_mono 1); 
923  16 
by (REPEAT (ares_tac basic_monos 1)); 
17 
qed "Fin_mono"; 

18 

19 
goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)"; 

2922  20 
by (blast_tac (!claset addSIs [lfp_lowerbound]) 1); 
923  21 
qed "Fin_subset_Pow"; 
22 

23 
(* A : Fin(B) ==> A <= B *) 

24 
val FinD = Fin_subset_Pow RS subsetD RS PowD; 

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

25 
*) 
923  26 

27 
(*Discharging ~ x:y entails extra work*) 

28 
val major::prems = goal Finite.thy 

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

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

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

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

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

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

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

37 

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

38 
val major::prems = goal Finite.thy 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

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

41 
\ !!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

42 
\ ] ==> F <= A > P(F)"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

44 
by(ALLGOALS (blast_tac (!claset addIs prems))); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

45 
val lemma = result(); 
923  46 

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

47 
val prems = goal Finite.thy 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

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

50 
\ !!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

51 
\ ] ==> P(F)"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

52 
by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

54 

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

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

56 
AddSIs Finites.intrs; 
923  57 

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

59 
val major::prems = goal Finite.thy 

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

60 
"[ finite F; finite G ] ==> finite(F Un G)"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

61 
by (rtac (major RS finite_induct) 1); 
1264  62 
by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left])))); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

63 
qed "finite_UnI"; 
923  64 

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

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

66 
val [subs,fin] = goal Finite.thy "[ A<=B; finite B ] ==> finite A"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

67 
by (EVERY1 [subgoal_tac "ALL C. C<=B > finite C", 
1465  68 
rtac mp, etac spec, 
69 
rtac subs]); 

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

70 
by (rtac (fin RS finite_induct) 1); 
1264  71 
by (simp_tac (!simpset addsimps [subset_Un_eq]) 1); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

72 
by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1])); 
923  73 
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); 
1264  74 
by (ALLGOALS Asm_simp_tac); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

75 
qed "finite_subset"; 
923  76 

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

77 
goal Finite.thy "finite(F Un G) = (finite F & finite G)"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

78 
by (blast_tac (!claset addIs [finite_UnI] addDs 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

79 
[Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

81 
AddIffs[finite_Un]; 
1531  82 

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

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

85 
by (simp_tac (HOL_ss addsimps [finite_Un]) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

86 
by (blast_tac (!claset addSIs Finites.intrs) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

88 
Addsimps[finite_insert]; 
1531  89 

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

90 
(*The image of a finite set is finite *) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

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

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

95 
qed "finite_imageI"; 
923  96 

97 
val major::prems = goal Finite.thy 

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

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

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

102 
by (rtac (major RS finite_induct) 1); 
2031  103 
by (stac Diff_insert 2); 
923  104 
by (ALLGOALS (asm_simp_tac 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

105 
(!simpset addsimps (prems@[Diff_subset RS finite_subset])))); 
1531  106 
val lemma = result(); 
923  107 

108 
val prems = goal Finite.thy 

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

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

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

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

1531  114 
by (rtac (lemma RS mp) 1); 
923  115 
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

116 
qed "finite_empty_induct"; 
1531  117 

118 

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

1531  121 
Addsimps [finite_Diff]; 
122 

3368  123 
goal Finite.thy "finite(A{a}) = finite(A)"; 
124 
by (case_tac "a:A" 1); 

125 
br (finite_insert RS sym RS trans) 1; 

126 
by (stac insert_Diff 1); 

127 
by (ALLGOALS Asm_simp_tac); 

128 
qed "finite_Diff_singleton"; 

129 
AddIffs [finite_Diff_singleton]; 

130 

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

131 
(*** FIXME > equalities.ML ***) 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

132 
goal Set.thy "(f``A = {}) = (A = {})"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

133 
by (blast_tac (!claset addSEs [equalityE]) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

135 
Addsimps [image_is_empty]; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

136 

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

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

139 
by (ALLGOALS Asm_simp_tac); 
3368  140 
by (Step_tac 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

141 
by (subgoal_tac "EX y:A. f y = x & F = f``(A{y})" 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

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

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

144 
by (Blast_tac 1); 
3368  145 
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

146 
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); 
3368  147 
by (Step_tac 1); 
148 
by (res_inst_tac [("x","xa")] bexI 1); 

149 
by (ALLGOALS Asm_simp_tac); 

150 
be equalityE 1; 

151 
br equalityI 1; 

152 
by (Blast_tac 2); 

153 
by (Best_tac 1); 

154 
val lemma = result(); 

155 

156 
goal Finite.thy "!!A. [ finite(f``A); inj_onto f A ] ==> finite A"; 

157 
bd lemma 1; 

158 
by (Blast_tac 1); 

159 
qed "finite_imageD"; 

160 

161 

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

163 

164 
goal Finite.thy "!!A. finite(Pow A) ==> finite A"; 

165 
by (subgoal_tac "finite ((%x.{x})``A)" 1); 

166 
br finite_subset 2; 

167 
ba 3; 

168 
by (ALLGOALS 

169 
(fast_tac (!claset addSDs [rewrite_rule [inj_onto_def] finite_imageD]))); 

170 
val lemma = result(); 

171 

172 
goal Finite.thy "finite(Pow A) = finite A"; 

173 
br iffI 1; 

174 
be lemma 1; 

175 
(*Opposite inclusion: finite A ==> finite (Pow A) *) 

3340  176 
by (etac finite_induct 1); 
177 
by (ALLGOALS 

178 
(asm_simp_tac 

179 
(!simpset addsimps [finite_UnI, finite_imageI, Pow_insert]))); 

3368  180 
qed "finite_Pow_iff"; 
181 
AddIffs [finite_Pow_iff]; 

3340  182 

1531  183 

1548  184 
section "Finite cardinality  'card'"; 
1531  185 

186 
goal Set.thy "{f i i. P i  i=n} = insert (f n) {f ii. P i}"; 

2922  187 
by (Blast_tac 1); 
1531  188 
val Collect_conv_insert = result(); 
189 

190 
goalw Finite.thy [card_def] "card {} = 0"; 

1553  191 
by (rtac Least_equality 1); 
192 
by (ALLGOALS Asm_full_simp_tac); 

1531  193 
qed "card_empty"; 
194 
Addsimps [card_empty]; 

195 

196 
val [major] = goal Finite.thy 

197 
"finite A ==> ? (n::nat) f. A = {f i i. i<n}"; 

1553  198 
by (rtac (major RS finite_induct) 1); 
199 
by (res_inst_tac [("x","0")] exI 1); 

200 
by (Simp_tac 1); 

201 
by (etac exE 1); 

202 
by (etac exE 1); 

203 
by (hyp_subst_tac 1); 

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

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

1660  206 
by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
1548  207 
addcongs [rev_conj_cong]) 1); 
1531  208 
qed "finite_has_card"; 
209 

210 
goal Finite.thy 

211 
"!!A.[ x ~: A; insert x A = {f ii.i<n} ] ==> \ 

212 
\ ? m::nat. m<n & (? g. A = {g ii.i<m})"; 

1553  213 
by (res_inst_tac [("n","n")] natE 1); 
214 
by (hyp_subst_tac 1); 

215 
by (Asm_full_simp_tac 1); 

216 
by (rename_tac "m" 1); 

217 
by (hyp_subst_tac 1); 

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

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

220 
by (Simp_tac 2); 

2922  221 
by (Blast_tac 2); 
1553  222 
by (etac exE 1); 
1660  223 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1553  224 
by (rtac exI 1); 
1782  225 
by (rtac (refl RS disjI2 RS conjI) 1); 
1553  226 
by (etac equalityE 1); 
227 
by (asm_full_simp_tac 

1660  228 
(!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1); 
2922  229 
by (safe_tac (!claset)); 
1553  230 
by (Asm_full_simp_tac 1); 
231 
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1); 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

232 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  233 
by (subgoal_tac "x ~= f m" 1); 
2922  234 
by (Blast_tac 2); 
1553  235 
by (subgoal_tac "? k. f k = x & k<m" 1); 
2922  236 
by (Blast_tac 2); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

237 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  238 
by (res_inst_tac [("x","k")] exI 1); 
239 
by (Asm_simp_tac 1); 

240 
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); 

2922  241 
by (Blast_tac 1); 
1531  242 
bd sym 1; 
1553  243 
by (rotate_tac ~1 1); 
244 
by (Asm_full_simp_tac 1); 

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

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

246 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  247 
by (subgoal_tac "x ~= f m" 1); 
2922  248 
by (Blast_tac 2); 
1553  249 
by (subgoal_tac "? k. f k = x & k<m" 1); 
2922  250 
by (Blast_tac 2); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

251 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  252 
by (res_inst_tac [("x","k")] exI 1); 
253 
by (Asm_simp_tac 1); 

254 
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); 

2922  255 
by (Blast_tac 1); 
1553  256 
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

257 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  258 
by (subgoal_tac "x ~= f i" 1); 
2922  259 
by (Blast_tac 2); 
1553  260 
by (case_tac "x = f m" 1); 
261 
by (res_inst_tac [("x","i")] exI 1); 

262 
by (Asm_simp_tac 1); 

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

2922  264 
by (Blast_tac 2); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

265 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  266 
by (res_inst_tac [("x","k")] exI 1); 
267 
by (Asm_simp_tac 1); 

268 
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); 

2922  269 
by (Blast_tac 1); 
1531  270 
val lemma = result(); 
271 

272 
goal Finite.thy "!!A. [ finite A; x ~: A ] ==> \ 

273 
\ (LEAST n. ? f. insert x A = {f ii.i<n}) = Suc(LEAST n. ? f. A={f ii.i<n})"; 

1553  274 
by (rtac Least_equality 1); 
1531  275 
bd finite_has_card 1; 
276 
be exE 1; 

1553  277 
by (dres_inst_tac [("P","%n.? f. A={f ii.i<n}")] LeastI 1); 
1531  278 
be exE 1; 
1553  279 
by (res_inst_tac 
1531  280 
[("x","%i. if i<(LEAST n. ? f. A={f i i. i < n}) then f i else x")] exI 1); 
1553  281 
by (simp_tac 
1660  282 
(!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
2031  283 
addcongs [rev_conj_cong]) 1); 
1531  284 
be subst 1; 
285 
br refl 1; 

1553  286 
by (rtac notI 1); 
287 
by (etac exE 1); 

288 
by (dtac lemma 1); 

1531  289 
ba 1; 
1553  290 
by (etac exE 1); 
291 
by (etac conjE 1); 

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

293 
by (dtac le_less_trans 1 THEN atac 1); 

1660  294 
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1553  295 
by (etac disjE 1); 
296 
by (etac less_asym 1 THEN atac 1); 

297 
by (hyp_subst_tac 1); 

298 
by (Asm_full_simp_tac 1); 

1531  299 
val lemma = result(); 
300 

301 
goalw Finite.thy [card_def] 

302 
"!!A. [ finite A; x ~: A ] ==> card(insert x A) = Suc(card A)"; 

1553  303 
by (etac lemma 1); 
304 
by (assume_tac 1); 

1531  305 
qed "card_insert_disjoint"; 
3352  306 
Addsimps [card_insert_disjoint]; 
307 

308 
goal Finite.thy "!!A. finite A ==> !B. B <= A > card(B) <= card(A)"; 

309 
by (etac finite_induct 1); 

310 
by (Simp_tac 1); 

311 
by (strip_tac 1); 

312 
by (case_tac "x:B" 1); 

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

313 
by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); 
3352  314 
by (SELECT_GOAL(safe_tac (!claset))1); 
315 
by (rotate_tac ~1 1); 

316 
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); 

317 
by (rotate_tac ~1 1); 

318 
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); 

319 
qed_spec_mp "card_mono"; 

320 

321 
goal Finite.thy "!!A B. [ finite A; finite B ]\ 

322 
\ ==> A Int B = {} > card(A Un B) = card A + card B"; 

323 
by (etac finite_induct 1); 

324 
by (ALLGOALS 

325 
(asm_simp_tac (!simpset addsimps [Un_insert_left, Int_insert_left] 

326 
setloop split_tac [expand_if]))); 

327 
qed_spec_mp "card_Un_disjoint"; 

328 

329 
goal Finite.thy "!!A. [ finite A; B<=A ] ==> card A  card B = card (A  B)"; 

330 
by (subgoal_tac "(AB) Un B = A" 1); 

331 
by (Blast_tac 2); 

332 
br (add_right_cancel RS iffD1) 1; 

333 
br (card_Un_disjoint RS subst) 1; 

334 
be ssubst 4; 

335 
by (Blast_tac 3); 

336 
by (ALLGOALS 

337 
(asm_simp_tac 

338 
(!simpset addsimps [add_commute, not_less_iff_le, 

339 
add_diff_inverse, card_mono, finite_subset]))); 

340 
qed "card_Diff_subset"; 

1531  341 

1618  342 
goal Finite.thy "!!A. [ finite A; x: A ] ==> Suc(card(A{x})) = card A"; 
343 
by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); 

344 
by (assume_tac 1); 

3352  345 
by (Asm_simp_tac 1); 
1618  346 
qed "card_Suc_Diff"; 
347 

348 
goal Finite.thy "!!A. [ finite A; x: A ] ==> card(A{x}) < card A"; 

2031  349 
by (rtac Suc_less_SucD 1); 
1618  350 
by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1); 
351 
qed "card_Diff"; 

352 

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

353 

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

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

355 

1531  356 
val [major] = goal Finite.thy 
357 
"finite A ==> card(insert x A) = Suc(card(A{x}))"; 

1553  358 
by (case_tac "x:A" 1); 
359 
by (asm_simp_tac (!simpset addsimps [insert_absorb]) 1); 

360 
by (dtac mk_disjoint_insert 1); 

361 
by (etac exE 1); 

362 
by (Asm_simp_tac 1); 

363 
by (rtac card_insert_disjoint 1); 

364 
by (rtac (major RSN (2,finite_subset)) 1); 

2922  365 
by (Blast_tac 1); 
366 
by (Blast_tac 1); 

1553  367 
by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1); 
1531  368 
qed "card_insert"; 
369 
Addsimps [card_insert]; 

370 

3340  371 
goal Finite.thy "!!A. finite(A) ==> inj_onto f A > card (f `` A) = card A"; 
372 
by (etac finite_induct 1); 

373 
by (ALLGOALS Asm_simp_tac); 

374 
by (Step_tac 1); 

375 
bw inj_onto_def; 

376 
by (Blast_tac 1); 

377 
by (stac card_insert_disjoint 1); 

378 
by (etac finite_imageI 1); 

379 
by (Blast_tac 1); 

380 
by (Blast_tac 1); 

381 
qed_spec_mp "card_image"; 

382 

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

383 
goal thy "!!A. finite A ==> card (Pow A) = 2 ^ card A"; 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

384 
by (etac finite_induct 1); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

385 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Pow_insert]))); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

386 
by (stac card_Un_disjoint 1); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

387 
by (EVERY (map (blast_tac (!claset addIs [finite_imageI])) [3,2,1])); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

388 
by (subgoal_tac "inj_onto (insert x) (Pow F)" 1); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

389 
by (asm_simp_tac (!simpset addsimps [card_image, Pow_insert]) 1); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

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

391 
by (blast_tac (!claset addSEs [equalityE]) 1); 
3150eba724a1
New theorem about the cardinality of the powerset (uses exponentiation)
paulson
parents:
3382
diff
changeset

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

393 
Addsimps [card_Pow]; 
3340  394 

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

395 

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

396 
(*Proper subsets*) 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

397 
goalw Finite.thy [psubset_def] 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

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

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

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

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

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

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

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

406 
by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

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

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

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

411 
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

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

414 
(*2*) 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

416 
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2922
diff
changeset

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

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

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

420 
qed_spec_mp "psubset_card" ; 
3368  421 

422 

423 
(*Relates to equivalence classes. Based on a theorem of F. Kammüller's. 

424 
The "finite C" premise is redundant*) 

425 
goal thy "!!C. finite C ==> finite (Union C) > \ 

426 
\ (! c : C. k dvd card c) > \ 

427 
\ (! c1: C. ! c2: C. c1 ~= c2 > c1 Int c2 = {}) \ 

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

429 
by (etac finite_induct 1); 

430 
by (ALLGOALS Asm_simp_tac); 

431 
by (strip_tac 1); 

432 
by (REPEAT (etac conjE 1)); 

433 
by (stac card_Un_disjoint 1); 

434 
by (ALLGOALS 

435 
(asm_full_simp_tac (!simpset 

436 
addsimps [dvd_add, disjoint_eq_subset_Compl]))); 

437 
by (thin_tac "?PP>?QQ" 1); 

438 
by (thin_tac "!c:F. ?PP(c)" 1); 

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

440 
by (Step_tac 1); 

441 
by (ball_tac 1); 

442 
by (Blast_tac 1); 

443 
qed_spec_mp "dvd_partition"; 

444 