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