1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 16:47:23 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 13 19:49:07 2005 +0200
     1.3 @@ -10,33 +10,6 @@
     1.4  imports Log
     1.5  begin
     1.6  
     1.7 -(* FIXME generalize? *)
     1.8 -lemma sumr_offset:
     1.9 - "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    1.10 -by (induct "n", auto)
    1.11 -
    1.12 -lemma sumr_offset2:
    1.13 - "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    1.14 -by (induct "n", auto)
    1.15 -
    1.16 -lemma sumr_offset3:
    1.17 -  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    1.18 -by (simp  add: sumr_offset)
    1.19 -
    1.20 -lemma sumr_offset4:
    1.21 - "\<forall>n f. setsum f {0::nat..<n+k} =
    1.22 -        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    1.23 -by (simp add: sumr_offset)
    1.24 -
    1.25 -(*
    1.26 -lemma sumr_from_1_from_0: "0 < n ==>
    1.27 -      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
    1.28 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
    1.29 -      (\<Sum>n=0..<Suc n. if even(n) then 0 else
    1.30 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
    1.31 -by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
    1.32 -*)
    1.33 -
    1.34  subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
    1.35  
    1.36  text{*This is a very long, messy proof even now that it's been broken down