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 

1531

11 
(*** Fin ***)


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 


101 
(*** finite ***)


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 


166 
(*** Cardinality ***)


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 
(*Addsimps [Collect_conv_insert];*)


179 


180 
val [major] = goal Finite.thy


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


182 
br (major RS finite_induct) 1;


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


184 
by(Simp_tac 1);


185 
be exE 1;


186 
be exE 1;


187 
by(hyp_subst_tac 1);


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


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


190 
by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]


191 
addcongs [Collect_cong1]) 1);


192 
qed "finite_has_card";


193 


194 
goal Finite.thy


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


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


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


198 
by(hyp_subst_tac 1);


199 
by(Asm_full_simp_tac 1);


200 
by(rename_tac "m" 1);


201 
by(hyp_subst_tac 1);


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


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


204 
by(Simp_tac 2);


205 
by(fast_tac eq_cs 2);


206 
be exE 1;


207 
by(Simp_tac 1);


208 
br exI 1;


209 
br conjI 1;


210 
br disjI2 1;


211 
br refl 1;


212 
be equalityE 1;


213 
by(asm_full_simp_tac


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


215 
by(SELECT_GOAL(safe_tac eq_cs)1);


216 
by(Asm_full_simp_tac 1);


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


218 
by(SELECT_GOAL(safe_tac eq_cs)1);


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


220 
by(fast_tac set_cs 2);


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


222 
by(best_tac set_cs 2);


223 
by(SELECT_GOAL(safe_tac HOL_cs)1);


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


225 
by(Asm_simp_tac 1);


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


227 
by(best_tac set_cs 1);


228 
bd sym 1;


229 
by(rotate_tac ~1 1);


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


232 
by(SELECT_GOAL(safe_tac eq_cs)1);


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


234 
by(fast_tac set_cs 2);


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


236 
by(best_tac set_cs 2);


237 
by(SELECT_GOAL(safe_tac HOL_cs)1);


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


241 
by(best_tac set_cs 1);


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


243 
by(SELECT_GOAL(safe_tac eq_cs)1);


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


245 
by(fast_tac set_cs 2);


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


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


248 
by(Asm_simp_tac 1);


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


250 
by(best_tac set_cs 2);


251 
by(SELECT_GOAL(safe_tac HOL_cs)1);


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


255 
by(best_tac set_cs 1);


256 
val lemma = result();


257 


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


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


260 
br Least_equality 1;


261 
bd finite_has_card 1;


262 
be exE 1;


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


264 
be exE 1;


265 
by(res_inst_tac


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


267 
by(simp_tac


268 
(!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);


269 
be subst 1;


270 
br refl 1;


271 
br notI 1;


272 
be exE 1;


273 
bd lemma 1;


274 
ba 1;


275 
be exE 1;


276 
be conjE 1;


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


278 
by(dtac le_less_trans 1 THEN atac 1);


279 
by(Asm_full_simp_tac 1);


280 
be disjE 1;


281 
by(etac less_asym 1 THEN atac 1);


282 
by(hyp_subst_tac 1);


283 
by(Asm_full_simp_tac 1);


284 
val lemma = result();


285 


286 
goalw Finite.thy [card_def]


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


288 
be lemma 1;


289 
ba 1;


290 
qed "card_insert_disjoint";


291 


292 
val [major] = goal Finite.thy


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


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


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


296 
bd mk_disjoint_insert 1;


297 
be exE 1;


298 
by(Asm_simp_tac 1);


299 
br card_insert_disjoint 1;


300 
br (major RSN (2,finite_subset)) 1;


301 
by(fast_tac set_cs 1);


302 
by(fast_tac HOL_cs 1);


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


304 
qed "card_insert";


305 
Addsimps [card_insert];


306 


307 


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


309 
be finite_induct 1;


310 
by(Simp_tac 1);


311 
by(strip_tac 1);


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


313 
bd mk_disjoint_insert 1;


314 
by(SELECT_GOAL(safe_tac HOL_cs)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";
