src/HOL/PreList.thy
author wenzelm
Tue Feb 05 23:18:08 2002 +0100 (2002-02-05)
changeset 12869 f362c0323d92
parent 12397 6766aa05e4eb
child 12919 d6a0d168291e
permissions -rw-r--r--
moved SVC stuff to ex;
     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:
    13 
    14 (*belongs to theory Divides*)
    15 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
    16 
    17 (*belongs to theory Nat*)
    18 lemmas less_induct = nat_less_induct [rule_format, case_names less]
    19 
    20 (*belongs to theory Wellfounded_Recursion*)
    21 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    22 
    23 
    24 (* generic summation indexed over nat *)
    25 
    26 consts
    27   Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
    28 primrec
    29   "Summation f 0 = 0"
    30   "Summation f (Suc n) = Summation f n + f n"
    31 
    32 syntax
    33   "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    34 translations
    35   "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    36 
    37 theorem Summation_step:
    38     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    39   by (induct n) simp_all
    40 
    41 end