src/HOL/Rings.thy
 author blanchet Fri Oct 18 10:43:20 2013 +0200 (2013-10-18) changeset 54147 97a8ff4e4ac9 parent 52435 6646bb548c6b child 54225 8a49a5a30284 permissions -rw-r--r--
killed most "no_atp", to make Sledgehammer more complete
     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 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" (infix "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 [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: distrib_left)

   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: distrib_right [symmetric])

   231

   232 lemma minus_mult_right: "- (a * b) = a * - b"

   233 by (rule minus_unique) (simp add: distrib_left [symmetric])

   234

   235 text{*Extract signs from products*}

   236 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]

   237 lemmas mult_minus_right [simp] = 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: distrib_left diff_minus)

   247

   248 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"

   249 by (simp add: distrib_right diff_minus)

   250

   251 lemmas ring_distribs =

   252   distrib_left distrib_right 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 =

   265   distrib_left distrib_right 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 lemma square_diff_square_factored:

   274   "x * x - y * y = (x + y) * (x - y)"

   275   by (simp add: algebra_simps)

   276

   277 end

   278

   279 class ring_1 = ring + zero_neq_one + monoid_mult

   280 begin

   281

   282 subclass semiring_1_cancel ..

   283

   284 lemma square_diff_one_factored:

   285   "x * x - 1 = (x + 1) * (x - 1)"

   286   by (simp add: algebra_simps)

   287

   288 end

   289

   290 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   291   (*previously ring*)

   292 begin

   293

   294 subclass ring_1 ..

   295 subclass comm_semiring_1_cancel ..

   296

   297 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"

   298 proof

   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 next

   303   assume "x dvd y"

   304   then have "x dvd - 1 * y" by (rule dvd_mult)

   305   then show "x dvd - y" by simp

   306 qed

   307

   308 lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"

   309 proof

   310   assume "- x dvd y"

   311   then obtain k where "y = - x * k" ..

   312   then have "y = x * - k" by simp

   313   then show "x dvd y" ..

   314 next

   315   assume "x dvd y"

   316   then obtain k where "y = x * k" ..

   317   then have "y = - x * - k" by simp

   318   then show "- x dvd y" ..

   319 qed

   320

   321 lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"

   322 by (simp only: diff_minus dvd_add dvd_minus_iff)

   323

   324 end

   325

   326 class ring_no_zero_divisors = ring + no_zero_divisors

   327 begin

   328

   329 lemma mult_eq_0_iff [simp]:

   330   shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"

   331 proof (cases "a = 0 \<or> b = 0")

   332   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto

   333     then show ?thesis using no_zero_divisors by simp

   334 next

   335   case True then show ?thesis by auto

   336 qed

   337

   338 text{*Cancellation of equalities with a common factor*}

   339 lemma mult_cancel_right [simp]:

   340   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"

   341 proof -

   342   have "(a * c = b * c) = ((a - b) * c = 0)"

   343     by (simp add: algebra_simps)

   344   thus ?thesis by (simp add: disj_commute)

   345 qed

   346

   347 lemma mult_cancel_left [simp]:

   348   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"

   349 proof -

   350   have "(c * a = c * b) = (c * (a - b) = 0)"

   351     by (simp add: algebra_simps)

   352   thus ?thesis by simp

   353 qed

   354

   355 end

   356

   357 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   358 begin

   359

   360 lemma square_eq_1_iff:

   361   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"

   362 proof -

   363   have "(x - 1) * (x + 1) = x * x - 1"

   364     by (simp add: algebra_simps)

   365   hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"

   366     by simp

   367   thus ?thesis

   368     by (simp add: eq_neg_iff_add_eq_0)

   369 qed

   370

   371 lemma mult_cancel_right1 [simp]:

   372   "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"

   373 by (insert mult_cancel_right [of 1 c b], force)

   374

   375 lemma mult_cancel_right2 [simp]:

   376   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"

   377 by (insert mult_cancel_right [of a c 1], simp)

   378

   379 lemma mult_cancel_left1 [simp]:

   380   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"

   381 by (insert mult_cancel_left [of c 1 b], force)

   382

   383 lemma mult_cancel_left2 [simp]:

   384   "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"

   385 by (insert mult_cancel_left [of c a 1], simp)

   386

   387 end

   388

   389 class idom = comm_ring_1 + no_zero_divisors

   390 begin

   391

   392 subclass ring_1_no_zero_divisors ..

   393

   394 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"

   395 proof

   396   assume "a * a = b * b"

   397   then have "(a - b) * (a + b) = 0"

   398     by (simp add: algebra_simps)

   399   then show "a = b \<or> a = - b"

   400     by (simp add: eq_neg_iff_add_eq_0)

   401 next

   402   assume "a = b \<or> a = - b"

   403   then show "a * a = b * b" by auto

   404 qed

   405

   406 lemma dvd_mult_cancel_right [simp]:

   407   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"

   408 proof -

   409   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   410     unfolding dvd_def by (simp add: mult_ac)

   411   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   412     unfolding dvd_def by simp

   413   finally show ?thesis .

   414 qed

   415

   416 lemma dvd_mult_cancel_left [simp]:

   417   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"

   418 proof -

   419   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"

   420     unfolding dvd_def by (simp add: mult_ac)

   421   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"

   422     unfolding dvd_def by simp

   423   finally show ?thesis .

   424 qed

   425

   426 end

   427

   428 text {*

   429   The theory of partially ordered rings is taken from the books:

   430   \begin{itemize}

   431   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

   432   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

   433   \end{itemize}

   434   Most of the used notions can also be looked up in

   435   \begin{itemize}

   436   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.

   437   \item \emph{Algebra I} by van der Waerden, Springer.

   438   \end{itemize}

   439 *}

   440

   441 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

   442   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   443   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"

   444 begin

   445

   446 lemma mult_mono:

   447   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

   448 apply (erule mult_right_mono [THEN order_trans], assumption)

   449 apply (erule mult_left_mono, assumption)

   450 done

   451

   452 lemma mult_mono':

   453   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"

   454 apply (rule mult_mono)

   455 apply (fast intro: order_trans)+

   456 done

   457

   458 end

   459

   460 class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add

   461 begin

   462

   463 subclass semiring_0_cancel ..

   464

   465 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"

   466 using mult_left_mono [of 0 b a] by simp

   467

   468 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"

   469 using mult_left_mono [of b 0 a] by simp

   470

   471 lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"

   472 using mult_right_mono [of a 0 b] by simp

   473

   474 text {* Legacy - use @{text mult_nonpos_nonneg} *}

   475 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"

   476 by (drule mult_right_mono [of b 0], auto)

   477

   478 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"

   479 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   480

   481 end

   482

   483 class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add

   484 begin

   485

   486 subclass ordered_cancel_semiring ..

   487

   488 subclass ordered_comm_monoid_add ..

   489

   490 lemma mult_left_less_imp_less:

   491   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

   492 by (force simp add: mult_left_mono not_le [symmetric])

   493

   494 lemma mult_right_less_imp_less:

   495   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"

   496 by (force simp add: mult_right_mono not_le [symmetric])

   497

   498 end

   499

   500 class linordered_semiring_1 = linordered_semiring + semiring_1

   501 begin

   502

   503 lemma convex_bound_le:

   504   assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1"

   505   shows "u * x + v * y \<le> a"

   506 proof-

   507   from assms have "u * x + v * y \<le> u * a + v * a"

   508     by (simp add: add_mono mult_left_mono)

   509   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

   510 qed

   511

   512 end

   513

   514 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

   515   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   516   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"

   517 begin

   518

   519 subclass semiring_0_cancel ..

   520

   521 subclass linordered_semiring

   522 proof

   523   fix a b c :: 'a

   524   assume A: "a \<le> b" "0 \<le> c"

   525   from A show "c * a \<le> c * b"

   526     unfolding le_less

   527     using mult_strict_left_mono by (cases "c = 0") auto

   528   from A show "a * c \<le> b * c"

   529     unfolding le_less

   530     using mult_strict_right_mono by (cases "c = 0") auto

   531 qed

   532

   533 lemma mult_left_le_imp_le:

   534   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

   535 by (force simp add: mult_strict_left_mono _not_less [symmetric])

   536

   537 lemma mult_right_le_imp_le:

   538   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"

   539 by (force simp add: mult_strict_right_mono not_less [symmetric])

   540

   541 lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"

   542 using mult_strict_left_mono [of 0 b a] by simp

   543

   544 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"

   545 using mult_strict_left_mono [of b 0 a] by simp

   546

   547 lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"

   548 using mult_strict_right_mono [of a 0 b] by simp

   549

   550 text {* Legacy - use @{text mult_neg_pos} *}

   551 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"

   552 by (drule mult_strict_right_mono [of b 0], auto)

   553

   554 lemma zero_less_mult_pos:

   555   "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

   556 apply (cases "b\<le>0")

   557  apply (auto simp add: le_less not_less)

   558 apply (drule_tac mult_pos_neg [of a b])

   559  apply (auto dest: less_not_sym)

   560 done

   561

   562 lemma zero_less_mult_pos2:

   563   "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"

   564 apply (cases "b\<le>0")

   565  apply (auto simp add: le_less not_less)

   566 apply (drule_tac mult_pos_neg2 [of a b])

   567  apply (auto dest: less_not_sym)

   568 done

   569

   570 text{*Strict monotonicity in both arguments*}

   571 lemma mult_strict_mono:

   572   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"

   573   shows "a * c < b * d"

   574   using assms apply (cases "c=0")

   575   apply (simp add: mult_pos_pos)

   576   apply (erule mult_strict_right_mono [THEN less_trans])

   577   apply (force simp add: le_less)

   578   apply (erule mult_strict_left_mono, assumption)

   579   done

   580

   581 text{*This weaker variant has more natural premises*}

   582 lemma mult_strict_mono':

   583   assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"

   584   shows "a * c < b * d"

   585 by (rule mult_strict_mono) (insert assms, auto)

   586

   587 lemma mult_less_le_imp_less:

   588   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"

   589   shows "a * c < b * d"

   590   using assms apply (subgoal_tac "a * c < b * c")

   591   apply (erule less_le_trans)

   592   apply (erule mult_left_mono)

   593   apply simp

   594   apply (erule mult_strict_right_mono)

   595   apply assumption

   596   done

   597

   598 lemma mult_le_less_imp_less:

   599   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"

   600   shows "a * c < b * d"

   601   using assms apply (subgoal_tac "a * c \<le> b * c")

   602   apply (erule le_less_trans)

   603   apply (erule mult_strict_left_mono)

   604   apply simp

   605   apply (erule mult_right_mono)

   606   apply simp

   607   done

   608

   609 lemma mult_less_imp_less_left:

   610   assumes less: "c * a < c * b" and nonneg: "0 \<le> c"

   611   shows "a < b"

   612 proof (rule ccontr)

   613   assume "\<not>  a < b"

   614   hence "b \<le> a" by (simp add: linorder_not_less)

   615   hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)

   616   with this and less show False by (simp add: not_less [symmetric])

   617 qed

   618

   619 lemma mult_less_imp_less_right:

   620   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"

   621   shows "a < b"

   622 proof (rule ccontr)

   623   assume "\<not> a < b"

   624   hence "b \<le> a" by (simp add: linorder_not_less)

   625   hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)

   626   with this and less show False by (simp add: not_less [symmetric])

   627 qed

   628

   629 end

   630

   631 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   632 begin

   633

   634 subclass linordered_semiring_1 ..

   635

   636 lemma convex_bound_lt:

   637   assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1"

   638   shows "u * x + v * y < a"

   639 proof -

   640   from assms have "u * x + v * y < u * a + v * a"

   641     by (cases "u = 0")

   642        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)

   643   thus ?thesis using assms unfolding distrib_right[symmetric] by simp

   644 qed

   645

   646 end

   647

   648 class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +

   649   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   650 begin

   651

   652 subclass ordered_semiring

   653 proof

   654   fix a b c :: 'a

   655   assume "a \<le> b" "0 \<le> c"

   656   thus "c * a \<le> c * b" by (rule comm_mult_left_mono)

   657   thus "a * c \<le> b * c" by (simp only: mult_commute)

   658 qed

   659

   660 end

   661

   662 class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add

   663 begin

   664

   665 subclass comm_semiring_0_cancel ..

   666 subclass ordered_comm_semiring ..

   667 subclass ordered_cancel_semiring ..

   668

   669 end

   670

   671 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

   672   assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   673 begin

   674

   675 subclass linordered_semiring_strict

   676 proof

   677   fix a b c :: 'a

   678   assume "a < b" "0 < c"

   679   thus "c * a < c * b" by (rule comm_mult_strict_left_mono)

   680   thus "a * c < b * c" by (simp only: mult_commute)

   681 qed

   682

   683 subclass ordered_cancel_comm_semiring

   684 proof

   685   fix a b c :: 'a

   686   assume "a \<le> b" "0 \<le> c"

   687   thus "c * a \<le> c * b"

   688     unfolding le_less

   689     using mult_strict_left_mono by (cases "c = 0") auto

   690 qed

   691

   692 end

   693

   694 class ordered_ring = ring + ordered_cancel_semiring

   695 begin

   696

   697 subclass ordered_ab_group_add ..

   698

   699 lemma less_add_iff1:

   700   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"

   701 by (simp add: algebra_simps)

   702

   703 lemma less_add_iff2:

   704   "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"

   705 by (simp add: algebra_simps)

   706

   707 lemma le_add_iff1:

   708   "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"

   709 by (simp add: algebra_simps)

   710

   711 lemma le_add_iff2:

   712   "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"

   713 by (simp add: algebra_simps)

   714

   715 lemma mult_left_mono_neg:

   716   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"

   717   apply (drule mult_left_mono [of _ _ "- c"])

   718   apply simp_all

   719   done

   720

   721 lemma mult_right_mono_neg:

   722   "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"

   723   apply (drule mult_right_mono [of _ _ "- c"])

   724   apply simp_all

   725   done

   726

   727 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"

   728 using mult_right_mono_neg [of a 0 b] by simp

   729

   730 lemma split_mult_pos_le:

   731   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"

   732 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   733

   734 end

   735

   736 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   737 begin

   738

   739 subclass ordered_ring ..

   740

   741 subclass ordered_ab_group_add_abs

   742 proof

   743   fix a b

   744   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

   745     by (auto simp add: abs_if not_less)

   746     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],

   747      auto intro!: less_imp_le add_neg_neg)

   748 qed (auto simp add: abs_if)

   749

   750 lemma zero_le_square [simp]: "0 \<le> a * a"

   751   using linear [of 0 a]

   752   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   753

   754 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"

   755   by (simp add: not_less)

   756

   757 end

   758

   759 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.

   760    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

   761  *)

   762 class linordered_ring_strict = ring + linordered_semiring_strict

   763   + ordered_ab_group_add + abs_if

   764 begin

   765

   766 subclass linordered_ring ..

   767

   768 lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"

   769 using mult_strict_left_mono [of b a "- c"] by simp

   770

   771 lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"

   772 using mult_strict_right_mono [of b a "- c"] by simp

   773

   774 lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"

   775 using mult_strict_right_mono_neg [of a 0 b] by simp

   776

   777 subclass ring_no_zero_divisors

   778 proof

   779   fix a b

   780   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)

   781   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)

   782   have "a * b < 0 \<or> 0 < a * b"

   783   proof (cases "a < 0")

   784     case True note A' = this

   785     show ?thesis proof (cases "b < 0")

   786       case True with A'

   787       show ?thesis by (auto dest: mult_neg_neg)

   788     next

   789       case False with B have "0 < b" by auto

   790       with A' show ?thesis by (auto dest: mult_strict_right_mono)

   791     qed

   792   next

   793     case False with A have A': "0 < a" by auto

   794     show ?thesis proof (cases "b < 0")

   795       case True with A'

   796       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   797     next

   798       case False with B have "0 < b" by auto

   799       with A' show ?thesis by (auto dest: mult_pos_pos)

   800     qed

   801   qed

   802   then show "a * b \<noteq> 0" by (simp add: neq_iff)

   803 qed

   804

   805 lemma zero_less_mult_iff:

   806   "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"

   807   apply (auto simp add: mult_pos_pos mult_neg_neg)

   808   apply (simp_all add: not_less le_less)

   809   apply (erule disjE) apply assumption defer

   810   apply (erule disjE) defer apply (drule sym) apply simp

   811   apply (erule disjE) defer apply (drule sym) apply simp

   812   apply (erule disjE) apply assumption apply (drule sym) apply simp

   813   apply (drule sym) apply simp

   814   apply (blast dest: zero_less_mult_pos)

   815   apply (blast dest: zero_less_mult_pos2)

   816   done

   817

   818 lemma zero_le_mult_iff:

   819   "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"

   820 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)

   821

   822 lemma mult_less_0_iff:

   823   "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"

   824   apply (insert zero_less_mult_iff [of "-a" b])

   825   apply force

   826   done

   827

   828 lemma mult_le_0_iff:

   829   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"

   830   apply (insert zero_le_mult_iff [of "-a" b])

   831   apply force

   832   done

   833

   834 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},

   835    also with the relations @{text "\<le>"} and equality.*}

   836

   837 text{*These disjunction'' versions produce two cases when the comparison is

   838  an assumption, but effectively four when the comparison is a goal.*}

   839

   840 lemma mult_less_cancel_right_disj:

   841   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

   842   apply (cases "c = 0")

   843   apply (auto simp add: neq_iff mult_strict_right_mono

   844                       mult_strict_right_mono_neg)

   845   apply (auto simp add: not_less

   846                       not_le [symmetric, of "a*c"]

   847                       not_le [symmetric, of a])

   848   apply (erule_tac [!] notE)

   849   apply (auto simp add: less_imp_le mult_right_mono

   850                       mult_right_mono_neg)

   851   done

   852

   853 lemma mult_less_cancel_left_disj:

   854   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"

   855   apply (cases "c = 0")

   856   apply (auto simp add: neq_iff mult_strict_left_mono

   857                       mult_strict_left_mono_neg)

   858   apply (auto simp add: not_less

   859                       not_le [symmetric, of "c*a"]

   860                       not_le [symmetric, of a])

   861   apply (erule_tac [!] notE)

   862   apply (auto simp add: less_imp_le mult_left_mono

   863                       mult_left_mono_neg)

   864   done

   865

   866 text{*The conjunction of implication'' lemmas produce two cases when the

   867 comparison is a goal, but give four when the comparison is an assumption.*}

   868

   869 lemma mult_less_cancel_right:

   870   "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

   871   using mult_less_cancel_right_disj [of a c b] by auto

   872

   873 lemma mult_less_cancel_left:

   874   "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)"

   875   using mult_less_cancel_left_disj [of c a b] by auto

   876

   877 lemma mult_le_cancel_right:

   878    "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

   879 by (simp add: not_less [symmetric] mult_less_cancel_right_disj)

   880

   881 lemma mult_le_cancel_left:

   882   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"

   883 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)

   884

   885 lemma mult_le_cancel_left_pos:

   886   "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"

   887 by (auto simp: mult_le_cancel_left)

   888

   889 lemma mult_le_cancel_left_neg:

   890   "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"

   891 by (auto simp: mult_le_cancel_left)

   892

   893 lemma mult_less_cancel_left_pos:

   894   "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"

   895 by (auto simp: mult_less_cancel_left)

   896

   897 lemma mult_less_cancel_left_neg:

   898   "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"

   899 by (auto simp: mult_less_cancel_left)

   900

   901 end

   902

   903 lemmas mult_sign_intros =

   904   mult_nonneg_nonneg mult_nonneg_nonpos

   905   mult_nonpos_nonneg mult_nonpos_nonpos

   906   mult_pos_pos mult_pos_neg

   907   mult_neg_pos mult_neg_neg

   908

   909 class ordered_comm_ring = comm_ring + ordered_comm_semiring

   910 begin

   911

   912 subclass ordered_ring ..

   913 subclass ordered_cancel_comm_semiring ..

   914

   915 end

   916

   917 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

   918   (*previously linordered_semiring*)

   919   assumes zero_less_one [simp]: "0 < 1"

   920 begin

   921

   922 lemma pos_add_strict:

   923   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"

   924   using add_strict_mono [of 0 a b c] by simp

   925

   926 lemma zero_le_one [simp]: "0 \<le> 1"

   927 by (rule zero_less_one [THEN less_imp_le])

   928

   929 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"

   930 by (simp add: not_le)

   931

   932 lemma not_one_less_zero [simp]: "\<not> 1 < 0"

   933 by (simp add: not_less)

   934

   935 lemma less_1_mult:

   936   assumes "1 < m" and "1 < n"

   937   shows "1 < m * n"

   938   using assms mult_strict_mono [of 1 m 1 n]

   939     by (simp add:  less_trans [OF zero_less_one])

   940

   941 end

   942

   943 class linordered_idom = comm_ring_1 +

   944   linordered_comm_semiring_strict + ordered_ab_group_add +

   945   abs_if + sgn_if

   946   (*previously linordered_ring*)

   947 begin

   948

   949 subclass linordered_semiring_1_strict ..

   950 subclass linordered_ring_strict ..

   951 subclass ordered_comm_ring ..

   952 subclass idom ..

   953

   954 subclass linordered_semidom

   955 proof

   956   have "0 \<le> 1 * 1" by (rule zero_le_square)

   957   thus "0 < 1" by (simp add: le_less)

   958 qed

   959

   960 lemma linorder_neqE_linordered_idom:

   961   assumes "x \<noteq> y" obtains "x < y" | "y < x"

   962   using assms by (rule neqE)

   963

   964 text {* These cancellation simprules also produce two cases when the comparison is a goal. *}

   965

   966 lemma mult_le_cancel_right1:

   967   "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

   968 by (insert mult_le_cancel_right [of 1 c b], simp)

   969

   970 lemma mult_le_cancel_right2:

   971   "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

   972 by (insert mult_le_cancel_right [of a c 1], simp)

   973

   974 lemma mult_le_cancel_left1:

   975   "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"

   976 by (insert mult_le_cancel_left [of c 1 b], simp)

   977

   978 lemma mult_le_cancel_left2:

   979   "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"

   980 by (insert mult_le_cancel_left [of c a 1], simp)

   981

   982 lemma mult_less_cancel_right1:

   983   "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

   984 by (insert mult_less_cancel_right [of 1 c b], simp)

   985

   986 lemma mult_less_cancel_right2:

   987   "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

   988 by (insert mult_less_cancel_right [of a c 1], simp)

   989

   990 lemma mult_less_cancel_left1:

   991   "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"

   992 by (insert mult_less_cancel_left [of c 1 b], simp)

   993

   994 lemma mult_less_cancel_left2:

   995   "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"

   996 by (insert mult_less_cancel_left [of c a 1], simp)

   997

   998 lemma sgn_sgn [simp]:

   999   "sgn (sgn a) = sgn a"

  1000 unfolding sgn_if by simp

  1001

  1002 lemma sgn_0_0:

  1003   "sgn a = 0 \<longleftrightarrow> a = 0"

  1004 unfolding sgn_if by simp

  1005

  1006 lemma sgn_1_pos:

  1007   "sgn a = 1 \<longleftrightarrow> a > 0"

  1008 unfolding sgn_if by simp

  1009

  1010 lemma sgn_1_neg:

  1011   "sgn a = - 1 \<longleftrightarrow> a < 0"

  1012 unfolding sgn_if by auto

  1013

  1014 lemma sgn_pos [simp]:

  1015   "0 < a \<Longrightarrow> sgn a = 1"

  1016 unfolding sgn_1_pos .

  1017

  1018 lemma sgn_neg [simp]:

  1019   "a < 0 \<Longrightarrow> sgn a = - 1"

  1020 unfolding sgn_1_neg .

  1021

  1022 lemma sgn_times:

  1023   "sgn (a * b) = sgn a * sgn b"

  1024 by (auto simp add: sgn_if zero_less_mult_iff)

  1025

  1026 lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"

  1027 unfolding sgn_if abs_if by auto

  1028

  1029 lemma sgn_greater [simp]:

  1030   "0 < sgn a \<longleftrightarrow> 0 < a"

  1031   unfolding sgn_if by auto

  1032

  1033 lemma sgn_less [simp]:

  1034   "sgn a < 0 \<longleftrightarrow> a < 0"

  1035   unfolding sgn_if by auto

  1036

  1037 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"

  1038   by (simp add: abs_if)

  1039

  1040 lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"

  1041   by (simp add: abs_if)

  1042

  1043 lemma dvd_if_abs_eq:

  1044   "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"

  1045 by(subst abs_dvd_iff[symmetric]) simp

  1046

  1047 end

  1048

  1049 text {* Simprules for comparisons where common factors can be cancelled. *}

  1050

  1051 lemmas mult_compare_simps =

  1052     mult_le_cancel_right mult_le_cancel_left

  1053     mult_le_cancel_right1 mult_le_cancel_right2

  1054     mult_le_cancel_left1 mult_le_cancel_left2

  1055     mult_less_cancel_right mult_less_cancel_left

  1056     mult_less_cancel_right1 mult_less_cancel_right2

  1057     mult_less_cancel_left1 mult_less_cancel_left2

  1058     mult_cancel_right mult_cancel_left

  1059     mult_cancel_right1 mult_cancel_right2

  1060     mult_cancel_left1 mult_cancel_left2

  1061

  1062 text {* Reasoning about inequalities with division *}

  1063

  1064 context linordered_semidom

  1065 begin

  1066

  1067 lemma less_add_one: "a < a + 1"

  1068 proof -

  1069   have "a + 0 < a + 1"

  1070     by (blast intro: zero_less_one add_strict_left_mono)

  1071   thus ?thesis by simp

  1072 qed

  1073

  1074 lemma zero_less_two: "0 < 1 + 1"

  1075 by (blast intro: less_trans zero_less_one less_add_one)

  1076

  1077 end

  1078

  1079 context linordered_idom

  1080 begin

  1081

  1082 lemma mult_right_le_one_le:

  1083   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"

  1084   by (auto simp add: mult_le_cancel_left2)

  1085

  1086 lemma mult_left_le_one_le:

  1087   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"

  1088   by (auto simp add: mult_le_cancel_right2)

  1089

  1090 end

  1091

  1092 text {* Absolute Value *}

  1093

  1094 context linordered_idom

  1095 begin

  1096

  1097 lemma mult_sgn_abs:

  1098   "sgn x * \<bar>x\<bar> = x"

  1099   unfolding abs_if sgn_if by auto

  1100

  1101 lemma abs_one [simp]:

  1102   "\<bar>1\<bar> = 1"

  1103   by (simp add: abs_if)

  1104

  1105 end

  1106

  1107 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1108   assumes abs_eq_mult:

  1109     "(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>"

  1110

  1111 context linordered_idom

  1112 begin

  1113

  1114 subclass ordered_ring_abs proof

  1115 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1116

  1117 lemma abs_mult:

  1118   "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"

  1119   by (rule abs_eq_mult) auto

  1120

  1121 lemma abs_mult_self:

  1122   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"

  1123   by (simp add: abs_if)

  1124

  1125 lemma abs_mult_less:

  1126   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"

  1127 proof -

  1128   assume ac: "\<bar>a\<bar> < c"

  1129   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)

  1130   assume "\<bar>b\<bar> < d"

  1131   thus ?thesis by (simp add: ac cpos mult_strict_mono)

  1132 qed

  1133

  1134 lemma less_minus_self_iff:

  1135   "a < - a \<longleftrightarrow> a < 0"

  1136   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)

  1137

  1138 lemma abs_less_iff:

  1139   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"

  1140   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)

  1141

  1142 lemma abs_mult_pos:

  1143   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"

  1144   by (simp add: abs_mult)

  1145

  1146 lemma abs_diff_less_iff:

  1147   "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"

  1148   by (auto simp add: diff_less_eq ac_simps abs_less_iff)

  1149

  1150 end

  1151

  1152 code_identifier

  1153   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  1154

  1155 end

  1156