src/HOL/Ring_and_Field.thy
author haftmann
Thu Oct 29 11:41:37 2009 +0100 (2009-10-29)
changeset 33319 74f0dcc0b5fb
parent 32960 69916a850301
child 33364 2bd12592c5e8
permissions -rw-r--r--
moved algebraic classes to Ring_and_Field
     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 end
  1305 
  1306 class ordered_field = field + ordered_idom
  1307 
  1308 text {* Simprules for comparisons where common factors can be cancelled. *}
  1309 
  1310 lemmas mult_compare_simps[noatp] =
  1311     mult_le_cancel_right mult_le_cancel_left
  1312     mult_le_cancel_right1 mult_le_cancel_right2
  1313     mult_le_cancel_left1 mult_le_cancel_left2
  1314     mult_less_cancel_right mult_less_cancel_left
  1315     mult_less_cancel_right1 mult_less_cancel_right2
  1316     mult_less_cancel_left1 mult_less_cancel_left2
  1317     mult_cancel_right mult_cancel_left
  1318     mult_cancel_right1 mult_cancel_right2
  1319     mult_cancel_left1 mult_cancel_left2
  1320 
  1321 -- {* FIXME continue localization here *}
  1322 
  1323 lemma inverse_nonzero_iff_nonzero [simp]:
  1324    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
  1325 by (force dest: inverse_zero_imp_zero) 
  1326 
  1327 lemma inverse_minus_eq [simp]:
  1328    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
  1329 proof cases
  1330   assume "a=0" thus ?thesis by (simp add: inverse_zero)
  1331 next
  1332   assume "a\<noteq>0" 
  1333   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  1334 qed
  1335 
  1336 lemma inverse_eq_imp_eq:
  1337   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
  1338 apply (cases "a=0 | b=0") 
  1339  apply (force dest!: inverse_zero_imp_zero
  1340               simp add: eq_commute [of "0::'a"])
  1341 apply (force dest!: nonzero_inverse_eq_imp_eq) 
  1342 done
  1343 
  1344 lemma inverse_eq_iff_eq [simp]:
  1345   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
  1346 by (force dest!: inverse_eq_imp_eq)
  1347 
  1348 lemma inverse_inverse_eq [simp]:
  1349      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
  1350   proof cases
  1351     assume "a=0" thus ?thesis by simp
  1352   next
  1353     assume "a\<noteq>0" 
  1354     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  1355   qed
  1356 
  1357 text{*This version builds in division by zero while also re-orienting
  1358       the right-hand side.*}
  1359 lemma inverse_mult_distrib [simp]:
  1360      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
  1361   proof cases
  1362     assume "a \<noteq> 0 & b \<noteq> 0" 
  1363     thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
  1364   next
  1365     assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
  1366     thus ?thesis by force
  1367   qed
  1368 
  1369 lemma inverse_divide [simp]:
  1370   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  1371 by (simp add: divide_inverse mult_commute)
  1372 
  1373 
  1374 subsection {* Calculations with fractions *}
  1375 
  1376 text{* There is a whole bunch of simp-rules just for class @{text
  1377 field} but none for class @{text field} and @{text nonzero_divides}
  1378 because the latter are covered by a simproc. *}
  1379 
  1380 lemma mult_divide_mult_cancel_left:
  1381   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
  1382 apply (cases "b = 0")
  1383 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
  1384 done
  1385 
  1386 lemma mult_divide_mult_cancel_right:
  1387   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
  1388 apply (cases "b = 0")
  1389 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
  1390 done
  1391 
  1392 lemma divide_divide_eq_right [simp,noatp]:
  1393   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
  1394 by (simp add: divide_inverse mult_ac)
  1395 
  1396 lemma divide_divide_eq_left [simp,noatp]:
  1397   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  1398 by (simp add: divide_inverse mult_assoc)
  1399 
  1400 
  1401 subsubsection{*Special Cancellation Simprules for Division*}
  1402 
  1403 lemma mult_divide_mult_cancel_left_if[simp,noatp]:
  1404 fixes c :: "'a :: {field,division_by_zero}"
  1405 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
  1406 by (simp add: mult_divide_mult_cancel_left)
  1407 
  1408 
  1409 subsection {* Division and Unary Minus *}
  1410 
  1411 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1412 by (simp add: divide_inverse)
  1413 
  1414 lemma divide_minus_right [simp, noatp]:
  1415   "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
  1416 by (simp add: divide_inverse)
  1417 
  1418 lemma minus_divide_divide:
  1419   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1420 apply (cases "b=0", simp) 
  1421 apply (simp add: nonzero_minus_divide_divide) 
  1422 done
  1423 
  1424 lemma eq_divide_eq:
  1425   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1426 by (simp add: nonzero_eq_divide_eq)
  1427 
  1428 lemma divide_eq_eq:
  1429   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1430 by (force simp add: nonzero_divide_eq_eq)
  1431 
  1432 
  1433 subsection {* Ordered Fields *}
  1434 
  1435 lemma positive_imp_inverse_positive: 
  1436 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
  1437 proof -
  1438   have "0 < a * inverse a" 
  1439     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1440   thus "0 < inverse a" 
  1441     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1442 qed
  1443 
  1444 lemma negative_imp_inverse_negative:
  1445   "a < 0 ==> inverse a < (0::'a::ordered_field)"
  1446 by (insert positive_imp_inverse_positive [of "-a"], 
  1447     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1448 
  1449 lemma inverse_le_imp_le:
  1450 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1451 shows "b \<le> (a::'a::ordered_field)"
  1452 proof (rule classical)
  1453   assume "~ b \<le> a"
  1454   hence "a < b"  by (simp add: linorder_not_le)
  1455   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1456   hence "a * inverse a \<le> a * inverse b"
  1457     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1458   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1459     by (simp add: bpos order_less_imp_le mult_right_mono)
  1460   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1461 qed
  1462 
  1463 lemma inverse_positive_imp_positive:
  1464 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1465 shows "0 < (a::'a::ordered_field)"
  1466 proof -
  1467   have "0 < inverse (inverse a)"
  1468     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1469   thus "0 < a"
  1470     using nz by (simp add: nonzero_inverse_inverse_eq)
  1471 qed
  1472 
  1473 lemma inverse_positive_iff_positive [simp]:
  1474   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1475 apply (cases "a = 0", simp)
  1476 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1477 done
  1478 
  1479 lemma inverse_negative_imp_negative:
  1480 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1481 shows "a < (0::'a::ordered_field)"
  1482 proof -
  1483   have "inverse (inverse a) < 0"
  1484     using inv_less_0 by (rule negative_imp_inverse_negative)
  1485   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1486 qed
  1487 
  1488 lemma inverse_negative_iff_negative [simp]:
  1489   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1490 apply (cases "a = 0", simp)
  1491 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1492 done
  1493 
  1494 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1495   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1496 by (simp add: linorder_not_less [symmetric])
  1497 
  1498 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1499   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1500 by (simp add: linorder_not_less [symmetric])
  1501 
  1502 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
  1503 proof
  1504   fix x::'a
  1505   have m1: "- (1::'a) < 0" by simp
  1506   from add_strict_right_mono[OF m1, where c=x] 
  1507   have "(- 1) + x < x" by simp
  1508   thus "\<exists>y. y < x" by blast
  1509 qed
  1510 
  1511 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
  1512 proof
  1513   fix x::'a
  1514   have m1: " (1::'a) > 0" by simp
  1515   from add_strict_right_mono[OF m1, where c=x] 
  1516   have "1 + x > x" by simp
  1517   thus "\<exists>y. y > x" by blast
  1518 qed
  1519 
  1520 subsection{*Anti-Monotonicity of @{term inverse}*}
  1521 
  1522 lemma less_imp_inverse_less:
  1523 assumes less: "a < b" and apos:  "0 < a"
  1524 shows "inverse b < inverse (a::'a::ordered_field)"
  1525 proof (rule ccontr)
  1526   assume "~ inverse b < inverse a"
  1527   hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
  1528   hence "~ (a < b)"
  1529     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1530   thus False by (rule notE [OF _ less])
  1531 qed
  1532 
  1533 lemma inverse_less_imp_less:
  1534   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1535 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1536 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1537 done
  1538 
  1539 text{*Both premises are essential. Consider -1 and 1.*}
  1540 lemma inverse_less_iff_less [simp,noatp]:
  1541   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1542 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1543 
  1544 lemma le_imp_inverse_le:
  1545   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1546 by (force simp add: order_le_less less_imp_inverse_less)
  1547 
  1548 lemma inverse_le_iff_le [simp,noatp]:
  1549  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1550 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1551 
  1552 
  1553 text{*These results refer to both operands being negative.  The opposite-sign
  1554 case is trivial, since inverse preserves signs.*}
  1555 lemma inverse_le_imp_le_neg:
  1556   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1557 apply (rule classical) 
  1558 apply (subgoal_tac "a < 0") 
  1559  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1560 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1561 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1562 done
  1563 
  1564 lemma less_imp_inverse_less_neg:
  1565    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1566 apply (subgoal_tac "a < 0") 
  1567  prefer 2 apply (blast intro: order_less_trans) 
  1568 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1569 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1570 done
  1571 
  1572 lemma inverse_less_imp_less_neg:
  1573    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1574 apply (rule classical) 
  1575 apply (subgoal_tac "a < 0") 
  1576  prefer 2
  1577  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1578 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1579 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1580 done
  1581 
  1582 lemma inverse_less_iff_less_neg [simp,noatp]:
  1583   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1584 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1585 apply (simp del: inverse_less_iff_less 
  1586             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1587 done
  1588 
  1589 lemma le_imp_inverse_le_neg:
  1590   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1591 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1592 
  1593 lemma inverse_le_iff_le_neg [simp,noatp]:
  1594  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1595 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1596 
  1597 
  1598 subsection{*Inverses and the Number One*}
  1599 
  1600 lemma one_less_inverse_iff:
  1601   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
  1602 proof cases
  1603   assume "0 < x"
  1604     with inverse_less_iff_less [OF zero_less_one, of x]
  1605     show ?thesis by simp
  1606 next
  1607   assume notless: "~ (0 < x)"
  1608   have "~ (1 < inverse x)"
  1609   proof
  1610     assume "1 < inverse x"
  1611     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1612     also have "... < 1" by (rule zero_less_one) 
  1613     finally show False by auto
  1614   qed
  1615   with notless show ?thesis by simp
  1616 qed
  1617 
  1618 lemma inverse_eq_1_iff [simp]:
  1619   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1620 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1621 
  1622 lemma one_le_inverse_iff:
  1623   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
  1624 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1625                     eq_commute [of 1]) 
  1626 
  1627 lemma inverse_less_1_iff:
  1628   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
  1629 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1630 
  1631 lemma inverse_le_1_iff:
  1632   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  1633 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1634 
  1635 
  1636 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1637 
  1638 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1639 proof -
  1640   assume less: "0<c"
  1641   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1642     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1643   also have "... = (a*c \<le> b)"
  1644     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1645   finally show ?thesis .
  1646 qed
  1647 
  1648 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1649 proof -
  1650   assume less: "c<0"
  1651   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1652     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1653   also have "... = (b \<le> a*c)"
  1654     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1655   finally show ?thesis .
  1656 qed
  1657 
  1658 lemma le_divide_eq:
  1659   "(a \<le> b/c) = 
  1660    (if 0 < c then a*c \<le> b
  1661              else if c < 0 then b \<le> a*c
  1662              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1663 apply (cases "c=0", simp) 
  1664 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1665 done
  1666 
  1667 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1668 proof -
  1669   assume less: "0<c"
  1670   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1671     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1672   also have "... = (b \<le> a*c)"
  1673     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1674   finally show ?thesis .
  1675 qed
  1676 
  1677 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1678 proof -
  1679   assume less: "c<0"
  1680   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1681     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1682   also have "... = (a*c \<le> b)"
  1683     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1684   finally show ?thesis .
  1685 qed
  1686 
  1687 lemma divide_le_eq:
  1688   "(b/c \<le> a) = 
  1689    (if 0 < c then b \<le> a*c
  1690              else if c < 0 then a*c \<le> b
  1691              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1692 apply (cases "c=0", simp) 
  1693 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1694 done
  1695 
  1696 lemma pos_less_divide_eq:
  1697      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1698 proof -
  1699   assume less: "0<c"
  1700   hence "(a < b/c) = (a*c < (b/c)*c)"
  1701     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1702   also have "... = (a*c < b)"
  1703     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1704   finally show ?thesis .
  1705 qed
  1706 
  1707 lemma neg_less_divide_eq:
  1708  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1709 proof -
  1710   assume less: "c<0"
  1711   hence "(a < b/c) = ((b/c)*c < a*c)"
  1712     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1713   also have "... = (b < a*c)"
  1714     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1715   finally show ?thesis .
  1716 qed
  1717 
  1718 lemma less_divide_eq:
  1719   "(a < b/c) = 
  1720    (if 0 < c then a*c < b
  1721              else if c < 0 then b < a*c
  1722              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1723 apply (cases "c=0", simp) 
  1724 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1725 done
  1726 
  1727 lemma pos_divide_less_eq:
  1728      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1729 proof -
  1730   assume less: "0<c"
  1731   hence "(b/c < a) = ((b/c)*c < a*c)"
  1732     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1733   also have "... = (b < a*c)"
  1734     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1735   finally show ?thesis .
  1736 qed
  1737 
  1738 lemma neg_divide_less_eq:
  1739  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1740 proof -
  1741   assume less: "c<0"
  1742   hence "(b/c < a) = (a*c < (b/c)*c)"
  1743     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1744   also have "... = (a*c < b)"
  1745     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1746   finally show ?thesis .
  1747 qed
  1748 
  1749 lemma divide_less_eq:
  1750   "(b/c < a) = 
  1751    (if 0 < c then b < a*c
  1752              else if c < 0 then a*c < b
  1753              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1754 apply (cases "c=0", simp) 
  1755 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1756 done
  1757 
  1758 
  1759 subsection{*Field simplification*}
  1760 
  1761 text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
  1762 if they can be proved to be non-zero (for equations) or positive/negative
  1763 (for inequations). Can be too aggressive and is therefore separate from the
  1764 more benign @{text algebra_simps}. *}
  1765 
  1766 lemmas field_simps[noatp] = field_eq_simps
  1767   (* multiply ineqn *)
  1768   pos_divide_less_eq neg_divide_less_eq
  1769   pos_less_divide_eq neg_less_divide_eq
  1770   pos_divide_le_eq neg_divide_le_eq
  1771   pos_le_divide_eq neg_le_divide_eq
  1772 
  1773 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1774 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1775 sign_simps} to @{text field_simps} because the former can lead to case
  1776 explosions. *}
  1777 
  1778 lemmas sign_simps[noatp] = group_simps
  1779   zero_less_mult_iff  mult_less_0_iff
  1780 
  1781 (* Only works once linear arithmetic is installed:
  1782 text{*An example:*}
  1783 lemma fixes a b c d e f :: "'a::ordered_field"
  1784 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1785  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1786  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1787 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1788  prefer 2 apply(simp add:sign_simps)
  1789 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1790  prefer 2 apply(simp add:sign_simps)
  1791 apply(simp add:field_simps)
  1792 done
  1793 *)
  1794 
  1795 
  1796 subsection{*Division and Signs*}
  1797 
  1798 lemma zero_less_divide_iff:
  1799      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1800 by (simp add: divide_inverse zero_less_mult_iff)
  1801 
  1802 lemma divide_less_0_iff:
  1803      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1804       (0 < a & b < 0 | a < 0 & 0 < b)"
  1805 by (simp add: divide_inverse mult_less_0_iff)
  1806 
  1807 lemma zero_le_divide_iff:
  1808      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1809       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1810 by (simp add: divide_inverse zero_le_mult_iff)
  1811 
  1812 lemma divide_le_0_iff:
  1813      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1814       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1815 by (simp add: divide_inverse mult_le_0_iff)
  1816 
  1817 lemma divide_eq_0_iff [simp,noatp]:
  1818      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1819 by (simp add: divide_inverse)
  1820 
  1821 lemma divide_pos_pos:
  1822   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
  1823 by(simp add:field_simps)
  1824 
  1825 
  1826 lemma divide_nonneg_pos:
  1827   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
  1828 by(simp add:field_simps)
  1829 
  1830 lemma divide_neg_pos:
  1831   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1832 by(simp add:field_simps)
  1833 
  1834 lemma divide_nonpos_pos:
  1835   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1836 by(simp add:field_simps)
  1837 
  1838 lemma divide_pos_neg:
  1839   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  1840 by(simp add:field_simps)
  1841 
  1842 lemma divide_nonneg_neg:
  1843   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
  1844 by(simp add:field_simps)
  1845 
  1846 lemma divide_neg_neg:
  1847   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1848 by(simp add:field_simps)
  1849 
  1850 lemma divide_nonpos_neg:
  1851   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1852 by(simp add:field_simps)
  1853 
  1854 
  1855 subsection{*Cancellation Laws for Division*}
  1856 
  1857 lemma divide_cancel_right [simp,noatp]:
  1858      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1859 apply (cases "c=0", simp)
  1860 apply (simp add: divide_inverse)
  1861 done
  1862 
  1863 lemma divide_cancel_left [simp,noatp]:
  1864      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1865 apply (cases "c=0", simp)
  1866 apply (simp add: divide_inverse)
  1867 done
  1868 
  1869 
  1870 subsection {* Division and the Number One *}
  1871 
  1872 text{*Simplify expressions equated with 1*}
  1873 lemma divide_eq_1_iff [simp,noatp]:
  1874      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1875 apply (cases "b=0", simp)
  1876 apply (simp add: right_inverse_eq)
  1877 done
  1878 
  1879 lemma one_eq_divide_iff [simp,noatp]:
  1880      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1881 by (simp add: eq_commute [of 1])
  1882 
  1883 lemma zero_eq_1_divide_iff [simp,noatp]:
  1884      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1885 apply (cases "a=0", simp)
  1886 apply (auto simp add: nonzero_eq_divide_eq)
  1887 done
  1888 
  1889 lemma one_divide_eq_0_iff [simp,noatp]:
  1890      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  1891 apply (cases "a=0", simp)
  1892 apply (insert zero_neq_one [THEN not_sym])
  1893 apply (auto simp add: nonzero_divide_eq_eq)
  1894 done
  1895 
  1896 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1897 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1898 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1899 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1900 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1901 
  1902 declare zero_less_divide_1_iff [simp,noatp]
  1903 declare divide_less_0_1_iff [simp,noatp]
  1904 declare zero_le_divide_1_iff [simp,noatp]
  1905 declare divide_le_0_1_iff [simp,noatp]
  1906 
  1907 
  1908 subsection {* Ordering Rules for Division *}
  1909 
  1910 lemma divide_strict_right_mono:
  1911      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1912 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1913               positive_imp_inverse_positive)
  1914 
  1915 lemma divide_right_mono:
  1916      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1917 by (force simp add: divide_strict_right_mono order_le_less)
  1918 
  1919 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1920     ==> c <= 0 ==> b / c <= a / c"
  1921 apply (drule divide_right_mono [of _ _ "- c"])
  1922 apply auto
  1923 done
  1924 
  1925 lemma divide_strict_right_mono_neg:
  1926      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1927 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1928 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1929 done
  1930 
  1931 text{*The last premise ensures that @{term a} and @{term b} 
  1932       have the same sign*}
  1933 lemma divide_strict_left_mono:
  1934   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1935 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1936 
  1937 lemma divide_left_mono:
  1938   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1939 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1940 
  1941 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1942     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1943   apply (drule divide_left_mono [of _ _ "- c"])
  1944   apply (auto simp add: mult_commute)
  1945 done
  1946 
  1947 lemma divide_strict_left_mono_neg:
  1948   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1949 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1950 
  1951 
  1952 text{*Simplify quotients that are compared with the value 1.*}
  1953 
  1954 lemma le_divide_eq_1 [noatp]:
  1955   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1956   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1957 by (auto simp add: le_divide_eq)
  1958 
  1959 lemma divide_le_eq_1 [noatp]:
  1960   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1961   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1962 by (auto simp add: divide_le_eq)
  1963 
  1964 lemma less_divide_eq_1 [noatp]:
  1965   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1966   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1967 by (auto simp add: less_divide_eq)
  1968 
  1969 lemma divide_less_eq_1 [noatp]:
  1970   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1971   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1972 by (auto simp add: divide_less_eq)
  1973 
  1974 
  1975 subsection{*Conditional Simplification Rules: No Case Splits*}
  1976 
  1977 lemma le_divide_eq_1_pos [simp,noatp]:
  1978   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1979   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1980 by (auto simp add: le_divide_eq)
  1981 
  1982 lemma le_divide_eq_1_neg [simp,noatp]:
  1983   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1984   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1985 by (auto simp add: le_divide_eq)
  1986 
  1987 lemma divide_le_eq_1_pos [simp,noatp]:
  1988   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1989   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1990 by (auto simp add: divide_le_eq)
  1991 
  1992 lemma divide_le_eq_1_neg [simp,noatp]:
  1993   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1994   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1995 by (auto simp add: divide_le_eq)
  1996 
  1997 lemma less_divide_eq_1_pos [simp,noatp]:
  1998   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1999   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  2000 by (auto simp add: less_divide_eq)
  2001 
  2002 lemma less_divide_eq_1_neg [simp,noatp]:
  2003   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2004   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  2005 by (auto simp add: less_divide_eq)
  2006 
  2007 lemma divide_less_eq_1_pos [simp,noatp]:
  2008   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2009   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  2010 by (auto simp add: divide_less_eq)
  2011 
  2012 lemma divide_less_eq_1_neg [simp,noatp]:
  2013   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2014   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  2015 by (auto simp add: divide_less_eq)
  2016 
  2017 lemma eq_divide_eq_1 [simp,noatp]:
  2018   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2019   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  2020 by (auto simp add: eq_divide_eq)
  2021 
  2022 lemma divide_eq_eq_1 [simp,noatp]:
  2023   fixes a :: "'a :: {ordered_field,division_by_zero}"
  2024   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  2025 by (auto simp add: divide_eq_eq)
  2026 
  2027 
  2028 subsection {* Reasoning about inequalities with division *}
  2029 
  2030 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2031     ==> x * y <= x"
  2032 by (auto simp add: mult_compare_simps)
  2033 
  2034 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  2035     ==> y * x <= x"
  2036 by (auto simp add: mult_compare_simps)
  2037 
  2038 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  2039     x / y <= z"
  2040 by (subst pos_divide_le_eq, assumption+)
  2041 
  2042 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  2043     z <= x / y"
  2044 by(simp add:field_simps)
  2045 
  2046 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  2047     x / y < z"
  2048 by(simp add:field_simps)
  2049 
  2050 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  2051     z < x / y"
  2052 by(simp add:field_simps)
  2053 
  2054 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  2055     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2056   apply (rule mult_imp_div_pos_le)
  2057   apply simp
  2058   apply (subst times_divide_eq_left)
  2059   apply (rule mult_imp_le_div_pos, assumption)
  2060   apply (rule mult_mono)
  2061   apply simp_all
  2062 done
  2063 
  2064 lemma frac_less: "(0::'a::ordered_field) <= x ==> 
  2065     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  2066   apply (rule mult_imp_div_pos_less)
  2067   apply simp
  2068   apply (subst times_divide_eq_left)
  2069   apply (rule mult_imp_less_div_pos, assumption)
  2070   apply (erule mult_less_le_imp_less)
  2071   apply simp_all
  2072 done
  2073 
  2074 lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  2075     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2076   apply (rule mult_imp_div_pos_less)
  2077   apply simp_all
  2078   apply (subst times_divide_eq_left)
  2079   apply (rule mult_imp_less_div_pos, assumption)
  2080   apply (erule mult_le_less_imp_less)
  2081   apply simp_all
  2082 done
  2083 
  2084 text{*It's not obvious whether these should be simprules or not. 
  2085   Their effect is to gather terms into one big fraction, like
  2086   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2087   seem to need them.*}
  2088 
  2089 declare times_divide_eq [simp]
  2090 
  2091 
  2092 subsection {* Ordered Fields are Dense *}
  2093 
  2094 context ordered_semidom
  2095 begin
  2096 
  2097 lemma less_add_one: "a < a + 1"
  2098 proof -
  2099   have "a + 0 < a + 1"
  2100     by (blast intro: zero_less_one add_strict_left_mono)
  2101   thus ?thesis by simp
  2102 qed
  2103 
  2104 lemma zero_less_two: "0 < 1 + 1"
  2105 by (blast intro: less_trans zero_less_one less_add_one)
  2106 
  2107 end
  2108 
  2109 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  2110 by (simp add: field_simps zero_less_two)
  2111 
  2112 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  2113 by (simp add: field_simps zero_less_two)
  2114 
  2115 instance ordered_field < dense_linear_order
  2116 proof
  2117   fix x y :: 'a
  2118   have "x < x + 1" by simp
  2119   then show "\<exists>y. x < y" .. 
  2120   have "x - 1 < x" by simp
  2121   then show "\<exists>y. y < x" ..
  2122   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2123 qed
  2124 
  2125 
  2126 subsection {* Absolute Value *}
  2127 
  2128 context ordered_idom
  2129 begin
  2130 
  2131 lemma mult_sgn_abs: "sgn x * abs x = x"
  2132   unfolding abs_if sgn_if by auto
  2133 
  2134 end
  2135 
  2136 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  2137 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2138 
  2139 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
  2140   assumes abs_eq_mult:
  2141     "(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>"
  2142 
  2143 
  2144 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
  2145 begin
  2146 
  2147 subclass lordered_ab_group_add_meet ..
  2148 subclass lordered_ab_group_add_join ..
  2149 
  2150 end
  2151 
  2152 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  2153 proof -
  2154   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  2155   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2156   have a: "(abs a) * (abs b) = ?x"
  2157     by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
  2158   {
  2159     fix u v :: 'a
  2160     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  2161               u * v = pprt a * pprt b + pprt a * nprt b + 
  2162                       nprt a * pprt b + nprt a * nprt b"
  2163       apply (subst prts[of u], subst prts[of v])
  2164       apply (simp add: algebra_simps) 
  2165       done
  2166   }
  2167   note b = this[OF refl[of a] refl[of b]]
  2168   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
  2169   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
  2170   have xy: "- ?x <= ?y"
  2171     apply (simp)
  2172     apply (rule_tac y="0::'a" in order_trans)
  2173     apply (rule addm2)
  2174     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2175     apply (rule addm)
  2176     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2177     done
  2178   have yx: "?y <= ?x"
  2179     apply (simp add:diff_def)
  2180     apply (rule_tac y=0 in order_trans)
  2181     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2182     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2183     done
  2184   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  2185   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  2186   show ?thesis
  2187     apply (rule abs_leI)
  2188     apply (simp add: i1)
  2189     apply (simp add: i2[simplified minus_le_iff])
  2190     done
  2191 qed
  2192 
  2193 instance lordered_ring \<subseteq> pordered_ring_abs
  2194 proof
  2195   fix a b :: "'a\<Colon> lordered_ring"
  2196   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
  2197   show "abs (a*b) = abs a * abs b"
  2198 proof -
  2199   have s: "(0 <= a*b) | (a*b <= 0)"
  2200     apply (auto)    
  2201     apply (rule_tac split_mult_pos_le)
  2202     apply (rule_tac contrapos_np[of "a*b <= 0"])
  2203     apply (simp)
  2204     apply (rule_tac split_mult_neg_le)
  2205     apply (insert prems)
  2206     apply (blast)
  2207     done
  2208   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
  2209     by (simp add: prts[symmetric])
  2210   show ?thesis
  2211   proof cases
  2212     assume "0 <= a * b"
  2213     then show ?thesis
  2214       apply (simp_all add: mulprts abs_prts)
  2215       apply (insert prems)
  2216       apply (auto simp add: 
  2217         algebra_simps 
  2218         iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
  2219         iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
  2220         apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  2221         apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  2222       done
  2223   next
  2224     assume "~(0 <= a*b)"
  2225     with s have "a*b <= 0" by simp
  2226     then show ?thesis
  2227       apply (simp_all add: mulprts abs_prts)
  2228       apply (insert prems)
  2229       apply (auto simp add: algebra_simps)
  2230       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  2231       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  2232       done
  2233   qed
  2234 qed
  2235 qed
  2236 
  2237 context ordered_idom
  2238 begin
  2239 
  2240 subclass pordered_ring_abs proof
  2241 qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
  2242 
  2243 lemma abs_mult:
  2244   "abs (a * b) = abs a * abs b" 
  2245   by (rule abs_eq_mult) auto
  2246 
  2247 lemma abs_mult_self:
  2248   "abs a * abs a = a * a"
  2249   by (simp add: abs_if) 
  2250 
  2251 end
  2252 
  2253 lemma nonzero_abs_inverse:
  2254      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  2255 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2256                       negative_imp_inverse_negative)
  2257 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2258 done
  2259 
  2260 lemma abs_inverse [simp]:
  2261      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  2262       inverse (abs a)"
  2263 apply (cases "a=0", simp) 
  2264 apply (simp add: nonzero_abs_inverse) 
  2265 done
  2266 
  2267 lemma nonzero_abs_divide:
  2268      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  2269 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2270 
  2271 lemma abs_divide [simp]:
  2272      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  2273 apply (cases "b=0", simp) 
  2274 apply (simp add: nonzero_abs_divide) 
  2275 done
  2276 
  2277 lemma abs_mult_less:
  2278      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
  2279 proof -
  2280   assume ac: "abs a < c"
  2281   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2282   assume "abs b < d"
  2283   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2284 qed
  2285 
  2286 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  2287 
  2288 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
  2289   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2290 
  2291 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
  2292 apply (simp add: order_less_le abs_le_iff)  
  2293 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2294 done
  2295 
  2296 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  2297     (abs y) * x = abs (y * x)"
  2298   apply (subst abs_mult)
  2299   apply simp
  2300 done
  2301 
  2302 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  2303     abs x / y = abs (x / y)"
  2304   apply (subst abs_divide)
  2305   apply (simp add: order_less_imp_le)
  2306 done
  2307 
  2308 
  2309 subsection {* Bounds of products via negative and positive Part *}
  2310 
  2311 lemma mult_le_prts:
  2312   assumes
  2313   "a1 <= (a::'a::lordered_ring)"
  2314   "a <= a2"
  2315   "b1 <= b"
  2316   "b <= b2"
  2317   shows
  2318   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  2319 proof - 
  2320   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  2321     apply (subst prts[symmetric])+
  2322     apply simp
  2323     done
  2324   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2325     by (simp add: algebra_simps)
  2326   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  2327     by (simp_all add: prems mult_mono)
  2328   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  2329   proof -
  2330     have "pprt a * nprt b <= pprt a * nprt b2"
  2331       by (simp add: mult_left_mono prems)
  2332     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  2333       by (simp add: mult_right_mono_neg prems)
  2334     ultimately show ?thesis
  2335       by simp
  2336   qed
  2337   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  2338   proof - 
  2339     have "nprt a * pprt b <= nprt a2 * pprt b"
  2340       by (simp add: mult_right_mono prems)
  2341     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  2342       by (simp add: mult_left_mono_neg prems)
  2343     ultimately show ?thesis
  2344       by simp
  2345   qed
  2346   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  2347   proof -
  2348     have "nprt a * nprt b <= nprt a * nprt b1"
  2349       by (simp add: mult_left_mono_neg prems)
  2350     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  2351       by (simp add: mult_right_mono_neg prems)
  2352     ultimately show ?thesis
  2353       by simp
  2354   qed
  2355   ultimately show ?thesis
  2356     by - (rule add_mono | simp)+
  2357 qed
  2358 
  2359 lemma mult_ge_prts:
  2360   assumes
  2361   "a1 <= (a::'a::lordered_ring)"
  2362   "a <= a2"
  2363   "b1 <= b"
  2364   "b <= b2"
  2365   shows
  2366   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  2367 proof - 
  2368   from prems have a1:"- a2 <= -a" by auto
  2369   from prems have a2: "-a <= -a1" by auto
  2370   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  2371   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  2372   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  2373     by (simp only: minus_le_iff)
  2374   then show ?thesis by simp
  2375 qed
  2376 
  2377 end