src/HOL/Library/Formal_Power_Series.thy
changeset 32042 df28ead1cf19
parent 31968 0314441a53a6
child 32047 c141f139ce26
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 10 12:55:06 2009 -0400
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Jul 14 20:58:53 2009 -0400
     1.3 @@ -2514,7 +2514,7 @@
     1.4  proof-
     1.5    {fix n
     1.6      have "?l$n = ?r $ n"
     1.7 -  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
     1.8 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
     1.9    by (simp add: of_nat_mult ring_simps)}
    1.10  then show ?thesis by (simp add: fps_eq_iff)
    1.11  qed
    1.12 @@ -2530,8 +2530,8 @@
    1.13        apply (induct n)
    1.14        apply simp
    1.15        unfolding th
    1.16 -      using fact_gt_zero
    1.17 -      apply (simp add: field_simps del: of_nat_Suc fact.simps)
    1.18 +      using fact_gt_zero_nat
    1.19 +      apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
    1.20        apply (drule sym)
    1.21        by (simp add: ring_simps of_nat_mult power_Suc)}
    1.22    note th' = this
    1.23 @@ -2697,7 +2697,7 @@
    1.24        also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
    1.25  	using en by (simp add: fps_sin_def)
    1.26        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    1.27 -	unfolding fact_Suc of_nat_mult
    1.28 +	unfolding fact_Suc_nat of_nat_mult
    1.29  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    1.30        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
    1.31  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    1.32 @@ -2721,7 +2721,7 @@
    1.33        also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
    1.34  	using en by (simp add: fps_cos_def)
    1.35        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    1.36 -	unfolding fact_Suc of_nat_mult
    1.37 +	unfolding fact_Suc_nat of_nat_mult
    1.38  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    1.39        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
    1.40  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    1.41 @@ -2747,9 +2747,6 @@
    1.42    finally show ?thesis .
    1.43  qed
    1.44  
    1.45 -lemma fact_1 [simp]: "fact 1 = 1"
    1.46 -unfolding One_nat_def fact_Suc by simp
    1.47 -
    1.48  lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
    1.49  by auto
    1.50  
    1.51 @@ -2766,7 +2763,7 @@
    1.52    "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
    1.53  unfolding fps_sin_def
    1.54  apply (cases n, simp)
    1.55 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    1.56 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    1.57  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    1.58  done
    1.59  
    1.60 @@ -2779,7 +2776,7 @@
    1.61  lemma fps_cos_nth_add_2:
    1.62    "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
    1.63  unfolding fps_cos_def
    1.64 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    1.65 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    1.66  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    1.67  done
    1.68