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