src/HOL/Rings.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35097 4554bb2abfa3
child 35216 7641e8d831d2
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 inverse =
   414   fixes inverse :: "'a \<Rightarrow> 'a"
   415     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
   416 
   417 class division_ring = ring_1 + inverse +
   418   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   419   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   420   assumes divide_inverse: "a / b = a * inverse b"
   421 begin
   422 
   423 subclass ring_1_no_zero_divisors
   424 proof
   425   fix a b :: 'a
   426   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   427   show "a * b \<noteq> 0"
   428   proof
   429     assume ab: "a * b = 0"
   430     hence "0 = inverse a * (a * b) * inverse b" by simp
   431     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   432       by (simp only: mult_assoc)
   433     also have "\<dots> = 1" using a b by simp
   434     finally show False by simp
   435   qed
   436 qed
   437 
   438 lemma nonzero_imp_inverse_nonzero:
   439   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   440 proof
   441   assume ianz: "inverse a = 0"
   442   assume "a \<noteq> 0"
   443   hence "1 = a * inverse a" by simp
   444   also have "... = 0" by (simp add: ianz)
   445   finally have "1 = 0" .
   446   thus False by (simp add: eq_commute)
   447 qed
   448 
   449 lemma inverse_zero_imp_zero:
   450   "inverse a = 0 \<Longrightarrow> a = 0"
   451 apply (rule classical)
   452 apply (drule nonzero_imp_inverse_nonzero)
   453 apply auto
   454 done
   455 
   456 lemma inverse_unique: 
   457   assumes ab: "a * b = 1"
   458   shows "inverse a = b"
   459 proof -
   460   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   461   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
   462   ultimately show ?thesis by (simp add: mult_assoc [symmetric])
   463 qed
   464 
   465 lemma nonzero_inverse_minus_eq:
   466   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
   467 by (rule inverse_unique) simp
   468 
   469 lemma nonzero_inverse_inverse_eq:
   470   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
   471 by (rule inverse_unique) simp
   472 
   473 lemma nonzero_inverse_eq_imp_eq:
   474   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
   475   shows "a = b"
   476 proof -
   477   from `inverse a = inverse b`
   478   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
   479   with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
   480     by (simp add: nonzero_inverse_inverse_eq)
   481 qed
   482 
   483 lemma inverse_1 [simp]: "inverse 1 = 1"
   484 by (rule inverse_unique) simp
   485 
   486 lemma nonzero_inverse_mult_distrib: 
   487   assumes "a \<noteq> 0" and "b \<noteq> 0"
   488   shows "inverse (a * b) = inverse b * inverse a"
   489 proof -
   490   have "a * (b * inverse b) * inverse a = 1" using assms by simp
   491   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
   492   thus ?thesis by (rule inverse_unique)
   493 qed
   494 
   495 lemma division_ring_inverse_add:
   496   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   497 by (simp add: algebra_simps)
   498 
   499 lemma division_ring_inverse_diff:
   500   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   501 by (simp add: algebra_simps)
   502 
   503 end
   504 
   505 class mult_mono = times + zero + ord +
   506   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   507   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   508 
   509 class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
   510 begin
   511 
   512 lemma mult_mono:
   513   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   514      \<Longrightarrow> a * c \<le> b * d"
   515 apply (erule mult_right_mono [THEN order_trans], assumption)
   516 apply (erule mult_left_mono, assumption)
   517 done
   518 
   519 lemma mult_mono':
   520   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   521      \<Longrightarrow> a * c \<le> b * d"
   522 apply (rule mult_mono)
   523 apply (fast intro: order_trans)+
   524 done
   525 
   526 end
   527 
   528 class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
   529   + semiring + cancel_comm_monoid_add
   530 begin
   531 
   532 subclass semiring_0_cancel ..
   533 subclass ordered_semiring ..
   534 
   535 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   536 using mult_left_mono [of zero b a] by simp
   537 
   538 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   539 using mult_left_mono [of b zero a] by simp
   540 
   541 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
   542 using mult_right_mono [of a zero b] by simp
   543 
   544 text {* Legacy - use @{text mult_nonpos_nonneg} *}
   545 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   546 by (drule mult_right_mono [of b zero], auto)
   547 
   548 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   549 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   550 
   551 end
   552 
   553 class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
   554 begin
   555 
   556 subclass ordered_cancel_semiring ..
   557 
   558 subclass ordered_comm_monoid_add ..
   559 
   560 lemma mult_left_less_imp_less:
   561   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   562 by (force simp add: mult_left_mono not_le [symmetric])
   563  
   564 lemma mult_right_less_imp_less:
   565   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   566 by (force simp add: mult_right_mono not_le [symmetric])
   567 
   568 end
   569 
   570 class linordered_semiring_1 = linordered_semiring + semiring_1
   571 
   572 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   573   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   574   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   575 begin
   576 
   577 subclass semiring_0_cancel ..
   578 
   579 subclass linordered_semiring
   580 proof
   581   fix a b c :: 'a
   582   assume A: "a \<le> b" "0 \<le> c"
   583   from A show "c * a \<le> c * b"
   584     unfolding le_less
   585     using mult_strict_left_mono by (cases "c = 0") auto
   586   from A show "a * c \<le> b * c"
   587     unfolding le_less
   588     using mult_strict_right_mono by (cases "c = 0") auto
   589 qed
   590 
   591 lemma mult_left_le_imp_le:
   592   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   593 by (force simp add: mult_strict_left_mono _not_less [symmetric])
   594  
   595 lemma mult_right_le_imp_le:
   596   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   597 by (force simp add: mult_strict_right_mono not_less [symmetric])
   598 
   599 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   600 using mult_strict_left_mono [of zero b a] by simp
   601 
   602 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   603 using mult_strict_left_mono [of b zero a] by simp
   604 
   605 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
   606 using mult_strict_right_mono [of a zero b] by simp
   607 
   608 text {* Legacy - use @{text mult_neg_pos} *}
   609 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   610 by (drule mult_strict_right_mono [of b zero], auto)
   611 
   612 lemma zero_less_mult_pos:
   613   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   614 apply (cases "b\<le>0")
   615  apply (auto simp add: le_less not_less)
   616 apply (drule_tac mult_pos_neg [of a b])
   617  apply (auto dest: less_not_sym)
   618 done
   619 
   620 lemma zero_less_mult_pos2:
   621   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   622 apply (cases "b\<le>0")
   623  apply (auto simp add: le_less not_less)
   624 apply (drule_tac mult_pos_neg2 [of a b])
   625  apply (auto dest: less_not_sym)
   626 done
   627 
   628 text{*Strict monotonicity in both arguments*}
   629 lemma mult_strict_mono:
   630   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   631   shows "a * c < b * d"
   632   using assms apply (cases "c=0")
   633   apply (simp add: mult_pos_pos)
   634   apply (erule mult_strict_right_mono [THEN less_trans])
   635   apply (force simp add: le_less)
   636   apply (erule mult_strict_left_mono, assumption)
   637   done
   638 
   639 text{*This weaker variant has more natural premises*}
   640 lemma mult_strict_mono':
   641   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
   642   shows "a * c < b * d"
   643 by (rule mult_strict_mono) (insert assms, auto)
   644 
   645 lemma mult_less_le_imp_less:
   646   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   647   shows "a * c < b * d"
   648   using assms apply (subgoal_tac "a * c < b * c")
   649   apply (erule less_le_trans)
   650   apply (erule mult_left_mono)
   651   apply simp
   652   apply (erule mult_strict_right_mono)
   653   apply assumption
   654   done
   655 
   656 lemma mult_le_less_imp_less:
   657   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   658   shows "a * c < b * d"
   659   using assms apply (subgoal_tac "a * c \<le> b * c")
   660   apply (erule le_less_trans)
   661   apply (erule mult_strict_left_mono)
   662   apply simp
   663   apply (erule mult_right_mono)
   664   apply simp
   665   done
   666 
   667 lemma mult_less_imp_less_left:
   668   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
   669   shows "a < b"
   670 proof (rule ccontr)
   671   assume "\<not>  a < b"
   672   hence "b \<le> a" by (simp add: linorder_not_less)
   673   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
   674   with this and less show False by (simp add: not_less [symmetric])
   675 qed
   676 
   677 lemma mult_less_imp_less_right:
   678   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   679   shows "a < b"
   680 proof (rule ccontr)
   681   assume "\<not> a < b"
   682   hence "b \<le> a" by (simp add: linorder_not_less)
   683   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
   684   with this and less show False by (simp add: not_less [symmetric])
   685 qed  
   686 
   687 end
   688 
   689 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
   690 
   691 class mult_mono1 = times + zero + ord +
   692   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   693 
   694 class ordered_comm_semiring = comm_semiring_0
   695   + ordered_ab_semigroup_add + mult_mono1
   696 begin
   697 
   698 subclass ordered_semiring
   699 proof
   700   fix a b c :: 'a
   701   assume "a \<le> b" "0 \<le> c"
   702   thus "c * a \<le> c * b" by (rule mult_mono1)
   703   thus "a * c \<le> b * c" by (simp only: mult_commute)
   704 qed
   705 
   706 end
   707 
   708 class ordered_cancel_comm_semiring = comm_semiring_0_cancel
   709   + ordered_ab_semigroup_add + mult_mono1
   710 begin
   711 
   712 subclass ordered_comm_semiring ..
   713 subclass ordered_cancel_semiring ..
   714 
   715 end
   716 
   717 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
   718   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   719 begin
   720 
   721 subclass linordered_semiring_strict
   722 proof
   723   fix a b c :: 'a
   724   assume "a < b" "0 < c"
   725   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   726   thus "a * c < b * c" by (simp only: mult_commute)
   727 qed
   728 
   729 subclass ordered_cancel_comm_semiring
   730 proof
   731   fix a b c :: 'a
   732   assume "a \<le> b" "0 \<le> c"
   733   thus "c * a \<le> c * b"
   734     unfolding le_less
   735     using mult_strict_left_mono by (cases "c = 0") auto
   736 qed
   737 
   738 end
   739 
   740 class ordered_ring = ring + ordered_cancel_semiring 
   741 begin
   742 
   743 subclass ordered_ab_group_add ..
   744 
   745 text{*Legacy - use @{text algebra_simps} *}
   746 lemmas ring_simps[noatp] = algebra_simps
   747 
   748 lemma less_add_iff1:
   749   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   750 by (simp add: algebra_simps)
   751 
   752 lemma less_add_iff2:
   753   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   754 by (simp add: algebra_simps)
   755 
   756 lemma le_add_iff1:
   757   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   758 by (simp add: algebra_simps)
   759 
   760 lemma le_add_iff2:
   761   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   762 by (simp add: algebra_simps)
   763 
   764 lemma mult_left_mono_neg:
   765   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   766   apply (drule mult_left_mono [of _ _ "uminus c"])
   767   apply (simp_all add: minus_mult_left [symmetric]) 
   768   done
   769 
   770 lemma mult_right_mono_neg:
   771   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   772   apply (drule mult_right_mono [of _ _ "uminus c"])
   773   apply (simp_all add: minus_mult_right [symmetric]) 
   774   done
   775 
   776 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   777 using mult_right_mono_neg [of a zero b] by simp
   778 
   779 lemma split_mult_pos_le:
   780   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   781 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   782 
   783 end
   784 
   785 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   786 begin
   787 
   788 subclass ordered_ring ..
   789 
   790 subclass ordered_ab_group_add_abs
   791 proof
   792   fix a b
   793   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   794     by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   795     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
   796      neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
   797       auto intro!: less_imp_le add_neg_neg)
   798 qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
   799 
   800 end
   801 
   802 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
   803    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
   804  *)
   805 class linordered_ring_strict = ring + linordered_semiring_strict
   806   + ordered_ab_group_add + abs_if
   807 begin
   808 
   809 subclass linordered_ring ..
   810 
   811 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   812 using mult_strict_left_mono [of b a "- c"] by simp
   813 
   814 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   815 using mult_strict_right_mono [of b a "- c"] by simp
   816 
   817 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   818 using mult_strict_right_mono_neg [of a zero b] by simp
   819 
   820 subclass ring_no_zero_divisors
   821 proof
   822   fix a b
   823   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   824   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   825   have "a * b < 0 \<or> 0 < a * b"
   826   proof (cases "a < 0")
   827     case True note A' = this
   828     show ?thesis proof (cases "b < 0")
   829       case True with A'
   830       show ?thesis by (auto dest: mult_neg_neg)
   831     next
   832       case False with B have "0 < b" by auto
   833       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   834     qed
   835   next
   836     case False with A have A': "0 < a" by auto
   837     show ?thesis proof (cases "b < 0")
   838       case True with A'
   839       show ?thesis by (auto dest: mult_strict_right_mono_neg)
   840     next
   841       case False with B have "0 < b" by auto
   842       with A' show ?thesis by (auto dest: mult_pos_pos)
   843     qed
   844   qed
   845   then show "a * b \<noteq> 0" by (simp add: neq_iff)
   846 qed
   847 
   848 lemma zero_less_mult_iff:
   849   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   850   apply (auto simp add: mult_pos_pos mult_neg_neg)
   851   apply (simp_all add: not_less le_less)
   852   apply (erule disjE) apply assumption defer
   853   apply (erule disjE) defer apply (drule sym) apply simp
   854   apply (erule disjE) defer apply (drule sym) apply simp
   855   apply (erule disjE) apply assumption apply (drule sym) apply simp
   856   apply (drule sym) apply simp
   857   apply (blast dest: zero_less_mult_pos)
   858   apply (blast dest: zero_less_mult_pos2)
   859   done
   860 
   861 lemma zero_le_mult_iff:
   862   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   863 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
   864 
   865 lemma mult_less_0_iff:
   866   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   867   apply (insert zero_less_mult_iff [of "-a" b]) 
   868   apply (force simp add: minus_mult_left[symmetric]) 
   869   done
   870 
   871 lemma mult_le_0_iff:
   872   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   873   apply (insert zero_le_mult_iff [of "-a" b]) 
   874   apply (force simp add: minus_mult_left[symmetric]) 
   875   done
   876 
   877 lemma zero_le_square [simp]: "0 \<le> a * a"
   878 by (simp add: zero_le_mult_iff linear)
   879 
   880 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   881 by (simp add: not_less)
   882 
   883 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   884    also with the relations @{text "\<le>"} and equality.*}
   885 
   886 text{*These ``disjunction'' versions produce two cases when the comparison is
   887  an assumption, but effectively four when the comparison is a goal.*}
   888 
   889 lemma mult_less_cancel_right_disj:
   890   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   891   apply (cases "c = 0")
   892   apply (auto simp add: neq_iff mult_strict_right_mono 
   893                       mult_strict_right_mono_neg)
   894   apply (auto simp add: not_less 
   895                       not_le [symmetric, of "a*c"]
   896                       not_le [symmetric, of a])
   897   apply (erule_tac [!] notE)
   898   apply (auto simp add: less_imp_le mult_right_mono 
   899                       mult_right_mono_neg)
   900   done
   901 
   902 lemma mult_less_cancel_left_disj:
   903   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   904   apply (cases "c = 0")
   905   apply (auto simp add: neq_iff mult_strict_left_mono 
   906                       mult_strict_left_mono_neg)
   907   apply (auto simp add: not_less 
   908                       not_le [symmetric, of "c*a"]
   909                       not_le [symmetric, of a])
   910   apply (erule_tac [!] notE)
   911   apply (auto simp add: less_imp_le mult_left_mono 
   912                       mult_left_mono_neg)
   913   done
   914 
   915 text{*The ``conjunction of implication'' lemmas produce two cases when the
   916 comparison is a goal, but give four when the comparison is an assumption.*}
   917 
   918 lemma mult_less_cancel_right:
   919   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   920   using mult_less_cancel_right_disj [of a c b] by auto
   921 
   922 lemma mult_less_cancel_left:
   923   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   924   using mult_less_cancel_left_disj [of c a b] by auto
   925 
   926 lemma mult_le_cancel_right:
   927    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   928 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
   929 
   930 lemma mult_le_cancel_left:
   931   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   932 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
   933 
   934 lemma mult_le_cancel_left_pos:
   935   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
   936 by (auto simp: mult_le_cancel_left)
   937 
   938 lemma mult_le_cancel_left_neg:
   939   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
   940 by (auto simp: mult_le_cancel_left)
   941 
   942 lemma mult_less_cancel_left_pos:
   943   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
   944 by (auto simp: mult_less_cancel_left)
   945 
   946 lemma mult_less_cancel_left_neg:
   947   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
   948 by (auto simp: mult_less_cancel_left)
   949 
   950 end
   951 
   952 text{*Legacy - use @{text algebra_simps} *}
   953 lemmas ring_simps[noatp] = algebra_simps
   954 
   955 lemmas mult_sign_intros =
   956   mult_nonneg_nonneg mult_nonneg_nonpos
   957   mult_nonpos_nonneg mult_nonpos_nonpos
   958   mult_pos_pos mult_pos_neg
   959   mult_neg_pos mult_neg_neg
   960 
   961 class ordered_comm_ring = comm_ring + ordered_comm_semiring
   962 begin
   963 
   964 subclass ordered_ring ..
   965 subclass ordered_cancel_comm_semiring ..
   966 
   967 end
   968 
   969 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
   970   (*previously linordered_semiring*)
   971   assumes zero_less_one [simp]: "0 < 1"
   972 begin
   973 
   974 lemma pos_add_strict:
   975   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   976   using add_strict_mono [of zero a b c] by simp
   977 
   978 lemma zero_le_one [simp]: "0 \<le> 1"
   979 by (rule zero_less_one [THEN less_imp_le]) 
   980 
   981 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   982 by (simp add: not_le) 
   983 
   984 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
   985 by (simp add: not_less) 
   986 
   987 lemma less_1_mult:
   988   assumes "1 < m" and "1 < n"
   989   shows "1 < m * n"
   990   using assms mult_strict_mono [of 1 m 1 n]
   991     by (simp add:  less_trans [OF zero_less_one]) 
   992 
   993 end
   994 
   995 class linordered_idom = comm_ring_1 +
   996   linordered_comm_semiring_strict + ordered_ab_group_add +
   997   abs_if + sgn_if
   998   (*previously linordered_ring*)
   999 begin
  1000 
  1001 subclass linordered_ring_strict ..
  1002 subclass ordered_comm_ring ..
  1003 subclass idom ..
  1004 
  1005 subclass linordered_semidom
  1006 proof
  1007   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1008   thus "0 < 1" by (simp add: le_less)
  1009 qed 
  1010 
  1011 lemma linorder_neqE_linordered_idom:
  1012   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1013   using assms by (rule neqE)
  1014 
  1015 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1016 
  1017 lemma mult_le_cancel_right1:
  1018   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1019 by (insert mult_le_cancel_right [of 1 c b], simp)
  1020 
  1021 lemma mult_le_cancel_right2:
  1022   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1023 by (insert mult_le_cancel_right [of a c 1], simp)
  1024 
  1025 lemma mult_le_cancel_left1:
  1026   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1027 by (insert mult_le_cancel_left [of c 1 b], simp)
  1028 
  1029 lemma mult_le_cancel_left2:
  1030   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1031 by (insert mult_le_cancel_left [of c a 1], simp)
  1032 
  1033 lemma mult_less_cancel_right1:
  1034   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1035 by (insert mult_less_cancel_right [of 1 c b], simp)
  1036 
  1037 lemma mult_less_cancel_right2:
  1038   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1039 by (insert mult_less_cancel_right [of a c 1], simp)
  1040 
  1041 lemma mult_less_cancel_left1:
  1042   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1043 by (insert mult_less_cancel_left [of c 1 b], simp)
  1044 
  1045 lemma mult_less_cancel_left2:
  1046   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1047 by (insert mult_less_cancel_left [of c a 1], simp)
  1048 
  1049 lemma sgn_sgn [simp]:
  1050   "sgn (sgn a) = sgn a"
  1051 unfolding sgn_if by simp
  1052 
  1053 lemma sgn_0_0:
  1054   "sgn a = 0 \<longleftrightarrow> a = 0"
  1055 unfolding sgn_if by simp
  1056 
  1057 lemma sgn_1_pos:
  1058   "sgn a = 1 \<longleftrightarrow> a > 0"
  1059 unfolding sgn_if by (simp add: neg_equal_zero)
  1060 
  1061 lemma sgn_1_neg:
  1062   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1063 unfolding sgn_if by (auto simp add: equal_neg_zero)
  1064 
  1065 lemma sgn_pos [simp]:
  1066   "0 < a \<Longrightarrow> sgn a = 1"
  1067 unfolding sgn_1_pos .
  1068 
  1069 lemma sgn_neg [simp]:
  1070   "a < 0 \<Longrightarrow> sgn a = - 1"
  1071 unfolding sgn_1_neg .
  1072 
  1073 lemma sgn_times:
  1074   "sgn (a * b) = sgn a * sgn b"
  1075 by (auto simp add: sgn_if zero_less_mult_iff)
  1076 
  1077 lemma abs_sgn: "abs k = k * sgn k"
  1078 unfolding sgn_if abs_if by auto
  1079 
  1080 lemma sgn_greater [simp]:
  1081   "0 < sgn a \<longleftrightarrow> 0 < a"
  1082   unfolding sgn_if by auto
  1083 
  1084 lemma sgn_less [simp]:
  1085   "sgn a < 0 \<longleftrightarrow> a < 0"
  1086   unfolding sgn_if by auto
  1087 
  1088 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  1089   by (simp add: abs_if)
  1090 
  1091 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  1092   by (simp add: abs_if)
  1093 
  1094 lemma dvd_if_abs_eq:
  1095   "abs l = abs (k) \<Longrightarrow> l dvd k"
  1096 by(subst abs_dvd_iff[symmetric]) simp
  1097 
  1098 end
  1099 
  1100 text {* Simprules for comparisons where common factors can be cancelled. *}
  1101 
  1102 lemmas mult_compare_simps[noatp] =
  1103     mult_le_cancel_right mult_le_cancel_left
  1104     mult_le_cancel_right1 mult_le_cancel_right2
  1105     mult_le_cancel_left1 mult_le_cancel_left2
  1106     mult_less_cancel_right mult_less_cancel_left
  1107     mult_less_cancel_right1 mult_less_cancel_right2
  1108     mult_less_cancel_left1 mult_less_cancel_left2
  1109     mult_cancel_right mult_cancel_left
  1110     mult_cancel_right1 mult_cancel_right2
  1111     mult_cancel_left1 mult_cancel_left2
  1112 
  1113 -- {* FIXME continue localization here *}
  1114 
  1115 subsection {* Reasoning about inequalities with division *}
  1116 
  1117 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  1118     ==> x * y <= x"
  1119 by (auto simp add: mult_compare_simps)
  1120 
  1121 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  1122     ==> y * x <= x"
  1123 by (auto simp add: mult_compare_simps)
  1124 
  1125 context linordered_semidom
  1126 begin
  1127 
  1128 lemma less_add_one: "a < a + 1"
  1129 proof -
  1130   have "a + 0 < a + 1"
  1131     by (blast intro: zero_less_one add_strict_left_mono)
  1132   thus ?thesis by simp
  1133 qed
  1134 
  1135 lemma zero_less_two: "0 < 1 + 1"
  1136 by (blast intro: less_trans zero_less_one less_add_one)
  1137 
  1138 end
  1139 
  1140 
  1141 subsection {* Absolute Value *}
  1142 
  1143 context linordered_idom
  1144 begin
  1145 
  1146 lemma mult_sgn_abs: "sgn x * abs x = x"
  1147   unfolding abs_if sgn_if by auto
  1148 
  1149 end
  1150 
  1151 lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
  1152 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  1153 
  1154 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1155   assumes abs_eq_mult:
  1156     "(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>"
  1157 
  1158 context linordered_idom
  1159 begin
  1160 
  1161 subclass ordered_ring_abs proof
  1162 qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
  1163 
  1164 lemma abs_mult:
  1165   "abs (a * b) = abs a * abs b" 
  1166   by (rule abs_eq_mult) auto
  1167 
  1168 lemma abs_mult_self:
  1169   "abs a * abs a = a * a"
  1170   by (simp add: abs_if) 
  1171 
  1172 end
  1173 
  1174 lemma abs_mult_less:
  1175      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
  1176 proof -
  1177   assume ac: "abs a < c"
  1178   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  1179   assume "abs b < d"
  1180   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1181 qed
  1182 
  1183 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  1184 
  1185 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
  1186   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  1187 
  1188 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
  1189 apply (simp add: order_less_le abs_le_iff)  
  1190 apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
  1191 done
  1192 
  1193 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
  1194     (abs y) * x = abs (y * x)"
  1195   apply (subst abs_mult)
  1196   apply simp
  1197 done
  1198 
  1199 code_modulename SML
  1200   Rings Arith
  1201 
  1202 code_modulename OCaml
  1203   Rings Arith
  1204 
  1205 code_modulename Haskell
  1206   Rings Arith
  1207 
  1208 end