src/HOL/Library/Set_Algebras.thy
 changeset 47444 d21c95af2df7 parent 47443 aeff49a3369b child 47445 69e96e5500df
```     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 19:58:59 2012 +0200
1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 22:55:11 2012 +0200
1.3 @@ -333,18 +333,13 @@
1.4    fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
1.5    unfolding set_plus_def by (fastforce simp: image_iff)
1.6
1.7 -text {* Legacy syntax: *}
1.8 -
1.9 -abbreviation (input) setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
1.10 -   "setsum_set == setsum"
1.11 -
1.12  lemma set_setsum_alt:
1.13    assumes fin: "finite I"
1.14 -  shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
1.15 +  shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
1.16      (is "_ = ?setsum I")
1.17  using fin proof induct
1.18    case (insert x F)
1.19 -  have "setsum_set S (insert x F) = S x \<oplus> ?setsum F"
1.20 +  have "setsum S (insert x F) = S x \<oplus> ?setsum F"
1.21      using insert.hyps by auto
1.22    also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
1.23      unfolding set_plus_def
1.24 @@ -363,12 +358,12 @@
1.25    assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A \<oplus> B)" "P {0}"
1.26      and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A \<oplus> B) = f A \<oplus> f B" "f {0} = {0}"
1.27    assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
1.28 -  shows "f (setsum_set S I) = setsum_set (f \<circ> S) I"
1.29 +  shows "f (setsum S I) = setsum (f \<circ> S) I"
1.30  proof cases
1.31    assume "finite I" from this all show ?thesis
1.32    proof induct
1.33      case (insert x F)
1.34 -    from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum_set S F)"
1.35 +    from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
1.36        by induct auto
1.37      with insert show ?case
1.38        by (simp, subst f) auto
1.39 @@ -378,7 +373,7 @@
1.40  lemma setsum_set_linear: