declare fps_nth as a typedef morphism; clean up instance proofs
authorhuffman
Sat Feb 14 11:11:30 2009 -0800 (2009-02-14)
changeset 29911c790a70a3d19
parent 29910 623c9c20966b
child 29912 f4ac160d2e77
declare fps_nth as a typedef morphism; clean up instance proofs
src/HOL/Library/Formal_Power_Series.thy
     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.140 -instantiation fps :: (semigroup_add) semigroup_add
   1.141 -begin
   1.142 -
   1.143 -instance
   1.144 +instance fps :: (semigroup_add) semigroup_add
   1.145  proof
   1.146    fix a b c :: "'a fps" show "a + b + c = a + (b + c)"
   1.147 -    by (auto simp add: fps_plus_def expand_fun_eq add_assoc)
   1.148 +    by (simp add: fps_ext add_assoc)
   1.149 +qed
   1.150 +
   1.151 +instance fps :: (ab_semigroup_add) ab_semigroup_add
   1.152 +proof
   1.153 +  fix a b :: "'a fps" show "a + b = b + a"
   1.154 +    by (simp add: fps_ext add_commute)
   1.155  qed
   1.156  
   1.157 -end
   1.158 -
   1.159 -instantiation fps :: (ab_semigroup_add) ab_semigroup_add
   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.169 +    by (simp add: Suc_diff_le setsum_addf add_assoc
   1.170 +             cong: strong_setsum_cong)
   1.171 +qed
   1.172  
   1.173 -instance by (intro_classes, simp add: fps_plus_def expand_fun_eq add_commute)
   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.223 -      by (simp add: add_ac mult_assoc)
   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.284 -instantiation fps :: (monoid_add) monoid_add
   1.285 -begin
   1.286 -
   1.287 -instance
   1.288 +instance fps :: (monoid_add) monoid_add
   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.300 -instantiation fps :: (comm_monoid_add) comm_monoid_add
   1.301 -begin
   1.302 -
   1.303 -instance
   1.304 +instance fps :: (comm_monoid_add) comm_monoid_add
   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.340 -instantiation fps :: (cancel_semigroup_add) cancel_semigroup_add
   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.345 +instance fps :: (cancel_semigroup_add) cancel_semigroup_add
   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.356 -instantiation fps :: (group_add) group_add
   1.357 -begin
   1.358 +instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
   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.366 +instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
   1.367 +
   1.368 +instance fps :: (group_add) group_add
   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.383 -subclass group_add proof qed
   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.391 +instance fps :: (ab_group_add) ab_group_add
   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.413 -    unfolding setsum_addf[symmetric]
   1.414 -    apply (simp add: ring_simps)
   1.415 -    done
   1.416 +  show "(a + b) * c = a * c + b * c"
   1.417 +    by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf)
   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.422 -    unfolding setsum_addf[symmetric]
   1.423 -    apply (simp add: ring_simps)
   1.424 -    done
   1.425 +  show "a * (b + c) = a * b + a * c"
   1.426 +    by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf)
   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.569 -  unfolding fps_eq_iff fps_add_nth by (simp add: fps_const_def)
   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.573 -  unfolding fps_eq_iff fps_add_nth by (simp add: fps_const_def)
   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.704      by (simp add: fps_inverse_def)
   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.748      by(simp add: setsum_delta)
   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.795  	  unfolding fps_radical_def n1
   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.822      apply (simp add: expand_set_eq)
   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