51 "{)m..n}" => "{m<..n}" |
51 "{)m..n}" => "{m<..n}" |
52 |
52 |
53 |
53 |
54 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
54 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
55 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
55 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
56 @{term"{m..<n}"} may not exist for in @{term"{..<n}"}-form as well. *} |
56 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
57 |
57 |
58 syntax |
58 syntax |
59 "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
59 "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
60 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
60 "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
61 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
61 "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
535 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
535 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
536 |
536 |
537 |
537 |
538 subsection {* Summation indexed over intervals *} |
538 subsection {* Summation indexed over intervals *} |
539 |
539 |
540 text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for |
|
541 @{term"\<Sum>x\<in>{a..b}. e"}, @{text"\<Sum>x=a..<b. e"} for |
|
542 @{term"\<Sum>x\<in>{a..<b}. e"}, and @{text"\<Sum>x<b. e"} for @{term"\<Sum>x\<in>{..<b}. e"}. |
|
543 |
|
544 Note that for uniformity on @{typ nat} it is better to use |
|
545 @{text"\<Sum>x=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may |
|
546 not provide all lemmas available for @{term"{m..<n}"} also in the |
|
547 special form for @{term"{..<n}"}. *} |
|
548 |
|
549 syntax |
540 syntax |
550 "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) |
541 "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) |
551 "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) |
542 "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) |
552 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) |
543 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) |
553 syntax (xsymbols) |
544 syntax (xsymbols) |
556 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
547 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
557 syntax (HTML output) |
548 syntax (HTML output) |
558 "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
549 "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
559 "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
550 "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
560 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
551 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
|
552 syntax (latex output) |
|
553 "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
554 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
555 "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
556 ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
557 "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
558 ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) |
561 |
559 |
562 translations |
560 translations |
563 "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" |
561 "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" |
564 "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" |
562 "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" |
565 "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}" |
563 "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}" |
566 |
564 |
|
565 text{* The above introduces some pretty alternative syntaxes for |
|
566 summation over intervals as shown on the left-hand side: |
|
567 \begin{center} |
|
568 \begin{tabular}{lll} |
|
569 Sets & Indexed & TeX\\ |
|
570 @{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term[source]"\<Sum>x=a..b. e"} & @{term"\<Sum>x=a..b. e"}\\ |
|
571 @{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term[source]"\<Sum>x=a..<b. e"} & @{term"\<Sum>x=a..<b. e"}\\ |
|
572 @{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term[source]"\<Sum>x<b. e"} & @{term"\<Sum>x<b. e"} |
|
573 \end{tabular} |
|
574 \end{center} |
|
575 |
|
576 Note that for uniformity on @{typ nat} it is better to use |
|
577 @{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may |
|
578 not provide all lemmas available for @{term"{m..<n}"} also in the |
|
579 special form for @{term"{..<n}"}. *} |
|
580 |
567 |
581 |
568 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)" |
582 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)" |
569 by (simp add:lessThan_Suc) |
583 by (simp add:lessThan_Suc) |
570 |
584 |
571 end |
585 end |