|
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 +
|
|
10261
|
12 |
Relation_Power + Calculation + SVC_Oracle:
|
|
8490
|
13 |
|
|
10261
|
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]
|
|
9066
|
19 |
|
|
10519
|
20 |
(*belongs to theory Datatype_Universe; hides popular names *)
|
|
|
21 |
hide const Node Atom Leaf Numb Lim Funs Split Case
|
|
10733
|
22 |
hide type node item
|
|
10519
|
23 |
|
|
10671
|
24 |
|
|
10680
|
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 |
|
|
10671
|
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 |
|
|
8490
|
45 |
end
|