src/HOL/Library/Set_Algebras.thy

--- a/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:06:46 2013 -0700
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:33:36 2013 -0700
@@ -90,6 +90,11 @@
 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
   by (auto simp add: set_plus_def)
 
+lemma set_plus_elim:
+  assumes "x \<in> A + B"
+  obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_plus_def by fast
+
 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   by (auto simp add: elt_set_plus_def)
 
@@ -201,6 +206,11 @@
 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
   by (auto simp add: set_times_def)
 
+lemma set_times_elim:
+  assumes "x \<in> A * B"
+  obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
+  using assms unfolding set_times_def by fast
+
 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   by (auto simp add: elt_set_times_def)
 
@@ -321,10 +331,20 @@
     - a : (- 1) *o C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_plus_image:
-  fixes S T :: "'n::semigroup_add set" shows "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
+lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   unfolding set_plus_def by (fastforce simp: image_iff)
 
+lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
+  unfolding set_times_def by (fastforce simp: image_iff)
+
+lemma finite_set_plus:
+  assumes "finite s" and "finite t" shows "finite (s + t)"
+  using assms unfolding set_plus_image by simp
+
+lemma finite_set_times:
+  assumes "finite s" and "finite t" shows "finite (s * t)"
+  using assms unfolding set_times_image by simp
+
 lemma set_setsum_alt:
   assumes fin: "finite I"
   shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"