# HG changeset patch
# User nipkow
# Date 1116869985 -7200
# Node ID 880b0e786c1b04f98598137f9d1a3cd472af5a4a
# Parent  b6a945f205b720f46f193095b17d6674d00d7fc4
tuned setsum rewrites

diff -r b6a945f205b7 -r 880b0e786c1b src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Mon May 23 19:14:16 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Mon May 23 19:39:45 2005 +0200
@@ -117,15 +117,16 @@
 
 (* Basic facts --- move to HOL!!! *)
 
+(* needed because natsum_cong (below) disables atMost_0 *)
 lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
 by simp
-
+(*
 lemma natsum_Suc [simp]:
   "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
 by (simp add: atMost_Suc)
-
+*)
 lemma natsum_Suc2:
-  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::comm_monoid_add)"
+  "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
 proof (induct n)
   case 0 show ?case by simp
 next
diff -r b6a945f205b7 -r 880b0e786c1b src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon May 23 19:14:16 2005 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon May 23 19:39:45 2005 +0200
@@ -286,7 +286,7 @@
     proof (cases n)
       case 0 then show ?thesis by simp
     next
-      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
+      case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2)
     qed
   qed
   show "(p + q) * r = p * r + q * r"
diff -r b6a945f205b7 -r 880b0e786c1b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon May 23 19:14:16 2005 +0200
+++ b/src/HOL/SetInterval.thy	Mon May 23 19:39:45 2005 +0200
@@ -555,26 +555,32 @@
 syntax
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
-  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
 syntax (xsymbols)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
-  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
 syntax (HTML output)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
-  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
 syntax (latex_sum output)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
 
 translations
   "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
   "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
+  "\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}"
   "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
 
 text{* The above introduces some pretty alternative syntaxes for
@@ -584,6 +590,7 @@
 Old & New & \LaTeX\\
 @{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\
 @{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\
+@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\
 @{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"}
 \end{tabular}
 \end{center}
@@ -615,6 +622,9 @@
 (* FIXME why are the following simp rules but the corresponding eqns
 on intervals are not? *)
 
+lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
+by (simp add:atMost_Suc add_ac)
+
 lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
 by (simp add:lessThan_Suc add_ac)