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