--- a/src/HOL/Library/Formal_Power_Series.thy Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Aug 31 14:09:42 2009 +0200
@@ -633,8 +633,7 @@
by (auto simp add: inverse_eq_divide power_divide)
from k have kn: "k > n"
- apply (simp add: leastP_def setge_def fps_sum_rep_nth)
- by (cases "k \<le> n", auto)
+ by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
then have "dist (?s n) a < (1/2)^n" unfolding dth
by (auto intro: power_strict_decreasing)
also have "\<dots> <= (1/2)^n0" using nn0
@@ -1244,10 +1243,9 @@
{assume n0: "n \<noteq> 0"
then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
"{0..n - 1}\<union>{n} = {0..n}"
- apply (simp_all add: expand_set_eq) by presburger+
+ by (auto simp: expand_set_eq)
have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
- "{0..n - 1}\<inter>{n} ={}" using n0
- by (simp_all add: expand_set_eq, presburger+)
+ "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
have f: "finite {0}" "finite {1}" "finite {2 .. n}"
"finite {0 .. n - 1}" "finite {n}" by simp_all
have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"