src/HOL/Rings.thy
 author blanchet Thu Mar 18 12:58:52 2010 +0100 (2010-03-18) changeset 35828 46cfc4b8112e parent 35631 0b8a5fd339ab child 36301 72f4d079ebf8 permissions -rw-r--r--
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
     1 (*  Title:      HOL/Rings.thy

     2     Author:     Gertrud Bauer

     3     Author:     Steven Obua

     4     Author:     Tobias Nipkow

     5     Author:     Lawrence C Paulson

     6     Author:     Markus Wenzel

     7     Author:     Jeremy Avigad

     8 *)

     9

    10 header {* Rings *}

    11

    12 theory Rings

    13 imports Groups

    14 begin

    15

    16 class semiring = ab_semigroup_add + semigroup_mult +

    17   assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"

    18   assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"

    19 begin

    20

    21 text{*For the @{text combine_numerals} simproc*}

    22 lemma combine_common_factor:

    23   "a * e + (b * e + c) = (a + b) * e + c"

    24 by (simp add: left_distrib add_ac)

    25

    26 end

    27

    28 class mult_zero = times + zero +

    29   assumes mult_zero_left [simp]: "0 * a = 0"

    30   assumes mult_zero_right [simp]: "a * 0 = 0"

    31

    32 class semiring_0 = semiring + comm_monoid_add + mult_zero

    33

    34 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    35 begin

    36

    37 subclass semiring_0

    38 proof

    39   fix a :: 'a

    40   have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])

    41   thus "0 * a = 0" by (simp only: add_left_cancel)

    42 next

    43   fix a :: 'a

    44   have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])

    45   thus "a * 0 = 0" by (simp only: add_left_cancel)

    46 qed

    47

    48 end

    49

    50 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

    51   assumes distrib: "(a + b) * c = a * c + b * c"

    52 begin

    53

    54 subclass semiring

    55 proof

    56   fix a b c :: 'a

    57   show "(a + b) * c = a * c + b * c" by (simp add: distrib)

    58   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)

    59   also have "... = b * a + c * a" by (simp only: distrib)

    60   also have "... = a * b + a * c" by (simp add: mult_ac)

    61   finally show "a * (b + c) = a * b + a * c" by blast

    62 qed

    63

    64 end

    65

    66 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    67 begin

    68

    69 subclass semiring_0 ..

    70

    71 end

    72

    73 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    74 begin

    75

    76 subclass semiring_0_cancel ..

    77

    78 subclass comm_semiring_0 ..

    79

    80 end

    81

    82 class zero_neq_one = zero + one +

    83   assumes zero_neq_one [simp]: "0 \<noteq> 1"

    84 begin

    85

    86 lemma one_neq_zero [simp]: "1 \<noteq> 0"

    87 by (rule not_sym) (rule zero_neq_one)

    88

    89 end

    90

    91 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

    92

    93 text {* Abstract divisibility *}

    94

    95 class dvd = times

    96 begin

    97

    98 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where

    99   [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"

   100

   101 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"

   102   unfolding dvd_def ..

   103

   104 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"

   105   unfolding dvd_def by blast

   106

   107 end

   108

   109 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd

   110   (*previously almost_semiring*)

   111 begin

   112

   113 subclass semiring_1 ..

   114

   115 lemma dvd_refl[simp]: "a dvd a"

   116 proof

   117   show "a = a * 1" by simp

   118 qed

   119

   120 lemma dvd_trans:

   121   assumes "a dvd b" and "b dvd c"

   122   shows "a dvd c"

   123 proof -

   124   from assms obtain v where "b = a * v" by (auto elim!: dvdE)

   125   moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE)

   126   ultimately have "c = a * (v * w)" by (simp add: mult_assoc)

   127   then show ?thesis ..

   128 qed

   129

   130 lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"

   131 by (auto intro: dvd_refl elim!: dvdE)

   132

   133 lemma dvd_0_right [iff]: "a dvd 0"

   134 proof

   135   show "0 = a * 0" by simp

   136 qed

   137

   138 lemma one_dvd [simp]: "1 dvd a"

   139 by (auto intro!: dvdI)

   140

   141 lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"

   142 by (auto intro!: mult_left_commute dvdI elim!: dvdE)

   143

   144 lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"

   145   apply (subst mult_commute)

   146   apply (erule dvd_mult)

   147   done

   148

   149 lemma dvd_triv_right [simp]: "a dvd b * a"

   150 by (rule dvd_mult) (rule dvd_refl)

   151

   152 lemma dvd_triv_left [simp]: "a dvd a * b"

   153 by (rule dvd_mult2) (rule dvd_refl)

   154

   155 lemma mult_dvd_mono:

   156   assumes "a dvd b"

   157     and "c dvd d"

   158   shows "a * c dvd b * d"

   159 proof -

   160   from a dvd b obtain b' where "b = a * b'" ..

   161   moreover from c dvd d obtain d' where "d = c * d'" ..

   162   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)

   163   then show ?thesis ..

   164 qed

   165

   166 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"

   167 by (simp add: dvd_def mult_assoc, blast)

   168

   169 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"

   170   unfolding mult_ac [of a] by (rule dvd_mult_left)

   171

   172 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"

   173 by simp

   174

   175 lemma dvd_add[simp]:

   176   assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)"

   177 proof -

   178   from a dvd b obtain b' where "b = a * b'" ..

   179   moreover from a dvd c obtain c' where "c = a * c'" ..

   180   ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)

   181   then show ?thesis ..

   182 qed

   183

   184 end

   185

   186

   187 class no_zero_divisors = zero + times +

   188   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"

   189

   190 class semiring_1_cancel = semiring + cancel_comm_monoid_add

   191   + zero_neq_one + monoid_mult

   192 begin

   193

   194 subclass semiring_0_cancel ..

   195

   196 subclass semiring_1 ..

   197

   198 end

   199

   200 class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add

   201   + zero_neq_one + comm_monoid_mult

   202 begin

   203

   204 subclass semiring_1_cancel ..

   205 subclass comm_semiring_0_cancel ..

   206 subclass comm_semiring_1 ..

   207

   208 end

   209

   210 class ring = semiring + ab_group_add

   211 begin

   212

   213 subclass semiring_0_cancel ..

   214

   215 text {* Distribution rules *}

   216

   217 lemma minus_mult_left: "- (a * b) = - a * b"

   218 by (rule minus_unique) (simp add: left_distrib [symmetric])

   219

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

   221 by (rule minus_unique) (simp add: right_distrib [symmetric])

   222

   223 text{*Extract signs from products*}

   224 lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]

   225 lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]

   226

   227 lemma minus_mult_minus [simp]: "- a * - b = a * b"

   228 by simp

   229

   230 lemma minus_mult_commute: "- a * b = a * - b"

   231 by simp

   232

   233 lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"

   234 by (simp add: right_distrib diff_minus)

   235

   236 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"

   237 by (simp add: left_distrib diff_minus)

   238

   239 lemmas ring_distribs[no_atp] =

   240   right_distrib left_distrib left_diff_distrib right_diff_distrib

   241

   242 text{*Legacy - use @{text algebra_simps} *}

   243 lemmas ring_simps[no_atp] = algebra_simps

   244

   245 lemma eq_add_iff1:

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

   247 by (simp add: algebra_simps)

   248

   249 lemma eq_add_iff2:

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

   251 by (simp add: algebra_simps)

   252

   253 end

   254

   255 lemmas ring_distribs[no_atp] =

   256   right_distrib left_distrib left_diff_distrib right_diff_distrib

   257

   258 class comm_ring = comm_semiring + ab_group_add

   259 begin

   260

   261 subclass ring ..

   262 subclass comm_semiring_0_cancel ..

   263

   264 end

   265

   266 class ring_1 = ring + zero_neq_one + monoid_mult

   267 begin

   268

   269 subclass semiring_1_cancel ..

   270

   271 end

   272

   273 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   274   (*previously ring*)

   275 begin

   276

   277 subclass ring_1 ..

   278 subclass comm_semiring_1_cancel ..

   279

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

   281 proof

   282   assume "x dvd - y"

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

   284   then show "x dvd y" by simp

   285 next

   286   assume "x dvd y"

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

   288   then show "x dvd - y" by simp

   289 qed

   290

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

   292 proof

   293   assume "- x dvd y"

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

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

   296   then show "x dvd y" ..

   297 next

   298   assume "x dvd y"

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

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

   301   then show "- x dvd y" ..

   302 qed

   303

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

   305 by (simp only: diff_minus dvd_add dvd_minus_iff)

   306

   307 end

   308

   309 class ring_no_zero_divisors = ring + no_zero_divisors

   310 begin

   311

   312 lemma mult_eq_0_iff [simp]:

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

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

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

   316     then show ?thesis using no_zero_divisors by simp

   317 next

   318   case True then show ?thesis by auto

   319 qed

   320

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

   322 lemma mult_cancel_right [simp, no_atp]:

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

   324 proof -

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

   326     by (simp add: algebra_simps)

   327   thus ?thesis by (simp add: disj_commute)

   328 qed

   329

   330 lemma mult_cancel_left [simp, no_atp]:

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

   332 proof -

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

   334     by (simp add: algebra_simps)

   335   thus ?thesis by simp

   336 qed

   337

   338 end

   339

   340 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   341 begin

   342

   343 lemma mult_cancel_right1 [simp]:

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

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

   346

   347 lemma mult_cancel_right2 [simp]:

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

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

   350

   351 lemma mult_cancel_left1 [simp]:

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

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

   354

   355 lemma mult_cancel_left2 [simp]:

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

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

   358

   359 end

   360

   361 class idom = comm_ring_1 + no_zero_divisors

   362 begin

   363

   364 subclass ring_1_no_zero_divisors ..

   365

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

   367 proof

   368   assume "a * a = b * b"

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

   370     by (simp add: algebra_simps)

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

   372     by (simp add: eq_neg_iff_add_eq_0)

   373 next

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

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

   376 qed

   377

   378 lemma dvd_mult_cancel_right [simp]:

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

   380 proof -

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

   382     unfolding dvd_def by (simp add: mult_ac)

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

   384     unfolding dvd_def by simp

   385   finally show ?thesis .

   386 qed

   387

   388 lemma dvd_mult_cancel_left [simp]:

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

   390 proof -

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

   392     unfolding dvd_def by (simp add: mult_ac)

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

   394     unfolding dvd_def by simp

   395   finally show ?thesis .

   396 qed

   397

   398 end

   399

   400 class inverse =

   401   fixes inverse :: "'a \<Rightarrow> 'a"

   402     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)

   403

   404 class division_ring = ring_1 + inverse +

   405   assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

   406   assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"

   407   assumes divide_inverse: "a / b = a * inverse b"

   408 begin

   409

   410 subclass ring_1_no_zero_divisors

   411 proof

   412   fix a b :: 'a

   413   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"

   414   show "a * b \<noteq> 0"

   415   proof

   416     assume ab: "a * b = 0"

   417     hence "0 = inverse a * (a * b) * inverse b" by simp

   418     also have "\<dots> = (inverse a * a) * (b * inverse b)"

   419       by (simp only: mult_assoc)

   420     also have "\<dots> = 1" using a b by simp

   421     finally show False by simp

   422   qed

   423 qed

   424

   425 lemma nonzero_imp_inverse_nonzero:

   426   "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"

   427 proof

   428   assume ianz: "inverse a = 0"

   429   assume "a \<noteq> 0"

   430   hence "1 = a * inverse a" by simp

   431   also have "... = 0" by (simp add: ianz)

   432   finally have "1 = 0" .

   433   thus False by (simp add: eq_commute)

   434 qed

   435

   436 lemma inverse_zero_imp_zero:

   437   "inverse a = 0 \<Longrightarrow> a = 0"

   438 apply (rule classical)

   439 apply (drule nonzero_imp_inverse_nonzero)

   440 apply auto

   441 done

   442

   443 lemma inverse_unique:

   444   assumes ab: "a * b = 1"

   445   shows "inverse a = b"

   446 proof -

   447   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all

   448   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)

   449   ultimately show ?thesis by (simp add: mult_assoc [symmetric])

   450 qed

   451

   452 lemma nonzero_inverse_minus_eq:

   453   "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"

   454 by (rule inverse_unique) simp

   455

   456 lemma nonzero_inverse_inverse_eq:

   457   "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"

   458 by (rule inverse_unique) simp

   459

   460 lemma nonzero_inverse_eq_imp_eq:

   461   assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"

   462   shows "a = b"

   463 proof -

   464   from inverse a = inverse b

   465   have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)

   466   with a \<noteq> 0 and b \<noteq> 0 show "a = b"

   467     by (simp add: nonzero_inverse_inverse_eq)

   468 qed

   469

   470 lemma inverse_1 [simp]: "inverse 1 = 1"

   471 by (rule inverse_unique) simp

   472

   473 lemma nonzero_inverse_mult_distrib:

   474   assumes "a \<noteq> 0" and "b \<noteq> 0"

   475   shows "inverse (a * b) = inverse b * inverse a"

   476 proof -

   477   have "a * (b * inverse b) * inverse a = 1" using assms by simp

   478   hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)

   479   thus ?thesis by (rule inverse_unique)

   480 qed

   481

   482 lemma division_ring_inverse_add:

   483   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"

   484 by (simp add: algebra_simps)

   485

   486 lemma division_ring_inverse_diff:

   487   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"

   488 by (simp add: algebra_simps)

   489

   490 end

   491

   492 class mult_mono = times + zero + ord +

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

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

   495

   496 text {*

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

   498   \begin{itemize}

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

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

   501   \end{itemize}

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

   503   \begin{itemize}

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

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

   506   \end{itemize}

   507 *}

   508

   509 class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add

   510 begin

   511

   512 lemma mult_mono:

   513   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c

   514      \<Longrightarrow> a * c \<le> b * d"

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

   516 apply (erule mult_left_mono, assumption)

   517 done

   518

   519 lemma mult_mono':

   520   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c

   521      \<Longrightarrow> a * c \<le> b * d"

   522 apply (rule mult_mono)

   523 apply (fast intro: order_trans)+

   524 done

   525

   526 end

   527

   528 class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add

   529   + semiring + cancel_comm_monoid_add

   530 begin

   531

   532 subclass semiring_0_cancel ..

   533 subclass ordered_semiring ..

   534

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

   536 using mult_left_mono [of zero b a] by simp

   537

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

   539 using mult_left_mono [of b zero a] by simp

   540

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

   542 using mult_right_mono [of a zero b] by simp

   543

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

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

   546 by (drule mult_right_mono [of b zero], auto)

   547

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

   549 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   550

   551 end

   552

   553 class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono

   554 begin

   555

   556 subclass ordered_cancel_semiring ..

   557

   558 subclass ordered_comm_monoid_add ..

   559

   560 lemma mult_left_less_imp_less:

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

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

   563

   564 lemma mult_right_less_imp_less:

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

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

   567

   568 end

   569

   570 class linordered_semiring_1 = linordered_semiring + semiring_1

   571

   572 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

   575 begin

   576

   577 subclass semiring_0_cancel ..

   578

   579 subclass linordered_semiring

   580 proof

   581   fix a b c :: 'a

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

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

   584     unfolding le_less

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

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

   587     unfolding le_less

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

   589 qed

   590

   591 lemma mult_left_le_imp_le:

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

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

   594

   595 lemma mult_right_le_imp_le:

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

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

   598

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

   600 using mult_strict_left_mono [of zero b a] by simp

   601

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

   603 using mult_strict_left_mono [of b zero a] by simp

   604

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

   606 using mult_strict_right_mono [of a zero b] by simp

   607

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

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

   610 by (drule mult_strict_right_mono [of b zero], auto)

   611

   612 lemma zero_less_mult_pos:

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

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

   615  apply (auto simp add: le_less not_less)

   616 apply (drule_tac mult_pos_neg [of a b])

   617  apply (auto dest: less_not_sym)

   618 done

   619

   620 lemma zero_less_mult_pos2:

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

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

   623  apply (auto simp add: le_less not_less)

   624 apply (drule_tac mult_pos_neg2 [of a b])

   625  apply (auto dest: less_not_sym)

   626 done

   627

   628 text{*Strict monotonicity in both arguments*}

   629 lemma mult_strict_mono:

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

   631   shows "a * c < b * d"

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

   633   apply (simp add: mult_pos_pos)

   634   apply (erule mult_strict_right_mono [THEN less_trans])

   635   apply (force simp add: le_less)

   636   apply (erule mult_strict_left_mono, assumption)

   637   done

   638

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

   640 lemma mult_strict_mono':

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

   642   shows "a * c < b * d"

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

   644

   645 lemma mult_less_le_imp_less:

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

   647   shows "a * c < b * d"

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

   649   apply (erule less_le_trans)

   650   apply (erule mult_left_mono)

   651   apply simp

   652   apply (erule mult_strict_right_mono)

   653   apply assumption

   654   done

   655

   656 lemma mult_le_less_imp_less:

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

   658   shows "a * c < b * d"

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

   660   apply (erule le_less_trans)

   661   apply (erule mult_strict_left_mono)

   662   apply simp

   663   apply (erule mult_right_mono)

   664   apply simp

   665   done

   666

   667 lemma mult_less_imp_less_left:

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

   669   shows "a < b"

   670 proof (rule ccontr)

   671   assume "\<not>  a < b"

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

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

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

   675 qed

   676

   677 lemma mult_less_imp_less_right:

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

   679   shows "a < b"

   680 proof (rule ccontr)

   681   assume "\<not> a < b"

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

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

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

   685 qed

   686

   687 end

   688

   689 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   690

   691 class mult_mono1 = times + zero + ord +

   692   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"

   693

   694 class ordered_comm_semiring = comm_semiring_0

   695   + ordered_ab_semigroup_add + mult_mono1

   696 begin

   697

   698 subclass ordered_semiring

   699 proof

   700   fix a b c :: 'a

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

   702   thus "c * a \<le> c * b" by (rule mult_mono1)

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

   704 qed

   705

   706 end

   707

   708 class ordered_cancel_comm_semiring = comm_semiring_0_cancel

   709   + ordered_ab_semigroup_add + mult_mono1

   710 begin

   711

   712 subclass ordered_comm_semiring ..

   713 subclass ordered_cancel_semiring ..

   714

   715 end

   716

   717 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

   718   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

   719 begin

   720

   721 subclass linordered_semiring_strict

   722 proof

   723   fix a b c :: 'a

   724   assume "a < b" "0 < c"

   725   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)

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

   727 qed

   728

   729 subclass ordered_cancel_comm_semiring

   730 proof

   731   fix a b c :: 'a

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

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

   734     unfolding le_less

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

   736 qed

   737

   738 end

   739

   740 class ordered_ring = ring + ordered_cancel_semiring

   741 begin

   742

   743 subclass ordered_ab_group_add ..

   744

   745 text{*Legacy - use @{text algebra_simps} *}

   746 lemmas ring_simps[no_atp] = algebra_simps

   747

   748 lemma less_add_iff1:

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

   750 by (simp add: algebra_simps)

   751

   752 lemma less_add_iff2:

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

   754 by (simp add: algebra_simps)

   755

   756 lemma le_add_iff1:

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

   758 by (simp add: algebra_simps)

   759

   760 lemma le_add_iff2:

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

   762 by (simp add: algebra_simps)

   763

   764 lemma mult_left_mono_neg:

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

   766   apply (drule mult_left_mono [of _ _ "uminus c"])

   767   apply simp_all

   768   done

   769

   770 lemma mult_right_mono_neg:

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

   772   apply (drule mult_right_mono [of _ _ "uminus c"])

   773   apply simp_all

   774   done

   775

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

   777 using mult_right_mono_neg [of a zero b] by simp

   778

   779 lemma split_mult_pos_le:

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

   781 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   782

   783 end

   784

   785 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   786 begin

   787

   788 subclass ordered_ring ..

   789

   790 subclass ordered_ab_group_add_abs

   791 proof

   792   fix a b

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

   794     by (auto simp add: abs_if not_less)

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

   796      auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)

   797 qed (auto simp add: abs_if)

   798

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

   800   using linear [of 0 a]

   801   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   802

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

   804   by (simp add: not_less)

   805

   806 end

   807

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

   809    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

   810  *)

   811 class linordered_ring_strict = ring + linordered_semiring_strict

   812   + ordered_ab_group_add + abs_if

   813 begin

   814

   815 subclass linordered_ring ..

   816

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

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

   819

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

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

   822

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

   824 using mult_strict_right_mono_neg [of a zero b] by simp

   825

   826 subclass ring_no_zero_divisors

   827 proof

   828   fix a b

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

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

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

   832   proof (cases "a < 0")

   833     case True note A' = this

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

   835       case True with A'

   836       show ?thesis by (auto dest: mult_neg_neg)

   837     next

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

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

   840     qed

   841   next

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

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

   844       case True with A'

   845       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   846     next

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

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

   849     qed

   850   qed

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

   852 qed

   853

   854 lemma zero_less_mult_iff:

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

   856   apply (auto simp add: mult_pos_pos mult_neg_neg)

   857   apply (simp_all add: not_less le_less)

   858   apply (erule disjE) apply assumption defer

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

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

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

   862   apply (drule sym) apply simp

   863   apply (blast dest: zero_less_mult_pos)

   864   apply (blast dest: zero_less_mult_pos2)

   865   done

   866

   867 lemma zero_le_mult_iff:

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

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

   870

   871 lemma mult_less_0_iff:

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

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

   874   apply force

   875   done

   876

   877 lemma mult_le_0_iff:

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

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

   880   apply force

   881   done

   882

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

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

   885

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

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

   888

   889 lemma mult_less_cancel_right_disj:

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

   891   apply (cases "c = 0")

   892   apply (auto simp add: neq_iff mult_strict_right_mono

   893                       mult_strict_right_mono_neg)

   894   apply (auto simp add: not_less

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

   896                       not_le [symmetric, of a])

   897   apply (erule_tac [!] notE)

   898   apply (auto simp add: less_imp_le mult_right_mono

   899                       mult_right_mono_neg)

   900   done

   901

   902 lemma mult_less_cancel_left_disj:

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

   904   apply (cases "c = 0")

   905   apply (auto simp add: neq_iff mult_strict_left_mono

   906                       mult_strict_left_mono_neg)

   907   apply (auto simp add: not_less

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

   909                       not_le [symmetric, of a])

   910   apply (erule_tac [!] notE)

   911   apply (auto simp add: less_imp_le mult_left_mono

   912                       mult_left_mono_neg)

   913   done

   914

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

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

   917

   918 lemma mult_less_cancel_right:

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

   920   using mult_less_cancel_right_disj [of a c b] by auto

   921

   922 lemma mult_less_cancel_left:

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

   924   using mult_less_cancel_left_disj [of c a b] by auto

   925

   926 lemma mult_le_cancel_right:

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

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

   929

   930 lemma mult_le_cancel_left:

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

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

   933

   934 lemma mult_le_cancel_left_pos:

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

   936 by (auto simp: mult_le_cancel_left)

   937

   938 lemma mult_le_cancel_left_neg:

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

   940 by (auto simp: mult_le_cancel_left)

   941

   942 lemma mult_less_cancel_left_pos:

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

   944 by (auto simp: mult_less_cancel_left)

   945

   946 lemma mult_less_cancel_left_neg:

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

   948 by (auto simp: mult_less_cancel_left)

   949

   950 end

   951

   952 text{*Legacy - use @{text algebra_simps} *}

   953 lemmas ring_simps[no_atp] = algebra_simps

   954

   955 lemmas mult_sign_intros =

   956   mult_nonneg_nonneg mult_nonneg_nonpos

   957   mult_nonpos_nonneg mult_nonpos_nonpos

   958   mult_pos_pos mult_pos_neg

   959   mult_neg_pos mult_neg_neg

   960

   961 class ordered_comm_ring = comm_ring + ordered_comm_semiring

   962 begin

   963

   964 subclass ordered_ring ..

   965 subclass ordered_cancel_comm_semiring ..

   966

   967 end

   968

   969 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

   970   (*previously linordered_semiring*)

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

   972 begin

   973

   974 lemma pos_add_strict:

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

   976   using add_strict_mono [of zero a b c] by simp

   977

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

   979 by (rule zero_less_one [THEN less_imp_le])

   980

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

   982 by (simp add: not_le)

   983

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

   985 by (simp add: not_less)

   986

   987 lemma less_1_mult:

   988   assumes "1 < m" and "1 < n"

   989   shows "1 < m * n"

   990   using assms mult_strict_mono [of 1 m 1 n]

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

   992

   993 end

   994

   995 class linordered_idom = comm_ring_1 +

   996   linordered_comm_semiring_strict + ordered_ab_group_add +

   997   abs_if + sgn_if

   998   (*previously linordered_ring*)

   999 begin

  1000

  1001 subclass linordered_ring_strict ..

  1002 subclass ordered_comm_ring ..

  1003 subclass idom ..

  1004

  1005 subclass linordered_semidom

  1006 proof

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

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

  1009 qed

  1010

  1011 lemma linorder_neqE_linordered_idom:

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

  1013   using assms by (rule neqE)

  1014

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

  1016

  1017 lemma mult_le_cancel_right1:

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

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

  1020

  1021 lemma mult_le_cancel_right2:

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

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

  1024

  1025 lemma mult_le_cancel_left1:

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

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

  1028

  1029 lemma mult_le_cancel_left2:

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

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

  1032

  1033 lemma mult_less_cancel_right1:

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

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

  1036

  1037 lemma mult_less_cancel_right2:

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

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

  1040

  1041 lemma mult_less_cancel_left1:

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

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

  1044

  1045 lemma mult_less_cancel_left2:

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

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

  1048

  1049 lemma sgn_sgn [simp]:

  1050   "sgn (sgn a) = sgn a"

  1051 unfolding sgn_if by simp

  1052

  1053 lemma sgn_0_0:

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

  1055 unfolding sgn_if by simp

  1056

  1057 lemma sgn_1_pos:

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

  1059 unfolding sgn_if by simp

  1060

  1061 lemma sgn_1_neg:

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

  1063 unfolding sgn_if by auto

  1064

  1065 lemma sgn_pos [simp]:

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

  1067 unfolding sgn_1_pos .

  1068

  1069 lemma sgn_neg [simp]:

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

  1071 unfolding sgn_1_neg .

  1072

  1073 lemma sgn_times:

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

  1075 by (auto simp add: sgn_if zero_less_mult_iff)

  1076

  1077 lemma abs_sgn: "abs k = k * sgn k"

  1078 unfolding sgn_if abs_if by auto

  1079

  1080 lemma sgn_greater [simp]:

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

  1082   unfolding sgn_if by auto

  1083

  1084 lemma sgn_less [simp]:

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

  1086   unfolding sgn_if by auto

  1087

  1088 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"

  1089   by (simp add: abs_if)

  1090

  1091 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"

  1092   by (simp add: abs_if)

  1093

  1094 lemma dvd_if_abs_eq:

  1095   "abs l = abs (k) \<Longrightarrow> l dvd k"

  1096 by(subst abs_dvd_iff[symmetric]) simp

  1097

  1098 end

  1099

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

  1101

  1102 lemmas mult_compare_simps[no_atp] =

  1103     mult_le_cancel_right mult_le_cancel_left

  1104     mult_le_cancel_right1 mult_le_cancel_right2

  1105     mult_le_cancel_left1 mult_le_cancel_left2

  1106     mult_less_cancel_right mult_less_cancel_left

  1107     mult_less_cancel_right1 mult_less_cancel_right2

  1108     mult_less_cancel_left1 mult_less_cancel_left2

  1109     mult_cancel_right mult_cancel_left

  1110     mult_cancel_right1 mult_cancel_right2

  1111     mult_cancel_left1 mult_cancel_left2

  1112

  1113 -- {* FIXME continue localization here *}

  1114

  1115 subsection {* Reasoning about inequalities with division *}

  1116

  1117 lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1

  1118     ==> x * y <= x"

  1119 by (auto simp add: mult_le_cancel_left2)

  1120

  1121 lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1

  1122     ==> y * x <= x"

  1123 by (auto simp add: mult_le_cancel_right2)

  1124

  1125 context linordered_semidom

  1126 begin

  1127

  1128 lemma less_add_one: "a < a + 1"

  1129 proof -

  1130   have "a + 0 < a + 1"

  1131     by (blast intro: zero_less_one add_strict_left_mono)

  1132   thus ?thesis by simp

  1133 qed

  1134

  1135 lemma zero_less_two: "0 < 1 + 1"

  1136 by (blast intro: less_trans zero_less_one less_add_one)

  1137

  1138 end

  1139

  1140

  1141 subsection {* Absolute Value *}

  1142

  1143 context linordered_idom

  1144 begin

  1145

  1146 lemma mult_sgn_abs: "sgn x * abs x = x"

  1147   unfolding abs_if sgn_if by auto

  1148

  1149 end

  1150

  1151 lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"

  1152 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])

  1153

  1154 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1155   assumes abs_eq_mult:

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

  1157

  1158 context linordered_idom

  1159 begin

  1160

  1161 subclass ordered_ring_abs proof

  1162 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1163

  1164 lemma abs_mult:

  1165   "abs (a * b) = abs a * abs b"

  1166   by (rule abs_eq_mult) auto

  1167

  1168 lemma abs_mult_self:

  1169   "abs a * abs a = a * a"

  1170   by (simp add: abs_if)

  1171

  1172 end

  1173

  1174 lemma abs_mult_less:

  1175      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"

  1176 proof -

  1177   assume ac: "abs a < c"

  1178   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)

  1179   assume "abs b < d"

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

  1181 qed

  1182

  1183 lemmas eq_minus_self_iff[no_atp] = equal_neg_zero

  1184

  1185 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"

  1186   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..

  1187

  1188 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))"

  1189 apply (simp add: order_less_le abs_le_iff)

  1190 apply (auto simp add: abs_if)

  1191 done

  1192

  1193 lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==>

  1194     (abs y) * x = abs (y * x)"

  1195   apply (subst abs_mult)

  1196   apply simp

  1197 done

  1198

  1199 code_modulename SML

  1200   Rings Arith

  1201

  1202 code_modulename OCaml

  1203   Rings Arith

  1204

  1205 code_modulename Haskell

  1206   Rings Arith

  1207

  1208 end