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