src/HOL/Library/Set_Algebras.thy
 changeset 64267 b9a1486e79be parent 63680 6e1e8b5abbfa child 69313 b021008c5397
```     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Sun Oct 16 22:43:51 2016 +0200
1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Mon Oct 17 11:46:22 2016 +0200
1.3 @@ -347,24 +347,24 @@
1.4  lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
1.6
1.7 -lemma set_setsum_alt:
1.8 +lemma set_sum_alt:
1.9    assumes fin: "finite I"
1.10 -  shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
1.11 -    (is "_ = ?setsum I")
1.12 +  shows "sum S I = {sum s I |s. \<forall>i\<in>I. s i \<in> S i}"
1.13 +    (is "_ = ?sum I")
1.14    using fin
1.15  proof induct
1.16    case empty
1.17    then show ?case by simp
1.18  next
1.19    case (insert x F)
1.20 -  have "setsum S (insert x F) = S x + ?setsum F"
1.21 +  have "sum S (insert x F) = S x + ?sum F"
1.22      using insert.hyps by auto
1.23 -  also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
1.24 +  also have "\<dots> = {s x + sum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
1.25      unfolding set_plus_def
1.26    proof safe
1.27      fix y s
1.28      assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
1.29 -    then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
1.30 +    then show "\<exists>s'. y + sum s F = s' x + sum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
1.31        using insert.hyps
1.32        by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
1.33    qed auto
1.34 @@ -372,12 +372,12 @@
1.35      using insert.hyps by auto
1.36  qed
1.37
1.38 -lemma setsum_set_cond_linear:
1.39 +lemma sum_set_cond_linear:
1.41    assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A + B)" "P {0}"
1.42      and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
1.43    assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
1.44 -  shows "f (setsum S I) = setsum (f \<circ> S) I"
1.45 +  shows "f (sum S I) = sum (f \<circ> S) I"
1.46  proof (cases "finite I")
1.47    case True
1.48    from this all show ?thesis
1.49 @@ -386,7 +386,7 @@
1.50      then show ?case by (auto intro!: f)
1.51    next
1.52      case (insert x F)
1.53 -    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (setsum S F)"
1.54 +    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (sum S F)"
1.55        by induct auto
1.56      with insert show ?case
1.57        by (simp, subst f) auto
1.58 @@ -396,11 +396,11 @@
1.59    then show ?thesis by (auto intro!: f)
1.60  qed
1.61
1.62 -lemma setsum_set_linear:
1.63 +lemma sum_set_linear: