1.1 --- a/src/HOL/Finite.ML	Thu Apr 02 12:45:47 1998 +0200
     1.2 +++ b/src/HOL/Finite.ML	Thu Apr 02 13:47:03 1998 +0200
     1.3 @@ -10,20 +10,6 @@
     1.4  
     1.5  section "finite";
     1.6  
     1.7 -(*
     1.8 -goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
     1.9 -by (rtac lfp_mono 1);
    1.10 -by (REPEAT (ares_tac basic_monos 1));
    1.11 -qed "Fin_mono";
    1.12 -
    1.13 -goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
    1.14 -by (blast_tac (claset() addSIs [lfp_lowerbound]) 1);
    1.15 -qed "Fin_subset_Pow";
    1.16 -
    1.17 -(* A : Fin(B) ==> A <= B *)
    1.18 -val FinD = Fin_subset_Pow RS subsetD RS PowD;
    1.19 -*)
    1.20 -
    1.21  (*Discharging ~ x:y entails extra work*)
    1.22  val major::prems = goal Finite.thy 
    1.23      "[| finite F;  P({}); \
    1.24 @@ -323,6 +309,11 @@
    1.25  qed "card_insert_disjoint";
    1.26  Addsimps [card_insert_disjoint];
    1.27  
    1.28 +goal Finite.thy "!!A. finite A ==> card A <= card (insert x A)";
    1.29 +by (case_tac "x: A" 1);
    1.30 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
    1.31 +qed "card_insert_le";
    1.32 +
    1.33  goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
    1.34  by (etac finite_induct 1);
    1.35  by (Simp_tac 1);
    1.36 @@ -366,21 +357,18 @@
    1.37  by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
    1.38  qed "card_Diff";
    1.39  
    1.40 +goal Finite.thy "!!A. finite A ==> card(A-{x}) <= card A";
    1.41 +by (case_tac "x: A" 1);
    1.42 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le])));
    1.43 +qed "card_Diff_le";
    1.44 +
    1.45  
    1.46  (*** Cardinality of the Powerset ***)
    1.47  
    1.48 -val [major] = goal Finite.thy
    1.49 -  "finite A ==> card(insert x A) = Suc(card(A-{x}))";
    1.50 +goal Finite.thy "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))";
    1.51  by (case_tac "x:A" 1);
    1.52 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
    1.53 -by (dtac mk_disjoint_insert 1);
    1.54 -by (etac exE 1);
    1.55 -by (Asm_simp_tac 1);
    1.56 -by (rtac card_insert_disjoint 1);
    1.57 -by (rtac (major RSN (2,finite_subset)) 1);
    1.58 -by (Blast_tac 1);
    1.59 -by (Blast_tac 1);
    1.60 -by (asm_simp_tac (simpset() addsimps [major RS card_insert_disjoint]) 1);
    1.61 +by (ALLGOALS 
    1.62 +    (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
    1.63  qed "card_insert";
    1.64  Addsimps [card_insert];
    1.65