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