# HG changeset patch
# User nipkow
# Date 1089793521 -7200
# Node ID b21fce6d146a4601e3d7e8c17175f33e305768d2
# Parent  fa7d27ef7e59224e18fcce134da5f56e7b0c007b
?

diff -r fa7d27ef7e59 -r b21fce6d146a src/HOL/HoareParallel/OG_Examples.thy
--- 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)
diff -r fa7d27ef7e59 -r b21fce6d146a src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Wed Jul 14 10:25:03 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Wed Jul 14 10:25:21 2004 +0200
@@ -187,7 +187,7 @@
 
 subsubsection {* Parameterized *}
 
-lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
+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)
@@ -204,13 +204,13 @@
 apply arith
 done 
 
-lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+lemma Example2_lemma2_aux2: "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)
@@ -225,10 +225,10 @@
 apply simp_all
 done
 
-lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< 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< n. b i)=(\<Sum>i< n. (b (j:=Suc 0)) i)"
 by(simp add:Example2_lemma2)
 
-lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i<n. b i)= n"
+lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i::nat<n. b i)= n"
 apply (induct n)
 apply auto
 done
diff -r fa7d27ef7e59 -r b21fce6d146a src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Wed Jul 14 10:25:03 2004 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Wed Jul 14 10:25:21 2004 +0200
@@ -31,7 +31,7 @@
 *}
 
 theorem sum_of_naturals:
-  "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+  "2 * (\<Sum>i::nat < n + 1. i) = n * (n + 1)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
@@ -86,7 +86,7 @@
 *}
 
 theorem sum_of_odds:
-  "(\<Sum>i < n. 2 * i + 1) = n^Suc (Suc 0)"
+  "(\<Sum>i::nat < n. 2 * i + 1) = n^Suc (Suc 0)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
@@ -106,7 +106,7 @@
 lemmas distrib = add_mult_distrib add_mult_distrib2
 
 theorem sum_of_squares:
-  "6 * (\<Sum>i < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
+  "6 * (\<Sum>i::nat < n + 1. 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 +119,7 @@
 qed
 
 theorem sum_of_cubes:
-  "4 * (\<Sum>i < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
+  "4 * (\<Sum>i::nat < n + 1. 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)