added {0::nat..n(} = {..n(}
authornipkow
Wed Jul 14 10:25:03 2004 +0200 (2004-07-14)
changeset 15042fa7d27ef7e59
parent 15041 a6b1f0cef7b3
child 15043 b21fce6d146a
added {0::nat..n(} = {..n(}
src/HOL/Finite_Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 13 12:32:01 2004 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jul 14 10:25:03 2004 +0200
     1.3 @@ -761,6 +761,9 @@
     1.4    setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
     1.5    "setsum f A == if finite A then fold (op + o f) 0 A else 0"
     1.6  
     1.7 +text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
     1.8 +written @{text"\<Sum>x\<in>A. e"}. *}
     1.9 +
    1.10  syntax
    1.11    "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
    1.12  syntax (xsymbols)
    1.13 @@ -770,6 +773,34 @@
    1.14  translations
    1.15    "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
    1.16  
    1.17 +text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
    1.18 + @{text"\<Sum>x|P. e"}. *}
    1.19 +
    1.20 +syntax
    1.21 +  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ | / _./ _)" [0,0,10] 10)
    1.22 +syntax (xsymbols)
    1.23 +  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.24 +syntax (HTML output)
    1.25 +  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.26 +
    1.27 +translations "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
    1.28 +
    1.29 +print_translation {*
    1.30 +let
    1.31 +  fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
    1.32 +    (if x<>y then raise Match
    1.33 +     else let val x' = Syntax.mark_bound x
    1.34 +              val t' = subst_bound(x',t)
    1.35 +              val P' = subst_bound(x',P)
    1.36 +          in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end)
    1.37 +in
    1.38 +[("setsum", setsum_tr')]
    1.39 +end
    1.40 +*}
    1.41 +
    1.42 +text{* As Jeremy Avigad notes: ultimately the analogous
    1.43 +   thing should be done for setprod as well \dots *}
    1.44 +
    1.45  
    1.46  lemma setsum_empty [simp]: "setsum f {} = 0"
    1.47    by (simp add: setsum_def)
     2.1 --- a/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Wed Jul 14 10:25:03 2004 +0200
     2.3 @@ -229,6 +229,9 @@
     2.4  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
     2.5  by blast
     2.6  
     2.7 +lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
     2.8 +by(simp add:lessThan_def atLeastLessThan_def)
     2.9 +
    2.10  text {* Intervals of nats with @{text Suc} *}
    2.11  
    2.12  lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
    2.13 @@ -478,16 +481,30 @@
    2.14  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
    2.15  
    2.16  
    2.17 -subsection {* Summation indexed over natural numbers *}
    2.18 +subsection {* Summation indexed over intervals *}
    2.19 +
    2.20 +text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
    2.21 +@{term"\<Sum>x\<in>{a..b}. e"}. *}
    2.22 +
    2.23 +syntax
    2.24 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
    2.25 +syntax (xsymbols)
    2.26 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    2.27 +syntax (HTML output)
    2.28 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    2.29 +
    2.30 +translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
    2.31 +
    2.32 +
    2.33 +subsection {* Summation up to *}
    2.34  
    2.35  text{* Legacy, only used in HoareParallel and Isar-Examples. Really
    2.36 -needed? Probably better to replace it with a more generic operator
    2.37 -like ``SUM i = m..n. b''. *}
    2.38 +needed? Probably better to replace it with above syntax. *}
    2.39  
    2.40  syntax
    2.41 -  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    2.42 +  "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    2.43  translations
    2.44 -  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
    2.45 +  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
    2.46  
    2.47  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    2.48  by (simp add:lessThan_Suc)