--- a/src/HOL/Algebra/abstract/NatSum.ML Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/abstract/NatSum.ML Sat Feb 10 08:52:41 2001 +0100
@@ -6,18 +6,18 @@
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);
@@ -27,8 +27,8 @@
(* 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));
@@ -38,7 +38,7 @@
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);
@@ -47,7 +47,8 @@
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);
@@ -56,7 +57,7 @@
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);
@@ -64,7 +65,8 @@
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);
@@ -76,8 +78,8 @@
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);
@@ -93,14 +95,15 @@
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 *)
@@ -111,7 +114,9 @@
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";
@@ -120,7 +125,7 @@
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);
@@ -133,8 +138,8 @@
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);
@@ -148,23 +153,24 @@
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);
@@ -176,8 +182,8 @@
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";
@@ -186,8 +192,8 @@
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);
@@ -198,8 +204,8 @@
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";