src/HOL/Library/Formal_Power_Series.thy
changeset 29689 dd086f26ee4f
parent 29687 4d934a895d11
child 29692 121289b1ae27
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jan 29 14:56:29 2009 +0000
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jan 29 15:29:41 2009 +0000
     1.3 @@ -1100,17 +1100,12 @@
     1.4  lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)"
     1.5    by simp
     1.6  
     1.7 -
     1.8 -fun funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.9 -  "funpow 0 f = id"
    1.10 -  | "funpow (Suc n) f = f o funpow n f"
    1.11 -
    1.12 -lemma XDN_linear: "(funpow n XD) (fps_const c * a + fps_const d * b) = fps_const c * (funpow n XD) a + fps_const d * (funpow n XD) (b :: ('a::comm_ring_1) fps)"
    1.13 +lemma XDN_linear: "(XD^n) (fps_const c * a + fps_const d * b) = fps_const c * (XD^n) a + fps_const d * (XD^n) (b :: ('a::comm_ring_1) fps)"
    1.14    by (induct n, simp_all)
    1.15  
    1.16  lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff)
    1.17  
    1.18 -lemma fps_mult_XD_shift: "funpow k XD (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
    1.19 +lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
    1.20  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
    1.21  
    1.22  subsection{* Rule 3 is trivial and is given by fps_times_def*}