author  berghofe 
Mon, 03 Jun 1996 17:10:56 +0200  
changeset 1786  8a31d85d27b8 
parent 1782  ab45b881fa62 
child 2031  03a843f0f447 
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 

1548  11 
section "The finite powerset operator  Fin"; 
1531  12 

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

17 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

19 
by (fast_tac (!claset addSIs [lfp_lowerbound]) 1); 
923  20 
qed "Fin_subset_Pow"; 
21 

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

23 
val FinD = Fin_subset_Pow RS subsetD RS PowD; 

24 

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

26 
val major::prems = goal Finite.thy 

27 
"[ F:Fin(A); P({}); \ 

1465  28 
\ !!F x. [ x:A; F:Fin(A); x~:F; P(F) ] ==> P(insert x F) \ 
923  29 
\ ] ==> P(F)"; 
30 
by (rtac (major RS Fin.induct) 1); 

31 
by (excluded_middle_tac "a:b" 2); 

32 
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) 

33 
by (REPEAT (ares_tac prems 1)); 

34 
qed "Fin_induct"; 

35 

1264  36 
Addsimps Fin.intrs; 
923  37 

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

39 
val major::prems = goal Finite.thy 

40 
"[ F: Fin(A); G: Fin(A) ] ==> F Un G : Fin(A)"; 

41 
by (rtac (major RS Fin_induct) 1); 

1264  42 
by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left])))); 
923  43 
qed "Fin_UnI"; 
44 

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

46 
val [subs,fin] = goal Finite.thy "[ A<=B; B: Fin(M) ] ==> A: Fin(M)"; 

47 
by (EVERY1 [subgoal_tac "ALL C. C<=B > C: Fin(M)", 

1465  48 
rtac mp, etac spec, 
49 
rtac subs]); 

923  50 
by (rtac (fin RS Fin_induct) 1); 
1264  51 
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

52 
by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1])); 
923  53 
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); 
1264  54 
by (ALLGOALS Asm_simp_tac); 
923  55 
qed "Fin_subset"; 
56 

1531  57 
goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))"; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

58 
by (fast_tac (!claset addIs [Fin_UnI] addDs 
1531  59 
[Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1); 
60 
qed "subset_Fin"; 

61 
Addsimps[subset_Fin]; 

62 

63 
goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)"; 

1553  64 
by (stac insert_is_Un 1); 
65 
by (Simp_tac 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

66 
by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1); 
1531  67 
qed "insert_Fin"; 
68 
Addsimps[insert_Fin]; 

69 

923  70 
(*The image of a finite set is finite*) 
71 
val major::_ = goal Finite.thy 

72 
"F: Fin(A) ==> h``F : Fin(h``A)"; 

73 
by (rtac (major RS Fin_induct) 1); 

1264  74 
by (Simp_tac 1); 
75 
by (asm_simp_tac 

1660  76 
(!simpset addsimps [image_eqI RS Fin.insertI, image_insert] 
77 
delsimps [insert_Fin]) 1); 

923  78 
qed "Fin_imageI"; 
79 

80 
val major::prems = goal Finite.thy 

1465  81 
"[ c: Fin(A); b: Fin(A); \ 
82 
\ P(b); \ 

923  83 
\ !!(x::'a) y. [ x:A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \ 
84 
\ ] ==> c<=b > P(bc)"; 

85 
by (rtac (major RS Fin_induct) 1); 

86 
by (rtac (Diff_insert RS ssubst) 2); 

87 
by (ALLGOALS (asm_simp_tac 

1264  88 
(!simpset addsimps (prems@[Diff_subset RS Fin_subset])))); 
1531  89 
val lemma = result(); 
923  90 

91 
val prems = goal Finite.thy 

1465  92 
"[ b: Fin(A); \ 
93 
\ P(b); \ 

923  94 
\ !!x y. [ x:A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \ 
95 
\ ] ==> P({})"; 

96 
by (rtac (Diff_cancel RS subst) 1); 

1531  97 
by (rtac (lemma RS mp) 1); 
923  98 
by (REPEAT (ares_tac (subset_refl::prems) 1)); 
99 
qed "Fin_empty_induct"; 

1531  100 

101 

1548  102 
section "The predicate 'finite'"; 
1531  103 

104 
val major::prems = goalw Finite.thy [finite_def] 

105 
"[ finite F; P({}); \ 

106 
\ !!F x. [ finite F; x~:F; P(F) ] ==> P(insert x F) \ 

107 
\ ] ==> P(F)"; 

