src/HOL/Rings.thy
author haftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 54225 8a49a5a30284
parent 54147 97a8ff4e4ac9
child 54230 b1d955791529
permissions -rw-r--r--
generalized of_bool conversion
     1 (*  Title:      HOL/Rings.thy
     2     Author:     Gertrud Bauer
     3     Author:     Steven Obua
     4     Author:     Tobias Nipkow
     5     Author:     Lawrence C Paulson
     6     Author:     Markus Wenzel
     7     Author:     Jeremy Avigad
     8 *)
     9 
    10 header {* Rings *}
    11 
    12 theory Rings
    13 imports Groups
    14 begin
    15 
    16 class semiring = ab_semigroup_add + semigroup_mult +
    17   assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
    18   assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
    19 begin
    20 
    21 text{*For the @{text combine_numerals} simproc*}
    22 lemma combine_common_factor:
    23   "a * e + (b * e + c) = (a + b) * e + c"
    24 by (simp add: distrib_right add_ac)
    25 
    26 end
    27 
    28 class mult_zero = times + zero +
    29   assumes mult_zero_left [simp]: "0 * a = 0"
    30   assumes mult_zero_right [simp]: "a * 0 = 0"
    31 
    32 class semiring_0 = semiring + comm_monoid_add + mult_zero
    33 
    34 class semiring_0_cancel = semiring + cancel_comm_monoid_add
    35 begin
    36 
    37 subclass semiring_0
    38 proof
    39   fix a :: 'a
    40   have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
    41   thus "0 * a = 0" by (simp only: add_left_cancel)
    42 next
    43   fix a :: 'a
    44   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
    45   thus "a * 0 = 0" by (simp only: add_left_cancel)
    46 qed
    47 
    48 end
    49 
    50 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
    51   assumes distrib: "(a + b) * c = a * c + b * c"
    52 begin
    53 
    54 subclass semiring
    55 proof
    56   fix a b c :: 'a
    57   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
    58   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
    59   also have "... = b * a + c * a" by (simp only: distrib)
    60   also have "... = a * b + a * c" by (simp add: mult_ac)
    61   finally show "a * (b + c) = a * b + a * c" by blast
    62 qed
    63 
    64 end
    65 
    66 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
    67 begin
    68 
    69 subclass semiring_0 ..
    70 
    71 end
    72 
    73 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
    74 begin
    75 
    76 subclass semiring_0_cancel ..
    77 
    78 subclass comm_semiring_0 ..
    79 
    80 end
    81 
    82 class zero_neq_one = zero + one +
    83   assumes zero_neq_one [simp]: "0 \<noteq> 1"
    84 begin
    85 
    86 lemma one_neq_zero [simp]: "1 \<noteq> 0"
    87 by (rule not_sym) (rule zero_neq_one)
    88 
    89 definition of_bool :: "bool \<Rightarrow> 'a"
    90 where
    91   "of_bool p = (if p then 1 else 0)" 
    92 
    93 lemma of_bool_eq [simp, code]:
    94   "of_bool False = 0"
    95   "of_bool True = 1"
    96   by (simp_all add: of_bool_def)
    97 
    98 lemma of_bool_eq_iff:
    99   "of_bool p = of_bool q \<longleftrightarrow> p = q"
   100   by (simp add: of_bool_def)
   101 
   102 end  
   103 
   104 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
   105 
   106 text {* Abstract divisibility *}
   107 
   108 class dvd = times
   109 begin
   110 
   111 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) where
   112   "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   113 
   114 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   115   unfolding dvd_def ..
   116 
   117 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   118   unfolding dvd_def by blast 
   119 
   120 end
   121 
   122 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd
   123   (*previously almost_semiring*)
   124 begin
   125 
   126 subclass semiring_1 ..
   127 
   128 lemma dvd_refl[simp]: "a dvd a"
   129 proof
   130   show "a = a * 1" by simp
   131 qed
   132 
   133 lemma dvd_trans:
   134   assumes "a dvd b" and "b dvd c"
   135   shows "a dvd c"
   136 proof -
   137   from assms obtain v where "b = a * v" by (auto elim!: dvdE)
   138   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)
   139   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
   140   then show ?thesis ..
   141 qed
   142 
   143 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
   144 by (auto intro: dvd_refl elim!: dvdE)
   145 
   146 lemma dvd_0_right [iff]: "a dvd 0"
   147 proof
   148   show "0 = a * 0" by simp
   149 qed
   150 
   151 lemma one_dvd [simp]: "1 dvd a"
   152 by (auto intro!: dvdI)
   153 
   154 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
   155 by (auto intro!: mult_left_commute dvdI elim!: dvdE)
   156 
   157 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   158   apply (subst mult_commute)
   159   apply (erule dvd_mult)
   160   done
   161 
   162 lemma dvd_triv_right [simp]: "a dvd b * a"
   163 by (rule dvd_mult) (rule dvd_refl)
   164 
   165 lemma dvd_triv_left [simp]: "a dvd a * b"
   166 by (rule dvd_mult2) (rule dvd_refl)
   167 
   168 lemma mult_dvd_mono:
   169   assumes "a dvd b"
   170     and "c dvd d"
   171   shows "a * c dvd b * d"
   172 proof -
   173   from `a dvd b` obtain b' where "b = a * b'" ..
   174   moreover from `c dvd d` obtain d' where "d = c * d'" ..
   175   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   176   then show ?thesis ..
   177 qed
   178 
   179 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
   180 by (simp add: dvd_def mult_assoc, blast)
   181 
   182 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   183   unfolding mult_ac [of a] by (rule dvd_mult_left)
   184 
   185 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   186 by simp
   187 
   188 lemma dvd_add[simp]:
   189   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"
   190 proof -
   191   from `a dvd b` obtain b' where "b = a * b'" ..
   192   moreover from `a dvd c` obtain c' where "c = a * c'" ..
   193   ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
   194   then show ?thesis ..
   195 qed
   196 
   197 end
   198 
   199 class no_zero_divisors = zero + times +
   200   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   201 begin
   202 
   203 lemma divisors_zero:
   204   assumes "a * b = 0"
   205   shows "a = 0 \<or> b = 0"
   206 proof (rule classical)
   207   assume "\<not> (a = 0 \<or> b = 0)"
   208   then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   209   with no_zero_divisors have "a * b \<noteq> 0" by blast
   210   with assms show ?thesis by simp
   211 qed
   212 
   213 end
   214 
   215 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   216   + zero_neq_one + monoid_mult
   217 begin
   218 
   219 subclass semiring_0_cancel ..
   220 
   221 subclass semiring_1 ..
   222 
   223 end
   224 
   225 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
   226   + zero_neq_one + comm_monoid_mult
   227 begin
   228 
   229 subclass semiring_1_cancel ..
   230 subclass comm_semiring_0_cancel ..
   231 subclass comm_semiring_1 ..
   232 
   233 end
   234 
   235 class ring = semiring + ab_group_add
   236 begin
   237 
   238 subclass semiring_0_cancel ..
   239 
   240 text {* Distribution rules *}
   241 
   242 lemma minus_mult_left: "- (a * b) = - a * b"
   243 by (rule minus_unique) (simp add: distrib_right [symmetric]) 
   244 
   245 lemma minus_mult_right: "- (a * b) = a * - b"
   246 by (rule minus_unique) (simp add: distrib_left [symmetric]) 
   247 
   248 text{*Extract signs from products*}
   249 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
   250 lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
   251 
   252 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   253 by simp
   254 
   255 lemma minus_mult_commute: "- a * b = a * - b"
   256 by simp
   257 
   258 lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
   259 by (simp add: distrib_left diff_minus)
   260 
   261 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
   262 by (simp add: distrib_right diff_minus)
   263 
   264 lemmas ring_distribs =
   265   distrib_left distrib_right left_diff_distrib right_diff_distrib
   266 
   267 lemma eq_add_iff1:
   268   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   269 by (simp add: algebra_simps)
   270 
   271 lemma eq_add_iff2:
   272   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   273 by (simp add: algebra_simps)
   274 
   275 end
   276 
   277 lemmas ring_distribs =
   278   distrib_left distrib_right left_diff_distrib right_diff_distrib
   279 
   280 class comm_ring = comm_semiring + ab_group_add
   281 begin
   282 
   283 subclass ring ..
   284 subclass comm_semiring_0_cancel ..
   285 
   286 lemma square_diff_square_factored:
   287   "x * x - y * y = (x + y) * (x - y)"
   288   by (simp add: algebra_simps)
   289 
   290 end
   291 
   292 class ring_1 = ring + zero_neq_one + monoid_mult
   293 begin
   294 
   295 subclass semiring_1_cancel ..
   296 
   297 lemma square_diff_one_factored:
   298   "x * x - 1 = (x + 1) * (x - 1)"
   299   by (simp add: algebra_simps)
   300 
   301 end
   302 
   303 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   304   (*previously ring*)
   305 begin
   306 
   307 subclass ring_1 ..
   308 subclass comm_semiring_1_cancel ..
   309 
   310 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   311 proof
   312   assume "x dvd - y"
   313   then have "x dvd - 1 * - y" by (rule dvd_mult)
   314   then show "x dvd y" by simp
   315 next
   316   assume "x dvd y"
   317   then have "x dvd - 1 * y" by (rule dvd_mult)
   318   then show "x dvd - y" by simp
   319 qed
   320 
   321 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   322 proof
   323   assume "- x dvd y"
   324   then obtain k where "y = - x * k" ..
   325   then have "y = x * - k" by simp
   326   then show "x dvd y" ..
   327 next
   328   assume "x dvd y"
   329   then obtain k where "y = x * k" ..
   330   then have "y = - x * - k" by simp
   331   then show "- x dvd y" ..
   332 qed
   333 
   334 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   335 by (simp only: diff_minus dvd_add dvd_minus_iff)
   336 
   337 end
   338 
   339 class ring_no_zero_divisors = ring + no_zero_divisors
   340 begin
   341 
   342 lemma mult_eq_0_iff [simp]:
   343   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   344 proof (cases "a = 0 \<or> b = 0")
   345   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   346     then show ?thesis using no_zero_divisors by simp
   347 next
   348   case True then show ?thesis by auto
   349 qed
   350 
   351 text{*Cancellation of equalities with a common factor*}
   352 lemma mult_cancel_right [simp]:
   353   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   354 proof -
   355   have "(a * c = b * c) = ((a - b) * c = 0)"
   356     by (simp add: algebra_simps)
   357   thus ?thesis by (simp add: disj_commute)
   358 qed
   359 
   360 lemma mult_cancel_left [simp]:
   361   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   362 proof -
   363   have "(c * a = c * b) = (c * (a - b) = 0)"
   364     by (simp add: algebra_simps)
   365   thus ?thesis by simp
   366 qed
   367 
   368 end
   369 
   370 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   371 begin
   372 
   373 lemma square_eq_1_iff:
   374   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
   375 proof -
   376   have "(x - 1) * (x + 1) = x * x - 1"
   377     by (simp add: algebra_simps)
   378   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
   379     by simp
   380   thus ?thesis
   381     by (simp add: eq_neg_iff_add_eq_0)
   382 qed
   383 
   384 lemma mult_cancel_right1 [simp]:
   385   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   386 by (insert mult_cancel_right [of 1 c b], force)
   387 
   388 lemma mult_cancel_right2 [simp]:
   389   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   390 by (insert mult_cancel_right [of a c 1], simp)
   391  
   392 lemma mult_cancel_left1 [simp]:
   393   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   394 by (insert mult_cancel_left [of c 1 b], force)
   395 
   396 lemma mult_cancel_left2 [simp]:
   397   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   398 by (insert mult_cancel_left [of c a 1], simp)
   399 
   400 end
   401 
   402 class idom = comm_ring_1 + no_zero_divisors
   403 begin
   404 
   405 subclass ring_1_no_zero_divisors ..
   406 
   407 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
   408 proof
   409   assume "a * a = b * b"
   410   then have "(a - b) * (a + b) = 0"
   411     by (simp add: algebra_simps)
   412   then show "a = b \<or> a = - b"
   413     by (simp add: eq_neg_iff_add_eq_0)
   414 next
   415   assume "a = b \<or> a = - b"
   416   then show "a * a = b * b" by auto
   417 qed
   418 
   419 lemma dvd_mult_cancel_right [simp]:
   420   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   421 proof -
   422   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   423     unfolding dvd_def by (simp add: mult_ac)
   424   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   425     unfolding dvd_def by simp
   426   finally show ?thesis .
   427 qed
   428 
   429 lemma dvd_mult_cancel_left [simp]:
   430   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   431 proof -
   432   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   433     unfolding dvd_def by (simp add: mult_ac)
   434   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   435     unfolding dvd_def by simp
   436   finally show ?thesis .
   437 qed
   438 
   439 end
   440 
   441 text {*
   442   The theory of partially ordered rings is taken from the books:
   443   \begin{itemize}
   444   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   445   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   446   \end{itemize}
   447   Most of the used notions can also be looked up in 
   448   \begin{itemize}
   449   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   450   \item \emph{Algebra I} by van der Waerden, Springer.
   451   \end{itemize}
   452 *}
   453 
   454 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   455   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   456   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   457 begin
   458 
   459 lemma mult_mono:
   460   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   461 apply (erule mult_right_mono [THEN order_trans], assumption)
   462 apply (erule mult_left_mono, assumption)
   463 done
   464 
   465 lemma mult_mono':
   466   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
   467 apply (rule mult_mono)
   468 apply (fast intro: order_trans)+
   469 done
   470 
   471 end
   472 
   473 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
   474 begin
   475 
   476 subclass semiring_0_cancel ..
   477 
   478 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   479 using mult_left_mono [of 0 b a] by simp
   480 
   481 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   482 using mult_left_mono [of b 0 a] by simp
   483 
   484 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
   485 using mult_right_mono [of a 0 b] by simp
   486 
   487 text {* Legacy - use @{text mult_nonpos_nonneg} *}
   488 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   489 by (drule mult_right_mono [of b 0], auto)
   490 
   491 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   492 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   493 
   494 end
   495 
   496 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
   497 begin
   498 
   499 subclass ordered_cancel_semiring ..
   500 
   501 subclass ordered_comm_monoid_add ..
   502 
   503 lemma mult_left_less_imp_less:
   504   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   505 by (force simp add: mult_left_mono not_le [symmetric])
   506  
   507 lemma mult_right_less_imp_less:
   508   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   509 by (force simp add: mult_right_mono not_le [symmetric])
   510 
   511 end
   512 
   513 class linordered_semiring_1 = linordered_semiring + semiring_1
   514 begin
   515 
   516 lemma convex_bound_le:
   517   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   518   shows "u * x + v * y \<le> a"
   519 proof-
   520   from assms have "u * x + v * y \<le> u * a + v * a"
   521     by (simp add: add_mono mult_left_mono)
   522   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
   523 qed
   524 
   525 end
   526 
   527 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   528   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   529   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   530 begin
   531 
   532 subclass semiring_0_cancel ..
   533 
   534 subclass linordered_semiring
   535 proof
   536   fix a b c :: 'a
   537   assume A: "a \<le> b" "0 \<le> c"
   538   from A show "c * a \<le> c * b"
   539     unfolding le_less
   540     using mult_strict_left_mono by (cases "c = 0") auto
   541   from A show "a * c \<le> b * c"
   542     unfolding le_less
   543     using mult_strict_right_mono by (cases "c = 0") auto
   544 qed
   545 
   546 lemma mult_left_le_imp_le:
   547   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   548 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   549  
   550 lemma mult_right_le_imp_le:
   551   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   552 by (force simp add: mult_strict_right_mono not_less [symmetric])
   553 
   554 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   555 using mult_strict_left_mono [of 0 b a] by simp
   556 
   557 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   558 using mult_strict_left_mono [of b 0 a] by simp
   559 
   560 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
   561 using mult_strict_right_mono [of a 0 b] by simp
   562 
   563 text {* Legacy - use @{text mult_neg_pos} *}
   564 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   565 by (drule mult_strict_right_mono [of b 0], auto)
   566 
   567 lemma zero_less_mult_pos:
   568   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   569 apply (cases "b\<le>0")
   570  apply (auto simp add: le_less not_less)
   571 apply (drule_tac mult_pos_neg [of a b])
   572  apply (auto dest: less_not_sym)
   573 done
   574 
   575 lemma zero_less_mult_pos2:
   576   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   577 apply (cases "b\<le>0")
   578  apply (auto simp add: le_less not_less)
   579 apply (drule_tac mult_pos_neg2 [of a b])
   580  apply (auto dest: less_not_sym)
   581 done
   582 
   583 text{*Strict monotonicity in both arguments*}
   584 lemma mult_strict_mono:
   585   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   586   shows "a * c < b * d"
   587   using assms apply (cases "c=0")
   588   apply (simp add: mult_pos_pos)
   589   apply (erule mult_strict_right_mono [THEN less_trans])
   590   apply (force simp add: le_less)
   591   apply (erule mult_strict_left_mono, assumption)
   592   done
   593 
   594 text{*This weaker variant has more natural premises*}
   595 lemma mult_strict_mono':
   596   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   597   shows "a * c < b * d"
   598 by (rule mult_strict_mono) (insert assms, auto)
   599 
   600 lemma mult_less_le_imp_less:
   601   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   602   shows "a * c < b * d"
   603   using assms apply (subgoal_tac "a * c < b * c")
   604   apply (erule less_le_trans)
   605   apply (erule mult_left_mono)
   606   apply simp
   607   apply (erule mult_strict_right_mono)
   608   apply assumption
   609   done
   610 
   611 lemma mult_le_less_imp_less:
   612   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   613   shows "a * c < b * d"
   614   using assms apply (subgoal_tac "a * c \<le> b * c")
   615   apply (erule le_less_trans)
   616   apply (erule mult_strict_left_mono)
   617   apply simp
   618   apply (erule mult_right_mono)
   619   apply simp
   620   done
   621 
   622 lemma mult_less_imp_less_left:
   623   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   624   shows "a < b"
   625 proof (rule ccontr)
   626   assume "\<not>  a < b"
   627   hence "b \<le> a" by (simp add: linorder_not_less)
   628   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   629   with this and less show False by (simp add: not_less [symmetric])
   630 qed
   631 
   632 lemma mult_less_imp_less_right:
   633   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   634   shows "a < b"
   635 proof (rule ccontr)
   636   assume "\<not> a < b"
   637   hence "b \<le> a" by (simp add: linorder_not_less)
   638   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   639   with this and less show False by (simp add: not_less [symmetric])
   640 qed  
   641 
   642 end
   643 
   644 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
   645 begin
   646 
   647 subclass linordered_semiring_1 ..
   648 
   649 lemma convex_bound_lt:
   650   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"
   651   shows "u * x + v * y < a"
   652 proof -
   653   from assms have "u * x + v * y < u * a + v * a"
   654     by (cases "u = 0")
   655        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
   656   thus ?thesis using assms unfolding distrib_right[symmetric] by simp
   657 qed
   658 
   659 end
   660 
   661 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
   662   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   663 begin
   664 
   665 subclass ordered_semiring
   666 proof
   667   fix a b c :: 'a
   668   assume "a \<le> b" "0 \<le> c"
   669   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
   670   thus "a * c \<le> b * c" by (simp only: mult_commute)
   671 qed
   672 
   673 end
   674 
   675 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
   676 begin
   677 
   678 subclass comm_semiring_0_cancel ..
   679 subclass ordered_comm_semiring ..
   680 subclass ordered_cancel_semiring ..
   681 
   682 end
   683 
   684 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
   685   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   686 begin
   687 
   688 subclass linordered_semiring_strict
   689 proof
   690   fix a b c :: 'a
   691   assume "a < b" "0 < c"
   692   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
   693   thus "a * c < b * c" by (simp only: mult_commute)
   694 qed
   695 
   696 subclass ordered_cancel_comm_semiring
   697 proof
   698   fix a b c :: 'a
   699   assume "a \<le> b" "0 \<le> c"
   700   thus "c * a \<le> c * b"
   701     unfolding le_less
   702     using mult_strict_left_mono by (cases "c = 0") auto
   703 qed
   704 
   705 end
   706 
   707 class ordered_ring = ring + ordered_cancel_semiring 
   708 begin
   709 
   710 subclass ordered_ab_group_add ..
   711 
   712 lemma less_add_iff1:
   713   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   714 by (simp add: algebra_simps)
   715 
   716 lemma less_add_iff2:
   717   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   718 by (simp add: algebra_simps)
   719 
   720 lemma le_add_iff1:
   721   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   722 by (simp add: algebra_simps)
   723 
   724 lemma le_add_iff2:
   725   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   726 by (simp add: algebra_simps)
   727 
   728 lemma mult_left_mono_neg:
   729   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   730   apply (drule mult_left_mono [of _ _ "- c"])
   731   apply simp_all
   732   done
   733 
   734 lemma mult_right_mono_neg:
   735   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   736   apply (drule mult_right_mono [of _ _ "- c"])
   737   apply simp_all
   738   done
   739 
   740 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   741 using mult_right_mono_neg [of a 0 b] by simp
   742 
   743 lemma split_mult_pos_le:
   744   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   745 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   746 
   747 end
   748 
   749 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   750 begin
   751 
   752 subclass ordered_ring ..
   753 
   754 subclass ordered_ab_group_add_abs
   755 proof
   756   fix a b
   757   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   758     by (auto simp add: abs_if not_less)
   759     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   760      auto intro!: less_imp_le add_neg_neg)
   761 qed (auto simp add: abs_if)
   762 
   763 lemma zero_le_square [simp]: "0 \<le> a * a"
   764   using linear [of 0 a]
   765   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   766 
   767 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   768   by (simp add: not_less)
   769 
   770 end
   771 
   772 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
   773    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
   774  *)
   775 class linordered_ring_strict = ring + linordered_semiring_strict
   776   + ordered_ab_group_add + abs_if
   777 begin
   778 
   779 subclass linordered_ring ..
   780 
   781 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   782 using mult_strict_left_mono [of b a "- c"] by simp
   783 
   784 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   785 using mult_strict_right_mono [of b a "- c"] by simp
   786 
   787 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   788 using mult_strict_right_mono_neg [of a 0 b] by simp
   789 
   790 subclass ring_no_zero_divisors
   791 proof
   792   fix a b
   793   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   794   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   795   have "a * b < 0 \<or> 0 < a * b"
   796   proof (cases "a < 0")
   797     case True note A' = this
   798     show ?thesis proof (cases "b < 0")
   799       case True with A'
   800       show ?thesis by (auto dest: mult_neg_neg)
   801     next
   802       case False with B have "0 < b" by auto
   803       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   804     qed
   805   next
   806     case False with A have A': "0 < a" by auto
   807     show ?thesis proof (cases "b < 0")
   808       case True with A'
   809       show ?thesis by (auto dest: mult_strict_right_mono_neg)
   810     next
   811       case False with B have "0 < b" by auto
   812       with A' show ?thesis by (auto dest: mult_pos_pos)
   813     qed
   814   qed
   815   then show "a * b \<noteq> 0" by (simp add: neq_iff)
   816 qed
   817 
   818 lemma zero_less_mult_iff:
   819   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   820   apply (auto simp add: mult_pos_pos mult_neg_neg)
   821   apply (simp_all add: not_less le_less)
   822   apply (erule disjE) apply assumption defer
   823   apply (erule disjE) defer apply (drule sym) apply simp
   824   apply (erule disjE) defer apply (drule sym) apply simp
   825   apply (erule disjE) apply assumption apply (drule sym) apply simp
   826   apply (drule sym) apply simp
   827   apply (blast dest: zero_less_mult_pos)
   828   apply (blast dest: zero_less_mult_pos2)
   829   done
   830 
   831 lemma zero_le_mult_iff:
   832   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   833 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
   834 
   835 lemma mult_less_0_iff:
   836   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   837   apply (insert zero_less_mult_iff [of "-a" b])
   838   apply force
   839   done
   840 
   841 lemma mult_le_0_iff:
   842   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   843   apply (insert zero_le_mult_iff [of "-a" b]) 
   844   apply force
   845   done
   846 
   847 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   848    also with the relations @{text "\<le>"} and equality.*}
   849 
   850 text{*These ``disjunction'' versions produce two cases when the comparison is
   851  an assumption, but effectively four when the comparison is a goal.*}
   852 
   853 lemma mult_less_cancel_right_disj:
   854   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   855   apply (cases "c = 0")
   856   apply (auto simp add: neq_iff mult_strict_right_mono 
   857                       mult_strict_right_mono_neg)
   858   apply (auto simp add: not_less 
   859                       not_le [symmetric, of "a*c"]
   860                       not_le [symmetric, of a])
   861   apply (erule_tac [!] notE)
   862   apply (auto simp add: less_imp_le mult_right_mono 
   863                       mult_right_mono_neg)
   864   done
   865 
   866 lemma mult_less_cancel_left_disj:
   867   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   868   apply (cases "c = 0")
   869   apply (auto simp add: neq_iff mult_strict_left_mono 
   870                       mult_strict_left_mono_neg)
   871   apply (auto simp add: not_less 
   872                       not_le [symmetric, of "c*a"]
   873                       not_le [symmetric, of a])
   874   apply (erule_tac [!] notE)
   875   apply (auto simp add: less_imp_le mult_left_mono 
   876                       mult_left_mono_neg)
   877   done
   878 
   879 text{*The ``conjunction of implication'' lemmas produce two cases when the
   880 comparison is a goal, but give four when the comparison is an assumption.*}
   881 
   882 lemma mult_less_cancel_right:
   883   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   884   using mult_less_cancel_right_disj [of a c b] by auto
   885 
   886 lemma mult_less_cancel_left:
   887   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   888   using mult_less_cancel_left_disj [of c a b] by auto
   889 
   890 lemma mult_le_cancel_right:
   891    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   892 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
   893 
   894 lemma mult_le_cancel_left:
   895   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   896 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
   897 
   898 lemma mult_le_cancel_left_pos:
   899   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
   900 by (auto simp: mult_le_cancel_left)
   901 
   902 lemma mult_le_cancel_left_neg:
   903   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
   904 by (auto simp: mult_le_cancel_left)
   905 
   906 lemma mult_less_cancel_left_pos:
   907   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
   908 by (auto simp: mult_less_cancel_left)
   909 
   910 lemma mult_less_cancel_left_neg:
   911   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
   912 by (auto simp: mult_less_cancel_left)
   913 
   914 end
   915 
   916 lemmas mult_sign_intros =
   917   mult_nonneg_nonneg mult_nonneg_nonpos
   918   mult_nonpos_nonneg mult_nonpos_nonpos
   919   mult_pos_pos mult_pos_neg
   920   mult_neg_pos mult_neg_neg
   921 
   922 class ordered_comm_ring = comm_ring + ordered_comm_semiring
   923 begin
   924 
   925 subclass ordered_ring ..
   926 subclass ordered_cancel_comm_semiring ..
   927 
   928 end
   929 
   930 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
   931   (*previously linordered_semiring*)
   932   assumes zero_less_one [simp]: "0 < 1"
   933 begin
   934 
   935 lemma pos_add_strict:
   936   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   937   using add_strict_mono [of 0 a b c] by simp
   938 
   939 lemma zero_le_one [simp]: "0 \<le> 1"
   940 by (rule zero_less_one [THEN less_imp_le]) 
   941 
   942 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   943 by (simp add: not_le) 
   944 
   945 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
   946 by (simp add: not_less) 
   947 
   948 lemma less_1_mult:
   949   assumes "1 < m" and "1 < n"
   950   shows "1 < m * n"
   951   using assms mult_strict_mono [of 1 m 1 n]
   952     by (simp add:  less_trans [OF zero_less_one]) 
   953 
   954 end
   955 
   956 class linordered_idom = comm_ring_1 +
   957   linordered_comm_semiring_strict + ordered_ab_group_add +
   958   abs_if + sgn_if
   959   (*previously linordered_ring*)
   960 begin
   961 
   962 subclass linordered_semiring_1_strict ..
   963 subclass linordered_ring_strict ..
   964 subclass ordered_comm_ring ..
   965 subclass idom ..
   966 
   967 subclass linordered_semidom
   968 proof
   969   have "0 \<le> 1 * 1" by (rule zero_le_square)
   970   thus "0 < 1" by (simp add: le_less)
   971 qed 
   972 
   973 lemma linorder_neqE_linordered_idom:
   974   assumes "x \<noteq> y" obtains "x < y" | "y < x"
   975   using assms by (rule neqE)
   976 
   977 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
   978 
   979 lemma mult_le_cancel_right1:
   980   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
   981 by (insert mult_le_cancel_right [of 1 c b], simp)
   982 
   983 lemma mult_le_cancel_right2:
   984   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
   985 by (insert mult_le_cancel_right [of a c 1], simp)
   986 
   987 lemma mult_le_cancel_left1:
   988   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
   989 by (insert mult_le_cancel_left [of c 1 b], simp)
   990 
   991 lemma mult_le_cancel_left2:
   992   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
   993 by (insert mult_le_cancel_left [of c a 1], simp)
   994 
   995 lemma mult_less_cancel_right1:
   996   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
   997 by (insert mult_less_cancel_right [of 1 c b], simp)
   998 
   999 lemma mult_less_cancel_right2:
  1000   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1001 by (insert mult_less_cancel_right [of a c 1], simp)
  1002 
  1003 lemma mult_less_cancel_left1:
  1004   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1005 by (insert mult_less_cancel_left [of c 1 b], simp)
  1006 
  1007 lemma mult_less_cancel_left2:
  1008   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1009 by (insert mult_less_cancel_left [of c a 1], simp)
  1010 
  1011 lemma sgn_sgn [simp]:
  1012   "sgn (sgn a) = sgn a"
  1013 unfolding sgn_if by simp
  1014 
  1015 lemma sgn_0_0:
  1016   "sgn a = 0 \<longleftrightarrow> a = 0"
  1017 unfolding sgn_if by simp
  1018 
  1019 lemma sgn_1_pos:
  1020   "sgn a = 1 \<longleftrightarrow> a > 0"
  1021 unfolding sgn_if by simp
  1022 
  1023 lemma sgn_1_neg:
  1024   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1025 unfolding sgn_if by auto
  1026 
  1027 lemma sgn_pos [simp]:
  1028   "0 < a \<Longrightarrow> sgn a = 1"
  1029 unfolding sgn_1_pos .
  1030 
  1031 lemma sgn_neg [simp]:
  1032   "a < 0 \<Longrightarrow> sgn a = - 1"
  1033 unfolding sgn_1_neg .
  1034 
  1035 lemma sgn_times:
  1036   "sgn (a * b) = sgn a * sgn b"
  1037 by (auto simp add: sgn_if zero_less_mult_iff)
  1038 
  1039 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  1040 unfolding sgn_if abs_if by auto
  1041 
  1042 lemma sgn_greater [simp]:
  1043   "0 < sgn a \<longleftrightarrow> 0 < a"
  1044   unfolding sgn_if by auto
  1045 
  1046 lemma sgn_less [simp]:
  1047   "sgn a < 0 \<longleftrightarrow> a < 0"
  1048   unfolding sgn_if by auto
  1049 
  1050 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1051   by (simp add: abs_if)
  1052 
  1053 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  1054   by (simp add: abs_if)
  1055 
  1056 lemma dvd_if_abs_eq:
  1057   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  1058 by(subst abs_dvd_iff[symmetric]) simp
  1059 
  1060 end
  1061 
  1062 text {* Simprules for comparisons where common factors can be cancelled. *}
  1063 
  1064 lemmas mult_compare_simps =
  1065     mult_le_cancel_right mult_le_cancel_left
  1066     mult_le_cancel_right1 mult_le_cancel_right2
  1067     mult_le_cancel_left1 mult_le_cancel_left2
  1068     mult_less_cancel_right mult_less_cancel_left
  1069     mult_less_cancel_right1 mult_less_cancel_right2
  1070     mult_less_cancel_left1 mult_less_cancel_left2
  1071     mult_cancel_right mult_cancel_left
  1072     mult_cancel_right1 mult_cancel_right2
  1073     mult_cancel_left1 mult_cancel_left2
  1074 
  1075 text {* Reasoning about inequalities with division *}
  1076 
  1077 context linordered_semidom
  1078 begin
  1079 
  1080 lemma less_add_one: "a < a + 1"
  1081 proof -
  1082   have "a + 0 < a + 1"
  1083     by (blast intro: zero_less_one add_strict_left_mono)
  1084   thus ?thesis by simp
  1085 qed
  1086 
  1087 lemma zero_less_two: "0 < 1 + 1"
  1088 by (blast intro: less_trans zero_less_one less_add_one)
  1089 
  1090 end
  1091 
  1092 context linordered_idom
  1093 begin
  1094 
  1095 lemma mult_right_le_one_le:
  1096   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  1097   by (auto simp add: mult_le_cancel_left2)
  1098 
  1099 lemma mult_left_le_one_le:
  1100   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  1101   by (auto simp add: mult_le_cancel_right2)
  1102 
  1103 end
  1104 
  1105 text {* Absolute Value *}
  1106 
  1107 context linordered_idom
  1108 begin
  1109 
  1110 lemma mult_sgn_abs:
  1111   "sgn x * \<bar>x\<bar> = x"
  1112   unfolding abs_if sgn_if by auto
  1113 
  1114 lemma abs_one [simp]:
  1115   "\<bar>1\<bar> = 1"
  1116   by (simp add: abs_if)
  1117 
  1118 end
  1119 
  1120 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1121   assumes abs_eq_mult:
  1122     "(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>"
  1123 
  1124 context linordered_idom
  1125 begin
  1126 
  1127 subclass ordered_ring_abs proof
  1128 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1129 
  1130 lemma abs_mult:
  1131   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
  1132   by (rule abs_eq_mult) auto
  1133 
  1134 lemma abs_mult_self:
  1135   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  1136   by (simp add: abs_if) 
  1137 
  1138 lemma abs_mult_less:
  1139   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  1140 proof -
  1141   assume ac: "\<bar>a\<bar> < c"
  1142   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  1143   assume "\<bar>b\<bar> < d"
  1144   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1145 qed
  1146 
  1147 lemma less_minus_self_iff:
  1148   "a < - a \<longleftrightarrow> a < 0"
  1149   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
  1150 
  1151 lemma abs_less_iff:
  1152   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
  1153   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  1154 
  1155 lemma abs_mult_pos:
  1156   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  1157   by (simp add: abs_mult)
  1158 
  1159 lemma abs_diff_less_iff:
  1160   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
  1161   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
  1162 
  1163 end
  1164 
  1165 code_identifier
  1166   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1167 
  1168 end
  1169