src/HOL/Ring_and_Field.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30242 aea5d7fa7ef5
child 30630 4fbe1401bac2
child 30649 57753e0ec1d4
permissions -rw-r--r--
added lemmas
     1 (*  Title:   HOL/Ring_and_Field.thy
     2     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
     3              with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* (Ordered) Rings and Fields *}
     7 
     8 theory Ring_and_Field
     9 imports OrderedGroup
    10 begin
    11 
    12 text {*
    13   The theory of partially ordered rings is taken from the books:
    14   \begin{itemize}
    15   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    16   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    17   \end{itemize}
    18   Most of the used notions can also be looked up in 
    19   \begin{itemize}
    20   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    21   \item \emph{Algebra I} by van der Waerden, Springer.
    22   \end{itemize}
    23 *}
    24 
    25 class semiring = ab_semigroup_add + semigroup_mult +
    26   assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"
    27   assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"
    28 begin
    29 
    30 text{*For the @{text combine_numerals} simproc*}
    31 lemma combine_common_factor:
    32   "a * e + (b * e + c) = (a + b) * e + c"
    33 by (simp add: left_distrib add_ac)
    34 
    35 end
    36 
    37 class mult_zero = times + zero +
    38   assumes mult_zero_left [simp]: "0 * a = 0"
    39   assumes mult_zero_right [simp]: "a * 0 = 0"
    40 
    41 class semiring_0 = semiring + comm_monoid_add + mult_zero
    42 
    43 class semiring_0_cancel = semiring + cancel_comm_monoid_add
    44 begin
    45 
    46 subclass semiring_0
    47 proof
    48   fix a :: 'a
    49   have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])
    50   thus "0 * a = 0" by (simp only: add_left_cancel)
    51 next
    52   fix a :: 'a
    53   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])
    54   thus "a * 0 = 0" by (simp only: add_left_cancel)
    55 qed
    56 
    57 end
    58 
    59 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
    60   assumes distrib: "(a + b) * c = a * c + b * c"
    61 begin
    62 
    63 subclass semiring
    64 proof
    65   fix a b c :: 'a
    66   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
    67   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
    68   also have "... = b * a + c * a" by (simp only: distrib)
    69   also have "... = a * b + a * c" by (simp add: mult_ac)
    70   finally show "a * (b + c) = a * b + a * c" by blast
    71 qed
    72 
    73 end
    74 
    75 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
    76 begin
    77 
    78 subclass semiring_0 ..
    79 
    80 end
    81 
    82 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
    83 begin
    84 
    85 subclass semiring_0_cancel ..
    86 
    87 subclass comm_semiring_0 ..
    88 
    89 end
    90 
    91 class zero_neq_one = zero + one +
    92   assumes zero_neq_one [simp]: "0 \<noteq> 1"
    93 begin
    94 
    95 lemma one_neq_zero [simp]: "1 \<noteq> 0"
    96 by (rule not_sym) (rule zero_neq_one)
    97 
    98 end
    99 
   100 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   101 
   102 text {* Abstract divisibility *}
   103 
   104 class dvd = times
   105 begin
   106 
   107 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
   108   [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   109 
   110 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   111   unfolding dvd_def ..
   112 
   113 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   114   unfolding dvd_def by blast 
   115 
   116 end
   117 
   118 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
   119   (*previously almost_semiring*)
   120 begin
   121 
   122 subclass semiring_1 ..
   123 
   124 lemma dvd_refl[simp]: "a dvd a"
   125 proof
   126   show "a = a * 1" by simp
   127 qed
   128 
   129 lemma dvd_trans:
   130   assumes "a dvd b" and "b dvd c"
   131   shows "a dvd c"
   132 proof -
   133   from assms obtain v where "b = a * v" by (auto elim!: dvdE)
   134   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
   135   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   136   then show ?thesis ..
   137 qed
   138 
   139 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
   140 by (auto intro: dvd_refl elim!: dvdE)
   141 
   142 lemma dvd_0_right [iff]: "a dvd 0"
   143 proof
   144   show "0 = a * 0" by simp
   145 qed
   146 
   147 lemma one_dvd [simp]: "1 dvd a"
   148 by (auto intro!: dvdI)
   149 
   150 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
   151 by (auto intro!: mult_left_commute dvdI elim!: dvdE)
   152 
   153 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   154   apply (subst mult_commute)
   155   apply (erule dvd_mult)
   156   done
   157 
   158 lemma dvd_triv_right [simp]: "a dvd b * a"
   159 by (rule dvd_mult) (rule dvd_refl)
   160 
   161 lemma dvd_triv_left [simp]: "a dvd a * b"
   162 by (rule dvd_mult2) (rule dvd_refl)
   163 
   164 lemma mult_dvd_mono:
   165   assumes "a dvd b"
   166     and "c dvd d"
   167   shows "a * c dvd b * d"
   168 proof -
   169   from `a dvd b` obtain b' where "b = a * b'" ..
   170   moreover from `c dvd d` obtain d' where "d = c * d'" ..
   171   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   172   then show ?thesis ..
   173 qed
   174 
   175 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   176 by (simp add: dvd_def mult_assoc, blast)
   177 
   178 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   179   unfolding mult_ac [of a] by (rule dvd_mult_left)
   180 
   181 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   182 by simp
   183 
   184 lemma dvd_add[simp]:
   185   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
   186 proof -
   187   from `a dvd b` obtain b' where "b = a * b'" ..
   188   moreover from `a dvd c` obtain c' where "c = a * c'" ..
   189   ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
   190   then show ?thesis ..
   191 qed
   192 
   193 end
   194 
   195 
   196 class no_zero_divisors = zero + times +
   197   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   198 
   199 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   200   + zero_neq_one + monoid_mult
   201 begin
   202 
   203 subclass semiring_0_cancel ..
   204 
   205 subclass semiring_1 ..
   206 
   207 end
   208 
   209 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
   210   + zero_neq_one + comm_monoid_mult
   211 begin
   212 
   213 subclass semiring_1_cancel ..
   214 subclass comm_semiring_0_cancel ..
   215 subclass comm_semiring_1 ..
   216 
   217 end
   218 
   219 class ring = semiring + ab_group_add
   220 begin
   221 
   222 subclass semiring_0_cancel ..
   223 
   224 text {* Distribution rules *}
   225 
   226 lemma minus_mult_left: "- (a * b) = - a * b"
   227 by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
   228 
   229 lemma minus_mult_right: "- (a * b) = a * - b"
   230 by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
   231 
   232 text{*Extract signs from products*}
   233 lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
   234 lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
   235 
   236 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   237 by simp
   238 
   239 lemma minus_mult_commute: "- a * b = a * - b"
   240 by simp
   241 
   242 lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"
   243 by (simp add: right_distrib diff_minus)
   244 
   245 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
   246 by (simp add: left_distrib diff_minus)
   247 
   248 lemmas ring_distribs[noatp] =
   249   right_distrib left_distrib left_diff_distrib right_diff_distrib
   250 
   251 text{*Legacy - use @{text algebra_simps} *}
   252 lemmas ring_simps[noatp] = algebra_simps
   253 
   254 lemma eq_add_iff1:
   255   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   256 by (simp add: algebra_simps)
   257 
   258 lemma eq_add_iff2:
   259   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   260 by (simp add: algebra_simps)
   261 
   262 end
   263 
   264 lemmas ring_distribs[noatp] =
   265   right_distrib left_distrib left_diff_distrib right_diff_distrib
   266 
   267 class comm_ring = comm_semiring + ab_group_add
   268 begin
   269 
   270 subclass ring ..
   271 subclass comm_semiring_0_cancel ..
   272 
   273 end
   274 
   275 class ring_1 = ring + zero_neq_one + monoid_mult
   276 begin
   277 
   278 subclass semiring_1_cancel ..
   279 
   280 end
   281 
   282 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   283   (*previously ring*)
   284 begin
   285 
   286 subclass ring_1 ..
   287 subclass comm_semiring_1_cancel ..
   288 
   289 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   290 proof
   291   assume "x dvd - y"
   292   then have "x dvd - 1 * - y" by (rule dvd_mult)
   293   then show "x dvd y" by simp
   294 next
   295   assume "x dvd y"
   296   then have "x dvd - 1 * y" by (rule dvd_mult)
   297   then show "x dvd - y" by simp
   298 qed
   299 
   300 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   301 proof
   302   assume "- x dvd y"
   303   then obtain k where "y = - x * k" ..
   304   then have "y = x * - k" by simp
   305   then show "x dvd y" ..
   306 next
   307   assume "x dvd y"
   308   then obtain k where "y = x * k" ..
   309   then have "y = - x * - k" by simp
   310   then show "- x dvd y" ..
   311 qed
   312 
   313 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   314 by (simp add: diff_minus dvd_minus_iff)
   315 
   316 end
   317 
   318 class ring_no_zero_divisors = ring + no_zero_divisors
   319 begin
   320 
   321 lemma mult_eq_0_iff [simp]:
   322   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   323 proof (cases "a = 0 \<or> b = 0")
   324   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   325     then show ?thesis using no_zero_divisors by simp
   326 next
   327   case True then show ?thesis by auto
   328 qed
   329 
   330 text{*Cancellation of equalities with a common factor*}
   331 lemma mult_cancel_right [simp, noatp]:
   332   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   333 proof -
   334   have "(a * c = b * c) = ((a - b) * c = 0)"
   335     by (simp add: algebra_simps right_minus_eq)
   336   thus ?thesis by (simp add: disj_commute right_minus_eq)
   337 qed
   338 
   339 lemma mult_cancel_left [simp, noatp]:
   340   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   341 proof -
   342   have "(c * a = c * b) = (c * (a - b) = 0)"
   343     by (simp add: algebra_simps right_minus_eq)
   344   thus ?thesis by (simp add: right_minus_eq)
   345 qed
   346 
   347 end
   348 
   349 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   350 begin
   351 
   352 lemma mult_cancel_right1 [simp]:
   353   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   354 by (insert mult_cancel_right [of 1 c b], force)
   355 
   356 lemma mult_cancel_right2 [simp]:
   357   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   358 by (insert mult_cancel_right [of a c 1], simp)
   359  
   360 lemma mult_cancel_left1 [simp]:
   361   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   362 by (insert mult_cancel_left [of c 1 b], force)
   363 
   364 lemma mult_cancel_left2 [simp]:
   365   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   366 by (insert mult_cancel_left [of c a 1], simp)
   367 
   368 end
   369 
   370 class idom = comm_ring_1 + no_zero_divisors
   371 begin
   372 
   373 subclass ring_1_no_zero_divisors ..
   374 
   375 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
   376 proof
   377   assume "a * a = b * b"
   378   then have "(a - b) * (a + b) = 0"
   379     by (simp add: algebra_simps)
   380   then show "a = b \<or> a = - b"
   381     by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
   382 next
   383   assume "a = b \<or> a = - b"
   384   then show "a * a = b * b" by auto
   385 qed
   386 
   387 lemma dvd_mult_cancel_right [simp]:
   388   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   389 proof -
   390   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   391     unfolding dvd_def by (simp add: mult_ac)
   392   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   393     unfolding dvd_def by simp
   394   finally show ?thesis .
   395 qed
   396 
   397 lemma dvd_mult_cancel_left [simp]:
   398   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   399 proof -
   400   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   401     unfolding dvd_def by (simp add: mult_ac)
   402   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   403     unfolding dvd_def by simp
   404   finally show ?thesis .
   405 qed
   406 
   407 end
   408 
   409 class division_ring = ring_1 + inverse +
   410   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   411   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   412 begin
   413 
   414 subclass ring_1_no_zero_divisors
   415 proof
   416   fix a b :: 'a
   417   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   418   show "a * b \<noteq> 0"
   419   proof
   420     assume ab: "a * b = 0"
   421     hence "0 = inverse a * (a * b) * inverse b" by simp
   422     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   423       by (simp only: mult_assoc)
   424     also have "\<dots> = 1" using a b by simp
   425     finally show False by simp
   426   qed
   427 qed
   428 
   429 lemma nonzero_imp_inverse_nonzero:
   430   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   431 proof
   432   assume ianz: "inverse a = 0"
   433   assume "a \<noteq> 0"
   434   hence "1 = a * inverse a" by simp
   435   also have "... = 0" by (simp add: ianz)
   436   finally have "1 = 0" .
   437   thus False by (simp add: eq_commute)
   438 qed
   439 
   440 lemma inverse_zero_imp_zero:
   441   "inverse a = 0 \<Longrightarrow> a = 0"
   442 apply (rule classical)
   443 apply (drule nonzero_imp_inverse_nonzero)
   444 apply auto
   445 done
   446 
   447 lemma inverse_unique: 
   448   assumes ab: "a * b = 1"
   449   shows "inverse a = b"
   450 proof -
   451   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   452   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
   453   ultimately show ?thesis by (simp add: mult_assoc [symmetric])
   454 qed
   455 
   456 lemma nonzero_inverse_minus_eq:
   457   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
   458 by (rule inverse_unique) simp
   459 
   460 lemma nonzero_inverse_inverse_eq:
   461   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
   462 by (rule inverse_unique) simp
   463 
   464 lemma nonzero_inverse_eq_imp_eq:
   465   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
   466   shows "a = b"
   467 proof -
   468   from `inverse a = inverse b`
   469   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
   470   with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
   471     by (simp add: nonzero_inverse_inverse_eq)
   472 qed
   473 
   474 lemma inverse_1 [simp]: "inverse 1 = 1"
   475 by (rule inverse_unique) simp
   476 
   477 lemma nonzero_inverse_mult_distrib: 
   478   assumes "a \<noteq> 0" and "b \<noteq> 0"
   479   shows "inverse (a * b) = inverse b * inverse a"
   480 proof -
   481   have "a * (b * inverse b) * inverse a = 1" using assms by simp
   482   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
   483   thus ?thesis by (rule inverse_unique)
   484 qed
   485 
   486 lemma division_ring_inverse_add:
   487   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   488 by (simp add: algebra_simps)
   489 
   490 lemma division_ring_inverse_diff:
   491   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   492 by (simp add: algebra_simps)
   493 
   494 end
   495 
   496 class field = comm_ring_1 + inverse +
   497   assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   498   assumes divide_inverse: "a / b = a * inverse b"
   499 begin
   500 
   501 subclass division_ring
   502 proof
   503   fix a :: 'a
   504   assume "a \<noteq> 0"
   505   thus "inverse a * a = 1" by (rule field_inverse)
   506   thus "a * inverse a = 1" by (simp only: mult_commute)
   507 qed
   508 
   509 subclass idom ..
   510 
   511 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
   512 proof
   513   assume neq: "b \<noteq> 0"
   514   {
   515     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
   516     also assume "a / b = 1"
   517     finally show "a = b" by simp
   518   next
   519     assume "a = b"
   520     with neq show "a / b = 1" by (simp add: divide_inverse)
   521   }
   522 qed
   523 
   524 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
   525 by (simp add: divide_inverse)
   526 
   527 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
   528 by (simp add: divide_inverse)
   529 
   530 lemma divide_zero_left [simp]: "0 / a = 0"
   531 by (simp add: divide_inverse)
   532 
   533 lemma inverse_eq_divide: "inverse a = 1 / a"
   534 by (simp add: divide_inverse)
   535 
   536 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
   537 by (simp add: divide_inverse algebra_simps) 
   538 
   539 end
   540 
   541 class division_by_zero = zero + inverse +
   542   assumes inverse_zero [simp]: "inverse 0 = 0"
   543 
   544 lemma divide_zero [simp]:
   545   "a / 0 = (0::'a::{field,division_by_zero})"
   546 by (simp add: divide_inverse)
   547 
   548 lemma divide_self_if [simp]:
   549   "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   550 by simp
   551 
   552 class mult_mono = times + zero + ord +
   553   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   554   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   555 
   556 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   557 begin
   558 
   559 lemma mult_mono:
   560   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   561      \<Longrightarrow> a * c \<le> b * d"
   562 apply (erule mult_right_mono [THEN order_trans], assumption)
   563 apply (erule mult_left_mono, assumption)
   564 done
   565 
   566 lemma mult_mono':
   567   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   568      \<Longrightarrow> a * c \<le> b * d"
   569 apply (rule mult_mono)
   570 apply (fast intro: order_trans)+
   571 done
   572 
   573 end
   574 
   575 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   576   + semiring + cancel_comm_monoid_add
   577 begin
   578 
   579 subclass semiring_0_cancel ..
   580 subclass pordered_semiring ..
   581 
   582 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   583 by (drule mult_left_mono [of zero b], auto)
   584 
   585 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   586 by (drule mult_left_mono [of b zero], auto)
   587 
   588 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   589 by (drule mult_right_mono [of b zero], auto)
   590 
   591 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   592 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   593 
   594 end
   595 
   596 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   597 begin
   598 
   599 subclass pordered_cancel_semiring ..
   600 
   601 subclass pordered_comm_monoid_add ..
   602 
   603 lemma mult_left_less_imp_less:
   604   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   605 by (force simp add: mult_left_mono not_le [symmetric])
   606  
   607 lemma mult_right_less_imp_less:
   608   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   609 by (force simp add: mult_right_mono not_le [symmetric])
   610 
   611 end
   612 
   613 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   614   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   615   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   616 begin
   617 
   618 subclass semiring_0_cancel ..
   619 
   620 subclass ordered_semiring
   621 proof
   622   fix a b c :: 'a
   623   assume A: "a \<le> b" "0 \<le> c"
   624   from A show "c * a \<le> c * b"
   625     unfolding le_less
   626     using mult_strict_left_mono by (cases "c = 0") auto
   627   from A show "a * c \<le> b * c"
   628     unfolding le_less
   629     using mult_strict_right_mono by (cases "c = 0") auto
   630 qed
   631 
   632 lemma mult_left_le_imp_le:
   633   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   634 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   635  
   636 lemma mult_right_le_imp_le:
   637   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   638 by (force simp add: mult_strict_right_mono not_less [symmetric])
   639 
   640 lemma mult_pos_pos:
   641   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   642 by (drule mult_strict_left_mono [of zero b], auto)
   643 
   644 lemma mult_pos_neg:
   645   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   646 by (drule mult_strict_left_mono [of b zero], auto)
   647 
   648 lemma mult_pos_neg2:
   649   "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   650 by (drule mult_strict_right_mono [of b zero], auto)
   651 
   652 lemma zero_less_mult_pos:
   653   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   654 apply (cases "b\<le>0") 
   655  apply (auto simp add: le_less not_less)
   656 apply (drule_tac mult_pos_neg [of a b]) 
   657  apply (auto dest: less_not_sym)
   658 done
   659 
   660 lemma zero_less_mult_pos2:
   661   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   662 apply (cases "b\<le>0") 
   663  apply (auto simp add: le_less not_less)
   664 apply (drule_tac mult_pos_neg2 [of a b]) 
   665  apply (auto dest: less_not_sym)
   666 done
   667 
   668 text{*Strict monotonicity in both arguments*}
   669 lemma mult_strict_mono:
   670   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   671   shows "a * c < b * d"
   672   using assms apply (cases "c=0")
   673   apply (simp add: mult_pos_pos) 
   674   apply (erule mult_strict_right_mono [THEN less_trans])
   675   apply (force simp add: le_less) 
   676   apply (erule mult_strict_left_mono, assumption)
   677   done
   678 
   679 text{*This weaker variant has more natural premises*}
   680 lemma mult_strict_mono':
   681   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   682   shows "a * c < b * d"
   683 by (rule mult_strict_mono) (insert assms, auto)
   684 
   685 lemma mult_less_le_imp_less:
   686   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   687   shows "a * c < b * d"
   688   using assms apply (subgoal_tac "a * c < b * c")
   689   apply (erule less_le_trans)
   690   apply (erule mult_left_mono)
   691   apply simp
   692   apply (erule mult_strict_right_mono)
   693   apply assumption
   694   done
   695 
   696 lemma mult_le_less_imp_less:
   697   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   698   shows "a * c < b * d"
   699   using assms apply (subgoal_tac "a * c \<le> b * c")
   700   apply (erule le_less_trans)
   701   apply (erule mult_strict_left_mono)
   702   apply simp
   703   apply (erule mult_right_mono)
   704   apply simp
   705   done
   706 
   707 lemma mult_less_imp_less_left:
   708   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   709   shows "a < b"
   710 proof (rule ccontr)
   711   assume "\<not>  a < b"
   712   hence "b \<le> a" by (simp add: linorder_not_less)
   713   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   714   with this and less show False by (simp add: not_less [symmetric])
   715 qed
   716 
   717 lemma mult_less_imp_less_right:
   718   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   719   shows "a < b"
   720 proof (rule ccontr)
   721   assume "\<not> a < b"
   722   hence "b \<le> a" by (simp add: linorder_not_less)
   723   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   724   with this and less show False by (simp add: not_less [symmetric])
   725 qed  
   726 
   727 end
   728 
   729 class mult_mono1 = times + zero + ord +
   730   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   731 
   732 class pordered_comm_semiring = comm_semiring_0
   733   + pordered_ab_semigroup_add + mult_mono1
   734 begin
   735 
   736 subclass pordered_semiring
   737 proof
   738   fix a b c :: 'a
   739   assume "a \<le> b" "0 \<le> c"
   740   thus "c * a \<le> c * b" by (rule mult_mono1)
   741   thus "a * c \<le> b * c" by (simp only: mult_commute)
   742 qed
   743 
   744 end
   745 
   746 class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   747   + pordered_ab_semigroup_add + mult_mono1
   748 begin
   749 
   750 subclass pordered_comm_semiring ..
   751 subclass pordered_cancel_semiring ..
   752 
   753 end
   754 
   755 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   756   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   757 begin
   758 
   759 subclass ordered_semiring_strict
   760 proof
   761   fix a b c :: 'a
   762   assume "a < b" "0 < c"
   763   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   764   thus "a * c < b * c" by (simp only: mult_commute)
   765 qed
   766 
   767 subclass pordered_cancel_comm_semiring
   768 proof
   769   fix a b c :: 'a
   770   assume "a \<le> b" "0 \<le> c"
   771   thus "c * a \<le> c * b"
   772     unfolding le_less
   773     using mult_strict_left_mono by (cases "c = 0") auto
   774 qed
   775 
   776 end
   777 
   778 class pordered_ring = ring + pordered_cancel_semiring 
   779 begin
   780 
   781 subclass pordered_ab_group_add ..
   782 
   783 text{*Legacy - use @{text algebra_simps} *}
   784 lemmas ring_simps[noatp] = algebra_simps
   785 
   786 lemma less_add_iff1:
   787   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   788 by (simp add: algebra_simps)
   789 
   790 lemma less_add_iff2:
   791   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   792 by (simp add: algebra_simps)
   793 
   794 lemma le_add_iff1:
   795   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   796 by (simp add: algebra_simps)
   797 
   798 lemma le_add_iff2:
   799   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   800 by (simp add: algebra_simps)
   801 
   802 lemma mult_left_mono_neg:
   803   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   804   apply (drule mult_left_mono [of _ _ "uminus c"])
   805   apply (simp_all add: minus_mult_left [symmetric]) 
   806   done
   807 
   808 lemma mult_right_mono_neg:
   809   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   810   apply (drule mult_right_mono [of _ _ "uminus c"])
   811   apply (simp_all add: minus_mult_right [symmetric]) 
   812   done
   813 
   814 lemma mult_nonpos_nonpos:
   815   "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   816 by (drule mult_right_mono_neg [of a zero b]) auto
   817 
   818 lemma split_mult_pos_le:
   819   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   820 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   821 
   822 end
   823 
   824 class abs_if = minus + uminus + ord + zero + abs +
   825   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
   826 
   827 class sgn_if = minus + uminus + zero + one + ord + sgn +
   828   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   829 
   830 lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
   831 by(simp add:sgn_if)
   832 
   833 class ordered_ring = ring + ordered_semiring
   834   + ordered_ab_group_add + abs_if
   835 begin
   836 
   837 subclass pordered_ring ..
   838 
   839 subclass pordered_ab_group_add_abs
   840 proof
   841   fix a b
   842   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   843 by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   844    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
   845      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
   846       auto intro!: less_imp_le add_neg_neg)
   847 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
   848 
   849 end
   850 
   851 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
   852    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
   853  *)
   854 class ordered_ring_strict = ring + ordered_semiring_strict
   855   + ordered_ab_group_add + abs_if
   856 begin
   857 
   858 subclass ordered_ring ..
   859 
   860 lemma mult_strict_left_mono_neg:
   861   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   862   apply (drule mult_strict_left_mono [of _ _ "uminus c"])
   863   apply (simp_all add: minus_mult_left [symmetric]) 
   864   done
   865 
   866 lemma mult_strict_right_mono_neg:
   867   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   868   apply (drule mult_strict_right_mono [of _ _ "uminus c"])
   869   apply (simp_all add: minus_mult_right [symmetric]) 
   870   done
   871 
   872 lemma mult_neg_neg:
   873   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   874 by (drule mult_strict_right_mono_neg, auto)
   875 
   876 subclass ring_no_zero_divisors
   877 proof
   878   fix a b
   879   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   880   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   881   have "a * b < 0 \<or> 0 < a * b"
   882   proof (cases "a < 0")
   883     case True note A' = this
   884     show ?thesis proof (cases "b < 0")
   885       case True with A'
   886       show ?thesis by (auto dest: mult_neg_neg)
   887     next
   888       case False with B have "0 < b" by auto
   889       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   890     qed
   891   next
   892     case False with A have A': "0 < a" by auto
   893     show ?thesis proof (cases "b < 0")
   894       case True with A'
   895       show ?thesis by (auto dest: mult_strict_right_mono_neg)
   896     next
   897       case False with B have "0 < b" by auto
   898       with A' show ?thesis by (auto dest: mult_pos_pos)
   899     qed
   900   qed
   901   then show "a * b \<noteq> 0" by (simp add: neq_iff)
   902 qed
   903 
   904 lemma zero_less_mult_iff:
   905   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   906   apply (auto simp add: mult_pos_pos mult_neg_neg)
   907   apply (simp_all add: not_less le_less)
   908   apply (erule disjE) apply assumption defer
   909   apply (erule disjE) defer apply (drule sym) apply simp
   910   apply (erule disjE) defer apply (drule sym) apply simp
   911   apply (erule disjE) apply assumption apply (drule sym) apply simp
   912   apply (drule sym) apply simp
   913   apply (blast dest: zero_less_mult_pos)
   914   apply (blast dest: zero_less_mult_pos2)
   915   done
   916 
   917 lemma zero_le_mult_iff:
   918   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   919 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
   920 
   921 lemma mult_less_0_iff:
   922   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   923   apply (insert zero_less_mult_iff [of "-a" b]) 
   924   apply (force simp add: minus_mult_left[symmetric]) 
   925   done
   926 
   927 lemma mult_le_0_iff:
   928   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   929   apply (insert zero_le_mult_iff [of "-a" b]) 
   930   apply (force simp add: minus_mult_left[symmetric]) 
   931   done
   932 
   933 lemma zero_le_square [simp]: "0 \<le> a * a"
   934 by (simp add: zero_le_mult_iff linear)
   935 
   936 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   937 by (simp add: not_less)
   938 
   939 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   940    also with the relations @{text "\<le>"} and equality.*}
   941 
   942 text{*These ``disjunction'' versions produce two cases when the comparison is
   943  an assumption, but effectively four when the comparison is a goal.*}
   944 
   945 lemma mult_less_cancel_right_disj:
   946   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   947   apply (cases "c = 0")
   948   apply (auto simp add: neq_iff mult_strict_right_mono 
   949                       mult_strict_right_mono_neg)
   950   apply (auto simp add: not_less 
   951                       not_le [symmetric, of "a*c"]
   952                       not_le [symmetric, of a])
   953   apply (erule_tac [!] notE)
   954   apply (auto simp add: less_imp_le mult_right_mono 
   955                       mult_right_mono_neg)
   956   done
   957 
   958 lemma mult_less_cancel_left_disj:
   959   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   960   apply (cases "c = 0")
   961   apply (auto simp add: neq_iff mult_strict_left_mono 
   962                       mult_strict_left_mono_neg)
   963   apply (auto simp add: not_less 
   964                       not_le [symmetric, of "c*a"]
   965                       not_le [symmetric, of a])
   966   apply (erule_tac [!] notE)
   967   apply (auto simp add: less_imp_le mult_left_mono 
   968                       mult_left_mono_neg)
   969   done
   970 
   971 text{*The ``conjunction of implication'' lemmas produce two cases when the
   972 comparison is a goal, but give four when the comparison is an assumption.*}
   973 
   974 lemma mult_less_cancel_right:
   975   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   976   using mult_less_cancel_right_disj [of a c b] by auto
   977 
   978 lemma mult_less_cancel_left:
   979   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   980   using mult_less_cancel_left_disj [of c a b] by auto
   981 
   982 lemma mult_le_cancel_right:
   983    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   984 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
   985 
   986 lemma mult_le_cancel_left:
   987   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   988 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
   989 
   990 end
   991 
   992 text{*Legacy - use @{text algebra_simps} *}
   993 lemmas ring_simps[noatp] = algebra_simps
   994 
   995 
   996 class pordered_comm_ring = comm_ring + pordered_comm_semiring
   997 begin
   998 
   999 subclass pordered_ring ..
  1000 subclass pordered_cancel_comm_semiring ..
  1001 
  1002 end
  1003 
  1004 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
  1005   (*previously ordered_semiring*)
  1006   assumes zero_less_one [simp]: "0 < 1"
  1007 begin
  1008 
  1009 lemma pos_add_strict:
  1010   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1011   using add_strict_mono [of zero a b c] by simp
  1012 
  1013 lemma zero_le_one [simp]: "0 \<le> 1"
  1014 by (rule zero_less_one [THEN less_imp_le]) 
  1015 
  1016 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1017 by (simp add: not_le) 
  1018 
  1019 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1020 by (simp add: not_less) 
  1021 
  1022 lemma less_1_mult:
  1023   assumes "1 < m" and "1 < n"
  1024   shows "1 < m * n"
  1025   using assms mult_strict_mono [of 1 m 1 n]
  1026     by (simp add:  less_trans [OF zero_less_one]) 
  1027 
  1028 end
  1029 
  1030 class ordered_idom = comm_ring_1 +
  1031   ordered_comm_semiring_strict + ordered_ab_group_add +
  1032   abs_if + sgn_if
  1033   (*previously ordered_ring*)
  1034 begin
  1035 
  1036 subclass ordered_ring_strict ..
  1037 subclass pordered_comm_ring ..
  1038 subclass idom ..
  1039 
  1040 subclass ordered_semidom
  1041 proof
  1042   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1043   thus "0 < 1" by (simp add: le_less)
  1044 qed 
  1045 
  1046 lemma linorder_neqE_ordered_idom:
  1047   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1048   using assms by (rule neqE)
  1049 
  1050 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1051 
  1052 lemma mult_le_cancel_right1:
  1053   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1054 by (insert mult_le_cancel_right [of 1 c b], simp)
  1055 
  1056 lemma mult_le_cancel_right2:
  1057   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1058 by (insert mult_le_cancel_right [of a c 1], simp)
  1059 
  1060 lemma mult_le_cancel_left1:
  1061   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1062 by (insert mult_le_cancel_left [of c 1 b], simp)
  1063 
  1064 lemma mult_le_cancel_left2:
  1065   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1066 by (insert mult_le_cancel_left [of c a 1], simp)
  1067 
  1068 lemma mult_less_cancel_right1:
  1069   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1070 by (insert mult_less_cancel_right [of 1 c b], simp)
  1071 
  1072 lemma mult_less_cancel_right2:
  1073   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1074 by (insert mult_less_cancel_right [of a c 1], simp)
  1075 
  1076 lemma mult_less_cancel_left1:
  1077   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1078 by (insert mult_less_cancel_left [of c 1 b], simp)
  1079 
  1080 lemma mult_less_cancel_left2:
  1081   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1082 by (insert mult_less_cancel_left [of c a 1], simp)
  1083 
  1084 lemma sgn_sgn [simp]:
  1085   "sgn (sgn a) = sgn a"
  1086 unfolding sgn_if by simp
  1087 
  1088 lemma sgn_0_0:
  1089   "sgn a = 0 \<longleftrightarrow> a = 0"
  1090 unfolding sgn_if by simp
  1091 
  1092 lemma sgn_1_pos:
  1093   "sgn a = 1 \<longleftrightarrow> a > 0"
  1094 unfolding sgn_if by (simp add: neg_equal_zero)
  1095 
  1096 lemma sgn_1_neg:
  1097   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1098 unfolding sgn_if by (auto simp add: equal_neg_zero)
  1099 
  1100 lemma sgn_pos [simp]:
  1101   "0 < a \<Longrightarrow> sgn a = 1"
  1102 unfolding sgn_1_pos .
  1103 
  1104 lemma sgn_neg [simp]:
  1105   "a < 0 \<Longrightarrow> sgn a = - 1"
  1106 unfolding sgn_1_neg .
  1107 
  1108 lemma sgn_times:
  1109   "sgn (a * b) = sgn a * sgn b"
  1110 by (auto simp add: sgn_if zero_less_mult_iff)
  1111 
  1112 lemma abs_sgn: "abs k = k * sgn k"
  1113 unfolding sgn_if abs_if by auto
  1114 
  1115 lemma sgn_greater [simp]:
  1116   "0 < sgn a \<longleftrightarrow> 0 < a"
  1117   unfolding sgn_if by auto
  1118 
  1119 lemma sgn_less [simp]:
  1120   "sgn a < 0 \<longleftrightarrow> a < 0"
  1121   unfolding sgn_if by auto
  1122 
  1123 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  1124   by (simp add: abs_if)
  1125 
  1126 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  1127   by (simp add: abs_if)
  1128 
  1129 end
  1130 
  1131 class ordered_field = field + ordered_idom
  1132 
  1133 text {* Simprules for comparisons where common factors can be cancelled. *}
  1134 
  1135 lemmas mult_compare_simps[noatp] =
  1136     mult_le_cancel_right mult_le_cancel_left
  1137     mult_le_cancel_right1 mult_le_cancel_right2
  1138     mult_le_cancel_left1 mult_le_cancel_left2
  1139     mult_less_cancel_right mult_less_cancel_left
  1140     mult_less_cancel_right1 mult_less_cancel_right2
  1141     mult_less_cancel_left1 mult_less_cancel_left2
  1142     mult_cancel_right mult_cancel_left
  1143     mult_cancel_right1 mult_cancel_right2
  1144     mult_cancel_left1 mult_cancel_left2
  1145 
  1146 -- {* FIXME continue localization here *}
  1147 
  1148 lemma inverse_nonzero_iff_nonzero [simp]:
  1149    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
  1150 by (force dest: inverse_zero_imp_zero) 
  1151 
  1152 lemma inverse_minus_eq [simp]:
  1153    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
  1154 proof cases
  1155   assume "a=0" thus ?thesis by (simp add: inverse_zero)
  1156 next
  1157   assume "a\<noteq>0" 
  1158   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  1159 qed
  1160 
  1161 lemma inverse_eq_imp_eq:
  1162   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
  1163 apply (cases "a=0 | b=0") 
  1164  apply (force dest!: inverse_zero_imp_zero
  1165               simp add: eq_commute [of "0::'a"])
  1166 apply (force dest!: nonzero_inverse_eq_imp_eq) 
  1167 done
  1168 
  1169 lemma inverse_eq_iff_eq [simp]:
  1170   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
  1171 by (force dest!: inverse_eq_imp_eq)
  1172 
  1173 lemma inverse_inverse_eq [simp]:
  1174      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
  1175   proof cases
  1176     assume "a=0" thus ?thesis by simp
  1177   next
  1178     assume "a\<noteq>0" 
  1179     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  1180   qed
  1181 
  1182 text{*This version builds in division by zero while also re-orienting
  1183       the right-hand side.*}
  1184 lemma inverse_mult_distrib [simp]:
  1185      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
  1186   proof cases
  1187     assume "a \<noteq> 0 & b \<noteq> 0" 
  1188     thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
  1189   next
  1190     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
  1191     thus ?thesis by force
  1192   qed
  1193 
  1194 text{*There is no slick version using division by zero.*}
  1195 lemma inverse_add:
  1196   "[|a \<noteq> 0;  b \<noteq> 0|]
  1197    ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
  1198 by (simp add: division_ring_inverse_add mult_ac)
  1199 
  1200 lemma inverse_divide [simp]:
  1201   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  1202 by (simp add: divide_inverse mult_commute)
  1203 
  1204 
  1205 subsection {* Calculations with fractions *}
  1206 
  1207 text{* There is a whole bunch of simp-rules just for class @{text
  1208 field} but none for class @{text field} and @{text nonzero_divides}
  1209 because the latter are covered by a simproc. *}
  1210 
  1211 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
  1212 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
  1213 proof -
  1214   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
  1215     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
  1216   also have "... =  a * inverse b * (inverse c * c)"
  1217     by (simp only: mult_ac)
  1218   also have "... =  a * inverse b" by simp
  1219     finally show ?thesis by (simp add: divide_inverse)
  1220 qed
  1221 
  1222 lemma mult_divide_mult_cancel_left:
  1223   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  1224 apply (cases "b = 0")
  1225 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  1226 done
  1227 
  1228 lemma nonzero_mult_divide_mult_cancel_right [noatp]:
  1229   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
  1230 by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
  1231 
  1232 lemma mult_divide_mult_cancel_right:
  1233   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  1234 apply (cases "b = 0")
  1235 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  1236 done
  1237 
  1238 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
  1239 by (simp add: divide_inverse)
  1240 
  1241 lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
  1242 by (simp add: divide_inverse mult_assoc)
  1243 
  1244 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
  1245 by (simp add: divide_inverse mult_ac)
  1246 
  1247 lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
  1248 
  1249 lemma divide_divide_eq_right [simp,noatp]:
  1250   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  1251 by (simp add: divide_inverse mult_ac)
  1252 
  1253 lemma divide_divide_eq_left [simp,noatp]:
  1254   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  1255 by (simp add: divide_inverse mult_assoc)
  1256 
  1257 lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1258     x / y + w / z = (x * z + w * y) / (y * z)"
  1259 apply (subgoal_tac "x / y = (x * z) / (y * z)")
  1260 apply (erule ssubst)
  1261 apply (subgoal_tac "w / z = (w * y) / (y * z)")
  1262 apply (erule ssubst)
  1263 apply (rule add_divide_distrib [THEN sym])
  1264 apply (subst mult_commute)
  1265 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
  1266 apply assumption
  1267 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
  1268 apply assumption
  1269 done
  1270 
  1271 
  1272 subsubsection{*Special Cancellation Simprules for Division*}
  1273 
  1274 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
  1275 fixes c :: "'a :: {field,division_by_zero}"
  1276 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  1277 by (simp add: mult_divide_mult_cancel_left)
  1278 
  1279 lemma nonzero_mult_divide_cancel_right[simp,noatp]:
  1280   "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
  1281 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
  1282 
  1283 lemma nonzero_mult_divide_cancel_left[simp,noatp]:
  1284   "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
  1285 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
  1286 
  1287 
  1288 lemma nonzero_divide_mult_cancel_right[simp,noatp]:
  1289   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
  1290 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
  1291 
  1292 lemma nonzero_divide_mult_cancel_left[simp,noatp]:
  1293   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
  1294 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
  1295 
  1296 
  1297 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
  1298   "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
  1299 using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
  1300 
  1301 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
  1302   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
  1303 using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
  1304 
  1305 
  1306 subsection {* Division and Unary Minus *}
  1307 
  1308 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
  1309 by (simp add: divide_inverse)
  1310 
  1311 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
  1312 by (simp add: divide_inverse nonzero_inverse_minus_eq)
  1313 
  1314 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
  1315 by (simp add: divide_inverse nonzero_inverse_minus_eq)
  1316 
  1317 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
  1318 by (simp add: divide_inverse)
  1319 
  1320 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1321 by (simp add: divide_inverse)
  1322 
  1323 
  1324 text{*The effect is to extract signs from divisions*}
  1325 lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
  1326 lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
  1327 declare divide_minus_left [simp]   divide_minus_right [simp]
  1328 
  1329 lemma minus_divide_divide [simp]:
  1330   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1331 apply (cases "b=0", simp) 
  1332 apply (simp add: nonzero_minus_divide_divide) 
  1333 done
  1334 
  1335 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
  1336 by (simp add: diff_minus add_divide_distrib) 
  1337 
  1338 lemma add_divide_eq_iff:
  1339   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
  1340 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1341 
  1342 lemma divide_add_eq_iff:
  1343   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
  1344 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1345 
  1346 lemma diff_divide_eq_iff:
  1347   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
  1348 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1349 
  1350 lemma divide_diff_eq_iff:
  1351   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
  1352 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1353 
  1354 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
  1355 proof -
  1356   assume [simp]: "c\<noteq>0"
  1357   have "(a = b/c) = (a*c = (b/c)*c)" by simp
  1358   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
  1359   finally show ?thesis .
  1360 qed
  1361 
  1362 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
  1363 proof -
  1364   assume [simp]: "c\<noteq>0"
  1365   have "(b/c = a) = ((b/c)*c = a*c)"  by simp
  1366   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc) 
  1367   finally show ?thesis .
  1368 qed
  1369 
  1370 lemma eq_divide_eq:
  1371   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1372 by (simp add: nonzero_eq_divide_eq) 
  1373 
  1374 lemma divide_eq_eq:
  1375   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1376 by (force simp add: nonzero_divide_eq_eq) 
  1377 
  1378 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1379     b = a * c ==> b / c = a"
  1380 by (subst divide_eq_eq, simp)
  1381 
  1382 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1383     a * c = b ==> a = b / c"
  1384 by (subst eq_divide_eq, simp)
  1385 
  1386 
  1387 lemmas field_eq_simps[noatp] = algebra_simps
  1388   (* pull / out*)
  1389   add_divide_eq_iff divide_add_eq_iff
  1390   diff_divide_eq_iff divide_diff_eq_iff
  1391   (* multiply eqn *)
  1392   nonzero_eq_divide_eq nonzero_divide_eq_eq
  1393 (* is added later:
  1394   times_divide_eq_left times_divide_eq_right
  1395 *)
  1396 
  1397 text{*An example:*}
  1398 lemma fixes a b c d e f :: "'a::field"
  1399 shows "\<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"
  1400 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
  1401  apply(simp add:field_eq_simps)
  1402 apply(simp)
  1403 done
  1404 
  1405 
  1406 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1407     x / y - w / z = (x * z - w * y) / (y * z)"
  1408 by (simp add:field_eq_simps times_divide_eq)
  1409 
  1410 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1411     (x / y = w / z) = (x * z = w * y)"
  1412 by (simp add:field_eq_simps times_divide_eq)
  1413 
  1414 
  1415 subsection {* Ordered Fields *}
  1416 
  1417 lemma positive_imp_inverse_positive: 
  1418 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
  1419 proof -
  1420   have "0 < a * inverse a" 
  1421     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1422   thus "0 < inverse a" 
  1423     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1424 qed
  1425 
  1426 lemma negative_imp_inverse_negative:
  1427   "a < 0 ==> inverse a < (0::'a::ordered_field)"
  1428 by (insert positive_imp_inverse_positive [of "-a"], 
  1429     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1430 
  1431 lemma inverse_le_imp_le:
  1432 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1433 shows "b \<le> (a::'a::ordered_field)"
  1434 proof (rule classical)
  1435   assume "~ b \<le> a"
  1436   hence "a < b"  by (simp add: linorder_not_le)
  1437   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1438   hence "a * inverse a \<le> a * inverse b"
  1439     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1440   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1441     by (simp add: bpos order_less_imp_le mult_right_mono)
  1442   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1443 qed
  1444 
  1445 lemma inverse_positive_imp_positive:
  1446 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1447 shows "0 < (a::'a::ordered_field)"
  1448 proof -
  1449   have "0 < inverse (inverse a)"
  1450     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1451   thus "0 < a"
  1452     using nz by (simp add: nonzero_inverse_inverse_eq)
  1453 qed
  1454 
  1455 lemma inverse_positive_iff_positive [simp]:
  1456   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1457 apply (cases "a = 0", simp)
  1458 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1459 done
  1460 
  1461 lemma inverse_negative_imp_negative:
  1462 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1463 shows "a < (0::'a::ordered_field)"
  1464 proof -
  1465   have "inverse (inverse a) < 0"
  1466     using inv_less_0 by (rule negative_imp_inverse_negative)
  1467   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1468 qed
  1469 
  1470 lemma inverse_negative_iff_negative [simp]:
  1471   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1472 apply (cases "a = 0", simp)
  1473 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1474 done
  1475 
  1476 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1477   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1478 by (simp add: linorder_not_less [symmetric])
  1479 
  1480 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1481   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1482 by (simp add: linorder_not_less [symmetric])
  1483 
  1484 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
  1485 proof
  1486   fix x::'a
  1487   have m1: "- (1::'a) < 0" by simp
  1488   from add_strict_right_mono[OF m1, where c=x] 
  1489   have "(- 1) + x < x" by simp
  1490   thus "\<exists>y. y < x" by blast
  1491 qed
  1492 
  1493 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
  1494 proof
  1495   fix x::'a
  1496   have m1: " (1::'a) > 0" by simp
  1497   from add_strict_right_mono[OF m1, where c=x] 
  1498   have "1 + x > x" by simp
  1499   thus "\<exists>y. y > x" by blast
  1500 qed
  1501 
  1502 subsection{*Anti-Monotonicity of @{term inverse}*}
  1503 
  1504 lemma less_imp_inverse_less:
  1505 assumes less: "a < b" and apos:  "0 < a"
  1506 shows "inverse b < inverse (a::'a::ordered_field)"
  1507 proof (rule ccontr)
  1508   assume "~ inverse b < inverse a"
  1509   hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
  1510   hence "~ (a < b)"
  1511     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1512   thus False by (rule notE [OF _ less])
  1513 qed
  1514 
  1515 lemma inverse_less_imp_less:
  1516   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1517 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1518 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1519 done
  1520 
  1521 text{*Both premises are essential. Consider -1 and 1.*}
  1522 lemma inverse_less_iff_less [simp,noatp]:
  1523   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1524 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1525 
  1526 lemma le_imp_inverse_le:
  1527   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1528 by (force simp add: order_le_less less_imp_inverse_less)
  1529 
  1530 lemma inverse_le_iff_le [simp,noatp]:
  1531  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1532 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1533 
  1534 
  1535 text{*These results refer to both operands being negative.  The opposite-sign
  1536 case is trivial, since inverse preserves signs.*}
  1537 lemma inverse_le_imp_le_neg:
  1538   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1539 apply (rule classical) 
  1540 apply (subgoal_tac "a < 0") 
  1541  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1542 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1543 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1544 done
  1545 
  1546 lemma less_imp_inverse_less_neg:
  1547    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1548 apply (subgoal_tac "a < 0") 
  1549  prefer 2 apply (blast intro: order_less_trans) 
  1550 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1551 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1552 done
  1553 
  1554 lemma inverse_less_imp_less_neg:
  1555    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1556 apply (rule classical) 
  1557 apply (subgoal_tac "a < 0") 
  1558  prefer 2
  1559  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1560 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1561 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1562 done
  1563 
  1564 lemma inverse_less_iff_less_neg [simp,noatp]:
  1565   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1566 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1567 apply (simp del: inverse_less_iff_less 
  1568             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1569 done
  1570 
  1571 lemma le_imp_inverse_le_neg:
  1572   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1573 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1574 
  1575 lemma inverse_le_iff_le_neg [simp,noatp]:
  1576  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1577 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1578 
  1579 
  1580 subsection{*Inverses and the Number One*}
  1581 
  1582 lemma one_less_inverse_iff:
  1583   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
  1584 proof cases
  1585   assume "0 < x"
  1586     with inverse_less_iff_less [OF zero_less_one, of x]
  1587     show ?thesis by simp
  1588 next
  1589   assume notless: "~ (0 < x)"
  1590   have "~ (1 < inverse x)"
  1591   proof
  1592     assume "1 < inverse x"
  1593     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1594     also have "... < 1" by (rule zero_less_one) 
  1595     finally show False by auto
  1596   qed
  1597   with notless show ?thesis by simp
  1598 qed
  1599 
  1600 lemma inverse_eq_1_iff [simp]:
  1601   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1602 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1603 
  1604 lemma one_le_inverse_iff:
  1605   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
  1606 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1607                     eq_commute [of 1]) 
  1608 
  1609 lemma inverse_less_1_iff:
  1610   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
  1611 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1612 
  1613 lemma inverse_le_1_iff:
  1614   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  1615 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1616 
  1617 
  1618 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1619 
  1620 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1621 proof -
  1622   assume less: "0<c"
  1623   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1624     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1625   also have "... = (a*c \<le> b)"
  1626     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1627   finally show ?thesis .
  1628 qed
  1629 
  1630 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1631 proof -
  1632   assume less: "c<0"
  1633   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1634     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1635   also have "... = (b \<le> a*c)"
  1636     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1637   finally show ?thesis .
  1638 qed
  1639 
  1640 lemma le_divide_eq:
  1641   "(a \<le> b/c) = 
  1642    (if 0 < c then a*c \<le> b
  1643              else if c < 0 then b \<le> a*c
  1644              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1645 apply (cases "c=0", simp) 
  1646 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1647 done
  1648 
  1649 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1650 proof -
  1651   assume less: "0<c"
  1652   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1653     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1654   also have "... = (b \<le> a*c)"
  1655     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1656   finally show ?thesis .
  1657 qed
  1658 
  1659 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1660 proof -
  1661   assume less: "c<0"
  1662   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1663     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1664   also have "... = (a*c \<le> b)"
  1665     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1666   finally show ?thesis .
  1667 qed
  1668 
  1669 lemma divide_le_eq:
  1670   "(b/c \<le> a) = 
  1671    (if 0 < c then b \<le> a*c
  1672              else if c < 0 then a*c \<le> b
  1673              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1674 apply (cases "c=0", simp) 
  1675 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1676 done
  1677 
  1678 lemma pos_less_divide_eq:
  1679      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1680 proof -
  1681   assume less: "0<c"
  1682   hence "(a < b/c) = (a*c < (b/c)*c)"
  1683     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1684   also have "... = (a*c < b)"
  1685     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1686   finally show ?thesis .
  1687 qed
  1688 
  1689 lemma neg_less_divide_eq:
  1690  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1691 proof -
  1692   assume less: "c<0"
  1693   hence "(a < b/c) = ((b/c)*c < a*c)"
  1694     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1695   also have "... = (b < a*c)"
  1696     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1697   finally show ?thesis .
  1698 qed
  1699 
  1700 lemma less_divide_eq:
  1701   "(a < b/c) = 
  1702    (if 0 < c then a*c < b
  1703              else if c < 0 then b < a*c
  1704              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1705 apply (cases "c=0", simp) 
  1706 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1707 done
  1708 
  1709 lemma pos_divide_less_eq:
  1710      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1711 proof -
  1712   assume less: "0<c"
  1713   hence "(b/c < a) = ((b/c)*c < a*c)"
  1714     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1715   also have "... = (b < a*c)"
  1716     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1717   finally show ?thesis .
  1718 qed
  1719 
  1720 lemma neg_divide_less_eq:
  1721  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1722 proof -
  1723   assume less: "c<0"
  1724   hence "(b/c < a) = (a*c < (b/c)*c)"
  1725     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1726   also have "... = (a*c < b)"
  1727     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1728   finally show ?thesis .
  1729 qed
  1730 
  1731 lemma divide_less_eq:
  1732   "(b/c < a) = 
  1733    (if 0 < c then b < a*c
  1734              else if c < 0 then a*c < b
  1735              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1736 apply (cases "c=0", simp) 
  1737 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1738 done
  1739 
  1740 
  1741 subsection{*Field simplification*}
  1742 
  1743 text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
  1744 if they can be proved to be non-zero (for equations) or positive/negative
  1745 (for inequations). Can be too aggressive and is therefore separate from the
  1746 more benign @{text algebra_simps}. *}
  1747 
  1748 lemmas field_simps[noatp] = field_eq_simps
  1749   (* multiply ineqn *)
  1750   pos_divide_less_eq neg_divide_less_eq
  1751   pos_less_divide_eq neg_less_divide_eq
  1752   pos_divide_le_eq neg_divide_le_eq
  1753   pos_le_divide_eq neg_le_divide_eq
  1754 
  1755 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1756 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1757 sign_simps} to @{text field_simps} because the former can lead to case
  1758 explosions. *}
  1759 
  1760 lemmas sign_simps[noatp] = group_simps
  1761   zero_less_mult_iff  mult_less_0_iff
  1762 
  1763 (* Only works once linear arithmetic is installed:
  1764 text{*An example:*}
  1765 lemma fixes a b c d e f :: "'a::ordered_field"
  1766 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1767  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1768  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1769 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1770  prefer 2 apply(simp add:sign_simps)
  1771 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1772  prefer 2 apply(simp add:sign_simps)
  1773 apply(simp add:field_simps)
  1774 done
  1775 *)
  1776 
  1777 
  1778 subsection{*Division and Signs*}
  1779 
  1780 lemma zero_less_divide_iff:
  1781      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1782 by (simp add: divide_inverse zero_less_mult_iff)
  1783 
  1784 lemma divide_less_0_iff:
  1785      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1786       (0 < a & b < 0 | a < 0 & 0 < b)"
  1787 by (simp add: divide_inverse mult_less_0_iff)
  1788 
  1789 lemma zero_le_divide_iff:
  1790      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1791       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1792 by (simp add: divide_inverse zero_le_mult_iff)
  1793 
  1794 lemma divide_le_0_iff:
  1795      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1796       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1797 by (simp add: divide_inverse mult_le_0_iff)
  1798 
  1799 lemma divide_eq_0_iff [simp,noatp]:
  1800      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1801 by (simp add: divide_inverse)
  1802 
  1803 lemma divide_pos_pos:
  1804   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
  1805 by(simp add:field_simps)
  1806 
  1807 
  1808 lemma divide_nonneg_pos:
  1809   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
  1810 by(simp add:field_simps)
  1811 
  1812 lemma divide_neg_pos:
  1813   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1814 by(simp add:field_simps)
  1815 
  1816 lemma divide_nonpos_pos:
  1817   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1818 by(simp add:field_simps)
  1819 
  1820 lemma divide_pos_neg:
  1821   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  1822 by(simp add:field_simps)
  1823 
  1824 lemma divide_nonneg_neg:
  1825   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
  1826 by(simp add:field_simps)
  1827 
  1828 lemma divide_neg_neg:
  1829   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1830 by(simp add:field_simps)
  1831 
  1832 lemma divide_nonpos_neg:
  1833   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1834 by(simp add:field_simps)
  1835 
  1836 
  1837 subsection{*Cancellation Laws for Division*}
  1838 
  1839 lemma divide_cancel_right [simp,noatp]:
  1840      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1841 apply (cases "c=0", simp)
  1842 apply (simp add: divide_inverse)
  1843 done
  1844 
  1845 lemma divide_cancel_left [simp,noatp]:
  1846      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1847 apply (cases "c=0", simp)
  1848 apply (simp add: divide_inverse)
  1849 done
  1850 
  1851 
  1852 subsection {* Division and the Number One *}
  1853 
  1854 text{*Simplify expressions equated with 1*}
  1855 lemma divide_eq_1_iff [simp,noatp]:
  1856      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1857 apply (cases "b=0", simp)
  1858 apply (simp add: right_inverse_eq)
  1859 done
  1860 
  1861 lemma one_eq_divide_iff [simp,noatp]:
  1862      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1863 by (simp add: eq_commute [of 1])
  1864 
  1865 lemma zero_eq_1_divide_iff [simp,noatp]:
  1866      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1867 apply (cases "a=0", simp)
  1868 apply (auto simp add: nonzero_eq_divide_eq)
  1869 done
  1870 
  1871 lemma one_divide_eq_0_iff [simp,noatp]:
  1872      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  1873 apply (cases "a=0", simp)
  1874 apply (insert zero_neq_one [THEN not_sym])
  1875 apply (auto simp add: nonzero_divide_eq_eq)
  1876 done
  1877 
  1878 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1879 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1880 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1881 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1882 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1883 
  1884 declare zero_less_divide_1_iff [simp,noatp]
  1885 declare divide_less_0_1_iff [simp,noatp]
  1886 declare zero_le_divide_1_iff [simp,noatp]
  1887 declare divide_le_0_1_iff [simp,noatp]
  1888 
  1889 
  1890 subsection {* Ordering Rules for Division *}
  1891 
  1892 lemma divide_strict_right_mono:
  1893      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1894 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1895               positive_imp_inverse_positive)
  1896 
  1897 lemma divide_right_mono:
  1898      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1899 by (force simp add: divide_strict_right_mono order_le_less)
  1900 
  1901 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1902     ==> c <= 0 ==> b / c <= a / c"
  1903 apply (drule divide_right_mono [of _ _ "- c"])
  1904 apply auto
  1905 done
  1906 
  1907 lemma divide_strict_right_mono_neg:
  1908      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1909 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1910 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1911 done
  1912 
  1913 text{*The last premise ensures that @{term a} and @{term b} 
  1914       have the same sign*}
  1915 lemma divide_strict_left_mono:
  1916   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1917 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1918 
  1919 lemma divide_left_mono:
  1920   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1921 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1922 
  1923 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1924     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1925   apply (drule divide_left_mono [of _ _ "- c"])
  1926   apply (auto simp add: mult_commute)
  1927 done
  1928 
  1929 lemma divide_strict_left_mono_neg:
  1930   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1931 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1932 
  1933 
  1934 text{*Simplify quotients that are compared with the value 1.*}
  1935 
  1936 lemma le_divide_eq_1 [noatp]:
  1937   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1938   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1939 by (auto simp add: le_divide_eq)
  1940 
  1941 lemma divide_le_eq_1 [noatp]:
  1942   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1943   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1944 by (auto simp add: divide_le_eq)
  1945 
  1946 lemma less_divide_eq_1 [noatp]:
  1947   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1948   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1949 by (auto simp add: less_divide_eq)
  1950 
  1951 lemma divide_less_eq_1 [noatp]:
  1952   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1953   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1954 by (auto simp add: divide_less_eq)
  1955 
  1956 
  1957 subsection{*Conditional Simplification Rules: No Case Splits*}
  1958 
  1959 lemma le_divide_eq_1_pos [simp,noatp]:
  1960   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1961   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1962 by (auto simp add: le_divide_eq)
  1963 
  1964 lemma le_divide_eq_1_neg [simp,noatp]:
  1965   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1966   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1967 by (auto simp add: le_divide_eq)
  1968 
  1969 lemma divide_le_eq_1_pos [simp,noatp]:
  1970   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1971   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1972 by (auto simp add: divide_le_eq)
  1973 
  1974 lemma divide_le_eq_1_neg [simp,noatp]:
  1975   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1976   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1977 by (auto simp add: divide_le_eq)
  1978 
  1979 lemma less_divide_eq_1_pos [simp,noatp]:
  1980   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1981   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  1982 by (auto simp add: less_divide_eq)
  1983 
  1984 lemma less_divide_eq_1_neg [simp,noatp]:
  1985   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1986   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  1987 by (auto simp add: less_divide_eq)
  1988 
  1989 lemma divide_less_eq_1_pos [simp,noatp]:
  1990   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1991   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  1992 by (auto simp add: divide_less_eq)
  1993 
  1994 lemma divide_less_eq_1_neg [simp,noatp]:
  1995   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1996   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  1997 by (auto simp add: divide_less_eq)
  1998 
  1999 lemma eq_divide_eq_1 [simp,noatp]:
  2000   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2001   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  2002 by (auto simp add: eq_divide_eq)
  2003 
  2004 lemma divide_eq_eq_1 [simp,noatp]:
  2005   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2006   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  2007 by (auto simp add: divide_eq_eq)
  2008 
  2009 
  2010 subsection {* Reasoning about inequalities with division *}
  2011 
  2012 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2013     ==> x * y <= x"
  2014 by (auto simp add: mult_compare_simps);
  2015 
  2016 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2017     ==> y * x <= x"
  2018 by (auto simp add: mult_compare_simps);
  2019 
  2020 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  2021     x / y <= z";
  2022 by (subst pos_divide_le_eq, assumption+);
  2023 
  2024 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  2025     z <= x / y"
  2026 by(simp add:field_simps)
  2027 
  2028 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  2029     x / y < z"
  2030 by(simp add:field_simps)
  2031 
  2032 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  2033     z < x / y"
  2034 by(simp add:field_simps)
  2035 
  2036 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  2037     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2038   apply (rule mult_imp_div_pos_le)
  2039   apply simp
  2040   apply (subst times_divide_eq_left)
  2041   apply (rule mult_imp_le_div_pos, assumption)
  2042   apply (rule mult_mono)
  2043   apply simp_all
  2044 done
  2045 
  2046 lemma frac_less: "(0::'a::ordered_field) <= x ==> 
  2047     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  2048   apply (rule mult_imp_div_pos_less)
  2049   apply simp;
  2050   apply (subst times_divide_eq_left);
  2051   apply (rule mult_imp_less_div_pos, assumption)
  2052   apply (erule mult_less_le_imp_less)
  2053   apply simp_all
  2054 done
  2055 
  2056 lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  2057     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2058   apply (rule mult_imp_div_pos_less)
  2059   apply simp_all
  2060   apply (subst times_divide_eq_left);
  2061   apply (rule mult_imp_less_div_pos, assumption)
  2062   apply (erule mult_le_less_imp_less)
  2063   apply simp_all
  2064 done
  2065 
  2066 text{*It's not obvious whether these should be simprules or not. 
  2067   Their effect is to gather terms into one big fraction, like
  2068   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2069   seem to need them.*}
  2070 
  2071 declare times_divide_eq [simp]
  2072 
  2073 
  2074 subsection {* Ordered Fields are Dense *}
  2075 
  2076 context ordered_semidom
  2077 begin
  2078 
  2079 lemma less_add_one: "a < a + 1"
  2080 proof -
  2081   have "a + 0 < a + 1"
  2082     by (blast intro: zero_less_one add_strict_left_mono)
  2083   thus ?thesis by simp
  2084 qed
  2085 
  2086 lemma zero_less_two: "0 < 1 + 1"
  2087 by (blast intro: less_trans zero_less_one less_add_one)
  2088 
  2089 end
  2090 
  2091 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  2092 by (simp add: field_simps zero_less_two)
  2093 
  2094 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  2095 by (simp add: field_simps zero_less_two)
  2096 
  2097 instance ordered_field < dense_linear_order
  2098 proof
  2099   fix x y :: 'a
  2100   have "x < x + 1" by simp
  2101   then show "\<exists>y. x < y" .. 
  2102   have "x - 1 < x" by simp
  2103   then show "\<exists>y. y < x" ..
  2104   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2105 qed
  2106 
  2107 
  2108 subsection {* Absolute Value *}
  2109 
  2110 context ordered_idom
  2111 begin
  2112 
  2113 lemma mult_sgn_abs: "sgn x * abs x = x"
  2114   unfolding abs_if sgn_if by auto
  2115 
  2116 end
  2117 
  2118 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  2119 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2120 
  2121 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
  2122   assumes abs_eq_mult:
  2123     "(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>"
  2124 
  2125 
  2126 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
  2127 begin
  2128 
  2129 subclass lordered_ab_group_add_meet ..
  2130 subclass lordered_ab_group_add_join ..
  2131 
  2132 end
  2133 
  2134 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  2135 proof -
  2136   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  2137   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2138   have a: "(abs a) * (abs b) = ?x"
  2139     by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
  2140   {
  2141     fix u v :: 'a
  2142     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  2143               u * v = pprt a * pprt b + pprt a * nprt b + 
  2144                       nprt a * pprt b + nprt a * nprt b"
  2145       apply (subst prts[of u], subst prts[of v])
  2146       apply (simp add: algebra_simps) 
  2147       done
  2148   }
  2149   note b = this[OF refl[of a] refl[of b]]
  2150   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
  2151   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
  2152   have xy: "- ?x <= ?y"
  2153     apply (simp)
  2154     apply (rule_tac y="0::'a" in order_trans)
  2155     apply (rule addm2)
  2156     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2157     apply (rule addm)
  2158     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2159     done
  2160   have yx: "?y <= ?x"
  2161     apply (simp add:diff_def)
  2162     apply (rule_tac y=0 in order_trans)
  2163     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2164     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2165     done
  2166   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  2167   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  2168   show ?thesis
  2169     apply (rule abs_leI)
  2170     apply (simp add: i1)
  2171     apply (simp add: i2[simplified minus_le_iff])
  2172     done
  2173 qed
  2174 
  2175 instance lordered_ring \<subseteq> pordered_ring_abs
  2176 proof
  2177   fix a b :: "'a\<Colon> lordered_ring"
  2178   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
  2179   show "abs (a*b) = abs a * abs b"
  2180 proof -
  2181   have s: "(0 <= a*b) | (a*b <= 0)"
  2182     apply (auto)    
  2183     apply (rule_tac split_mult_pos_le)
  2184     apply (rule_tac contrapos_np[of "a*b <= 0"])
  2185     apply (simp)
  2186     apply (rule_tac split_mult_neg_le)
  2187     apply (insert prems)
  2188     apply (blast)
  2189     done
  2190   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
  2191     by (simp add: prts[symmetric])
  2192   show ?thesis
  2193   proof cases
  2194     assume "0 <= a * b"
  2195     then show ?thesis
  2196       apply (simp_all add: mulprts abs_prts)
  2197       apply (insert prems)
  2198       apply (auto simp add: 
  2199 	algebra_simps 
  2200 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
  2201 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
  2202 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  2203 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  2204       done
  2205   next
  2206     assume "~(0 <= a*b)"
  2207     with s have "a*b <= 0" by simp
  2208     then show ?thesis
  2209       apply (simp_all add: mulprts abs_prts)
  2210       apply (insert prems)
  2211       apply (auto simp add: algebra_simps)
  2212       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  2213       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  2214       done
  2215   qed
  2216 qed
  2217 qed
  2218 
  2219 instance ordered_idom \<subseteq> pordered_ring_abs
  2220 by default (auto simp add: abs_if not_less
  2221   equal_neg_zero neg_equal_zero mult_less_0_iff)
  2222 
  2223 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
  2224 by (simp add: abs_eq_mult linorder_linear)
  2225 
  2226 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
  2227 by (simp add: abs_if) 
  2228 
  2229 lemma nonzero_abs_inverse:
  2230      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  2231 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2232                       negative_imp_inverse_negative)
  2233 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2234 done
  2235 
  2236 lemma abs_inverse [simp]:
  2237      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  2238       inverse (abs a)"
  2239 apply (cases "a=0", simp) 
  2240 apply (simp add: nonzero_abs_inverse) 
  2241 done
  2242 
  2243 lemma nonzero_abs_divide:
  2244      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  2245 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2246 
  2247 lemma abs_divide [simp]:
  2248      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  2249 apply (cases "b=0", simp) 
  2250 apply (simp add: nonzero_abs_divide) 
  2251 done
  2252 
  2253 lemma abs_mult_less:
  2254      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
  2255 proof -
  2256   assume ac: "abs a < c"
  2257   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2258   assume "abs b < d"
  2259   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2260 qed
  2261 
  2262 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  2263 
  2264 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
  2265   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2266 
  2267 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
  2268 apply (simp add: order_less_le abs_le_iff)  
  2269 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2270 done
  2271 
  2272 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  2273     (abs y) * x = abs (y * x)"
  2274   apply (subst abs_mult)
  2275   apply simp
  2276 done
  2277 
  2278 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  2279     abs x / y = abs (x / y)"
  2280   apply (subst abs_divide)
  2281   apply (simp add: order_less_imp_le)
  2282 done
  2283 
  2284 
  2285 subsection {* Bounds of products via negative and positive Part *}
  2286 
  2287 lemma mult_le_prts:
  2288   assumes
  2289   "a1 <= (a::'a::lordered_ring)"
  2290   "a <= a2"
  2291   "b1 <= b"
  2292   "b <= b2"
  2293   shows
  2294   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  2295 proof - 
  2296   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  2297     apply (subst prts[symmetric])+
  2298     apply simp
  2299     done
  2300   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2301     by (simp add: algebra_simps)
  2302   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  2303     by (simp_all add: prems mult_mono)
  2304   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  2305   proof -
  2306     have "pprt a * nprt b <= pprt a * nprt b2"
  2307       by (simp add: mult_left_mono prems)
  2308     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  2309       by (simp add: mult_right_mono_neg prems)
  2310     ultimately show ?thesis
  2311       by simp
  2312   qed
  2313   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  2314   proof - 
  2315     have "nprt a * pprt b <= nprt a2 * pprt b"
  2316       by (simp add: mult_right_mono prems)
  2317     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  2318       by (simp add: mult_left_mono_neg prems)
  2319     ultimately show ?thesis
  2320       by simp
  2321   qed
  2322   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  2323   proof -
  2324     have "nprt a * nprt b <= nprt a * nprt b1"
  2325       by (simp add: mult_left_mono_neg prems)
  2326     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  2327       by (simp add: mult_right_mono_neg prems)
  2328     ultimately show ?thesis
  2329       by simp
  2330   qed
  2331   ultimately show ?thesis
  2332     by - (rule add_mono | simp)+
  2333 qed
  2334 
  2335 lemma mult_ge_prts:
  2336   assumes
  2337   "a1 <= (a::'a::lordered_ring)"
  2338   "a <= a2"
  2339   "b1 <= b"
  2340   "b <= b2"
  2341   shows
  2342   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  2343 proof - 
  2344   from prems have a1:"- a2 <= -a" by auto
  2345   from prems have a2: "-a <= -a1" by auto
  2346   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  2347   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  2348   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  2349     by (simp only: minus_le_iff)
  2350   then show ?thesis by simp
  2351 qed
  2352 
  2353 end