more syntax
authornipkow
Thu Jul 15 15:39:40 2004 +0200 (2004-07-15)
changeset 1504811b4dce71d73
parent 15047 fa62de5862b9
child 15049 82fb87151718
more syntax
src/HOL/NatArith.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/NatArith.thy	Thu Jul 15 15:32:32 2004 +0200
     1.2 +++ b/src/HOL/NatArith.thy	Thu Jul 15 15:39:40 2004 +0200
     1.3 @@ -36,22 +36,4 @@
     1.4  
     1.5  lemmas [arith_split] = nat_diff_split split_min split_max
     1.6  
     1.7 -(*
     1.8 -subsection {* Generic summation indexed over natural numbers *}
     1.9 -
    1.10 -consts
    1.11 -  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
    1.12 -primrec
    1.13 -  "Summation f 0 = 0"
    1.14 -  "Summation f (Suc n) = Summation f n + f n"
    1.15 -
    1.16 -syntax
    1.17 -  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.18 -translations
    1.19 -  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    1.20 -
    1.21 -theorem Summation_step:
    1.22 -    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    1.23 -  by (induct n) simp_all
    1.24 -*)
    1.25  end
     2.1 --- a/src/HOL/SetInterval.thy	Thu Jul 15 15:32:32 2004 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Thu Jul 15 15:39:40 2004 +0200
     2.3 @@ -50,6 +50,11 @@
     2.4    "{m..n(}" => "{m..<n}"
     2.5    "{)m..n}" => "{m<..n}"
     2.6  
     2.7 +
     2.8 +text{* A note of warning when using @{term"{..<n}"} on type @{typ
     2.9 +nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    2.10 +@{term"{m..<n}"} may not exist for in @{term"{..<n}"}-form as well. *}
    2.11 +
    2.12  syntax
    2.13    "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
    2.14    "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
    2.15 @@ -533,27 +538,32 @@
    2.16  subsection {* Summation indexed over intervals *}
    2.17  
    2.18  text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
    2.19 -@{term"\<Sum>x\<in>{a..b}. e"}. *}
    2.20 +@{term"\<Sum>x\<in>{a..b}. e"}, @{text"\<Sum>x=a..<b. e"} for
    2.21 +@{term"\<Sum>x\<in>{a..<b}. e"}, and @{text"\<Sum>x<b. e"} for @{term"\<Sum>x\<in>{..<b}. e"}.
    2.22 +
    2.23 +Note that for uniformity on @{typ nat} it is better to use
    2.24 +@{text"\<Sum>x=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
    2.25 +not provide all lemmas available for @{term"{m..<n}"} also in the
    2.26 +special form for @{term"{..<n}"}. *}
    2.27  
    2.28  syntax
    2.29    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
    2.30 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
    2.31 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
    2.32  syntax (xsymbols)
    2.33    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    2.34 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
    2.35 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
    2.36  syntax (HTML output)
    2.37    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    2.38 -
    2.39 -translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
    2.40 -
    2.41 -
    2.42 -subsection {* Summation up to *}
    2.43 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
    2.44 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
    2.45  
    2.46 -text{* Legacy, only used in HoareParallel and Isar-Examples. Really
    2.47 -needed? Probably better to replace it with above syntax. *}
    2.48 +translations
    2.49 +  "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
    2.50 +  "\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}"
    2.51 +  "\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}"
    2.52  
    2.53 -syntax
    2.54 -  "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    2.55 -translations
    2.56 -  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}"
    2.57  
    2.58  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    2.59  by (simp add:lessThan_Suc)