# HG changeset patch
# User paulson
# Date 891517623 -7200
# Node ID c342d63173e95f87f503402fff4af6d720a08fc9
# Parent  b9f3468c6ee22337d0240d7629be4c578c3739ce
New theorems card_Diff_le and card_insert_le; tidied

diff -r b9f3468c6ee2 -r c342d63173e9 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Apr 02 12:45:47 1998 +0200
+++ b/src/HOL/Finite.ML	Thu Apr 02 13:47:03 1998 +0200
@@ -10,20 +10,6 @@
 
 section "finite";
 
-(*
-goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "Fin_mono";
-
-goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (blast_tac (claset() addSIs [lfp_lowerbound]) 1);
-qed "Fin_subset_Pow";
-
-(* A : Fin(B) ==> A <= B *)
-val FinD = Fin_subset_Pow RS subsetD RS PowD;
-*)
-
 (*Discharging ~ x:y entails extra work*)
 val major::prems = goal Finite.thy 
     "[| finite F;  P({}); \
@@ -323,6 +309,11 @@
 qed "card_insert_disjoint";
 Addsimps [card_insert_disjoint];
 
+goal Finite.thy "!!A. finite A ==> card A <= card (insert x A)";
+by (case_tac "x: A" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
+qed "card_insert_le";
+
 goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
@@ -366,21 +357,18 @@
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
 qed "card_Diff";
 
+goal Finite.thy "!!A. finite A ==> card(A-{x}) <= card A";
+by (case_tac "x: A" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le])));
+qed "card_Diff_le";
+
 
 (*** Cardinality of the Powerset ***)
 
-val [major] = goal Finite.thy
-  "finite A ==> card(insert x A) = Suc(card(A-{x}))";
+goal Finite.thy "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))";
 by (case_tac "x:A" 1);
-by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
-by (dtac mk_disjoint_insert 1);
-by (etac exE 1);
-by (Asm_simp_tac 1);
-by (rtac card_insert_disjoint 1);
-by (rtac (major RSN (2,finite_subset)) 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addsimps [major RS card_insert_disjoint]) 1);
+by (ALLGOALS 
+    (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
 qed "card_insert";
 Addsimps [card_insert];