src/HOL/Rings.thy
 author haftmann Mon Apr 26 11:34:15 2010 +0200 (2010-04-26) changeset 36348 89c54f51f55a parent 36304 6984744e6b34 child 36622 e393a91f86df permissions -rw-r--r--
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
     1 (*  Title:      HOL/Rings.thy

     2     Author:     Gertrud Bauer

     3     Author:     Steven Obua

     4     Author:     Tobias Nipkow

     5     Author:     Lawrence C Paulson

     6     Author:     Markus Wenzel

     7     Author:     Jeremy Avigad

     8 *)

     9

    10 header {* Rings *}

    11

    12 theory Rings

    13 imports Groups

    14 begin

    15

    16 class semiring = ab_semigroup_add + semigroup_mult +

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

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

    19 begin

    20

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

    22 lemma combine_common_factor:

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

    24 by (simp add: left_distrib add_ac)

    25

    26 end

    27

    28 class mult_zero = times + zero +

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

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

    31

    32 class semiring_0 = semiring + comm_monoid_add + mult_zero

    33

    34 class semiring_0_cancel = semiring + cancel_comm_monoid_add

    35 begin

    36

    37 subclass semiring_0

    38 proof

    39   fix a :: 'a

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

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

    42 next

    43   fix a :: 'a

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

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

    46 qed

    47

    48 end

    49

    50 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

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

    52 begin

    53

    54 subclass semiring

    55 proof

    56   fix a b c :: 'a

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

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

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

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

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

    62 qed

    63

    64 end

    65

    66 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    67 begin

    68

    69 subclass semiring_0 ..

    70

    71 end

    72

    73 class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add

    74 begin

    75

    76 subclass semiring_0_cancel ..

    77

    78 subclass comm_semiring_0 ..

    79

    80 end

    81

    82 class zero_neq_one = zero + one +

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

    84 begin

    85

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

    87 by (rule not_sym) (rule zero_neq_one)

    88

    89 end

    90

    91 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

    92

    93 text {* Abstract divisibility *}

    94

    95 class dvd = times

    96 begin

    97

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

    99   [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, field_simps]: "a * (b - c) = a * b - a * c"

   234 by (simp add: right_distrib diff_minus)

   235

   236 lemma left_diff_distrib[algebra_simps, field_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 lemma eq_add_iff1:

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

   244 by (simp add: algebra_simps)

   245

   246 lemma eq_add_iff2:

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

   248 by (simp add: algebra_simps)

   249

   250 end

   251

   252 lemmas ring_distribs[no_atp] =

   253   right_distrib left_distrib left_diff_distrib right_diff_distrib

   254

   255 class comm_ring = comm_semiring + ab_group_add

   256 begin

   257

   258 subclass ring ..

   259 subclass comm_semiring_0_cancel ..

   260

   261 end

   262

   263 class ring_1 = ring + zero_neq_one + monoid_mult

   264 begin

   265

   266 subclass semiring_1_cancel ..

   267

   268 end

   269

   270 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   271   (*previously ring*)

   272 begin

   273

   274 subclass ring_1 ..

   275 subclass comm_semiring_1_cancel ..

   276

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

   278 proof

   279   assume "x dvd - y"

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

   281   then show "x dvd y" by simp

   282 next

   283   assume "x dvd y"

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

   285   then show "x dvd - y" by simp

   286 qed

   287

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

   289 proof

   290   assume "- x dvd y"

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

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

   293   then show "x dvd y" ..

   294 next

   295   assume "x dvd y"

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

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

   298   then show "- x dvd y" ..

   299 qed

   300

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

   302 by (simp only: diff_minus dvd_add dvd_minus_iff)

   303

   304 end

   305

   306 class ring_no_zero_divisors = ring + no_zero_divisors

   307 begin

   308

   309 lemma mult_eq_0_iff [simp]:

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

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

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

   313     then show ?thesis using no_zero_divisors by simp

   314 next

   315   case True then show ?thesis by auto

   316 qed

   317

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

   319 lemma mult_cancel_right [simp, no_atp]:

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

   321 proof -

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

   323     by (simp add: algebra_simps)

   324   thus ?thesis by (simp add: disj_commute)

   325 qed

   326

   327 lemma mult_cancel_left [simp, no_atp]:

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

   329 proof -

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

   331     by (simp add: algebra_simps)

   332   thus ?thesis by simp

   333 qed

   334

   335 end

   336

   337 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   338 begin

   339

   340 lemma mult_cancel_right1 [simp]:

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

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

   343

   344 lemma mult_cancel_right2 [simp]:

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

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

   347

   348 lemma mult_cancel_left1 [simp]:

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

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

   351

   352 lemma mult_cancel_left2 [simp]:

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

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

   355

   356 end

   357

   358 class idom = comm_ring_1 + no_zero_divisors

   359 begin

   360

   361 subclass ring_1_no_zero_divisors ..

   362

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

   364 proof

   365   assume "a * a = b * b"

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

   367     by (simp add: algebra_simps)

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

   369     by (simp add: eq_neg_iff_add_eq_0)

   370 next

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

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

   373 qed

   374

   375 lemma dvd_mult_cancel_right [simp]:

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

   377 proof -

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

   379     unfolding dvd_def by (simp add: mult_ac)

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

   381     unfolding dvd_def by simp

   382   finally show ?thesis .

   383 qed

   384

   385 lemma dvd_mult_cancel_left [simp]:

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

   387 proof -

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

   389     unfolding dvd_def by (simp add: mult_ac)

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

   391     unfolding dvd_def by simp

   392   finally show ?thesis .

   393 qed

   394

   395 end

   396

   397 class inverse =

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

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

   400

   401 class division_ring = ring_1 + inverse +

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

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

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

   405 begin

   406

   407 subclass ring_1_no_zero_divisors

   408 proof

   409   fix a b :: 'a

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

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

   412   proof

   413     assume ab: "a * b = 0"

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

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

   416       by (simp only: mult_assoc)

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

   418     finally show False by simp

   419   qed

   420 qed

   421

   422 lemma nonzero_imp_inverse_nonzero:

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

   424 proof

   425   assume ianz: "inverse a = 0"

   426   assume "a \<noteq> 0"

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

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

   429   finally have "1 = 0" .

   430   thus False by (simp add: eq_commute)

   431 qed

   432

   433 lemma inverse_zero_imp_zero:

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

   435 apply (rule classical)

   436 apply (drule nonzero_imp_inverse_nonzero)

   437 apply auto

   438 done

   439

   440 lemma inverse_unique:

   441   assumes ab: "a * b = 1"

   442   shows "inverse a = b"

   443 proof -

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

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

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

   447 qed

   448

   449 lemma nonzero_inverse_minus_eq:

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

   451 by (rule inverse_unique) simp

   452

   453 lemma nonzero_inverse_inverse_eq:

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

   455 by (rule inverse_unique) simp

   456

   457 lemma nonzero_inverse_eq_imp_eq:

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

   459   shows "a = b"

   460 proof -

   461   from inverse a = inverse b

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

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

   464     by (simp add: nonzero_inverse_inverse_eq)

   465 qed

   466

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

   468 by (rule inverse_unique) simp

   469

   470 lemma nonzero_inverse_mult_distrib:

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

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

   473 proof -

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

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

   476   thus ?thesis by (rule inverse_unique)

   477 qed

   478

   479 lemma division_ring_inverse_add:

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

   481 by (simp add: algebra_simps)

   482

   483 lemma division_ring_inverse_diff:

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

   485 by (simp add: algebra_simps)

   486

   487 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"

   488 proof

   489   assume neq: "b \<noteq> 0"

   490   {

   491     hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)

   492     also assume "a / b = 1"

   493     finally show "a = b" by simp

   494   next

   495     assume "a = b"

   496     with neq show "a / b = 1" by (simp add: divide_inverse)

   497   }

   498 qed

   499

   500 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"

   501 by (simp add: divide_inverse)

   502

   503 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"

   504 by (simp add: divide_inverse)

   505

   506 lemma divide_zero_left [simp]: "0 / a = 0"

   507 by (simp add: divide_inverse)

   508

   509 lemma inverse_eq_divide: "inverse a = 1 / a"

   510 by (simp add: divide_inverse)

   511

   512 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"

   513 by (simp add: divide_inverse algebra_simps)

   514

   515 lemma divide_1 [simp]: "a / 1 = a"

   516   by (simp add: divide_inverse)

   517

   518 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"

   519   by (simp add: divide_inverse mult_assoc)

   520

   521 lemma minus_divide_left: "- (a / b) = (-a) / b"

   522   by (simp add: divide_inverse)

   523

   524 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"

   525   by (simp add: divide_inverse nonzero_inverse_minus_eq)

   526

   527 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"

   528   by (simp add: divide_inverse nonzero_inverse_minus_eq)

   529

   530 lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"

   531   by (simp add: divide_inverse)

   532

   533 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"

   534   by (simp add: diff_minus add_divide_distrib)

   535

   536 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"

   537 proof -

   538   assume [simp]: "c \<noteq> 0"

   539   have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp

   540   also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)

   541   finally show ?thesis .

   542 qed

   543

   544 lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"

   545 proof -

   546   assume [simp]: "c \<noteq> 0"

   547   have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp

   548   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)

   549   finally show ?thesis .

   550 qed

   551

   552 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"

   553   by (simp add: divide_inverse mult_assoc)

   554

   555 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"

   556   by (drule sym) (simp add: divide_inverse mult_assoc)

   557

   558 end

   559

   560 class division_ring_inverse_zero = division_ring +

   561   assumes inverse_zero [simp]: "inverse 0 = 0"

   562 begin

   563

   564 lemma divide_zero [simp]:

   565   "a / 0 = 0"

   566   by (simp add: divide_inverse)

   567

   568 lemma divide_self_if [simp]:

   569   "a / a = (if a = 0 then 0 else 1)"

   570   by simp

   571

   572 lemma inverse_nonzero_iff_nonzero [simp]:

   573   "inverse a = 0 \<longleftrightarrow> a = 0"

   574   by rule (fact inverse_zero_imp_zero, simp)

   575

   576 lemma inverse_minus_eq [simp]:

   577   "inverse (- a) = - inverse a"

   578 proof cases

   579   assume "a=0" thus ?thesis by simp

   580 next

   581   assume "a\<noteq>0"

   582   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   583 qed

   584

   585 lemma inverse_eq_imp_eq:

   586   "inverse a = inverse b \<Longrightarrow> a = b"

   587 apply (cases "a=0 | b=0")

   588  apply (force dest!: inverse_zero_imp_zero

   589               simp add: eq_commute [of "0::'a"])

   590 apply (force dest!: nonzero_inverse_eq_imp_eq)

   591 done

   592

   593 lemma inverse_eq_iff_eq [simp]:

   594   "inverse a = inverse b \<longleftrightarrow> a = b"

   595   by (force dest!: inverse_eq_imp_eq)

   596

   597 lemma inverse_inverse_eq [simp]:

   598   "inverse (inverse a) = a"

   599 proof cases

   600   assume "a=0" thus ?thesis by simp

   601 next

   602   assume "a\<noteq>0"

   603   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

   604 qed

   605

   606 end

   607

   608 class mult_mono = times + zero + ord +

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

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

   611

   612 text {*

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

   614   \begin{itemize}

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

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

   617   \end{itemize}

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

   619   \begin{itemize}

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

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

   622   \end{itemize}

   623 *}

   624

   625 class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add

   626 begin

   627

   628 lemma mult_mono:

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

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

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

   632 apply (erule mult_left_mono, assumption)

   633 done

   634

   635 lemma mult_mono':

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

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

   638 apply (rule mult_mono)

   639 apply (fast intro: order_trans)+

   640 done

   641

   642 end

   643

   644 class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add

   645   + semiring + cancel_comm_monoid_add

   646 begin

   647

   648 subclass semiring_0_cancel ..

   649 subclass ordered_semiring ..

   650

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

   652 using mult_left_mono [of 0 b a] by simp

   653

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

   655 using mult_left_mono [of b 0 a] by simp

   656

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

   658 using mult_right_mono [of a 0 b] by simp

   659

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

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

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

   663

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

   665 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   666

   667 end

   668

   669 class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono

   670 begin

   671

   672 subclass ordered_cancel_semiring ..

   673

   674 subclass ordered_comm_monoid_add ..

   675

   676 lemma mult_left_less_imp_less:

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

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

   679

   680 lemma mult_right_less_imp_less:

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

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

   683

   684 end

   685

   686 class linordered_semiring_1 = linordered_semiring + semiring_1

   687

   688 class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +

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

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

   691 begin

   692

   693 subclass semiring_0_cancel ..

   694

   695 subclass linordered_semiring

   696 proof

   697   fix a b c :: 'a

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

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

   700     unfolding le_less

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

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

   703     unfolding le_less

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

   705 qed

   706

   707 lemma mult_left_le_imp_le:

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

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

   710

   711 lemma mult_right_le_imp_le:

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

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

   714

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

   716 using mult_strict_left_mono [of 0 b a] by simp

   717

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

   719 using mult_strict_left_mono [of b 0 a] by simp

   720

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

   722 using mult_strict_right_mono [of a 0 b] by simp

   723

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

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

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

   727

   728 lemma zero_less_mult_pos:

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

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

   731  apply (auto simp add: le_less not_less)

   732 apply (drule_tac mult_pos_neg [of a b])

   733  apply (auto dest: less_not_sym)

   734 done

   735

   736 lemma zero_less_mult_pos2:

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

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

   739  apply (auto simp add: le_less not_less)

   740 apply (drule_tac mult_pos_neg2 [of a b])

   741  apply (auto dest: less_not_sym)

   742 done

   743

   744 text{*Strict monotonicity in both arguments*}

   745 lemma mult_strict_mono:

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

   747   shows "a * c < b * d"

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

   749   apply (simp add: mult_pos_pos)

   750   apply (erule mult_strict_right_mono [THEN less_trans])

   751   apply (force simp add: le_less)

   752   apply (erule mult_strict_left_mono, assumption)

   753   done

   754

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

   756 lemma mult_strict_mono':

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

   758   shows "a * c < b * d"

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

   760

   761 lemma mult_less_le_imp_less:

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

   763   shows "a * c < b * d"

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

   765   apply (erule less_le_trans)

   766   apply (erule mult_left_mono)

   767   apply simp

   768   apply (erule mult_strict_right_mono)

   769   apply assumption

   770   done

   771

   772 lemma mult_le_less_imp_less:

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

   774   shows "a * c < b * d"

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

   776   apply (erule le_less_trans)

   777   apply (erule mult_strict_left_mono)

   778   apply simp

   779   apply (erule mult_right_mono)

   780   apply simp

   781   done

   782

   783 lemma mult_less_imp_less_left:

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

   785   shows "a < b"

   786 proof (rule ccontr)

   787   assume "\<not>  a < b"

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

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

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

   791 qed

   792

   793 lemma mult_less_imp_less_right:

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

   795   shows "a < b"

   796 proof (rule ccontr)

   797   assume "\<not> a < b"

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

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

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

   801 qed

   802

   803 end

   804

   805 class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1

   806

   807 class mult_mono1 = times + zero + ord +

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

   809

   810 class ordered_comm_semiring = comm_semiring_0

   811   + ordered_ab_semigroup_add + mult_mono1

   812 begin

   813

   814 subclass ordered_semiring

   815 proof

   816   fix a b c :: 'a

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

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

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

   820 qed

   821

   822 end

   823

   824 class ordered_cancel_comm_semiring = comm_semiring_0_cancel

   825   + ordered_ab_semigroup_add + mult_mono1

   826 begin

   827

   828 subclass ordered_comm_semiring ..

   829 subclass ordered_cancel_semiring ..

   830

   831 end

   832

   833 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +

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

   835 begin

   836

   837 subclass linordered_semiring_strict

   838 proof

   839   fix a b c :: 'a

   840   assume "a < b" "0 < c"

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

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

   843 qed

   844

   845 subclass ordered_cancel_comm_semiring

   846 proof

   847   fix a b c :: 'a

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

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

   850     unfolding le_less

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

   852 qed

   853

   854 end

   855

   856 class ordered_ring = ring + ordered_cancel_semiring

   857 begin

   858

   859 subclass ordered_ab_group_add ..

   860

   861 lemma less_add_iff1:

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

   863 by (simp add: algebra_simps)

   864

   865 lemma less_add_iff2:

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

   867 by (simp add: algebra_simps)

   868

   869 lemma le_add_iff1:

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

   871 by (simp add: algebra_simps)

   872

   873 lemma le_add_iff2:

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

   875 by (simp add: algebra_simps)

   876

   877 lemma mult_left_mono_neg:

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

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

   880   apply simp_all

   881   done

   882

   883 lemma mult_right_mono_neg:

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

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

   886   apply simp_all

   887   done

   888

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

   890 using mult_right_mono_neg [of a 0 b] by simp

   891

   892 lemma split_mult_pos_le:

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

   894 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   895

   896 end

   897

   898 class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if

   899 begin

   900

   901 subclass ordered_ring ..

   902

   903 subclass ordered_ab_group_add_abs

   904 proof

   905   fix a b

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

   907     by (auto simp add: abs_if not_less)

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

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

   910 qed (auto simp add: abs_if)

   911

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

   913   using linear [of 0 a]

   914   by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   915

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

   917   by (simp add: not_less)

   918

   919 end

   920

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

   922    Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.

   923  *)

   924 class linordered_ring_strict = ring + linordered_semiring_strict

   925   + ordered_ab_group_add + abs_if

   926 begin

   927

   928 subclass linordered_ring ..

   929

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

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

   932

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

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

   935

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

   937 using mult_strict_right_mono_neg [of a 0 b] by simp

   938

   939 subclass ring_no_zero_divisors

   940 proof

   941   fix a b

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

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

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

   945   proof (cases "a < 0")

   946     case True note A' = this

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

   948       case True with A'

   949       show ?thesis by (auto dest: mult_neg_neg)

   950     next

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

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

   953     qed

   954   next

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

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

   957       case True with A'

   958       show ?thesis by (auto dest: mult_strict_right_mono_neg)

   959     next

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

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

   962     qed

   963   qed

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

   965 qed

   966

   967 lemma zero_less_mult_iff:

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

   969   apply (auto simp add: mult_pos_pos mult_neg_neg)

   970   apply (simp_all add: not_less le_less)

   971   apply (erule disjE) apply assumption defer

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

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

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

   975   apply (drule sym) apply simp

   976   apply (blast dest: zero_less_mult_pos)

   977   apply (blast dest: zero_less_mult_pos2)

   978   done

   979

   980 lemma zero_le_mult_iff:

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

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

   983

   984 lemma mult_less_0_iff:

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

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

   987   apply force

   988   done

   989

   990 lemma mult_le_0_iff:

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

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

   993   apply force

   994   done

   995

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

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

   998

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

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

  1001

  1002 lemma mult_less_cancel_right_disj:

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

  1004   apply (cases "c = 0")

  1005   apply (auto simp add: neq_iff mult_strict_right_mono

  1006                       mult_strict_right_mono_neg)

  1007   apply (auto simp add: not_less

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

  1009                       not_le [symmetric, of a])

  1010   apply (erule_tac [!] notE)

  1011   apply (auto simp add: less_imp_le mult_right_mono

  1012                       mult_right_mono_neg)

  1013   done

  1014

  1015 lemma mult_less_cancel_left_disj:

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

  1017   apply (cases "c = 0")

  1018   apply (auto simp add: neq_iff mult_strict_left_mono

  1019                       mult_strict_left_mono_neg)

  1020   apply (auto simp add: not_less

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

  1022                       not_le [symmetric, of a])

  1023   apply (erule_tac [!] notE)

  1024   apply (auto simp add: less_imp_le mult_left_mono

  1025                       mult_left_mono_neg)

  1026   done

  1027

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

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

  1030

  1031 lemma mult_less_cancel_right:

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

  1033   using mult_less_cancel_right_disj [of a c b] by auto

  1034

  1035 lemma mult_less_cancel_left:

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

  1037   using mult_less_cancel_left_disj [of c a b] by auto

  1038

  1039 lemma mult_le_cancel_right:

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

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

  1042

  1043 lemma mult_le_cancel_left:

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

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

  1046

  1047 lemma mult_le_cancel_left_pos:

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

  1049 by (auto simp: mult_le_cancel_left)

  1050

  1051 lemma mult_le_cancel_left_neg:

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

  1053 by (auto simp: mult_le_cancel_left)

  1054

  1055 lemma mult_less_cancel_left_pos:

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

  1057 by (auto simp: mult_less_cancel_left)

  1058

  1059 lemma mult_less_cancel_left_neg:

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

  1061 by (auto simp: mult_less_cancel_left)

  1062

  1063 end

  1064

  1065 lemmas mult_sign_intros =

  1066   mult_nonneg_nonneg mult_nonneg_nonpos

  1067   mult_nonpos_nonneg mult_nonpos_nonpos

  1068   mult_pos_pos mult_pos_neg

  1069   mult_neg_pos mult_neg_neg

  1070

  1071 class ordered_comm_ring = comm_ring + ordered_comm_semiring

  1072 begin

  1073

  1074 subclass ordered_ring ..

  1075 subclass ordered_cancel_comm_semiring ..

  1076

  1077 end

  1078

  1079 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +

  1080   (*previously linordered_semiring*)

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

  1082 begin

  1083

  1084 lemma pos_add_strict:

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

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

  1087

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

  1089 by (rule zero_less_one [THEN less_imp_le])

  1090

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

  1092 by (simp add: not_le)

  1093

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

  1095 by (simp add: not_less)

  1096

  1097 lemma less_1_mult:

  1098   assumes "1 < m" and "1 < n"

  1099   shows "1 < m * n"

  1100   using assms mult_strict_mono [of 1 m 1 n]

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

  1102

  1103 end

  1104

  1105 class linordered_idom = comm_ring_1 +

  1106   linordered_comm_semiring_strict + ordered_ab_group_add +

  1107   abs_if + sgn_if

  1108   (*previously linordered_ring*)

  1109 begin

  1110

  1111 subclass linordered_ring_strict ..

  1112 subclass ordered_comm_ring ..

  1113 subclass idom ..

  1114

  1115 subclass linordered_semidom

  1116 proof

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

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

  1119 qed

  1120

  1121 lemma linorder_neqE_linordered_idom:

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

  1123   using assms by (rule neqE)

  1124

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

  1126

  1127 lemma mult_le_cancel_right1:

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

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

  1130

  1131 lemma mult_le_cancel_right2:

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

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

  1134

  1135 lemma mult_le_cancel_left1:

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

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

  1138

  1139 lemma mult_le_cancel_left2:

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

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

  1142

  1143 lemma mult_less_cancel_right1:

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

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

  1146

  1147 lemma mult_less_cancel_right2:

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

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

  1150

  1151 lemma mult_less_cancel_left1:

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

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

  1154

  1155 lemma mult_less_cancel_left2:

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

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

  1158

  1159 lemma sgn_sgn [simp]:

  1160   "sgn (sgn a) = sgn a"

  1161 unfolding sgn_if by simp

  1162

  1163 lemma sgn_0_0:

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

  1165 unfolding sgn_if by simp

  1166

  1167 lemma sgn_1_pos:

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

  1169 unfolding sgn_if by simp

  1170

  1171 lemma sgn_1_neg:

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

  1173 unfolding sgn_if by auto

  1174

  1175 lemma sgn_pos [simp]:

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

  1177 unfolding sgn_1_pos .

  1178

  1179 lemma sgn_neg [simp]:

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

  1181 unfolding sgn_1_neg .

  1182

  1183 lemma sgn_times:

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

  1185 by (auto simp add: sgn_if zero_less_mult_iff)

  1186

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

  1188 unfolding sgn_if abs_if by auto

  1189

  1190 lemma sgn_greater [simp]:

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

  1192   unfolding sgn_if by auto

  1193

  1194 lemma sgn_less [simp]:

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

  1196   unfolding sgn_if by auto

  1197

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

  1199   by (simp add: abs_if)

  1200

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

  1202   by (simp add: abs_if)

  1203

  1204 lemma dvd_if_abs_eq:

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

  1206 by(subst abs_dvd_iff[symmetric]) simp

  1207

  1208 end

  1209

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

  1211

  1212 lemmas mult_compare_simps[no_atp] =

  1213     mult_le_cancel_right mult_le_cancel_left

  1214     mult_le_cancel_right1 mult_le_cancel_right2

  1215     mult_le_cancel_left1 mult_le_cancel_left2

  1216     mult_less_cancel_right mult_less_cancel_left

  1217     mult_less_cancel_right1 mult_less_cancel_right2

  1218     mult_less_cancel_left1 mult_less_cancel_left2

  1219     mult_cancel_right mult_cancel_left

  1220     mult_cancel_right1 mult_cancel_right2

  1221     mult_cancel_left1 mult_cancel_left2

  1222

  1223 text {* Reasoning about inequalities with division *}

  1224

  1225 context linordered_semidom

  1226 begin

  1227

  1228 lemma less_add_one: "a < a + 1"

  1229 proof -

  1230   have "a + 0 < a + 1"

  1231     by (blast intro: zero_less_one add_strict_left_mono)

  1232   thus ?thesis by simp

  1233 qed

  1234

  1235 lemma zero_less_two: "0 < 1 + 1"

  1236 by (blast intro: less_trans zero_less_one less_add_one)

  1237

  1238 end

  1239

  1240 context linordered_idom

  1241 begin

  1242

  1243 lemma mult_right_le_one_le:

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

  1245   by (auto simp add: mult_le_cancel_left2)

  1246

  1247 lemma mult_left_le_one_le:

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

  1249   by (auto simp add: mult_le_cancel_right2)

  1250

  1251 end

  1252

  1253 text {* Absolute Value *}

  1254

  1255 context linordered_idom

  1256 begin

  1257

  1258 lemma mult_sgn_abs:

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

  1260   unfolding abs_if sgn_if by auto

  1261

  1262 lemma abs_one [simp]:

  1263   "\<bar>1\<bar> = 1"

  1264   by (simp add: abs_if zero_less_one [THEN less_not_sym])

  1265

  1266 end

  1267

  1268 class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +

  1269   assumes abs_eq_mult:

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

  1271

  1272 context linordered_idom

  1273 begin

  1274

  1275 subclass ordered_ring_abs proof

  1276 qed (auto simp add: abs_if not_less mult_less_0_iff)

  1277

  1278 lemma abs_mult:

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

  1280   by (rule abs_eq_mult) auto

  1281

  1282 lemma abs_mult_self:

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

  1284   by (simp add: abs_if)

  1285

  1286 lemma abs_mult_less:

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

  1288 proof -

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

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

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

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

  1293 qed

  1294

  1295 lemma less_minus_self_iff:

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

  1297   by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)

  1298

  1299 lemma abs_less_iff:

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

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

  1302

  1303 lemma abs_mult_pos:

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

  1305   by (simp add: abs_mult)

  1306

  1307 end

  1308

  1309 code_modulename SML

  1310   Rings Arith

  1311

  1312 code_modulename OCaml

  1313   Rings Arith

  1314

  1315 code_modulename Haskell

  1316   Rings Arith

  1317

  1318 end