src/HOL/Library/Formal_Power_Series.thy
 changeset 29911 c790a70a3d19 parent 29906 80369da39838 child 29912 f4ac160d2e77
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 11:10:35 2009 -0800
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 11:11:30 2009 -0800
1.3 @@ -11,81 +11,96 @@
1.4
1.5  subsection {* The type of formal power series*}
1.6
1.7 -typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
1.8 +typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
1.9 +  morphisms fps_nth Abs_fps
1.10    by simp
1.11
1.12 +notation fps_nth (infixl "\$" 75)
1.13 +
1.14 +lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p \$ n = q \$ n)"
1.15 +  by (simp add: fps_nth_inject [symmetric] expand_fun_eq)
1.16 +
1.17 +lemma fps_ext: "(\<And>n. p \$ n = q \$ n) \<Longrightarrow> p = q"
1.18 +  by (simp add: expand_fps_eq)
1.19 +
1.20 +lemma fps_nth_Abs_fps [simp]: "Abs_fps f \$ n = f n"
1.21 +  by (simp add: Abs_fps_inverse)
1.22 +
1.23  text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
1.24
1.25  instantiation fps :: (zero)  zero
1.26  begin
1.27
1.28 -definition fps_zero_def: "(0 :: 'a fps) \<equiv> Abs_fps (\<lambda>(n::nat). 0)"
1.29 +definition fps_zero_def:
1.30 +  "0 = Abs_fps (\<lambda>n. 0)"
1.31 +
1.32  instance ..
1.33  end
1.34
1.35 +lemma fps_zero_nth [simp]: "0 \$ n = 0"
1.36 +  unfolding fps_zero_def by simp
1.37 +
1.38  instantiation fps :: ("{one,zero}")  one
1.39  begin
1.40
1.41 -definition fps_one_def: "(1 :: 'a fps) \<equiv> Abs_fps (\<lambda>(n::nat). if n = 0 then 1 else 0)"
1.42 +definition fps_one_def:
1.43 +  "1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)"
1.44 +
1.45  instance ..
1.46  end
1.47
1.48 +lemma fps_one_nth [simp]: "1 \$ n = (if n = 0 then 1 else 0)"
1.49 +  unfolding fps_one_def by simp
1.50 +
1.51  instantiation fps :: (plus)  plus
1.52  begin
1.53
1.54 -definition fps_plus_def: "op + \<equiv> (\<lambda>(f::'a fps) (g:: 'a fps). Abs_fps (\<lambda>(n::nat). Rep_fps (f) n + Rep_fps (g) n))"
1.55 +definition fps_plus_def:
1.56 +  "op + = (\<lambda>f g. Abs_fps (\<lambda>n. f \$ n + g \$ n))"
1.57 +
1.58  instance ..
1.59  end
1.60
1.61 -instantiation fps :: (minus)  minus
1.62 +lemma fps_add_nth [simp]: "(f + g) \$ n = f \$ n + g \$ n"
1.63 +  unfolding fps_plus_def by simp
1.64 +
1.65 +instantiation fps :: (minus) minus
1.66  begin
1.67
1.68 -definition fps_minus_def: "op - \<equiv> (\<lambda>(f::'a fps) (g:: 'a fps). Abs_fps (\<lambda>(n::nat). Rep_fps (f) n - Rep_fps (g) n))"
1.69 +definition fps_minus_def:
1.70 +  "op - = (\<lambda>f g. Abs_fps (\<lambda>n. f \$ n - g \$ n))"
1.71 +
1.72  instance ..
1.73  end
1.74
1.75 -instantiation fps :: (uminus)  uminus
1.76 +lemma fps_sub_nth [simp]: "(f - g) \$ n = f \$ n - g \$ n"
1.77 +  unfolding fps_minus_def by simp
1.78 +
1.79 +instantiation fps :: (uminus) uminus
1.80  begin
1.81
1.82 -definition fps_uminus_def: "uminus \<equiv> (\<lambda>(f::'a fps). Abs_fps (\<lambda>(n::nat). - Rep_fps (f) n))"
1.83 +definition fps_uminus_def:
1.84 +  "uminus = (\<lambda>f. Abs_fps (\<lambda>n. - (f \$ n)))"
1.85 +
1.86  instance ..
1.87  end
1.88
1.89 +lemma fps_neg_nth [simp]: "(- f) \$ n = - (f \$ n)"
1.90 +  unfolding fps_uminus_def by simp
1.91 +
1.92  instantiation fps :: ("{comm_monoid_add, times}")  times
1.93  begin
1.94
1.95 -definition fps_times_def:
1.96 -  "op * \<equiv> (\<lambda>(f::'a fps) (g:: 'a fps). Abs_fps (\<lambda>(n::nat). setsum (\<lambda>i. Rep_fps (f) i  * Rep_fps (g) (n - i)) {0.. n}))"
1.97 +definition fps_times_def:
1.98 +  "op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f \$ i * g \$ (n - i)))"
1.99 +
1.100  instance ..
1.101  end
1.102
1.103 -text{* Some useful theorems to get rid of Abs and Rep *}
1.104 +lemma fps_mult_nth: "(f * g) \$ n = (\<Sum>i=0..n. f\$i * g\$(n - i))"
1.105 +  unfolding fps_times_def by simp
1.106
1.107 -lemma mem_fps_set_trivial[intro, simp]: "f \<in> fps" unfolding fps_def by blast
1.108 -lemma Rep_fps_Abs_fps[simp]: "Rep_fps (Abs_fps f) = f"
1.109 -  by (blast intro: Abs_fps_inverse)
1.110 -lemma Abs_fps_Rep_fps[simp]: "Abs_fps (Rep_fps f) = f"
1.111 -  by (blast intro: Rep_fps_inverse)
1.112 -lemma Abs_fps_eq[simp]: "Abs_fps f = Abs_fps g \<longleftrightarrow> f = g"
1.113 -proof-
1.114 -  {assume "f = g" hence "Abs_fps f = Abs_fps g" by simp}
1.115 -  moreover
1.116 -  {assume a: "Abs_fps f = Abs_fps g"
1.117 -    from a have "Rep_fps (Abs_fps f) = Rep_fps (Abs_fps g)" by simp
1.118 -    hence "f = g" by simp}
1.119 -  ultimately show ?thesis by blast
1.120 -qed
1.121 -
1.122 -lemma Rep_fps_eq[simp]: "Rep_fps f = Rep_fps g \<longleftrightarrow> f = g"
1.123 -proof-
1.124 -  {assume "Rep_fps f = Rep_fps g"
1.125 -    hence "Abs_fps (Rep_fps f) = Abs_fps (Rep_fps g)" by simp hence "f=g" by simp}
1.126 -  moreover
1.127 -  {assume "f = g" hence "Rep_fps f = Rep_fps g" by simp}
1.128 -  ultimately show ?thesis by blast
1.129 -qed
1.130 -
1.131 -declare atLeastAtMost_iff[presburger]
1.132 +declare atLeastAtMost_iff[presburger]
1.133  declare Bex_def[presburger]
1.134  declare Ball_def[presburger]
1.135
1.136 @@ -97,350 +112,276 @@
1.137  subsection{* Formal power series form a commutative ring with unity, if the range of sequences
1.138    they represent is a commutative ring with unity*}
1.139
1.141 -begin
1.142 -
1.143 -instance
1.145  proof
1.146    fix a b c :: "'a fps" show "a + b + c = a + (b + c)"
1.149 +qed
1.150 +
1.152 +proof
1.153 +  fix a b :: "'a fps" show "a + b = b + a"
1.155  qed
1.156
1.157 -end
1.158 -
1.160 -begin
1.161 +lemma fps_mult_assoc_lemma:
1.162 +  fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
1.163 +  shows "(\<Sum>j=0..k. \<Sum>i=0..j. f i (j - i) (n - j)) =
1.164 +         (\<Sum>j=0..k. \<Sum>i=0..k - j. f j i (n - j - i))"
1.165 +proof (induct k)
1.166 +  case 0 show ?case by simp
1.167 +next
1.168 +  case (Suc k) thus ?case
1.170 +             cong: strong_setsum_cong)
1.171 +qed
1.172
1.174 -end
1.175 -
1.176 -instantiation fps :: (semiring_1) semigroup_mult
1.177 -begin
1.178 -
1.179 -instance
1.180 +instance fps :: (semiring_0) semigroup_mult
1.181  proof
1.182    fix a b c :: "'a fps"
1.183 -  let ?a = "Rep_fps a"
1.184 -  let ?b = "Rep_fps b"
1.185 -  let ?c = "Rep_fps c"
1.186 -  let ?x = "\<lambda> i k. if k \<le> i then (1::'a) else 0"
1.187 -  show "a*b*c = a* (b * c)"
1.188 -  proof(auto simp add: fps_times_def setsum_right_distrib setsum_left_distrib, rule ext)
1.189 -    fix n::nat
1.190 -    let ?r = "\<lambda>i. n - i"
1.191 -    have i: "inj_on ?r {0..n}" by (auto simp add: inj_on_def)
1.192 -    have ri: "{0 .. n} = ?r ` {0..n}" apply (auto simp add: image_iff)
1.193 -      by presburger
1.194 -    let ?f = "\<lambda>i j. ?a j * ?b (i - j) * ?c (n -i)"
1.195 -    let ?g = "\<lambda>i j. ?a i * (?b j * ?c (n - (i + j)))"
1.196 -    have "setsum (\<lambda>i. setsum (?f i) {0..i}) {0..n}
1.197 -      = setsum (\<lambda>i. setsum (\<lambda>j. ?f i j * ?x i j) {0..i}) {0..n}"
1.198 -      by (rule setsum_cong2)+ auto
1.199 -    also have "\<dots> = setsum (\<lambda>i. setsum (\<lambda>j. ?f i j * ?x i j) {0..n}) {0..n}"
1.200 -    proof(rule setsum_cong2)
1.201 -      fix i assume i: "i \<in> {0..n}"
1.202 -      have eq: "{0 .. n} = {0 ..i} \<union> {i+1 .. n}" using i by auto
1.203 -      have d: "{0 ..i} \<inter> {i+1 .. n} = {}" using i by auto
1.204 -      have f: "finite {0..i}" "finite {i+1 ..n}" by auto
1.205 -      have s0: "setsum (\<lambda>j. ?f i j * ?x i j) {i+1 ..n} = 0" by simp
1.206 -      show "setsum (\<lambda>j. ?f i j * ?x i j) {0..i} = setsum (\<lambda>j. ?f i j * ?x i j) {0..n}"
1.207 -	unfolding eq setsum_Un_disjoint[OF f d] s0
1.208 -	by simp
1.209 -    qed
1.210 -    also have "\<dots> = setsum (\<lambda>i. setsum (\<lambda>j. ?f j i * ?x j i) {0 .. n}) {0 .. n}"
1.211 -      by (rule setsum_commute)
1.212 -    also have "\<dots> = setsum (\<lambda>i. setsum (\<lambda>j. ?f j i * ?x j i) {i .. n}) {0 .. n}"
1.213 -      apply(rule setsum_cong2)
1.214 -      apply (rule setsum_mono_zero_right)
1.215 -      apply auto
1.216 -      done
1.217 -    also have "\<dots> = setsum (\<lambda>i. setsum (?g i) {0..n - i}) {0..n}"
1.218 -      apply (rule setsum_cong2)
1.219 -      apply (rule_tac f="\<lambda>i. i + x" in setsum_reindex_cong)
1.220 -      apply (simp add: inj_on_def)
1.221 -      apply (rule set_ext)
1.222 -      apply (presburger add: image_iff)
1.224 -    finally  show "setsum (\<lambda>i. setsum (\<lambda>j. ?a j * ?b (i - j) * ?c (n -i)) {0..i}) {0..n}
1.225 -      = setsum (\<lambda>i. setsum (\<lambda>j. ?a i * (?b j * ?c (n - (i + j)))) {0..n - i}) {0..n}".
1.226 +  show "(a * b) * c = a * (b * c)"
1.227 +  proof (rule fps_ext)
1.228 +    fix n :: nat
1.229 +    have "(\<Sum>j=0..n. \<Sum>i=0..j. a\$i * b\$(j - i) * c\$(n - j)) =
1.230 +          (\<Sum>j=0..n. \<Sum>i=0..n - j. a\$j * b\$i * c\$(n - j - i))"
1.231 +      by (rule fps_mult_assoc_lemma)
1.232 +    thus "((a * b) * c) \$ n = (a * (b * c)) \$ n"
1.233 +      by (simp add: fps_mult_nth setsum_right_distrib
1.234 +                    setsum_left_distrib mult_assoc)
1.235 +  qed
1.236 +qed
1.237 +
1.238 +lemma fps_mult_commute_lemma:
1.239 +  fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
1.240 +  shows "(\<Sum>i=0..n. f i (n - i)) = (\<Sum>i=0..n. f (n - i) i)"
1.241 +proof (rule setsum_reindex_cong)
1.242 +  show "inj_on (\<lambda>i. n - i) {0..n}"
1.243 +    by (rule inj_onI) simp
1.244 +  show "{0..n} = (\<lambda>i. n - i) ` {0..n}"
1.245 +    by (auto, rule_tac x="n - x" in image_eqI, simp_all)
1.246 +next
1.247 +  fix i assume "i \<in> {0..n}"
1.248 +  hence "n - (n - i) = i" by simp
1.249 +  thus "f (n - i) i = f (n - i) (n - (n - i))" by simp
1.250 +qed
1.251 +
1.252 +instance fps :: (comm_semiring_0) ab_semigroup_mult
1.253 +proof
1.254 +  fix a b :: "'a fps"
1.255 +  show "a * b = b * a"
1.256 +  proof (rule fps_ext)
1.257 +    fix n :: nat
1.258 +    have "(\<Sum>i=0..n. a\$i * b\$(n - i)) = (\<Sum>i=0..n. a\$(n - i) * b\$i)"
1.259 +      by (rule fps_mult_commute_lemma)
1.260 +    thus "(a * b) \$ n = (b * a) \$ n"
1.261 +      by (simp add: fps_mult_nth mult_commute)
1.262    qed
1.263  qed
1.264
1.265 -end
1.266 -
1.267 -instantiation fps :: (comm_semiring_1) ab_semigroup_mult
1.268 -begin
1.269 -
1.270 -instance
1.271 -proof
1.272 -  fix a b :: "'a fps"
1.273 -  show "a*b = b*a"
1.274 -  apply(auto simp add: fps_times_def setsum_right_distrib setsum_left_distrib, rule ext)
1.275 -  apply (rule_tac f = "\<lambda>i. n - i" in setsum_reindex_cong)
1.276 -  apply (simp add: inj_on_def)
1.277 -  apply presburger
1.278 -  apply (rule set_ext)
1.279 -  apply (presburger add: image_iff)
1.280 -  by (simp add: mult_commute)
1.281 -qed
1.282 -end
1.283 -
1.285 -begin
1.286 -
1.287 -instance
1.289  proof
1.290    fix a :: "'a fps" show "0 + a = a "
1.291 -    by (auto simp add: fps_plus_def fps_zero_def intro: ext)
1.292 +    by (simp add: fps_ext)
1.293  next
1.294    fix a :: "'a fps" show "a + 0 = a "
1.295 -    by (auto simp add: fps_plus_def fps_zero_def intro: ext)
1.296 +    by (simp add: fps_ext)
1.297  qed
1.298
1.299 -end
1.301 -begin
1.302 -
1.303 -instance
1.305  proof
1.306    fix a :: "'a fps" show "0 + a = a "
1.307 -    by (auto simp add: fps_plus_def fps_zero_def intro: ext)
1.308 +    by (simp add: fps_ext)
1.309  qed
1.310
1.311 -end
1.312 -
1.313 -instantiation fps :: (semiring_1) monoid_mult
1.314 -begin
1.315 -
1.316 -instance
1.317 +instance fps :: (semiring_1) monoid_mult
1.318  proof
1.319    fix a :: "'a fps" show "1 * a = a"
1.320 -    apply (auto simp add: fps_one_def fps_times_def)
1.321 -    apply (subst (2) Abs_fps_Rep_fps[of a, symmetric])
1.322 -    unfolding Abs_fps_eq
1.323 -    apply (rule ext)
1.324 +    apply (rule fps_ext)
1.325 +    apply (simp add: fps_mult_nth)
1.326      by (simp add: cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
1.327  next
1.328 -  fix a :: "'a fps" show "a*1 = a"
1.329 -    apply (auto simp add: fps_one_def fps_times_def)
1.330 -    apply (subst (2) Abs_fps_Rep_fps[of a, symmetric])
1.331 -    unfolding Abs_fps_eq
1.332 -    apply (rule ext)
1.333 +  fix a :: "'a fps" show "a * 1 = a"
1.334 +    apply (rule fps_ext)
1.335 +    apply (simp add: fps_mult_nth)
1.336      by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
1.337  qed
1.338 -end
1.339 -
1.341 -begin
1.342
1.343 -instance by (intro_classes) (auto simp add: fps_plus_def expand_fun_eq Rep_fps_eq[symmetric])
1.344 -end
1.346 +proof
1.347 +  fix a b c :: "'a fps"
1.348 +  assume "a + b = a + c" then show "b = c"
1.349 +    by (simp add: expand_fps_eq)
1.350 +next
1.351 +  fix a b c :: "'a fps"
1.352 +  assume "b + a = c + a" then show "b = c"
1.353 +    by (simp add: expand_fps_eq)
1.354 +qed
1.355
1.357 -begin
1.359 +proof
1.360 +  fix a b c :: "'a fps"
1.361 +  assume "a + b = a + c" then show "b = c"
1.362 +    by (simp add: expand_fps_eq)
1.363 +qed
1.364
1.365 -instance
1.367 +
1.369  proof
1.370    fix a :: "'a fps" show "- a + a = 0"
1.371 -    by (auto simp add: fps_plus_def fps_uminus_def fps_zero_def intro: ext)
1.372 +    by (simp add: fps_ext)
1.373  next
1.374    fix a b :: "'a fps" show "a - b = a + - b"
1.375 -    by (auto simp add: fps_plus_def fps_uminus_def fps_zero_def
1.376 -      fps_minus_def expand_fun_eq diff_minus)
1.377 +    by (simp add: fps_ext diff_minus)
1.378  qed
1.379 -end
1.380 -
1.381 -context comm_ring_1
1.382 -begin
1.384 -end
1.385
1.386 -instantiation fps :: (zero_neq_one) zero_neq_one
1.387 -begin
1.388 -instance by (intro_classes, auto simp add: zero_neq_one
1.389 -  fps_one_def fps_zero_def expand_fun_eq)
1.390 -end
1.392 +proof
1.393 +  fix a :: "'a fps"
1.394 +  show "- a + a = 0"
1.395 +    by (simp add: fps_ext)
1.396 +next
1.397 +  fix a b :: "'a fps"
1.398 +  show "a - b = a + - b"
1.399 +    by (simp add: fps_ext)
1.400 +qed
1.401
1.402 -instantiation fps :: (semiring_1) semiring
1.403 -begin
1.404 +instance fps :: (zero_neq_one) zero_neq_one
1.405 +  by default (simp add: expand_fps_eq)
1.406
1.407 -instance
1.408 +instance fps :: (semiring_0) semiring
1.409  proof
1.410    fix a b c :: "'a fps"
1.411 -  show "(a + b) * c = a * c + b*c"
1.412 -    apply (auto simp add: fps_plus_def fps_times_def, rule ext)
1.414 -    apply (simp add: ring_simps)
1.415 -    done
1.416 +  show "(a + b) * c = a * c + b * c"
1.418  next
1.419    fix a b c :: "'a fps"
1.420 -  show "a * (b + c) = a * b + a*c"
1.421 -    apply (auto simp add: fps_plus_def fps_times_def, rule ext)
1.423 -    apply (simp add: ring_simps)
1.424 -    done
1.425 +  show "a * (b + c) = a * b + a * c"
1.427  qed
1.428 -end
1.429
1.430 -instantiation fps :: (semiring_1) semiring_0
1.431 -begin
1.432 -
1.433 -instance
1.434 +instance fps :: (semiring_0) semiring_0
1.435  proof
1.436 -  fix a:: "'a fps" show "0 * a = 0" by (simp add: fps_zero_def fps_times_def)
1.437 +  fix a:: "'a fps" show "0 * a = 0"
1.438 +    by (simp add: fps_ext fps_mult_nth)
1.439  next
1.440 -  fix a:: "'a fps" show "a*0 = 0" by (simp add: fps_zero_def fps_times_def)
1.441 +  fix a:: "'a fps" show "a * 0 = 0"
1.442 +    by (simp add: fps_ext fps_mult_nth)
1.443  qed
1.444 -end
1.445 -
1.446 +
1.447 +instance fps :: (semiring_0_cancel) semiring_0_cancel ..
1.448 +
1.449  subsection {* Selection of the nth power of the implicit variable in the infinite sum*}
1.450
1.451 -definition fps_nth:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" (infixl "\$" 75)
1.452 -  where "f \$ n = Rep_fps f n"
1.453 -
1.454 -lemma fps_nth_Abs_fps[simp]: "Abs_fps a \$ n = a n" by (simp add: fps_nth_def)
1.455 -lemma fps_zero_nth[simp]: "0 \$ n = 0" by (simp add: fps_zero_def)
1.456 -lemma fps_one_nth[simp]: "1 \$ n = (if n = 0 then 1 else 0)"
1.457 -  by (simp add: fps_one_def)
1.458 -lemma fps_add_nth[simp]: "(f + g) \$ n = f\$n + g\$n" by (simp add: fps_plus_def fps_nth_def)
1.459 -lemma fps_mult_nth: "(f * g) \$ n = setsum (\<lambda>i. f\$i * g\$(n - i)) {0..n}"
1.460 -  by (simp add: fps_times_def fps_nth_def)
1.461 -lemma fps_neg_nth[simp]: "(- f) \$n = - (f \$n)" by (simp add: fps_nth_def fps_uminus_def)
1.462 -lemma fps_sub_nth[simp]: "(f - g)\$n = f\$n - g\$n" by (simp add: fps_nth_def fps_minus_def)
1.463 -
1.464  lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f \$n \<noteq> 0)"
1.465 -proof-
1.466 -  {assume "f \<noteq> 0"
1.467 -    hence "Rep_fps f \<noteq> Rep_fps 0" by simp
1.468 -    hence "\<exists>n. f \$n \<noteq> 0" by (simp add: expand_fun_eq fps_zero_def fps_nth_def )}
1.469 -  moreover
1.470 -  {assume "\<exists>n. f\$n \<noteq> 0" and "f = 0"
1.471 -    then have False by (simp add: expand_fun_eq fps_zero_def fps_nth_def )}
1.472 -  ultimately show ?thesis by blast
1.473 -qed
1.474 +  by (simp add: expand_fps_eq)
1.475
1.476 -lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f \$n \<noteq> 0 \<and> (\<forall>m <n. f \$m = 0))"
1.477 -proof-
1.478 -  let ?S = "{n. f\$n \<noteq> 0}"
1.479 -  {assume "\<exists>n. f\$n \<noteq> 0 \<and> (\<forall>m <n. f \$m = 0)" and "f = 0"
1.480 -    then have False by (simp add: expand_fun_eq fps_zero_def fps_nth_def )}
1.481 -  moreover
1.482 -  {assume f0: "f \<noteq> 0"
1.483 -    from f0 fps_nonzero_nth have ex: "\<exists>n. f\$n \<noteq> 0" by blast
1.484 -    hence Se: "?S\<noteq> {}" by blast
1.485 -    from ex obtain n where n: "f\$n \<noteq> 0" by blast
1.486 -    from n have nS: "n \<in> ?S" by blast
1.487 -        let ?U = "?S \<inter> {0..n}"
1.488 -    have fU: "finite ?U" by auto
1.489 -    from n have Ue: "?U \<noteq> {}" by auto
1.490 -    let ?m = "Min ?U"
1.491 -    have mU: "?m \<in> ?U" using Min_in[OF fU Ue] .
1.492 -    hence mn: "?m \<le> n" by simp
1.493 -    from mU have mf: "f \$ ?m \<noteq> 0" by blast
1.494 -    {fix m assume m: "m < ?m" and f: "f \$m \<noteq> 0"
1.495 -      from m mn have mn': "m < n" by arith
1.496 -      with f have mU': "m \<in> ?U" by simp
1.497 -      from Min_le[OF fU mU'] m have False by arith}
1.498 -    hence "\<forall>m <?m. f\$m = 0" by blast
1.499 -    with mf have "\<exists> n. f \$n \<noteq> 0 \<and> (\<forall>m <n. f \$m = 0)" by blast}
1.500 -  ultimately show ?thesis by blast
1.501 +lemma fps_nonzero_nth_minimal:
1.502 +  "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f \$ n \<noteq> 0 \<and> (\<forall>m<n. f \$ m = 0))"
1.503 +proof
1.504 +  let ?n = "LEAST n. f \$ n \<noteq> 0"
1.505 +  assume "f \<noteq> 0"
1.506 +  then have "\<exists>n. f \$ n \<noteq> 0"
1.507 +    by (simp add: fps_nonzero_nth)
1.508 +  then have "f \$ ?n \<noteq> 0"
1.509 +    by (rule LeastI_ex)
1.510 +  moreover have "\<forall>m<?n. f \$ m = 0"
1.511 +    by (auto dest: not_less_Least)
1.512 +  ultimately have "f \$ ?n \<noteq> 0 \<and> (\<forall>m<?n. f \$ m = 0)" ..
1.513 +  then show "\<exists>n. f \$ n \<noteq> 0 \<and> (\<forall>m<n. f \$ m = 0)" ..
1.514 +next
1.515 +  assume "\<exists>n. f \$ n \<noteq> 0 \<and> (\<forall>m<n. f \$ m = 0)"
1.516 +  then show "f \<noteq> 0" by (auto simp add: expand_fps_eq)
1.517  qed
1.518
1.519  lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f \$ n = g \$n)"
1.520 -  by (auto simp add: fps_nth_def Rep_fps_eq[unfolded expand_fun_eq])
1.521 +  by (rule expand_fps_eq)
1.522
1.523  lemma fps_setsum_nth: "(setsum f S) \$ n = setsum (\<lambda>k. (f k) \$ n) S"
1.524 -proof-
1.525 -  {assume "\<not> finite S" hence ?thesis by simp}
1.526 -  moreover
1.527 -  {assume fS: "finite S"
1.528 -    have ?thesis by(induct rule: finite_induct[OF fS]) auto}
1.529 -  ultimately show ?thesis by blast
1.530 +proof (cases "finite S")
1.531 +  assume "\<not> finite S" then show ?thesis by simp
1.532 +next
1.533 +  assume "finite S"
1.534 +  then show ?thesis by (induct set: finite) auto
1.535  qed
1.536
1.537  subsection{* Injection of the basic ring elements and multiplication by scalars *}
1.538
1.539 -definition "fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)"
1.540 -lemma fps_const_0_eq_0[simp]: "fps_const 0 = 0" by (simp add: fps_const_def fps_eq_iff)
1.541 -lemma fps_const_1_eq_1[simp]: "fps_const 1 = 1" by (simp add: fps_const_def fps_eq_iff)
1.542 -lemma fps_const_neg[simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)"
1.543 -  by (simp add: fps_uminus_def fps_const_def fps_eq_iff)
1.544 -lemma fps_const_add[simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
1.545 -  by (simp add: fps_plus_def fps_const_def fps_eq_iff)
1.546 +definition
1.547 +  "fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)"
1.548 +
1.549 +lemma fps_nth_fps_const [simp]: "fps_const c \$ n = (if n = 0 then c else 0)"
1.550 +  unfolding fps_const_def by simp
1.551 +
1.552 +lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0"
1.553 +  by (simp add: fps_ext)
1.554 +
1.555 +lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1"
1.556 +  by (simp add: fps_ext)
1.557 +
1.558 +lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)"
1.559 +  by (simp add: fps_ext)
1.560 +
1.561 +lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
1.562 +  by (simp add: fps_ext)
1.563 +
1.564  lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
1.565 -  by (auto simp add: fps_times_def fps_const_def fps_eq_iff intro: setsum_0')
1.566 +  by (simp add: fps_eq_iff fps_mult_nth setsum_0')
1.567
1.568  lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f = Abs_fps (\<lambda>n. if n = 0 then c + f\$0 else f\$n)"
1.570 +  by (simp add: fps_ext)
1.571 +
1.572  lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = Abs_fps (\<lambda>n. if n = 0 then f\$0 + c else f\$n)"
1.574 +  by (simp add: fps_ext)
1.575
1.576  lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f\$n)"
1.577 -  unfolding fps_eq_iff fps_mult_nth
1.578 +  unfolding fps_eq_iff fps_mult_nth
1.579    by (simp add: fps_const_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
1.580 +
1.581  lemma fps_const_mult_right: "f * fps_const (c::'a\<Colon>semiring_0) = Abs_fps (\<lambda>n. f\$n * c)"
1.582 -  unfolding fps_eq_iff fps_mult_nth
1.583 +  unfolding fps_eq_iff fps_mult_nth
1.584    by (simp add: fps_const_def cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong)
1.585
1.586 -lemma fps_const_nth[simp]: "(fps_const c) \$n = (if n = 0 then c else 0)"
1.587 -  by (simp add: fps_const_def)
1.588 +lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)\$n = c* f\$n"
1.589 +  by (simp add: fps_mult_nth cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
1.590
1.591 -lemma fps_mult_left_const_nth[simp]: "(fps_const (c::'a::semiring_1) * f)\$n = c* f\$n"
1.592 -  by (simp add: fps_mult_nth fps_const_nth cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
1.593 -
1.594 -lemma fps_mult_right_const_nth[simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c"
1.595 -  by (simp add: fps_mult_nth fps_const_nth cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong)
1.596 +lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c"
1.597 +  by (simp add: fps_mult_nth cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong)
1.598
1.599  subsection {* Formal power series form an integral domain*}
1.600
1.601 -instantiation fps :: (ring_1) ring_1
1.602 -begin
1.603 +instance fps :: (ring) ring ..
1.604
1.605 -instance by (intro_classes, auto simp add: diff_minus left_distrib)
1.606 -end
1.607 +instance fps :: (ring_1) ring_1
1.608 +  by (intro_classes, auto simp add: diff_minus left_distrib)
1.609
1.610 -instantiation fps :: (comm_ring_1) comm_ring_1
1.611 -begin
1.612 +instance fps :: (comm_ring_1) comm_ring_1
1.613 +  by (intro_classes, auto simp add: diff_minus left_distrib)
1.614
1.615 -instance by (intro_classes, auto simp add: diff_minus left_distrib)
1.616 -end
1.617 -instantiation fps :: ("{ring_no_zero_divisors, comm_ring_1}") ring_no_zero_divisors
1.618 -begin
1.619 -
1.620 -instance
1.621 +instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
1.622  proof
1.623    fix a b :: "'a fps"
1.624    assume a0: "a \<noteq> 0" and b0: "b \<noteq> 0"
1.625    then obtain i j where i: "a\$i\<noteq>0" "\<forall>k<i. a\$k=0"
1.626      and j: "b\$j \<noteq>0" "\<forall>k<j. b\$k =0" unfolding fps_nonzero_nth_minimal
1.627      by blast+
1.628 -  have eq: "({0..i+j} -{i}) \<union> {i} = {0..i+j}" by auto
1.629 -  have d: "({0..i+j} -{i}) \<inter> {i} = {}" by auto
1.630 -  have f: "finite ({0..i+j} -{i})" "finite {i}" by auto
1.631 -  have th0: "setsum (\<lambda>k. a\$k * b\$(i+j - k)) ({0..i+j} -{i}) = 0"
1.632 -    apply (rule setsum_0')
1.633 -    apply auto
1.634 -    apply (case_tac "aa < i")
1.635 -    using i
1.636 -    apply auto
1.637 -    apply (subgoal_tac "b \$ (i+j - aa) = 0")
1.638 -    apply blast
1.639 -    apply (rule j(2)[rule_format])
1.640 -    by arith
1.641 -  have "(a*b) \$ (i+j) =  setsum (\<lambda>k. a\$k * b\$(i+j - k)) {0..i+j}"
1.642 +  have "(a * b) \$ (i+j) = (\<Sum>k=0..i+j. a\$k * b\$(i+j-k))"
1.643      by (rule fps_mult_nth)
1.644 -  hence "(a*b) \$ (i+j) = a\$i * b\$j"
1.645 -    unfolding setsum_Un_disjoint[OF f d, unfolded eq] th0 by simp
1.646 -  with i j have "(a*b) \$ (i+j) \<noteq> 0" by simp
1.647 +  also have "\<dots> = (a\$i * b\$(i+j-i)) + (\<Sum>k\<in>{0..i+j}-{i}. a\$k * b\$(i+j-k))"
1.648 +    by (rule setsum_diff1') simp_all
1.649 +  also have "(\<Sum>k\<in>{0..i+j}-{i}. a\$k * b\$(i+j-k)) = 0"
1.650 +    proof (rule setsum_0' [rule_format])
1.651 +      fix k assume "k \<in> {0..i+j} - {i}"
1.652 +      then have "k < i \<or> i+j-k < j" by auto
1.653 +      then show "a\$k * b\$(i+j-k) = 0" using i j by auto
1.654 +    qed
1.655 +  also have "a\$i * b\$(i+j-i) + 0 = a\$i * b\$j" by simp
1.656 +  also have "a\$i * b\$j \<noteq> 0" using i j by simp
1.657 +  finally have "(a*b) \$ (i+j) \<noteq> 0" .
1.658    then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast
1.659  qed
1.660 -end
1.661
1.662 -instantiation fps :: (idom) idom
1.663 -begin
1.664 -
1.665 -instance ..
1.666 -end
1.667 +instance fps :: (idom) idom ..
1.668
1.669  subsection{* Inverses of formal power series *}
1.670
1.671 @@ -456,24 +397,20 @@
1.672
1.673  definition fps_inverse_def:
1.674    "inverse f = (if f\$0 = 0 then 0 else Abs_fps (natfun_inverse f))"
1.675 -definition fps_divide_def: "divide \<equiv> (\<lambda>(f::'a fps) g. f * inverse g)"
1.676 +definition fps_divide_def: "divide = (\<lambda>(f::'a fps) g. f * inverse g)"
1.677  instance ..
1.678  end
1.679
1.680  lemma fps_inverse_zero[simp]:
1.681    "inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0"
1.682 -  by (simp add: fps_zero_def fps_inverse_def)
1.683 +  by (simp add: fps_ext fps_inverse_def)
1.684
1.685  lemma fps_inverse_one[simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1"
1.686 -  apply (auto simp add: fps_one_def fps_inverse_def expand_fun_eq)
1.687 -  by (case_tac x, auto)
1.688 +  apply (auto simp add: expand_fps_eq fps_inverse_def)
1.689 +  by (case_tac n, auto)
1.690
1.691 -instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}")  division_by_zero
1.692 -begin
1.693 -instance
1.694 -  apply (intro_classes)
1.695 -  by (rule fps_inverse_zero)
1.696 -end
1.697 +instance fps :: ("{comm_monoid_add,inverse, times, uminus}")  division_by_zero
1.698 +  by default (rule fps_inverse_zero)
1.699
1.700  lemma inverse_mult_eq_1[intro]: assumes f0: "f\$0 \<noteq> (0::'a::field)"
1.701    shows "inverse f * f = 1"
1.702 @@ -482,14 +419,14 @@
1.703    from f0 have ifn: "\<And>n. inverse f \$ n = natfun_inverse f n"
1.705    from f0 have th0: "(inverse f * f) \$ 0 = 1"
1.706 -    by (simp add: fps_inverse_def fps_one_def fps_mult_nth)
1.707 +    by (simp add: fps_mult_nth fps_inverse_def)
1.708    {fix n::nat assume np: "n >0 "
1.709      from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto
1.710      have d: "{0} \<inter> {1 .. n} = {}" by auto
1.711      have f: "finite {0::nat}" "finite {1..n}" by auto
1.712      from f0 np have th0: "- (inverse f\$n) =
1.713        (setsum (\<lambda>i. f\$i * natfun_inverse f (n - i)) {1..n}) / (f\$0)"
1.714 -      by (cases n, simp_all add: divide_inverse fps_inverse_def fps_nth_def ring_simps)
1.715 +      by (cases n, simp, simp add: divide_inverse fps_inverse_def)
1.716      from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]]
1.717      have th1: "setsum (\<lambda>i. f\$i * natfun_inverse f (n - i)) {1..n} =
1.718        - (f\$0) * (inverse f)\$n"
1.719 @@ -506,8 +443,7 @@
1.720  qed
1.721
1.722  lemma fps_inverse_0_iff[simp]: "(inverse f)\$0 = (0::'a::division_ring) \<longleftrightarrow> f\$0 = 0"
1.723 -  apply (simp add: fps_inverse_def)
1.724 -  by (metis fps_nth_def fps_nth_def inverse_zero_imp_zero)
1.725 +  by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero)
1.726
1.727  lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f \$0 = 0"
1.728  proof-
1.729 @@ -533,15 +469,14 @@
1.730    from inverse_mult_eq_1[OF f0] fg
1.731    have th0: "inverse f * f = g * f" by (simp add: mult_ac)
1.732    then show ?thesis using f0  unfolding mult_cancel_right
1.733 -    unfolding Rep_fps_eq[of f 0, symmetric]
1.734 -    by (auto simp add: fps_zero_def expand_fun_eq fps_nth_def)
1.735 +    by (auto simp add: expand_fps_eq)
1.736  qed
1.737
1.738  lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
1.739    = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
1.740    apply (rule fps_inverse_unique)
1.741    apply simp
1.742 -  apply (simp add: fps_eq_iff fps_nth_def fps_times_def fps_one_def)
1.743 +  apply (simp add: fps_eq_iff fps_mult_nth)
1.744  proof(clarsimp)
1.745    fix n::nat assume n: "n > 0"
1.746    let ?f = "\<lambda>i. if n = i then (1\<Colon>'a) else if n - i = 1 then - 1 else 0"
1.747 @@ -561,7 +496,7 @@
1.749  qed
1.750
1.751 -subsection{* Formal Derivatives, and the McLauren theorem around 0*}
1.752 +subsection{* Formal Derivatives, and the McLaurin theorem around 0*}
1.753
1.754  definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f \$ (n + 1))"
1.755
1.756 @@ -625,7 +560,7 @@
1.757  qed
1.758
1.759  lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: ('a:: comm_ring_1) fps)) = - (fps_deriv f)"
1.760 -  by (simp add: fps_uminus_def fps_eq_iff fps_deriv_def fps_nth_def)
1.761 +  by (simp add: fps_eq_iff fps_deriv_def)
1.762  lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g"
1.763    using fps_deriv_linear[of 1 f 1 g] by simp
1.764
1.765 @@ -633,7 +568,7 @@
1.766    unfolding diff_minus by simp
1.767
1.768  lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
1.769 -  by (simp add: fps_deriv_def fps_const_def fps_zero_def)
1.770 +  by (simp add: fps_ext fps_deriv_def fps_const_def)
1.771
1.772  lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
1.773    by simp
1.774 @@ -772,7 +707,7 @@
1.775  qed
1.776
1.777  lemma fps_power_zeroth_eq_one: "a\$0 =1 \<Longrightarrow> a^n \$ 0 = (1::'a::semiring_1)"
1.778 -  by (induct n, auto simp add: fps_power_def fps_times_def fps_nth_def fps_one_def)
1.779 +  by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
1.780
1.781  lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)\$0 =1 \<Longrightarrow> a^n \$ 1 = of_nat n * a\$1"
1.782  proof(induct n)
1.783 @@ -954,7 +889,7 @@
1.784
1.785  lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
1.786    = 1 - X"
1.787 -  by (simp add: fps_inverse_gp fps_eq_iff X_def fps_minus_def fps_one_def)
1.788 +  by (simp add: fps_inverse_gp fps_eq_iff X_def)
1.789
1.790  lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))"
1.791  proof-
1.792 @@ -1684,7 +1619,7 @@
1.793  	then have "a\$n = ?r \$n"
1.794  	  apply (simp del: of_nat_Suc)
1.796 -	  by (simp add: field_simps n1 fps_nth_def th00 del: of_nat_Suc)}
1.797 +	  by (simp add: field_simps n1 th00 del: of_nat_Suc)}
1.798  	ultimately show "a\$n = ?r \$ n" by (cases n, auto)
1.799        qed}
1.800      then have "a = ?r" by (simp add: fps_eq_iff)}
1.801 @@ -1935,7 +1870,7 @@
1.802  	have "?i \$ n = setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + fps_inv a \$ Suc n1 * (a \$ 1)^ Suc n1"
1.803  	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
1.804  	also have "\<dots> = setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + (X\$ Suc n1 - setsum (\<lambda>i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1})"
1.805 -	  using a0 a1 n1 by (simp add: fps_inv_def fps_nth_def)
1.806 +	  using a0 a1 n1 by (simp add: fps_inv_def)
1.807  	also have "\<dots> = X\$n" using n1 by simp
1.808  	finally have "?i \$ n = X\$n" .}
1.809        ultimately show "?i \$ n = X\$n" by (cases n, auto)
1.810 @@ -1965,7 +1900,7 @@
1.811  	have "?i \$ n = setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + fps_ginv b a \$ Suc n1 * (a \$ 1)^ Suc n1"
1.812  	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
1.813  	also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + (b\$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1})"
1.814 -	  using a0 a1 n1 by (simp add: fps_ginv_def fps_nth_def)
1.815 +	  using a0 a1 n1 by (simp add: fps_ginv_def)
1.816  	also have "\<dots> = b\$n" using n1 by simp
1.817  	finally have "?i \$ n = b\$n" .}
1.818        ultimately show "?i \$ n = b\$n" by (cases n, auto)
1.819 @@ -2092,7 +2027,7 @@
1.820    let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})"
1.821    have th0: "?KM = UNION {0..n} ?f"
1.823 -    apply arith
1.824 +    apply arith (* FIXME: VERY slow! *)
1.825      done
1.826    show "?l = ?r "
1.827      unfolding th0
1.828 @@ -2399,7 +2334,7 @@
1.829    (is "?lhs = ?rhs")
1.830  proof-
1.831    have th0: "\<And>n. - ((- 1::'a) ^ n) = (- 1)^Suc n" by (simp add: power_Suc)
1.832 -  have th1: "\<And>n. odd n\<Longrightarrow> Suc ((n - 1) div 2) = Suc n div 2" by presburger
1.833 +  have th1: "\<And>n. odd n\<Longrightarrow> Suc ((n - 1) div 2) = Suc n div 2" by presburger (* FIXME: VERY slow! *)
1.834    {fix n::nat
1.835      {assume en: "odd n"
1.836        from en have n0: "n \<noteq>0 " by presburger
1.837 @@ -2414,10 +2349,10 @@
1.838        also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)"
1.839  	unfolding th0 unfolding th1[OF en] by simp
1.840        finally have "?lhs \$n = ?rhs\$n" using en
1.841 -	by (simp add: fps_sin_def fps_uminus_def ring_simps power_Suc)}
1.842 +	by (simp add: fps_sin_def ring_simps power_Suc)}
1.843      then have "?lhs \$ n = ?rhs \$ n"
1.844        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def
1.845 -	fps_cos_def fps_uminus_def) }
1.846 +	fps_cos_def) }
1.847    then show ?thesis by (auto simp add: fps_eq_iff)
1.848  qed
1.849
1.850 @@ -2430,7 +2365,7 @@
1.851    then have "?lhs = fps_const (?lhs \$ 0)"
1.852      unfolding fps_deriv_eq_0_iff .
1.853    also have "\<dots> = 1"
1.854 -    by (auto simp add: fps_eq_iff fps_power_def nat_number fps_mult_nth fps_cos_def fps_sin_def)
1.855 +    by (auto simp add: fps_eq_iff fps_power_def numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
1.856    finally show ?thesis .
1.857  qed
1.858
1.859 @@ -2445,4 +2380,5 @@
1.860      unfolding right_distrib[symmetric]
1.861      by simp
1.862  qed
1.863 -end
1.864 \ No newline at end of file
1.865 +
1.866 +end
```