src/HOL/Ring_and_Field.thy
author haftmann
Mon Apr 27 10:11:44 2009 +0200 (2009-04-27)
changeset 31001 7e6ffd8f51a9
parent 30961 541bfff659af
child 32960 69916a850301
permissions -rw-r--r--
cleaned up theory power further
     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 text{*There is no slick version using division by zero.*}
   540 lemma inverse_add:
   541   "[| a \<noteq> 0;  b \<noteq> 0 |]
   542    ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
   543 by (simp add: division_ring_inverse_add mult_ac)
   544 
   545 lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
   546 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
   547 proof -
   548   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
   549     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   550   also have "... =  a * inverse b * (inverse c * c)"
   551     by (simp only: mult_ac)
   552   also have "... =  a * inverse b" by simp
   553     finally show ?thesis by (simp add: divide_inverse)
   554 qed
   555 
   556 lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
   557   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
   558 by (simp add: mult_commute [of _ c])
   559 
   560 lemma divide_1 [simp]: "a / 1 = a"
   561 by (simp add: divide_inverse)
   562 
   563 lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
   564 by (simp add: divide_inverse mult_assoc)
   565 
   566 lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
   567 by (simp add: divide_inverse mult_ac)
   568 
   569 text {* These are later declared as simp rules. *}
   570 lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
   571 
   572 lemma add_frac_eq:
   573   assumes "y \<noteq> 0" and "z \<noteq> 0"
   574   shows "x / y + w / z = (x * z + w * y) / (y * z)"
   575 proof -
   576   have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
   577     using assms by simp
   578   also have "\<dots> = (x * z + y * w) / (y * z)"
   579     by (simp only: add_divide_distrib)
   580   finally show ?thesis
   581     by (simp only: mult_commute)
   582 qed
   583 
   584 text{*Special Cancellation Simprules for Division*}
   585 
   586 lemma nonzero_mult_divide_cancel_right [simp, noatp]:
   587   "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
   588 using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
   589 
   590 lemma nonzero_mult_divide_cancel_left [simp, noatp]:
   591   "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
   592 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
   593 
   594 lemma nonzero_divide_mult_cancel_right [simp, noatp]:
   595   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
   596 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
   597 
   598 lemma nonzero_divide_mult_cancel_left [simp, noatp]:
   599   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
   600 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
   601 
   602 lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
   603   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
   604 using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
   605 
   606 lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
   607   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
   608 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
   609 
   610 lemma minus_divide_left: "- (a / b) = (-a) / b"
   611 by (simp add: divide_inverse)
   612 
   613 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
   614 by (simp add: divide_inverse nonzero_inverse_minus_eq)
   615 
   616 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
   617 by (simp add: divide_inverse nonzero_inverse_minus_eq)
   618 
   619 lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
   620 by (simp add: divide_inverse)
   621 
   622 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
   623 by (simp add: diff_minus add_divide_distrib)
   624 
   625 lemma add_divide_eq_iff:
   626   "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
   627 by (simp add: add_divide_distrib)
   628 
   629 lemma divide_add_eq_iff:
   630   "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
   631 by (simp add: add_divide_distrib)
   632 
   633 lemma diff_divide_eq_iff:
   634   "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
   635 by (simp add: diff_divide_distrib)
   636 
   637 lemma divide_diff_eq_iff:
   638   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
   639 by (simp add: diff_divide_distrib)
   640 
   641 lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   642 proof -
   643   assume [simp]: "c \<noteq> 0"
   644   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
   645   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
   646   finally show ?thesis .
   647 qed
   648 
   649 lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
   650 proof -
   651   assume [simp]: "c \<noteq> 0"
   652   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
   653   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
   654   finally show ?thesis .
   655 qed
   656 
   657 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   658 by simp
   659 
   660 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   661 by (erule subst, simp)
   662 
   663 lemmas field_eq_simps[noatp] = algebra_simps
   664   (* pull / out*)
   665   add_divide_eq_iff divide_add_eq_iff
   666   diff_divide_eq_iff divide_diff_eq_iff
   667   (* multiply eqn *)
   668   nonzero_eq_divide_eq nonzero_divide_eq_eq
   669 (* is added later:
   670   times_divide_eq_left times_divide_eq_right
   671 *)
   672 
   673 text{*An example:*}
   674 lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
   675 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
   676  apply(simp add:field_eq_simps)
   677 apply(simp)
   678 done
   679 
   680 lemma diff_frac_eq:
   681   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   682 by (simp add: field_eq_simps times_divide_eq)
   683 
   684 lemma frac_eq_eq:
   685   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   686 by (simp add: field_eq_simps times_divide_eq)
   687 
   688 end
   689 
   690 class division_by_zero = zero + inverse +
   691   assumes inverse_zero [simp]: "inverse 0 = 0"
   692 
   693 lemma divide_zero [simp]:
   694   "a / 0 = (0::'a::{field,division_by_zero})"
   695 by (simp add: divide_inverse)
   696 
   697 lemma divide_self_if [simp]:
   698   "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   699 by simp
   700 
   701 class mult_mono = times + zero + ord +
   702   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   703   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   704 
   705 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   706 begin
   707 
   708 lemma mult_mono:
   709   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   710      \<Longrightarrow> a * c \<le> b * d"
   711 apply (erule mult_right_mono [THEN order_trans], assumption)
   712 apply (erule mult_left_mono, assumption)
   713 done
   714 
   715 lemma mult_mono':
   716   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   717      \<Longrightarrow> a * c \<le> b * d"
   718 apply (rule mult_mono)
   719 apply (fast intro: order_trans)+
   720 done
   721 
   722 end
   723 
   724 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   725   + semiring + cancel_comm_monoid_add
   726 begin
   727 
   728 subclass semiring_0_cancel ..
   729 subclass pordered_semiring ..
   730 
   731 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   732 using mult_left_mono [of zero b a] by simp
   733 
   734 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   735 using mult_left_mono [of b zero a] by simp
   736 
   737 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
   738 using mult_right_mono [of a zero b] by simp
   739 
   740 text {* Legacy - use @{text mult_nonpos_nonneg} *}
   741 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   742 by (drule mult_right_mono [of b zero], auto)
   743 
   744 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   745 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   746 
   747 end
   748 
   749 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   750 begin
   751 
   752 subclass pordered_cancel_semiring ..
   753 
   754 subclass pordered_comm_monoid_add ..
   755 
   756 lemma mult_left_less_imp_less:
   757   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   758 by (force simp add: mult_left_mono not_le [symmetric])
   759  
   760 lemma mult_right_less_imp_less:
   761   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   762 by (force simp add: mult_right_mono not_le [symmetric])
   763 
   764 end
   765 
   766 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   767   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   768   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   769 begin
   770 
   771 subclass semiring_0_cancel ..
   772 
   773 subclass ordered_semiring
   774 proof
   775   fix a b c :: 'a
   776   assume A: "a \<le> b" "0 \<le> c"
   777   from A show "c * a \<le> c * b"
   778     unfolding le_less
   779     using mult_strict_left_mono by (cases "c = 0") auto
   780   from A show "a * c \<le> b * c"
   781     unfolding le_less
   782     using mult_strict_right_mono by (cases "c = 0") auto
   783 qed
   784 
   785 lemma mult_left_le_imp_le:
   786   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   787 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   788  
   789 lemma mult_right_le_imp_le:
   790   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   791 by (force simp add: mult_strict_right_mono not_less [symmetric])
   792 
   793 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   794 using mult_strict_left_mono [of zero b a] by simp
   795 
   796 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   797 using mult_strict_left_mono [of b zero a] by simp
   798 
   799 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
   800 using mult_strict_right_mono [of a zero b] by simp
   801 
   802 text {* Legacy - use @{text mult_neg_pos} *}
   803 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   804 by (drule mult_strict_right_mono [of b zero], auto)
   805 
   806 lemma zero_less_mult_pos:
   807   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   808 apply (cases "b\<le>0")
   809  apply (auto simp add: le_less not_less)
   810 apply (drule_tac mult_pos_neg [of a b])
   811  apply (auto dest: less_not_sym)
   812 done
   813 
   814 lemma zero_less_mult_pos2:
   815   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   816 apply (cases "b\<le>0")
   817  apply (auto simp add: le_less not_less)
   818 apply (drule_tac mult_pos_neg2 [of a b])
   819  apply (auto dest: less_not_sym)
   820 done
   821 
   822 text{*Strict monotonicity in both arguments*}
   823 lemma mult_strict_mono:
   824   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   825   shows "a * c < b * d"
   826   using assms apply (cases "c=0")
   827   apply (simp add: mult_pos_pos)
   828   apply (erule mult_strict_right_mono [THEN less_trans])
   829   apply (force simp add: le_less)
   830   apply (erule mult_strict_left_mono, assumption)
   831   done
   832 
   833 text{*This weaker variant has more natural premises*}
   834 lemma mult_strict_mono':
   835   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   836   shows "a * c < b * d"
   837 by (rule mult_strict_mono) (insert assms, auto)
   838 
   839 lemma mult_less_le_imp_less:
   840   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   841   shows "a * c < b * d"
   842   using assms apply (subgoal_tac "a * c < b * c")
   843   apply (erule less_le_trans)
   844   apply (erule mult_left_mono)
   845   apply simp
   846   apply (erule mult_strict_right_mono)
   847   apply assumption
   848   done
   849 
   850 lemma mult_le_less_imp_less:
   851   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   852   shows "a * c < b * d"
   853   using assms apply (subgoal_tac "a * c \<le> b * c")
   854   apply (erule le_less_trans)
   855   apply (erule mult_strict_left_mono)
   856   apply simp
   857   apply (erule mult_right_mono)
   858   apply simp
   859   done
   860 
   861 lemma mult_less_imp_less_left:
   862   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   863   shows "a < b"
   864 proof (rule ccontr)
   865   assume "\<not>  a < b"
   866   hence "b \<le> a" by (simp add: linorder_not_less)
   867   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   868   with this and less show False by (simp add: not_less [symmetric])
   869 qed
   870 
   871 lemma mult_less_imp_less_right:
   872   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   873   shows "a < b"
   874 proof (rule ccontr)
   875   assume "\<not> a < b"
   876   hence "b \<le> a" by (simp add: linorder_not_less)
   877   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   878   with this and less show False by (simp add: not_less [symmetric])
   879 qed  
   880 
   881 end
   882 
   883 class mult_mono1 = times + zero + ord +
   884   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   885 
   886 class pordered_comm_semiring = comm_semiring_0
   887   + pordered_ab_semigroup_add + mult_mono1
   888 begin
   889 
   890 subclass pordered_semiring
   891 proof
   892   fix a b c :: 'a
   893   assume "a \<le> b" "0 \<le> c"
   894   thus "c * a \<le> c * b" by (rule mult_mono1)
   895   thus "a * c \<le> b * c" by (simp only: mult_commute)
   896 qed
   897 
   898 end
   899 
   900 class pordered_cancel_comm_semiring = comm_semiring_0_cancel
   901   + pordered_ab_semigroup_add + mult_mono1
   902 begin
   903 
   904 subclass pordered_comm_semiring ..
   905 subclass pordered_cancel_semiring ..
   906 
   907 end
   908 
   909 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   910   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   911 begin
   912 
   913 subclass ordered_semiring_strict
   914 proof
   915   fix a b c :: 'a
   916   assume "a < b" "0 < c"
   917   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   918   thus "a * c < b * c" by (simp only: mult_commute)
   919 qed
   920 
   921 subclass pordered_cancel_comm_semiring
   922 proof
   923   fix a b c :: 'a
   924   assume "a \<le> b" "0 \<le> c"
   925   thus "c * a \<le> c * b"
   926     unfolding le_less
   927     using mult_strict_left_mono by (cases "c = 0") auto
   928 qed
   929 
   930 end
   931 
   932 class pordered_ring = ring + pordered_cancel_semiring 
   933 begin
   934 
   935 subclass pordered_ab_group_add ..
   936 
   937 text{*Legacy - use @{text algebra_simps} *}
   938 lemmas ring_simps[noatp] = algebra_simps
   939 
   940 lemma less_add_iff1:
   941   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   942 by (simp add: algebra_simps)
   943 
   944 lemma less_add_iff2:
   945   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   946 by (simp add: algebra_simps)
   947 
   948 lemma le_add_iff1:
   949   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   950 by (simp add: algebra_simps)
   951 
   952 lemma le_add_iff2:
   953   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   954 by (simp add: algebra_simps)
   955 
   956 lemma mult_left_mono_neg:
   957   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   958   apply (drule mult_left_mono [of _ _ "uminus c"])
   959   apply (simp_all add: minus_mult_left [symmetric]) 
   960   done
   961 
   962 lemma mult_right_mono_neg:
   963   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   964   apply (drule mult_right_mono [of _ _ "uminus c"])
   965   apply (simp_all add: minus_mult_right [symmetric]) 
   966   done
   967 
   968 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   969 using mult_right_mono_neg [of a zero b] by simp
   970 
   971 lemma split_mult_pos_le:
   972   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   973 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   974 
   975 end
   976 
   977 class abs_if = minus + uminus + ord + zero + abs +
   978   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
   979 
   980 class sgn_if = minus + uminus + zero + one + ord + sgn +
   981   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   982 
   983 lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
   984 by(simp add:sgn_if)
   985 
   986 class ordered_ring = ring + ordered_semiring
   987   + ordered_ab_group_add + abs_if
   988 begin
   989 
   990 subclass pordered_ring ..
   991 
   992 subclass pordered_ab_group_add_abs
   993 proof
   994   fix a b
   995   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   996 by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   997    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
   998      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
   999       auto intro!: less_imp_le add_neg_neg)
  1000 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
  1001 
  1002 end
  1003 
  1004 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
  1005    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
  1006  *)
  1007 class ordered_ring_strict = ring + ordered_semiring_strict
  1008   + ordered_ab_group_add + abs_if
  1009 begin
  1010 
  1011 subclass ordered_ring ..
  1012 
  1013 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1014 using mult_strict_left_mono [of b a "- c"] by simp
  1015 
  1016 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1017 using mult_strict_right_mono [of b a "- c"] by simp
  1018 
  1019 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1020 using mult_strict_right_mono_neg [of a zero b] by simp
  1021 
  1022 subclass ring_no_zero_divisors
  1023 proof
  1024   fix a b
  1025   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1026   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1027   have "a * b < 0 \<or> 0 < a * b"
  1028   proof (cases "a < 0")
  1029     case True note A' = this
  1030     show ?thesis proof (cases "b < 0")
  1031       case True with A'
  1032       show ?thesis by (auto dest: mult_neg_neg)
  1033     next
  1034       case False with B have "0 < b" by auto
  1035       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1036     qed
  1037   next
  1038     case False with A have A': "0 < a" by auto
  1039     show ?thesis proof (cases "b < 0")
  1040       case True with A'
  1041       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1042     next
  1043       case False with B have "0 < b" by auto
  1044       with A' show ?thesis by (auto dest: mult_pos_pos)
  1045     qed
  1046   qed
  1047   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1048 qed
  1049 
  1050 lemma zero_less_mult_iff:
  1051   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1052   apply (auto simp add: mult_pos_pos mult_neg_neg)
  1053   apply (simp_all add: not_less le_less)
  1054   apply (erule disjE) apply assumption defer
  1055   apply (erule disjE) defer apply (drule sym) apply simp
  1056   apply (erule disjE) defer apply (drule sym) apply simp
  1057   apply (erule disjE) apply assumption apply (drule sym) apply simp
  1058   apply (drule sym) apply simp
  1059   apply (blast dest: zero_less_mult_pos)
  1060   apply (blast dest: zero_less_mult_pos2)
  1061   done
  1062 
  1063 lemma zero_le_mult_iff:
  1064   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
  1065 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1066 
  1067 lemma mult_less_0_iff:
  1068   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1069   apply (insert zero_less_mult_iff [of "-a" b]) 
  1070   apply (force simp add: minus_mult_left[symmetric]) 
  1071   done
  1072 
  1073 lemma mult_le_0_iff:
  1074   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1075   apply (insert zero_le_mult_iff [of "-a" b]) 
  1076   apply (force simp add: minus_mult_left[symmetric]) 
  1077   done
  1078 
  1079 lemma zero_le_square [simp]: "0 \<le> a * a"
  1080 by (simp add: zero_le_mult_iff linear)
  1081 
  1082 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1083 by (simp add: not_less)
  1084 
  1085 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1086    also with the relations @{text "\<le>"} and equality.*}
  1087 
  1088 text{*These ``disjunction'' versions produce two cases when the comparison is
  1089  an assumption, but effectively four when the comparison is a goal.*}
  1090 
  1091 lemma mult_less_cancel_right_disj:
  1092   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1093   apply (cases "c = 0")
  1094   apply (auto simp add: neq_iff mult_strict_right_mono 
  1095                       mult_strict_right_mono_neg)
  1096   apply (auto simp add: not_less 
  1097                       not_le [symmetric, of "a*c"]
  1098                       not_le [symmetric, of a])
  1099   apply (erule_tac [!] notE)
  1100   apply (auto simp add: less_imp_le mult_right_mono 
  1101                       mult_right_mono_neg)
  1102   done
  1103 
  1104 lemma mult_less_cancel_left_disj:
  1105   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1106   apply (cases "c = 0")
  1107   apply (auto simp add: neq_iff mult_strict_left_mono 
  1108                       mult_strict_left_mono_neg)
  1109   apply (auto simp add: not_less 
  1110                       not_le [symmetric, of "c*a"]
  1111                       not_le [symmetric, of a])
  1112   apply (erule_tac [!] notE)
  1113   apply (auto simp add: less_imp_le mult_left_mono 
  1114                       mult_left_mono_neg)
  1115   done
  1116 
  1117 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1118 comparison is a goal, but give four when the comparison is an assumption.*}
  1119 
  1120 lemma mult_less_cancel_right:
  1121   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1122   using mult_less_cancel_right_disj [of a c b] by auto
  1123 
  1124 lemma mult_less_cancel_left:
  1125   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1126   using mult_less_cancel_left_disj [of c a b] by auto
  1127 
  1128 lemma mult_le_cancel_right:
  1129    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1130 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1131 
  1132 lemma mult_le_cancel_left:
  1133   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1134 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1135 
  1136 lemma mult_le_cancel_left_pos:
  1137   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1138 by (auto simp: mult_le_cancel_left)
  1139 
  1140 lemma mult_le_cancel_left_neg:
  1141   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1142 by (auto simp: mult_le_cancel_left)
  1143 
  1144 lemma mult_less_cancel_left_pos:
  1145   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1146 by (auto simp: mult_less_cancel_left)
  1147 
  1148 lemma mult_less_cancel_left_neg:
  1149   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1150 by (auto simp: mult_less_cancel_left)
  1151 
  1152 end
  1153 
  1154 text{*Legacy - use @{text algebra_simps} *}
  1155 lemmas ring_simps[noatp] = algebra_simps
  1156 
  1157 lemmas mult_sign_intros =
  1158   mult_nonneg_nonneg mult_nonneg_nonpos
  1159   mult_nonpos_nonneg mult_nonpos_nonpos
  1160   mult_pos_pos mult_pos_neg
  1161   mult_neg_pos mult_neg_neg
  1162 
  1163 class pordered_comm_ring = comm_ring + pordered_comm_semiring
  1164 begin
  1165 
  1166 subclass pordered_ring ..
  1167 subclass pordered_cancel_comm_semiring ..
  1168 
  1169 end
  1170 
  1171 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
  1172   (*previously ordered_semiring*)
  1173   assumes zero_less_one [simp]: "0 < 1"
  1174 begin
  1175 
  1176 lemma pos_add_strict:
  1177   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1178   using add_strict_mono [of zero a b c] by simp
  1179 
  1180 lemma zero_le_one [simp]: "0 \<le> 1"
  1181 by (rule zero_less_one [THEN less_imp_le]) 
  1182 
  1183 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1184 by (simp add: not_le) 
  1185 
  1186 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1187 by (simp add: not_less) 
  1188 
  1189 lemma less_1_mult:
  1190   assumes "1 < m" and "1 < n"
  1191   shows "1 < m * n"
  1192   using assms mult_strict_mono [of 1 m 1 n]
  1193     by (simp add:  less_trans [OF zero_less_one]) 
  1194 
  1195 end
  1196 
  1197 class ordered_idom = comm_ring_1 +
  1198   ordered_comm_semiring_strict + ordered_ab_group_add +
  1199   abs_if + sgn_if
  1200   (*previously ordered_ring*)
  1201 begin
  1202 
  1203 subclass ordered_ring_strict ..
  1204 subclass pordered_comm_ring ..
  1205 subclass idom ..
  1206 
  1207 subclass ordered_semidom
  1208 proof
  1209   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1210   thus "0 < 1" by (simp add: le_less)
  1211 qed 
  1212 
  1213 lemma linorder_neqE_ordered_idom:
  1214   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1215   using assms by (rule neqE)
  1216 
  1217 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1218 
  1219 lemma mult_le_cancel_right1:
  1220   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1221 by (insert mult_le_cancel_right [of 1 c b], simp)
  1222 
  1223 lemma mult_le_cancel_right2:
  1224   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1225 by (insert mult_le_cancel_right [of a c 1], simp)
  1226 
  1227 lemma mult_le_cancel_left1:
  1228   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1229 by (insert mult_le_cancel_left [of c 1 b], simp)
  1230 
  1231 lemma mult_le_cancel_left2:
  1232   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1233 by (insert mult_le_cancel_left [of c a 1], simp)
  1234 
  1235 lemma mult_less_cancel_right1:
  1236   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1237 by (insert mult_less_cancel_right [of 1 c b], simp)
  1238 
  1239 lemma mult_less_cancel_right2:
  1240   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1241 by (insert mult_less_cancel_right [of a c 1], simp)
  1242 
  1243 lemma mult_less_cancel_left1:
  1244   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1245 by (insert mult_less_cancel_left [of c 1 b], simp)
  1246 
  1247 lemma mult_less_cancel_left2:
  1248   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1249 by (insert mult_less_cancel_left [of c a 1], simp)
  1250 
  1251 lemma sgn_sgn [simp]:
  1252   "sgn (sgn a) = sgn a"
  1253 unfolding sgn_if by simp
  1254 
  1255 lemma sgn_0_0:
  1256   "sgn a = 0 \<longleftrightarrow> a = 0"
  1257 unfolding sgn_if by simp
  1258 
  1259 lemma sgn_1_pos:
  1260   "sgn a = 1 \<longleftrightarrow> a > 0"
  1261 unfolding sgn_if by (simp add: neg_equal_zero)
  1262 
  1263 lemma sgn_1_neg:
  1264   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1265 unfolding sgn_if by (auto simp add: equal_neg_zero)
  1266 
  1267 lemma sgn_pos [simp]:
  1268   "0 < a \<Longrightarrow> sgn a = 1"
  1269 unfolding sgn_1_pos .
  1270 
  1271 lemma sgn_neg [simp]:
  1272   "a < 0 \<Longrightarrow> sgn a = - 1"
  1273 unfolding sgn_1_neg .
  1274 
  1275 lemma sgn_times:
  1276   "sgn (a * b) = sgn a * sgn b"
  1277 by (auto simp add: sgn_if zero_less_mult_iff)
  1278 
  1279 lemma abs_sgn: "abs k = k * sgn k"
  1280 unfolding sgn_if abs_if by auto
  1281 
  1282 lemma sgn_greater [simp]:
  1283   "0 < sgn a \<longleftrightarrow> 0 < a"
  1284   unfolding sgn_if by auto
  1285 
  1286 lemma sgn_less [simp]:
  1287   "sgn a < 0 \<longleftrightarrow> a < 0"
  1288   unfolding sgn_if by auto
  1289 
  1290 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  1291   by (simp add: abs_if)
  1292 
  1293 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  1294   by (simp add: abs_if)
  1295 
  1296 end
  1297 
  1298 class ordered_field = field + ordered_idom
  1299 
  1300 text {* Simprules for comparisons where common factors can be cancelled. *}
  1301 
  1302 lemmas mult_compare_simps[noatp] =
  1303     mult_le_cancel_right mult_le_cancel_left
  1304     mult_le_cancel_right1 mult_le_cancel_right2
  1305     mult_le_cancel_left1 mult_le_cancel_left2
  1306     mult_less_cancel_right mult_less_cancel_left
  1307     mult_less_cancel_right1 mult_less_cancel_right2
  1308     mult_less_cancel_left1 mult_less_cancel_left2
  1309     mult_cancel_right mult_cancel_left
  1310     mult_cancel_right1 mult_cancel_right2
  1311     mult_cancel_left1 mult_cancel_left2
  1312 
  1313 -- {* FIXME continue localization here *}
  1314 
  1315 lemma inverse_nonzero_iff_nonzero [simp]:
  1316    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
  1317 by (force dest: inverse_zero_imp_zero) 
  1318 
  1319 lemma inverse_minus_eq [simp]:
  1320    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
  1321 proof cases
  1322   assume "a=0" thus ?thesis by (simp add: inverse_zero)
  1323 next
  1324   assume "a\<noteq>0" 
  1325   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  1326 qed
  1327 
  1328 lemma inverse_eq_imp_eq:
  1329   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
  1330 apply (cases "a=0 | b=0") 
  1331  apply (force dest!: inverse_zero_imp_zero
  1332               simp add: eq_commute [of "0::'a"])
  1333 apply (force dest!: nonzero_inverse_eq_imp_eq) 
  1334 done
  1335 
  1336 lemma inverse_eq_iff_eq [simp]:
  1337   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
  1338 by (force dest!: inverse_eq_imp_eq)
  1339 
  1340 lemma inverse_inverse_eq [simp]:
  1341      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
  1342   proof cases
  1343     assume "a=0" thus ?thesis by simp
  1344   next
  1345     assume "a\<noteq>0" 
  1346     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  1347   qed
  1348 
  1349 text{*This version builds in division by zero while also re-orienting
  1350       the right-hand side.*}
  1351 lemma inverse_mult_distrib [simp]:
  1352      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
  1353   proof cases
  1354     assume "a \<noteq> 0 & b \<noteq> 0" 
  1355     thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
  1356   next
  1357     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
  1358     thus ?thesis by force
  1359   qed
  1360 
  1361 lemma inverse_divide [simp]:
  1362   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  1363 by (simp add: divide_inverse mult_commute)
  1364 
  1365 
  1366 subsection {* Calculations with fractions *}
  1367 
  1368 text{* There is a whole bunch of simp-rules just for class @{text
  1369 field} but none for class @{text field} and @{text nonzero_divides}
  1370 because the latter are covered by a simproc. *}
  1371 
  1372 lemma mult_divide_mult_cancel_left:
  1373   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  1374 apply (cases "b = 0")
  1375 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  1376 done
  1377 
  1378 lemma mult_divide_mult_cancel_right:
  1379   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  1380 apply (cases "b = 0")
  1381 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  1382 done
  1383 
  1384 lemma divide_divide_eq_right [simp,noatp]:
  1385   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  1386 by (simp add: divide_inverse mult_ac)
  1387 
  1388 lemma divide_divide_eq_left [simp,noatp]:
  1389   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  1390 by (simp add: divide_inverse mult_assoc)
  1391 
  1392 
  1393 subsubsection{*Special Cancellation Simprules for Division*}
  1394 
  1395 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
  1396 fixes c :: "'a :: {field,division_by_zero}"
  1397 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  1398 by (simp add: mult_divide_mult_cancel_left)
  1399 
  1400 
  1401 subsection {* Division and Unary Minus *}
  1402 
  1403 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1404 by (simp add: divide_inverse)
  1405 
  1406 lemma divide_minus_right [simp, noatp]:
  1407   "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
  1408 by (simp add: divide_inverse)
  1409 
  1410 lemma minus_divide_divide:
  1411   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1412 apply (cases "b=0", simp) 
  1413 apply (simp add: nonzero_minus_divide_divide) 
  1414 done
  1415 
  1416 lemma eq_divide_eq:
  1417   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1418 by (simp add: nonzero_eq_divide_eq)
  1419 
  1420 lemma divide_eq_eq:
  1421   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1422 by (force simp add: nonzero_divide_eq_eq)
  1423 
  1424 
  1425 subsection {* Ordered Fields *}
  1426 
  1427 lemma positive_imp_inverse_positive: 
  1428 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
  1429 proof -
  1430   have "0 < a * inverse a" 
  1431     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1432   thus "0 < inverse a" 
  1433     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1434 qed
  1435 
  1436 lemma negative_imp_inverse_negative:
  1437   "a < 0 ==> inverse a < (0::'a::ordered_field)"
  1438 by (insert positive_imp_inverse_positive [of "-a"], 
  1439     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1440 
  1441 lemma inverse_le_imp_le:
  1442 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1443 shows "b \<le> (a::'a::ordered_field)"
  1444 proof (rule classical)
  1445   assume "~ b \<le> a"
  1446   hence "a < b"  by (simp add: linorder_not_le)
  1447   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1448   hence "a * inverse a \<le> a * inverse b"
  1449     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1450   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1451     by (simp add: bpos order_less_imp_le mult_right_mono)
  1452   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1453 qed
  1454 
  1455 lemma inverse_positive_imp_positive:
  1456 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1457 shows "0 < (a::'a::ordered_field)"
  1458 proof -
  1459   have "0 < inverse (inverse a)"
  1460     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1461   thus "0 < a"
  1462     using nz by (simp add: nonzero_inverse_inverse_eq)
  1463 qed
  1464 
  1465 lemma inverse_positive_iff_positive [simp]:
  1466   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1467 apply (cases "a = 0", simp)
  1468 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1469 done
  1470 
  1471 lemma inverse_negative_imp_negative:
  1472 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1473 shows "a < (0::'a::ordered_field)"
  1474 proof -
  1475   have "inverse (inverse a) < 0"
  1476     using inv_less_0 by (rule negative_imp_inverse_negative)
  1477   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1478 qed
  1479 
  1480 lemma inverse_negative_iff_negative [simp]:
  1481   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1482 apply (cases "a = 0", simp)
  1483 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1484 done
  1485 
  1486 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1487   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1488 by (simp add: linorder_not_less [symmetric])
  1489 
  1490 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1491   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1492 by (simp add: linorder_not_less [symmetric])
  1493 
  1494 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
  1495 proof
  1496   fix x::'a
  1497   have m1: "- (1::'a) < 0" by simp
  1498   from add_strict_right_mono[OF m1, where c=x] 
  1499   have "(- 1) + x < x" by simp
  1500   thus "\<exists>y. y < x" by blast
  1501 qed
  1502 
  1503 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
  1504 proof
  1505   fix x::'a
  1506   have m1: " (1::'a) > 0" by simp
  1507   from add_strict_right_mono[OF m1, where c=x] 
  1508   have "1 + x > x" by simp
  1509   thus "\<exists>y. y > x" by blast
  1510 qed
  1511 
  1512 subsection{*Anti-Monotonicity of @{term inverse}*}
  1513 
  1514 lemma less_imp_inverse_less:
  1515 assumes less: "a < b" and apos:  "0 < a"
  1516 shows "inverse b < inverse (a::'a::ordered_field)"
  1517 proof (rule ccontr)
  1518   assume "~ inverse b < inverse a"
  1519   hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
  1520   hence "~ (a < b)"
  1521     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1522   thus False by (rule notE [OF _ less])
  1523 qed
  1524 
  1525 lemma inverse_less_imp_less:
  1526   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1527 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1528 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1529 done
  1530 
  1531 text{*Both premises are essential. Consider -1 and 1.*}
  1532 lemma inverse_less_iff_less [simp,noatp]:
  1533   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1534 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1535 
  1536 lemma le_imp_inverse_le:
  1537   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1538 by (force simp add: order_le_less less_imp_inverse_less)
  1539 
  1540 lemma inverse_le_iff_le [simp,noatp]:
  1541  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1542 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1543 
  1544 
  1545 text{*These results refer to both operands being negative.  The opposite-sign
  1546 case is trivial, since inverse preserves signs.*}
  1547 lemma inverse_le_imp_le_neg:
  1548   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1549 apply (rule classical) 
  1550 apply (subgoal_tac "a < 0") 
  1551  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1552 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1553 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1554 done
  1555 
  1556 lemma less_imp_inverse_less_neg:
  1557    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1558 apply (subgoal_tac "a < 0") 
  1559  prefer 2 apply (blast intro: order_less_trans) 
  1560 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1561 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1562 done
  1563 
  1564 lemma inverse_less_imp_less_neg:
  1565    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1566 apply (rule classical) 
  1567 apply (subgoal_tac "a < 0") 
  1568  prefer 2
  1569  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1570 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1571 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1572 done
  1573 
  1574 lemma inverse_less_iff_less_neg [simp,noatp]:
  1575   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1576 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1577 apply (simp del: inverse_less_iff_less 
  1578             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1579 done
  1580 
  1581 lemma le_imp_inverse_le_neg:
  1582   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1583 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1584 
  1585 lemma inverse_le_iff_le_neg [simp,noatp]:
  1586  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1587 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1588 
  1589 
  1590 subsection{*Inverses and the Number One*}
  1591 
  1592 lemma one_less_inverse_iff:
  1593   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
  1594 proof cases
  1595   assume "0 < x"
  1596     with inverse_less_iff_less [OF zero_less_one, of x]
  1597     show ?thesis by simp
  1598 next
  1599   assume notless: "~ (0 < x)"
  1600   have "~ (1 < inverse x)"
  1601   proof
  1602     assume "1 < inverse x"
  1603     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1604     also have "... < 1" by (rule zero_less_one) 
  1605     finally show False by auto
  1606   qed
  1607   with notless show ?thesis by simp
  1608 qed
  1609 
  1610 lemma inverse_eq_1_iff [simp]:
  1611   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1612 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1613 
  1614 lemma one_le_inverse_iff:
  1615   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
  1616 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1617                     eq_commute [of 1]) 
  1618 
  1619 lemma inverse_less_1_iff:
  1620   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
  1621 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1622 
  1623 lemma inverse_le_1_iff:
  1624   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  1625 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1626 
  1627 
  1628 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1629 
  1630 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1631 proof -
  1632   assume less: "0<c"
  1633   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1634     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1635   also have "... = (a*c \<le> b)"
  1636     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1637   finally show ?thesis .
  1638 qed
  1639 
  1640 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1641 proof -
  1642   assume less: "c<0"
  1643   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1644     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1645   also have "... = (b \<le> a*c)"
  1646     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1647   finally show ?thesis .
  1648 qed
  1649 
  1650 lemma le_divide_eq:
  1651   "(a \<le> b/c) = 
  1652    (if 0 < c then a*c \<le> b
  1653              else if c < 0 then b \<le> a*c
  1654              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1655 apply (cases "c=0", simp) 
  1656 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1657 done
  1658 
  1659 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1660 proof -
  1661   assume less: "0<c"
  1662   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1663     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1664   also have "... = (b \<le> a*c)"
  1665     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1666   finally show ?thesis .
  1667 qed
  1668 
  1669 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1670 proof -
  1671   assume less: "c<0"
  1672   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1673     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1674   also have "... = (a*c \<le> b)"
  1675     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1676   finally show ?thesis .
  1677 qed
  1678 
  1679 lemma divide_le_eq:
  1680   "(b/c \<le> a) = 
  1681    (if 0 < c then b \<le> a*c
  1682              else if c < 0 then a*c \<le> b
  1683              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1684 apply (cases "c=0", simp) 
  1685 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1686 done
  1687 
  1688 lemma pos_less_divide_eq:
  1689      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1690 proof -
  1691   assume less: "0<c"
  1692   hence "(a < b/c) = (a*c < (b/c)*c)"
  1693     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1694   also have "... = (a*c < b)"
  1695     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1696   finally show ?thesis .
  1697 qed
  1698 
  1699 lemma neg_less_divide_eq:
  1700  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1701 proof -
  1702   assume less: "c<0"
  1703   hence "(a < b/c) = ((b/c)*c < a*c)"
  1704     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1705   also have "... = (b < a*c)"
  1706     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1707   finally show ?thesis .
  1708 qed
  1709 
  1710 lemma less_divide_eq:
  1711   "(a < b/c) = 
  1712    (if 0 < c then a*c < b
  1713              else if c < 0 then b < a*c
  1714              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1715 apply (cases "c=0", simp) 
  1716 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1717 done
  1718 
  1719 lemma pos_divide_less_eq:
  1720      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1721 proof -
  1722   assume less: "0<c"
  1723   hence "(b/c < a) = ((b/c)*c < a*c)"
  1724     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1725   also have "... = (b < a*c)"
  1726     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1727   finally show ?thesis .
  1728 qed
  1729 
  1730 lemma neg_divide_less_eq:
  1731  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1732 proof -
  1733   assume less: "c<0"
  1734   hence "(b/c < a) = (a*c < (b/c)*c)"
  1735     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1736   also have "... = (a*c < b)"
  1737     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1738   finally show ?thesis .
  1739 qed
  1740 
  1741 lemma divide_less_eq:
  1742   "(b/c < a) = 
  1743    (if 0 < c then b < a*c
  1744              else if c < 0 then a*c < b
  1745              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1746 apply (cases "c=0", simp) 
  1747 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1748 done
  1749 
  1750 
  1751 subsection{*Field simplification*}
  1752 
  1753 text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
  1754 if they can be proved to be non-zero (for equations) or positive/negative
  1755 (for inequations). Can be too aggressive and is therefore separate from the
  1756 more benign @{text algebra_simps}. *}
  1757 
  1758 lemmas field_simps[noatp] = field_eq_simps
  1759   (* multiply ineqn *)
  1760   pos_divide_less_eq neg_divide_less_eq
  1761   pos_less_divide_eq neg_less_divide_eq
  1762   pos_divide_le_eq neg_divide_le_eq
  1763   pos_le_divide_eq neg_le_divide_eq
  1764 
  1765 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1766 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1767 sign_simps} to @{text field_simps} because the former can lead to case
  1768 explosions. *}
  1769 
  1770 lemmas sign_simps[noatp] = group_simps
  1771   zero_less_mult_iff  mult_less_0_iff
  1772 
  1773 (* Only works once linear arithmetic is installed:
  1774 text{*An example:*}
  1775 lemma fixes a b c d e f :: "'a::ordered_field"
  1776 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1777  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1778  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1779 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1780  prefer 2 apply(simp add:sign_simps)
  1781 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1782  prefer 2 apply(simp add:sign_simps)
  1783 apply(simp add:field_simps)
  1784 done
  1785 *)
  1786 
  1787 
  1788 subsection{*Division and Signs*}
  1789 
  1790 lemma zero_less_divide_iff:
  1791      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1792 by (simp add: divide_inverse zero_less_mult_iff)
  1793 
  1794 lemma divide_less_0_iff:
  1795      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1796       (0 < a & b < 0 | a < 0 & 0 < b)"
  1797 by (simp add: divide_inverse mult_less_0_iff)
  1798 
  1799 lemma zero_le_divide_iff:
  1800      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1801       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1802 by (simp add: divide_inverse zero_le_mult_iff)
  1803 
  1804 lemma divide_le_0_iff:
  1805      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1806       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1807 by (simp add: divide_inverse mult_le_0_iff)
  1808 
  1809 lemma divide_eq_0_iff [simp,noatp]:
  1810      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1811 by (simp add: divide_inverse)
  1812 
  1813 lemma divide_pos_pos:
  1814   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
  1815 by(simp add:field_simps)
  1816 
  1817 
  1818 lemma divide_nonneg_pos:
  1819   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
  1820 by(simp add:field_simps)
  1821 
  1822 lemma divide_neg_pos:
  1823   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1824 by(simp add:field_simps)
  1825 
  1826 lemma divide_nonpos_pos:
  1827   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1828 by(simp add:field_simps)
  1829 
  1830 lemma divide_pos_neg:
  1831   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  1832 by(simp add:field_simps)
  1833 
  1834 lemma divide_nonneg_neg:
  1835   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
  1836 by(simp add:field_simps)
  1837 
  1838 lemma divide_neg_neg:
  1839   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1840 by(simp add:field_simps)
  1841 
  1842 lemma divide_nonpos_neg:
  1843   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1844 by(simp add:field_simps)
  1845 
  1846 
  1847 subsection{*Cancellation Laws for Division*}
  1848 
  1849 lemma divide_cancel_right [simp,noatp]:
  1850      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1851 apply (cases "c=0", simp)
  1852 apply (simp add: divide_inverse)
  1853 done
  1854 
  1855 lemma divide_cancel_left [simp,noatp]:
  1856      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1857 apply (cases "c=0", simp)
  1858 apply (simp add: divide_inverse)
  1859 done
  1860 
  1861 
  1862 subsection {* Division and the Number One *}
  1863 
  1864 text{*Simplify expressions equated with 1*}
  1865 lemma divide_eq_1_iff [simp,noatp]:
  1866      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1867 apply (cases "b=0", simp)
  1868 apply (simp add: right_inverse_eq)
  1869 done
  1870 
  1871 lemma one_eq_divide_iff [simp,noatp]:
  1872      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1873 by (simp add: eq_commute [of 1])
  1874 
  1875 lemma zero_eq_1_divide_iff [simp,noatp]:
  1876      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1877 apply (cases "a=0", simp)
  1878 apply (auto simp add: nonzero_eq_divide_eq)
  1879 done
  1880 
  1881 lemma one_divide_eq_0_iff [simp,noatp]:
  1882      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  1883 apply (cases "a=0", simp)
  1884 apply (insert zero_neq_one [THEN not_sym])
  1885 apply (auto simp add: nonzero_divide_eq_eq)
  1886 done
  1887 
  1888 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1889 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1890 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1891 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1892 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1893 
  1894 declare zero_less_divide_1_iff [simp,noatp]
  1895 declare divide_less_0_1_iff [simp,noatp]
  1896 declare zero_le_divide_1_iff [simp,noatp]
  1897 declare divide_le_0_1_iff [simp,noatp]
  1898 
  1899 
  1900 subsection {* Ordering Rules for Division *}
  1901 
  1902 lemma divide_strict_right_mono:
  1903      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1904 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1905               positive_imp_inverse_positive)
  1906 
  1907 lemma divide_right_mono:
  1908      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1909 by (force simp add: divide_strict_right_mono order_le_less)
  1910 
  1911 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1912     ==> c <= 0 ==> b / c <= a / c"
  1913 apply (drule divide_right_mono [of _ _ "- c"])
  1914 apply auto
  1915 done
  1916 
  1917 lemma divide_strict_right_mono_neg:
  1918      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1919 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1920 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1921 done
  1922 
  1923 text{*The last premise ensures that @{term a} and @{term b} 
  1924       have the same sign*}
  1925 lemma divide_strict_left_mono:
  1926   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1927 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1928 
  1929 lemma divide_left_mono:
  1930   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1931 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1932 
  1933 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1934     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1935   apply (drule divide_left_mono [of _ _ "- c"])
  1936   apply (auto simp add: mult_commute)
  1937 done
  1938 
  1939 lemma divide_strict_left_mono_neg:
  1940   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1941 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1942 
  1943 
  1944 text{*Simplify quotients that are compared with the value 1.*}
  1945 
  1946 lemma le_divide_eq_1 [noatp]:
  1947   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1948   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1949 by (auto simp add: le_divide_eq)
  1950 
  1951 lemma divide_le_eq_1 [noatp]:
  1952   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1953   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1954 by (auto simp add: divide_le_eq)
  1955 
  1956 lemma less_divide_eq_1 [noatp]:
  1957   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1958   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1959 by (auto simp add: less_divide_eq)
  1960 
  1961 lemma divide_less_eq_1 [noatp]:
  1962   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1963   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1964 by (auto simp add: divide_less_eq)
  1965 
  1966 
  1967 subsection{*Conditional Simplification Rules: No Case Splits*}
  1968 
  1969 lemma le_divide_eq_1_pos [simp,noatp]:
  1970   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1971   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1972 by (auto simp add: le_divide_eq)
  1973 
  1974 lemma le_divide_eq_1_neg [simp,noatp]:
  1975   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1976   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1977 by (auto simp add: le_divide_eq)
  1978 
  1979 lemma divide_le_eq_1_pos [simp,noatp]:
  1980   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1981   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1982 by (auto simp add: divide_le_eq)
  1983 
  1984 lemma divide_le_eq_1_neg [simp,noatp]:
  1985   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1986   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1987 by (auto simp add: divide_le_eq)
  1988 
  1989 lemma less_divide_eq_1_pos [simp,noatp]:
  1990   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1991   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  1992 by (auto simp add: less_divide_eq)
  1993 
  1994 lemma less_divide_eq_1_neg [simp,noatp]:
  1995   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1996   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  1997 by (auto simp add: less_divide_eq)
  1998 
  1999 lemma divide_less_eq_1_pos [simp,noatp]:
  2000   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2001   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  2002 by (auto simp add: divide_less_eq)
  2003 
  2004 lemma divide_less_eq_1_neg [simp,noatp]:
  2005   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2006   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  2007 by (auto simp add: divide_less_eq)
  2008 
  2009 lemma eq_divide_eq_1 [simp,noatp]:
  2010   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2011   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  2012 by (auto simp add: eq_divide_eq)
  2013 
  2014 lemma divide_eq_eq_1 [simp,noatp]:
  2015   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2016   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  2017 by (auto simp add: divide_eq_eq)
  2018 
  2019 
  2020 subsection {* Reasoning about inequalities with division *}
  2021 
  2022 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2023     ==> x * y <= x"
  2024 by (auto simp add: mult_compare_simps);
  2025 
  2026 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2027     ==> y * x <= x"
  2028 by (auto simp add: mult_compare_simps);
  2029 
  2030 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  2031     x / y <= z";
  2032 by (subst pos_divide_le_eq, assumption+);
  2033 
  2034 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  2035     z <= x / y"
  2036 by(simp add:field_simps)
  2037 
  2038 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  2039     x / y < z"
  2040 by(simp add:field_simps)
  2041 
  2042 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  2043     z < x / y"
  2044 by(simp add:field_simps)
  2045 
  2046 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  2047     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2048   apply (rule mult_imp_div_pos_le)
  2049   apply simp
  2050   apply (subst times_divide_eq_left)
  2051   apply (rule mult_imp_le_div_pos, assumption)
  2052   apply (rule mult_mono)
  2053   apply simp_all
  2054 done
  2055 
  2056 lemma frac_less: "(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;
  2060   apply (subst times_divide_eq_left);
  2061   apply (rule mult_imp_less_div_pos, assumption)
  2062   apply (erule mult_less_le_imp_less)
  2063   apply simp_all
  2064 done
  2065 
  2066 lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  2067     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2068   apply (rule mult_imp_div_pos_less)
  2069   apply simp_all
  2070   apply (subst times_divide_eq_left);
  2071   apply (rule mult_imp_less_div_pos, assumption)
  2072   apply (erule mult_le_less_imp_less)
  2073   apply simp_all
  2074 done
  2075 
  2076 text{*It's not obvious whether these should be simprules or not. 
  2077   Their effect is to gather terms into one big fraction, like
  2078   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2079   seem to need them.*}
  2080 
  2081 declare times_divide_eq [simp]
  2082 
  2083 
  2084 subsection {* Ordered Fields are Dense *}
  2085 
  2086 context ordered_semidom
  2087 begin
  2088 
  2089 lemma less_add_one: "a < a + 1"
  2090 proof -
  2091   have "a + 0 < a + 1"
  2092     by (blast intro: zero_less_one add_strict_left_mono)
  2093   thus ?thesis by simp
  2094 qed
  2095 
  2096 lemma zero_less_two: "0 < 1 + 1"
  2097 by (blast intro: less_trans zero_less_one less_add_one)
  2098 
  2099 end
  2100 
  2101 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  2102 by (simp add: field_simps zero_less_two)
  2103 
  2104 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  2105 by (simp add: field_simps zero_less_two)
  2106 
  2107 instance ordered_field < dense_linear_order
  2108 proof
  2109   fix x y :: 'a
  2110   have "x < x + 1" by simp
  2111   then show "\<exists>y. x < y" .. 
  2112   have "x - 1 < x" by simp
  2113   then show "\<exists>y. y < x" ..
  2114   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2115 qed
  2116 
  2117 
  2118 subsection {* Absolute Value *}
  2119 
  2120 context ordered_idom
  2121 begin
  2122 
  2123 lemma mult_sgn_abs: "sgn x * abs x = x"
  2124   unfolding abs_if sgn_if by auto
  2125 
  2126 end
  2127 
  2128 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  2129 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2130 
  2131 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
  2132   assumes abs_eq_mult:
  2133     "(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>"
  2134 
  2135 
  2136 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
  2137 begin
  2138 
  2139 subclass lordered_ab_group_add_meet ..
  2140 subclass lordered_ab_group_add_join ..
  2141 
  2142 end
  2143 
  2144 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  2145 proof -
  2146   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  2147   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2148   have a: "(abs a) * (abs b) = ?x"
  2149     by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
  2150   {
  2151     fix u v :: 'a
  2152     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  2153               u * v = pprt a * pprt b + pprt a * nprt b + 
  2154                       nprt a * pprt b + nprt a * nprt b"
  2155       apply (subst prts[of u], subst prts[of v])
  2156       apply (simp add: algebra_simps) 
  2157       done
  2158   }
  2159   note b = this[OF refl[of a] refl[of b]]
  2160   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
  2161   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
  2162   have xy: "- ?x <= ?y"
  2163     apply (simp)
  2164     apply (rule_tac y="0::'a" in order_trans)
  2165     apply (rule addm2)
  2166     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2167     apply (rule addm)
  2168     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2169     done
  2170   have yx: "?y <= ?x"
  2171     apply (simp add:diff_def)
  2172     apply (rule_tac y=0 in order_trans)
  2173     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2174     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2175     done
  2176   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  2177   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  2178   show ?thesis
  2179     apply (rule abs_leI)
  2180     apply (simp add: i1)
  2181     apply (simp add: i2[simplified minus_le_iff])
  2182     done
  2183 qed
  2184 
  2185 instance lordered_ring \<subseteq> pordered_ring_abs
  2186 proof
  2187   fix a b :: "'a\<Colon> lordered_ring"
  2188   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
  2189   show "abs (a*b) = abs a * abs b"
  2190 proof -
  2191   have s: "(0 <= a*b) | (a*b <= 0)"
  2192     apply (auto)    
  2193     apply (rule_tac split_mult_pos_le)
  2194     apply (rule_tac contrapos_np[of "a*b <= 0"])
  2195     apply (simp)
  2196     apply (rule_tac split_mult_neg_le)
  2197     apply (insert prems)
  2198     apply (blast)
  2199     done
  2200   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
  2201     by (simp add: prts[symmetric])
  2202   show ?thesis
  2203   proof cases
  2204     assume "0 <= a * b"
  2205     then show ?thesis
  2206       apply (simp_all add: mulprts abs_prts)
  2207       apply (insert prems)
  2208       apply (auto simp add: 
  2209 	algebra_simps 
  2210 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
  2211 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
  2212 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  2213 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  2214       done
  2215   next
  2216     assume "~(0 <= a*b)"
  2217     with s have "a*b <= 0" by simp
  2218     then show ?thesis
  2219       apply (simp_all add: mulprts abs_prts)
  2220       apply (insert prems)
  2221       apply (auto simp add: algebra_simps)
  2222       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  2223       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  2224       done
  2225   qed
  2226 qed
  2227 qed
  2228 
  2229 context ordered_idom
  2230 begin
  2231 
  2232 subclass pordered_ring_abs proof
  2233 qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
  2234 
  2235 lemma abs_mult:
  2236   "abs (a * b) = abs a * abs b" 
  2237   by (rule abs_eq_mult) auto
  2238 
  2239 lemma abs_mult_self:
  2240   "abs a * abs a = a * a"
  2241   by (simp add: abs_if) 
  2242 
  2243 end
  2244 
  2245 lemma nonzero_abs_inverse:
  2246      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  2247 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2248                       negative_imp_inverse_negative)
  2249 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2250 done
  2251 
  2252 lemma abs_inverse [simp]:
  2253      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  2254       inverse (abs a)"
  2255 apply (cases "a=0", simp) 
  2256 apply (simp add: nonzero_abs_inverse) 
  2257 done
  2258 
  2259 lemma nonzero_abs_divide:
  2260      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  2261 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2262 
  2263 lemma abs_divide [simp]:
  2264      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  2265 apply (cases "b=0", simp) 
  2266 apply (simp add: nonzero_abs_divide) 
  2267 done
  2268 
  2269 lemma abs_mult_less:
  2270      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
  2271 proof -
  2272   assume ac: "abs a < c"
  2273   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2274   assume "abs b < d"
  2275   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2276 qed
  2277 
  2278 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  2279 
  2280 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
  2281   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2282 
  2283 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
  2284 apply (simp add: order_less_le abs_le_iff)  
  2285 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2286 done
  2287 
  2288 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  2289     (abs y) * x = abs (y * x)"
  2290   apply (subst abs_mult)
  2291   apply simp
  2292 done
  2293 
  2294 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  2295     abs x / y = abs (x / y)"
  2296   apply (subst abs_divide)
  2297   apply (simp add: order_less_imp_le)
  2298 done
  2299 
  2300 
  2301 subsection {* Bounds of products via negative and positive Part *}
  2302 
  2303 lemma mult_le_prts:
  2304   assumes
  2305   "a1 <= (a::'a::lordered_ring)"
  2306   "a <= a2"
  2307   "b1 <= b"
  2308   "b <= b2"
  2309   shows
  2310   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  2311 proof - 
  2312   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  2313     apply (subst prts[symmetric])+
  2314     apply simp
  2315     done
  2316   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2317     by (simp add: algebra_simps)
  2318   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  2319     by (simp_all add: prems mult_mono)
  2320   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  2321   proof -
  2322     have "pprt a * nprt b <= pprt a * nprt b2"
  2323       by (simp add: mult_left_mono prems)
  2324     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  2325       by (simp add: mult_right_mono_neg prems)
  2326     ultimately show ?thesis
  2327       by simp
  2328   qed
  2329   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  2330   proof - 
  2331     have "nprt a * pprt b <= nprt a2 * pprt b"
  2332       by (simp add: mult_right_mono prems)
  2333     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  2334       by (simp add: mult_left_mono_neg prems)
  2335     ultimately show ?thesis
  2336       by simp
  2337   qed
  2338   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  2339   proof -
  2340     have "nprt a * nprt b <= nprt a * nprt b1"
  2341       by (simp add: mult_left_mono_neg prems)
  2342     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  2343       by (simp add: mult_right_mono_neg prems)
  2344     ultimately show ?thesis
  2345       by simp
  2346   qed
  2347   ultimately show ?thesis
  2348     by - (rule add_mono | simp)+
  2349 qed
  2350 
  2351 lemma mult_ge_prts:
  2352   assumes
  2353   "a1 <= (a::'a::lordered_ring)"
  2354   "a <= a2"
  2355   "b1 <= b"
  2356   "b <= b2"
  2357   shows
  2358   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  2359 proof - 
  2360   from prems have a1:"- a2 <= -a" by auto
  2361   from prems have a2: "-a <= -a1" by auto
  2362   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  2363   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  2364   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  2365     by (simp only: minus_le_iff)
  2366   then show ?thesis by simp
  2367 qed
  2368 
  2369 end