tuned and renamed group_eq_simps and ring_eq_simps
authornipkow
Sat Jun 23 19:33:22 2007 +0200 (2007-06-23)
changeset 23477f4b83f03cac9
parent 23476 839db6346cc8
child 23478 26a5ef187e8b
tuned and renamed group_eq_simps and ring_eq_simps
src/HOL/Arith_Tools.thy
src/HOL/Complex/Complex.thy
src/HOL/Complex/ex/BinEx.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Finite_Set.thy
src/HOL/Groebner_Basis.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/Ln.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Library/Word.thy
src/HOL/Matrix/LP.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/MetisExamples/BigO.thy
src/HOL/OrderedGroup.thy
src/HOL/Presburger.thy
src/HOL/Real/Float.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Ring_and_Field.thy
src/HOL/SetInterval.thy
src/HOL/ZF/LProd.thy
src/HOL/ex/Adder.thy
src/HOL/ex/Lagrange.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Reflected_Presburger.thy
src/HOL/ex/ReflectionEx.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/Arith_Tools.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -614,7 +614,7 @@
     1.4  lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))"
     1.5  proof-
     1.6    assume H: "c < 0"
     1.7 -  have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_eq_simps)
     1.8 +  have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps)
     1.9    also have "\<dots> = (0 < x)" by simp
    1.10    finally show  "(c*x < 0) == (x > 0)" by simp
    1.11  qed
    1.12 @@ -622,7 +622,7 @@
    1.13  lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))"
    1.14  proof-
    1.15    assume H: "c > 0"
    1.16 -  hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_eq_simps)
    1.17 +  hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps)
    1.18    also have "\<dots> = (0 > x)" by simp
    1.19    finally show  "(c*x < 0) == (x < 0)" by simp
    1.20  qed
    1.21 @@ -631,7 +631,7 @@
    1.22  proof-
    1.23    assume H: "c < 0"
    1.24    have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
    1.25 -  also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_eq_simps)
    1.26 +  also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps)
    1.27    also have "\<dots> = ((- 1/c)*t < x)" by simp
    1.28    finally show  "(c*x + t < 0) == (x > (- 1/c)*t)" by simp
    1.29  qed
    1.30 @@ -640,7 +640,7 @@
    1.31  proof-
    1.32    assume H: "c > 0"
    1.33    have "c*x + t< 0 = (c*x < -t)"  by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
    1.34 -  also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_eq_simps)
    1.35 +  also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps)
    1.36    also have "\<dots> = ((- 1/c)*t > x)" by simp
    1.37    finally show  "(c*x + t < 0) == (x < (- 1/c)*t)" by simp
    1.38  qed
    1.39 @@ -651,7 +651,7 @@
    1.40  lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))"
    1.41  proof-
    1.42    assume H: "c < 0"
    1.43 -  have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_eq_simps)
    1.44 +  have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps)
    1.45    also have "\<dots> = (0 <= x)" by simp
    1.46    finally show  "(c*x <= 0) == (x >= 0)" by simp
    1.47  qed
    1.48 @@ -659,7 +659,7 @@
    1.49  lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))"
    1.50  proof-
    1.51    assume H: "c > 0"
    1.52 -  hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_eq_simps)
    1.53 +  hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps)
    1.54    also have "\<dots> = (0 >= x)" by simp
    1.55    finally show  "(c*x <= 0) == (x <= 0)" by simp
    1.56  qed
    1.57 @@ -668,7 +668,7 @@
    1.58  proof-
    1.59    assume H: "c < 0"
    1.60    have "c*x + t <= 0 = (c*x <= -t)"  by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
    1.61 -  also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_eq_simps)
    1.62 +  also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps)
    1.63    also have "\<dots> = ((- 1/c)*t <= x)" by simp
    1.64    finally show  "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp
    1.65  qed
    1.66 @@ -677,7 +677,7 @@
    1.67  proof-
    1.68    assume H: "c > 0"
    1.69    have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
    1.70 -  also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_eq_simps)
    1.71 +  also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps)
    1.72    also have "\<dots> = ((- 1/c)*t >= x)" by simp
    1.73    finally show  "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp
    1.74  qed
    1.75 @@ -690,7 +690,7 @@
    1.76  proof-
    1.77    assume H: "c \<noteq> 0"
    1.78    have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp)
    1.79 -  also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_eq_simps)
    1.80 +  also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_simps)
    1.81    finally show  "(c*x + t = 0) == (x = (- 1/c)*t)" by simp
    1.82  qed
    1.83  lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)"
     2.1 --- a/src/HOL/Complex/Complex.thy	Fri Jun 22 22:41:17 2007 +0200
     2.2 +++ b/src/HOL/Complex/Complex.thy	Sat Jun 23 19:33:22 2007 +0200
     2.3 @@ -153,7 +153,7 @@
     2.4  proof
     2.5    fix x y z :: complex
     2.6    show "(x * y) * z = x * (y * z)"
     2.7 -    by (simp add: expand_complex_eq ring_eq_simps)
     2.8 +    by (simp add: expand_complex_eq ring_simps)
     2.9    show "x * y = y * x"
    2.10      by (simp add: expand_complex_eq mult_commute add_commute)
    2.11    show "1 * x = x"
    2.12 @@ -161,7 +161,7 @@
    2.13    show "0 \<noteq> (1::complex)"
    2.14      by (simp add: expand_complex_eq)
    2.15    show "(x + y) * z = x * z + y * z"
    2.16 -    by (simp add: expand_complex_eq ring_eq_simps)
    2.17 +    by (simp add: expand_complex_eq ring_simps)
    2.18    show "x / y = x * inverse y"
    2.19      by (simp only: complex_divide_def)
    2.20    show "x \<noteq> 0 \<Longrightarrow> inverse x * x = 1"
    2.21 @@ -251,9 +251,9 @@
    2.22    show "scaleR 1 x = x"
    2.23      by (simp add: expand_complex_eq)
    2.24    show "scaleR a x * y = scaleR a (x * y)"
    2.25 -    by (simp add: expand_complex_eq ring_eq_simps)
    2.26 +    by (simp add: expand_complex_eq ring_simps)
    2.27    show "x * scaleR a y = scaleR a (x * y)"
    2.28 -    by (simp add: expand_complex_eq ring_eq_simps)
    2.29 +    by (simp add: expand_complex_eq ring_simps)
    2.30  qed
    2.31  
    2.32  
    2.33 @@ -319,7 +319,7 @@
    2.34         (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
    2.35    show "norm (x * y) = norm x * norm y"
    2.36      by (induct x, induct y)
    2.37 -       (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_eq_simps)
    2.38 +       (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
    2.39  qed
    2.40  
    2.41  lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
     3.1 --- a/src/HOL/Complex/ex/BinEx.thy	Fri Jun 22 22:41:17 2007 +0200
     3.2 +++ b/src/HOL/Complex/ex/BinEx.thy	Sat Jun 23 19:33:22 2007 +0200
     3.3 @@ -20,379 +20,377 @@
     3.4  subsubsection {*Addition *}
     3.5  
     3.6  lemma "(1359::real) + -2468 = -1109"
     3.7 -  by simp
     3.8 +by simp
     3.9  
    3.10  lemma "(93746::real) + -46375 = 47371"
    3.11 -  by simp
    3.12 +by simp
    3.13  
    3.14  
    3.15  subsubsection {*Negation *}
    3.16  
    3.17  lemma "- (65745::real) = -65745"
    3.18 -  by simp
    3.19 +by simp
    3.20  
    3.21  lemma "- (-54321::real) = 54321"
    3.22 -  by simp
    3.23 +by simp
    3.24  
    3.25  
    3.26  subsubsection {*Multiplication *}
    3.27  
    3.28  lemma "(-84::real) * 51 = -4284"
    3.29 -  by simp
    3.30 +by simp
    3.31  
    3.32  lemma "(255::real) * 255 = 65025"
    3.33 -  by simp
    3.34 +by simp
    3.35  
    3.36  lemma "(1359::real) * -2468 = -3354012"
    3.37 -  by simp
    3.38 +by simp
    3.39  
    3.40  
    3.41  subsubsection {*Inequalities *}
    3.42  
    3.43  lemma "(89::real) * 10 \<noteq> 889"
    3.44 -  by simp
    3.45 +by simp
    3.46  
    3.47  lemma "(13::real) < 18 - 4"
    3.48 -  by simp
    3.49 +by simp
    3.50  
    3.51  lemma "(-345::real) < -242 + -100"
    3.52 -  by simp
    3.53 +by simp
    3.54  
    3.55  lemma "(13557456::real) < 18678654"
    3.56 -  by simp
    3.57 +by simp
    3.58  
    3.59  lemma "(999999::real) \<le> (1000001 + 1) - 2"
    3.60 -  by simp
    3.61 +by simp
    3.62  
    3.63  lemma "(1234567::real) \<le> 1234567"
    3.64 -  by simp
    3.65 +by simp
    3.66  
    3.67  
    3.68  subsubsection {*Powers *}
    3.69  
    3.70  lemma "2 ^ 15 = (32768::real)"
    3.71 -  by simp
    3.72 +by simp
    3.73  
    3.74  lemma "-3 ^ 7 = (-2187::real)"
    3.75 -  by simp
    3.76 +by simp
    3.77  
    3.78  lemma "13 ^ 7 = (62748517::real)"
    3.79 -  by simp
    3.80 +by simp
    3.81  
    3.82  lemma "3 ^ 15 = (14348907::real)"
    3.83 -  by simp
    3.84 +by simp
    3.85  
    3.86  lemma "-5 ^ 11 = (-48828125::real)"
    3.87 -  by simp
    3.88 +by simp
    3.89  
    3.90  
    3.91  subsubsection {*Tests *}
    3.92  
    3.93  lemma "(x + y = x) = (y = (0::real))"
    3.94 -  by arith
    3.95 +by arith
    3.96  
    3.97  lemma "(x + y = y) = (x = (0::real))"
    3.98 -  by arith
    3.99 +by arith
   3.100  
   3.101  lemma "(x + y = (0::real)) = (x = -y)"
   3.102 -  by arith
   3.103 +by arith
   3.104  
   3.105  lemma "(x + y = (0::real)) = (y = -x)"
   3.106 -  by arith
   3.107 +by arith
   3.108  
   3.109  lemma "((x + y) < (x + z)) = (y < (z::real))"
   3.110 -  by arith
   3.111 +by arith
   3.112  
   3.113  lemma "((x + z) < (y + z)) = (x < (y::real))"
   3.114 -  by arith
   3.115 +by arith
   3.116  
   3.117  lemma "(\<not> x < y) = (y \<le> (x::real))"
   3.118 -  by arith
   3.119 +by arith
   3.120  
   3.121  lemma "\<not> (x < y \<and> y < (x::real))"
   3.122 -  by arith
   3.123 +by arith
   3.124  
   3.125  lemma "(x::real) < y ==> \<not> y < x"
   3.126 -  by arith
   3.127 +by arith
   3.128  
   3.129  lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
   3.130 -  by arith
   3.131 +by arith
   3.132  
   3.133  lemma "(\<not> x \<le> y) = (y < (x::real))"
   3.134 -  by arith
   3.135 +by arith
   3.136  
   3.137  lemma "x \<le> y \<or> y \<le> (x::real)"
   3.138 -  by arith
   3.139 +by arith
   3.140  
   3.141  lemma "x \<le> y \<or> y < (x::real)"
   3.142 -  by arith
   3.143 +by arith
   3.144  
   3.145  lemma "x < y \<or> y \<le> (x::real)"
   3.146 -  by arith
   3.147 +by arith
   3.148  
   3.149  lemma "x \<le> (x::real)"
   3.150 -  by arith
   3.151 +by arith
   3.152  
   3.153  lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
   3.154 -  by arith
   3.155 +by arith
   3.156  
   3.157  lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
   3.158 -  by arith
   3.159 +by arith
   3.160  
   3.161  lemma "\<not>(x < y \<and> y \<le> (x::real))"
   3.162 -  by arith
   3.163 +by arith
   3.164  
   3.165  lemma "\<not>(x \<le> y \<and> y < (x::real))"
   3.166 -  by arith
   3.167 +by arith
   3.168  
   3.169  lemma "(-x < (0::real)) = (0 < x)"
   3.170 -  by arith
   3.171 +by arith
   3.172  
   3.173  lemma "((0::real) < -x) = (x < 0)"
   3.174 -  by arith
   3.175 +by arith
   3.176  
   3.177  lemma "(-x \<le> (0::real)) = (0 \<le> x)"
   3.178 -  by arith
   3.179 +by arith
   3.180  
   3.181  lemma "((0::real) \<le> -x) = (x \<le> 0)"
   3.182 -  by arith
   3.183 +by arith
   3.184  
   3.185  lemma "(x::real) = y \<or> x < y \<or> y < x"
   3.186 -  by arith
   3.187 +by arith
   3.188  
   3.189  lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
   3.190 -  by arith
   3.191 +by arith
   3.192  
   3.193  lemma "(0::real) \<le> x \<or> 0 \<le> -x"
   3.194 -  by arith
   3.195 +by arith
   3.196  
   3.197  lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
   3.198 -  by arith
   3.199 +by arith
   3.200  
   3.201  lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
   3.202 -  by arith
   3.203 +by arith
   3.204  
   3.205  lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
   3.206 -  by arith
   3.207 +by arith
   3.208  
   3.209  lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
   3.210 -  by arith
   3.211 +by arith
   3.212  
   3.213  lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
   3.214 -  by arith
   3.215 +by arith
   3.216  
   3.217  lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
   3.218 -  by arith
   3.219 +by arith
   3.220  
   3.221  lemma "(-x < y) = (0 < x + (y::real))"
   3.222 -  by arith
   3.223 +by arith
   3.224  
   3.225  lemma "(x < -y) = (x + y < (0::real))"
   3.226 -  by arith
   3.227 +by arith
   3.228  
   3.229  lemma "(y < x + -z) = (y + z < (x::real))"
   3.230 -  by arith
   3.231 +by arith
   3.232  
   3.233  lemma "(x + -y < z) = (x < z + (y::real))"
   3.234 -  by arith
   3.235 +by arith
   3.236  
   3.237  lemma "x \<le> y ==> x < y + (1::real)"
   3.238 -  by arith
   3.239 +by arith
   3.240  
   3.241  lemma "(x - y) + y = (x::real)"
   3.242 -  by arith
   3.243 +by arith
   3.244  
   3.245  lemma "y + (x - y) = (x::real)"
   3.246 -  by arith
   3.247 +by arith
   3.248  
   3.249  lemma "x - x = (0::real)"
   3.250 -  by arith
   3.251 +by arith
   3.252  
   3.253  lemma "(x - y = 0) = (x = (y::real))"
   3.254 -  by arith
   3.255 +by arith
   3.256  
   3.257  lemma "((0::real) \<le> x + x) = (0 \<le> x)"
   3.258 -  by arith
   3.259 +by arith
   3.260  
   3.261  lemma "(-x \<le> x) = ((0::real) \<le> x)"
   3.262 -  by arith
   3.263 +by arith
   3.264  
   3.265  lemma "(x \<le> -x) = (x \<le> (0::real))"
   3.266 -  by arith
   3.267 +by arith
   3.268  
   3.269  lemma "(-x = (0::real)) = (x = 0)"
   3.270 -  by arith
   3.271 +by arith
   3.272  
   3.273  lemma "-(x - y) = y - (x::real)"
   3.274 -  by arith
   3.275 +by arith
   3.276  
   3.277  lemma "((0::real) < x - y) = (y < x)"
   3.278 -  by arith
   3.279 +by arith
   3.280  
   3.281  lemma "((0::real) \<le> x - y) = (y \<le> x)"
   3.282 -  by arith
   3.283 +by arith
   3.284  
   3.285  lemma "(x + y) - x = (y::real)"
   3.286 -  by arith
   3.287 +by arith
   3.288  
   3.289  lemma "(-x = y) = (x = (-y::real))"
   3.290 -  by arith
   3.291 +by arith
   3.292  
   3.293  lemma "x < (y::real) ==> \<not>(x = y)"
   3.294 -  by arith
   3.295 +by arith
   3.296  
   3.297  lemma "(x \<le> x + y) = ((0::real) \<le> y)"
   3.298 -  by arith
   3.299 +by arith
   3.300  
   3.301  lemma "(y \<le> x + y) = ((0::real) \<le> x)"
   3.302 -  by arith
   3.303 +by arith
   3.304  
   3.305  lemma "(x < x + y) = ((0::real) < y)"
   3.306 -  by arith
   3.307 +by arith
   3.308  
   3.309  lemma "(y < x + y) = ((0::real) < x)"
   3.310 -  by arith
   3.311 +by arith
   3.312  
   3.313  lemma "(x - y) - x = (-y::real)"
   3.314 -  by arith
   3.315 +by arith
   3.316  
   3.317  lemma "(x + y < z) = (x < z - (y::real))"
   3.318 -  by arith
   3.319 +by arith
   3.320  
   3.321  lemma "(x - y < z) = (x < z + (y::real))"
   3.322 -  by arith
   3.323 +by arith
   3.324  
   3.325  lemma "(x < y - z) = (x + z < (y::real))"
   3.326 -  by arith
   3.327 +by arith
   3.328  
   3.329  lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
   3.330 -  by arith
   3.331 +by arith
   3.332  
   3.333  lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
   3.334 -  by arith
   3.335 +by arith
   3.336  
   3.337  lemma "(-x < -y) = (y < (x::real))"
   3.338 -  by arith
   3.339 +by arith
   3.340  
   3.341  lemma "(-x \<le> -y) = (y \<le> (x::real))"
   3.342 -  by arith
   3.343 +by arith
   3.344  
   3.345  lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
   3.346 -  by arith
   3.347 +by arith
   3.348  
   3.349  lemma "(0::real) - x = -x"
   3.350 -  by arith
   3.351 +by arith
   3.352  
   3.353  lemma "x - (0::real) = x"
   3.354 -  by arith
   3.355 +by arith
   3.356  
   3.357  lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
   3.358 -  by arith
   3.359 +by arith
   3.360  
   3.361  lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
   3.362 -  by arith
   3.363 +by arith
   3.364  
   3.365  lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
   3.366 -  by arith
   3.367 +by arith
   3.368  
   3.369  lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
   3.370 -  by arith
   3.371 +by arith
   3.372  
   3.373  lemma "-x - y = -(x + (y::real))"
   3.374 -  by arith
   3.375 +by arith
   3.376  
   3.377  lemma "x - (-y) = x + (y::real)"
   3.378 -  by arith
   3.379 +by arith
   3.380  
   3.381  lemma "-x - -y = y - (x::real)"
   3.382 -  by arith
   3.383 +by arith
   3.384  
   3.385  lemma "(a - b) + (b - c) = a - (c::real)"
   3.386 -  by arith
   3.387 +by arith
   3.388  
   3.389  lemma "(x = y - z) = (x + z = (y::real))"
   3.390 -  by arith
   3.391 +by arith
   3.392  
   3.393  lemma "(x - y = z) = (x = z + (y::real))"
   3.394 -  by arith
   3.395 +by arith
   3.396  
   3.397  lemma "x - (x - y) = (y::real)"
   3.398 -  by arith
   3.399 +by arith
   3.400  
   3.401  lemma "x - (x + y) = -(y::real)"
   3.402 -  by arith
   3.403 +by arith
   3.404  
   3.405  lemma "x = y ==> x \<le> (y::real)"
   3.406 -  by arith
   3.407 +by arith
   3.408  
   3.409  lemma "(0::real) < x ==> \<not>(x = 0)"
   3.410 -  by arith
   3.411 +by arith
   3.412  
   3.413  lemma "(x + y) * (x - y) = (x * x) - (y * y)"
   3.414    oops
   3.415  
   3.416  lemma "(-x = -y) = (x = (y::real))"
   3.417 -  by arith
   3.418 +by arith
   3.419  
   3.420  lemma "(-x < -y) = (y < (x::real))"
   3.421 -  by arith
   3.422 +by arith
   3.423  
   3.424  lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
   3.425 -  by (tactic "fast_arith_tac 1")
   3.426 +by (tactic "fast_arith_tac 1")
   3.427  
   3.428  lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
   3.429 -  by (tactic "fast_arith_tac 1")
   3.430 +by (tactic "fast_arith_tac 1")
   3.431  
   3.432  lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
   3.433 -  by (tactic "fast_arith_tac 1")
   3.434 +by (tactic "fast_arith_tac 1")
   3.435  
   3.436  lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
   3.437 -  by (tactic "fast_arith_tac 1")
   3.438 +by (tactic "fast_arith_tac 1")
   3.439  
   3.440  lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
   3.441 -  by (tactic "fast_arith_tac 1")
   3.442 +by (tactic "fast_arith_tac 1")
   3.443  
   3.444  lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
   3.445 -  by arith
   3.446 +by arith
   3.447  
   3.448  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   3.449      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
   3.450 -  by (tactic "fast_arith_tac 1")
   3.451 +by (tactic "fast_arith_tac 1")
   3.452  
   3.453  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   3.454      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
   3.455 -  by (tactic "fast_arith_tac 1")
   3.456 +by (tactic "fast_arith_tac 1")
   3.457  
   3.458  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   3.459      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
   3.460 -  by (tactic "fast_arith_tac 1")
   3.461 +by (tactic "fast_arith_tac 1")
   3.462  
   3.463  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   3.464      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
   3.465 -  by (tactic "fast_arith_tac 1")
   3.466 +by (tactic "fast_arith_tac 1")
   3.467  
   3.468  
   3.469  subsection{*Complex Arithmetic*}
   3.470  
   3.471  lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
   3.472 -  by simp
   3.473 +by simp
   3.474  
   3.475  lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
   3.476 -  by simp
   3.477 +by simp
   3.478  
   3.479  text{*Multiplication requires distributive laws.  Perhaps versions instantiated
   3.480  to literal constants should be added to the simpset.*}
   3.481  
   3.482 -lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib
   3.483 -
   3.484  lemma "(1 + ii) * (1 - ii) = 2"
   3.485 -by (simp add: distrib)
   3.486 +by (simp add: ring_distribs)
   3.487  
   3.488  lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
   3.489 -by (simp add: distrib)
   3.490 +by (simp add: ring_distribs)
   3.491  
   3.492  lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
   3.493 -by (simp add: distrib)
   3.494 +by (simp add: ring_distribs)
   3.495  
   3.496  text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
   3.497  
     4.1 --- a/src/HOL/Complex/ex/MIR.thy	Fri Jun 22 22:41:17 2007 +0200
     4.2 +++ b/src/HOL/Complex/ex/MIR.thy	Sat Jun 23 19:33:22 2007 +0200
     4.3 @@ -714,11 +714,11 @@
     4.4  next
     4.5    case (2 n c t)  hence gd: "g dvd c" by simp
     4.6    from gp have gnz: "g \<noteq> 0" by simp
     4.7 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_eq_simps)
     4.8 +  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps)
     4.9  next
    4.10    case (3 c s t)  hence gd: "g dvd c" by simp
    4.11    from gp have gnz: "g \<noteq> 0" by simp
    4.12 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_eq_simps) 
    4.13 +  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps) 
    4.14  qed (auto simp add: numgcd_def gp)
    4.15  consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
    4.16  recdef ismaxcoeff "measure size"
    4.17 @@ -855,13 +855,13 @@
    4.18  
    4.19  lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
    4.20  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
    4.21 -apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
    4.22 -apply (case_tac "n1 = n2", simp_all add: ring_eq_simps)
    4.23 -apply (simp only: ring_eq_simps(1)[symmetric]) 
    4.24 -apply simp
    4.25 + apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
    4.26 +  apply (case_tac "n1 = n2", simp_all add: ring_simps)
    4.27 +  apply (simp only: left_distrib[symmetric])
    4.28 + apply simp
    4.29  apply (case_tac "lex_bnd t1 t2", simp_all)
    4.30 -apply (case_tac "c1+c2 = 0")
    4.31 -by (case_tac "t1 = t2", simp_all add: ring_eq_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
    4.32 + apply (case_tac "c1+c2 = 0")
    4.33 +  by (case_tac "t1 = t2", simp_all add: ring_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
    4.34  
    4.35  lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
    4.36  by (induct t s rule: numadd.induct, auto simp add: Let_def)
    4.37 @@ -874,7 +874,7 @@
    4.38    "nummul t = (\<lambda> i. Mul i t)"
    4.39  
    4.40  lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
    4.41 -by (induct t rule: nummul.induct, auto simp add: ring_eq_simps)
    4.42 +by (induct t rule: nummul.induct, auto simp add: ring_simps)
    4.43  
    4.44  lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
    4.45  by (induct t rule: nummul.induct, auto)
    4.46 @@ -934,7 +934,7 @@
    4.47    with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
    4.48    from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def)
    4.49    from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)
    4.50 -qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def ring_eq_simps)
    4.51 +qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def ring_simps)
    4.52  
    4.53  lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "
    4.54  by (induct t rule: split_int.induct, auto simp add: Let_def split_def)
    4.55 @@ -1771,7 +1771,7 @@
    4.56    have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
    4.57    show ?thesis using myless[rule_format, where b="real (floor b)"] 
    4.58      by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 
    4.59 -    (simp add: ring_eq_simps diff_def[symmetric],arith)
    4.60 +    (simp add: ring_simps diff_def[symmetric],arith)
    4.61  qed
    4.62  
    4.63  lemma split_int_le_real: 
    4.64 @@ -1798,7 +1798,7 @@
    4.65  proof- 
    4.66    have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith
    4.67    show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
    4.68 -    (simp add: ring_eq_simps diff_def[symmetric],arith)
    4.69 +    (simp add: ring_simps diff_def[symmetric],arith)
    4.70  qed
    4.71  
    4.72  lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")
    4.73 @@ -2276,9 +2276,9 @@
    4.74        (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")
    4.75        hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
    4.76        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 
    4.77 -	by (simp add: ring_eq_simps di_def)
    4.78 +	by (simp add: ring_simps di_def)
    4.79        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"
    4.80 -	by (simp add: ring_eq_simps)
    4.81 +	by (simp add: ring_simps)
    4.82        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast
    4.83        thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp
    4.84      next
    4.85 @@ -2287,7 +2287,7 @@
    4.86        hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
    4.87        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
    4.88        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)
    4.89 -      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_eq_simps)
    4.90 +      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
    4.91        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
    4.92  	by blast
    4.93        thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
    4.94 @@ -2303,9 +2303,9 @@
    4.95        (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")
    4.96        hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)
    4.97        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 
    4.98 -	by (simp add: ring_eq_simps di_def)
    4.99 +	by (simp add: ring_simps di_def)
   4.100        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"
   4.101 -	by (simp add: ring_eq_simps)
   4.102 +	by (simp add: ring_simps)
   4.103        hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast
   4.104        thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp
   4.105      next
   4.106 @@ -2314,7 +2314,7 @@
   4.107        hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)
   4.108        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp
   4.109        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)
   4.110 -      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_eq_simps)
   4.111 +      hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: ring_simps)
   4.112        hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"
   4.113  	by blast
   4.114        thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp
   4.115 @@ -2446,7 +2446,7 @@
   4.116         (real j rdvd - (real c * real x - Inum (real x # bs) e))"
   4.117      by (simp only: rdvd_minus[symmetric])
   4.118    from prems show  ?case
   4.119 -    by (simp add: ring_eq_simps th[simplified ring_eq_simps diff_def]
   4.120 +    by (simp add: ring_simps th[simplified ring_simps]
   4.121        numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
   4.122  next
   4.123      case (10 j c e)
   4.124 @@ -2454,7 +2454,7 @@
   4.125         (real j rdvd - (real c * real x - Inum (real x # bs) e))"
   4.126      by (simp only: rdvd_minus[symmetric])
   4.127    from prems show  ?case
   4.128 -    by (simp add: ring_eq_simps th[simplified ring_eq_simps diff_def]
   4.129 +    by (simp add: ring_simps th[simplified ring_simps]
   4.130        numbound0_I[where bs="bs" and b'="real x" and b="- real x"])
   4.131  qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2)
   4.132  
   4.133 @@ -2540,7 +2540,7 @@
   4.134      hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
   4.135            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)"
   4.136        by simp
   4.137 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.138 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: ring_simps)
   4.139      also have "\<dots> = (real c * real x + Inum (real x # bs) e < 0)"
   4.140      using mult_less_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.141    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be  isint_Mul[OF ei] by simp
   4.142 @@ -2558,7 +2558,7 @@
   4.143      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
   4.144            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<le> 0)"
   4.145        by simp
   4.146 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.147 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: ring_simps)
   4.148      also have "\<dots> = (real c * real x + Inum (real x # bs) e \<le> 0)"
   4.149      using mult_le_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.150    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
   4.151 @@ -2576,7 +2576,7 @@
   4.152      hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
   4.153            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)"
   4.154        by simp
   4.155 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.156 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: ring_simps)
   4.157      also have "\<dots> = (real c * real x + Inum (real x # bs) e > 0)"
   4.158      using zero_less_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.159    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
   4.160 @@ -2594,7 +2594,7 @@
   4.161      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
   4.162            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<ge> 0)"
   4.163        by simp
   4.164 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.165 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: ring_simps)
   4.166      also have "\<dots> = (real c * real x + Inum (real x # bs) e \<ge> 0)"
   4.167      using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.168    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
   4.169 @@ -2612,7 +2612,7 @@
   4.170      hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
   4.171            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)"
   4.172        by simp
   4.173 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.174 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: ring_simps)
   4.175      also have "\<dots> = (real c * real x + Inum (real x # bs) e = 0)"
   4.176      using mult_eq_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.177    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
   4.178 @@ -2630,7 +2630,7 @@
   4.179      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
   4.180            (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<noteq> 0)"
   4.181        by simp
   4.182 -    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: ring_eq_simps)
   4.183 +    also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: ring_simps)
   4.184      also have "\<dots> = (real c * real x + Inum (real x # bs) e \<noteq> 0)"
   4.185      using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp
   4.186    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp
   4.187 @@ -2646,7 +2646,7 @@
   4.188      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   4.189        by simp
   4.190      hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
   4.191 -    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_eq_simps)
   4.192 +    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
   4.193      also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
   4.194      using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
   4.195    also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
   4.196 @@ -2663,7 +2663,7 @@
   4.197      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   4.198        by simp
   4.199      hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
   4.200 -    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_eq_simps)
   4.201 +    also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: ring_simps)
   4.202      also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"
   4.203      using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp
   4.204    also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp
   4.205 @@ -2718,7 +2718,7 @@
   4.206        hence "x + floor ?e \<ge> 1 \<and> x + floor ?e \<le> d"  by simp
   4.207        hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e" by simp
   4.208        hence "\<exists> (j::int) \<in> {1 .. d}. real x = real (- floor ?e + j)" 
   4.209 -	by (simp only: real_of_int_inject) (simp add: ring_eq_simps)
   4.210 +	by (simp only: real_of_int_inject) (simp add: ring_simps)
   4.211        hence "\<exists> (j::int) \<in> {1 .. d}. real x = - ?e + real j" 
   4.212  	by (simp add: ie[simplified isint_iff])
   4.213        with nob have ?case by auto}
   4.214 @@ -2743,7 +2743,7 @@
   4.215  	using ie by simp
   4.216        hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
   4.217        hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
   4.218 -      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_eq_simps)
   4.219 +      hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: ring_simps)
   4.220        hence "\<exists> (j::int) \<in> {1 .. d}. real x= real (- floor ?e - 1 + j)" 
   4.221  	by (simp only: real_of_int_inject)
   4.222        hence "\<exists> (j::int) \<in> {1 .. d}. real x= - ?e - 1 + real j" 
   4.223 @@ -2758,7 +2758,7 @@
   4.224      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
   4.225      from p have "real x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
   4.226        by simp (erule ballE[where x="1"],
   4.227 -	simp_all add:ring_eq_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
   4.228 +	simp_all add:ring_simps numbound0_I[OF bn,where b="real x"and b'="a"and bs="bs"])
   4.229  next
   4.230    case (4 c e)hence p: "Ifm (real x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" 
   4.231      and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
   4.232 @@ -2982,7 +2982,7 @@
   4.233        from prems have "?I (real x) (?s (Eq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k = 0)"
   4.234  	using real_of_int_div[OF knz kdt]
   4.235  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.236 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.237 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.238        also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.239  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.240  	by (simp add: ti)
   4.241 @@ -3004,7 +3004,7 @@
   4.242        from prems have "?I (real x) (?s (NEq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<noteq> 0)"
   4.243  	using real_of_int_div[OF knz kdt]
   4.244  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.245 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.246 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.247        also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))" using nonzero_eq_divide_eq[OF knz', where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.248  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.249  	by (simp add: ti)
   4.250 @@ -3026,7 +3026,7 @@
   4.251        from prems have "?I (real x) (?s (Lt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k < 0)"
   4.252  	using real_of_int_div[OF knz kdt]
   4.253  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.254 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.255 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.256        also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))" using pos_less_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.257  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.258  	by (simp add: ti)
   4.259 @@ -3048,7 +3048,7 @@
   4.260        from prems have "?I (real x) (?s (Le (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<le> 0)"
   4.261  	using real_of_int_div[OF knz kdt]
   4.262  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.263 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.264 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.265        also have "\<dots> = (?I ?tk (Le (CN 0 c e)))" using pos_le_divide_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.266  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.267  	by (simp add: ti)
   4.268 @@ -3070,7 +3070,7 @@
   4.269        from prems have "?I (real x) (?s (Gt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k > 0)"
   4.270  	using real_of_int_div[OF knz kdt]
   4.271  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.272 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.273 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.274        also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))" using pos_divide_less_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.275  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.276  	by (simp add: ti)
   4.277 @@ -3092,7 +3092,7 @@
   4.278        from prems have "?I (real x) (?s (Ge (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<ge> 0)"
   4.279  	using real_of_int_div[OF knz kdt]
   4.280  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.281 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.282 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.283        also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))" using pos_divide_le_eq[OF kpos, where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.284  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.285  	by (simp add: ti)
   4.286 @@ -3113,7 +3113,7 @@
   4.287        from prems have "?I (real x) (?s (Dvd i (CN 0 c e))) = (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k)"
   4.288  	using real_of_int_div[OF knz kdt]
   4.289  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.290 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.291 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.292        also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.293  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.294  	by (simp add: ti)
   4.295 @@ -3134,7 +3134,7 @@
   4.296        from prems have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\<not> (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))"
   4.297  	using real_of_int_div[OF knz kdt]
   4.298  	  numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.299 -	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_eq_simps)
   4.300 +	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti ring_simps)
   4.301        also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))" using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   4.302  	  numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   4.303  	by (simp add: ti)
   4.304 @@ -3153,7 +3153,7 @@
   4.305    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.306      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.307      moreover 
   4.308 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.309 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.310      ultimately show ?case by blast 
   4.311  next
   4.312    case (4 c e)   
   4.313 @@ -3161,7 +3161,7 @@
   4.314    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.315      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.316      moreover 
   4.317 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.318 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] nonzero_eq_divide_eq[OF knz', where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.319      ultimately show ?case by blast 
   4.320  next
   4.321    case (5 c e)   
   4.322 @@ -3169,7 +3169,7 @@
   4.323    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.324      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.325      moreover 
   4.326 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.327 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_less_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.328      ultimately show ?case by blast 
   4.329  next
   4.330    case (6 c e)    
   4.331 @@ -3177,7 +3177,7 @@
   4.332    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.333      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.334      moreover 
   4.335 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.336 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_le_divide_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.337      ultimately show ?case by blast 
   4.338  next
   4.339    case (7 c e)    
   4.340 @@ -3185,7 +3185,7 @@
   4.341    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.342      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.343      moreover 
   4.344 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.345 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_less_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.346      ultimately show ?case by blast 
   4.347  next
   4.348    case (8 c e)    
   4.349 @@ -3193,7 +3193,7 @@
   4.350    from kp have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   4.351      {assume kdc: "k dvd c" from prems have  ?case using real_of_int_div[OF knz kdc] by simp } 
   4.352      moreover 
   4.353 -    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_eq_simps)}
   4.354 +    {assume nkdc: "\<not> k dvd c" hence ?case using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] pos_divide_le_eq[OF kp, where b="0" and a="real c * real x + Inum (real x # bs) e", symmetric] by (simp add: ring_simps)}
   4.355      ultimately show ?case by blast 
   4.356  next
   4.357    case (9 i c e)
   4.358 @@ -3205,7 +3205,7 @@
   4.359      hence "Ifm (real (x*k)#bs) (a\<rho> (Dvd i (CN 0 c e)) k) = 
   4.360        (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k)" 
   4.361        using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
   4.362 -      by (simp add: ring_eq_simps)
   4.363 +      by (simp add: ring_simps)
   4.364      also have "\<dots> = (Ifm (real x#bs) (Dvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
   4.365      finally have ?case . }
   4.366    ultimately show ?case by blast 
   4.367 @@ -3219,7 +3219,7 @@
   4.368      hence "Ifm (real (x*k)#bs) (a\<rho> (NDvd i (CN 0 c e)) k) = 
   4.369        (\<not> (real i * real k rdvd (real c * real x + Inum (real x#bs) e) * real k))" 
   4.370        using numbound0_I[OF nb, where bs="bs" and b="real (x*k)" and b'="real x"] 
   4.371 -      by (simp add: ring_eq_simps)
   4.372 +      by (simp add: ring_simps)
   4.373      also have "\<dots> = (Ifm (real x#bs) (NDvd i (CN 0 c e)))" by (simp add: rdvd_mult[OF knz, where n="i"])
   4.374      finally have ?case . }
   4.375    ultimately show ?case by blast 
   4.376 @@ -3232,7 +3232,7 @@
   4.377  proof-
   4.378    have "(\<exists> x. ?D x \<and> ?P' x) = (\<exists> x. k dvd x \<and> ?P' x)" using int_rdvd_iff by simp
   4.379    also have "\<dots> = (\<exists>x. ?P' (x*k))" using unity_coeff_ex[where P="?P'" and l="k", simplified]
   4.380 -    by (simp add: ring_eq_simps)
   4.381 +    by (simp add: ring_simps)
   4.382    also have "\<dots> = (\<exists> x. ?P x)" using a\<rho> iszlfm_gen[OF lp] kp by auto
   4.383    finally show ?thesis .
   4.384  qed
   4.385 @@ -3296,7 +3296,7 @@
   4.386      by simp+
   4.387    {assume "real (c*i) \<noteq> - ?N i e + real (c*d)"
   4.388      with numbound0_I[OF nb, where bs="bs" and b="real i - real d" and b'="real i"]
   4.389 -    have ?case by (simp add: ring_eq_simps)}
   4.390 +    have ?case by (simp add: ring_simps)}
   4.391    moreover
   4.392    {assume pi: "real (c*i) = - ?N i e + real (c*d)"
   4.393      from mult_strict_left_mono[OF dp cp] have d: "(c*d) \<in> {1 .. c*d}" by simp
   4.394 @@ -3308,27 +3308,27 @@
   4.395      real_of_int_mult]
   4.396    show ?case using prems dp 
   4.397      by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
   4.398 -      ring_eq_simps)
   4.399 +      ring_simps)
   4.400  next
   4.401    case (6 c e)  hence cp: "c > 0" by simp
   4.402    from prems mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
   4.403      real_of_int_mult]
   4.404    show ?case using prems dp 
   4.405      by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
   4.406 -      ring_eq_simps)
   4.407 +      ring_simps)
   4.408  next
   4.409    case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
   4.410      and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
   4.411      and pi: "real (c*i) + ?N i e > 0" and cp': "real c >0"
   4.412      by simp+
   4.413    let ?fe = "floor (?N i e)"
   4.414 -  from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: ring_eq_simps)
   4.415 +  from pi cp have th:"(real i +?N i e / real c)*real c > 0" by (simp add: ring_simps)
   4.416    from pi ei[simplified isint_iff] have "real (c*i + ?fe) > real (0::int)" by simp
   4.417    hence pi': "c*i + ?fe > 0" by (simp only: real_of_int_less_iff[symmetric])
   4.418    have "real (c*i) + ?N i e > real (c*d) \<or> real (c*i) + ?N i e \<le> real (c*d)" by auto
   4.419    moreover
   4.420    {assume "real (c*i) + ?N i e > real (c*d)" hence ?case
   4.421 -      by (simp add: ring_eq_simps 
   4.422 +      by (simp add: ring_simps 
   4.423  	numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} 
   4.424    moreover 
   4.425    {assume H:"real (c*i) + ?N i e \<le> real (c*d)"
   4.426 @@ -3336,7 +3336,7 @@
   4.427      hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
   4.428      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
   4.429      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1" 
   4.430 -      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_eq_simps)
   4.431 +      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps)
   4.432      with nob  have ?case by blast }
   4.433    ultimately show ?case by blast
   4.434  next
   4.435 @@ -3345,13 +3345,13 @@
   4.436      and pi: "real (c*i) + ?N i e \<ge> 0" and cp': "real c >0"
   4.437      by simp+
   4.438    let ?fe = "floor (?N i e)"
   4.439 -  from pi cp have th:"(real i +?N i e / real c)*real c \<ge> 0" by (simp add: ring_eq_simps)
   4.440 +  from pi cp have th:"(real i +?N i e / real c)*real c \<ge> 0" by (simp add: ring_simps)
   4.441    from pi ei[simplified isint_iff] have "real (c*i + ?fe) \<ge> real (0::int)" by simp
   4.442    hence pi': "c*i + 1 + ?fe \<ge> 1" by (simp only: real_of_int_le_iff[symmetric])
   4.443    have "real (c*i) + ?N i e \<ge> real (c*d) \<or> real (c*i) + ?N i e < real (c*d)" by auto
   4.444    moreover
   4.445    {assume "real (c*i) + ?N i e \<ge> real (c*d)" hence ?case
   4.446 -      by (simp add: ring_eq_simps 
   4.447 +      by (simp add: ring_simps 
   4.448  	numbound0_I[OF nb,where bs="bs" and b="real i - real d" and b'="real i"])} 
   4.449    moreover 
   4.450    {assume H:"real (c*i) + ?N i e < real (c*d)"
   4.451 @@ -3359,9 +3359,9 @@
   4.452      hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
   4.453      with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
   4.454      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
   4.455 -      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_eq_simps real_of_one) 
   4.456 +      by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] ring_simps real_of_one) 
   4.457      hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
   4.458 -      by (simp only: ring_eq_simps diff_def[symmetric])
   4.459 +      by (simp only: ring_simps diff_def[symmetric])
   4.460          hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
   4.461  	  by (simp only: add_ac diff_def)
   4.462      with nob  have ?case by blast }
   4.463 @@ -3382,10 +3382,10 @@
   4.464        using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
   4.465        ie by simp
   4.466      also have "\<dots> = (real j rdvd real (c*(i - d)) + ?e)" 
   4.467 -      using ie by (simp add:ring_eq_simps)
   4.468 +      using ie by (simp add:ring_simps)
   4.469      finally show ?case 
   4.470        using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 
   4.471 -      by (simp add: ring_eq_simps)
   4.472 +      by (simp add: ring_simps)
   4.473  next
   4.474    case (10 j c e)   hence p: "\<not> (real j rdvd real (c*i) + ?N i e)" (is "?p x") and cp: "c > 0" and bn:"numbound0 e"  by simp+
   4.475      let ?e = "Inum (real i # bs) e"
   4.476 @@ -3402,10 +3402,10 @@
   4.477        using int_rdvd_iff[where i="j" and t="(c*i - c*d + floor ?e)",symmetric, simplified]
   4.478        ie by simp
   4.479      also have "\<dots> = Not (real j rdvd real (c*(i - d)) + ?e)" 
   4.480 -      using ie by (simp add:ring_eq_simps)
   4.481 +      using ie by (simp add:ring_simps)
   4.482      finally show ?case 
   4.483        using numbound0_I[OF bn,where b="real i - real d" and b'="real i" and bs="bs"] p 
   4.484 -      by (simp add: ring_eq_simps)
   4.485 +      by (simp add: ring_simps)
   4.486  qed(auto simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] nth_pos2)
   4.487  
   4.488  lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
   4.489 @@ -3648,7 +3648,7 @@
   4.490  	from H 
   4.491  	have "?I (?p (p',n',s') j) \<longrightarrow> 
   4.492  	  (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
   4.493 -	  by (simp add: fp_def np ring_eq_simps numsub numadd numfloor)
   4.494 +	  by (simp add: fp_def np ring_simps numsub numadd numfloor)
   4.495  	also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
   4.496  	  using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp
   4.497  	moreover
   4.498 @@ -3674,7 +3674,7 @@
   4.499  	from H 
   4.500  	have "?I (?p (p',n',s') j) \<longrightarrow> 
   4.501  	  (((?N ?nxs \<ge> real ?l) \<and> (?N ?nxs < real (?l + 1))) \<and> (?N a = ?N ?nxs ))" 
   4.502 -	  by (simp add: np fp_def ring_eq_simps numneg numfloor numadd numsub)
   4.503 +	  by (simp add: np fp_def ring_simps numneg numfloor numadd numsub)
   4.504  	also have "\<dots> \<longrightarrow> ((floor (?N ?nxs) = ?l) \<and> (?N a = ?N ?nxs ))"
   4.505  	  using floor_int_eq[where x="?N ?nxs" and n="?l"] by simp
   4.506  	moreover
   4.507 @@ -3686,7 +3686,7 @@
   4.508      qed
   4.509  next
   4.510    case (3 a b) thus ?case by auto 
   4.511 -qed (auto simp add: Let_def allpairs_set split_def ring_eq_simps conj_rl)
   4.512 +qed (auto simp add: Let_def allpairs_set split_def ring_simps conj_rl)
   4.513  
   4.514  lemma real_in_int_intervals: 
   4.515    assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
   4.516 @@ -3790,7 +3790,7 @@
   4.517      hence "\<exists> j\<in> {0 .. n}. 0 \<le> real n *x + ?N s - ?N (Floor s) - real j \<and> real n *x + ?N s - ?N (Floor s) - real (j+1) < 0"
   4.518        by(simp only: myl[rule_format, where b="real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"]) 
   4.519      hence "\<exists> j\<in> {0.. n}. ?I (?p (p,n,s) j)"
   4.520 -      using pns by (simp add: fp_def np ring_eq_simps numsub numadd)
   4.521 +      using pns by (simp add: fp_def np ring_simps numsub numadd)
   4.522      then obtain "j" where j_def: "j\<in> {0 .. n} \<and> ?I (?p (p,n,s) j)" by blast
   4.523      hence "\<exists>x \<in> {?p (p,n,s) j |j. 0\<le> j \<and> j \<le> n }. ?I x" by auto
   4.524      hence ?case using pns 
   4.525 @@ -3808,7 +3808,7 @@
   4.526        have "real n *x + ?N s \<ge> real n + ?N s" by simp 
   4.527        moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
   4.528        ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
   4.529 -	by (simp only: ring_eq_simps)}
   4.530 +	by (simp only: ring_simps)}
   4.531      ultimately have "?N (Floor s) + real n \<le> real n *x + ?N s\<and> real n *x + ?N s < ?N (Floor s) + real (1::int)" by simp
   4.532      hence th: "real n \<le> real n *x + ?N s - ?N (Floor s) \<and> real n *x + ?N s - ?N (Floor s) < real (1::int)" by simp
   4.533      have th1: "\<forall> (a::real). (- a > 0) = (a < 0)" by auto
   4.534 @@ -3911,7 +3911,7 @@
   4.535    fix a n s
   4.536    assume H: "?N a = ?N (CN 0 n s)"
   4.537    show "?I (lt n s) = ?I (Lt a)" using H by (cases "n=0", (simp add: lt_def))
   4.538 -  (cases "n > 0", simp_all add: lt_def ring_eq_simps myless[rule_format, where b="0"])
   4.539 +  (cases "n > 0", simp_all add: lt_def ring_simps myless[rule_format, where b="0"])
   4.540  qed
   4.541  
   4.542  lemma lt_l: "isrlfm (rsplit lt a)"
   4.543 @@ -3923,7 +3923,7 @@
   4.544    fix a n s
   4.545    assume H: "?N a = ?N (CN 0 n s)"
   4.546    show "?I (le n s) = ?I (Le a)" using H by (cases "n=0", (simp add: le_def))
   4.547 -  (cases "n > 0", simp_all add: le_def ring_eq_simps myl[rule_format, where b="0"])
   4.548 +  (cases "n > 0", simp_all add: le_def ring_simps myl[rule_format, where b="0"])
   4.549  qed
   4.550  
   4.551  lemma le_l: "isrlfm (rsplit le a)"
   4.552 @@ -3935,7 +3935,7 @@
   4.553    fix a n s
   4.554    assume H: "?N a = ?N (CN 0 n s)"
   4.555    show "?I (gt n s) = ?I (Gt a)" using H by (cases "n=0", (simp add: gt_def))
   4.556 -  (cases "n > 0", simp_all add: gt_def ring_eq_simps myless[rule_format, where b="0"])
   4.557 +  (cases "n > 0", simp_all add: gt_def ring_simps myless[rule_format, where b="0"])
   4.558  qed
   4.559  lemma gt_l: "isrlfm (rsplit gt a)"
   4.560    by (rule rsplit_l[where f="gt" and a="a"], auto simp add: gt_def) 
   4.561 @@ -3946,7 +3946,7 @@
   4.562    fix a n s 
   4.563    assume H: "?N a = ?N (CN 0 n s)"
   4.564    show "?I (ge n s) = ?I (Ge a)" using H by (cases "n=0", (simp add: ge_def))
   4.565 -  (cases "n > 0", simp_all add: ge_def ring_eq_simps myl[rule_format, where b="0"])
   4.566 +  (cases "n > 0", simp_all add: ge_def ring_simps myl[rule_format, where b="0"])
   4.567  qed
   4.568  lemma ge_l: "isrlfm (rsplit ge a)"
   4.569    by (rule rsplit_l[where f="ge" and a="a"], auto simp add: ge_def) 
   4.570 @@ -3956,7 +3956,7 @@
   4.571  proof(clarify)
   4.572    fix a n s 
   4.573    assume H: "?N a = ?N (CN 0 n s)"
   4.574 -  show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def ring_eq_simps)
   4.575 +  show "?I (eq n s) = ?I (Eq a)" using H by (auto simp add: eq_def ring_simps)
   4.576  qed
   4.577  lemma eq_l: "isrlfm (rsplit eq a)"
   4.578    by (rule rsplit_l[where f="eq" and a="a"], auto simp add: eq_def) 
   4.579 @@ -3966,7 +3966,7 @@
   4.580  proof(clarify)
   4.581    fix a n s bs
   4.582    assume H: "?N a = ?N (CN 0 n s)"
   4.583 -  show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def ring_eq_simps)
   4.584 +  show "?I (neq n s) = ?I (NEq a)" using H by (auto simp add: neq_def ring_simps)
   4.585  qed
   4.586  
   4.587  lemma neq_l: "isrlfm (rsplit neq a)"
   4.588 @@ -4010,10 +4010,10 @@
   4.589    also have "\<dots> = (?DE \<and> ?a \<ge> 0 \<and> ?a < n)" by(simp only: small_le[OF ss0 ss1] small_lt[OF ss0 ss1])
   4.590    also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. ?a = j))" by simp
   4.591    also have "\<dots> = (?DE \<and> (\<exists> j\<in> {0 .. (n - 1)}. real (\<lfloor>real n * u - s\<rfloor>) = real j - real \<lfloor>s\<rfloor> ))"
   4.592 -    by (simp only: ring_eq_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
   4.593 +    by (simp only: ring_simps real_of_int_diff[symmetric] real_of_int_inject del: real_of_int_diff)
   4.594    also have "\<dots> = ((\<exists> j\<in> {0 .. (n - 1)}. real n * u - s = real j - real \<lfloor>s\<rfloor> \<and> real i rdvd real n * u - s))" using int_rdvd_iff[where i="i" and t="\<lfloor>real n * u - s\<rfloor>"]
   4.595      by (auto cong: conj_cong)
   4.596 -  also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: ring_eq_simps )
   4.597 +  also have "\<dots> = ?rhs" by(simp cong: conj_cong) (simp add: ring_simps )
   4.598    finally show ?thesis .
   4.599  qed
   4.600  
   4.601 @@ -4029,7 +4029,7 @@
   4.602    from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   4.603    have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   4.604      by (simp add: iupt_set np DVDJ_def del: iupt.simps)
   4.605 -  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: ring_eq_simps diff_def[symmetric])
   4.606 +  also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: ring_simps diff_def[symmetric])
   4.607    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   4.608    have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
   4.609    finally show ?thesis by simp
   4.610 @@ -4044,7 +4044,7 @@
   4.611    from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   4.612    have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   4.613      by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
   4.614 -  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: ring_eq_simps diff_def[symmetric])
   4.615 +  also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: ring_simps diff_def[symmetric])
   4.616    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   4.617    have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
   4.618    finally show ?thesis by simp
   4.619 @@ -4630,40 +4630,40 @@
   4.620      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.621    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"
   4.622      by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.623 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.624 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.625    also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"
   4.626      using np by simp 
   4.627 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.628 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.629  next
   4.630    case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.631    have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"
   4.632      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.633    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
   4.634      by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.635 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.636 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.637    also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"
   4.638      using np by simp 
   4.639 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.640 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.641  next
   4.642    case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.643    have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"
   4.644      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.645    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"
   4.646      by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.647 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.648 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.649    also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"
   4.650      using np by simp 
   4.651 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.652 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.653  next
   4.654    case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.655    have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"
   4.656      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.657    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
   4.658      by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.659 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.660 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.661    also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"
   4.662      using np by simp 
   4.663 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.664 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.665  next
   4.666    case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.667    from np have np: "real n \<noteq> 0" by simp
   4.668 @@ -4671,10 +4671,10 @@
   4.669      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.670    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)"
   4.671      by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.672 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.673 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.674    also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"
   4.675      using np by simp 
   4.676 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.677 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.678  next
   4.679    case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   4.680    from np have np: "real n \<noteq> 0" by simp
   4.681 @@ -4682,10 +4682,10 @@
   4.682      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   4.683    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
   4.684      by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   4.685 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   4.686 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   4.687    also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
   4.688      using np by simp 
   4.689 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   4.690 +  finally show ?case using nbt nb by (simp add: ring_simps)
   4.691  qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
   4.692  
   4.693  lemma \<Upsilon>_l:
   4.694 @@ -4736,7 +4736,7 @@
   4.695  using lp px noS
   4.696  proof (induct p rule: isrlfm.induct)
   4.697    case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.698 -    from prems have "x * real c + ?N x e < 0" by (simp add: ring_eq_simps)
   4.699 +    from prems have "x * real c + ?N x e < 0" by (simp add: ring_simps)
   4.700      hence pxc: "x < (- ?N x e) / real c" 
   4.701        by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.702      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.703 @@ -4745,7 +4745,7 @@
   4.704      moreover {assume y: "y < (-?N x e)/ real c"
   4.705        hence "y * real c < - ?N x e"
   4.706  	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.707 -      hence "real c * y + ?N x e < 0" by (simp add: ring_eq_simps)
   4.708 +      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
   4.709        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.710      moreover {assume y: "y > (- ?N x e) / real c" 
   4.711        with yu have eu: "u > (- ?N x e) / real c" by auto
   4.712 @@ -4755,7 +4755,7 @@
   4.713      ultimately show ?case by blast
   4.714  next
   4.715    case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp +
   4.716 -    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_eq_simps)
   4.717 +    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_simps)
   4.718      hence pxc: "x \<le> (- ?N x e) / real c" 
   4.719        by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
   4.720      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.721 @@ -4764,7 +4764,7 @@
   4.722      moreover {assume y: "y < (-?N x e)/ real c"
   4.723        hence "y * real c < - ?N x e"
   4.724  	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.725 -      hence "real c * y + ?N x e < 0" by (simp add: ring_eq_simps)
   4.726 +      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
   4.727        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.728      moreover {assume y: "y > (- ?N x e) / real c" 
   4.729        with yu have eu: "u > (- ?N x e) / real c" by auto
   4.730 @@ -4774,7 +4774,7 @@
   4.731      ultimately show ?case by blast
   4.732  next
   4.733    case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.734 -    from prems have "x * real c + ?N x e > 0" by (simp add: ring_eq_simps)
   4.735 +    from prems have "x * real c + ?N x e > 0" by (simp add: ring_simps)
   4.736      hence pxc: "x > (- ?N x e) / real c" 
   4.737        by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
   4.738      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.739 @@ -4783,7 +4783,7 @@
   4.740      moreover {assume y: "y > (-?N x e)/ real c"
   4.741        hence "y * real c > - ?N x e"
   4.742  	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.743 -      hence "real c * y + ?N x e > 0" by (simp add: ring_eq_simps)
   4.744 +      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
   4.745        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.746      moreover {assume y: "y < (- ?N x e) / real c" 
   4.747        with ly have eu: "l < (- ?N x e) / real c" by auto
   4.748 @@ -4793,7 +4793,7 @@
   4.749      ultimately show ?case by blast
   4.750  next
   4.751    case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.752 -    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_eq_simps)
   4.753 +    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_simps)
   4.754      hence pxc: "x \<ge> (- ?N x e) / real c" 
   4.755        by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
   4.756      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.757 @@ -4802,7 +4802,7 @@
   4.758      moreover {assume y: "y > (-?N x e)/ real c"
   4.759        hence "y * real c > - ?N x e"
   4.760  	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   4.761 -      hence "real c * y + ?N x e > 0" by (simp add: ring_eq_simps)
   4.762 +      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
   4.763        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   4.764      moreover {assume y: "y < (- ?N x e) / real c" 
   4.765        with ly have eu: "l < (- ?N x e) / real c" by auto
   4.766 @@ -4813,7 +4813,7 @@
   4.767  next
   4.768    case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   4.769      from cp have cnz: "real c \<noteq> 0" by simp
   4.770 -    from prems have "x * real c + ?N x e = 0" by (simp add: ring_eq_simps)
   4.771 +    from prems have "x * real c + ?N x e = 0" by (simp add: ring_simps)
   4.772      hence pxc: "x = (- ?N x e) / real c" 
   4.773        by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
   4.774      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   4.775 @@ -4826,9 +4826,9 @@
   4.776      with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   4.777      hence "y* real c \<noteq> -?N x e"      
   4.778        by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
   4.779 -    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_eq_simps)
   4.780 +    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
   4.781      thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
   4.782 -      by (simp add: ring_eq_simps)
   4.783 +      by (simp add: ring_simps)
   4.784  qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
   4.785  
   4.786  lemma finite_set_intervals:
   4.787 @@ -4991,7 +4991,7 @@
   4.788  	by (simp add: mult_commute)
   4.789        from tnb snb have st_nb: "numbound0 ?st" by simp
   4.790        have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   4.791 -	using mnp mp np by (simp add: ring_eq_simps add_divide_distrib)
   4.792 +	using mnp mp np by (simp add: ring_simps add_divide_distrib)
   4.793        from \<upsilon>_I[OF lp mnp st_nb, where x="x" and bs="bs"] 
   4.794        have "?I x (\<upsilon> p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])}
   4.795      with rinf_\<Upsilon>[OF lp nmi npi px] have "?F" by blast hence "?D" by blast}
   4.796 @@ -5060,7 +5060,7 @@
   4.797  
   4.798  lemma exsplitnum: 
   4.799    "Inum (x#y#bs) (exsplitnum t) = Inum ((x+y) #bs) t"
   4.800 -  by(induct t rule: exsplitnum.induct) (simp_all add: ring_eq_simps)
   4.801 +  by(induct t rule: exsplitnum.induct) (simp_all add: ring_simps)
   4.802  
   4.803  lemma exsplit: 
   4.804    assumes qfp: "qfree p"
   4.805 @@ -5151,14 +5151,14 @@
   4.806    from Ul th have mnz: "m \<noteq> 0" by auto
   4.807    from Ul th have  nnz: "n \<noteq> 0" by auto  
   4.808    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   4.809 -   using mnz nnz by (simp add: ring_eq_simps add_divide_distrib)
   4.810 +   using mnz nnz by (simp add: ring_simps add_divide_distrib)
   4.811   
   4.812    thus "(real m *  Inum (x # bs) t + real n * Inum (x # bs) s) /
   4.813         (2 * real n * real m)
   4.814         \<in> (\<lambda>((t, n), s, m).
   4.815               (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) `
   4.816           (set U \<times> set U)"using mnz nnz th  
   4.817 -    apply (auto simp add: th add_divide_distrib ring_eq_simps split_def image_def)
   4.818 +    apply (auto simp add: th add_divide_distrib ring_simps split_def image_def)
   4.819      by (rule_tac x="(s,m)" in bexI,simp_all) 
   4.820    (rule_tac x="(t,n)" in bexI,simp_all)
   4.821  next
   4.822 @@ -5169,7 +5169,7 @@
   4.823    from Ul smU have mnz: "m \<noteq> 0" by auto
   4.824    from Ul tnU have  nnz: "n \<noteq> 0" by auto  
   4.825    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   4.826 -   using mnz nnz by (simp add: ring_eq_simps add_divide_distrib)
   4.827 +   using mnz nnz by (simp add: ring_simps add_divide_distrib)
   4.828   let ?P = "\<lambda> (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2"
   4.829   have Pc:"\<forall> a b. ?P a b = ?P b a"
   4.830     by auto
   4.831 @@ -5182,7 +5182,7 @@
   4.832   from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" by auto
   4.833   let ?st' = "Add (Mul m' t') (Mul n' s')"
   4.834     have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')"
   4.835 -   using mnz' nnz' by (simp add: ring_eq_simps add_divide_distrib)
   4.836 +   using mnz' nnz' by (simp add: ring_simps add_divide_distrib)
   4.837   from Pts' have 
   4.838     "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp
   4.839   also have "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st')
   4.840 @@ -5212,7 +5212,7 @@
   4.841        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
   4.842      from tnb snb have stnb: "numbound0 ?st" by simp
   4.843    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   4.844 -   using mp np by (simp add: ring_eq_simps add_divide_distrib)
   4.845 +   using mp np by (simp add: ring_simps add_divide_distrib)
   4.846    from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast
   4.847    hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')"
   4.848      by auto (rule_tac x="(a,b)" in bexI, auto)
   4.849 @@ -5240,7 +5240,7 @@
   4.850        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
   4.851      from tnb snb have stnb: "numbound0 ?st" by simp
   4.852    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   4.853 -   using mp np by (simp add: ring_eq_simps add_divide_distrib)
   4.854 +   using mp np by (simp add: ring_simps add_divide_distrib)
   4.855    from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto
   4.856    from \<upsilon>_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt'
   4.857    have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp
     5.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Jun 22 22:41:17 2007 +0200
     5.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sat Jun 23 19:33:22 2007 +0200
     5.3 @@ -533,7 +533,7 @@
     5.4  next
     5.5    case (2 n c t)  hence gd: "g dvd c" by simp
     5.6    from gp have gnz: "g \<noteq> 0" by simp
     5.7 -  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_eq_simps)
     5.8 +  from prems show ?case by (simp add: real_of_int_div[OF gnz gd] ring_simps)
     5.9  qed (auto simp add: numgcd_def gp)
    5.10  consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
    5.11  recdef ismaxcoeff "measure size"
    5.12 @@ -637,8 +637,8 @@
    5.13  lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
    5.14  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
    5.15  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
    5.16 -apply (case_tac "n1 = n2", simp_all add: ring_eq_simps)
    5.17 -by (simp only: ring_eq_simps(1)[symmetric],simp)
    5.18 +apply (case_tac "n1 = n2", simp_all add: ring_simps)
    5.19 +by (simp only: left_distrib[symmetric],simp)
    5.20  
    5.21  lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
    5.22  by (induct t s rule: numadd.induct, auto simp add: Let_def)
    5.23 @@ -649,7 +649,7 @@
    5.24    "nummul t = (\<lambda> i. Mul i t)"
    5.25  
    5.26  lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
    5.27 -by (induct t rule: nummul.induct, auto simp add: ring_eq_simps)
    5.28 +by (induct t rule: nummul.induct, auto simp add: ring_simps)
    5.29  
    5.30  lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
    5.31  by (induct t rule: nummul.induct, auto )
    5.32 @@ -1002,10 +1002,10 @@
    5.33      by(cases "rsplit0 a",auto simp add: Let_def split_def)
    5.34    have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = 
    5.35      Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)"
    5.36 -    by (simp add: Let_def split_def ring_eq_simps)
    5.37 +    by (simp add: Let_def split_def ring_simps)
    5.38    also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a", simp_all)
    5.39    finally show ?case using nb by simp 
    5.40 -qed(auto simp add: Let_def split_def ring_eq_simps , simp add: ring_eq_simps(2)[symmetric])
    5.41 +qed(auto simp add: Let_def split_def ring_simps , simp add: right_distrib[symmetric])
    5.42  
    5.43      (* Linearize a formula*)
    5.44  consts 
    5.45 @@ -1370,40 +1370,40 @@
    5.46      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    5.47    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)"
    5.48      by (simp only: pos_less_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
    5.49 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
    5.50 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
    5.51    also have "\<dots> = (real c *?t + ?n* (?N x e) < 0)"
    5.52      using np by simp 
    5.53 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
    5.54 +  finally show ?case using nbt nb by (simp add: ring_simps)
    5.55  next
    5.56    case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
    5.57    have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)"
    5.58      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    5.59    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
    5.60      by (simp only: pos_le_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
    5.61 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
    5.62 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
    5.63    also have "\<dots> = (real c *?t + ?n* (?N x e) \<le> 0)"
    5.64      using np by simp 
    5.65 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
    5.66 +  finally show ?case using nbt nb by (simp add: ring_simps)
    5.67  next
    5.68    case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
    5.69    have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)"
    5.70      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    5.71    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)"
    5.72      by (simp only: pos_divide_less_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
    5.73 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
    5.74 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
    5.75    also have "\<dots> = (real c *?t + ?n* (?N x e) > 0)"
    5.76      using np by simp 
    5.77 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
    5.78 +  finally show ?case using nbt nb by (simp add: ring_simps)
    5.79  next
    5.80    case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
    5.81    have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)"
    5.82      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    5.83    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
    5.84      by (simp only: pos_divide_le_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
    5.85 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
    5.86 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
    5.87    also have "\<dots> = (real c *?t + ?n* (?N x e) \<ge> 0)"
    5.88      using np by simp 
    5.89 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
    5.90 +  finally show ?case using nbt nb by (simp add: ring_simps)
    5.91  next
    5.92    case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
    5.93    from np have np: "real n \<noteq> 0" by simp
    5.94 @@ -1411,10 +1411,10 @@
    5.95      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
    5.96    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) = 0)"
    5.97      by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
    5.98 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
    5.99 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   5.100    also have "\<dots> = (real c *?t + ?n* (?N x e) = 0)"
   5.101      using np by simp 
   5.102 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   5.103 +  finally show ?case using nbt nb by (simp add: ring_simps)
   5.104  next
   5.105    case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+
   5.106    from np have np: "real n \<noteq> 0" by simp
   5.107 @@ -1422,10 +1422,10 @@
   5.108      using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
   5.109    also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
   5.110      by (simp only: nonzero_eq_divide_eq[OF np, where a="real c *(?t/?n) + (?N x e)" 
   5.111 -      and b="0", simplified divide_zero_left]) (simp only: ring_eq_simps)
   5.112 +      and b="0", simplified divide_zero_left]) (simp only: ring_simps)
   5.113    also have "\<dots> = (real c *?t + ?n* (?N x e) \<noteq> 0)"
   5.114      using np by simp 
   5.115 -  finally show ?case using nbt nb by (simp add: ring_eq_simps)
   5.116 +  finally show ?case using nbt nb by (simp add: ring_simps)
   5.117  qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real n" and b'="x"] nth_pos2)
   5.118  
   5.119  lemma uset_l:
   5.120 @@ -1476,7 +1476,7 @@
   5.121  using lp px noS
   5.122  proof (induct p rule: isrlfm.induct)
   5.123    case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   5.124 -    from prems have "x * real c + ?N x e < 0" by (simp add: ring_eq_simps)
   5.125 +    from prems have "x * real c + ?N x e < 0" by (simp add: ring_simps)
   5.126      hence pxc: "x < (- ?N x e) / real c" 
   5.127        by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
   5.128      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   5.129 @@ -1485,7 +1485,7 @@
   5.130      moreover {assume y: "y < (-?N x e)/ real c"
   5.131        hence "y * real c < - ?N x e"
   5.132  	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   5.133 -      hence "real c * y + ?N x e < 0" by (simp add: ring_eq_simps)
   5.134 +      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
   5.135        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   5.136      moreover {assume y: "y > (- ?N x e) / real c" 
   5.137        with yu have eu: "u > (- ?N x e) / real c" by auto
   5.138 @@ -1495,7 +1495,7 @@
   5.139      ultimately show ?case by blast
   5.140  next
   5.141    case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp +
   5.142 -    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_eq_simps)
   5.143 +    from prems have "x * real c + ?N x e \<le> 0" by (simp add: ring_simps)
   5.144      hence pxc: "x \<le> (- ?N x e) / real c" 
   5.145        by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
   5.146      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   5.147 @@ -1504,7 +1504,7 @@
   5.148      moreover {assume y: "y < (-?N x e)/ real c"
   5.149        hence "y * real c < - ?N x e"
   5.150  	by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   5.151 -      hence "real c * y + ?N x e < 0" by (simp add: ring_eq_simps)
   5.152 +      hence "real c * y + ?N x e < 0" by (simp add: ring_simps)
   5.153        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   5.154      moreover {assume y: "y > (- ?N x e) / real c" 
   5.155        with yu have eu: "u > (- ?N x e) / real c" by auto
   5.156 @@ -1514,7 +1514,7 @@
   5.157      ultimately show ?case by blast
   5.158  next
   5.159    case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   5.160 -    from prems have "x * real c + ?N x e > 0" by (simp add: ring_eq_simps)
   5.161 +    from prems have "x * real c + ?N x e > 0" by (simp add: ring_simps)
   5.162      hence pxc: "x > (- ?N x e) / real c" 
   5.163        by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
   5.164      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   5.165 @@ -1523,7 +1523,7 @@
   5.166      moreover {assume y: "y > (-?N x e)/ real c"
   5.167        hence "y * real c > - ?N x e"
   5.168  	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   5.169 -      hence "real c * y + ?N x e > 0" by (simp add: ring_eq_simps)
   5.170 +      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
   5.171        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   5.172      moreover {assume y: "y < (- ?N x e) / real c" 
   5.173        with ly have eu: "l < (- ?N x e) / real c" by auto
   5.174 @@ -1533,7 +1533,7 @@
   5.175      ultimately show ?case by blast
   5.176  next
   5.177    case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   5.178 -    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_eq_simps)
   5.179 +    from prems have "x * real c + ?N x e \<ge> 0" by (simp add: ring_simps)
   5.180      hence pxc: "x \<ge> (- ?N x e) / real c" 
   5.181        by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
   5.182      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   5.183 @@ -1542,7 +1542,7 @@
   5.184      moreover {assume y: "y > (-?N x e)/ real c"
   5.185        hence "y * real c > - ?N x e"
   5.186  	by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
   5.187 -      hence "real c * y + ?N x e > 0" by (simp add: ring_eq_simps)
   5.188 +      hence "real c * y + ?N x e > 0" by (simp add: ring_simps)
   5.189        hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp}
   5.190      moreover {assume y: "y < (- ?N x e) / real c" 
   5.191        with ly have eu: "l < (- ?N x e) / real c" by auto
   5.192 @@ -1553,7 +1553,7 @@
   5.193  next
   5.194    case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+
   5.195      from cp have cnz: "real c \<noteq> 0" by simp
   5.196 -    from prems have "x * real c + ?N x e = 0" by (simp add: ring_eq_simps)
   5.197 +    from prems have "x * real c + ?N x e = 0" by (simp add: ring_simps)
   5.198      hence pxc: "x = (- ?N x e) / real c" 
   5.199        by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
   5.200      from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto
   5.201 @@ -1566,9 +1566,9 @@
   5.202      with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto
   5.203      hence "y* real c \<noteq> -?N x e"      
   5.204        by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
   5.205 -    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_eq_simps)
   5.206 +    hence "y* real c + ?N x e \<noteq> 0" by (simp add: ring_simps)
   5.207      thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] 
   5.208 -      by (simp add: ring_eq_simps)
   5.209 +      by (simp add: ring_simps)
   5.210  qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"])
   5.211  
   5.212  lemma finite_set_intervals:
   5.213 @@ -1731,7 +1731,7 @@
   5.214  	by (simp add: mult_commute)
   5.215        from tnb snb have st_nb: "numbound0 ?st" by simp
   5.216        have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   5.217 -	using mnp mp np by (simp add: ring_eq_simps add_divide_distrib)
   5.218 +	using mnp mp np by (simp add: ring_simps add_divide_distrib)
   5.219        from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"] 
   5.220        have "?I x (usubst p (?st,2*n*m)) = ?I ((?N t / real n + ?N s / real m) /2) p" by (simp only: st[symmetric])}
   5.221      with rinf_uset[OF lp nmi npi px] have "?F" by blast hence "?D" by blast}
   5.222 @@ -1782,14 +1782,14 @@
   5.223    from Ul th have mnz: "m \<noteq> 0" by auto
   5.224    from Ul th have  nnz: "n \<noteq> 0" by auto  
   5.225    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   5.226 -   using mnz nnz by (simp add: ring_eq_simps add_divide_distrib)
   5.227 +   using mnz nnz by (simp add: ring_simps add_divide_distrib)
   5.228   
   5.229    thus "(real m *  Inum (x # bs) t + real n * Inum (x # bs) s) /
   5.230         (2 * real n * real m)
   5.231         \<in> (\<lambda>((t, n), s, m).
   5.232               (Inum (x # bs) t / real n + Inum (x # bs) s / real m) / 2) `
   5.233           (set U \<times> set U)"using mnz nnz th  
   5.234 -    apply (auto simp add: th add_divide_distrib ring_eq_simps split_def image_def)
   5.235 +    apply (auto simp add: th add_divide_distrib ring_simps split_def image_def)
   5.236      by (rule_tac x="(s,m)" in bexI,simp_all) 
   5.237    (rule_tac x="(t,n)" in bexI,simp_all)
   5.238  next
   5.239 @@ -1800,7 +1800,7 @@
   5.240    from Ul smU have mnz: "m \<noteq> 0" by auto
   5.241    from Ul tnU have  nnz: "n \<noteq> 0" by auto  
   5.242    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   5.243 -   using mnz nnz by (simp add: ring_eq_simps add_divide_distrib)
   5.244 +   using mnz nnz by (simp add: ring_simps add_divide_distrib)
   5.245   let ?P = "\<lambda> (t',n') (s',m'). (Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2"
   5.246   have Pc:"\<forall> a b. ?P a b = ?P b a"
   5.247     by auto
   5.248 @@ -1813,7 +1813,7 @@
   5.249   from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0" by auto
   5.250   let ?st' = "Add (Mul m' t') (Mul n' s')"
   5.251     have st': "(?N t' / real n' + ?N s' / real m')/2 = ?N ?st' / real (2*n'*m')"
   5.252 -   using mnz' nnz' by (simp add: ring_eq_simps add_divide_distrib)
   5.253 +   using mnz' nnz' by (simp add: ring_simps add_divide_distrib)
   5.254   from Pts' have 
   5.255     "(Inum (x # bs) t / real n + Inum (x # bs) s / real m)/2 = (Inum (x # bs) t' / real n' + Inum (x # bs) s' / real m')/2" by simp
   5.256   also have "\<dots> = ((\<lambda>(t, n). Inum (x # bs) t / real n) ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t',n'),(s',m'))))" by (simp add: st')
   5.257 @@ -1843,7 +1843,7 @@
   5.258        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
   5.259      from tnb snb have stnb: "numbound0 ?st" by simp
   5.260    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   5.261 -   using mp np by (simp add: ring_eq_simps add_divide_distrib)
   5.262 +   using mp np by (simp add: ring_simps add_divide_distrib)
   5.263    from tnU smU UU' have "?g ((t,n),(s,m)) \<in> ?f ` U'" by blast
   5.264    hence "\<exists> (t',n') \<in> U'. ?g ((t,n),(s,m)) = ?f (t',n')"
   5.265      by auto (rule_tac x="(a,b)" in bexI, auto)
   5.266 @@ -1871,7 +1871,7 @@
   5.267        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
   5.268      from tnb snb have stnb: "numbound0 ?st" by simp
   5.269    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
   5.270 -   using mp np by (simp add: ring_eq_simps add_divide_distrib)
   5.271 +   using mp np by (simp add: ring_simps add_divide_distrib)
   5.272    from U' tnU' have tnb': "numbound0 t'" and np': "real n' > 0" by auto
   5.273    from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified th[simplified split_def fst_conv snd_conv] st] Pt'
   5.274    have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real (2 * n * m) # bs) p" by simp
   5.275 @@ -1972,8 +1972,6 @@
   5.276  using ferrack qelim_ci prep
   5.277  unfolding linrqe_def by auto
   5.278  
   5.279 -declare max_def [code unfold]
   5.280 -
   5.281  code_module Ferrack
   5.282  file "generated_ferrack.ML"
   5.283  contains linrqe = "linrqe"
     6.1 --- a/src/HOL/Finite_Set.thy	Fri Jun 22 22:41:17 2007 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Sat Jun 23 19:33:22 2007 +0200
     6.3 @@ -970,12 +970,12 @@
     6.4  lemma setsum_Un_nat: "finite A ==> finite B ==>
     6.5      (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
     6.6    -- {* For the natural numbers, we have subtraction. *}
     6.7 -  by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
     6.8 +  by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
     6.9  
    6.10  lemma setsum_Un: "finite A ==> finite B ==>
    6.11      (setsum f (A Un B) :: 'a :: ab_group_add) =
    6.12        setsum f A + setsum f B - setsum f (A Int B)"
    6.13 -  by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
    6.14 +  by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
    6.15  
    6.16  lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
    6.17      (if a:A then setsum f A - f a else setsum f A)"
    6.18 @@ -1649,7 +1649,7 @@
    6.19  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
    6.20  apply (cases "finite A")
    6.21  apply (erule finite_induct)
    6.22 -apply (auto simp add: ring_distrib add_ac)
    6.23 +apply (auto simp add: ring_simps)
    6.24  done
    6.25  
    6.26  lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
     7.1 --- a/src/HOL/Groebner_Basis.thy	Fri Jun 22 22:41:17 2007 +0200
     7.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Jun 23 19:33:22 2007 +0200
     7.3 @@ -168,7 +168,7 @@
     7.4  
     7.5  interpretation class_semiring: gb_semiring
     7.6      ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
     7.7 -  by unfold_locales (auto simp add: ring_eq_simps power_Suc)
     7.8 +  by unfold_locales (auto simp add: ring_simps power_Suc)
     7.9  
    7.10  lemmas nat_arith =
    7.11    add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
    7.12 @@ -341,13 +341,13 @@
    7.13  
    7.14  interpretation class_ringb: ringb
    7.15    ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
    7.16 -proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)
    7.17 +proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    7.18    fix w x y z ::"'a::{idom,recpower,number_ring}"
    7.19    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    7.20    hence ynz': "y - z \<noteq> 0" by simp
    7.21    from p have "w * y + x* z - w*z - x*y = 0" by simp
    7.22 -  hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_eq_simps)
    7.23 -  hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps)
    7.24 +  hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps)
    7.25 +  hence "(y - z) * (w - x) = 0" by (simp add: ring_simps)
    7.26    with  no_zero_divirors_neq0 [OF ynz']
    7.27    have "w - x = 0" by blast
    7.28    thus "w = x"  by simp
    7.29 @@ -368,20 +368,20 @@
    7.30  
    7.31  interpretation natgb: semiringb
    7.32    ["op +" "op *" "op ^" "0::nat" "1"]
    7.33 -proof (unfold_locales, simp add: ring_eq_simps power_Suc)
    7.34 +proof (unfold_locales, simp add: ring_simps power_Suc)
    7.35    fix w x y z ::"nat"
    7.36    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    7.37      hence "y < z \<or> y > z" by arith
    7.38      moreover {
    7.39        assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
    7.40        then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    7.41 -      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps)
    7.42 +      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps)
    7.43        hence "x*k = w*k" by simp
    7.44        hence "w = x" using kp by (simp add: mult_cancel2) }
    7.45      moreover {
    7.46        assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    7.47        then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    7.48 -      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps)
    7.49 +      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps)
    7.50        hence "w*k = x*k" by simp
    7.51        hence "w = x" using kp by (simp add: mult_cancel2)}
    7.52      ultimately have "w=x" by blast }
     8.1 --- a/src/HOL/Hyperreal/Deriv.thy	Fri Jun 22 22:41:17 2007 +0200
     8.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Sat Jun 23 19:33:22 2007 +0200
     8.3 @@ -89,7 +89,7 @@
     8.4  lemma DERIV_mult_lemma:
     8.5    fixes a b c d :: "'a::real_field"
     8.6    shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
     8.7 -by (simp add: diff_minus add_divide_distrib [symmetric] ring_distrib)
     8.8 +by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs)
     8.9  
    8.10  lemma DERIV_mult':
    8.11    assumes f: "DERIV f x :> D"
    8.12 @@ -147,7 +147,7 @@
    8.13  lemma inverse_diff_inverse:
    8.14    "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    8.15     \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
    8.16 -by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
    8.17 +by (simp add: ring_simps)
    8.18  
    8.19  lemma DERIV_inverse_lemma:
    8.20    "\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
    8.21 @@ -198,7 +198,7 @@
    8.22  apply (unfold divide_inverse)
    8.23  apply (erule DERIV_mult')
    8.24  apply (erule (1) DERIV_inverse')
    8.25 -apply (simp add: left_diff_distrib nonzero_inverse_mult_distrib)
    8.26 +apply (simp add: ring_distribs nonzero_inverse_mult_distrib)
    8.27  apply (simp add: mult_ac)
    8.28  done
    8.29  
    8.30 @@ -211,7 +211,7 @@
    8.31    show ?case by (simp add: power_Suc f)
    8.32  case (Suc k)
    8.33    from DERIV_mult' [OF f Suc] show ?case
    8.34 -    apply (simp only: of_nat_Suc left_distrib mult_1_left)
    8.35 +    apply (simp only: of_nat_Suc ring_distribs mult_1_left)
    8.36      apply (simp only: power_Suc right_distrib mult_ac add_ac)
    8.37      done
    8.38  qed
    8.39 @@ -1050,7 +1050,7 @@
    8.40  apply (rule linorder_cases [of a b], auto)
    8.41  apply (drule_tac [!] f = f in MVT)
    8.42  apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
    8.43 -apply (auto dest: DERIV_unique simp add: left_distrib diff_minus)
    8.44 +apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus)
    8.45  done
    8.46  
    8.47  lemma DERIV_const_ratio_const2:
     9.1 --- a/src/HOL/Hyperreal/Ln.thy	Fri Jun 22 22:41:17 2007 +0200
     9.2 +++ b/src/HOL/Hyperreal/Ln.thy	Sat Jun 23 19:33:22 2007 +0200
     9.3 @@ -150,7 +150,7 @@
     9.4  lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"
     9.5    apply (subst pos_divide_le_eq)
     9.6    apply (simp add: zero_compare_simps)
     9.7 -  apply (simp add: ring_eq_simps zero_compare_simps)
     9.8 +  apply (simp add: ring_simps zero_compare_simps)
     9.9  done
    9.10  
    9.11  lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
    9.12 @@ -199,7 +199,7 @@
    9.13  proof -
    9.14    assume a: "0 <= (x::real)" and b: "x < 1"
    9.15    have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
    9.16 -    by (simp add: ring_eq_simps power2_eq_square power3_eq_cube)
    9.17 +    by (simp add: ring_simps power2_eq_square power3_eq_cube)
    9.18    also have "... <= 1"
    9.19      by (auto intro: zero_le_power simp add: a)
    9.20    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    9.21 @@ -283,12 +283,9 @@
    9.22    have e: "-x - 2 * x^2 <= - x / (1 - x)"
    9.23      apply (rule mult_imp_le_div_pos)
    9.24      apply (insert prems, force)
    9.25 -    apply (auto simp add: ring_eq_simps power2_eq_square)
    9.26 -    apply (subgoal_tac "- (x * x) + x * (x * (x * 2)) = x^2 * (2 * x - 1)")
    9.27 -    apply (erule ssubst)
    9.28 -    apply (rule mult_nonneg_nonpos)
    9.29 -    apply auto
    9.30 -    apply (auto simp add: ring_eq_simps power2_eq_square)
    9.31 +    apply (auto simp add: ring_simps power2_eq_square)
    9.32 +    apply(insert mult_right_le_one_le[of "x*x" "2*x"])
    9.33 +    apply (simp)
    9.34      done
    9.35    from e d show "- x - 2 * x^2 <= ln (1 - x)"
    9.36      by (rule order_trans)
    9.37 @@ -404,7 +401,7 @@
    9.38    apply simp
    9.39    apply (subst ln_div [THEN sym])
    9.40    apply arith
    9.41 -  apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq 
    9.42 +  apply (auto simp add: ring_simps add_frac_eq frac_eq_eq 
    9.43      add_divide_distrib power2_eq_square)
    9.44    apply (rule mult_pos_pos, assumption)+
    9.45    apply assumption
    9.46 @@ -423,7 +420,7 @@
    9.47      apply auto
    9.48      done
    9.49    have "x * ln y - x * ln x = x * (ln y - ln x)"
    9.50 -    by (simp add: ring_eq_simps)
    9.51 +    by (simp add: ring_simps)
    9.52    also have "... = x * ln(y / x)"
    9.53      apply (subst ln_div)
    9.54      apply (rule b, rule a, rule refl)
    10.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 22 22:41:17 2007 +0200
    10.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Sat Jun 23 19:33:22 2007 +0200
    10.3 @@ -571,12 +571,12 @@
    10.4  lemma power2_sum:
    10.5    fixes x y :: "'a::{number_ring,recpower}"
    10.6    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    10.7 -by (simp add: left_distrib right_distrib power2_eq_square)
    10.8 +by (simp add: ring_distribs power2_eq_square)
    10.9  
   10.10  lemma power2_diff:
   10.11    fixes x y :: "'a::{number_ring,recpower}"
   10.12    shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   10.13 -by (simp add: left_diff_distrib right_diff_distrib power2_eq_square)
   10.14 +by (simp add: ring_distribs power2_eq_square)
   10.15  
   10.16  lemma real_sqrt_sum_squares_triangle_ineq:
   10.17    "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
   10.18 @@ -586,7 +586,7 @@
   10.19  apply (rule mult_left_mono)
   10.20  apply (rule power2_le_imp_le)
   10.21  apply (simp add: power2_sum power_mult_distrib)
   10.22 -apply (simp add: ring_distrib)
   10.23 +apply (simp add: ring_distribs)
   10.24  apply (subgoal_tac "0 \<le> b\<twosuperior> * c\<twosuperior> + a\<twosuperior> * d\<twosuperior> - 2 * (a * c) * (b * d)", simp)
   10.25  apply (rule_tac b="(a * d - b * c)\<twosuperior>" in ord_le_eq_trans)
   10.26  apply (rule zero_le_power2)
    11.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Jun 22 22:41:17 2007 +0200
    11.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Sat Jun 23 19:33:22 2007 +0200
    11.3 @@ -392,7 +392,7 @@
    11.4  lemma inverse_diff_inverse:
    11.5    "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    11.6     \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
    11.7 -by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
    11.8 +by (simp add: ring_simps)
    11.9  
   11.10  lemma Bseq_inverse_lemma:
   11.11    fixes x :: "'a::real_normed_div_algebra"
   11.12 @@ -1065,7 +1065,7 @@
   11.13  apply (erule mult_left_mono)
   11.14  apply (rule add_increasing [OF x], simp)
   11.15  apply (simp add: real_of_nat_Suc)
   11.16 -apply (simp add: ring_distrib)
   11.17 +apply (simp add: ring_distribs)
   11.18  apply (simp add: mult_nonneg_nonneg x)
   11.19  done
   11.20  
    12.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Fri Jun 22 22:41:17 2007 +0200
    12.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sat Jun 23 19:33:22 2007 +0200
    12.3 @@ -40,7 +40,7 @@
    12.4  apply (simp add: right_distrib del: setsum_op_ivl_Suc)
    12.5  apply (subst mult_left_commute [where a="x - y"])
    12.6  apply (erule subst)
    12.7 -apply (simp add: power_Suc ring_eq_simps)
    12.8 +apply (simp add: power_Suc ring_simps)
    12.9  done
   12.10  
   12.11  lemma lemma_realpow_rev_sumr:
   12.12 @@ -423,7 +423,7 @@
   12.13        apply (rule sums_summable [OF diffs_equiv [OF C]])
   12.14        apply (rule_tac f="suminf" in arg_cong)
   12.15        apply (rule ext)
   12.16 -      apply (simp add: ring_eq_simps)
   12.17 +      apply (simp add: ring_simps)
   12.18        done
   12.19    next
   12.20      show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
   12.21 @@ -2031,7 +2031,7 @@
   12.22    also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   12.23      by (simp only: cos_add sin_add)
   12.24    also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
   12.25 -    by (simp add: ring_eq_simps power2_eq_square)
   12.26 +    by (simp add: ring_simps power2_eq_square)
   12.27    finally have "?c\<twosuperior> = (sqrt 3 / 2)\<twosuperior>"
   12.28      using pos_c by (simp add: sin_squared_eq power_divide)
   12.29    thus ?thesis
    13.1 --- a/src/HOL/IntDef.thy	Fri Jun 22 22:41:17 2007 +0200
    13.2 +++ b/src/HOL/IntDef.thy	Sat Jun 23 19:33:22 2007 +0200
    13.3 @@ -137,13 +137,13 @@
    13.4    show "i - j = i + - j"
    13.5      by (simp add: diff_int_def)
    13.6    show "(i * j) * k = i * (j * k)"
    13.7 -    by (cases i, cases j, cases k) (simp add: mult ring_eq_simps)
    13.8 +    by (cases i, cases j, cases k) (simp add: mult ring_simps)
    13.9    show "i * j = j * i"
   13.10 -    by (cases i, cases j) (simp add: mult ring_eq_simps)
   13.11 +    by (cases i, cases j) (simp add: mult ring_simps)
   13.12    show "1 * i = i"
   13.13      by (cases i) (simp add: One_int_def mult)
   13.14    show "(i + j) * k = i * k + j * k"
   13.15 -    by (cases i, cases j, cases k) (simp add: add mult ring_eq_simps)
   13.16 +    by (cases i, cases j, cases k) (simp add: add mult ring_simps)
   13.17    show "0 \<noteq> (1::int)"
   13.18      by (simp add: Zero_int_def One_int_def)
   13.19  qed
   13.20 @@ -358,7 +358,7 @@
   13.21    also have "\<dots> = (\<exists>n. z - w = int n)"
   13.22      by (auto elim: zero_le_imp_eq_int)
   13.23    also have "\<dots> = (\<exists>n. z = w + int n)"
   13.24 -    by (simp only: group_eq_simps)
   13.25 +    by (simp only: group_simps)
   13.26    finally show ?thesis .
   13.27  qed
   13.28  
    14.1 --- a/src/HOL/IntDiv.thy	Fri Jun 22 22:41:17 2007 +0200
    14.2 +++ b/src/HOL/IntDiv.thy	Sat Jun 23 19:33:22 2007 +0200
    14.3 @@ -1210,7 +1210,7 @@
    14.4    done
    14.5  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    14.6    using zmod_zdiv_equality[where a="m" and b="n"]
    14.7 -  by (simp add: ring_eq_simps)
    14.8 +  by (simp add: ring_simps)
    14.9  
   14.10  lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
   14.11  apply (subgoal_tac "m mod n = 0")
    15.1 --- a/src/HOL/Library/BigO.thy	Fri Jun 22 22:41:17 2007 +0200
    15.2 +++ b/src/HOL/Library/BigO.thy	Sat Jun 23 19:33:22 2007 +0200
    15.3 @@ -103,7 +103,7 @@
    15.4    apply (auto simp add: bigo_alt_def set_plus)
    15.5    apply (rule_tac x = "c + ca" in exI)
    15.6    apply auto
    15.7 -  apply (simp add: ring_distrib func_plus)
    15.8 +  apply (simp add: ring_distribs func_plus)
    15.9    apply (rule order_trans)
   15.10    apply (rule abs_triangle_ineq)
   15.11    apply (rule add_mono)
   15.12 @@ -134,7 +134,7 @@
   15.13    apply (simp)
   15.14    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   15.15    apply (erule order_trans)
   15.16 -  apply (simp add: ring_distrib)
   15.17 +  apply (simp add: ring_distribs)
   15.18    apply (rule mult_left_mono)
   15.19    apply assumption
   15.20    apply (simp add: order_less_le)
   15.21 @@ -155,7 +155,7 @@
   15.22    apply (simp)
   15.23    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   15.24    apply (erule order_trans)
   15.25 -  apply (simp add: ring_distrib)
   15.26 +  apply (simp add: ring_distribs)
   15.27    apply (rule mult_left_mono)
   15.28    apply (simp add: order_less_le)
   15.29    apply (simp add: order_less_le)
   15.30 @@ -192,7 +192,7 @@
   15.31    apply clarify
   15.32    apply (drule_tac x = "xa" in spec)+
   15.33    apply (subgoal_tac "0 <= f xa + g xa")
   15.34 -  apply (simp add: ring_distrib)
   15.35 +  apply (simp add: ring_distribs)
   15.36    apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
   15.37    apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
   15.38        max c ca * f xa + max c ca * g xa")
   15.39 @@ -349,7 +349,7 @@
   15.40    apply (drule set_plus_imp_minus)
   15.41    apply (rule set_minus_imp_plus)
   15.42    apply (drule bigo_mult3 [where g = g and j = g])
   15.43 -  apply (auto simp add: ring_eq_simps mult_ac)
   15.44 +  apply (auto simp add: ring_simps)
   15.45    done
   15.46  
   15.47  lemma bigo_mult5: "ALL x. f x ~= 0 ==>
    16.1 --- a/src/HOL/Library/Commutative_Ring.thy	Fri Jun 22 22:41:17 2007 +0200
    16.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Sat Jun 23 19:33:22 2007 +0200
    16.3 @@ -174,11 +174,11 @@
    16.4  
    16.5  text {* mkPinj preserve semantics *}
    16.6  lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
    16.7 -  by (induct B) (auto simp add: mkPinj_def ring_eq_simps)
    16.8 +  by (induct B) (auto simp add: mkPinj_def ring_simps)
    16.9  
   16.10  text {* mkPX preserves semantics *}
   16.11  lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
   16.12 -  by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_eq_simps)
   16.13 +  by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_simps)
   16.14  
   16.15  text {* Correctness theorems for the implemented operations *}
   16.16  
   16.17 @@ -193,13 +193,13 @@
   16.18    show ?case
   16.19    proof (rule linorder_cases)
   16.20      assume "x < y"
   16.21 -    with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)
   16.22 +    with 6 show ?case by (simp add: mkPinj_ci ring_simps)
   16.23    next
   16.24      assume "x = y"
   16.25      with 6 show ?case by (simp add: mkPinj_ci)
   16.26    next
   16.27      assume "x > y"
   16.28 -    with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)
   16.29 +    with 6 show ?case by (simp add: mkPinj_ci ring_simps)
   16.30    qed
   16.31  next
   16.32    case (7 x P Q y R)
   16.33 @@ -207,7 +207,7 @@
   16.34    moreover
   16.35    { assume "x = 0" with 7 have ?case by simp }
   16.36    moreover
   16.37 -  { assume "x = 1" with 7 have ?case by (simp add: ring_eq_simps) }
   16.38 +  { assume "x = 1" with 7 have ?case by (simp add: ring_simps) }
   16.39    moreover
   16.40    { assume "x > 1" from 7 have ?case by (cases x) simp_all }
   16.41    ultimately show ?case by blast
   16.42 @@ -226,20 +226,20 @@
   16.43    show ?case
   16.44    proof (rule linorder_cases)
   16.45      assume a: "x < y" hence "EX d. d + x = y" by arith
   16.46 -    with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_eq_simps)
   16.47 +    with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_simps)
   16.48    next
   16.49      assume a: "y < x" hence "EX d. d + y = x" by arith
   16.50 -    with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_eq_simps)
   16.51 +    with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_simps)
   16.52    next
   16.53      assume "x = y"
   16.54 -    with 9 show ?case by (simp add: mkPX_ci ring_eq_simps)
   16.55 +    with 9 show ?case by (simp add: mkPX_ci ring_simps)
   16.56    qed
   16.57 -qed (auto simp add: ring_eq_simps)
   16.58 +qed (auto simp add: ring_simps)
   16.59  
   16.60  text {* Multiplication *}
   16.61  lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
   16.62    by (induct P Q arbitrary: l rule: mul.induct)
   16.63 -    (simp_all add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
   16.64 +    (simp_all add: mkPX_ci mkPinj_ci ring_simps add_ci power_add)
   16.65  
   16.66  text {* Substraction *}
   16.67  lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
   16.68 @@ -248,7 +248,7 @@
   16.69  text {* Square *}
   16.70  lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
   16.71    by (induct P arbitrary: ls)
   16.72 -    (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_eq_simps power_add)
   16.73 +    (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_simps power_add)
   16.74  
   16.75  text {* Power *}
   16.76  lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
    17.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Jun 22 22:41:17 2007 +0200
    17.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Sat Jun 23 19:33:22 2007 +0200
    17.3 @@ -88,7 +88,7 @@
    17.4  instance "fun" :: (type,comm_ring_1)comm_ring_1
    17.5    apply default
    17.6     apply (auto simp add: func_plus func_times func_minus func_diff ext
    17.7 -     func_one func_zero ring_eq_simps)
    17.8 +     func_one func_zero ring_simps)
    17.9    apply (drule fun_cong)
   17.10    apply simp
   17.11    done
   17.12 @@ -328,21 +328,21 @@
   17.13  
   17.14  lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   17.15      (a * b) +o (a *o C)"
   17.16 -  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
   17.17 +  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   17.18  
   17.19  lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
   17.20      (a *o B) + (a *o C)"
   17.21 -  apply (auto simp add: set_plus elt_set_times_def ring_distrib)
   17.22 +  apply (auto simp add: set_plus elt_set_times_def ring_distribs)
   17.23     apply blast
   17.24    apply (rule_tac x = "b + bb" in exI)
   17.25 -  apply (auto simp add: ring_distrib)
   17.26 +  apply (auto simp add: ring_distribs)
   17.27    done
   17.28  
   17.29  lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
   17.30      a *o D + C * D"
   17.31    apply (auto intro!: subsetI simp add:
   17.32      elt_set_plus_def elt_set_times_def set_times
   17.33 -    set_plus ring_distrib)
   17.34 +    set_plus ring_distribs)
   17.35    apply auto
   17.36    done
   17.37  
    18.1 --- a/src/HOL/Library/Word.thy	Fri Jun 22 22:41:17 2007 +0200
    18.2 +++ b/src/HOL/Library/Word.thy	Sat Jun 23 19:33:22 2007 +0200
    18.3 @@ -443,7 +443,7 @@
    18.4            bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
    18.5            by simp
    18.6          also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
    18.7 -          by (simp add: ring_distrib)
    18.8 +          by (simp add: ring_distribs)
    18.9          finally show ?thesis .
   18.10        qed
   18.11      qed
    19.1 --- a/src/HOL/Matrix/LP.thy	Fri Jun 22 22:41:17 2007 +0200
    19.2 +++ b/src/HOL/Matrix/LP.thy	Sat Jun 23 19:33:22 2007 +0200
    19.3 @@ -20,7 +20,7 @@
    19.4  proof -
    19.5    from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    19.6    from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    19.7 -  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_eq_simps)  
    19.8 +  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_simps)  
    19.9    from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
   19.10    have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
   19.11      by (simp only: 4 estimate_by_abs)  
   19.12 @@ -32,7 +32,7 @@
   19.13      by (simp add: abs_triangle_ineq mult_right_mono)    
   19.14    have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
   19.15      by (simp add: abs_le_mult mult_right_mono)  
   19.16 -  have 10: "c'-c = -(c-c')" by (simp add: ring_eq_simps)
   19.17 +  have 10: "c'-c = -(c-c')" by (simp add: ring_simps)
   19.18    have 11: "abs (c'-c) = abs (c-c')" 
   19.19      by (subst 10, subst abs_minus_cancel, simp)
   19.20    have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
   19.21 @@ -85,7 +85,7 @@
   19.22      apply simp
   19.23      done
   19.24    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   19.25 -    by (simp add: ring_eq_simps)
   19.26 +    by (simp add: ring_simps)
   19.27    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
   19.28      by (simp_all add: prems mult_mono)
   19.29    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
   19.30 @@ -134,10 +134,10 @@
   19.31    (is "_ <= _ + ?C")
   19.32  proof -
   19.33    from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   19.34 -  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_eq_simps)  
   19.35 +  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_simps)  
   19.36    ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   19.37    then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   19.38 -  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_eq_simps)
   19.39 +  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_simps)
   19.40    have s2: "c - y * A <= c2 - y * A1"
   19.41      by (simp add: diff_def prems add_mono mult_left_mono)
   19.42    have s1: "c1 - y * A2 <= c - y * A"
    20.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jun 22 22:41:17 2007 +0200
    20.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Jun 23 19:33:22 2007 +0200
    20.3 @@ -59,17 +59,17 @@
    20.4    show "A * B * C = A * (B * C)"
    20.5      apply (simp add: times_matrix_def)
    20.6      apply (rule mult_matrix_assoc)
    20.7 -    apply (simp_all add: associative_def ring_eq_simps)
    20.8 +    apply (simp_all add: associative_def ring_simps)
    20.9      done
   20.10    show "(A + B) * C = A * C + B * C"
   20.11      apply (simp add: times_matrix_def plus_matrix_def)
   20.12      apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
   20.13 -    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   20.14 +    apply (simp_all add: associative_def commutative_def ring_simps)
   20.15      done
   20.16    show "A * (B + C) = A * B + A * C"
   20.17      apply (simp add: times_matrix_def plus_matrix_def)
   20.18      apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
   20.19 -    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   20.20 +    apply (simp_all add: associative_def commutative_def ring_simps)
   20.21      done  
   20.22    show "abs A = sup A (-A)" 
   20.23      by (simp add: abs_matrix_def)
   20.24 @@ -264,24 +264,24 @@
   20.25    "scalar_mult a m == apply_matrix (op * a) m"
   20.26  
   20.27  lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   20.28 -  by (simp add: scalar_mult_def)
   20.29 +by (simp add: scalar_mult_def)
   20.30  
   20.31  lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
   20.32 -  by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
   20.33 +by (simp add: scalar_mult_def apply_matrix_add ring_simps)
   20.34  
   20.35  lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
   20.36 -  by (simp add: scalar_mult_def)
   20.37 +by (simp add: scalar_mult_def)
   20.38  
   20.39  lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
   20.40 -  apply (subst Rep_matrix_inject[symmetric])
   20.41 -  apply (rule ext)+
   20.42 -  apply (auto)
   20.43 -  done
   20.44 +apply (subst Rep_matrix_inject[symmetric])
   20.45 +apply (rule ext)+
   20.46 +apply (auto)
   20.47 +done
   20.48  
   20.49  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
   20.50 -  by (simp add: minus_matrix_def)
   20.51 +by (simp add: minus_matrix_def)
   20.52  
   20.53  lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
   20.54 -  by (simp add: abs_lattice sup_matrix_def)
   20.55 +by (simp add: abs_lattice sup_matrix_def)
   20.56  
   20.57  end
    21.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Jun 22 22:41:17 2007 +0200
    21.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Sat Jun 23 19:33:22 2007 +0200
    21.3 @@ -282,7 +282,7 @@
    21.4      apply (rule conjI)
    21.5      apply (intro strip)
    21.6      apply (frule_tac as=brr in sorted_spvec_cons1)
    21.7 -    apply (simp add: ring_eq_simps sparse_row_matrix_cons)
    21.8 +    apply (simp add: ring_simps sparse_row_matrix_cons)
    21.9      apply (simplesubst Rep_matrix_zero_imp_mult_zero) 
   21.10      apply (simp)
   21.11      apply (intro strip)
   21.12 @@ -304,7 +304,7 @@
   21.13      
   21.14      apply (intro strip | rule conjI)+
   21.15      apply (frule_tac as=arr in sorted_spvec_cons1)
   21.16 -    apply (simp add: ring_eq_simps)
   21.17 +    apply (simp add: ring_simps)
   21.18      apply (subst Rep_matrix_zero_imp_mult_zero)
   21.19      apply (simp)
   21.20      apply (rule disjI2)
   21.21 @@ -318,7 +318,7 @@
   21.22      apply (simp_all)
   21.23      apply (frule_tac as=arr in sorted_spvec_cons1)
   21.24      apply (frule_tac as=brr in sorted_spvec_cons1)
   21.25 -    apply (simp add: sparse_row_matrix_cons ring_eq_simps sparse_row_vector_addmult_spvec)
   21.26 +    apply (simp add: sparse_row_matrix_cons ring_simps sparse_row_vector_addmult_spvec)
   21.27      apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
   21.28      apply (auto)
   21.29      apply (rule sorted_sparse_row_matrix_zero)
   21.30 @@ -368,7 +368,7 @@
   21.31  lemma sparse_row_mult_spmat[rule_format]: 
   21.32    "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
   21.33    apply (induct A)
   21.34 -  apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_eq_simps move_matrix_mult)
   21.35 +  apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_simps move_matrix_mult)
   21.36    done
   21.37  
   21.38  lemma sorted_spvec_mult_spmat[rule_format]:
   21.39 @@ -1146,8 +1146,8 @@
   21.40    add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
   21.41    apply (simp add: Let_def)
   21.42    apply (insert prems)
   21.43 -  apply (simp add: sparse_row_matrix_op_simps ring_eq_simps)  
   21.44 -  apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_eq_simps])
   21.45 +  apply (simp add: sparse_row_matrix_op_simps ring_simps)  
   21.46 +  apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
   21.47    apply (auto)
   21.48    done
   21.49  
    22.1 --- a/src/HOL/MetisExamples/BigO.thy	Fri Jun 22 22:41:17 2007 +0200
    22.2 +++ b/src/HOL/MetisExamples/BigO.thy	Sat Jun 23 19:33:22 2007 +0200
    22.3 @@ -476,7 +476,7 @@
    22.4    apply (auto simp add: bigo_alt_def set_plus)
    22.5    apply (rule_tac x = "c + ca" in exI)
    22.6    apply auto
    22.7 -  apply (simp add: ring_distrib func_plus)
    22.8 +  apply (simp add: ring_distribs func_plus)
    22.9    apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
   22.10  done
   22.11  
   22.12 @@ -503,7 +503,7 @@
   22.13    apply (simp)
   22.14    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   22.15    apply (erule order_trans)
   22.16 -  apply (simp add: ring_distrib)
   22.17 +  apply (simp add: ring_distribs)
   22.18    apply (rule mult_left_mono)
   22.19    apply assumption
   22.20    apply (simp add: order_less_le)
   22.21 @@ -524,7 +524,7 @@
   22.22    apply (simp)
   22.23    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   22.24    apply (erule order_trans)
   22.25 -  apply (simp add: ring_distrib)
   22.26 +  apply (simp add: ring_distribs)
   22.27    apply (rule mult_left_mono)
   22.28    apply (simp add: order_less_le)
   22.29    apply (simp add: order_less_le)
   22.30 @@ -563,7 +563,7 @@
   22.31    apply clarify
   22.32    apply (drule_tac x = "xa" in spec)+
   22.33    apply (subgoal_tac "0 <= f xa + g xa")
   22.34 -  apply (simp add: ring_distrib)
   22.35 +  apply (simp add: ring_distribs)
   22.36    apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
   22.37    apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
   22.38        max c ca * f xa + max c ca * g xa")
    23.1 --- a/src/HOL/OrderedGroup.thy	Fri Jun 22 22:41:17 2007 +0200
    23.2 +++ b/src/HOL/OrderedGroup.thy	Sat Jun 23 19:33:22 2007 +0200
    23.3 @@ -171,6 +171,9 @@
    23.4  lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
    23.5  by (simp add: diff_minus)
    23.6  
    23.7 +lemma uminus_add_conv_diff: "-a + b = b - (a::'a::ab_group_add)"
    23.8 +by(simp add:diff_minus add_commute)
    23.9 +
   23.10  lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))" 
   23.11  proof 
   23.12    assume "- a = - b"
   23.13 @@ -1036,21 +1039,18 @@
   23.14    apply (simp_all add: prems)
   23.15    done
   23.16  
   23.17 -lemmas group_eq_simps =
   23.18 +lemmas group_simps =
   23.19    mult_ac
   23.20    add_ac
   23.21    add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   23.22 -  diff_eq_eq eq_diff_eq
   23.23 +  diff_eq_eq eq_diff_eq  diff_minus[symmetric] uminus_add_conv_diff
   23.24 +  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   23.25  
   23.26  lemma estimate_by_abs:
   23.27  "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
   23.28  proof -
   23.29 -  assume 1: "a+b <= c"
   23.30 -  have 2: "a <= c+(-b)"
   23.31 -    apply (insert 1)
   23.32 -    apply (drule_tac add_right_mono[where c="-b"])
   23.33 -    apply (simp add: group_eq_simps)
   23.34 -    done
   23.35 +  assume "a+b <= c"
   23.36 +  hence 2: "a <= c+(-b)" by (simp add: group_simps)
   23.37    have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
   23.38    show ?thesis by (rule le_add_right_mono[OF 2 3])
   23.39  qed
    24.1 --- a/src/HOL/Presburger.thy	Fri Jun 22 22:41:17 2007 +0200
    24.2 +++ b/src/HOL/Presburger.thy	Sat Jun 23 19:33:22 2007 +0200
    24.3 @@ -60,7 +60,7 @@
    24.4    "\<forall>x k. F = F"
    24.5  by simp_all
    24.6    (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
    24.7 -    simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
    24.8 +    simp add: ring_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_simps)+
    24.9  
   24.10  subsection{* The A and B sets *}
   24.11  lemma bset:
   24.12 @@ -98,7 +98,7 @@
   24.13    {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x - D) > t"
   24.14      hence "x -t \<le> D" and "1 \<le> x - t" by simp+
   24.15        hence "\<exists>j \<in> {1 .. D}. x - t = j" by auto
   24.16 -      hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_eq_simps)
   24.17 +      hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_simps)
   24.18        with nob tB have "False" by simp}
   24.19    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t)" by blast
   24.20  next
   24.21 @@ -106,18 +106,18 @@
   24.22    {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x - D) \<ge> t"
   24.23      hence "x - (t - 1) \<le> D" and "1 \<le> x - (t - 1)" by simp+
   24.24        hence "\<exists>j \<in> {1 .. D}. x - (t - 1) = j" by auto
   24.25 -      hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_eq_simps)
   24.26 +      hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_simps)
   24.27        with nob tB have "False" by simp}
   24.28    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast
   24.29  next
   24.30    assume d: "d dvd D"
   24.31    {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
   24.32 -      by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_eq_simps)}
   24.33 +      by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_simps)}
   24.34    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
   24.35  next
   24.36    assume d: "d dvd D"
   24.37    {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t"
   24.38 -      by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_eq_simps)}
   24.39 +      by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_simps)}
   24.40    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto
   24.41  qed blast
   24.42  
   24.43 @@ -156,26 +156,26 @@
   24.44    {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x < t" and ng: "\<not> (x + D) < t"
   24.45      hence "t - x \<le> D" and "1 \<le> t - x" by simp+
   24.46        hence "\<exists>j \<in> {1 .. D}. t - x = j" by auto
   24.47 -      hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_eq_simps) 
   24.48 +      hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_simps) 
   24.49        with nob tA have "False" by simp}
   24.50    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast
   24.51  next
   24.52    assume dp: "D > 0" and tA:"t + 1\<in> A"
   24.53    {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t"
   24.54 -    hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_eq_simps)
   24.55 +    hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_simps)
   24.56        hence "\<exists>j \<in> {1 .. D}. (t + 1) - x = j" by auto
   24.57 -      hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_eq_simps)
   24.58 +      hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_simps)
   24.59        with nob tA have "False" by simp}
   24.60    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast
   24.61  next
   24.62    assume d: "d dvd D"
   24.63    {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t"
   24.64 -      by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_eq_simps)}
   24.65 +      by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_simps)}
   24.66    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp
   24.67  next
   24.68    assume d: "d dvd D"
   24.69    {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
   24.70 -      by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
   24.71 +      by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_simps)}
   24.72    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
   24.73  qed blast
   24.74  
   24.75 @@ -302,7 +302,7 @@
   24.76    from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
   24.77    let ?w' = "x + (abs(x-z)+1) * d"
   24.78    let ?w = "x - (-(abs(x-z) + 1))*d"
   24.79 -  have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
   24.80 +  have ww'[simp]: "?w = ?w'" by (simp add: ring_simps)
   24.81    from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   24.82    hence "P' x = P' ?w" using P1eqP1 by blast
   24.83    also have "\<dots> = P(?w)" using w P1eqP by blast
    25.1 --- a/src/HOL/Real/Float.thy	Fri Jun 22 22:41:17 2007 +0200
    25.2 +++ b/src/HOL/Real/Float.thy	Sat Jun 23 19:33:22 2007 +0200
    25.3 @@ -39,7 +39,7 @@
    25.4    show ?thesis
    25.5    proof (induct a)
    25.6      case (1 n)
    25.7 -    from pos show ?case by (simp add: ring_eq_simps)
    25.8 +    from pos show ?case by (simp add: ring_simps)
    25.9    next
   25.10      case (2 n)
   25.11      show ?case
   25.12 @@ -60,7 +60,7 @@
   25.13      show ?case by simp
   25.14    next
   25.15      case (Suc m)
   25.16 -    show ?case by (auto simp add: ring_eq_simps pow2_add1 prems)
   25.17 +    show ?case by (auto simp add: ring_simps pow2_add1 prems)
   25.18    qed
   25.19  next
   25.20    case (2 n)
   25.21 @@ -73,7 +73,7 @@
   25.22        apply (subst pow2_neg[of "-1"])
   25.23        apply (simp)
   25.24        apply (insert pow2_add1[of "-a"])
   25.25 -      apply (simp add: ring_eq_simps)
   25.26 +      apply (simp add: ring_simps)
   25.27        apply (subst pow2_neg[of "-a"])
   25.28        apply (simp)
   25.29        done
   25.30 @@ -84,7 +84,7 @@
   25.31        apply (auto)
   25.32        apply (subst pow2_neg[of "a + (-2 - int m)"])
   25.33        apply (subst pow2_neg[of "-2 - int m"])
   25.34 -      apply (auto simp add: ring_eq_simps)
   25.35 +      apply (auto simp add: ring_simps)
   25.36        apply (subst a)
   25.37        apply (subst b)
   25.38        apply (simp only: pow2_add1)
   25.39 @@ -92,13 +92,13 @@
   25.40        apply (subst pow2_neg[of "int m + 1"])
   25.41        apply auto
   25.42        apply (insert prems)
   25.43 -      apply (auto simp add: ring_eq_simps)
   25.44 +      apply (auto simp add: ring_simps)
   25.45        done
   25.46    qed
   25.47  qed
   25.48  
   25.49  lemma "float (a, e) + float (b, e) = float (a + b, e)"
   25.50 -by (simp add: float_def ring_eq_simps)
   25.51 +by (simp add: float_def ring_simps)
   25.52  
   25.53  definition
   25.54    int_of_real :: "real \<Rightarrow> int" where
   25.55 @@ -255,7 +255,7 @@
   25.56  
   25.57  lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
   25.58    apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
   25.59 -  apply (simp_all add: pow2_def even_def real_is_int_def ring_eq_simps)
   25.60 +  apply (simp_all add: pow2_def even_def real_is_int_def ring_simps)
   25.61    apply (auto)
   25.62  proof -
   25.63    fix q::int
   25.64 @@ -324,7 +324,7 @@
   25.65    "float (a1, e1) + float (a2, e2) =
   25.66    (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
   25.67    else float (a1*2^(nat (e1-e2))+a2, e2))"
   25.68 -  apply (simp add: float_def ring_eq_simps)
   25.69 +  apply (simp add: float_def ring_simps)
   25.70    apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
   25.71    done
   25.72  
    26.1 --- a/src/HOL/Real/RComplete.thy	Fri Jun 22 22:41:17 2007 +0200
    26.2 +++ b/src/HOL/Real/RComplete.thy	Sat Jun 23 19:33:22 2007 +0200
    26.3 @@ -377,7 +377,7 @@
    26.4    hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1"
    26.5      by (rule mult_strict_left_mono) simp
    26.6    hence "x < real (Suc n)"
    26.7 -    by (simp add: ring_eq_simps)
    26.8 +    by (simp add: ring_simps)
    26.9    thus "\<exists>(n::nat). x < real n" ..
   26.10  qed
   26.11  
   26.12 @@ -392,9 +392,9 @@
   26.13    hence "y * inverse x * x < real n * x"
   26.14      using x_greater_zero by (simp add: mult_strict_right_mono)
   26.15    hence "x * inverse x * y < x * real n"
   26.16 -    by (simp add: ring_eq_simps)
   26.17 +    by (simp add: ring_simps)
   26.18    hence "y < real (n::nat) * x"
   26.19 -    using x_not_zero by (simp add: ring_eq_simps)
   26.20 +    using x_not_zero by (simp add: ring_simps)
   26.21    thus "\<exists>(n::nat). y < real n * x" ..
   26.22  qed
   26.23  
   26.24 @@ -1226,7 +1226,7 @@
   26.25      by simp
   26.26    also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
   26.27      real y + (x - real(natfloor x)) / real y"
   26.28 -    by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib
   26.29 +    by (auto simp add: ring_simps add_divide_distrib
   26.30        diff_divide_distrib prems)
   26.31    finally have "natfloor (x / real y) = natfloor(...)" by simp
   26.32    also have "... = natfloor(real((natfloor x) mod y) /
    27.1 --- a/src/HOL/Real/RealDef.thy	Fri Jun 22 22:41:17 2007 +0200
    27.2 +++ b/src/HOL/Real/RealDef.thy	Sat Jun 23 19:33:22 2007 +0200
    27.3 @@ -253,8 +253,7 @@
    27.4  apply (rule_tac [2]
    27.5          x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
    27.6         in exI)
    27.7 -apply (auto simp add: real_mult ring_distrib
    27.8 -              preal_mult_inverse_right add_ac mult_ac)
    27.9 +apply (auto simp add: real_mult preal_mult_inverse_right ring_simps)
   27.10  done
   27.11  
   27.12  lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
   27.13 @@ -632,7 +631,7 @@
   27.14    then have "real x / real d = ... / real d"
   27.15      by simp
   27.16    then show ?thesis
   27.17 -    by (auto simp add: add_divide_distrib ring_eq_simps prems)
   27.18 +    by (auto simp add: add_divide_distrib ring_simps prems)
   27.19  qed
   27.20  
   27.21  lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   27.22 @@ -776,7 +775,7 @@
   27.23    then have "real x / real d = \<dots> / real d"
   27.24      by simp
   27.25    then show ?thesis
   27.26 -    by (auto simp add: add_divide_distrib ring_eq_simps prems)
   27.27 +    by (auto simp add: add_divide_distrib ring_simps prems)
   27.28  qed
   27.29  
   27.30  lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
    28.1 --- a/src/HOL/Real/RealPow.thy	Fri Jun 22 22:41:17 2007 +0200
    28.2 +++ b/src/HOL/Real/RealPow.thy	Sat Jun 23 19:33:22 2007 +0200
    28.3 @@ -57,7 +57,7 @@
    28.4  lemma realpow_two_diff:
    28.5       "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
    28.6  apply (unfold real_diff_def)
    28.7 -apply (simp add: right_distrib left_distrib mult_ac)
    28.8 +apply (simp add: ring_simps)
    28.9  done
   28.10  
   28.11  lemma realpow_two_disj:
    29.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jun 22 22:41:17 2007 +0200
    29.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jun 23 19:33:22 2007 +0200
    29.3 @@ -1,6 +1,6 @@
    29.4  (*  Title:   HOL/Ring_and_Field.thy
    29.5      ID:      $Id$
    29.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
    29.7 +    Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
    29.8               with contributions by Jeremy Avigad
    29.9  *)
   29.10  
   29.11 @@ -173,8 +173,6 @@
   29.12  
   29.13  subsection {* Distribution rules *}
   29.14  
   29.15 -theorems ring_distrib = right_distrib left_distrib
   29.16 -
   29.17  text{*For the @{text combine_numerals} simproc*}
   29.18  lemma combine_common_factor:
   29.19       "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
   29.20 @@ -204,6 +202,15 @@
   29.21  by (simp add: left_distrib diff_minus 
   29.22                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   29.23  
   29.24 +lemmas ring_distribs =
   29.25 +  right_distrib left_distrib left_diff_distrib right_diff_distrib
   29.26 +
   29.27 +text{*This list of rewrites simplifies ring terms by multiplying
   29.28 +everything out and bringing sums and products into a canonical form
   29.29 +(by ordered rewriting). As a result it decides ring equalities but
   29.30 +also helps with inequalities. *}
   29.31 +lemmas ring_simps = group_simps ring_distribs
   29.32 +
   29.33  class mult_mono = times + zero + ord +
   29.34    assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
   29.35    assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
   29.36 @@ -308,81 +315,68 @@
   29.37   linorder_neqE[where 'a = "?'b::ordered_idom"]
   29.38  
   29.39  lemma eq_add_iff1:
   29.40 -     "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   29.41 -apply (simp add: diff_minus left_distrib)
   29.42 -apply (simp add: diff_minus left_distrib add_ac)
   29.43 -apply (simp add: compare_rls minus_mult_left [symmetric])
   29.44 -done
   29.45 +  "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   29.46 +by (simp add: ring_simps)
   29.47  
   29.48  lemma eq_add_iff2:
   29.49 -     "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
   29.50 -apply (simp add: diff_minus left_distrib add_ac)
   29.51 -apply (simp add: compare_rls minus_mult_left [symmetric]) 
   29.52 -done
   29.53 +  "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
   29.54 +by (simp add: ring_simps)
   29.55  
   29.56  lemma less_add_iff1:
   29.57 -     "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
   29.58 -apply (simp add: diff_minus left_distrib add_ac)
   29.59 -apply (simp add: compare_rls minus_mult_left [symmetric]) 
   29.60 -done
   29.61 +  "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
   29.62 +by (simp add: ring_simps)
   29.63  
   29.64  lemma less_add_iff2:
   29.65 -     "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
   29.66 -apply (simp add: diff_minus left_distrib add_ac)
   29.67 -apply (simp add: compare_rls minus_mult_left [symmetric]) 
   29.68 -done
   29.69 +  "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
   29.70 +by (simp add: ring_simps)
   29.71  
   29.72  lemma le_add_iff1:
   29.73 -     "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
   29.74 -apply (simp add: diff_minus left_distrib add_ac)
   29.75 -apply (simp add: compare_rls minus_mult_left [symmetric]) 
   29.76 -done
   29.77 +  "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
   29.78 +by (simp add: ring_simps)
   29.79  
   29.80  lemma le_add_iff2:
   29.81 -     "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
   29.82 -apply (simp add: diff_minus left_distrib add_ac)
   29.83 -apply (simp add: compare_rls minus_mult_left [symmetric]) 
   29.84 -done
   29.85 +  "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
   29.86 +by (simp add: ring_simps)
   29.87  
   29.88  
   29.89  subsection {* Ordering Rules for Multiplication *}
   29.90  
   29.91  lemma mult_left_le_imp_le:
   29.92 -     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
   29.93 -  by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   29.94 +  "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
   29.95 +by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   29.96   
   29.97  lemma mult_right_le_imp_le:
   29.98 -     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
   29.99 -  by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
  29.100 +  "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
  29.101 +by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
  29.102  
  29.103  lemma mult_left_less_imp_less:
  29.104 -     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
  29.105 -  by (force simp add: mult_left_mono linorder_not_le [symmetric])
  29.106 +  "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
  29.107 +by (force simp add: mult_left_mono linorder_not_le [symmetric])
  29.108   
  29.109  lemma mult_right_less_imp_less:
  29.110 -     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
  29.111 -  by (force simp add: mult_right_mono linorder_not_le [symmetric])
  29.112 +  "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"
  29.113 +by (force simp add: mult_right_mono linorder_not_le [symmetric])
  29.114  
  29.115  lemma mult_strict_left_mono_neg:
  29.116 -     "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
  29.117 +  "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
  29.118  apply (drule mult_strict_left_mono [of _ _ "-c"])
  29.119  apply (simp_all add: minus_mult_left [symmetric]) 
  29.120  done
  29.121  
  29.122  lemma mult_left_mono_neg:
  29.123 -     "[|b \<le> a; c \<le> 0|] ==> c * a \<le>  c * (b::'a::pordered_ring)"
  29.124 +  "[|b \<le> a; c \<le> 0|] ==> c * a \<le>  c * (b::'a::pordered_ring)"
  29.125  apply (drule mult_left_mono [of _ _ "-c"])
  29.126  apply (simp_all add: minus_mult_left [symmetric]) 
  29.127  done
  29.128  
  29.129  lemma mult_strict_right_mono_neg:
  29.130 -     "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
  29.131 +  "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
  29.132  apply (drule mult_strict_right_mono [of _ _ "-c"])
  29.133  apply (simp_all add: minus_mult_right [symmetric]) 
  29.134  done
  29.135  
  29.136  lemma mult_right_mono_neg:
  29.137 -     "[|b \<le> a; c \<le> 0|] ==> a * c \<le>  (b::'a::pordered_ring) * c"
  29.138 +  "[|b \<le> a; c \<le> 0|] ==> a * c \<le>  (b::'a::pordered_ring) * c"
  29.139  apply (drule mult_right_mono [of _ _ "-c"])
  29.140  apply (simp)
  29.141  apply (simp_all add: minus_mult_right [symmetric]) 
  29.142 @@ -648,7 +642,7 @@
  29.143    shows "(a * c = b * c) = (c = 0 \<or> a = b)"
  29.144  proof -
  29.145    have "(a * c = b * c) = ((a - b) * c = 0)"
  29.146 -    by (simp add: left_diff_distrib)
  29.147 +    by (simp add: ring_distribs)
  29.148    thus ?thesis
  29.149      by (simp add: disj_commute)
  29.150  qed
  29.151 @@ -658,7 +652,7 @@
  29.152    shows "(c * a = c * b) = (c = 0 \<or> a = b)"
  29.153  proof -
  29.154    have "(c * a = c * b) = (c * (a - b) = 0)"
  29.155 -    by (simp add: right_diff_distrib)
  29.156 +    by (simp add: ring_distribs)
  29.157    thus ?thesis
  29.158      by simp
  29.159  qed
  29.160 @@ -742,16 +736,6 @@
  29.161      mult_cancel_left1 mult_cancel_left2
  29.162  
  29.163  
  29.164 -text{*This list of rewrites decides ring equalities by ordered rewriting.*}
  29.165 -lemmas ring_eq_simps =  
  29.166 -(*  mult_ac*)
  29.167 -  left_distrib right_distrib left_diff_distrib right_diff_distrib
  29.168 -  group_eq_simps
  29.169 -(*  add_ac
  29.170 -  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
  29.171 -  diff_eq_eq eq_diff_eq *)
  29.172 -    
  29.173 -
  29.174  subsection {* Fields *}
  29.175  
  29.176  lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
  29.177 @@ -787,7 +771,7 @@
  29.178  by (simp add: divide_inverse)
  29.179  
  29.180  lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
  29.181 -by (simp add: divide_inverse left_distrib) 
  29.182 +by (simp add: divide_inverse ring_distribs) 
  29.183  
  29.184  
  29.185  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
  29.186 @@ -957,22 +941,22 @@
  29.187  lemma division_ring_inverse_add:
  29.188    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
  29.189     ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
  29.190 -  by (simp add: right_distrib left_distrib mult_assoc)
  29.191 +by (simp add: ring_simps)
  29.192  
  29.193  lemma division_ring_inverse_diff:
  29.194    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
  29.195     ==> inverse a - inverse b = inverse a * (b-a) * inverse b"
  29.196 -by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
  29.197 +by (simp add: ring_simps)
  29.198  
  29.199  text{*There is no slick version using division by zero.*}
  29.200  lemma inverse_add:
  29.201 -     "[|a \<noteq> 0;  b \<noteq> 0|]
  29.202 -      ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
  29.203 +  "[|a \<noteq> 0;  b \<noteq> 0|]
  29.204 +   ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
  29.205  by (simp add: division_ring_inverse_add mult_ac)
  29.206  
  29.207  lemma inverse_divide [simp]:
  29.208 -      "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  29.209 -  by (simp add: divide_inverse mult_commute)
  29.210 +  "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  29.211 +by (simp add: divide_inverse mult_commute)
  29.212  
  29.213  
  29.214  subsection {* Calculations with fractions *}
  29.215 @@ -982,8 +966,7 @@
  29.216  because the latter are covered by a simproc. *}
  29.217  
  29.218  lemma nonzero_mult_divide_mult_cancel_left[simp]:
  29.219 -  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
  29.220 -    shows "(c*a)/(c*b) = a/(b::'a::field)"
  29.221 +assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
  29.222  proof -
  29.223    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
  29.224      by (simp add: field_mult_eq_0_iff divide_inverse 
  29.225 @@ -997,23 +980,23 @@
  29.226  qed
  29.227  
  29.228  lemma mult_divide_mult_cancel_left:
  29.229 -     "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  29.230 +  "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  29.231  apply (cases "b = 0")
  29.232  apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  29.233  done
  29.234  
  29.235  lemma nonzero_mult_divide_mult_cancel_right:
  29.236 -     "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
  29.237 +  "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
  29.238  by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
  29.239  
  29.240  lemma mult_divide_mult_cancel_right:
  29.241 -     "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  29.242 +  "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  29.243  apply (cases "b = 0")
  29.244  apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  29.245  done
  29.246  
  29.247  lemma divide_1 [simp]: "a/1 = (a::'a::field)"
  29.248 -  by (simp add: divide_inverse)
  29.249 +by (simp add: divide_inverse)
  29.250  
  29.251  lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
  29.252  by (simp add: divide_inverse mult_assoc)
  29.253 @@ -1022,33 +1005,33 @@
  29.254  by (simp add: divide_inverse mult_ac)
  29.255  
  29.256  lemma divide_divide_eq_right [simp]:
  29.257 -     "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  29.258 +  "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  29.259  by (simp add: divide_inverse mult_ac)
  29.260  
  29.261  lemma divide_divide_eq_left [simp]:
  29.262 -     "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  29.263 +  "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  29.264  by (simp add: divide_inverse mult_assoc)
  29.265  
  29.266  lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  29.267      x / y + w / z = (x * z + w * y) / (y * z)"
  29.268 -  apply (subgoal_tac "x / y = (x * z) / (y * z)")
  29.269 -  apply (erule ssubst)
  29.270 -  apply (subgoal_tac "w / z = (w * y) / (y * z)")
  29.271 -  apply (erule ssubst)
  29.272 -  apply (rule add_divide_distrib [THEN sym])
  29.273 -  apply (subst mult_commute)
  29.274 -  apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
  29.275 -  apply assumption
  29.276 -  apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
  29.277 -  apply assumption
  29.278 +apply (subgoal_tac "x / y = (x * z) / (y * z)")
  29.279 +apply (erule ssubst)
  29.280 +apply (subgoal_tac "w / z = (w * y) / (y * z)")
  29.281 +apply (erule ssubst)
  29.282 +apply (rule add_divide_distrib [THEN sym])
  29.283 +apply (subst mult_commute)
  29.284 +apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
  29.285 +apply assumption
  29.286 +apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
  29.287 +apply assumption
  29.288  done
  29.289  
  29.290  
  29.291  subsubsection{*Special Cancellation Simprules for Division*}
  29.292  
  29.293  lemma mult_divide_mult_cancel_left_if[simp]:
  29.294 -  fixes c :: "'a :: {field,division_by_zero}"
  29.295 -  shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  29.296 +fixes c :: "'a :: {field,division_by_zero}"
  29.297 +shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  29.298  by (simp add: mult_divide_mult_cancel_left)
  29.299  
  29.300  lemma nonzero_mult_divide_cancel_right[simp]:
  29.301 @@ -1070,62 +1053,14 @@
  29.302  
  29.303  
  29.304  lemma nonzero_mult_divide_mult_cancel_left2[simp]:
  29.305 -     "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
  29.306 +  "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
  29.307  using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
  29.308  
  29.309  lemma nonzero_mult_divide_mult_cancel_right2[simp]:
  29.310 -     "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
  29.311 +  "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
  29.312  using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
  29.313  
  29.314  
  29.315 -(* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
  29.316 -lemma mult_divide_cancel_right_if:
  29.317 -  fixes c :: "'a :: {field,division_by_zero}"
  29.318 -  shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
  29.319 -by (simp add: mult_divide_cancel_right)
  29.320 -
  29.321 -lemma mult_divide_cancel_left_if1 [simp]:
  29.322 -  fixes c :: "'a :: {field,division_by_zero}"
  29.323 -  shows "c / (c*b) = (if c=0 then 0 else 1/b)"
  29.324 -apply (insert mult_divide_cancel_left_if [of c 1 b]) 
  29.325 -apply (simp del: mult_divide_cancel_left_if)
  29.326 -done
  29.327 -
  29.328 -lemma mult_divide_cancel_left_if2 [simp]:
  29.329 -  fixes c :: "'a :: {field,division_by_zero}"
  29.330 -  shows "(c*a) / c = (if c=0 then 0 else a)" 
  29.331 -apply (insert mult_divide_cancel_left_if [of c a 1]) 
  29.332 -apply (simp del: mult_divide_cancel_left_if)
  29.333 -done
  29.334 -
  29.335 -lemma mult_divide_cancel_right_if1 [simp]:
  29.336 -  fixes c :: "'a :: {field,division_by_zero}"
  29.337 -  shows "c / (b*c) = (if c=0 then 0 else 1/b)"
  29.338 -apply (insert mult_divide_cancel_right_if [of 1 c b]) 
  29.339 -apply (simp del: mult_divide_cancel_right_if)
  29.340 -done
  29.341 -
  29.342 -lemma mult_divide_cancel_right_if2 [simp]:
  29.343 -  fixes c :: "'a :: {field,division_by_zero}"
  29.344 -  shows "(a*c) / c = (if c=0 then 0 else a)" 
  29.345 -apply (insert mult_divide_cancel_right_if [of a c 1]) 
  29.346 -apply (simp del: mult_divide_cancel_right_if)
  29.347 -done
  29.348 -
  29.349 -text{*Two lemmas for cancelling the denominator*}
  29.350 -
  29.351 -lemma times_divide_self_right [simp]: 
  29.352 -  fixes a :: "'a :: {field,division_by_zero}"
  29.353 -  shows "a * (b/a) = (if a=0 then 0 else b)"
  29.354 -by (simp add: times_divide_eq_right)
  29.355 -
  29.356 -lemma times_divide_self_left [simp]: 
  29.357 -  fixes a :: "'a :: {field,division_by_zero}"
  29.358 -  shows "(b/a) * a = (if a=0 then 0 else b)"
  29.359 -by (simp add: times_divide_eq_left)
  29.360 -*)
  29.361 -
  29.362 -
  29.363  subsection {* Division and Unary Minus *}
  29.364  
  29.365  lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
  29.366 @@ -1155,7 +1090,7 @@
  29.367  declare mult_minus_left [simp]   mult_minus_right [simp]
  29.368  
  29.369  lemma minus_divide_divide [simp]:
  29.370 -     "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  29.371 +  "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  29.372  apply (cases "b=0", simp) 
  29.373  apply (simp add: nonzero_minus_divide_divide) 
  29.374  done
  29.375 @@ -1165,10 +1100,10 @@
  29.376  
  29.377  lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  29.378      x / y - w / z = (x * z - w * y) / (y * z)"
  29.379 -  apply (subst diff_def)+
  29.380 -  apply (subst minus_divide_left)
  29.381 -  apply (subst add_frac_eq)
  29.382 -  apply simp_all
  29.383 +apply (subst diff_def)+
  29.384 +apply (subst minus_divide_left)
  29.385 +apply (subst add_frac_eq)
  29.386 +apply simp_all
  29.387  done
  29.388  
  29.389  
  29.390 @@ -1897,10 +1832,10 @@
  29.391    by (blast intro: order_less_trans zero_less_one less_add_one) 
  29.392  
  29.393  lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  29.394 -by (simp add: zero_less_two pos_less_divide_eq right_distrib) 
  29.395 +by (simp add: zero_less_two pos_less_divide_eq ring_distribs) 
  29.396  
  29.397  lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  29.398 -by (simp add: zero_less_two pos_divide_less_eq right_distrib) 
  29.399 +by (simp add: zero_less_two pos_divide_less_eq ring_distribs) 
  29.400  
  29.401  lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
  29.402  by (blast intro!: less_half_sum gt_half_sum)
  29.403 @@ -1909,21 +1844,21 @@
  29.404  subsection {* Absolute Value *}
  29.405  
  29.406  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  29.407 -  by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) 
  29.408 +by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  29.409  
  29.410  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  29.411  proof -
  29.412    let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  29.413    let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  29.414    have a: "(abs a) * (abs b) = ?x"
  29.415 -    by (simp only: abs_prts[of a] abs_prts[of b] ring_eq_simps)
  29.416 +    by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)
  29.417    {
  29.418      fix u v :: 'a
  29.419      have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  29.420                u * v = pprt a * pprt b + pprt a * nprt b + 
  29.421                        nprt a * pprt b + nprt a * nprt b"
  29.422        apply (subst prts[of u], subst prts[of v])
  29.423 -      apply (simp add: left_distrib right_distrib add_ac) 
  29.424 +      apply (simp add: ring_simps) 
  29.425        done
  29.426    }
  29.427    note b = this[OF refl[of a] refl[of b]]
  29.428 @@ -1974,7 +1909,7 @@
  29.429        apply (simp_all add: mulprts abs_prts)
  29.430        apply (insert prems)
  29.431        apply (auto simp add: 
  29.432 -	ring_eq_simps 
  29.433 +	ring_simps 
  29.434  	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
  29.435  	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
  29.436  	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  29.437 @@ -1986,7 +1921,7 @@
  29.438      then show ?thesis
  29.439        apply (simp_all add: mulprts abs_prts)
  29.440        apply (insert prems)
  29.441 -      apply (auto simp add: ring_eq_simps)
  29.442 +      apply (auto simp add: ring_simps)
  29.443        apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  29.444        apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  29.445        done
  29.446 @@ -2073,7 +2008,7 @@
  29.447      apply simp
  29.448      done
  29.449    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  29.450 -    by (simp add: ring_eq_simps)
  29.451 +    by (simp add: ring_simps)
  29.452    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  29.453      by (simp_all add: prems mult_mono)
  29.454    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
    30.1 --- a/src/HOL/SetInterval.thy	Fri Jun 22 22:41:17 2007 +0200
    30.2 +++ b/src/HOL/SetInterval.thy	Sat Jun 23 19:33:22 2007 +0200
    30.3 @@ -756,7 +756,7 @@
    30.4    show ?case by simp
    30.5  next
    30.6    case (Suc n)
    30.7 -  then show ?case by (simp add: ring_eq_simps)
    30.8 +  then show ?case by (simp add: ring_simps)
    30.9  qed
   30.10  
   30.11  theorem arith_series_general:
    31.1 --- a/src/HOL/ZF/LProd.thy	Fri Jun 22 22:41:17 2007 +0200
    31.2 +++ b/src/HOL/ZF/LProd.thy	Sat Jun 23 19:33:22 2007 +0200
    31.3 @@ -45,9 +45,9 @@
    31.4    case (lprod_list ah at bh bt a b) 
    31.5    from prems have transR: "transP R" by auto
    31.6    have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
    31.7 -    by (simp add: ring_eq_simps)
    31.8 +    by (simp add: ring_simps)
    31.9    have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
   31.10 -    by (simp add: ring_eq_simps)
   31.11 +    by (simp add: ring_simps)
   31.12    from prems have "mult R ?ma ?mb"
   31.13      by auto
   31.14    with mult_implies_one_step[OF transR] have 
   31.15 @@ -66,7 +66,7 @@
   31.16      then show ?thesis
   31.17        apply (simp only: as bs)
   31.18        apply (simp only: decomposed True)
   31.19 -      apply (simp add: ring_eq_simps)
   31.20 +      apply (simp add: ring_simps)
   31.21        done
   31.22    next
   31.23      case False
   31.24 @@ -78,7 +78,7 @@
   31.25      then show ?thesis
   31.26        apply (simp only: as bs)
   31.27        apply (simp only: decomposed)
   31.28 -      apply (simp add: ring_eq_simps)
   31.29 +      apply (simp add: ring_simps)
   31.30        done
   31.31    qed
   31.32  qed
    32.1 --- a/src/HOL/ex/Adder.thy	Fri Jun 22 22:41:17 2007 +0200
    32.2 +++ b/src/HOL/ex/Adder.thy	Sat Jun 23 19:33:22 2007 +0200
    32.3 @@ -64,7 +64,7 @@
    32.4    apply (induct as)
    32.5     apply (cases c, simp_all add: Let_def bv_to_nat_dist_append)
    32.6    apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull]
    32.7 -    ring_distrib bv_to_nat_helper)
    32.8 +    ring_distribs bv_to_nat_helper)
    32.9    done
   32.10  
   32.11  consts
   32.12 @@ -107,7 +107,7 @@
   32.13        apply (simp add: Let_def)
   32.14        apply (subst bv_to_nat_dist_append)
   32.15        apply (simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull]
   32.16 -        ring_distrib bv_to_nat_helper cca_length)
   32.17 +        ring_distribs bv_to_nat_helper cca_length)
   32.18        done
   32.19    qed
   32.20  qed
    33.1 --- a/src/HOL/ex/Lagrange.thy	Fri Jun 22 22:41:17 2007 +0200
    33.2 +++ b/src/HOL/ex/Lagrange.thy	Sat Jun 23 19:33:22 2007 +0200
    33.3 @@ -16,37 +16,31 @@
    33.4  The enterprising reader might consider proving all of Lagrange's
    33.5  theorem.  *}
    33.6  
    33.7 -definition
    33.8 -  sq :: "'a::times => 'a" where
    33.9 -  "sq x == x*x"
   33.10 +definition sq :: "'a::times => 'a" where "sq x == x*x"
   33.11  
   33.12  text {* The following lemma essentially shows that every natural
   33.13  number is the sum of four squares, provided all prime numbers are.
   33.14  However, this is an abstract theorem about commutative rings.  It has,
   33.15  a priori, nothing to do with nat. *}
   33.16  
   33.17 +(* These two simprocs are even less efficient than ordered rewriting
   33.18 +   and kill the second example: *)
   33.19  ML_setup {*
   33.20    Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   33.21  *}
   33.22  
   33.23 -lemma Lagrange_lemma:
   33.24 -  fixes x1 :: "'a::comm_ring"
   33.25 -  shows
   33.26 +lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
   33.27    "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
   33.28 -    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
   33.29 -    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
   33.30 -    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
   33.31 -    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
   33.32 -  by (simp add: sq_def ring_eq_simps)
   33.33 +   sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
   33.34 +   sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
   33.35 +   sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
   33.36 +   sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
   33.37 +by (simp add: sq_def ring_simps)
   33.38  
   33.39  
   33.40 -text {*
   33.41 -  A challenge by John Harrison. Takes about 17s on a 1.6GHz machine.
   33.42 -*}
   33.43 +text {* A challenge by John Harrison. Takes about 17s on a 1.6GHz machine. *}
   33.44  
   33.45 -lemma
   33.46 -  fixes p1 :: "'a::comm_ring"
   33.47 -  shows
   33.48 +lemma fixes p1 :: "'a::comm_ring" shows
   33.49    "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
   33.50     (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
   33.51      = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
   33.52 @@ -57,6 +51,6 @@
   33.53        sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
   33.54        sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
   33.55        sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
   33.56 -  by (simp add: sq_def ring_eq_simps)
   33.57 +by (simp add: sq_def ring_simps)
   33.58  
   33.59  end
    34.1 --- a/src/HOL/ex/NatSum.thy	Fri Jun 22 22:41:17 2007 +0200
    34.2 +++ b/src/HOL/ex/NatSum.thy	Sat Jun 23 19:33:22 2007 +0200
    34.3 @@ -15,8 +15,7 @@
    34.4  *}
    34.5  
    34.6  lemmas [simp] =
    34.7 -  left_distrib right_distrib
    34.8 -  left_diff_distrib right_diff_distrib --{*for true subtraction*}
    34.9 +  ring_distribs
   34.10    diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
   34.11  
   34.12  text {*
    35.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jun 22 22:41:17 2007 +0200
    35.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sat Jun 23 19:33:22 2007 +0200
    35.3 @@ -1,7 +1,7 @@
    35.4  theory Reflected_Presburger
    35.5 -  imports GCD Main EfficientNat
    35.6 -  uses ("coopereif.ML") ("coopertac.ML")
    35.7 -  begin
    35.8 +imports GCD Main EfficientNat
    35.9 +uses ("coopereif.ML") ("coopertac.ML")
   35.10 +begin
   35.11  
   35.12  lemma allpairs_set: "set (allpairs Pair xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
   35.13  by (induct xs) auto
   35.14 @@ -463,8 +463,10 @@
   35.15  lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   35.16  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   35.17  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   35.18 -by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
   35.19 -(simp add: ring_eq_simps(1)[symmetric]) 
   35.20 + apply (case_tac "n1 = n2")
   35.21 +  apply(simp_all add: ring_simps)
   35.22 +apply(simp add: left_distrib[symmetric])
   35.23 +done
   35.24  
   35.25  lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   35.26  by (induct t s rule: numadd.induct, auto simp add: Let_def)
   35.27 @@ -476,7 +478,7 @@
   35.28    "nummul t = (\<lambda> i. Mul i t)"
   35.29  
   35.30  lemma nummul: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
   35.31 -by (induct t rule: nummul.induct, auto simp add: ring_eq_simps numadd)
   35.32 +by (induct t rule: nummul.induct, auto simp add: ring_simps numadd)
   35.33  
   35.34  lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
   35.35  by (induct t rule: nummul.induct, auto simp add: numadd_nb)
   35.36 @@ -907,7 +909,7 @@
   35.37    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.38    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.39    from prems Ia nb  show ?case 
   35.40 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.41 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.42  next
   35.43    case (6 a)  
   35.44    let ?c = "fst (zsplit0 a)"
   35.45 @@ -917,7 +919,7 @@
   35.46    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.47    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.48    from prems Ia nb  show ?case 
   35.49 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.50 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.51  next
   35.52    case (7 a)  
   35.53    let ?c = "fst (zsplit0 a)"
   35.54 @@ -927,7 +929,7 @@
   35.55    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.56    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.57    from prems Ia nb  show ?case 
   35.58 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.59 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.60  next
   35.61    case (8 a)  
   35.62    let ?c = "fst (zsplit0 a)"
   35.63 @@ -937,7 +939,7 @@
   35.64    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.65    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.66    from prems Ia nb  show ?case 
   35.67 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.68 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.69  next
   35.70    case (9 a)  
   35.71    let ?c = "fst (zsplit0 a)"
   35.72 @@ -947,7 +949,7 @@
   35.73    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.74    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.75    from prems Ia nb  show ?case 
   35.76 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.77 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.78  next
   35.79    case (10 a)  
   35.80    let ?c = "fst (zsplit0 a)"
   35.81 @@ -957,7 +959,7 @@
   35.82    have Ia:"Inum (i # bs) a = Inum (i #bs) (CX ?c ?r)" and nb: "numbound0 ?r" by auto 
   35.83    let ?N = "\<lambda> t. Inum (i#bs) t"
   35.84    from prems Ia nb  show ?case 
   35.85 -    by (auto simp add: Let_def split_def ring_eq_simps) (cases "?r",auto)
   35.86 +    by (auto simp add: Let_def split_def ring_simps) (cases "?r",auto)
   35.87  next
   35.88    case (11 j a)  
   35.89    let ?c = "fst (zsplit0 a)"
   35.90 @@ -1264,9 +1266,9 @@
   35.91        (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
   35.92        hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
   35.93        hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
   35.94 -	by (simp add: ring_eq_simps di_def)
   35.95 +	by (simp add: ring_simps di_def)
   35.96        hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
   35.97 -	by (simp add: ring_eq_simps)
   35.98 +	by (simp add: ring_simps)
   35.99        hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  35.100        thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  35.101      next
  35.102 @@ -1275,7 +1277,7 @@
  35.103        hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  35.104        hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  35.105        hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  35.106 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_eq_simps)
  35.107 +      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
  35.108        hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  35.109  	by blast
  35.110        thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  35.111 @@ -1291,9 +1293,9 @@
  35.112        (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
  35.113        hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
  35.114        hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
  35.115 -	by (simp add: ring_eq_simps di_def)
  35.116 +	by (simp add: ring_simps di_def)
  35.117        hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
  35.118 -	by (simp add: ring_eq_simps)
  35.119 +	by (simp add: ring_simps)
  35.120        hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  35.121        thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  35.122      next
  35.123 @@ -1302,7 +1304,7 @@
  35.124        hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  35.125        hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  35.126        hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  35.127 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_eq_simps)
  35.128 +      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: ring_simps)
  35.129        hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  35.130  	by blast
  35.131        thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  35.132 @@ -1355,7 +1357,7 @@
  35.133      by (simp only: zdvd_zminus_iff)
  35.134    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  35.135      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
  35.136 -    by (simp add: ring_eq_simps)
  35.137 +    by (simp add: ring_simps)
  35.138    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
  35.139      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  35.140      by simp
  35.141 @@ -1367,7 +1369,7 @@
  35.142      by (simp only: zdvd_zminus_iff)
  35.143    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  35.144      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
  35.145 -    by (simp add: ring_eq_simps)
  35.146 +    by (simp add: ring_simps)
  35.147    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CX c e))"
  35.148      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  35.149      by simp
  35.150 @@ -1439,7 +1441,7 @@
  35.151      hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
  35.152            ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
  35.153        by simp
  35.154 -    also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_eq_simps)
  35.155 +    also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: ring_simps)
  35.156      also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
  35.157      using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  35.158    finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be  by simp
  35.159 @@ -1457,7 +1459,7 @@
  35.160      hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
  35.161            ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
  35.162        by simp
  35.163 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_eq_simps)
  35.164 +    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: ring_simps)
  35.165      also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
  35.166      using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  35.167    finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  be by simp
  35.168 @@ -1475,7 +1477,7 @@
  35.169      hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
  35.170            ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
  35.171        by simp
  35.172 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_eq_simps)
  35.173 +    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: ring_simps)
  35.174      also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
  35.175      using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  35.176    finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  35.177 @@ -1494,7 +1496,7 @@
  35.178            ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
  35.179        by simp
  35.180      also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" 
  35.181 -      by (simp add: ring_eq_simps)
  35.182 +      by (simp add: ring_simps)
  35.183      also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" using ldcp 
  35.184        zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
  35.185    finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  
  35.186 @@ -1513,7 +1515,7 @@
  35.187      hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
  35.188            ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
  35.189        by simp
  35.190 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_eq_simps)
  35.191 +    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: ring_simps)
  35.192      also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
  35.193      using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  35.194    finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  35.195 @@ -1531,7 +1533,7 @@
  35.196      hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
  35.197            ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
  35.198        by simp
  35.199 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_eq_simps)
  35.200 +    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: ring_simps)
  35.201      also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
  35.202      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  35.203    finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  35.204 @@ -1547,7 +1549,7 @@
  35.205      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  35.206        by simp
  35.207      hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
  35.208 -    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_eq_simps)
  35.209 +    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
  35.210      also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  35.211      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  35.212    also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  35.213 @@ -1564,7 +1566,7 @@
  35.214      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  35.215        by simp
  35.216      hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
  35.217 -    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_eq_simps)
  35.218 +    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: ring_simps)
  35.219      also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  35.220      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  35.221    also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  35.222 @@ -1613,7 +1615,7 @@
  35.223        hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
  35.224        hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
  35.225        hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
  35.226 -	by (simp add: ring_eq_simps)
  35.227 +	by (simp add: ring_simps)
  35.228        with nob have ?case by auto}
  35.229      ultimately show ?case by blast
  35.230  next
  35.231 @@ -1632,7 +1634,7 @@
  35.232        from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
  35.233        hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
  35.234        hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
  35.235 -      hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_eq_simps)
  35.236 +      hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: ring_simps)
  35.237        with nob have ?case by simp }
  35.238      ultimately show ?case by blast
  35.239  next
  35.240 @@ -1642,7 +1644,7 @@
  35.241      have vb: "?v \<in> set (\<beta> (Eq (CX c e)))" by simp
  35.242      from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp
  35.243        by simp (erule ballE[where x="1"],
  35.244 -	simp_all add:ring_eq_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
  35.245 +	simp_all add:ring_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
  35.246  next
  35.247    case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CX c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
  35.248      let ?e = "Inum (x # bs) e"
    36.1 --- a/src/HOL/ex/ReflectionEx.thy	Fri Jun 22 22:41:17 2007 +0200
    36.2 +++ b/src/HOL/ex/ReflectionEx.thy	Sat Jun 23 19:33:22 2007 +0200
    36.3 @@ -164,7 +164,7 @@
    36.4  lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)"
    36.5  apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
    36.6  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
    36.7 -by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
    36.8 +by (case_tac "n1 = n2", simp_all add: ring_simps)
    36.9  
   36.10  consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   36.11  recdef lin_mul "measure size "
   36.12 @@ -173,7 +173,7 @@
   36.13    "lin_mul t = (\<lambda> i. Mul i t)"
   36.14  
   36.15  lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
   36.16 -by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
   36.17 +by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_simps)
   36.18  
   36.19  consts linum:: "num \<Rightarrow> num"
   36.20  recdef linum "measure num_size"