src/HOL/Finite.ML
author paulson
Wed Mar 06 13:57:07 1996 +0100 (1996-03-06)
changeset 1553 4eb4a9c7d736
parent 1548 afe750876848
child 1618 372880456b5b
permissions -rw-r--r--
Ran expandshort
     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 (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({}); \
    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 (set_cs 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 (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 
    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]) 1);
    77 qed "Fin_imageI";
    78 
    79 val major::prems = goal Finite.thy 
    80     "[| c: Fin(A);  b: Fin(A);                                  \
    81 \       P(b);                                                   \
    82 \       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    83 \    |] ==> c<=b --> P(b-c)";
    84 by (rtac (major RS Fin_induct) 1);
    85 by (rtac (Diff_insert RS ssubst) 2);
    86 by (ALLGOALS (asm_simp_tac
    87                 (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
    88 val lemma = result();
    89 
    90 val prems = goal Finite.thy 
    91     "[| b: Fin(A);                                              \
    92 \       P(b);                                                   \
    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);
    96 by (rtac (lemma RS mp) 1);
    97 by (REPEAT (ares_tac (subset_refl::prems) 1));
    98 qed "Fin_empty_induct";
    99 
   100 
   101 section "The predicate '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 by (etac Fin_subset 1);
   129 by (assume_tac 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(A-B)";
   143 by (etac 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 by (etac 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 section "Finite cardinality -- 'card'";
   167 
   168 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. 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 by (rtac 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 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]
   189                           addcongs [rev_conj_cong]) 1);
   190 qed "finite_has_card";
   191 
   192 goal Finite.thy
   193   "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
   194 \  ? m::nat. m<n & (? g. A = {g i|i.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 by (etac exE 1);
   205 by (Simp_tac 1);
   206 by (rtac exI 1);
   207 by (rtac conjI 1);
   208  br disjI2 1;
   209  br refl 1;
   210 by (etac 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 i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
   258 by (rtac Least_equality 1);
   259  bd finite_has_card 1;
   260  be exE 1;
   261  by (dres_inst_tac [("P","%n.? f. A={f i|i.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
   266     (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
   267  be subst 1;
   268  br refl 1;
   269 by (rtac notI 1);
   270 by (etac exE 1);
   271 by (dtac lemma 1);
   272  ba 1;
   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);
   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 by (etac lemma 1);
   287 by (assume_tac 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 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);
   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 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);
   317 qed_spec_mp "card_mono";