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