src/HOL/Finite.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2031 03a843f0f447
child 2922 580647a879cf
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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";