src/HOL/Ring_and_Field.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 28141 193c3ea0f63b
child 28559 55c003a5600a
permissions -rw-r--r--
moved global ML bindings to global place;
     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 unfold_locales
    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 unfold_locales
    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
   113   dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
   114 where
   115   [code func del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   116 
   117 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   118   unfolding dvd_def ..
   119 
   120 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   121   unfolding dvd_def by blast 
   122 
   123 end
   124 
   125 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
   126   (*previously almost_semiring*)
   127 begin
   128 
   129 subclass semiring_1 ..
   130 
   131 lemma dvd_refl: "a dvd a"
   132 proof -
   133   have "a = a * 1" by simp
   134   then show ?thesis unfolding dvd_def ..
   135 qed
   136 
   137 lemma dvd_trans:
   138   assumes "a dvd b" and "b dvd c"
   139   shows "a dvd c"
   140 proof -
   141   from assms obtain v where "b = a * v" unfolding dvd_def by auto
   142   moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
   143   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   144   then show ?thesis unfolding dvd_def ..
   145 qed
   146 
   147 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
   148   unfolding dvd_def by simp
   149 
   150 lemma dvd_0 [simp]: "a dvd 0"
   151 unfolding dvd_def proof
   152   show "0 = a * 0" by simp
   153 qed
   154 
   155 lemma one_dvd [simp]: "1 dvd a"
   156   unfolding dvd_def by simp
   157 
   158 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
   159   unfolding dvd_def by (blast intro: mult_left_commute)
   160 
   161 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   162   apply (subst mult_commute)
   163   apply (erule dvd_mult)
   164   done
   165 
   166 lemma dvd_triv_right [simp]: "a dvd b * a"
   167   by (rule dvd_mult) (rule dvd_refl)
   168 
   169 lemma dvd_triv_left [simp]: "a dvd a * b"
   170   by (rule dvd_mult2) (rule dvd_refl)
   171 
   172 lemma mult_dvd_mono:
   173   assumes ab: "a dvd b"
   174     and "cd": "c dvd d"
   175   shows "a * c dvd b * d"
   176 proof -
   177   from ab obtain b' where "b = a * b'" ..
   178   moreover from "cd" obtain d' where "d = c * d'" ..
   179   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   180   then show ?thesis ..
   181 qed
   182 
   183 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   184   by (simp add: dvd_def mult_assoc, blast)
   185 
   186 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   187   unfolding mult_ac [of a] by (rule dvd_mult_left)
   188 
   189 lemma dvd_0_right [iff]: "a dvd 0"
   190 proof -
   191   have "0 = a * 0" by simp
   192   then show ?thesis unfolding dvd_def ..
   193 qed
   194 
   195 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   196   by simp
   197 
   198 lemma dvd_add:
   199   assumes ab: "a dvd b"
   200     and ac: "a dvd c"
   201     shows "a dvd (b + c)"
   202 proof -
   203   from ab obtain b' where "b = a * b'" ..
   204   moreover from ac obtain c' where "c = a * c'" ..
   205   ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
   206   then show ?thesis ..
   207 qed
   208 
   209 end
   210 
   211 class no_zero_divisors = zero + times +
   212   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   213 
   214 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   215   + cancel_ab_semigroup_add + monoid_mult
   216 begin
   217 
   218 subclass semiring_0_cancel ..
   219 
   220 subclass semiring_1 ..
   221 
   222 end
   223 
   224 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
   225   + zero_neq_one + cancel_ab_semigroup_add
   226 begin
   227 
   228 subclass semiring_1_cancel ..
   229 subclass comm_semiring_0_cancel ..
   230 subclass comm_semiring_1 ..
   231 
   232 end
   233 
   234 class ring = semiring + ab_group_add
   235 begin
   236 
   237 subclass semiring_0_cancel ..
   238 
   239 text {* Distribution rules *}
   240 
   241 lemma minus_mult_left: "- (a * b) = - a * b"
   242   by (rule equals_zero_I) (simp add: left_distrib [symmetric]) 
   243 
   244 lemma minus_mult_right: "- (a * b) = a * - b"
   245   by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
   246 
   247 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   248   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   249 
   250 lemma minus_mult_commute: "- a * b = a * - b"
   251   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   252 
   253 lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
   254   by (simp add: right_distrib diff_minus 
   255     minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   256 
   257 lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
   258   by (simp add: left_distrib diff_minus 
   259     minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   260 
   261 lemmas ring_distribs =
   262   right_distrib left_distrib left_diff_distrib right_diff_distrib
   263 
   264 lemmas ring_simps =
   265   add_ac
   266   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   267   diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   268   ring_distribs
   269 
   270 lemma eq_add_iff1:
   271   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   272   by (simp add: ring_simps)
   273 
   274 lemma eq_add_iff2:
   275   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   276   by (simp add: ring_simps)
   277 
   278 end
   279 
   280 lemmas ring_distribs =
   281   right_distrib left_distrib left_diff_distrib right_diff_distrib
   282 
   283 class comm_ring = comm_semiring + ab_group_add
   284 begin
   285 
   286 subclass ring ..
   287 subclass comm_semiring_0_cancel ..
   288 
   289 end
   290 
   291 class ring_1 = ring + zero_neq_one + monoid_mult
   292 begin
   293 
   294 subclass semiring_1_cancel ..
   295 
   296 end
   297 
   298 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   299   (*previously ring*)
   300 begin
   301 
   302 subclass ring_1 ..
   303 subclass comm_semiring_1_cancel ..
   304 
   305 end
   306 
   307 class ring_no_zero_divisors = ring + no_zero_divisors
   308 begin
   309 
   310 lemma mult_eq_0_iff [simp]:
   311   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   312 proof (cases "a = 0 \<or> b = 0")
   313   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   314     then show ?thesis using no_zero_divisors by simp
   315 next
   316   case True then show ?thesis by auto
   317 qed
   318 
   319 text{*Cancellation of equalities with a common factor*}
   320 lemma mult_cancel_right [simp, noatp]:
   321   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   322 proof -
   323   have "(a * c = b * c) = ((a - b) * c = 0)"
   324     by (simp add: ring_distribs right_minus_eq)
   325   thus ?thesis
   326     by (simp add: disj_commute right_minus_eq)
   327 qed
   328 
   329 lemma mult_cancel_left [simp, noatp]:
   330   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   331 proof -
   332   have "(c * a = c * b) = (c * (a - b) = 0)"
   333     by (simp add: ring_distribs right_minus_eq)
   334   thus ?thesis
   335     by (simp add: right_minus_eq)
   336 qed
   337 
   338 end
   339 
   340 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   341 begin
   342 
   343 lemma mult_cancel_right1 [simp]:
   344   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   345   by (insert mult_cancel_right [of 1 c b], force)
   346 
   347 lemma mult_cancel_right2 [simp]:
   348   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   349   by (insert mult_cancel_right [of a c 1], simp)
   350  
   351 lemma mult_cancel_left1 [simp]:
   352   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   353   by (insert mult_cancel_left [of c 1 b], force)
   354 
   355 lemma mult_cancel_left2 [simp]:
   356   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   357   by (insert mult_cancel_left [of c a 1], simp)
   358 
   359 end
   360 
   361 class idom = comm_ring_1 + no_zero_divisors
   362 begin
   363 
   364 subclass ring_1_no_zero_divisors ..
   365 
   366 end
   367 
   368 class division_ring = ring_1 + inverse +
   369   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   370   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   371 begin
   372 
   373 subclass ring_1_no_zero_divisors
   374 proof unfold_locales
   375   fix a b :: 'a
   376   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   377   show "a * b \<noteq> 0"
   378   proof
   379     assume ab: "a * b = 0"
   380     hence "0 = inverse a * (a * b) * inverse b"
   381       by simp
   382     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   383       by (simp only: mult_assoc)
   384     also have "\<dots> = 1"
   385       using a b by simp
   386     finally show False
   387       by simp
   388   qed
   389 qed
   390 
   391 lemma nonzero_imp_inverse_nonzero:
   392   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   393 proof
   394   assume ianz: "inverse a = 0"
   395   assume "a \<noteq> 0"
   396   hence "1 = a * inverse a" by simp
   397   also have "... = 0" by (simp add: ianz)
   398   finally have "1 = 0" .
   399   thus False by (simp add: eq_commute)
   400 qed
   401 
   402 lemma inverse_zero_imp_zero:
   403   "inverse a = 0 \<Longrightarrow> a = 0"
   404 apply (rule classical)
   405 apply (drule nonzero_imp_inverse_nonzero)
   406 apply auto
   407 done
   408 
   409 lemma nonzero_inverse_minus_eq:
   410   assumes "a \<noteq> 0"
   411   shows "inverse (- a) = - inverse a"
   412 proof -
   413   have "- a * inverse (- a) = - a * - inverse a"
   414     using assms by simp
   415   then show ?thesis unfolding mult_cancel_left using assms by simp 
   416 qed
   417 
   418 lemma nonzero_inverse_inverse_eq:
   419   assumes "a \<noteq> 0"
   420   shows "inverse (inverse a) = a"
   421 proof -
   422   have "(inverse (inverse a) * inverse a) * a = a" 
   423     using assms by (simp add: nonzero_imp_inverse_nonzero)
   424   then show ?thesis using assms by (simp add: mult_assoc)
   425 qed
   426 
   427 lemma nonzero_inverse_eq_imp_eq:
   428   assumes inveq: "inverse a = inverse b"
   429     and anz:  "a \<noteq> 0"
   430     and bnz:  "b \<noteq> 0"
   431   shows "a = b"
   432 proof -
   433   have "a * inverse b = a * inverse a"
   434     by (simp add: inveq)
   435   hence "(a * inverse b) * b = (a * inverse a) * b"
   436     by simp
   437   then show "a = b"
   438     by (simp add: mult_assoc anz bnz)
   439 qed
   440 
   441 lemma inverse_1 [simp]: "inverse 1 = 1"
   442 proof -
   443   have "inverse 1 * 1 = 1" 
   444     by (rule left_inverse) (rule one_neq_zero)
   445   then show ?thesis by simp
   446 qed
   447 
   448 lemma inverse_unique: 
   449   assumes ab: "a * b = 1"
   450   shows "inverse a = b"
   451 proof -
   452   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   453   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
   454   ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
   455 qed
   456 
   457 lemma nonzero_inverse_mult_distrib: 
   458   assumes anz: "a \<noteq> 0"
   459     and bnz: "b \<noteq> 0"
   460   shows "inverse (a * b) = inverse b * inverse a"
   461 proof -
   462   have "inverse (a * b) * (a * b) * inverse b = inverse b" 
   463     by (simp add: anz bnz)
   464   hence "inverse (a * b) * a = inverse b" 
   465     by (simp add: mult_assoc bnz)
   466   hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 
   467     by simp
   468   thus ?thesis
   469     by (simp add: mult_assoc anz)
   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 unfold_locales
   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 add: divide_self)
   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 unfold_locales
   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 unfold_locales
   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 unfold_locales
   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 unfold_locales
   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 unfold_locales
   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 unfold_locales
   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 unfold_locales
  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 minus_mult_left)
  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 minus_mult_right)
  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 minus_mult_left [symmetric])
  1288 
  1289 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  1290 by (simp add: divide_inverse minus_mult_right [symmetric])
  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 text{*Also, extract signs from products*}
  1299 lemmas mult_minus_left = minus_mult_left [symmetric]
  1300 lemmas mult_minus_right = minus_mult_right [symmetric]
  1301 declare mult_minus_left [simp]   mult_minus_right [simp]
  1302 
  1303 lemma minus_divide_divide [simp]:
  1304   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
  1305 apply (cases "b=0", simp) 
  1306 apply (simp add: nonzero_minus_divide_divide) 
  1307 done
  1308 
  1309 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
  1310 by (simp add: diff_minus add_divide_distrib) 
  1311 
  1312 lemma add_divide_eq_iff:
  1313   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
  1314 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1315 
  1316 lemma divide_add_eq_iff:
  1317   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
  1318 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
  1319 
  1320 lemma diff_divide_eq_iff:
  1321   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
  1322 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1323 
  1324 lemma divide_diff_eq_iff:
  1325   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
  1326 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
  1327 
  1328 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
  1329 proof -
  1330   assume [simp]: "c\<noteq>0"
  1331   have "(a = b/c) = (a*c = (b/c)*c)" by simp
  1332   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
  1333   finally show ?thesis .
  1334 qed
  1335 
  1336 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
  1337 proof -
  1338   assume [simp]: "c\<noteq>0"
  1339   have "(b/c = a) = ((b/c)*c = a*c)"  by simp
  1340   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc) 
  1341   finally show ?thesis .
  1342 qed
  1343 
  1344 lemma eq_divide_eq:
  1345   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
  1346 by (simp add: nonzero_eq_divide_eq) 
  1347 
  1348 lemma divide_eq_eq:
  1349   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  1350 by (force simp add: nonzero_divide_eq_eq) 
  1351 
  1352 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1353     b = a * c ==> b / c = a"
  1354   by (subst divide_eq_eq, simp)
  1355 
  1356 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  1357     a * c = b ==> a = b / c"
  1358   by (subst eq_divide_eq, simp)
  1359 
  1360 
  1361 lemmas field_eq_simps = ring_simps
  1362   (* pull / out*)
  1363   add_divide_eq_iff divide_add_eq_iff
  1364   diff_divide_eq_iff divide_diff_eq_iff
  1365   (* multiply eqn *)
  1366   nonzero_eq_divide_eq nonzero_divide_eq_eq
  1367 (* is added later:
  1368   times_divide_eq_left times_divide_eq_right
  1369 *)
  1370 
  1371 text{*An example:*}
  1372 lemma fixes a b c d e f :: "'a::field"
  1373 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"
  1374 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
  1375  apply(simp add:field_eq_simps)
  1376 apply(simp)
  1377 done
  1378 
  1379 
  1380 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1381     x / y - w / z = (x * z - w * y) / (y * z)"
  1382 by (simp add:field_eq_simps times_divide_eq)
  1383 
  1384 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  1385     (x / y = w / z) = (x * z = w * y)"
  1386 by (simp add:field_eq_simps times_divide_eq)
  1387 
  1388 
  1389 subsection {* Ordered Fields *}
  1390 
  1391 lemma positive_imp_inverse_positive: 
  1392 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
  1393 proof -
  1394   have "0 < a * inverse a" 
  1395     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  1396   thus "0 < inverse a" 
  1397     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  1398 qed
  1399 
  1400 lemma negative_imp_inverse_negative:
  1401   "a < 0 ==> inverse a < (0::'a::ordered_field)"
  1402 by (insert positive_imp_inverse_positive [of "-a"], 
  1403     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
  1404 
  1405 lemma inverse_le_imp_le:
  1406 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
  1407 shows "b \<le> (a::'a::ordered_field)"
  1408 proof (rule classical)
  1409   assume "~ b \<le> a"
  1410   hence "a < b"  by (simp add: linorder_not_le)
  1411   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
  1412   hence "a * inverse a \<le> a * inverse b"
  1413     by (simp add: apos invle order_less_imp_le mult_left_mono)
  1414   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  1415     by (simp add: bpos order_less_imp_le mult_right_mono)
  1416   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  1417 qed
  1418 
  1419 lemma inverse_positive_imp_positive:
  1420 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
  1421 shows "0 < (a::'a::ordered_field)"
  1422 proof -
  1423   have "0 < inverse (inverse a)"
  1424     using inv_gt_0 by (rule positive_imp_inverse_positive)
  1425   thus "0 < a"
  1426     using nz by (simp add: nonzero_inverse_inverse_eq)
  1427 qed
  1428 
  1429 lemma inverse_positive_iff_positive [simp]:
  1430   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  1431 apply (cases "a = 0", simp)
  1432 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
  1433 done
  1434 
  1435 lemma inverse_negative_imp_negative:
  1436 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
  1437 shows "a < (0::'a::ordered_field)"
  1438 proof -
  1439   have "inverse (inverse a) < 0"
  1440     using inv_less_0 by (rule negative_imp_inverse_negative)
  1441   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
  1442 qed
  1443 
  1444 lemma inverse_negative_iff_negative [simp]:
  1445   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  1446 apply (cases "a = 0", simp)
  1447 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
  1448 done
  1449 
  1450 lemma inverse_nonnegative_iff_nonnegative [simp]:
  1451   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1452 by (simp add: linorder_not_less [symmetric])
  1453 
  1454 lemma inverse_nonpositive_iff_nonpositive [simp]:
  1455   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1456 by (simp add: linorder_not_less [symmetric])
  1457 
  1458 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
  1459 proof
  1460   fix x::'a
  1461   have m1: "- (1::'a) < 0" by simp
  1462   from add_strict_right_mono[OF m1, where c=x] 
  1463   have "(- 1) + x < x" by simp
  1464   thus "\<exists>y. y < x" by blast
  1465 qed
  1466 
  1467 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
  1468 proof
  1469   fix x::'a
  1470   have m1: " (1::'a) > 0" by simp
  1471   from add_strict_right_mono[OF m1, where c=x] 
  1472   have "1 + x > x" by simp
  1473   thus "\<exists>y. y > x" by blast
  1474 qed
  1475 
  1476 subsection{*Anti-Monotonicity of @{term inverse}*}
  1477 
  1478 lemma less_imp_inverse_less:
  1479 assumes less: "a < b" and apos:  "0 < a"
  1480 shows "inverse b < inverse (a::'a::ordered_field)"
  1481 proof (rule ccontr)
  1482   assume "~ inverse b < inverse a"
  1483   hence "inverse a \<le> inverse b"
  1484     by (simp add: linorder_not_less)
  1485   hence "~ (a < b)"
  1486     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  1487   thus False
  1488     by (rule notE [OF _ less])
  1489 qed
  1490 
  1491 lemma inverse_less_imp_less:
  1492   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  1493 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  1494 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  1495 done
  1496 
  1497 text{*Both premises are essential. Consider -1 and 1.*}
  1498 lemma inverse_less_iff_less [simp,noatp]:
  1499   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1500 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  1501 
  1502 lemma le_imp_inverse_le:
  1503   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1504 by (force simp add: order_le_less less_imp_inverse_less)
  1505 
  1506 lemma inverse_le_iff_le [simp,noatp]:
  1507  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1508 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  1509 
  1510 
  1511 text{*These results refer to both operands being negative.  The opposite-sign
  1512 case is trivial, since inverse preserves signs.*}
  1513 lemma inverse_le_imp_le_neg:
  1514   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  1515 apply (rule classical) 
  1516 apply (subgoal_tac "a < 0") 
  1517  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  1518 apply (insert inverse_le_imp_le [of "-b" "-a"])
  1519 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1520 done
  1521 
  1522 lemma less_imp_inverse_less_neg:
  1523    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  1524 apply (subgoal_tac "a < 0") 
  1525  prefer 2 apply (blast intro: order_less_trans) 
  1526 apply (insert less_imp_inverse_less [of "-b" "-a"])
  1527 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1528 done
  1529 
  1530 lemma inverse_less_imp_less_neg:
  1531    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  1532 apply (rule classical) 
  1533 apply (subgoal_tac "a < 0") 
  1534  prefer 2
  1535  apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  1536 apply (insert inverse_less_imp_less [of "-b" "-a"])
  1537 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  1538 done
  1539 
  1540 lemma inverse_less_iff_less_neg [simp,noatp]:
  1541   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  1542 apply (insert inverse_less_iff_less [of "-b" "-a"])
  1543 apply (simp del: inverse_less_iff_less 
  1544             add: order_less_imp_not_eq nonzero_inverse_minus_eq)
  1545 done
  1546 
  1547 lemma le_imp_inverse_le_neg:
  1548   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  1549 by (force simp add: order_le_less less_imp_inverse_less_neg)
  1550 
  1551 lemma inverse_le_iff_le_neg [simp,noatp]:
  1552  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  1553 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  1554 
  1555 
  1556 subsection{*Inverses and the Number One*}
  1557 
  1558 lemma one_less_inverse_iff:
  1559   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
  1560 proof cases
  1561   assume "0 < x"
  1562     with inverse_less_iff_less [OF zero_less_one, of x]
  1563     show ?thesis by simp
  1564 next
  1565   assume notless: "~ (0 < x)"
  1566   have "~ (1 < inverse x)"
  1567   proof
  1568     assume "1 < inverse x"
  1569     also with notless have "... \<le> 0" by (simp add: linorder_not_less)
  1570     also have "... < 1" by (rule zero_less_one) 
  1571     finally show False by auto
  1572   qed
  1573   with notless show ?thesis by simp
  1574 qed
  1575 
  1576 lemma inverse_eq_1_iff [simp]:
  1577   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
  1578 by (insert inverse_eq_iff_eq [of x 1], simp) 
  1579 
  1580 lemma one_le_inverse_iff:
  1581   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
  1582 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
  1583                     eq_commute [of 1]) 
  1584 
  1585 lemma inverse_less_1_iff:
  1586   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
  1587 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
  1588 
  1589 lemma inverse_le_1_iff:
  1590   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  1591 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  1592 
  1593 
  1594 subsection{*Simplification of Inequalities Involving Literal Divisors*}
  1595 
  1596 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  1597 proof -
  1598   assume less: "0<c"
  1599   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
  1600     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1601   also have "... = (a*c \<le> b)"
  1602     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1603   finally show ?thesis .
  1604 qed
  1605 
  1606 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  1607 proof -
  1608   assume less: "c<0"
  1609   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
  1610     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1611   also have "... = (b \<le> a*c)"
  1612     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1613   finally show ?thesis .
  1614 qed
  1615 
  1616 lemma le_divide_eq:
  1617   "(a \<le> b/c) = 
  1618    (if 0 < c then a*c \<le> b
  1619              else if c < 0 then b \<le> a*c
  1620              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"
  1621 apply (cases "c=0", simp) 
  1622 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
  1623 done
  1624 
  1625 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
  1626 proof -
  1627   assume less: "0<c"
  1628   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
  1629     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1630   also have "... = (b \<le> a*c)"
  1631     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1632   finally show ?thesis .
  1633 qed
  1634 
  1635 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
  1636 proof -
  1637   assume less: "c<0"
  1638   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
  1639     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
  1640   also have "... = (a*c \<le> b)"
  1641     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1642   finally show ?thesis .
  1643 qed
  1644 
  1645 lemma divide_le_eq:
  1646   "(b/c \<le> a) = 
  1647    (if 0 < c then b \<le> a*c
  1648              else if c < 0 then a*c \<le> b
  1649              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
  1650 apply (cases "c=0", simp) 
  1651 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  1652 done
  1653 
  1654 lemma pos_less_divide_eq:
  1655      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  1656 proof -
  1657   assume less: "0<c"
  1658   hence "(a < b/c) = (a*c < (b/c)*c)"
  1659     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1660   also have "... = (a*c < b)"
  1661     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1662   finally show ?thesis .
  1663 qed
  1664 
  1665 lemma neg_less_divide_eq:
  1666  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
  1667 proof -
  1668   assume less: "c<0"
  1669   hence "(a < b/c) = ((b/c)*c < a*c)"
  1670     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1671   also have "... = (b < a*c)"
  1672     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
  1673   finally show ?thesis .
  1674 qed
  1675 
  1676 lemma less_divide_eq:
  1677   "(a < b/c) = 
  1678    (if 0 < c then a*c < b
  1679              else if c < 0 then b < a*c
  1680              else  a < (0::'a::{ordered_field,division_by_zero}))"
  1681 apply (cases "c=0", simp) 
  1682 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
  1683 done
  1684 
  1685 lemma pos_divide_less_eq:
  1686      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
  1687 proof -
  1688   assume less: "0<c"
  1689   hence "(b/c < a) = ((b/c)*c < a*c)"
  1690     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
  1691   also have "... = (b < a*c)"
  1692     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
  1693   finally show ?thesis .
  1694 qed
  1695 
  1696 lemma neg_divide_less_eq:
  1697  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
  1698 proof -
  1699   assume less: "c<0"
  1700   hence "(b/c < a) = (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_eq [OF less] divide_inverse mult_assoc) 
  1704   finally show ?thesis .
  1705 qed
  1706 
  1707 lemma divide_less_eq:
  1708   "(b/c < a) = 
  1709    (if 0 < c then b < a*c
  1710              else if c < 0 then a*c < b
  1711              else 0 < (a::'a::{ordered_field,division_by_zero}))"
  1712 apply (cases "c=0", simp) 
  1713 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
  1714 done
  1715 
  1716 
  1717 subsection{*Field simplification*}
  1718 
  1719 text{* Lemmas @{text field_simps} multiply with denominators in
  1720 in(equations) if they can be proved to be non-zero (for equations) or
  1721 positive/negative (for inequations). *}
  1722 
  1723 lemmas field_simps = field_eq_simps
  1724   (* multiply ineqn *)
  1725   pos_divide_less_eq neg_divide_less_eq
  1726   pos_less_divide_eq neg_less_divide_eq
  1727   pos_divide_le_eq neg_divide_le_eq
  1728   pos_le_divide_eq neg_le_divide_eq
  1729 
  1730 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
  1731 of positivity/negativity needed for @{text field_simps}. Have not added @{text
  1732 sign_simps} to @{text field_simps} because the former can lead to case
  1733 explosions. *}
  1734 
  1735 lemmas sign_simps = group_simps
  1736   zero_less_mult_iff  mult_less_0_iff
  1737 
  1738 (* Only works once linear arithmetic is installed:
  1739 text{*An example:*}
  1740 lemma fixes a b c d e f :: "'a::ordered_field"
  1741 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
  1742  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
  1743  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
  1744 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
  1745  prefer 2 apply(simp add:sign_simps)
  1746 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  1747  prefer 2 apply(simp add:sign_simps)
  1748 apply(simp add:field_simps)
  1749 done
  1750 *)
  1751 
  1752 
  1753 subsection{*Division and Signs*}
  1754 
  1755 lemma zero_less_divide_iff:
  1756      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  1757 by (simp add: divide_inverse zero_less_mult_iff)
  1758 
  1759 lemma divide_less_0_iff:
  1760      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  1761       (0 < a & b < 0 | a < 0 & 0 < b)"
  1762 by (simp add: divide_inverse mult_less_0_iff)
  1763 
  1764 lemma zero_le_divide_iff:
  1765      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  1766       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  1767 by (simp add: divide_inverse zero_le_mult_iff)
  1768 
  1769 lemma divide_le_0_iff:
  1770      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  1771       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  1772 by (simp add: divide_inverse mult_le_0_iff)
  1773 
  1774 lemma divide_eq_0_iff [simp,noatp]:
  1775      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  1776 by (simp add: divide_inverse)
  1777 
  1778 lemma divide_pos_pos:
  1779   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
  1780 by(simp add:field_simps)
  1781 
  1782 
  1783 lemma divide_nonneg_pos:
  1784   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
  1785 by(simp add:field_simps)
  1786 
  1787 lemma divide_neg_pos:
  1788   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  1789 by(simp add:field_simps)
  1790 
  1791 lemma divide_nonpos_pos:
  1792   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  1793 by(simp add:field_simps)
  1794 
  1795 lemma divide_pos_neg:
  1796   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  1797 by(simp add:field_simps)
  1798 
  1799 lemma divide_nonneg_neg:
  1800   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
  1801 by(simp add:field_simps)
  1802 
  1803 lemma divide_neg_neg:
  1804   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  1805 by(simp add:field_simps)
  1806 
  1807 lemma divide_nonpos_neg:
  1808   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  1809 by(simp add:field_simps)
  1810 
  1811 
  1812 subsection{*Cancellation Laws for Division*}
  1813 
  1814 lemma divide_cancel_right [simp,noatp]:
  1815      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  1816 apply (cases "c=0", simp)
  1817 apply (simp add: divide_inverse)
  1818 done
  1819 
  1820 lemma divide_cancel_left [simp,noatp]:
  1821      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  1822 apply (cases "c=0", simp)
  1823 apply (simp add: divide_inverse)
  1824 done
  1825 
  1826 
  1827 subsection {* Division and the Number One *}
  1828 
  1829 text{*Simplify expressions equated with 1*}
  1830 lemma divide_eq_1_iff [simp,noatp]:
  1831      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1832 apply (cases "b=0", simp)
  1833 apply (simp add: right_inverse_eq)
  1834 done
  1835 
  1836 lemma one_eq_divide_iff [simp,noatp]:
  1837      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  1838 by (simp add: eq_commute [of 1])
  1839 
  1840 lemma zero_eq_1_divide_iff [simp,noatp]:
  1841      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  1842 apply (cases "a=0", simp)
  1843 apply (auto simp add: nonzero_eq_divide_eq)
  1844 done
  1845 
  1846 lemma one_divide_eq_0_iff [simp,noatp]:
  1847      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  1848 apply (cases "a=0", simp)
  1849 apply (insert zero_neq_one [THEN not_sym])
  1850 apply (auto simp add: nonzero_divide_eq_eq)
  1851 done
  1852 
  1853 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
  1854 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
  1855 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
  1856 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
  1857 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  1858 
  1859 declare zero_less_divide_1_iff [simp]
  1860 declare divide_less_0_1_iff [simp,noatp]
  1861 declare zero_le_divide_1_iff [simp]
  1862 declare divide_le_0_1_iff [simp,noatp]
  1863 
  1864 
  1865 subsection {* Ordering Rules for Division *}
  1866 
  1867 lemma divide_strict_right_mono:
  1868      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
  1869 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  1870               positive_imp_inverse_positive)
  1871 
  1872 lemma divide_right_mono:
  1873      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  1874 by (force simp add: divide_strict_right_mono order_le_less)
  1875 
  1876 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1877     ==> c <= 0 ==> b / c <= a / c"
  1878 apply (drule divide_right_mono [of _ _ "- c"])
  1879 apply auto
  1880 done
  1881 
  1882 lemma divide_strict_right_mono_neg:
  1883      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  1884 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  1885 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  1886 done
  1887 
  1888 text{*The last premise ensures that @{term a} and @{term b} 
  1889       have the same sign*}
  1890 lemma divide_strict_left_mono:
  1891   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1892 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  1893 
  1894 lemma divide_left_mono:
  1895   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
  1896 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  1897 
  1898 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  1899     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  1900   apply (drule divide_left_mono [of _ _ "- c"])
  1901   apply (auto simp add: mult_commute)
  1902 done
  1903 
  1904 lemma divide_strict_left_mono_neg:
  1905   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  1906 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  1907 
  1908 
  1909 text{*Simplify quotients that are compared with the value 1.*}
  1910 
  1911 lemma le_divide_eq_1 [noatp]:
  1912   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1913   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  1914 by (auto simp add: le_divide_eq)
  1915 
  1916 lemma divide_le_eq_1 [noatp]:
  1917   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1918   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  1919 by (auto simp add: divide_le_eq)
  1920 
  1921 lemma less_divide_eq_1 [noatp]:
  1922   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1923   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  1924 by (auto simp add: less_divide_eq)
  1925 
  1926 lemma divide_less_eq_1 [noatp]:
  1927   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1928   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  1929 by (auto simp add: divide_less_eq)
  1930 
  1931 
  1932 subsection{*Conditional Simplification Rules: No Case Splits*}
  1933 
  1934 lemma le_divide_eq_1_pos [simp,noatp]:
  1935   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1936   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  1937 by (auto simp add: le_divide_eq)
  1938 
  1939 lemma le_divide_eq_1_neg [simp,noatp]:
  1940   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1941   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  1942 by (auto simp add: le_divide_eq)
  1943 
  1944 lemma divide_le_eq_1_pos [simp,noatp]:
  1945   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1946   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  1947 by (auto simp add: divide_le_eq)
  1948 
  1949 lemma divide_le_eq_1_neg [simp,noatp]:
  1950   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1951   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  1952 by (auto simp add: divide_le_eq)
  1953 
  1954 lemma less_divide_eq_1_pos [simp,noatp]:
  1955   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1956   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  1957 by (auto simp add: less_divide_eq)
  1958 
  1959 lemma less_divide_eq_1_neg [simp,noatp]:
  1960   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1961   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  1962 by (auto simp add: less_divide_eq)
  1963 
  1964 lemma divide_less_eq_1_pos [simp,noatp]:
  1965   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1966   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  1967 by (auto simp add: divide_less_eq)
  1968 
  1969 lemma divide_less_eq_1_neg [simp,noatp]:
  1970   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1971   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  1972 by (auto simp add: divide_less_eq)
  1973 
  1974 lemma eq_divide_eq_1 [simp,noatp]:
  1975   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1976   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  1977 by (auto simp add: eq_divide_eq)
  1978 
  1979 lemma divide_eq_eq_1 [simp,noatp]:
  1980   fixes a :: "'a :: {ordered_field,division_by_zero}"
  1981   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  1982 by (auto simp add: divide_eq_eq)
  1983 
  1984 
  1985 subsection {* Reasoning about inequalities with division *}
  1986 
  1987 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  1988     ==> x * y <= x"
  1989   by (auto simp add: mult_compare_simps);
  1990 
  1991 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  1992     ==> y * x <= x"
  1993   by (auto simp add: mult_compare_simps);
  1994 
  1995 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  1996     x / y <= z";
  1997   by (subst pos_divide_le_eq, assumption+);
  1998 
  1999 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  2000     z <= x / y"
  2001 by(simp add:field_simps)
  2002 
  2003 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  2004     x / y < z"
  2005 by(simp add:field_simps)
  2006 
  2007 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  2008     z < x / y"
  2009 by(simp add:field_simps)
  2010 
  2011 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  2012     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  2013   apply (rule mult_imp_div_pos_le)
  2014   apply simp
  2015   apply (subst times_divide_eq_left)
  2016   apply (rule mult_imp_le_div_pos, assumption)
  2017   apply (rule mult_mono)
  2018   apply simp_all
  2019 done
  2020 
  2021 lemma frac_less: "(0::'a::ordered_field) <= x ==> 
  2022     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  2023   apply (rule mult_imp_div_pos_less)
  2024   apply simp;
  2025   apply (subst times_divide_eq_left);
  2026   apply (rule mult_imp_less_div_pos, assumption)
  2027   apply (erule mult_less_le_imp_less)
  2028   apply simp_all
  2029 done
  2030 
  2031 lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  2032     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  2033   apply (rule mult_imp_div_pos_less)
  2034   apply simp_all
  2035   apply (subst times_divide_eq_left);
  2036   apply (rule mult_imp_less_div_pos, assumption)
  2037   apply (erule mult_le_less_imp_less)
  2038   apply simp_all
  2039 done
  2040 
  2041 text{*It's not obvious whether these should be simprules or not. 
  2042   Their effect is to gather terms into one big fraction, like
  2043   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  2044   seem to need them.*}
  2045 
  2046 declare times_divide_eq [simp]
  2047 
  2048 
  2049 subsection {* Ordered Fields are Dense *}
  2050 
  2051 context ordered_semidom
  2052 begin
  2053 
  2054 lemma less_add_one: "a < a + 1"
  2055 proof -
  2056   have "a + 0 < a + 1"
  2057     by (blast intro: zero_less_one add_strict_left_mono)
  2058   thus ?thesis by simp
  2059 qed
  2060 
  2061 lemma zero_less_two: "0 < 1 + 1"
  2062   by (blast intro: less_trans zero_less_one less_add_one)
  2063 
  2064 end
  2065 
  2066 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
  2067 by (simp add: field_simps zero_less_two)
  2068 
  2069 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
  2070 by (simp add: field_simps zero_less_two)
  2071 
  2072 instance ordered_field < dense_linear_order
  2073 proof
  2074   fix x y :: 'a
  2075   have "x < x + 1" by simp
  2076   then show "\<exists>y. x < y" .. 
  2077   have "x - 1 < x" by simp
  2078   then show "\<exists>y. y < x" ..
  2079   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  2080 qed
  2081 
  2082 
  2083 subsection {* Absolute Value *}
  2084 
  2085 context ordered_idom
  2086 begin
  2087 
  2088 lemma mult_sgn_abs: "sgn x * abs x = x"
  2089   unfolding abs_if sgn_if by auto
  2090 
  2091 end
  2092 
  2093 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  2094   by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  2095 
  2096 class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
  2097   assumes abs_eq_mult:
  2098     "(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>"
  2099 
  2100 
  2101 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
  2102 begin
  2103 
  2104 subclass lordered_ab_group_add_meet ..
  2105 subclass lordered_ab_group_add_join ..
  2106 
  2107 end
  2108 
  2109 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
  2110 proof -
  2111   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
  2112   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2113   have a: "(abs a) * (abs b) = ?x"
  2114     by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)
  2115   {
  2116     fix u v :: 'a
  2117     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
  2118               u * v = pprt a * pprt b + pprt a * nprt b + 
  2119                       nprt a * pprt b + nprt a * nprt b"
  2120       apply (subst prts[of u], subst prts[of v])
  2121       apply (simp add: ring_simps) 
  2122       done
  2123   }
  2124   note b = this[OF refl[of a] refl[of b]]
  2125   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
  2126   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
  2127   have xy: "- ?x <= ?y"
  2128     apply (simp)
  2129     apply (rule_tac y="0::'a" in order_trans)
  2130     apply (rule addm2)
  2131     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2132     apply (rule addm)
  2133     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  2134     done
  2135   have yx: "?y <= ?x"
  2136     apply (simp add:diff_def)
  2137     apply (rule_tac y=0 in order_trans)
  2138     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2139     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  2140     done
  2141   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  2142   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  2143   show ?thesis
  2144     apply (rule abs_leI)
  2145     apply (simp add: i1)
  2146     apply (simp add: i2[simplified minus_le_iff])
  2147     done
  2148 qed
  2149 
  2150 instance lordered_ring \<subseteq> pordered_ring_abs
  2151 proof
  2152   fix a b :: "'a\<Colon> lordered_ring"
  2153   assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
  2154   show "abs (a*b) = abs a * abs b"
  2155 proof -
  2156   have s: "(0 <= a*b) | (a*b <= 0)"
  2157     apply (auto)    
  2158     apply (rule_tac split_mult_pos_le)
  2159     apply (rule_tac contrapos_np[of "a*b <= 0"])
  2160     apply (simp)
  2161     apply (rule_tac split_mult_neg_le)
  2162     apply (insert prems)
  2163     apply (blast)
  2164     done
  2165   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
  2166     by (simp add: prts[symmetric])
  2167   show ?thesis
  2168   proof cases
  2169     assume "0 <= a * b"
  2170     then show ?thesis
  2171       apply (simp_all add: mulprts abs_prts)
  2172       apply (insert prems)
  2173       apply (auto simp add: 
  2174 	ring_simps 
  2175 	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
  2176 	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
  2177 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  2178 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  2179       done
  2180   next
  2181     assume "~(0 <= a*b)"
  2182     with s have "a*b <= 0" by simp
  2183     then show ?thesis
  2184       apply (simp_all add: mulprts abs_prts)
  2185       apply (insert prems)
  2186       apply (auto simp add: ring_simps)
  2187       apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  2188       apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  2189       done
  2190   qed
  2191 qed
  2192 qed
  2193 
  2194 instance ordered_idom \<subseteq> pordered_ring_abs
  2195 by default (auto simp add: abs_if not_less
  2196   equal_neg_zero neg_equal_zero mult_less_0_iff)
  2197 
  2198 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
  2199   by (simp add: abs_eq_mult linorder_linear)
  2200 
  2201 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
  2202   by (simp add: abs_if) 
  2203 
  2204 lemma nonzero_abs_inverse:
  2205      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
  2206 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  2207                       negative_imp_inverse_negative)
  2208 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  2209 done
  2210 
  2211 lemma abs_inverse [simp]:
  2212      "abs (inverse (a::'a::{ordered_field,division_by_zero})) = 
  2213       inverse (abs a)"
  2214 apply (cases "a=0", simp) 
  2215 apply (simp add: nonzero_abs_inverse) 
  2216 done
  2217 
  2218 lemma nonzero_abs_divide:
  2219      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  2220 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  2221 
  2222 lemma abs_divide [simp]:
  2223      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
  2224 apply (cases "b=0", simp) 
  2225 apply (simp add: nonzero_abs_divide) 
  2226 done
  2227 
  2228 lemma abs_mult_less:
  2229      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"
  2230 proof -
  2231   assume ac: "abs a < c"
  2232   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  2233   assume "abs b < d"
  2234   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  2235 qed
  2236 
  2237 lemmas eq_minus_self_iff = equal_neg_zero
  2238 
  2239 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
  2240   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  2241 
  2242 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
  2243 apply (simp add: order_less_le abs_le_iff)  
  2244 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  2245 done
  2246 
  2247 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  2248     (abs y) * x = abs (y * x)"
  2249   apply (subst abs_mult)
  2250   apply simp
  2251 done
  2252 
  2253 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  2254     abs x / y = abs (x / y)"
  2255   apply (subst abs_divide)
  2256   apply (simp add: order_less_imp_le)
  2257 done
  2258 
  2259 
  2260 subsection {* Bounds of products via negative and positive Part *}
  2261 
  2262 lemma mult_le_prts:
  2263   assumes
  2264   "a1 <= (a::'a::lordered_ring)"
  2265   "a <= a2"
  2266   "b1 <= b"
  2267   "b <= b2"
  2268   shows
  2269   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
  2270 proof - 
  2271   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
  2272     apply (subst prts[symmetric])+
  2273     apply simp
  2274     done
  2275   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
  2276     by (simp add: ring_simps)
  2277   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
  2278     by (simp_all add: prems mult_mono)
  2279   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
  2280   proof -
  2281     have "pprt a * nprt b <= pprt a * nprt b2"
  2282       by (simp add: mult_left_mono prems)
  2283     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
  2284       by (simp add: mult_right_mono_neg prems)
  2285     ultimately show ?thesis
  2286       by simp
  2287   qed
  2288   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
  2289   proof - 
  2290     have "nprt a * pprt b <= nprt a2 * pprt b"
  2291       by (simp add: mult_right_mono prems)
  2292     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
  2293       by (simp add: mult_left_mono_neg prems)
  2294     ultimately show ?thesis
  2295       by simp
  2296   qed
  2297   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
  2298   proof -
  2299     have "nprt a * nprt b <= nprt a * nprt b1"
  2300       by (simp add: mult_left_mono_neg prems)
  2301     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  2302       by (simp add: mult_right_mono_neg prems)
  2303     ultimately show ?thesis
  2304       by simp
  2305   qed
  2306   ultimately show ?thesis
  2307     by - (rule add_mono | simp)+
  2308 qed
  2309 
  2310 lemma mult_ge_prts:
  2311   assumes
  2312   "a1 <= (a::'a::lordered_ring)"
  2313   "a <= a2"
  2314   "b1 <= b"
  2315   "b <= b2"
  2316   shows
  2317   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
  2318 proof - 
  2319   from prems have a1:"- a2 <= -a" by auto
  2320   from prems have a2: "-a <= -a1" by auto
  2321   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
  2322   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
  2323   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
  2324     by (simp only: minus_le_iff)
  2325   then show ?thesis by simp
  2326 qed
  2327 
  2328 end