# HG changeset patch
# User nipkow
# Date 878043805 -3600
# Node ID df6cd80b6387fcfc9093ad31c3c1676a78b4951f
# Parent  9ffb96bd2924869695966ed13fe923e284445f65
Added finite_UNION/SigmaI.

diff -r 9ffb96bd2924 -r df6cd80b6387 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Oct 27 16:01:53 1997 +0100
+++ b/src/HOL/Finite.ML	Tue Oct 28 14:03:25 1997 +0100
@@ -149,6 +149,22 @@
 by (Blast_tac 1);
 qed "finite_imageD";
 
+(** The finite UNION of finite sets **)
+
+val [prem] = goal Finite.thy
+ "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
+br (prem RS finite_induct) 1;
+by(ALLGOALS Asm_simp_tac);
+bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
+Addsimps [finite_UnionI];
+
+(** Sigma of finite sets **)
+
+goalw Finite.thy [Sigma_def]
+ "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
+by(blast_tac (!claset addSIs [finite_UnionI]) 1);
+bind_thm("finite_SigmaI", ballI RSN (2,result()));
+Addsimps [finite_SigmaI];
 
 (** The powerset of a finite set **)