108 
by (rtac (major RS Fin_induct) 1); 

109 
by (REPEAT (ares_tac prems 1)); 

110 
qed "finite_induct"; 

111 

112 

113 
goalw Finite.thy [finite_def] "finite {}"; 

1553  114 
by (Simp_tac 1); 
1531  115 
qed "finite_emptyI"; 
116 
Addsimps [finite_emptyI]; 

117 

118 
goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)"; 

1553  119 
by (Asm_simp_tac 1); 
1531  120 
qed "finite_insertI"; 
121 

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

123 
goalw Finite.thy [finite_def] 

124 
"!!F. [ finite F; finite G ] ==> finite(F Un G)"; 

1553  125 
by (Asm_simp_tac 1); 
1531  126 
qed "finite_UnI"; 
127 

128 
goalw Finite.thy [finite_def] "!!A. [ A<=B; finite B ] ==> finite A"; 

1553  129 
by (etac Fin_subset 1); 
130 
by (assume_tac 1); 

1531  131 
qed "finite_subset"; 
132 

133 
goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)"; 

1553  134 
by (Simp_tac 1); 
1531  135 
qed "subset_finite"; 
136 
Addsimps[subset_finite]; 

137 

138 
goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)"; 

1553  139 
by (Simp_tac 1); 
1531  140 
qed "insert_finite"; 
141 
Addsimps[insert_finite]; 

142 

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

1531  145 
Addsimps [finite_Diff]; 
146 

147 
(*The image of a finite set is finite*) 

148 
goal Finite.thy "!!F. finite F ==> finite(h``F)"; 

1553  149 
by (etac finite_induct 1); 
150 
by (ALLGOALS Asm_simp_tac); 

1531  151 
qed "finite_imageI"; 
152 

153 
val major::prems = goalw Finite.thy [finite_def] 

154 
"[ finite A; \ 

155 
\ P(A); \ 

156 
\ !!a A. [ finite A; a:A; P(A) ] ==> P(A{a}) \ 

157 
\ ] ==> P({})"; 

158 
by (rtac (major RS Fin_empty_induct) 1); 

159 
by (REPEAT (ares_tac (subset_refl::prems) 1)); 

160 
qed "finite_empty_induct"; 

161 

162 

1548  163 
section "Finite cardinality  'card'"; 
1531  164 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

166 
by (Fast_tac 1); 
1531  167 
val Collect_conv_insert = result(); 
168 

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

1553  170 
by (rtac Least_equality 1); 
171 
by (ALLGOALS Asm_full_simp_tac); 

1531  172 
qed "card_empty"; 
173 
Addsimps [card_empty]; 

174 

175 
val [major] = goal Finite.thy 

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

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

179 
by (Simp_tac 1); 

180 
by (etac exE 1); 

181 
by (etac exE 1); 

182 
by (hyp_subst_tac 1); 

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

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

1660  185 
by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
1548  186 
addcongs [rev_conj_cong]) 1); 
1531  187 
qed "finite_has_card"; 
188 

189 
goal Finite.thy 

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

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

1553  192 
by (res_inst_tac [("n","n")] natE 1); 
193 
by (hyp_subst_tac 1); 

194 
by (Asm_full_simp_tac 1); 

195 
by (rename_tac "m" 1); 

196 
by (hyp_subst_tac 1); 

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

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

199 
by (Simp_tac 2); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

