--- 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