src/HOL/Ring_and_Field.thy
author haftmann
Mon Feb 08 14:22:22 2010 +0100 (2010-02-08)
changeset 35043 07dbdf60d5ad
parent 35032 7efe662e41b4
permissions -rw-r--r--
dropped accidental duplication of "lin" prefix from cs. 108662d50512
     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 minus_unique) (simp add: left_distrib [symmetric]) 
   232 
   233 lemma minus_mult_right: "- (a * b) = a * - b"
   234 by (rule minus_unique) (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 ordered_semiring = mult_mono + semiring_0 + ordered_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 ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
   729   + semiring + cancel_comm_monoid_add
   730 begin
   731 
   732 subclass semiring_0_cancel ..
   733 subclass ordered_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 linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
   754 begin
   755 
   756 subclass ordered_cancel_semiring ..
   757 
   758 subclass ordered_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 linordered_semiring_1 = linordered_semiring + semiring_1
   771 
   772 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_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 linordered_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 linlinordered_semiring_1_strict = linordered_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 ordered_comm_semiring = comm_semiring_0
   895   + ordered_ab_semigroup_add + mult_mono1
   896 begin
   897 
   898 subclass ordered_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 ordered_cancel_comm_semiring = comm_semiring_0_cancel
   909   + ordered_ab_semigroup_add + mult_mono1
   910 begin
   911 
   912 subclass ordered_comm_semiring ..
   913 subclass ordered_cancel_semiring ..
   914 
   915 end
   916 
   917 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_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 linordered_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 ordered_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 ordered_ring = ring + ordered_cancel_semiring 
   941 begin
   942 
   943 subclass ordered_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 linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   995 begin
   996 
   997 subclass ordered_ring ..
   998 
   999 subclass ordered_ab_group_add_abs
  1000 proof
  1001   fix a b
  1002   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1003     by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
  1004     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
  1005      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
  1006       auto intro!: less_imp_le add_neg_neg)
  1007 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
  1008 
  1009 end
  1010 
  1011 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
  1012    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
  1013  *)
  1014 class linordered_ring_strict = ring + linordered_semiring_strict
  1015   + ordered_ab_group_add + abs_if
  1016 begin
  1017 
  1018 subclass linordered_ring ..
  1019 
  1020 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
  1021 using mult_strict_left_mono [of b a "- c"] by simp
  1022 
  1023 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
  1024 using mult_strict_right_mono [of b a "- c"] by simp
  1025 
  1026 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  1027 using mult_strict_right_mono_neg [of a zero b] by simp
  1028 
  1029 subclass ring_no_zero_divisors
  1030 proof
  1031   fix a b
  1032   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
  1033   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
  1034   have "a * b < 0 \<or> 0 < a * b"
  1035   proof (cases "a < 0")
  1036     case True note A' = this
  1037     show ?thesis proof (cases "b < 0")
  1038       case True with A'
  1039       show ?thesis by (auto dest: mult_neg_neg)
  1040     next
  1041       case False with B have "0 < b" by auto
  1042       with A' show ?thesis by (auto dest: mult_strict_right_mono)
  1043     qed
  1044   next
  1045     case False with A have A': "0 < a" by auto
  1046     show ?thesis proof (cases "b < 0")
  1047       case True with A'
  1048       show ?thesis by (auto dest: mult_strict_right_mono_neg)
  1049     next
  1050       case False with B have "0 < b" by auto
  1051       with A' show ?thesis by (auto dest: mult_pos_pos)
  1052     qed
  1053   qed
  1054   then show "a * b \<noteq> 0" by (simp add: neq_iff)
  1055 qed
  1056 
  1057 lemma zero_less_mult_iff:
  1058   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
  1059   apply (auto simp add: mult_pos_pos mult_neg_neg)
  1060   apply (simp_all add: not_less le_less)
  1061   apply (erule disjE) apply assumption defer
  1062   apply (erule disjE) defer apply (drule sym) apply simp
  1063   apply (erule disjE) defer apply (drule sym) apply simp
  1064   apply (erule disjE) apply assumption apply (drule sym) apply simp
  1065   apply (drule sym) apply simp
  1066   apply (blast dest: zero_less_mult_pos)
  1067   apply (blast dest: zero_less_mult_pos2)
  1068   done
  1069 
  1070 lemma zero_le_mult_iff:
  1071   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
  1072 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
  1073 
  1074 lemma mult_less_0_iff:
  1075   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
  1076   apply (insert zero_less_mult_iff [of "-a" b]) 
  1077   apply (force simp add: minus_mult_left[symmetric]) 
  1078   done
  1079 
  1080 lemma mult_le_0_iff:
  1081   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
  1082   apply (insert zero_le_mult_iff [of "-a" b]) 
  1083   apply (force simp add: minus_mult_left[symmetric]) 
  1084   done
  1085 
  1086 lemma zero_le_square [simp]: "0 \<le> a * a"
  1087 by (simp add: zero_le_mult_iff linear)
  1088 
  1089 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
  1090 by (simp add: not_less)
  1091 
  1092 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  1093    also with the relations @{text "\<le>"} and equality.*}
  1094 
  1095 text{*These ``disjunction'' versions produce two cases when the comparison is
  1096  an assumption, but effectively four when the comparison is a goal.*}
  1097 
  1098 lemma mult_less_cancel_right_disj:
  1099   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1100   apply (cases "c = 0")
  1101   apply (auto simp add: neq_iff mult_strict_right_mono 
  1102                       mult_strict_right_mono_neg)
  1103   apply (auto simp add: not_less 
  1104                       not_le [symmetric, of "a*c"]
  1105                       not_le [symmetric, of a])
  1106   apply (erule_tac [!] notE)
  1107   apply (auto simp add: less_imp_le mult_right_mono 
  1108                       mult_right_mono_neg)
  1109   done
  1110 
  1111 lemma mult_less_cancel_left_disj:
  1112   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
  1113   apply (cases "c = 0")
  1114   apply (auto simp add: neq_iff mult_strict_left_mono 
  1115                       mult_strict_left_mono_neg)
  1116   apply (auto simp add: not_less 
  1117                       not_le [symmetric, of "c*a"]
  1118                       not_le [symmetric, of a])
  1119   apply (erule_tac [!] notE)
  1120   apply (auto simp add: less_imp_le mult_left_mono 
  1121                       mult_left_mono_neg)
  1122   done
  1123 
  1124 text{*The ``conjunction of implication'' lemmas produce two cases when the
  1125 comparison is a goal, but give four when the comparison is an assumption.*}
  1126 
  1127 lemma mult_less_cancel_right:
  1128   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1129   using mult_less_cancel_right_disj [of a c b] by auto
  1130 
  1131 lemma mult_less_cancel_left:
  1132   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
  1133   using mult_less_cancel_left_disj [of c a b] by auto
  1134 
  1135 lemma mult_le_cancel_right:
  1136    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1137 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
  1138 
  1139 lemma mult_le_cancel_left:
  1140   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
  1141 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
  1142 
  1143 lemma mult_le_cancel_left_pos:
  1144   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
  1145 by (auto simp: mult_le_cancel_left)
  1146 
  1147 lemma mult_le_cancel_left_neg:
  1148   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
  1149 by (auto simp: mult_le_cancel_left)
  1150 
  1151 lemma mult_less_cancel_left_pos:
  1152   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
  1153 by (auto simp: mult_less_cancel_left)
  1154 
  1155 lemma mult_less_cancel_left_neg:
  1156   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
  1157 by (auto simp: mult_less_cancel_left)
  1158 
  1159 end
  1160 
  1161 text{*Legacy - use @{text algebra_simps} *}
  1162 lemmas ring_simps[noatp] = algebra_simps
  1163 
  1164 lemmas mult_sign_intros =
  1165   mult_nonneg_nonneg mult_nonneg_nonpos
  1166   mult_nonpos_nonneg mult_nonpos_nonpos
  1167   mult_pos_pos mult_pos_neg
  1168   mult_neg_pos mult_neg_neg
  1169 
  1170 class ordered_comm_ring = comm_ring + ordered_comm_semiring
  1171 begin
  1172 
  1173 subclass ordered_ring ..
  1174 subclass ordered_cancel_comm_semiring ..
  1175 
  1176 end
  1177 
  1178 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
  1179   (*previously linordered_semiring*)
  1180   assumes zero_less_one [simp]: "0 < 1"
  1181 begin
  1182 
  1183 lemma pos_add_strict:
  1184   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1185   using add_strict_mono [of zero a b c] by simp
  1186 
  1187 lemma zero_le_one [simp]: "0 \<le> 1"
  1188 by (rule zero_less_one [THEN less_imp_le]) 
  1189 
  1190 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
  1191 by (simp add: not_le) 
  1192 
  1193 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
  1194 by (simp add: not_less) 
  1195 
  1196 lemma less_1_mult:
  1197   assumes "1 < m" and "1 < n"
  1198   shows "1 < m * n"
  1199   using assms mult_strict_mono [of 1 m 1 n]
  1200     by (simp add:  less_trans [OF zero_less_one]) 
  1201 
  1202 end
  1203 
  1204 class linordered_idom = comm_ring_1 +
  1205   linordered_comm_semiring_strict + ordered_ab_group_add +
  1206   abs_if + sgn_if
  1207   (*previously linordered_ring*)
  1208 begin
  1209 
  1210 subclass linordered_ring_strict ..
  1211 subclass ordered_comm_ring ..
  1212 subclass idom ..
  1213 
  1214 subclass linordered_semidom
  1215 proof
  1216   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1217   thus "0 < 1" by (simp add: le_less)
  1218 qed 
  1219 
  1220 lemma linorder_neqE_linordered_idom:
  1221   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1222   using assms by (rule neqE)
  1223 
  1224 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1225 
  1226 lemma mult_le_cancel_right1:
  1227   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1228 by (insert mult_le_cancel_right [of 1 c b], simp)
  1229 
  1230 lemma mult_le_cancel_right2:
  1231   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1232 by (insert mult_le_cancel_right [of a c 1], simp)
  1233 
  1234 lemma mult_le_cancel_left1:
  1235   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1236 by (insert mult_le_cancel_left [of c 1 b], simp)
  1237 
  1238 lemma mult_le_cancel_left2:
  1239   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1240 by (insert mult_le_cancel_left [of c a 1], simp)
  1241 
  1242 lemma mult_less_cancel_right1:
  1243   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1244 by (insert mult_less_cancel_right [of 1 c b], simp)
  1245 
  1246 lemma mult_less_cancel_right2:
  1247   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1248 by (insert mult_less_cancel_right [of a c 1], simp)
  1249 
  1250 lemma mult_less_cancel_left1:
  1251   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1252 by (insert mult_less_cancel_left [of c 1 b], simp)
  1253 
  1254 lemma mult_less_cancel_left2:
  1255   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1256 by (insert mult_less_cancel_left [of c a 1], simp)
  1257 
  1258 lemma sgn_sgn [simp]:
  1259   "sgn (sgn a) = sgn a"
  1260 unfolding sgn_if by simp
  1261 
  1262 lemma sgn_0_0:
  1263   "sgn a = 0 \<longleftrightarrow> a = 0"
  1264 unfolding sgn_if by simp
  1265 
  1266 lemma sgn_1_pos:
  1267   "sgn a = 1 \<longleftrightarrow> a > 0"
  1268 unfolding sgn_if by (simp add: neg_equal_zero)
  1269 
  1270 lemma sgn_1_neg:
  1271   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1272 unfolding sgn_if by (auto simp add: equal_neg_zero)
  1273 
  1274 lemma sgn_pos [simp]:
  1275   "0 < a \<Longrightarrow> sgn a = 1"
  1276 unfolding sgn_1_pos .
  1277 
  1278 lemma sgn_neg [simp]:
  1279   "a < 0 \<Longrightarrow> sgn a = - 1"
  1280 unfolding sgn_1_neg .
  1281 
  1282 lemma sgn_times:
  1283   "sgn (a * b) = sgn a * sgn b"
  1284 by (auto simp add: sgn_if zero_less_mult_iff)
  1285 
  1286 lemma abs_sgn: "abs k = k * sgn k"
  1287 unfolding sgn_if abs_if by auto
  1288 
  1289 lemma sgn_greater [simp]:
  1290   "0 < sgn a \<longleftrightarrow> 0 < a"
  1291   unfolding sgn_if by auto
  1292 
  1293 lemma sgn_less [simp]:
  1294   "sgn a < 0 \<longleftrightarrow> a < 0"
  1295   unfolding sgn_if by auto
  1296 
  1297 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  1298   by (simp add: abs_if)
  1299 
  1300 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  1301   by (simp add: abs_if)
  1302 
  1303 lemma dvd_if_abs_eq:
  1304   "abs l = abs (k) \<Longrightarrow> l dvd k"
  1305 by(subst abs_dvd_iff[symmetric]) simp
  1306 
  1307 end
  1308 
  1309 class linordered_field = field + linordered_idom
  1310 
  1311 text {* Simprules for comparisons where common factors can be cancelled. *}
  1312 
  1313 lemmas mult_compare_simps[noatp] =
  1314     mult_le_cancel_right mult_le_cancel_left
  1315     mult_le_cancel_right1 mult_le_cancel_right2
  1316     mult_le_cancel_left1 mult_le_cancel_left2
  1317     mult_less_cancel_right mult_less_cancel_left
  1318     mult_less_cancel_right1 mult_less_cancel_right2
  1319     mult_less_cancel_left1 mult_less_cancel_left2
  1320     mult_cancel_right mult_cancel_left
  1321     mult_cancel_right1 mult_cancel_right2
  1322     mult_cancel_left1 mult_cancel_left2
  1323 
  1324 -- {* FIXME continue localization here *}
  1325 
  1326 lemma inverse_nonzero_iff_nonzero [simp]:
  1327    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
  1328 by (force dest: inverse_zero_imp_zero) 
  1329 
  1330 lemma inverse_minus_eq [simp]:
  1331    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
  1332 proof cases
  1333   assume "a=0" thus ?thesis by (simp add: inverse_zero)
  1334 next
  1335   assume "a\<noteq>0" 
  1336   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  1337 qed
  1338 
  1339 lemma inverse_eq_imp_eq:
  1340   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
  1341 apply (cases "a=0 | b=0") 
  1342  apply (force dest!: inverse_zero_imp_zero
  1343               simp add: eq_commute [of "0::'a"])
  1344 apply (force dest!: nonzero_inverse_eq_imp_eq) 
  1345 done
  1346 
  1347 lemma inverse_eq_iff_eq [simp]:
  1348   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
  1349 by (force dest!: inverse_eq_imp_eq)
  1350 
  1351 lemma inverse_inverse_eq [simp]:
  1352      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
  1353   proof cases
  1354     assume "a=0" thus ?thesis by simp
  1355   next
  1356     assume "a\<noteq>0" 
  1357     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  1358   qed
  1359 
  1360 text{*This version builds in division by zero while also re-orienting
  1361       the right-hand side.*}
  1362 lemma inverse_mult_distrib [simp]:
  1363      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
  1364   proof cases
  1365     assume "a \<noteq> 0 & b \<noteq> 0" 
  1366     thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
  1367   next
  1368     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
  1369     thus ?thesis by force
  1370   qed
  1371 
  1372 lemma inverse_divide [simp]:
  1373   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  1374 by (simp add: divide_inverse mult_commute)
  1375 
  1376 
  1377 subsection {* Calculations with fractions *}
  1378 
  1379 text{* There is a whole bunch of simp-rules just for class @{text
  1380 field} but none for class @{text field} and @{text nonzero_divides}
  1381 because the latter are covered by a simproc. *}
  1382 
  1383 lemma mult_divide_mult_cancel_left:
  1384   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  1385 apply (cases "b = 0")
  1386 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  1387 done
  1388 
  1389 lemma mult_divide_mult_cancel_right:
  1390   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  1391 apply (cases "b = 0")
  1392 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  1393 done
  1394 
  1395 lemma divide_divide_eq_right [simp,noatp]:
  1396   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  1397 by (simp add: divide_inverse mult_ac)
  1398 
  1399 lemma divide_divide_eq_left [simp,noatp]:
  1400   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  1401 by (simp add: divide_inverse mult_assoc)
  1402 
  1403 
  1404 subsubsection{*Special Cancellation Simprules for Division*}
  1405 
  1406 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
  1407 fixes c :: "'a :: {field,division_by_zero}"
  1408 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  1409 by (simp add: mult_divide_mult_cancel_left)
  1410 
  1411 
  1412 subsection {* Division and Unary Minus *}
  1413 
  1414 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1415 by (simp add: divide_inverse)
  1416 
  1417 lemma divide_minus_right [simp, noatp]:
  1418   "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
  1419 by (simp add: divide_inverse)
  1420 
  1421 lemma minus_divide_divide:
  1422   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1423 apply (cases "b=0", simp) 
  1424 apply (simp add: nonzero_minus_divide_divide) 
  1425 done
  1426 
  1427 lemma eq_divide_eq:
  1428   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1429 by (simp add: nonzero_eq_divide_eq)
  1430 
  1431 lemma divide_eq_eq:
  1432   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1433 by (force simp add: nonzero_divide_eq_eq)
  1434 
  1435 
  1436 subsection {* Ordered Fields *}
  1437 
  1438 lemma positive_imp_inverse_positive: 
  1439 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"
  1440 proof -
  1441   have "0 < a * inverse a" 
  1442     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1443   thus "0 < inverse a" 
  1444     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1445 qed
  1446 
  1447 lemma negative_imp_inverse_negative:
  1448   "a < 0 ==> inverse a < (0::'a::linordered_field)"
  1449 by (insert positive_imp_inverse_positive [of "-a"], 
  1450     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1451 
  1452 lemma inverse_le_imp_le:
  1453 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1454 shows "b \<le> (a::'a::linordered_field)"
  1455 proof (rule classical)
  1456   assume "~ b \<le> a"
  1457   hence "a < b"  by (simp add: linorder_not_le)
  1458   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1459   hence "a * inverse a \<le> a * inverse b"
  1460     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1461   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1462     by (simp add: bpos order_less_imp_le mult_right_mono)
  1463   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1464 qed
  1465 
  1466 lemma inverse_positive_imp_positive:
  1467 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1468 shows "0 < (a::'a::linordered_field)"
  1469 proof -
  1470   have "0 < inverse (inverse a)"
  1471     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1472   thus "0 < a"
  1473     using nz by (simp add: nonzero_inverse_inverse_eq)
  1474 qed
  1475 
  1476 lemma inverse_positive_iff_positive [simp]:
  1477   "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"
  1478 apply (cases "a = 0", simp)
  1479 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1480 done
  1481 
  1482 lemma inverse_negative_imp_negative:
  1483 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1484 shows "a < (0::'a::linordered_field)"
  1485 proof -
  1486   have "inverse (inverse a) < 0"
  1487     using inv_less_0 by (rule negative_imp_inverse_negative)
  1488   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1489 qed
  1490 
  1491 lemma inverse_negative_iff_negative [simp]:
  1492   "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"
  1493 apply (cases "a = 0", simp)
  1494 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1495 done
  1496 
  1497 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1498   "(0 \<le> inverse a) = (0 \<le> (a::'a::{linordered_field,division_by_zero}))"
  1499 by (simp add: linorder_not_less [symmetric])
  1500 
  1501 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1502   "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
  1503 by (simp add: linorder_not_less [symmetric])
  1504 
  1505 lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
  1506 proof
  1507   fix x::'a
  1508   have m1: "- (1::'a) < 0" by simp
  1509   from add_strict_right_mono[OF m1, where c=x] 
  1510   have "(- 1) + x < x" by simp
  1511   thus "\<exists>y. y < x" by blast
  1512 qed
  1513 
  1514 lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
  1515 proof
  1516   fix x::'a
  1517   have m1: " (1::'a) > 0" by simp
  1518   from add_strict_right_mono[OF m1, where c=x] 
  1519   have "1 + x > x" by simp
  1520   thus "\<exists>y. y > x" by blast
  1521 qed
  1522 
  1523 subsection{*Anti-Monotonicity of @{term inverse}*}
  1524 
  1525 lemma less_imp_inverse_less:
  1526 assumes less: "a < b" and apos:  "0 < a"
  1527 shows "inverse b < inverse (a::'a::linordered_field)"
  1528 proof (rule ccontr)
  1529   assume "~ inverse b < inverse a"
  1530   hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
  1531   hence "~ (a < b)"
  1532     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1533   thus False by (rule notE [OF _ less])
  1534 qed
  1535 
  1536 lemma inverse_less_imp_less:
  1537   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)"
  1538 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1539 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1540 done
  1541 
  1542 text{*Both premises are essential. Consider -1 and 1.*}
  1543 lemma inverse_less_iff_less [simp,noatp]:
  1544   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
  1545 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1546 
  1547 lemma le_imp_inverse_le:
  1548   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
  1549 by (force simp add: order_le_less less_imp_inverse_less)
  1550 
  1551 lemma inverse_le_iff_le [simp,noatp]:
  1552  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
  1553 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1554 
  1555 
  1556 text{*These results refer to both operands being negative.  The opposite-sign
  1557 case is trivial, since inverse preserves signs.*}
  1558 lemma inverse_le_imp_le_neg:
  1559   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::linordered_field)"
  1560 apply (rule classical) 
  1561 apply (subgoal_tac "a < 0") 
  1562  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1563 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1564 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1565 done
  1566 
  1567 lemma less_imp_inverse_less_neg:
  1568    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)"
  1569 apply (subgoal_tac "a < 0") 
  1570  prefer 2 apply (blast intro: order_less_trans) 
  1571 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1572 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1573 done
  1574 
  1575 lemma inverse_less_imp_less_neg:
  1576    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)"
  1577 apply (rule classical) 
  1578 apply (subgoal_tac "a < 0") 
  1579  prefer 2
  1580  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1581 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1582 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1583 done
  1584 
  1585 lemma inverse_less_iff_less_neg [simp,noatp]:
  1586   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
  1587 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1588 apply (simp del: inverse_less_iff_less 
  1589             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1590 done
  1591 
  1592 lemma le_imp_inverse_le_neg:
  1593   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
  1594 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1595 
  1596 lemma inverse_le_iff_le_neg [simp,noatp]:
  1597  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
  1598 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1599 
  1600 
  1601 subsection{*Inverses and the Number One*}
  1602 
  1603 lemma one_less_inverse_iff:
  1604   "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))"
  1605 proof cases
  1606   assume "0 < x"
  1607     with inverse_less_iff_less [OF zero_less_one, of x]
  1608     show ?thesis by simp
  1609 next
  1610   assume notless: "~ (0 < x)"
  1611   have "~ (1 < inverse x)"
  1612   proof
  1613     assume "1 < inverse x"
  1614     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1615     also have "... < 1" by (rule zero_less_one) 
  1616     finally show False by auto
  1617   qed
  1618   with notless show ?thesis by simp
  1619 qed
  1620 
  1621 lemma inverse_eq_1_iff [simp]:
  1622   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1623 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1624 
  1625 lemma one_le_inverse_iff:
  1626   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
  1627 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1628                     eq_commute [of 1]) 
  1629 
  1630 lemma inverse_less_1_iff:
  1631   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))"
  1632 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1633 
  1634 lemma inverse_le_1_iff:
  1635   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))"
  1636 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1637 
  1638 
  1639 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1640 
  1641 lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1642 proof -
  1643   assume less: "0<c"
  1644   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1645     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1646   also have "... = (a*c \<le> b)"
  1647     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1648   finally show ?thesis .
  1649 qed
  1650 
  1651 lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1652 proof -
  1653   assume less: "c<0"
  1654   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1655     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1656   also have "... = (b \<le> a*c)"
  1657     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1658   finally show ?thesis .
  1659 qed
  1660 
  1661 lemma le_divide_eq:
  1662   "(a \<le> b/c) = 
  1663    (if 0 < c then a*c \<le> b
  1664              else if c < 0 then b \<le> a*c
  1665              else  a \<le> (0::'a::{linordered_field,division_by_zero}))"
  1666 apply (cases "c=0", simp) 
  1667 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1668 done
  1669 
  1670 lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1671 proof -
  1672   assume less: "0<c"
  1673   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1674     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1675   also have "... = (b \<le> a*c)"
  1676     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1677   finally show ?thesis .
  1678 qed
  1679 
  1680 lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1681 proof -
  1682   assume less: "c<0"
  1683   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1684     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1685   also have "... = (a*c \<le> b)"
  1686     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1687   finally show ?thesis .
  1688 qed
  1689 
  1690 lemma divide_le_eq:
  1691   "(b/c \<le> a) = 
  1692    (if 0 < c then b \<le> a*c
  1693              else if c < 0 then a*c \<le> b
  1694              else 0 \<le> (a::'a::{linordered_field,division_by_zero}))"
  1695 apply (cases "c=0", simp) 
  1696 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1697 done
  1698 
  1699 lemma pos_less_divide_eq:
  1700      "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)"
  1701 proof -
  1702   assume less: "0<c"
  1703   hence "(a < b/c) = (a*c < (b/c)*c)"
  1704     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1705   also have "... = (a*c < b)"
  1706     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1707   finally show ?thesis .
  1708 qed
  1709 
  1710 lemma neg_less_divide_eq:
  1711  "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)"
  1712 proof -
  1713   assume less: "c<0"
  1714   hence "(a < b/c) = ((b/c)*c < a*c)"
  1715     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1716   also have "... = (b < a*c)"
  1717     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1718   finally show ?thesis .
  1719 qed
  1720 
  1721 lemma less_divide_eq:
  1722   "(a < b/c) = 
  1723    (if 0 < c then a*c < b
  1724              else if c < 0 then b < a*c
  1725              else  a < (0::'a::{linordered_field,division_by_zero}))"
  1726 apply (cases "c=0", simp) 
  1727 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1728 done
  1729 
  1730 lemma pos_divide_less_eq:
  1731      "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)"
  1732 proof -
  1733   assume less: "0<c"
  1734   hence "(b/c < a) = ((b/c)*c < a*c)"
  1735     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1736   also have "... = (b < a*c)"
  1737     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1738   finally show ?thesis .
  1739 qed
  1740 
  1741 lemma neg_divide_less_eq:
  1742  "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)"
  1743 proof -
  1744   assume less: "c<0"
  1745   hence "(b/c < a) = (a*c < (b/c)*c)"
  1746     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1747   also have "... = (a*c < b)"
  1748     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1749   finally show ?thesis .
  1750 qed
  1751 
  1752 lemma divide_less_eq:
  1753   "(b/c < a) = 
  1754    (if 0 < c then b < a*c
  1755              else if c < 0 then a*c < b
  1756              else 0 < (a::'a::{linordered_field,division_by_zero}))"
  1757 apply (cases "c=0", simp) 
  1758 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1759 done
  1760 
  1761 
  1762 subsection{*Field simplification*}
  1763 
  1764 text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
  1765 if they can be proved to be non-zero (for equations) or positive/negative
  1766 (for inequations). Can be too aggressive and is therefore separate from the
  1767 more benign @{text algebra_simps}. *}
  1768 
  1769 lemmas field_simps[noatp] = field_eq_simps
  1770   (* multiply ineqn *)
  1771   pos_divide_less_eq neg_divide_less_eq
  1772   pos_less_divide_eq neg_less_divide_eq
  1773   pos_divide_le_eq neg_divide_le_eq
  1774   pos_le_divide_eq neg_le_divide_eq
  1775 
  1776 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1777 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1778 sign_simps} to @{text field_simps} because the former can lead to case
  1779 explosions. *}
  1780 
  1781 lemmas sign_simps[noatp] = group_simps
  1782   zero_less_mult_iff  mult_less_0_iff
  1783 
  1784 (* Only works once linear arithmetic is installed:
  1785 text{*An example:*}
  1786 lemma fixes a b c d e f :: "'a::linordered_field"
  1787 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1788  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1789  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1790 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1791  prefer 2 apply(simp add:sign_simps)
  1792 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1793  prefer 2 apply(simp add:sign_simps)
  1794 apply(simp add:field_simps)
  1795 done
  1796 *)
  1797 
  1798 
  1799 subsection{*Division and Signs*}
  1800 
  1801 lemma zero_less_divide_iff:
  1802      "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1803 by (simp add: divide_inverse zero_less_mult_iff)
  1804 
  1805 lemma divide_less_0_iff:
  1806      "(a/b < (0::'a::{linordered_field,division_by_zero})) = 
  1807       (0 < a & b < 0 | a < 0 & 0 < b)"
  1808 by (simp add: divide_inverse mult_less_0_iff)
  1809 
  1810 lemma zero_le_divide_iff:
  1811      "((0::'a::{linordered_field,division_by_zero}) \<le> a/b) =
  1812       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1813 by (simp add: divide_inverse zero_le_mult_iff)
  1814 
  1815 lemma divide_le_0_iff:
  1816      "(a/b \<le> (0::'a::{linordered_field,division_by_zero})) =
  1817       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1818 by (simp add: divide_inverse mult_le_0_iff)
  1819 
  1820 lemma divide_eq_0_iff [simp,noatp]:
  1821      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1822 by (simp add: divide_inverse)
  1823 
  1824 lemma divide_pos_pos:
  1825   "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y"
  1826 by(simp add:field_simps)
  1827 
  1828 
  1829 lemma divide_nonneg_pos:
  1830   "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y"
  1831 by(simp add:field_simps)
  1832 
  1833 lemma divide_neg_pos:
  1834   "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1835 by(simp add:field_simps)
  1836 
  1837 lemma divide_nonpos_pos:
  1838   "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1839 by(simp add:field_simps)
  1840 
  1841 lemma divide_pos_neg:
  1842   "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0"
  1843 by(simp add:field_simps)
  1844 
  1845 lemma divide_nonneg_neg:
  1846   "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" 
  1847 by(simp add:field_simps)
  1848 
  1849 lemma divide_neg_neg:
  1850   "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1851 by(simp add:field_simps)
  1852 
  1853 lemma divide_nonpos_neg:
  1854   "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1855 by(simp add:field_simps)
  1856 
  1857 
  1858 subsection{*Cancellation Laws for Division*}
  1859 
  1860 lemma divide_cancel_right [simp,noatp]:
  1861      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1862 apply (cases "c=0", simp)
  1863 apply (simp add: divide_inverse)
  1864 done
  1865 
  1866 lemma divide_cancel_left [simp,noatp]:
  1867      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1868 apply (cases "c=0", simp)
  1869 apply (simp add: divide_inverse)
  1870 done
  1871 
  1872 
  1873 subsection {* Division and the Number One *}
  1874 
  1875 text{*Simplify expressions equated with 1*}
  1876 lemma divide_eq_1_iff [simp,noatp]:
  1877      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1878 apply (cases "b=0", simp)
  1879 apply (simp add: right_inverse_eq)
  1880 done
  1881 
  1882 lemma one_eq_divide_iff [simp,noatp]:
  1883      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1884 by (simp add: eq_commute [of 1])
  1885 
  1886 lemma zero_eq_1_divide_iff [simp,noatp]:
  1887      "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1888 apply (cases "a=0", simp)
  1889 apply (auto simp add: nonzero_eq_divide_eq)
  1890 done
  1891 
  1892 lemma one_divide_eq_0_iff [simp,noatp]:
  1893      "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"
  1894 apply (cases "a=0", simp)
  1895 apply (insert zero_neq_one [THEN not_sym])
  1896 apply (auto simp add: nonzero_divide_eq_eq)
  1897 done
  1898 
  1899 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1900 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1901 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1902 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1903 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1904 
  1905 declare zero_less_divide_1_iff [simp,noatp]
  1906 declare divide_less_0_1_iff [simp,noatp]
  1907 declare zero_le_divide_1_iff [simp,noatp]
  1908 declare divide_le_0_1_iff [simp,noatp]
  1909 
  1910 
  1911 subsection {* Ordering Rules for Division *}
  1912 
  1913 lemma divide_strict_right_mono:
  1914      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)"
  1915 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1916               positive_imp_inverse_positive)
  1917 
  1918 lemma divide_right_mono:
  1919      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_by_zero})"
  1920 by (force simp add: divide_strict_right_mono order_le_less)
  1921 
  1922 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b 
  1923     ==> c <= 0 ==> b / c <= a / c"
  1924 apply (drule divide_right_mono [of _ _ "- c"])
  1925 apply auto
  1926 done
  1927 
  1928 lemma divide_strict_right_mono_neg:
  1929      "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)"
  1930 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1931 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1932 done
  1933 
  1934 text{*The last premise ensures that @{term a} and @{term b} 
  1935       have the same sign*}
  1936 lemma divide_strict_left_mono:
  1937   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
  1938 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1939 
  1940 lemma divide_left_mono:
  1941   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::linordered_field)"
  1942 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1943 
  1944 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b 
  1945     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1946   apply (drule divide_left_mono [of _ _ "- c"])
  1947   apply (auto simp add: mult_commute)
  1948 done
  1949 
  1950 lemma divide_strict_left_mono_neg:
  1951   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
  1952 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1953 
  1954 
  1955 text{*Simplify quotients that are compared with the value 1.*}
  1956 
  1957 lemma le_divide_eq_1 [noatp]:
  1958   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1959   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1960 by (auto simp add: le_divide_eq)
  1961 
  1962 lemma divide_le_eq_1 [noatp]:
  1963   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1964   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1965 by (auto simp add: divide_le_eq)
  1966 
  1967 lemma less_divide_eq_1 [noatp]:
  1968   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1969   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1970 by (auto simp add: less_divide_eq)
  1971 
  1972 lemma divide_less_eq_1 [noatp]:
  1973   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1974   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1975 by (auto simp add: divide_less_eq)
  1976 
  1977 
  1978 subsection{*Conditional Simplification Rules: No Case Splits*}
  1979 
  1980 lemma le_divide_eq_1_pos [simp,noatp]:
  1981   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1982   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1983 by (auto simp add: le_divide_eq)
  1984 
  1985 lemma le_divide_eq_1_neg [simp,noatp]:
  1986   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1987   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1988 by (auto simp add: le_divide_eq)
  1989 
  1990 lemma divide_le_eq_1_pos [simp,noatp]:
  1991   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1992   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1993 by (auto simp add: divide_le_eq)
  1994 
  1995 lemma divide_le_eq_1_neg [simp,noatp]:
  1996   fixes a :: "'a :: {linordered_field,division_by_zero}"
  1997   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1998 by (auto simp add: divide_le_eq)
  1999 
  2000 lemma less_divide_eq_1_pos [simp,noatp]:
  2001   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2002   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  2003 by (auto simp add: less_divide_eq)
  2004 
  2005 lemma less_divide_eq_1_neg [simp,noatp]:
  2006   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2007   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  2008 by (auto simp add: less_divide_eq)
  2009 
  2010 lemma divide_less_eq_1_pos [simp,noatp]:
  2011   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2012   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  2013 by (auto simp add: divide_less_eq)
  2014 
  2015 lemma divide_less_eq_1_neg [simp,noatp]:
  2016   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2017   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  2018 by (auto simp add: divide_less_eq)
  2019 
  2020 lemma eq_divide_eq_1 [simp,noatp]:
  2021   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2022   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  2023 by (auto simp add: eq_divide_eq)
  2024 
  2025 lemma divide_eq_eq_1 [simp,noatp]:
  2026   fixes a :: "'a :: {linordered_field,division_by_zero}"
  2027   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  2028 by (auto simp add: divide_eq_eq)
  2029 
  2030 
  2031 subsection {* Reasoning about inequalities with division *}
  2032 
  2033 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  2034     ==> x * y <= x"
  2035 by (auto simp add: mult_compare_simps)
  2036 
  2037 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  2038     ==> y * x <= x"
  2039 by (auto simp add: mult_compare_simps)
  2040 
  2041 lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==>
  2042     x / y <= z"
  2043 by (subst pos_divide_le_eq, assumption+)
  2044 
  2045 lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==>
  2046     z <= x / y"
  2047 by(simp add:field_simps)
  2048 
  2049 lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==>
  2050     x / y < z"
  2051 by(simp add:field_simps)
  2052 
  2053 lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==>
  2054     z < x / y"
  2055 by(simp add:field_simps)
  2056 
  2057 lemma frac_le: "(0::'a::linordered_field) <= x ==> 
  2058     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2059   apply (rule mult_imp_div_pos_le)
  2060   apply simp
  2061   apply (subst times_divide_eq_left)
  2062   apply (rule mult_imp_le_div_pos, assumption)
  2063   apply (rule mult_mono)
  2064   apply simp_all
  2065 done
  2066 
  2067 lemma frac_less: "(0::'a::linordered_field) <= x ==> 
  2068     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  2069   apply (rule mult_imp_div_pos_less)
  2070   apply simp
  2071   apply (subst times_divide_eq_left)
  2072   apply (rule mult_imp_less_div_pos, assumption)
  2073   apply (erule mult_less_le_imp_less)
  2074   apply simp_all
  2075 done
  2076 
  2077 lemma frac_less2: "(0::'a::linordered_field) < x ==> 
  2078     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2079   apply (rule mult_imp_div_pos_less)
  2080   apply simp_all
  2081   apply (subst times_divide_eq_left)
  2082   apply (rule mult_imp_less_div_pos, assumption)
  2083   apply (erule mult_le_less_imp_less)
  2084   apply simp_all
  2085 done
  2086 
  2087 text{*It's not obvious whether these should be simprules or not. 
  2088   Their effect is to gather terms into one big fraction, like
  2089   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2090   seem to need them.*}
  2091 
  2092 declare times_divide_eq [simp]
  2093 
  2094 
  2095 subsection {* Ordered Fields are Dense *}
  2096 
  2097 context linordered_semidom
  2098 begin
  2099 
  2100 lemma less_add_one: "a < a + 1"
  2101 proof -
  2102   have "a + 0 < a + 1"
  2103     by (blast intro: zero_less_one add_strict_left_mono)
  2104   thus ?thesis by simp
  2105 qed
  2106 
  2107 lemma zero_less_two: "0 < 1 + 1"
  2108 by (blast intro: less_trans zero_less_one less_add_one)
  2109 
  2110 end
  2111 
  2112 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)"
  2113 by (simp add: field_simps zero_less_two)
  2114 
  2115 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b"
  2116 by (simp add: field_simps zero_less_two)
  2117 
  2118 instance linordered_field < dense_linorder
  2119 proof
  2120   fix x y :: 'a
  2121   have "x < x + 1" by simp
  2122   then show "\<exists>y. x < y" .. 
  2123   have "x - 1 < x" by simp
  2124   then show "\<exists>y. y < x" ..
  2125   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2126 qed
  2127 
  2128 
  2129 subsection {* Absolute Value *}
  2130 
  2131 context linordered_idom
  2132 begin
  2133 
  2134 lemma mult_sgn_abs: "sgn x * abs x = x"
  2135   unfolding abs_if sgn_if by auto
  2136 
  2137 end
  2138 
  2139 lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
  2140 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2141 
  2142 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  2143   assumes abs_eq_mult:
  2144     "(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>"
  2145 
  2146 context linordered_idom
  2147 begin
  2148 
  2149 subclass ordered_ring_abs proof
  2150 qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
  2151 
  2152 lemma abs_mult:
  2153   "abs (a * b) = abs a * abs b" 
  2154   by (rule abs_eq_mult) auto
  2155 
  2156 lemma abs_mult_self:
  2157   "abs a * abs a = a * a"
  2158   by (simp add: abs_if) 
  2159 
  2160 end
  2161 
  2162 lemma nonzero_abs_inverse:
  2163      "a \<noteq> 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)"
  2164 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2165                       negative_imp_inverse_negative)
  2166 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2167 done
  2168 
  2169 lemma abs_inverse [simp]:
  2170      "abs (inverse (a::'a::{linordered_field,division_by_zero})) = 
  2171       inverse (abs a)"
  2172 apply (cases "a=0", simp) 
  2173 apply (simp add: nonzero_abs_inverse) 
  2174 done
  2175 
  2176 lemma nonzero_abs_divide:
  2177      "b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b"
  2178 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2179 
  2180 lemma abs_divide [simp]:
  2181      "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b"
  2182 apply (cases "b=0", simp) 
  2183 apply (simp add: nonzero_abs_divide) 
  2184 done
  2185 
  2186 lemma abs_mult_less:
  2187      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
  2188 proof -
  2189   assume ac: "abs a < c"
  2190   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2191   assume "abs b < d"
  2192   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2193 qed
  2194 
  2195 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  2196 
  2197 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
  2198   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2199 
  2200 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
  2201 apply (simp add: order_less_le abs_le_iff)  
  2202 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2203 done
  2204 
  2205 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
  2206     (abs y) * x = abs (y * x)"
  2207   apply (subst abs_mult)
  2208   apply simp
  2209 done
  2210 
  2211 lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> 
  2212     abs x / y = abs (x / y)"
  2213   apply (subst abs_divide)
  2214   apply (simp add: order_less_imp_le)
  2215 done
  2216 
  2217 code_modulename SML
  2218   Ring_and_Field Arith
  2219 
  2220 code_modulename OCaml
  2221   Ring_and_Field Arith
  2222 
  2223 code_modulename Haskell
  2224   Ring_and_Field Arith
  2225 
  2226 end