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.6  
     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.14  
    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.18  
    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.26  
    1.27 @@ -321,10 +331,20 @@
    1.28      - a : (- 1) *o C"
    1.29    by (auto simp add: elt_set_times_def)
    1.30  
    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.35  
    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}"