1.1 --- a/src/HOL/Ring_and_Field.thy Mon Feb 08 15:49:01 2010 -0800
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,2391 +0,0 @@
1.4 -(* Title: HOL/Ring_and_Field.thy
1.5 - Author: Gertrud Bauer
1.6 - Author: Steven Obua
1.7 - Author: Tobias Nipkow
1.8 - Author: Lawrence C Paulson
1.9 - Author: Markus Wenzel
1.10 - Author: Jeremy Avigad
1.11 -*)
1.12 -
1.13 -header {* (Ordered) Rings and Fields *}
1.14 -
1.15 -theory Ring_and_Field
1.16 -imports OrderedGroup
1.17 -begin
1.18 -
1.19 -text {*
1.20 - The theory of partially ordered rings is taken from the books:
1.21 - \begin{itemize}
1.22 - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
1.23 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
1.24 - \end{itemize}
1.25 - Most of the used notions can also be looked up in
1.26 - \begin{itemize}
1.27 - \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
1.28 - \item \emph{Algebra I} by van der Waerden, Springer.
1.29 - \end{itemize}
1.30 -*}
1.31 -
1.32 -class semiring = ab_semigroup_add + semigroup_mult +
1.33 - assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"
1.34 - assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"
1.35 -begin
1.36 -
1.37 -text{*For the @{text combine_numerals} simproc*}
1.38 -lemma combine_common_factor:
1.39 - "a * e + (b * e + c) = (a + b) * e + c"
1.40 -by (simp add: left_distrib add_ac)
1.41 -
1.42 -end
1.43 -
1.44 -class mult_zero = times + zero +
1.45 - assumes mult_zero_left [simp]: "0 * a = 0"
1.46 - assumes mult_zero_right [simp]: "a * 0 = 0"
1.47 -
1.48 -class semiring_0 = semiring + comm_monoid_add + mult_zero
1.49 -
1.50 -class semiring_0_cancel = semiring + cancel_comm_monoid_add
1.51 -begin
1.52 -
1.53 -subclass semiring_0
1.54 -proof
1.55 - fix a :: 'a
1.56 - have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])
1.57 - thus "0 * a = 0" by (simp only: add_left_cancel)
1.58 -next
1.59 - fix a :: 'a
1.60 - have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])
1.61 - thus "a * 0 = 0" by (simp only: add_left_cancel)
1.62 -qed
1.63 -
1.64 -end
1.65 -
1.66 -class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
1.67 - assumes distrib: "(a + b) * c = a * c + b * c"
1.68 -begin
1.69 -
1.70 -subclass semiring
1.71 -proof
1.72 - fix a b c :: 'a
1.73 - show "(a + b) * c = a * c + b * c" by (simp add: distrib)
1.74 - have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
1.75 - also have "... = b * a + c * a" by (simp only: distrib)
1.76 - also have "... = a * b + a * c" by (simp add: mult_ac)
1.77 - finally show "a * (b + c) = a * b + a * c" by blast
1.78 -qed
1.79 -
1.80 -end
1.81 -
1.82 -class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
1.83 -begin
1.84 -
1.85 -subclass semiring_0 ..
1.86 -
1.87 -end
1.88 -
1.89 -class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
1.90 -begin
1.91 -
1.92 -subclass semiring_0_cancel ..
1.93 -
1.94 -subclass comm_semiring_0 ..
1.95 -
1.96 -end
1.97 -
1.98 -class zero_neq_one = zero + one +
1.99 - assumes zero_neq_one [simp]: "0 \<noteq> 1"
1.100 -begin
1.101 -
1.102 -lemma one_neq_zero [simp]: "1 \<noteq> 0"
1.103 -by (rule not_sym) (rule zero_neq_one)
1.104 -
1.105 -end
1.106 -
1.107 -class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
1.108 -
1.109 -text {* Abstract divisibility *}
1.110 -
1.111 -class dvd = times
1.112 -begin
1.113 -
1.114 -definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
1.115 - [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
1.116 -
1.117 -lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
1.118 - unfolding dvd_def ..
1.119 -
1.120 -lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
1.121 - unfolding dvd_def by blast
1.122 -
1.123 -end
1.124 -
1.125 -class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
1.126 - (*previously almost_semiring*)
1.127 -begin
1.128 -
1.129 -subclass semiring_1 ..
1.130 -
1.131 -lemma dvd_refl[simp]: "a dvd a"
1.132 -proof
1.133 - show "a = a * 1" by simp
1.134 -qed
1.135 -
1.136 -lemma dvd_trans:
1.137 - assumes "a dvd b" and "b dvd c"
1.138 - shows "a dvd c"
1.139 -proof -
1.140 - from assms obtain v where "b = a * v" by (auto elim!: dvdE)
1.141 - moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
1.142 - ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
1.143 - then show ?thesis ..
1.144 -qed
1.145 -
1.146 -lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
1.147 -by (auto intro: dvd_refl elim!: dvdE)
1.148 -
1.149 -lemma dvd_0_right [iff]: "a dvd 0"
1.150 -proof
1.151 - show "0 = a * 0" by simp
1.152 -qed
1.153 -
1.154 -lemma one_dvd [simp]: "1 dvd a"
1.155 -by (auto intro!: dvdI)
1.156 -
1.157 -lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
1.158 -by (auto intro!: mult_left_commute dvdI elim!: dvdE)
1.159 -
1.160 -lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
1.161 - apply (subst mult_commute)
1.162 - apply (erule dvd_mult)
1.163 - done
1.164 -
1.165 -lemma dvd_triv_right [simp]: "a dvd b * a"
1.166 -by (rule dvd_mult) (rule dvd_refl)
1.167 -
1.168 -lemma dvd_triv_left [simp]: "a dvd a * b"
1.169 -by (rule dvd_mult2) (rule dvd_refl)
1.170 -
1.171 -lemma mult_dvd_mono:
1.172 - assumes "a dvd b"
1.173 - and "c dvd d"
1.174 - shows "a * c dvd b * d"
1.175 -proof -
1.176 - from `a dvd b` obtain b' where "b = a * b'" ..
1.177 - moreover from `c dvd d` obtain d' where "d = c * d'" ..
1.178 - ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
1.179 - then show ?thesis ..
1.180 -qed
1.181 -
1.182 -lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
1.183 -by (simp add: dvd_def mult_assoc, blast)
1.184 -
1.185 -lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
1.186 - unfolding mult_ac [of a] by (rule dvd_mult_left)
1.187 -
1.188 -lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
1.189 -by simp
1.190 -
1.191 -lemma dvd_add[simp]:
1.192 - assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
1.193 -proof -
1.194 - from `a dvd b` obtain b' where "b = a * b'" ..
1.195 - moreover from `a dvd c` obtain c' where "c = a * c'" ..
1.196 - ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
1.197 - then show ?thesis ..
1.198 -qed
1.199 -
1.200 -end
1.201 -
1.202 -
1.203 -class no_zero_divisors = zero + times +
1.204 - assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
1.205 -
1.206 -class semiring_1_cancel = semiring + cancel_comm_monoid_add
1.207 - + zero_neq_one + monoid_mult
1.208 -begin
1.209 -
1.210 -subclass semiring_0_cancel ..
1.211 -
1.212 -subclass semiring_1 ..
1.213 -
1.214 -end
1.215 -
1.216 -class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
1.217 - + zero_neq_one + comm_monoid_mult
1.218 -begin
1.219 -
1.220 -subclass semiring_1_cancel ..
1.221 -subclass comm_semiring_0_cancel ..
1.222 -subclass comm_semiring_1 ..
1.223 -
1.224 -end
1.225 -
1.226 -class ring = semiring + ab_group_add
1.227 -begin
1.228 -
1.229 -subclass semiring_0_cancel ..
1.230 -
1.231 -text {* Distribution rules *}
1.232 -
1.233 -lemma minus_mult_left: "- (a * b) = - a * b"
1.234 -by (rule minus_unique) (simp add: left_distrib [symmetric])
1.235 -
1.236 -lemma minus_mult_right: "- (a * b) = a * - b"
1.237 -by (rule minus_unique) (simp add: right_distrib [symmetric])
1.238 -
1.239 -text{*Extract signs from products*}
1.240 -lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
1.241 -lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
1.242 -
1.243 -lemma minus_mult_minus [simp]: "- a * - b = a * b"
1.244 -by simp
1.245 -
1.246 -lemma minus_mult_commute: "- a * b = a * - b"
1.247 -by simp
1.248 -
1.249 -lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"
1.250 -by (simp add: right_distrib diff_minus)
1.251 -
1.252 -lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
1.253 -by (simp add: left_distrib diff_minus)
1.254 -
1.255 -lemmas ring_distribs[noatp] =
1.256 - right_distrib left_distrib left_diff_distrib right_diff_distrib
1.257 -
1.258 -text{*Legacy - use @{text algebra_simps} *}
1.259 -lemmas ring_simps[noatp] = algebra_simps
1.260 -
1.261 -lemma eq_add_iff1:
1.262 - "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
1.263 -by (simp add: algebra_simps)
1.264 -
1.265 -lemma eq_add_iff2:
1.266 - "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
1.267 -by (simp add: algebra_simps)
1.268 -
1.269 -end
1.270 -
1.271 -lemmas ring_distribs[noatp] =
1.272 - right_distrib left_distrib left_diff_distrib right_diff_distrib
1.273 -
1.274 -class comm_ring = comm_semiring + ab_group_add
1.275 -begin
1.276 -
1.277 -subclass ring ..
1.278 -subclass comm_semiring_0_cancel ..
1.279 -
1.280 -end
1.281 -
1.282 -class ring_1 = ring + zero_neq_one + monoid_mult
1.283 -begin
1.284 -
1.285 -subclass semiring_1_cancel ..
1.286 -
1.287 -end
1.288 -
1.289 -class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
1.290 - (*previously ring*)
1.291 -begin
1.292 -
1.293 -subclass ring_1 ..
1.294 -subclass comm_semiring_1_cancel ..
1.295 -
1.296 -lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
1.297 -proof
1.298 - assume "x dvd - y"
1.299 - then have "x dvd - 1 * - y" by (rule dvd_mult)
1.300 - then show "x dvd y" by simp
1.301 -next
1.302 - assume "x dvd y"
1.303 - then have "x dvd - 1 * y" by (rule dvd_mult)
1.304 - then show "x dvd - y" by simp
1.305 -qed
1.306 -
1.307 -lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
1.308 -proof
1.309 - assume "- x dvd y"
1.310 - then obtain k where "y = - x * k" ..
1.311 - then have "y = x * - k" by simp
1.312 - then show "x dvd y" ..
1.313 -next
1.314 - assume "x dvd y"
1.315 - then obtain k where "y = x * k" ..
1.316 - then have "y = - x * - k" by simp
1.317 - then show "- x dvd y" ..
1.318 -qed
1.319 -
1.320 -lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
1.321 -by (simp add: diff_minus dvd_minus_iff)
1.322 -
1.323 -end
1.324 -
1.325 -class ring_no_zero_divisors = ring + no_zero_divisors
1.326 -begin
1.327 -
1.328 -lemma mult_eq_0_iff [simp]:
1.329 - shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
1.330 -proof (cases "a = 0 \<or> b = 0")
1.331 - case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.332 - then show ?thesis using no_zero_divisors by simp
1.333 -next
1.334 - case True then show ?thesis by auto
1.335 -qed
1.336 -
1.337 -text{*Cancellation of equalities with a common factor*}
1.338 -lemma mult_cancel_right [simp, noatp]:
1.339 - "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
1.340 -proof -
1.341 - have "(a * c = b * c) = ((a - b) * c = 0)"
1.342 - by (simp add: algebra_simps right_minus_eq)
1.343 - thus ?thesis by (simp add: disj_commute right_minus_eq)
1.344 -qed
1.345 -
1.346 -lemma mult_cancel_left [simp, noatp]:
1.347 - "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
1.348 -proof -
1.349 - have "(c * a = c * b) = (c * (a - b) = 0)"
1.350 - by (simp add: algebra_simps right_minus_eq)
1.351 - thus ?thesis by (simp add: right_minus_eq)
1.352 -qed
1.353 -
1.354 -end
1.355 -
1.356 -class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
1.357 -begin
1.358 -
1.359 -lemma mult_cancel_right1 [simp]:
1.360 - "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
1.361 -by (insert mult_cancel_right [of 1 c b], force)
1.362 -
1.363 -lemma mult_cancel_right2 [simp]:
1.364 - "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
1.365 -by (insert mult_cancel_right [of a c 1], simp)
1.366 -
1.367 -lemma mult_cancel_left1 [simp]:
1.368 - "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
1.369 -by (insert mult_cancel_left [of c 1 b], force)
1.370 -
1.371 -lemma mult_cancel_left2 [simp]:
1.372 - "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
1.373 -by (insert mult_cancel_left [of c a 1], simp)
1.374 -
1.375 -end
1.376 -
1.377 -class idom = comm_ring_1 + no_zero_divisors
1.378 -begin
1.379 -
1.380 -subclass ring_1_no_zero_divisors ..
1.381 -
1.382 -lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
1.383 -proof
1.384 - assume "a * a = b * b"
1.385 - then have "(a - b) * (a + b) = 0"
1.386 - by (simp add: algebra_simps)
1.387 - then show "a = b \<or> a = - b"
1.388 - by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
1.389 -next
1.390 - assume "a = b \<or> a = - b"
1.391 - then show "a * a = b * b" by auto
1.392 -qed
1.393 -
1.394 -lemma dvd_mult_cancel_right [simp]:
1.395 - "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
1.396 -proof -
1.397 - have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
1.398 - unfolding dvd_def by (simp add: mult_ac)
1.399 - also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
1.400 - unfolding dvd_def by simp
1.401 - finally show ?thesis .
1.402 -qed
1.403 -
1.404 -lemma dvd_mult_cancel_left [simp]:
1.405 - "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
1.406 -proof -
1.407 - have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
1.408 - unfolding dvd_def by (simp add: mult_ac)
1.409 - also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
1.410 - unfolding dvd_def by simp
1.411 - finally show ?thesis .
1.412 -qed
1.413 -
1.414 -end
1.415 -
1.416 -class division_ring = ring_1 + inverse +
1.417 - assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
1.418 - assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
1.419 -begin
1.420 -
1.421 -subclass ring_1_no_zero_divisors
1.422 -proof
1.423 - fix a b :: 'a
1.424 - assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
1.425 - show "a * b \<noteq> 0"
1.426 - proof
1.427 - assume ab: "a * b = 0"
1.428 - hence "0 = inverse a * (a * b) * inverse b" by simp
1.429 - also have "\<dots> = (inverse a * a) * (b * inverse b)"
1.430 - by (simp only: mult_assoc)
1.431 - also have "\<dots> = 1" using a b by simp
1.432 - finally show False by simp
1.433 - qed
1.434 -qed
1.435 -
1.436 -lemma nonzero_imp_inverse_nonzero:
1.437 - "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
1.438 -proof
1.439 - assume ianz: "inverse a = 0"
1.440 - assume "a \<noteq> 0"
1.441 - hence "1 = a * inverse a" by simp
1.442 - also have "... = 0" by (simp add: ianz)
1.443 - finally have "1 = 0" .
1.444 - thus False by (simp add: eq_commute)
1.445 -qed
1.446 -
1.447 -lemma inverse_zero_imp_zero:
1.448 - "inverse a = 0 \<Longrightarrow> a = 0"
1.449 -apply (rule classical)
1.450 -apply (drule nonzero_imp_inverse_nonzero)
1.451 -apply auto
1.452 -done
1.453 -
1.454 -lemma inverse_unique:
1.455 - assumes ab: "a * b = 1"
1.456 - shows "inverse a = b"
1.457 -proof -
1.458 - have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
1.459 - moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
1.460 - ultimately show ?thesis by (simp add: mult_assoc [symmetric])
1.461 -qed
1.462 -
1.463 -lemma nonzero_inverse_minus_eq:
1.464 - "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
1.465 -by (rule inverse_unique) simp
1.466 -
1.467 -lemma nonzero_inverse_inverse_eq:
1.468 - "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
1.469 -by (rule inverse_unique) simp
1.470 -
1.471 -lemma nonzero_inverse_eq_imp_eq:
1.472 - assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
1.473 - shows "a = b"
1.474 -proof -
1.475 - from `inverse a = inverse b`
1.476 - have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
1.477 - with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
1.478 - by (simp add: nonzero_inverse_inverse_eq)
1.479 -qed
1.480 -
1.481 -lemma inverse_1 [simp]: "inverse 1 = 1"
1.482 -by (rule inverse_unique) simp
1.483 -
1.484 -lemma nonzero_inverse_mult_distrib:
1.485 - assumes "a \<noteq> 0" and "b \<noteq> 0"
1.486 - shows "inverse (a * b) = inverse b * inverse a"
1.487 -proof -
1.488 - have "a * (b * inverse b) * inverse a = 1" using assms by simp
1.489 - hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
1.490 - thus ?thesis by (rule inverse_unique)
1.491 -qed
1.492 -
1.493 -lemma division_ring_inverse_add:
1.494 - "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
1.495 -by (simp add: algebra_simps)
1.496 -
1.497 -lemma division_ring_inverse_diff:
1.498 - "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
1.499 -by (simp add: algebra_simps)
1.500 -
1.501 -end
1.502 -
1.503 -class field = comm_ring_1 + inverse +
1.504 - assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
1.505 - assumes divide_inverse: "a / b = a * inverse b"
1.506 -begin
1.507 -
1.508 -subclass division_ring
1.509 -proof
1.510 - fix a :: 'a
1.511 - assume "a \<noteq> 0"
1.512 - thus "inverse a * a = 1" by (rule field_inverse)
1.513 - thus "a * inverse a = 1" by (simp only: mult_commute)
1.514 -qed
1.515 -
1.516 -subclass idom ..
1.517 -
1.518 -lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
1.519 -proof
1.520 - assume neq: "b \<noteq> 0"
1.521 - {
1.522 - hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
1.523 - also assume "a / b = 1"
1.524 - finally show "a = b" by simp
1.525 - next
1.526 - assume "a = b"
1.527 - with neq show "a / b = 1" by (simp add: divide_inverse)
1.528 - }
1.529 -qed
1.530 -
1.531 -lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
1.532 -by (simp add: divide_inverse)
1.533 -
1.534 -lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
1.535 -by (simp add: divide_inverse)
1.536 -
1.537 -lemma divide_zero_left [simp]: "0 / a = 0"
1.538 -by (simp add: divide_inverse)
1.539 -
1.540 -lemma inverse_eq_divide: "inverse a = 1 / a"
1.541 -by (simp add: divide_inverse)
1.542 -
1.543 -lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
1.544 -by (simp add: divide_inverse algebra_simps)
1.545 -
1.546 -text{*There is no slick version using division by zero.*}
1.547 -lemma inverse_add:
1.548 - "[| a \<noteq> 0; b \<noteq> 0 |]
1.549 - ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
1.550 -by (simp add: division_ring_inverse_add mult_ac)
1.551 -
1.552 -lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
1.553 -assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
1.554 -proof -
1.555 - have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
1.556 - by (simp add: divide_inverse nonzero_inverse_mult_distrib)
1.557 - also have "... = a * inverse b * (inverse c * c)"
1.558 - by (simp only: mult_ac)
1.559 - also have "... = a * inverse b" by simp
1.560 - finally show ?thesis by (simp add: divide_inverse)
1.561 -qed
1.562 -
1.563 -lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
1.564 - "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
1.565 -by (simp add: mult_commute [of _ c])
1.566 -
1.567 -lemma divide_1 [simp]: "a / 1 = a"
1.568 -by (simp add: divide_inverse)
1.569 -
1.570 -lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
1.571 -by (simp add: divide_inverse mult_assoc)
1.572 -
1.573 -lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
1.574 -by (simp add: divide_inverse mult_ac)
1.575 -
1.576 -text {* These are later declared as simp rules. *}
1.577 -lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
1.578 -
1.579 -lemma add_frac_eq:
1.580 - assumes "y \<noteq> 0" and "z \<noteq> 0"
1.581 - shows "x / y + w / z = (x * z + w * y) / (y * z)"
1.582 -proof -
1.583 - have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
1.584 - using assms by simp
1.585 - also have "\<dots> = (x * z + y * w) / (y * z)"
1.586 - by (simp only: add_divide_distrib)
1.587 - finally show ?thesis
1.588 - by (simp only: mult_commute)
1.589 -qed
1.590 -
1.591 -text{*Special Cancellation Simprules for Division*}
1.592 -
1.593 -lemma nonzero_mult_divide_cancel_right [simp, noatp]:
1.594 - "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
1.595 -using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
1.596 -
1.597 -lemma nonzero_mult_divide_cancel_left [simp, noatp]:
1.598 - "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
1.599 -using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
1.600 -
1.601 -lemma nonzero_divide_mult_cancel_right [simp, noatp]:
1.602 - "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
1.603 -using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
1.604 -
1.605 -lemma nonzero_divide_mult_cancel_left [simp, noatp]:
1.606 - "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
1.607 -using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
1.608 -
1.609 -lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
1.610 - "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
1.611 -using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
1.612 -
1.613 -lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
1.614 - "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
1.615 -using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
1.616 -
1.617 -lemma minus_divide_left: "- (a / b) = (-a) / b"
1.618 -by (simp add: divide_inverse)
1.619 -
1.620 -lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
1.621 -by (simp add: divide_inverse nonzero_inverse_minus_eq)
1.622 -
1.623 -lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
1.624 -by (simp add: divide_inverse nonzero_inverse_minus_eq)
1.625 -
1.626 -lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
1.627 -by (simp add: divide_inverse)
1.628 -
1.629 -lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
1.630 -by (simp add: diff_minus add_divide_distrib)
1.631 -
1.632 -lemma add_divide_eq_iff:
1.633 - "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
1.634 -by (simp add: add_divide_distrib)
1.635 -
1.636 -lemma divide_add_eq_iff:
1.637 - "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
1.638 -by (simp add: add_divide_distrib)
1.639 -
1.640 -lemma diff_divide_eq_iff:
1.641 - "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
1.642 -by (simp add: diff_divide_distrib)
1.643 -
1.644 -lemma divide_diff_eq_iff:
1.645 - "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
1.646 -by (simp add: diff_divide_distrib)
1.647 -
1.648 -lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
1.649 -proof -
1.650 - assume [simp]: "c \<noteq> 0"
1.651 - have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
1.652 - also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
1.653 - finally show ?thesis .
1.654 -qed
1.655 -
1.656 -lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
1.657 -proof -
1.658 - assume [simp]: "c \<noteq> 0"
1.659 - have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
1.660 - also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
1.661 - finally show ?thesis .
1.662 -qed
1.663 -
1.664 -lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
1.665 -by simp
1.666 -
1.667 -lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
1.668 -by (erule subst, simp)
1.669 -
1.670 -lemmas field_eq_simps[noatp] = algebra_simps
1.671 - (* pull / out*)
1.672 - add_divide_eq_iff divide_add_eq_iff
1.673 - diff_divide_eq_iff divide_diff_eq_iff
1.674 - (* multiply eqn *)
1.675 - nonzero_eq_divide_eq nonzero_divide_eq_eq
1.676 -(* is added later:
1.677 - times_divide_eq_left times_divide_eq_right
1.678 -*)
1.679 -
1.680 -text{*An example:*}
1.681 -lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
1.682 -apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
1.683 - apply(simp add:field_eq_simps)
1.684 -apply(simp)
1.685 -done
1.686 -
1.687 -lemma diff_frac_eq:
1.688 - "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
1.689 -by (simp add: field_eq_simps times_divide_eq)
1.690 -
1.691 -lemma frac_eq_eq:
1.692 - "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
1.693 -by (simp add: field_eq_simps times_divide_eq)
1.694 -
1.695 -end
1.696 -
1.697 -class division_by_zero = zero + inverse +
1.698 - assumes inverse_zero [simp]: "inverse 0 = 0"
1.699 -
1.700 -lemma divide_zero [simp]:
1.701 - "a / 0 = (0::'a::{field,division_by_zero})"
1.702 -by (simp add: divide_inverse)
1.703 -
1.704 -lemma divide_self_if [simp]:
1.705 - "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
1.706 -by simp
1.707 -
1.708 -class mult_mono = times + zero + ord +
1.709 - assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.710 - assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
1.711 -
1.712 -class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add
1.713 -begin
1.714 -
1.715 -lemma mult_mono:
1.716 - "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
1.717 - \<Longrightarrow> a * c \<le> b * d"
1.718 -apply (erule mult_right_mono [THEN order_trans], assumption)
1.719 -apply (erule mult_left_mono, assumption)
1.720 -done
1.721 -
1.722 -lemma mult_mono':
1.723 - "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
1.724 - \<Longrightarrow> a * c \<le> b * d"
1.725 -apply (rule mult_mono)
1.726 -apply (fast intro: order_trans)+
1.727 -done
1.728 -
1.729 -end
1.730 -
1.731 -class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
1.732 - + semiring + cancel_comm_monoid_add
1.733 -begin
1.734 -
1.735 -subclass semiring_0_cancel ..
1.736 -subclass pordered_semiring ..
1.737 -
1.738 -lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
1.739 -using mult_left_mono [of zero b a] by simp
1.740 -
1.741 -lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
1.742 -using mult_left_mono [of b zero a] by simp
1.743 -
1.744 -lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
1.745 -using mult_right_mono [of a zero b] by simp
1.746 -
1.747 -text {* Legacy - use @{text mult_nonpos_nonneg} *}
1.748 -lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
1.749 -by (drule mult_right_mono [of b zero], auto)
1.750 -
1.751 -lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
1.752 -by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
1.753 -
1.754 -end
1.755 -
1.756 -class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
1.757 -begin
1.758 -
1.759 -subclass pordered_cancel_semiring ..
1.760 -
1.761 -subclass pordered_comm_monoid_add ..
1.762 -
1.763 -lemma mult_left_less_imp_less:
1.764 - "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
1.765 -by (force simp add: mult_left_mono not_le [symmetric])
1.766 -
1.767 -lemma mult_right_less_imp_less:
1.768 - "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
1.769 -by (force simp add: mult_right_mono not_le [symmetric])
1.770 -
1.771 -end
1.772 -
1.773 -class ordered_semiring_1 = ordered_semiring + semiring_1
1.774 -
1.775 -class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
1.776 - assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
1.777 - assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
1.778 -begin
1.779 -
1.780 -subclass semiring_0_cancel ..
1.781 -
1.782 -subclass ordered_semiring
1.783 -proof
1.784 - fix a b c :: 'a
1.785 - assume A: "a \<le> b" "0 \<le> c"
1.786 - from A show "c * a \<le> c * b"
1.787 - unfolding le_less
1.788 - using mult_strict_left_mono by (cases "c = 0") auto
1.789 - from A show "a * c \<le> b * c"
1.790 - unfolding le_less
1.791 - using mult_strict_right_mono by (cases "c = 0") auto
1.792 -qed
1.793 -
1.794 -lemma mult_left_le_imp_le:
1.795 - "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
1.796 -by (force simp add: mult_strict_left_mono _not_less [symmetric])
1.797 -
1.798 -lemma mult_right_le_imp_le:
1.799 - "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
1.800 -by (force simp add: mult_strict_right_mono not_less [symmetric])
1.801 -
1.802 -lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
1.803 -using mult_strict_left_mono [of zero b a] by simp
1.804 -
1.805 -lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
1.806 -using mult_strict_left_mono [of b zero a] by simp
1.807 -
1.808 -lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
1.809 -using mult_strict_right_mono [of a zero b] by simp
1.810 -
1.811 -text {* Legacy - use @{text mult_neg_pos} *}
1.812 -lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
1.813 -by (drule mult_strict_right_mono [of b zero], auto)
1.814 -
1.815 -lemma zero_less_mult_pos:
1.816 - "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
1.817 -apply (cases "b\<le>0")
1.818 - apply (auto simp add: le_less not_less)
1.819 -apply (drule_tac mult_pos_neg [of a b])
1.820 - apply (auto dest: less_not_sym)
1.821 -done
1.822 -
1.823 -lemma zero_less_mult_pos2:
1.824 - "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
1.825 -apply (cases "b\<le>0")
1.826 - apply (auto simp add: le_less not_less)
1.827 -apply (drule_tac mult_pos_neg2 [of a b])
1.828 - apply (auto dest: less_not_sym)
1.829 -done
1.830 -
1.831 -text{*Strict monotonicity in both arguments*}
1.832 -lemma mult_strict_mono:
1.833 - assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
1.834 - shows "a * c < b * d"
1.835 - using assms apply (cases "c=0")
1.836 - apply (simp add: mult_pos_pos)
1.837 - apply (erule mult_strict_right_mono [THEN less_trans])
1.838 - apply (force simp add: le_less)
1.839 - apply (erule mult_strict_left_mono, assumption)
1.840 - done
1.841 -
1.842 -text{*This weaker variant has more natural premises*}
1.843 -lemma mult_strict_mono':
1.844 - assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
1.845 - shows "a * c < b * d"
1.846 -by (rule mult_strict_mono) (insert assms, auto)
1.847 -
1.848 -lemma mult_less_le_imp_less:
1.849 - assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
1.850 - shows "a * c < b * d"
1.851 - using assms apply (subgoal_tac "a * c < b * c")
1.852 - apply (erule less_le_trans)
1.853 - apply (erule mult_left_mono)
1.854 - apply simp
1.855 - apply (erule mult_strict_right_mono)
1.856 - apply assumption
1.857 - done
1.858 -
1.859 -lemma mult_le_less_imp_less:
1.860 - assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
1.861 - shows "a * c < b * d"
1.862 - using assms apply (subgoal_tac "a * c \<le> b * c")
1.863 - apply (erule le_less_trans)
1.864 - apply (erule mult_strict_left_mono)
1.865 - apply simp
1.866 - apply (erule mult_right_mono)
1.867 - apply simp
1.868 - done
1.869 -
1.870 -lemma mult_less_imp_less_left:
1.871 - assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
1.872 - shows "a < b"
1.873 -proof (rule ccontr)
1.874 - assume "\<not> a < b"
1.875 - hence "b \<le> a" by (simp add: linorder_not_less)
1.876 - hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
1.877 - with this and less show False by (simp add: not_less [symmetric])
1.878 -qed
1.879 -
1.880 -lemma mult_less_imp_less_right:
1.881 - assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
1.882 - shows "a < b"
1.883 -proof (rule ccontr)
1.884 - assume "\<not> a < b"
1.885 - hence "b \<le> a" by (simp add: linorder_not_less)
1.886 - hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
1.887 - with this and less show False by (simp add: not_less [symmetric])
1.888 -qed
1.889 -
1.890 -end
1.891 -
1.892 -class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
1.893 -
1.894 -class mult_mono1 = times + zero + ord +
1.895 - assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.896 -
1.897 -class pordered_comm_semiring = comm_semiring_0
1.898 - + pordered_ab_semigroup_add + mult_mono1
1.899 -begin
1.900 -
1.901 -subclass pordered_semiring
1.902 -proof
1.903 - fix a b c :: 'a
1.904 - assume "a \<le> b" "0 \<le> c"
1.905 - thus "c * a \<le> c * b" by (rule mult_mono1)
1.906 - thus "a * c \<le> b * c" by (simp only: mult_commute)
1.907 -qed
1.908 -
1.909 -end
1.910 -
1.911 -class pordered_cancel_comm_semiring = comm_semiring_0_cancel
1.912 - + pordered_ab_semigroup_add + mult_mono1
1.913 -begin
1.914 -
1.915 -subclass pordered_comm_semiring ..
1.916 -subclass pordered_cancel_semiring ..
1.917 -
1.918 -end
1.919 -
1.920 -class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
1.921 - assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
1.922 -begin
1.923 -
1.924 -subclass ordered_semiring_strict
1.925 -proof
1.926 - fix a b c :: 'a
1.927 - assume "a < b" "0 < c"
1.928 - thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
1.929 - thus "a * c < b * c" by (simp only: mult_commute)
1.930 -qed
1.931 -
1.932 -subclass pordered_cancel_comm_semiring
1.933 -proof
1.934 - fix a b c :: 'a
1.935 - assume "a \<le> b" "0 \<le> c"
1.936 - thus "c * a \<le> c * b"
1.937 - unfolding le_less
1.938 - using mult_strict_left_mono by (cases "c = 0") auto
1.939 -qed
1.940 -
1.941 -end
1.942 -
1.943 -class pordered_ring = ring + pordered_cancel_semiring
1.944 -begin
1.945 -
1.946 -subclass pordered_ab_group_add ..
1.947 -
1.948 -text{*Legacy - use @{text algebra_simps} *}
1.949 -lemmas ring_simps[noatp] = algebra_simps
1.950 -
1.951 -lemma less_add_iff1:
1.952 - "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
1.953 -by (simp add: algebra_simps)
1.954 -
1.955 -lemma less_add_iff2:
1.956 - "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
1.957 -by (simp add: algebra_simps)
1.958 -
1.959 -lemma le_add_iff1:
1.960 - "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
1.961 -by (simp add: algebra_simps)
1.962 -
1.963 -lemma le_add_iff2:
1.964 - "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
1.965 -by (simp add: algebra_simps)
1.966 -
1.967 -lemma mult_left_mono_neg:
1.968 - "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
1.969 - apply (drule mult_left_mono [of _ _ "uminus c"])
1.970 - apply (simp_all add: minus_mult_left [symmetric])
1.971 - done
1.972 -
1.973 -lemma mult_right_mono_neg:
1.974 - "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
1.975 - apply (drule mult_right_mono [of _ _ "uminus c"])
1.976 - apply (simp_all add: minus_mult_right [symmetric])
1.977 - done
1.978 -
1.979 -lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
1.980 -using mult_right_mono_neg [of a zero b] by simp
1.981 -
1.982 -lemma split_mult_pos_le:
1.983 - "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
1.984 -by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
1.985 -
1.986 -end
1.987 -
1.988 -class abs_if = minus + uminus + ord + zero + abs +
1.989 - assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
1.990 -
1.991 -class sgn_if = minus + uminus + zero + one + ord + sgn +
1.992 - assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
1.993 -
1.994 -lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
1.995 -by(simp add:sgn_if)
1.996 -
1.997 -class ordered_ring = ring + ordered_semiring
1.998 - + ordered_ab_group_add + abs_if
1.999 -begin
1.1000 -
1.1001 -subclass pordered_ring ..
1.1002 -
1.1003 -subclass pordered_ab_group_add_abs
1.1004 -proof
1.1005 - fix a b
1.1006 - show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.1007 -by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
1.1008 - (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
1.1009 - neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
1.1010 - auto intro!: less_imp_le add_neg_neg)
1.1011 -qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
1.1012 -
1.1013 -end
1.1014 -
1.1015 -(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
1.1016 - Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
1.1017 - *)
1.1018 -class ordered_ring_strict = ring + ordered_semiring_strict
1.1019 - + ordered_ab_group_add + abs_if
1.1020 -begin
1.1021 -
1.1022 -subclass ordered_ring ..
1.1023 -
1.1024 -lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
1.1025 -using mult_strict_left_mono [of b a "- c"] by simp
1.1026 -
1.1027 -lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
1.1028 -using mult_strict_right_mono [of b a "- c"] by simp
1.1029 -
1.1030 -lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
1.1031 -using mult_strict_right_mono_neg [of a zero b] by simp
1.1032 -
1.1033 -subclass ring_no_zero_divisors
1.1034 -proof
1.1035 - fix a b
1.1036 - assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
1.1037 - assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
1.1038 - have "a * b < 0 \<or> 0 < a * b"
1.1039 - proof (cases "a < 0")
1.1040 - case True note A' = this
1.1041 - show ?thesis proof (cases "b < 0")
1.1042 - case True with A'
1.1043 - show ?thesis by (auto dest: mult_neg_neg)
1.1044 - next
1.1045 - case False with B have "0 < b" by auto
1.1046 - with A' show ?thesis by (auto dest: mult_strict_right_mono)
1.1047 - qed
1.1048 - next
1.1049 - case False with A have A': "0 < a" by auto
1.1050 - show ?thesis proof (cases "b < 0")
1.1051 - case True with A'
1.1052 - show ?thesis by (auto dest: mult_strict_right_mono_neg)
1.1053 - next
1.1054 - case False with B have "0 < b" by auto
1.1055 - with A' show ?thesis by (auto dest: mult_pos_pos)
1.1056 - qed
1.1057 - qed
1.1058 - then show "a * b \<noteq> 0" by (simp add: neq_iff)
1.1059 -qed
1.1060 -
1.1061 -lemma zero_less_mult_iff:
1.1062 - "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
1.1063 - apply (auto simp add: mult_pos_pos mult_neg_neg)
1.1064 - apply (simp_all add: not_less le_less)
1.1065 - apply (erule disjE) apply assumption defer
1.1066 - apply (erule disjE) defer apply (drule sym) apply simp
1.1067 - apply (erule disjE) defer apply (drule sym) apply simp
1.1068 - apply (erule disjE) apply assumption apply (drule sym) apply simp
1.1069 - apply (drule sym) apply simp
1.1070 - apply (blast dest: zero_less_mult_pos)
1.1071 - apply (blast dest: zero_less_mult_pos2)
1.1072 - done
1.1073 -
1.1074 -lemma zero_le_mult_iff:
1.1075 - "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
1.1076 -by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
1.1077 -
1.1078 -lemma mult_less_0_iff:
1.1079 - "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
1.1080 - apply (insert zero_less_mult_iff [of "-a" b])
1.1081 - apply (force simp add: minus_mult_left[symmetric])
1.1082 - done
1.1083 -
1.1084 -lemma mult_le_0_iff:
1.1085 - "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
1.1086 - apply (insert zero_le_mult_iff [of "-a" b])
1.1087 - apply (force simp add: minus_mult_left[symmetric])
1.1088 - done
1.1089 -
1.1090 -lemma zero_le_square [simp]: "0 \<le> a * a"
1.1091 -by (simp add: zero_le_mult_iff linear)
1.1092 -
1.1093 -lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
1.1094 -by (simp add: not_less)
1.1095 -
1.1096 -text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
1.1097 - also with the relations @{text "\<le>"} and equality.*}
1.1098 -
1.1099 -text{*These ``disjunction'' versions produce two cases when the comparison is
1.1100 - an assumption, but effectively four when the comparison is a goal.*}
1.1101 -
1.1102 -lemma mult_less_cancel_right_disj:
1.1103 - "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
1.1104 - apply (cases "c = 0")
1.1105 - apply (auto simp add: neq_iff mult_strict_right_mono
1.1106 - mult_strict_right_mono_neg)
1.1107 - apply (auto simp add: not_less
1.1108 - not_le [symmetric, of "a*c"]
1.1109 - not_le [symmetric, of a])
1.1110 - apply (erule_tac [!] notE)
1.1111 - apply (auto simp add: less_imp_le mult_right_mono
1.1112 - mult_right_mono_neg)
1.1113 - done
1.1114 -
1.1115 -lemma mult_less_cancel_left_disj:
1.1116 - "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
1.1117 - apply (cases "c = 0")
1.1118 - apply (auto simp add: neq_iff mult_strict_left_mono
1.1119 - mult_strict_left_mono_neg)
1.1120 - apply (auto simp add: not_less
1.1121 - not_le [symmetric, of "c*a"]
1.1122 - not_le [symmetric, of a])
1.1123 - apply (erule_tac [!] notE)
1.1124 - apply (auto simp add: less_imp_le mult_left_mono
1.1125 - mult_left_mono_neg)
1.1126 - done
1.1127 -
1.1128 -text{*The ``conjunction of implication'' lemmas produce two cases when the
1.1129 -comparison is a goal, but give four when the comparison is an assumption.*}
1.1130 -
1.1131 -lemma mult_less_cancel_right:
1.1132 - "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
1.1133 - using mult_less_cancel_right_disj [of a c b] by auto
1.1134 -
1.1135 -lemma mult_less_cancel_left:
1.1136 - "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
1.1137 - using mult_less_cancel_left_disj [of c a b] by auto
1.1138 -
1.1139 -lemma mult_le_cancel_right:
1.1140 - "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
1.1141 -by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
1.1142 -
1.1143 -lemma mult_le_cancel_left:
1.1144 - "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
1.1145 -by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
1.1146 -
1.1147 -lemma mult_le_cancel_left_pos:
1.1148 - "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
1.1149 -by (auto simp: mult_le_cancel_left)
1.1150 -
1.1151 -lemma mult_le_cancel_left_neg:
1.1152 - "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
1.1153 -by (auto simp: mult_le_cancel_left)
1.1154 -
1.1155 -lemma mult_less_cancel_left_pos:
1.1156 - "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
1.1157 -by (auto simp: mult_less_cancel_left)
1.1158 -
1.1159 -lemma mult_less_cancel_left_neg:
1.1160 - "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
1.1161 -by (auto simp: mult_less_cancel_left)
1.1162 -
1.1163 -end
1.1164 -
1.1165 -text{*Legacy - use @{text algebra_simps} *}
1.1166 -lemmas ring_simps[noatp] = algebra_simps
1.1167 -
1.1168 -lemmas mult_sign_intros =
1.1169 - mult_nonneg_nonneg mult_nonneg_nonpos
1.1170 - mult_nonpos_nonneg mult_nonpos_nonpos
1.1171 - mult_pos_pos mult_pos_neg
1.1172 - mult_neg_pos mult_neg_neg
1.1173 -
1.1174 -class pordered_comm_ring = comm_ring + pordered_comm_semiring
1.1175 -begin
1.1176 -
1.1177 -subclass pordered_ring ..
1.1178 -subclass pordered_cancel_comm_semiring ..
1.1179 -
1.1180 -end
1.1181 -
1.1182 -class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
1.1183 - (*previously ordered_semiring*)
1.1184 - assumes zero_less_one [simp]: "0 < 1"
1.1185 -begin
1.1186 -
1.1187 -lemma pos_add_strict:
1.1188 - shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
1.1189 - using add_strict_mono [of zero a b c] by simp
1.1190 -
1.1191 -lemma zero_le_one [simp]: "0 \<le> 1"
1.1192 -by (rule zero_less_one [THEN less_imp_le])
1.1193 -
1.1194 -lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
1.1195 -by (simp add: not_le)
1.1196 -
1.1197 -lemma not_one_less_zero [simp]: "\<not> 1 < 0"
1.1198 -by (simp add: not_less)
1.1199 -
1.1200 -lemma less_1_mult:
1.1201 - assumes "1 < m" and "1 < n"
1.1202 - shows "1 < m * n"
1.1203 - using assms mult_strict_mono [of 1 m 1 n]
1.1204 - by (simp add: less_trans [OF zero_less_one])
1.1205 -
1.1206 -end
1.1207 -
1.1208 -class ordered_idom = comm_ring_1 +
1.1209 - ordered_comm_semiring_strict + ordered_ab_group_add +
1.1210 - abs_if + sgn_if
1.1211 - (*previously ordered_ring*)
1.1212 -begin
1.1213 -
1.1214 -subclass ordered_ring_strict ..
1.1215 -subclass pordered_comm_ring ..
1.1216 -subclass idom ..
1.1217 -
1.1218 -subclass ordered_semidom
1.1219 -proof
1.1220 - have "0 \<le> 1 * 1" by (rule zero_le_square)
1.1221 - thus "0 < 1" by (simp add: le_less)
1.1222 -qed
1.1223 -
1.1224 -lemma linorder_neqE_ordered_idom:
1.1225 - assumes "x \<noteq> y" obtains "x < y" | "y < x"
1.1226 - using assms by (rule neqE)
1.1227 -
1.1228 -text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
1.1229 -
1.1230 -lemma mult_le_cancel_right1:
1.1231 - "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
1.1232 -by (insert mult_le_cancel_right [of 1 c b], simp)
1.1233 -
1.1234 -lemma mult_le_cancel_right2:
1.1235 - "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
1.1236 -by (insert mult_le_cancel_right [of a c 1], simp)
1.1237 -
1.1238 -lemma mult_le_cancel_left1:
1.1239 - "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
1.1240 -by (insert mult_le_cancel_left [of c 1 b], simp)
1.1241 -
1.1242 -lemma mult_le_cancel_left2:
1.1243 - "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
1.1244 -by (insert mult_le_cancel_left [of c a 1], simp)
1.1245 -
1.1246 -lemma mult_less_cancel_right1:
1.1247 - "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
1.1248 -by (insert mult_less_cancel_right [of 1 c b], simp)
1.1249 -
1.1250 -lemma mult_less_cancel_right2:
1.1251 - "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
1.1252 -by (insert mult_less_cancel_right [of a c 1], simp)
1.1253 -
1.1254 -lemma mult_less_cancel_left1:
1.1255 - "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
1.1256 -by (insert mult_less_cancel_left [of c 1 b], simp)
1.1257 -
1.1258 -lemma mult_less_cancel_left2:
1.1259 - "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
1.1260 -by (insert mult_less_cancel_left [of c a 1], simp)
1.1261 -
1.1262 -lemma sgn_sgn [simp]:
1.1263 - "sgn (sgn a) = sgn a"
1.1264 -unfolding sgn_if by simp
1.1265 -
1.1266 -lemma sgn_0_0:
1.1267 - "sgn a = 0 \<longleftrightarrow> a = 0"
1.1268 -unfolding sgn_if by simp
1.1269 -
1.1270 -lemma sgn_1_pos:
1.1271 - "sgn a = 1 \<longleftrightarrow> a > 0"
1.1272 -unfolding sgn_if by (simp add: neg_equal_zero)
1.1273 -
1.1274 -lemma sgn_1_neg:
1.1275 - "sgn a = - 1 \<longleftrightarrow> a < 0"
1.1276 -unfolding sgn_if by (auto simp add: equal_neg_zero)
1.1277 -
1.1278 -lemma sgn_pos [simp]:
1.1279 - "0 < a \<Longrightarrow> sgn a = 1"
1.1280 -unfolding sgn_1_pos .
1.1281 -
1.1282 -lemma sgn_neg [simp]:
1.1283 - "a < 0 \<Longrightarrow> sgn a = - 1"
1.1284 -unfolding sgn_1_neg .
1.1285 -
1.1286 -lemma sgn_times:
1.1287 - "sgn (a * b) = sgn a * sgn b"
1.1288 -by (auto simp add: sgn_if zero_less_mult_iff)
1.1289 -
1.1290 -lemma abs_sgn: "abs k = k * sgn k"
1.1291 -unfolding sgn_if abs_if by auto
1.1292 -
1.1293 -lemma sgn_greater [simp]:
1.1294 - "0 < sgn a \<longleftrightarrow> 0 < a"
1.1295 - unfolding sgn_if by auto
1.1296 -
1.1297 -lemma sgn_less [simp]:
1.1298 - "sgn a < 0 \<longleftrightarrow> a < 0"
1.1299 - unfolding sgn_if by auto
1.1300 -
1.1301 -lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
1.1302 - by (simp add: abs_if)
1.1303 -
1.1304 -lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
1.1305 - by (simp add: abs_if)
1.1306 -
1.1307 -lemma dvd_if_abs_eq:
1.1308 - "abs l = abs (k) \<Longrightarrow> l dvd k"
1.1309 -by(subst abs_dvd_iff[symmetric]) simp
1.1310 -
1.1311 -end
1.1312 -
1.1313 -class ordered_field = field + ordered_idom
1.1314 -
1.1315 -text {* Simprules for comparisons where common factors can be cancelled. *}
1.1316 -
1.1317 -lemmas mult_compare_simps[noatp] =
1.1318 - mult_le_cancel_right mult_le_cancel_left
1.1319 - mult_le_cancel_right1 mult_le_cancel_right2
1.1320 - mult_le_cancel_left1 mult_le_cancel_left2
1.1321 - mult_less_cancel_right mult_less_cancel_left
1.1322 - mult_less_cancel_right1 mult_less_cancel_right2
1.1323 - mult_less_cancel_left1 mult_less_cancel_left2
1.1324 - mult_cancel_right mult_cancel_left
1.1325 - mult_cancel_right1 mult_cancel_right2
1.1326 - mult_cancel_left1 mult_cancel_left2
1.1327 -
1.1328 --- {* FIXME continue localization here *}
1.1329 -
1.1330 -lemma inverse_nonzero_iff_nonzero [simp]:
1.1331 - "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
1.1332 -by (force dest: inverse_zero_imp_zero)
1.1333 -
1.1334 -lemma inverse_minus_eq [simp]:
1.1335 - "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
1.1336 -proof cases
1.1337 - assume "a=0" thus ?thesis by (simp add: inverse_zero)
1.1338 -next
1.1339 - assume "a\<noteq>0"
1.1340 - thus ?thesis by (simp add: nonzero_inverse_minus_eq)
1.1341 -qed
1.1342 -
1.1343 -lemma inverse_eq_imp_eq:
1.1344 - "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
1.1345 -apply (cases "a=0 | b=0")
1.1346 - apply (force dest!: inverse_zero_imp_zero
1.1347 - simp add: eq_commute [of "0::'a"])
1.1348 -apply (force dest!: nonzero_inverse_eq_imp_eq)
1.1349 -done
1.1350 -
1.1351 -lemma inverse_eq_iff_eq [simp]:
1.1352 - "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
1.1353 -by (force dest!: inverse_eq_imp_eq)
1.1354 -
1.1355 -lemma inverse_inverse_eq [simp]:
1.1356 - "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
1.1357 - proof cases
1.1358 - assume "a=0" thus ?thesis by simp
1.1359 - next
1.1360 - assume "a\<noteq>0"
1.1361 - thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
1.1362 - qed
1.1363 -
1.1364 -text{*This version builds in division by zero while also re-orienting
1.1365 - the right-hand side.*}
1.1366 -lemma inverse_mult_distrib [simp]:
1.1367 - "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
1.1368 - proof cases
1.1369 - assume "a \<noteq> 0 & b \<noteq> 0"
1.1370 - thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
1.1371 - next
1.1372 - assume "~ (a \<noteq> 0 & b \<noteq> 0)"
1.1373 - thus ?thesis by force
1.1374 - qed
1.1375 -
1.1376 -lemma inverse_divide [simp]:
1.1377 - "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
1.1378 -by (simp add: divide_inverse mult_commute)
1.1379 -
1.1380 -
1.1381 -subsection {* Calculations with fractions *}
1.1382 -
1.1383 -text{* There is a whole bunch of simp-rules just for class @{text
1.1384 -field} but none for class @{text field} and @{text nonzero_divides}
1.1385 -because the latter are covered by a simproc. *}
1.1386 -
1.1387 -lemma mult_divide_mult_cancel_left:
1.1388 - "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
1.1389 -apply (cases "b = 0")
1.1390 -apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
1.1391 -done
1.1392 -
1.1393 -lemma mult_divide_mult_cancel_right:
1.1394 - "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
1.1395 -apply (cases "b = 0")
1.1396 -apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
1.1397 -done
1.1398 -
1.1399 -lemma divide_divide_eq_right [simp,noatp]:
1.1400 - "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
1.1401 -by (simp add: divide_inverse mult_ac)
1.1402 -
1.1403 -lemma divide_divide_eq_left [simp,noatp]:
1.1404 - "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
1.1405 -by (simp add: divide_inverse mult_assoc)
1.1406 -
1.1407 -
1.1408 -subsubsection{*Special Cancellation Simprules for Division*}
1.1409 -
1.1410 -lemma mult_divide_mult_cancel_left_if[simp,noatp]:
1.1411 -fixes c :: "'a :: {field,division_by_zero}"
1.1412 -shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
1.1413 -by (simp add: mult_divide_mult_cancel_left)
1.1414 -
1.1415 -
1.1416 -subsection {* Division and Unary Minus *}
1.1417 -
1.1418 -lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
1.1419 -by (simp add: divide_inverse)
1.1420 -
1.1421 -lemma divide_minus_right [simp, noatp]:
1.1422 - "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
1.1423 -by (simp add: divide_inverse)
1.1424 -
1.1425 -lemma minus_divide_divide:
1.1426 - "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
1.1427 -apply (cases "b=0", simp)
1.1428 -apply (simp add: nonzero_minus_divide_divide)
1.1429 -done
1.1430 -
1.1431 -lemma eq_divide_eq:
1.1432 - "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
1.1433 -by (simp add: nonzero_eq_divide_eq)
1.1434 -
1.1435 -lemma divide_eq_eq:
1.1436 - "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
1.1437 -by (force simp add: nonzero_divide_eq_eq)
1.1438 -
1.1439 -
1.1440 -subsection {* Ordered Fields *}
1.1441 -
1.1442 -lemma positive_imp_inverse_positive:
1.1443 -assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)"
1.1444 -proof -
1.1445 - have "0 < a * inverse a"
1.1446 - by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
1.1447 - thus "0 < inverse a"
1.1448 - by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
1.1449 -qed
1.1450 -
1.1451 -lemma negative_imp_inverse_negative:
1.1452 - "a < 0 ==> inverse a < (0::'a::ordered_field)"
1.1453 -by (insert positive_imp_inverse_positive [of "-a"],
1.1454 - simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
1.1455 -
1.1456 -lemma inverse_le_imp_le:
1.1457 -assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
1.1458 -shows "b \<le> (a::'a::ordered_field)"
1.1459 -proof (rule classical)
1.1460 - assume "~ b \<le> a"
1.1461 - hence "a < b" by (simp add: linorder_not_le)
1.1462 - hence bpos: "0 < b" by (blast intro: apos order_less_trans)
1.1463 - hence "a * inverse a \<le> a * inverse b"
1.1464 - by (simp add: apos invle order_less_imp_le mult_left_mono)
1.1465 - hence "(a * inverse a) * b \<le> (a * inverse b) * b"
1.1466 - by (simp add: bpos order_less_imp_le mult_right_mono)
1.1467 - thus "b \<le> a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
1.1468 -qed
1.1469 -
1.1470 -lemma inverse_positive_imp_positive:
1.1471 -assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
1.1472 -shows "0 < (a::'a::ordered_field)"
1.1473 -proof -
1.1474 - have "0 < inverse (inverse a)"
1.1475 - using inv_gt_0 by (rule positive_imp_inverse_positive)
1.1476 - thus "0 < a"
1.1477 - using nz by (simp add: nonzero_inverse_inverse_eq)
1.1478 -qed
1.1479 -
1.1480 -lemma inverse_positive_iff_positive [simp]:
1.1481 - "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
1.1482 -apply (cases "a = 0", simp)
1.1483 -apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
1.1484 -done
1.1485 -
1.1486 -lemma inverse_negative_imp_negative:
1.1487 -assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
1.1488 -shows "a < (0::'a::ordered_field)"
1.1489 -proof -
1.1490 - have "inverse (inverse a) < 0"
1.1491 - using inv_less_0 by (rule negative_imp_inverse_negative)
1.1492 - thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
1.1493 -qed
1.1494 -
1.1495 -lemma inverse_negative_iff_negative [simp]:
1.1496 - "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
1.1497 -apply (cases "a = 0", simp)
1.1498 -apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
1.1499 -done
1.1500 -
1.1501 -lemma inverse_nonnegative_iff_nonnegative [simp]:
1.1502 - "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1.1503 -by (simp add: linorder_not_less [symmetric])
1.1504 -
1.1505 -lemma inverse_nonpositive_iff_nonpositive [simp]:
1.1506 - "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
1.1507 -by (simp add: linorder_not_less [symmetric])
1.1508 -
1.1509 -lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
1.1510 -proof
1.1511 - fix x::'a
1.1512 - have m1: "- (1::'a) < 0" by simp
1.1513 - from add_strict_right_mono[OF m1, where c=x]
1.1514 - have "(- 1) + x < x" by simp
1.1515 - thus "\<exists>y. y < x" by blast
1.1516 -qed
1.1517 -
1.1518 -lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
1.1519 -proof
1.1520 - fix x::'a
1.1521 - have m1: " (1::'a) > 0" by simp
1.1522 - from add_strict_right_mono[OF m1, where c=x]
1.1523 - have "1 + x > x" by simp
1.1524 - thus "\<exists>y. y > x" by blast
1.1525 -qed
1.1526 -
1.1527 -subsection{*Anti-Monotonicity of @{term inverse}*}
1.1528 -
1.1529 -lemma less_imp_inverse_less:
1.1530 -assumes less: "a < b" and apos: "0 < a"
1.1531 -shows "inverse b < inverse (a::'a::ordered_field)"
1.1532 -proof (rule ccontr)
1.1533 - assume "~ inverse b < inverse a"
1.1534 - hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
1.1535 - hence "~ (a < b)"
1.1536 - by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
1.1537 - thus False by (rule notE [OF _ less])
1.1538 -qed
1.1539 -
1.1540 -lemma inverse_less_imp_less:
1.1541 - "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
1.1542 -apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
1.1543 -apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
1.1544 -done
1.1545 -
1.1546 -text{*Both premises are essential. Consider -1 and 1.*}
1.1547 -lemma inverse_less_iff_less [simp,noatp]:
1.1548 - "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.1549 -by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
1.1550 -
1.1551 -lemma le_imp_inverse_le:
1.1552 - "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.1553 -by (force simp add: order_le_less less_imp_inverse_less)
1.1554 -
1.1555 -lemma inverse_le_iff_le [simp,noatp]:
1.1556 - "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.1557 -by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
1.1558 -
1.1559 -
1.1560 -text{*These results refer to both operands being negative. The opposite-sign
1.1561 -case is trivial, since inverse preserves signs.*}
1.1562 -lemma inverse_le_imp_le_neg:
1.1563 - "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
1.1564 -apply (rule classical)
1.1565 -apply (subgoal_tac "a < 0")
1.1566 - prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
1.1567 -apply (insert inverse_le_imp_le [of "-b" "-a"])
1.1568 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.1569 -done
1.1570 -
1.1571 -lemma less_imp_inverse_less_neg:
1.1572 - "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
1.1573 -apply (subgoal_tac "a < 0")
1.1574 - prefer 2 apply (blast intro: order_less_trans)
1.1575 -apply (insert less_imp_inverse_less [of "-b" "-a"])
1.1576 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.1577 -done
1.1578 -
1.1579 -lemma inverse_less_imp_less_neg:
1.1580 - "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
1.1581 -apply (rule classical)
1.1582 -apply (subgoal_tac "a < 0")
1.1583 - prefer 2
1.1584 - apply (force simp add: linorder_not_less intro: order_le_less_trans)
1.1585 -apply (insert inverse_less_imp_less [of "-b" "-a"])
1.1586 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.1587 -done
1.1588 -
1.1589 -lemma inverse_less_iff_less_neg [simp,noatp]:
1.1590 - "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.1591 -apply (insert inverse_less_iff_less [of "-b" "-a"])
1.1592 -apply (simp del: inverse_less_iff_less
1.1593 - add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.1594 -done
1.1595 -
1.1596 -lemma le_imp_inverse_le_neg:
1.1597 - "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.1598 -by (force simp add: order_le_less less_imp_inverse_less_neg)
1.1599 -
1.1600 -lemma inverse_le_iff_le_neg [simp,noatp]:
1.1601 - "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.1602 -by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
1.1603 -
1.1604 -
1.1605 -subsection{*Inverses and the Number One*}
1.1606 -
1.1607 -lemma one_less_inverse_iff:
1.1608 - "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
1.1609 -proof cases
1.1610 - assume "0 < x"
1.1611 - with inverse_less_iff_less [OF zero_less_one, of x]
1.1612 - show ?thesis by simp
1.1613 -next
1.1614 - assume notless: "~ (0 < x)"
1.1615 - have "~ (1 < inverse x)"
1.1616 - proof
1.1617 - assume "1 < inverse x"
1.1618 - also with notless have "... \<le> 0" by (simp add: linorder_not_less)
1.1619 - also have "... < 1" by (rule zero_less_one)
1.1620 - finally show False by auto
1.1621 - qed
1.1622 - with notless show ?thesis by simp
1.1623 -qed
1.1624 -
1.1625 -lemma inverse_eq_1_iff [simp]:
1.1626 - "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
1.1627 -by (insert inverse_eq_iff_eq [of x 1], simp)
1.1628 -
1.1629 -lemma one_le_inverse_iff:
1.1630 - "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
1.1631 -by (force simp add: order_le_less one_less_inverse_iff zero_less_one
1.1632 - eq_commute [of 1])
1.1633 -
1.1634 -lemma inverse_less_1_iff:
1.1635 - "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
1.1636 -by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)
1.1637 -
1.1638 -lemma inverse_le_1_iff:
1.1639 - "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
1.1640 -by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
1.1641 -
1.1642 -
1.1643 -subsection{*Simplification of Inequalities Involving Literal Divisors*}
1.1644 -
1.1645 -lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
1.1646 -proof -
1.1647 - assume less: "0<c"
1.1648 - hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
1.1649 - by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1.1650 - also have "... = (a*c \<le> b)"
1.1651 - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1.1652 - finally show ?thesis .
1.1653 -qed
1.1654 -
1.1655 -lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
1.1656 -proof -
1.1657 - assume less: "c<0"
1.1658 - hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
1.1659 - by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1.1660 - also have "... = (b \<le> a*c)"
1.1661 - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1.1662 - finally show ?thesis .
1.1663 -qed
1.1664 -
1.1665 -lemma le_divide_eq:
1.1666 - "(a \<le> b/c) =
1.1667 - (if 0 < c then a*c \<le> b
1.1668 - else if c < 0 then b \<le> a*c
1.1669 - else a \<le> (0::'a::{ordered_field,division_by_zero}))"
1.1670 -apply (cases "c=0", simp)
1.1671 -apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
1.1672 -done
1.1673 -
1.1674 -lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
1.1675 -proof -
1.1676 - assume less: "0<c"
1.1677 - hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
1.1678 - by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1.1679 - also have "... = (b \<le> a*c)"
1.1680 - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1.1681 - finally show ?thesis .
1.1682 -qed
1.1683 -
1.1684 -lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
1.1685 -proof -
1.1686 - assume less: "c<0"
1.1687 - hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
1.1688 - by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
1.1689 - also have "... = (a*c \<le> b)"
1.1690 - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1.1691 - finally show ?thesis .
1.1692 -qed
1.1693 -
1.1694 -lemma divide_le_eq:
1.1695 - "(b/c \<le> a) =
1.1696 - (if 0 < c then b \<le> a*c
1.1697 - else if c < 0 then a*c \<le> b
1.1698 - else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1.1699 -apply (cases "c=0", simp)
1.1700 -apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
1.1701 -done
1.1702 -
1.1703 -lemma pos_less_divide_eq:
1.1704 - "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
1.1705 -proof -
1.1706 - assume less: "0<c"
1.1707 - hence "(a < b/c) = (a*c < (b/c)*c)"
1.1708 - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1.1709 - also have "... = (a*c < b)"
1.1710 - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1.1711 - finally show ?thesis .
1.1712 -qed
1.1713 -
1.1714 -lemma neg_less_divide_eq:
1.1715 - "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
1.1716 -proof -
1.1717 - assume less: "c<0"
1.1718 - hence "(a < b/c) = ((b/c)*c < a*c)"
1.1719 - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1.1720 - also have "... = (b < a*c)"
1.1721 - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1.1722 - finally show ?thesis .
1.1723 -qed
1.1724 -
1.1725 -lemma less_divide_eq:
1.1726 - "(a < b/c) =
1.1727 - (if 0 < c then a*c < b
1.1728 - else if c < 0 then b < a*c
1.1729 - else a < (0::'a::{ordered_field,division_by_zero}))"
1.1730 -apply (cases "c=0", simp)
1.1731 -apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
1.1732 -done
1.1733 -
1.1734 -lemma pos_divide_less_eq:
1.1735 - "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
1.1736 -proof -
1.1737 - assume less: "0<c"
1.1738 - hence "(b/c < a) = ((b/c)*c < a*c)"
1.1739 - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1.1740 - also have "... = (b < a*c)"
1.1741 - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
1.1742 - finally show ?thesis .
1.1743 -qed
1.1744 -
1.1745 -lemma neg_divide_less_eq:
1.1746 - "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
1.1747 -proof -
1.1748 - assume less: "c<0"
1.1749 - hence "(b/c < a) = (a*c < (b/c)*c)"
1.1750 - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
1.1751 - also have "... = (a*c < b)"
1.1752 - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
1.1753 - finally show ?thesis .
1.1754 -qed
1.1755 -
1.1756 -lemma divide_less_eq:
1.1757 - "(b/c < a) =
1.1758 - (if 0 < c then b < a*c
1.1759 - else if c < 0 then a*c < b
1.1760 - else 0 < (a::'a::{ordered_field,division_by_zero}))"
1.1761 -apply (cases "c=0", simp)
1.1762 -apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
1.1763 -done
1.1764 -
1.1765 -
1.1766 -subsection{*Field simplification*}
1.1767 -
1.1768 -text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
1.1769 -if they can be proved to be non-zero (for equations) or positive/negative
1.1770 -(for inequations). Can be too aggressive and is therefore separate from the
1.1771 -more benign @{text algebra_simps}. *}
1.1772 -
1.1773 -lemmas field_simps[noatp] = field_eq_simps
1.1774 - (* multiply ineqn *)
1.1775 - pos_divide_less_eq neg_divide_less_eq
1.1776 - pos_less_divide_eq neg_less_divide_eq
1.1777 - pos_divide_le_eq neg_divide_le_eq
1.1778 - pos_le_divide_eq neg_le_divide_eq
1.1779 -
1.1780 -text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
1.1781 -of positivity/negativity needed for @{text field_simps}. Have not added @{text
1.1782 -sign_simps} to @{text field_simps} because the former can lead to case
1.1783 -explosions. *}
1.1784 -
1.1785 -lemmas sign_simps[noatp] = group_simps
1.1786 - zero_less_mult_iff mult_less_0_iff
1.1787 -
1.1788 -(* Only works once linear arithmetic is installed:
1.1789 -text{*An example:*}
1.1790 -lemma fixes a b c d e f :: "'a::ordered_field"
1.1791 -shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
1.1792 - ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
1.1793 - ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
1.1794 -apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
1.1795 - prefer 2 apply(simp add:sign_simps)
1.1796 -apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
1.1797 - prefer 2 apply(simp add:sign_simps)
1.1798 -apply(simp add:field_simps)
1.1799 -done
1.1800 -*)
1.1801 -
1.1802 -
1.1803 -subsection{*Division and Signs*}
1.1804 -
1.1805 -lemma zero_less_divide_iff:
1.1806 - "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
1.1807 -by (simp add: divide_inverse zero_less_mult_iff)
1.1808 -
1.1809 -lemma divide_less_0_iff:
1.1810 - "(a/b < (0::'a::{ordered_field,division_by_zero})) =
1.1811 - (0 < a & b < 0 | a < 0 & 0 < b)"
1.1812 -by (simp add: divide_inverse mult_less_0_iff)
1.1813 -
1.1814 -lemma zero_le_divide_iff:
1.1815 - "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
1.1816 - (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
1.1817 -by (simp add: divide_inverse zero_le_mult_iff)
1.1818 -
1.1819 -lemma divide_le_0_iff:
1.1820 - "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
1.1821 - (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
1.1822 -by (simp add: divide_inverse mult_le_0_iff)
1.1823 -
1.1824 -lemma divide_eq_0_iff [simp,noatp]:
1.1825 - "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
1.1826 -by (simp add: divide_inverse)
1.1827 -
1.1828 -lemma divide_pos_pos:
1.1829 - "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
1.1830 -by(simp add:field_simps)
1.1831 -
1.1832 -
1.1833 -lemma divide_nonneg_pos:
1.1834 - "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
1.1835 -by(simp add:field_simps)
1.1836 -
1.1837 -lemma divide_neg_pos:
1.1838 - "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
1.1839 -by(simp add:field_simps)
1.1840 -
1.1841 -lemma divide_nonpos_pos:
1.1842 - "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
1.1843 -by(simp add:field_simps)
1.1844 -
1.1845 -lemma divide_pos_neg:
1.1846 - "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
1.1847 -by(simp add:field_simps)
1.1848 -
1.1849 -lemma divide_nonneg_neg:
1.1850 - "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0"
1.1851 -by(simp add:field_simps)
1.1852 -
1.1853 -lemma divide_neg_neg:
1.1854 - "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
1.1855 -by(simp add:field_simps)
1.1856 -
1.1857 -lemma divide_nonpos_neg:
1.1858 - "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
1.1859 -by(simp add:field_simps)
1.1860 -
1.1861 -
1.1862 -subsection{*Cancellation Laws for Division*}
1.1863 -
1.1864 -lemma divide_cancel_right [simp,noatp]:
1.1865 - "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1.1866 -apply (cases "c=0", simp)
1.1867 -apply (simp add: divide_inverse)
1.1868 -done
1.1869 -
1.1870 -lemma divide_cancel_left [simp,noatp]:
1.1871 - "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1.1872 -apply (cases "c=0", simp)
1.1873 -apply (simp add: divide_inverse)
1.1874 -done
1.1875 -
1.1876 -
1.1877 -subsection {* Division and the Number One *}
1.1878 -
1.1879 -text{*Simplify expressions equated with 1*}
1.1880 -lemma divide_eq_1_iff [simp,noatp]:
1.1881 - "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1.1882 -apply (cases "b=0", simp)
1.1883 -apply (simp add: right_inverse_eq)
1.1884 -done
1.1885 -
1.1886 -lemma one_eq_divide_iff [simp,noatp]:
1.1887 - "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1.1888 -by (simp add: eq_commute [of 1])
1.1889 -
1.1890 -lemma zero_eq_1_divide_iff [simp,noatp]:
1.1891 - "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
1.1892 -apply (cases "a=0", simp)
1.1893 -apply (auto simp add: nonzero_eq_divide_eq)
1.1894 -done
1.1895 -
1.1896 -lemma one_divide_eq_0_iff [simp,noatp]:
1.1897 - "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
1.1898 -apply (cases "a=0", simp)
1.1899 -apply (insert zero_neq_one [THEN not_sym])
1.1900 -apply (auto simp add: nonzero_divide_eq_eq)
1.1901 -done
1.1902 -
1.1903 -text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
1.1904 -lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
1.1905 -lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
1.1906 -lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
1.1907 -lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
1.1908 -
1.1909 -declare zero_less_divide_1_iff [simp,noatp]
1.1910 -declare divide_less_0_1_iff [simp,noatp]
1.1911 -declare zero_le_divide_1_iff [simp,noatp]
1.1912 -declare divide_le_0_1_iff [simp,noatp]
1.1913 -
1.1914 -
1.1915 -subsection {* Ordering Rules for Division *}
1.1916 -
1.1917 -lemma divide_strict_right_mono:
1.1918 - "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
1.1919 -by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono
1.1920 - positive_imp_inverse_positive)
1.1921 -
1.1922 -lemma divide_right_mono:
1.1923 - "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
1.1924 -by (force simp add: divide_strict_right_mono order_le_less)
1.1925 -
1.1926 -lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1.1927 - ==> c <= 0 ==> b / c <= a / c"
1.1928 -apply (drule divide_right_mono [of _ _ "- c"])
1.1929 -apply auto
1.1930 -done
1.1931 -
1.1932 -lemma divide_strict_right_mono_neg:
1.1933 - "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
1.1934 -apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
1.1935 -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
1.1936 -done
1.1937 -
1.1938 -text{*The last premise ensures that @{term a} and @{term b}
1.1939 - have the same sign*}
1.1940 -lemma divide_strict_left_mono:
1.1941 - "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.1942 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
1.1943 -
1.1944 -lemma divide_left_mono:
1.1945 - "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
1.1946 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
1.1947 -
1.1948 -lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1.1949 - ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
1.1950 - apply (drule divide_left_mono [of _ _ "- c"])
1.1951 - apply (auto simp add: mult_commute)
1.1952 -done
1.1953 -
1.1954 -lemma divide_strict_left_mono_neg:
1.1955 - "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.1956 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
1.1957 -
1.1958 -
1.1959 -text{*Simplify quotients that are compared with the value 1.*}
1.1960 -
1.1961 -lemma le_divide_eq_1 [noatp]:
1.1962 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1963 - shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
1.1964 -by (auto simp add: le_divide_eq)
1.1965 -
1.1966 -lemma divide_le_eq_1 [noatp]:
1.1967 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1968 - shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
1.1969 -by (auto simp add: divide_le_eq)
1.1970 -
1.1971 -lemma less_divide_eq_1 [noatp]:
1.1972 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1973 - shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
1.1974 -by (auto simp add: less_divide_eq)
1.1975 -
1.1976 -lemma divide_less_eq_1 [noatp]:
1.1977 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1978 - shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
1.1979 -by (auto simp add: divide_less_eq)
1.1980 -
1.1981 -
1.1982 -subsection{*Conditional Simplification Rules: No Case Splits*}
1.1983 -
1.1984 -lemma le_divide_eq_1_pos [simp,noatp]:
1.1985 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1986 - shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
1.1987 -by (auto simp add: le_divide_eq)
1.1988 -
1.1989 -lemma le_divide_eq_1_neg [simp,noatp]:
1.1990 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1991 - shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
1.1992 -by (auto simp add: le_divide_eq)
1.1993 -
1.1994 -lemma divide_le_eq_1_pos [simp,noatp]:
1.1995 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.1996 - shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
1.1997 -by (auto simp add: divide_le_eq)
1.1998 -
1.1999 -lemma divide_le_eq_1_neg [simp,noatp]:
1.2000 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2001 - shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
1.2002 -by (auto simp add: divide_le_eq)
1.2003 -
1.2004 -lemma less_divide_eq_1_pos [simp,noatp]:
1.2005 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2006 - shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
1.2007 -by (auto simp add: less_divide_eq)
1.2008 -
1.2009 -lemma less_divide_eq_1_neg [simp,noatp]:
1.2010 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2011 - shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
1.2012 -by (auto simp add: less_divide_eq)
1.2013 -
1.2014 -lemma divide_less_eq_1_pos [simp,noatp]:
1.2015 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2016 - shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
1.2017 -by (auto simp add: divide_less_eq)
1.2018 -
1.2019 -lemma divide_less_eq_1_neg [simp,noatp]:
1.2020 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2021 - shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
1.2022 -by (auto simp add: divide_less_eq)
1.2023 -
1.2024 -lemma eq_divide_eq_1 [simp,noatp]:
1.2025 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2026 - shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
1.2027 -by (auto simp add: eq_divide_eq)
1.2028 -
1.2029 -lemma divide_eq_eq_1 [simp,noatp]:
1.2030 - fixes a :: "'a :: {ordered_field,division_by_zero}"
1.2031 - shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
1.2032 -by (auto simp add: divide_eq_eq)
1.2033 -
1.2034 -
1.2035 -subsection {* Reasoning about inequalities with division *}
1.2036 -
1.2037 -lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
1.2038 - ==> x * y <= x"
1.2039 -by (auto simp add: mult_compare_simps)
1.2040 -
1.2041 -lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
1.2042 - ==> y * x <= x"
1.2043 -by (auto simp add: mult_compare_simps)
1.2044 -
1.2045 -lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
1.2046 - x / y <= z"
1.2047 -by (subst pos_divide_le_eq, assumption+)
1.2048 -
1.2049 -lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
1.2050 - z <= x / y"
1.2051 -by(simp add:field_simps)
1.2052 -
1.2053 -lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
1.2054 - x / y < z"
1.2055 -by(simp add:field_simps)
1.2056 -
1.2057 -lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
1.2058 - z < x / y"
1.2059 -by(simp add:field_simps)
1.2060 -
1.2061 -lemma frac_le: "(0::'a::ordered_field) <= x ==>
1.2062 - x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w"
1.2063 - apply (rule mult_imp_div_pos_le)
1.2064 - apply simp
1.2065 - apply (subst times_divide_eq_left)
1.2066 - apply (rule mult_imp_le_div_pos, assumption)
1.2067 - apply (rule mult_mono)
1.2068 - apply simp_all
1.2069 -done
1.2070 -
1.2071 -lemma frac_less: "(0::'a::ordered_field) <= x ==>
1.2072 - x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
1.2073 - apply (rule mult_imp_div_pos_less)
1.2074 - apply simp
1.2075 - apply (subst times_divide_eq_left)
1.2076 - apply (rule mult_imp_less_div_pos, assumption)
1.2077 - apply (erule mult_less_le_imp_less)
1.2078 - apply simp_all
1.2079 -done
1.2080 -
1.2081 -lemma frac_less2: "(0::'a::ordered_field) < x ==>
1.2082 - x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
1.2083 - apply (rule mult_imp_div_pos_less)
1.2084 - apply simp_all
1.2085 - apply (subst times_divide_eq_left)
1.2086 - apply (rule mult_imp_less_div_pos, assumption)
1.2087 - apply (erule mult_le_less_imp_less)
1.2088 - apply simp_all
1.2089 -done
1.2090 -
1.2091 -text{*It's not obvious whether these should be simprules or not.
1.2092 - Their effect is to gather terms into one big fraction, like
1.2093 - a*b*c / x*y*z. The rationale for that is unclear, but many proofs
1.2094 - seem to need them.*}
1.2095 -
1.2096 -declare times_divide_eq [simp]
1.2097 -
1.2098 -
1.2099 -subsection {* Ordered Fields are Dense *}
1.2100 -
1.2101 -context ordered_semidom
1.2102 -begin
1.2103 -
1.2104 -lemma less_add_one: "a < a + 1"
1.2105 -proof -
1.2106 - have "a + 0 < a + 1"
1.2107 - by (blast intro: zero_less_one add_strict_left_mono)
1.2108 - thus ?thesis by simp
1.2109 -qed
1.2110 -
1.2111 -lemma zero_less_two: "0 < 1 + 1"
1.2112 -by (blast intro: less_trans zero_less_one less_add_one)
1.2113 -
1.2114 -end
1.2115 -
1.2116 -lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
1.2117 -by (simp add: field_simps zero_less_two)
1.2118 -
1.2119 -lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
1.2120 -by (simp add: field_simps zero_less_two)
1.2121 -
1.2122 -instance ordered_field < dense_linear_order
1.2123 -proof
1.2124 - fix x y :: 'a
1.2125 - have "x < x + 1" by simp
1.2126 - then show "\<exists>y. x < y" ..
1.2127 - have "x - 1 < x" by simp
1.2128 - then show "\<exists>y. y < x" ..
1.2129 - show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
1.2130 -qed
1.2131 -
1.2132 -
1.2133 -subsection {* Absolute Value *}
1.2134 -
1.2135 -context ordered_idom
1.2136 -begin
1.2137 -
1.2138 -lemma mult_sgn_abs: "sgn x * abs x = x"
1.2139 - unfolding abs_if sgn_if by auto
1.2140 -
1.2141 -end
1.2142 -
1.2143 -lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
1.2144 -by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
1.2145 -
1.2146 -class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
1.2147 - assumes abs_eq_mult:
1.2148 - "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
1.2149 -
1.2150 -
1.2151 -class lordered_ring = pordered_ring + lordered_ab_group_add_abs
1.2152 -begin
1.2153 -
1.2154 -subclass lordered_ab_group_add_meet ..
1.2155 -subclass lordered_ab_group_add_join ..
1.2156 -
1.2157 -end
1.2158 -
1.2159 -lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"
1.2160 -proof -
1.2161 - let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
1.2162 - let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.2163 - have a: "(abs a) * (abs b) = ?x"
1.2164 - by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
1.2165 - {
1.2166 - fix u v :: 'a
1.2167 - have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
1.2168 - u * v = pprt a * pprt b + pprt a * nprt b +
1.2169 - nprt a * pprt b + nprt a * nprt b"
1.2170 - apply (subst prts[of u], subst prts[of v])
1.2171 - apply (simp add: algebra_simps)
1.2172 - done
1.2173 - }
1.2174 - note b = this[OF refl[of a] refl[of b]]
1.2175 - note addm = add_mono[of "0::'a" _ "0::'a", simplified]
1.2176 - note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
1.2177 - have xy: "- ?x <= ?y"
1.2178 - apply (simp)
1.2179 - apply (rule_tac y="0::'a" in order_trans)
1.2180 - apply (rule addm2)
1.2181 - apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1.2182 - apply (rule addm)
1.2183 - apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1.2184 - done
1.2185 - have yx: "?y <= ?x"
1.2186 - apply (simp add:diff_def)
1.2187 - apply (rule_tac y=0 in order_trans)
1.2188 - apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
1.2189 - apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
1.2190 - done
1.2191 - have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
1.2192 - have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
1.2193 - show ?thesis
1.2194 - apply (rule abs_leI)
1.2195 - apply (simp add: i1)
1.2196 - apply (simp add: i2[simplified minus_le_iff])
1.2197 - done
1.2198 -qed
1.2199 -
1.2200 -instance lordered_ring \<subseteq> pordered_ring_abs
1.2201 -proof
1.2202 - fix a b :: "'a\<Colon> lordered_ring"
1.2203 - assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
1.2204 - show "abs (a*b) = abs a * abs b"
1.2205 -proof -
1.2206 - have s: "(0 <= a*b) | (a*b <= 0)"
1.2207 - apply (auto)
1.2208 - apply (rule_tac split_mult_pos_le)
1.2209 - apply (rule_tac contrapos_np[of "a*b <= 0"])
1.2210 - apply (simp)
1.2211 - apply (rule_tac split_mult_neg_le)
1.2212 - apply (insert prems)
1.2213 - apply (blast)
1.2214 - done
1.2215 - have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1.2216 - by (simp add: prts[symmetric])
1.2217 - show ?thesis
1.2218 - proof cases
1.2219 - assume "0 <= a * b"
1.2220 - then show ?thesis
1.2221 - apply (simp_all add: mulprts abs_prts)
1.2222 - apply (insert prems)
1.2223 - apply (auto simp add:
1.2224 - algebra_simps
1.2225 - iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
1.2226 - iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
1.2227 - apply(drule (1) mult_nonneg_nonpos[of a b], simp)
1.2228 - apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
1.2229 - done
1.2230 - next
1.2231 - assume "~(0 <= a*b)"
1.2232 - with s have "a*b <= 0" by simp
1.2233 - then show ?thesis
1.2234 - apply (simp_all add: mulprts abs_prts)
1.2235 - apply (insert prems)
1.2236 - apply (auto simp add: algebra_simps)
1.2237 - apply(drule (1) mult_nonneg_nonneg[of a b],simp)
1.2238 - apply(drule (1) mult_nonpos_nonpos[of a b],simp)
1.2239 - done
1.2240 - qed
1.2241 -qed
1.2242 -qed
1.2243 -
1.2244 -context ordered_idom
1.2245 -begin
1.2246 -
1.2247 -subclass pordered_ring_abs proof
1.2248 -qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
1.2249 -
1.2250 -lemma abs_mult:
1.2251 - "abs (a * b) = abs a * abs b"
1.2252 - by (rule abs_eq_mult) auto
1.2253 -
1.2254 -lemma abs_mult_self:
1.2255 - "abs a * abs a = a * a"
1.2256 - by (simp add: abs_if)
1.2257 -
1.2258 -end
1.2259 -
1.2260 -lemma nonzero_abs_inverse:
1.2261 - "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
1.2262 -apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq
1.2263 - negative_imp_inverse_negative)
1.2264 -apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)
1.2265 -done
1.2266 -
1.2267 -lemma abs_inverse [simp]:
1.2268 - "abs (inverse (a::'a::{ordered_field,division_by_zero})) =
1.2269 - inverse (abs a)"
1.2270 -apply (cases "a=0", simp)
1.2271 -apply (simp add: nonzero_abs_inverse)
1.2272 -done
1.2273 -
1.2274 -lemma nonzero_abs_divide:
1.2275 - "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
1.2276 -by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
1.2277 -
1.2278 -lemma abs_divide [simp]:
1.2279 - "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
1.2280 -apply (cases "b=0", simp)
1.2281 -apply (simp add: nonzero_abs_divide)
1.2282 -done
1.2283 -
1.2284 -lemma abs_mult_less:
1.2285 - "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
1.2286 -proof -
1.2287 - assume ac: "abs a < c"
1.2288 - hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
1.2289 - assume "abs b < d"
1.2290 - thus ?thesis by (simp add: ac cpos mult_strict_mono)
1.2291 -qed
1.2292 -
1.2293 -lemmas eq_minus_self_iff[noatp] = equal_neg_zero
1.2294 -
1.2295 -lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
1.2296 - unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
1.2297 -
1.2298 -lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"
1.2299 -apply (simp add: order_less_le abs_le_iff)
1.2300 -apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
1.2301 -done
1.2302 -
1.2303 -lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==>
1.2304 - (abs y) * x = abs (y * x)"
1.2305 - apply (subst abs_mult)
1.2306 - apply simp
1.2307 -done
1.2308 -
1.2309 -lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==>
1.2310 - abs x / y = abs (x / y)"
1.2311 - apply (subst abs_divide)
1.2312 - apply (simp add: order_less_imp_le)
1.2313 -done
1.2314 -
1.2315 -
1.2316 -subsection {* Bounds of products via negative and positive Part *}
1.2317 -
1.2318 -lemma mult_le_prts:
1.2319 - assumes
1.2320 - "a1 <= (a::'a::lordered_ring)"
1.2321 - "a <= a2"
1.2322 - "b1 <= b"
1.2323 - "b <= b2"
1.2324 - shows
1.2325 - "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
1.2326 -proof -
1.2327 - have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1.2328 - apply (subst prts[symmetric])+
1.2329 - apply simp
1.2330 - done
1.2331 - then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.2332 - by (simp add: algebra_simps)
1.2333 - moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
1.2334 - by (simp_all add: prems mult_mono)
1.2335 - moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
1.2336 - proof -
1.2337 - have "pprt a * nprt b <= pprt a * nprt b2"
1.2338 - by (simp add: mult_left_mono prems)
1.2339 - moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
1.2340 - by (simp add: mult_right_mono_neg prems)
1.2341 - ultimately show ?thesis
1.2342 - by simp
1.2343 - qed
1.2344 - moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
1.2345 - proof -
1.2346 - have "nprt a * pprt b <= nprt a2 * pprt b"
1.2347 - by (simp add: mult_right_mono prems)
1.2348 - moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
1.2349 - by (simp add: mult_left_mono_neg prems)
1.2350 - ultimately show ?thesis
1.2351 - by simp
1.2352 - qed
1.2353 - moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
1.2354 - proof -
1.2355 - have "nprt a * nprt b <= nprt a * nprt b1"
1.2356 - by (simp add: mult_left_mono_neg prems)
1.2357 - moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
1.2358 - by (simp add: mult_right_mono_neg prems)
1.2359 - ultimately show ?thesis
1.2360 - by simp
1.2361 - qed
1.2362 - ultimately show ?thesis
1.2363 - by - (rule add_mono | simp)+
1.2364 -qed
1.2365 -
1.2366 -lemma mult_ge_prts:
1.2367 - assumes
1.2368 - "a1 <= (a::'a::lordered_ring)"
1.2369 - "a <= a2"
1.2370 - "b1 <= b"
1.2371 - "b <= b2"
1.2372 - shows
1.2373 - "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
1.2374 -proof -
1.2375 - from prems have a1:"- a2 <= -a" by auto
1.2376 - from prems have a2: "-a <= -a1" by auto
1.2377 - from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]
1.2378 - have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp
1.2379 - then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
1.2380 - by (simp only: minus_le_iff)
1.2381 - then show ?thesis by simp
1.2382 -qed
1.2383 -
1.2384 -
1.2385 -code_modulename SML
1.2386 - Ring_and_Field Arith
1.2387 -
1.2388 -code_modulename OCaml
1.2389 - Ring_and_Field Arith
1.2390 -
1.2391 -code_modulename Haskell
1.2392 - Ring_and_Field Arith
1.2393 -
1.2394 -end