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


58 
by(fast_tac (set_cs addIs [Fin_UnI] addDs


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


64 
by(stac insert_is_Un 1);


65 
by(Simp_tac 1);


66 
by(fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);


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


113 
by(Simp_tac 1);


114 
qed "finite_emptyI";


115 
Addsimps [finite_emptyI];


116 


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


118 
by(Asm_simp_tac 1);


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


124 
by(Asm_simp_tac 1);


125 
qed "finite_UnI";


126 


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


128 
be Fin_subset 1;


129 
ba 1;


130 
qed "finite_subset";


131 


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


133 
by(Simp_tac 1);


134 
qed "subset_finite";


135 
Addsimps[subset_finite];


136 


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


138 
by(Simp_tac 1);


139 
qed "insert_finite";


140 
Addsimps[insert_finite];


141 


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


143 
be finite_induct 1;


144 
by(Simp_tac 1);


145 
by(asm_simp_tac (!simpset addsimps [insert_Diff_if]


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


152 
be finite_induct 1;


153 
by(ALLGOALS Asm_simp_tac);


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


169 
by(fast_tac eq_cs 1);


170 
val Collect_conv_insert = result();


171 


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


173 
br Least_equality 1;


174 
by(ALLGOALS Asm_full_simp_tac);


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


180 
br (major RS finite_induct) 1;


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


182 
by(Simp_tac 1);


183 
be exE 1;


184 
be 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})";


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 
be exE 1;


205 
by(Simp_tac 1);


206 
br exI 1;


207 
br conjI 1;


208 
br disjI2 1;


209 
br refl 1;


210 
be equalityE 1;


211 
by(asm_full_simp_tac


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


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


226 
bd sym 1;


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


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


258 
br Least_equality 1;


259 
bd finite_has_card 1;


260 
be exE 1;


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


262 
be exE 1;


263 
by(res_inst_tac


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


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;


269 
br notI 1;


270 
be exE 1;


271 
bd lemma 1;


272 
ba 1;


273 
be exE 1;


274 
be 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 
be disjE 1;


279 
by(etac less_asym 1 THEN atac 1);


280 
by(hyp_subst_tac 1);


281 
by(Asm_full_simp_tac 1);


282 
val lemma = result();


283 


284 
goalw Finite.thy [card_def]


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


286 
be lemma 1;


287 
ba 1;


288 
qed "card_insert_disjoint";


289 


290 
val [major] = goal Finite.thy


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


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


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


294 
bd mk_disjoint_insert 1;


295 
be exE 1;


296 
by(Asm_simp_tac 1);


297 
br card_insert_disjoint 1;


298 
br (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);


302 
qed "card_insert";


303 
Addsimps [card_insert];


304 


305 


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


307 
be finite_induct 1;


308 
by(Simp_tac 1);


309 
by(strip_tac 1);


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


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


317 
qed_spec_mp "card_mono";
