# HG changeset patch
# User wenzelm
# Date 976819008 -3600
# Node ID ac6b3b6711989a69ebffc86ef32ceb93483c498b
# Parent  4b0e346c8ca365e1415b2e790c0117577c7c44f6
added Summation;

diff -r 4b0e346c8ca3 -r ac6b3b671198 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Thu Dec 14 10:30:45 2000 +0100
+++ b/src/HOL/PreList.thy	Thu Dec 14 19:36:48 2000 +0100
@@ -20,4 +20,21 @@
 (*belongs to theory Datatype_Universe; hides popular names *)
 hide const Node Atom Leaf Numb Lim Funs Split Case
 
+
+(*belongs to theory Nat, but requires Datatype*)
+consts
+  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
+primrec
+  "Summation f 0 = 0"
+  "Summation f (Suc n) = Summation f n + f n"
+
+syntax
+  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
+translations
+  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
+
+theorem Summation_step:
+    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
+  by (induct n) simp_all
+
 end