src/HOL/PreList.thy
author wenzelm
Thu, 14 Dec 2000 19:36:48 +0100
changeset 10671 ac6b3b671198
parent 10519 ade64af4c57c
child 10680 26e4aecf3207
permissions -rw-r--r--
added Summation;
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$
2746bc9a7ef2 comments
nipkow
parents: 8490
diff changeset
     3
    Author:     Tobias Nipkow
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 +
10261
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    12
  Relation_Power + Calculation + SVC_Oracle:
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    13
10261
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    14
(*belongs to theory HOL*)
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    15
declare case_split [cases type: bool]
bb2f1e859177 tuned declarations;
wenzelm
parents: 10212
diff changeset
    16
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
10519
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10261
diff changeset
    20
(*belongs to theory Datatype_Universe; hides popular names *)
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10261
diff changeset
    21
hide const Node Atom Leaf Numb Lim Funs Split Case
ade64af4c57c hide many names from Datatype_Universe.
nipkow
parents: 10261
diff changeset
    22
10671
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    23
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    24
(*belongs to theory Nat, but requires Datatype*)
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    25
consts
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    26
  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    27
primrec
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    28
  "Summation f 0 = 0"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    29
  "Summation f (Suc n) = Summation f n + f n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    30
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    31
syntax
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    32
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    33
translations
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    34
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    35
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    36
theorem Summation_step:
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    37
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    38
  by (induct n) simp_all
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    39
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    40
end