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)";


19 
by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);


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);

923

52 
by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));


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))";

1553

58 
by (fast_tac (set_cs 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);


66 
by (fast_tac (set_cs 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


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

923

77 
qed "Fin_imageI";


78 


79 
val major::prems = goal Finite.thy

1465

80 
"[ c: Fin(A); b: Fin(A); \


81 
\ P(b); \

923

82 
\ !!(x::'a) y. [ x:A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \


83 
\ ] ==> c<=b > P(bc)";


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


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


86 
by (ALLGOALS (asm_simp_tac

1264

87 
(!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));

1531

88 
val lemma = result();

923

89 


90 
val prems = goal Finite.thy

1465

91 
"[ b: Fin(A); \


92 
\ P(b); \

923

93 
\ !!x y. [ x:A; y: Fin(A); x:y; P(y) ] ==> P(y{x}) \


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


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

1531

96 
by (rtac (lemma RS mp) 1);

923

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


98 
qed "Fin_empty_induct";

1531

99 


100 

1548

101 
section "The predicate 'finite'";

1531

102 


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


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


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


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


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


108 
by (REPEAT (ares_tac prems 1));


109 
qed "finite_induct";


110 


111 


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

1553

113 
by (Simp_tac 1);

1531

114 
qed "finite_emptyI";


115 
Addsimps [finite_emptyI];


116 


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

1553

118 
by (Asm_simp_tac 1);

1531

119 
qed "finite_insertI";


120 


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


122 
goalw Finite.thy [finite_def]


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

1553

124 
by (Asm_simp_tac 1);

1531

125 
qed "finite_UnI";


126 


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

1553

128 
by (etac Fin_subset 1);


129 
by (assume_tac 1);

1531

130 
qed "finite_subset";


131 


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

1553

133 
by (Simp_tac 1);

1531

134 
qed "subset_finite";


135 
Addsimps[subset_finite];


136 


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

1553

138 
by (Simp_tac 1);

1531

139 
qed "insert_finite";


140 
Addsimps[insert_finite];


141 

1618

142 
(* finite B ==> finite (B  Ba) *)


143 
bind_thm ("finite_Diff", Diff_subset RS finite_subset);

1531

144 
Addsimps [finite_Diff];


145 


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


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

1553

148 
by (etac finite_induct 1);


149 
by (ALLGOALS Asm_simp_tac);

1531

150 
qed "finite_imageI";


151 


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


153 
"[ finite A; \


154 
\ P(A); \


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


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


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


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


159 
qed "finite_empty_induct";


160 


161 

1548

162 
section "Finite cardinality  'card'";

1531

163 


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

1553

165 
by (fast_tac eq_cs 1);

1531

166 
val Collect_conv_insert = result();


167 


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

1553

169 
by (rtac Least_equality 1);


170 
by (ALLGOALS Asm_full_simp_tac);

1531

171 
qed "card_empty";


172 
Addsimps [card_empty];


173 


174 
val [major] = goal Finite.thy


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

1553

176 
by (rtac (major RS finite_induct) 1);


177 
by (res_inst_tac [("x","0")] exI 1);


178 
by (Simp_tac 1);


179 
by (etac exE 1);


180 
by (etac exE 1);


181 
by (hyp_subst_tac 1);


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


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


184 
by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]

1548

185 
addcongs [rev_conj_cong]) 1);

1531

186 
qed "finite_has_card";


187 


188 
goal Finite.thy


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


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

1553

191 
by (res_inst_tac [("n","n")] natE 1);


192 
by (hyp_subst_tac 1);


193 
by (Asm_full_simp_tac 1);


194 
by (rename_tac "m" 1);


195 
by (hyp_subst_tac 1);


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


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


198 
by (Simp_tac 2);


199 
by (fast_tac eq_cs 2);


200 
by (etac exE 1);


201 
by (Simp_tac 1);


202 
by (rtac exI 1);


203 
by (rtac conjI 1);

1531

204 
br disjI2 1;


205 
br refl 1;

1553

206 
by (etac equalityE 1);


207 
by (asm_full_simp_tac

1531

208 
(!simpset addsimps [subset_insert,Collect_conv_insert]) 1);

1553

209 
by (SELECT_GOAL(safe_tac eq_cs)1);


210 
by (Asm_full_simp_tac 1);


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


212 
by (SELECT_GOAL(safe_tac eq_cs)1);


213 
by (subgoal_tac "x ~= f m" 1);


214 
by (fast_tac set_cs 2);


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


216 
by (best_tac set_cs 2);


217 
by (SELECT_GOAL(safe_tac HOL_cs)1);


218 
by (res_inst_tac [("x","k")] exI 1);


219 
by (Asm_simp_tac 1);


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


221 
by (best_tac set_cs 1);

1531

222 
bd sym 1;

1553

223 
by (rotate_tac ~1 1);


224 
by (Asm_full_simp_tac 1);


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


226 
by (SELECT_GOAL(safe_tac eq_cs)1);


227 
by (subgoal_tac "x ~= f m" 1);


228 
by (fast_tac set_cs 2);


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


230 
by (best_tac set_cs 2);


231 
by (SELECT_GOAL(safe_tac HOL_cs)1);


232 
by (res_inst_tac [("x","k")] exI 1);


233 
by (Asm_simp_tac 1);


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


235 
by (best_tac set_cs 1);


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


237 
by (SELECT_GOAL(safe_tac eq_cs)1);


238 
by (subgoal_tac "x ~= f i" 1);


239 
by (fast_tac set_cs 2);


240 
by (case_tac "x = f m" 1);


241 
by (res_inst_tac [("x","i")] exI 1);


242 
by (Asm_simp_tac 1);


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


244 
by (best_tac set_cs 2);


245 
by (SELECT_GOAL(safe_tac HOL_cs)1);


246 
by (res_inst_tac [("x","k")] exI 1);


247 
by (Asm_simp_tac 1);


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


249 
by (best_tac set_cs 1);

1531

250 
val lemma = result();


251 


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


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

1553

254 
by (rtac Least_equality 1);

1531

255 
bd finite_has_card 1;


256 
be exE 1;

1553

257 
by (dres_inst_tac [("P","%n.? f. A={f ii.i<n}")] LeastI 1);

1531

258 
be exE 1;

1553

259 
by (res_inst_tac

1531

260 
[("x","%i. if i<(LEAST n. ? f. A={f i i. i < n}) then f i else x")] exI 1);

1553

261 
by (simp_tac

1548

262 
(!simpset addsimps [Collect_conv_insert] 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);


273 
by (Asm_full_simp_tac 1);


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);


306 
by (fast_tac set_cs 1);


307 
by (fast_tac HOL_cs 1);


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);


319 
by (SELECT_GOAL(safe_tac HOL_cs)1);


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";
