10519

1 
(* Title: HOL/PreList.thy

8563

2 
ID: $Id$

10733

3 
Author: Tobias Nipkow and Markus Wenzel

8563

4 
Copyright 2000 TU Muenchen


5 


6 
A basis for building theory List on. Is defined separately to serve as a


7 
basis for theory ToyList in the documentation.


8 
*)

8490

9 


10 
theory PreList =

10212

11 
Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +

12020

12 
Relation_Power + SVC_Oracle:


13 


14 
(*belongs to theory Divides*)


15 
declare dvd_trans [trans]

8490

16 

10261

17 
(*belongs to theory Wellfounded_Recursion*)


18 
declare wf_induct [induct set: wf]

9066

19 

10671

20 

10680

21 
(* generic summation indexed over nat *)


22 

10671

23 
consts

11803

24 
Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"

10671

25 
primrec


26 
"Summation f 0 = 0"


27 
"Summation f (Suc n) = Summation f n + f n"


28 


29 
syntax


30 
"_Summation" :: "idt => nat => 'a => nat" ("\<Sum>_<_. _" [0, 51, 10] 10)


31 
translations


32 
"\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"


33 


34 
theorem Summation_step:


35 
"0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n  1. f i) + f (n  1)"


36 
by (induct n) simp_all


37 

8490

38 
end
