src/HOL/Library/Formal_Power_Series.thy
changeset 36350 bc7982c54e37
parent 36311 ed3a87a7f977
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -588,7 +588,7 @@
     1.4    from k have "real k > - log y x" by simp
     1.5    then have "ln y * real k > - ln x" unfolding log_def
     1.6      using ln_gt_zero_iff[OF yp] y1
     1.7 -    by (simp add: minus_divide_left field_simps field_eq_simps del:minus_divide_left[symmetric])
     1.8 +    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric])
     1.9    then have "ln y * real k + ln x > 0" by simp
    1.10    then have "exp (real k * ln y + ln x) > exp 0"
    1.11      by (simp add: mult_ac)
    1.12 @@ -596,7 +596,7 @@
    1.13      unfolding exp_zero exp_add exp_real_of_nat_mult
    1.14      exp_ln[OF xp] exp_ln[OF yp] by simp
    1.15    then have "x > (1/y)^k" using yp 
    1.16 -    by (simp add: field_simps field_eq_simps nonzero_power_divide)
    1.17 +    by (simp add: field_simps nonzero_power_divide)
    1.18    then show ?thesis using kp by blast
    1.19  qed
    1.20  lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
    1.21 @@ -693,7 +693,7 @@
    1.22      from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]]
    1.23      have th1: "setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n} =
    1.24        - (f$0) * (inverse f)$n"
    1.25 -      by (simp add: ring_simps)
    1.26 +      by (simp add: field_simps)
    1.27      have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n - i))"
    1.28        unfolding fps_mult_nth ifn ..
    1.29      also have "\<dots> = f$0 * natfun_inverse f n
    1.30 @@ -766,7 +766,7 @@
    1.31  lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def)
    1.32  
    1.33  lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g"
    1.34 -  unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: ring_simps)
    1.35 +  unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
    1.36  
    1.37  lemma fps_deriv_mult[simp]:
    1.38    fixes f :: "('a :: comm_ring_1) fps"
    1.39 @@ -817,7 +817,7 @@
    1.40        unfolding s0 s1
    1.41        unfolding setsum_addf[symmetric] setsum_right_distrib
    1.42        apply (rule setsum_cong2)
    1.43 -      by (auto simp add: of_nat_diff ring_simps)
    1.44 +      by (auto simp add: of_nat_diff field_simps)
    1.45      finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" .}
    1.46    then show ?thesis unfolding fps_eq_iff by auto
    1.47  qed
    1.48 @@ -878,7 +878,7 @@
    1.49  proof-
    1.50    have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0" by simp
    1.51    also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)" unfolding fps_deriv_eq_0_iff ..
    1.52 -  finally show ?thesis by (simp add: ring_simps)
    1.53 +  finally show ?thesis by (simp add: field_simps)
    1.54  qed
    1.55  
    1.56  lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
    1.57 @@ -929,7 +929,7 @@
    1.58  qed
    1.59  
    1.60  lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
    1.61 -  by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult)
    1.62 +  by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
    1.63  
    1.64  subsection {* Powers*}
    1.65  
    1.66 @@ -943,7 +943,7 @@
    1.67    case (Suc n)
    1.68    note h = Suc.hyps[OF `a$0 = 1`]
    1.69    show ?case unfolding power_Suc fps_mult_nth
    1.70 -    using h `a$0 = 1`  fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: ring_simps)
    1.71 +    using h `a$0 = 1`  fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: field_simps)
    1.72  qed
    1.73  
    1.74  lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
    1.75 @@ -1005,7 +1005,7 @@
    1.76    case 0 thus ?case by (simp add: power_0)
    1.77  next
    1.78    case (Suc n)
    1.79 -  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: ring_simps power_Suc)
    1.80 +  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: field_simps power_Suc)
    1.81    also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth)
    1.82    also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {n .. Suc n}"
    1.83      apply (rule setsum_mono_zero_right)
    1.84 @@ -1045,8 +1045,8 @@
    1.85  qed
    1.86  
    1.87  lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
    1.88 -  apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add)
    1.89 -  by (case_tac n, auto simp add: power_Suc ring_simps)
    1.90 +  apply (induct n, auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
    1.91 +  by (case_tac n, auto simp add: power_Suc field_simps)
    1.92  
    1.93  lemma fps_inverse_deriv:
    1.94    fixes a:: "('a :: field) fps"
    1.95 @@ -1060,11 +1060,11 @@
    1.96    with inverse_mult_eq_1[OF a0]
    1.97    have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
    1.98      unfolding power2_eq_square
    1.99 -    apply (simp add: ring_simps)
   1.100 +    apply (simp add: field_simps)
   1.101      by (simp add: mult_assoc[symmetric])
   1.102    hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 = 0 - fps_deriv a * inverse a ^ 2"
   1.103      by simp
   1.104 -  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: ring_simps)
   1.105 +  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: field_simps)
   1.106  qed
   1.107  
   1.108  lemma fps_inverse_mult:
   1.109 @@ -1084,7 +1084,7 @@
   1.110      from inverse_mult_eq_1[OF ab0]
   1.111      have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp
   1.112      then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b"
   1.113 -      by (simp add: ring_simps)
   1.114 +      by (simp add: field_simps)
   1.115      then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp}
   1.116  ultimately show ?thesis by blast
   1.117  qed
   1.118 @@ -1105,7 +1105,7 @@
   1.119    assumes a0: "b$0 \<noteq> 0"
   1.120    shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
   1.121    using fps_inverse_deriv[OF a0]
   1.122 -  by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
   1.123 +  by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
   1.124  
   1.125  
   1.126  lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
   1.127 @@ -1121,7 +1121,7 @@
   1.128  proof-
   1.129    have eq: "(1 + X) * ?r = 1"
   1.130      unfolding minus_one_power_iff
   1.131 -    by (auto simp add: ring_simps fps_eq_iff)
   1.132 +    by (auto simp add: field_simps fps_eq_iff)
   1.133    show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
   1.134  qed
   1.135  
   1.136 @@ -1185,7 +1185,7 @@
   1.137      next
   1.138        case (Suc k)
   1.139        note th = Suc.hyps[symmetric]
   1.140 -      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps)
   1.141 +      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: field_simps)
   1.142        also  have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
   1.143          using th
   1.144          unfolding fps_sub_nth by simp
   1.145 @@ -1209,10 +1209,10 @@
   1.146  definition "XD = op * X o fps_deriv"
   1.147  
   1.148  lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)"
   1.149 -  by (simp add: XD_def ring_simps)
   1.150 +  by (simp add: XD_def field_simps)
   1.151  
   1.152  lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
   1.153 -  by (simp add: XD_def ring_simps)
   1.154 +  by (simp add: XD_def field_simps)
   1.155  
   1.156  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.157    by simp
   1.158 @@ -1226,7 +1226,7 @@
   1.159  
   1.160  lemma fps_mult_XD_shift:
   1.161    "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   1.162 -  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   1.163 +  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff field_simps del: One_nat_def)
   1.164  
   1.165  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   1.166  subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
   1.167 @@ -1688,7 +1688,7 @@
   1.168          then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
   1.169            by (simp add: natpermute_max_card[OF nz, simplified])
   1.170          also have "\<dots> = a$n - setsum ?f ?Pnknn"
   1.171 -          unfolding n1 using r00 a0 by (simp add: field_eq_simps fps_radical_def del: of_nat_Suc)
   1.172 +          unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc)
   1.173          finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
   1.174          have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
   1.175            unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] ..
   1.176 @@ -1764,7 +1764,7 @@
   1.177    shows "a = b / c"
   1.178  proof-
   1.179    from eq have "a * c * inverse c = b * inverse c" by simp
   1.180 -  hence "a * (inverse c * c) = b/c" by (simp only: field_eq_simps divide_inverse)
   1.181 +  hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse)
   1.182    then show "a = b/c" unfolding  field_inverse[OF c0] by simp
   1.183  qed
   1.184  
   1.185 @@ -1837,7 +1837,7 @@
   1.186            show "a$(xs !i) = ?r$(xs!i)" .
   1.187          qed
   1.188          have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
   1.189 -          by (simp add: field_eq_simps del: of_nat_Suc)
   1.190 +          by (simp add: field_simps del: of_nat_Suc)
   1.191          from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
   1.192          also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
   1.193            unfolding fps_power_nth_Suc
   1.194 @@ -1854,7 +1854,7 @@
   1.195          then have "a$n = ?r $n"
   1.196            apply (simp del: of_nat_Suc)
   1.197            unfolding fps_radical_def n1
   1.198 -          by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)}
   1.199 +          by (simp add: field_simps n1 th00 del: of_nat_Suc)}
   1.200          ultimately show "a$n = ?r $ n" by (cases n, auto)
   1.201        qed}
   1.202      then have "a = ?r" by (simp add: fps_eq_iff)}
   1.203 @@ -2018,11 +2018,11 @@
   1.204  proof-
   1.205    {fix n
   1.206      have "(fps_deriv (a oo b))$n = setsum (\<lambda>i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}"
   1.207 -      by (simp add: fps_compose_def ring_simps setsum_right_distrib del: of_nat_Suc)
   1.208 +      by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc)
   1.209      also have "\<dots> = setsum (\<lambda>i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}"
   1.210 -      by (simp add: ring_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc)
   1.211 +      by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc)
   1.212    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}"
   1.213 -    unfolding fps_mult_left_const_nth  by (simp add: ring_simps)
   1.214 +    unfolding fps_mult_left_const_nth  by (simp add: field_simps)
   1.215    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}"
   1.216      unfolding fps_mult_nth ..
   1.217    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}"
   1.218 @@ -2170,7 +2170,7 @@
   1.219    by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0')
   1.220  
   1.221  lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
   1.222 -  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
   1.223 +  by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_addf)
   1.224  
   1.225  lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
   1.226  proof-
   1.227 @@ -2212,7 +2212,7 @@
   1.228      apply (simp add: fps_mult_nth setsum_right_distrib)
   1.229      apply (subst setsum_commute)
   1.230      apply (rule setsum_cong2)
   1.231 -    by (auto simp add: ring_simps)
   1.232 +    by (auto simp add: field_simps)
   1.233    also have "\<dots> = ?l"
   1.234      apply (simp add: fps_mult_nth fps_compose_nth setsum_product)
   1.235      apply (rule setsum_cong2)
   1.236 @@ -2312,7 +2312,7 @@
   1.237  qed
   1.238  
   1.239  lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
   1.240 -  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric])
   1.241 +  by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric])
   1.242  
   1.243  lemma fps_compose_sub_distrib:
   1.244    shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   1.245 @@ -2469,7 +2469,7 @@
   1.246  proof-
   1.247    let ?r = "fps_inv"
   1.248    have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
   1.249 -  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_eq_simps)
   1.250 +  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
   1.251    have X0: "X$0 = 0" by simp
   1.252    from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
   1.253    then have "?r (?r a) oo ?r a oo a = X oo a" by simp
   1.254 @@ -2486,7 +2486,7 @@
   1.255  proof-
   1.256    let ?r = "fps_ginv"
   1.257    from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
   1.258 -  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_eq_simps)
   1.259 +  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
   1.260    from fps_ginv[OF rca0 rca1] 
   1.261    have "?r b (?r c a) oo ?r c a = b" .
   1.262    then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
   1.263 @@ -2534,8 +2534,8 @@
   1.264  proof-
   1.265    {fix n
   1.266      have "?l$n = ?r $ n"
   1.267 -  apply (auto simp add: E_def field_eq_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   1.268 -  by (simp add: of_nat_mult ring_simps)}
   1.269 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   1.270 +  by (simp add: of_nat_mult field_simps)}
   1.271  then show ?thesis by (simp add: fps_eq_iff)
   1.272  qed
   1.273  
   1.274 @@ -2545,15 +2545,15 @@
   1.275  proof-
   1.276    {assume d: ?lhs
   1.277    from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
   1.278 -    by (simp add: fps_deriv_def fps_eq_iff field_eq_simps del: of_nat_Suc)
   1.279 +    by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
   1.280    {fix n have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
   1.281        apply (induct n)
   1.282        apply simp
   1.283        unfolding th
   1.284        using fact_gt_zero_nat
   1.285 -      apply (simp add: field_eq_simps del: of_nat_Suc fact_Suc)
   1.286 +      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
   1.287        apply (drule sym)
   1.288 -      by (simp add: ring_simps of_nat_mult power_Suc)}
   1.289 +      by (simp add: field_simps of_nat_mult power_Suc)}
   1.290    note th' = this
   1.291    have ?rhs
   1.292      by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')}
   1.293 @@ -2570,7 +2570,7 @@
   1.294  lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
   1.295  proof-
   1.296    have "fps_deriv (?r) = fps_const (a+b) * ?r"
   1.297 -    by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
   1.298 +    by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
   1.299    then have "?r = ?l" apply (simp only: E_unique_ODE)
   1.300      by (simp add: fps_mult_nth E_def)
   1.301    then show ?thesis ..
   1.302 @@ -2618,13 +2618,13 @@
   1.303    (is "inverse ?l = ?r")
   1.304  proof-
   1.305    have th: "?l * ?r = 1"
   1.306 -    by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff)
   1.307 +    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
   1.308    have th': "?l $ 0 \<noteq> 0" by (simp add: )
   1.309    from fps_inverse_unique[OF th' th] show ?thesis .
   1.310  qed
   1.311  
   1.312  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
   1.313 -  by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
   1.314 +  by (induct n, auto simp add: field_simps E_add_mult power_Suc)
   1.315  
   1.316  lemma radical_E:
   1.317    assumes r: "r (Suc k) 1 = 1" 
   1.318 @@ -2649,18 +2649,18 @@
   1.319  text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
   1.320  
   1.321  lemma gbinomial_theorem: 
   1.322 -  "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   1.323 +  "((a::'a::{field_char_0, division_ring_inverse_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   1.324  proof-
   1.325    from E_add_mult[of a b] 
   1.326    have "(E (a + b)) $ n = (E a * E b)$n" by simp
   1.327    then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
   1.328 -    by (simp add: field_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   1.329 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   1.330    then show ?thesis 
   1.331      apply simp
   1.332      apply (rule setsum_cong2)
   1.333      apply simp
   1.334      apply (frule binomial_fact[where ?'a = 'a, symmetric])
   1.335 -    by (simp add: field_eq_simps of_nat_mult)
   1.336 +    by (simp add: field_simps of_nat_mult)
   1.337  qed
   1.338  
   1.339  text{* And the nat-form -- also available from Binomial.thy *}
   1.340 @@ -2683,7 +2683,7 @@
   1.341    by (simp add: L_def fps_eq_iff del: of_nat_Suc)
   1.342  
   1.343  lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   1.344 -  by (simp add: L_def field_eq_simps)
   1.345 +  by (simp add: L_def field_simps)
   1.346  
   1.347  lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
   1.348  lemma L_E_inv:
   1.349 @@ -2694,9 +2694,9 @@
   1.350    have b0: "?b $ 0 = 0" by simp
   1.351    have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
   1.352    have "fps_deriv (E a - 1) oo fps_inv (E a - 1) = (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)"
   1.353 -    by (simp add: ring_simps)
   1.354 +    by (simp add: field_simps)
   1.355    also have "\<dots> = fps_const a * (X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
   1.356 -    by (simp add: ring_simps)
   1.357 +    by (simp add: field_simps)
   1.358    finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
   1.359    from fps_inv_deriv[OF b0 b1, unfolded eq]
   1.360    have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
   1.361 @@ -2713,7 +2713,7 @@
   1.362    shows "L c + L d = fps_const (c+d) * L (c*d)"
   1.363    (is "?r = ?l")
   1.364  proof-
   1.365 -  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_eq_simps)
   1.366 +  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
   1.367    have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
   1.368      by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
   1.369    also have "\<dots> = fps_deriv ?l"
   1.370 @@ -2743,7 +2743,7 @@
   1.371    have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
   1.372    also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
   1.373      apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
   1.374 -    by (simp add: ring_simps)
   1.375 +    by (simp add: field_simps)
   1.376    finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
   1.377    moreover
   1.378    {assume h: "?l = ?r" 
   1.379 @@ -2752,8 +2752,8 @@
   1.380        
   1.381        from lrn 
   1.382        have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
   1.383 -        apply (simp add: ring_simps del: of_nat_Suc)
   1.384 -        by (cases n, simp_all add: field_eq_simps del: of_nat_Suc)
   1.385 +        apply (simp add: field_simps del: of_nat_Suc)
   1.386 +        by (cases n, simp_all add: field_simps del: of_nat_Suc)
   1.387      }
   1.388      note th0 = this
   1.389      {fix n have "a$n = (c gchoose n) * a$0"
   1.390 @@ -2762,24 +2762,24 @@
   1.391        next
   1.392          case (Suc m)
   1.393          thus ?case unfolding th0
   1.394 -          apply (simp add: field_eq_simps del: of_nat_Suc)
   1.395 +          apply (simp add: field_simps del: of_nat_Suc)
   1.396            unfolding mult_assoc[symmetric] gbinomial_mult_1
   1.397 -          by (simp add: ring_simps)
   1.398 +          by (simp add: field_simps)
   1.399        qed}
   1.400      note th1 = this
   1.401      have ?rhs
   1.402        apply (simp add: fps_eq_iff)
   1.403        apply (subst th1)
   1.404 -      by (simp add: ring_simps)}
   1.405 +      by (simp add: field_simps)}
   1.406    moreover
   1.407    {assume h: ?rhs
   1.408    have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
   1.409      have "?l = ?r" 
   1.410        apply (subst h)
   1.411        apply (subst (2) h)
   1.412 -      apply (clarsimp simp add: fps_eq_iff ring_simps)
   1.413 +      apply (clarsimp simp add: fps_eq_iff field_simps)
   1.414        unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
   1.415 -      by (simp add: ring_simps gbinomial_mult_1)}
   1.416 +      by (simp add: field_simps gbinomial_mult_1)}
   1.417    ultimately show ?thesis by blast
   1.418  qed
   1.419  
   1.420 @@ -2798,9 +2798,9 @@
   1.421    have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   1.422    also have "\<dots> = inverse (1 + X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))"
   1.423      unfolding fps_binomial_deriv
   1.424 -    by (simp add: fps_divide_def ring_simps)
   1.425 +    by (simp add: fps_divide_def field_simps)
   1.426    also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   1.427 -    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   1.428 +    by (simp add: field_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   1.429    finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   1.430      by (simp add: fps_divide_def)
   1.431    have "?P = fps_const (?P$0) * ?b (c + d)"
   1.432 @@ -2880,7 +2880,7 @@
   1.433            using kn pochhammer_minus'[where k=k and n=n and b=b]
   1.434            apply (simp add:  pochhammer_same)
   1.435            using bn0
   1.436 -          by (simp add: field_eq_simps power_add[symmetric])}
   1.437 +          by (simp add: field_simps power_add[symmetric])}
   1.438        moreover
   1.439        {assume nk: "k \<noteq> n"
   1.440          have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" 
   1.441 @@ -2905,7 +2905,7 @@
   1.442            unfolding m1nk 
   1.443            
   1.444            unfolding m h pochhammer_Suc_setprod
   1.445 -          apply (simp add: field_eq_simps del: fact_Suc id_def)
   1.446 +          apply (simp add: field_simps del: fact_Suc id_def)
   1.447            unfolding fact_altdef_nat id_def
   1.448            unfolding of_nat_setprod
   1.449            unfolding setprod_timesf[symmetric]
   1.450 @@ -2942,10 +2942,10 @@
   1.451            apply auto
   1.452            done
   1.453          then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}" 
   1.454 -          using nz' by (simp add: field_eq_simps)
   1.455 +          using nz' by (simp add: field_simps)
   1.456          have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
   1.457            using bnz0
   1.458 -          by (simp add: field_eq_simps)
   1.459 +          by (simp add: field_simps)
   1.460          also have "\<dots> = b gchoose (n - k)" 
   1.461            unfolding th1 th2
   1.462            using kn' by (simp add: gbinomial_def)
   1.463 @@ -2959,15 +2959,15 @@
   1.464    note th00 = this
   1.465    have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
   1.466      unfolding gbinomial_pochhammer 
   1.467 -    using bn0 by (auto simp add: field_eq_simps)
   1.468 +    using bn0 by (auto simp add: field_simps)
   1.469    also have "\<dots> = ?l"
   1.470      unfolding gbinomial_Vandermonde[symmetric]
   1.471      apply (simp add: th00)
   1.472      unfolding gbinomial_pochhammer
   1.473 -    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_eq_simps)
   1.474 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
   1.475      apply (rule setsum_cong2)
   1.476      apply (drule th00(2))
   1.477 -    by (simp add: field_eq_simps power_add[symmetric])
   1.478 +    by (simp add: field_simps power_add[symmetric])
   1.479    finally show ?thesis by simp
   1.480  qed 
   1.481  
   1.482 @@ -2992,7 +2992,7 @@
   1.483    have nz: "pochhammer c n \<noteq> 0" using c
   1.484      by (simp add: pochhammer_eq_0_iff)
   1.485    from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
   1.486 -  show ?thesis using nz by (simp add: field_eq_simps setsum_right_distrib)
   1.487 +  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
   1.488  qed
   1.489  
   1.490  subsubsection{* Formal trigonometric functions  *}
   1.491 @@ -3014,11 +3014,11 @@
   1.492          using en by (simp add: fps_sin_def)
   1.493        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   1.494          unfolding fact_Suc of_nat_mult
   1.495 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   1.496 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   1.497        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
   1.498 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   1.499 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   1.500        finally have "?lhs $n = ?rhs$n" using en
   1.501 -        by (simp add: fps_cos_def ring_simps power_Suc )}
   1.502 +        by (simp add: fps_cos_def field_simps power_Suc )}
   1.503      then show "?lhs $ n = ?rhs $ n"
   1.504        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def)
   1.505  qed
   1.506 @@ -3038,13 +3038,13 @@
   1.507          using en by (simp add: fps_cos_def)
   1.508        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   1.509          unfolding fact_Suc of_nat_mult
   1.510 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   1.511 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   1.512        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
   1.513 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   1.514 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   1.515        also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)"
   1.516          unfolding th0 unfolding th1[OF en] by simp
   1.517        finally have "?lhs $n = ?rhs$n" using en
   1.518 -        by (simp add: fps_sin_def ring_simps power_Suc)}
   1.519 +        by (simp add: fps_sin_def field_simps power_Suc)}
   1.520      then show "?lhs $ n = ?rhs $ n"
   1.521        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def
   1.522          fps_cos_def)
   1.523 @@ -3055,7 +3055,7 @@
   1.524  proof-
   1.525    have "fps_deriv ?lhs = 0"
   1.526      apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc)
   1.527 -    by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg)
   1.528 +    by (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
   1.529    then have "?lhs = fps_const (?lhs $ 0)"
   1.530      unfolding fps_deriv_eq_0_iff .
   1.531    also have "\<dots> = 1"
   1.532 @@ -3177,7 +3177,7 @@
   1.533    have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)
   1.534    show ?thesis
   1.535      using fps_sin_cos_sum_of_squares[of c]
   1.536 -    apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] ring_simps power2_eq_square del: fps_const_neg)
   1.537 +    apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] field_simps power2_eq_square del: fps_const_neg)
   1.538      unfolding right_distrib[symmetric]
   1.539      by simp
   1.540  qed
   1.541 @@ -3252,7 +3252,7 @@
   1.542  subsection {* Hypergeometric series *}
   1.543  
   1.544  
   1.545 -definition "F as bs (c::'a::{field_char_0, division_by_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   1.546 +definition "F as bs (c::'a::{field_char_0, division_ring_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   1.547  
   1.548  lemma F_nth[simp]: "F as bs c $ n =  (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
   1.549    by (simp add: F_def)
   1.550 @@ -3321,9 +3321,9 @@
   1.551    by (simp add: fps_eq_iff fps_integral_def)
   1.552  
   1.553  lemma F_minus_nat: 
   1.554 -  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
   1.555 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
   1.556      (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
   1.557 -  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_by_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
   1.558 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
   1.559      (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
   1.560    by (auto simp add: pochhammer_eq_0_iff)
   1.561