--- a/src/HOL/Finite.ML Tue Sep 01 10:11:06 1998 +0200
+++ b/src/HOL/Finite.ML Tue Sep 01 10:25:05 1998 +0200
@@ -56,11 +56,23 @@
Goal "finite(F Un G) = (finite F & finite G)";
by (blast_tac (claset()
- addIs [read_instantiate [("B", "?AA Un ?BB")] finite_subset,
+ addIs [read_instantiate [("B", "?X Un ?Y")] finite_subset,
finite_UnI]) 1);
qed "finite_Un";
AddIffs[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)";
+by (blast_tac (claset() addIs [finite_subset]) 1);
+qed "finite_Int2";
+
+Addsimps[finite_Int1, finite_Int2];
+AddIs[finite_Int1, finite_Int2];
+
+
Goal "finite(insert a A) = finite A";
by (stac insert_is_Un 1);
by (simp_tac (HOL_ss addsimps [finite_Un]) 1);