src/HOL/Algebra/abstract/NatSum.ML

     Author: Clemens Ballarin, started 12 December 1996
 *)
 
 section "Basic Properties";
 
-Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
+Goal "setsum f {..0::nat} = (f 0::'a::ring)";
 by (Asm_simp_tac 1);
 qed "SUM_0";
 
-Goalw [SUM_def]
-  "SUM (Suc n) f = (f (Suc n) + SUM n f::'a::ring)";
-by (Simp_tac 1);
+Goal "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::ring)";
+by (simp_tac (simpset() addsimps [atMost_Suc]) 1);
 qed "SUM_Suc";
 
 Addsimps [SUM_0, SUM_Suc];
 
-Goal "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
+Goal
+  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::ring)";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);
 qed "SUM_Suc2";
 
 (* Congruence rules *)
 
-Goal "ALL j'. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
-\     --> SUM j f = SUM j' f'";
+Goal "ALL j'::nat. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \
+\     --> setsum f {..j} = setsum f' {..j'}";
 by (induct_tac "j" 1);
 by Auto_tac;  
 bind_thm ("SUM_cong", (impI RS allI) RSN (2, result() RS spec RS mp RS mp));
 Addcongs [SUM_cong];
 
 (* Results needed for the development of polynomials *)
 
 section "Ring Properties";
 
-Goal "SUM n (%i. <0>) = (<0>::'a::ring)";
+Goal "setsum (%i. 0) {..n::nat} = (0::'a::ring)";
 by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "SUM_zero";
 
 Addsimps [SUM_zero];
 
 Goal
-  "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";
+  "!!f::nat=>'a::ring. \
+\  setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (asm_simp_tac (simpset() addsimps a_ac) 1);
 qed "SUM_add";
 
 Goal
-  "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";
+  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
 qed "SUM_ldistr";
 
-Goal "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
+Goal
+  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (asm_simp_tac (simpset() addsimps [r_distr]) 1);

 
 section "Results for the Construction of Polynomials";
 
 Goal
   "!!a::nat=>'a::ring. k <= n --> \
-\  SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
-\  SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";
+\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = \
+\  setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}";
 by (induct_tac "k" 1);
 (* Base case *)
 by (simp_tac (simpset() addsimps [m_assoc]) 1);
 (* Induction step *)
 by (rtac impI 1);

 by (asm_simp_tac (simpset() addsimps a_ac@ [SUM_ldistr, m_assoc]) 1);
 qed_spec_mp "poly_assoc_lemma1";
 
 Goal
   "!!a::nat=>'a::ring. \
-\  SUM n (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
-\  SUM n (%j. a j * SUM (n-j) (%i. b i * c (n-(j+i))))";
+\  setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..n} = \
+\  setsum (%j. a j * setsum (%i. b i * c (n-(j+i))) {..n-j}) {..n}";
 by (asm_simp_tac (simpset() addsimps [poly_assoc_lemma1]) 1);
 qed "poly_assoc_lemma";
 
 Goal
   "!! a::nat=>'a::ring. j <= n --> \
-\    SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
+\    setsum (%i. a i * b (n-i)) {..j} = \
+\    setsum (%i. a (n-i-(n-j)) * b (i+(n-j))) {..j}";
 by (Simp_tac 1); 
 by (induct_tac "j" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (stac SUM_Suc2 1);
 by (asm_simp_tac (simpset() addsimps [a_comm]) 1);
 qed "poly_comm_lemma1";
 
 Goal
- "!!a::nat=>'a::ring. SUM n (%i. a i * b (n-i)) = SUM n (%i. a (n-i) * b i)";
+ "!!a::nat=>'a::ring. \
+\   setsum (%i. a i * b (n-i)) {..n} = \
+\   setsum (%i. a (n-i) * b i) {..n}";
 by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);
 by (Asm_full_simp_tac 1);
 qed "poly_comm_lemma";
 
 section "Changing the Range of Summation";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
+\   setsum (%i. if i = x then f i else 0) {..n} = (if x <= n then f x else 0)";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (Asm_simp_tac 1);

 by (arith_tac 1);
 qed "SUM_if_singleton";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \
-\    SUM m f = SUM n f";
+\    m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
+\    setsum f {..m} = setsum f {..n}";
 by (induct_tac "n" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (case_tac "m <= n" 1);

 by (fast_arith_tac 1);
 val SUM_shrink_lemma = result();
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM n f) |] ==> \
-\      P (SUM m f)";
+\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
+\  ==> P (setsum f {..m})";
 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
 by (Asm_full_simp_tac 1);
 qed "SUM_shrink";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM m f) |] ==> \
-\      P (SUM n f)";
+\    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
+\    ==> P (setsum f {..n})";
 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
 by (Asm_full_simp_tac 1);
 qed "SUM_extend";
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";
+\    (ALL i. i < m --> f i = 0) --> \
+\      setsum (%i. f (i+m)) {..d} = setsum f {..m+d}";
 by (induct_tac "d" 1);
 (* Base case *)
 by (induct_tac "m" 1);
 by (Simp_tac 1);
 by (Force_tac 1);

 by (asm_simp_tac (simpset() addsimps add_ac) 1);
 val SUM_shrink_below_lemma = result();
 
 Goal
   "!! f::(nat=>'a::ring). \
-\    [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \
-\    P (SUM n f)";
+\    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
+\    ==> P (setsum f {..n})";
 by (asm_full_simp_tac 
     (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
 qed "SUM_extend_below";
 
 section "Result for the Univeral Property of Polynomials";
 
 Goal
   "!!f::nat=>'a::ring. j <= n + m --> \
-\    SUM j (%k. SUM k (%i. f i * g (k - i))) = \
-\    SUM j (%k. SUM (j - k) (%i. f k * g i))";
+\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
+\    setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
 by (induct_tac "j" 1);
 (* Base case *)
 by (Simp_tac 1);
 (* Induction step *)
 by (simp_tac (simpset() addsimps [Suc_diff_le, SUM_add]) 1);
 by (asm_simp_tac (simpset() addsimps a_ac) 1);
 val DiagSum_lemma = result();
 
 Goal
   "!!f::nat=>'a::ring. \
-\    SUM (n + m) (%k. SUM k (%i. f i * g (k - i))) = \
-\    SUM (n + m) (%k. SUM (n + m - k) (%i. f k * g i))";
+\    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
+\    setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
 by (rtac (DiagSum_lemma RS mp) 1);
 by (rtac le_refl 1);
 qed "DiagSum";