1.1 --- a/src/HOL/SetInterval.thy	Wed Feb 18 11:17:29 2009 +0000
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Feb 18 11:18:01 2009 +0000
     1.3 @@ -66,10 +66,10 @@
     1.4    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
     1.8 -  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
     1.9 -  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
    1.10 -  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
    1.11 +  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    1.12 +  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    1.13 +  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
    1.14 +  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
    1.15  
    1.16  translations
    1.17    "UN i<=n. A"  == "UN i:{..n}. A"
    1.18 @@ -946,4 +946,37 @@
    1.19    show ?case by simp
    1.20  qed
    1.21  
    1.22 +subsection {* Products indexed over intervals *}
    1.23 +
    1.24 +syntax
    1.25 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
    1.26 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
    1.27 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
    1.28 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
    1.29 +syntax (xsymbols)
    1.30 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
    1.31 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
    1.32 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
    1.33 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
    1.34 +syntax (HTML output)
    1.35 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
    1.36 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
    1.37 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
    1.38 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
    1.39 +syntax (latex_prod output)
    1.40 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.41 + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
    1.42 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.43 + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
    1.44 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.45 + ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
    1.46 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    1.47 + ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
    1.48 +
    1.49 +translations
    1.50 +  "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
    1.51 +  "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
    1.52 +  "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
    1.53 +  "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
    1.54 +
    1.55  end