src/HOL/Finite.ML
 author nipkow Mon Oct 21 09:50:50 1996 +0200 (1996-10-21) changeset 2115 9709f9188549 parent 2031 03a843f0f447 child 2922 580647a879cf permissions -rw-r--r--
```     1 (*  Title:      HOL/Finite.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson & Tobias Nipkow
```
```     4     Copyright   1995  University of Cambridge & TU Muenchen
```
```     5
```
```     6 Finite sets and their cardinality
```
```     7 *)
```
```     8
```
```     9 open Finite;
```
```    10
```
```    11 section "The finite powerset operator -- Fin";
```
```    12
```
```    13 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
```
```    14 by (rtac lfp_mono 1);
```
```    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 (!claset 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({}); \
```
```    28 \       !!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
```
```    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
```
```    36 Addsimps Fin.intrs;
```
```    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);
```
```    42 by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
```
```    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)",
```
```    48             rtac mp, etac spec,
```
```    49             rtac subs]);
```
```    50 by (rtac (fin RS Fin_induct) 1);
```
```    51 by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
```
```    52 by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
```
```    53 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
```
```    54 by (ALLGOALS Asm_simp_tac);
```
```    55 qed "Fin_subset";
```
```    56
```
```    57 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
```
```    58 by (fast_tac (!claset 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 (!claset addSIs Fin.intrs addDs [FinD]) 1);
```
```    67 qed "insert_Fin";
```
```    68 Addsimps[insert_Fin];
```
```    69
```
```    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);
```
```    74 by (Simp_tac 1);
```
```    75 by (asm_simp_tac
```
```    76     (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
```
```    77               delsimps [insert_Fin]) 1);
```
```    78 qed "Fin_imageI";
```
```    79
```
```    80 val major::prems = goal Finite.thy
```
```    81     "[| c: Fin(A);  b: Fin(A);                                  \
```
```    82 \       P(b);                                                   \
```
```    83 \       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
```
```    84 \    |] ==> c<=b --> P(b-c)";
```
```    85 by (rtac (major RS Fin_induct) 1);
```
```    86 by (stac Diff_insert 2);
```
```    87 by (ALLGOALS (asm_simp_tac
```
```    88                 (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
```
```    89 val lemma = result();
```
```    90
```
```    91 val prems = goal Finite.thy
```
```    92     "[| b: Fin(A);                                              \
```
```    93 \       P(b);                                                   \
```
```    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);
```
```    97 by (rtac (lemma RS mp) 1);
```
```    98 by (REPEAT (ares_tac (subset_refl::prems) 1));
```
```    99 qed "Fin_empty_induct";
```
```   100
```
```   101
```
```   102 section "The predicate 'finite'";
```
```   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 {}";
```
```   114 by (Simp_tac 1);
```
```   115 qed "finite_emptyI";
```
```   116 Addsimps [finite_emptyI];
```
```   117
```
```   118 goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
```
```   119 by (Asm_simp_tac 1);
```
```   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)";
```
```   125 by (Asm_simp_tac 1);
```
```   126 qed "finite_UnI";
```
```   127
```
```   128 goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
```
```   129 by (etac Fin_subset 1);
```
```   130 by (assume_tac 1);
```
```   131 qed "finite_subset";
```
```   132
```
```   133 goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
```
```   134 by (Simp_tac 1);
```
```   135 qed "subset_finite";
```
```   136 Addsimps[subset_finite];
```
```   137
```
```   138 goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
```
```   139 by (Simp_tac 1);
```
```   140 qed "insert_finite";
```
```   141 Addsimps[insert_finite];
```
```   142
```
```   143 (* finite B ==> finite (B - Ba) *)
```
```   144 bind_thm ("finite_Diff", Diff_subset RS finite_subset);
```
```   145 Addsimps [finite_Diff];
```
```   146
```
```   147 (*The image of a finite set is finite*)
```
```   148 goal Finite.thy "!!F. finite F ==> finite(h``F)";
```
```   149 by (etac finite_induct 1);
```
```   150 by (ALLGOALS Asm_simp_tac);
```
```   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
```
```   163 section "Finite cardinality -- 'card'";
```
```   164
```
```   165 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
```
```   166 by (Fast_tac 1);
```
```   167 val Collect_conv_insert = result();
```
```   168
```
```   169 goalw Finite.thy [card_def] "card {} = 0";
```
```   170 by (rtac Least_equality 1);
```
```   171 by (ALLGOALS Asm_full_simp_tac);
```
```   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}";
```
```   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);
```
```   185 by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
```
```   186                           addcongs [rev_conj_cong]) 1);
```
```   187 qed "finite_has_card";
```
```   188
```
```   189 goal Finite.thy
```
```   190   "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
```
```   191 \  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
```
```   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);
```
```   200  by (Fast_tac 2);
```
```   201 by (etac exE 1);
```
```   202 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
```
```   203 by (rtac exI 1);
```
```   204 by (rtac (refl RS disjI2 RS conjI) 1);
```
```   205 by (etac equalityE 1);
```
```   206 by (asm_full_simp_tac
```
```   207      (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
```
```   208 by (SELECT_GOAL(safe_tac (!claset))1);
```
```   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);
```
```   211   by (SELECT_GOAL(safe_tac (!claset))1);
```
```   212    by (subgoal_tac "x ~= f m" 1);
```
```   213     by (Fast_tac 2);
```
```   214    by (subgoal_tac "? k. f k = x & k<m" 1);
```
```   215     by (best_tac (!claset) 2);
```
```   216    by (SELECT_GOAL(safe_tac (!claset))1);
```
```   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);
```
```   220   by (best_tac (!claset) 1);
```
```   221  bd sym 1;
```
```   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);
```
```   225  by (SELECT_GOAL(safe_tac (!claset))1);
```
```   226   by (subgoal_tac "x ~= f m" 1);
```
```   227    by (Fast_tac 2);
```
```   228   by (subgoal_tac "? k. f k = x & k<m" 1);
```
```   229    by (best_tac (!claset) 2);
```
```   230   by (SELECT_GOAL(safe_tac (!claset))1);
```
```   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);
```
```   234  by (best_tac (!claset) 1);
```
```   235 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
```
```   236 by (SELECT_GOAL(safe_tac (!claset))1);
```
```   237  by (subgoal_tac "x ~= f i" 1);
```
```   238   by (Fast_tac 2);
```
```   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);
```
```   243   by (best_tac (!claset) 2);
```
```   244  by (SELECT_GOAL(safe_tac (!claset))1);
```
```   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);
```
```   248 by (best_tac (!claset) 1);
```
```   249 val lemma = result();
```
```   250
```
```   251 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
```
```   252 \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
```
```   253 by (rtac Least_equality 1);
```
```   254  bd finite_has_card 1;
```
```   255  be exE 1;
```
```   256  by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
```
```   257  be exE 1;
```
```   258  by (res_inst_tac
```
```   259    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
```
```   260  by (simp_tac
```
```   261     (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
```
```   262               addcongs [rev_conj_cong]) 1);
```
```   263  be subst 1;
```
```   264  br refl 1;
```
```   265 by (rtac notI 1);
```
```   266 by (etac exE 1);
```
```   267 by (dtac lemma 1);
```
```   268  ba 1;
```
```   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 (!simpset addsimps [less_Suc_eq]) 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);
```
```   278 val lemma = result();
```
```   279
```
```   280 goalw Finite.thy [card_def]
```
```   281   "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
```
```   282 by (etac lemma 1);
```
```   283 by (assume_tac 1);
```
```   284 qed "card_insert_disjoint";
```
```   285
```
```   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 (rtac Suc_less_SucD 1);
```
```   294 by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1);
```
```   295 qed "card_Diff";
```
```   296
```
```   297 val [major] = goal Finite.thy
```
```   298   "finite A ==> card(insert x A) = Suc(card(A-{x}))";
```
```   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 1);
```
```   307 by (Fast_tac 1);
```
```   308 by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
```
```   309 qed "card_insert";
```
```   310 Addsimps [card_insert];
```
```   311
```
```   312
```
```   313 goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
```
```   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 (!claset))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);
```
```   324 qed_spec_mp "card_mono";
```