# 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" ("\_<_. _" [0, 51, 10] 10) +translations + "\i < n. b" == "Summation (\i. b) n" + +theorem Summation_step: + "0 < n ==> (\i < n. f i) = (\i < n - 1. f i) + f (n - 1)" + by (induct n) simp_all + end