--- a/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 14 10:25:03 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 14 10:25:21 2004 +0200
@@ -487,7 +487,7 @@
text {* First some lemmas about summation properties. Summation is
defined in PreList. *}
-lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
+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)
@@ -505,13 +505,13 @@
done
lemma Example2_lemma2_aux2:
- "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+ "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<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< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+ "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< 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)