src/HOL/Finite.ML
author nipkow
Mon Mar 04 14:37:33 1996 +0100 (1996-03-04)
changeset 1531 e5eb247ad13c
parent 1465 5d7a7e439cec
child 1548 afe750876848
permissions -rw-r--r--
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.
     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 (*** 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 (*** 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(A-B)";
   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 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 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 i|i.i<n} |] ==> \
   196 \  ? m::nat. m<n & (? g. A = {g i|i.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 i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.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 i|i.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";