--- a/src/HOL/HoareParallel/OG_Examples.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/HoareParallel/OG_Examples.thy Wed Mar 02 12:06:15 2005 +0100
@@ -484,17 +484,19 @@
subsubsection {* Increment a Variable in Parallel *}
-text {* First some lemmas about summation properties. Summation is
-defined in PreList. *}
+declare setsum_op_ivl_Suc [simp]
+text {* First some lemmas about summation properties. *}
+(*
lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
apply(induct n)
apply simp_all
apply(force simp add: less_Suc_eq)
done
-
+*)
lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow>
- (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
+ (\<Sum>i=0..<n. (b i::nat)) =
+ (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
apply(induct n)
apply simp_all
apply(simp add:less_Suc_eq)
@@ -505,18 +507,18 @@
done
lemma Example2_lemma2_aux2:
- "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+ "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
apply(induct j)
apply (simp_all cong:setsum_cong)
done
lemma Example2_lemma2:
- "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+ "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
+apply(erule_tac t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac t="setsum b {..<n}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac t="setsum b {0..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j\<le>j")
@@ -526,7 +528,7 @@
apply simp_all
done
-lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
+lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
apply (induct n)
apply auto
done
@@ -536,12 +538,12 @@
x :: nat
lemma Example_2: "0<n \<Longrightarrow>
- \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i< n. \<acute>c i)=0}.
+ \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.
COBEGIN
SCHEME [0\<le>i<n]
- .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=0}.
+ .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}.
\<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
- .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
+ .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
COEND
.{\<acute>x=n}."
apply oghoare
--- a/src/HOL/HoareParallel/RG_Examples.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/HoareParallel/RG_Examples.thy Wed Mar 02 12:06:15 2005 +0100
@@ -154,14 +154,11 @@
subsubsection {* Parameterized *}
-lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
-apply(induct n)
- apply simp_all
-apply(force simp add: less_Suc_eq)
-done
+declare setsum_op_ivl_Suc [simp]
-lemma Example2_lemma2_aux:
- "j<n \<Longrightarrow> (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
+lemma Example2_lemma2_aux: "j<n \<Longrightarrow>
+ (\<Sum>i=0..<n. (b i::nat)) =
+ (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
apply(induct n)
apply simp_all
apply(simp add:less_Suc_eq)
@@ -169,20 +166,21 @@
apply(subgoal_tac "n - j = Suc(n- Suc j)")
apply simp
apply arith
-done
+done
-lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+lemma Example2_lemma2_aux2:
+ "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
apply(induct j)
apply (simp_all cong:setsum_cong)
done
lemma Example2_lemma2:
- "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+ "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
+apply(erule_tac t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac t="setsum b {..<n}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac t="setsum b {0..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j\<le>j")
@@ -192,14 +190,10 @@
apply simp_all
done
-lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j:=Suc 0)) i)"
+lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
+ Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
by(simp add:Example2_lemma2)
-lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i::nat<n. b i)= n"
-apply (induct n)
-apply auto
-done
-
record Example2_parameterized =
C :: "nat \<Rightarrow> nat"
y :: nat
@@ -207,21 +201,21 @@
lemma Example2_parameterized: "0<n \<Longrightarrow>
\<turnstile> COBEGIN SCHEME [0\<le>i<n]
(\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>,
- \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
+ \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
\<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and>
- (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
+ (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and>
- (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
- \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
+ (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
+ \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
COEND
- SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
+ SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i=0..<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
apply(rule Parallel)
apply force
apply force
-apply(force elim:Example2_lemma1)
+apply(force)
apply clarify
apply simp
-apply(force intro:Example2_lemma3)
+apply(simp cong:setsum_ivl_cong)
apply clarify
apply simp
apply(rule Await)
--- a/src/HOL/Hyperreal/MacLaurin.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Mar 02 12:06:15 2005 +0100
@@ -99,9 +99,9 @@
prefer 3 apply (simp add: fact_diff_Suc)
prefer 2 apply simp
apply (frule_tac m = m in less_add_one, clarify)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (rule lemma_DERIV_subst)
apply (rule DERIV_add)
apply (rule_tac [2] DERIV_const)
@@ -157,9 +157,9 @@
apply (erule exE)
apply (subgoal_tac "g 0 = 0 & g h =0")
prefer 2
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
apply (cut_tac n = m and k = 1 in sumr_offset2)
- apply (simp add: eq_diff_eq' del: setsum_Suc)
+ apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
prefer 2 apply blast
apply (erule exE)
@@ -178,9 +178,9 @@
apply clarify
apply simp
apply (frule_tac m = ma in less_add_one, clarify)
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
apply (rule allI, rule impI)
apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
@@ -515,7 +515,7 @@
apply (simp (no_asm))
apply (simp (no_asm))
apply (case_tac "n", simp)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
--- a/src/HOL/Hyperreal/Series.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy Wed Mar 02 12:06:15 2005 +0100
@@ -11,10 +11,9 @@
theory Series
imports SEQ Lim
begin
-thm atLeastLessThan_empty
-(* FIXME why not globally? *)
-declare atLeastLessThan_empty[simp];
+
declare atLeastLessThan_iff[iff]
+declare setsum_op_ivl_Suc[simp]
constdefs
sums :: "(nat => real) => real => bool" (infixr "sums" 80)
@@ -31,9 +30,6 @@
translations
"\<Sum>i. b" == "suminf (%i. b)"
-lemma setsum_Suc[simp]:
- "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
-by (simp add: atLeastLessThanSuc add_commute)
lemma sumr_diff_mult_const:
"setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Mar 02 12:06:15 2005 +0100
@@ -360,7 +360,7 @@
lemma lemma_realpow_diff_sumr:
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =
y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
-apply (auto simp add: setsum_mult simp del: setsum_Suc)
+apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc)
apply (rule setsum_cong[OF refl])
apply (subst lemma_realpow_diff)
apply (auto simp add: mult_ac)
@@ -370,21 +370,21 @@
"x ^ (Suc n) - y ^ (Suc n) =
(x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
apply (induct "n", simp)
-apply (auto simp del: setsum_Suc)
-apply (subst setsum_Suc)
+apply (auto simp del: setsum_op_ivl_Suc)
+apply (subst setsum_op_ivl_Suc)
apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
+apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc)
done
lemma lemma_realpow_rev_sumr:
"(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
(\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
apply (case_tac "x = y")
-apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
+apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc)
apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
apply (rule_tac [2] minus_minus [THEN subst], simp)
apply (subst minus_mult_left)
-apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
+apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc)
done
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
@@ -490,14 +490,14 @@
apply (case_tac "n")
apply (auto simp add: lemma_realpow_diff_sumr2
right_diff_distrib [symmetric] mult_assoc
- simp del: realpow_Suc setsum_Suc)
-apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc)
+ simp del: realpow_Suc setsum_op_ivl_Suc)
+apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_op_ivl_Suc)
apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib
sumdiff lemma_termdiff1 setsum_mult)
apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
- del: setsum_Suc realpow_Suc)
+ del: setsum_op_ivl_Suc realpow_Suc)
done
lemma lemma_termdiff3:
@@ -517,13 +517,13 @@
apply clarify
apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
K ^ p * (real (Suc (Suc (p + d))) * K ^ d)")
-apply (simp (no_asm_simp) add: power_add del: setsum_Suc)
-apply (auto intro!: mult_mono simp del: setsum_Suc)
-apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc)
+apply (simp (no_asm_simp) add: power_add del: setsum_op_ivl_Suc)
+apply (auto intro!: mult_mono simp del: setsum_op_ivl_Suc)
+apply (auto intro!: power_mono simp add: power_abs simp del: setsum_op_ivl_Suc)
apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
apply (subgoal_tac [2] "0 \<le> K")
apply (drule_tac [2] n = d in zero_le_power)
-apply (auto simp del: setsum_Suc)
+apply (auto simp del: setsum_op_ivl_Suc)
apply (rule setsum_abs [THEN real_le_trans])
apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
@@ -1412,7 +1412,7 @@
"\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
in order_less_trans)
apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
-apply (simp (no_asm) add: mult_assoc del: setsum_Suc)
+apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
--- a/src/HOL/Isar_examples/Summation.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Isar_examples/Summation.thy Wed Mar 02 12:06:15 2005 +0100
@@ -5,7 +5,11 @@
header {* Summing natural numbers *}
-theory Summation = Main:
+theory Summation
+imports Main
+begin
+
+declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp]
text_raw {*
\footnote{This example is somewhat reminiscent of the
@@ -31,7 +35,7 @@
*}
theorem sum_of_naturals:
- "2 * (\<Sum>i::nat < n + 1. i) = n * (n + 1)"
+ "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -86,7 +90,7 @@
*}
theorem sum_of_odds:
- "(\<Sum>i::nat < n. 2 * i + 1) = n^Suc (Suc 0)"
+ "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -106,7 +110,7 @@
lemmas distrib = add_mult_distrib add_mult_distrib2
theorem sum_of_squares:
- "6 * (\<Sum>i::nat < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
+ "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -119,7 +123,7 @@
qed
theorem sum_of_cubes:
- "4 * (\<Sum>i::nat < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
+ "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by (simp add: power_eq_if)
--- a/src/HOL/SetInterval.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/SetInterval.thy Wed Mar 02 12:06:15 2005 +0100
@@ -392,7 +392,7 @@
lemma image_atLeastLessThan_int_shift:
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
- apply (auto simp add: image_def atLeastLessThan_iff)
+ apply (auto simp add: image_def)
apply (rule_tac x = "x - l" in bexI)
apply auto
done
@@ -612,15 +612,23 @@
setsum f {a..<b} = setsum g {c..<d}"
by(rule setsum_cong, simp_all)
-lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
- (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
-
(* FIXME delete
lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
by (simp add:lessThan_Suc)
*)
+lemma setsum_cl_ivl_Suc:
+ "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
+by (auto simp:add_ac atLeastAtMostSuc_conv)
+
+lemma setsum_op_ivl_Suc:
+ "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
+by (auto simp:add_ac atLeastLessThanSuc)
+
+lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
+ (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
+by (auto simp:add_ac atLeastAtMostSuc_conv)
+
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
--- a/src/HOL/ex/NatSum.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/ex/NatSum.thy Wed Mar 02 12:06:15 2005 +0100
@@ -17,16 +17,18 @@
\url{http://www.research.att.com/~njas/sequences/}.
*}
-lemmas [simp] = lessThan_Suc atMost_Suc left_distrib right_distrib
- left_diff_distrib right_diff_distrib --{*for true subtraction*}
- diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
+lemmas [simp] =
+ lessThan_Suc atMost_Suc setsum_op_ivl_Suc setsum_cl_ivl_Suc
+ left_distrib right_distrib
+ left_diff_distrib right_diff_distrib --{*for true subtraction*}
+ diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
text {*
\medskip The sum of the first @{text n} odd numbers equals @{text n}
squared.
*}
-lemma sum_of_odds: "(\<Sum>i \<in> {..<n}. Suc (i + i)) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {0..<n}. Suc (i + i)) = n * n"
apply (induct n)
apply auto
done
@@ -37,8 +39,7 @@
*}
lemma sum_of_odd_squares:
- "3 * (\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i)) =
- n * (4 * n * n - 1)"
+ "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
apply (induct n)
apply (auto split: nat_diff_split) (*eliminate the subtraction*)
done
@@ -48,10 +49,10 @@
\medskip The sum of the first @{text n} odd cubes
*}
-lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by (auto );
+lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by auto
lemma sum_of_odd_cubes:
- "(\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
+ "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
n * n * (2 * n * n - 1)"
apply (induct n)
apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -62,30 +63,30 @@
@{text "n (n + 1) / 2"}.*}
lemma sum_of_naturals:
- "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
+ "2 * (\<Sum>i=0..n. i) = n * Suc n"
apply (induct n)
apply auto
done
lemma sum_of_squares:
- "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
+ "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
apply (induct n)
apply auto
done
lemma sum_of_cubes:
- "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
+ "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
apply (induct n)
apply auto
done
text {*
- \medskip Sum of fourth powers: two versions.
+ \medskip Sum of fourth powers: three versions.
*}
lemma sum_of_fourth_powers:
- "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
+ "30 * (\<Sum>i=0..n. i * i * i * i) =
n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
apply (induct n)
apply simp_all
@@ -94,11 +95,19 @@
done
text {*
- Alternative proof, with a change of variables and much more
+ Tow alternative proofs, with a change of variables and much more
subtraction, performed using the integers. *}
lemma int_sum_of_fourth_powers:
- "30 * of_nat (\<Sum>i \<in> {..<m}. i * i * i * i) =
+ "30 * int (\<Sum>i=0..<m. i * i * i * i) =
+ int m * (int m - 1) * (int(2 * m) - 1) *
+ (int(3 * m * m) - int(3 * m) - 1)"
+ apply (induct m)
+ apply (simp_all add:zmult_int[symmetric])
+ done
+
+lemma of_nat_sum_of_fourth_powers:
+ "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
(of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
apply (induct m)
@@ -111,17 +120,17 @@
general case.
*}
-lemma sum_of_2_powers: "(\<Sum>i \<in> {..<n}. 2^i) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
apply (induct n)
apply (auto split: nat_diff_split)
done
-lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..<n}. 3^i) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
apply (induct n)
apply auto
done
-lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..<n}. k^i) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
apply (induct n)
apply auto
done