# HG changeset patch
# User kleing
# Date 1078114903 -3600
# Node ID b62323c85134777910a45c1994ba5cf4c7eb9758
# Parent  34ffa53db76ca68f3b2ea72ddafe5ceef1c53d83
union/intersection over intervals

diff -r 34ffa53db76c -r b62323c85134 NEWS
--- a/NEWS	Sun Feb 29 23:05:48 2004 +0100
+++ b/NEWS	Mon Mar 01 05:21:43 2004 +0100
@@ -129,6 +129,11 @@
   Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>.
   The subscript version is also accepted as input syntax.
 
+* Unions and Intersections over Intervals:
+  There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is 
+  also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" 
+  like in normal math, and corresponding versions for < and for intersection.
+
 * ML: the legacy theory structures Int and List have been removed. They had
   conflicted with ML Basis Library structures having the same names.
 
diff -r 34ffa53db76c -r b62323c85134 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Feb 29 23:05:48 2004 +0100
+++ b/src/HOL/SetInterval.thy	Mon Mar 01 05:21:43 2004 +0100
@@ -33,6 +33,31 @@
   atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
   "{l..u} == {l..} Int {..u}"
 
+syntax
+  "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
+  "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
+  "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
+  "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
+
+syntax (input)
+  "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
+  "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
+  "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 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>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
+  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10)
+  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
+  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10)
+
+translations
+  "UN i<=n. A"  == "UN i:{..n}. A"
+  "UN i<n. A"   == "UN i:{..n(}. A"
+  "INT i<=n. A" == "INT i:{..n}. A"
+  "INT i<n. A"  == "INT i:{..n(}. A"
+
+
 subsection {*lessThan*}
 
 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"