diff -r 179ff9cb160b -r 5b25fee0362c src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/SetInterval.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -66,10 +66,10 @@
   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
 
 syntax (xsymbols)
-  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
-  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
-  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
-  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
+  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
+  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
+  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
+  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
 
 translations
   "UN i<=n. A"  == "UN i:{..n}. A"
@@ -352,11 +352,11 @@
 
 corollary image_Suc_atLeastAtMost[simp]:
   "Suc ` {i..j} = {Suc i..Suc j}"
-using image_add_atLeastAtMost[where k=1] by simp
+using image_add_atLeastAtMost[where k="Suc 0"] by simp
 
 corollary image_Suc_atLeastLessThan[simp]:
   "Suc ` {i..<j} = {Suc i..<Suc j}"
-using image_add_atLeastLessThan[where k=1] by simp
+using image_add_atLeastLessThan[where k="Suc 0"] by simp
 
 lemma image_add_int_atLeastLessThan:
     "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
@@ -556,7 +556,7 @@
 qed
 
 lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
-apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"])
+apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
 apply simp
 apply fastsimp
 apply auto
@@ -803,7 +803,7 @@
 
 lemma setsum_head_upt_Suc:
   "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
-apply(insert setsum_head_Suc[of m "n - 1" f])
+apply(insert setsum_head_Suc[of m "n - Suc 0" f])
 apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
 done
 
@@ -835,11 +835,11 @@
 
 corollary setsum_shift_bounds_cl_Suc_ivl:
   "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
-by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
 
 corollary setsum_shift_bounds_Suc_ivl:
   "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
-by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
 
 lemma setsum_shift_lb_Suc0_0:
   "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
@@ -883,6 +883,7 @@
     by (rule setsum_addf)
   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
+    unfolding One_nat_def
     by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
   also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
     by (simp add: left_distrib right_distrib)
@@ -890,7 +891,7 @@
     by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   also from ngt1
   have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
-    by (simp only: mult_ac gauss_sum [of "n - 1"])
+    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
        (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
   finally show ?thesis by (simp add: algebra_simps)
 next
@@ -906,7 +907,8 @@
     "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
     of_nat(n) * (a + (a + of_nat(n - 1)*d))"
     by (rule arith_series_general)
-  thus ?thesis by (auto simp add: of_nat_id)
+  thus ?thesis
+    unfolding One_nat_def by (auto simp add: of_nat_id)
 qed
 
 lemma arith_series_int:
@@ -946,4 +948,37 @@
   show ?case by simp
 qed
 
+subsection {* Products indexed over intervals *}
+
+syntax
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
+syntax (xsymbols)
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax (HTML output)
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax (latex_prod output)
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+
+translations
+  "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
+  "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
+  "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
+  "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
+
 end