added Summation;
authorwenzelm
Thu Dec 14 19:36:48 2000 +0100 (2000-12-14)
changeset 10671ac6b3b671198
parent 10670 4b0e346c8ca3
child 10672 3b1c2d74a01b
added Summation;
src/HOL/PreList.thy
     1.1 --- a/src/HOL/PreList.thy	Thu Dec 14 10:30:45 2000 +0100
     1.2 +++ b/src/HOL/PreList.thy	Thu Dec 14 19:36:48 2000 +0100
     1.3 @@ -20,4 +20,21 @@
     1.4  (*belongs to theory Datatype_Universe; hides popular names *)
     1.5  hide const Node Atom Leaf Numb Lim Funs Split Case
     1.6  
     1.7 +
     1.8 +(*belongs to theory Nat, but requires Datatype*)
     1.9 +consts
    1.10 +  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
    1.11 +primrec
    1.12 +  "Summation f 0 = 0"
    1.13 +  "Summation f (Suc n) = Summation f n + f n"
    1.14 +
    1.15 +syntax
    1.16 +  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.17 +translations
    1.18 +  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    1.19 +
    1.20 +theorem Summation_step:
    1.21 +    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    1.22 +  by (induct n) simp_all
    1.23 +
    1.24  end