src/HOL/Finite.ML
changeset 923 ff1574a81019
child 1264 3eb91524b938
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Finite.ML	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,84 @@
     1.4 +(*  Title: 	HOL/Finite.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +Finite powerset operator
    1.10 +*)
    1.11 +
    1.12 +open Finite;
    1.13 +
    1.14 +goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    1.15 +br lfp_mono 1;
    1.16 +by (REPEAT (ares_tac basic_monos 1));
    1.17 +qed "Fin_mono";
    1.18 +
    1.19 +goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
    1.20 +by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
    1.21 +qed "Fin_subset_Pow";
    1.22 +
    1.23 +(* A : Fin(B) ==> A <= B *)
    1.24 +val FinD = Fin_subset_Pow RS subsetD RS PowD;
    1.25 +
    1.26 +(*Discharging ~ x:y entails extra work*)
    1.27 +val major::prems = goal Finite.thy 
    1.28 +    "[| F:Fin(A);  P({}); \
    1.29 +\	!!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
    1.30 +\    |] ==> P(F)";
    1.31 +by (rtac (major RS Fin.induct) 1);
    1.32 +by (excluded_middle_tac "a:b" 2);
    1.33 +by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
    1.34 +by (REPEAT (ares_tac prems 1));
    1.35 +qed "Fin_induct";
    1.36 +
    1.37 +(** Simplification for Fin **)
    1.38 +
    1.39 +val Fin_ss = set_ss addsimps Fin.intrs;
    1.40 +
    1.41 +(*The union of two finite sets is finite*)
    1.42 +val major::prems = goal Finite.thy
    1.43 +    "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
    1.44 +by (rtac (major RS Fin_induct) 1);
    1.45 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
    1.46 +qed "Fin_UnI";
    1.47 +
    1.48 +(*Every subset of a finite set is finite*)
    1.49 +val [subs,fin] = goal Finite.thy "[| A<=B;  B: Fin(M) |] ==> A: Fin(M)";
    1.50 +by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
    1.51 +	    rtac mp, etac spec,
    1.52 +	    rtac subs]);
    1.53 +by (rtac (fin RS Fin_induct) 1);
    1.54 +by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
    1.55 +by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
    1.56 +by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    1.57 +by (ALLGOALS (asm_simp_tac Fin_ss));
    1.58 +qed "Fin_subset";
    1.59 +
    1.60 +(*The image of a finite set is finite*)
    1.61 +val major::_ = goal Finite.thy
    1.62 +    "F: Fin(A) ==> h``F : Fin(h``A)";
    1.63 +by (rtac (major RS Fin_induct) 1);
    1.64 +by (simp_tac Fin_ss 1);
    1.65 +by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
    1.66 +qed "Fin_imageI";
    1.67 +
    1.68 +val major::prems = goal Finite.thy 
    1.69 +    "[| c: Fin(A);  b: Fin(A);  				\
    1.70 +\       P(b);       						\
    1.71 +\       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    1.72 +\    |] ==> c<=b --> P(b-c)";
    1.73 +by (rtac (major RS Fin_induct) 1);
    1.74 +by (rtac (Diff_insert RS ssubst) 2);
    1.75 +by (ALLGOALS (asm_simp_tac
    1.76 +                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
    1.77 +qed "Fin_empty_induct_lemma";
    1.78 +
    1.79 +val prems = goal Finite.thy 
    1.80 +    "[| b: Fin(A);  						\
    1.81 +\       P(b);        						\
    1.82 +\       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    1.83 +\    |] ==> P({})";
    1.84 +by (rtac (Diff_cancel RS subst) 1);
    1.85 +by (rtac (Fin_empty_induct_lemma RS mp) 1);
    1.86 +by (REPEAT (ares_tac (subset_refl::prems) 1));
    1.87 +qed "Fin_empty_induct";