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 


142 
goal Finite.thy "!!A. finite(A) ==> finite(AB)";

1553

143 
by (etac finite_induct 1);


144 
by (Simp_tac 1);


145 
by (asm_simp_tac (!simpset addsimps [insert_Diff_if]

1531

146 
setloop split_tac[expand_if]) 1);


147 
qed "finite_Diff";


148 
Addsimps [finite_Diff];


149 


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


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

1553

152 
by (etac finite_induct 1);


153 
by (ALLGOALS Asm_simp_tac);

1531

154 
qed "finite_imageI";


155 


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


157 
"[ finite A; \


158 
\ P(A); \


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


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


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


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


163 
qed "finite_empty_induct";


164 


165 

1548

166 
section "Finite cardinality  'card'";

1531

167 


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

1553

169 
by (fast_tac eq_cs 1);

1531

170 
val Collect_conv_insert = result();


171 


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

1553

173 
by (rtac Least_equality 1);


174 
by (ALLGOALS Asm_full_simp_tac);

1531

175 
qed "card_empty";


176 
Addsimps [card_empty];


177 


178 
val [major] = goal Finite.thy


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

1553

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


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


182 
by (Simp_tac 1);


183 
by (etac exE 1);


184 
by (etac exE 1);


185 
by (hyp_subst_tac 1);


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


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


188 
by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]

1548

189 
addcongs [rev_conj_cong]) 1);

1531

190 
qed "finite_has_card";


191 


192 
goal Finite.thy


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


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

1553

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


196 
by (hyp_subst_tac 1);


197 
by (Asm_full_simp_tac 1);


198 
by (rename_tac "m" 1);


199 
by (hyp_subst_tac 1);


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


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


202 
by (Simp_tac 2);


203 
by (fast_tac eq_cs 2);


204 
by (etac exE 1);


205 
by (Simp_tac 1);


206 
by (rtac exI 1);


207 
by (rtac conjI 1);

1531

208 
br disjI2 1;


209 
br refl 1;

1553

210 
by (etac equalityE 1);


211 
by (asm_full_simp_tac

1531

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

1553

213 
by (SELECT_GOAL(safe_tac eq_cs)1);


214 
by (Asm_full_simp_tac 1);


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


216 
by (SELECT_GOAL(safe_tac eq_cs)1);


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


218 
by (fast_tac set_cs 2);


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


220 
by (best_tac set_cs 2);


221 
by (SELECT_GOAL(safe_tac HOL_cs)1);


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


223 
by (Asm_simp_tac 1);


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


225 
by (best_tac set_cs 1);

1531

226 
bd sym 1;

1553

227 
by (rotate_tac ~1 1);


228 
by (Asm_full_simp_tac 1);


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


230 
by (SELECT_GOAL(safe_tac eq_cs)1);


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


232 
by (fast_tac set_cs 2);


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


234 
by (best_tac set_cs 2);


235 
by (SELECT_GOAL(safe_tac HOL_cs)1);


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


237 
by (Asm_simp_tac 1);


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


239 
by (best_tac set_cs 1);


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


241 
by (SELECT_GOAL(safe_tac eq_cs)1);


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


243 
by (fast_tac set_cs 2);


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


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


246 
by (Asm_simp_tac 1);


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


248 
by (best_tac set_cs 2);


249 
by (SELECT_GOAL(safe_tac HOL_cs)1);


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


251 
by (Asm_simp_tac 1);


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


253 
by (best_tac set_cs 1);

1531

254 
val lemma = result();


255 


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


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

1553

258 
by (rtac Least_equality 1);

1531

259 
bd finite_has_card 1;


260 
be exE 1;

1553

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

1531

262 
be exE 1;

1553

263 
by (res_inst_tac

1531

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

1553

265 
by (simp_tac

1548

266 
(!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);

1531

267 
be subst 1;


268 
br refl 1;

1553

269 
by (rtac notI 1);


270 
by (etac exE 1);


271 
by (dtac lemma 1);

1531

272 
ba 1;

1553

273 
by (etac exE 1);


274 
by (etac conjE 1);


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


276 
by (dtac le_less_trans 1 THEN atac 1);


277 
by (Asm_full_simp_tac 1);


278 
by (etac disjE 1);


279 
by (etac less_asym 1 THEN atac 1);


280 
by (hyp_subst_tac 1);


281 
by (Asm_full_simp_tac 1);

1531

282 
val lemma = result();


283 


284 
goalw Finite.thy [card_def]


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

1553

286 
by (etac lemma 1);


287 
by (assume_tac 1);

1531

288 
qed "card_insert_disjoint";


289 


290 
val [major] = goal Finite.thy


291 
"finite A ==> card(insert x A) = Suc(card(A{x}))";

1553

292 
by (case_tac "x:A" 1);


293 
by (asm_simp_tac (!simpset addsimps [insert_absorb]) 1);


294 
by (dtac mk_disjoint_insert 1);


295 
by (etac exE 1);


296 
by (Asm_simp_tac 1);


297 
by (rtac card_insert_disjoint 1);


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


299 
by (fast_tac set_cs 1);


300 
by (fast_tac HOL_cs 1);


301 
by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);

1531

302 
qed "card_insert";


303 
Addsimps [card_insert];


304 


305 


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

1553

307 
by (etac finite_induct 1);


308 
by (Simp_tac 1);


309 
by (strip_tac 1);


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


311 
by (dtac mk_disjoint_insert 1);


312 
by (SELECT_GOAL(safe_tac HOL_cs)1);


313 
by (rotate_tac ~1 1);


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


315 
by (rotate_tac ~1 1);


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

1531

317 
qed_spec_mp "card_mono";
