# HG changeset patch # User paulson # Date 1234955881 0 # Node ID 9d5c6f376768cd377f011507e2caa560a8b7b4bc # Parent 50271a1b79c8d203bf4219cf1cf9edc916205912 Syntactic support for products over set intervals diff -r 50271a1b79c8 -r 9d5c6f376768 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Wed Feb 18 11:17:29 2009 +0000 +++ b/src/HOL/SetInterval.thy Wed Feb 18 11:18:01 2009 +0000 @@ -66,10 +66,10 @@ "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) syntax (xsymbols) - "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) - "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) - "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) - "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) + "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) + "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) translations "UN i<=n. A" == "UN i:{..n}. A" @@ -946,4 +946,37 @@ show ?case by simp qed +subsection {* Products indexed over intervals *} + +syntax + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) +syntax (xsymbols) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax (HTML output) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax (latex_prod output) + "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) + "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) + "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) + "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" + ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) + +translations + "\x=a..b. t" == "CONST setprod (%x. t) {a..b}" + "\x=a..i\n. t" == "CONST setprod (\i. t) {..n}" + "\ii. t) {..