# HG changeset patch
# User paulson
# Date 904638305 -7200
# Node ID 9d11f2d39b1325436aabdae5455197dc44a37291
# Parent  0c2472c74c2496e148c68567105a7a837d896029
New lemmas involving Int

diff -r 0c2472c74c24 -r 9d11f2d39b13 src/HOL/Finite.ML
--- 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);