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