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.5    by (simp add: set_times_image)
     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.40    fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
    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:
    1.64    fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
    1.65    assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
    1.66 -  shows "f (setsum S I) = setsum (f \<circ> S) I"
    1.67 -  using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
    1.68 +  shows "f (sum S I) = sum (f \<circ> S) I"
    1.69 +  using sum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
    1.70  
    1.71  lemma set_times_Un_distrib:
    1.72    "A * (B \<union> C) = A * B \<union> A * C"