src/HOL/PreList.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10733 59f82484e000
child 11787 85b3735a51e1
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     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 *)
     9 
    10 theory PreList =
    11   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    12   Relation_Power + Calculation + SVC_Oracle:
    13 
    14 (*belongs to theory HOL*)
    15 declare case_split [cases type: bool]
    16 
    17 (*belongs to theory Wellfounded_Recursion*)
    18 declare wf_induct [induct set: wf]
    19 
    20 (*belongs to theory Datatype_Universe; hides popular names *)
    21 hide const Node Atom Leaf Numb Lim Funs Split Case
    22 hide type node item
    23 
    24 
    25 (* generic summation indexed over nat *)
    26 
    27 (*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
    28 (*FIXME port theorems from Algebra/abstract/NatSum*)
    29 
    30 consts
    31   Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
    32 primrec
    33   "Summation f 0 = 0"
    34   "Summation f (Suc n) = Summation f n + f n"
    35 
    36 syntax
    37   "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    38 translations
    39   "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    40 
    41 theorem Summation_step:
    42     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    43   by (induct n) simp_all
    44 
    45 end