# HG changeset patch
# User nipkow
# Date 1089714721 -7200
# Node ID a6b1f0cef7b33097534d03781473e67d0a6fc101
# Parent  ed574b4f7e7058e6e6ac8fdbeaa13a1e76de551d
Got rid of Summation and made it a translation into setsum instead.

diff -r ed574b4f7e70 -r a6b1f0cef7b3 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -507,16 +507,16 @@
 lemma Example2_lemma2_aux2: 
   "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
 apply(induct j)
- apply simp_all
+ apply (simp_all cong:setsum_cong)
 done
 
 lemma Example2_lemma2: 
  "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac  t="Summation (b(j := (Suc 0))) n" in ssubst)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="Summation b n" in ssubst)
-apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+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(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
@@ -548,7 +548,6 @@
 apply simp_all
 apply (tactic {* ALLGOALS Clarify_tac *})
 apply simp_all
-    apply(force elim:Example2_lemma1)
    apply(erule Example2_lemma2)
    apply simp
   apply(erule Example2_lemma2)
diff -r ed574b4f7e70 -r a6b1f0cef7b3 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -206,21 +206,22 @@
 
 lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
 apply(induct j)
- apply simp_all
+ apply (simp_all cong:setsum_cong)
 done
 
-lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
-apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
-apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
+lemma Example2_lemma2: 
+ "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< 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(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="Summation b n" in ssubst)
-apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
- apply(rotate_tac -1)
- apply(erule ssubst)
- apply(subgoal_tac "j\<le>j")
-  apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
-  apply(rotate_tac -1)
-  apply(erule ssubst)
+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(rotate_tac -1)
+apply(erule ssubst)
+apply(subgoal_tac "j\<le>j")
+ apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
+apply(rotate_tac -1)
+apply(erule ssubst)
 apply simp_all
 done
 
diff -r ed574b4f7e70 -r a6b1f0cef7b3 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/NatArith.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -36,7 +36,7 @@
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-
+(*
 subsection {* Generic summation indexed over natural numbers *}
 
 consts
@@ -53,5 +53,5 @@
 theorem Summation_step:
     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
   by (induct n) simp_all
-
+*)
 end
diff -r ed574b4f7e70 -r a6b1f0cef7b3 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -477,4 +477,19 @@
 
 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
 
+
+subsection {* Summation indexed over natural numbers *}
+
+text{* Legacy, only used in HoareParallel and Isar-Examples. Really
+needed? Probably better to replace it with a more generic operator
+like ``SUM i = m..n. b''. *}
+
+syntax
+  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
+translations
+  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
+
+lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
+by (simp add:lessThan_Suc)
+
 end