nipkow@10519: (*  Title:      HOL/PreList.thy
nipkow@8563:     ID:         $Id$
nipkow@8563:     Author:     Tobias Nipkow
nipkow@8563:     Copyright   2000 TU Muenchen
nipkow@8563: 
nipkow@8563: A basis for building theory List on. Is defined separately to serve as a
nipkow@8563: basis for theory ToyList in the documentation.
nipkow@8563: *)
wenzelm@8490: 
wenzelm@8490: theory PreList =
nipkow@10212:   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
wenzelm@10261:   Relation_Power + Calculation + SVC_Oracle:
wenzelm@8490: 
wenzelm@10261: (*belongs to theory HOL*)
wenzelm@10261: declare case_split [cases type: bool]
wenzelm@10261: 
wenzelm@10261: (*belongs to theory Wellfounded_Recursion*)
wenzelm@10261: declare wf_induct [induct set: wf]
wenzelm@9066: 
nipkow@10519: (*belongs to theory Datatype_Universe; hides popular names *)
nipkow@10519: hide const Node Atom Leaf Numb Lim Funs Split Case
nipkow@10519: 
wenzelm@10671: 
wenzelm@10671: (*belongs to theory Nat, but requires Datatype*)
wenzelm@10671: consts
wenzelm@10671:   Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
wenzelm@10671: primrec
wenzelm@10671:   "Summation f 0 = 0"
wenzelm@10671:   "Summation f (Suc n) = Summation f n + f n"
wenzelm@10671: 
wenzelm@10671: syntax
wenzelm@10671:   "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
wenzelm@10671: translations
wenzelm@10671:   "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
wenzelm@10671: 
wenzelm@10671: theorem Summation_step:
wenzelm@10671:     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
wenzelm@10671:   by (induct n) simp_all
wenzelm@10671: 
wenzelm@8490: end