src/HOL/Library/Set_Algebras.thy
 changeset 53596 d29d63460d84 parent 47446 ed0795caec95 child 54230 b1d955791529
1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:06:46 2013 -0700
1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Sep 12 09:33:36 2013 -0700
1.3 @@ -90,6 +90,11 @@
1.4  lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
1.5    by (auto simp add: set_plus_def)
1.7 +lemma set_plus_elim:
1.8 +  assumes "x \<in> A + B"
1.9 +  obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
1.10 +  using assms unfolding set_plus_def by fast
1.11 +
1.12  lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
1.13    by (auto simp add: elt_set_plus_def)
1.15 @@ -201,6 +206,11 @@
1.16  lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
1.17    by (auto simp add: set_times_def)
1.19 +lemma set_times_elim:
1.20 +  assumes "x \<in> A * B"
1.21 +  obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
1.22 +  using assms unfolding set_times_def by fast
1.23 +
1.24  lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
1.25    by (auto simp add: elt_set_times_def)
1.27 @@ -321,10 +331,20 @@
1.28      - a : (- 1) *o C"
1.29    by (auto simp add: elt_set_times_def)
1.31 -lemma set_plus_image:
1.32 -  fixes S T :: "'n::semigroup_add set" shows "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
1.33 +lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
1.34    unfolding set_plus_def by (fastforce simp: image_iff)
1.36 +lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
1.37 +  unfolding set_times_def by (fastforce simp: image_iff)
1.38 +
1.39 +lemma finite_set_plus:
1.40 +  assumes "finite s" and "finite t" shows "finite (s + t)"
1.41 +  using assms unfolding set_plus_image by simp
1.42 +
1.43 +lemma finite_set_times:
1.44 +  assumes "finite s" and "finite t" shows "finite (s * t)"
1.45 +  using assms unfolding set_times_image by simp
1.46 +
1.47  lemma set_setsum_alt:
1.48    assumes fin: "finite I"
1.49    shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"