|
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 +
|
|
12020
|
12 |
Relation_Power + SVC_Oracle:
|
|
|
13 |
|
|
|
14 |
(*belongs to theory Divides*)
|
|
12304
|
15 |
declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]
|
|
8490
|
16 |
|
|
10261
|
17 |
(*belongs to theory Wellfounded_Recursion*)
|
|
|
18 |
declare wf_induct [induct set: wf]
|
|
9066
|
19 |
|
|
10671
|
20 |
|
|
10680
|
21 |
(* generic summation indexed over nat *)
|
|
|
22 |
|
|
10671
|
23 |
consts
|
|
11803
|
24 |
Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
|
|
10671
|
25 |
primrec
|
|
|
26 |
"Summation f 0 = 0"
|
|
|
27 |
"Summation f (Suc n) = Summation f n + f n"
|
|
|
28 |
|
|
|
29 |
syntax
|
|
|
30 |
"_Summation" :: "idt => nat => 'a => nat" ("\<Sum>_<_. _" [0, 51, 10] 10)
|
|
|
31 |
translations
|
|
|
32 |
"\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
|
|
|
33 |
|
|
|
34 |
theorem Summation_step:
|
|
|
35 |
"0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
|
|
|
36 |
by (induct n) simp_all
|
|
|
37 |
|
|
8490
|
38 |
end
|