equal
deleted
inserted
replaced
7 |
7 |
8 Series = SEQ + Lim + |
8 Series = SEQ + Lim + |
9 |
9 |
10 consts sumr :: "[nat,nat,(nat=>real)] => real" |
10 consts sumr :: "[nat,nat,(nat=>real)] => real" |
11 primrec |
11 primrec |
12 sumr_0 "sumr m 0 f = #0" |
12 sumr_0 "sumr m 0 f = Numeral0" |
13 sumr_Suc "sumr m (Suc n) f = (if n < m then #0 |
13 sumr_Suc "sumr m (Suc n) f = (if n < m then Numeral0 |
14 else sumr m n f + f(n))" |
14 else sumr m n f + f(n))" |
15 |
15 |
16 constdefs |
16 constdefs |
17 sums :: [nat=>real,real] => bool (infixr 80) |
17 sums :: [nat=>real,real] => bool (infixr 80) |
18 "f sums s == (%n. sumr 0 n f) ----> s" |
18 "f sums s == (%n. sumr 0 n f) ----> s" |