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