author paulson Wed, 22 Mar 2000 13:22:11 +0100 changeset 8554 ba33995b87ff parent 8553 a79f6fb4d426 child 8555 17325ee838ab
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the default claset. Used "inst"
 src/HOL/Finite.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite.ML	Wed Mar 22 13:01:57 2000 +0100
+++ b/src/HOL/Finite.ML	Wed Mar 22 13:22:11 2000 +0100
@@ -54,22 +54,17 @@

Goal "finite(F Un G) = (finite F & finite G)";
by (blast_tac (claset()
-			finite_UnI]) 1);
+	         addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1);
qed "finite_Un";

-Goal "finite F ==> finite(F Int G)";
-by (blast_tac (claset() addIs [finite_subset]) 1);
-qed "finite_Int1";
-
-Goal "finite G ==> finite(F Int G)";
+(*The converse obviously fails*)
+Goal "finite F | finite G ==> finite(F Int G)";
by (blast_tac (claset() addIs [finite_subset]) 1);
-qed "finite_Int2";
+qed "finite_Int";

-

Goal "finite(insert a A) = finite A";
by (stac insert_is_Un 1);
@@ -125,12 +120,11 @@
qed "finite_Diff_insert";

-(* lemma merely for classical reasoner *)
+(*lemma merely for classical reasoner in the proof below: force_tac can't
+  prove it.*)
Goal "finite(A-{}) = finite A";
by (Simp_tac 1);
val lemma = result();