--- 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