dropped group_simps, ring_simps, field_eq_simps
authorhaftmann
Mon Apr 26 11:34:19 2010 +0200 (2010-04-26)
changeset 36350bc7982c54e37
parent 36349 39be26d1bc28
child 36351 85ee44388f7b
child 36409 d323e7773aa8
dropped group_simps, ring_simps, field_eq_simps
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/GCD.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/SMT/Tools/z3_proof_rules.ML
src/HOL/SMT/Z3.thy
src/HOL/SetInterval.thy
src/HOL/ex/Lagrange.thy
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -283,11 +283,11 @@
     1.4  apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
     1.5  apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
     1.6  apply (drule_tac x = "Suc (length q)" in spec)
     1.7 -apply (auto simp add: ring_simps)
     1.8 +apply (auto simp add: field_simps)
     1.9  apply (drule_tac x = xa in spec)
    1.10 -apply (clarsimp simp add: ring_simps)
    1.11 +apply (clarsimp simp add: field_simps)
    1.12  apply (drule_tac x = m in spec)
    1.13 -apply (auto simp add:ring_simps)
    1.14 +apply (auto simp add:field_simps)
    1.15  done
    1.16  lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard]
    1.17  
    1.18 @@ -327,7 +327,7 @@
    1.19  apply (drule_tac x = "a#i" in spec)
    1.20  apply (auto simp only: poly_mult List.list.size)
    1.21  apply (drule_tac x = xa in spec)
    1.22 -apply (clarsimp simp add: ring_simps)
    1.23 +apply (clarsimp simp add: field_simps)
    1.24  done
    1.25  
    1.26  lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
    1.27 @@ -413,7 +413,7 @@
    1.28  by (auto intro!: ext)
    1.29  
    1.30  lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
    1.31 -by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult)
    1.32 +by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
    1.33  
    1.34  lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
    1.35  by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
     2.1 --- a/src/HOL/GCD.thy	Mon Apr 26 11:34:17 2010 +0200
     2.2 +++ b/src/HOL/GCD.thy	Mon Apr 26 11:34:19 2010 +0200
     2.3 @@ -1034,11 +1034,11 @@
     2.4      thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
     2.5        apply (simp add: bezw_non_0 gcd_non_0_nat)
     2.6        apply (erule subst)
     2.7 -      apply (simp add: ring_simps)
     2.8 +      apply (simp add: field_simps)
     2.9        apply (subst mod_div_equality [of m n, symmetric])
    2.10        (* applying simp here undoes the last substitution!
    2.11           what is procedure cancel_div_mod? *)
    2.12 -      apply (simp only: ring_simps zadd_int [symmetric]
    2.13 +      apply (simp only: field_simps zadd_int [symmetric]
    2.14          zmult_int [symmetric])
    2.15        done
    2.16  qed
    2.17 @@ -1389,7 +1389,7 @@
    2.18    show "lcm (lcm n m) p = lcm n (lcm m p)"
    2.19      by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
    2.20    show "lcm m n = lcm n m"
    2.21 -    by (simp add: lcm_nat_def gcd_commute_nat ring_simps)
    2.22 +    by (simp add: lcm_nat_def gcd_commute_nat field_simps)
    2.23  qed
    2.24  
    2.25  interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
     3.1 --- a/src/HOL/Library/Binomial.thy	Mon Apr 26 11:34:17 2010 +0200
     3.2 +++ b/src/HOL/Library/Binomial.thy	Mon Apr 26 11:34:19 2010 +0200
     3.3 @@ -236,10 +236,10 @@
     3.4      have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
     3.5        (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
     3.6        apply (rule setprod_reindex_cong[where f = "Suc"])
     3.7 -      using n0 by (auto simp add: expand_fun_eq ring_simps)
     3.8 +      using n0 by (auto simp add: expand_fun_eq field_simps)
     3.9      have ?thesis apply (simp add: pochhammer_def)
    3.10      unfolding setprod_insert[OF th0, unfolded eq]
    3.11 -    using th1 by (simp add: ring_simps)}
    3.12 +    using th1 by (simp add: field_simps)}
    3.13  ultimately show ?thesis by blast
    3.14  qed
    3.15  
    3.16 @@ -378,10 +378,10 @@
    3.17        by simp
    3.18      from n h th0 
    3.19      have "fact k * fact (n - k) * (n choose k) = k * (fact h * fact (m - h) * (m choose h)) +  (m - h) * (fact k * fact (m - k) * (m choose k))"
    3.20 -      by (simp add: ring_simps)
    3.21 +      by (simp add: field_simps)
    3.22      also have "\<dots> = (k + (m - h)) * fact m"
    3.23        using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
    3.24 -      by (simp add: ring_simps)
    3.25 +      by (simp add: field_simps)
    3.26      finally have ?ths using h n km by simp}
    3.27    moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (EX m h. n=Suc m \<and> k = Suc h \<and> h < m)" using kn by presburger
    3.28    ultimately show ?ths by blast
    3.29 @@ -391,13 +391,13 @@
    3.30    assumes kn: "k \<le> n" 
    3.31    shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
    3.32    using binomial_fact_lemma[OF kn]
    3.33 -  by (simp add: field_eq_simps of_nat_mult [symmetric])
    3.34 +  by (simp add: field_simps of_nat_mult [symmetric])
    3.35  
    3.36  lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
    3.37  proof-
    3.38    {assume kn: "k > n" 
    3.39      from kn binomial_eq_0[OF kn] have ?thesis 
    3.40 -      by (simp add: gbinomial_pochhammer field_eq_simps
    3.41 +      by (simp add: gbinomial_pochhammer field_simps
    3.42          pochhammer_of_nat_eq_0_iff)}
    3.43    moreover
    3.44    {assume "k=0" then have ?thesis by simp}
    3.45 @@ -414,13 +414,13 @@
    3.46        apply clarsimp
    3.47        apply (presburger)
    3.48        apply presburger
    3.49 -      by (simp add: expand_fun_eq ring_simps of_nat_add[symmetric] del: of_nat_add)
    3.50 +      by (simp add: expand_fun_eq field_simps of_nat_add[symmetric] del: of_nat_add)
    3.51      have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
    3.52  "{1..n - Suc h} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
    3.53      from eq[symmetric]
    3.54      have ?thesis using kn
    3.55        apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
    3.56 -        gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
    3.57 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
    3.58        apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
    3.59        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
    3.60        unfolding mult_assoc[symmetric] 
    3.61 @@ -449,9 +449,9 @@
    3.62    have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
    3.63      unfolding gbinomial_pochhammer
    3.64      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
    3.65 -    by (simp add:  field_eq_simps del: of_nat_Suc)
    3.66 +    by (simp add:  field_simps del: of_nat_Suc)
    3.67    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
    3.68 -    by (simp add: ring_simps)
    3.69 +    by (simp add: field_simps)
    3.70    finally show ?thesis ..
    3.71  qed
    3.72  
    3.73 @@ -482,17 +482,17 @@
    3.74  
    3.75      have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)" 
    3.76        unfolding h
    3.77 -      apply (simp add: ring_simps del: fact_Suc)
    3.78 +      apply (simp add: field_simps del: fact_Suc)
    3.79        unfolding gbinomial_mult_fact'
    3.80        apply (subst fact_Suc)
    3.81        unfolding of_nat_mult 
    3.82        apply (subst mult_commute)
    3.83        unfolding mult_assoc
    3.84        unfolding gbinomial_mult_fact
    3.85 -      by (simp add: ring_simps)
    3.86 +      by (simp add: field_simps)
    3.87      also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
    3.88        unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
    3.89 -      by (simp add: ring_simps h)
    3.90 +      by (simp add: field_simps h)
    3.91      also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
    3.92        using eq0
    3.93        unfolding h  setprod_nat_ivl_1_Suc
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 11:34:17 2010 +0200
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 11:34:19 2010 +0200
     4.3 @@ -588,7 +588,7 @@
     4.4    from k have "real k > - log y x" by simp
     4.5    then have "ln y * real k > - ln x" unfolding log_def
     4.6      using ln_gt_zero_iff[OF yp] y1
     4.7 -    by (simp add: minus_divide_left field_simps field_eq_simps del:minus_divide_left[symmetric])
     4.8 +    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric])
     4.9    then have "ln y * real k + ln x > 0" by simp
    4.10    then have "exp (real k * ln y + ln x) > exp 0"
    4.11      by (simp add: mult_ac)
    4.12 @@ -596,7 +596,7 @@
    4.13      unfolding exp_zero exp_add exp_real_of_nat_mult
    4.14      exp_ln[OF xp] exp_ln[OF yp] by simp
    4.15    then have "x > (1/y)^k" using yp 
    4.16 -    by (simp add: field_simps field_eq_simps nonzero_power_divide)
    4.17 +    by (simp add: field_simps nonzero_power_divide)
    4.18    then show ?thesis using kp by blast
    4.19  qed
    4.20  lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
    4.21 @@ -693,7 +693,7 @@
    4.22      from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]]
    4.23      have th1: "setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n} =
    4.24        - (f$0) * (inverse f)$n"
    4.25 -      by (simp add: ring_simps)
    4.26 +      by (simp add: field_simps)
    4.27      have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n - i))"
    4.28        unfolding fps_mult_nth ifn ..
    4.29      also have "\<dots> = f$0 * natfun_inverse f n
    4.30 @@ -766,7 +766,7 @@
    4.31  lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def)
    4.32  
    4.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"
    4.34 -  unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: ring_simps)
    4.35 +  unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
    4.36  
    4.37  lemma fps_deriv_mult[simp]:
    4.38    fixes f :: "('a :: comm_ring_1) fps"
    4.39 @@ -817,7 +817,7 @@
    4.40        unfolding s0 s1
    4.41        unfolding setsum_addf[symmetric] setsum_right_distrib
    4.42        apply (rule setsum_cong2)
    4.43 -      by (auto simp add: of_nat_diff ring_simps)
    4.44 +      by (auto simp add: of_nat_diff field_simps)
    4.45      finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" .}
    4.46    then show ?thesis unfolding fps_eq_iff by auto
    4.47  qed
    4.48 @@ -878,7 +878,7 @@
    4.49  proof-
    4.50    have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0" by simp
    4.51    also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)" unfolding fps_deriv_eq_0_iff ..
    4.52 -  finally show ?thesis by (simp add: ring_simps)
    4.53 +  finally show ?thesis by (simp add: field_simps)
    4.54  qed
    4.55  
    4.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)"
    4.57 @@ -929,7 +929,7 @@
    4.58  qed
    4.59  
    4.60  lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
    4.61 -  by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult)
    4.62 +  by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
    4.63  
    4.64  subsection {* Powers*}
    4.65  
    4.66 @@ -943,7 +943,7 @@
    4.67    case (Suc n)
    4.68    note h = Suc.hyps[OF `a$0 = 1`]
    4.69    show ?case unfolding power_Suc fps_mult_nth
    4.70 -    using h `a$0 = 1`  fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: ring_simps)
    4.71 +    using h `a$0 = 1`  fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: field_simps)
    4.72  qed
    4.73  
    4.74  lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
    4.75 @@ -1005,7 +1005,7 @@
    4.76    case 0 thus ?case by (simp add: power_0)
    4.77  next
    4.78    case (Suc n)
    4.79 -  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: ring_simps power_Suc)
    4.80 +  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: field_simps power_Suc)
    4.81    also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth)
    4.82    also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {n .. Suc n}"
    4.83      apply (rule setsum_mono_zero_right)
    4.84 @@ -1045,8 +1045,8 @@
    4.85  qed
    4.86  
    4.87  lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
    4.88 -  apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add)
    4.89 -  by (case_tac n, auto simp add: power_Suc ring_simps)
    4.90 +  apply (induct n, auto simp add: power_Suc field_simps fps_const_add[symmetric] simp del: fps_const_add)
    4.91 +  by (case_tac n, auto simp add: power_Suc field_simps)
    4.92  
    4.93  lemma fps_inverse_deriv:
    4.94    fixes a:: "('a :: field) fps"
    4.95 @@ -1060,11 +1060,11 @@
    4.96    with inverse_mult_eq_1[OF a0]
    4.97    have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
    4.98      unfolding power2_eq_square
    4.99 -    apply (simp add: ring_simps)
   4.100 +    apply (simp add: field_simps)
   4.101      by (simp add: mult_assoc[symmetric])
   4.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"
   4.103      by simp
   4.104 -  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: ring_simps)
   4.105 +  then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: field_simps)
   4.106  qed
   4.107  
   4.108  lemma fps_inverse_mult:
   4.109 @@ -1084,7 +1084,7 @@
   4.110      from inverse_mult_eq_1[OF ab0]
   4.111      have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp
   4.112      then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b"
   4.113 -      by (simp add: ring_simps)
   4.114 +      by (simp add: field_simps)
   4.115      then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp}
   4.116  ultimately show ?thesis by blast
   4.117  qed
   4.118 @@ -1105,7 +1105,7 @@
   4.119    assumes a0: "b$0 \<noteq> 0"
   4.120    shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
   4.121    using fps_inverse_deriv[OF a0]
   4.122 -  by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
   4.123 +  by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
   4.124  
   4.125  
   4.126  lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
   4.127 @@ -1121,7 +1121,7 @@
   4.128  proof-
   4.129    have eq: "(1 + X) * ?r = 1"
   4.130      unfolding minus_one_power_iff
   4.131 -    by (auto simp add: ring_simps fps_eq_iff)
   4.132 +    by (auto simp add: field_simps fps_eq_iff)
   4.133    show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
   4.134  qed
   4.135  
   4.136 @@ -1185,7 +1185,7 @@
   4.137      next
   4.138        case (Suc k)
   4.139        note th = Suc.hyps[symmetric]
   4.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)
   4.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)
   4.142        also  have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
   4.143          using th
   4.144          unfolding fps_sub_nth by simp
   4.145 @@ -1209,10 +1209,10 @@
   4.146  definition "XD = op * X o fps_deriv"
   4.147  
   4.148  lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)"
   4.149 -  by (simp add: XD_def ring_simps)
   4.150 +  by (simp add: XD_def field_simps)
   4.151  
   4.152  lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
   4.153 -  by (simp add: XD_def ring_simps)
   4.154 +  by (simp add: XD_def field_simps)
   4.155  
   4.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)"
   4.157    by simp
   4.158 @@ -1226,7 +1226,7 @@
   4.159  
   4.160  lemma fps_mult_XD_shift:
   4.161    "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   4.162 -  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
   4.163 +  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff field_simps del: One_nat_def)
   4.164  
   4.165  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
   4.166  subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
   4.167 @@ -1688,7 +1688,7 @@
   4.168          then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
   4.169            by (simp add: natpermute_max_card[OF nz, simplified])
   4.170          also have "\<dots> = a$n - setsum ?f ?Pnknn"
   4.171 -          unfolding n1 using r00 a0 by (simp add: field_eq_simps fps_radical_def del: of_nat_Suc)
   4.172 +          unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc)
   4.173          finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
   4.174          have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
   4.175            unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] ..
   4.176 @@ -1764,7 +1764,7 @@
   4.177    shows "a = b / c"
   4.178  proof-
   4.179    from eq have "a * c * inverse c = b * inverse c" by simp
   4.180 -  hence "a * (inverse c * c) = b/c" by (simp only: field_eq_simps divide_inverse)
   4.181 +  hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse)
   4.182    then show "a = b/c" unfolding  field_inverse[OF c0] by simp
   4.183  qed
   4.184  
   4.185 @@ -1837,7 +1837,7 @@
   4.186            show "a$(xs !i) = ?r$(xs!i)" .
   4.187          qed
   4.188          have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
   4.189 -          by (simp add: field_eq_simps del: of_nat_Suc)
   4.190 +          by (simp add: field_simps del: of_nat_Suc)
   4.191          from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
   4.192          also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
   4.193            unfolding fps_power_nth_Suc
   4.194 @@ -1854,7 +1854,7 @@
   4.195          then have "a$n = ?r $n"
   4.196            apply (simp del: of_nat_Suc)
   4.197            unfolding fps_radical_def n1
   4.198 -          by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)}
   4.199 +          by (simp add: field_simps n1 th00 del: of_nat_Suc)}
   4.200          ultimately show "a$n = ?r $ n" by (cases n, auto)
   4.201        qed}
   4.202      then have "a = ?r" by (simp add: fps_eq_iff)}
   4.203 @@ -2018,11 +2018,11 @@
   4.204  proof-
   4.205    {fix n
   4.206      have "(fps_deriv (a oo b))$n = setsum (\<lambda>i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}"
   4.207 -      by (simp add: fps_compose_def ring_simps setsum_right_distrib del: of_nat_Suc)
   4.208 +      by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc)
   4.209      also have "\<dots> = setsum (\<lambda>i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}"
   4.210 -      by (simp add: ring_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc)
   4.211 +      by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc)
   4.212    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}"
   4.213 -    unfolding fps_mult_left_const_nth  by (simp add: ring_simps)
   4.214 +    unfolding fps_mult_left_const_nth  by (simp add: field_simps)
   4.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}"
   4.216      unfolding fps_mult_nth ..
   4.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}"
   4.218 @@ -2170,7 +2170,7 @@
   4.219    by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0')
   4.220  
   4.221  lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
   4.222 -  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
   4.223 +  by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_addf)
   4.224  
   4.225  lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
   4.226  proof-
   4.227 @@ -2212,7 +2212,7 @@
   4.228      apply (simp add: fps_mult_nth setsum_right_distrib)
   4.229      apply (subst setsum_commute)
   4.230      apply (rule setsum_cong2)
   4.231 -    by (auto simp add: ring_simps)
   4.232 +    by (auto simp add: field_simps)
   4.233    also have "\<dots> = ?l"
   4.234      apply (simp add: fps_mult_nth fps_compose_nth setsum_product)
   4.235      apply (rule setsum_cong2)
   4.236 @@ -2312,7 +2312,7 @@
   4.237  qed
   4.238  
   4.239  lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
   4.240 -  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric])
   4.241 +  by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric])
   4.242  
   4.243  lemma fps_compose_sub_distrib:
   4.244    shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   4.245 @@ -2469,7 +2469,7 @@
   4.246  proof-
   4.247    let ?r = "fps_inv"
   4.248    have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
   4.249 -  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_eq_simps)
   4.250 +  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
   4.251    have X0: "X$0 = 0" by simp
   4.252    from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
   4.253    then have "?r (?r a) oo ?r a oo a = X oo a" by simp
   4.254 @@ -2486,7 +2486,7 @@
   4.255  proof-
   4.256    let ?r = "fps_ginv"
   4.257    from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
   4.258 -  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_eq_simps)
   4.259 +  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
   4.260    from fps_ginv[OF rca0 rca1] 
   4.261    have "?r b (?r c a) oo ?r c a = b" .
   4.262    then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
   4.263 @@ -2534,8 +2534,8 @@
   4.264  proof-
   4.265    {fix n
   4.266      have "?l$n = ?r $ n"
   4.267 -  apply (auto simp add: E_def field_eq_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   4.268 -  by (simp add: of_nat_mult ring_simps)}
   4.269 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   4.270 +  by (simp add: of_nat_mult field_simps)}
   4.271  then show ?thesis by (simp add: fps_eq_iff)
   4.272  qed
   4.273  
   4.274 @@ -2545,15 +2545,15 @@
   4.275  proof-
   4.276    {assume d: ?lhs
   4.277    from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
   4.278 -    by (simp add: fps_deriv_def fps_eq_iff field_eq_simps del: of_nat_Suc)
   4.279 +    by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
   4.280    {fix n have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
   4.281        apply (induct n)
   4.282        apply simp
   4.283        unfolding th
   4.284        using fact_gt_zero_nat
   4.285 -      apply (simp add: field_eq_simps del: of_nat_Suc fact_Suc)
   4.286 +      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
   4.287        apply (drule sym)
   4.288 -      by (simp add: ring_simps of_nat_mult power_Suc)}
   4.289 +      by (simp add: field_simps of_nat_mult power_Suc)}
   4.290    note th' = this
   4.291    have ?rhs
   4.292      by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')}
   4.293 @@ -2570,7 +2570,7 @@
   4.294  lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
   4.295  proof-
   4.296    have "fps_deriv (?r) = fps_const (a+b) * ?r"
   4.297 -    by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add)
   4.298 +    by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
   4.299    then have "?r = ?l" apply (simp only: E_unique_ODE)
   4.300      by (simp add: fps_mult_nth E_def)
   4.301    then show ?thesis ..
   4.302 @@ -2618,13 +2618,13 @@
   4.303    (is "inverse ?l = ?r")
   4.304  proof-
   4.305    have th: "?l * ?r = 1"
   4.306 -    by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff)
   4.307 +    by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
   4.308    have th': "?l $ 0 \<noteq> 0" by (simp add: )
   4.309    from fps_inverse_unique[OF th' th] show ?thesis .
   4.310  qed
   4.311  
   4.312  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
   4.313 -  by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
   4.314 +  by (induct n, auto simp add: field_simps E_add_mult power_Suc)
   4.315  
   4.316  lemma radical_E:
   4.317    assumes r: "r (Suc k) 1 = 1" 
   4.318 @@ -2649,18 +2649,18 @@
   4.319  text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
   4.320  
   4.321  lemma gbinomial_theorem: 
   4.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))"
   4.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))"
   4.324  proof-
   4.325    from E_add_mult[of a b] 
   4.326    have "(E (a + b)) $ n = (E a * E b)$n" by simp
   4.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))))"
   4.328 -    by (simp add: field_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   4.329 +    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   4.330    then show ?thesis 
   4.331      apply simp
   4.332      apply (rule setsum_cong2)
   4.333      apply simp
   4.334      apply (frule binomial_fact[where ?'a = 'a, symmetric])
   4.335 -    by (simp add: field_eq_simps of_nat_mult)
   4.336 +    by (simp add: field_simps of_nat_mult)
   4.337  qed
   4.338  
   4.339  text{* And the nat-form -- also available from Binomial.thy *}
   4.340 @@ -2683,7 +2683,7 @@
   4.341    by (simp add: L_def fps_eq_iff del: of_nat_Suc)
   4.342  
   4.343  lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   4.344 -  by (simp add: L_def field_eq_simps)
   4.345 +  by (simp add: L_def field_simps)
   4.346  
   4.347  lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
   4.348  lemma L_E_inv:
   4.349 @@ -2694,9 +2694,9 @@
   4.350    have b0: "?b $ 0 = 0" by simp
   4.351    have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
   4.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)"
   4.353 -    by (simp add: ring_simps)
   4.354 +    by (simp add: field_simps)
   4.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])
   4.356 -    by (simp add: ring_simps)
   4.357 +    by (simp add: field_simps)
   4.358    finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
   4.359    from fps_inv_deriv[OF b0 b1, unfolded eq]
   4.360    have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
   4.361 @@ -2713,7 +2713,7 @@
   4.362    shows "L c + L d = fps_const (c+d) * L (c*d)"
   4.363    (is "?r = ?l")
   4.364  proof-
   4.365 -  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_eq_simps)
   4.366 +  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
   4.367    have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
   4.368      by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
   4.369    also have "\<dots> = fps_deriv ?l"
   4.370 @@ -2743,7 +2743,7 @@
   4.371    have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
   4.372    also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
   4.373      apply (simp only: fps_divide_def  mult_assoc[symmetric] inverse_mult_eq_1[OF x10])
   4.374 -    by (simp add: ring_simps)
   4.375 +    by (simp add: field_simps)
   4.376    finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
   4.377    moreover
   4.378    {assume h: "?l = ?r" 
   4.379 @@ -2752,8 +2752,8 @@
   4.380        
   4.381        from lrn 
   4.382        have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
   4.383 -        apply (simp add: ring_simps del: of_nat_Suc)
   4.384 -        by (cases n, simp_all add: field_eq_simps del: of_nat_Suc)
   4.385 +        apply (simp add: field_simps del: of_nat_Suc)
   4.386 +        by (cases n, simp_all add: field_simps del: of_nat_Suc)
   4.387      }
   4.388      note th0 = this
   4.389      {fix n have "a$n = (c gchoose n) * a$0"
   4.390 @@ -2762,24 +2762,24 @@
   4.391        next
   4.392          case (Suc m)
   4.393          thus ?case unfolding th0
   4.394 -          apply (simp add: field_eq_simps del: of_nat_Suc)
   4.395 +          apply (simp add: field_simps del: of_nat_Suc)
   4.396            unfolding mult_assoc[symmetric] gbinomial_mult_1
   4.397 -          by (simp add: ring_simps)
   4.398 +          by (simp add: field_simps)
   4.399        qed}
   4.400      note th1 = this
   4.401      have ?rhs
   4.402        apply (simp add: fps_eq_iff)
   4.403        apply (subst th1)
   4.404 -      by (simp add: ring_simps)}
   4.405 +      by (simp add: field_simps)}
   4.406    moreover
   4.407    {assume h: ?rhs
   4.408    have th00:"\<And>x y. x * (a$0 * y) = a$0 * (x*y)" by (simp add: mult_commute)
   4.409      have "?l = ?r" 
   4.410        apply (subst h)
   4.411        apply (subst (2) h)
   4.412 -      apply (clarsimp simp add: fps_eq_iff ring_simps)
   4.413 +      apply (clarsimp simp add: fps_eq_iff field_simps)
   4.414        unfolding mult_assoc[symmetric] th00 gbinomial_mult_1
   4.415 -      by (simp add: ring_simps gbinomial_mult_1)}
   4.416 +      by (simp add: field_simps gbinomial_mult_1)}
   4.417    ultimately show ?thesis by blast
   4.418  qed
   4.419  
   4.420 @@ -2798,9 +2798,9 @@
   4.421    have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
   4.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))"
   4.423      unfolding fps_binomial_deriv
   4.424 -    by (simp add: fps_divide_def ring_simps)
   4.425 +    by (simp add: fps_divide_def field_simps)
   4.426    also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
   4.427 -    by (simp add: ring_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   4.428 +    by (simp add: field_simps fps_divide_def fps_const_add[symmetric] del: fps_const_add)
   4.429    finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
   4.430      by (simp add: fps_divide_def)
   4.431    have "?P = fps_const (?P$0) * ?b (c + d)"
   4.432 @@ -2880,7 +2880,7 @@
   4.433            using kn pochhammer_minus'[where k=k and n=n and b=b]
   4.434            apply (simp add:  pochhammer_same)
   4.435            using bn0
   4.436 -          by (simp add: field_eq_simps power_add[symmetric])}
   4.437 +          by (simp add: field_simps power_add[symmetric])}
   4.438        moreover
   4.439        {assume nk: "k \<noteq> n"
   4.440          have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" 
   4.441 @@ -2905,7 +2905,7 @@
   4.442            unfolding m1nk 
   4.443            
   4.444            unfolding m h pochhammer_Suc_setprod
   4.445 -          apply (simp add: field_eq_simps del: fact_Suc id_def)
   4.446 +          apply (simp add: field_simps del: fact_Suc id_def)
   4.447            unfolding fact_altdef_nat id_def
   4.448            unfolding of_nat_setprod
   4.449            unfolding setprod_timesf[symmetric]
   4.450 @@ -2942,10 +2942,10 @@
   4.451            apply auto
   4.452            done
   4.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}" 
   4.454 -          using nz' by (simp add: field_eq_simps)
   4.455 +          using nz' by (simp add: field_simps)
   4.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)"
   4.457            using bnz0
   4.458 -          by (simp add: field_eq_simps)
   4.459 +          by (simp add: field_simps)
   4.460          also have "\<dots> = b gchoose (n - k)" 
   4.461            unfolding th1 th2
   4.462            using kn' by (simp add: gbinomial_def)
   4.463 @@ -2959,15 +2959,15 @@
   4.464    note th00 = this
   4.465    have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
   4.466      unfolding gbinomial_pochhammer 
   4.467 -    using bn0 by (auto simp add: field_eq_simps)
   4.468 +    using bn0 by (auto simp add: field_simps)
   4.469    also have "\<dots> = ?l"
   4.470      unfolding gbinomial_Vandermonde[symmetric]
   4.471      apply (simp add: th00)
   4.472      unfolding gbinomial_pochhammer
   4.473 -    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_eq_simps)
   4.474 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
   4.475      apply (rule setsum_cong2)
   4.476      apply (drule th00(2))
   4.477 -    by (simp add: field_eq_simps power_add[symmetric])
   4.478 +    by (simp add: field_simps power_add[symmetric])
   4.479    finally show ?thesis by simp
   4.480  qed 
   4.481  
   4.482 @@ -2992,7 +2992,7 @@
   4.483    have nz: "pochhammer c n \<noteq> 0" using c
   4.484      by (simp add: pochhammer_eq_0_iff)
   4.485    from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
   4.486 -  show ?thesis using nz by (simp add: field_eq_simps setsum_right_distrib)
   4.487 +  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
   4.488  qed
   4.489  
   4.490  subsubsection{* Formal trigonometric functions  *}
   4.491 @@ -3014,11 +3014,11 @@
   4.492          using en by (simp add: fps_sin_def)
   4.493        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   4.494          unfolding fact_Suc of_nat_mult
   4.495 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   4.496 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   4.497        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
   4.498 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   4.499 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   4.500        finally have "?lhs $n = ?rhs$n" using en
   4.501 -        by (simp add: fps_cos_def ring_simps power_Suc )}
   4.502 +        by (simp add: fps_cos_def field_simps power_Suc )}
   4.503      then show "?lhs $ n = ?rhs $ n"
   4.504        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def)
   4.505  qed
   4.506 @@ -3038,13 +3038,13 @@
   4.507          using en by (simp add: fps_cos_def)
   4.508        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   4.509          unfolding fact_Suc of_nat_mult
   4.510 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   4.511 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   4.512        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
   4.513 -        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   4.514 +        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   4.515        also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)"
   4.516          unfolding th0 unfolding th1[OF en] by simp
   4.517        finally have "?lhs $n = ?rhs$n" using en
   4.518 -        by (simp add: fps_sin_def ring_simps power_Suc)}
   4.519 +        by (simp add: fps_sin_def field_simps power_Suc)}
   4.520      then show "?lhs $ n = ?rhs $ n"
   4.521        by (cases "even n", simp_all add: fps_deriv_def fps_sin_def
   4.522          fps_cos_def)
   4.523 @@ -3055,7 +3055,7 @@
   4.524  proof-
   4.525    have "fps_deriv ?lhs = 0"
   4.526      apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc)
   4.527 -    by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg)
   4.528 +    by (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
   4.529    then have "?lhs = fps_const (?lhs $ 0)"
   4.530      unfolding fps_deriv_eq_0_iff .
   4.531    also have "\<dots> = 1"
   4.532 @@ -3177,7 +3177,7 @@
   4.533    have th0: "fps_cos c $ 0 \<noteq> 0" by (simp add: fps_cos_def)
   4.534    show ?thesis
   4.535      using fps_sin_cos_sum_of_squares[of c]
   4.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)
   4.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)
   4.538      unfolding right_distrib[symmetric]
   4.539      by simp
   4.540  qed
   4.541 @@ -3252,7 +3252,7 @@
   4.542  subsection {* Hypergeometric series *}
   4.543  
   4.544  
   4.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)))"
   4.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)))"
   4.547  
   4.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))"
   4.549    by (simp add: F_def)
   4.550 @@ -3321,9 +3321,9 @@
   4.551    by (simp add: fps_eq_iff fps_integral_def)
   4.552  
   4.553  lemma F_minus_nat: 
   4.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 /
   4.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 /
   4.556      (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
   4.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 /
   4.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 /
   4.559      (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
   4.560    by (auto simp add: pochhammer_eq_0_iff)
   4.561  
     5.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Apr 26 11:34:17 2010 +0200
     5.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Apr 26 11:34:19 2010 +0200
     5.3 @@ -213,7 +213,7 @@
     5.4  
     5.5  lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
     5.6  apply (intro_classes, unfold definitions)
     5.7 -apply (simp_all add: Rep_simps zmod_simps ring_simps)
     5.8 +apply (simp_all add: Rep_simps zmod_simps field_simps)
     5.9  done
    5.10  
    5.11  end
     6.1 --- a/src/HOL/Library/Polynomial.thy	Mon Apr 26 11:34:17 2010 +0200
     6.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Apr 26 11:34:19 2010 +0200
     6.3 @@ -1093,10 +1093,10 @@
     6.4  apply (cases "r = 0")
     6.5  apply (cases "r' = 0")
     6.6  apply (simp add: pdivmod_rel_def)
     6.7 -apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
     6.8 +apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
     6.9  apply (cases "r' = 0")
    6.10  apply (simp add: pdivmod_rel_def degree_mult_eq)
    6.11 -apply (simp add: pdivmod_rel_def ring_simps)
    6.12 +apply (simp add: pdivmod_rel_def field_simps)
    6.13  apply (simp add: degree_mult_eq degree_add_less)
    6.14  done
    6.15  
     7.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Apr 26 11:34:17 2010 +0200
     7.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Apr 26 11:34:19 2010 +0200
     7.3 @@ -1282,9 +1282,9 @@
     7.4    fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS
     7.5   val concl = Thm.dest_arg o cprop_of
     7.6   val shuffle1 =
     7.7 -   fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) })
     7.8 +   fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: field_simps) })
     7.9   val shuffle2 =
    7.10 -    fconv_rule (rewr_conv @{lemma "(x + a == y) ==  (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps)})
    7.11 +    fconv_rule (rewr_conv @{lemma "(x + a == y) ==  (x == y - (a::real))" by (atomize (full)) (simp add: field_simps)})
    7.12   fun substitutable_monomial fvs tm = case term_of tm of
    7.13      Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm)
    7.14                             else raise Failure "substitutable_monomial"
     8.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 11:34:17 2010 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 11:34:19 2010 +0200
     8.3 @@ -1383,7 +1383,7 @@
     8.4      apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+
     8.5      unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE)
     8.6      unfolding vector_dist_norm apply(simp add: * norm_minus_commute) . note x = this
     8.7 -  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:group_simps)
     8.8 +  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps)
     8.9    hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto 
    8.10    thus False using x using assms by auto qed
    8.11  
    8.12 @@ -1396,7 +1396,7 @@
    8.13   "interval_bij (a,b) (u,v) = (\<lambda>x. (\<chi> i. (v$i - u$i) / (b$i - a$i) * x$i) +
    8.14              (\<chi> i. u$i - (v$i - u$i) / (b$i - a$i) * a$i))"
    8.15    apply rule unfolding Cart_eq interval_bij_def vector_component_simps
    8.16 -  by(auto simp add:group_simps field_simps add_divide_distrib[THEN sym]) 
    8.17 +  by(auto simp add: field_simps add_divide_distrib[THEN sym]) 
    8.18  
    8.19  lemma continuous_interval_bij:
    8.20    "continuous (at x) (interval_bij (a,b::real^'n) (u,v))" 
     9.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 26 11:34:17 2010 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 26 11:34:19 2010 +0200
     9.3 @@ -646,7 +646,7 @@
     9.4        using assms(1)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
     9.5        using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x=u]]
     9.6        apply - apply(rule add_mono) by auto
     9.7 -    hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: ring_simps)  }
     9.8 +    hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps)  }
     9.9    thus ?thesis unfolding convex_on_def by auto 
    9.10  qed
    9.11  
    9.12 @@ -654,7 +654,7 @@
    9.13    assumes "0 \<le> (c::real)" "convex_on s f"
    9.14    shows "convex_on s (\<lambda>x. c * f x)"
    9.15  proof-
    9.16 -  have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: ring_simps)
    9.17 +  have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
    9.18    show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
    9.19  qed
    9.20  
    9.21 @@ -1060,7 +1060,7 @@
    9.22  proof-
    9.23    have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
    9.24    have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
    9.25 -         "\<And>x y z ::real^_. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: ring_simps)
    9.26 +         "\<And>x y z ::real^_. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
    9.27    show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
    9.28      unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
    9.29      apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
    9.30 @@ -2310,7 +2310,7 @@
    9.31    } moreover
    9.32    { fix a b assume "\<not> u * a + v * b \<le> a"
    9.33      hence "v * b > (1 - u) * a" unfolding not_le using as(4) by(auto simp add: field_simps)
    9.34 -    hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps)
    9.35 +    hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
    9.36      hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
    9.37    ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
    9.38      using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
    10.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 26 11:34:17 2010 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 26 11:34:19 2010 +0200
    10.3 @@ -1,11 +1,12 @@
    10.4 -(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
    10.5 -    Author:                     John Harrison
    10.6 -    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
    10.7 +(*  Title:                       HOL/Multivariate_Analysis/Derivative.thy
    10.8 +    Author:                      John Harrison
    10.9 +    Translation from HOL Light:  Robert Himmelmann, TU Muenchen
   10.10 +*)
   10.11  
   10.12  header {* Multivariate calculus in Euclidean space. *}
   10.13  
   10.14  theory Derivative
   10.15 -  imports Brouwer_Fixpoint RealVector
   10.16 +imports Brouwer_Fixpoint RealVector
   10.17  begin
   10.18  
   10.19  
   10.20 @@ -40,7 +41,7 @@
   10.21    show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe)
   10.22      apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE)
   10.23      unfolding vector_dist_norm diff_0_right norm_scaleR
   10.24 -    unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps *) qed
   10.25 +    unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed
   10.26  
   10.27  lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof 
   10.28    assume ?l note as = this[unfolded fderiv_def]
   10.29 @@ -50,14 +51,14 @@
   10.30      thus "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
   10.31        dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e"
   10.32        apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE)
   10.33 -      unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed next
   10.34 +      unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next
   10.35    assume ?r note as = this[unfolded has_derivative_def]
   10.36    show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule)
   10.37      fix e::real assume "e>0"
   10.38      guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] ..
   10.39      thus "\<exists>s>0. \<forall>xa. xa \<noteq> 0 \<and> dist xa 0 < s \<longrightarrow> dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply-
   10.40        apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE)
   10.41 -      unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:group_simps) qed qed
   10.42 +      unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed
   10.43  
   10.44  subsection {* These are the only cases we'll care about, probably. *}
   10.45  
   10.46 @@ -76,7 +77,7 @@
   10.47          (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm(x' - x) \<and> norm(x' - x) < d
   10.48          \<longrightarrow> norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)"
   10.49    unfolding has_derivative_within Lim_within vector_dist_norm
   10.50 -  unfolding diff_0_right norm_mul by(simp add: group_simps)
   10.51 +  unfolding diff_0_right norm_mul by (simp add: diff_diff_eq)
   10.52  
   10.53  lemma has_derivative_at':
   10.54   "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
   10.55 @@ -186,14 +187,14 @@
   10.56    note as = assms[unfolded has_derivative_def]
   10.57    show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
   10.58      using Lim_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
   10.59 -    by(auto simp add:group_simps scaleR_right_diff_distrib scaleR_right_distrib) qed
   10.60 +    by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib) qed
   10.61  
   10.62  lemma has_derivative_add_const:"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
   10.63    apply(drule has_derivative_add) apply(rule has_derivative_const) by auto
   10.64  
   10.65  lemma has_derivative_sub:
   10.66   "(f has_derivative f') net \<Longrightarrow> (g has_derivative g') net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_derivative (\<lambda>h. f'(h) - g'(h))) net"
   10.67 -  apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:group_simps)
   10.68 +  apply(drule has_derivative_add) apply(drule has_derivative_neg,assumption) by(simp add:algebra_simps)
   10.69  
   10.70  lemma has_derivative_setsum: assumes "finite s" "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
   10.71    shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
   10.72 @@ -391,8 +392,8 @@
   10.73        case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\<in>s`]
   10.74  	unfolding vector_dist_norm diff_0_right norm_mul using as(3)
   10.75  	using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded vector_dist_norm]
   10.76 -	by(auto simp add:linear_0 linear_sub group_simps)
   10.77 -      thus ?thesis by(auto simp add:group_simps) qed qed next
   10.78 +	by (auto simp add: linear_0 linear_sub)
   10.79 +      thus ?thesis by(auto simp add:algebra_simps) qed qed next
   10.80    assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption)
   10.81      apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI)
   10.82      apply(erule conjE,rule,assumption,rule,rule) unfolding vector_dist_norm diff_0_right norm_scaleR
   10.83 @@ -400,7 +401,7 @@
   10.84      fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \<in> s" "0 < norm (y - x) \<and> norm (y - x) < d"
   10.85          "norm (f y - f x - f' (y - x)) \<le> e / 2 * norm (y - x)"
   10.86      thus "\<bar>1 / norm (y - x)\<bar> * norm (f y - (f x + f' (y - x))) < e"
   10.87 -      apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed
   10.88 +      apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:algebra_simps) qed auto qed
   10.89  
   10.90  lemma has_derivative_at_alt:
   10.91    "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
   10.92 @@ -435,8 +436,8 @@
   10.93      hence 1:"norm (f y - f x - f' (y - x)) \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x))" using d1 d2 d by auto
   10.94  
   10.95      have "norm (f y - f x) \<le> norm (f y - f x - f' (y - x)) + norm (f' (y - x))"
   10.96 -      using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:group_simps)
   10.97 -    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:group_simps)
   10.98 +      using norm_triangle_sub[of "f y - f x" "f' (y - x)"] by(auto simp add:algebra_simps)
   10.99 +    also have "\<dots> \<le> norm (f y - f x - f' (y - x)) + B1 * norm (y - x)" apply(rule add_left_mono) using B1 by(auto simp add:algebra_simps)
  10.100      also have "\<dots> \<le> min (norm (y - x)) (e / 2 / B2 * norm (y - x)) + B1 * norm (y - x)" apply(rule add_right_mono) using d1 d2 d as by auto
  10.101      also have "\<dots> \<le> norm (y - x) + B1 * norm (y - x)" by auto
  10.102      also have "\<dots> = norm (y - x) * (1 + B1)" by(auto simp add:field_simps)
  10.103 @@ -453,8 +454,8 @@
  10.104      interpret g': bounded_linear g' using assms(2) by auto
  10.105      interpret f': bounded_linear f' using assms(1) by auto
  10.106      have "norm (- g' (f' (y - x)) + g' (f y - f x)) = norm (g' (f y - f x - f' (y - x)))"
  10.107 -      by(auto simp add:group_simps f'.diff g'.diff g'.add)
  10.108 -    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:group_simps)
  10.109 +      by(auto simp add:algebra_simps f'.diff g'.diff g'.add)
  10.110 +    also have "\<dots> \<le> B2 * norm (f y - f x - f' (y - x))" using B2 by(auto simp add:algebra_simps)
  10.111      also have "\<dots> \<le> B2 * (e / 2 / B2 * norm (y - x))" apply(rule mult_left_mono) using as d1 d2 d B2 by auto 
  10.112      also have "\<dots> \<le> e / 2 * norm (y - x)" using B2 by auto
  10.113      finally have 5:"norm (- g' (f' (y - x)) + g' (f y - f x)) \<le> e / 2 * norm (y - x)" by auto
  10.114 @@ -535,7 +536,7 @@
  10.115        unfolding scaleR_right_distrib by auto
  10.116      also have "\<dots> = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))"  
  10.117        unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto
  10.118 -    also have "\<dots> = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by(auto simp add:group_simps)
  10.119 +    also have "\<dots> = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus)
  10.120      finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm 
  10.121        unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed
  10.122  
  10.123 @@ -623,7 +624,7 @@
  10.124    have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
  10.125    show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
  10.126      using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
  10.127 -    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding group_simps by (auto intro: mult_pos_pos)
  10.128 +    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
  10.129  qed
  10.130  
  10.131  subsection {* In particular if we have a mapping into @{typ "real^1"}. *}
  10.132 @@ -727,7 +728,7 @@
  10.133    shows "norm(f x - f y) \<le> B * norm(x - y)" proof-
  10.134    let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
  10.135    have *:"\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
  10.136 -    using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:group_simps)
  10.137 +    using assms(1)[unfolded convex_alt,rule_format,OF x y] unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by(auto simp add:algebra_simps)
  10.138    hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply- apply(rule continuous_on_intros continuous_on_vmul)+
  10.139      unfolding continuous_on_eq_continuous_within apply(rule,rule differentiable_imp_continuous_within)
  10.140      unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
  10.141 @@ -862,7 +863,7 @@
  10.142    assumes "compact t" "convex t"  "t \<noteq> {}" "continuous_on t f"
  10.143    "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t" "x\<in>s"
  10.144    shows "\<exists>y\<in>t. f y = x" proof-
  10.145 -  have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y" by(auto simp add:group_simps)
  10.146 +  have *:"\<And>x y. f y = x \<longleftrightarrow> x + (y - f y) = y" by(auto simp add:algebra_simps)
  10.147    show ?thesis  unfolding * apply(rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
  10.148      apply(rule continuous_on_intros assms)+ using assms(4-6) by auto qed
  10.149  
  10.150 @@ -907,8 +908,8 @@
  10.151      finally have *:"norm (x + g' (z - f x) - x) < e0" by auto
  10.152      have **:"f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto
  10.153      have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le> norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
  10.154 -      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:group_simps)
  10.155 -    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding group_simps ** by auto 
  10.156 +      using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:algebra_simps)
  10.157 +    also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding algebra_simps ** by auto 
  10.158      also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball vector_dist_norm] by auto
  10.159      also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2" using * and B by(auto simp add:field_simps)
  10.160      also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2" by auto
  10.161 @@ -983,7 +984,7 @@
  10.162  (* we know for some other reason that the inverse function exists, it's OK. *}
  10.163  
  10.164  lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g ==> bounded_linear (\<lambda>x. f x - g x)"
  10.165 -  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps)
  10.166 +  using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] by(auto simp add:algebra_simps)
  10.167  
  10.168  lemma has_derivative_locally_injective: fixes f::"real^'n \<Rightarrow> real^'m"
  10.169    assumes "a \<in> s" "open s" "bounded_linear g'" "g' o f'(a) = id"
  10.170 @@ -1004,7 +1005,7 @@
  10.171      show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x" proof(intro strip)
  10.172        fix x y assume as:"x\<in>ball a d" "y\<in>ball a d" "f x = f y"
  10.173        def ph \<equiv> "\<lambda>w. w - g'(f w - f x)" have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
  10.174 -	unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:group_simps)
  10.175 +	unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:algebra_simps)
  10.176        have "norm (ph x - ph y) \<le> (1/2) * norm (x - y)"
  10.177  	apply(rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
  10.178  	apply(rule_tac[!] ballI) proof- fix u assume u:"u \<in> ball a d" hence "u\<in>s" using d d2 by auto
  10.179 @@ -1020,7 +1021,7 @@
  10.180  	  unfolding linear_conv_bounded_linear by(rule assms(3) **)+ 
  10.181  	also have "\<dots> \<le> onorm g' * k" apply(rule mult_left_mono) 
  10.182  	  using d1[THEN conjunct2,rule_format,of u] using onorm_neg[OF **(1)[unfolded linear_linear]]
  10.183 -	  using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:group_simps) 
  10.184 +	  using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:algebra_simps) 
  10.185  	also have "\<dots> \<le> 1/2" unfolding k_def by auto
  10.186  	finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" by assumption qed
  10.187        moreover have "norm (ph y - ph x) = norm (y - x)" apply(rule arg_cong[where f=norm])
  10.188 @@ -1039,7 +1040,7 @@
  10.189      fix x assume "x\<in>s" show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
  10.190        by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
  10.191      { fix h have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
  10.192 -	using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:group_simps) 
  10.193 +	using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:algebra_simps) 
  10.194        also have "\<dots> \<le> e * norm h+ e * norm h"  using assms(3)[rule_format,OF `N\<le>m` `x\<in>s`, of h] assms(3)[rule_format,OF `N\<le>n` `x\<in>s`, of h]
  10.195  	by(auto simp add:field_simps)
  10.196        finally have "norm (f' m x h - f' n x h) \<le> 2 * e * norm h" by auto }
  10.197 @@ -1083,7 +1084,7 @@
  10.198        have "eventually (\<lambda>xa. norm (f n x - f n y - (f xa x - f xa y)) \<le> e * norm (x - y)) sequentially" 
  10.199  	unfolding eventually_sequentially apply(rule_tac x=N in exI) proof(rule,rule)
  10.200  	fix m assume "N\<le>m" thus "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
  10.201 -	  using N[rule_format, of n m x y] and as by(auto simp add:group_simps) qed
  10.202 +	  using N[rule_format, of n m x y] and as by(auto simp add:algebra_simps) qed
  10.203        thus "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" apply-
  10.204  	apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
  10.205  	apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption qed qed
  10.206 @@ -1120,10 +1121,10 @@
  10.207  	have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)" using d1 and as by auto ultimately
  10.208  	have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)" 
  10.209  	  using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] 
  10.210 -	  by (auto simp add:group_simps) moreover
  10.211 +	  by (auto simp add:algebra_simps) moreover
  10.212  	have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)" using N1 `x\<in>s` by auto
  10.213  	ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
  10.214 -	  using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:group_simps)
  10.215 +	  using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:algebra_simps)
  10.216  	qed qed qed qed
  10.217  
  10.218  subsection {* Can choose to line up antiderivatives if we want. *}
  10.219 @@ -1274,7 +1275,7 @@
  10.220    unfolding has_vector_derivative_def using has_derivative_id by auto
  10.221  
  10.222  lemma has_vector_derivative_cmul:  "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
  10.223 -  unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps)
  10.224 +  unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:algebra_simps)
  10.225  
  10.226  lemma has_vector_derivative_cmul_eq: assumes "c \<noteq> 0"
  10.227    shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
    11.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 11:34:17 2010 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 11:34:19 2010 +0200
    11.3 @@ -55,7 +55,7 @@
    11.4  done
    11.5  
    11.6    (* FIXME: In Finite_Set there is a useless further assumption *)
    11.7 -lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})"
    11.8 +lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})"
    11.9    apply (erule finite_induct)
   11.10    apply (simp)
   11.11    apply simp
   11.12 @@ -352,13 +352,13 @@
   11.13      apply (rule setprod_insert)
   11.14      apply simp
   11.15      by blast
   11.16 -  also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" by (simp add: ring_simps)
   11.17 +  also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" by (simp add: field_simps)
   11.18    also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)" by (metis th1 th2)
   11.19    also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
   11.20      unfolding  setprod_insert[OF th3] by simp
   11.21    finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U" unfolding kU[symmetric] .
   11.22    then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U"
   11.23 -    by (simp add: ring_simps)
   11.24 +    by (simp add: field_simps)
   11.25  qed
   11.26  
   11.27  lemma det_row_mul:
   11.28 @@ -389,14 +389,14 @@
   11.29      apply (rule setprod_insert)
   11.30      apply simp
   11.31      by blast
   11.32 -  also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: ring_simps)
   11.33 +  also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: field_simps)
   11.34    also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
   11.35      unfolding th1 by (simp add: mult_ac)
   11.36    also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
   11.37      unfolding  setprod_insert[OF th3] by simp
   11.38    finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] .
   11.39    then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)"
   11.40 -    by (simp add: ring_simps)
   11.41 +    by (simp add: field_simps)
   11.42  qed
   11.43  
   11.44  lemma det_row_0:
   11.45 @@ -604,7 +604,7 @@
   11.46    have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"
   11.47      unfolding setprod_timesf ..
   11.48    then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
   11.49 -        setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: ring_simps)
   11.50 +        setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: field_simps)
   11.51  qed
   11.52  
   11.53  lemma det_mul:
   11.54 @@ -681,7 +681,7 @@
   11.55          using permutes_in_image[OF q] by vector
   11.56        show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B$i$(q o inv p) i) ?U)"
   11.57          using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
   11.58 -        by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose)
   11.59 +        by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose)
   11.60      qed
   11.61    }
   11.62    then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B"
   11.63 @@ -772,7 +772,7 @@
   11.64    have fUk: "finite ?Uk" by simp
   11.65    have kUk: "k \<notin> ?Uk" by simp
   11.66    have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
   11.67 -    by (vector ring_simps)
   11.68 +    by (vector field_simps)
   11.69    have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)
   11.70    have "(\<chi> i. row i A) = A" by (vector row_def)
   11.71    then have thd1: "det (\<chi> i. row i A) = det A"  by simp
   11.72 @@ -793,7 +793,7 @@
   11.73      unfolding thd0
   11.74      unfolding det_row_mul
   11.75      unfolding th001[of k "\<lambda>i. row i A"]
   11.76 -    unfolding thd1  by (simp add: ring_simps)
   11.77 +    unfolding thd1  by (simp add: field_simps)
   11.78  qed
   11.79  
   11.80  lemma cramer_lemma:
   11.81 @@ -901,7 +901,7 @@
   11.82    have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")
   11.83    proof-
   11.84      fix x:: 'a
   11.85 -    have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps)
   11.86 +    have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: field_simps)
   11.87      have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
   11.88        apply (subst eq_iff_diff_eq_0) by simp
   11.89      have "x*x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp
   11.90 @@ -929,7 +929,7 @@
   11.91        unfolding dot_norm_neg dist_norm[symmetric]
   11.92        unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   11.93    note fc = this
   11.94 -  show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc ring_simps)
   11.95 +  show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc field_simps)
   11.96  qed
   11.97  
   11.98  lemma isometry_linear:
   11.99 @@ -980,7 +980,7 @@
  11.100        using H(5-9)
  11.101        apply (simp add: norm_eq norm_eq_1)
  11.102        apply (simp add: inner_simps smult_conv_scaleR) unfolding *
  11.103 -      by (simp add: ring_simps) }
  11.104 +      by (simp add: field_simps) }
  11.105    note th0 = this
  11.106    let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
  11.107    {fix x:: "real ^'n" assume nx: "norm x = 1"
  11.108 @@ -1079,7 +1079,7 @@
  11.109    unfolding permutes_sing
  11.110    apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
  11.111    apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
  11.112 -  by (simp add: ring_simps)
  11.113 +  by (simp add: field_simps)
  11.114  qed
  11.115  
  11.116  end
    12.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 11:34:17 2010 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 11:34:19 2010 +0200
    12.3 @@ -257,14 +257,14 @@
    12.4    | "vector_power x (Suc n) = x * vector_power x n"
    12.5  
    12.6  instance cart :: (semiring,finite) semiring
    12.7 -  apply (intro_classes) by (vector ring_simps)+
    12.8 +  apply (intro_classes) by (vector field_simps)+
    12.9  
   12.10  instance cart :: (semiring_0,finite) semiring_0
   12.11 -  apply (intro_classes) by (vector ring_simps)+
   12.12 +  apply (intro_classes) by (vector field_simps)+
   12.13  instance cart :: (semiring_1,finite) semiring_1
   12.14    apply (intro_classes) by vector
   12.15  instance cart :: (comm_semiring,finite) comm_semiring
   12.16 -  apply (intro_classes) by (vector ring_simps)+
   12.17 +  apply (intro_classes) by (vector field_simps)+
   12.18  
   12.19  instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)
   12.20  instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
   12.21 @@ -278,7 +278,7 @@
   12.22  
   12.23  instance cart :: (real_algebra,finite) real_algebra
   12.24    apply intro_classes
   12.25 -  apply (simp_all add: vector_scaleR_def ring_simps)
   12.26 +  apply (simp_all add: vector_scaleR_def field_simps)
   12.27    apply vector
   12.28    apply vector
   12.29    done
   12.30 @@ -318,19 +318,19 @@
   12.31  lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
   12.32    by (vector mult_assoc)
   12.33  lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
   12.34 -  by (vector ring_simps)
   12.35 +  by (vector field_simps)
   12.36  lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
   12.37 -  by (vector ring_simps)
   12.38 +  by (vector field_simps)
   12.39  lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
   12.40  lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
   12.41  lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
   12.42 -  by (vector ring_simps)
   12.43 +  by (vector field_simps)
   12.44  lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
   12.45  lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
   12.46  lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
   12.47  lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
   12.48  lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
   12.49 -  by (vector ring_simps)
   12.50 +  by (vector field_simps)
   12.51  
   12.52  lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
   12.53    by (simp add: Cart_eq)
   12.54 @@ -752,7 +752,7 @@
   12.55  lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
   12.56  proof-
   12.57    have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
   12.58 -  thus ?thesis by (simp add: ring_simps power2_eq_square)
   12.59 +  thus ?thesis by (simp add: field_simps power2_eq_square)
   12.60  qed
   12.61  
   12.62  lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
   12.63 @@ -828,7 +828,7 @@
   12.64  lemma norm_triangle_sub:
   12.65    fixes x y :: "'a::real_normed_vector"
   12.66    shows "norm x \<le> norm y  + norm (x - y)"
   12.67 -  using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
   12.68 +  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
   12.69  
   12.70  lemma component_le_norm: "\<bar>x$i\<bar> <= norm x"
   12.71    apply (simp add: norm_vector_def)
   12.72 @@ -867,7 +867,7 @@
   12.73  
   12.74  lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
   12.75  proof-
   12.76 -  have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square)
   12.77 +  have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: field_simps power2_eq_square)
   12.78    also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith
   12.79  finally show ?thesis ..
   12.80  qed
   12.81 @@ -898,7 +898,7 @@
   12.82    unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
   12.83  
   12.84  lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
   12.85 -  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:group_simps)
   12.86 +  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps)
   12.87  
   12.88  text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
   12.89  
   12.90 @@ -909,7 +909,7 @@
   12.91    assume ?rhs
   12.92    then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
   12.93    hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
   12.94 -  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps inner_simps inner_commute)
   12.95 +  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_simps inner_commute)
   12.96    then show "x = y" by (simp)
   12.97  qed
   12.98  
   12.99 @@ -930,7 +930,7 @@
  12.100    by (rule order_trans [OF norm_triangle_ineq add_mono])
  12.101  
  12.102  lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
  12.103 -  by (simp add: ring_simps)
  12.104 +  by (simp add: field_simps)
  12.105  
  12.106  lemma pth_1:
  12.107    fixes x :: "'a::real_normed_vector"
  12.108 @@ -1430,15 +1430,15 @@
  12.109    shows "linear f" using assms unfolding linear_def by auto
  12.110  
  12.111  lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"
  12.112 -  by (vector linear_def Cart_eq ring_simps)
  12.113 +  by (vector linear_def Cart_eq field_simps)
  12.114  
  12.115  lemma linear_compose_neg: "linear (f :: 'a ^'n \<Rightarrow> 'a::comm_ring ^'m) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)
  12.116  
  12.117  lemma linear_compose_add: "linear (f :: 'a ^'n \<Rightarrow> 'a::semiring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
  12.118 -  by (vector linear_def Cart_eq ring_simps)
  12.119 +  by (vector linear_def Cart_eq field_simps)
  12.120  
  12.121  lemma linear_compose_sub: "linear (f :: 'a ^'n \<Rightarrow> 'a::ring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
  12.122 -  by (vector linear_def Cart_eq ring_simps)
  12.123 +  by (vector linear_def Cart_eq field_simps)
  12.124  
  12.125  lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"
  12.126    by (simp add: linear_def)
  12.127 @@ -1460,7 +1460,7 @@
  12.128    shows "linear (\<lambda>x. f x $ k *s v)"
  12.129    using lf
  12.130    apply (auto simp add: linear_def )
  12.131 -  by (vector ring_simps)+
  12.132 +  by (vector field_simps)+
  12.133  
  12.134  lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)"
  12.135    unfolding linear_def
  12.136 @@ -1536,7 +1536,7 @@
  12.137        unfolding norm_mul
  12.138        apply (simp only: mult_commute)
  12.139        apply (rule mult_mono)
  12.140 -      by (auto simp add: ring_simps norm_ge_zero) }
  12.141 +      by (auto simp add: field_simps norm_ge_zero) }
  12.142      then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
  12.143      from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
  12.144      have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
  12.145 @@ -1562,7 +1562,7 @@
  12.146      {fix x::"real ^ 'n"
  12.147        have "norm (f x) \<le> ?K *  norm x"
  12.148        using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
  12.149 -      apply (auto simp add: ring_simps split add: abs_split)
  12.150 +      apply (auto simp add: field_simps split add: abs_split)
  12.151        apply (erule order_trans, simp)
  12.152        done
  12.153    }
  12.154 @@ -1631,12 +1631,12 @@
  12.155  lemma bilinear_lzero:
  12.156    fixes h :: "'a::ring^'n \<Rightarrow> _" assumes bh: "bilinear h" shows "h 0 x = 0"
  12.157    using bilinear_ladd[OF bh, of 0 0 x]
  12.158 -    by (simp add: eq_add_iff ring_simps)
  12.159 +    by (simp add: eq_add_iff field_simps)
  12.160  
  12.161  lemma bilinear_rzero:
  12.162    fixes h :: "'a::ring^_ \<Rightarrow> _" assumes bh: "bilinear h" shows "h x 0 = 0"
  12.163    using bilinear_radd[OF bh, of x 0 0 ]
  12.164 -    by (simp add: eq_add_iff ring_simps)
  12.165 +    by (simp add: eq_add_iff field_simps)
  12.166  
  12.167  lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ _)) z = h x z - h y z"
  12.168    by (simp  add: diff_def bilinear_ladd bilinear_lneg)
  12.169 @@ -1677,7 +1677,7 @@
  12.170        apply (rule real_setsum_norm_le)
  12.171        using fN fM
  12.172        apply simp
  12.173 -      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
  12.174 +      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul field_simps)
  12.175        apply (rule mult_mono)
  12.176        apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
  12.177        apply (rule mult_mono)
  12.178 @@ -1767,7 +1767,7 @@
  12.179          by (simp add: linear_cmul[OF lf])
  12.180        finally have "f x \<bullet> y = x \<bullet> ?w"
  12.181          apply (simp only: )
  12.182 -        apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)
  12.183 +        apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps)
  12.184          done}
  12.185    }
  12.186    then show ?thesis unfolding adjoint_def
  12.187 @@ -1832,7 +1832,7 @@
  12.188  
  12.189  lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
  12.190  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
  12.191 -  by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
  12.192 +  by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps)
  12.193  
  12.194  lemma matrix_mul_lid:
  12.195    fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  12.196 @@ -1951,7 +1951,7 @@
  12.197  where "matrix f = (\<chi> i j. (f(basis j))$i)"
  12.198  
  12.199  lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ _))"
  12.200 -  by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf)
  12.201 +  by (simp add: linear_def matrix_vector_mult_def Cart_eq field_simps setsum_right_distrib setsum_addf)
  12.202  
  12.203  lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)"
  12.204  apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute)
  12.205 @@ -2005,7 +2005,7 @@
  12.206  proof-
  12.207    have uv': "u = 0 \<longrightarrow> v \<noteq> 0" using u v uv by arith
  12.208    have "a = a * (u + v)" unfolding uv  by simp
  12.209 -  hence th: "u * a + v * a = a" by (simp add: ring_simps)
  12.210 +  hence th: "u * a + v * a = a" by (simp add: field_simps)
  12.211    from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_compare_simps)
  12.212    from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_compare_simps)
  12.213    from xa ya u v have "u * x + v * y < u * a + v * a"
  12.214 @@ -2028,7 +2028,7 @@
  12.215    shows "u * x + v * y \<le> a"
  12.216  proof-
  12.217    from xa ya u v have "u * x + v * y \<le> u * a + v * a" by (simp add: add_mono mult_left_mono)
  12.218 -  also have "\<dots> \<le> (u + v) * a" by (simp add: ring_simps)
  12.219 +  also have "\<dots> \<le> (u + v) * a" by (simp add: field_simps)
  12.220    finally show ?thesis unfolding uv by simp
  12.221  qed
  12.222  
  12.223 @@ -2049,7 +2049,7 @@
  12.224    shows "x <= y + z"
  12.225  proof-
  12.226    have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y  by (simp add: zero_compare_simps)
  12.227 -  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square ring_simps)
  12.228 +  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
  12.229    from y z have yz: "y + z \<ge> 0" by arith
  12.230    from power2_le_imp_le[OF th yz] show ?thesis .
  12.231  qed
  12.232 @@ -2534,9 +2534,9 @@
  12.233    from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp
  12.234    from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp
  12.235    also have "\<dots> \<le> (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric])
  12.236 -    apply (simp add: ring_simps)
  12.237 +    apply (simp add: field_simps)
  12.238      using mult_left_mono[OF p Suc.prems] by simp
  12.239 -  finally show ?case  by (simp add: real_of_nat_Suc ring_simps)
  12.240 +  finally show ?case  by (simp add: real_of_nat_Suc field_simps)
  12.241  qed
  12.242  
  12.243  lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
  12.244 @@ -2602,10 +2602,10 @@
  12.245      from geometric_sum[OF x1, of "Suc n", unfolded x1']
  12.246      have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
  12.247        unfolding atLeastLessThanSuc_atLeastAtMost
  12.248 -      using x1' apply (auto simp only: field_eq_simps)
  12.249 -      apply (simp add: ring_simps)
  12.250 +      using x1' apply (auto simp only: field_simps)
  12.251 +      apply (simp add: field_simps)
  12.252        done
  12.253 -    then have ?thesis by (simp add: ring_simps) }
  12.254 +    then have ?thesis by (simp add: field_simps) }
  12.255    ultimately show ?thesis by metis
  12.256  qed
  12.257  
  12.258 @@ -2624,7 +2624,7 @@
  12.259    from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
  12.260    have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
  12.261    then show ?thesis unfolding sum_gp_basic using mn
  12.262 -    by (simp add: ring_simps power_add[symmetric])
  12.263 +    by (simp add: field_simps power_add[symmetric])
  12.264  qed
  12.265  
  12.266  lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
  12.267 @@ -2637,7 +2637,7 @@
  12.268      {assume x: "x = 1"  hence ?thesis by simp}
  12.269      moreover
  12.270      {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
  12.271 -      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_eq_simps)}
  12.272 +      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
  12.273      ultimately have ?thesis by metis
  12.274    }
  12.275    ultimately show ?thesis by metis
  12.276 @@ -2646,7 +2646,7 @@
  12.277  lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
  12.278    (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
  12.279    unfolding sum_gp[of x m "m + n"] power_Suc
  12.280 -  by (simp add: ring_simps power_add)
  12.281 +  by (simp add: field_simps power_add)
  12.282  
  12.283  
  12.284  subsection{* A bit of linear algebra. *}
  12.285 @@ -2920,14 +2920,14 @@
  12.286      apply (simp only: )
  12.287      apply (rule span_add[unfolded mem_def])
  12.288      apply assumption+
  12.289 -    apply (vector ring_simps)
  12.290 +    apply (vector field_simps)
  12.291      apply (clarsimp simp add: mem_def)
  12.292      apply (rule_tac x= "c*k" in exI)
  12.293      apply (subgoal_tac "c *s x - (c * k) *s b = c*s (x - k*s b)")
  12.294      apply (simp only: )
  12.295      apply (rule span_mul[unfolded mem_def])
  12.296      apply assumption
  12.297 -    by (vector ring_simps)
  12.298 +    by (vector field_simps)
  12.299    ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis
  12.300  qed
  12.301  
  12.302 @@ -3073,7 +3073,7 @@
  12.303            setsum_clauses(2)[OF fS] cong del: if_weak_cong)
  12.304        also have "\<dots> = (\<Sum>v\<in>S. u v *s v) + c *s x"
  12.305          apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]])
  12.306 -        by (vector ring_simps)
  12.307 +        by (vector field_simps)
  12.308        also have "\<dots> = c*s x + y"
  12.309          by (simp add: add_commute u)
  12.310        finally have "setsum (\<lambda>v. ?u v *s v) ?S = c*s x + y" .
  12.311 @@ -3110,7 +3110,7 @@
  12.312      from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto
  12.313      have s0: "setsum (\<lambda>v. ?u v *s v) ?S = 0"
  12.314        using fS aS
  12.315 -      apply (simp add: vector_smult_lneg vector_smult_lid setsum_clauses ring_simps )
  12.316 +      apply (simp add: vector_smult_lneg vector_smult_lid setsum_clauses field_simps )
  12.317        apply (subst (2) ua[symmetric])
  12.318        apply (rule setsum_cong2)
  12.319        by auto
  12.320 @@ -3643,7 +3643,7 @@
  12.321    from C(1) have fC: "finite ?C" by simp
  12.322    from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)" by (simp add: card_insert_if)
  12.323    {fix x k
  12.324 -    have th0: "\<And>(a::'b::comm_ring) b c. a - (b - c) = c + (a - b)" by (simp add: ring_simps)
  12.325 +    have th0: "\<And>(a::'b::comm_ring) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps)
  12.326      have "x - k *s (a - (\<Sum>x\<in>C. (x \<bullet> a / (x \<bullet> x)) *s x)) \<in> span C \<longleftrightarrow> x - k *s a \<in> span C"
  12.327        apply (simp only: vector_ssub_ldistrib th0)
  12.328        apply (rule span_add_eq)
  12.329 @@ -3863,7 +3863,7 @@
  12.330        using z .
  12.331      {fix k assume k: "z - k *s a \<in> span b"
  12.332        have eq: "z - ?h z *s a - (z - k*s a) = (k - ?h z) *s a"
  12.333 -        by (simp add: ring_simps vector_sadd_rdistrib[symmetric])
  12.334 +        by (simp add: field_simps vector_sadd_rdistrib[symmetric])
  12.335        from span_sub[OF th0 k]
  12.336        have khz: "(k - ?h z) *s a \<in> span b" by (simp add: eq)
  12.337        {assume "k \<noteq> ?h z" hence k0: "k - ?h z \<noteq> 0" by simp
  12.338 @@ -3877,7 +3877,7 @@
  12.339    let ?g = "\<lambda>z. ?h z *s f a + g (z - ?h z *s a)"
  12.340    {fix x y assume x: "x \<in> span (insert a b)" and y: "y \<in> span (insert a b)"
  12.341      have tha: "\<And>(x::'a^'n) y a k l. (x + y) - (k + l) *s a = (x - k *s a) + (y - l *s a)"
  12.342 -      by (vector ring_simps)
  12.343 +      by (vector field_simps)
  12.344      have addh: "?h (x + y) = ?h x + ?h y"
  12.345        apply (rule conjunct2[OF h, rule_format, symmetric])
  12.346        apply (rule span_add[OF x y])
  12.347 @@ -3890,14 +3890,14 @@
  12.348    moreover
  12.349    {fix x:: "'a^'n" and c:: 'a  assume x: "x \<in> span (insert a b)"
  12.350      have tha: "\<And>(x::'a^'n) c k a. c *s x - (c * k) *s a = c *s (x - k *s a)"
  12.351 -      by (vector ring_simps)
  12.352 +      by (vector field_simps)
  12.353      have hc: "?h (c *s x) = c * ?h x"
  12.354        apply (rule conjunct2[OF h, rule_format, symmetric])
  12.355        apply (metis span_mul x)
  12.356        by (metis tha span_mul x conjunct1[OF h])
  12.357      have "?g (c *s x) = c*s ?g x"
  12.358        unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]]
  12.359 -      by (vector ring_simps)}
  12.360 +      by (vector field_simps)}
  12.361    moreover
  12.362    {fix x assume x: "x \<in> (insert a b)"
  12.363      {assume xa: "x = a"
  12.364 @@ -4276,7 +4276,7 @@
  12.365              fix j
  12.366              have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
  12.367             else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" using i(1)
  12.368 -              by (simp add: ring_simps)
  12.369 +              by (simp add: field_simps)
  12.370              have "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
  12.371             else (x$xa) * ((column xa A$j))) ?U = setsum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U"
  12.372                apply (rule setsum_cong[OF refl])
  12.373 @@ -4619,7 +4619,7 @@
  12.374    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
  12.375    have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
  12.376      "infnorm y \<le> infnorm (x - y) + infnorm x"
  12.377 -    by (simp_all add: ring_simps infnorm_neg diff_def[symmetric])
  12.378 +    by (simp_all add: field_simps infnorm_neg diff_def[symmetric])
  12.379    from th[OF ths]  show ?thesis .
  12.380  qed
  12.381  
  12.382 @@ -4718,9 +4718,9 @@
  12.383        using x y
  12.384        unfolding inner_simps smult_conv_scaleR
  12.385        unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute)
  12.386 -      apply (simp add: ring_simps) by metis
  12.387 +      apply (simp add: field_simps) by metis
  12.388      also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
  12.389 -      by (simp add: ring_simps inner_commute)
  12.390 +      by (simp add: field_simps inner_commute)
  12.391      also have "\<dots> \<longleftrightarrow> ?lhs" using x y
  12.392        apply simp
  12.393        by metis
  12.394 @@ -4766,7 +4766,7 @@
  12.395      also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
  12.396        unfolding norm_cauchy_schwarz_eq[symmetric]
  12.397        unfolding power2_norm_eq_inner inner_simps
  12.398 -      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute ring_simps)
  12.399 +      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
  12.400      finally have ?thesis .}
  12.401    ultimately show ?thesis by blast
  12.402  qed
  12.403 @@ -4852,10 +4852,10 @@
  12.404  unfolding vector_smult_assoc
  12.405  unfolding norm_mul
  12.406  apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
  12.407 -apply (case_tac "c <= 0", simp add: ring_simps)
  12.408 -apply (simp add: ring_simps)
  12.409 -apply (case_tac "c <= 0", simp add: ring_simps)
  12.410 -apply (simp add: ring_simps)
  12.411 +apply (case_tac "c <= 0", simp add: field_simps)
  12.412 +apply (simp add: field_simps)
  12.413 +apply (case_tac "c <= 0", simp add: field_simps)
  12.414 +apply (simp add: field_simps)
  12.415  apply simp
  12.416  apply simp
  12.417  done
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 11:34:17 2010 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 11:34:19 2010 +0200
    13.3 @@ -1131,7 +1131,7 @@
    13.4      guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this
    13.5      guess p by(rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this
    13.6      let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
    13.7 -      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:group_simps norm_minus_commute)
    13.8 +      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] by(auto simp add:algebra_simps norm_minus_commute)
    13.9      also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
   13.10        apply(rule add_strict_mono) apply(rule_tac[!] d2(2) d1(2)) using p unfolding fine_def by auto
   13.11      finally show False by auto
   13.12 @@ -1244,7 +1244,7 @@
   13.13            unfolding scaleR_right_distrib setsum_addf[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,THEN sym]
   13.14            by(rule setsum_cong2,auto)
   13.15          have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) = norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
   13.16 -          unfolding * by(auto simp add:group_simps) also let ?res = "\<dots>"
   13.17 +          unfolding * by(auto simp add:algebra_simps) also let ?res = "\<dots>"
   13.18          from as have *:"d1 fine p" "d2 fine p" unfolding fine_inter by auto
   13.19          have "?res < e/2 + e/2" apply(rule le_less_trans[OF norm_triangle_ineq])
   13.20            apply(rule add_strict_mono) using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)] by auto
   13.21 @@ -1268,7 +1268,7 @@
   13.22  
   13.23  lemma has_integral_sub:
   13.24    shows "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) has_integral (k - l)) s"
   13.25 -  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding group_simps by auto
   13.26 +  using has_integral_add[OF _ has_integral_neg,of f k s g l] unfolding algebra_simps by auto
   13.27  
   13.28  lemma integral_0: "integral s (\<lambda>x::real^'n. 0::real^'m) = 0"
   13.29    by(rule integral_unique has_integral_0)+
   13.30 @@ -1703,7 +1703,7 @@
   13.31        proof- guess p using fine_division_exists[OF d(1), of a' b] . note p=this
   13.32          show ?thesis using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
   13.33            using as unfolding interval_split b'_def[symmetric] a'_def[symmetric]
   13.34 -          using p using assms by(auto simp add:group_simps)
   13.35 +          using p using assms by(auto simp add:algebra_simps)
   13.36        qed qed  
   13.37      show "?P {x. x $ k \<ge> c}" apply(rule_tac x=d in exI) apply(rule,rule d) apply(rule,rule,rule)
   13.38      proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b} \<inter> {x. x $ k \<ge> c} \<and> d fine p1 \<and> p2 tagged_division_of {a..b} \<inter> {x. x $ k \<ge> c} \<and> d fine p2"
   13.39 @@ -1711,7 +1711,7 @@
   13.40        proof- guess p using fine_division_exists[OF d(1), of a b'] . note p=this
   13.41          show ?thesis using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
   13.42            using as unfolding interval_split b'_def[symmetric] a'_def[symmetric]
   13.43 -          using p using assms by(auto simp add:group_simps) qed qed qed qed
   13.44 +          using p using assms by(auto simp add:algebra_simps) qed qed qed qed
   13.45  
   13.46  subsection {* Generalized notion of additivity. *}
   13.47  
   13.48 @@ -1848,7 +1848,7 @@
   13.49  
   13.50  lemma monoidal_monoid[intro]:
   13.51    shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
   13.52 -  unfolding monoidal_def neutral_monoid by(auto simp add: group_simps) 
   13.53 +  unfolding monoidal_def neutral_monoid by(auto simp add: algebra_simps) 
   13.54  
   13.55  lemma operative_integral: fixes f::"real^'n \<Rightarrow> 'a::banach"
   13.56    shows "operative (lifted(op +)) (\<lambda>i. if f integrable_on i then Some(integral i f) else None)"
   13.57 @@ -2381,8 +2381,8 @@
   13.58        have lem2:"\<And>s1 s2 i1 i2. norm(s2 - s1) \<le> e/2 \<Longrightarrow> norm(s1 - i1) < e / 4 \<Longrightarrow> norm(s2 - i2) < e / 4 \<Longrightarrow>norm(i1 - i2) < e"
   13.59        proof- case goal1 have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
   13.60            using norm_triangle_ineq[of "i1 - s1" "s1 - i2"]
   13.61 -          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"] by(auto simp add:group_simps)
   13.62 -        also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:group_simps)
   13.63 +          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"] by(auto simp add:algebra_simps)
   13.64 +        also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
   13.65          finally show ?case .
   13.66        qed
   13.67        show ?case unfolding vector_dist_norm apply(rule lem2) defer
   13.68 @@ -2399,7 +2399,7 @@
   13.69          also have "\<dots> = 2 / real M" unfolding real_divide_def by auto
   13.70          finally show "norm (g n x - g m x) \<le> 2 / real M"
   13.71            using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
   13.72 -          by(auto simp add:group_simps simp add:norm_minus_commute)
   13.73 +          by(auto simp add:algebra_simps simp add:norm_minus_commute)
   13.74        qed qed qed
   13.75    from this[unfolded convergent_eq_cauchy[THEN sym]] guess s .. note s=this
   13.76  
   13.77 @@ -2413,8 +2413,8 @@
   13.78      have lem:"\<And>sf sg i. norm(sf - sg) \<le> e / 3 \<Longrightarrow> norm(i - s) < e / 3 \<Longrightarrow> norm(sg - i) < e / 3 \<Longrightarrow> norm(sf - s) < e"
   13.79      proof- case goal1 have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
   13.80          using norm_triangle_ineq[of "sf - sg" "sg - s"]
   13.81 -        using norm_triangle_ineq[of "sg -  i" " i - s"] by(auto simp add:group_simps)
   13.82 -      also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:group_simps)
   13.83 +        using norm_triangle_ineq[of "sg -  i" " i - s"] by(auto simp add:algebra_simps)
   13.84 +      also have "\<dots> < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps)
   13.85        finally show ?case .
   13.86      qed
   13.87      show ?case apply(rule_tac x=g' in exI) apply(rule,rule g')
   13.88 @@ -2956,7 +2956,7 @@
   13.89        have ball:"\<forall>xa\<in>k. xa \<in> ball x (d (dest_vec1 x))" using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`,unfolded split_conv subset_eq] .
   13.90        have "norm ((v$1 - u$1) *\<^sub>R f' x - (f v - f u)) \<le> norm (f u - f x - (u$1 - x$1) *\<^sub>R f' x) + norm (f v - f x - (v$1 - x$1) *\<^sub>R f' x)"
   13.91          apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
   13.92 -        unfolding scaleR.diff_left by(auto simp add:group_simps)
   13.93 +        unfolding scaleR.diff_left by(auto simp add:algebra_simps)
   13.94        also have "... \<le> e * norm (dest_vec1 u - dest_vec1 x) + e * norm (dest_vec1 v - dest_vec1 x)"
   13.95          apply(rule add_mono) apply(rule d(2)[of "x$1" "u$1",unfolded o_def vec1_dest_vec1]) prefer 4
   13.96          apply(rule d(2)[of "x$1" "v$1",unfolded o_def vec1_dest_vec1])
   13.97 @@ -3098,7 +3098,7 @@
   13.98    proof(rule,rule,rule d,safe) case goal1 show ?case proof(cases "y < x")
   13.99        case False have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 y}" apply(rule integrable_subinterval,rule integrable_continuous)
  13.100          apply(rule continuous_on_o_dest_vec1 assms)+  unfolding not_less using assms(2) goal1 by auto
  13.101 -      hence *:"?I a y - ?I a x = ?I x y" unfolding group_simps apply(subst eq_commute) apply(rule integral_combine)
  13.102 +      hence *:"?I a y - ?I a x = ?I x y" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
  13.103          using False unfolding not_less using assms(2) goal1 by auto
  13.104        have **:"norm (y - x) = content {vec1 x..vec1 y}" apply(subst content_1) using False unfolding not_less by auto
  13.105        show ?thesis unfolding ** apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x) o dest_vec1"]) unfolding * unfolding o_def
  13.106 @@ -3112,7 +3112,7 @@
  13.107        qed(insert e,auto)
  13.108      next case True have "f \<circ> dest_vec1 integrable_on {vec1 a..vec1 x}" apply(rule integrable_subinterval,rule integrable_continuous)
  13.109          apply(rule continuous_on_o_dest_vec1 assms)+  unfolding not_less using assms(2) goal1 by auto
  13.110 -      hence *:"?I a x - ?I a y = ?I y x" unfolding group_simps apply(subst eq_commute) apply(rule integral_combine)
  13.111 +      hence *:"?I a x - ?I a y = ?I y x" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
  13.112          using True using assms(2) goal1 by auto
  13.113        have **:"norm (y - x) = content {vec1 y..vec1 x}" apply(subst content_1) using True unfolding not_less by auto
  13.114        have ***:"\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" unfolding scaleR_left.diff by auto 
  13.115 @@ -3194,7 +3194,7 @@
  13.116            apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI)
  13.117            using X(2) assms(3)[rule_format,of x] by auto
  13.118        qed note ** = d(2)[OF this] have *:"inj_on (\<lambda>(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastsimp
  13.119 -       have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding group_simps add_left_cancel
  13.120 +       have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
  13.121          unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
  13.122          apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
  13.123        also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym]
  13.124 @@ -3332,7 +3332,7 @@
  13.125  
  13.126  lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
  13.127    apply(subst(asm)(2) norm_minus_cancel[THEN sym])
  13.128 -  apply(drule norm_triangle_le) by(auto simp add:group_simps)
  13.129 +  apply(drule norm_triangle_le) by(auto simp add:algebra_simps)
  13.130  
  13.131  lemma fundamental_theorem_of_calculus_interior:
  13.132    assumes"a \<le> b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
  13.133 @@ -3641,11 +3641,11 @@
  13.134    proof safe show "0 < ?d" using d(1) assms(3) unfolding Cart_simps by auto
  13.135      fix t::"_^1" assume as:"c \<le> t" "t$1 < c$1 + ?d"
  13.136      have *:"integral{a..c} f = integral{a..b} f - integral{c..b} f"
  13.137 -      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding group_simps
  13.138 +      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding algebra_simps
  13.139        apply(rule_tac[!] integral_combine) using assms as unfolding Cart_simps by auto
  13.140      have "(- c)$1 - d < (- t)$1 \<and> - t \<le> - c" using as by auto note d(2)[rule_format,OF this]
  13.141      thus "norm (integral {a..c} f - integral {a..t} f) < e" unfolding * 
  13.142 -      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:group_simps) qed qed
  13.143 +      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:algebra_simps) qed qed
  13.144  
  13.145  declare dest_vec1_eq[simp del] not_less[simp] not_le[simp]
  13.146  
  13.147 @@ -3715,7 +3715,7 @@
  13.148      apply safe apply(rule conv) using assms(4,7) by auto
  13.149    have *:"\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
  13.150    proof- case goal1 hence "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c" 
  13.151 -      unfolding scaleR_simps by(auto simp add:group_simps)
  13.152 +      unfolding scaleR_simps by(auto simp add:algebra_simps)
  13.153      thus ?case using `x\<noteq>c` by auto qed
  13.154    have as2:"finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}" using assms(2) 
  13.155      apply(rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
  13.156 @@ -4390,7 +4390,7 @@
  13.157    have *:"\<And>ir ip i cr cp. norm((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow> 
  13.158      ip + ir = i \<Longrightarrow> norm(cp - ip) \<le> e + k" 
  13.159    proof- case goal1 thus ?case  using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"]  
  13.160 -      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed
  13.161 +      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:algebra_simps) qed
  13.162    
  13.163    have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
  13.164      unfolding split_def setsum_subtractf ..
  13.165 @@ -4501,7 +4501,7 @@
  13.166              norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e" 
  13.167        proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
  13.168            norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel
  13.169 -          by(auto simp add:group_simps) qed
  13.170 +          by(auto simp add:algebra_simps) qed
  13.171        show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where
  13.172            b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
  13.173        proof safe case goal1
  13.174 @@ -5152,7 +5152,7 @@
  13.175    assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  13.176    shows "(\<lambda>x. f(x) - g(x)) absolutely_integrable_on s"
  13.177    using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
  13.178 -  unfolding group_simps .
  13.179 +  unfolding algebra_simps .
  13.180  
  13.181  lemma absolutely_integrable_linear: fixes f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
  13.182    assumes "f absolutely_integrable_on s" "bounded_linear h"
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 11:34:17 2010 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 11:34:19 2010 +0200
    14.3 @@ -4442,7 +4442,7 @@
    14.4    let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
    14.5    obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
    14.6    { fix x y assume "x \<in> s" "y \<in> s"
    14.7 -    hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
    14.8 +    hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: field_simps)  }
    14.9    note * = this
   14.10    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
   14.11      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`  
   14.12 @@ -5752,7 +5752,7 @@
   14.13    shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
   14.14  proof
   14.15    assume h: "m *s x + c = y"
   14.16 -  hence "m *s x = y - c" by (simp add: ring_simps)
   14.17 +  hence "m *s x = y - c" by (simp add: field_simps)
   14.18    hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
   14.19    then show "x = inverse m *s y + - (inverse m *s c)"
   14.20      using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
   14.21 @@ -5854,11 +5854,11 @@
   14.22        also have "\<dots> \<le> (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"
   14.23          using cf_z[of "m + k"] and c by auto
   14.24        also have "\<dots> \<le> c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
   14.25 -        using Suc by (auto simp add: ring_simps)
   14.26 +        using Suc by (auto simp add: field_simps)
   14.27        also have "\<dots> = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
   14.28 -        unfolding power_add by (auto simp add: ring_simps)
   14.29 +        unfolding power_add by (auto simp add: field_simps)
   14.30        also have "\<dots> \<le> (c ^ m) * d * (1 - c ^ Suc k)"
   14.31 -        using c by (auto simp add: ring_simps)
   14.32 +        using c by (auto simp add: field_simps)
   14.33        finally show ?case by auto
   14.34      qed
   14.35    } note cf_z2 = this
   14.36 @@ -6015,7 +6015,7 @@
   14.37          apply(erule_tac x="Na+Nb+n" in allE) apply simp
   14.38          using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
   14.39            "-b"  "- f (r (Na + Nb + n)) y"]
   14.40 -        unfolding ** unfolding group_simps(12) by (auto simp add: dist_commute)
   14.41 +        unfolding ** by (auto simp add: algebra_simps dist_commute)
   14.42        moreover
   14.43        have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
   14.44          using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
    15.1 --- a/src/HOL/NSA/HyperDef.thy	Mon Apr 26 11:34:17 2010 +0200
    15.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 26 11:34:19 2010 +0200
    15.3 @@ -140,12 +140,12 @@
    15.4  
    15.5  lemma of_hypreal_inverse [simp]:
    15.6    "\<And>x. of_hypreal (inverse x) =
    15.7 -   inverse (of_hypreal x :: 'a::{real_div_algebra,division_by_zero} star)"
    15.8 +   inverse (of_hypreal x :: 'a::{real_div_algebra,division_ring_inverse_zero} star)"
    15.9  by transfer (rule of_real_inverse)
   15.10  
   15.11  lemma of_hypreal_divide [simp]:
   15.12    "\<And>x y. of_hypreal (x / y) =
   15.13 -   (of_hypreal x / of_hypreal y :: 'a::{real_field,division_by_zero} star)"
   15.14 +   (of_hypreal x / of_hypreal y :: 'a::{real_field,division_ring_inverse_zero} star)"
   15.15  by transfer (rule of_real_divide)
   15.16  
   15.17  lemma of_hypreal_eq_iff [simp]:
   15.18 @@ -454,7 +454,7 @@
   15.19  by transfer (rule field_power_not_zero)
   15.20  
   15.21  lemma hyperpow_inverse:
   15.22 -  "\<And>r n. r \<noteq> (0::'a::{division_by_zero,field} star)
   15.23 +  "\<And>r n. r \<noteq> (0::'a::{division_ring_inverse_zero,field} star)
   15.24     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
   15.25  by transfer (rule power_inverse)
   15.26    
    16.1 --- a/src/HOL/Number_Theory/Binomial.thy	Mon Apr 26 11:34:17 2010 +0200
    16.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Mon Apr 26 11:34:19 2010 +0200
    16.3 @@ -208,7 +208,7 @@
    16.4    have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
    16.5        fact (k + 1) * fact (n - k) * (n choose (k + 1)) + 
    16.6        fact (k + 1) * fact (n - k) * (n choose k)" 
    16.7 -    by (subst choose_reduce_nat, auto simp add: ring_simps)
    16.8 +    by (subst choose_reduce_nat, auto simp add: field_simps)
    16.9    also note one
   16.10    also note two
   16.11    also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
   16.12 @@ -279,7 +279,7 @@
   16.13    also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
   16.14                    (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
   16.15      by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le 
   16.16 -             power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
   16.17 +             power_Suc field_simps One_nat_def del:setsum_cl_ivl_Suc)
   16.18    also have "... = a^(n+1) + b^(n+1) +
   16.19                    (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
   16.20                    (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
   16.21 @@ -287,10 +287,10 @@
   16.22    also have
   16.23        "... = a^(n+1) + b^(n+1) + 
   16.24           (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
   16.25 -    by (auto simp add: ring_simps setsum_addf [symmetric]
   16.26 +    by (auto simp add: field_simps setsum_addf [symmetric]
   16.27        choose_reduce_nat)
   16.28    also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
   16.29 -    using decomp by (simp add: ring_simps)
   16.30 +    using decomp by (simp add: field_simps)
   16.31    finally show "?P (n + 1)" by simp
   16.32  qed
   16.33  
    17.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Apr 26 11:34:17 2010 +0200
    17.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Apr 26 11:34:19 2010 +0200
    17.3 @@ -350,7 +350,7 @@
    17.4    apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
    17.5    (* any way around this? *)
    17.6    apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
    17.7 -  apply (auto simp add: ring_simps)
    17.8 +  apply (auto simp add: field_simps)
    17.9  done
   17.10  
   17.11  lemma cong_mult_rcancel_int:
   17.12 @@ -416,7 +416,7 @@
   17.13  done
   17.14  
   17.15  lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   17.16 -  apply (auto simp add: cong_altdef_int dvd_def ring_simps)
   17.17 +  apply (auto simp add: cong_altdef_int dvd_def field_simps)
   17.18    apply (rule_tac [!] x = "-k" in exI, auto)
   17.19  done
   17.20  
   17.21 @@ -428,14 +428,14 @@
   17.22    apply (unfold dvd_def, auto)
   17.23    apply (rule_tac x = k in exI)
   17.24    apply (rule_tac x = 0 in exI)
   17.25 -  apply (auto simp add: ring_simps)
   17.26 +  apply (auto simp add: field_simps)
   17.27    apply (subst (asm) cong_sym_eq_nat)
   17.28    apply (subst (asm) cong_altdef_nat)
   17.29    apply force
   17.30    apply (unfold dvd_def, auto)
   17.31    apply (rule_tac x = 0 in exI)
   17.32    apply (rule_tac x = k in exI)
   17.33 -  apply (auto simp add: ring_simps)
   17.34 +  apply (auto simp add: field_simps)
   17.35    apply (unfold cong_nat_def)
   17.36    apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   17.37    apply (erule ssubst)back
   17.38 @@ -533,7 +533,7 @@
   17.39    apply (auto simp add: cong_iff_lin_nat dvd_def)
   17.40    apply (rule_tac x="k1 * k" in exI)
   17.41    apply (rule_tac x="k2 * k" in exI)
   17.42 -  apply (simp add: ring_simps)
   17.43 +  apply (simp add: field_simps)
   17.44  done
   17.45  
   17.46  lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   17.47 @@ -559,7 +559,7 @@
   17.48  lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   17.49    apply (simp add: cong_altdef_int)
   17.50    apply (subst dvd_minus_iff [symmetric])
   17.51 -  apply (simp add: ring_simps)
   17.52 +  apply (simp add: field_simps)
   17.53  done
   17.54  
   17.55  lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   17.56 @@ -603,7 +603,7 @@
   17.57    apply (unfold dvd_def)
   17.58    apply auto [1]
   17.59    apply (rule_tac x = k in exI)
   17.60 -  apply (auto simp add: ring_simps) [1]
   17.61 +  apply (auto simp add: field_simps) [1]
   17.62    apply (subst cong_altdef_nat)
   17.63    apply (auto simp add: dvd_def)
   17.64  done
   17.65 @@ -611,7 +611,7 @@
   17.66  lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   17.67    apply (subst cong_altdef_nat)
   17.68    apply assumption
   17.69 -  apply (unfold dvd_def, auto simp add: ring_simps)
   17.70 +  apply (unfold dvd_def, auto simp add: field_simps)
   17.71    apply (rule_tac x = k in exI)
   17.72    apply auto
   17.73  done
    18.1 --- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:17 2010 +0200
    18.2 +++ b/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:19 2010 +0200
    18.3 @@ -143,9 +143,9 @@
    18.4    apply (induct n rule: fib_induct_nat)
    18.5    apply auto
    18.6    apply (subst fib_reduce_nat)
    18.7 -  apply (auto simp add: ring_simps)
    18.8 +  apply (auto simp add: field_simps)
    18.9    apply (subst (1 3 5) fib_reduce_nat)
   18.10 -  apply (auto simp add: ring_simps Suc_eq_plus1)
   18.11 +  apply (auto simp add: field_simps Suc_eq_plus1)
   18.12  (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   18.13    apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   18.14    apply (erule ssubst) back back
   18.15 @@ -184,7 +184,7 @@
   18.16  lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) - 
   18.17      (fib (int n + 1))^2 = (-1)^(n + 1)"
   18.18    apply (induct n)
   18.19 -  apply (auto simp add: ring_simps power2_eq_square fib_reduce_int
   18.20 +  apply (auto simp add: field_simps power2_eq_square fib_reduce_int
   18.21        power_add)
   18.22  done
   18.23  
   18.24 @@ -222,7 +222,7 @@
   18.25    apply (subst (2) fib_reduce_nat)
   18.26    apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   18.27    apply (subst add_commute, auto)
   18.28 -  apply (subst gcd_commute_nat, auto simp add: ring_simps)
   18.29 +  apply (subst gcd_commute_nat, auto simp add: field_simps)
   18.30  done
   18.31  
   18.32  lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   18.33 @@ -305,7 +305,7 @@
   18.34  theorem fib_mult_eq_setsum_nat:
   18.35      "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   18.36    apply (induct n)
   18.37 -  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps)
   18.38 +  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
   18.39  done
   18.40  
   18.41  theorem fib_mult_eq_setsum'_nat:
    19.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Apr 26 11:34:17 2010 +0200
    19.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Apr 26 11:34:19 2010 +0200
    19.3 @@ -69,7 +69,7 @@
    19.4    apply (subst mod_add_eq [symmetric])
    19.5    apply (subst mult_commute)
    19.6    apply (subst zmod_zmult1_eq [symmetric])
    19.7 -  apply (simp add: ring_simps)
    19.8 +  apply (simp add: field_simps)
    19.9  done
   19.10  
   19.11  end
    20.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Mon Apr 26 11:34:17 2010 +0200
    20.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Mon Apr 26 11:34:19 2010 +0200
    20.3 @@ -1137,7 +1137,8 @@
    20.4    handle THM _ => NONE
    20.5  in
    20.6  val z3_simpset = HOL_ss addsimps @{thms array_rules}
    20.7 -  addsimps @{thms ring_distribs} addsimps @{thms field_eq_simps}
    20.8 +  addsimps @{thms ring_distribs} addsimps @{thms field_simps}
    20.9 +  addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
   20.10    addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
   20.11    addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
   20.12    addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
    21.1 --- a/src/HOL/SMT/Z3.thy	Mon Apr 26 11:34:17 2010 +0200
    21.2 +++ b/src/HOL/SMT/Z3.thy	Mon Apr 26 11:34:19 2010 +0200
    21.3 @@ -19,7 +19,7 @@
    21.4  
    21.5  lemmas [z3_rewrite] =
    21.6    refl eq_commute conj_commute disj_commute simp_thms nnf_simps
    21.7 -  ring_distribs field_eq_simps if_True if_False
    21.8 +  ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False
    21.9  
   21.10  lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast
   21.11  
    22.1 --- a/src/HOL/SetInterval.thy	Mon Apr 26 11:34:17 2010 +0200
    22.2 +++ b/src/HOL/SetInterval.thy	Mon Apr 26 11:34:19 2010 +0200
    22.3 @@ -1095,7 +1095,7 @@
    22.4    next
    22.5      case (Suc n)
    22.6      moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
    22.7 -    ultimately show ?case by (simp add: field_eq_simps divide_inverse)
    22.8 +    ultimately show ?case by (simp add: field_simps divide_inverse)
    22.9    qed
   22.10    ultimately show ?thesis by simp
   22.11  qed
    23.1 --- a/src/HOL/ex/Lagrange.thy	Mon Apr 26 11:34:17 2010 +0200
    23.2 +++ b/src/HOL/ex/Lagrange.thy	Mon Apr 26 11:34:19 2010 +0200
    23.3 @@ -34,7 +34,7 @@
    23.4     sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    23.5     sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    23.6     sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    23.7 -by (simp only: sq_def ring_simps)
    23.8 +by (simp only: sq_def field_simps)
    23.9  
   23.10  
   23.11  text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
   23.12 @@ -50,6 +50,6 @@
   23.13        sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
   23.14        sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
   23.15        sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
   23.16 -by (simp only: sq_def ring_simps)
   23.17 +by (simp only: sq_def field_simps)
   23.18  
   23.19  end