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