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"