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