src/HOL/PreList.thy
author wenzelm
Fri, 15 Dec 2000 17:59:30 +0100
changeset 10680 26e4aecf3207
parent 10671 ac6b3b671198
child 10733 59f82484e000
permissions -rw-r--r--
tuned comment;
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
10680
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    24
(* generic summation indexed over nat *)
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    25
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    26
(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    27
(*FIXME port theorems from Algebra/abstract/NatSum*)
26e4aecf3207 tuned comment;
wenzelm
parents: 10671
diff changeset
    28
10671
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    29
consts
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    30
  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    31
primrec
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    32
  "Summation f 0 = 0"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    33
  "Summation f (Suc n) = Summation f n + f n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    34
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    35
syntax
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    36
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    37
translations
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    38
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    39
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    40
theorem Summation_step:
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    41
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    42
  by (induct n) simp_all
ac6b3b671198 added Summation;
wenzelm
parents: 10519
diff changeset
    43
8490
6e0f23304061 added HOL/PreLIst.thy;
wenzelm
parents:
diff changeset
    44
end