src/HOL/PreList.thy
author wenzelm
Fri, 02 Nov 2001 22:01:58 +0100
changeset 12020 a24373086908
parent 11955 5818c5abb415
child 12304 8df202daf55d
permissions -rw-r--r--
theory Calculation move to Set;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10519
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10261
diff changeset
     1
(*  Title:      HOL/PreList.thy
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     2
    ID:         $Id$
10733
59f82484e000 hide type node item;
wenzelm
parents: 10680
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel
8563
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     4
    Copyright   2000 TU Muenchen
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     5
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     6
A basis for building theory List on. Is defined separately to serve as a
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     7
basis for theory ToyList in the documentation.
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     8
*)
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
     9
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    10
theory PreList =
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 9619
diff changeset
    11
  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
12020
a24373086908 theory Calculation move to Set;
wenzelm
parents: 11955
diff changeset
    12
  Relation_Power + SVC_Oracle:
a24373086908 theory Calculation move to Set;
wenzelm
parents: 11955
diff changeset
    13
a24373086908 theory Calculation move to Set;
wenzelm
parents: 11955
diff changeset
    14
(*belongs to theory Divides*)
a24373086908 theory Calculation move to Set;
wenzelm
parents: 11955
diff changeset
    15
declare dvd_trans [trans]
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    16
10261
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    17
(*belongs to theory Wellfounded_Recursion*)
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    18
declare wf_induct [induct set: wf]
9066
b1e874e38dab theorems [cases type: bool] = case_split;
wenzelm
parents: 8862
diff changeset
    19
10671
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    20
10680
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    21
(* generic summation indexed over nat *)
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    22
10671
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    23
consts
11803
wenzelm
parents: 11787
diff changeset
    24
  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
10671
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    25
primrec
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    26
  "Summation f 0 = 0"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    27
  "Summation f (Suc n) = Summation f n + f n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    28
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    29
syntax
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    30
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    31
translations
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    32
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    33
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    34
theorem Summation_step:
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    35
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    36
  by (induct n) simp_all
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    37
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    38
end