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
nipkow@10519
     1
(*  Title:      HOL/PreList.thy
nipkow@8563
     2
    ID:         $Id$
wenzelm@10733
     3
    Author:     Tobias Nipkow and Markus Wenzel
nipkow@8563
     4
    Copyright   2000 TU Muenchen
nipkow@8563
     5
nipkow@8563
     6
A basis for building theory List on. Is defined separately to serve as a
nipkow@8563
     7
basis for theory ToyList in the documentation.
nipkow@8563
     8
*)
wenzelm@8490
     9
wenzelm@8490
    10
theory PreList =
nipkow@10212
    11
  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
wenzelm@10261
    12
  Relation_Power + Calculation + SVC_Oracle:
wenzelm@8490
    13
wenzelm@10261
    14
(*belongs to theory HOL*)
wenzelm@10261
    15
declare case_split [cases type: bool]
wenzelm@10261
    16
wenzelm@10261
    17
(*belongs to theory Wellfounded_Recursion*)
wenzelm@10261
    18
declare wf_induct [induct set: wf]
wenzelm@9066
    19
nipkow@10519
    20
(*belongs to theory Datatype_Universe; hides popular names *)
nipkow@10519
    21
hide const Node Atom Leaf Numb Lim Funs Split Case
wenzelm@10733
    22
hide type node item
nipkow@10519
    23
wenzelm@10671
    24
wenzelm@10680
    25
(* generic summation indexed over nat *)
wenzelm@10680
    26
wenzelm@10680
    27
(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
wenzelm@10680
    28
(*FIXME port theorems from Algebra/abstract/NatSum*)
wenzelm@10680
    29
wenzelm@10671
    30
consts
wenzelm@10671
    31
  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
wenzelm@10671
    32
primrec
wenzelm@10671
    33
  "Summation f 0 = 0"
wenzelm@10671
    34
  "Summation f (Suc n) = Summation f n + f n"
wenzelm@10671
    35
wenzelm@10671
    36
syntax
wenzelm@10671
    37
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
wenzelm@10671
    38
translations
wenzelm@10671
    39
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
wenzelm@10671
    40
wenzelm@10671
    41
theorem Summation_step:
wenzelm@10671
    42
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
wenzelm@10671
    43
  by (induct n) simp_all
wenzelm@10671
    44
wenzelm@8490
    45
end