src/HOL/Rings.thy
author haftmann
Mon Feb 22 15:53:18 2010 +0100 (2010-02-22)
changeset 35302 4bc6b4d70e08
parent 35216 7641e8d831d2
child 35631 0b8a5fd339ab
permissions -rw-r--r--
tuned text
     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]: "(a + b) * c = a * c + b * c"
    18   assumes right_distrib[algebra_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   [code del]: "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 [noatp, 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 
   187 class no_zero_divisors = zero + times +
   188   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
   189 
   190 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   191   + zero_neq_one + monoid_mult
   192 begin
   193 
   194 subclass semiring_0_cancel ..
   195 
   196 subclass semiring_1 ..
   197 
   198 end
   199 
   200 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
   201   + zero_neq_one + comm_monoid_mult
   202 begin
   203 
   204 subclass semiring_1_cancel ..
   205 subclass comm_semiring_0_cancel ..
   206 subclass comm_semiring_1 ..
   207 
   208 end
   209 
   210 class ring = semiring + ab_group_add
   211 begin
   212 
   213 subclass semiring_0_cancel ..
   214 
   215 text {* Distribution rules *}
   216 
   217 lemma minus_mult_left: "- (a * b) = - a * b"
   218 by (rule minus_unique) (simp add: left_distrib [symmetric]) 
   219 
   220 lemma minus_mult_right: "- (a * b) = a * - b"
   221 by (rule minus_unique) (simp add: right_distrib [symmetric]) 
   222 
   223 text{*Extract signs from products*}
   224 lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
   225 lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
   226 
   227 lemma minus_mult_minus [simp]: "- a * - b = a * b"
   228 by simp
   229 
   230 lemma minus_mult_commute: "- a * b = a * - b"
   231 by simp
   232 
   233 lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"
   234 by (simp add: right_distrib diff_minus)
   235 
   236 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
   237 by (simp add: left_distrib diff_minus)
   238 
   239 lemmas ring_distribs[noatp] =
   240   right_distrib left_distrib left_diff_distrib right_diff_distrib
   241 
   242 text{*Legacy - use @{text algebra_simps} *}
   243 lemmas ring_simps[noatp] = algebra_simps
   244 
   245 lemma eq_add_iff1:
   246   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   247 by (simp add: algebra_simps)
   248 
   249 lemma eq_add_iff2:
   250   "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
   251 by (simp add: algebra_simps)
   252 
   253 end
   254 
   255 lemmas ring_distribs[noatp] =
   256   right_distrib left_distrib left_diff_distrib right_diff_distrib
   257 
   258 class comm_ring = comm_semiring + ab_group_add
   259 begin
   260 
   261 subclass ring ..
   262 subclass comm_semiring_0_cancel ..
   263 
   264 end
   265 
   266 class ring_1 = ring + zero_neq_one + monoid_mult
   267 begin
   268 
   269 subclass semiring_1_cancel ..
   270 
   271 end
   272 
   273 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
   274   (*previously ring*)
   275 begin
   276 
   277 subclass ring_1 ..
   278 subclass comm_semiring_1_cancel ..
   279 
   280 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   281 proof
   282   assume "x dvd - y"
   283   then have "x dvd - 1 * - y" by (rule dvd_mult)
   284   then show "x dvd y" by simp
   285 next
   286   assume "x dvd y"
   287   then have "x dvd - 1 * y" by (rule dvd_mult)
   288   then show "x dvd - y" by simp
   289 qed
   290 
   291 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
   292 proof
   293   assume "- x dvd y"
   294   then obtain k where "y = - x * k" ..
   295   then have "y = x * - k" by simp
   296   then show "x dvd y" ..
   297 next
   298   assume "x dvd y"
   299   then obtain k where "y = x * k" ..
   300   then have "y = - x * - k" by simp
   301   then show "- x dvd y" ..
   302 qed
   303 
   304 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   305 by (simp only: diff_minus dvd_add dvd_minus_iff)
   306 
   307 end
   308 
   309 class ring_no_zero_divisors = ring + no_zero_divisors
   310 begin
   311 
   312 lemma mult_eq_0_iff [simp]:
   313   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
   314 proof (cases "a = 0 \<or> b = 0")
   315   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   316     then show ?thesis using no_zero_divisors by simp
   317 next
   318   case True then show ?thesis by auto
   319 qed
   320 
   321 text{*Cancellation of equalities with a common factor*}
   322 lemma mult_cancel_right [simp, noatp]:
   323   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   324 proof -
   325   have "(a * c = b * c) = ((a - b) * c = 0)"
   326     by (simp add: algebra_simps)
   327   thus ?thesis by (simp add: disj_commute)
   328 qed
   329 
   330 lemma mult_cancel_left [simp, noatp]:
   331   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   332 proof -
   333   have "(c * a = c * b) = (c * (a - b) = 0)"
   334     by (simp add: algebra_simps)
   335   thus ?thesis by simp
   336 qed
   337 
   338 end
   339 
   340 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   341 begin
   342 
   343 lemma mult_cancel_right1 [simp]:
   344   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
   345 by (insert mult_cancel_right [of 1 c b], force)
   346 
   347 lemma mult_cancel_right2 [simp]:
   348   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   349 by (insert mult_cancel_right [of a c 1], simp)
   350  
   351 lemma mult_cancel_left1 [simp]:
   352   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   353 by (insert mult_cancel_left [of c 1 b], force)
   354 
   355 lemma mult_cancel_left2 [simp]:
   356   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
   357 by (insert mult_cancel_left [of c a 1], simp)
   358 
   359 end
   360 
   361 class idom = comm_ring_1 + no_zero_divisors
   362 begin
   363 
   364 subclass ring_1_no_zero_divisors ..
   365 
   366 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
   367 proof
   368   assume "a * a = b * b"
   369   then have "(a - b) * (a + b) = 0"
   370     by (simp add: algebra_simps)
   371   then show "a = b \<or> a = - b"
   372     by (simp add: eq_neg_iff_add_eq_0)
   373 next
   374   assume "a = b \<or> a = - b"
   375   then show "a * a = b * b" by auto
   376 qed
   377 
   378 lemma dvd_mult_cancel_right [simp]:
   379   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   380 proof -
   381   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   382     unfolding dvd_def by (simp add: mult_ac)
   383   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   384     unfolding dvd_def by simp
   385   finally show ?thesis .
   386 qed
   387 
   388 lemma dvd_mult_cancel_left [simp]:
   389   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   390 proof -
   391   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   392     unfolding dvd_def by (simp add: mult_ac)
   393   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   394     unfolding dvd_def by simp
   395   finally show ?thesis .
   396 qed
   397 
   398 end
   399 
   400 class inverse =
   401   fixes inverse :: "'a \<Rightarrow> 'a"
   402     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
   403 
   404 class division_ring = ring_1 + inverse +
   405   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   406   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
   407   assumes divide_inverse: "a / b = a * inverse b"
   408 begin
   409 
   410 subclass ring_1_no_zero_divisors
   411 proof
   412   fix a b :: 'a
   413   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   414   show "a * b \<noteq> 0"
   415   proof
   416     assume ab: "a * b = 0"
   417     hence "0 = inverse a * (a * b) * inverse b" by simp
   418     also have "\<dots> = (inverse a * a) * (b * inverse b)"
   419       by (simp only: mult_assoc)
   420     also have "\<dots> = 1" using a b by simp
   421     finally show False by simp
   422   qed
   423 qed
   424 
   425 lemma nonzero_imp_inverse_nonzero:
   426   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
   427 proof
   428   assume ianz: "inverse a = 0"
   429   assume "a \<noteq> 0"
   430   hence "1 = a * inverse a" by simp
   431   also have "... = 0" by (simp add: ianz)
   432   finally have "1 = 0" .
   433   thus False by (simp add: eq_commute)
   434 qed
   435 
   436 lemma inverse_zero_imp_zero:
   437   "inverse a = 0 \<Longrightarrow> a = 0"
   438 apply (rule classical)
   439 apply (drule nonzero_imp_inverse_nonzero)
   440 apply auto
   441 done
   442 
   443 lemma inverse_unique: 
   444   assumes ab: "a * b = 1"
   445   shows "inverse a = b"
   446 proof -
   447   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
   448   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
   449   ultimately show ?thesis by (simp add: mult_assoc [symmetric])
   450 qed
   451 
   452 lemma nonzero_inverse_minus_eq:
   453   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
   454 by (rule inverse_unique) simp
   455 
   456 lemma nonzero_inverse_inverse_eq:
   457   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
   458 by (rule inverse_unique) simp
   459 
   460 lemma nonzero_inverse_eq_imp_eq:
   461   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
   462   shows "a = b"
   463 proof -
   464   from `inverse a = inverse b`
   465   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
   466   with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
   467     by (simp add: nonzero_inverse_inverse_eq)
   468 qed
   469 
   470 lemma inverse_1 [simp]: "inverse 1 = 1"
   471 by (rule inverse_unique) simp
   472 
   473 lemma nonzero_inverse_mult_distrib: 
   474   assumes "a \<noteq> 0" and "b \<noteq> 0"
   475   shows "inverse (a * b) = inverse b * inverse a"
   476 proof -
   477   have "a * (b * inverse b) * inverse a = 1" using assms by simp
   478   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
   479   thus ?thesis by (rule inverse_unique)
   480 qed
   481 
   482 lemma division_ring_inverse_add:
   483   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
   484 by (simp add: algebra_simps)
   485 
   486 lemma division_ring_inverse_diff:
   487   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
   488 by (simp add: algebra_simps)
   489 
   490 end
   491 
   492 class mult_mono = times + zero + ord +
   493   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   494   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   495 
   496 text {*
   497   The theory of partially ordered rings is taken from the books:
   498   \begin{itemize}
   499   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   500   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   501   \end{itemize}
   502   Most of the used notions can also be looked up in 
   503   \begin{itemize}
   504   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   505   \item \emph{Algebra I} by van der Waerden, Springer.
   506   \end{itemize}
   507 *}
   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
   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
   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)
   795     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
   796      auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
   797 qed (auto simp add: abs_if)
   798 
   799 end
   800 
   801 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
   802    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
   803  *)
   804 class linordered_ring_strict = ring + linordered_semiring_strict
   805   + ordered_ab_group_add + abs_if
   806 begin
   807 
   808 subclass linordered_ring ..
   809 
   810 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   811 using mult_strict_left_mono [of b a "- c"] by simp
   812 
   813 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   814 using mult_strict_right_mono [of b a "- c"] by simp
   815 
   816 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   817 using mult_strict_right_mono_neg [of a zero b] by simp
   818 
   819 subclass ring_no_zero_divisors
   820 proof
   821   fix a b
   822   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   823   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   824   have "a * b < 0 \<or> 0 < a * b"
   825   proof (cases "a < 0")
   826     case True note A' = this
   827     show ?thesis proof (cases "b < 0")
   828       case True with A'
   829       show ?thesis by (auto dest: mult_neg_neg)
   830     next
   831       case False with B have "0 < b" by auto
   832       with A' show ?thesis by (auto dest: mult_strict_right_mono)
   833     qed
   834   next
   835     case False with A have A': "0 < a" by auto
   836     show ?thesis proof (cases "b < 0")
   837       case True with A'
   838       show ?thesis by (auto dest: mult_strict_right_mono_neg)
   839     next
   840       case False with B have "0 < b" by auto
   841       with A' show ?thesis by (auto dest: mult_pos_pos)
   842     qed
   843   qed
   844   then show "a * b \<noteq> 0" by (simp add: neq_iff)
   845 qed
   846 
   847 lemma zero_less_mult_iff:
   848   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   849   apply (auto simp add: mult_pos_pos mult_neg_neg)
   850   apply (simp_all add: not_less le_less)
   851   apply (erule disjE) apply assumption defer
   852   apply (erule disjE) defer apply (drule sym) apply simp
   853   apply (erule disjE) defer apply (drule sym) apply simp
   854   apply (erule disjE) apply assumption apply (drule sym) apply simp
   855   apply (drule sym) apply simp
   856   apply (blast dest: zero_less_mult_pos)
   857   apply (blast dest: zero_less_mult_pos2)
   858   done
   859 
   860 lemma zero_le_mult_iff:
   861   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   862 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
   863 
   864 lemma mult_less_0_iff:
   865   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   866   apply (insert zero_less_mult_iff [of "-a" b])
   867   apply force
   868   done
   869 
   870 lemma mult_le_0_iff:
   871   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   872   apply (insert zero_le_mult_iff [of "-a" b]) 
   873   apply force
   874   done
   875 
   876 lemma zero_le_square [simp]: "0 \<le> a * a"
   877 by (simp add: zero_le_mult_iff linear)
   878 
   879 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   880 by (simp add: not_less)
   881 
   882 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   883    also with the relations @{text "\<le>"} and equality.*}
   884 
   885 text{*These ``disjunction'' versions produce two cases when the comparison is
   886  an assumption, but effectively four when the comparison is a goal.*}
   887 
   888 lemma mult_less_cancel_right_disj:
   889   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   890   apply (cases "c = 0")
   891   apply (auto simp add: neq_iff mult_strict_right_mono 
   892                       mult_strict_right_mono_neg)
   893   apply (auto simp add: not_less 
   894                       not_le [symmetric, of "a*c"]
   895                       not_le [symmetric, of a])
   896   apply (erule_tac [!] notE)
   897   apply (auto simp add: less_imp_le mult_right_mono 
   898                       mult_right_mono_neg)
   899   done
   900 
   901 lemma mult_less_cancel_left_disj:
   902   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   903   apply (cases "c = 0")
   904   apply (auto simp add: neq_iff mult_strict_left_mono 
   905                       mult_strict_left_mono_neg)
   906   apply (auto simp add: not_less 
   907                       not_le [symmetric, of "c*a"]
   908                       not_le [symmetric, of a])
   909   apply (erule_tac [!] notE)
   910   apply (auto simp add: less_imp_le mult_left_mono 
   911                       mult_left_mono_neg)
   912   done
   913 
   914 text{*The ``conjunction of implication'' lemmas produce two cases when the
   915 comparison is a goal, but give four when the comparison is an assumption.*}
   916 
   917 lemma mult_less_cancel_right:
   918   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   919   using mult_less_cancel_right_disj [of a c b] by auto
   920 
   921 lemma mult_less_cancel_left:
   922   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"
   923   using mult_less_cancel_left_disj [of c a b] by auto
   924 
   925 lemma mult_le_cancel_right:
   926    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   927 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)
   928 
   929 lemma mult_le_cancel_left:
   930   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   931 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
   932 
   933 lemma mult_le_cancel_left_pos:
   934   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
   935 by (auto simp: mult_le_cancel_left)
   936 
   937 lemma mult_le_cancel_left_neg:
   938   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
   939 by (auto simp: mult_le_cancel_left)
   940 
   941 lemma mult_less_cancel_left_pos:
   942   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
   943 by (auto simp: mult_less_cancel_left)
   944 
   945 lemma mult_less_cancel_left_neg:
   946   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
   947 by (auto simp: mult_less_cancel_left)
   948 
   949 end
   950 
   951 text{*Legacy - use @{text algebra_simps} *}
   952 lemmas ring_simps[noatp] = algebra_simps
   953 
   954 lemmas mult_sign_intros =
   955   mult_nonneg_nonneg mult_nonneg_nonpos
   956   mult_nonpos_nonneg mult_nonpos_nonpos
   957   mult_pos_pos mult_pos_neg
   958   mult_neg_pos mult_neg_neg
   959 
   960 class ordered_comm_ring = comm_ring + ordered_comm_semiring
   961 begin
   962 
   963 subclass ordered_ring ..
   964 subclass ordered_cancel_comm_semiring ..
   965 
   966 end
   967 
   968 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
   969   (*previously linordered_semiring*)
   970   assumes zero_less_one [simp]: "0 < 1"
   971 begin
   972 
   973 lemma pos_add_strict:
   974   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   975   using add_strict_mono [of zero a b c] by simp
   976 
   977 lemma zero_le_one [simp]: "0 \<le> 1"
   978 by (rule zero_less_one [THEN less_imp_le]) 
   979 
   980 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   981 by (simp add: not_le) 
   982 
   983 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
   984 by (simp add: not_less) 
   985 
   986 lemma less_1_mult:
   987   assumes "1 < m" and "1 < n"
   988   shows "1 < m * n"
   989   using assms mult_strict_mono [of 1 m 1 n]
   990     by (simp add:  less_trans [OF zero_less_one]) 
   991 
   992 end
   993 
   994 class linordered_idom = comm_ring_1 +
   995   linordered_comm_semiring_strict + ordered_ab_group_add +
   996   abs_if + sgn_if
   997   (*previously linordered_ring*)
   998 begin
   999 
  1000 subclass linordered_ring_strict ..
  1001 subclass ordered_comm_ring ..
  1002 subclass idom ..
  1003 
  1004 subclass linordered_semidom
  1005 proof
  1006   have "0 \<le> 1 * 1" by (rule zero_le_square)
  1007   thus "0 < 1" by (simp add: le_less)
  1008 qed 
  1009 
  1010 lemma linorder_neqE_linordered_idom:
  1011   assumes "x \<noteq> y" obtains "x < y" | "y < x"
  1012   using assms by (rule neqE)
  1013 
  1014 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
  1015 
  1016 lemma mult_le_cancel_right1:
  1017   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1018 by (insert mult_le_cancel_right [of 1 c b], simp)
  1019 
  1020 lemma mult_le_cancel_right2:
  1021   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1022 by (insert mult_le_cancel_right [of a c 1], simp)
  1023 
  1024 lemma mult_le_cancel_left1:
  1025   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
  1026 by (insert mult_le_cancel_left [of c 1 b], simp)
  1027 
  1028 lemma mult_le_cancel_left2:
  1029   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
  1030 by (insert mult_le_cancel_left [of c a 1], simp)
  1031 
  1032 lemma mult_less_cancel_right1:
  1033   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1034 by (insert mult_less_cancel_right [of 1 c b], simp)
  1035 
  1036 lemma mult_less_cancel_right2:
  1037   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1038 by (insert mult_less_cancel_right [of a c 1], simp)
  1039 
  1040 lemma mult_less_cancel_left1:
  1041   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
  1042 by (insert mult_less_cancel_left [of c 1 b], simp)
  1043 
  1044 lemma mult_less_cancel_left2:
  1045   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
  1046 by (insert mult_less_cancel_left [of c a 1], simp)
  1047 
  1048 lemma sgn_sgn [simp]:
  1049   "sgn (sgn a) = sgn a"
  1050 unfolding sgn_if by simp
  1051 
  1052 lemma sgn_0_0:
  1053   "sgn a = 0 \<longleftrightarrow> a = 0"
  1054 unfolding sgn_if by simp
  1055 
  1056 lemma sgn_1_pos:
  1057   "sgn a = 1 \<longleftrightarrow> a > 0"
  1058 unfolding sgn_if by simp
  1059 
  1060 lemma sgn_1_neg:
  1061   "sgn a = - 1 \<longleftrightarrow> a < 0"
  1062 unfolding sgn_if by auto
  1063 
  1064 lemma sgn_pos [simp]:
  1065   "0 < a \<Longrightarrow> sgn a = 1"
  1066 unfolding sgn_1_pos .
  1067 
  1068 lemma sgn_neg [simp]:
  1069   "a < 0 \<Longrightarrow> sgn a = - 1"
  1070 unfolding sgn_1_neg .
  1071 
  1072 lemma sgn_times:
  1073   "sgn (a * b) = sgn a * sgn b"
  1074 by (auto simp add: sgn_if zero_less_mult_iff)
  1075 
  1076 lemma abs_sgn: "abs k = k * sgn k"
  1077 unfolding sgn_if abs_if by auto
  1078 
  1079 lemma sgn_greater [simp]:
  1080   "0 < sgn a \<longleftrightarrow> 0 < a"
  1081   unfolding sgn_if by auto
  1082 
  1083 lemma sgn_less [simp]:
  1084   "sgn a < 0 \<longleftrightarrow> a < 0"
  1085   unfolding sgn_if by auto
  1086 
  1087 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  1088   by (simp add: abs_if)
  1089 
  1090 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  1091   by (simp add: abs_if)
  1092 
  1093 lemma dvd_if_abs_eq:
  1094   "abs l = abs (k) \<Longrightarrow> l dvd k"
  1095 by(subst abs_dvd_iff[symmetric]) simp
  1096 
  1097 end
  1098 
  1099 text {* Simprules for comparisons where common factors can be cancelled. *}
  1100 
  1101 lemmas mult_compare_simps[noatp] =
  1102     mult_le_cancel_right mult_le_cancel_left
  1103     mult_le_cancel_right1 mult_le_cancel_right2
  1104     mult_le_cancel_left1 mult_le_cancel_left2
  1105     mult_less_cancel_right mult_less_cancel_left
  1106     mult_less_cancel_right1 mult_less_cancel_right2
  1107     mult_less_cancel_left1 mult_less_cancel_left2
  1108     mult_cancel_right mult_cancel_left
  1109     mult_cancel_right1 mult_cancel_right2
  1110     mult_cancel_left1 mult_cancel_left2
  1111 
  1112 -- {* FIXME continue localization here *}
  1113 
  1114 subsection {* Reasoning about inequalities with division *}
  1115 
  1116 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  1117     ==> x * y <= x"
  1118 by (auto simp add: mult_le_cancel_left2)
  1119 
  1120 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  1121     ==> y * x <= x"
  1122 by (auto simp add: mult_le_cancel_right2)
  1123 
  1124 context linordered_semidom
  1125 begin
  1126 
  1127 lemma less_add_one: "a < a + 1"
  1128 proof -
  1129   have "a + 0 < a + 1"
  1130     by (blast intro: zero_less_one add_strict_left_mono)
  1131   thus ?thesis by simp
  1132 qed
  1133 
  1134 lemma zero_less_two: "0 < 1 + 1"
  1135 by (blast intro: less_trans zero_less_one less_add_one)
  1136 
  1137 end
  1138 
  1139 
  1140 subsection {* Absolute Value *}
  1141 
  1142 context linordered_idom
  1143 begin
  1144 
  1145 lemma mult_sgn_abs: "sgn x * abs x = x"
  1146   unfolding abs_if sgn_if by auto
  1147 
  1148 end
  1149 
  1150 lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
  1151 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  1152 
  1153 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  1154   assumes abs_eq_mult:
  1155     "(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>"
  1156 
  1157 context linordered_idom
  1158 begin
  1159 
  1160 subclass ordered_ring_abs proof
  1161 qed (auto simp add: abs_if not_less mult_less_0_iff)
  1162 
  1163 lemma abs_mult:
  1164   "abs (a * b) = abs a * abs b" 
  1165   by (rule abs_eq_mult) auto
  1166 
  1167 lemma abs_mult_self:
  1168   "abs a * abs a = a * a"
  1169   by (simp add: abs_if) 
  1170 
  1171 end
  1172 
  1173 lemma abs_mult_less:
  1174      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
  1175 proof -
  1176   assume ac: "abs a < c"
  1177   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  1178   assume "abs b < d"
  1179   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  1180 qed
  1181 
  1182 lemmas eq_minus_self_iff[noatp] = equal_neg_zero
  1183 
  1184 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
  1185   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  1186 
  1187 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
  1188 apply (simp add: order_less_le abs_le_iff)  
  1189 apply (auto simp add: abs_if)
  1190 done
  1191 
  1192 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
  1193     (abs y) * x = abs (y * x)"
  1194   apply (subst abs_mult)
  1195   apply simp
  1196 done
  1197 
  1198 code_modulename SML
  1199   Rings Arith
  1200 
  1201 code_modulename OCaml
  1202   Rings Arith
  1203 
  1204 code_modulename Haskell
  1205   Rings Arith
  1206 
  1207 end