200 
by (Fast_tac 2); 
1553  201 
by (etac exE 1); 
1660  202 
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1553  203 
by (rtac exI 1); 
1782  204 
by (rtac (refl RS disjI2 RS conjI) 1); 
1553  205 
by (etac equalityE 1); 
206 
by (asm_full_simp_tac 

1660  207 
(!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

208 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  209 
by (Asm_full_simp_tac 1); 
210 
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

211 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  212 
by (subgoal_tac "x ~= f m" 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

213 
by (Fast_tac 2); 
1553  214 
by (subgoal_tac "? k. f k = x & k<m" 1); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

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

216 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  217 
by (res_inst_tac [("x","k")] exI 1); 
218 
by (Asm_simp_tac 1); 

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

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

220 
by (best_tac (!claset) 1); 
1531  221 
bd sym 1; 
1553  222 
by (rotate_tac ~1 1); 
223 
by (Asm_full_simp_tac 1); 

224 
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

225 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  226 
by (subgoal_tac "x ~= f m" 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

227 
by (Fast_tac 2); 
1553  228 
by (subgoal_tac "? k. f k = x & k<m" 1); 
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1782
diff
changeset

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

230 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  231 
by (res_inst_tac [("x","k")] exI 1); 
232 
by (Asm_simp_tac 1); 

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

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

234 
by (best_tac (!claset) 1); 
1553  235 
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

236 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  237 
by (subgoal_tac "x ~= f i" 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

238 
by (Fast_tac 2); 
1553  239 
by (case_tac "x = f m" 1); 
240 
by (res_inst_tac [("x","i")] exI 1); 

241 
by (Asm_simp_tac 1); 

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

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

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

244 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  245 
by (res_inst_tac [("x","k")] exI 1); 
246 
by (Asm_simp_tac 1); 

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

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

248 
by (best_tac (!claset) 1); 
1531  249 
val lemma = result(); 
250 

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

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

1553  253 
by (rtac Least_equality 1); 
1531  254 
bd finite_has_card 1; 
255 
be exE 1; 

1553  256 
by (dres_inst_tac [("P","%n.? f. A={f ii.i<n}")] LeastI 1); 
1531  257 
be exE 1; 
1553  258 
by (res_inst_tac 
1531  259 
[("x","%i. if i<(LEAST n. ? f. A={f i i. i < n}) then f i else x")] exI 1); 
1553  260 
by (simp_tac 
1660  261 
(!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
262 
addcongs [rev_conj_cong]) 1); 

1531  263 
be subst 1; 
264 
br refl 1; 

1553  265 
by (rtac notI 1); 
266 
by (etac exE 1); 

267 
by (dtac lemma 1); 

1531  268 
ba 1; 
1553  269 
by (etac exE 1); 
270 
by (etac conjE 1); 

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

272 
by (dtac le_less_trans 1 THEN atac 1); 

1660  273 
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
1553  274 
by (etac disjE 1); 
275 
by (etac less_asym 1 THEN atac 1); 

276 
by (hyp_subst_tac 1); 

277 
by (Asm_full_simp_tac 1); 

1531  278 
val lemma = result(); 
279 

280 
goalw Finite.thy [card_def] 

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

1553  282 
by (etac lemma 1); 
283 
by (assume_tac 1); 

1531  284 
qed "card_insert_disjoint"; 
285 

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

288 
by (assume_tac 1); 

289 
by (asm_simp_tac (!simpset addsimps [card_insert_disjoint]) 1); 

290 
qed "card_Suc_Diff"; 

291 

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

293 
by (resolve_tac [Suc_less_SucD] 1); 

294 
by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1); 

295 
qed "card_Diff"; 

296 

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

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

301 
by (dtac mk_disjoint_insert 1); 

302 
by (etac exE 1); 

303 
by (Asm_simp_tac 1); 

304 
by (rtac card_insert_disjoint 1); 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

306 
by (Fast_tac 1); 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1660
diff
changeset

307 
by (Fast_tac 1); 
1553  308 
by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1); 
1531  309 
qed "card_insert"; 
310 
Addsimps [card_insert]; 

311 

312 

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

1553  314 
by (etac finite_induct 1); 
315 
by (Simp_tac 1); 

316 
by (strip_tac 1); 

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

318 
by (dtac mk_disjoint_insert 1); 

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

319 
by (SELECT_GOAL(safe_tac (!claset))1); 
1553  320 
by (rotate_tac ~1 1); 
321 
by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); 

322 
by (rotate_tac ~1 1); 

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

1531  324 
qed_spec_mp "card_mono"; 