# HG changeset patch
# User nipkow
# Date 1089898780 -7200
# Node ID 11b4dce71d7377e8be0c192786e32c80936f7c2f
# Parent  fa62de5862b9910ebf650fbb4a5fa2df82f84dee
more syntax

diff -r fa62de5862b9 -r 11b4dce71d73 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Thu Jul 15 15:32:32 2004 +0200
+++ b/src/HOL/NatArith.thy	Thu Jul 15 15:39:40 2004 +0200
@@ -36,22 +36,4 @@
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-(*
-subsection {* Generic summation indexed over natural numbers *}
-
-consts
-  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
-primrec
-  "Summation f 0 = 0"
-  "Summation f (Suc n) = Summation f n + f n"
-
-syntax
-  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
-translations
-  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
-
-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 fa62de5862b9 -r 11b4dce71d73 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Jul 15 15:32:32 2004 +0200
+++ b/src/HOL/SetInterval.thy	Thu Jul 15 15:39:40 2004 +0200
@@ -50,6 +50,11 @@
   "{m..n(}" => "{m..<n}"
   "{)m..n}" => "{m<..n}"
 
+
+text{* A note of warning when using @{term"{..<n}"} on type @{typ
+nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
+@{term"{m..<n}"} may not exist for in @{term"{..<n}"}-form as well. *}
+
 syntax
   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
@@ -533,27 +538,32 @@
 subsection {* Summation indexed over intervals *}
 
 text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
-@{term"\<Sum>x\<in>{a..b}. e"}. *}
+@{term"\<Sum>x\<in>{a..b}. e"}, @{text"\<Sum>x=a..<b. e"} for
+@{term"\<Sum>x\<in>{a..<b}. e"}, and @{text"\<Sum>x<b. e"} for @{term"\<Sum>x\<in>{..<b}. e"}.
+
+Note that for uniformity on @{typ nat} it is better to use
+@{text"\<Sum>x=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
+not provide all lemmas available for @{term"{m..<n}"} also in the
+special form for @{term"{..<n}"}. *}
 
 syntax
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
 syntax (xsymbols)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
 syntax (HTML output)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
-
-translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
-
-
-subsection {* Summation up to *}
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
 
-text{* Legacy, only used in HoareParallel and Isar-Examples. Really
-needed? Probably better to replace it with above syntax. *}
+translations
+  "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
+  "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
+  "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
 
-syntax
-  "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
-translations
-  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}"
 
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)